Here is a fascinating program that I would like to write, but cannot with Backpack today:

unit p where
    signature Key where
        import GHC.Exts (Constraint)
        data Key k :: Constraint
        instance Key Bool
    signature Map where
        import Key
        data Map k a
        empty :: Map k a
        insert :: Key k => k -> a -> Map k a -> Map k a
        lookup :: Key k => k -> Map k a -> Maybe a
    module M where
        import Map
        import Key
        x = insert True "foo" empty

The point is to make the *constraint* for Map parametrizable, so that HashMap can levy a different constraint (Hashable) than Map (Ord).

data Key k :: Constraint is implementable, because we can implement abstract data types using type synonyms in Backpack, and synonyms can have more kinds than just *. However, GHC chokes on this declaration, because it thinks that data types always have to have kind *.