MEP 5. Type Inference

Field	Value
MEP	5
Title	Type Inference
Author	Mochi core
Status	Standards Track
Type	Standards Track
Created	2026-05-08
Revised	2026-05-11
Requires	MEP 2, MEP 3, MEP 4
Informs	MEP 11, MEP 12, MEP 13, MEP 14, MEP 15

Abstract

Mochi's type system is strictly static and algebraic. Every well-typed expression has a principal type, derivable without runtime evidence. Types are built from a fixed set of primitive kinds, two algebraic constructors (product as StructType, sum as UnionType), the function arrow, parametric type variables, and two designated parameterised kinds for partiality: Option[T] for absence and Result[T, E] for failure. There is no implicit any. There is no implicit nullability. The escape hatch (AnyType) is an explicit surface annotation, never produced by inference. Failures of inference are diagnostic errors, not silent widening.

The rules below are normative. They replace the previous version of this document, which described inference as it happens to behave rather than as it must behave.

Motivation

The previous MEP-5 acknowledged in its Open Questions section that inference falls back to any "when in doubt". That sentence is the source of most type-system bugs the language ships. A user who reads let x = m["k"] and sees x : any cannot pattern-match on the absence; a user who reads let r = parse_int(s) and sees r : int cannot tell the parse failed; a user who reads match shape { Circle(r) => ..., Square(s) => ... } and sees the arm types disagree gets any for the whole expression with no diagnostic. Each any is a soundness hole that downstream code papers over with runtime checks.

The two specific design errors the system inherited:

1. Implicit widening to any. Inference returns AnyType{} on roughly forty paths in types/infer.go when it cannot synthesise a tighter type. Every one of these is a missed diagnostic. The user is told their program type-checks when in fact the system has given up on the expression.
2. Null as a value of every type. Several runtime paths return nil for "missing", "failed", or "uninitialised". The type system has no syntactic discipline that forces the caller to consume the absence. This is the well-known billion-dollar mistake; Mochi inherits it through the Go-level value representation.

A strict, algebraic type system makes both errors structural. Inference either produces a principal type or rejects the program. Absence and failure are first-class parameterised types that the consumer must destructure. The surface language adds no new keywords; the rules in this document are sufficient to derive each construct's behaviour from its parser output and the typing context.

Terminology

The following terms are used with their standard programming-language-theory meaning. A type is a closed expression in the grammar of types/check.go. A type scheme is a type prefixed by zero or more universally quantified type variables, written ∀α₁ … αₙ. τ. The position of an expression in source code determines a typing context Γ, a finite map from identifiers to type schemes. The judgement Γ ⊢ e : τ reads "in context Γ, expression e has type τ". A type is principal if every other type the same expression could be assigned is an instance of it.

Unification is the operation that produces a substitution S such that S(τ₁) = S(τ₂). Generalisation closes a type over the type variables not appearing in the surrounding context, turning τ into a scheme ∀ᾱ. τ. Instantiation replaces the bound variables of a scheme with fresh type variables at each use site. The triple of these operations is Algorithm W (Damas-Milner). Mochi's checker follows that algorithm with the simplifications listed in MEP 12.

The phrase "the type system rejects the program" means the checker emits a diagnostic with a stable T0xx code (see MEP 4 §Diagnostic codes). It does not mean the checker silently substitutes a wider type.

Specification

Judgement form

Every typing rule produces a judgement of the form

Γ ⊢ e : τ

where Γ maps identifiers to type schemes and τ is a type. The checker computes τ by structural recursion on e; the recursion never returns AnyType{} as a fallback. Where a sub-derivation does not pin a type, the rule either picks a fresh type variable (to be unified later) or emits a diagnostic.

The AnyType{} kind continues to exist in the value language only when it appears in source as the literal annotation any. The inference algorithm never produces it. A surface annotation such as let x: any = 1 enters any into the context exactly once, at that binder; the result of x + 1 is then a type error (T030) rather than silently any.

Type schemes and let-generalisation

Let-bound names get generalised; lambda-bound names do not. Concretely:

Γ ⊢ e : τ        τ' = generalise(Γ, τ)
─────────────────────────────────────── [T-Let]
Γ ⊢ let x = e in body :  Γ, x : τ' ⊢ body

Γ, x : τ₁ ⊢ body : τ₂
─────────────────────────────────────── [T-Lam]
Γ ⊢ fun(x: τ₁) => body : τ₁ → τ₂

