Note [Wiring in unsafeCoerce#]

GHC/HsToCore.hs:643 compiler

We want (Haskell)

  unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                          (a :: TYPE r1) (b :: TYPE r2).
                   a -> b
  unsafeCoerce# x = case unsafeEqualityProof @r1 @r2 of
    UnsafeRefl -> case unsafeEqualityProof @a @b of
      UnsafeRefl -> x

or (Core)

  unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                          (a :: TYPE r1) (b :: TYPE r2).
                   a -> b
  unsafeCoerce# = \ @r1 @r2 @a @b (x :: a).
    case unsafeEqualityProof @RuntimeRep @r1 @r2 of
      UnsafeRefl (co1 :: r1 ~# r2) ->
        case unsafeEqualityProof @(TYPE r2) @(a |> TYPE co1) @b of
          UnsafeRefl (co2 :: (a |> TYPE co1) ~# b) ->
            (x |> (GRefl :: a ~# (a |> TYPE co1)) ; co2)

It looks like we can write this in Haskell directly, but we can't:
the representation polymorphism checks defeat us. Note that `x` is a
representation-polymorphic variable. So we must wire it in with a
compulsory unfolding, like other representation-polymorphic primops.

The challenge is that UnsafeEquality is a GADT, and wiring in a GADT
is *hard*: it has a worker separate from its wrapper, with all manner
of complications. (Simon and Richard tried to do this. We nearly wept.)

The solution is documented in Note [Patching magic definitions]. We now
simply look up the UnsafeEquality GADT in the environment, leaving us
only to wire in unsafeCoerce# directly.

Wrinkle: see Note [Always expose compulsory unfoldings] in GHC.Iface.Tidy

References 2

Referenced by 3