Can't unsafeCoerce a GADT with a coercion

[TristanAllwood]

type family Blah a 
type instance Blah Int = Int
data E where
  E :: (Blah a ~ Int) => a -> E

*Example Unsafe.Coerce GHC.Prim> (unsafeCoerce E) :: Any

<interactive>:1:15:
    Couldn't match type `Blah a0' with `Int'
    In the first argument of `unsafeCoerce', namely `E'
    In the expression: (unsafeCoerce E) :: Any
    In an equation for `it': it = (unsafeCoerce E) :: Any

This also doesn't work with less dangerous operators, like seq:

*Example Unsafe.Coerce GHC.Prim> (id E) `seq` ()

<interactive>:1:5:
    Couldn't match type `Blah a0' with `Int'
    In the first argument of `id', namely `E'
    In the first argument of `seq', namely `(id E)'
    In the expression: (id E) `seq` ()

[diatchki]

This is not a bug, GHC is working as expected.

The constructor E has a polymorphic type, which is automatically instantiated when you use it. This means that every use of E will be at a monomorphic type of the form a0 -> E for some type a0 and, one the side, GHC has to check that Blah a0 ~ Int.

In these examples there is no reason to believe that Blah a0 is Int, which is what the type error says. You could fix this by specifying the instantiation type explicitly. For example, unsafeCoerce (E :: Int -> E) will probably type-check (although it will probably crash if you tried to use it).