Module typeck 

Static type checking, between resolution and execution.

ADR 0004 decides what this checks and how: annotations are mandatory at boundaries and inferred inside, types are nominal with no subtyping, and checking is per-module. A module sees its own declarations, whatever it imports with use, and the builtins. ADR 0006 replaces that ADR’s “parametric and unbounded” with “parametric with bounds”, which is the change it anticipated.

The import environment

ADR 0005 makes a module able to name another module’s exported declarations, and ADR 0004 anticipated exactly one change for it: the checker gains an import environment. That is Checker::import, and nothing else about the pass is different.

One rule holds it together. A declaration is known by the module that declares it: its table key is its bare name inside that module, and module.Name everywhere else. So two modules may each declare a Config without the checker confusing them, and a type keeps one identity however many imports it is reached through. Traits and conformances travel with it, so an imported trait can be named in a bound and a conformance declared anywhere in the package is found wherever the trait and the type are both in scope. Modules are checked in dependency order, which exists because ADR 0005 forbids import cycles.

Traits and the two dispatch forms

A bound (fn render<T: Display>(value: T)) is checked at the call site that instantiates T, because that is the only place a type parameter is given a type. Inside the body the parameter is rigid and its bound is a fact: a method call on a value of type T resolves through T’s bounds, and a parameter with no bound has no methods at all.

dyn Display is a type of its own, not a type parameter. Only the trait’s plain self-taking methods can be called on it: an associated function has no receiver to dispatch on, and a var self method needs the caller’s own place, which a converted value is not. It never satisfies a bound either — not even its own trait’s — because it is not a type parameter.

The one implicit conversion

A concrete value is accepted where a dyn Trait is expected, exactly when it conforms to that trait. That is the language’s only implicit conversion, and it is deliberately narrow:

• it runs one way only: a dyn Trait value is never a concrete type, and never converts to another dyn Trait;
• it never reaches inside a generic argument. Array<Booking> is not an Array<dyn Display>, because generic arguments are invariant here like everywhere else. [booking, receipt] is an Array<dyn Display>, because each element is checked against dyn Display on its own;
• it satisfies no bound. render(someDyn) is an error even when render<T: Display> and the value is a dyn Display.

It is spelled out here, in coerces, and nowhere else: every place that compares a found type against an expected one goes through Checker::expect or unify, and both consult it.

The type representation

Ty is a closed enum of the builtin types, the structs and enums the module declares, function types, rigid type parameters, dyn Trait, and the Any a Host API schema declares. Two types are equal when they name the same declaration and their arguments are equal: there is no subtyping and no variance, so Array<Int> is not an Array<Any>.

Three variants are not types a program can write:

• Ty::Unknown is the checker does not know, and carries an Unknown saying why. It compares equal to every type whatever the reason, and every operation on it produces an unknown again, so one unknown never becomes a cascade of wrong errors.
• Ty::Never is the type of an expression that does not produce a value, such as return. It also compares equal to every type, because an arm that never produces a value never disagrees with one that does.
• Ty::Any is what a Host API schema declares where nothing it does depends on a type. It compares equal to every type and every operation on it abstains, which is what the schema promised; what it is not is a Ty::Unknown, because a promise and an absence are different facts and a reader of Facts has to be able to tell them apart. The two share one erased representation in the backends, which is cove_ir’s Shapes to decide and not this pass’s.

The four kinds of unknown

Unknown is one variant doing four jobs, and telling them apart is what makes a successful cove check worth reading. The kind is carried by the type, not implied by which constructor built it, so a form can ask what the silence around it is made of — and so one kind can be asserted never to escape:

kind	constructor	cove check
Unknown::Recovery	Ty::recovery	silent
Unknown::DynamicBoundary	Ty::dynamic_boundary	silent here; see below
Unknown::Unconstrained	Ty::unconstrained	error
Unknown::Placeholder	Ty::placeholder	must not escape
language gap	none	warning or error

Recovery is an unknown the checker owes no further word about, because everything there was to say was said — here, a few lines above the constructor, or upstream where the unknown being propagated came from. Every “the receiver is already unknown, so abstain” branch is one of these, and none of them adds a diagnostic. This is the job that keeps one mistake from printing as ten. Its reach goes one step further than the branch that builds it: the arguments of a rejected call are walked against a recovery expectation, so an empty array or an unannotated lambda parameter written inside one is not reported as a second mistake.

