Lesson 7.6 — Local and flow-based inference: Rust, Kotlin, TypeScript, and Pebble

Techniques: Rust — HM-style unification inside one function body, without generalization, with separate integer and float literal variables and a fallback to i32/f64 [RUSTC-Infer, RUSTC-Fallback]; Kotlin — declaration-local inference plus builder inference for lambdas whose receiver's type parameters are still unknown (PCLA in the K2 compiler) [KOTLIN-Spec, KOTLIN-PCLA]; TypeScript — a declaration's type is its initializer's type, widened, with contextual typing into lambdas and flow-based "evolving" types for let x; [TS-Handbook, TS-Checker]; Pebble's inference mode — the numeric literals and unannotated let/var of Chapter 6 re-derived as unification with numeric variables and defaulting (pebble-spec §8.9) · Pebble implements: inferTypes (exercises E1–E4) · Drills: — (see §9) · Prerequisites: Lessons 7.1, 7.4; Lesson 6.4 · Time: 5 hours

The languages that most programmers use every day infer types, but not like ML: they infer locally. Signatures of functions are written; inside a body, let x = … needs no annotation. This lesson surveys three production designs — Rust (unification within a function), Kotlin (within a declaration, with a special case for builders), TypeScript (from the initializer, then along the control flow) — and then Pebble's own: Chapter 6's bidirectional checker with its literal rule, rebuilt on unification so that let y = 1.5; let z = y * 2; works. That is the checker you implement in this chapter's exercises.

1. Problem and motivation

Rust

The problem. Rust wants function signatures to be the documented, checked interface (no inference across functions, no generalization inside them) but wants bodies free of annotations, including let v = Vec::new(); whose element type is decided by a later v.push(1.5). Rust's type checker (rustc_hir_typeck) therefore runs HM-style unification over the whole body of one function, with the expected-type propagation of Lesson 6.4 [RUSTC-Typeck], and resolves trait obligations as types become known. Integer literals get an integer inference variable ({integer}) that unifies only with integer types; if nothing decides it, it falls back to i32 (and {float} to f64) at the end of the body [RUSTC-Fallback].

Kotlin

