#13149: Giving Backpack a Promotion -------------------------------------+------------------------------------- Reporter: ezyang | Owner: Type: task | Status: new Priority: normal | Milestone: Research needed Component: Compiler | Version: 8.1 (Type checker) | Keywords: backpack | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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, 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. * (Put more problems here) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13149 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler