Documentation

public interface to the typechecker

The ordered context of the typechecking algorithm.

The context is a sequence of Elements. The typechecking algorithm appends to it, retracts a suffix of it (everything after a marker), replaces one element with a few (e.g. an existential solved to an arrow, with the arrow's fresh existentials inserted before it), and asks scoping questions: is this variable declared, as an existential or a universal, and at what position? Is it solved, and to what?

The sequence only orders the elements. What is known about each variable is kept in indexes keyed by variable name, beside the sequence, and each of those maps a variable to a position in the sequence (CtxPosition): every element in the sequence has one, and vars maps each variable to its element together with that position.

So for instance, a solution proposed for an existential β may only mention variables declared before β in the context, existentials and universals alike (the universals are the rigid type variables of enclosing quantifiers). solve therefore looks up each free variable of the solution in vars, checks that it is declared as the kind of variable it occurs as, and compares its position with β's. Once β is solved, its solution is read from the same entry. anns and refinements are the same idea for term variable annotations and for the branch-local refinements of a universal.

The sequence is a finger tree whose measure includes the greatest position in a subtree (so that the element at a position can be found in logarithmic time), and a count of Inconsistent elements (so that inconsistent can tell in constant time whether the pattern-match branch being checked has been marked unreachable by contradictory GADT refinements, in which case its body is skipped).

Every change keeps the indexes describing exactly the elements in the sequence: an append or replacement records the new elements, and a retraction walks the elements it discards and forgets them. Each element is appended once and discarded at most once, so a retraction costs no more than the appends it undoes.

Segments of a context that have been retracted are plain lists (CtxSegment); the typechecker reads them whole (to generalize over their unsolved existentials, apply their solutions, or push some of them back).

The elements, in order.

Elements of an ordered algorithmic context. Every element but Refined declares its variable; a context is valid when no variable is declared twice and every type in it mentions only variables declared before it.

Replace any existentials with their solution in the context, and any refined universals with their refinement.