ConstraintKinds feature suggestion and question about type family peculiarity

[Merijn Verstraaten]

Hello fellow haskellers!

I was experimenting with restricting functions operating on GADTs with phantom types to only work on a subset of the possible phantom types. I ended up with the following code:

{-# LANGUAGE ConstraintKinds, DataKinds, GADTs, TypeFamilies, TypeOperators #-}

import GHC.Prim (Constraint)

data Foo a where
    Foo :: Foo Int
    Bar :: Foo Char
    Baz :: Foo Bool

type family Restrict a (as :: [*]) :: Constraint
type instance where
    Restrict a (a ': as) = ()
    Restrict x (a ': as) = Restrict x as

foo :: Restrict a '[Char, Bool] => Foo a -> Bool
foo Bar = True
foo Baz = False


This seems to works marvellously, but in writing it I ran into 2 annoyances.

1) The type errors produced by trying to use a function on a disallowed phantom type are rather unclear. 

    "Could not deduce (Restrict Int ('[] *)) arising from a use of ‛foo"

Which got me thinking, it would be really nice to have a vacuous Constraint that takes an error string as argument, i.e. a constraint that never holds and returns it's error string as type error. This would let you produce far nicer type errors when (ab)using ConstraintKinds and TypeFamilies by, for example, adding an extra Restrict instance "Restrict x '[] = Vacuous "Applying restricted function to disallowed type"" (or something to that effect), producing that message as error rather than the "Could not deduce (Restrict Int ('[] *)" which is a rather unhelpful error if you're not the person that wrote this code and are just using a function with such a Restrict constraint.

2) for some reason the type families syntax always requires a full argument list, which I find rather ugly. I would much prefer to use KindSignatures and write "type family Restrict :: * -> [*] -> Constraint", but GHC does not allow this. Is there a specific reason for not allowing this syntax?

Cheers,
Merijn Verstraaten