Note [Implementing unsafeCoerce]

The implementation of unsafeCoerce is surprisingly subtle.
This Note describes the moving parts.  You will find more
background in MR !1869 and ticket #16893.

The key challenge is this.  Suppose we have
   case sameTypeRep t1 t2 of
      False -> blah2
      True  -> ...(case (x |> UnsafeCo @t1 @t2) of { K -> blah })...

The programmer thinks that the unsafeCoerce from 't1' to 't2' is safe,
because it is justified by a runtime test (sameTypeRep t1 t2).
It used to compile to a cast, with a magical 'UnsafeCo' coercion.

But alas, if `x` is known to be evaluated, nothing then stops GHC floating that
call to unsafeCoerce outwards so we get
   case (x |> UnsafeCo @t1 @t2) of
     K -> case sameTypeRep t1 t2 of
             False -> blah2
             True  -> ...blah...

and this is utterly wrong, because the unsafeCoerce is being performed
before the dynamic test. This is exactly the setup in #16893 (search for
"Diagnosis").

The solution is this:

* In the library GHC.Internal.Unsafe.Coerce we define:

     unsafeEqualityProof :: forall k (a :: k) (b :: k).
                            UnsafeEquality a b

* It uses a GADT, Unsafe.Coerce.UnsafeEquality, that is exactly like :~:

    data UnsafeEquality (a :: k) (b :: k) where
      UnsafeRefl :: UnsafeEquality a a

* We can now define GHC.Internal.Unsafe.Coerce.unsafeCoerce very simply:

   unsafeCoerce :: forall (a :: Type) (b :: Type) . a -> b
   unsafeCoerce x = case unsafeEqualityProof @a @b of
                      UnsafeRefl -> x

  There is nothing special about unsafeCoerce; it is an
  ordinary library definition, and can be freely inlined.

Now our bad case can't happen.  We'll have
     case unsafeEqualityProof @t1 @t2 of
        UnsafeRefl (co :: t1 ~ t2) -> ....(x |> co)....

and the (x |> co) mentions the evidence 'co', which prevents it
floating. See also wrinkle (U11) below.

While unsafeCoerce is a perfectly ordinary function that needs no
special treatment, GHC.Internal.Unsafe.Coerce.unsafeEqualityProof is magical, in
several ways

(U1) unsafeEqualityProof is /never/ inlined.

(U2) In CoreToStg.coreToStgExpr, we transform
       case unsafeEqualityProof of UnsafeRefl g -> blah
      ==>
       blah

     This eliminates the overhead of evaluating the unsafe equality proof.
     (It follows that the Case is trivial iff `blah` is.)

     Any /other/ occurrence of unsafeEqualityProof is left alone.
     For example you could write
         f :: UnsafeEquality a b -> blah
         f eq_proof = case eq_proof of UnsafeRefl -> ...
    (Nothing special about that.)  In a call, you might write
         f unsafeEqualityProof

    and we'll generate code simply by passing the top-level
    unsafeEqualityProof to f.  As (U5) says, it is implemented as
    UnsafeRefl so all is good.

    NB: Don't discard the case if the case-binder is used
           case unsafeEqualityProof of wild_xx { UnsafeRefl ->
           ...wild_xx...
        That rarely happens, but see #18227.

(U3) In GHC.CoreToStg.Prep.cpeRhsE, if we see
       let x = case unsafeEqualityProof ... of
                 UnsafeRefl -> K e
       in ...

     there is a danger that we'll go to
        let x = case unsafeEqualityProof ... of
                  UnsafeRefl -> let a = e in K a
        in ...

     and produce a thunk even after discarding the unsafeEqualityProof.
     So instead we float out the case to give
        case unsafeEqualityProof ... of { UnsafeRefl ->
        let a = e
            x = K a
        in ...  }
     NB: Floating the case is OK here, even though it broadens the scope,
     because we are done with simplification and won't float out of
     branching Case alternatives such as in the `sameTypeRep` example above.

     Neglecting this transformation triggered test failures in GHCi debugger
     test cases such as `print003`, because it could no longer identify things
     such as `x` above as a value.

(U4) `case unsafeEqualityProof of UnsafeRefl -> rhs` as trivial iff `rhs` is,
     see `exprIsTrivial`. One reason is that we want to treat the RHS
     of unsafeCoerce as very small; see Note [Inline unsafeCoerce] in
     GHC.Core.Unfold.
     Another reason is
       f (case unsafeEqualitProof ... of UnsafeRefl co -> x |> co))
     we do not want to ANF-ise to
        let arg = case unsafeEqualitProof ... of UnsafeRefl co -> x |> co
        in f arg
     because that `let` will turn into a silly indirection `let arg = x in ..`
     in CoreToStg. Triviality means we can "look through" the Case in CoreToStg.