A dynamic boundary is a host no Host API schema describes. ADR 0001’s Host API schema is cove_schema, which this crate reads: console.println, http.Request, and every other operation and type of a shipped host module is checked against the same description the boundary dispatches it through — and so is every operation and type of a module an embedder describes, because ADR 0017 lets an embedding hand its own cove_schema::ModuleSchema to Compiler::with_host_schema and this pass reads the two the same way. What stays unknown is a module neither table names: a host may register whatever it likes, and one it never described is one no compiler could read.

Nothing is reported per call into one. The fact is about the use that named the module and about the compilation that was not shown it: no edit to sensors.read can fix it, the remedy is one thing to say however many calls a program makes, and it is the same remedy for a call, a member read, and a value passed in. cove::resolve::unchecked_host puts that warning at the use, where it belongs. What this pass owes such a call is the abstention itself, handed to the arguments as their expected type, so that a callback registered with an unschema’d host — the shape an embedding is written in — is not asked to state a type nothing on this side could have stated. A type named through such a module still warns (HOST_TYPE), as it did before this classification existed.

Checker::host_schema is the one place an embedder-supplied schema has to reach, and reaching it is all it takes to turn any of that back into ordinary checking.

An unconstrained unknown is a type nothing that has been read states: a type parameter no argument, annotation, expected type or later use settles. It is UNCONSTRAINED, and it is an error — an empty array literal, a bare None, a struct’s parameter no field mentions, an unannotated lambda parameter nothing expects a type of, a binding whose uses say nothing, and Ok(1) in a place expecting no Result are all the same fact and are all refused. crates/cove-sema/tests/settled.rs is the invariant that says why: a type nothing settles has no layout, so a program holding one is not a program a backend can run, and a cove check that reported no error about it would be reporting that the program is ready.

A schema’s Any is not one of these. It used to be — the same value, from a source that had said something exact — and it is Ty::Any now. What the schema said still costs the rest of the program wherever it is a result or a field, and those are noted (UNCONSTRAINED_RESULT, UNCONSTRAINED_FIELD). A note rather than a warning, because the schema chose this and no strictness setting can make the checker prove what nobody stated.

One shape of unconstrained type gets a diagnostic of its own. A use that describes a binding in terms of itself — v.push(v) — asks for μX. Vector<X>: regular, finitely representable, and with no surface syntax, because recursion here is nominal and this inference is structural. That is RECURSIVE_TYPE, and it points at the use and names the declaration that would write the type instead.

A placeholder is not a fourth kind of not-knowing; it is the marker for a position no reachable program observes. Some are internal positions the surrounding form settles before reading them, and some are branches no reachable program takes at all. Checker::expr and Checker::declare assert in debug builds that one never reaches a type a program can observe, so the claim each site makes about itself is one the test suite holds it to rather than a comment. Two sites used to break it — a struct’s type parameter that no field mentions, and Result.mapError’s expected callback result — and each let a program check clean and then be wrong at run time.

A language gap is information the checker should have been given and was not. These are the ones that used to pass silently, and none of them does now:

• a name nothing in scope explains, capitalized or not, is an error (UNRESOLVED_NAME, UNKNOWN_NAME, UNKNOWN_TYPE). A capitalized one used to be assumed to come from a host and warn; a host reaches a module through use like everything else, so the assumption named no real way for the name to arrive and only let an unknown through to validate whatever was done with it;
• a type or a module written where a value belongs is an error (NOT_A_VALUE). Vector in Vector.of(1, 2) is understood as part of the call; a bare Vector, console, or Counter is not a form with a type in this system, and never was. A host operation is not one of these: it is a value, and reading the schema gives it the function type it declares, so let log = console.println keeps working and a call through the value is checked. The one exception is a variadic operation, which no fn type in this language can describe — the language’s own gap, said out loud as a note (VARIADIC_AS_VALUE) rather than hidden or refused;
• an early return in a function value nothing expects is an error (LAMBDA_RETURN). Such a lambda takes its result from its body’s value, so a return produces one where the body’s value is not, and nothing written anywhere says what the two have to agree on. “Nothing expects it” is asked of the expected result type: an expectation this pass abstained about answers for it, and one whose own result is a placeholder does not;
• an unannotated lambda parameter, an empty array literal, a bare None, and a struct’s type parameter no field mentions, each in a place that expects nothing in particular, are refused (UNCONSTRAINED). Writing the type is always available, which is what each help says. “Expects nothing in particular” excludes a place this pass already abstained about — a schema’s Any answers for what is given to it — and a sibling or a branch that settles the type counts as saying it: [[], [1]] and if c { None } else { Some(1) } are proved, and are silent.

One thing is deliberately not an unknown: the value a scope binds is Ty::Scope, a type the language gives no name to but this pass knows exactly.

What a scope asks of the function it is written in

