This module contains a compiler pass that checks if all type constructors in type expressions are fully applied and type variables are not applied.

For simplification, all type variables have kind *. Therefore, all type constructors must be fully applied, so partial application of type constructors is not allowed. This pass also checks that type variables and function types do not occur on the left-hand side of a type application. If a type expression is found that does not match this rules, a fatal error is reported. For simplification, a type expression that satisfies all of these rules is called kind-correct.

Example

The following module contains three invalid definitions.

module Failures where

data MyList a = MyNil | MyCons a (MyList a)

-- Invalid because 'MyList' is applied to 2 arguments.
fail1 :: MyList (MyList a a) -> Integer
fail1 x = 42

-- Invalid because type variable 'a' is on the right-hand side of a type
-- application.
fail2 :: a a -> Integer
fail2 x = 42

-- Fails because 'MyList' is applied to no arguments.
fail3 :: MyList -> Integer
fail3 x = 42

Specification

Preconditions

The environment must contain entries for all type constructors that are used in the module.

Translations

The AST is not changed. It is checked if all type constructor applications have the right number of arguments. It is also checked whether there are type variables or function types on the left-hand side of type applications. In these cases, a fatal error is reported. Otherwise, the pass finishes with the given module unchanged.

Postcondition

All type constructors in type expressions are applied to the correct number of arguments and there are no type variables or function types on the left-hand side of type applications.