[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:                    |
-------------------------------------+-------------------------------------
Description changed by ezyang:

@@ -34,0 +34,8 @@
+    This will fail in a puzzling way:
+
+ {{{
+ <no location info>: error:
+     The identifier D:R:F does not exist in the signature for <A>
+     (Try adding it to the export list in that hsig file.)
+ }}}
+

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
 }}}

    This will fail in a puzzling way:

 {{{
 <no location info>: error:
     The identifier D:R:F does not exist in the signature for <A>
     (Try adding it to the export list in that hsig file.)
 }}}

 * (Put more problems here)

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13149#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler