Subtyping Rules

Subtyping determines when one type can be used where another is expected. In verification mode, ordinary type compatibility is further constrained by ownership, heap identity, and contract preservation.

Overview

Sector9 uses structural subtyping. Two types are compatible based on their structure, not their names. If type A can safely substitute for type B, we write A <: B (read "A is a subtype of B").

Key principle: if A <: B, then any value of type A can be used where type B is expected.

Numeric Subtyping

Nat is a subtype of Int. Natural numbers automatically promote to integers:

subtype-nat-int.sr9

// Nat is a subtype of Int - automatic promotion
import Nat "mo:core/Nat";

module {
  // Nat values automatically work where Int is expected
  public func processInt(x : Int) : Int { x * 2 };

  public func example() : Int {
    let n : Nat = 42;
    processInt(n)  // OK: Nat promoted to Int
  };

  // Int to Nat requires proof of non-negativity
  public pure func toNat(x : Int) : Nat
    requires x >= 0;
  {
    Nat.fromInt(x)
  };
}

The promotion is asymmetric:

• Nat to Int: Automatic. Every Nat is a valid Int.
• Int to Nat: Requires an explicit conversion such as Nat.fromInt(x) or Int.toNat(x), plus a proof or runtime guard that x >= 0.

When combining Nat and Int in expressions, the result type is Int.

Record Subtyping (Width and Depth)

Records support width subtyping: a record with more fields is a subtype of one with fewer fields.

subtype-record-width.sr9

// Record width subtyping: more fields -> fewer fields
module {
  type Point2D = { x : Int; y : Int };
  type Point3D = { x : Int; y : Int; z : Int };

  // A function expecting Point2D
  public pure func getX(p : Point2D) : Int { p.x };

  // Point3D can be passed where Point2D is expected
  public func example() : Int {
    let p3d : Point3D = { x = 1; y = 2; z = 3 };
    getX(p3d)  // OK: Point3D has all fields of Point2D
  };

  // Extra fields are ignored
  public pure func project(p : Point3D) : Point2D {
    p  // OK: Point3D <: Point2D
  };
}

Width subtyping rules:

• Extra fields in the source type are allowed
• All required fields must be present
• Field names must match exactly (order does not matter)
• Field types must be compatible (covariant)

Depth subtyping: Field types themselves follow subtyping rules. If { x : Nat } is expected and you provide { x : Nat; y : Int }, the x field's Nat type is checked against the expected Nat.

Mutability restriction: A var field cannot substitute for an immutable field or vice versa. Mutability is part of the field's type.

Variant Subtyping

Variants support subtyping in the opposite direction from records: a variant with fewer cases is a subtype of one with more cases.

subtype-variant.sr9

