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)