MEP 11. Subtyping and Variance

Field	Value
MEP	11
Title	Subtyping and Variance
Author	Mochi core
Status	Active
Type	Standards Track
Created	2026-05-08

Delivery status (2026-05-12)

All sub-tasks landed. MEP-11 is Active at v0.12.0.

• MEP-11.1, Subtype predicate in types/subtype.go. Replaces the unify-as-assignment shortcut.
• MEP-11.2, every assignment / argument / return position routes through Assignable (the Subtype wrapper with the element-context carve-out for empty-collection literals).
• MEP-11.3, any flowing into a concrete slot requires an explicit _ as T cast; the strict direction is closed.
• MEP-11.4, list element read is covariant (T-List-Read); writes use invariance (T-List-Inv) via equalKinds.
• MEP-11.5, map key and value are invariant on both sides via equalKinds.
• MEP-11.6, function arg is contravariant, result is covariant.
• MEP-11.7, any as T carries a runtime guard. The type-check side admits the cast (per MEP-10 A5); the VM checks the runtime tag and raises a clear error on mismatch.
• MEP-11.8, a variant struct is a subtype of its declared union (T-Variant).

Aliasing-induced write hazards are closed at the checker by MEP-10 A3 (T051, let-into-var) and MEP-10 B3 (T052, var-element-widen). The runtime guard from MEP-11.7 catches the residual case where a value typed any flows through a cast and lands in a slot whose runtime kind it does not match.

Abstract

Mochi's type checker conflates two distinct judgements. unify resolves type variables for substitution, and it also decides whether one type may flow into a position that expects another. Treating these as one operation introduces unsound shortcuts, the largest of which is that AnyType unifies in either direction. This MEP separates the two judgements. It introduces a dedicated subtype predicate, fixes the variance rules for the structural type constructors, and reduces any to a one-way top type crossable only by an explicit cast with a runtime guard.

Motivation

A sound static type system needs a clear answer to two questions:

1. When does a value of type S flow into a position that expects type T? This is the subtype judgement, written S <: T.
2. When do two open types S and T become equal under a substitution [α₁ ↦ U₁, ..., αₙ ↦ Uₙ]? This is unification, used by parametric inference.

Mochi mixes these. unify(s, t) in types/check.go returns true if s and t would match under a free interpretation of AnyType and the numeric tower. The function is called at assignment, argument, return, and join positions, all of which want the subtype answer, and it is also called when binding a TypeVar, which wants the unification answer. As a result every soundness gap traced in MEP 10 Tier A and most of Tier B shares a single root cause: subtype and unification have been answering each other's questions.

Splitting them is a refactor, not a rewrite. The subtype predicate is small. Variance positions in the language are already enumerated. The work in this MEP makes the two judgements explicit, removes the "any in either direction" rule, and pins every variance position with a fixture.

Specification

The subtype predicate

Define subtype(s, t) to mean s is acceptable wherever t is expected. The rules below are mutually recursive and total. Failure to match any clause is a false return.

[T-Refl]              ─────────────────
                          T <: T

[T-Top]               ─────────────────                (T ≠ AnyType)
                          T <: any

[T-NumTower]          int <: int64
                      int <: bigint
                      int <: float
                      int <: bigrat
                      int64 <: bigint
                      int64 <: float
                      bigint <: bigrat
                      float <: bigrat

[T-List-Read]               S <: T
                      ─────────────────                  (read position)
                          [S] <: [T]

[T-List-Inv]                S = T
                      ─────────────────                  (write position)
                          [S] = [T]

[T-Map-Inv]            K1 = K2    V1 = V2
                      ─────────────────────
                       {K1: V1} = {K2: V2}

[T-Fun]              Q1 <: P1 ... Qn <: Pn    R1 <: R2
                     ──────────────────────────────────
                      fun(P1...Pn) : R1 <: fun(Q1...Qn) : R2

[T-Variant]           V is a declared variant of U
                      ─────────────────────────────
                              V <: U

[T-Struct-Nominal]    s and t name the same declared struct
                      ───────────────────────────────────────
                                    s <: t

[T-Option-Cov]              S <: T
                      ─────────────────
                       option<S> <: option<T>

There is no clause any <: T. The downcast from the top is reachable only through an explicit as cast, which is checked by castOk (see MEP 10 A5) and guarded at runtime (§"The any cast" below).

Variance positions

The variance applied at each position in the surface syntax:

Construct	Position	Variance
let x: T = e	T against infer e	S <: T
var x: T = e	T against infer e	S <: T
x = e (assign)	inferred LHS, RHS	infer e <: T
fun f(p: T): R { ... return e }	T (param)	contravariant
fun f(p: T): R { ... return e }	R (result vs e)	infer e <: R
call f(e₁, ..., eₙ)	Pi	infer eᵢ <: Pᵢ
[T] element	read	covariant
[T] element	write	invariant
{K: V} key		invariant
{K: V} value		invariant
match e { p => r } arms	r joined	covariant
Tagged union variant	V <: U	covariant
option<T> element	read	covariant