(U5) The definition of unsafeEqualityProof in GHC.Internal.Unsafe.Coerce
     looks very strange:
        unsafeEqualityProof = case unsafeEqualityProof @a @b of
                                 UnsafeRefl -> UnsafeRefl

     It looks recursive!  But the above-mentioned CoreToStg
     transform will change it to
        unsafeEqualityProof = UnsafeRefl
     And that is exactly the code we want!  For example, if we say
        f unsafeEqualityProof
     we want to pass an UnsafeRefl constructor to f.

     We turn off strictness analysis in this module, otherwise
     the strictness analyser will mark unsafeEqualityProof as
     bottom, which is utterly wrong.

(U6) The UnsafeEquality data type is also special in one way.
     Consider this piece of Core
        case unsafeEqualityProof @Int @Bool of
           UnsafeRefl (g :: Int ~# Bool) -> ...g...

     The simplifier normally eliminates case alternatives with
     contradicatory GADT data constructors; here we bring into
     scope evidence (g :: Int~Bool).  But we do not want to
     eliminate this particular alternative!  So we put a special
     case into DataCon.dataConCannotMatch to account for this.

(U7) We add a built-in RULE
       unsafeEqualityProof k t t  ==>  UnsafeRefl (Refl t)
     to simplify the case when the two types are equal.

(U8) The is a super-magic RULE in GHC.base
         map coerce = coerce
     (see Note [Getting the map/coerce RULE to work] in GHC.Core.SimpleOpt)
     But it's all about turning coerce into a cast, and unsafeCoerce
     no longer does that.  So we need a separate map/unsafeCoerce
     RULE, in this module.

     Adding these RULES means we must delay inlining unsafeCoerce
     until the RULES have had a chance to fire; hence the INLINE[1]
     pragma on unsafeCoerce.  (Side note: this has the coincidental
     benefit of making the unsafeCoerce-based version of the `reflection`
     library work -- see #21575.)

There are yet more wrinkles

(U9) unsafeCoerce works only over types of kind `Type`.
     But what about other types?  In GHC.Internal.Unsafe.Coerce we also define

      unsafeCoerceUnlifted :: forall (a :: TYPE UnliftedRep)
                                     (b :: TYPE UnliftedRep).
                              a -> b
      unsafeCoerceUnlifted x
        = case unsafeEqualityProof @a @b of
              UnsafeRefl -> x

     and similarly for unsafeCoerceAddr, unsafeCoerceInt, etc.

(U10) We also want a representation-polymorphic unsafeCoerce#:

       unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                        (a :: TYPE r1) (b :: TYPE r2).
                        a -> b

      This is even more dangerous, because it converts between two types
      *with different runtime representations*!!  Our goal is to deprecate
      it entirely.  But for now we want it.

      But having it is hard!  It is defined by a kind of stub in Unsafe.Coerce,
      and overwritten by the desugarer.  See Note [Wiring in unsafeCoerce#]
      in Desugar.  Here's the code for it
        unsafeCoerce# x = case unsafeEqualityProof @r1 @r2 of UnsafeRefl ->
                          case unsafeEqualityProof @a  @b  of UnsafeRefl ->
                          x
      Notice that we can define this kind-/heterogeneous/ function by calling
      the kind-/homogeneous/ unsafeEqualityProof twice.

      See Note [Wiring in unsafeCoerce#] in Desugar.

(U11) But what stops the whole (case unsafeEqualityProof of ...) from
      being speculated out of a conditional? (E.g., strict float out.)
      Answer: we never float a case on something that is not an HNF
      ('exprIsHNF') outside a conditional.
      See Note [Floating single-alternative cases].

(U12) In #20143 we found
         case unsafeEqualityProof @t1 @t2 of UnsafeRefl cv[dead] -> blah
      where 'blah' didn't mention 'cv'.  We'd like to discard this
      redundant use of unsafeEqualityProof, via GHC.Core.Opt.Simplify.rebuildCase.
      To do this we need to know
        (a) that cv is unused (done by OccAnal), and
        (b) that unsafeEqualityProof terminates rapidly without side effects.
      At the moment we check that explicitly in GHC.Core.Utils.exprOkToDiscard,
      but one might imagine a more systematic check in future.