A type error along with various contextual information to help us generate better error messages.

Errors that can occur during type checking. The idea is that each error carries information that can be used to help explain what went wrong (though the amount of information carried can and should be very much improved in the future); errors can then separately be pretty-printed to display them to the user.

Various reasons the body of an atomic might be invalid.

The source of a type during typechecking.

Generic eliminator for Source. Choose the first argument if the Source is Expected, and the second argument if Actual.

A "join" where an expected thing meets an actual thing.

Convert a Join into a pair of (expected, actual).

A frame to keep track of something we were in the middle of doing during typechecking.

A typechecking stack frame together with the relevant SrcLoc.

A typechecking stack keeps track of what we are currently in the middle of doing during typechecking.

Push a frame on the typechecking stack within a local TC computation.

Get the current typechecking stack.

The concrete monad used for type checking. IntBindingT is a monad transformer provided by the unification-fd library which supports various operations such as generating fresh variables and unifying things.

Note that we are sort of constrained to use a concrete monad stack by unification-fd, which has some strange types on some of its exported functions that actually require various monad transformers to be stacked in certain ways. For example, see https://hackage.haskell.org/package/unification-fd-0.11.2/docs/Control-Unification.html#v:unify. I don't really see a way to use "capability style" like we do elsewhere in the codebase.

Run a top-level inference computation, returning either a TypeErr or a fully resolved TModule.

Generate a fresh unification variable.

Perform a substitution over a UType, substituting for both type and unification variables. Note that since UTypes do not have any binding constructs, we don't have to worry about ignoring bound variables; all variables in a UType are free.

unify t expTy actTy ensures that the given two types are equal. If we know the actual term t which is supposed to have these types, we can use it to generate better error messages.

We first do a quick-and-dirty check to see whether we know for sure the types either are or cannot be equal, generating an equality constraint for the unifier as a last resort.

unification-fd provides a function applyBindings which fully substitutes for any bound unification variables (for efficiency, it does not perform such substitution as it goes along). The HasBindings class is for anything which has unification variables in it and to which we can usefully apply applyBindings.

To instantiate a UPolytype, we generate a fresh unification variable for each variable bound by the Forall, and then substitute them throughout the type.

skolemize is like instantiate, except we substitute fresh type variables instead of unification variables. Such variables cannot unify with anything other than themselves. This is used when checking something with a polytype explicitly specified by the user.

generalize is the opposite of instantiate: add a Forall which closes over all free type and unification variables.

Pick nice type variable names instead of reusing whatever fresh names happened to be used for the free variables.

Top-level type inference function: given a context of definition types and a top-level term, either return a type error or its type as a TModule.

Infer the signature of a top-level expression which might contain definitions.

Infer the type of a term which does not contain definitions, returning a type-annotated term.

The only cases explicitly handled in infer are those where pushing an expected type down into the term can't possibly help, e.g. most primitives, function application, and binds.

For most everything else we prefer check because it can often result in better and more localized type error messages.

Infer the type of a constant.

check t ty checks that t has type ty, returning a type-annotated AST if so.

We try to stay in checking mode as far as possible, decomposing the expected type as we go and pushing it through the recursion.

A simple type is a sum or product of base types.