Module typer

Expand description

This module contains the type checker pass of the language

It works with the source AST and will perform two jobs:

I have no idea how that works; so bear with me while I explore the space, make mistake and (hopefully) learn something :)

Some papers on type inference:

A type inference problem consists of a type environment Γ , an expression t, and a type T of kind ?

Constraint generation rules:

Equation 1: ⟦x : T⟧ = x ≼ T “x has type T if and only if T is an instance of the type scheme associated with x” Important part: There is no relation to the typing environment Γ, instead x appears free (and will be bound to Γ later)
Equation 2: ⟦λz.t : T⟧ = ∃X1X2.(let z : X1 in ⟦t : X2⟧ ∧ X1 → X2 ≤ T) “λz.t has type T if and only if, for some X1 and X2, (i) under the assumption that z has type X1, t has type X2, and (ii) T is a supertype of X1 → X2.” z and t types must be fresh (can’t generally guess them). They are existentially bound because we are going to solve their values. Note that z is not fresh in the condition (i).
Equation 3: ⟦t1 t2 : T⟧ = ∃X2.(⟦t1 : X2 → T⟧ ∧ ⟦t2 : X2⟧) “t1 t2 has type T if and only if, for some X2, t1 has type X2 → T and t2 has type X2”
Equation 4: ⟦let z = t1 in t2 : T⟧ = let z : ∀X[⟦t1 : X⟧].X in ⟦t2 : T⟧ “let z = t1 in t2 has type T if and only if, under the assumption that z has every type X such that ⟦t1 : X⟧ holds, t2 has type T”

Structs§

Cause: One piece of source text, and why it required a type: the answer to “where did this type come from”.
Error: A type error: what went wrong, where, and in which declaration.
Origin: Where a constraint came from, and — once inference has moved types around — where each of its two types came from.
TypeCheck: What type_check_recovering found in one module: an answer for every declaration, and every error inference reported, side by side.
TypeVariable: A type variable: a placeholder unify may solve to a type, or a rigid one, which it may not.

Binder: What a rigid variable was written in: the three kinds of declared type a body is held to.
ErrorKind: What went wrong, and — for everything unification can raise — where.
Reason: Why two types were required to match.
RecordUse: Which use of a record wrote a FieldConstraint. It decides what the constraint’s errors say and which text their carets are under; nothing about how the constraint is solved depends on it.
Supplier: What could supply the record type an ErrorKind::RecordTypeUnknown is missing — which is what its note tells the reader to do about it. unifier::unknown decides it.
Type
TypeLiteral: The type of an opaque scalar: a type nothing in the language builds or inspects, whose values arrive as literals.
Written: What a constraint would have to be written in, for ErrorKind::MissingConstraint.

infer: infer the type of the given term given known function defined in the outer scopes. This is a translation of the algorithm demonstrated by Ionut Gan at I T.A.K.E Unconference 2015
type_check: type_check_recovering, reduced to a module that either type checked or did not: the solved map when no declaration failed, every error otherwise.
type_check_recovering: Type check one canonical module and hand back what it solved, reporting every value whose inference produced a reportable error rather than stopping at the first — the shape compile_package is built to accumulate.