Type inference for Haskell, part 13

Posted on January 13, 2019

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:

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:

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.

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

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.

(THIH Section 4, Types)

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

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

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

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:

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:

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)

You can find the updated code in kinds.hs.


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:

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.