Milestone M5

The Type Checker

Part VI described a checker that types a program before it runs. The checker has one rule per form, as the evaluator does. It checks or synthesizes depending on whether the context supplies a type, and it names what neither mode supplies with an inference variable that unification solves. At each use of a generic function, it instantiates the function’s type parameters afresh. This milestone puts that checker into src/types/check.rs. Nothing in the evaluator changes, and every M1–M4 test must still pass.

From this milestone on, the checker stands between the parser and the evaluator. The interpreter checks every declaration in the program and runs main only if all of them are accepted, so a program with a type error prints nothing at all. New on the provided side is the driver that walks the declarations and judges each one when its body has been checked. There is also a module of helpers, printed in the helper module below, which you paste into your own file.

To-dos

grep -rn 'todo_m5!' src lists the holes, all in src/types/check.rs: an arm of check_expr for each form of M1–M4, and the body of unify. Each hole names the rules it implements:

// src/types/check.rs — some of the M5 holes
Expr::Lit(..)    => todo_m5!("T-Int / T-Bool / T-Str / T-Unit"),
Expr::Var(..)    => todo_m5!("T-Var / T-Self"),
Expr::Block(..)  => todo_m5!("T-Block / T-Let / T-Seq"),
Expr::Return(..) => todo_m5!("T-Return (reads ctx.ret())"),
Expr::Call(..)   => todo_m5!("T-App (first-order matching of generics at the call)"),
// … and the rest of the M1–M4 forms

pub fn unify(&mut self, a: &Ty, b: &Ty, span: Span) -> Result<(), TyError> {
    todo_m5!(
        "unify (structural agreement; solves TyKind::Meta with an occurs check)"
    )
}

The stub’s let _ = (ctx, expected); keeps the compiler quiet until your arms read those parameters, and can be deleted once they do. The arms for relations, constructors, match, ?, structs, and methods stay holes until their milestones, and so does check_rule.

One requirement has no hole of its own: check_expr must stop recursing past a fixed depth. It is described with the arms below.

Milestone specification

Each form, the rules that type it, and the cases in which the checker rejects it:

Wherever two types must agree, unify decides, and it fails with a mismatch or, when a type would have to contain itself, an infinite type. The rules are collected in Appendix D’s typing rules, and the static errors by name gives the TyError variant a test expects for each case and the span it carries. A type checker and Function types and polymorphism turn the rules into the algorithm the arms follow; this table is the checklist your checker is measured against.

The provided driver does the checks that belong to a whole declaration. It builds the top-level context from the signatures, checks each global in initialization order and reports a cycle among them, and checks every other declaration in source order, so the first error in the file is the one reported. It validates every written signature, requires main to take no parameters, and turns a mismatch in a body whose fn omits -> T into a message saying the result type was left off. After each declaration it applies the determination rule to every type your arms recorded, and it judges the bounds your arms and the native functions’ types asked for: NoEquality, NotPrintable, and UnsatisfiedBound come from there.

These contracts hold across the arms:

• Every arm ends the same way. When there is an expected type, the arm unifies the type it has built with it ($\text{Chk-Sub}$), then resolves the type and records it at its own span with record. This holds for the arms that pass the expected type down to their parts as well. A list checked against Int, or a pair against a triple, gets nothing from the expected type, and the final unification is where its mismatch is found; where the parts did use it, the final unification succeeds. The determination rule reads only what was recorded, so a type that is never recorded is never judged.
• unify(a, b, span) takes the type found first and the type required second. A failure is Mismatch { expected: b, found: a, span }, both resolved. Inside compound types the pair reported is the innermost one that disagrees: a [Int] passed where [String] is required is expected String, found Int, at the argument.
• Premises are checked in the order the rule writes them, left to right: an operator’s left operand before its right, a call’s callee before its arguments, a condition before its branches. The first failure is the one reported, and the tests check which one it is.
• A mismatch is reported where the type goes wrong. An arm that passes its expected type down to a subexpression lets the mismatch surface at the smallest expression whose type disagrees: (0 - n) in describe, "one" in an if whose other branch is 1.

Implementing Milestone M5

