Kind inference in Haskell is one of the first steps in typechecking. It allows programmers to write type signatures without mentioning their kind.

Having a sound typechecker that demands type terms to be explicitly kinded, I was thinking of using the typechecker itself to do the kind inference.

Up to date, I am not aware of any similar “bootstrapping” method for kind inference and I am not sure if the resulting system is sound.

For more information about kind inference in Haskell, you may refer to:

Haskell 2010 Report

“A Static Semantics for Haskell” by Karl-Filip Faxen

“Giving Haskell a Promotion” — about the new extensions to GHC

In the following, I am going to sketch my idea with concrete examples. I used GHCi 7.4.1 with -XNoMonomorphismRestriction, -XKindSignature and -XExplicitForAll flags.

`{-# LANGUAGE NoMonomorphismRestriction, KindSignatures, ExplicitForAll #-}`

First I define the ***** kind:

`data Star :: *`

star :: Star

star = undefined

Then, for each primitive type, I define a function with explicit type:

`tInt :: Star`

tInt = undefined

I also define a function to represent the function type constructor (->):

infixr 6 -->

(-->) :: Star -> Star -> Star

a --> b = undefined

With GHC 7.2, if I am not mistaken, we have the “constraint” kind reserved as the kind of class constraints.

I code it as:

`data Constraint :: *`

constraint :: Constraint

constraint = undefined

For example:

`cEq :: Star -> Constraint`

cEq = undefined

A combinator to represent the predicates:

`infixr 5 ==>`

(==>) :: Constraint -> Star -> Star

(==>) = undefined

Now it is time to use these combinators to represent type signatures. For example:

f1 :: a -> Int

f1 = undefined

```
```f2 :: a

f2 = undefined

f3 :: Int

f3 = undefined

`f4 :: Eq a => a -> Int`

f4 = undefined

is modeled as:

`-- inferred type: tf1 :: Star -> Star`

tf1 a = a --> tInt

```
```-- inferred type: tf2 :: forall (t :: *). t -> t

tf2 a = a

-- inferred type: tf3 :: Star

tf3 = tInt

`-- inferred type: tf4 :: Star -> Star`

tf4 a = cEq a ==> a --> tInt

Here is the trick; we demote the type living in the type-universe to a normal value. Consequently, the inferred type for this value, hopefully,

represents the kind of the original type. Therefore, by this technique we can use the typechecker to also infer kinds.

For example, the inferred type of tf1 represents the kind of f1.

GHCi> :t tf1

tf1 :: Star -> Star

Now let us go one step further and model ADTs by the same technique. We first define the sum operator.

`infixr 4 <+>`

(<+>) :: Star -> Star -> Star

(<+>) = undefined

and then we can represent

`data T a b = T1 b Int`

| T2 (b -> Int)

| T3 (a b)

-- | T4 a -- ill-kinded

-- | T5 c -- ill-kinded

with

`-- inferred type: tT :: (Star -> Star) -> Star -> Star`

tT a b = (b --> tInt --> tT a b)

<+> ((b --> tInt) --> tT a b)

<+> (a b --> tT a b)

-- <+> (a --> tT a b) -- ill-typed

-- <+> (c --> tT a b) -- ill-typed

Brilliant! If one part of the original definition is ill-kinded, the representation becomes ill-typed.

Now to add support for type classes, we model the cons operator in the same fashion:

`infixr 4 <:>`

(<:>) :: forall (a :: *). (a -> Star)-> Constraint -> Constraint

(<:>) = undefined

Now we model the following definition,

`class C a where`

c1 :: a b -> Int

c2 :: b (a c) -> Int

-- f3 :: a c b -> Int -- ill-kinded

```
```class D a where

d0 :: a -> Int

`class E a where`

e1 :: E a => a -> Int

to:

`cC a = (\b -> a b --> tInt)`

<:>(\(b,c)-> b --> (a c) --> tInt)

-- <:> (\(b,c)-> a c b --> tInt) -- ill-typed

<:>constraint

```
```cd a = (\() -> tInt)

<:>constraint

`cD a = (\ () -> cD a ==> a --> tInt)`

<:>constraint

Notice, the definition of class E is recursive through the use of predicate “E a” but typechecker has no difficulty inferring the right type.

Finally, the support for type synonyms is straightforward:

`type S a b c d = T a b`

```
```

`sS a b c d = tT a b`

According to Haskell report, definitions should be grouped by their dependency order. Having this framework we can reuse the dependency analysis of let bindings

by simply putting the definition in the same let binding.

This kind system, in addition to features of Haskell 2010, supports constraint kinds and kind polymorphism.

I’m just a layman, I don’t know formal type theory, but this resembles a system I saw somewhere else, the calculus of constructions.

In CoC or any system with dependent typing there is no distinction between types and values, therefore they are handled in a rather similar way . Here we have a vanilla Haskell 2010 typechecker , that doesn’t even support local assumptions (GADTs , Typefamilies and etc). I just demonstrated a simple trick to use the same system to infer kinds. I assume any typechecker with a reasonable design would reuse the same machinery.

How is this Haskell 2010 when you’re using KindSignatures?

Indeed, the original typechecker does not accept the standard Haskell 2010 code since it “demands type terms to be explicitly kinded”. As I mentioned in the reply above it is a vanilla Haskell 2010 typechecker, i.e. there is no kind inference. With the bootstrapping method described in the post we add the support.