GHC issueshttps://gitlab.haskell.org/ghc/ghc/-/issues2019-11-27T16:57:26Zhttps://gitlab.haskell.org/ghc/ghc/-/issues/13149Giving Backpack a Promotion2019-11-27T16:57:26ZEdward Z. YangGiving Backpack a PromotionThis 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...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)Research needed