Changes between Initial Version and Version 2 of Ticket #13149


Ignore:
Timestamp:
Jan 19, 2017 4:49:29 AM (20 months ago)
Author:
ezyang
Comment:

Thanks! It was an easy matter to turn it into a Backpack failure; I've added it to the ticket.

Legend:

Unmodified
Added
Removed
Modified
  • Ticket #13149 – Description

    initial v2  
    33* We currently assume that it is impossible for a typechecked-only module (that is, one with no Core unfoldings) to refer to a DFun or a coercion axiom. In the absence of promotion, I'm pretty sure this is the case, since there is no way to refer to a term from a type (DFun), and coercions do not ordinarily occur at the type level.
    44
    5   With promotion, the situation is murkier.  If I understand correctly, `CoercionTy` embeds coercions in types, so in principle it should be possible to end up with a type that refers to a coercion explicitly, when you promote a GADT.  However, I haven't tried too hard to find an example source program where this happens. goldfire, perhaps you would know? I can probably turn it into a panic with GHC HEAD.
     5  With promotion, this is not true:
     6
     7{{{
     8{-# LANGUAGE TypeFamilies #-}
     9{-# LANGUAGE Rank2Types #-}
     10{-# LANGUAGE TypeInType #-}
     11unit p where
     12    signature A where
     13        import GHC.Types
     14        type family F a where
     15          F Bool = Type
     16    module B where
     17        import A
     18        foo :: forall (a :: F Bool). a -> a
     19        foo x = x
     20unit q where
     21    dependency p[A=<A>]
     22    module C where
     23        import B
     24}}}
    625
    726* (Put more problems here)