generalise(Γ, τ) quantifies over every type variable in τ that does not appear free in Γ. The result is a scheme, written ∀ᾱ. τ. At every use site of a generalised name the scheme is instantiated with fresh type variables.

This is the standard ML rule. It gives let id = fun(x) => x the scheme ∀α. α → α, and lets a single call site such as id(1) and another id("x") both type-check at the same binding. The fragment of Algorithm W needed for this is specified in MEP 12.

Primitive operators

The result types of primitive operators follow the lattice in MEP 4 §Numeric tower. The rules below give the lattice as judgements rather than as a table:

Γ ⊢ a : τₐ        Γ ⊢ b : τᵦ        τ = numericJoin(τₐ, τᵦ)
─────────────────────────────────────────────────────────── [T-Arith]
Γ ⊢ a ⊕ b : τ                            where ⊕ ∈ {+, -, *, /, %}

Γ ⊢ a : τ        Γ ⊢ b : τ        τ ∈ {int, int64, float, bigint, bigrat, string}
─────────────────────────────────────────────────────────────────────────────────── [T-Cmp]
Γ ⊢ a ◇ b : bool                         where ◇ ∈ {<, <=, >, >=}

Γ ⊢ a : τ        Γ ⊢ b : τ
─────────────────────────────────────── [T-Eq]
Γ ⊢ a ◆ b : bool                         where ◆ ∈ {==, !=}

Γ ⊢ a : bool        Γ ⊢ b : bool
─────────────────────────────────────── [T-Bool]
Γ ⊢ a ⊗ b : bool                         where ⊗ ∈ {&&, ||}

numericJoin is total over the numeric carrier set defined in MEP 4; applied outside that set it is undefined and the rule does not fire. When the rule does not fire, the checker emits T030 (operand type mismatch). The previous "returns any if operands disagree" behaviour is removed.

Equality (==, !=) requires both operands to share a type up to unification. Cross-kind comparison is rejected (T030). The previous looseness here was MEP 4 problem 9, fixed in #21204.

Boolean connectives require both operands to be bool. The previous "either side non-bool yields any" rule is removed.

Operator precedence and associativity are specified in MEP 2. They affect parse trees, not the typing rules above.

Declarations

Γ ⊢ e : τ        σ = generalise(Γ, τ)
─────────────────────────────────────── [T-LetDecl]
Γ ⊢ let x = e          :  Γ, x : σ ⊢ ...

Γ ⊢ e : τ        unify(σ, τ)
─────────────────────────────────────── [T-LetAnno]
Γ ⊢ let x : σ = e      :  Γ, x : σ ⊢ ...

(no rule)
─────────────────────────────────────── [T-LetBare]   diagnostic T000
Γ ⊢ let x : σ

let without value or annotation is rejected (T000). var is identical to let except the binding is recorded as mutable; the type system does not track mutability further. Aliasing and mutation discipline are MEP 15.

Function declarations behave like let f = fun(...) => .... Top-level functions are generalised before being added to Γ; method receivers are not (the receiver type is fixed at the enclosing struct).

Control flow

Γ ⊢ c : bool        Γ ⊢ t : τ        Γ ⊢ e : τ
────────────────────────────────────────────── [T-If]
Γ ⊢ if c then t else e : τ

Γ ⊢ c : bool        Γ ⊢ body : unit
─────────────────────────────────────── [T-While]
Γ ⊢ while c { body } : unit

The two arms of if must unify. A previous rule widened them to any; the new rule rejects with T008. Programs that relied on the loose join migrate by introducing an explicit Option[T] or by annotating the result.

Γ ⊢ xs : [τ]                Γ, x : τ ⊢ body : unit
────────────────────────────────────────────── [T-ForList]
Γ ⊢ for x in xs { body } : unit

Γ ⊢ xs : {κ : ν}            Γ, x : κ ⊢ body : unit
────────────────────────────────────────────── [T-ForMap]
Γ ⊢ for x in xs { body } : unit

Γ ⊢ s : string              Γ, x : string ⊢ body : unit
────────────────────────────────────────────── [T-ForStr]
Γ ⊢ for x in s { body } : unit

Γ ⊢ a : ι        Γ ⊢ b : ι        ι ∈ {int, int64}
────────────────────────────────────────────── [T-ForRange]
Γ, x : ι ⊢ body : unit
─────────────────────────────────────────────
Γ ⊢ for x in a..b { body } : unit

Any other shape for the source raises T022. The previous fallback to AnyType for unknown source types is removed.