Paste the helper module into src/types/check.rs first; several arms call it. Then destructure each arm’s .. into the fields you need, as at M4:

A block’s statements are Stmt::Let(Name, Option<Ty>, Expr, Span), the span covering the whole binding, and Stmt::Expr(Expr). Types are built with Ty’s constructors (Ty::int(), Ty::list(t), Ty::func(params, ret), Ty::reference(t), and the rest in ast.rs) and taken apart by matching on ty.kind, a TyKind. Match on a type only after resolve, since an inference variable that has been solved still looks like a TyKind::Meta until it is resolved.

The provided checker

A type checker shows Ctx and the inference variables (fresh_meta, solve, resolve, record), and Function types and polymorphism shows decl. The arms also use these, provided in src/types/mod.rs:

impl Checker {
    /// Record that `ty` must satisfy trait `trait_` (a bound met at a use site).
    pub fn require_bound(&mut self, trait_: Name, ty: Ty, span: Span);
    /// The same, for a bound with type arguments (`T: Conv<String>`).
    pub fn require_trait(&mut self, trait_: TraitRef, ty: Ty, span: Span);
    /// The expression at `span` never produces a value.
    pub fn record_diverging(&mut self, span: Span);
    pub fn is_diverging(&self, span: Span) -> bool;
    /// `whole` leaves because its part `sub` does: mark `whole` diverging
    /// and the code after `sub` within it as never running.
    pub fn dead_after(&mut self, sub: Span, whole: Span);
    /// T-Eq's side condition; and whether `ty` is a bare type parameter.
    pub(super) fn admits_eq(&self, ty: &Ty, visiting: &mut HashSet<Name>) -> bool;
    pub(super) fn is_type_param(&self, ty: &Ty) -> bool;
    // and the field `depth: usize`, the nesting of the expression being checked
}

/// Whether `ty` still contains an inference variable.
pub(super) fn contains_meta(ty: &Ty) -> bool;
pub const MAX_NESTING: usize = 150_000;

admits_eq takes a set it uses to stop on recursive types; pass it &mut HashSet::new().

The arms

What follows adds to the content chapters what a test will hold you to. A rule’s premises are checked in the order the rule writes them, and every arm ends as the first contract above says, with the final unification and record.

