#13149: Giving Backpack a Promotion -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: task | Status: new Priority: normal | Milestone: Research Component: Compiler (Type | needed checker) | Version: 8.1 Resolution: | Keywords: backpack Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- @@ -13,6 +13,20 @@ - 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. + With promotion, this is not true: + + {{{ + {-# LANGUAGE TypeFamilies #-} + {-# LANGUAGE Rank2Types #-} + {-# LANGUAGE TypeInType #-} + unit p where + signature A where + import GHC.Types + type family F a where + F Bool = Type + module B where + import A + foo :: forall (a :: F Bool). a -> a + foo x = x + unit q where + dependency p[A=<A>] + module C where + import B + }}} New description: This ticket is tracking assumptions the current implementation of Backpack makes about terms and types, which may be violated when more and more term-level things start being lifted into the type level. I don't expect any work to be done on this in the near future, but I'd like to keep track of these breadcrumbs. * 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. With promotion, this is not true: {{{ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE Rank2Types #-} {-# LANGUAGE TypeInType #-} unit p where signature A where import GHC.Types type family F a where F Bool = Type module B where import A foo :: forall (a :: F Bool). a -> a foo x = x unit q where dependency p[A=<A>] module C where import B }}} * (Put more problems here) -- Comment (by ezyang): Thanks! It was an easy matter to turn it into a Backpack failure; I've added it to the ticket. -- Ticket URL: GHC The Glasgow Haskell Compiler