Collections

Γ ⊢ eᵢ : τ                                 (for every i, with one principal τ)
─────────────────────────────────────────── [T-List]
Γ ⊢ [e₁, …, eₙ] : [τ]

Γ ⊢ [] : [α]                                 α fresh                       [T-ListEmpty]

The principal τ is the most general type that unifies every eᵢ. If unification fails, the diagnostic is T031 (heterogeneous list). The previous rule, "fall back to [any]", is removed.

Empty lists are typed at the fresh variable α. Generalisation defers the decision until a use site fixes α. If the list escapes the binding without a fixing use, the checker emits T032 (cannot generalise empty list); the user must add an annotation. This is the price of removing any, empty literals are no longer self-typing.

Γ ⊢ kᵢ : κ        Γ ⊢ vᵢ : ν                 (for every i, with principal κ and ν)
─────────────────────────────────────────── [T-Map]
Γ ⊢ {k₁: v₁, …, kₙ: vₙ} : {κ : ν}

The previous "promote to anonymous struct when every key is a literal" rule is retained as a constructor for the same syntax, but it is a separate parser rule, not an inference rule: the parser annotates the literal at parse time, and the checker types the annotated form. The inference algorithm itself never produces an anonymous struct from a map literal; that decision is fixed by the surrounding syntactic context (e.g. when the literal stands in a position whose expected type is a struct).

Γ ⊢ xs : [τ]        Γ ⊢ i : int
─────────────────────────────────────── [T-IndexList]
Γ ⊢ xs[i] : τ

Γ ⊢ m : {κ : ν}        Γ ⊢ k : κ
─────────────────────────────────────── [T-IndexMap]
Γ ⊢ m[k] : Option[ν]

Γ ⊢ s : string        Γ ⊢ i : int
─────────────────────────────────────── [T-IndexStr]
Γ ⊢ s[i] : string

Indexing a map returns Option[ν], not ν. This is the only routine source of Option in the inference layer; combined with the absence of implicit null, it forces the consumer to destructure the result before using it. Programs that previously wrote m[k] + 1 must now write match m[k] { Some(v) => v + 1, None => 0 } or pattern-bind in let. The cost of this churn is the price of removing the billion-dollar mistake.

Slicing follows the same indexing kinds: xs[a:b] is defined when xs : [τ] or xs : string; it returns the same kind. Slicing a map is rejected (T017).

Option and Result

The two designated parameterised kinds are part of MEP-4 and surface as ordinary algebraic types. Their typing rules are uniform:

Γ ⊢ e : τ
─────────────────────────────────────── [T-Some]
Γ ⊢ Some(e) : Option[τ]

Γ ⊢ None : Option[α]                     α fresh                          [T-None]

Γ ⊢ e : τ
─────────────────────────────────────── [T-Ok]
Γ ⊢ Ok(e) : Result[τ, β]                 β fresh

Γ ⊢ e : ε
─────────────────────────────────────── [T-Err]
Γ ⊢ Err(e) : Result[α, ε]                α fresh

Some, None, Ok, and Err are nominal constructors; pattern matching is the only legal consumer. The fresh-variable disciplines on None, Ok, and Err mean an isolated None or Err must have its element type fixed by a surrounding context (assignment annotation, return position, or pattern). When the context does not fix the variable the checker emits T032 (cannot generalise constructor).

There is no rule that gives an arbitrary type a null inhabitant. nil is not in the value grammar. Functions that previously returned a nilable value return Option (for "missing") or Result (for "may fail") according to their semantic intent; the inference rules above force the caller to consume the constructor.

Match

Γ ⊢ e : τ        for each i : Γ ⊢ pᵢ ⇐ τ   Γ, bind(pᵢ) ⊢ rᵢ : ρ
─────────────────────────────────────────────────────────────── [T-Match]
Γ ⊢ match e { p₁ => r₁, …, pₙ => rₙ } : ρ
provided  exhaustive(τ, {p₁ … pₙ})

The single principal type ρ is the join of every arm's type. The join is defined by unification only; the previous fallback "widen to any" is removed. Heterogeneous arms are a diagnostic (T008).

Exhaustiveness is enforced. The check is the algorithm in MEP 13. A match that omits a variant of a closed UnionType is rejected (T046). A wildcard _ arm covers any residual case.

Within an arm whose pattern names a variant, the bound names see the narrowed type:

e : Shape        p = Circle(r)
─────────────────────────────────────── [narrow]
in arm body: r : float, e : Circle

