This module contains a compiler pass that associates top-level type signatures with the corresponding function declarations.

Examples

Example 1

For example, the following module that declares an unary function null with a type signature

null :: forall a. [a] -> Bool
null xs = case xs of { [] -> True; x : xs' -> False }

will be be converted to a module that still contains the type signature but the types of the argument xs and the return type of head are also annotated explicitly in the function declaration itself. In addition, the type arguments of the type scheme are copied from the type signature to the function declaration's type argument list.

null :: forall a. [a] -> Bool
null @a (xs :: [a]) :: Bool = case xs of {
    []      -> True;
    x : xs' -> False
  }

Example 2

The type signature of an n-ary function declaration must not necessarily be a function type with n-1 arrows. For example, the type signature could contain type synonyms.

type Subst = String -> Expr

identity :: Subst
identity x = Var x

In this case, the type synonym needs to be expanded in order to determine the type of the argument x and the return type of identity.

type Subst = String -> Expr

identity :: Subst
identity (x :: String) :: Expr = Var x

The original type signature is left unchanged (not expanded) and type synonyms are only expanded when necessary.

Specification

Preconditions

The environment contains entries for all type synonyms. Otherwise this pass fails if a type synonym needs to be expanded to determine the type of an argument.

Translation

The declaration of every n-ary function f

f x₁ … xₙ = e

for which there exists a top-level type signature

…, f, … :: forall α₁ … αₘ. τ

will be converted into a function declaration with explicit type annotations and type arguments

f @α₁ … @αₘ (x₁ :: τ₁) … (xₙ :: τₙ) :: τ' = e

where τ₁ -> … -> τₙ -> τ is the smallest type that can be derived from τ by expanding type synonyms.

Postconditions

The argument and return types of every function declaration that has a top-level type signature are annotated explicitly.

Error cases

• A fatal error is reported if the type of an argument cannot be determined because a type synonym could not be expanded.
• A fatal error is reported if there are multiple type signatures for the same function declaration.
• A warning is reported if there is a type signature without accompanying function declaration.