Function type_check_recovering 

pub fn type_check_recovering(
    module: &Module,
    interfaces: &HashMap<Name, Interface>,
) -> TypeCheck

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.

What comes back

One Solved per declaration, keyed the way module.values is, whether or not any declaration failed. A declaration the typer could not type is present and says so; none is ever merely absent, because absent is indistinguishable from checked-and-fine to whatever reads this next (DEC-18 decision 1). One that inference reported an error for is Solved::Rejected, with the error in TypeCheck::errors, so a module with a type error still has a typed term for each of its other declarations (DEC-23 decision 5).

The term inside Solved::Typed is the one annotate built, with unify’s final substitution applied to every node rather than to the declaration’s own type alone. That interior is the point — a backend needs the type of each sub-expression, not just of the declaration containing it.

Every instance the module declares is answered for the same way, one SolvedInstance each, with a Solved for each binding of its body: a binding is a declaration whose annotation is the member’s signature at the instance’s type.

Where an Error is built

Here, and only here: this is the last frame that holds the canonical::Value, so it is the only one that knows the declaration’s name and its span. What went wrong and where inside the declaration comes up from inference on the ErrorKind; see Error.

What a declaration is checked against

interfaces is the map module was canonicalized against. Every value and union it exposes is put in the typer’s environment beside this module’s own, so a declaration that forwards an imported value, builds an imported constructor or matches on one is checked like any other. Each use of one of those names gets a fresh instance of its declared type, so one declaration can use Just or Maybe.withDefault at two types — see Types.

A name’s entry is a context and a type (Scheme). A class member’s is its signature with its class’s constraint in front, from the module’s own classes and from every imported interface’s; a function’s is its annotation’s context and type. Each use of one raises the obligations its context asks, which are answered once the declaration’s equations are solved — see the classes module.