The same narrowing applies in if e is Variant { ... } blocks. Flow-sensitive narrowing replaces the previous behaviour, where the union type leaked into every arm.

Casts

e as σ requires subtype(ExprType(e), σ) per MEP 11. The previous "no compatibility check" rule is removed. Successful casts have type σ; failing casts are a diagnostic (T033, incompatible cast). The dynamic check fired at runtime by as is unchanged; the static rule simply rejects casts that cannot succeed.

The wildcard cast e as any is permitted (explicit erasure into the escape hatch). The reverse e as σ from e : any is also permitted and produces a runtime check; this is the only path that turns any back into a useful static type.

Function application

Γ ⊢ f : ∀ᾱ. (τ₁, …, τₙ) → ρ
ᾱ' fresh                σ = [ᾱ ↦ ᾱ']
Γ ⊢ aᵢ : σ(τᵢ)
─────────────────────────────────────── [T-App]
Γ ⊢ f(a₁, …, aₙ) : σ(ρ)

Variadic functions follow the same rule with the trailing arguments each unified against the variadic element type (MEP-4 P13). Argument-count mismatches are T006 (too few) or T039 (too many). Argument-type mismatches are T007.

Purity, when relevant, is enforced per MEP 15. The Pure flag participates in unification: a Pure function arrow does not unify with an impure one in a Pure-required position (e.g. where predicates in queries).

Queries

The shape of a query, clause by clause, is specified in MEP 14. The relevant inference rules:

• The iteration variable of from x in xs carries the element type of xs : [τ].
• where p and having p require p : bool and p to be Pure. Impure predicates are T044.
• group by k into g types g as Group[κ, τ] where κ = ExprType(k) and τ is the iteration variable's type. The synthetic Group kind is an internal alias for {key: κ, items: [τ]}.
• Aggregates have precise return types:
  • count(g) : int
  • sum(g) : τ where g : [τ] and τ is numeric
  • avg(g) : float
  • min(g), max(g) : τ where τ is comparable

The previous mismatch between the inferrer (sum returns τ) and the query checker (sum returns int or float) is resolved by adopting the inferrer's rule. This is MEP-5 problem 2.

The projection select r has type [ExprType(r)]. The previous looseness, where r could fall through to a general expression position without validation, is removed; the result type is computed by the same rules as any other expression and must not be any unless r was annotated any at source.

I/O and side-effecting builtins

load p as σ with opts returns Result[[σ], IOError]. save x to p with opts returns Result[unit, IOError]. fetch url with opts returns Result[any, IOError] (the response body is unknown until parsed). These departures from the previous "type is always [σ] / void / any" rules reflect that I/O can fail and the caller must consume the failure.

IOError is a closed UnionType declared in the prelude. Programs that previously ignored the failure case migrate by adding an explicit _ => … arm or by using the ? propagation operator from MEP 15.

Closures

Γ, p₁ : τ₁, …, pₙ : τₙ ⊢ body : ρ
─────────────────────────────────────── [T-Closure]
Γ ⊢ fun(p₁, …, pₙ) => body : (τ₁, …, τₙ) → ρ

Closures do not generalise. A lambda-bound name has a monotype within the closure body, even if the closure is passed to a generic function. Generalisation happens at let f = fun(...), not at the lambda. This is the standard ML restriction.

Pure for closures is computed (the body is scanned for impure calls) but not declared. The result of the computation is recorded on the closure's FuncType and participates in subsequent unification.

Rationale

The previous version of this document said "we prefer to keep error messages tied to concrete source positions" and treated any as the price of that preference. That trade is false. Hindley-Milner inference also produces error messages tied to concrete positions; the messages are sharper because the system never silently agrees with a wrong program. The audit in MEP-4 §Problems found nineteen specific places where any covered for an inference failure. Each one is a position where the user wrote let x = e and the checker accepted it without committing to a useful type.

The choice of Option and Result rather than Maybe and Either follows Rust's vocabulary. The choice is not load-bearing: the constructors are nominal and the type names could be aliased. We prefer the Rust naming because the surrounding ecosystem (LSP, error messages, third-party documentation) is the dominant source of vocabulary for newcomers.

The strict no-implicit-any rule is the largest source of breaking changes. A migration tool (mochi fix --infer) will be required to insert explicit any annotations where users intend the escape hatch and to convert nilable returns to Option returns. The tool is part of the v0.12.0 milestone (see Open Questions).

Backwards Compatibility

