MEP 11. Subtyping and Variance

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

Abstract

Mochi has a small subtyping relation today and an unfortunate unify that treats any as a top type in both directions. This MEP proposes a clean subtype(s, t) predicate that matches the standard variance rules and replaces the loose any behaviour with a deliberate cast at the boundary.

Motivation

The current unify plays two roles: structural unification of type variables and ad-hoc subtyping. The conflation makes both jobs harder. A separate subtype predicate, called from the positions where subtyping is intended, lets us state the rules clearly and lets unify focus on substitution.

Specification

The relation

Define S <: T to mean S is acceptable wherever T is expected. The intended rules:

T <: any
S <: any
any <: T                (only by explicit cast)

int <: int
int <: int64            (numeric promotion)
int <: bigint           (numeric promotion)
int <: bigrat
int <: float
int64 <: bigint
int64 <: float
bigint <: bigrat
float <: bigrat         (lossy, but the inference uses bigrat as the join)

[S] <: [T]              if S <: T  (read only positions)
[S] = [T]               if S = T   (read write positions, after MEP 10 A3 lands)
{K1: V1} = {K2: V2}     if K1 = K2 and V1 = V2
fun(P1...) : R1 <: fun(Q1...) : R2
                        if Pi <: Qi (contravariance flipped) and R1 <: R2
struct named N <: struct named N
union named U <: union named U
variant V of U <: U     for every variant V declared in U

The "any in either direction" rule we have today violates several of the above, but it is what unify does at the moment.

Variance positions

Positions where types appear and the variance applied at each:

Construct	Position	Variance
let x: T = e	T	invariant
var x: T = e	T	invariant
fun(p: T) : R	T (param)	contravariant
fun(p: T) : R	R (result)	covariant
[T] element	read	covariant
[T] element	write	invariant
{K: V} key		invariant
{K: V} value		invariant
match e { p => r } arms	r	covariant
Tagged union variant	V <: U	covariant

Width subtyping (proposed)

Records do not have width subtyping today. We do not propose adding it broadly, because the language is nominal. The exceptions we want:

• Struct literal under a hint. let p: Point = {x: 1, y: 2}. The hint drives validation. Width is required to match exactly today and we keep that.
• Inline struct types in function parameters. fun f(p: {x: int, y: int}) accepts any value whose runtime shape includes the listed fields. Today the inline struct must match exactly. Width subtyping here would let callers pass richer records. We mark it as future work.

any cast in either direction

Casting to any should always succeed at type check time: it is the top type. Casting from any should be limited:

• any as T should be accepted at type check time, with a runtime guard that raises a typed runtime error if the dynamic type does not match.
• Casts among numeric types should be accepted at type check time and should perform the documented coercion at runtime.
• Casts among unrelated types (int as string, string as bool) should be rejected.

The runtime guard is on the roadmap. A cleaner design is in MEP 10 A5.

How the checker computes subtyping

Today the only subtyping logic is inside unify and equalTypes. We want a proper subtype(s, t) predicate. Implementation sketch:

subtype(s, t):
  if t is AnyType: true
  if s is t (structural): true
  if s and t both numeric: lattice ordering
  if s = ListType{S0} and t = ListType{T0} (read only): subtype(S0, T0)
  if s = MapType{Sk, Sv} and t = MapType{Tk, Tv}: equal(Sk, Tk) and equal(Sv, Tv)
  if s = FuncType{Pi, R1} and t = FuncType{Qi, R2}:
        all i. subtype(Qi, Pi) and subtype(R1, R2)
  if s is a variant of t: true
  otherwise: false

Replace direct calls to unify with subtype at the positions where subtyping is intended (assignment context, argument passing, return of inner block matching outer signature).

unify keeps its role: it is the substitution resolver for type variables. It should not be confused with subtyping.

Fixture obligations

For each rule above, fixtures live under tests/types/valid/ and tests/types/errors/.

Numeric tower fixtures:

• subtype_int_to_int64 (valid).
• subtype_int_to_bigint (valid).
• subtype_bigint_to_bigrat (valid).
• subtype_float_unrelated_to_bigint (valid: result widens to bigrat).
• subtype_string_not_int (error).

List variance fixtures:

• variance_list_read_covariant (valid, snapshots current behaviour).
• variance_list_write_invariant (error, after MEP 10 A3 lands).

Map invariance fixtures:

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

Function variance fixtures:

• variance_fun_arg_contravariant (valid, after fix).
• variance_fun_result_covariant (valid, after fix).
• variance_fun_arg_covariant_rejected (error).

Tagged union variance fixtures:

• subtype_variant_to_union (valid).
• subtype_union_to_variant_via_cast (valid via as, with runtime guard).

any escape hatch fixtures:

• any_top_silent_widen (valid, snapshots current loose behaviour).
• any_to_int_via_cast (valid, after the cast tightening lands).
• any_to_int_no_cast (error, after the cast tightening lands).

Rationale

Splitting subtype from unify is the smallest refactor that lets us reason about the two distinct relationships independently. The variance table is standard. We choose nominal record subtyping because it matches the structural identity that StructType already carries through its Name field.

We accept lossy float <: bigrat because the alternative is forcing every numeric mix to widen to a non-comparable join. Programs that care about precision should declare types explicitly and not rely on the default join.

Backwards Compatibility

Tightening any to require an explicit cast is a breaking change. Programs that rely on the current "any in either direction" behaviour will fail to type-check. We pin the current behaviour in any_top_silent_widen and document the migration in this MEP.

Adding the runtime guard for any as T is a behavioural change rather than a type-check change. Programs that previously crashed in unspecified ways now raise a typed runtime error.

Reference Implementation

• types/check.go:148-387 — current unify.
• types/infer.go — current equalTypes.
• types/check.go:1687-1688 — current as cast (no compatibility check).

Open Questions

• Lossy float to bigrat. Whether to include this in the lattice or to require an explicit cast.
• Width subtyping for inline struct parameters. Adopt or defer.
• Bounded quantification. TAPL chapter 26. Out of scope for v0.11.0; revisit when sorted query support generalises beyond numeric and string ordering.

References

• Benjamin C. Pierce, Types and Programming Languages, chapters 15 and 26.

Copyright

This document is placed in the public domain.