Opened 9 months ago

Last modified 8 months ago

#13149 new task

Giving Backpack a Promotion

Reported by: ezyang Owned by:
Priority: low Milestone: Research needed
Component: Compiler (Type checker) Version: 8.1
Keywords: backpack Cc: goldfire
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 (last modified by ezyang)

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)

Change History (5)

comment:1 Changed 9 months ago by goldfire

Yes, with -XTypeInType, coercions appear in types. For example:

type family F a where
  F Bool = Type

foo :: forall (a :: F Bool). a -> a
foo x = x

(Panics in GHC 8.0.1, but works in HEAD.)

The type of foo will contain a reference to a coercion axiom.

comment:2 Changed 9 months ago by ezyang

Description: modified (diff)

Thanks! It was an easy matter to turn it into a Backpack failure; I've added it to the ticket.

comment:3 Changed 9 months ago by ezyang

Description: modified (diff)

comment:4 Changed 9 months ago by Edward Z. Yang <ezyang@…>

In 9ef237b/ghc:

Failing test for #13149.

Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>

comment:5 Changed 8 months ago by ezyang

Priority: normallow
Note: See TracTickets for help on using tickets.