• The nesting bound. When self.depth has reached MAX_NESTING, check_expr returns TooDeep { limit: MAX_NESTING, span } for the expression in hand instead of matching on it. Otherwise it increments depth, checks the expression, and decrements depth again whatever the outcome. This is the balance enter_call and leave_call kept at M4. Applying ? to the result before decrementing would leave depth incremented after every error, so take the result as a value, decrement, and then return it. Moving the match into a method of its own keeps the increment and the decrement in one place.
• Var looks a name up in this order: the Ctx; a top-level fn, through decl; a global, through global_type; a native prelude function, through native_fn_type. A name found in none of them is UnboundVariable at the name. A fn declaration gives the type fn(params) -> result from its signature. If it declares type parameters, map each one to a fresh inference variable, a new map at every use, and apply the map with Ty::substitute, which ast.rs provides. For each parameter declared with a bound T: C, record the bound with require_trait on the variable T became, at the name’s span, with the bound’s own type arguments substituted in the same way.
• Operators. Arithmetic and ordering check both operands against Int, and and or against Bool, - and not their operand likewise. Equality synthesizes the left operand and checks the right against its type. If that type, resolved, still contains a variable, require an Eq bound on it for the driver to judge. Otherwise, a type that does not admit equality is NoEquality { ty, is_param, span } at the whole expression, with is_param from is_type_param. Concatenation synthesizes the left operand. One whose resolved type is neither a string, a list, nor an unsolved variable is Mismatch { expected: String, … } at that operand. The right operand is then checked against the left’s type, and a type still unsolved after both is Ambiguous at the whole expression. Cons synthesizes the element and checks the list against a list of its type.
• Tuples, lists, and projection. A tuple checked against a tuple type of the same width passes each component its counterpart; otherwise its components are synthesized. A list takes its element type from an expected list type, or else from a fresh variable, and checks every element against it in order. The empty list is that fresh variable and nothing more, for the context or the determination rule to settle. A projection synthesizes its operand and resolves it: a tuple wide enough gives the component, a narrower one is NoSuchComponent { index, arity }, a type not yet known goes to undetermined, and anything else is NotATuple { index, found }, all at the projection’s span.
• References. ref e is a reference to whatever e synthesizes. deref e checks e against a reference to a fresh variable and has that variable as its type. e1 := e2 checks e1 against a reference to a fresh variable, checks e2 against the variable, and has type ().
• Blocks thread a Ctx through their statements, each let extending it for the statements after. A let with an annotation passes it through annotation at the statement’s span, checks the initializer against the type annotation returns, and binds the name at that type. A let without an annotation binds the name at the type its initializer synthesizes. An expression statement is synthesized and its type discarded. The block’s tail is checked against the expected type, and a block with no tail has type ().
• if, while, for. A condition is checked against Bool. With an else, the then branch is checked against the expected type and the else branch against the then branch’s type, which is the if’s type. Without one, the branch is checked with no expected type and must unify with (). A branch that does not is IfWithoutElse { found } at the branch, and the if has type (). A while body is checked against (). A for checks its iterable against a list of a fresh variable and its body against (), in the context extended with the loop variable at that variable. Both loops have type ().
• return e reads the enclosing function’s result type with ctx.ret(). With none, it is ReturnOutsideFunction. Otherwise e is checked against it, the return is recorded as diverging, and its own type is a fresh variable, so it fits whatever its context requires.
• Lambdas. Each parameter’s type is its annotation, through annotation at the parameter’s span; failing that, the matching parameter of an expected function type with the same number of parameters; failing that, a fresh variable. The result type is the expected function type’s, or a fresh variable. The body is checked against the result type in ctx.enter(Some(result), ctx.self_ty()) extended with the parameters, so a return inside the body targets the lambda. The lambda’s type is the function type of the parameters and result, each resolved.
• Calls. check_callee synthesizes the callee and returns its type, resolved, with the range of bounds it recorded. A function type with a different number of parameters than there are arguments is ArityMismatch at the whole call, naming the callee if it is a variable and "this function" otherwise. Each argument is checked against its parameter’s type, left to right; then finish_call moves the callee’s bounds onto the arguments that supply them, and the call has the function type’s result type. When the callee’s type is still an unsolved variable, as in |f| f(1), the call infers a function type for it: synthesize the arguments, make a fresh result variable, and unify the callee’s type with the function type they form, at the call’s span. Any other callee type is NotAFunction { found } at the callee.
• unify resolves both types first. An unsolved variable agrees with itself. An unsolved variable against any other type is solved as that type, unless it occurs in that type, which is InfiniteType at span. Int, Bool, String, (), and Self agree with themselves. Two tuples of the same width, two lists, two references, two function types with the same number of parameters (the parameters in order, then the results), and two named types with the same name and number of arguments agree when their parts unify pairwise, left to right. Any other pair is the mismatch.

Leaving and dead code

Three provided calls tell the driver what your arms know about control flow:

• record_diverging(span) marks an expression that produces no value. A diverging expression’s type is exempt from the determination rule, which is why return 0 can stand in a branch whose type nothing else fixes. The return arm marks itself. A block whose tail diverges is marked too, and so is an if whose branches both diverge.
• dead_after(sub, whole) marks whole as diverging because its part sub is, and the code after sub within whole as never running. A block calls it as soon as a statement’s expression, or a let initializer, diverges, with that statement’s span and the block’s, and before it checks the statements after it. Those are still checked, inside the region now marked dead, so the call has to come first for undetermined and the determination rule to treat them as dead. Only the first diverging statement calls it. A block that leaves this way and has no tail has a fresh variable as its type, where it would otherwise have (). An if or while calls it when its condition diverges, and a for when its iterable does.
• note_callee(span) exempts a named callee from the determination rule, since whatever is unknown in its type is unknown in an argument or in the call, which are the places to report it. check_callee calls it.

Code that never runs needs no annotations, so the determination rule skips it, and undetermined returns a fresh variable for it where it would otherwise report Ambiguous. A mismatch in dead code is still an error. So

