| 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. This is part of a more general question about how to generate better type error messages. The Helium folk did some good work on this. There's a very interesting PhD to be had here. | 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? We need to fix the "arity" of a type family, because type families must always be fully applied. If you write type family F a :: * -> * then F *must* always be applied to one argument, and in a 'type instance' you can dispatch on one argument type instance F Int = [] type instance F Bool = Maybe If you instead write type family F a b :: * then you must always apply F to two arguments, and in a 'type instance' you can dispatch on two arguments. type instance F Int Bool = Char It is *unsatisfactory* that we get the clue about arity from the syntactic form of the 'type family' declaration. But it's a convenient hack; less clunky than, say type family F [arity = 1] :: * -> * -> * Simon