# 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:

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:

```
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.

*(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 `* -> * -> *`

:

```
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:

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.