fn f() -> Int { return 1; let y = []; println(y); 2 }

checks, although nothing fixes the element type of y. In fn f() -> Int { return 1; 1 + true }, by contrast, 1 + true is still rejected.

Where the calls go

The two arms below show where the calls are made and when, with the typing left as comments for you to fill in. Each ends as every arm does: unify the type with the expected one, if there is one, then resolve the type, record it at the arm’s span, and return it. Those last lines are the same in every arm, and a method of your own can save writing them out each time.

Expr::Block(stmts, tail, span) => {
    let mut cx = ctx.clone();
    let mut leaves = false;
    for stmt in stmts {
        // T-Let / T-Seq: check the statement, extending `cx` for a `let`.
        // `e` is the statement's expression or the `let`'s initializer,
        // `at` is the statement's span.
        let (e, at) = /* … */;
        // The first statement that leaves makes the rest of the block dead;
        // the call comes before the remaining statements are checked.
        if !leaves && self.is_diverging(e.span()) {
            leaves = true;
            self.dead_after(at, *span);
        }
    }
    let ty = match tail {
        Some(e) => /* the tail, checked in `cx` against `expected` */,
        None if leaves => self.fresh_meta(), // a block that leaves fits anywhere
        None => Ty::unit(),
    };
    if tail.as_ref().is_some_and(|e| self.is_diverging(e.span())) {
        self.record_diverging(*span);
    }
    // Chk-Sub, then record: the end of every arm
    if let Some(exp) = expected {
        self.unify(&ty, exp, *span)?;
    }
    let ty = self.resolve(&ty);
    self.record(*span, ty.clone());
    Ok(ty)
}

Expr::If(cond, then, els, span) => {
    // the condition, checked against Bool
    if self.is_diverging(cond.span()) {
        self.dead_after(cond.span(), *span); // both branches are dead
    }
    // the `then` branch, checked against `expected` when there is an `else`
    // and against `None` when there is not; its type `t` is the `if`'s
    let t = /* … */;
    match els {
        Some(e) => {
            // the `else` branch, against `t`
            if self.is_diverging(then.span()) && self.is_diverging(e.span()) {
                self.record_diverging(*span); // every path leaves
            }
        }
        None => { /* `t` must unify with (), or it is IfWithoutElse */ }
    }
    // Chk-Sub, then record: the end of every arm
    if let Some(exp) = expected {
        self.unify(&t, exp, *span)?;
    }
    let t = self.resolve(&t);
    self.record(*span, t.clone());
    Ok(t)
}

The other forms follow the same pattern. A while calls dead_after(cond.span(), *span) when its condition diverges, a for makes the same call with its iterable’s span when the iterable diverges, and a return calls record_diverging(*span) on itself.

The helper module

The starter leaves the module below out. Paste it at the end of src/types/check.rs, after the closing brace of the impl Checker block. It is a module of its own with its own use lines, so it cannot clash with the imports your arms add. Its methods are public, so one you have not called yet raises no warning. It can read the Checker’s private fields because check.rs is part of the types module.

• annotation(ty, ctx, span) checks a type written inside a body, a let’s or a lambda parameter’s, against the declared types and the type parameters in scope. It also replaces Self by the type an impl is for, which matters from Part IX on.
• native_fn_type(name, span) is the type of a native prelude function, with fresh variables for its generic parts and the bounds of Appendix C recorded on them, or None if name is not a native function. The entries marked #[cfg(not(feature = "m8"))] drop out at M8, where those functions become Bridger code in the prelude that decl finds.
• global_type(x) is the type of the global x: its annotation, or the type the driver recorded when it checked the initializer. It is None if x is not a global.
• check_callee(f, ctx) and finish_call(bounds, param_tys, args, call_span) bracket a call. A bound the callee carries, such as Ord on min’s parameter, is recorded where the callee is named. finish_call moves it to the argument whose parameter mentions the bounded type, where the type that fails it is written, so let g = min(f, f); with f a function is reported at the first f.
• undetermined(span) is for an operand whose type a rule needs and does not yet know: a fresh variable in dead code, Ambiguous at span elsewhere.