This MEP introduces breaking changes. Programs that relied on any of the following will fail to type-check under the new rules:

1. Implicit fallback to [any] for empty list literals not bound in a position with an expected type.
2. Implicit fallback to any for the result of an arithmetic operator applied to mismatched operands.
3. Implicit fallback to any for the result of match with heterogeneous arms.
4. Direct use of m[k] as a ν rather than Option[ν].
5. nil as a value.
6. Casts e as σ where e's static type is incompatible with σ.

A deprecation cycle is provided. v0.11.0 emits warnings (W1xx) for each of the above; v0.12.0 promotes them to errors (T0xx). The corresponding warning and error codes are listed in MEP-4 §Diagnostic codes.

Reference Implementation

• types/check.go: typing context (Env), unification (unify), generalisation (helper not yet extracted), instantiation (likewise).
• types/infer.go: structural recursion of the algorithm. The per-construct rules in this MEP each correspond to a clause of inferPrimaryType, inferPostfixType, inferUnaryType, or inferBinaryType.
• types/util.go: equality and the numeric carrier predicates.
• types/equal_types_test.go: regression tests pinning the per-kind equality contract.
• The Algorithm W generalisation/instantiation pair is partially implemented; the full version is the deliverable for MEP 12.

Open Questions

• Anonymous union types in match joins. The current rule rejects heterogeneous arms outright. A more permissive rule would synthesise τ₁ | τ₂ and require the consumer to destructure. The decision is gated on whether UnionType becomes structural (it is nominal today, see MEP 13 §Structural unions).
• Numeric subtyping vs unification. MEP 11 proposes a subtype lattice for the numeric tower; this MEP unifies them directly. The two cannot both be in force. The decision is to be made on a single PR that lands one or the other; the rest of this MEP is independent.
• Migration tool. mochi fix --infer to insert explicit any and convert nilable returns. Scope and milestone deferred to MEP 9 §Migration.
• Bidirectional checking. Some constructs (lambdas without parameter annotations, struct literals in argument position) are easier to type if the expected type is known. A bidirectional layer over Algorithm W is sketched in MEP 12 §Bidirectional.

Problems

The following are concrete code-level defects against the rules above. Each is tracked separately; PRs reference both the problem number here and the issue number.

1. Inference returns AnyType{} as a fallback. types/infer.go produces AnyType{} on ~40 paths (inferPrimaryType, inferPostfixType indexing, selector tail, cast, query select fall-through). Every path should either compute a tighter type or emit a diagnostic. The fix is mechanical per call site; the cost is the migration cycle. The list-literal sub-case (heterogeneous elements widening to [any]) is fixed in #21270. Status: substantively closed. The remaining AnyType returns in infer.go are bounded by MEP-11.3 (any-to-T requires explicit cast, so a silent any cannot flow into a concrete slot without a diagnostic) and MEP-10 A1 / A5 (cast routing and compatibility). Per-call-site cleanup of the surviving paths is cosmetic and tracked as follow-up; the soundness obligation is discharged.

2. sum() return type disagrees between inferrer and checker. types/infer.go returns the element type; types/check.go widens to int or float. The rule in this MEP is the inferrer's. Fixed in #21261.

3. Empty list and map literals self-type. [] infers as [any]; {} infers as {any:any}. Under the new rule both should produce a fresh type variable and require a use site to fix it. Fix: change inferPrimaryType for the empty cases and rely on let-generalisation.

4. Cast e as σ has no compatibility check. Documented hole; the rule in this MEP requires subtype(ExprType(e), σ). Fix: gate as on the predicate from MEP 11.

5. Match arms widen to any on disagreement. The check rejects heterogeneous arms; the inferrer widens. Fixed in #21267.

6. MapType indexing producing Option[V] is inconsistent with other partial reads. Struct field reads of an unknown name return any; query select of an unknown column does the same. The new rule is that partial reads return Option. Status: closed. All three paths are consistent now: struct field of unknown name raises T026 (a hard error, stronger than the proposed Option), map index of an absent key returns Option[V] via MEP-16 N1/N3, and a query select x["k"] propagates the option through the projection, yielding list<Option<V>> at the let-binding (verified with let ys: list<int> = from x in xs select x["c"] raising T008 because [option[int]] does not flow into [int]).

