Giving Backpack a Promotion
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)