/// Provided helpers (Milestone M5): plumbing that no typing rule describes.
/// Paste this module at the end of the file, unchanged.
mod helpers {
    use crate::ast::{Decl, Expr, Name, Span, Ty, TyKind};
    use crate::types::{Checker, Ctx, TyError};
    use std::ops::Range;

    type Res<T> = Result<T, TyError>;
    type Bounds = Range<usize>;

    impl Checker {
        /// A type annotation written inside a body (`let x: T`, `|x: T|`): `Self`
        /// resolved to the enclosing `impl`'s type, and every name it uses checked
        /// to be a declared type or a type parameter in scope (`Self` outside an
        /// `impl` names no type).
        pub fn annotation(&self, ty: &Ty, ctx: &Ctx, span: Span) -> Res<Ty> {
            let ty = match ctx.self_ty() {
                Some(self_ty) => ty.with_self(&self_ty),
                None => ty.clone(),
            };
            self.validate_type(&ty, span)?;
            Ok(ty)
        }

        /// The type of a native prelude function (Appendix C, "Functions").
        /// `print` / `println` / `to_string` carry a `Print` bound and `contains`
        /// an `Eq` bound; until M8 `len` carries `Len` and `min` / `max` /
        /// `minimum` / `maximum` carry `Ord`, which the built-in types satisfy.
        /// `None` for a name that is not a native primitive.
        pub fn native_fn_type(&mut self, name: &str, span: Span) -> Option<Ty> {
            let opt = |t: Ty| Ty::named("Option".to_string(), vec![t]);
            let sig = match name {
                "print" | "println" => {
                    let t = self.fresh_meta();
                    self.require_bound("Print".to_string(), t.clone(), span);
                    Ty::func(vec![t], Ty::unit())
                }
                "to_string" => {
                    let t = self.fresh_meta();
                    self.require_bound("Print".to_string(), t.clone(), span);
                    Ty::func(vec![t], Ty::str())
                }
                "abs" => Ty::func(vec![Ty::int()], Ty::int()),
                "even" | "odd" => Ty::func(vec![Ty::int()], Ty::bool()),
                "range" => Ty::func(vec![Ty::int(), Ty::int()], Ty::list(Ty::int())),
                #[cfg(not(feature = "m8"))]
                "len" => {
                    let t = self.fresh_meta();
                    self.require_bound("Len".to_string(), t.clone(), span);
                    Ty::func(vec![t], Ty::int())
                }
                #[cfg(not(feature = "m8"))]
                "min" | "max" => {
                    let t = self.fresh_meta();
                    self.require_bound("Ord".to_string(), t.clone(), span);
                    Ty::func(vec![t.clone(), t.clone()], t)
                }
                #[cfg(not(feature = "m8"))]
                "minimum" | "maximum" => {
                    let t = self.fresh_meta();
                    self.require_bound("Ord".to_string(), t.clone(), span);
                    Ty::func(vec![Ty::list(t.clone())], opt(t))
                }
                "contains" => {
                    let t = self.fresh_meta();
                    self.require_bound("Eq".to_string(), t.clone(), span);
                    Ty::func(vec![Ty::list(t.clone()), t], Ty::bool())
                }
                "head" => {
                    let t = self.fresh_meta();
                    Ty::func(vec![Ty::list(t.clone())], opt(t))
                }
                "tail" => {
                    let t = self.fresh_meta();
                    Ty::func(vec![Ty::list(t.clone())], opt(Ty::list(t)))
                }
                "unwrap_or" => {
                    let t = self.fresh_meta();
                    Ty::func(vec![opt(t.clone()), t.clone()], t)
                }
                "map" => {
                    let (a, b) = (self.fresh_meta(), self.fresh_meta());
                    Ty::func(
                        vec![Ty::list(a.clone()), Ty::func(vec![a], b.clone())],
                        Ty::list(b),
                    )
                }
                "filter" => {
                    let a = self.fresh_meta();
                    let keep = Ty::func(vec![a.clone()], Ty::bool());
                    Ty::func(vec![Ty::list(a.clone()), keep], Ty::list(a))
                }
                "fold" => {
                    let (a, b) = (self.fresh_meta(), self.fresh_meta());
                    Ty::func(
                        vec![
                            Ty::list(a.clone()),
                            b.clone(),
                            Ty::func(vec![b.clone(), a], b.clone()),
                        ],
                        b,
                    )
                }
                "is_some" => {
                    let t = self.fresh_meta();
                    Ty::func(vec![opt(t)], Ty::bool())
                }
                "read_int" => Ty::func(vec![], Ty::int()),
                "read_bool" => Ty::func(vec![], Ty::bool()),
                "read_line" => Ty::func(vec![], Ty::str()),
                "read_int_opt" => Ty::func(vec![], opt(Ty::int())),
                "read_bool_opt" => Ty::func(vec![], opt(Ty::bool())),
                "read_line_opt" => Ty::func(vec![], opt(Ty::str())),
                _ => return None,
            };
            Some(sig)
        }