7. nil is a value of every type. Several runtime entry points return Go nil for "missing", surfaced as AnyType{} to the user. The fix is to wrap them in Option/Result constructors at the runtime boundary; the inference rules above already forbid nil. Status: closed. The remaining VM nil-leaks were the indexing paths whose static result type is τ (not option[τ]): list xs[i] and string s[i] returned ValueNull on out-of-range and on a non-int string index, and OpIndex's default arm returned ValueNull when the target was not a list, map, or string. These all now raise at runtime (runtime/vm/vm_eval.go OpIndex; the constant-folder is matched at runtime/vm/constfold.go so a compile-time OOB no longer folds to a silent null either). For Option-typed reads (first() on an empty list and m[k] on a missing key) the runtime keeps using ValueNull as the in-memory representation of None; consumers (match, ??, ?[, optional chaining) destructure on the null/non-null pivot. There is intentionally no boxed ValueSome tag because introducing one would cascade through every code generator without strengthening the type story already in place. The ?[i] safe-index operator stays as the way to recover an Option for partial reads.

8. I/O builtins return raw [σ], void, any. Should return Result[…, IOError]. Fix: change the registered FuncType for load, save, fetch; add IOError to the prelude as a closed union.

9. Flow-sensitive narrowing is not implemented. Pattern arms bind variant fields but do not narrow the matched expression. Fix: extend the match checker to substitute the narrowed type in the arm's context.

10. Generics are not unified across call sites. Tracked by MEP 12; included here for completeness because the let-generalisation rule in this MEP depends on it.

11. Generalisation is not extracted as a function. The checker does the work inline for top-level functions and not at all for let-bindings. Fix: extract generalise(Γ, τ) and instantiate(σ) to functions and call them at the binders specified in this MEP.

12. Equality (==, !=) accepts cross-kind operands when one is any. Tracked as part of removing the implicit any; covered by problem 1 but called out separately because the check.go path is distinct from the infer.go path.

13. for x in source for unknown source falls back to x : any. Per the rules above, an unknown source is T022. Fixed in #21265.

14. select r in a query falls through to general expression inference. Under the new rule the projection's type must be principal, not any. Status: closed. checkQueryExpr in types/check_expr.go already calls checkExpr proper on the select expression and returns ListType{Elem: selT} (or the scalar aggregate result), so the projection is principal by construction. The original loose-any concern came from generic builtins returning any; that was sealed by MEP-10 A1 (Assignable routing on call arguments) and MEP-12.4 (parametric TypeVar signatures on first, distinct, keys, values, push, append, min, max, etc.). See bb4f1d2c87 for the MEP-10 B6 close, which is the same closure for this row. The only any-typed projections that remain are user-declared : any returns, which are opt-in.

15. Exhaustiveness is not enforced. Tracked by MEP 13. Without it, Option consumption is unsafe. Required for this MEP to be sound.

16. Boolean connectives produce any when an operand is non-bool. Should be T030. Fixed in #21263.

17. Closure return type is inferred without parameter types. A lambda without annotations is typed at (any, …) → any. The strict rule requires either annotations or an enclosing expected type. Fix: gate unannotated lambdas on bidirectional checking (MEP 12).

18. Builtins still declare any parameters. The shape-preserving collection builtins were retyped to ∀α. ...α... schemes in the MEP-12.4 batch: first (#21315), distinct, keys, values (#21315), push, append (#21333), min, max, collect, concat, reduce (same batch). Status: substantively closed. The remaining loose signatures (reverse, len, count, exists, sum) are sound but not parametric; tightening them needs row polymorphism or numeric bounds (a future MEP-12 extension), and reverse keeps its (any) → any declaration on purpose so the list-or-string discriminator in checkBuiltinCall still applies. The call-site post-processor in types/check_expr.go pins the static return shape for reverse, keys, and values even when the declared type is loose.

19. The ExprType / ExprTypeHint split duplicates list/map hint logic. Should be a single bidirectional pass. Fix: collapse the two entry points and route the hint through the recursion.

References

• MEP 2: grammar and parser invariants.
• MEP 4: type kinds and diagnostic codes.
• MEP 11: subtyping lattice (the alternative to numeric unification used here).
• MEP 12: parametric polymorphism, Algorithm W details, bidirectional layer.
• MEP 13: algebraic data types, match exhaustiveness, narrowing.
• MEP 14: query clause-by-clause rules.
• MEP 15: purity, mutability, ? propagation.
• Damas, L. and Milner, R. (1982). Principal type-schemes for functional programs. POPL '82.
• Pierce, B. C. (2002). Types and Programming Languages. MIT Press.

Copyright

This document is placed in the public domain.