[GHC] #13149: Giving Backpack a Promotion

[GHC]

#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: <http://ghc.haskell.org/trac/ghc/ticket/13149#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler