Type inference for Haskell, part 13

This is part 13 of the series on type inference for Haskell.

There’s a kind of error our type system doesn’t check for yet. Right now, nothing prevents you from writing down a type that makes no sense. Consider this example:

foo :: Int Maybe
foo = foo

That type signature makes no sense for two reasons: first, you cannot apply another type to Int. Second, Maybe needs to have another type applied to it. Most likely the user intended to write Maybe Int. But how do you catch that sort of error?

Trying to apply Int to another type seems really similar to trying to apply a number like 123 to a value. The type system catches the later error. Do we perhaps create a sort of meta-type system to catch the former error?

It turns out that Haskell does have such a system. The “meta types” are called kinds. You can see the compiler talking about kinds if you try to compile the example above:

• Expecting one fewer argument to ‘Int’
  Expected kind ‘(* -> *) -> *’, but ‘Int’ has kind ‘*’
• In the type signature:
    foo :: Int Maybe

(THIH Section 3, Kinds)

Kinds are a simpler system than types. All they really need to capture is how many types a given type wants to be applied to. Int wants to be applied to no other types, Maybe wants to be applied to one, and Either wants to be applied to two. Kinds also recursively capture the kinds of those other types that this type will be applied to.

The way kinds are written looks a lot like function types. The kind of Maybe is * -> *. The kind of Either is * -> * -> *. The kind of Int is just *. The kind * indicates that the type doesn’t need to be applied to anything more. When you apply a type of kind * -> * to a type of kind *, you get another type of kind *. That’s what happens when you apply Maybe to Int getting Maybe Int.

Note that it is possible to express a kind like (* -> *) -> *. This is different from the kind of Either, which instead groups like * -> (* -> *). A kind like this means that the type needs to be applied to another type of kind * -> *. Here’s an example of a type with this kind:

data SomeKind a = SomeKind (a Int)

You can run :k SomeKind in GHCi to print out the kind of a type.

*Main> :k SomeKind
SomeKind :: (* -> *) -> *

It has that kind because the type a is applied to Int. The type Maybe would be valid to use as a:

*Main> :k (SomeKind Maybe)
(SomeKind Maybe) :: *

Most of the possible places where a kind error could take place are in type declarations. Our code assumes that these have already been checked for validity. The actual type inference algorithm only needs to check that it doesn’t accidentally change kinds when it refines types. In other words, the substitutions need to be kind-preserving (see THIH Section 5, Substitutions).

Code changes

The data structure used to store kinds is fairly simple.

data Kind
  = Star
  | Kfun Kind Kind
  deriving (Eq, Ord, Show)

A kind is then attached to type variables and type constructors:

data Tyvar
  = Tyvar Id Kind
  deriving (Eq, Ord, Show)

data Tycon
  = Tycon Id Kind
  deriving (Eq, Ord, Show)

Schemes also keep a list of kinds. When there is a TGen n in the scheme’s type, that n is an index into the list of kinds. That’s how it knows what kind the type variables should be when the scheme is instantiated.

data Scheme
  = Forall [Kind] Type
  deriving (Eq, Show)

(THIH Section 4, Types)

Most of the type definitions are of kind * (because they cannot be applied to other types). They now look like:

tUnit :: Type
tUnit    = TCon (Tycon "()" Star)

tChar :: Type
tChar    = TCon (Tycon "Char" Star)

The types that do need to be applied to some types get a kind like * -> * or * -> * -> *:

tList :: Type
tList    = TCon (Tycon "[]" (Kfun Star Star))

tArrow :: Type
tArrow   = TCon (Tycon "(->)" (Kfun Star (Kfun Star Star)))

tTuple2 :: Type
tTuple2  = TCon (Tycon "(,)" (Kfun Star (Kfun Star Star)))

We also need a function to get the kind back out of these structures:

class HasKind t where
  kind :: t -> Kind

instance HasKind Tyvar where
  kind (Tyvar _ k) = k

instance HasKind Tycon where
  kind (Tycon _ k) = k

instance HasKind Type where
  kind (TCon tc) = kind tc
  kind (TVar u)  = kind u
  kind (TAp t _) = case (kind t) of
    (Kfun _ k) -> k

Note the logic for getting the kind of a TAp. It trusts that the TAp has been constructed correctly. If that’s the case, the kind of the left-hand side will be some Kfun. The kind of the result of applying the two types is the right-hand side of that kind.

Say the type on the left was Either (which has the kind * -> * -> *) and the type on the right was Bool (which has the kind *). The kind of Either Bool would then be * -> * because that’s the right hand side of * -> (* -> *) (parens added for clarity). Note that the left hand side of the kind matches the kind of Bool.

When creating a new type variable, we now need to supply the kind it should have:

newTVar :: Kind -> TI Type
newTVar k = TI (\s n -> let v = Tyvar (enumId n) k
                        in  (s, n+1, TVar v))

The calls to newTVar in tiExpr and tiImpls always use Star. That’s because bindings and variables shouldn’t be of an incomplete type. Any kind other than * indicates that the type needs to be applied to more types.

The functions for creating a scheme are also updated. Note that quantification now stores the original kinds of the type variables that are being generalized:

toScheme :: Type -> Scheme
toScheme t = Forall [] t

quantify :: [Tyvar] -> Type -> Scheme
quantify vs t = Forall ks (apply s t)
 where vs' = [ v | v <- tv t, v `elem` vs ]
       ks = map kind vs'
       s = zip vs' (map TGen [0..])

freshInst :: Scheme -> TI Type
freshInst (Forall ks t) = do
  ts <- mapM newTVar ks
  return (inst ts t)

Finally, the kinds are checked during unification. Specifically, they are checked when replacing a type variable with another type. A type variable should only be replaced with another type of the same kind.

(THIH Section 6, Unification and Matching)

varBind :: Monad m => Tyvar -> Type -> m Subst
varBind u t | t == TVar u      = return nullSubst
            | u `elem` tv t    = fail "occurs check fails"
            | kind u /= kind t = fail "kinds do not match"
            | otherwise        = return (u +-> t)

You can find the updated code in kinds.hs.

Example

It’s not easy to construct an expression that fails the “kinds do not match” check. Here’s one I was able to find. This fails in the definition of foo:

data SomeKind a = SomeKind (a Int)

unwrap :: a b -> b
unwrap = unwrap

getVal (SomeKind x) = x

foo y = (getVal y, unwrap y)

It’s interesting to look at why this causes the error. The getVal function has type SomeKind t -> t Int. Applying getVal to y means that the type of y has to be SomeKind t (for some t). The kind of t there is * -> *. That means that the type of y is the type constructor SomeKind applied to another type of kind * -> *.

The unwrap function is also applied to y. In the type of unwrap, the kind of b is simply *. When unwrap is applied to y, it requires that the type of y unify with a b. Pay attention to b. Here the right-hand side of y’s type needs to be of kind *, but the getVal y expression forced it to be a type of kind * -> *. And thus, there is an error.

This wraps up the fourth extension to the simple type system we originally defined. There is still a little bit left to do before moving on to type classes.