        /// The type of the top-level global `x`: its annotation, or the type
        /// the driver recorded for its initializer. `None` if `x` is not a
        /// global.
        pub fn global_type(&mut self, x: &Name) -> Option<Res<Ty>> {
            let (annot, init) = match self.decl(x) {
                Some(Decl::Global(annot, init)) => (annot.clone(), init.clone()),
                _ => return None,
            };
            Some(match (annot, self.global_types.get(x)) {
                (Some(ty), _) => Ok(ty),
                (None, Some(ty)) => Ok(ty.clone()),
                (None, None) => self.check_expr(&init, &Ctx::new(None, None), None),
            })
        }

        /// Synthesize the type of a call's callee, resolved, and note what the
        /// call's bookkeeping needs: a named callee is exempt from the
        /// determination rule, and the bounds the callee's type carries come
        /// back as a range to pass to `finish_call`.
        pub fn check_callee(&mut self, f: &Expr, ctx: &Ctx) -> Res<(Ty, Bounds)> {
            let start = self.obligations.len();
            let ty = self.check_expr(f, ctx, None)?;
            if matches!(f, Expr::Var(..)) {
                self.note_callee(f.span());
            }
            Ok((self.resolve(&ty), start..self.obligations.len()))
        }

        /// Call after checking a call's arguments against the parameter types
        /// `param_tys`: a bound the callee placed on a type parameter is
        /// reported at the argument whose parameter mentions it, or at the
        /// whole call if none does.
        pub fn finish_call(
            &mut self,
            bounds: Bounds,
            param_tys: &[Ty],
            args: &[Expr],
            call_span: Span,
        ) {
            for i in bounds {
                let want = &self.obligations[i].1;
                let blamed = param_tys.iter().position(|p| contains_ty(p, want));
                self.obligations[i].2 = match blamed {
                    Some(j) => args[j].span(),
                    None => call_span,
                };
            }
        }

        /// An operand whose type is still unknown where its rule needs it: in
        /// code that never runs nothing is required of it; elsewhere its type
        /// is undetermined.
        pub fn undetermined(&mut self, span: Span) -> Res<Ty> {
            if self.in_dead_code(span) {
                Ok(self.fresh_meta())
            } else {
                Err(TyError::Ambiguous { span })
            }
        }
    }

    /// Whether `needle` occurs in `hay` (structurally, spans aside).
    fn contains_ty(hay: &Ty, needle: &Ty) -> bool {
        if hay == needle {
            return true;
        }
        let any = |ts: &[Ty]| ts.iter().any(|t| contains_ty(t, needle));
        match &hay.kind {
            TyKind::Tuple(ts) | TyKind::Named(_, ts) => any(ts),
            TyKind::List(t) | TyKind::Ref(t) => contains_ty(t, needle),
            TyKind::Fn(ps, r) => any(ps) || contains_ty(r, needle),
            _ => false,
        }
    }
}

Running a program

From this milestone on, cargo run --features m5 checks a program before it runs it. A program the checker rejects stops with the error before main is called, and the exit status is 1. In late.brg, total is an ordinary variable, and := assigns only through a reference. The M4 interpreter runs the program until it reaches the assignment:

$ cat late.brg
fn main() {
    println("start");
    let total = 0;
    total := total + 1;
}