// Variant subtyping: fewer cases -> more cases
module {
  type Shape = { #circle : Nat; #square : Nat; #triangle : Nat };
  type SimpleShape = { #circle : Nat; #square : Nat };

  // A SimpleShape can be used where Shape is expected
  public pure func describe(s : Shape) : Nat {
    switch s {
      case (#circle r) { r };
      case (#square s) { s };
      case (#triangle t) { t };
    }
  };

  public func example() : Nat {
    let simple : SimpleShape = #circle(5);
    describe(simple)  // OK: SimpleShape <: Shape
  };
}

Variant subtyping rules:

• The subtype can have fewer cases than the supertype
• All cases in the subtype must exist in the supertype
• Payload types are covariant (follow normal subtyping)

This makes sense: a value that can only be #circle or #square is safe to use where #circle, #square, or #triangle might be expected.

Function Subtyping

Functions follow the standard variance rules:

• Parameters are contravariant: The subtype can accept a wider input type
• Return types are covariant: The subtype can return a narrower output type

subtype-function.sr9

// Function subtyping: contravariant parameters, covariant returns
module {
  // A function accepting Int can be used where Nat->() is expected
  // because Int :> Nat (caller passes Nat, function accepts wider Int)
  public func example1() : Nat -> () {
    let f : Int -> () = func (x : Int) {};
    f  // OK: (Int -> ()) <: (Nat -> ())
  };

  // A function returning Nat can be used where ()->Int is expected
  // because Nat <: Int (function returns Nat, caller expects Int)
  public func example2() : () -> Int {
    let f : () -> Nat = func () : Nat { 42 };
    f  // OK: (() -> Nat) <: (() -> Int)
  };
}

Why contravariance for parameters?

If you have a function f : Int -> () and need a Nat -> (), this works because:

1. The caller will pass a Nat
2. Your function accepts Int, which includes all Nat values
3. The function handles the input safely

Why covariance for returns?

If you have a function f : () -> Nat and need a () -> Int, this works because:

1. Your function returns a Nat
2. The caller expects an Int
3. Every Nat is a valid Int

Contract-Aware Subtyping (Verification)

When function types carry contracts, verification uses logical implication:

• requires is contravariant
• ensures is covariant

A function value can only be coerced to a contract-bearing type if the contract is satisfied by implication. Contracts are not silently dropped when the expected type has contracts.

Option Subtyping

null is a subtype of every option type. Options are covariant in their element type.

subtype-option.sr9

// Option subtyping: null is subtype of all option types
module {
  // null can be assigned to any option type
  public func examples() {
    let _a : ?Nat = null;   // OK: Null <: ?Nat
    let _b : ?Text = null;  // OK: Null <: ?Text
    let _c : ?Int = null;   // OK: Null <: ?Int
  };

  // Options are covariant in their element type
  public pure func promote(x : ?Nat) : ?Int {
    x  // OK: ?Nat <: ?Int because Nat <: Int
  };
}

Option subtyping rules:

• Null <: ?T for any type T
• ?A <: ?B when A <: B

Top and Bottom Types

Any is the top type - every type is a subtype of Any. None is the bottom type - it is a subtype of every type.

subtype-top-bottom.sr9

// Top and bottom types: Any and None
module {
  // Any is the top type - supertype of everything
  public pure func toAny(x : Nat) : Any { x };
  public pure func recordToAny(r : { a : Int }) : Any { r };

  // None is the bottom type - subtype of everything
  // None has no values, so functions returning None never return
  public func fromNone(x : None) : Int { x };
  public func noneToRecord(x : None) : { a : Int } { x };
}

Use cases:

• Any: Accepting values of unknown type at API boundaries where you do not need to inspect them later
• None: Functions that never return (infinite loops, always trap)

Limitation: You cannot pattern match on Any because the original type information is lost.

Arrays, Tuples, and Mutable Identity

Immutable arrays and tuples are covariant in the ordinary type relation:

• [A] <: [B] when A <: B
• (A1, A2) <: (B1, B2) when each Ai <: Bi

Mutable element positions are different. [var T] is represented as an array whose element type is mutable, and mutable types require exact equality. A [var Nat] cannot be used as [var Int], because writing -1 through the wider view would corrupt the original array.

Verification adds another restriction: even an immutable array carries heap identity. A coercion such as [Nat] to [Int] is rejected in verified code with M0339, because it is a structural coercion involving array identity.

Rejected

subtype-invariant_reject.sr9

// Verified structural coercions cannot hide array or mutable identity.
module {
  // Immutable arrays are covariant in ordinary type checking, but verified code
  // rejects this coercion because arrays carry heap identity.
  public func arrayFail() {
    let arr : [Nat] = [1, 2, 3];
    let x : [Int] = arr;  // REJECT: M0339, array identity coercion
  };

  // Mutable element types require exact compatibility.
  public func mutableArrayFail() {
    let arr : [var Nat] = [var 1, 2, 3];
    let x : [var Int] = arr;  // REJECT: M0339, mutable array identity coercion
  };
}

Tuples do not carry heap identity by themselves, so covariant tuple coercions are allowed unless one of the element coercions is itself forbidden by verification.

Subtyping Summary Table

Type	Variance	Rule
Nat / Int	—	Nat <: Int
Records	Width + Depth	More fields <: fewer fields; fields covariant
Variants	Width + Depth	Fewer cases <: more cases; payloads covariant
Functions	Mixed	Parameters contravariant; returns covariant
Options	Covariant	?A <: ?B when A <: B; Null <: ?T
Immutable arrays	Covariant in type checking; restricted in verification	[A] <: [B] when A <: B; verified structural coercions involving arrays are rejected
Mutable arrays	Invariant element type	[var A] and [var B] require exact mutable element compatibility
Tuples	Covariant	Same arity; elements subtype position-by-position
Any	Top	T <: Any for all T
None	Bottom	None <: T for all T

Verification Mode Restrictions

Verification adds stricter rules for structural subtyping:

• Records/modules: Structural subtyping is allowed only for spec-immutable types (no var fields, arrays, functions, actors, modules, or async/async* values). Error M0338.
• Mutable identity: Structural coercions involving arrays, mutable records, mutable fields, actor references, mixins, or memory objects are rejected. Error M0339.

These restrictions keep ownership and framing sound when code is verified. When a coercion is rejected, prefer an explicit immutable snapshot, a spec collection model, or a function contract that states the relationship you need.

Common Errors

M0096: Expression cannot produce expected type

expression of type { x : Nat; y : Nat }
cannot produce expected type { x : Nat; y : Nat; z : Nat }

The source type has fewer fields than required. Width subtyping only works when the source has more fields.

M0200: Cannot decide subtyping

cannot decide subtyping between type A and B

The type checker cannot determine if a subtype relationship exists. This often happens with complex recursive types.

Summary

• Sector9 uses structural subtyping based on type structure, not names
• Nat <: Int - natural numbers promote to integers automatically
• Records: more fields is a subtype of fewer fields (width subtyping)
• Variants: fewer cases is a subtype of more cases
• Functions: contravariant in parameters, covariant in returns
• Options: covariant; null is subtype of all option types
• Immutable arrays and tuples are covariant in the type relation
• Verification rejects structural coercions that involve array or mutable identity
• Any is top type; None is bottom type

Related Topics

• Verified subtyping for the verification-specific rules
• Function type contracts for contract-aware function subtyping
• Reads and modifies for the framing rules behind heap-identity restrictions