63 | | * We first declare a new ''kind'' {{{Nat}}}, that is defined by two types, {{{Zero}}} and {{{Succ}}}. Although {{{Zero}}} and {{{Succ}}} are types, they do not classify any haskell values (including undefined/bottom). So the {{{ foo :: Zero -> Succ Zero -> Bool }}} type signature from earlier would be rejected by the compiler. |

64 | | |

65 | | * We then declare the type {{{List}}}, but we now say the second argument to {{{List}}} has to be a type of kind {{{Nat}}}. With this extra information, the compiler can statically detect our erroneous {{{Cons}}} declaration and would also reject silly types like {{{List Int Int}}}. |

| 63 | * We first declare a new ''kind'' {{{Nat}}}, that is defined by two types, {{{Zero}}} and {{{Succ}}}. Although {{{Zero}}} and {{{Succ}}} are types, they do not classify any haskell values (including undefined/bottom). So the {{{ foo :: Zero -> Succ Zero -> Bool }}} type signature from earlier would be rejected by the compiler. |

| 64 | |

| 65 | * We then declare the type {{{List}}}, but we now say the second argument to {{{List}}} has to be a type of kind {{{Nat}}}. With this extra information, the compiler can statically detect our erroneous {{{Cons}}} declaration and would also reject silly types like {{{List Int Int}}}. |