Leaving a scope waits for every task nothing awaited, and a task whose value is Err(error) returns that error from the enclosing function, exactly as ? would — that is cove_runtime::task::wait_for_children, and it is the whole reason this pass has anything to say about a scope.

So a scope constrains its function only where one of its children can produce a Cove Err. A scope of Unit-answering children asks nothing, and stays at home in a function that answers nothing. Checker::spawned, Checker::handle_awaited and Checker::leaving_scope are the three points of that: what was spawned, what the program settled itself, and what is left for the scope to return. A child that raises — fuel, an invariant, a Host-boundary failure — is not part of it: that travels as a runtime fault rather than as the function’s value, so it depends on no Cove return type.

Inference variables

One of those unknowns carries a number. Unknown::Var is an unconstrained unknown with an identity, and the identity is what lets the uses of a local binding settle a type its initializer left open:

var log = Vector.of()      // Vector<a>
log.push(text)             // a = String

Checker::open_result mints one wherever a call’s result mentions a type parameter that neither its arguments nor its call site settled. A let or a var with no written type gives every variable in the type it takes to that binding (Checker::attach). Every comparison of a found type with an expected one is read for what it says about them (Checker::constrain, reached from Checker::expect and Checker::check_argument), so a method call, an argument position, an assignment and a declared return type are one rule and not four. And the end of the body writes the answers back (Checker::finish_inference).

Issue #240 decided this, and drew the boundaries around it:

• only a local binding holds one. A parameter, a return type, and everything else a declaration publishes state their types where they are written, and none of them reaches this;
• two uses that disagree are an error (INFERENCE_CONFLICT) naming both, rather than the first one quietly winning;
• a variable nothing settled is asked for the annotation (UNCONSTRAINED), in the same shape the empty array literal is: at the binding when one took it, and at the call that produced the value when none did;
• the scope ends with the body. A variable never outlives the declaration that minted it, so no use in one declaration settles a type in another, and nothing downstream of the checker sees one: what reaches Facts is the settled type, or the plain unconstrained unknown that a variable nothing settled was all along.

It is one mechanism and not a rule per collection: Vector.of(), Set.of(), Map.of(), a generic declaration of the package’s own, a generic enum case, and every builtin method whose result mentions an unsettled parameter all reach open_result. Two nearby gaps are deliberately not on it, because both report where they are written rather than carrying a type forward: an empty array literal and an unannotated lambda parameter. Moving them onto this would move their diagnostics as well, which is a decision about where those warnings belong rather than one about inference.

What a constraint cannot say, it does not say. A use whose own type still holds a variable settles nothing — v.push(v) asks for a Vector of itself, and no annotation writes that either. TyVar::spoken_for is that case, and it is RECURSIVE_TYPE: the type exists, it cannot be written, and a declared type is what writes it instead. It used to be carried silently, which made it the one way a check that reported nothing could hand a backend a Vector<_>.

A variable given to a place this pass abstained about is settled by the abstention rather than reported. A schema declaring Any said there is nothing here that depends on a type, so Ok(()) written in such a callback takes Any as its failure type; asking the program to state one would be asking it to state what the place declared it need not. TyVar::abstained is that.

What a clean check guarantees

cove check reporting nothing at all means every type the package wrote down was checked: every struct field, declared parameter, call to a declared or imported function, and call into a Host API module some schema describes — shipped or embedder-supplied — was checked against a written or schema-declared type.

One silence is not covered by that, and it is named here rather than left to be discovered: a host module no schema describes. Nothing about a call into one is proved, and nothing is said about it here either, because the fact belongs to the use that names the module, where cove::resolve::unchecked_host warns about it once. So a package reaching such a host does not have a clean check: it has one warning per use, naming the module whose schema was never handed over. It is the one exclusion crates/cove-sema/tests/settled.rs makes, for the same reason: what is missing is a description this build was never given, no edit to the call fixes it, and a program that reaches one cannot be lowered.

There used to be a second: a type parameter of a builtin constructor that nothing settles. Ok(1) in a place expecting no Result was a Result<Int, _> with the _ carried rather than reported. What Ok(1) alone means is settled now, and the answer is that it means nothing until something says what the failure type is — Result is generic in both, and a package writing Result<Int, ParseError> is why guessing Error would be a guess. The constructor opens an inference variable like any other call, a later use may settle it, and UNCONSTRAINED asks for the annotation when none does.

A check whose only output is notes means the same, except at the places the notes name: a shipped schema declared Any there, or a variadic host operation was used as a value, and what the program does with the value from that point on is the boundary’s to check.

A check with warnings means the package left the checker something to infer that nothing written settles. cove check --deny-warnings is exactly the request that it did not.

