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
_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