The any cast

Casting toward any is always accepted at type check time. Casting away from any is accepted at type check time only via an explicit as and is checked at runtime.

[Cast-To-Any]                      [Cast-From-Any]
   ─────────────────                ──────────────────
   Γ ⊢ e as any : any                Γ ⊢ e as T : T

   where the runtime guard `assert dynType(e) <: T` is inserted at the
   cast site by the compiler. On guard failure the program raises
   `RuntimeError: cast from any to T but dynamic type was U`.

The runtime guard is in place at both runtimes (MEP-11.7, closed). The bytecode VM's OpCast calls castValue in runtime/vm/vm.go, which inspects the dynamic tag and aborts with a cannot cast %T to %s error when the underlying value does not match the named type. The tree-walking interpreter mirrors the same predicate via interpreter.applyCast and castValue in interpreter/runtime_utils.go. Both predicates recurse structurally through list<T>, map<K,V>, and named struct types, so a cast like xs as list<int> checks each element. Casts already covered by MEP 10 A5 (castOk) keep their compile-time rejection; the runtime guard catches the residual cases where the checker accepts the cast on type but cannot prove the dynamic tag.

Splitting unify

The post-MEP-11 contract:

• subtype(s, t Type) bool, defined here. Used at every variance position in §Variance positions.
• unify(s, t Type, sub Subst) (Subst, error), defined in MEP 12 MEP-12.1. Used only to resolve type variables during parametric inference. It does not consult the numeric tower, does not accept any in either direction, and does not perform variant subtyping. It performs structural recursion and TypeVar binding.
• equalTypes(s, t Type) bool, keeps its current meaning: structural equality on closed types, with the int/int64 carve-out removed in task #104.

Concretely, every call to unify in types/check.go is replaced. If the position is a variance position, it becomes subtype. If the position is a parametric-inference binding (introduced in MEP-12), it becomes unify with a substitution.

Fixtures

Every rule above is pinned by at least one fixture under tests/types/valid/ or tests/types/errors/.

Numeric tower:

• subtype_int_to_int64 (valid).
• subtype_int_to_bigint (valid).
• subtype_bigint_to_bigrat (valid).
• subtype_float_to_bigrat (valid).
• subtype_int64_to_float (valid).
• subtype_string_not_int (error T0xx).

Lists:

• variance_list_read_covariant (valid).
• variance_list_write_invariant (error). Closes MEP 10 B3.

Maps:

• variance_map_key_invariant (error).
• variance_map_value_invariant (error).

Functions:

• variance_fun_arg_contravariant (valid).
• variance_fun_result_covariant (valid).
• variance_fun_arg_covariant_rejected (error).
• variance_fun_result_contravariant_rejected (error).

Tagged unions:

• subtype_variant_to_union (valid).
• subtype_union_to_variant_via_cast (valid, requires as).
• subtype_union_to_variant_no_cast (error T046).

Option:

• subtype_option_element_covariant (valid). Depends on MEP 10 A2.

any:

• any_top_accepts_widen (valid: let x: any = 1).
• any_to_int_via_cast_runtime_ok (valid).
• any_to_int_via_cast_runtime_fail (runtime error).
• any_to_int_no_cast (error T0xx, replaces the previous any_top_silent_widen valid fixture).

Error codes

This MEP introduces:

• T055: type does not satisfy subtype obligation at variance position. Help text names the position (e.g. "list element write requires invariance") and prints the two types side by side.
• T056: implicit widening from any to non-any requires an as cast at this position.

Migration

Programs that compile today and rely on any flowing implicitly into a typed slot will fail with T056. The fix in user code is one of:

• Add the as T cast and accept the runtime guard.
• Tighten the producer's type so the value is not typed any to begin with.
• Replace with a typed alternative (most often, drop a generic builtin that was loosely typed to any before MEP-12.4).

Programs that aliased a let list into a var of a different element type fail at MEP-11.4. The migration is to copy explicitly with the new copy<T>([T]): [T] builtin (introduced in MEP-12.4 alongside the other parametric list builtins).

Rationale

Why split

Combining unification and subtyping is the standard textbook anti-pattern. Pierce, Types and Programming Languages, §22.4 notes that mixing the two in an ML-like checker leads to either an inferred result that depends on argument order, or to silent acceptance of an unsound program, or to both. Mochi has both pathologies today (see MEP 10 B2 and A1). The fix is structural: separate predicates, called from distinct positions.

Why not row polymorphism

Row polymorphism would give us structural width subtyping on records. Mochi has a nominal struct system today, and the language's idioms lean on it (type Point { x: int, y: int } is referred to by name throughout the program). Width subtyping would force a second concept of struct identity into the language; the cost is not worth the gain at v0.11.0. We leave the door open via the inline struct parameter case (deferred to the Open Questions section).

Why a runtime guard on the any cast

Statically rejecting every any -> T flow without an escape is too strict for interop. Code that consumes a value out of a json decode or a foreign call legitimately has an any in hand and a known target type. The runtime guard turns the unchecked cast into a checked cast: the program still has to declare the target type, the checker accepts the cast, and the runtime enforces it. This is the standard refinement-type pattern: static acceptance with dynamic enforcement.

