[GHC] #13149: Giving Backpack a Promotion

[GHC]

#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