Note [Wiring in unsafeCoerce#]
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
- Patching magic definitions GHC.HsToCore
- Always expose compulsory unfoldings GHC.Iface.Tidy
Referenced by 3
- GHC.HsToCore call site
- Representation-polymorphism checking built-ins GHC.Tc.Utils.Concrete
- GHC.Tc.Utils.Concrete call site