The problem. Kotlin infers the type of a declaration from its initializer and the type arguments of a call from its arguments and expected type (Lesson 6.4's local type inference), but that fails for DSL-style builders: in buildList { add(1) } the list's element type is determined only by what the lambda does, yet the lambda's receiver type depends on it. Kotlin's builder inference (reworked as "PCLA", partially constrained lambda analysis, in the K2 compiler) analyzes the lambda while the type variable is still unfixed, collects the constraints the calls inside impose, and fixes the variable afterwards [KOTLIN-Builders, KOTLIN-PCLA].

TypeScript

The problem. TypeScript types existing JavaScript: variables are declared without types and reassigned, arrays start empty and are filled, a literal 1 may be meant as the type 1 (in a union of literal types) or as number. TypeScript infers a declaration's type from its initializer, widens literal types for mutable declarations (let n = 1 is number, const one = 1 is 1), computes a best common type for array literals, types callback parameters from the contextual type, and — for let x; without an initializer or let acc = [] — follows the control flow, giving x a different type at each point (evolving or auto types) [TS-Handbook, TS-Checker].

Pebble's inference mode

The problem. Chapter 6's checker (pebble-spec §8.1) decides an integer literal's type locally: float if it is checked against float, int otherwise. So let y = 1.5; let z = y * 2; is an error (E0402): the operands of * are synthesized independently and 2 synthesizes int. Rust would accept the analogous program for its integer types; Swift would too (Lesson 7.5). Pebble's inference mode (pebble-spec §8.9, the tool ch07-infer) makes the literal's type a variable, decided by unification anywhere in the function body and defaulted to int at the end — the constraint system of Lesson 7.4 with X = "is int or float", solved eagerly. It accepts every program Chapter 6 accepts, with the same types, and more.

2. Definitions and algorithms

Definition 7.6.1 (Inference scope)

The inference scope of a checker is the largest program region whose constraints are solved together: an expression (Swift, Lesson 7.5), a declaration with its initializer (Kotlin, TypeScript), a function body (Rust, Pebble's inference mode), a whole module (ML, Haskell). Types that cross a scope boundary must be written (signatures) or are fixed when the scope is closed.

Definition 7.6.2 (Literal variables and defaulting)

A literal variable \(\nu\) is a type variable restricted to a finite set \(K(\nu)\) of types (Pebble: \(\{\mathsf{int}, \mathsf{float}\}\) for integer literals; Rust: all integer types for {integer}, \(\{\mathtt{f32}, \mathtt{f64}\}\) for {float}). It unifies with a type \(\tau\) only if \(\tau \in K(\nu)\), and with another literal variable \(\nu'\) by merging, restricted to \(K(\nu) \cap K(\nu')\). Defaulting (Rust: fallback) binds every literal variable still unbound when its scope closes to a designated default \(d(\nu) \in K(\nu)\) (Pebble: int; Rust: i32, f64).

Rust

Algorithm 7.6.3 (Checking a Rust function body, simplified)

• Input: a function with its written signature; the trait impls in scope.
• Output: a type for every expression of the body, or errors.
• Precondition: the signature is fully written (no inference across functions).
• Postcondition: every inference variable is resolved (by unification, by trait selection, or by fallback), or error E0282 "type annotations needed" is reported.
• Invariant: inference variables live in union-find tables (general, integer, float); trait obligations whose self type is still a variable are kept pending and retried.

function CheckBody(f):
    for each parameter p: bind p to its written type
    CheckExprWithExpectation(body, ExpectHasType(return type))   # Lesson 6.4's modes
        # literals: 1 → fresh {integer} var; 1.0 → fresh {float} var
        # let x = e: x's type is e's type (possibly containing variables)
        # method calls and operators register trait obligations  τ: Trait
    SelectPendingObligations()             # trait selection may unify variables
    for every unresolved {integer} var: bind to i32;  {float}: bind to f64   # fallback
    SelectPendingObligations()             # fallback may unblock obligations
    for every still-unresolved general type variable: error E0282 at its origin

Kotlin

Algorithm 7.6.4 (Builder inference, after Kotlin's PCLA)

• Input: a call builder { … } whose lambda's receiver type mentions a type parameter \(E\) of the call, not fixed by the arguments or the expected type.
• Output: a type for \(E\) and for every expression in the lambda.
• Precondition: the calls inside the lambda on the receiver are to members whose signatures mention \(E\) (add(e: E)).
• Postcondition: \(E\) is fixed to a type satisfying every constraint collected from the lambda, or the call is rejected ("cannot infer type").
• Invariant: while the lambda is analyzed, \(E\) is a postponed variable: calls may constrain it but nothing may depend on its final value.

function InferBuilderCall(call, lambda):
    E ← fresh postponed type variable
    analyze lambda with receiver type Builder<E>:
        each call add(arg) on the receiver adds the constraint  type(arg) <: E
    solve the collected constraints for E (least upper bound of the lower bounds)
    if E has no constraint: error "cannot infer type for type parameter"
    fix E; complete the types of the lambda's expressions

TypeScript

Definition 7.6.5 (Literal types, widening, best common type)

A literal type is the type of exactly one value (1, "a", true). A literal expression has a fresh literal type; the widening of a type replaces fresh literal types by their base types (1 ↦ number). A let/var declaration without annotation gets the widened type of its initializer, a const declaration the unwidened one. The best common type of an array literal's elements is their union (after widening), and an empty array literal [] in a let starts an evolving array whose element type is the union of the types later pushed along the control flow.

Algorithm 7.6.6 (The type of a TypeScript declaration)

• Input: a declaration let x = e, const x = e or let x;, with its uses.
• Output: the declared type of x, and the flow type of x at each use.
• Precondition: e is checked with its contextual type (if the declaration is itself in a typed position).
• Postcondition: every assignment to x must be assignable to the declared type; each read has the narrowed flow type (Lesson 6.6).
• Invariant: the declared type never depends on later uses; only the flow type does.

function DeclaredType(decl):
    case decl of
        const x = e:  return TypeOf(e)                        # literal types kept
        let x = e:    return Widen(TypeOf(e))                 # 1 ↦ number, [] ↦ evolving
        let x:        return auto                             # evolving: follow assignments
function FlowTypeAt(x, use):
    if DeclaredType(x) is auto or evolving:
        return the union of the types assigned on the paths reaching use   # Lesson 6.6
    return Narrow(DeclaredType(x), the guards on the paths reaching use)

Pebble's inference mode

Algorithm 7.6.7 (Pebble's inference mode: pebble-spec §8.9)

• Input: a resolved Pebble module (Chapter 5).
• Output: a type on every declaration and expression, and the diagnostics of §13.3 plus E0416.
• Precondition: struct fields, parameters and results have written types (as in Chapter 6).
• Postcondition: on programs Chapter 6 accepts, the same type table (Theorem 7.6.11); more programs accepted (§3).
• Invariant: every numeric variable class is unbound or bound to int or float, and remembers where it was bound; a failed unification binds nothing.

function InferFunction(f):
    classes ← empty union-find;  recorded ← []
    CheckBlock(f.body)                          # Chapter 6's synth/check, with:
        # integer literal:           ν ← fresh class;  record(literal, ν)
        # let/var x = e (no type):   τx ← Synth(e)   (may contain ν, e.g. [ν; 3])
        # "types must be equal":     Unify(τ1, τ2, origin)   instead of τ1 = τ2
        #    failure → E0416 if one side is an inferred name whose class was bound
        #              earlier and a fresh class would have fit; else the §13.3 code
        # & | ^ on a variable:       Unify(ν, int, the operator)
    for every class still unbound: bind it to int   # defaulting
    for every recorded (node, τ): node.setType(Zonk(τ))

function Unify(τ1, τ2, origin):              # both sides resolved through the classes
    if either is <error>: return ok
    if both are classes: merge them; return ok
    if one is a class ν and the other a type t:
        if t ∉ {int, float}: return fail
        bind ν to t;  origin(ν) ← origin;  return ok
    if both are arrays of the same length: return Unify(elements)
    return τ1 = τ2 (concrete types, by identity)

3. Worked examples

Rust

The Rust version of the running example (the box of §7 runs it): let a = 1; let b: u8 = a; gives a an {integer} variable that the annotation on b binds to u8 — a later use decides an earlier binding, exactly as in Pebble's inference mode. let c = 2; is never constrained and falls back to i32 (size_of_val(&c) = 4). let mut v = Vec::new(); v.push(1.5); creates Vec<?T> and the push binds ?T := {float}, which falls back to f64. let v = Vec::new(); with no later push leaves ?T unresolved: E0282 at the declaration.

Kotlin

buildList { add(1); add(2) }: the element type \(E\) is postponed; each add contributes \(\mathsf{Int} <: E\); after the lambda, \(E := \mathsf{Int}\) and the result is List<Int>. val n = 1 fixes n : Int at the declaration (Kotlin's scope is the declaration), so val d: Double = n is an error rather than a later decision; emptyList() with no expected type has no constraint on its T: "cannot infer type".

TypeScript

declaration	initializer's type	declared type
let n = 1	fresh literal 1	number (widened)
const one = 1	fresh literal 1	1
const pair = [1, "a"]	(1 \| "a")[]	(string \| number)[] (best common type, widened)
const r = twice(y => y + 1, 3)	T := number from 3, then y : number contextually	number
let acc = []; acc.push(1); acc.push("s")	evolving array	(string \| number)[] at the return

Pebble's inference mode

The file of the §7 box, fn main() -> int { let y = 1.5; let z = y * 2; let n = 1; let a: int = n; let b: float = n; return 0; }, under Algorithm 7.6.7 (classes \(\nu_2\) for 2, \(\nu_1'\) for the 1 of n, \(\nu_0\) for 0):

step	statement / node	action	classes afterwards
1	let y = 1.5	\(y : \mathsf{float}\) (a float literal)	—
2	y * 2	synth 2: fresh \(\nu_2\); unify \(\mathsf{float} = \nu_2\) at *	\(\nu_2 \mapsto \mathsf{float}\) (origin *)
3	let z = y * 2	\(z : \mathsf{float}\)	unchanged
4	let n = 1	fresh \(\nu_1'\); \(n : \nu_1'\) — inferred binding	\(\nu_1'\) unbound
5	let a: int = n	check n against int: unify \(\nu_1' = \mathsf{int}\) at n (5:18)	\(\nu_1' \mapsto \mathsf{int}\) (origin 5:18)
6	let b: float = n	unify \(\mathsf{int} = \mathsf{float}\) fails; n is inferred, its class was bound at 5:18, and a fresh class would unify with float	E0416 at 6:20, note at 5:18
7	return 0	fresh \(\nu_0\); unify with int	\(\nu_0 \mapsto \mathsf{int}\)
8	end of body	defaulting: no class left unbound; write the types	—

Chapter 6's checker rejects the same file twice: E0402 at the * (3:15) and E0401 at 6:20. The inference mode accepts line 3 (the literal becomes a float) and replaces the second error by E0416, which names the binding whose type the program asked for twice and points at the first request. Remove line 5 and the program is accepted with n : float, decided by line 6.

4. Invariants and correctness

Rust

Proposition 7.6.8 (Fallback preserves typability)

If a Rust function body type-checks except for unresolved {integer} variables whose only constraints are membership in the integer types (and equalities among themselves), then binding each such class to i32 makes the body type-check.

Proof

A class \(\nu\) that is unresolved at fallback time occurs in no equality with a concrete type (otherwise unification would have bound it) and in no trait obligation that selection could not satisfy for every integer type (otherwise selection would have failed or bound it). Binding \(\nu\) to i32 satisfies its membership constraint (\(\mathtt{i32} \in K(\nu)\)), satisfies every equality among classes (all members of the merged class receive i32), and every pending obligation on it is re-selected after fallback (Algorithm 7.6.3), which is where a missing i32 impl would surface. Note that the behavior can depend on the choice (overflow at i32 width), which is why fallback is a language rule, not an implementation detail.

Kotlin

Proposition 7.6.9 (Builder inference agrees with an explicit type argument)

If the constraints collected in Algorithm 7.6.4 have a least solution \(E_0\), then the call is accepted with \(E = E_0\), and the program with the explicit type argument buildList<E0> { … } type-checks with the same types.

Proof

With the explicit argument, every add(arg) requires \(\mathrm{type}(arg) <: E_0\); these are exactly the collected constraints, which \(E_0\) satisfies by definition, and the lambda's other expressions do not depend on \(E\) (the postponement invariant). Conversely the builder-inferred call assigns \(E_0\) and then completes the lambda's types exactly as the explicit version would, because the lambda is checked against the same receiver type MutableList<E0>.

TypeScript

Proposition 7.6.10 (Widening keeps a declaration usable, not more precise)

For let x = e, every value of \(e\)'s widened type may later be assigned to \(x\), and every read of \(x\) is typed by a supertype of every value it can hold at that point.

Proof

The declared type is \(\mathrm{Widen}(\mathrm{TypeOf}(e)) \supseteq \mathrm{TypeOf}(e)\) (widening only replaces a literal type by its base type, a supertype), so the initial value conforms, and any later assignment is checked against the declared type (Algorithm 7.6.6's postcondition). A read's flow type is the declared type narrowed by guards (Lesson 6.6, Theorem 6.6.7), which contains every value that can reach the read. The price is precision: let n = 1 cannot be used where the literal type 1 is required, which is why const keeps it.

Pebble's inference mode

Theorem 7.6.11 (Conservative extension)

If Chapter 6's checker (pebble-spec §8.1) accepts a Pebble module, the inference mode accepts it and assigns every declaration and expression the same type.

Proof

Fix one function body; run both checkers side by side — they visit the same nodes in the same order with the same checking forms. Map each Chapter 6 literal to its Chapter 6 type (\(\mathsf{float}\) if it was checked against float, else \(\mathsf{int}\)) and each inference-mode class accordingly; call this assignment \(\rho\). (1) \(\rho\) satisfies every unification the inference mode performs: each unification corresponds to a place where Chapter 6 required two types to be equal (the mode switch, operator operands, arguments, …) and found them equal, since it accepted; under \(\rho\) the inference-mode types are exactly Chapter 6's types (by induction over the visit: an unannotated binding gets its initializer's type in both). So no unification fails and no error is reported. (2) The solution computed equals \(\rho\): unification computes the most general solution (Theorem 7.1.17), of which \(\rho\) is an instance. A class is bound to float in the MGU only if a chain of equations links it to float; \(\rho\) satisfies those equations, so \(\rho\) gives the literal float too. A class left unbound by the MGU is defaulted to int; Chapter 6 gives such a literal float only when checking it against float, which in the inference mode is an equation with float that would have bound the class — so Chapter 6 gave it int as well. Hence both checkers write identical types. ch07.Infer.E1_ReproducesEveryChapter6Table checks the statement on every Chapter 6 golden table.

Proposition 7.6.12 (Eager and generate-then-solve agree)

On every module the inference mode accepts, solving each unification eagerly (Algorithm 7.6.7, the C++ reference) and generating all constraints of a function first, then solving them (the Python oracle pebble_infer, Lesson 7.4's Algorithm 7.4.4) produce the same types.

Proof

Both compute a most general solution of the same set of equations — the order in which Martelli–Montanari or union-find processes equations does not change the MGU up to renaming of unbound classes (Theorem 7.1.15) — and both then bind every unbound class to int. The membership constraints (\(\nu \in \{\mathsf{int}, \mathsf{float}\}\), and "int or bool" for &) are satisfied by any solution of an accepted program. tests/ch07/update_goldens.py and test_ch07.PebbleInference check the agreement on every golden.

5. Complexity

Technique	Time (worst)	Time (typical)	Space	Variables
Rust (body-local unification + trait selection)	trait selection can be exponential or diverge (bounded by recursion_limit); unification near-linear	near-linear per body	union-find tables per body	\(n\) body size
Kotlin (declaration-local + builder inference)	per call, constraint solving over the call's variables	linear in practice	constraints of one call	\(m\) constraints per call
TypeScript (initializer + flow)	flow typing \(O(n \cdot \lvert\mathcal{P}\rvert)\) (Lesson 6.6); generic inference per call	linear-ish, with caching	flow-node cache	\(n\) nodes, \(\mathcal{P}\) reference paths
Pebble's inference mode	\(O(n\,\alpha(n))\) per function	linear	one class per integer literal	\(n\) nodes of the body

Justification. Pebble: one union-find operation per equation, at most one equation per node (Algorithm 7.6.7), no generalization, no search: \(O(n\,\alpha(n))\); defaulting and writing back are linear. Rust adds trait selection, which is a logic-programming search (Lesson 7.7) and can blow up with recursive impls; the compiler bounds it. TypeScript's flow typing is Lesson 6.6's analysis.

Pathological family (Pebble). A chain let x1 = 1; let x2 = x1 + 1; …; let xn = x(n-1) + 1; let f: float = xn; merges \(n\) literal classes into one class that the last line binds to float: \(n\) merges, one binding, linear — but the explanation for any later conflict involving x1 passes through all \(n\) equations, which is why E0416 reports only the first binding (Lesson 7.9).

6. Variants and refinements

Rust

• Never-type fallback (! falls back to (); being changed across editions) [RUSTC-Fallback]. Trade-off: keeps diverging expressions typable; subtle behavior when the fallback type changes.
• Literal suffixes (1u8, 2.5f32): fix a literal's type at the literal instead of by unification [RUSTC-DevGuide]. Trade-off: local and explicit, but noisy; unification makes them unnecessary in most code.

Kotlin

• Builder inference, reimplemented as PCLA in K2 [KOTLIN-PCLA, KOTLIN-Builders]: the K2 compiler analyzes a lambda with partially constrained type variables as a separate inference session. Trade-off: more builder DSLs infer without annotations; the rules for what a postponed variable may influence are intricate.
• Integer literal types: val l: Long = 1 gives the literal the expected integer type (§7). Trade-off: like Pebble's literal rule, but local to the declaration.

TypeScript

• as const and satisfies: keep literal types or check against a type without widening. Trade-off: precision on request, at the cost of annotations.
• Contextual typing vs inference from uses: TypeScript never infers a parameter from its uses in the body (noImplicitAny reports it). Trade-off: predictable local types; callbacks need a contextual type.

Pebble's inference mode

• Scope = one statement (Swift-like): generate and solve per statement, defaulting at its end. Trade-off: let n = 1; let x: float = n; would be rejected again; errors stay very local.
• Scope = the module (ML-like, with inferred function signatures). Trade-off: needs polymorphism and generalization (Lessons 7.2–7.3) and gives errors far from their causes.
• Report the whole conflict set (Lesson 7.9's minimal unsatisfiable subsets) instead of E0416's two locations. Trade-off: complete explanations, more solver work.

7. In real compilers

Rust

rustc creates integer and float variables with next_int_var/next_float_var and keeps them in separate union-find tables (int_unification_table in compiler/rustc_infer/src/infer/mod.rs) [RUSTC-Infer]; fallback happens in type_inference_fallback/fallback_if_possible in compiler/rustc_hir_typeck/src/fallback.rs, whose doc comment states "Unconstrained ints are replaced with i32" [RUSTC-Fallback].

Body-local inference and fallback in rustc 1.94

Reproduce (rustc 1.94.1):

mkdir -p rs && cat > rs/infer.rs <<'EOF'
fn main() {
    let a = 1;                         // {integer}: decided later, or i32
    let b: u8 = a;                     // a : u8, from this later use
    let c = 2;                         // never constrained: falls back to i32
    let mut v = Vec::new();            // Vec<?T>
    v.push(1.5);                       // ?T := f64
    println!("{} {} {} {}", b, std::mem::size_of_val(&c), v.len(), v[0]);
}
EOF
rustc --edition 2021 rs/infer.rs -o rs/infer && ./rs/infer
cat > rs/noinfo.rs <<'EOF'
fn main() {
    let v = Vec::new();
    println!("{}", v.len());
}
EOF
rustc --edition 2021 rs/noinfo.rs -o rs/noinfo

Output (complete):

1 4 1 1.5
error[E0282]: type annotations needed for `Vec<_>`
 --> rs/noinfo.rs:2:9
  |
2 |     let v = Vec::new();
  |         ^   ---------- type must be known at this point
  |
help: consider giving `v` an explicit type, where the type for type parameter `T` is specified
  |
2 |     let v: Vec<T> = Vec::new();
  |          ++++++++

error: aborting due to 1 previous error

For more information about this error, try `rustc --explain E0282`.

What to notice: a is decided by the later annotation on b (scope = function body); c falls back to a 4-byte i32; v's element type comes from push. When nothing constrains a general type variable, there is no fallback: E0282 at the binding — Algorithm 7.6.3's last line.

Kotlin

kotlinc (K2): the postponed-variable analysis is FirPCLAInferenceSession in compiler/fir/resolve/src/org/jetbrains/kotlin/fir/resolve/inference/FirPCLAInferenceSession.kt [KOTLIN-PCLA]; the specification's chapter "Type inference" describes declaration-local inference and builder inference [KOTLIN-Spec].

Declaration-local inference and builder inference in Kotlin 2.2

Reproduce (kotlinc-jvm 2.2.20 from the kotlin-compiler-2.2.20.zip release on GitHub, on JRE 21):

mkdir -p kt && cat > kt/Infer.kt <<'EOF'
fun main() {
    val xs = buildList {            // builder inference: E := Int, from add(1)
        add(1)
        add(2)
    }
    val big = 3_000_000_000         // Long: the literal does not fit in Int
    val l: Long = 1                 // an integer literal takes the expected integer type
    println("$xs ${big + l}")
}
EOF
kotlinc kt/Infer.kt -d kt/out 2>&1 | grep -v JAVA_TOOL
kotlin -cp kt/out InferKt 2>&1 | grep -v JAVA_TOOL
cat > kt/Errors.kt <<'EOF'
fun errors() {
    val n = 1                       // Int, fixed at the declaration
    val d: Double = n               // no Int -> Double, and no inference from this use
    val e: Double = 1               // an integer literal is never a Double
    val empty = emptyList()         // nothing determines T
}
EOF
kotlinc kt/Errors.kt -d kt/out2 2>&1 | grep -v JAVA_TOOL

Output (complete; grep removes the container's JAVA_TOOL_OPTIONS banner):

[1, 2] 3000000001
kt/Errors.kt:3:21: error: initializer type mismatch: expected 'Double', actual 'Int'.
    val d: Double = n               // no Int -> Double, and no inference from this use
                    ^
kt/Errors.kt:4:21: error: initializer type mismatch: expected 'Double', actual 'Int'.
    val e: Double = 1               // an integer literal is never a Double
                    ^
kt/Errors.kt:5:17: error: cannot infer type for type parameter 'T'. Specify it explicitly.
    val empty = emptyList()         // nothing determines T
                ^^^^^^^^^

What to notice: buildList infers List<Int> from the calls inside its lambda (Algorithm 7.6.4); val l: Long = 1 shows Kotlin's literal rule (an integer literal takes an expected integer type). But n's type is fixed when its declaration is checked: the later val d: Double = n cannot change it — the declaration-local scope, where Pebble's inference mode (scope = function body) would make n a float.

TypeScript

tsc: getWidenedTypeForVariableLikeDeclaration and getWidenedLiteralType compute declared types, getEvolvingArrayType implements evolving arrays, inferTypes infers type arguments, and getFlowTypeOfReference the flow types, all in src/compiler/checker.ts [TS-Checker].

Declared types, widening and flow types in tsc 6.0

Reproduce (tsc 6.0.2):

mkdir -p ts && cat > ts/infer.ts <<'EOF'
export let n = 1;                        // widened: number
export const one = 1;                    // literal type 1
export const pair = [1, "a"];            // best common type: (string | number)[]
export const point = { x: 0, y: 0 };     // object literal: { x: number; y: number }
export function twice<T>(f: (x: T) => T, x: T) { return f(f(x)); }
export const r = twice(y => y + 1, 3);   // T := number from 3, then y : number
export function first<T>(xs: T[]) { return xs[0]; }
export const h = first([]);              // nothing constrains T: never[] -> never
export function late() {
    let acc = [];                        // evolving array type (--noImplicitAny)
    acc.push(1);
    acc.push("s");
    return acc;
}
EOF
tsc --strict --declaration --emitDeclarationOnly --outDir ts/out ts/infer.ts
cat ts/out/infer.d.ts
cat > ts/flow.ts <<'EOF'
let n = 1;
n = "one";                               // the declared type was fixed by the initializer
let x;                                   // no initializer: the type follows assignments
x = 1;
const a: number = x;                     // x is number here (control-flow typing)
x = "s";
const b: number = x;                     // and string here
function inc(y) { return y + 1; }        // parameters are not inferred from uses
EOF
tsc --strict --noEmit ts/flow.ts

Output (complete):

export declare let n: number;
export declare const one = 1;
export declare const pair: (string | number)[];
export declare const point: {
    x: number;
    y: number;
};
export declare function twice<T>(f: (x: T) => T, x: T): T;
export declare const r: number;
export declare function first<T>(xs: T[]): T;
export declare const h: never;
export declare function late(): (string | number)[];
ts/flow.ts(2,1): error TS2322: Type 'string' is not assignable to type 'number'.
ts/flow.ts(7,7): error TS2322: Type 'string' is not assignable to type 'number'.
ts/flow.ts(8,14): error TS7006: Parameter 'y' implicitly has an 'any' type.

What to notice: the .d.ts file shows the declared types of Algorithm 7.6.6: let n widened, const one literal, the evolving acc resolved to (string | number)[]. flow.ts shows the two scopes at once: n's declared type is fixed by its initializer (line 2 fails), while x, declared without one, has a flow type that changes with each assignment (line 5 passes, line 7 fails). Parameters are never inferred from their uses (line 8).

Pebble's inference mode

The reference is solutions/pebble/lib/Sema/Infer/src/ (the Solver class: union-find over numeric classes with origins; the checker adapted from Chapter 6). Clang shows the other end of the design space: auto x = 1; is deduced from the initializer alone by Sema::DeduceAutoType in clang/lib/Sema/SemaTemplateDeduction.cpp — template argument deduction applied to the initializer [CLANG-Deduce] — and no later use can change it, like Kotlin's declarations.

Chapter 6's checker and Chapter 7's inference mode on one file

Reproduce (the course's reference build, -DPEBBLE_USE_SOLUTION=all, clang 23.1.2; build/<preset>/bin on the PATH):

cat > infer.pbl <<'EOF'
fn main() -> int {
    let y = 1.5;
    let z = y * 2;
    let n = 1;
    let a: int = n;
    let b: float = n;
    return 0;
}
EOF
ch06-typecheck infer.pbl | grep -v '^[0-9]*:[0-9]* [a-z]'
ch07-infer infer.pbl | grep -E 'int 2|let z|let n|E0416|note'

Output (complete):

3:15: error[E0402]: invalid operands to '*': 'float' and 'int'
6:20: error[E0401]: mismatched types: expected 'float', found 'int'
6:12: note: expected 'float' because of this
3:9 let z : float
3:17 int 2 : float value
4:9 let n : int
6:20: error[E0416]: cannot infer the type of 'n'; add a type annotation
5:18: note: 'n' is inferred to have type 'int' because of this

What to notice: the first grep keeps only Chapter 6's diagnostics: the literal 2 next to a float is E0402. The inference mode types it float (line 3:17), and the conflict on n becomes E0416 with the note at the use that decided n : int — the trace of §3.

8. Comparison

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Rust	Unification over a whole body; literals decided by later uses; fallback i32/f64 (Proposition 7.6.8); no generalization	near-linear unification; trait selection bounded by limits	E0282 "type annotations needed" with a suggested annotation; mismatch errors name the expected type's origin	High: tables, obligations, fallback, expectations	Rust
Kotlin	Declaration-local; builder inference for lambdas (Proposition 7.6.9); literals take expected integer types	per call · fast	"cannot infer type for type parameter"; mismatches at the use	High (K2's PCLA)	Kotlin, DSLs built on builders
TypeScript	Initializer types widened (Proposition 7.6.10); contextual typing; evolving flow types	linear-ish with caches	Errors at assignments against the declared type; implicit-any for uninferable parameters	High: widening, flow graph, generic inference	TypeScript, and JavaScript tooling
Pebble's inference mode	Conservative extension of Chapter 6 (Theorem 7.6.11); literals and bindings decided anywhere in the body; default int	\(O(n\,\alpha(n))\) per function · the same as Chapter 6's checker	Chapter 6's diagnostics, plus E0416 with the first binding's origin	Low: Chapter 6's checker plus a two-point union-find	ch07-infer, exercises E1–E4

Choose body-local unification (Rust, Pebble) when signatures are the interface and bodies should be annotation-free; add literal variables with defaults if your literals can have several types. Choose declaration-local inference (Kotlin, C++ auto) for predictability — a declaration's type never depends on code below it. Choose flow-based typing (TypeScript) when you must type existing dynamically typed code whose variables change type.

9. Assessment

Technique	Quiz ids	Drill	Flashcard tag	Exercises
Rust	rust-fallback, rust-scope	— (the quiz computes fallback and scope decisions on concrete programs; the unification drill covers the unifier)	rust-inference	—
Kotlin	kotlin-builder, kotlin-scope	— (as for Rust)	kotlin-inference	—
TypeScript	ts-widening, ts-evolving	— (as for Rust)	typescript-inference	—
Pebble's inference mode	pebble-literal-types, pebble-e0416	— (the exercises' tests and ch07-infer on your own files)	pebble-inference	E1–E4

References

See the chapter references.