The cost is a tag check per cast. We pay it because the alternative is either silent corruption (today) or banning interop (too strict).

Why no bounded quantification

T <: Comparable would let us write sort<T <: Comparable>(xs: [T]) and similar. We do not implement it because:

1. Mochi's surface for ordering is the numeric tower plus strings, both of which the checker already handles by special case.
2. The query layer's order by already resolves comparison at the operator level rather than at the type level.
3. Adding F-bounded quantification later does not invalidate the subtype predicate defined here.

This is the same reasoning Go applied through Go 1.17 and Java 1.4. The loss is real but small; the gain in implementation simplicity is large.

Backwards Compatibility

This is a breaking change. The break is intended.

The four breakages worth naming:

1. let x: int = anyVal (where anyVal : any) is rejected. Add as int.
2. let xs: [int] = [1, 2, 3] : [any] (covariant assignment) is rejected at the invariance position. Tighten the literal or copy.
3. let xs = listOfInt; var ys = xs; ys.push(...) (alias into var) is rejected at MEP-11.4. Copy explicitly.
4. fun f(g: fun(any): any): any accepting a fun(int): int is rejected at the contravariance check on g's parameter. Widen f's declared parameter to fun(int): any.

We accept these breaks because:

• The "perfect type system" directive supersedes backward compatibility.
• Each break is mechanical to fix and produces a clearer program.
• The fixtures pinned in this MEP make every break a deliberate, diff-visible change rather than a silent regression.

The pre-change behaviour is preserved in git log for archaeologists. It is not preserved in the codebase.

Reference Implementation

The subtype predicate, variance routing, and runtime guard live in:

• types/subtype.go (new). subtype(s, t Type) bool.
• types/check.go. Every variance position replaces unify with subtype. See MEP-11.2 for the position list.
• types/check.go cast site. The cast emits a CastInstr carrying the target type descriptor when the source type is any.
• runtime/vm/vm.go. OpCheckedCast consults the target descriptor and the dynamic tag.
• interpreter/interpreter.go. Mirror implementation for the interpreter backend.

Algorithm pseudocode

def subtype(s: Type, t: Type) -> bool:
    if isinstance(t, AnyType):
        return True
    if equal(s, t):
        return True
    if is_numeric(s) and is_numeric(t):
        return numeric_join(s, t) == t
    match (s, t):
        case (ListType(s0), ListType(t0)):
            # MEP-11.4: read covariant; write positions call equal
            return subtype(s0, t0)
        case (MapType(sk, sv), MapType(tk, tv)):
            return equal(sk, tk) and equal(sv, tv)
        case (FuncType(ps, r1), FuncType(qs, r2)):
            return (len(ps) == len(qs)
                    and all(subtype(q, p) for p, q in zip(ps, qs))
                    and subtype(r1, r2))
        case (variant_v, UnionType(u)) if variant_v in u.variants:
            return True
        case (OptionType(s0), OptionType(t0)):
            return subtype(s0, t0)
        case (StructType(name=a), StructType(name=b)):
            return a == b
    return False

equal is equalTypes post-int/int64 carve-out removal (task #104).

Performance

Subtype is invoked at every variance position and recurses into constructor children. For a program of n AST nodes, the total subtype work is O(n × d) where d is the maximum type depth. Typical Mochi programs have d ≤ 6. We do not memoize: the predicate is fast enough in practice and memoization complicates the fresh-TypeVar flow.

Open Questions

• Width subtyping for inline struct parameters. fun f(p: {x: int}) accepting any struct with at least field x would let the parser layer share field projection across many types. We defer; the same effect is reachable via a named alias today.
• Variant subtyping under casts. A match arm that binds a variant pattern gets the variant type. Whether to allow the bound name to flow back to the union type without an explicit upcast is a usability question; we leave the default as "yes, by T-Variant".
• Lossy float <: bigrat. The lattice listed under T-NumTower accepts a float as a bigrat, which loses precision. The alternative is to require an explicit cast. We pick acceptance because the bigrat side is the join used by the inference; programs that need exact rationals should declare bigrat at the boundary.
• Soft any removal. Once MEP-12.4 lands and most any usage is gone, we may further restrict as T from any to require an opt-in pragma. Out of scope for v0.11.0.

Reference Implementation

• types/check.go:148-387, current unify (to be split).
• types/infer.go, equalTypes (carve-out removal in task #104).
• types/check.go castOk, the type-check side of the as rule.

References

• Andrew Wright and Matthias Felleisen, "A Syntactic Approach to Type Soundness", Information and Computation, 1994.
• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002, chapters 15, 16, and 22.
• Luca Cardelli, "Type Systems", ACM Computing Surveys, 1996.
• Atsushi Igarashi, Benjamin C. Pierce, and Philip Wadler, "Featherweight Java", TOPLAS, 2001.

Copyright

This document is placed in the public domain.