Hi,
During experiments with Haskell type system I noticed following incompatibility between a plain class constraint and a constraint kind:
type ConstrList = [ Show, Read ] -- ok
type ShowRead a = (Show a, Read a)
type ConstrList = [ ShowRead ]
-- error: Expected kind ‘[* -> Constraint]’, but ‘[ShowRead]’ has kind ‘*’
Looks like ShowRead is expanded as tuple.
-- hint doesn't help
type ShowRead :: * -> Constraint
Why constraint kind is not expanded as follows:
{-# LANGUAGE UndecidableInstances #-} -- local
class (Show a, Read a) => ShowRead a
instance (Show a, Read a) => ShowRead a
There’s a basic reason that this won’t work: type synonyms must be fully applied. You can’t write ShowRead on its own. It must always be applied to an argument.
I don’t know if there are also more sophisticated reasons this doesn’t work.
Apart from the requirement for type synonyms to be fully applied, there’s an unfortunate ambiguity arising from punning: the same syntax [x] can represent either the type of lists, or the list value containing the single element x. Let’s avoid that by writing this with
data List a = Nil | Cons a (List a)
instead. Now this example
type ConstrList = [ Show, Read ]
must be a list containing two elements (because of the comma) so it becomes
type ConstrList = Cons Show (Cons Read Nil)
which is a well-kinded type-level expression of kind List (Type -> Constraint).
However
type ConstrList = [ ShowRead ]
is interpreted as the list type
type ConstrList = List ShowRead
which is ill-kinded, because ShowRead :: Type -> Constraint but List expects a Type.
Perhaps you meant (note the ')
type ConstrList = '[ ShowRead ]
which means the single-element list
type ConstrList = Cons ShowRead Nil
and this is well-kinded if ShowRead is a class constraint, although doesn’t work if ShowRead is a type synonym due to not being fully applied.
1 Like