What none of these guarantee is anything the runtime keeps for itself: task safety of a host resource, and every rule listed under What the runtime keeps below.

Two things about a shipped host module are read here and not enforced by the boundary, which is worth stating in one place. A host type’s fields are typed from the schema — request.path is a String because the schema says a Request has one — while the boundary checks a declared type by name only, so what this checks is that the program built the value the schema describes. And a host resource’s declared task-safety is still the runtime’s alone: Ty::Host says nothing about crossing a task boundary, so a resource declaring task_safe: false is refused where it crosses and not before.

Places, and what kind of analysis this pass is

This pass is not only a type checker. ADR 0021 settles what else it is: it may decide any fact the source settles through the binding structure it already walks, and mutability is one. let creates a read-only place and var a mutable one, so which places a program may write is read off the scope stack — Checker::place_mutability is the definition, and the interpreter and cove_ir::lower had a reading of it each until it moved here.

Four constructs are refused by it, in the words the interpreter refused them in: an assignment to a read-only place, a var argument that is a read-only place or is no place at all, and a mutating receiver that is either. A fifth is the same kind of fact about a call’s shape rather than about a place: labeled arguments appear in declaration order, and LABEL_ORDER is what says so.

Two more are facts about a declaration rather than about a call, and ADR 0021’s rule reaches them by the same test — the parameter list is structure this pass already walks to build a signature. A variadic parameter is the last one its declaration writes (VARIADIC_POSITION) and is not written with a default (VARIADIC_DEFAULT). Checker::check_variadic_shape is where both are decided. Unlike the five above, these two are wording of this pass’s own, because there was no behaviour to keep: Interpreter::assign_labels and bind_params disagreed about what a non-last variadic parameter binds, and nothing in either backend could ever reach a variadic parameter’s default.

A third is about where a variadic parameter may be written at all: on a declaration, and not on a function value (VARIADIC_LAMBDA, Checker::lambda). This one does not come from ADR 0021 but from ADR 0016 — a function type names a fixed list of parameters, and a function value has exactly the parameters its type names. It was the VM’s lowering that refused it first, and the two backends disagreed underneath that refusal: this pass typed such a parameter as its element type and dropped the ..., while Interpreter::bind_params wrapped the argument in an Array as it does for any variadic slot, so fn(items: Int...) called with 1 bound 1 on one backend and [1] on the other. Deciding it here makes it one diagnostic on both rather than one backend’s silence; issue #168 is where the question it does not settle — what such a parameter would mean — is written down.

Two things bound it, and both are abstentions rather than gaps in the rule. A name this pass did not bind is not a place and is not reported as one — see Checker::not_a_place. And a receiver whose type is an unknown or a host type is left alone, because the interpreter reaches a host resource’s own operations before it reaches any of this.

What the runtime keeps

The interpreter’s own checks stay, as ADR 0004 says. One rule about a call is left to it entirely, and it is worth naming because it is decidable here and is not decided here: whether a var marking written at a call site agrees with the one written at the declaration. A function type carries no marking, so a call through a value has nothing to check against, and the parameters this pass builds for a builtin, a host operation and a struct’s initializer are not written with a marking at all. ADR 0021 records it as unfinished rather than as decided.

Where a form’s value comes from

docs/LANGUAGE_REFERENCE.md states one rule per expression form, and the two that this pass and the interpreter used to answer differently are stated there because they had to be decided rather than discovered:

• An if with no else produces (), and its branch’s value is discarded. There is no second branch to give the missing case a value, so the branch that runs does not supply one either.
• Every loop produces (). A for runs out of items and a while runs out of condition, so a loop can reach its end without breaking and there is nothing at that end to produce but (); a break operand is checked on its own and its value discarded, exactly as an if’s branch value is. That a loop never carries a value is decided rather than pending: issue #87 settled it, and the Language Reference gives the reason.

The interpreter obeys both, so a checked program’s static and dynamic answers are the same one.

Structs

FnTy

A function type: fn(Int) -> Int, async fn() -> Result<Unit, Error>.

Enums

Ty

A Cove type.

Unknown

Why the checker does not know a type.

Constants

ALIAS_CYCLE

A type alias expands to itself.

ARITY

A call passes more arguments than the callee declares parameters.

AWAIT_OPERAND

await was applied to something that is not a Task.

BRANCHES

The branches of an if or the arms of a match produce different types.

CONDITION

A condition is not a Bool.

CONFORMANCE_SIGNATURE

A conformance’s method does not have the signature its trait declares.

DYN_ASSOCIATED

A trait method with no self was called through dyn Trait.

