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 termlevel 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 typecheckedonly 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)