Opened 6 years ago

Closed 6 years ago

#5015 closed bug (invalid)

Can't unsafeCoerce a GADT with a coercion

Reported by: TristanAllwood Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.0.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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

    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` ()

    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` ()

Change History (2)

comment:1 Changed 6 years ago by 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).

comment:2 Changed 6 years ago by simonpj

Resolution: invalid
Status: newclosed
Note: See TracTickets for help on using tickets.