Module ty 

Types, effect rows, unification, and the tier lattice.

docs/03-type-and-effect-system.md §3.1: “Hindley–Milner inference with bidirectional checking. Full inference inside bodies; mandatory annotations on public signatures.”

Phase 2’s change is §3.2: every function type carries an effect row, and the row is inferred. Ty::Fun therefore has three components, not two, and Subst unifies rows alongside types. The rows themselves live in crate::row; this module is where they meet the type system.

One deliberate omission remains, and it is named rather than implied: row polymorphism on records (§3.1). Models are nominal. Effect rows are polymorphic; record rows are not.

Re-exports

pub use crate::row::Ambient;

pub use crate::row::Effect;

pub use crate::row::Row;

pub use crate::row::RowVarId;

Structs

ImplSig

A published impl Trait for Type.

MethodSig

Scheme

A type scheme: forall vars rows. ty. Let-polymorphism over both dimensions, which is what §3.2 means by “effect polymorphism is what keeps one standard library”.

Subst

A unification variable’s binding, shared so that unifying in one place is visible everywhere.

TraitSig

A published trait: the signatures it requires, over an abstract Self.

Variant

Enums

Mismatch

Tier

Where code runs. §3.3’s table of what each tier can discharge.

Ty

TyDecl

A user-declared type: a model (record), a union (ADT), a newtype, or an alias.

Constants

CONCRETE_TIERS

The tiers a program can actually be placed on, in the order beck explain place reports them.

SCHEME_BASE

The base a declaration’s type parameters are numbered from.

Functions

instantiate_decl

Replace the positional parameters of a declaration with args.

Type Aliases

TyVarId