Permit abstract data types in signatures that don't have kind *

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 *.

changed weight to 3

added Tfeature request Trac import backpack typechecker labels

changed the description

This is, I think, another example of the tension between Constraint and *. See #11715 (closed).

Also, you may be tempted to implement this using a constraint family:

    signature Key where
        import GHC.Exts (Constraint)
        type family Key k :: Constraint
        instance Key Bool

But this doesn't work, because GHC expects an instance head to be a type class. (This will probably be a problem even if we allow data types that are not kind Constraint.) The "silver lining" is that you can just defer the "insoluble" constraint to the use-site. But this is terrible, and there are other problems too. Here is some code that type checks with HEAD, but it is not pretty.

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RoleAnnotations #-}
unit p where
    signature Key where
        import GHC.Exts (Constraint)
        type family Key :: * -> Constraint
    signature Map where
        import Key
        type role Map nominal representational
        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
        -- Need to stick the instance constraint here
        -- (and need to do it explicitly! GHC won't infer it.)
        x :: Key Bool => Map Bool String
        x = insert True "foo" empty
unit q where
    module Key where
        import GHC.Exts (Constraint)
        type family Key :: * -> Constraint
        type instance Key = Ord
    module Map(Map, M.empty, insert, lookup) where
        import Prelude hiding (lookup)
        import Data.Map (Map)
        import qualified Data.Map as M
        import Key
        -- Ord is NOT definitionally equal to Key, which means
        -- we have to massage the types
        insert :: Key k => k -> a -> Map k a -> Map k a
        insert = M.insert
        lookup :: Key k => k -> Map k a -> Maybe a
        lookup = M.lookup
unit r where
    dependency p[Key=q:Key, Map=q:Map] -- OK!

I don't think this is #11715 (closed) but is instead related to the commentary in #12680, where there seems to be some confusion about data vs type in signatures. See ticket:12680#comment:125894 and ticket:12680#comment:125997.

If data can be implemented by a type synonym (something I dislike, to be honest), then class should be too. Can you use class instead of data in your example? That would seem to meet your needs. After all, class is essentially the same as data but with a different result kind.

mentioned in issue #12703

mentioned in issue #12704

Richard is right. I put in a patch.

Trac metadata

Trac field	Value
Differential revisions	- → D2595

mentioned in commit 7e77c4b2

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

added Plow label