DYN_MUTATING

A var self trait method was called through dyn Trait.

ENTRY

An entry function’s shape does not fit the host boundary.

HOST_TYPE

A type reached through a host module the schema does not describe (warning).

INFERENCE_CONFLICT

Two uses of a local binding ask for different types where its initializer left one open.

ITERABLE

for was given something it cannot iterate.

LABEL_ORDER

A labeled argument fills a parameter that stands before one an earlier argument already filled.

LAMBDA_RETURN

A function value uses return, with nothing saying what it produces.

LAYOUT_CYCLE

A struct or an enum whose value layout would contain itself.

MISMATCH

An argument’s type does not match the parameter, field, or payload it is given to.

MISSING_ARGUMENT

A call omits a parameter that has no default.

MISSING_PARAMETER_TYPE

A declaration’s parameter has no written type. Unlike a lambda’s, it has no expected type at a call site to infer from.

NOT_A_PLACE

An expression written where a place is required is not one: an assignment’s target, a var argument, or a var self receiver.

NOT_A_VALUE

A type or a module is written where a value belongs.

NOT_CALLABLE

A call was made to something that is not a function.

OPAQUE_CONSTRUCTION

The synthesized labeled constructor of an export opaque struct is called outside the module that declares it.

OPAQUE_FIELD

A field of an export opaque struct is named outside the module that declares it.

OPERATOR

An operator is not defined for these operand types.

PATTERN

A pattern matches a different type than the scrutinee.

PAYLOAD_ARITY

An enum case is constructed with the wrong number of payload values.

READ_ONLY_PLACE

A place let made read-only is written, passed as var, or given to a var self receiver.

RECEIVER

A method was called without a receiver, or an associated function with one.

RECURSIVE_TYPE

A use asks a binding to hold a type that contains itself, which this language writes by declaring a type rather than by inferring one.

SCOPE_CHILD_FAILURE

A task nothing awaits can leave a scope as Err, and the function the scope was written in does not answer a Result that can carry it.

TASK_SAFETY

A type that may not cross a task boundary was written where one must.

TEST

A test fn does not have the shape the test runner calls.

TRY_OPERAND

? was applied to something that is not a Result or an Option.

TRY_RETURN

? propagates a failure the enclosing function cannot return.

TYPE_ARGUMENTS

A generic type is given the wrong number of type arguments.

UNBOUNDED_PARAMETER

A method was called on a type parameter that declares no bound.

UNCONSTRAINED

Nothing written anywhere says what a type is: an unannotated lambda parameter, an empty array literal, a bare None, a struct’s type parameter no field mentions, or a binding whose uses settle nothing, in a place that expects nothing in particular.

UNCONSTRAINED_FIELD

A host type’s field whose schema declares it Any, so the checker can prove nothing about the value read from it (note).

UNCONSTRAINED_RESULT

A host operation whose schema declares its result Any, so the checker can prove nothing about the value it produced (note).

UNKNOWN_ASSOCIATED

An associated call names no associated function of the type.

UNKNOWN_CASE

A qualified case names no case of the enum.

UNKNOWN_FIELD

A field access names no field of the receiver’s type.

UNKNOWN_HOST_OPERATION

A host module’s schema declares no operation of that name, on the module or on one of its resources.

UNKNOWN_HOST_TYPE

A host module’s schema declares no type of that name.

UNKNOWN_LABEL

An argument label names no parameter of the callee.

UNKNOWN_MEMBER

A qualified name reaches nothing an imported module exports.

UNKNOWN_METHOD

A method call names no method of the receiver’s type.

UNKNOWN_NAME

A lowercase name is not in scope.

UNKNOWN_TRAIT

A dyn or a bound names something that is not a trait this module can see.

UNKNOWN_TYPE

A type name no module declares.

UNRESOLVED_NAME

A capitalized name no module declares and no use reaches.

UNSATISFIED_BOUND

A type argument does not conform to the bound its type parameter declares.

UNSUPPORTED_BOUND

A bound was written where the MVP does not check one.

VARIADIC_AS_VALUE

A variadic host operation used as a value, which no function type in this language can describe (note).

VARIADIC_DEFAULT

A variadic parameter is written with a default.

VARIADIC_LAMBDA

A variadic parameter is written on a function value, whose parameters are its function type’s and so are a fixed list.

VARIADIC_POSITION

A variadic parameter stands somewhere other than last in its declaration’s parameter list.

Functions

check

Type-checks a resolved program.

check_facts

Type-checks a resolved program against schemas, keeping what the check worked out about each expression.

check_with

Type-checks a resolved program against schemas, the host modules this compilation may name.