$ cargo run -q --features m4 -- late.brg
start
  × type error: expected ref<()>, found Int
   ╭─[late.brg:4:5]
 3 │     let total = 0;
 4 │     total := total + 1;
   ·     ─────────┬────────
   ·              ╰── here
 5 │ }
   ╰────

With M5’s checker, the program never starts:

$ cargo run -q --features m5 -- late.brg
  × type mismatch: expected ref<_>, found Int
   ╭─[late.brg:4:5]
 3 │     let total = 0;
 4 │     total := total + 1;
   ·     ──┬──
   ·       ╰── here
 5 │ }
   ╰────

The evaluator reports the assignment, the expression that got stuck. The checker reports total, the expression whose type disagrees with what := requires of its target: a reference to a fresh variable, still unsolved when the mismatch is found. An unsolved variable is printed as _.

Because the checker runs first, no program runs under --features m5 until the arms it reaches are written: the first todo_m5! it meets stops the run. cargo run --features m4 still runs the evaluator with no checker in front of it.

Worked examples

An expression in an empty context, and the type the checker gives it:

(1, "a").1                                     : String
[] ++ [true]                                   : [Bool]
|x| x + 1                                      : fn(Int) -> Int
ref [1]                                        : ref<[Int]>
{ let r = ref 0; r := deref r + 1; deref r }   : Int
map([1, 2], to_string)                         : [String]
fold([1, 2, 3], 0, |acc, x| acc + x)           : Int

Expressions the checker rejects:

1 + "a"                          Mismatch (expected Int, found String), at "a"
(true, 1).4                      NoSuchComponent (index 4, arity 2)
{ let f = |x| x(x); () }         InfiniteType, at x(x)
{ let f = |x: Int| x; f == f }   NoEquality (fn(Int) -> Int)
len(42)                          UnsatisfiedBound (no impl Len for Int), at 42
{ let xs = []; xs := [1]; () }   Mismatch (expected ref<_>, found [_]), at xs
abs(1, 2)                        ArityMismatch (`abs` takes 1, given 2)

How to know it works

cargo m5 runs the provided milestone M5 tests and, with them, the M4, M3, M2, and M1 tests. The M5 tests come in two kinds. The first builds an Expr by hand with the builders of the earlier milestones and types it in an empty context with infer, or against a type with check. The second loads a program from source and checks it with check_program, on top of the prelude:

// |x| x + 1  :  fn(Int) -> Int
let f = lambda(&["x"], binary(Add, var("x", 1), int(1, 2), 3), 0);
assert_eq!(infer(&f).unwrap(), Ty::func(vec![Ty::int()], Ty::int()));

// a whole program, checked declaration by declaration
let src = "fn double(x: Int) -> Int = x * 2; fn main() -> Int = double(21);";
assert!(check_program(src).is_ok());

A rejection is tested by its TyError variant and, where it matters, by its span and payload, never by the text of its message. Fill the arms and unify, run cargo m5, and repeat until every M5 test, and every earlier one, passes. Then run the programs you wrote for M4 with cargo run --features m5: a correct program that the checker rejects is either a bug in an arm or one of the conservative rejections Part VI describes, and the error’s span says which expression to look at.

Design problems

fn apply(f: fn(Int) -> String) -> String = f(1);

fn main() {
    let g = |x: Int| x;
    println(apply(g) ++ "!");
}

let log = ref [];

fn note(s: String) { log := s :: deref log; }

fn main() {
    note("start");
    note("stop");
    println(deref log);
}

fn make_stack<T>() -> (fn(T) -> (), fn() -> Option<T>) {
    let items = ref [];
    let push = |x| items := x :: deref items;
    let pop = || {
        let top = head(deref items);
        items := unwrap_or(tail(deref items), []);
        top
    };
    (push, pop)
}

fn main() {
    let ints = make_stack();
    ints.0(1);
    ints.0(2);
    println(ints.1());          // Some(2)
    println(ints.1());          // Some(1)
    println(ints.1());          // None
    let words = make_stack();
    words.0("hi");
    println(words.1());         // Some("hi")
}

fn main() {
    let xs = [1, 2];
    let total = sum(xs);
    println(total);
}