Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity
Files
ee4107c721b8243155a15d5577bb18a56246b04b
AILang/crates/ailang-check/src/lib.rs
T
Brummel ee4107c721 fix(check): honour the written element type-arg on polymorphic (new T …) 
A `(new RawBuf (con Int) 3)` whose buffer is never observed by a later
get/set passed `ail check` but crashed `ail build` with
`RawBuf_new__Unit has no registered intercept`, and a forbidden
`(new RawBuf (con Unit) 3)` was wrongly accepted at check. Both legs
share one root: the `Term::New` desugar discarded the author's written
`NewArg::Type` before anything could use it.

This was never an inference problem. The element type is EXPLICITLY
known — the author wrote `(con Int)`. The defect was that the desugar
threw that known type away and relied on re-discovering it from
downstream use; with no use (size-only), `RawBuf.new`'s result-only
forall var stayed unpinned, mono Unit-defaulted it, and codegen aborted
on the unregistered `RawBuf_new__Unit` intercept. The fix USES the
written type instead of inferring it.

Mechanism:
- desugar.rs: a polymorphic `(new T <elem> …)` (carrying a written
  `NewArg::Type`) now SURVIVES into check instead of being lowered to
  `(app T.new …)`. A monomorphic `(new Counter 42)` (no type-arg) keeps
  the raw-buf.4 app-lowering unchanged.
- lib.rs synth `Term::New` arm: (a) validates the written element type
  against the constructed type's `param_in` set via
  `check_type_well_formed`, firing `ParamNotInRestrictedSet` naming the
  forbidden element (leg 2) — synth is the correct site because it has
  Env/registry access, unlike `pre_desugar_validation`; (b) binds the
  result-only forall var DIRECTLY to the written type (`?a := Int`, a
  trivial binding, no inference channel) by pushing a `FreeFnCall` whose
  metas are the written concrete types, so mono mints
  `RawBuf_new__<elem>` and never `__Unit`.
- mono.rs: `rewrite_mono_calls` and `interleave_slots` gain matching
  `Term::New` arms that each consume exactly one free-fn slot at a
  type-arg-bearing `Term::New` (mirroring synth's single observation,
  pushed before the value-args), and `rewrite_mono_calls` reduces the
  node to `(app <mangled> <value-args>)` so codegen never sees
  `Term::New` and the lib.rs:2200 `unreachable!` stays valid. The two
  walkers stay in lockstep.

The Unit-default policy in mono stays correct for genuinely-unobservable
vars (`is_empty(Nil)` etc.); only the case with a written `NewArg::Type`
is changed.

Alternatives rejected: an additive `type_args` field on `Term::App`
(~100 construction sites across 7 crates — a detour that builds a new
transport slot only to copy the already-known type into it); a runtime
type-witness parameter on `RawBuf.new` (invents a runtime value for a
pure type property); an identity-lambda wrapper carrying the element in
its param-type (hides a semantic property in a runtime construct). The
written type belongs where the author put it, carried to the one point
that consumes it.

Verification: both RED legs (committed 61b9d3f) now green; full
check/codegen/core/surface suites green; intercepts bijection and
hash-pin tests green; existing raw-buf int/float/bool fixtures still
build and run leak-clean (live=0).

Out of scope (pre-existing at HEAD, separate issue): a monomorphic
`(new Counter 42)` over a user ADT fails with `unknown variable:
Counter.new` — unrelated to the type-arg drop fixed here.

closes #51
2026-05-31 03:03:14 +02:00

8506 lines
369 KiB
Rust
Raw Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
//! Typechecker for AILang (MVP).
//!
//! Sits between `ailang-core` (AST + canonical JSON + content hash) and
//! `ailang-codegen` (LLVM IR emit) in the pipeline `core → check →
//! codegen → ail`. Top-level entry points: [`check_module`] (one module,
//! returns [`Diagnostic`]s), [`check_workspace`] (multi-module), and
//! [`check`] (single-error legacy form returning a [`CheckedModule`]).
//!
//! HM with explicit top-level polymorphism. All top-level defs must carry
//! their full type annotation; lambda bodies inside defs are checked
//! monomorphically against their declared types. Polymorphism is opt-in
//! via `Type::Forall { vars, body }` at top-level def types and is
//! instantiated at every use site (the textbook ML rule).
//!
//! Effects are propagated as a set and reconciled against the annotation
//! on the function type.
//!
//! Built-in operations are resolved via the [`builtins`] table installed
//! into every fresh [`Env`].
//!
//! ## Internals
//!
//! Type variables come in two flavours during checking:
//! - **Rigid vars** — universally quantified vars from a `Forall` that
//! end up in scope while checking a polymorphic def's body. They are
//! `Type::Var { name: "<name>" }` where `<name>` is the source-level
//! name (`a`, `b`, ...). They unify only with themselves.
//! - **Metavars** — fresh placeholders for instantiated forall vars at
//! use sites. Encoded inside the existing `Type::Var` as
//! `Type::Var { name: "$m<id>" }`. The naming convention keeps the AST
//! schema untouched (no new variant, hashes stay stable). Source-level
//! names cannot collide with the `$m` prefix because identifiers may
//! not start with `$`.
use ailang_core::ast::*;
use ailang_core::Workspace;
use indexmap::IndexMap;
use std::collections::{BTreeMap, BTreeSet};
mod linearity;
mod pre_desugar_validation;
mod reuse_shape;
mod suppress_filter;
pub mod uniqueness;
/// Metavariable substitution. Maps fresh metavar ids (from `$m<id>` in
/// `Type::Var.name`) to the type they have been unified against.
#[derive(Debug, Default, Clone)]
pub struct Subst {
map: BTreeMap<u32, Type>,
}
impl Subst {
/// Allocates a fresh metavar. The counter is owned by the caller so
/// that ids stay deterministic across `synth` calls within one
/// def-check.
fn fresh(counter: &mut u32) -> Type {
let id = *counter;
*counter += 1;
Type::Var { name: format!("$m{id}") }
}
/// `Some(id)` iff the var name is the metavar encoding `$m<id>`.
fn meta_id(name: &str) -> Option<u32> {
name.strip_prefix("$m").and_then(|s| s.parse::<u32>().ok())
}
fn lookup(&self, id: u32) -> Option<&Type> {
self.map.get(&id)
}
fn extend(&mut self, id: u32, t: Type) {
self.map.insert(id, t);
}
/// Walks `t`, replacing every metavar with its current binding (if
/// any) — recursively so chains collapse. Rigid vars and concrete
/// types pass through unchanged.
pub fn apply(&self, t: &Type) -> Type {
match t {
Type::Var { name } => {
if let Some(id) = Self::meta_id(name) {
if let Some(bound) = self.lookup(id) {
return self.apply(&bound.clone());
}
}
Type::Var { name: name.clone() }
}
Type::Con { name, args } => Type::Con {
name: name.clone(),
args: args.iter().map(|a| self.apply(a)).collect(),
},
Type::Fn { params, ret, effects, .. } => Type::Fn {
params: params.iter().map(|p| self.apply(p)).collect(),
ret: Box::new(self.apply(ret)),
effects: effects.clone(),
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
Type::Forall { vars, constraints, body } => Type::Forall {
vars: vars.clone(),
constraints: constraints.clone(),
body: Box::new(self.apply(body)),
},
}
}
}
/// Replaces every var named in `vars` inside `body` with a fresh metavar.
/// Used at use sites to instantiate a `Forall` type. Returns the
/// instantiated body and the parallel list of fresh metavars (one per
/// forall var, same order) — useful for codegen monomorphisation.
fn instantiate(forall_vars: &[String], body: &Type, counter: &mut u32) -> (Vec<Type>, Type) {
let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
let mut metas: Vec<Type> = Vec::with_capacity(forall_vars.len());
for v in forall_vars {
let m = Subst::fresh(counter);
mapping.insert(v.clone(), m.clone());
metas.push(m);
}
(metas, substitute_rigids(body, &mapping))
}
/// Substitutes named rigid vars throughout a type (used by
/// `instantiate`). Unlike `Subst::apply`, this targets vars by name —
/// it has no notion of metavar ids.
pub(crate) fn substitute_rigids(t: &Type, mapping: &BTreeMap<String, Type>) -> Type {
match t {
Type::Var { name } => mapping.get(name).cloned().unwrap_or_else(|| t.clone()),
Type::Con { name, args } => Type::Con {
name: name.clone(),
args: args.iter().map(|a| substitute_rigids(a, mapping)).collect(),
},
Type::Fn { params, param_modes, ret, ret_mode, effects } => Type::Fn {
params: params.iter().map(|p| substitute_rigids(p, mapping)).collect(),
ret: Box::new(substitute_rigids(ret, mapping)),
effects: effects.clone(),
// 2026-05-14 bugfix-print-leak-show-ret-mode: preserve
// param_modes and ret_mode through rigid substitution.
// The earlier `..` discarded both and hard-reset to
// Implicit, which silently stripped the Show class
// method's `ret_mode: Own` (declared in
// `examples/prelude.ail.json`) when mono synthesised
// `show__Int` via `synthesise_mono_fn`'s
// `substitute_rigids(&class_method.ty, …)`. Codegen's
// `is_rc_heap_allocated` App-arm then declined to track
// print's `let s = show x` binder, leaking the heap-Str.
param_modes: param_modes.clone(),
ret_mode: *ret_mode,
},
Type::Forall { vars, constraints, body } => {
// Inner forall shadows: only substitute vars not re-bound here.
let inner: BTreeMap<String, Type> = mapping
.iter()
.filter(|(k, _)| !vars.contains(k))
.map(|(k, v)| (k.clone(), v.clone()))
.collect();
Type::Forall {
vars: vars.clone(),
constraints: constraints.clone(),
body: Box::new(substitute_rigids(body, &inner)),
}
}
}
}
/// substitute named rigid vars throughout a `Term`,
/// recursing into every sub-Term and applying [`substitute_rigids`]
/// to every embedded `Type` (in `Term::Lam.param_tys`,
/// `Term::Lam.ret_ty`). All other Term variants carry no inline
/// types and recurse structurally.
///
/// Used by `mono::synthesise_mono_fn_for_free_fn` to specialise a
/// polymorphic free-fn body for a specific instantiation. The
/// class-method arm doesn't need this — instance bodies are
/// Lam-unwrapped during synthesis, dropping their `param_tys` —
/// but a free-fn body may carry arbitrary nested Lams whose
/// `param_tys` reference the outer Forall vars.
pub(crate) fn substitute_rigids_in_term(t: &Term, mapping: &BTreeMap<String, Type>) -> Term {
use ailang_core::ast::Arm;
match t {
Term::Lit { .. } | Term::Var { .. } => t.clone(),
Term::App { callee, args, tail } => Term::App {
callee: Box::new(substitute_rigids_in_term(callee, mapping)),
args: args.iter().map(|a| substitute_rigids_in_term(a, mapping)).collect(),
tail: *tail,
},
Term::Let { name, value, body } => Term::Let {
name: name.clone(),
value: Box::new(substitute_rigids_in_term(value, mapping)),
body: Box::new(substitute_rigids_in_term(body, mapping)),
},
Term::LetRec { name, ty, params, body, in_term } => Term::LetRec {
name: name.clone(),
ty: substitute_rigids(ty, mapping),
params: params.clone(),
body: Box::new(substitute_rigids_in_term(body, mapping)),
in_term: Box::new(substitute_rigids_in_term(in_term, mapping)),
},
Term::If { cond, then, else_ } => Term::If {
cond: Box::new(substitute_rigids_in_term(cond, mapping)),
then: Box::new(substitute_rigids_in_term(then, mapping)),
else_: Box::new(substitute_rigids_in_term(else_, mapping)),
},
Term::Do { op, args, tail } => Term::Do {
op: op.clone(),
args: args.iter().map(|a| substitute_rigids_in_term(a, mapping)).collect(),
tail: *tail,
},
Term::Ctor { type_name, ctor, args } => Term::Ctor {
type_name: type_name.clone(),
ctor: ctor.clone(),
args: args.iter().map(|a| substitute_rigids_in_term(a, mapping)).collect(),
},
Term::Match { scrutinee, arms } => Term::Match {
scrutinee: Box::new(substitute_rigids_in_term(scrutinee, mapping)),
arms: arms
.iter()
.map(|a| Arm {
pat: a.pat.clone(),
body: substitute_rigids_in_term(&a.body, mapping),
})
.collect(),
},
Term::Lam { params, param_tys, ret_ty, effects, body } => Term::Lam {
params: params.clone(),
param_tys: param_tys
.iter()
.map(|t| substitute_rigids(t, mapping))
.collect(),
ret_ty: Box::new(substitute_rigids(ret_ty, mapping)),
effects: effects.clone(),
body: Box::new(substitute_rigids_in_term(body, mapping)),
},
Term::Seq { lhs, rhs } => Term::Seq {
lhs: Box::new(substitute_rigids_in_term(lhs, mapping)),
rhs: Box::new(substitute_rigids_in_term(rhs, mapping)),
},
Term::Clone { value } => Term::Clone {
value: Box::new(substitute_rigids_in_term(value, mapping)),
},
Term::ReuseAs { source, body } => Term::ReuseAs {
source: Box::new(substitute_rigids_in_term(source, mapping)),
body: Box::new(substitute_rigids_in_term(body, mapping)),
},
Term::Loop { binders, body } => Term::Loop {
binders: binders
.iter()
.map(|b| ailang_core::ast::LoopBinder {
name: b.name.clone(),
ty: substitute_rigids(&b.ty, mapping),
init: substitute_rigids_in_term(&b.init, mapping),
})
.collect(),
body: Box::new(substitute_rigids_in_term(body, mapping)),
},
Term::Recur { args } => Term::Recur {
args: args
.iter()
.map(|a| substitute_rigids_in_term(a, mapping))
.collect(),
},
Term::New { type_name, args } => Term::New {
type_name: type_name.clone(),
args: args
.iter()
.map(|arg| match arg {
NewArg::Value(v) => NewArg::Value(substitute_rigids_in_term(v, mapping)),
NewArg::Type(t) => NewArg::Type(substitute_rigids(t, mapping)),
})
.collect(),
},
Term::Intrinsic => t.clone(),
}
}
/// Returns true if metavar `id` occurs in `t` (after applying the
/// current substitution). Used as the occurs check during unification.
fn occurs(id: u32, t: &Type, subst: &Subst) -> bool {
let t = subst.apply(t);
match &t {
Type::Var { name } => Subst::meta_id(name) == Some(id),
Type::Con { args, .. } => args.iter().any(|a| occurs(id, a, subst)),
Type::Fn { params, ret, .. } => {
params.iter().any(|p| occurs(id, p, subst)) || occurs(id, ret, subst)
}
Type::Forall { body, .. } => occurs(id, body, subst),
}
}
/// Unifies two types under the current substitution. Symmetric. Extends
/// the substitution as needed, with the standard occurs check.
fn unify(a: &Type, b: &Type, subst: &mut Subst) -> Result<()> {
let a = subst.apply(a);
let b = subst.apply(b);
match (&a, &b) {
// Metavar unification — bind the metavar to the other side.
(Type::Var { name }, _) if Subst::meta_id(name).is_some() => {
let id = Subst::meta_id(name).unwrap();
if let Type::Var { name: bn } = &b {
if Subst::meta_id(bn) == Some(id) {
return Ok(()); // same metavar, done
}
}
if occurs(id, &b, subst) {
return Err(CheckError::TypeMismatch {
expected: ailang_core::pretty::type_to_string(&a),
got: ailang_core::pretty::type_to_string(&b),
});
}
subst.extend(id, b);
Ok(())
}
(_, Type::Var { name }) if Subst::meta_id(name).is_some() => {
let id = Subst::meta_id(name).unwrap();
if occurs(id, &a, subst) {
return Err(CheckError::TypeMismatch {
expected: ailang_core::pretty::type_to_string(&a),
got: ailang_core::pretty::type_to_string(&b),
});
}
subst.extend(id, a);
Ok(())
}
// Rigid vars: only unify with the same name.
(Type::Var { name: an }, Type::Var { name: bn }) if an == bn => Ok(()),
// Concrete con: same name and same arity, then unify args
// pointwise. Iter 13a: parameterised ADTs unify arg-by-arg.
(
Type::Con { name: an, args: aa },
Type::Con { name: bn, args: ba },
) if an == bn && aa.len() == ba.len() => {
for (x, y) in aa.iter().zip(ba.iter()) {
unify(x, y, subst)?;
}
Ok(())
}
// Function types: zip params, unify ret, effects must match as a set.
(
Type::Fn { params: ap, ret: ar, effects: ae, .. },
Type::Fn { params: bp, ret: br, effects: be, .. },
) => {
if ap.len() != bp.len() {
return Err(CheckError::TypeMismatch {
expected: ailang_core::pretty::type_to_string(&a),
got: ailang_core::pretty::type_to_string(&b),
});
}
for (x, y) in ap.iter().zip(bp.iter()) {
unify(x, y, subst)?;
}
unify(ar, br, subst)?;
let mut ae = ae.clone();
let mut be = be.clone();
ae.sort();
be.sort();
if ae != be {
return Err(CheckError::TypeMismatch {
expected: ailang_core::pretty::type_to_string(&a),
got: ailang_core::pretty::type_to_string(&b),
});
}
Ok(())
}
_ => Err(CheckError::TypeMismatch {
expected: ailang_core::pretty::type_to_string(&a),
got: ailang_core::pretty::type_to_string(&b),
}),
}
}
pub mod builtins;
pub mod diagnostic;
pub mod lift;
pub mod mono;
pub use diagnostic::{Diagnostic, Severity};
pub use lift::lift_letrecs;
pub use mono::monomorphise_workspace;
/// Internal error type produced by the typechecker.
///
/// One variant per stable diagnostic code (see [`CheckError::code`]). The
/// [`CheckError::Def`] wrapper attaches the name of the def in which the
/// inner error was raised — recursive accessors ([`CheckError::code`],
/// [`CheckError::ctx`], [`CheckError::message`]) transparently see
/// through the wrapping.
///
/// Typically this enum is converted to [`Diagnostic`] via
/// [`CheckError::to_diagnostic`] before crossing the crate boundary;
/// public API functions [`check_module`] and [`check_workspace`] already
/// return `Vec<Diagnostic>`.
#[derive(Debug, thiserror::Error)]
pub enum CheckError {
/// Wraps an inner error with the name of the def it occurred in. The
/// inner error carries the actual code and ctx; the wrapper only the
/// def context that is later projected onto [`Diagnostic::def`].
#[error("def `{0}`: {1}")]
Def(String, Box<CheckError>),
/// Two types failed to unify. Code: `type-mismatch`.
#[error("type mismatch: expected {expected}, got {got}")]
TypeMismatch { expected: String, got: String },
/// A `Term::Var { name }` could not be resolved against locals,
/// globals, or the qualified-import path. Code: `unbound-var`.
#[error("unknown identifier: `{0}`")]
UnknownIdent(String),
/// `Term::Do { op }` referenced an op not in
/// [`Env::effect_ops`]. Code: `unknown-effect-op`.
#[error("unknown effect operation: `{0}`")]
UnknownEffectOp(String),
/// A non-function value was applied with `Term::App`. Code:
/// `not-a-function`.
#[error("`{0}` is not a function (got {1})")]
NotAFunction(String, String),
/// Wrong number of args at a call site. Code: `arity-mismatch`.
#[error("arity mismatch for `{name}`: expected {expected} args, got {got}")]
ArityMismatch {
name: String,
expected: usize,
got: usize,
},
/// An effect was raised in a body but not listed on the enclosing
/// fn's effect row. Code: `undeclared-effect`.
#[error("undeclared effect `{0}` used in body")]
UndeclaredEffect(String),
/// A `Def::Fn` was declared with a non-`Type::Fn` (and non-`Forall<Fn>`)
/// type. Code: `fn-type-required`.
#[error("function type required for fn `{0}`, got {1}")]
FnTypeRequired(String, String),
/// `FnDef.params.len()` does not match the parameter list of
/// `FnDef.ty`. Code: `param-count-mismatch`.
#[error("param count mismatch in `{name}`: type has {ty_count}, params has {param_count}")]
ParamCountMismatch {
name: String,
ty_count: usize,
param_count: usize,
},
/// A `Type::Forall` showed up where the MVP doesn't support
/// generalisation (e.g. inside `Def::Const`). Code:
/// `polymorphic-not-supported`.
#[error("polymorphic types not supported in MVP body of `{0}`")]
PolymorphicNotSupported(String),
/// A `Def::Const` body raised an effect — illegal because consts are
/// pure by construction. Code: `const-has-effects`.
#[error("const `{0}` may not have effects (got !{1:?})")]
ConstHasEffects(String, Vec<String>),
/// An `(export …)` fn has a parameter or return type that is not
/// a permitted embedding-ABI type. The embedding ABI is frozen as
/// of M3 (design/contracts/0003-embedding-abi.md):
/// `Int`/`Float` or a single-constructor record of those; every
/// other shape (multi-ctor sums, `Str`/`List`/nested-record
/// fields) is rejected at typecheck (the feature-acceptance
/// clause-3 discriminator, in code).
/// Code: `export-non-scalar-signature`.
#[error("export `{0}`: embedding ABI accepts `Int`/`Float` or a single-constructor record of those — {1} type `{2}` is not permitted (multi-constructor sums, and `Str`/`List`/nested-record fields, are a future M4 layer)")]
ExportNonScalarSignature(String, &'static str, String),
/// An `(export …)` fn has a non-empty effect set. An embedding
/// kernel must be pure (a `(State,Chunk)->State` fold has no
/// effects). Code: `export-has-effects`.
#[error("export `{0}` must be pure — declared effects !{1:?} are not allowed on an embedding boundary")]
ExportHasEffects(String, Vec<String>),
/// A `Type::Con` named a type not in [`Env::types`] or with a wrong
/// arity for a parameterised ADT. Code: `unknown-type`.
#[error("unknown type: `{0}`")]
UnknownType(String),
/// A `Term::Ctor` referenced a ctor that doesn't belong to the
/// declared ADT. Code: `unknown-ctor`.
#[error("type `{ty}` has no constructor `{ctor}`")]
UnknownCtor { ty: String, ctor: String },
/// A pattern referenced a ctor that does not exist in the
/// scrutinee's resolved [`TypeDef`]. The Pattern::Ctor lookup
/// is type-driven (post-canonical-type-form): it walks `td.ctors` for the
/// `expected` Type::Con's TypeDef and reports this code when
/// no ctor of that name is present. Code: `unknown-ctor-in-pattern`.
#[error("unknown constructor `{0}` in pattern")]
UnknownCtorInPattern(String),
/// Wrong number of fields in a ctor application or pattern. Code:
/// `arity-mismatch` (shared with `ArityMismatch`).
#[error("constructor `{ty}/{ctor}` arity: expected {expected} fields, got {got}")]
CtorArity {
ty: String,
ctor: String,
expected: usize,
got: usize,
},
/// A `Term::Match` does not cover every ctor of an ADT (and has no
/// open arm). Code: `non-exhaustive-match`. `ctx` carries the
/// `missing` ctor names.
#[error("non-exhaustive match on `{ty}`: missing cases {missing:?}")]
NonExhaustive { ty: String, missing: Vec<String> },
/// A `Term::Match` on a primitive type lacks a wildcard or var arm.
/// Code: `primitive-needs-wildcard`.
#[error("primitive type `{0}` requires a wildcard or variable arm in match")]
PrimitiveNeedsWildcard(String),
/// A `Pattern::Lit` matched against a `Literal::Float`. Float
/// patterns are semantically dubious (NaN never matches via
/// IEEE-`==`; equality is bit-exact not approximate), so the
/// typechecker hard-rejects them. The surface lex / parser
/// accept the syntax (iter 2); this diagnostic surfaces at
/// typecheck time. Code: `float-pattern-not-allowed`.
#[error("float-literal patterns are not allowed: use ordering operators (`<`, `>`, ...) and `is_nan` to discriminate floats")]
FloatPatternNotAllowed,
/// A `Pattern::Ctor` was matched against a value of a different ADT.
/// Code: `pattern-type-mismatch`.
#[error("cannot match constructor pattern `{ctor}` against type `{ty}`")]
PatternTypeMismatch { ctor: String, ty: String },
/// Two `Def::Type` defs share a name. Code: `duplicate-type`.
#[error("duplicate type definition: `{0}`")]
DuplicateType(String),
/// Same ctor name registered in two different ADTs. Code:
/// `duplicate-ctor`.
#[error("duplicate constructor: `{ctor}` (in types `{a}` and `{b}`)")]
DuplicateCtor { ctor: String, a: String, b: String },
/// Two top-level defs in the same module share a name. Code:
/// `duplicate-def`.
#[error("duplicate definition: `{0}`")]
DuplicateDef(String),
/// A `Pattern::Ctor` has a [`Pattern::Lit`] sub-pattern. Iter 16a
/// added an AST-level desugar that flattens nested **Ctor**
/// sub-patterns before the checker sees the module, so this
/// diagnostic now fires only for literal sub-patterns inside a
/// Ctor (still out of scope; a future iter would lower them as a
/// nested Match on the field). Code:
/// `nested-ctor-pattern-not-allowed`.
#[error("nested constructor pattern not allowed in MVP: `{0}`")]
NestedCtorPatternNotAllowed(String),
/// A qualified `Term::Var { name: "<m>.<n>" }` references a module
/// alias not declared in the current module's imports. Code:
/// `unknown-module`.
#[error("unknown module prefix `{module}` in qualified reference")]
UnknownModule { module: String },
/// The aliased module exists but does not export the named def.
/// Code: `unknown-import`.
#[error("module `{module}` has no top-level def `{name}`")]
UnknownImport { module: String, name: String },
/// A def was declared with a name containing `.`, which is reserved
/// for qualified cross-module references. Code: `invalid-def-name`.
#[error("invalid def name `{name}`: contains `.` (reserved for qualified refs)")]
InvalidDefName { name: String },
/// a `Term::App { tail: true, .. }` or
/// `Term::Do { tail: true, .. }` was found in a non-tail position.
/// Code: `tail-call-not-in-tail-position`. See `design/contracts/0012-tail-calls.md`.
#[error("call marked `tail` is not in tail position")]
TailCallNotInTailPosition,
/// a `Term::ReuseAs { body, .. }` was found whose `body`
/// is not an allocating Term variant (i.e. not `Term::Ctor` and not
/// `Term::Lam`). `(reuse-as ...)` only makes sense when the body
/// produces a fresh allocation that can take over the source's
/// memory slot; otherwise the wrapper is meaningless and is
/// rejected at typecheck. Code: `reuse-as-non-allocating-body`.
/// `ctx`: `{"got": "<term-tag>"}`. The `body_form_a` field carries
/// the form-A spelling of the inner body so [`Self::to_diagnostic`]
/// can attach a `SuggestedRewrite` that drops the wrapper.
#[error("reuse-as body must be an allocating term (Term::Ctor or Term::Lam), got {got}")]
ReuseAsNonAllocatingBody { got: String, body_form_a: String },
/// a polymorphic `FnDef` calls a class method
/// (e.g. `show x` where `x: a`), producing a residual class
/// constraint `(class, a)` at the call site, but the fn's declared
/// `Forall.constraints` does not list that constraint (and the
/// one-step superclass-expansion of the declared set still does
/// not cover it). Without an in-scope constraint, monomorphisation
/// (22b.3) would have no dictionary to thread, so this is a hard
/// soundness error. Code: `missing-constraint`. `ctx`:
/// `{"class": "<C>", "method": "<m>", "at_type": "<a>"}`.
/// Concrete-type residuals (`Type::Con`) are deferred to Task 10's
/// `no-instance` diagnostic.
#[error(
"fn `{def}` calls class method `{method}` (class `{class}`) at type `{at_type}`, \
but its declared constraints do not include `{class} {at_type}`"
)]
MissingConstraint {
def: String,
method: String,
class: String,
at_type: String,
},
/// a `FnDef` calls a class method at a
/// fully-concrete type (e.g. `show 42` resolves the residual class
/// param to `Int`), but the workspace registry has no
/// `instance class at_type` entry. This is the dual of
/// `MissingConstraint`: when the residual type is concrete, the fn
/// cannot push the obligation to a caller via `Forall.constraints`
/// — it can only be discharged by an existing instance. Without a
/// matching registry entry, monomorphisation (22b.3) would have no
/// dictionary to substitute. Code: `no-instance`. `ctx`:
/// `{"class": "<C>", "method": "<m>", "at_type": "<T>"}`.
#[error(
"fn `{def}` calls `{method}` requiring `instance {class} {at_type}`, \
but no such instance exists in the workspace"
)]
NoInstance {
def: String,
method: String,
class: String,
at_type: String,
/// additive candidate-class list. Empty on residuals from
/// the single-class dispatch path (pre-canonical-class-form shape preserved).
/// Non-empty when the diagnostic originated from the
/// multi-candidate refinement path with zero registry survivors.
candidate_classes: Vec<String>,
},
/// a monomorphic call site `<method> x` with multiple
/// candidate classes (each declaring `<method>` and each having an
/// instance for `x`'s concrete type) cannot be resolved unambiguously.
/// The LLM-author writes an explicit qualifier
/// (`<class-qualifier>.<method> x`) to disambiguate.
/// Code: `ambiguous-method-resolution`. `ctx`:
/// `{"method": "<m>", "at_type": "<T>", "candidate_classes": ["<C1>", ...]}`.
#[error(
"method `{method}` at type `{at_type}` is ambiguous: classes \
{candidate_classes:?} all declare it and provide an instance. \
Disambiguate with `<ClassQualifier>.{method}`."
)]
AmbiguousMethodResolution {
method: String,
at_type: String,
candidate_classes: Vec<String>,
},
/// an explicit class qualifier in `Term::Var.name` names a
/// qualified class that is not in the workspace registry of
/// candidate classes for the method. Code: `unknown-class`. `ctx`:
/// `{"name": "<qualified-class>"}`.
#[error("class `{name}` is not declared in any module of this workspace")]
UnknownClass {
name: String,
},
/// loop-recur iter loop-recur.tidy: `Term::Lam` reached typecheck
/// inside a lexically-enclosing `Term::Loop`, and the lambda's body
/// references a loop binder declared by that enclosing loop. Loop
/// binders are alloca-resident (codegen reuses the
/// `binder_allocas` registry, `std::mem::take`-emptied at the
/// lambda frame boundary). Capturing one into a closure would
/// require lifting it to the heap (deferred) or rejecting the
/// capture; this milestone takes the latter route rather than
/// panicking codegen on type-correct input.
#[error("loop binder `{name}` cannot be captured by a lambda — loop binders are alloca-resident and do not escape their enclosing loop. Either move the lambda outside the loop, or restructure to pass `{name}` as a lambda parameter (deferring escape to a future milestone with ref-types and the !Mut effect).")]
LoopBinderCapturedByLambda { name: String },
/// loop-recur iter 2: `Term::Recur` reached typecheck with no
/// lexically-enclosing `Term::Loop` (the `loop_stack` was empty).
#[error("`recur` is only valid inside a `loop` — there is no enclosing loop here")]
RecurOutsideLoop,
/// loop-recur iter 2: `Term::Recur`'s argument count differs from
/// the enclosing loop's binder count. `recur` rebinds every loop
/// binder positionally, so the counts must match exactly.
#[error("`recur` passes {got} argument(s) but the enclosing loop has {expected} binder(s) — recur must rebind every binder positionally")]
RecurArityMismatch { expected: usize, got: usize },
/// loop-recur iter 2: a `recur` argument's type differs from the
/// corresponding loop binder's declared type (0-based position).
#[error("`recur` argument {position} has type `{got}` but the enclosing loop's binder at that position is `{expected}` — every recur argument must match its binder's type")]
RecurTypeMismatch {
position: usize,
expected: String,
got: String,
},
/// loop-recur iter 2: `Term::Recur` appears somewhere other than
/// the tail position of its enclosing loop body. `recur` is a
/// structural back-jump; it cannot be a sub-expression.
#[error("`recur` must be in tail position of its enclosing `loop` body — it is a back-jump, not a value-producing sub-expression")]
RecurNotInTailPosition,
/// prep.1 (kernel-extension-mechanics): a dot-qualified
/// `Term::Var` whose receiver is a known `TypeDef` but the suffix
/// does not name a def in that type's home module. Code:
/// `type-scoped-member-not-found`.
#[error("type `{type_name}` (home module `{home_module}`) has no member `{member}`")]
TypeScopedMemberNotFound {
type_name: String,
member: String,
home_module: String,
},
/// prep.1 (kernel-extension-mechanics): a dot-qualified
/// `Term::Var` whose receiver is neither a known `TypeDef` nor an
/// imported module. Code: `type-scoped-receiver-not-a-type`.
#[error("`{name}` is neither a known type nor an imported module")]
TypeScopedReceiverNotAType {
name: String,
},
/// prep.2 (kernel-extension-mechanics): a `(new T args...)` call
/// where `T`'s home module declares no `new` def. Code:
/// `new-type-not-constructible`.
#[error("type `{type_name}` is not constructible: home module `{home_module}` declares no `new` def")]
NewTypeNotConstructible {
type_name: String,
home_module: String,
},
/// prep.2 (kernel-extension-mechanics): a `(new T args...)` call
/// whose Type-arg count vs. Value-arg count does not match `new`'s
/// declared signature (e.g. `new : forall a. (a) -> T a` needs one
/// Type-arg at position 0 and one Value-arg at position 1; a
/// call site with two Value-args trips this). Code:
/// `new-arg-kind-mismatch`.
#[error("`(new {type_name} …)` arg at position {position}: expected {expected}, got {got}")]
NewArgKindMismatch {
type_name: String,
position: usize,
expected: &'static str,
got: &'static str,
},
/// prep.3 (kernel-extension-mechanics): `param-in` violation. A
/// `Type::Con` for a TypeDef that restricts a type variable was
/// instantiated with a type-arg outside the allowed set. The
/// diagnostic carries the TypeDef name (which TypeDef
/// restricts), the variable name (which var was violated), the
/// rejected concrete type name (`found`), and the allowed set
/// (`allowed`, deterministically alphabetical from the BTreeSet
/// source). Code: `param-not-in-restricted-set`.
#[error(
"type-arg `{found}` is not in the restricted set for type-variable `{var}` of `{type_name}` (allowed: one of {allowed:?})"
)]
ParamNotInRestrictedSet {
type_name: String,
var: String,
found: String,
allowed: Vec<String>,
},
/// An `(intrinsic)` body appears in a module that is neither
/// kernel-tier nor the prelude. User code may not declare a body as
/// compiler-supplied — the honesty-rule guard at the workspace
/// boundary (design/contracts/0007-honesty-rule.md).
/// Code: `intrinsic-outside-kernel-tier`.
#[error("def `{def}` in module `{module}` uses an `(intrinsic)` body, which is allowed only in a kernel-tier module or the prelude")]
IntrinsicOutsideKernelTier { def: String, module: String },
/// an internal invariant in the typechecker / mono pass
/// was violated — surfaced as an error so callers can propagate
/// rather than abort, but in well-formed inputs (typecheck has
/// succeeded) it must never fire. Code: `internal`.
#[error("internal: {0}")]
Internal(String),
}
pub(crate) type Result<T> = std::result::Result<T, CheckError>;
impl CheckError {
/// Stable kebab-case code for machine consumption (`ail check --json`).
/// Passed through recursively via the `Def` wrapping — the inner error
/// carries the actual code, the wrapper only the def context.
pub fn code(&self) -> &'static str {
match self {
CheckError::Def(_, inner) => inner.code(),
CheckError::TypeMismatch { .. } => "type-mismatch",
CheckError::UnknownIdent(_) => "unbound-var",
CheckError::UnknownEffectOp(_) => "unknown-effect-op",
CheckError::NotAFunction(..) => "not-a-function",
CheckError::ArityMismatch { .. } => "arity-mismatch",
CheckError::UndeclaredEffect(_) => "undeclared-effect",
CheckError::FnTypeRequired(..) => "fn-type-required",
CheckError::ParamCountMismatch { .. } => "param-count-mismatch",
CheckError::PolymorphicNotSupported(_) => "polymorphic-not-supported",
CheckError::ConstHasEffects(..) => "const-has-effects",
CheckError::ExportNonScalarSignature(..) => "export-non-scalar-signature",
CheckError::ExportHasEffects(..) => "export-has-effects",
CheckError::UnknownType(_) => "unknown-type",
CheckError::UnknownCtor { .. } => "unknown-ctor",
CheckError::UnknownCtorInPattern(_) => "unknown-ctor-in-pattern",
CheckError::CtorArity { .. } => "arity-mismatch",
CheckError::NonExhaustive { .. } => "non-exhaustive-match",
CheckError::PrimitiveNeedsWildcard(_) => "primitive-needs-wildcard",
CheckError::FloatPatternNotAllowed => "float-pattern-not-allowed",
CheckError::PatternTypeMismatch { .. } => "pattern-type-mismatch",
CheckError::DuplicateType(_) => "duplicate-type",
CheckError::DuplicateCtor { .. } => "duplicate-ctor",
CheckError::DuplicateDef(_) => "duplicate-def",
CheckError::NestedCtorPatternNotAllowed(_) => "nested-ctor-pattern-not-allowed",
CheckError::UnknownModule { .. } => "unknown-module",
CheckError::UnknownImport { .. } => "unknown-import",
CheckError::InvalidDefName { .. } => "invalid-def-name",
CheckError::TailCallNotInTailPosition => "tail-call-not-in-tail-position",
CheckError::ReuseAsNonAllocatingBody { .. } => "reuse-as-non-allocating-body",
CheckError::MissingConstraint { .. } => "missing-constraint",
CheckError::NoInstance { .. } => "no-instance",
CheckError::AmbiguousMethodResolution { .. } => "ambiguous-method-resolution",
CheckError::UnknownClass { .. } => "unknown-class",
CheckError::LoopBinderCapturedByLambda { .. } => "loop-binder-captured-by-lambda",
CheckError::RecurOutsideLoop => "recur-outside-loop",
CheckError::RecurArityMismatch { .. } => "recur-arity-mismatch",
CheckError::RecurTypeMismatch { .. } => "recur-type-mismatch",
CheckError::RecurNotInTailPosition => "recur-not-in-tail-position",
CheckError::TypeScopedMemberNotFound { .. } => "type-scoped-member-not-found",
CheckError::TypeScopedReceiverNotAType { .. } => "type-scoped-receiver-not-a-type",
CheckError::NewTypeNotConstructible { .. } => "new-type-not-constructible",
CheckError::NewArgKindMismatch { .. } => "new-arg-kind-mismatch",
CheckError::ParamNotInRestrictedSet { .. } => "param-not-in-restricted-set",
CheckError::IntrinsicOutsideKernelTier { .. } => "intrinsic-outside-kernel-tier",
CheckError::Internal(_) => "internal",
}
}
/// Structured context for a diagnostic. Lands directly in the JSON
/// under the key `ctx`. Empty object when no context is available.
pub fn ctx(&self) -> serde_json::Value {
match self {
CheckError::Def(_, inner) => inner.ctx(),
CheckError::TypeMismatch { expected, got } => {
serde_json::json!({"expected": expected, "actual": got})
}
CheckError::ArityMismatch { expected, got, .. } => {
serde_json::json!({"expected": expected, "actual": got})
}
CheckError::CtorArity {
expected, got, ..
} => serde_json::json!({"expected": expected, "actual": got}),
CheckError::ParamCountMismatch {
ty_count,
param_count,
..
} => serde_json::json!({"expected": ty_count, "actual": param_count}),
CheckError::NonExhaustive { missing, .. } => {
serde_json::json!({"missing": missing})
}
CheckError::UnknownModule { module } => {
serde_json::json!({"module": module})
}
CheckError::UnknownImport { module, name } => {
serde_json::json!({"module": module, "name": name})
}
CheckError::InvalidDefName { name } => {
serde_json::json!({"name": name, "reason": "contains-dot"})
}
CheckError::ReuseAsNonAllocatingBody { got, .. } => {
serde_json::json!({"got": got})
}
CheckError::MissingConstraint { class, method, at_type, .. } => {
serde_json::json!({"class": class, "method": method, "at_type": at_type})
}
CheckError::NoInstance { class, method, at_type, candidate_classes, .. } => {
let mut obj = serde_json::json!({
"class": class,
"method": method,
"at_type": at_type,
});
if !candidate_classes.is_empty() {
obj["candidate_classes"] = serde_json::json!(candidate_classes);
}
obj
}
CheckError::AmbiguousMethodResolution { method, at_type, candidate_classes } => {
serde_json::json!({
"method": method,
"at_type": at_type,
"candidate_classes": candidate_classes,
})
}
CheckError::UnknownClass { name } => {
serde_json::json!({ "name": name })
}
CheckError::LoopBinderCapturedByLambda { name } => {
serde_json::json!({"name": name})
}
CheckError::RecurArityMismatch { expected, got } => {
serde_json::json!({"expected": expected, "actual": got})
}
CheckError::RecurTypeMismatch { position, expected, got } => {
serde_json::json!({"position": position, "expected": expected, "actual": got})
}
CheckError::TypeScopedMemberNotFound { type_name, member, home_module } => {
serde_json::json!({"type": type_name, "member": member, "home_module": home_module})
}
CheckError::TypeScopedReceiverNotAType { name } => {
serde_json::json!({"name": name})
}
CheckError::NewTypeNotConstructible { type_name, home_module } => {
serde_json::json!({"type": type_name, "home_module": home_module})
}
CheckError::NewArgKindMismatch { type_name, position, expected, got } => {
serde_json::json!({
"type": type_name,
"position": position,
"expected": expected,
"actual": got,
})
}
CheckError::ParamNotInRestrictedSet { type_name, var, found, allowed } => {
serde_json::json!({
"type": type_name,
"var": var,
"found": found,
"allowed": allowed,
})
}
_ => serde_json::Value::Object(serde_json::Map::new()),
}
}
/// If this error is wrapped by [`CheckError::Def`], returns the name
/// of the affected def. Otherwise `None`.
pub fn def(&self) -> Option<&str> {
match self {
CheckError::Def(n, _) => Some(n.as_str()),
_ => None,
}
}
/// Unwraps the error potentially wrapped by [`CheckError::Def`].
pub fn inner(&self) -> &CheckError {
match self {
CheckError::Def(_, inner) => inner.inner(),
other => other,
}
}
/// Non-`Def`-wrapped message. Without the `def: ...` prefix.
pub fn message(&self) -> String {
format!("{}", self.inner())
}
/// Lowers this error into the public [`Diagnostic`] shape consumed
/// by `ail check --json`. Pulls `code`, `message`, and `ctx` through
/// the recursive accessors and attaches the optional def name from
/// any wrapping [`CheckError::Def`].
pub fn to_diagnostic(&self) -> Diagnostic {
let mut d = Diagnostic::error(self.code(), self.message()).with_ctx(self.ctx());
if let Some(name) = self.def() {
d = d.with_def(name);
}
// typecheck-side suggested_rewrites for the
// reuse-as-non-allocating-body diagnostic. The replacement is
// simply the body without the `(reuse-as ...)` wrapper — the
// hint is meaningless here, so drop it.
if let CheckError::ReuseAsNonAllocatingBody { body_form_a, .. } = self.inner() {
d = d.with_suggested_rewrite(
"drop the meaningless reuse-as wrapper around the non-allocating body",
body_form_a.clone(),
);
}
// Float-aware addendum on `NoInstance`. When the
// unresolved class is `Eq` or `Ord` AND the type is `Float`,
// append a cross-reference to design/contracts/0005-float-semantics.md so
// the LLM author learns the partial-Float story immediately
// rather than seeing a bare "no instance" message. Float has
// neither Eq nor Ord by design (partial orderability per
// IEEE-754), and the polymorphic prelude helpers
// (`ne` / `lt` / `le` / `gt` / `ge` / direct `eq` / `compare`)
// are the natural surface where the LLM hits this.
if let CheckError::NoInstance { class, at_type, .. } = self.inner() {
// `class` carries the qualified workspace-key shape
// (`prelude.Eq` / `prelude.Ord`), not the bare name.
if (class == "prelude.Eq" || class == "prelude.Ord") && at_type == "Float" {
d.message = format!(
"{} — Float has no Eq/Ord instance by design (partial \
orderability per IEEE-754); use float_eq / float_lt \
(and siblings float_ne / float_le / float_gt / float_ge) \
for explicit IEEE-aware comparison. \
See design/contracts/0005-float-semantics.md.",
d.message
);
} else if class == "prelude.Show" {
// Show-aware addendum on `NoInstance`. Fires
// for any type lacking a Show instance — most commonly
// a function type (`print f` where f is bare-fn-typed)
// or a user type the LLM-author forgot to give an
// instance for. Cross-references
// design/contracts/0013-typeclasses.md so the author learns
// which types ship with built-in Show immediately.
d.message = format!(
"{} — `print` and `show` require a Show instance. \
Built-in Show ships for Int, Bool, Str, Float in \
the prelude; see design/contracts/0013-typeclasses.md. \
User types declare their own \
`instance prelude.Show <T>` in the type's defining \
module per the typeclass design coherence.",
d.message
);
}
}
d
}
}
/// Top-level API for structured diagnostics.
///
/// Empty Vec = green. From Iter 6 onwards the body-check phase is
/// multi-diagnose: each def in each module is checked independently and
/// failures accumulate, so a single `ail check` run reports every
/// independent body error in the workspace.
///
/// Pass-1 errors (top-level symbol-table construction:
/// `invalid-def-name`, `duplicate-def`) are still fail-fast — those
/// errors corrupt the symbol table, and any further diagnostic would be
/// unreliable. Likewise, the type-def installation is fail-fast within
/// a single module, but other modules continue being checked.
///
/// Backwards compatibility: a bare `&Module` is internally lifted into a
/// trivial workspace (`modules = {m.name: m}`, `entry = m.name`) so that
/// tooling checking individual modules avoids building a `Workspace`.
/// Modules with imports on other modules not present in the trivial
/// workspace will inevitably produce `unknown-module` errors on qualified
/// references — which is correct.
pub fn check_module(m: &Module) -> Vec<Diagnostic> {
// flatten nested constructor patterns before any check
// logic touches the AST. The rewrite is pure and runs in memory;
// canonical-JSON hashes (computed by `ailang_core::load_module` /
// `def_hash`) are unaffected because they use the on-disk form.
let m = ailang_core::desugar::desugar_module(m);
let mut modules = BTreeMap::new();
modules.insert(m.name.clone(), m.clone());
let ws = Workspace {
entry: m.name.clone(),
modules,
root_dir: std::path::PathBuf::from("."),
// single-module check_module entry point does not
// build a registry. The registry is workspace-load-time
// metadata; check_module is invoked from in-memory paths
// (tests, single-file CLI) where no workspace DFS happened.
// Once 22b.2 typecheck arms read the registry, those paths
// will need to populate it from the in-memory module too.
registry: ailang_core::workspace::Registry::default(),
};
check_workspace(&ws)
}
/// Top-level API for cross-module typecheck.
///
/// prep.1 (kernel-extension-mechanics): apply the pre-typecheck
/// preparation steps the workspace needs both for typechecking and
/// monomorphisation:
///
/// 1. Desugar every module via `ailang_core::desugar::desugar_module`.
/// 2. Normalize every consumer module's bare cross-module `Type::Con`
/// references to qualified `<home>.<Type>` form (so consumer-side
/// declared types unify with imported-fn signatures, which the
/// existing [`qualify_local_types`] step already qualifies at the
/// owner's side).
///
/// Both [`check_workspace`] and [`monomorphise_workspace`] call this
/// helper at their entry. The registry passes through unchanged.
pub fn prepare_workspace_for_check(ws: &Workspace) -> Workspace {
let workspace_types_pre: BTreeMap<String, IndexMap<String, TypeDef>> =
ws.modules
.iter()
.map(|(name, m)| {
let mut tys: IndexMap<String, TypeDef> = IndexMap::new();
for def in &m.defs {
if let Def::Type(td) = def {
tys.insert(td.name.clone(), td.clone());
}
}
(name.clone(), tys)
})
.collect();
// raw-buf.4: per-module set of *monomorphic* (non-`Forall`)
// top-level fn names. A type-scoped call `T.f` to a monomorphic
// op (e.g. the `raw_buf.RawBuf.new` produced by the Term::New
// desugar) is normalised to the module-qualified `<home>.f` form
// by `qualify_workspace_term` — codegen recognises that spelling
// directly. Polymorphic type-scoped ops stay in the `T.f` form so
// monomorphisation can mint their scope-qualified `T_f__<elem>`
// symbols (the raw-buf.3 mechanism RawBuf's ops use).
let workspace_mono_fns: BTreeMap<String, BTreeSet<String>> = ws
.modules
.iter()
.map(|(name, m)| {
let fns: BTreeSet<String> = m
.defs
.iter()
.filter_map(|def| match def {
Def::Fn(f) if !matches!(f.ty, Type::Forall { .. }) => Some(f.name.clone()),
_ => None,
})
.collect();
(name.clone(), fns)
})
.collect();
Workspace {
entry: ws.entry.clone(),
modules: ws
.modules
.iter()
.map(|(k, m)| {
let m = ailang_core::desugar::desugar_module(m);
let own_local_types = workspace_types_pre
.get(k)
.cloned()
.unwrap_or_default();
(
k.clone(),
qualify_workspace_module(
m,
&own_local_types,
&workspace_types_pre,
&workspace_mono_fns,
),
)
})
.collect(),
root_dir: ws.root_dir.clone(),
registry: ws.registry.clone(),
}
}
/// Iterates over all modules of the workspace and checks each with access
/// to the top-level symbol tables of all other modules. Qualified
/// references are resolved via the import map of the respective module:
/// `Term::Var { name }` with exactly one dot in the name is interpreted
/// as `<prefix>.<def>`; `<prefix>` is an import alias (or the module name,
/// if imported without an alias).
///
/// Multi-diagnose: pass-2 collects diagnostics per def across all modules.
/// Pass-1 (symbol table) stays fail-fast — see [`check_module`].
/// Module iteration order is deterministic: entry first, then the rest in
/// BTreeMap order, so output ordering is stable.
pub fn check_workspace(ws: &Workspace) -> Vec<Diagnostic> {
// Floats milestone post-fieldtest B1: hard-reject
// `Pattern::Lit { Literal::Float }` before desugar rewrites lit
// arms into `(== scrutinee lit)`. See `pre_desugar_validation`
// for the full rationale. Walked per-def so the diagnostic
// carries the offending def's name; modules are visited in
// BTreeMap order, defs in declaration order. All hits in this
// pass are accumulated and returned together (consistent with
// pass-2 multi-diagnose); if any are present, later passes do
// not run, since a violating Float-lit pattern would otherwise
// be silently rewritten by desugar before typecheck.
{
let mut pre_desugar_errors: Vec<Diagnostic> = Vec::new();
for m in ws.modules.values() {
for def in &m.defs {
if let Err(e) = pre_desugar_validation::reject_float_patterns_in_def(def) {
let wrapped = CheckError::Def(def.name().to_string(), Box::new(e));
pre_desugar_errors.push(wrapped.to_diagnostic());
}
}
}
if !pre_desugar_errors.is_empty() {
return pre_desugar_errors;
}
}
// desugar every module of the workspace before any check
// logic runs. The rewrite is pure and per-module; we rebuild a
// workspace shell around the desugared modules (paths and entry
// are unchanged).
//
// prep.1 (kernel-extension-mechanics): after desugar, normalize
// each consumer module's bare cross-module `Type::Con` references
// to qualified form via [`prepare_workspace_for_check`]. The
// monomorphisation pass mirrors this step in its own entry
// (`monomorphise_workspace`); the two passes consume identically
// shaped workspaces. The registry passes through unchanged — the
// desugar pass does not touch class/instance defs (see desugar.rs:
// 22b.1 passthrough), so the registry built at load time remains
// valid against the prepared workspace.
let ws_owned = prepare_workspace_for_check(ws);
let ws = &ws_owned;
// Pass 1: build per-module top-level symbol table — without checking
// bodies. This lets module A access defs from module B even when B
// comes later in the BTreeMap. Duplicate def names and dot-in-def
// names are reported here immediately, because without clean symbol
// tables all further diagnostics would be unreliable.
let module_globals = match build_module_globals(ws) {
Ok(g) => g,
Err(e) => return vec![e.to_diagnostic()],
};
// Pass 2: body-check per module. `check_in_workspace` builds the env
// with additional cross-module globals and an import map. Errors
// accumulate across modules.
let mut order: Vec<&String> = Vec::new();
if ws.modules.contains_key(&ws.entry) {
order.push(&ws.entry);
}
for name in ws.modules.keys() {
if name != &ws.entry {
order.push(name);
}
}
let mut diagnostics: Vec<Diagnostic> = Vec::new();
for name in order {
let m = &ws.modules[name];
// synth-time warnings collected per module then merged
// into the per-module diagnostic stream alongside typecheck
// errors. The synth warnings flow through `check_in_workspace`
// even when `had_typecheck_errors` is true; surface them so a
// shadowed-class-method warning is visible even when the
// module also has unrelated errors.
let mut synth_warnings: Vec<Diagnostic> = Vec::new();
let typecheck_errors = check_in_workspace(m, ws, &module_globals, &mut synth_warnings);
let had_typecheck_errors = !typecheck_errors.is_empty();
// Per-module diagnostic accumulator. The suppress filter
// (Iter 19b) runs at the end of the per-module block, so
// we keep this module's diagnostics in their own vec while
// accumulating, then merge into the workspace-wide list.
let mut module_diags: Vec<Diagnostic> = Vec::new();
for e in typecheck_errors {
module_diags.push(e.to_diagnostic());
}
module_diags.extend(synth_warnings);
// linearity check runs only on modules that
// typechecked clean. Running it on a body that already has a
// type error would wade into a partly-defined IR (e.g.
// unresolved Var lookups, mismatched ctor arities) and produce
// noise. Cleanly-typechecked modules with at least one
// all-explicit-mode fn are exactly the surface the check is
// designed to inspect.
if !had_typecheck_errors {
// linearity check needs visibility into
// polymorphic free fns + class methods from implicitly-
// imported modules (currently just the auto-injected
// prelude). Without this, a Borrow-mode user fn that
// forwards its borrow params into a prelude poly fn
// (e.g. `gt x y`) fires `consume-while-borrowed`
// false positives because `callee_arg_modes` defaults
// to Consume when it cannot see the callee's
// `param_modes`. Symmetric to the class-method case
// closed in iter 23.4-prep.
let visible_extra: Vec<&Module> = ws
.modules
.iter()
.filter_map(|(other_name, other_mod)| {
if other_name == name {
None
} else {
Some(other_mod)
}
})
.collect();
module_diags.extend(linearity::check_module_with_visible(m, &visible_extra));
// reuse-as shape compatibility check. Runs on
// the same activation gate as linearity (all-explicit-mode
// fns only). The check resolves each `(reuse-as <var>
// <body-ctor>)` site against the path-ctor of `<var>` and
// rejects mismatches with `reuse-as-shape-mismatch`. Runs
// after linearity so its output appears after linearity's
// diagnostics for the same def — stable ordering for the
// JSON consumer.
module_diags.extend(reuse_shape::check_module(m));
}
// apply per-fn `suppress` filter. Runs after every
// diagnostic source has appended so any code the author
// listed can actually be matched. Drops matching diagnostics
// and pushes `empty-suppress-reason` (Error) for malformed
// entries. See [`crate::suppress_filter`] for details.
suppress_filter::apply(m, &mut module_diags);
diagnostics.extend(module_diags);
}
diagnostics
}
/// Result of typechecking a module: mapping from symbol name to
/// (type, hash) — ready for `manifest` output.
#[derive(Debug, Clone)]
pub struct CheckedModule {
/// Top-level symbols of the module in declaration order. The value
/// is `(declared_type, content_hash)` — the hash is the BLAKE3 def
/// hash from `ailang_core::hash::def_hash`, used by `ail diff` and
/// the cross-module manifest.
pub symbols: IndexMap<String, (Type, String)>,
}
/// Single-error entry point. Typechecks `m` standalone (trivial
/// workspace), returning a [`CheckedModule`] with the symbol-to-hash
/// table on success or the **first** [`CheckError`] on failure.
///
/// Prefer [`check_module`] for new callers — it returns
/// `Vec<Diagnostic>` (multi-diagnose, JSON-ready). This function is
/// kept for legacy callers (snapshot tests, the `manifest` codepath
/// that needs the hash-to-type mapping).
pub fn check(m: &Module) -> Result<CheckedModule> {
// Floats milestone post-fieldtest B1: hard-reject
// `Pattern::Lit { Literal::Float }` before desugar runs, because
// `desugar::build_eq` rewrites lit-pattern arms (Float included)
// into `(== scrutinee lit)` and would otherwise hide the
// unreachable Float-pattern arm in `type_check_pattern`. See
// `pre_desugar_validation` for the full rationale.
pre_desugar_validation::reject_float_patterns_in_module(m)?;
// desugar nested ctor patterns before constructing the
// trivial workspace. See `check_module` for the rationale. The
// returned `CheckedModule.symbols` content hashes are derived from
// the *original* on-disk module so they keep the canonical-bytes
// identity that `ail diff` / `ail manifest` rely on.
let original = m;
let desugared = ailang_core::desugar::desugar_module(m);
let m = &desugared;
// Trivial workspace: the module alone, without cross-module resolution.
let mut modules = BTreeMap::new();
modules.insert(m.name.clone(), m.clone());
let ws = Workspace {
entry: m.name.clone(),
modules,
root_dir: std::path::PathBuf::from("."),
// the legacy single-module `check` entry point
// builds an empty registry. See `check_module` for the same
// pattern; once 22b.2 typecheck arms read the registry, both
// paths must populate it from the in-memory module.
registry: ailang_core::workspace::Registry::default(),
};
let module_globals = build_module_globals(&ws)?;
// `check` keeps single-error semantics for callers (snapshot tests,
// legacy code). Multi-diagnose is exposed via `check_module` /
// `check_workspace`. Synth warnings are collected here but
// discarded — `check`'s legacy contract returns only the first
// error, and warnings on this path have no surface to flow to.
let mut synth_warnings: Vec<Diagnostic> = Vec::new();
if let Some(first) = check_in_workspace(m, &ws, &module_globals, &mut synth_warnings).into_iter().next() {
return Err(first);
}
// Collect symbols for the return value (existing semantics).
// Hashes are computed over the *original* defs, so callers like
// `ail diff` see the on-disk identity, not a post-desugar one.
let mut symbols = IndexMap::new();
for def in &original.defs {
let h = ailang_core::hash::def_hash(def);
let ty = match def {
Def::Fn(f) => f.ty.clone(),
Def::Const(c) => c.ty.clone(),
Def::Type(_) => Type::Con {
name: def.name().to_string(),
args: vec![],
},
// class/instance defs are not yet checked.
// The symbols map is keyed by definition name; class/
// instance contribute their class name, but with no
// concrete pre-monomorphisation type we represent them
// as a placeholder Con. Tools that consume this map
// (`ail diff`, `ail manifest`) read kind separately
// via `def_kind`, so the placeholder type does not
// mislead them.
Def::Class(_) | Def::Instance(_) => Type::Con {
name: def.name().to_string(),
args: vec![],
},
};
symbols.insert(def.name().to_string(), (ty, h));
}
Ok(CheckedModule { symbols })
}
/// typecheck `m` and return both the [`CheckedModule`]
/// (for tooling that wants the original on-disk symbol identities)
/// AND the lifted module ready for codegen — i.e. the desugared
/// module with every surviving `Term::LetRec` replaced by a
/// synthetic top-level `Def::Fn`.
///
/// The check phase runs unchanged: same desugar, same typecheck,
/// same `CheckedModule.symbols` (built from the original `m`'s
/// defs). On success, the desugared module is fed through
/// [`lift_letrecs`] and the result is returned alongside.
///
/// `build` / `run` go through this entry; the `check` subcommand
/// stays on the legacy [`check`] entry (no lift needed for
/// type-checking only).
pub fn check_and_lift(m: &Module) -> Result<(CheckedModule, Module)> {
let cm = check(m)?;
// Run desugar exactly as `check` does. The `check` call already
// ran desugar internally, but its result is discarded (only the
// CheckedModule survives), so we have to re-run it here to get
// the post-desugar form for the lift.
let desugared = ailang_core::desugar::desugar_module(m);
let lifted = lift_letrecs(&desugared)?;
Ok((cm, lifted))
}
/// builds the ADT type-def table per module. Sibling of
/// [`build_module_globals`]: gives the body checker O(1) lookup of any
/// type declared anywhere in the workspace, keyed by module name.
/// Read by qualified `Type::Con.name` resolution
/// (`module.Type`), qualified `Term::Ctor.type_name`, and the
/// cross-module `Pattern::Ctor` fallback. Duplicate type / ctor errors
/// inside a single module surface during the per-module body-check
/// phase, not here.
pub(crate) fn build_module_types(
ws: &Workspace,
) -> BTreeMap<String, IndexMap<String, TypeDef>> {
let mut out: BTreeMap<String, IndexMap<String, TypeDef>> = BTreeMap::new();
for (mname, m) in &ws.modules {
let mut tys = IndexMap::new();
for def in &m.defs {
if let Def::Type(td) = def {
// Last definition wins on duplicate; the per-module
// body-check phase reports `duplicate-type` separately.
tys.insert(td.name.clone(), td.clone());
}
}
out.insert(mname.clone(), tys);
}
out
}
/// per-module top-level symbol table. Holds the classic
/// fn/const/type-name-to-type mapping in [`Self::fns`] and class-method
/// names in [`Self::class_methods`]. The two channels are kept separate
/// because class-method resolution at a call site needs more context
/// than a plain `Type` lookup (the owning class, the class param name,
/// and the defining module — see [`ClassMethodEntry`]). Pre-22b.2 the
/// inner shape was `IndexMap<String, Type>`; 22b.2 wraps that in this
/// struct so call sites that only need fn lookup can keep using
/// `mod_globals.fns` while typeclass code goes through `class_methods`.
#[derive(Debug, Default, Clone)]
pub struct ModuleGlobals {
/// Top-level fn / const / type symbols, by name. The pre-22b.2 inner
/// shape — every call site that only needs HM lookup goes through
/// here.
pub fns: IndexMap<String, Type>,
/// re-keyed by `(qualified-class-name, method-name)` tuple —
/// post-retirement of `MethodNameCollision`, two classes can declare
/// same-named methods within the same workspace. The tuple key
/// disambiguates without losing the per-module ordering guarantee
/// (`IndexMap` preserves insertion order). Lookups by method-name-
/// only consult `method_to_candidate_classes` (Env-level) to get
/// the candidate-class set, then index into `class_methods` with
/// `(resolved_class, method)`.
pub class_methods: IndexMap<(String, String), ClassMethodEntry>,
}
impl ModuleGlobals {
/// True if class `class` declares a method named `name` in this
/// module. Tuple-keyed lookup after `MethodNameCollision`
/// retirement.
pub fn has_class_method(&self, class: &str, name: &str) -> bool {
self.class_methods.contains_key(&(class.to_string(), name.to_string()))
}
/// The class that declared the method `name` in class `class`, or
/// `None` if no such entry exists. (Pre-canonical-class-form callers passed only the
/// method name; post-canonical-class-form they must disambiguate by class.)
pub fn class_method_class(&self, class: &str, name: &str) -> Option<&str> {
self.class_methods
.get(&(class.to_string(), name.to_string()))
.map(|e| e.class_name.as_str())
}
/// The full [`ClassMethodEntry`] for method `name` in class `class`,
/// or `None` if no such entry exists.
pub fn class_method(&self, class: &str, name: &str) -> Option<&ClassMethodEntry> {
self.class_methods.get(&(class.to_string(), name.to_string()))
}
/// enumerate all `(class, method) -> entry` pairs whose
/// method name matches `name`. Returns zero-or-more entries —
/// pre-canonical-class-form always at most one, post-canonical-class-form a workspace may have
/// multiple classes declaring the same method.
pub fn class_method_candidates(&self, name: &str) -> Vec<(&String, &ClassMethodEntry)> {
self.class_methods
.iter()
.filter_map(|((c, m), e)| if m == name { Some((c, e)) } else { None })
.collect()
}
}
/// per-class-method metadata stored in
/// [`ModuleGlobals::class_methods`]. Carries everything the 22b.2
/// typecheck arms (`missing-constraint`, `no-instance`) need to resolve
/// a `Term::Var { name }` that refers to a class method into a residual
/// class constraint at the call site.
#[derive(Debug, Clone)]
pub struct ClassMethodEntry {
/// The class that declared the method (e.g. `Show` for `show`).
///
/// carries the qualified form `<defining_module>.<Class>`;
/// flows downstream into `ResidualConstraint.class` and
/// `MonoTarget::ClassMethod.class` unchanged. Match the registry
/// key shape so discharge / mono lookups land on the right entry.
pub class_name: String,
/// The class's single type parameter name (e.g. `a` in
/// `class Show a`). The class param appears at this name inside
/// [`Self::method_ty`].
pub class_param: String,
/// The method's declared signature — a `Type::Fn` whose param /
/// return positions may contain `Type::Var { name: class_param }`.
/// Task 9 instantiates the class param with a fresh metavar at the
/// call site to build the residual constraint.
pub method_ty: Type,
/// Module that declared the class. Tasks 9 / 10 use this to find
/// the matching `Registry` entries when checking constraints.
pub defining_module: String,
}
/// Builds the top-level symbol table per module (for cross-module lookup),
/// without checking bodies. Duplicates and dot-in-def names are reported
/// here as errors immediately — they would taint all further diagnostics.
///
/// also collects class-method names from `Def::Class`
/// into [`ModuleGlobals::class_methods`], so that pass-2 lookup of a
/// class method via `Term::Var { name }` resolves to a known global
/// rather than firing `unbound-var`. The class-method channel is kept
/// separate from the fn / const / type channel because resolution
/// downstream needs the owning class and class-param name to build a
/// residual constraint at the call site.
pub fn build_module_globals(
ws: &Workspace,
) -> Result<BTreeMap<String, ModuleGlobals>> {
let mut out: BTreeMap<String, ModuleGlobals> = BTreeMap::new();
for (mname, m) in &ws.modules {
let mut globals = ModuleGlobals::default();
for def in &m.defs {
let def_name = def.name();
// for `Def::Instance`, `def.name()` returns
// `inst.class` which carries the canonical-form value
// (qualified for cross-module). The dot-in-def-name check
// is meant for `Fn`/`Const`/`Type` whose names are author-
// chosen identifiers — instances have no author-chosen
// name and are excluded.
if !matches!(def, Def::Instance(_)) && def_name.contains('.') {
return Err(CheckError::Def(
def_name.to_string(),
Box::new(CheckError::InvalidDefName {
name: def_name.to_string(),
}),
));
}
// pre-22b.2 the dup check ran across the single
// `IndexMap<String, Type>`, but class / instance defs early-
// `continue`d before the insert, so they never participated
// in dup detection (and `instance Foo` re-using the class
// name is legal). Preserving that, dup detection here is
// scoped to the `fns` channel exactly as before. Class /
// instance coherence (orphan / duplicate-instance /
// missing-method / method-name-collision) is enforced
// earlier at `workspace::build_registry`.
match def {
Def::Fn(f) => {
if globals.fns.contains_key(def_name) {
return Err(CheckError::Def(
def_name.to_string(),
Box::new(CheckError::DuplicateDef(def_name.to_string())),
));
}
globals.fns.insert(def_name.to_string(), f.ty.clone());
}
Def::Const(c) => {
if globals.fns.contains_key(def_name) {
return Err(CheckError::Def(
def_name.to_string(),
Box::new(CheckError::DuplicateDef(def_name.to_string())),
));
}
globals.fns.insert(def_name.to_string(), c.ty.clone());
}
Def::Type(_) => {
if globals.fns.contains_key(def_name) {
return Err(CheckError::Def(
def_name.to_string(),
Box::new(CheckError::DuplicateDef(def_name.to_string())),
));
}
globals.fns.insert(
def_name.to_string(),
Type::Con {
name: def_name.to_string(),
args: vec![],
},
);
}
Def::Class(cd) => {
// register every method
// declared by the class as a class-method global,
// with enough metadata for the typecheck arms in
// Tasks 9 / 10 to build a residual constraint at
// the call site.
//
// store the qualified class name
// (`<defining_module>.<Class>`) so the residual
// emitted at the call site matches the workspace
// registry's qualified key.
let qualified_class = format!("{mname}.{}", cd.name);
for meth in &cd.methods {
globals.class_methods.insert(
(qualified_class.clone(), meth.name.clone()),
ClassMethodEntry {
class_name: qualified_class.clone(),
class_param: cd.param.clone(),
method_ty: meth.ty.clone(),
defining_module: mname.clone(),
},
);
}
}
Def::Instance(_) => {
// Instances do not contribute globals; coherence
// is enforced earlier at
// `workspace::build_registry`.
}
}
}
out.insert(mname.clone(), globals);
}
Ok(out)
}
/// Build the workspace-flat `Env` shared by `check_in_workspace`
/// and `mono::build_workspace_env`. Populates every field whose
/// contents are derivable from `Workspace` alone — no
/// `current_module` overlay applied. Both call sites are thin
/// consumers: each clones this env and applies the per-call
/// overlay (`current_module`, `globals` augmented with module fns,
/// `imports`, `rigid_vars`) at the call site.
///
/// Pre-condition: typecheck has succeeded for the workspace
/// (otherwise `build_module_globals` panics — same caller-contract
/// as the pre-refactor `mono::build_workspace_env`).
pub fn build_check_env(ws: &Workspace) -> Env {
let mut env = Env::default();
builtins::install(&mut env);
// env.types + env.ctor_index — workspace-flat from every
// module's Def::Type. Safe to flatten because `check_workspace`
// has already accepted the workspace, so duplicate names cannot
// occur. Mirrors the per-module loop in the pre-refactor
// `check_in_workspace` (which fail-fast aborted on duplicates,
// unreachable here).
for m in ws.modules.values() {
for d in &m.defs {
if let Def::Type(td) = d {
for c in &td.ctors {
env.ctor_index.insert(
c.name.clone(),
CtorRef { type_name: td.name.clone() },
);
}
env.types.insert(td.name.clone(), td.clone());
}
}
}
// env.module_globals + env.class_methods — built from
// `build_module_globals(ws)`. The .fns projection feeds
// `module_globals`; the .class_methods entries are merged
// workspace-wide into `class_methods` (uniqueness enforced
// earlier by `workspace::build_registry`'s
// method-name-collision check).
let mg = build_module_globals(ws)
.expect("build_module_globals: pre-condition (typecheck succeeded) violated");
env.module_globals = mg
.iter()
.map(|(k, v)| (k.clone(), v.fns.clone()))
.collect();
for g in mg.values() {
for ((qualified_class, method_name), e) in &g.class_methods {
// env.class_methods is tuple-keyed by
// `(qualified-class, method-name)`. Multiple classes may
// share a method name post-`MethodNameCollision`-retirement.
env.class_methods.insert(
(qualified_class.clone(), method_name.clone()),
e.clone(),
);
// build the inverse method → candidate-class set in
// the same loop. `e.class_name` already carries the
// qualified form (canonical-class-form invariant), so the set is keyed on
// workspace-flat qualified class names directly.
env.method_to_candidate_classes
.entry(method_name.clone())
.or_default()
.insert(e.class_name.clone());
}
}
// env.module_types — per-module ADT index.
env.module_types = build_module_types(ws);
// env.module_imports — per-module alias-or-name -> module-name.
// Per-module because aliases collide across modules; sibling
// shape to `module_globals`.
//
// Implicit-import set: the literal name `"prelude"` (the
// legacy singleton implicit import, retained unconditionally
// for back-compat with workspaces whose prelude predates the
// kernel-flag) PLUS every workspace module flagged
// `kernel: true`. The kernel-flag half mirrors the loader's
// filter at `crates/ailang-surface/src/loader.rs`
// (`modules.filter(|m| m.kernel)`) that drives
// `implicit_imports` into `build_workspace`. The pre-pass
// `qualify_workspace_types` freely produces qualifiers like
// `raw_buf.RawBuf`; without this injection the type-
// validity check at ~line 1968 would reject `raw_buf` as
// an unknown module prefix. Fieldtest F3 surfaced the gap
// (the previous code force-injected only `prelude`, leaving
// `raw_buf` and any future kernel-tier module unreachable
// from consumers). The production prelude carries
// `kernel: true`, so the two halves are idempotent for it; the
// `"prelude"` literal stays so unit-test workspaces that
// construct a `kernel: false` prelude still see the contract.
let kernel_modules: Vec<String> = ws
.modules
.values()
.filter(|m| m.kernel)
.map(|m| m.name.clone())
.collect();
for m in ws.modules.values() {
let mut import_map: BTreeMap<String, String> = BTreeMap::new();
for imp in &m.imports {
let key = imp.alias.clone().unwrap_or_else(|| imp.module.clone());
import_map.insert(key, imp.module.clone());
}
// A user-declared explicit `import` of any implicit name
// would already have placed it in the map above
// (idempotent insert via `entry`). A module is not
// auto-imported into its own body.
if m.name != "prelude" {
import_map
.entry("prelude".to_string())
.or_insert_with(|| "prelude".to_string());
}
for k in &kernel_modules {
if &m.name != k {
import_map.entry(k.clone()).or_insert_with(|| k.clone());
}
}
env.module_imports.insert(m.name.clone(), import_map);
}
// env.class_superclasses — walk every module's Def::Class.
//
// key + value both carry the qualified class name. The map
// is queried by `expand_declared_constraints` with `c.class`
// (a `Constraint.class` value, which is canonical-form on the
// residual side post-canonical-class-form), so both halves of the map must match
// the same workspace-key shape. A bare `SuperclassRef.class`
// (same-module superclass) is lifted via `qualify_class_ref` —
// mirrored inline below to avoid pulling in the workspace helper.
for (mod_name, m) in &ws.modules {
for d in &m.defs {
if let Def::Class(cd) = d {
if let Some(sc) = &cd.superclass {
let class_qualified = format!("{mod_name}.{}", cd.name);
let sc_qualified = if sc.class.contains('.') {
sc.class.clone()
} else {
format!("{mod_name}.{}", sc.class)
};
env.class_superclasses.insert(class_qualified, sc_qualified);
}
}
}
}
// env.workspace_registry — clone of ws.registry. Used by
// `check_fn`'s concrete-residual no-instance check.
env.workspace_registry = ws.registry.clone();
env
}
/// Checks the bodies of a single module in the context of the workspace.
/// Assumption: `module_globals` already contains the top-level symbol
/// tables for **all** modules of the workspace (including `m`) — built
/// by `build_module_globals`.
///
/// Returns **all** errors found in this module, in def declaration order:
///
/// - The type-def setup phase is fail-fast within the module (duplicate
/// type or ctor names corrupt the env, so we abort *this* module after
/// the first such error and let the outer loop continue with others).
/// - The body-check phase is multi-diagnose: each def is checked
/// independently against the assembled env; a failure is recorded and
/// the next def is attempted.
fn check_in_workspace(
m: &Module,
ws: &Workspace,
module_globals: &BTreeMap<String, ModuleGlobals>,
// synth-time warnings collected here so the caller can
// surface them into the workspace-wide diagnostic stream. Today
// only `class-method-shadowed-by-fn` flows through this channel
// (emitted from `synth` via `check_fn`'s warnings accumulator).
out_warnings: &mut Vec<Diagnostic>,
) -> Vec<CheckError> {
let mut env = build_check_env(ws);
let mut errors: Vec<CheckError> = Vec::new();
// Per-module overlay for `env.types` / `env.ctor_index`:
// `build_check_env` populates these workspace-flat, but the
// per-module pass needs only THIS module's local entries.
// Clear and rebuild so that:
// - duplicate-type / duplicate-ctor detection (the in-band
// errors below) sees only this module's defs;
// - bare-name lookups (e.g. local `Term::Ctor` synth)
// resolve against this module's types, not against the
// workspace-flat union.
// Cross-module `Pattern::Ctor` resolution no longer touches
// this overlay — that path is type-driven via `expected` and
// consults `env.module_types` directly (the canonical-type lookup refactor).
env.types.clear();
env.ctor_index.clear();
for def in &m.defs {
if let Def::Type(td) = def {
if env.types.contains_key(&td.name) {
errors.push(CheckError::Def(
td.name.clone(),
Box::new(CheckError::DuplicateType(td.name.clone())),
));
return errors;
}
for c in &td.ctors {
if let Some(prev) = env.ctor_index.get(&c.name) {
errors.push(CheckError::Def(
td.name.clone(),
Box::new(CheckError::DuplicateCtor {
ctor: c.name.clone(),
a: prev.type_name.clone(),
b: td.name.clone(),
}),
));
return errors;
}
env.ctor_index.insert(
c.name.clone(),
CtorRef { type_name: td.name.clone() },
);
}
env.types.insert(td.name.clone(), td.clone());
}
}
if let Some(g) = module_globals.get(&m.name) {
for (n, t) in &g.fns {
env.globals.insert(n.clone(), t.clone());
}
}
let mut import_map: BTreeMap<String, String> = BTreeMap::new();
for imp in &m.imports {
let key = imp.alias.clone().unwrap_or_else(|| imp.module.clone());
import_map.insert(key, imp.module.clone());
}
// Implicit-import set for the per-module body-check env
// (mirrors `build_check_env`'s sibling injection into
// `env.module_imports`): the literal name `"prelude"` (legacy
// singleton, kept unconditionally) PLUS every workspace module
// flagged `kernel: true`. The kernel-flag half mirrors the
// loader's filter at `crates/ailang-surface/src/loader.rs`
// that drives `implicit_imports` into `build_workspace`. The
// two halves are populated from different code paths (the
// workspace-wide table in `build_check_env`, the per-module
// table here), hence the apparent duplication. A user-declared
// explicit `import` of the same name is idempotent via
// `entry`. A module is not auto-imported into its own body.
// Fieldtest F3 surfaced that the previous code force-injected
// only `prelude`, leaving `raw_buf` and any future
// kernel-tier module unreachable from consumers even though
// the pre-pass freely produces such qualifiers.
if m.name != "prelude" {
import_map
.entry("prelude".to_string())
.or_insert_with(|| "prelude".to_string());
}
for km in ws.modules.values().filter(|km| km.kernel) {
if km.name != m.name {
import_map
.entry(km.name.clone())
.or_insert_with(|| km.name.clone());
}
}
env.imports = import_map;
env.current_module = m.name.clone();
env.current_module_kernel_tier = m.kernel || m.name == "prelude";
for def in &m.defs {
match check_def(def, &env, out_warnings) {
Ok(()) => {}
Err(e) => {
errors.push(CheckError::Def(def.name().to_string(), Box::new(e)));
}
}
}
// stamp the synth warnings with the module's name as `def`
// so the JSON consumer can correlate them with the surrounding
// module. The warning's `def` field carries the call-site def name
// already (set inside `check_fn`); the workspace-wide caller
// extends without further annotation.
errors
}
fn check_def(
def: &Def,
env: &Env,
out_warnings: &mut Vec<Diagnostic>,
) -> Result<()> {
match def {
Def::Fn(f) => check_fn(f, env, out_warnings),
Def::Const(c) => check_const(c, env, out_warnings),
Def::Type(td) => check_type_def(td, env),
// bugfix-instance-body-unbound-var (2026-05-13): each instance
// method body is walked through `check_fn` via a synthetic
// `FnDef` lifted from the `Term::Lam` the InstanceMethod body
// carries. This routes instance bodies through the same
// identifier-resolution path as fn bodies, so an unbound
// identifier inside an instance method fires `[unbound-var]`
// at `ail check` instead of slipping past and surfacing as a
// degraded "monomorphise_workspace: unknown identifier"
// diagnostic at `ail build`. Class-method substitution
// (class param → instance type) happens inside
// `check_instance` before the body-walk. Class-schema
// validation (InvalidSuperclassParam, etc.) and the workspace-
// load coherence checks (Orphan / Duplicate / MissingMethod)
// fire from `workspace::build_registry` independently, so a
// malformed instance never reaches this body-walk. `Def::Class`
// remains schema-only at this layer.
Def::Class(_) => Ok(()),
Def::Instance(inst) => check_instance(inst, env, out_warnings),
}
}
/// Route each `InstanceMethod` body through `check_fn` by wrapping
/// it in a synthetic `FnDef`. The InstanceMethod body is by
/// convention a `Term::Lam` carrying its own `param-types` / `ret-type`
/// (the canonical class-form shape); we extract its `param_tys` /
/// `ret_ty` / `params` / `body` into an `FnDef` shape and reuse the
/// existing fn-body-check machinery.
///
/// Class-method substitution: the on-disk Lam's `param_tys` / `ret_ty`
/// reference the class's type parameter directly (e.g. the prelude
/// `instance Eq Int` body declares `(typed x a) (typed y a)` with `a`
/// being `Eq`'s class param). Before handing to `check_fn` we look up
/// the class's `param` name via `env.class_methods` and substitute it
/// to the instance's concrete `type_`, using the existing
/// `substitute_rigids` helper on type positions and
/// `substitute_rigids_in_term` on the body (which targets any embedded
/// Type annotations on nested Lams / LetRecs). Without this step
/// `check_fn` would fire `polymorphic-not-supported` on the class
/// param appearing in non-Forall position.
///
/// The synthetic fn name is `"<class>::<method>"`, used only for
/// diagnostic strings.
///
/// Non-Lam method bodies are not part of the current schema (all
/// fixtures in the corpus and the convention reaffirmed when method dispatch became type-driven
/// use `Term::Lam`); they are silently skipped here. If a future
/// schema admits non-Lam shapes, this arm must be extended to walk
/// them — silent skip is the conservative choice today because
/// the pre-fix behaviour was also silent.
fn check_instance(
inst: &InstanceDef,
env: &Env,
out_warnings: &mut Vec<Diagnostic>,
) -> Result<()> {
let qualified_class = qualify_class_ref_in_check(&inst.class, &env.current_module);
for im in &inst.methods {
// Look up the class's param name. Workspace-load's MissingMethod
// gates this — if the (class, method) pair isn't in the table,
// the instance was structurally rejected upstream and we never
// get here in practice. Defensive fallback: skip substitution
// (body walks without class-param resolution).
let subst_map: BTreeMap<String, Type> = env
.class_methods
.get(&(qualified_class.clone(), im.name.clone()))
.map(|entry| {
let mut m = BTreeMap::new();
m.insert(entry.class_param.clone(), inst.type_.clone());
m
})
.unwrap_or_default();
let Term::Lam { params, param_tys, ret_ty, effects, body } = &im.body else {
// Non-Lam method body: skip (see fn-level doc-comment).
continue;
};
let subst_param_tys: Vec<Type> = param_tys
.iter()
.map(|t| substitute_rigids(t, &subst_map))
.collect();
let subst_ret_ty = substitute_rigids(ret_ty, &subst_map);
let subst_body = substitute_rigids_in_term(body, &subst_map);
let fn_ty = Type::fn_implicit(
subst_param_tys,
subst_ret_ty,
effects.clone(),
);
let synthetic = FnDef {
name: format!("{}::{}", inst.class, im.name),
ty: fn_ty,
params: params.clone(),
body: subst_body,
doc: None,
suppress: Vec::new(),
export: None,
};
check_fn(&synthetic, env, out_warnings)?;
}
Ok(())
}
fn check_type_def(td: &TypeDef, env: &Env) -> Result<()> {
// a parameterised ADT (`vars` non-empty) installs its
// type parameters as rigid vars while checking the ctor field
// types, so `List a = ... | Cons(a, List a)` resolves both
// occurrences of `a` and the recursive use of `List a` correctly.
let mut env = env.clone();
for v in &td.vars {
env.rigid_vars.insert(v.clone());
}
for c in &td.ctors {
for f in &c.fields {
check_type_well_formed(f, &env)?;
}
}
Ok(())
}
fn check_type_well_formed(t: &Type, env: &Env) -> Result<()> {
match t {
Type::Con { name, args } => {
let is_primitive = ailang_core::primitives::is_primitive_name(name);
if is_primitive {
if !args.is_empty() {
return Err(CheckError::UnknownType(format!(
"{name} (primitive does not take type args)"
)));
}
return Ok(());
}
// a qualified type name `module.Type` resolves
// through the import map and the per-module type table.
// prep.1: a bare type name also resolves to any workspace
// TypeDef of that name (TypeDef-first ladder), symmetric
// to the `Term::Var` and `Term::Ctor` arms. This makes
// `(con Maybe a)` in a consumer module's type signature
// resolve when `Maybe` lives in an imported (explicit or
// implicit) module — matching the canonical-form rule
// already accepted by the workspace validator.
let td_opt: Option<&TypeDef> = if name.matches('.').count() == 1 {
let (prefix, suffix) = name.split_once('.').expect("checked");
let target_module = match env.imports.get(prefix) {
Some(m) => m.as_str(),
None => {
return Err(CheckError::UnknownModule {
module: prefix.to_string(),
});
}
};
env.module_types
.get(target_module)
.and_then(|tys| tys.get(suffix))
} else if let Some(td) = env.types.get(name) {
Some(td)
} else {
env.module_types
.values()
.find_map(|types| types.get(name))
};
if let Some(td) = td_opt {
if td.vars.len() != args.len() {
return Err(CheckError::UnknownType(format!(
"{name} expects {} type arg(s), got {}",
td.vars.len(),
args.len()
)));
}
// prep.3 (kernel-extension-mechanics): `param-in`
// enforcement. Every restricted var must have its
// corresponding positional arg's outermost type-name
// in the allowed set. Non-Con arg-types (vars, fn
// types, etc.) are not currently restrictable — the
// spec scopes `param-in` to closed-set named types.
for (var, allowed) in &td.param_in {
let Some(pos) = td.vars.iter().position(|v| v == var) else {
continue;
};
let Some(arg_ty) = args.get(pos) else {
continue;
};
if let Type::Con { name: arg_name, .. } = arg_ty {
if !allowed.contains(arg_name) {
return Err(CheckError::ParamNotInRestrictedSet {
type_name: name.clone(),
var: var.clone(),
found: arg_name.clone(),
allowed: allowed.iter().cloned().collect(),
});
}
}
}
for a in args {
check_type_well_formed(a, env)?;
}
Ok(())
} else {
Err(CheckError::UnknownType(name.clone()))
}
}
Type::Fn { params, ret, .. } => {
for p in params {
check_type_well_formed(p, env)?;
}
check_type_well_formed(ret, env)
}
Type::Var { name } => {
// Rigid var: legal iff it is in scope. Used inside a forall
// body when checking a polymorphic def, or inside a
// parameterised ADT's ctor fields.
if env.rigid_vars.contains(name) {
Ok(())
} else {
Err(CheckError::PolymorphicNotSupported("type def".into()))
}
}
Type::Forall { .. } => {
// ADT fields and lambda annotations cannot themselves be
// polymorphic — only top-level def types may carry a Forall.
Err(CheckError::PolymorphicNotSupported("type def".into()))
}
}
}
/// `true` when `f`'s body is an `(intrinsic)` marker: either the body
/// is `Term::Intrinsic` directly (a top-level intrinsic fn) or it is a
/// `Term::Lam` whose inner body is `Term::Intrinsic` (a synthesised
/// instance method). Such a body is signature-only — the typechecker
/// validates the signature and skips body inference, and the mono pass
/// collects no targets from it. Shared by `check_fn` and the mono
/// pass's `synth`-re-entry sites (`mono::collect_mono_targets`,
/// `mono::collect_residuals_ordered`) so every synth-on-body path
/// applies the same skip.
pub(crate) fn is_intrinsic_body(f: &FnDef) -> bool {
matches!(f.body, Term::Intrinsic)
|| matches!(&f.body, Term::Lam { body, .. } if matches!(**body, Term::Intrinsic))
}
fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<()> {
// Peel an outer Forall (Iter 12a). The vars become rigid in the
// inner env so they pass `check_type_well_formed` and unify only
// with themselves. An empty `vars` list (vacuously polymorphic)
// gets normalised to a non-polymorphic body.
let (rigids, inner_ty): (Vec<String>, Type) = match &f.ty {
Type::Forall { vars, constraints: _, body } => (vars.clone(), (**body).clone()),
other => (vec![], other.clone()),
};
let (param_tys, ret_ty, declared_effs) = match &inner_ty {
Type::Fn { params, ret, effects, .. } => {
(params.clone(), (**ret).clone(), effects.clone())
}
other => {
return Err(CheckError::FnTypeRequired(
f.name.clone(),
ailang_core::pretty::type_to_string(other),
));
}
};
if f.params.len() != param_tys.len() {
return Err(CheckError::ParamCountMismatch {
name: f.name.clone(),
ty_count: param_tys.len(),
param_count: f.params.len(),
});
}
// Install rigid vars. Cloning the env keeps the parent immutable
// and the rigid set scoped to this def.
let mut env = env.clone();
for v in &rigids {
env.rigid_vars.insert(v.clone());
}
// validate the declared parameter and return types
// against the type environment. Catches misuses like
// `Box<Int, Bool>` (arity mismatch on a parameterised ADT) before
// they leak into the body and produce confusing downstream errors.
for p in &param_tys {
check_type_well_formed(p, &env)?;
}
check_type_well_formed(&ret_ty, &env)?;
// An `(intrinsic)` body is signature-only: the signature is already
// validated above; codegen supplies the implementation via the
// intercept registry. The body is `Term::Intrinsic` directly (a
// top-level intrinsic fn) or a `Term::Lam` whose inner body is
// `Term::Intrinsic` (a synthesised instance method). Skip body
// inference, but first gate the honesty rule: an intrinsic body is
// legal only in a kernel-tier module or the prelude.
if is_intrinsic_body(f) {
if !env.current_module_kernel_tier {
return Err(CheckError::IntrinsicOutsideKernelTier {
def: f.name.clone(),
module: env.current_module.clone(),
});
}
return Ok(());
}
// Embedding-ABI gate (M1 scalars / M2 ctx / M3 record): an
// `(export …)` fn is the C call boundary. Its signature must be
// C-ABI-permitted — `Int`/`Float`, or a single-constructor
// record of those (M3) — and pure. Gate order: params → ret →
// effects, first violation wins (so a combined Str+IO export
// deterministically fails on the signature). Unconditional at
// check-time — independent of the codegen emit mode — this IS
// the clause-3 discriminator.
if f.export.is_some() {
fn is_c_scalar(t: &Type) -> bool {
matches!(t, Type::Con { name, args, .. }
if args.is_empty() && (name == "Int" || name == "Float"))
}
// M3 (spec 2026-05-18-embedding-abi-m3 §Architecture): a C
// scalar, OR a single-constructor `data` whose every field is a
// *bare* C scalar. Two-level by design — a record-typed field
// stays rejected (M4 owns nested-record recursion). Uses the
// in-scope `env.types: String -> TypeDef` (cf. lib.rs:1826).
fn is_c_abi_type(t: &Type, env: &Env) -> bool {
if is_c_scalar(t) {
return true;
}
if let Type::Con { name, args, .. } = t {
if args.is_empty() {
if let Some(td) = env.types.get(name) {
if td.ctors.len() == 1 {
return td.ctors[0]
.fields
.iter()
.all(is_c_scalar);
}
}
}
}
false
}
for p in &param_tys {
if !is_c_abi_type(p, &env) {
return Err(CheckError::ExportNonScalarSignature(
f.name.clone(),
"parameter",
ailang_core::pretty::type_to_string(p),
));
}
}
if !is_c_abi_type(&ret_ty, &env) {
return Err(CheckError::ExportNonScalarSignature(
f.name.clone(),
"return",
ailang_core::pretty::type_to_string(&ret_ty),
));
}
if !declared_effs.is_empty() {
return Err(CheckError::ExportHasEffects(
f.name.clone(),
declared_effs.clone(),
));
}
}
// build the post-superclass-expansion declared-constraint
// set ONCE here and stash on env, so synth's Var-arm class-method
// branch can hand it to `resolve_method_dispatch`'s constraint-
// driven filter. The post-synth missing-constraint check below
// re-reads the same expanded list from env to keep one source of
// truth.
//
// Canonical-class-form follow-on: declared constraints carry the canonical-form
// `class` value (bare for same-module, qualified for cross-module).
// Lift to the workspace-key shape (always qualified) before
// expanding — residuals always carry qualified `class` because
// they come from `ClassMethodEntry.class_name` which is qualified
// post-canonical-class-form
let declared_constraints: Vec<Constraint> = match &f.ty {
Type::Forall { constraints, .. } => constraints
.iter()
.map(|c| Constraint {
class: qualify_class_ref_in_check(&c.class, &env.current_module),
type_: c.type_.clone(),
})
.collect(),
_ => Vec::new(),
};
env.active_declared_constraints =
expand_declared_constraints(&declared_constraints, &env.class_superclasses);
let mut locals = IndexMap::new();
for (n, t) in f.params.iter().zip(param_tys.iter()) {
locals.insert(n.clone(), t.clone());
}
let mut effects = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
// Per-fn residual class constraints. Every call to a class method
// inside the body pushes a [`ResidualConstraint`] here; after the
// body finishes, we compare against the expanded declared set.
let mut residuals: Vec<ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
let mut warnings: Vec<Diagnostic> = Vec::new();
// loop-recur iter 2: fresh per-fn-body loop-binder-type stack.
// Empty at fn entry; pushed/popped by `Term::Loop` arms during
// the synth walk; discarded after the body type-checks.
let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
let body_ty = synth(&f.body, &env, &mut locals, &mut loop_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
unify(&ret_ty, &body_ty, &mut subst)?;
// surface synth-time warnings into the caller-supplied
// accumulator. The warnings already carry `def: Some(f.name)`
// set inside synth's emission site.
out_warnings.extend(warnings);
// tail-position verification (the explicit-tail-call contract). Runs after
// the main type-check so that a tail-call marker on a malformed
// call doesn't drown out the underlying type error.
verify_tail_positions(&f.body, true)?;
// loop-recur iter 2: recur-in-tail-position verification. Runs
// after synth (so RecurOutsideLoop/arity/type take code-
// precedence) and alongside verify_tail_positions (sibling, not
// a repurpose — verify_tail_positions' tail-app role is frozen).
verify_loop_body(&f.body, false)?;
let declared: BTreeSet<String> = declared_effs.into_iter().collect();
for e in &effects {
if !declared.contains(e) {
return Err(CheckError::UndeclaredEffect(e.clone()));
}
}
// missing-constraint check. The expanded
// declared-constraint set (declared + one-step superclass per
// the typeclass design) was computed pre-synth and stashed on
// `env.active_declared_constraints`. Var-shaped residuals
// not covered by the expanded set fire `MissingConstraint`. Concrete
// residuals are deferred to Task 10's `no-instance` arm.
let expanded = &env.active_declared_constraints;
for r in &residuals {
let r_ty = subst.apply(&r.type_);
// multi-candidate residuals refine before the existing
// single-class discharge path. `MethodNameCollision` keeps the
// candidate set singleton in real workspaces today; this branch
// is exercised exclusively by unit tests until the type-driven dispatch refactor.
if r.candidates.is_some() {
// Normalize the type before hashing — same contract as the
// single-class path below.
let r_ty_norm = env
.workspace_registry
.normalize_type_for_lookup(env.current_module.as_str(), &r_ty);
let normalized_residual = ResidualConstraint {
class: r.class.clone(),
type_: r_ty_norm,
method: r.method.clone(),
candidates: r.candidates.clone(),
};
let registry_unit: BTreeMap<(String, String), ()> = env
.workspace_registry
.entries
.keys()
.map(|k| (k.clone(), ()))
.collect();
match refine_multi_candidate_residual(
&normalized_residual,
expanded,
&registry_unit,
) {
RefineOutcome::Resolved(_) => {
// Discharge succeeded — the resolved class has an
// instance for this concrete type (or the rigid
// var has a matching declared constraint). Move
// on to the next residual; nothing to push.
continue;
}
RefineOutcome::NoInstance { method, at_type, candidate_classes } => {
return Err(CheckError::NoInstance {
def: f.name.clone(),
method,
class: r.class.clone(),
at_type,
candidate_classes,
});
}
RefineOutcome::Ambiguous { method, at_type, candidate_classes } => {
return Err(CheckError::AmbiguousMethodResolution {
method,
at_type,
candidate_classes,
});
}
RefineOutcome::MissingConstraint { method, candidate_classes } => {
return Err(CheckError::MissingConstraint {
def: f.name.clone(),
method,
class: candidate_classes.first().cloned().unwrap_or_default(),
at_type: ailang_core::pretty::type_to_string(&r_ty),
});
}
}
}
if let Type::Var { name } = &r_ty {
// Skip residuals over metavars (`$mN`) — those mean the
// residual is over a value the body never connected to a
// rigid var; treat as concrete-uncovered, which Task 10
// will handle. Only rigid (source-level) vars participate
// in the missing-constraint check here.
if Subst::meta_id(name).is_some() {
continue;
}
let satisfied = expanded
.iter()
.any(|d| d.class == r.class && constraint_type_matches(&d.type_, &r_ty));
if !satisfied {
return Err(CheckError::MissingConstraint {
def: f.name.clone(),
method: r.method.clone(),
class: r.class.clone(),
at_type: name.clone(),
});
}
} else if is_fully_concrete(&r_ty) {
// fully-concrete residual — the class
// method was called at a concrete type, so the obligation
// can only be discharged by an existing workspace instance.
// Look up `(class, type_hash(r_ty))` in the registry; absence
// → no-instance. The hash uses `canonical::type_hash`, the
// same key shape `workspace::build_registry` writes with, so
// representation-equal types match deterministically.
// normalize to match Registry::normalize_type_for_lookup contract
let r_ty_norm = env
.workspace_registry
.normalize_type_for_lookup(env.current_module.as_str(), &r_ty);
let key = (
r.class.clone(),
ailang_core::canonical::type_hash(&r_ty_norm),
);
if !env.workspace_registry.entries.contains_key(&key) {
return Err(CheckError::NoInstance {
def: f.name.clone(),
method: r.method.clone(),
class: r.class.clone(),
at_type: ailang_core::pretty::type_to_string(&r_ty),
candidate_classes: vec![],
});
}
}
// Other shapes (unsolved metavars inside a `Type::Con`,
// `Type::Fn`, `Type::Forall`) are out of scope for the 22b.2
// diagnostics: metavars mean the body never connected the
// class param to anything observable, and `Fn`/`Forall` cannot
// appear as instance heads (the typeclass design).
}
Ok(())
}
/// true iff the type tree contains no `Type::Var`
/// at any depth. A fully-concrete type is the only shape eligible for
/// the no-instance lookup — anything carrying a metavar / rigid-var
/// component is either covered by the missing-constraint check or
/// genuinely under-specified at the call site.
pub(crate) fn is_fully_concrete(t: &Type) -> bool {
match t {
Type::Con { args, .. } => args.iter().all(is_fully_concrete),
Type::Var { .. } => false,
Type::Fn { params, ret, .. } => {
params.iter().all(is_fully_concrete) && is_fully_concrete(ret)
}
Type::Forall { body, .. } => is_fully_concrete(body),
}
}
/// per-call-site residual class constraint
/// recorded by `synth` when a `Term::Var` resolves to a class method.
/// Carries the method name (for diagnostic rendering), the class, and
/// the type the class is applied to at the call site. The type is
/// typically a fresh metavar (which unification then ties to the
/// argument's actual type) or, after `subst.apply`, a rigid var or a
/// concrete `Type::Con`.
#[derive(Debug, Clone)]
pub struct ResidualConstraint {
/// Class name (e.g. `Show`).
///
/// When [`Self::candidates`] is `None`, this is the resolved class
/// (single-class dispatch path). When `Some(set)`, this is a
/// tentative value (typically the first set element in BTreeSet
/// order); discharge / mono refinement overwrites it with the
/// actually-resolved class.
pub class: String,
/// Class param's instance at this call site. Pre-substitution: the
/// fresh metavar inserted at the Var site. Post-substitution: the
/// solved type — rigid var, concrete con, or unsolved metavar.
pub type_: Type,
/// Method name (e.g. `show`); used by the missing-constraint
/// diagnostic to point the author at which call site triggered
/// the residual.
pub method: String,
/// candidate-class set for the multi-candidate dispatch
/// path. `None` ⇒ single-class semantics (pre-canonical-class-form behaviour);
/// the [`Self::class`] field is the resolved class. `Some(set)`
/// ⇒ multi-candidate residual; discharge / mono refinement filters
/// the set at fn-body-end. With `MethodNameCollision` still active
/// (pre-canonical-class-form), real workspaces only ever construct `None`-candidate
/// residuals; the `Some`-path is exercised exclusively by unit
/// tests until the type-driven dispatch refactor retires the workaround.
pub candidates: Option<BTreeSet<String>>,
}
/// outcome of the dispatch-resolution helper
/// [`resolve_method_dispatch`]. The synth Var-arm consumer translates
/// this enum into either a singleton [`ResidualConstraint`]
/// (`Resolved`) or a multi-candidate residual (`Multi`) for discharge-
/// time refinement, or a `CheckError` (`Unknown` / `Ambiguous`).
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum MethodDispatchOutcome {
/// Single class resolved unambiguously.
Resolved(String),
/// Explicit qualifier names a class not in the candidate set.
UnknownClass(String),
/// Bare-method call site survived both type-driven and
/// constraint-driven filters with > 1 candidate.
Ambiguous {
method: String,
at_type: String,
candidates: Vec<String>,
},
/// Bare-method call site with multiple candidates that need
/// discharge-time refinement (rigid var type at synth time;
/// concrete type only available at discharge).
Multi {
method: String,
candidates: BTreeSet<String>,
},
}
/// resolve a method-call site per the spec's 5-step rule. Pure
/// function — no Env mutation, no residual emission.
///
/// `qualifier_prefix` is the dot-stripped class prefix (e.g.
/// `"prelude.Show"` for a `Term::Var.name == "prelude.Show.show"`).
/// `None` = bare method form.
///
/// `concrete_arg_type` is `Some` when the caller has the arg type
/// available (e.g. discharge-time refinement); `None` when synth is at
/// the Var arm before App-arm unification. When `None`, the helper
/// emits `Multi` if the candidate set is non-singleton (no early
/// type-driven filter possible). When `Some(t)` with `t` a non-rigid
/// concrete type, the type-driven filter applies; when `t` is a rigid
/// `Type::Var`, the constraint-driven filter applies.
///
/// `declared_constraints` are the active forall-bound constraints in
/// scope at the call site; consulted for the rigid-var fallback.
///
/// `registry` is the workspace registry keyed by `(qualified_class,
/// type_hash)` for instance-existence checks. Values are unit; only
/// key presence matters.
pub fn resolve_method_dispatch(
method: &str,
qualifier_prefix: Option<&str>,
candidates: &BTreeSet<String>,
concrete_arg_type: Option<&Type>,
declared_constraints: &[ailang_core::ast::Constraint],
registry: &BTreeMap<(String, String), ()>,
) -> MethodDispatchOutcome {
// Step 3 (5-step rule): explicit qualifier present.
if let Some(q) = qualifier_prefix {
if candidates.contains(q) {
return MethodDispatchOutcome::Resolved(q.to_string());
}
return MethodDispatchOutcome::UnknownClass(q.to_string());
}
// Step 4: bare-method form, singleton candidate set — pre-canonical-class-form
// path. Returns immediately so the post-canonical-class-form multi-candidate
// logic below stays gated on a non-singleton candidate set.
if candidates.len() == 1 {
return MethodDispatchOutcome::Resolved(
candidates.iter().next().cloned().unwrap(),
);
}
// Multi-candidate path: type-driven filter first when the arg
// type is concrete (non-Var).
let concrete = concrete_arg_type
.filter(|t| !matches!(t, Type::Var { .. }));
if let Some(t) = concrete {
let type_h = ailang_core::canonical::type_hash(t);
let survivors: BTreeSet<String> = candidates
.iter()
.filter(|c| registry.contains_key(&((**c).clone(), type_h.clone())))
.cloned()
.collect();
if survivors.len() == 1 {
return MethodDispatchOutcome::Resolved(
survivors.into_iter().next().unwrap(),
);
}
if survivors.len() > 1 {
let mut sorted: Vec<String> = survivors.into_iter().collect();
sorted.sort();
let at_type = ailang_core::pretty::type_to_string(t);
return MethodDispatchOutcome::Ambiguous {
method: method.to_string(),
at_type,
candidates: sorted,
};
}
// Zero survivors after the type-driven filter: fall through
// to constraint-driven filter, then `Multi` for discharge-
// time refinement (where `NoInstance` with `candidate_classes`
// is fired against the full candidate set).
}
// Constraint-driven filter (rigid-var case or no concrete arg).
let survivors: BTreeSet<String> = candidates
.iter()
.filter(|c| {
declared_constraints
.iter()
.any(|dc| &dc.class == *c)
})
.cloned()
.collect();
if survivors.len() == 1 {
return MethodDispatchOutcome::Resolved(
survivors.into_iter().next().unwrap(),
);
}
// No filter narrowed; emit `Multi` for discharge-time refinement.
MethodDispatchOutcome::Multi {
method: method.to_string(),
candidates: candidates.clone(),
}
}
/// outcome of multi-candidate residual refinement at discharge
/// time. Consumed by `check_fn`'s residual loop and by mono's
/// residual-to-target mapping.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum RefineOutcome {
/// Refinement converged on a single class.
Resolved(String),
/// Concrete `type_` with zero registry survivors — the call site
/// must be discharged via an existing instance, but none of the
/// candidate classes has one for this type. Surfaces as a
/// `CheckError::NoInstance` with the full candidate set populated.
NoInstance {
method: String,
at_type: String,
candidate_classes: Vec<String>,
},
/// Concrete `type_` with multiple registry survivors — every
/// surviving candidate has an instance for this type; the author
/// must disambiguate explicitly. Surfaces as a
/// `CheckError::AmbiguousMethodResolution`.
Ambiguous {
method: String,
at_type: String,
candidate_classes: Vec<String>,
},
/// Rigid-var residual with non-singleton constraint-set survivors.
/// Surfaces as a `CheckError::MissingConstraint` (the body must
/// declare a constraint to commit to one of the candidates).
MissingConstraint {
method: String,
candidate_classes: Vec<String>,
},
}
/// refine a multi-candidate residual at discharge time per the
/// spec's 5-step rule (constraint-discharge refinement subsection).
/// Caller MUST pass a residual whose `candidates` is `Some(...)`;
/// single-candidate residuals (`candidates: None`) bypass this helper
/// and discharge directly against the registry as in pre-canonical-class-form
///
/// Refinement strategy:
/// - Concrete `type_`: filter the candidate set against the registry
/// keyed on `(class, type_hash(type_))`. 0 survivors → `NoInstance`;
/// 1 → `Resolved`; >1 → `Ambiguous`.
/// - Rigid-var `type_`: filter the candidate set against the active
/// declared-constraint list. 1 survivor → `Resolved`; otherwise
/// → `MissingConstraint`.
pub fn refine_multi_candidate_residual(
residual: &ResidualConstraint,
declared_constraints: &[ailang_core::ast::Constraint],
registry: &BTreeMap<(String, String), ()>,
) -> RefineOutcome {
let candidates = residual
.candidates
.as_ref()
.expect("refine_multi_candidate_residual called on single-candidate residual");
// Concrete-type path.
if !matches!(residual.type_, Type::Var { .. }) {
let type_h = ailang_core::canonical::type_hash(&residual.type_);
let survivors: Vec<String> = candidates
.iter()
.filter(|c| registry.contains_key(&((**c).clone(), type_h.clone())))
.cloned()
.collect();
let at_type = ailang_core::pretty::type_to_string(&residual.type_);
return match survivors.len() {
0 => RefineOutcome::NoInstance {
method: residual.method.clone(),
at_type,
candidate_classes: candidates.iter().cloned().collect(),
},
1 => RefineOutcome::Resolved(survivors.into_iter().next().unwrap()),
_ => {
let mut sorted = survivors;
sorted.sort();
RefineOutcome::Ambiguous {
method: residual.method.clone(),
at_type,
candidate_classes: sorted,
}
}
};
}
// Rigid-var path: filter against declared constraints requiring
// BOTH class-name match AND type-unification with the residual's
// `type_` (per spec §"Constraint-discharge refinement" 130-138).
// `constraint_type_matches` is the post-`subst.apply` Var/Con
// recursive matcher; the residual's `type_` has been `subst.apply`-d
// by the discharge caller, so rigid-var identity (Var("a") vs
// Var("b")) is a direct name comparison.
let survivors: Vec<String> = candidates
.iter()
.filter(|c| {
declared_constraints.iter().any(|dc| {
&dc.class == *c && constraint_type_matches(&dc.type_, &residual.type_)
})
})
.cloned()
.collect();
match survivors.len() {
1 => RefineOutcome::Resolved(survivors.into_iter().next().unwrap()),
_ => RefineOutcome::MissingConstraint {
method: residual.method.clone(),
candidate_classes: candidates.iter().cloned().collect(),
},
}
}
/// per-call-site polymorphic-free-fn observation recorded by
/// `synth` when a `Term::Var` resolves to a `Type::Forall`-quantified
/// top-level def (NOT a class method — those are pushed to
/// [`ResidualConstraint`] instead). Carries the bare name, the owning
/// module (resolved through the same lookup ladder as `synth`'s Var arm),
/// the polymorphic source's `Forall.vars` (declaration order), and the
/// fresh metavars instantiated for those vars at the call site.
///
/// Consumed by the mono pass: after `synth` completes a body, each
/// `metas\[i\]` is `subst.apply`'d to recover the concrete type at `vars\[i\]`.
/// Fully-concrete observations become [`crate::mono::MonoTarget::FreeFn`]
/// targets; non-concrete observations are silently dropped (covered by
/// the missing-constraint check on residuals if relevant).
#[derive(Debug, Clone)]
pub struct FreeFnCall {
/// Bare name of the polymorphic def at the call site.
pub name: String,
/// Module in which the polymorphic `Def::Fn` is declared, resolved
/// through `synth`'s lookup ladder (current module's globals,
/// implicitly-imported module's globals, or the dot-qualified
/// `prefix.name` path's target module).
pub owner_module: String,
/// The `Forall.vars` of the source def (declaration order).
pub forall_vars: Vec<String>,
/// Fresh metavars instantiated at this call site — same length as
/// `forall_vars`, same order. Post-`synth`, `subst.apply(&metas[i])`
/// yields the concrete type for `forall_vars[i]` iff the call site's
/// substitution was fully pinned.
pub metas: Vec<Type>,
/// The TypeDef scope the call resolved through, when it was
/// spelled type-scoped (`T.f`, prep.1) — `Some("RawBuf")` for
/// `RawBuf.new`, `Some("RawBuf")` for `RawBuf.get`. `None` for a
/// bare / dot-qualified / local resolution. raw-buf.3: drives the
/// scope-qualified mono symbol `T_f__<elem>` so two types' ops
/// of the same name never collide.
pub scope: Option<String>,
}
/// lift a canonical-form class-ref value to the qualified
/// workspace-key shape. Bare ⇒ prepend `caller_module` (the bare
/// form names the caller-module-local class under the canonical-form
/// rule); qualified ⇒ as-is. Sibling of `workspace::qualify_class_ref`
/// for the check-side; duplicated to keep `ailang-check` from
/// reaching across crates for one private helper.
pub(crate) fn qualify_class_ref_in_check(class_ref: &str, caller_module: &str) -> String {
if class_ref.contains('.') {
class_ref.to_string()
} else {
format!("{caller_module}.{class_ref}")
}
}
/// split a `Term::Var.name` into `(method_name,
/// optional_qualifier_prefix)` at the last dot.
///
/// - `"show"` → `("show", None)`
/// - `"prelude.Show.show"` → `("show", Some("prelude.Show"))`
/// - `"Show.show"` → `("show", Some("Show"))`
/// - `"std_list.length"` → `("length", Some("std_list"))`
///
/// Callers distinguish class qualifiers from cross-module-fn
/// qualifiers via [`qualifier_is_class_shape`]: PascalCase
/// single-segment prefixes (e.g. `"Show"`) and multi-segment
/// prefixes (e.g. `"prelude.Show"`) are class qualifiers per
/// the canonical-class-form rule; lowercase single-segment prefixes
/// (e.g. `"std_list"`) are module names and the caller falls
/// through to the cross-module-fn path.
pub(crate) fn parse_method_qualifier(name: &str) -> (&str, Option<String>) {
if let Some(dot_idx) = name.rfind('.') {
(&name[dot_idx + 1..], Some(name[..dot_idx].to_string()))
} else {
(name, None)
}
}
/// mq.tidy: predicate gating the synth Var-arm's class-method
/// dispatch entry on the qualifier shape. Accepts:
/// - bare-method form (qualifier absent), e.g. `"show"`.
/// - bare-class qualifier, e.g. `"Show.show"` — class names are
/// PascalCase per repo convention (first character uppercase).
/// - module-qualified class qualifier, e.g. `"prelude.Show.show"`.
///
/// Rejects qualifier shapes that look like cross-module-fn calls
/// (`"std_list.length"`): qualifier starts with lowercase, no
/// inner dot — falls through to the qualified-fn arm.
pub(crate) fn qualifier_is_class_shape(qualifier_opt: &Option<String>) -> bool {
match qualifier_opt {
None => true,
Some(q) => {
// Contains inner dot: module-qualified class
// (`prelude.Show`).
if q.contains('.') {
return true;
}
// Single segment: class iff the first char is uppercase
// (PascalCase convention).
q.chars().next().map(|c| c.is_uppercase()).unwrap_or(false)
}
}
}
/// Type-driven dispatch entry predicate: the synth Var-arm runs this to
/// decide whether `name` should be routed through the class-method
/// dispatch helper. Matches a bare method name (e.g. `"show"`) or a
/// class-shaped qualifier (`"Show.show"`, `"prelude.Show.show"`).
/// A 1-dot lowercase name (`"std_list.length"`) is structurally a
/// cross-module-fn call per the canonical-class-form rule's canonical-form rule and falls
/// through to the qualified-fn arm.
fn is_class_method_dispatch(name: &str, env: &Env) -> bool {
let (method_name, qualifier_opt) = parse_method_qualifier(name);
qualifier_is_class_shape(&qualifier_opt)
&& env.method_to_candidate_classes.contains_key(method_name)
}
/// mq.tidy: predicate for the `class-method-shadowed-by-fn`
/// warning emission. The full spec rule (§"Class-fn collisions"
/// 161-162) requires a class candidate WITH AN INSTANCE FOR THE
/// ACTUAL ARG TYPE; the arg type is unavailable at the synth
/// Var-arm where the warning fires (App-arm unification has not
/// run yet). This conservative approximation requires only that
/// at least one candidate class has SOME instance in the
/// workspace registry — stricter than today's "any class
/// declares the method" (which fires even for class methods
/// with zero instances anywhere), looser than the full spec
/// rule. A future tighten can defer the warning emission to a
/// later pass where the arg type is known.
pub(crate) fn any_candidate_class_has_instance(
method_to_candidate_classes: &BTreeMap<String, BTreeSet<String>>,
workspace_registry_entries: &BTreeMap<(String, String), ()>,
method_name: &str,
) -> bool {
let Some(cands) = method_to_candidate_classes.get(method_name) else {
return false;
};
cands.iter().any(|c| {
// BTreeMap is ordered lexicographically on the tuple key;
// `range((c, "")..).next()` is the first entry whose first
// component is >= `c`. The check `k == c` rejects spillover
// into the next class. O(log n) per candidate.
workspace_registry_entries
.range((c.clone(), String::new())..)
.next()
.map(|((k, _), _)| k == c)
.unwrap_or(false)
})
}
/// expand a list of declared class constraints
/// with their one-step superclass closure (the typeclass design). For every
/// declared `(C, t)`, append `(S, t)` if class `C` has a superclass
/// `S`. Only one step — The typeclass design forbids deeper chains. The
/// expanded list is what [`check_fn`] uses to decide whether a
/// residual is satisfied.
fn expand_declared_constraints(
declared: &[Constraint],
class_superclasses: &BTreeMap<String, String>,
) -> Vec<Constraint> {
let mut out: Vec<Constraint> = declared.to_vec();
for c in declared {
if let Some(sc) = class_superclasses.get(&c.class) {
out.push(Constraint {
class: sc.clone(),
type_: c.type_.clone(),
});
}
}
out
}
/// equality of constraint types for the
/// missing-constraint match. The residual type has been
/// `subst.apply`-d, so two rigid vars match iff their names are equal;
/// a `Type::Con` matches another `Type::Con` iff their head names and
/// args agree. Conservative: anything outside `Var` / `Con` is rejected
/// (the schema bounds Constraint.type_ to plain types, and Task 9 only
/// fires on Var residuals anyway).
fn constraint_type_matches(declared: &Type, residual: &Type) -> bool {
match (declared, residual) {
(Type::Var { name: a }, Type::Var { name: b }) => a == b,
(Type::Con { name: a, args: aa }, Type::Con { name: b, args: ba }) => {
a == b
&& aa.len() == ba.len()
&& aa.iter().zip(ba.iter()).all(|(x, y)| constraint_type_matches(x, y))
}
_ => false,
}
}
/// verifies that every `Term::App { tail: true, .. }` and
/// `Term::Do { tail: true, .. }` actually sits in tail position, per
/// the explicit-tail-call contract
/// (`design/contracts/0012-tail-calls.md`).
///
/// `is_tail` is the tail-context flag for the term currently being
/// visited. The propagation rules (from design/contracts/0012-tail-calls.md):
///
/// - The body of a fn / Lam is visited with `is_tail = true`.
/// - `Match { scrutinee, arms }`: the scrutinee is **not** in tail
/// position; each arm body inherits the same `is_tail` as the match.
/// - `Seq { lhs, rhs }`: lhs is non-tail; rhs inherits.
/// - `Let { value, body, .. }`: value is non-tail; body inherits.
/// - `App { callee, args, tail }`: the callee and all args are
/// non-tail. If `tail == true`, the App itself must have arrived
/// with `is_tail == true`; otherwise diagnostic.
/// - `Do { args, tail }`: same rule as App; all args are non-tail.
/// - `Ctor { args }`: all args are non-tail.
/// - `Lam { body }`: the Lam value is at whatever `is_tail` was; the
/// recursion **into** the body opens a fresh tail scope (the body
/// is visited with `is_tail = true`).
/// - `Lit`, `Var`: leaves; no further descent.
pub fn verify_tail_positions(t: &Term, is_tail: bool) -> Result<()> {
match t {
Term::Lit { .. } | Term::Var { .. } => Ok(()),
Term::App { callee, args, tail } => {
if *tail && !is_tail {
return Err(CheckError::TailCallNotInTailPosition);
}
verify_tail_positions(callee, false)?;
for a in args {
verify_tail_positions(a, false)?;
}
Ok(())
}
Term::Do { args, tail, .. } => {
if *tail && !is_tail {
return Err(CheckError::TailCallNotInTailPosition);
}
for a in args {
verify_tail_positions(a, false)?;
}
Ok(())
}
Term::Let { value, body, .. } => {
verify_tail_positions(value, false)?;
verify_tail_positions(body, is_tail)
}
Term::If { cond, then, else_ } => {
verify_tail_positions(cond, false)?;
verify_tail_positions(then, is_tail)?;
verify_tail_positions(else_, is_tail)
}
Term::Seq { lhs, rhs } => {
verify_tail_positions(lhs, false)?;
verify_tail_positions(rhs, is_tail)
}
Term::Match { scrutinee, arms } => {
verify_tail_positions(scrutinee, false)?;
for arm in arms {
verify_tail_positions(&arm.body, is_tail)?;
}
Ok(())
}
Term::Ctor { args, .. } => {
for a in args {
verify_tail_positions(a, false)?;
}
Ok(())
}
Term::Lam { body, .. } => {
// Entering a Lam body opens a fresh tail scope.
verify_tail_positions(body, true)
}
Term::LetRec { body, in_term, .. } => {
// `Term::LetRec` may now survive the desugar
// pass (when it captures `Term::Let`-bound names whose
// types are only known after typecheck). The body is the
// body of a fn-typed binding; the recursive name is what
// gets tail-called, so `body` is NOT in tail position. The
// in-clause IS in tail position iff the enclosing context
// is — same propagation rule as `Term::Let.body`.
verify_tail_positions(body, false)?;
verify_tail_positions(in_term, is_tail)
}
Term::Clone { value } => {
// clone is identity. Tail-position propagates
// through unchanged — `(clone tail-call)` is a tail call.
verify_tail_positions(value, is_tail)
}
Term::ReuseAs { source, body } => {
// reuse-as is identity at codegen. The `source`
// is a side-effect-free Var in shipping fixtures, so it is
// not a tail call; the `body` is the value of the whole
// expression and inherits the enclosing tail position.
verify_tail_positions(source, false)?;
verify_tail_positions(body, is_tail)
}
// loop-recur iter 1: binder inits are evaluated once on loop
// entry, NOT in tail position. The loop body inherits the
// enclosing tail position (the loop's value is the body's
// value on the exiting iteration). This arm only defines
// tail-app descent through the new node; it makes NO claim
// about recur tail-position (that is loop-recur iter 2's
// `verify_loop_body`). The tail-app verification role is
// unchanged — no pre-existing fixture contains a
// `loop`/`recur` node.
Term::Loop { binders, body } => {
for b in binders {
verify_tail_positions(&b.init, false)?;
}
verify_tail_positions(body, is_tail)
}
// recur transfers control and does not fall through, so there
// is no tail position to propagate. Its args are evaluated in
// non-tail position (call-argument-like). Introduces no
// tail-app violation.
Term::Recur { args } => {
for a in args {
verify_tail_positions(a, false)?;
}
Ok(())
}
// prep.2 (kernel-extension-mechanics): `(new T args...)` is
// resolved by synth to a call into the home module's `new` def.
// Its value-args are evaluated in non-tail position (call-arg
// semantics); type-args carry no runtime term. The Term::New
// node itself is not a tail-app — codegen lowers it via a
// synth/desugar step in a later milestone.
Term::New { args, .. } => {
for arg in args {
if let NewArg::Value(v) = arg {
verify_tail_positions(v, false)?;
}
}
Ok(())
}
Term::Intrinsic => Ok(()),
}
}
/// loop-recur iter 2: enforces that every `Term::Recur` occurs in
/// tail position of its lexically-innermost enclosing `Term::Loop`
/// body. A NEW private pass — a *sibling* of
/// `verify_tail_positions` (which is spec-frozen for its tail-app
/// role and unchanged). Invoked from `check_fn` *after* `synth`, so
/// `RecurOutsideLoop`/arity/type (raised in `synth`) take code-
/// precedence; by the time a `Recur` is reached here it is known to
/// be inside a loop with matching arity/types — this pass adds only
/// the tail-position rule. `in_loop_tail` is the loop analogue of
/// `verify_tail_positions`' `is_tail`, scoped to the innermost loop.
fn verify_loop_body(t: &Term, in_loop_tail: bool) -> Result<()> {
match t {
Term::Lit { .. } | Term::Var { .. } => Ok(()),
Term::Recur { args } => {
if !in_loop_tail {
return Err(CheckError::RecurNotInTailPosition);
}
// recur args are evaluated in non-tail position; a recur
// nested inside a recur arg is itself non-tail.
for a in args {
verify_loop_body(a, false)?;
}
Ok(())
}
Term::Loop { binders, body } => {
// Binder inits run once on loop entry — not in the
// loop's tail scope. The loop body opens a FRESH
// innermost-loop tail scope (independent of where the
// loop itself sits — the loop's tail scope is intrinsic).
for b in binders {
verify_loop_body(&b.init, false)?;
}
verify_loop_body(body, true)
}
Term::App { callee, args, .. } => {
verify_loop_body(callee, false)?;
for a in args {
verify_loop_body(a, false)?;
}
Ok(())
}
Term::Do { args, .. } => {
for a in args {
verify_loop_body(a, false)?;
}
Ok(())
}
Term::Let { value, body, .. } => {
verify_loop_body(value, false)?;
verify_loop_body(body, in_loop_tail)
}
Term::If { cond, then, else_ } => {
verify_loop_body(cond, false)?;
verify_loop_body(then, in_loop_tail)?;
verify_loop_body(else_, in_loop_tail)
}
Term::Seq { lhs, rhs } => {
verify_loop_body(lhs, false)?;
verify_loop_body(rhs, in_loop_tail)
}
Term::Match { scrutinee, arms } => {
verify_loop_body(scrutinee, false)?;
for arm in arms {
verify_loop_body(&arm.body, in_loop_tail)?;
}
Ok(())
}
Term::Ctor { args, .. } => {
for a in args {
verify_loop_body(a, false)?;
}
Ok(())
}
Term::Lam { body, .. } => {
// A `recur` cannot cross a lambda boundary (different
// control frame). Reset: a recur inside a lam is outside
// every enclosing loop's tail scope — and synth's
// loop_stack likewise does not cross the lam, so such a
// recur is already a synth `RecurOutsideLoop`.
verify_loop_body(body, false)
}
Term::LetRec { body, in_term, .. } => {
verify_loop_body(body, false)?;
verify_loop_body(in_term, in_loop_tail)
}
Term::Clone { value } => verify_loop_body(value, in_loop_tail),
Term::ReuseAs { source, body } => {
verify_loop_body(source, false)?;
verify_loop_body(body, in_loop_tail)
}
// prep.2 (kernel-extension-mechanics): Term::New's value-args
// are non-tail (call-arg semantics). The Term::New node itself
// is opaque to the loop/recur control transfer — value args
// are evaluated in non-tail position; type-args carry no term.
Term::New { args, .. } => {
for arg in args {
if let NewArg::Value(v) = arg {
verify_loop_body(v, false)?;
}
}
Ok(())
}
Term::Intrinsic => Ok(()),
}
}
fn check_const(c: &ConstDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<()> {
// Const types are never polymorphic — a Forall here is rejected
// outright. Any other type passes through to `synth` as before.
if matches!(&c.ty, Type::Forall { .. }) {
return Err(CheckError::PolymorphicNotSupported(c.name.clone()));
}
let mut locals = IndexMap::new();
let mut effects = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
// const bodies don't carry a `Forall.constraints`
// (rejected upstream), so any residual would have to be concrete —
// Task 10's no-instance arm will pick those up. We thread an
// accumulator only to keep `synth`'s signature uniform.
let mut residuals: Vec<ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
let mut warnings: Vec<Diagnostic> = Vec::new();
// loop-recur iter 2: a const value has no enclosing loop; any
// `recur` in a const body correctly fires `RecurOutsideLoop`.
let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
let v = synth(&c.value, env, &mut locals, &mut loop_stack, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
out_warnings.extend(warnings);
unify(&c.ty, &v, &mut subst)?;
if !effects.is_empty() {
return Err(CheckError::ConstHasEffects(
c.name.clone(),
effects.into_iter().collect(),
));
}
Ok(())
}
#[allow(clippy::too_many_arguments)]
pub(crate) fn synth(
t: &Term,
env: &Env,
locals: &mut IndexMap<String, Type>,
// loop-recur iter 2: per-walk loop-binder stack. Each frame is one
// `Term::Loop`'s binders in declaration order. `recur` rebinds
// binders by position, not name, so the type list is positional;
// iter loop-recur.tidy added the binder name alongside the type
// so `Term::Lam`'s escape guard can reject a free var that is an
// in-scope loop binder. Pushed on `Term::Loop` body entry, popped
// on exit; consulted innermost-first by `Term::Recur` for arity +
// per-position type, and across all frames by `Term::Lam` for the
// escape check. Position: locals-adjacent — per-fn-body
// lexical-control scope state.
loop_stack: &mut Vec<Vec<(String, Type)>>,
effects: &mut BTreeSet<String>,
in_def: &str,
subst: &mut Subst,
counter: &mut u32,
residuals: &mut Vec<ResidualConstraint>,
free_fn_calls: &mut Vec<FreeFnCall>,
// out-parameter for synth-time structured warnings. Symmetric
// to `residuals` / `free_fn_calls`. Currently only the
// `class-method-shadowed-by-fn` warning is emitted here; future
// synth-time warnings (if any) would flow through the same channel.
warnings: &mut Vec<crate::diagnostic::Diagnostic>,
) -> Result<Type> {
match t {
Term::Lit { lit } => Ok(match lit {
Literal::Int { .. } => Type::int(),
Literal::Bool { .. } => Type::bool_(),
Literal::Str { .. } => Type::str_(),
Literal::Unit => Type::unit(),
Literal::Float { .. } => Type::float(),
}),
Term::Var { name } => {
// Lookup precedence: locals → local globals → class-method
// table → qualified cross-module ref. A `Forall` resolved at
// any of these levels is instantiated with fresh metavars at
// the use site (textbook ML rule); rigid vars and concrete
// types pass through unchanged.
//
// the class-method channel sits between
// local globals and qualified cross-module ref. When a name
// resolves through `env.class_methods`, we substitute the
// class param with a fresh metavar and record a residual
// class constraint — `check_fn` later compares the residual
// set against the declared `Forall.constraints`.
// alongside the bare type, capture
// (owner_module, unqualified_name_in_owner_module)
// for any non-local resolution that lands on a
// `Type::Forall` AND is a real workspace-declared
// `Def::Fn` (NOT a builtin operator like `==`). The
// discriminator is whether the name appears in
// `env.module_globals[<owner>]` — builtins are installed
// into `env.globals` only. The unqualified-name capture
// matters for dot-qualified call sites: the FreeFnCall
// records the suffix (e.g. `length`), not the full
// `List.length` (prep.1's type-scoped form) or
// `std_list.length` (module-qualified form), so
// `synthesise_mono_fn_for_free_fn` can look up the
// source def by its bare name in the owner module's
// def list.
//
// After the resolution ladder, if `raw` is a `Type::Forall`
// AND a `free_fn_owner` is known, push a `FreeFnCall`
// observation; the mono pass `subst.apply`s the metas
// post-synth to recover concrete type-args at each
// polymorphic free-fn call site.
// a helper closure that emits the
// `class-method-shadowed-by-fn` warning when a fn-precedence
// branch resolves a name that ALSO has class-method
// candidates in the workspace. The fn resolution proceeds;
// the warning surfaces the shadow so the LLM-author can
// disambiguate via explicit class-qualified call if the
// shadow was unintentional. Locals/same-module-fn/implicit-
// import-fn all share this rule.
let emit_shadow_warning_if_class_method =
|name: &str, owner_module: &str, warnings: &mut Vec<crate::diagnostic::Diagnostic>| {
let (method_name, _) = parse_method_qualifier(name);
// mq.tidy: tighten emission per spec §"Class-fn
// collisions" — fire only when at least one
// candidate class has a registry instance (any
// type). Without this, the warning fires on any
// class declaring the method, including class
// methods with zero instances anywhere in the
// workspace.
let registry_unit_view: BTreeMap<(String, String), ()> = env
.workspace_registry
.entries
.keys()
.map(|k| (k.clone(), ()))
.collect();
if !any_candidate_class_has_instance(
&env.method_to_candidate_classes,
&registry_unit_view,
method_name,
) {
return;
}
if let Some(cands) = env.method_to_candidate_classes.get(method_name) {
let mut candidate_list: Vec<String> = cands.iter().cloned().collect();
candidate_list.sort();
let d = crate::diagnostic::Diagnostic::warning(
"class-method-shadowed-by-fn",
format!(
"free fn `{name}` in module `{owner_module}` shadows class method `{method_name}` \
declared in classes {candidate_list:?}. \
To call the class method instead, write `<ClassQualifier>.{method_name} ...`.",
),
)
.with_def(in_def.to_string())
.with_ctx(serde_json::json!({
"name": name,
"method": method_name,
"fn_owner_module": owner_module,
"candidate_classes": candidate_list,
}));
warnings.push(d);
}
};
let (raw, free_fn_owner): (Type, Option<(String, String, Option<String>)>) = if let Some(t) = locals.get(name) {
// Locals (lambda / let / fn-params) — fn wins per
// lookup precedence. A class method shadowed by a
// local binding fires the shadow warning so the
// author can disambiguate if unintentional.
emit_shadow_warning_if_class_method(name, env.current_module.as_str(), warnings);
(t.clone(), None)
} else if let Some(t) = env.globals.get(name) {
// Same-module global. Owner is the current module IFF
// the name is in this module's declared globals
// (i.e. it's a `Def::Fn`, not a builtin). The bare
// `name` works as the in-module key.
let owner = env
.module_globals
.get(&env.current_module)
.filter(|m| m.contains_key(name))
.map(|_| (env.current_module.clone(), name.clone(), None));
emit_shadow_warning_if_class_method(name, env.current_module.as_str(), warnings);
(t.clone(), owner)
} else if let Some((owner_module, raw_ty)) = env
.imports
.values()
.find_map(|mod_name| {
env.module_globals
.get(mod_name)
.and_then(|mg| mg.get(name).map(|ty| (mod_name.clone(), ty.clone())))
})
{
// implicit-import free-fn precedence runs BEFORE
// the class-method branch (fn wins per spec
// §"Class-fn collisions"). When the name has class-
// method candidates too, emit the shadow warning.
//
// bare-name fall-through to free fns of
// implicitly-imported modules. Today only the prelude is
// implicitly imported (see `build_check_env` and
// `check_in_workspace`'s prelude-injection), so the
// first match is unambiguous. If a second implicit
// import lands, the single-match-wins rule becomes a
// real ambiguity and this branch needs a
// duplicate-detection diagnostic.
emit_shadow_warning_if_class_method(name, owner_module.as_str(), warnings);
// Qualify any bare type-cons referring to a type defined in
// the owning module — same treatment the dot-qualified arm
// below applies — so signatures cross the module boundary
// with fully-qualified Type::Cons.
let owner_types = env
.module_types
.get(&owner_module)
.cloned()
.unwrap_or_default();
let qualified = qualify_local_types(&raw_ty, &owner_module, &owner_types);
// Bare name resolves through implicit import; the
// unqualified name in the owner module is the same `name`.
(qualified, Some((owner_module, name.clone(), None)))
} else if is_class_method_dispatch(name, env) {
// type-driven dispatch entry. The Var arm runs
// before App-arm unification, so the arg type is not
// available here. The dispatch helper resolves on
// (a) explicit class qualifier, (b) singleton candidate
// set (today's invariant), or (c) constraint-driven
// filter (rigid-var case); otherwise it emits `Multi`
// for discharge-time refinement.
//
// With `MethodNameCollision` still active (pre-canonical-class-form),
// real workspaces never reach the `Multi` branch — the
// candidate set is always singleton. The branch is
// installed here for the type-driven dispatch refactor to exercise without further
// dispatch-side edits.
let (method_name, qualifier_opt) = parse_method_qualifier(name);
let candidates = env
.method_to_candidate_classes
.get(method_name)
.expect("contains_key invariant: gate above guarantees presence");
// Build a unit-view of the workspace registry keyed by
// (qualified_class, type_hash). Values are unit; only
// key presence matters for the type-driven filter.
let registry_unit: BTreeMap<(String, String), ()> = env
.workspace_registry
.entries
.keys()
.map(|k| (k.clone(), ()))
.collect();
let outcome = resolve_method_dispatch(
method_name,
qualifier_opt.as_deref(),
candidates,
/*concrete_arg_type*/ None,
/*declared_constraints*/ &env.active_declared_constraints,
/*registry*/ &registry_unit,
);
let (residual_class, residual_candidates) = match outcome {
MethodDispatchOutcome::Resolved(class) => (class, None),
MethodDispatchOutcome::Multi { candidates: cs, method: _ } => {
// Tentative class: first BTreeSet element.
// Refinement at discharge / mono time overwrites it.
let tentative = cs.iter().next().cloned().unwrap_or_default();
(tentative, Some(cs))
}
MethodDispatchOutcome::UnknownClass(qname) => {
return Err(CheckError::UnknownClass { name: qname });
}
MethodDispatchOutcome::Ambiguous { method, at_type, candidates: cs } => {
return Err(CheckError::AmbiguousMethodResolution {
method,
at_type,
candidate_classes: cs,
});
}
};
// class_methods is tuple-keyed by
// `(qualified-class, method)`. The dispatcher above
// resolved a tentative class (single-survivor or first
// BTreeSet element for the multi-candidate path) — use
// it to disambiguate the lookup. The `expect` is sound
// by construction: `method_to_candidate_classes` and
// `class_methods` are built from the same source loop
// (every entry in one has a matching entry in the
// other; see `build_check_env`).
let cm = env
.class_methods
.get(&(residual_class.clone(), method_name.to_string()))
.expect(
"method_to_candidate_classes invariant: \
(resolved class, method) present implies class_methods entry",
);
let owner_types = env
.module_types
.get(&cm.defining_module)
.cloned()
.unwrap_or_default();
let qualified_method_ty =
qualify_local_types(&cm.method_ty, &cm.defining_module, &owner_types);
let fresh = Subst::fresh(counter);
let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
mapping.insert(cm.class_param.clone(), fresh.clone());
let inst_ty = substitute_rigids(&qualified_method_ty, &mapping);
residuals.push(ResidualConstraint {
class: residual_class,
type_: fresh,
method: method_name.to_string(),
candidates: residual_candidates,
});
return Ok(inst_ty);
} else if name.matches('.').count() == 1 {
let (prefix, suffix) = name.split_once('.').expect("checked");
// prep.1: TypeDef-first ladder. If `prefix` names a
// `TypeDef` anywhere in the workspace, that type's home
// module is the resolution target — type-scoped form
// `<TypeName>.<member>`. Otherwise fall back to the
// legacy module-as-receiver path via `env.imports`.
let type_home: Option<String> = env
.module_types
.iter()
.find_map(|(mod_name, types)| {
if types.contains_key(prefix) {
Some(mod_name.clone())
} else {
None
}
});
let target_module: String = if let Some(home) = type_home.clone() {
home
} else if let Some(m) = env.imports.get(prefix) {
m.clone()
} else {
return Err(CheckError::TypeScopedReceiverNotAType {
name: prefix.to_string(),
});
};
let g = env.module_globals.get(&target_module).ok_or_else(|| {
CheckError::UnknownModule {
module: target_module.clone(),
}
})?;
let raw_ty = g.get(suffix).cloned().ok_or_else(|| {
// If receiver resolved as a TypeDef but the suffix
// is missing in the home module, emit the
// type-scoped diagnostic; otherwise the legacy
// `UnknownImport`.
if type_home.is_some() {
CheckError::TypeScopedMemberNotFound {
type_name: prefix.to_string(),
member: suffix.to_string(),
home_module: target_module.clone(),
}
} else {
CheckError::UnknownImport {
module: target_module.clone(),
name: suffix.to_string(),
}
}
})?;
// qualify any bare type-cons referring to a
// type defined in the owning module so that signatures
// pulled across the boundary unify against
// qualified-form ctors and types in the consumer
// module.
//
// Same-module case: the pre-pass leaves own-module
// names bare (see `qualify_workspace_types`'s
// own-module rule), and the local `Term::Ctor` arm
// (~line 3644) also returns bare names. Qualifying
// here would produce `<this>.T` for sites the rest
// of the resolver represents as bare `T`, tripping
// a phantom type-mismatch on a same-module
// `(app Type.member …)` call. Fieldtest F1 surfaced
// this asymmetry; the fix is to no-op the qualifier
// when `target_module == env.current_module`.
let qualified = if target_module == env.current_module {
raw_ty
} else {
let owner_types = env
.module_types
.get(&target_module)
.cloned()
.unwrap_or_default();
qualify_local_types(&raw_ty, &target_module, &owner_types)
};
// Dot-qualified `prefix.suffix`: the unqualified name in
// the owner module is `suffix`. raw-buf.3: when the
// resolution went through the TypeDef-first ladder
// (`type_home.is_some()`), the call is type-scoped — carry
// the TypeDef prefix as the mono-symbol scope. The legacy
// module-as-receiver sub-case (`type_home == None`) is not
// type-scoped → `scope = None`.
let scope = if type_home.is_some() {
Some(prefix.to_string())
} else {
None
};
(qualified, Some((target_module, suffix.to_string(), scope)))
} else {
return Err(CheckError::UnknownIdent(name.clone()));
};
// if raw is `Type::Forall` AND we know the
// owner module (i.e. the resolution went through a non-
// local branch), record a FreeFnCall observation BEFORE
// instantiating. The metas are the fresh metavars we
// about to use; the mono pass `subst.apply`s them later.
// Note: `unqualified_name` is the name as seen inside the
// owner module (so the mono pass can find the `Def::Fn`
// by bare name); the source-level `name` may be a
// dot-qualified form (`prefix.suffix`) the synth started
// with.
if let (Type::Forall { vars, constraints, body }, Some((owner, unqualified_name, scope))) =
(&raw, &free_fn_owner)
{
let (metas, inst) = instantiate(vars, body, counter);
// push a residual for each declared constraint
// of the poly free fn with the rigid var substituted by
// its fresh metavar. The discharge loop at the enclosing
// `check_fn`'s post-synth phase resolves the residual
// against the workspace registry (fully-concrete after
// App-arm unification) and fires `NoInstance` if no
// instance ships for the unified type. Without this push,
// `print f` at a function type `f : Int -> Int` would
// typecheck silently — the `Show f`-shaped obligation
// would only surface at codegen as an `unknown variable`
// error from the synthesised mono body.
//
// The substitution mirrors `instantiate`'s body-side
// mapping: position-by-position pairing of `vars` with
// the freshly-generated `metas`. The discharge path
// post-`subst.apply` produces the same concrete type
// that the App-arm unified into the metavars.
let cmapping: BTreeMap<String, Type> = vars
.iter()
.cloned()
.zip(metas.iter().cloned())
.collect();
for c in constraints {
let c_class = qualify_class_ref_in_check(&c.class, owner);
let c_ty = substitute_rigids(&c.type_, &cmapping);
// Look up the class's method name via the workspace
// class index; we need it for the `ResidualConstraint`'s
// `method` field (used by `NoInstance`'s rendering).
let method_name = env
.class_methods
.iter()
.find_map(|((cls, m), _)| {
if *cls == c_class { Some(m.clone()) } else { None }
})
.expect(
"class_methods registry coherence — a declared constraint's \
class is missing from env.class_methods. The pre-pass \
`MissingClass` diagnostic should have rejected this earlier; \
reaching here means workspace-registry / class-index drift. \
Surface to debug skill rather than silently render NoInstance \
with an empty method name.",
);
residuals.push(ResidualConstraint {
class: c_class,
type_: c_ty,
method: method_name,
candidates: None,
});
}
free_fn_calls.push(FreeFnCall {
name: unqualified_name.clone(),
owner_module: owner.clone(),
forall_vars: vars.clone(),
metas: metas.clone(),
scope: scope.clone(),
});
return Ok(inst);
}
Ok(maybe_instantiate(raw, counter))
}
Term::App { callee, args, .. } => {
let cty = synth(callee, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let cty = subst.apply(&cty);
let (params, ret, fx) = match &cty {
Type::Fn { params, ret, effects: fx, .. } => {
(params.clone(), (**ret).clone(), fx.clone())
}
Type::Forall { vars, constraints: _, body } => {
// Defensive — Var should already have instantiated.
let (_, body) = instantiate(vars, body, counter);
match &body {
Type::Fn { params, ret, effects: fx, .. } => {
(params.clone(), (**ret).clone(), fx.clone())
}
other => {
return Err(CheckError::NotAFunction(
callee_name(callee),
ailang_core::pretty::type_to_string(other),
));
}
}
}
other => {
return Err(CheckError::NotAFunction(
callee_name(callee),
ailang_core::pretty::type_to_string(other),
));
}
};
if args.len() != params.len() {
return Err(CheckError::ArityMismatch {
name: callee_name(callee),
expected: params.len(),
got: args.len(),
});
}
for (a, exp) in args.iter().zip(params.iter()) {
let actual = synth(a, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
unify(exp, &actual, subst)?;
}
for e in fx {
effects.insert(e);
}
Ok(subst.apply(&ret))
}
Term::Let { name, value, body } => {
let v = synth(value, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let prev = locals.insert(name.clone(), v);
let r = synth(body, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
match prev {
Some(p) => {
locals.insert(name.clone(), p);
}
None => {
locals.shift_remove(name);
}
}
Ok(r)
}
Term::If { cond, then, else_ } => {
let c = synth(cond, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
unify(&Type::bool_(), &c, subst)?;
let t1 = synth(then, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let t2 = synth(else_, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
unify(&t1, &t2, subst)?;
Ok(subst.apply(&t1))
}
Term::Do { op, args, .. } => {
let sig = env
.effect_ops
.get(op)
.ok_or_else(|| CheckError::UnknownEffectOp(op.clone()))?
.clone();
if args.len() != sig.params.len() {
return Err(CheckError::ArityMismatch {
name: op.clone(),
expected: sig.params.len(),
got: args.len(),
});
}
for (a, exp) in args.iter().zip(sig.params.iter()) {
let actual = synth(a, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
unify(exp, &actual, subst)?;
}
effects.insert(sig.effect.clone());
Ok(sig.ret)
}
Term::Ctor { type_name, ctor, args } => {
// Canonical-type-lookup: Term::Ctor lookup is direct post-canonical-type-form
// Canonical type_name: bare = local TypeDef OR (prep.1) any
// bare type-name in scope via an imported module's TypeDef;
// qualified = explicit cross-module. The imports-fallback
// (iter 23.1.3) is gone — bare cross-module refs that are
// NOT in scope are rejected upstream by the workspace
// validator (via the canonical-form validator).
//
// prep.1: a bare `type_name` that does not match a local
// TypeDef falls back to a workspace-wide TypeDef-first
// lookup (symmetric to the `Term::Var` dot-qualified arm
// at lib.rs:3189). This makes `(term-ctor Maybe Just x)`
// resolve when `Maybe` is declared in an imported (explicit
// or implicit) module — matching the canonical-form rule
// already accepted by the workspace validator.
//
// when the type is cross-module, `cdef.fields` is
// written in the owning module's local namespace. A recursive
// self-reference like `Cons a (List a)` carries `Con
// { name: "List" }` even though, from the consumer's view,
// the type is `std_list.List`. Apply `qualify_local_types`
// with the owning module so that recursive ctor field types
// (and any other locally-named cross-module type-cons) are
// qualified before substitution / unification.
let owning_module: Option<String>;
let result_type_name: String;
let td = if type_name.matches('.').count() == 1 {
let (prefix, suffix) = type_name.split_once('.').expect("checked");
let target_module = match env.imports.get(prefix) {
Some(m) => m.clone(),
None => {
return Err(CheckError::UnknownModule {
module: prefix.to_string(),
});
}
};
let td = env.module_types
.get(&target_module)
.and_then(|tys| tys.get(suffix))
.cloned()
.ok_or_else(|| CheckError::UnknownType(type_name.clone()))?;
owning_module = Some(target_module);
result_type_name = type_name.clone();
td
} else if let Some(td) = env.types.get(type_name) {
owning_module = None;
result_type_name = type_name.clone();
td.clone()
} else if let Some((home, td)) = env
.module_types
.iter()
.find_map(|(m, types)| types.get(type_name).map(|td| (m.clone(), td.clone())))
{
// prep.1: TypeDef-first cross-module bare resolution.
// The result-type Con.name is qualified to the home
// module so it unifies against signatures already
// carrying the qualified form (e.g. `from_maybe`'s
// second arg of type `std_maybe.Maybe<a>`).
result_type_name = format!("{home}.{type_name}");
owning_module = Some(home);
td
} else {
return Err(CheckError::UnknownType(type_name.clone()));
};
let cdef = td
.ctors
.iter()
.find(|c| &c.name == ctor)
.ok_or_else(|| CheckError::UnknownCtor {
ty: type_name.clone(),
ctor: ctor.clone(),
})?
.clone();
if args.len() != cdef.fields.len() {
return Err(CheckError::CtorArity {
ty: type_name.clone(),
ctor: ctor.clone(),
expected: cdef.fields.len(),
got: args.len(),
});
}
// qualify local type-cons in the field types when
// the ctor's owning type is cross-module. No-op when the
// type is local (owning_module is None).
let qualified_fields: Vec<Type> = match &owning_module {
Some(m) => {
let owner_types = env
.module_types
.get(m)
.cloned()
.unwrap_or_default();
cdef.fields
.iter()
.map(|f| qualify_local_types(f, m, &owner_types))
.collect()
}
None => cdef.fields.clone(),
};
// parameterised ADT — instantiate the type's vars
// with fresh metavars, substitute them through every ctor
// field type, and let the field types' metavars be solved by
// unifying against the actual arg types. The result type
// carries the same metavars as type-args, so the surrounding
// context can pin them down.
let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
let mut type_args: Vec<Type> = Vec::with_capacity(td.vars.len());
for v in &td.vars {
let m = Subst::fresh(counter);
mapping.insert(v.clone(), m.clone());
type_args.push(m);
}
for (a, exp) in args.iter().zip(qualified_fields.iter()) {
let exp_inst = substitute_rigids(exp, &mapping);
let actual = synth(a, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
unify(&exp_inst, &actual, subst)?;
}
Ok(Type::Con {
name: result_type_name,
args: type_args,
})
}
Term::Match { scrutinee, arms } => {
let s_ty = synth(scrutinee, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
if arms.is_empty() {
return Err(CheckError::NonExhaustive {
ty: ailang_core::pretty::type_to_string(&s_ty),
missing: vec!["(no arms)".into()],
});
}
let mut covered_ctors: BTreeSet<String> = BTreeSet::new();
let mut has_open_arm = false;
let mut result_ty: Option<Type> = None;
for arm in arms {
let bindings = type_check_pattern(&arm.pat, &s_ty, env)?;
let mut pushed = Vec::new();
for (n, t) in &bindings {
let prev = locals.insert(n.clone(), t.clone());
pushed.push((n.clone(), prev));
}
let body_ty = synth(&arm.body, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
for (n, prev) in pushed.into_iter().rev() {
match prev {
Some(p) => {
locals.insert(n, p);
}
None => {
locals.shift_remove(&n);
}
}
}
if let Some(rt) = &result_ty {
unify(rt, &body_ty, subst)?;
} else {
result_ty = Some(body_ty);
}
match &arm.pat {
Pattern::Wild | Pattern::Var { .. } => {
has_open_arm = true;
}
Pattern::Ctor { ctor, .. } => {
covered_ctors.insert(ctor.clone());
}
Pattern::Lit { .. } => {
// Lit patterns don't structurally cover anything.
}
}
}
if !has_open_arm {
// a qualified scrutinee type (`module.Type`,
// produced by a cross-module ctor) resolves through
// `env.module_types`; bare names use `env.types` as
// before.
let td_opt: Option<&TypeDef> = match &s_ty {
Type::Con { name, .. } => {
if name.matches('.').count() == 1 {
let (prefix, suffix) = name.split_once('.').expect("checked");
env.module_types
.get(prefix)
.and_then(|tys| tys.get(suffix))
} else {
env.types.get(name)
}
}
_ => None,
};
match (td_opt, &s_ty) {
(Some(td), Type::Con { name, .. }) => {
let missing: Vec<String> = td
.ctors
.iter()
.filter(|c| !covered_ctors.contains(&c.name))
.map(|c| c.name.clone())
.collect();
if !missing.is_empty() {
return Err(CheckError::NonExhaustive {
ty: name.clone(),
missing,
});
}
}
_ => {
return Err(CheckError::PrimitiveNeedsWildcard(
ailang_core::pretty::type_to_string(&s_ty),
));
}
}
}
Ok(subst.apply(&result_ty.expect("checked arms is non-empty")))
}
Term::Seq { lhs, rhs } => {
let lty = synth(lhs, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
unify(&Type::unit(), &lty, subst)?;
synth(rhs, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
}
Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => {
// reject lambda-captures-of-loop-binder.
// Walk the lambda body for free Vars (names not bound by
// the lambda's own params) that match any loop binder on
// the enclosing `loop_stack`. Loop binders are
// alloca-resident and `std::mem::take`-emptied at the
// lambda frame boundary in codegen — capturing one panics
// `unreachable!()` at codegen, so the type checker rejects
// it here instead. Reuses `desugar::free_vars_in_term`
// (same walker `lift.rs` uses) which honours pattern
// bindings inside `Term::Match` arms; gated on a non-empty
// `loop_stack` so lambdas outside any loop typecheck
// unchanged.
if !loop_stack.is_empty() {
let mut lam_bound: BTreeSet<String> = BTreeSet::new();
for p in params {
lam_bound.insert(p.clone());
}
let mut frees: BTreeSet<String> = BTreeSet::new();
ailang_core::desugar::free_vars_in_term(body, &lam_bound, &mut frees);
for free_name in &frees {
for frame in loop_stack.iter() {
if frame.iter().any(|(n, _)| n == free_name) {
return Err(CheckError::LoopBinderCapturedByLambda {
name: free_name.clone(),
});
}
}
}
}
let mut pushed: Vec<(String, Option<Type>)> = Vec::new();
for (n, t) in params.iter().zip(param_tys.iter()) {
let prev = locals.insert(n.clone(), t.clone());
pushed.push((n.clone(), prev));
}
let mut body_effects: BTreeSet<String> = BTreeSet::new();
let body_ty = synth(body, env, locals, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
for (n, prev) in pushed.into_iter().rev() {
match prev {
Some(p) => {
locals.insert(n, p);
}
None => {
locals.shift_remove(&n);
}
}
}
let body_ty = body_ty?;
unify(ret_ty, &body_ty, subst)?;
let declared: BTreeSet<String> = lam_effects.iter().cloned().collect();
for e in &body_effects {
if !declared.contains(e) {
return Err(CheckError::UndeclaredEffect(e.clone()));
}
}
Ok(Type::Fn {
params: param_tys.clone(),
ret: Box::new((**ret_ty).clone()),
effects: lam_effects.clone(),
param_modes: vec![],
ret_mode: ParamMode::Implicit,
})
}
Term::LetRec { name, ty, params, body, in_term } => {
// a `Term::LetRec` reaches `synth` only when
// the desugar pass deferred it (some capture is
// `Term::Let`-bound and its type is only knowable here).
// We synthesize it as if it were a recursive fn-typed
// local binding:
// 1. Peel any `Forall` defensively (16b.6 still rejects
// Forall-typed LetRecs at desugar — this is just for
// shape uniformity with `check_fn`).
// 2. Validate that `params.len() == ty.params.len()`.
// 3. Extend `locals` with `name: ty` for the body
// (recursive self-reference) and each
// `params[i]: ty.params[i]`.
// 4. Synth the body, unify against `ty.ret`, check
// effects-subset against `ty.effects`.
// 5. Restore locals; extend with `name: ty`; synth
// `in_term`. Restore. Return `in_term`'s type.
let inner_ty = match ty {
Type::Forall { body, .. } => (**body).clone(),
other => other.clone(),
};
let (param_tys, ret_ty, declared_effs) = match &inner_ty {
Type::Fn { params: ps, ret, effects, .. } => {
(ps.clone(), (**ret).clone(), effects.clone())
}
other => {
return Err(CheckError::FnTypeRequired(
name.clone(),
ailang_core::pretty::type_to_string(other),
));
}
};
if param_tys.len() != params.len() {
return Err(CheckError::ParamCountMismatch {
name: name.clone(),
ty_count: param_tys.len(),
param_count: params.len(),
});
}
// Validate the LetRec's declared param/ret types against
// the type env (catches malformed types like ADT arity
// mismatches before they leak into the body).
for p in &param_tys {
check_type_well_formed(p, env)?;
}
check_type_well_formed(&ret_ty, env)?;
// Save and extend locals: name + params for the body's scope.
let mut pushed: Vec<(String, Option<Type>)> = Vec::new();
let prev_name = locals.insert(name.clone(), ty.clone());
pushed.push((name.clone(), prev_name));
for (n, t) in params.iter().zip(param_tys.iter()) {
let prev = locals.insert(n.clone(), t.clone());
pushed.push((n.clone(), prev));
}
// Body effects are tracked separately so we can check the
// subset rule against `declared_effs` — exactly like
// `Term::Lam`.
let mut body_effects: BTreeSet<String> = BTreeSet::new();
let body_ty = synth(body, env, locals, loop_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
// Restore body-scope locals (params + name).
for (n, prev) in pushed.into_iter().rev() {
match prev {
Some(p) => {
locals.insert(n, p);
}
None => {
locals.shift_remove(&n);
}
}
}
let body_ty = body_ty?;
unify(&ret_ty, &body_ty, subst)?;
let declared: BTreeSet<String> = declared_effs.into_iter().collect();
for e in &body_effects {
if !declared.contains(e) {
return Err(CheckError::UndeclaredEffect(e.clone()));
}
}
// Now extend locals with `name: ty` for the in-clause's
// scope (params are not visible here; only the recursive
// binding is).
let prev_in = locals.insert(name.clone(), ty.clone());
let in_ty = synth(in_term, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
match prev_in {
Some(p) => {
locals.insert(name.clone(), p);
}
None => {
locals.shift_remove(name);
}
}
in_ty
}
Term::Clone { value } => {
// `(clone X)` typechecks identically to `X`.
// No constraint generated, no environment change. The
// wrapper records author intent for the future RC inc/dec
// emission pass (18c.3); typing is pure passthrough.
synth(value, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
}
Term::ReuseAs { source, body } => {
// `(reuse-as SRC NEW-CTOR)` requires `body` to
// be an allocating term — `Term::Ctor` or `Term::Lam`. Any
// other shape is a structural error: the wrapper has
// nothing to rewrite. The `source` term has no body-shape
// constraint here — linearity (which runs only on
// all-explicit-mode fns) enforces "source must be a bare
// Var referring to an in-scope owned binder". Source-type
// and body-type need not match — that's a future
// shape-compatibility check (18d.2 will add a
// `reuse-as-shape-mismatch` diagnostic when codegen has
// the actual size info).
let _ = synth(source, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
match body.as_ref() {
Term::Ctor { .. } | Term::Lam { .. } => {}
other => {
let tag = match other {
Term::Lit { .. } => "lit",
Term::Var { .. } => "var",
Term::App { .. } => "app",
Term::Let { .. } => "let",
Term::LetRec { .. } => "let-rec",
Term::If { .. } => "if",
Term::Do { .. } => "do",
Term::Match { .. } => "match",
Term::Seq { .. } => "seq",
Term::Clone { .. } => "clone",
Term::ReuseAs { .. } => "reuse-as",
Term::Loop { .. } => "loop",
Term::Recur { .. } => "recur",
Term::New { .. } => "new",
Term::Intrinsic => "intrinsic",
Term::Ctor { .. } | Term::Lam { .. } => unreachable!(),
};
return Err(CheckError::ReuseAsNonAllocatingBody {
got: tag.to_string(),
body_form_a: ailang_surface::print::term_to_form_a(other),
});
}
}
// Body's type is the result type of the whole reuse-as
// expression.
synth(body, env, locals, loop_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
}
// loop-recur iter 2: each binder init is synthed in the
// outer scope plus already-declared binder names of THIS
// loop (declaration order; later inits + body see earlier
// binders via `locals`, exactly as `Term::Let` binds its
// name). The loop's static type is the body's type. The
// ordered binders (name + type) are pushed onto `loop_stack`
// for the body walk so an inner `Term::Recur` can
// position-check the types and `Term::Lam`'s escape guard
// (iter loop-recur.tidy) can reject capture of a binder name;
// popped on exit.
Term::Loop { binders, body } => {
let mut binder_frame: Vec<(String, Type)> = Vec::new();
let mut restore: Vec<(String, Option<Type>)> = Vec::new();
for b in binders {
let init_ty = synth(
&b.init, env, locals, loop_stack, effects,
in_def, subst, counter, residuals, free_fn_calls, warnings,
)?;
unify(&b.ty, &init_ty, subst)?;
binder_frame.push((b.name.clone(), b.ty.clone()));
let prev = locals.insert(b.name.clone(), b.ty.clone());
restore.push((b.name.clone(), prev));
}
loop_stack.push(binder_frame);
let body_result = synth(
body, env, locals, loop_stack, effects,
in_def, subst, counter, residuals, free_fn_calls, warnings,
);
loop_stack.pop();
for (name, prev) in restore.into_iter().rev() {
match prev {
Some(p) => {
locals.insert(name, p);
}
None => {
locals.shift_remove(&name);
}
}
}
body_result
}
// loop-recur iter 2: recur re-enters the innermost enclosing
// loop, rebinding its binders positionally. RecurOutsideLoop
// when `loop_stack` is empty; RecurArityMismatch on count
// disagreement; RecurTypeMismatch via the Assign-style
// subst-apply-then-structural-compare (Boss call 1) so the
// dedicated code fires point-exactly. recur's OWN type is a
// fresh metavar — it transfers control and never falls
// through, so it unifies with whatever sibling branch the
// enclosing if/match requires.
Term::Recur { args } => {
let binder_frame = match loop_stack.last() {
None => return Err(CheckError::RecurOutsideLoop),
Some(frame) => frame.clone(),
};
if args.len() != binder_frame.len() {
return Err(CheckError::RecurArityMismatch {
expected: binder_frame.len(),
got: args.len(),
});
}
for (i, a) in args.iter().enumerate() {
let arg_ty = synth(
a, env, locals, loop_stack, effects,
in_def, subst, counter, residuals, free_fn_calls, warnings,
)?;
let applied_binder = subst.apply(&binder_frame[i].1);
let applied_arg = subst.apply(&arg_ty);
if applied_binder != applied_arg {
return Err(CheckError::RecurTypeMismatch {
position: i,
expected: ailang_core::pretty::type_to_string(&applied_binder),
got: ailang_core::pretty::type_to_string(&applied_arg),
});
}
}
Ok(Subst::fresh(counter))
}
// prep.2 (kernel-extension-mechanics): functional construction
// `(new T args...)` calls the `new` def in T's home module.
// After the prep.1 pre-pass, `type_name` is qualified to
// `<home>.<TypeName>` whenever T is cross-module; it stays
// bare when T is local to the current module. Steps:
// 1. resolve home_module + bare_type from type_name.
// 2. look up `new` in the home module's globals →
// NewTypeNotConstructible if absent.
// 3. peel Forall (if any) → vars + (params, ret, effects).
// Count Type-positional vs. Value-positional args; the
// kind-pattern of the args (which positions are Type vs.
// Value) must match the sig — for each Forall var the
// corresponding arg slot is Type, for each value-param it
// is Value. Anything else → NewArgKindMismatch.
// 4. build the rigid→concrete map from Type-args (in order),
// substitute through param types and the return type.
// 5. synth each value-arg and unify against the substituted
// param type.
// 6. inherit `new`'s effects; the result type is the
// substituted ret.
Term::New { type_name, args } => {
// Step 1: resolve home module.
let (home_module, bare_type) = if let Some((m, t)) = type_name.split_once('.') {
(m.to_string(), t.to_string())
} else {
(env.current_module.clone(), type_name.clone())
};
// Step 2: look up `new` in home module's globals. Empty
// module_globals (e.g. when the home is the current
// module and globals live in env.globals instead) also
// counts as "no new def for this type" — we don't fall
// back to a different channel because spec semantics
// require `new` to be defined in the type's home module.
let new_ty = env
.module_globals
.get(&home_module)
.and_then(|g| g.get("new"))
.cloned()
.ok_or_else(|| CheckError::NewTypeNotConstructible {
type_name: bare_type.clone(),
home_module: home_module.clone(),
})?;
// Qualify any bare local Type::Cons in `new`'s signature
// against the home module's TypeDefs — mirrors the
// module-as-receiver path in Term::Ctor. Skip the
// qualification when `new` lives in the CURRENT module:
// the current module sees its own types bare (the
// workspace-wide qualify pre-pass leaves own-module names
// alone), so qualifying here would produce a mismatch
// against own-module declared types at unify time.
let qualified = if home_module == env.current_module {
new_ty
} else {
let owner_types = env
.module_types
.get(&home_module)
.cloned()
.unwrap_or_default();
qualify_local_types(&new_ty, &home_module, &owner_types)
};
// Step 3: peel Forall to (vars, params, ret, effects).
let (vars, param_tys, ret_ty, effects_sig) = match &qualified {
Type::Forall { vars, body, .. } => match body.as_ref() {
Type::Fn { params, ret, effects, .. } => (
vars.clone(),
params.clone(),
(**ret).clone(),
effects.clone(),
),
other => {
return Err(CheckError::FnTypeRequired(
"new".into(),
ailang_core::pretty::type_to_string(other),
));
}
},
Type::Fn { params, ret, effects, .. } => (
Vec::new(),
params.clone(),
(**ret).clone(),
effects.clone(),
),
other => {
return Err(CheckError::FnTypeRequired(
"new".into(),
ailang_core::pretty::type_to_string(other),
));
}
};
// Validate the arg-kind pattern positionally: the first
// `vars.len()` args must be NewArg::Type, the remaining
// `param_tys.len()` args must be NewArg::Value. The first
// mismatch fires NewArgKindMismatch with `position` and
// the expected/got kind labels.
let total_expected = vars.len() + param_tys.len();
if args.len() != total_expected {
// Mismatch on overall count maps to a kind-mismatch on
// the first position where the args run out (or the
// first extra), with `expected` set to what should
// have been there.
let pos = args.len().min(total_expected);
let expected_kind = if pos < vars.len() {
"type-arg"
} else if pos < total_expected {
"value-arg"
} else {
"no arg"
};
let got_kind = if pos < args.len() {
match &args[pos] {
NewArg::Type(_) => "type-arg",
NewArg::Value(_) => "value-arg",
}
} else {
"no arg"
};
return Err(CheckError::NewArgKindMismatch {
type_name: bare_type.clone(),
position: pos,
expected: expected_kind,
got: got_kind,
});
}
for (i, arg) in args.iter().enumerate() {
let expected_is_type = i < vars.len();
let got_is_type = matches!(arg, NewArg::Type(_));
if expected_is_type != got_is_type {
return Err(CheckError::NewArgKindMismatch {
type_name: bare_type.clone(),
position: i,
expected: if expected_is_type { "type-arg" } else { "value-arg" },
got: if got_is_type { "type-arg" } else { "value-arg" },
});
}
}
// Step 4: build the Forall-var → concrete-Type mapping
// from the Type-positional args (in order). The written type
// is the binding declaration of each result-only forall var
// (#51): the author's `(con Int)` IS the element type, never
// inferred from later use.
let mut mapping: BTreeMap<String, Type> = BTreeMap::new();
let mut written_type_args: Vec<Type> = Vec::with_capacity(vars.len());
for (var, arg) in vars.iter().zip(args.iter()) {
if let NewArg::Type(t) = arg {
mapping.insert(var.clone(), t.clone());
written_type_args.push(t.clone());
}
// The kind-check loop above guarantees this branch
// matches; defensive: a Value arg in a Type slot
// would have raised NewArgKindMismatch already.
}
// Steps 4b/4c (#51): only for a polymorphic `new` (the call
// carries written type-args binding result-only forall vars).
if !vars.is_empty() {
// Step 4b: the written element type is subject to the
// constructed type's `param-in` restricted set. synth is
// the correct site for this enforcement (unlike
// `pre_desugar_validation`, which has no registry
// access): construct the result `Type::Con` with the
// written args and run it through
// `check_type_well_formed`, which fires
// `ParamNotInRestrictedSet` naming the forbidden element
// (e.g. `Unit`). This is the leg-2 reject; it must run
// before codegen ever mints a `RawBuf_new__<elem>` symbol.
let constructed = Type::Con {
name: type_name.clone(),
args: written_type_args.clone(),
};
check_type_well_formed(&constructed, env)?;
// Step 4c: push a `FreeFnCall` observation so the mono
// pass mints the `RawBuf_new__<elem>` specialisation for
// the written element type — bound DIRECTLY (`?a := Int`),
// not via an inference channel. The metas carry the
// written concrete types, so `subst.apply` recovers them
// verbatim and the unobservable-var Unit-default (which
// still applies to genuinely-unpinned vars elsewhere) is
// never reached here. Pushed BEFORE the value-args are
// synthesised so the observation order matches the mono
// walker's `Term::New` arm (which consumes this site's
// slot before descending into the value-args). `new`
// carries no class constraints, so no residuals are
// pushed alongside.
free_fn_calls.push(FreeFnCall {
name: "new".to_string(),
owner_module: home_module.clone(),
forall_vars: vars.clone(),
metas: written_type_args.clone(),
scope: Some(bare_type.clone()),
});
}
// Step 5: synth each value-arg, unify against the
// (substituted) corresponding param type.
let value_args = &args[vars.len()..];
for (val_arg, expected_param) in value_args.iter().zip(param_tys.iter()) {
let v = match val_arg {
NewArg::Value(v) => v,
NewArg::Type(_) => unreachable!("kind-check above"),
};
let expected_inst = substitute_rigids(expected_param, &mapping);
let actual = synth(
v, env, locals, loop_stack, effects, in_def, subst, counter,
residuals, free_fn_calls, warnings,
)?;
unify(&expected_inst, &actual, subst)?;
}
// Step 6: inherit `new`'s declared effects, return the
// substituted result type.
for e in &effects_sig {
effects.insert(e.clone());
}
Ok(substitute_rigids(&ret_ty, &mapping))
}
// An intrinsic body is signature-only: the per-fn body check
// (`check_fn`) validates the signature from `f.ty` and never
// calls `synth` on a `Term::Intrinsic`. Reaching here means the
// skip-guard was bypassed — a checker-internal invariant break.
Term::Intrinsic => unreachable!(
"synth reached Term::Intrinsic; an intrinsic body is signature-only and must be \
skipped by check_fn before synth runs"
),
}
}
/// If `t` is a `Forall`, instantiate it with fresh metavars; otherwise
/// pass through unchanged. Used at every var-resolution site.
fn maybe_instantiate(t: Type, counter: &mut u32) -> Type {
if let Type::Forall { vars, constraints: _, body } = &t {
let (_, inst) = instantiate(vars, body, counter);
inst
} else {
t
}
}
/// rewrites bare `Type::Con` references that resolve against
/// `local_types` into qualified `module.Type` form. Used when pulling a
/// fn type across module boundaries: a `Maybe a` declared inside
/// `std_maybe` becomes `std_maybe.Maybe a` when seen from a consumer
/// module — otherwise it would fail to unify with terms whose types
/// the consumer module already qualifies.
///
/// Already-qualified names, primitives (`Int`, `Bool`, `Unit`, `Str`),
/// rigid type vars, and type names that are not in `local_types` pass
/// through unchanged.
fn qualify_local_types(t: &Type, owner_module: &str, local_types: &IndexMap<String, TypeDef>) -> Type {
match t {
Type::Con { name, args } => {
// The first two branches share the body `name.clone()` but
// express semantically distinct reasons (already qualified;
// primitive needs no qualification). Combining them with
// `||` would obscure why each disqualifies the name.
#[allow(clippy::if_same_then_else)]
let qualified_name = if name.contains('.') {
name.clone()
} else if ailang_core::primitives::is_primitive_name(name) {
name.clone()
} else if local_types.contains_key(name) {
format!("{owner_module}.{name}")
} else {
name.clone()
};
Type::Con {
name: qualified_name,
args: args
.iter()
.map(|a| qualify_local_types(a, owner_module, local_types))
.collect(),
}
}
Type::Fn { params, ret, effects, .. } => Type::Fn {
params: params
.iter()
.map(|p| qualify_local_types(p, owner_module, local_types))
.collect(),
ret: Box::new(qualify_local_types(ret, owner_module, local_types)),
effects: effects.clone(),
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
Type::Forall { vars, constraints, body } => Type::Forall {
vars: vars.clone(),
constraints: constraints
.iter()
.map(|c| Constraint {
class: c.class.clone(),
type_: qualify_local_types(&c.type_, owner_module, local_types),
})
.collect(),
body: Box::new(qualify_local_types(body, owner_module, local_types)),
},
Type::Var { .. } => t.clone(),
}
}
/// prep.1 (kernel-extension-mechanics): rewrites bare cross-module
/// `Type::Con` references in a consumer module's declared types into
/// qualified `<home>.<Type>` form. Symmetric to [`qualify_local_types`]
/// but operates from the consumer's perspective: a bare type-name
/// that is not local AND not primitive AND resolves to a `TypeDef`
/// in some other module is rewritten to the qualified form so that
/// the consumer's signature unifies with pulled-across-boundary
/// signatures (which `qualify_local_types` already rewrites bare ->
/// qualified at the owner's side).
pub(crate) fn qualify_workspace_types(
t: &Type,
own_local_types: &IndexMap<String, TypeDef>,
module_types: &BTreeMap<String, IndexMap<String, TypeDef>>,
) -> Type {
match t {
Type::Con { name, args } => {
let qualified_name = if name.contains('.') {
name.clone()
} else if ailang_core::primitives::is_primitive_name(name) {
name.clone()
} else if own_local_types.contains_key(name) {
name.clone()
} else if let Some(home) = module_types
.iter()
.find_map(|(m, types)| if types.contains_key(name) { Some(m.clone()) } else { None })
{
format!("{home}.{name}")
} else {
name.clone()
};
Type::Con {
name: qualified_name,
args: args
.iter()
.map(|a| qualify_workspace_types(a, own_local_types, module_types))
.collect(),
}
}
Type::Fn { params, ret, effects, param_modes, ret_mode } => Type::Fn {
params: params
.iter()
.map(|p| qualify_workspace_types(p, own_local_types, module_types))
.collect(),
ret: Box::new(qualify_workspace_types(ret, own_local_types, module_types)),
effects: effects.clone(),
param_modes: param_modes.clone(),
ret_mode: ret_mode.clone(),
},
Type::Forall { vars, constraints, body } => Type::Forall {
vars: vars.clone(),
constraints: constraints
.iter()
.map(|c| Constraint {
class: c.class.clone(),
type_: qualify_workspace_types(&c.type_, own_local_types, module_types),
})
.collect(),
body: Box::new(qualify_workspace_types(body, own_local_types, module_types)),
},
Type::Var { .. } => t.clone(),
}
}
/// prep.1: walk a [`Module`] and rewrite every `Type` annotation
/// (function signatures, const types, `Term::Lam.param_tys`/`ret_ty`,
/// `Term::LetRec.ty`) by applying [`qualify_workspace_types`]. Bare
/// cross-module `Type::Con` names are upgraded to qualified
/// `<home>.<Type>` form so that consumer-side declared types unify
/// against imported-fn signatures (which the existing
/// [`qualify_local_types`] step already qualifies on the owner side).
pub fn qualify_workspace_module(
mut m: Module,
own_local_types: &IndexMap<String, TypeDef>,
module_types: &BTreeMap<String, IndexMap<String, TypeDef>>,
module_mono_fns: &BTreeMap<String, BTreeSet<String>>,
) -> Module {
for def in &mut m.defs {
match def {
Def::Fn(f) => {
f.ty = qualify_workspace_types(&f.ty, own_local_types, module_types);
qualify_workspace_term(&mut f.body, own_local_types, module_types, module_mono_fns);
}
Def::Const(c) => {
c.ty = qualify_workspace_types(&c.ty, own_local_types, module_types);
qualify_workspace_term(&mut c.value, own_local_types, module_types, module_mono_fns);
}
Def::Type(td) => {
// #50: a consumer module's ADT field can reference a
// *cross-module* (kernel-tier auto-imported) type-con by
// its bare name (`(con RawBuf …)`). The owner's own type
// names stay bare — `qualify_workspace_types` skips
// `own_local_types` and primitives — so only genuinely
// cross-module field types are upgraded to `<home>.<T>`,
// matching the qualification the op/value positions and
// the imported-fn signatures already receive.
for ctor in &mut td.ctors {
for field in &mut ctor.fields {
*field =
qualify_workspace_types(field, own_local_types, module_types);
}
}
}
Def::Class(_) | Def::Instance(_) => {
// Class / Instance defs hold types qualified through
// other mechanisms.
}
}
}
m
}
pub(crate) fn qualify_workspace_term(
t: &mut Term,
own_local_types: &IndexMap<String, TypeDef>,
module_types: &BTreeMap<String, IndexMap<String, TypeDef>>,
module_mono_fns: &BTreeMap<String, BTreeSet<String>>,
) {
match t {
Term::Lit { .. } | Term::Recur { .. } => {}
Term::Var { name } => {
// raw-buf.4: normalise a *cross-module* type-scoped call
// `T.f` to a *monomorphic* op into the module-qualified
// `<home>.f` form. The Term::New desugar emits
// `(app T.new …)` for every type; for a cross-module
// monomorphic `new` (e.g. raw_buf's RawBuf.new) nothing
// downstream rewrites the `T.new` callee, so codegen would
// hit `unknown variable`. Three carve-outs:
// - a same-module type (`own_local_types`) keeps `T.f` —
// synth's TypeDef-first ladder resolves it directly and
// rewriting to the bare module self-name breaks the
// receiver resolution (`type-scoped-receiver-not-a-type`);
// - a *polymorphic* op keeps `T.f` so the raw-buf.3
// monomorphisation mechanism mints its scope-qualified
// `T_f__<elem>` symbol from that spelling (RawBuf's ops);
// - any non-TypeDef prefix is untouched (ordinary module
// or class-method dotted names).
if name.matches('.').count() == 1 {
let (prefix, suffix) = name.split_once('.').expect("checked");
if !own_local_types.contains_key(prefix) {
if let Some(home) = module_types.iter().find_map(|(m, types)| {
if types.contains_key(prefix) {
Some(m.clone())
} else {
None
}
}) {
let is_mono = module_mono_fns
.get(&home)
.is_some_and(|fns| fns.contains(suffix));
if is_mono {
*name = format!("{home}.{suffix}");
}
}
}
}
}
Term::App { callee, args, .. } => {
qualify_workspace_term(callee, own_local_types, module_types, module_mono_fns);
for a in args {
qualify_workspace_term(a, own_local_types, module_types, module_mono_fns);
}
}
Term::Let { value, body, .. } => {
qualify_workspace_term(value, own_local_types, module_types, module_mono_fns);
qualify_workspace_term(body, own_local_types, module_types, module_mono_fns);
}
Term::LetRec { ty, body, in_term, .. } => {
*ty = qualify_workspace_types(ty, own_local_types, module_types);
qualify_workspace_term(body, own_local_types, module_types, module_mono_fns);
qualify_workspace_term(in_term, own_local_types, module_types, module_mono_fns);
}
Term::If { cond, then, else_ } => {
qualify_workspace_term(cond, own_local_types, module_types, module_mono_fns);
qualify_workspace_term(then, own_local_types, module_types, module_mono_fns);
qualify_workspace_term(else_, own_local_types, module_types, module_mono_fns);
}
Term::Do { args, .. } => {
for a in args {
qualify_workspace_term(a, own_local_types, module_types, module_mono_fns);
}
}
Term::Ctor { type_name, args, .. } => {
// prep.1: normalize bare cross-module `type_name` to
// qualified form, mirroring [`qualify_workspace_types`]
// for the `Type::Con.name` path.
if !type_name.contains('.')
&& !ailang_core::primitives::is_primitive_name(type_name)
&& !own_local_types.contains_key(type_name)
{
if let Some(home) = module_types
.iter()
.find_map(|(m, types)| if types.contains_key(type_name) { Some(m.clone()) } else { None })
{
*type_name = format!("{home}.{type_name}");
}
}
for a in args {
qualify_workspace_term(a, own_local_types, module_types, module_mono_fns);
}
}
Term::Match { scrutinee, arms } => {
qualify_workspace_term(scrutinee, own_local_types, module_types, module_mono_fns);
for arm in arms {
qualify_workspace_term(&mut arm.body, own_local_types, module_types, module_mono_fns);
}
}
Term::Lam { param_tys, ret_ty, body, .. } => {
for p in param_tys.iter_mut() {
*p = qualify_workspace_types(p, own_local_types, module_types);
}
**ret_ty = qualify_workspace_types(ret_ty, own_local_types, module_types);
qualify_workspace_term(body, own_local_types, module_types, module_mono_fns);
}
Term::Seq { lhs, rhs } => {
qualify_workspace_term(lhs, own_local_types, module_types, module_mono_fns);
qualify_workspace_term(rhs, own_local_types, module_types, module_mono_fns);
}
Term::Clone { value } => {
qualify_workspace_term(value, own_local_types, module_types, module_mono_fns)
}
Term::ReuseAs { source, body } => {
qualify_workspace_term(source, own_local_types, module_types, module_mono_fns);
qualify_workspace_term(body, own_local_types, module_types, module_mono_fns);
}
Term::Loop { binders, body } => {
for b in binders {
b.ty = qualify_workspace_types(&b.ty, own_local_types, module_types);
qualify_workspace_term(&mut b.init, own_local_types, module_types, module_mono_fns);
}
qualify_workspace_term(body, own_local_types, module_types, module_mono_fns);
}
// prep.2 (kernel-extension-mechanics): prep.1 pre-pass partner.
// Mirror the Term::Ctor arm above — normalize a bare
// cross-module `type_name` to qualified `<home>.<Type>` form
// before the synth pass elaborates the `new`-call. NewArg::Type
// values are recursively type-qualified; NewArg::Value subterms
// are recursively term-qualified.
Term::New { type_name, args } => {
if !type_name.contains('.')
&& !ailang_core::primitives::is_primitive_name(type_name)
&& !own_local_types.contains_key(type_name)
{
if let Some(home) = module_types.iter().find_map(|(m, types)| {
if types.contains_key(type_name) {
Some(m.clone())
} else {
None
}
}) {
*type_name = format!("{home}.{type_name}");
}
}
for arg in args.iter_mut() {
match arg {
NewArg::Value(v) => {
qualify_workspace_term(v, own_local_types, module_types, module_mono_fns)
}
NewArg::Type(t) => {
*t = qualify_workspace_types(t, own_local_types, module_types)
}
}
}
}
Term::Intrinsic => {}
}
}
/// Checks a pattern against an expected type and returns the bindings
/// introduced by the pattern.
fn type_check_pattern(
p: &Pattern,
expected: &Type,
env: &Env,
) -> Result<Vec<(String, Type)>> {
match p {
Pattern::Wild => Ok(vec![]),
Pattern::Var { name } => Ok(vec![(name.clone(), expected.clone())]),
Pattern::Lit { lit } => {
let lt = match lit {
Literal::Int { .. } => Type::int(),
Literal::Bool { .. } => Type::bool_(),
Literal::Str { .. } => Type::str_(),
Literal::Unit => Type::unit(),
Literal::Float { .. } => {
return Err(CheckError::FloatPatternNotAllowed);
}
};
expect_eq(expected, &lt)?;
Ok(vec![])
}
Pattern::Ctor { ctor, fields } => {
// nested **Ctor** sub-patterns are removed by
// `ailang_core::desugar::desugar_module` before this checker
// runs, so we only have to defend against the still-rejected
// **Lit** sub-pattern case. The `nested-ctor-pattern-not-allowed`
// error code is reused for that — its meaning is now narrower
// ("non-flat: a Lit sub-pattern was found"), and the docstring
// on the variant reflects that.
for sub in fields {
match sub {
Pattern::Var { .. } | Pattern::Wild => {}
Pattern::Lit { .. } => {
return Err(CheckError::NestedCtorPatternNotAllowed(ctor.clone()));
}
Pattern::Ctor { .. } => {
unreachable!(
"nested Ctor sub-patterns are removed by \
ailang_core::desugar before check"
);
}
}
}
// Canonical-type-pattern lookup: Pattern::Ctor lookup is type-driven post-canonical-type-form
// The scrutinee's Type::Con name is canonical (bare = local
// TypeDef, qualified = explicit cross-module). Derive the
// TypeDef from `expected` and find the ctor by name within
// it; no env.ctor_index consult, no imports-walk.
let (resolved_type_name, resolved_td, resolved_owning_module, scrutinee_args) =
match expected {
Type::Con { name, args } => {
if let Some((owner, suffix)) = name.split_once('.') {
let td = env
.module_types
.get(owner)
.and_then(|tys| tys.get(suffix))
.cloned()
.ok_or_else(|| {
CheckError::PatternTypeMismatch {
ctor: ctor.clone(),
ty: ailang_core::pretty::type_to_string(expected),
}
})?;
(name.clone(), td, Some(owner.to_string()), args.clone())
} else {
let td = env.types.get(name).cloned().ok_or_else(|| {
CheckError::PatternTypeMismatch {
ctor: ctor.clone(),
ty: ailang_core::pretty::type_to_string(expected),
}
})?;
(name.clone(), td, None, args.clone())
}
}
_ => {
return Err(CheckError::PatternTypeMismatch {
ctor: ctor.clone(),
ty: ailang_core::pretty::type_to_string(expected),
});
}
};
let td = &resolved_td;
let cdef = td
.ctors
.iter()
.find(|c| &c.name == ctor)
.ok_or_else(|| CheckError::UnknownCtorInPattern(ctor.clone()))?;
if fields.len() != cdef.fields.len() {
return Err(CheckError::CtorArity {
ty: resolved_type_name.clone(),
ctor: ctor.clone(),
expected: cdef.fields.len(),
got: fields.len(),
});
}
// substitute the scrutinee's concrete type-args
// into each cdef field type (e.g. `Cons(a, List a)` checked
// against a `List Int` scrutinee yields field types
// `Int, List Int`).
//
// when the resolved ctor lives in an imported
// module, qualify any bare local type-cons in the field
// types first — symmetric to the term-ctor fix.
let qualified_fields: Vec<Type> = match &resolved_owning_module {
Some(m) => {
let owner_types = env
.module_types
.get(m)
.cloned()
.unwrap_or_default();
cdef.fields
.iter()
.map(|f| qualify_local_types(f, m, &owner_types))
.collect()
}
None => cdef.fields.clone(),
};
let mapping: BTreeMap<String, Type> = td
.vars
.iter()
.cloned()
.zip(scrutinee_args)
.collect();
let mut out = Vec::new();
for (sub, sub_ty) in fields.iter().zip(qualified_fields.iter()) {
let sub_ty_inst = substitute_rigids(sub_ty, &mapping);
out.extend(type_check_pattern(sub, &sub_ty_inst, env)?);
}
Ok(out)
}
}
}
fn callee_name(t: &Term) -> String {
match t {
Term::Var { name } => name.clone(),
_ => "<expr>".into(),
}
}
fn expect_eq(expected: &Type, got: &Type) -> Result<()> {
if expected == got {
Ok(())
} else {
Err(CheckError::TypeMismatch {
expected: ailang_core::pretty::type_to_string(expected),
got: ailang_core::pretty::type_to_string(got),
})
}
}
/// Typechecker environment for a single module-check pass.
///
/// Cloned cheaply when we need a scoped extension (e.g. installing
/// rigid vars while checking a polymorphic def's body) so that the
/// parent scope stays immutable. Construction goes through
/// [`Env::default`] / the internal `new`; population is the
/// responsibility of [`builtins::install`] and the per-module setup in
/// `check_in_workspace`.
///
/// Several of the fields are conceptually disjoint name-spaces (term
/// vars vs effect ops vs ADT names vs ctor names), kept as separate
/// maps because the AST already commits to which channel a reference
/// goes through (`Term::Var` vs `Term::Do` vs `Term::Ctor` vs
/// `Pattern::Ctor`).
#[derive(Debug, Default, Clone)]
pub struct Env {
/// Term-level names in scope — built-in operators, user fn/const
/// defs of the current module, and (after pass-1) an entry per
/// local def. Looked up by `Term::Var { name }` lookup.
pub globals: IndexMap<String, Type>,
/// Effect-op table. Looked up by `Term::Do { op }`. See
/// [`builtins::EffectOpSig`] for the payload shape.
pub effect_ops: IndexMap<String, builtins::EffectOpSig>,
/// User-declared ADTs of the current module, by name. Populated
/// from `Def::Type` entries; consulted by `Term::Ctor`,
/// `Pattern::Ctor`, and the well-formedness check on declared
/// types.
pub types: IndexMap<String, TypeDef>,
/// Inverse index: ctor name -> reference to the owning ADT.
pub ctor_index: IndexMap<String, CtorRef>,
/// Import map: alias-or-module-name → actual module name.
/// Used when `Term::Var { name }` contains a dot
/// (qualified cross-module reference).
pub imports: BTreeMap<String, String>,
/// Top-level symbol table per module of the workspace.
/// Populated by [`crate::build_check_env`] from
/// [`build_module_globals`].
pub module_globals: BTreeMap<String, IndexMap<String, Type>>,
/// Per-module import map: module-name → (alias-or-module-name →
/// actual-module-name). Sibling-shape to [`Self::module_globals`];
/// populated workspace-flat by [`crate::build_check_env`] so the
/// mono pass's per-fn entry points can re-seed the local
/// [`Self::imports`] before re-running `synth` on a body. Both
/// `check_in_workspace` and `mono::build_workspace_env` consume
/// the same env shape; `check_in_workspace` then overwrites
/// [`Self::imports`] with the current module's map at the call
/// site.
pub module_imports: BTreeMap<String, BTreeMap<String, String>>,
/// ADT type definitions per module of the workspace. Used
/// to resolve qualified type references (`module.Type` in
/// `Type::Con.name`) and qualified `Term::Ctor.type_name`, and to
/// fall back when a bare `Pattern::Ctor.ctor` cannot be resolved
/// against the local module. Populated by `check_in_workspace`.
pub module_types: BTreeMap<String, IndexMap<String, TypeDef>>,
/// Name of the currently checked module. Used during var lookup to
/// treat self-references (module name == own name) as local globals,
/// without touching the `imports` channel.
pub current_module: String,
/// `true` when the currently checked module is kernel-tier
/// (`module.kernel`) or the prelude. An `(intrinsic)` body is legal
/// only here; the per-fn body check reads this to gate
/// `IntrinsicOutsideKernelTier`. Set alongside `current_module`.
pub current_module_kernel_tier: bool,
/// Rigid type vars in scope (Iter 12a). Populated by `check_fn` when
/// it peels an outer `Forall` from the def's type. Inside the body,
/// these names are legal as `Type::Var { name }` and unify only
/// with themselves.
pub rigid_vars: BTreeSet<String>,
/// workspace-flat aggregate of every module's
/// [`ModuleGlobals::class_methods`], re-keyed to
/// `(qualified-class-name, method-name)` so post-retirement of
/// `MethodNameCollision` two classes can share a method name.
/// Consumed by `synth`'s `Term::Var` arm via the resolved class
/// (from `method_to_candidate_classes` + dispatch) plus the method
/// name. Mono's presence checks consult
/// [`Self::method_to_candidate_classes`] (method-keyed natively).
pub class_methods: BTreeMap<(String, String), ClassMethodEntry>,
/// workspace-flat inverse of [`Self::class_methods`] — for
/// each method name, the set of qualified class names that declare
/// it. Pre-canonical-class-form, the `MethodNameCollision` invariant guarantees
/// each set is singleton; the type-driven dispatch refactor lifts the invariant and any
/// cardinality above one becomes legal. Synth's `Term::Var` arm
/// consults this index for type-driven dispatch (spec
/// §Architecture's 5-step rule).
pub method_to_candidate_classes: BTreeMap<String, BTreeSet<String>>,
/// post-superclass-expansion declared constraints of the
/// active fn body being checked. Populated by `check_fn` before
/// invoking `synth` on the body; empty at workspace entry.
/// Consumed by `synth`'s Var-arm class-method branch when calling
/// `resolve_method_dispatch` — the constraint-driven filter
/// disambiguates multi-candidate residuals at the rigid-var
/// fallback (e.g. inside a polymorphic fn body where the arg
/// type is still a rigid type variable).
pub active_declared_constraints: Vec<Constraint>,
/// one-step superclass expansion table.
/// Maps each class name to its superclass class name. Absence from
/// the map means the class has no superclass — populated only for
/// classes that declare one. Used by `check_fn` to expand
/// `Forall.constraints` for the missing-constraint check (the
/// typeclass design caps superclass expansion at one step). The
/// schema permits at most one
/// superclass per class.
pub class_superclasses: BTreeMap<String, String>,
/// workspace-wide instance registry, threaded
/// through from [`Workspace::registry`]. Read by `check_fn` in the
/// concrete-residual path: when a class-method call at a fully-
/// concrete type produces a residual `(class, type_)` whose
/// `(class, type_hash(type_))` key is absent from `registry.entries`,
/// the fn fires `NoInstance`. Default-constructed (empty) for
/// the standalone [`check_module`] entry point — pre-22b fixtures
/// never invoke class methods, so the empty registry is harmless.
pub workspace_registry: ailang_core::workspace::Registry,
}
/// Back-pointer from a ctor name to the ADT that declared it. Stored
/// in [`Env::ctor_index`] so a `Pattern::Ctor` or `Term::Ctor` can
/// resolve the owning ADT in O(1).
#[derive(Debug, Clone)]
pub struct CtorRef {
/// Name of the ADT (i.e. the `Def::Type` name) that declared the
/// ctor.
pub type_name: String,
}
impl Env {
pub(crate) fn new() -> Self {
Self::default()
}
}
#[cfg(test)]
mod tests {
use super::*;
use ailang_core::SCHEMA;
/// Helper that synths a single Term against a default empty env +
/// fresh local / scope / effect state. Returns the substituted
/// final type.
fn synth_standalone(term: &Term) -> Type {
let env = Env::default();
let mut locals: IndexMap<String, Type> = IndexMap::new();
// loop-recur iter 2: loop-free unit-test call site — fresh
// empty loop-stack.
let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
let mut effects: BTreeSet<String> = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
let mut residuals: Vec<ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
let mut warnings: Vec<Diagnostic> = Vec::new();
let ty = synth(
term,
&env,
&mut locals,
&mut loop_stack,
&mut effects,
"<test>",
&mut subst,
&mut counter,
&mut residuals,
&mut free_fn_calls,
&mut warnings,
)
.expect("synth must succeed");
subst.apply(&ty)
}
/// `CheckError::LoopBinderCapturedByLambda`
/// carries the stable kebab code `loop-binder-captured-by-lambda`
/// and a non-panicking `ctx()` arm carrying the captured name —
/// symmetric to `mut_var_captured_by_lambda_diagnostic_has_kebab_code`.
#[test]
fn loop_binder_captured_by_lambda_diagnostic_has_kebab_code() {
let e = CheckError::LoopBinderCapturedByLambda { name: "acc".into() };
assert_eq!(e.code(), "loop-binder-captured-by-lambda");
let _ = e.ctx();
}
/// loop-recur iter 2: the four `Recur*` `CheckError` variants carry
/// the exact stable kebab codes the spec acceptance mandates
/// (`recur-outside-loop` / `recur-arity-mismatch` /
/// `recur-type-mismatch` / `recur-not-in-tail-position`).
#[test]
fn recur_checkerror_codes_are_exact() {
assert_eq!(CheckError::RecurOutsideLoop.code(), "recur-outside-loop");
assert_eq!(
CheckError::RecurArityMismatch { expected: 2, got: 1 }.code(),
"recur-arity-mismatch"
);
assert_eq!(
CheckError::RecurTypeMismatch {
position: 0,
expected: "Int".into(),
got: "Bool".into(),
}
.code(),
"recur-type-mismatch"
);
assert_eq!(
CheckError::RecurNotInTailPosition.code(),
"recur-not-in-tail-position"
);
}
/// Regression guard — a lambda built without any enclosing loop
/// typechecks unchanged. Property protected: the free-var scan in
/// `Term::Lam`'s synth arm is gated on `!loop_stack.is_empty()`
/// and must not disturb lambdas outside loops. The body refers to
/// the lambda's own param (no builtin lookup needed) so the test
/// stays pure in `Env::default()`.
#[test]
fn lambda_outside_loop_still_typechecks_clean() {
let term = Term::Lam {
params: vec!["x".into()],
param_tys: vec![Type::int()],
ret_ty: Box::new(Type::int()),
effects: vec![],
body: Box::new(Term::Var { name: "x".into() }),
};
let _ty = synth_standalone(&term);
}
/// a lambda nested inside a `Term::Loop`
/// whose body references a loop binder declared by the enclosing
/// loop is rejected with `LoopBinderCapturedByLambda`. The
/// captured-name field reports the offending binder.
#[test]
fn lambda_inside_loop_capturing_binder_emits_loop_binder_captured_by_lambda() {
// (loop (acc : Int = 0)
// (let f = (lam () : Int -> acc) in 0))
let term = Term::Loop {
binders: vec![ailang_core::ast::LoopBinder {
name: "acc".into(),
ty: Type::int(),
init: Term::Lit { lit: Literal::Int { value: 0 } },
}],
body: Box::new(Term::Let {
name: "f".into(),
value: Box::new(Term::Lam {
params: vec![],
param_tys: vec![],
ret_ty: Box::new(Type::int()),
effects: vec![],
body: Box::new(Term::Var { name: "acc".into() }),
}),
body: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
}),
};
let env = Env::default();
let mut locals: IndexMap<String, Type> = IndexMap::new();
let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
let mut effects: BTreeSet<String> = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
let mut residuals: Vec<ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
let mut warnings: Vec<Diagnostic> = Vec::new();
let err = synth(
&term, &env, &mut locals, &mut loop_stack, &mut effects,
"<test>", &mut subst, &mut counter, &mut residuals,
&mut free_fn_calls, &mut warnings,
)
.expect_err("lambda capturing loop binder must be rejected");
match err {
CheckError::LoopBinderCapturedByLambda { name } => assert_eq!(name, "acc"),
other => panic!("expected LoopBinderCapturedByLambda, got {other:?}"),
}
}
fn fn_def(name: &str, ty: Type, params: Vec<&str>, body: Term) -> Def {
Def::Fn(FnDef {
name: name.into(),
ty,
params: params.into_iter().map(|s| s.into()).collect(),
body,
suppress: vec![],
doc: None,
export: None,
})
}
#[test]
fn checks_simple_arithmetic_fn() {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"add",
Type::Fn {
params: vec![Type::int(), Type::int()],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["a", "b"],
Term::App {
callee: Box::new(Term::Var { name: "+".into() }),
args: vec![
Term::Var { name: "a".into() },
Term::Var { name: "b".into() },
],
tail: false,
},
)],
};
check(&m).expect("should typecheck");
}
#[test]
fn rejects_type_mismatch() {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"bad",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::Lit {
lit: Literal::Bool { value: true },
},
)],
};
let err = check(&m).unwrap_err();
let msg = format!("{err}");
assert!(msg.contains("type mismatch"), "got: {msg}");
}
#[test]
fn requires_effect_to_be_declared() {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"leaks",
Type::Fn {
params: vec![],
ret: Box::new(Type::unit()),
effects: vec![], // !IO missing,
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::Do {
op: "io/print_str".into(),
args: vec![Term::Lit {
lit: Literal::Str {
value: "hi".into(),
},
}],
tail: false,
},
)],
};
let err = check(&m).unwrap_err();
let msg = format!("{err}");
assert!(msg.contains("undeclared effect"), "got: {msg}");
}
#[test]
fn lets_local_shadow_global() {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"f",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::Let {
name: "x".into(),
value: Box::new(Term::Lit {
lit: Literal::Int { value: 7 },
}),
body: Box::new(Term::Var { name: "x".into() }),
},
)],
};
check(&m).expect("should typecheck");
}
#[test]
fn match_must_be_exhaustive() {
// Type Maybe = None | Some(Int); fn f only matches None -> error.
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(TypeDef {
name: "Maybe".into(),
vars: vec![],
ctors: vec![
Ctor { name: "None".into(), fields: vec![] },
Ctor {
name: "Some".into(),
fields: vec![Type::int()],
},
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}),
fn_def(
"f",
Type::Fn {
params: vec![Type::Con { name: "Maybe".into(), args: vec![] }],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["m"],
Term::Match {
scrutinee: Box::new(Term::Var { name: "m".into() }),
arms: vec![Arm {
pat: Pattern::Ctor {
ctor: "None".into(),
fields: vec![],
},
body: Term::Lit {
lit: Literal::Int { value: 0 },
},
}],
},
),
],
};
let err = check(&m).unwrap_err();
let msg = format!("{err}");
assert!(msg.contains("non-exhaustive"), "got: {msg}");
assert!(msg.contains("Some"), "got: {msg}");
}
#[test]
fn match_with_wildcard_is_exhaustive() {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(TypeDef {
name: "Maybe".into(),
vars: vec![],
ctors: vec![
Ctor { name: "None".into(), fields: vec![] },
Ctor {
name: "Some".into(),
fields: vec![Type::int()],
},
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}),
fn_def(
"f",
Type::Fn {
params: vec![Type::Con { name: "Maybe".into(), args: vec![] }],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["m"],
Term::Match {
scrutinee: Box::new(Term::Var { name: "m".into() }),
arms: vec![
Arm {
pat: Pattern::Ctor {
ctor: "None".into(),
fields: vec![],
},
body: Term::Lit {
lit: Literal::Int { value: 0 },
},
},
Arm {
pat: Pattern::Wild,
body: Term::Lit {
lit: Literal::Int { value: 1 },
},
},
],
},
),
],
};
check(&m).expect("wildcard must satisfy exhaustiveness");
}
#[test]
fn if_branches_must_match() {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"f",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::If {
cond: Box::new(Term::Lit {
lit: Literal::Bool { value: true },
}),
then: Box::new(Term::Lit {
lit: Literal::Int { value: 1 },
}),
else_: Box::new(Term::Lit { lit: Literal::Unit }),
},
)],
};
let err = check(&m).unwrap_err();
assert!(format!("{err}").contains("type mismatch"));
}
/// a top-level def annotated `forall a. (a) -> a` is
/// admitted; its body checks against a rigid type var. The
/// var name (`a`) is in scope as a rigid throughout the body.
#[test]
fn polymorphic_id_def_typechecks() {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"id",
Type::Forall {
vars: vec!["a".into()],
constraints: vec![],
body: Box::new(Type::Fn {
params: vec![Type::Var { name: "a".into() }],
ret: Box::new(Type::Var { name: "a".into() }),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
}),
},
vec!["x"],
Term::Var { name: "x".into() },
)],
};
check(&m).expect("polymorphic id should typecheck");
}
/// `id` instantiates fresh metavars at each use site.
/// Calling `id(42)` produces an `Int`; calling `id(true)` would
/// produce a `Bool`. Two distinct uses must not bleed into each
/// other (each gets its own metavar).
#[test]
fn polymorphic_id_can_be_used_at_int_and_bool() {
let id_def = fn_def(
"id",
Type::Forall {
vars: vec!["a".into()],
constraints: vec![],
body: Box::new(Type::Fn {
params: vec![Type::Var { name: "a".into() }],
ret: Box::new(Type::Var { name: "a".into() }),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
}),
},
vec!["x"],
Term::Var { name: "x".into() },
);
// `use_int` returns id(42) :: Int.
let use_int = fn_def(
"use_int",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::App {
callee: Box::new(Term::Var { name: "id".into() }),
args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
tail: false,
},
);
// `use_bool` returns id(true) :: Bool.
let use_bool = fn_def(
"use_bool",
Type::Fn {
params: vec![],
ret: Box::new(Type::bool_()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::App {
callee: Box::new(Term::Var { name: "id".into() }),
args: vec![Term::Lit { lit: Literal::Bool { value: true } }],
tail: false,
},
);
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![id_def, use_int, use_bool],
};
check(&m).expect("two distinct id instantiations should typecheck");
}
/// a `Forall` callee at App must instantiate consistently.
/// `id(42) :: Bool` is rejected because the metavar gets pinned to
/// `Int` by the arg, which conflicts with the declared `Bool` ret.
#[test]
fn polymorphic_id_consistency_is_enforced() {
let id_def = fn_def(
"id",
Type::Forall {
vars: vec!["a".into()],
constraints: vec![],
body: Box::new(Type::Fn {
params: vec![Type::Var { name: "a".into() }],
ret: Box::new(Type::Var { name: "a".into() }),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
}),
},
vec!["x"],
Term::Var { name: "x".into() },
);
// Returns id(42) but declared Bool — must fail.
let bad = fn_def(
"bad",
Type::Fn {
params: vec![],
ret: Box::new(Type::bool_()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::App {
callee: Box::new(Term::Var { name: "id".into() }),
args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
tail: false,
},
);
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![id_def, bad],
};
let err = check(&m).unwrap_err();
let msg = format!("{err}");
assert!(msg.contains("type mismatch"), "got: {msg}");
}
/// two-var polymorphism. `apply : forall a b. ((a -> b),
/// a) -> b`. Body applies the function. We instantiate at two
/// different use sites with different (a, b) pairs.
#[test]
fn polymorphic_apply_with_two_vars() {
let apply_def = fn_def(
"apply",
Type::Forall {
vars: vec!["a".into(), "b".into()],
constraints: vec![],
body: Box::new(Type::Fn {
params: vec![
Type::Fn {
params: vec![Type::Var { name: "a".into() }],
ret: Box::new(Type::Var { name: "b".into() }),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
Type::Var { name: "a".into() },
],
ret: Box::new(Type::Var { name: "b".into() }),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
}),
},
vec!["f", "x"],
Term::App {
callee: Box::new(Term::Var { name: "f".into() }),
args: vec![Term::Var { name: "x".into() }],
tail: false,
},
);
// A monomorphic helper to be passed to apply.
let succ = fn_def(
"succ",
Type::Fn {
params: vec![Type::int()],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["n"],
Term::App {
callee: Box::new(Term::Var { name: "+".into() }),
args: vec![
Term::Var { name: "n".into() },
Term::Lit { lit: Literal::Int { value: 1 } },
],
tail: false,
},
);
let use_apply = fn_def(
"use_apply",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::App {
callee: Box::new(Term::Var { name: "apply".into() }),
args: vec![
Term::Var { name: "succ".into() },
Term::Lit { lit: Literal::Int { value: 41 } },
],
tail: false,
},
);
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![apply_def, succ, use_apply],
};
check(&m).expect("apply instantiation should typecheck");
}
/// parameterised ADT — `type Box[a] = MkBox(a)` is well-
/// formed and `MkBox(42)` typechecks at result type `Box<Int>`.
#[test]
fn parameterised_adt_ctor_at_int() {
let box_def = Def::Type(TypeDef {
name: "Box".into(),
vars: vec!["a".into()],
ctors: vec![Ctor {
name: "MkBox".into(),
fields: vec![Type::Var { name: "a".into() }],
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
});
// fn make :: () -> Box<Int> = MkBox(42)
let make = fn_def(
"make",
Type::Fn {
params: vec![],
ret: Box::new(Type::Con {
name: "Box".into(),
args: vec![Type::int()],
}),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::Ctor {
type_name: "Box".into(),
ctor: "MkBox".into(),
args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
},
);
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![box_def, make],
};
check(&m).expect("Box<Int> ctor should typecheck");
}
/// ctor field type substitution and match-arm bindings.
/// `unbox :: forall a. (Box<a>) -> a` extracts the wrapped value.
#[test]
fn parameterised_adt_polymorphic_unbox() {
let box_def = Def::Type(TypeDef {
name: "Box".into(),
vars: vec!["a".into()],
ctors: vec![Ctor {
name: "MkBox".into(),
fields: vec![Type::Var { name: "a".into() }],
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
});
let unbox = Def::Fn(FnDef {
name: "unbox".into(),
ty: Type::Forall {
vars: vec!["a".into()],
constraints: vec![],
body: Box::new(Type::Fn {
params: vec![Type::Con {
name: "Box".into(),
args: vec![Type::Var { name: "a".into() }],
}],
ret: Box::new(Type::Var { name: "a".into() }),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
}),
},
params: vec!["b".into()],
body: Term::Match {
scrutinee: Box::new(Term::Var { name: "b".into() }),
arms: vec![Arm {
pat: Pattern::Ctor {
ctor: "MkBox".into(),
fields: vec![Pattern::Var { name: "x".into() }],
},
body: Term::Var { name: "x".into() },
}],
},
suppress: vec![],
doc: None,
export: None,
});
// Use unbox at Int and at Bool — both must succeed and not
// cross-contaminate the polymorphic variable.
let use_int = fn_def(
"ui",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::App {
callee: Box::new(Term::Var { name: "unbox".into() }),
args: vec![Term::Ctor {
type_name: "Box".into(),
ctor: "MkBox".into(),
args: vec![Term::Lit { lit: Literal::Int { value: 7 } }],
}],
tail: false,
},
);
let use_bool = fn_def(
"ub",
Type::Fn {
params: vec![],
ret: Box::new(Type::bool_()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::App {
callee: Box::new(Term::Var { name: "unbox".into() }),
args: vec![Term::Ctor {
type_name: "Box".into(),
ctor: "MkBox".into(),
args: vec![Term::Lit { lit: Literal::Bool { value: true } }],
}],
tail: false,
},
);
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![box_def, unbox, use_int, use_bool],
};
check(&m).expect("polymorphic Box should typecheck at both instantiations");
}
/// parameterised-ADT arity is enforced. `Box` (1 var)
/// used as `Box<Int, Bool>` must error.
#[test]
fn parameterised_adt_arity_is_enforced() {
let box_def = Def::Type(TypeDef {
name: "Box".into(),
vars: vec!["a".into()],
ctors: vec![Ctor {
name: "MkBox".into(),
fields: vec![Type::Var { name: "a".into() }],
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
});
let bad = fn_def(
"bad",
Type::Fn {
params: vec![Type::Con {
name: "Box".into(),
args: vec![Type::int(), Type::bool_()],
}],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["b"],
Term::Lit { lit: Literal::Int { value: 0 } },
);
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![box_def, bad],
};
let err = check(&m).unwrap_err();
let msg = format!("{err}");
assert!(msg.contains("expects 1 type arg"), "got: {msg}");
}
/// `seq` requires lhs to be Unit. A non-Unit lhs is a
/// type error — the value of lhs gets discarded so a useful (non-
/// Unit) value would silently vanish.
#[test]
fn seq_lhs_must_be_unit() {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"f",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::Seq {
lhs: Box::new(Term::Lit {
lit: Literal::Int { value: 7 },
}),
rhs: Box::new(Term::Lit {
lit: Literal::Int { value: 1 },
}),
},
)],
};
let err = check(&m).unwrap_err();
let msg = format!("{err}");
assert!(msg.contains("type mismatch"), "got: {msg}");
}
/// a `Term::App { tail: true, .. }` in non-tail position
/// must surface as `tail-call-not-in-tail-position`. Construction:
/// the recursive call sits as an argument to a Cons ctor (the
/// classic constructor-blocked recursion from the 14d survey).
#[test]
fn tail_call_in_non_tail_position_is_rejected() {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(TypeDef {
name: "L".into(),
vars: vec![],
ctors: vec![
Ctor { name: "N".into(), fields: vec![] },
Ctor {
name: "C".into(),
fields: vec![
Type::int(),
Type::Con { name: "L".into(), args: vec![] },
],
},
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}),
fn_def(
"loop",
Type::Fn {
params: vec![Type::Con { name: "L".into(), args: vec![] }],
ret: Box::new(Type::Con { name: "L".into(), args: vec![] }),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["xs"],
// Body: C(0, tail-app loop xs) — the recursion is
// an arg to C, which is NOT a tail position.
Term::Ctor {
type_name: "L".into(),
ctor: "C".into(),
args: vec![
Term::Lit { lit: Literal::Int { value: 0 } },
Term::App {
callee: Box::new(Term::Var { name: "loop".into() }),
args: vec![Term::Var { name: "xs".into() }],
tail: true,
},
],
},
),
],
};
let err = check(&m).unwrap_err();
assert_eq!(err.code(), "tail-call-not-in-tail-position", "{err}");
}
// ----- Iter 15a: cross-module type / ctor resolution ------------------
/// Helper for the cross-module tests: build a workspace whose entry
/// imports `lib` and exposes its types via qualified names.
fn cross_module_ws(consumer: Module) -> Workspace {
let lib = Module {
schema: SCHEMA.into(),
name: "lib".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Type(TypeDef {
name: "Box".into(),
vars: vec!["a".into()],
ctors: vec![Ctor {
name: "MkBox".into(),
fields: vec![Type::Var { name: "a".into() }],
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
})],
};
let mut modules = BTreeMap::new();
modules.insert("lib".into(), lib);
modules.insert(consumer.name.clone(), consumer.clone());
Workspace {
entry: consumer.name,
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
}
}
/// a qualified `Type::Con` (`lib.Box`) resolves
/// through `module_types` rather than the local-module `types`.
#[test]
fn cross_module_qualified_type_in_param_resolves() {
let consumer = Module {
schema: SCHEMA.into(),
name: "use_lib".into(),
kernel: false,
imports: vec![Import { module: "lib".into(), alias: None }],
defs: vec![fn_def(
"noop",
Type::Fn {
params: vec![Type::Con {
name: "lib.Box".into(),
args: vec![Type::int()],
}],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["b"],
Term::Lit { lit: Literal::Int { value: 0 } },
)],
};
let ws = cross_module_ws(consumer);
let diags = check_workspace(&ws);
assert!(diags.is_empty(), "expected green; got {diags:?}");
}
/// a qualified `Term::Ctor.type_name`
/// (`lib.Box`) resolves and constructs `lib.Box<Int>`.
#[test]
fn cross_module_qualified_term_ctor_resolves() {
let consumer = Module {
schema: SCHEMA.into(),
name: "use_lib".into(),
kernel: false,
imports: vec![Import { module: "lib".into(), alias: None }],
defs: vec![fn_def(
"make",
Type::Fn {
params: vec![],
ret: Box::new(Type::Con {
name: "lib.Box".into(),
args: vec![Type::int()],
}),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::Ctor {
type_name: "lib.Box".into(),
ctor: "MkBox".into(),
args: vec![Term::Lit { lit: Literal::Int { value: 7 } }],
},
)],
};
let ws = cross_module_ws(consumer);
let diags = check_workspace(&ws);
assert!(diags.is_empty(), "expected green; got {diags:?}");
}
/// a bare `Pattern::Ctor` (e.g. `MkBox x`)
/// against a scrutinee of type `lib.Box<Int>` resolves through
/// the type-driven lookup keyed on `expected.name`. Previously
/// this exercised an imports-fallback; post-canonical-type-form the lookup is
/// anchored to the scrutinee's qualified TypeDef directly.
#[test]
fn cross_module_pat_ctor_typedriven_resolves() {
let consumer = Module {
schema: SCHEMA.into(),
name: "use_lib".into(),
kernel: false,
imports: vec![Import { module: "lib".into(), alias: None }],
defs: vec![fn_def(
"open",
Type::Fn {
params: vec![Type::Con {
name: "lib.Box".into(),
args: vec![Type::int()],
}],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["b"],
Term::Match {
scrutinee: Box::new(Term::Var { name: "b".into() }),
arms: vec![Arm {
pat: Pattern::Ctor {
ctor: "MkBox".into(),
fields: vec![Pattern::Var { name: "x".into() }],
},
body: Term::Var { name: "x".into() },
}],
},
)],
};
let ws = cross_module_ws(consumer);
let diags = check_workspace(&ws);
assert!(diags.is_empty(), "expected green; got {diags:?}");
}
/// a recursive cross-module ADT (`std_list.List a` with a
/// `Cons a (List a)` ctor) round-trips through both `Term::Ctor` synth
/// and pattern-ctor binding without unqualified-field-name unification
/// failures. The bug fixed in 15b: `cdef.fields` on the imported side
/// carries `Con("List", _)` (unqualified, owner's local namespace),
/// while the consumer-visible scrutinee/result type is
/// `Con("std_list.List", _)`. Without `qualify_local_types` applied
/// to the fields at use sites, `unify` rejected the mismatch.
#[test]
fn cross_module_recursive_adt_term_and_pat_ctor() {
// Library: `data List a = Nil | Cons a (List a)`. The `Cons`
// field types reference the local-namespace `List`, exactly
// mirroring the std_list shape that tripped the gap.
let lib = Module {
schema: SCHEMA.into(),
name: "lst".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Type(TypeDef {
name: "List".into(),
vars: vec!["a".into()],
ctors: vec![
Ctor { name: "Nil".into(), fields: vec![] },
Ctor {
name: "Cons".into(),
fields: vec![
Type::Var { name: "a".into() },
Type::Con {
name: "List".into(),
args: vec![Type::Var { name: "a".into() }],
},
],
},
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
})],
};
// Consumer: builds `Cons 1 (Cons 2 (Nil))` via qualified
// `lst.List/Cons` and pattern-matches it back out. The match
// arm exercises the symmetric pat-ctor fix.
let cons = |head: i64, tail: Term| Term::Ctor {
type_name: "lst.List".into(),
ctor: "Cons".into(),
args: vec![
Term::Lit { lit: Literal::Int { value: head } },
tail,
],
};
let nil = Term::Ctor {
type_name: "lst.List".into(),
ctor: "Nil".into(),
args: vec![],
};
let consumer = Module {
schema: SCHEMA.into(),
name: "uses_lst".into(),
kernel: false,
imports: vec![Import { module: "lst".into(), alias: None }],
defs: vec![fn_def(
"head_or_zero",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::Match {
scrutinee: Box::new(cons(1, cons(2, nil.clone()))),
arms: vec![
Arm {
pat: Pattern::Ctor {
ctor: "Cons".into(),
fields: vec![
Pattern::Var { name: "h".into() },
Pattern::Wild,
],
},
body: Term::Var { name: "h".into() },
},
Arm {
pat: Pattern::Ctor {
ctor: "Nil".into(),
fields: vec![],
},
body: Term::Lit { lit: Literal::Int { value: 0 } },
},
],
},
)],
};
let mut modules = BTreeMap::new();
modules.insert("lst".into(), lib);
modules.insert("uses_lst".into(), consumer);
let ws = Workspace {
entry: "uses_lst".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(diags.is_empty(), "expected green; got {diags:?}");
}
/// Canonical-type qualification: a class method whose declared return type is a
/// bare local Type::Con in the defining module (e.g.
/// `compare : a -> a -> Ordering` declared inside `prelude`) must
/// be presented to a consumer module's typecheck context with the
/// return type qualified (`prelude.Ordering`). Without this, the
/// consumer's `Pattern::Ctor LT` against the scrutinee no longer
/// resolves once the post-canonical-type-form canonical form removes the
/// imports-fallback that previously papered over the mismatch.
#[test]
fn ct2_class_method_cross_module_qualifies_return_type() {
// Defining module declares `Ordering` locally and a class
// `Ord` with a method `compare : a -> a -> Ordering`. The
// `Ordering` Type::Con is bare-local in the class method's ty,
// which is canonical post-canonical-type-form (bare = local to defining module).
let prelude = Module {
schema: SCHEMA.into(),
name: "p".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(TypeDef {
name: "Ordering".into(),
vars: vec![],
ctors: vec![
Ctor { name: "LT".into(), fields: vec![] },
Ctor { name: "EQ".into(), fields: vec![] },
Ctor { name: "GT".into(), fields: vec![] },
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}),
Def::Class(ClassDef {
name: "Ord".into(),
param: "a".into(),
superclass: None,
methods: vec![ClassMethod {
name: "compare".into(),
ty: Type::Forall {
vars: vec!["a".into()],
constraints: vec![],
body: Box::new(Type::Fn {
params: vec![
Type::Var { name: "a".into() },
Type::Var { name: "a".into() },
],
ret: Box::new(Type::Con {
name: "Ordering".into(),
args: vec![],
}),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
}),
},
default: None,
}],
doc: None,
}),
Def::Instance(InstanceDef {
class: "Ord".into(),
type_: Type::int(),
methods: vec![InstanceMethod {
name: "compare".into(),
body: Term::Lam {
params: vec!["x".into(), "y".into()],
param_tys: vec![Type::int(), Type::int()],
ret_ty: Box::new(Type::Con {
name: "Ordering".into(),
args: vec![],
}),
effects: vec![],
body: Box::new(Term::Ctor {
type_name: "Ordering".into(),
ctor: "EQ".into(),
args: vec![],
}),
},
}],
doc: None,
}),
],
};
// Consumer module imports prelude and calls `compare` (bare).
// The return type seen by the consumer must be `p.Ordering`,
// not bare `Ordering` — otherwise the match arm below fails to
// typecheck because the Pattern::Ctor lookup is type-driven and
// would not find `LT` in any TypeDef named bare `Ordering` in
// the consumer's local types.
let consumer = Module {
schema: SCHEMA.into(),
name: "u".into(),
kernel: false,
imports: vec![Import { module: "p".into(), alias: None }],
defs: vec![fn_def(
"use_compare",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::Match {
scrutinee: Box::new(Term::App {
callee: Box::new(Term::Var { name: "compare".into() }),
args: vec![
Term::Lit { lit: Literal::Int { value: 1 } },
Term::Lit { lit: Literal::Int { value: 2 } },
],
tail: false,
}),
arms: vec![
Arm {
pat: Pattern::Ctor {
ctor: "LT".into(),
fields: vec![],
},
body: Term::Lit { lit: Literal::Int { value: 1 } },
},
Arm {
pat: Pattern::Ctor {
ctor: "EQ".into(),
fields: vec![],
},
body: Term::Lit { lit: Literal::Int { value: 2 } },
},
Arm {
pat: Pattern::Ctor {
ctor: "GT".into(),
fields: vec![],
},
body: Term::Lit { lit: Literal::Int { value: 3 } },
},
],
},
)],
};
let mut modules = BTreeMap::new();
modules.insert("p".into(), prelude);
modules.insert("u".into(), consumer);
let ws = Workspace {
entry: "u".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.is_empty(),
"consumer module must typecheck cleanly when calling a class \
method whose return type is bare-local in its defining \
module; the class-method channel must apply \
qualify_local_types just like the qualified Term::Var path \
does. Got diagnostics: {:?}",
diags
);
}
/// Canonical-type qualification: `qualify_local_types`'s `Type::Forall` arm must
/// recurse into `constraints[].type_`. A class method whose
/// declared type is `Forall<a>{Ord a}. Fn[..]` carries the
/// constraint type `Type::Var { name: "a" }` — fine — but a
/// hypothetical `Forall<a>{Show p.Foo}. Fn[..]` would carry a
/// bare-local `Foo` if the defining module is `p`, and the
/// consumer must see `p.Foo` after the cross-module qualifier
/// runs. Symmetric to the canonical-form-normalisation follow-up fix on
/// `normalize_type_for_registry`.
#[test]
fn ct2_qualify_local_types_recurses_into_forall_constraints() {
use crate::qualify_local_types;
let mut local_types: IndexMap<String, TypeDef> = IndexMap::new();
local_types.insert("Foo".into(), TypeDef {
name: "Foo".into(),
vars: vec![],
ctors: vec![Ctor { name: "MkFoo".into(), fields: vec![] }],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
});
let input = Type::Forall {
vars: vec!["a".into()],
constraints: vec![Constraint {
class: "Show".into(),
type_: Type::Con { name: "Foo".into(), args: vec![] },
}],
body: Box::new(Type::Fn {
params: vec![Type::Var { name: "a".into() }],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
}),
};
let out = qualify_local_types(&input, "p", &local_types);
match out {
Type::Forall { constraints, .. } => {
assert_eq!(constraints.len(), 1, "constraint count preserved");
match &constraints[0].type_ {
Type::Con { name, .. } => assert_eq!(
name, "p.Foo",
"constraint Type::Con must be qualified by qualify_local_types"
),
other => panic!("expected Type::Con, got {:?}", other),
}
}
other => panic!("expected Type::Forall, got {:?}", other),
}
}
/// a `Term::App { tail: true, .. }` that genuinely sits
/// in tail position (as the rhs of a `Seq` that is the body of a
/// `Match` arm that is the body of the fn) must pass.
#[test]
fn tail_call_in_tail_position_is_accepted() {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(TypeDef {
name: "L".into(),
vars: vec![],
ctors: vec![
Ctor { name: "N".into(), fields: vec![] },
Ctor {
name: "C".into(),
fields: vec![
Type::int(),
Type::Con { name: "L".into(), args: vec![] },
],
},
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}),
fn_def(
"drain",
Type::Fn {
params: vec![Type::Con { name: "L".into(), args: vec![] }],
ret: Box::new(Type::unit()),
effects: vec!["IO".into()],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["xs"],
Term::Match {
scrutinee: Box::new(Term::Var { name: "xs".into() }),
arms: vec![
Arm {
pat: Pattern::Ctor {
ctor: "N".into(),
fields: vec![],
},
body: Term::Lit { lit: Literal::Unit },
},
Arm {
pat: Pattern::Ctor {
ctor: "C".into(),
fields: vec![
Pattern::Var { name: "h".into() },
Pattern::Var { name: "t".into() },
],
},
body: Term::Seq {
lhs: Box::new(Term::Do {
op: "io/print_str".into(),
args: vec![Term::Lit {
lit: Literal::Str {
value: "x".into(),
},
}],
tail: false,
}),
rhs: Box::new(Term::App {
callee: Box::new(Term::Var { name: "drain".into() }),
args: vec![Term::Var { name: "t".into() }],
tail: true,
}),
},
},
],
},
),
],
};
check(&m).expect("tail-call in tail position should typecheck");
}
// 2026-05-21 operator-routing-eq-ord: the
// `letrec_with_let_binding_capture_typechecks` test relied on
// the builtin `>=` to express its `if (>= i threshold) ...`
// condition. With `>=` deleted from the builtin table, the test
// cannot be reconstructed inside this single-module check_module
// env (which has no prelude auto-import, so `ge` is unbound).
// The LetRec-captures-Let-binding property remains pinned by
// the workspace e2e tests `local_rec_let_capture` (and siblings)
// which DO carry the auto-imported prelude.
/// a LetRec whose body returns the wrong type (Bool
/// instead of the declared Int) is caught by the new typing rule.
/// Property protected: the new arm in `synth` for `Term::LetRec`
/// runs `unify(&ret_ty, &body_ty, subst)` just like `Term::Lam`
/// and `check_fn`.
#[test]
fn letrec_body_wrong_return_type_is_rejected() {
// (let-rec wrong (params x) (type (Int) -> Int) (body true)
// (in (app wrong 0)))
let letrec = Term::LetRec {
name: "wrong".into(),
ty: Type::Fn {
params: vec![Type::int()],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
params: vec!["x".into()],
body: Box::new(Term::Lit { lit: Literal::Bool { value: true } }),
in_term: Box::new(Term::App {
callee: Box::new(Term::Var { name: "wrong".into() }),
args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
tail: false,
}),
};
// Wrap in a Let so the desugar pass defers the LetRec (its
// body would otherwise lift cleanly with no captures, since
// `true` doesn't reference `x`).
let body = Term::Let {
name: "y".into(),
value: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
// Reference `y` inside the LetRec body so it captures.
body: Box::new(Term::LetRec {
name: "wrong".into(),
ty: Type::Fn {
params: vec![Type::int()],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
params: vec!["x".into()],
body: Box::new(Term::Seq {
// Use `y` so the LetRec captures it (forces deferral).
lhs: Box::new(Term::Lit { lit: Literal::Unit }),
rhs: Box::new(Term::App {
callee: Box::new(Term::Var { name: "+".into() }),
args: vec![
Term::Var { name: "y".into() },
Term::Lit { lit: Literal::Bool { value: true } },
],
tail: false,
}),
}),
in_term: Box::new(Term::App {
callee: Box::new(Term::Var { name: "wrong".into() }),
args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
tail: false,
}),
}),
};
// (Suppress dead-code warning on the unused unwrapped letrec.)
let _ = letrec;
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"outer",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
body,
)],
};
let err = check(&m).expect_err("LetRec body returning Bool but declared Int must error");
let msg = format!("{err}");
assert!(
msg.contains("type mismatch"),
"expected a type-mismatch diagnostic, got: {msg}"
);
}
/// `lift_letrecs` on a module containing a deferred
/// LetRec produces a module whose defs include a synthetic
/// `<hint>$lr_N` FnDef and whose original fn body has rewritten
/// call sites.
#[test]
fn lift_letrecs_on_let_capture_produces_synthetic_fn() {
// fn outer : () -> Int = \.
// let y = 7
// in let-rec helper : (Int) -> Int = \x. + x y
// in helper 1
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"outer",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::Let {
name: "y".into(),
value: Box::new(Term::Lit { lit: Literal::Int { value: 7 } }),
body: Box::new(Term::LetRec {
name: "helper".into(),
ty: Type::Fn {
params: vec![Type::int()],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
params: vec!["x".into()],
body: Box::new(Term::App {
callee: Box::new(Term::Var { name: "+".into() }),
args: vec![
Term::Var { name: "x".into() },
Term::Var { name: "y".into() },
],
tail: false,
}),
in_term: Box::new(Term::App {
callee: Box::new(Term::Var { name: "helper".into() }),
args: vec![Term::Lit { lit: Literal::Int { value: 1 } }],
tail: false,
}),
}),
},
)],
};
// Typecheck must succeed (the new LetRec rule accepts this).
check(&m).expect("typecheck before lift");
let desugared = ailang_core::desugar::desugar_module(&m);
// After desugar the LetRec is still present (Let-binding capture).
// After lift_letrecs it must be gone, replaced by a synthetic
// top-level fn with the capture appended to its signature.
let lifted = lift_letrecs(&desugared).expect("lift_letrecs");
assert_eq!(lifted.defs.len(), 2, "expected one synthetic fn appended");
let synth = match &lifted.defs[1] {
Def::Fn(f) => f,
_ => panic!("expected synthetic FnDef"),
};
assert!(
synth.name.starts_with("helper$lr_"),
"lifted name `{}` should start with `helper$lr_`",
synth.name
);
assert_eq!(
synth.ty,
Type::Fn {
params: vec![Type::int(), Type::int()],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
"lifted ty should have capture appended; got {:?}",
synth.ty
);
assert_eq!(synth.params, vec!["x".to_string(), "y".to_string()]);
// `outer`'s body must have the `(app helper 1)` rewritten to
// `(app helper$lr_0 1 y)`. The body is now
// `let y = 7 in (app helper$lr_0 1 y)`.
let outer_body = match &lifted.defs[0] {
Def::Fn(f) => &f.body,
_ => unreachable!(),
};
let inner = match outer_body {
Term::Let { body, .. } => body.as_ref(),
other => panic!("expected outer Let, got {other:?}"),
};
match inner {
Term::App { callee, args, .. } => {
match callee.as_ref() {
Term::Var { name } => assert_eq!(name, &synth.name),
other => panic!("expected lifted callee, got {other:?}"),
}
assert_eq!(args.len(), 2, "expected 2 args (1 original + 1 capture)");
match &args[1] {
Term::Var { name } => assert_eq!(name, "y"),
other => panic!("expected y as second arg, got {other:?}"),
}
}
other => panic!("expected App after Let, got {other:?}"),
}
}
/// a LetRec whose body captures a `Pattern::Ctor`-Var
/// match-arm binding is lifted by `lift_letrecs` to a synthetic
/// top-level fn whose signature has the binding's type appended.
/// Property protected: `type_check_pattern_for_lift` substitutes
/// the matched ADT's type args (`[Int, Int]`) into the ctor's
/// declared field types (`[a, b]`) and returns `[(x, Int),
/// (y, Int)]`; the lifted fn picks up `x: Int` as the capture
/// type. Without 16b.4, the desugar pass would have panicked
/// before reaching `lift_letrecs`.
#[test]
fn lift_letrecs_on_match_arm_capture_produces_synthetic_fn() {
// (data Pair (vars a b) (ctor MkPair a b))
// (fn outer : (Pair Int Int) -> Int = \p.
// match p
// case (pat-ctor MkPair x y) ->
// let-rec helper : (Int) -> Int = \z. + z x
// in (app helper 0))
let pair_td = TypeDef {
name: "Pair".into(),
vars: vec!["a".into(), "b".into()],
ctors: vec![Ctor {
name: "MkPair".into(),
fields: vec![
Type::Var { name: "a".into() },
Type::Var { name: "b".into() },
],
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
};
let letrec = Term::LetRec {
name: "helper".into(),
ty: Type::Fn {
params: vec![Type::int()],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
params: vec!["z".into()],
body: Box::new(Term::App {
callee: Box::new(Term::Var { name: "+".into() }),
args: vec![
Term::Var { name: "z".into() },
Term::Var { name: "x".into() },
],
tail: false,
}),
in_term: Box::new(Term::App {
callee: Box::new(Term::Var { name: "helper".into() }),
args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
tail: false,
}),
};
let outer_body = Term::Match {
scrutinee: Box::new(Term::Var { name: "p".into() }),
arms: vec![Arm {
pat: Pattern::Ctor {
ctor: "MkPair".into(),
fields: vec![
Pattern::Var { name: "x".into() },
Pattern::Var { name: "y".into() },
],
},
body: letrec,
}],
};
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(pair_td),
fn_def(
"outer",
Type::Fn {
params: vec![Type::Con {
name: "Pair".into(),
args: vec![Type::int(), Type::int()],
}],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["p"],
outer_body,
),
],
};
// Typecheck must succeed.
check(&m).expect("typecheck before lift");
let desugared = ailang_core::desugar::desugar_module(&m);
// Match-arm capture: desugar leaves the LetRec in place.
let lifted = lift_letrecs(&desugared).expect("lift_letrecs");
// Pair (Type) + outer (Fn) + helper$lr_0 (Fn) = 3.
assert_eq!(lifted.defs.len(), 3, "expected one synthetic fn appended");
let synth = match &lifted.defs[2] {
Def::Fn(f) => f,
_ => panic!("expected synthetic FnDef at index 2"),
};
assert!(
synth.name.starts_with("helper$lr_"),
"lifted name `{}` should start with `helper$lr_`",
synth.name
);
// Lifted ty: original (Int) -> Int with capture type Int
// appended → (Int, Int) -> Int.
assert_eq!(
synth.ty,
Type::Fn {
params: vec![Type::int(), Type::int()],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
"lifted ty should have the match-arm-capture type Int appended; got {:?}",
synth.ty
);
assert_eq!(synth.params, vec!["z".to_string(), "x".to_string()]);
}
// 2026-05-21 operator-routing-eq-ord: the
// `lift_letrecs_under_polymorphic_enclosing_fn_produces_forall_fn`
// test (originally here) relied on the builtin `==` to express
// its `if (== k 0) ...` condition. With `==` deleted from the
// builtin table the test cannot be reconstructed inside this
// single-module check env (`eq` from prelude.Eq is not visible
// without auto-import). The lift-letrec-under-polymorphic-fn
// property remains exercised by the workspace e2e tests
// `local_rec_let_capture` and siblings, which DO carry the
// implicit prelude import.
// 2026-05-21 operator-routing-eq-ord: the five `eq_*` tests
// formerly here (`eq_typechecks_at_int` / `_bool` / `_str` /
// `_unit` and `eq_rejects_mixed_int_bool`) pinned the
// polymorphic-`==` builtin shape (`forall a. (a, a) -> Bool`
// resolves at any concrete arg pair, type-mismatch on Int+Bool).
// With `==` deleted from the builtin table, the surface
// equivalent is the class method `eq` dispatched via prelude.Eq
// — which is not visible in this single-module check_module test
// env (no prelude auto-import). The properties move to
// `eq_user_adt_smoke_e2e` (Eq Unit), `eq_demo` (Int/Bool/Str
// dispatch via class-method), and `eq_float_noinstance` (the
// "no instance" rejection for an unsupported type).
/// a `(reuse-as xs 42)` where the body is a literal
/// (not a `Term::Ctor` and not `Term::Lam`) must emit
/// `reuse-as-non-allocating-body` with `ctx.got = "lit"`. The
/// suggested rewrite drops the wrapper; the replacement parses
/// via `parse_term`.
#[test]
fn reuse_as_with_non_allocating_body_is_reported() {
// Body: (reuse-as x 42) — `x` is the param, body is a lit.
let body = Term::ReuseAs {
source: Box::new(Term::Var { name: "x".into() }),
body: Box::new(Term::Lit { lit: Literal::Int { value: 42 } }),
};
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"f",
Type::Fn {
params: vec![Type::int()],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["x"],
body,
)],
};
let diags = check_module(&m);
let bad: Vec<&Diagnostic> = diags
.iter()
.filter(|d| d.code == "reuse-as-non-allocating-body")
.collect();
assert_eq!(
bad.len(),
1,
"want exactly one reuse-as-non-allocating-body; got: {diags:#?}"
);
let d = bad[0];
assert_eq!(d.severity, Severity::Error);
assert_eq!(d.def.as_deref(), Some("f"));
assert_eq!(d.ctx.get("got").and_then(|v| v.as_str()), Some("lit"));
assert_eq!(d.suggested_rewrites.len(), 1);
// Replacement is the body without the wrapper — must parse.
let rep = &d.suggested_rewrites[0].replacement;
ailang_surface::parse_term(rep)
.unwrap_or_else(|e| panic!("suggested rewrite must parse: {rep} ({e})"));
}
/// Floats milestone post-fieldtest B1 (RED): pattern-matching on a
/// `Literal::Float` literal must be hard-rejected at typecheck via
/// `CheckError::FloatPatternNotAllowed` per
/// design/contracts/0005-float-semantics.md — even when the match arm reaches `check` through
/// the *full* check pipeline (which runs `desugar_module` first).
///
/// The existing `reject_float_pattern_in_match` test in
/// `crates/ailang-check/src/builtins.rs` calls `synth(...)`
/// directly on a hand-built `Term::Match`, bypassing desugar; it
/// passes today but does not protect the property the spec
/// promises. The desugar pass `build_eq` rewrites
/// `Pattern::Lit { lit }` arms (including `Literal::Float`) into
/// `Term::If { cond: (== scrutinee lit), .. }` *before* typecheck
/// runs (see `crates/ailang-core/src/desugar.rs:1056`), so the
/// `Pattern::Lit { lit: Literal::Float { .. } }` arm at
/// `lib.rs:2316` is unreachable on input that flows through
/// `check`/`check_module`/`check_workspace`. This test exercises
/// the full pipeline and pins the Float-pattern hard-reject as
/// a property of the public check API.
#[test]
fn check_rejects_float_pattern_through_full_pipeline() {
// fn classify : (Float) -> Int = \x. match x { 0.0 -> 1; _ -> 0 }
let bits = 0.0_f64.to_bits();
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"classify",
Type::Fn {
params: vec![Type::float()],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["x"],
Term::Match {
scrutinee: Box::new(Term::Var { name: "x".into() }),
arms: vec![
Arm {
pat: Pattern::Lit {
lit: Literal::Float { bits },
},
body: Term::Lit { lit: Literal::Int { value: 1 } },
},
Arm {
pat: Pattern::Wild,
body: Term::Lit { lit: Literal::Int { value: 0 } },
},
],
},
)],
};
let err = check(&m).expect_err(
"Pattern::Lit { Literal::Float } must be rejected at typecheck",
);
assert!(
matches!(err, CheckError::FloatPatternNotAllowed),
"expected CheckError::FloatPatternNotAllowed, got {err:?}"
);
}
/// Canonical-type-pattern lookup: a `Pattern::Ctor` against a scrutinee of type
/// `Type::Con { name: "p.T", .. }` looks up the TypeDef in
/// `env.module_types["p"]["T"]` and finds the ctor by name within
/// it — no `env.ctor_index` consult, no imports-walk. This pins the
/// new lookup strategy.
#[test]
fn ct2_pattern_ctor_type_driven_lookup_cross_module() {
let lib = Module {
schema: SCHEMA.into(),
name: "lib".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Type(TypeDef {
name: "Box".into(),
vars: vec!["a".into()],
ctors: vec![Ctor {
name: "MkBox".into(),
fields: vec![Type::Var { name: "a".into() }],
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
})],
};
let consumer = Module {
schema: SCHEMA.into(),
name: "use_lib".into(),
kernel: false,
imports: vec![Import { module: "lib".into(), alias: None }],
defs: vec![fn_def(
"open",
Type::Fn {
params: vec![Type::Con {
name: "lib.Box".into(),
args: vec![Type::int()],
}],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["b"],
Term::Match {
scrutinee: Box::new(Term::Var { name: "b".into() }),
arms: vec![Arm {
pat: Pattern::Ctor {
ctor: "MkBox".into(),
fields: vec![Pattern::Var { name: "x".into() }],
},
body: Term::Var { name: "x".into() },
}],
},
)],
};
let mut modules = BTreeMap::new();
modules.insert("lib".into(), lib);
modules.insert("use_lib".into(), consumer);
let ws = Workspace {
entry: "use_lib".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(diags.is_empty(), "expected green; got {diags:?}");
}
/// Canonical-type-pattern lookup: when the scrutinee carries a Type::Con name that
/// doesn't resolve to any TypeDef (workspace-wide), the pattern
/// lookup must fail closed. The post-canonical-type-form validator catches this
/// shape earlier for canonical inputs; this test pins the residual
/// runtime guard against constructed (non-loaded) AST.
#[test]
fn ct2_pattern_ctor_fails_closed_when_scrutinee_type_unknown() {
let consumer = Module {
schema: SCHEMA.into(),
name: "u".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"f",
Type::Fn {
params: vec![Type::Con {
name: "Nonexistent".into(),
args: vec![],
}],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["x"],
Term::Match {
scrutinee: Box::new(Term::Var { name: "x".into() }),
arms: vec![Arm {
pat: Pattern::Ctor {
ctor: "Whatever".into(),
fields: vec![],
},
body: Term::Lit { lit: Literal::Int { value: 0 } },
}],
},
)],
};
let mut modules = BTreeMap::new();
modules.insert("u".into(), consumer);
let ws = Workspace {
entry: "u".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
!diags.is_empty(),
"expected at least one diagnostic for unknown scrutinee \
type, got none"
);
}
/// prep.1 (kernel-extension-mechanics): a bare `Term::Ctor.type_name`
/// that does not resolve to a local TypeDef AND does not resolve
/// via the workspace-wide TypeDef-first ladder must error with
/// `UnknownType`. Pre-prep.1 a bare cross-module ref was always
/// rejected at this site; post-prep.1 it is *accepted* when an
/// imported module declares the type (covered by
/// `ct2_term_ctor_bare_cross_module_via_workspace_resolves`).
/// This test uses a name (`Widget`) no module declares so the
/// runtime guard still fires.
#[test]
fn ct2_term_ctor_bare_cross_module_fails_closed() {
let consumer = Module {
schema: SCHEMA.into(),
name: "u".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"stale",
Type::Fn {
params: vec![],
ret: Box::new(Type::Con {
name: "Widget".into(),
args: vec![],
}),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::Ctor {
type_name: "Widget".into(),
ctor: "Mk".into(),
args: vec![],
},
)],
};
let mut modules = BTreeMap::new();
modules.insert("u".into(), consumer);
let ws = Workspace {
entry: "u".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.iter().any(|d| d.code == "unknown-type"),
"expected unknown-type diagnostic for bare cross-module \
Term::Ctor (no module declares Widget); got {diags:?}"
);
}
/// prep.1 (kernel-extension-mechanics): a bare `Term::Ctor.type_name`
/// resolves via the workspace-wide TypeDef-first ladder when an
/// imported module declares the type. Companion to
/// `ct2_term_ctor_bare_cross_module_fails_closed` (the negative
/// shape).
#[test]
fn ct2_term_ctor_bare_cross_module_via_workspace_resolves() {
let owner = Module {
schema: SCHEMA.into(),
name: "p".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Type(TypeDef {
name: "Ordering".into(),
vars: vec![],
ctors: vec![
Ctor { name: "LT".into(), fields: vec![] },
Ctor { name: "EQ".into(), fields: vec![] },
Ctor { name: "GT".into(), fields: vec![] },
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
})],
};
let consumer = Module {
schema: SCHEMA.into(),
name: "u".into(),
kernel: false,
imports: vec![Import { module: "p".into(), alias: None }],
defs: vec![fn_def(
"f",
Type::Fn {
params: vec![],
ret: Box::new(Type::Con {
name: "p.Ordering".into(),
args: vec![],
}),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::Ctor {
type_name: "Ordering".into(),
ctor: "LT".into(),
args: vec![],
},
)],
};
let mut modules = BTreeMap::new();
modules.insert("p".into(), owner);
modules.insert("u".into(), consumer);
let ws = Workspace {
entry: "u".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.is_empty(),
"bare `Ordering` in Term::Ctor must resolve via workspace TypeDef-first ladder; got {diags:?}"
);
}
/// Canonical-type-lookup: a qualified `Term::Ctor.type_name`
/// (`p.Ordering` / `LT`) continues to resolve cleanly through the
/// qualified branch. This is the canonical form post-canonical-type-form and the
/// hot path for every Term::Ctor in a migrated fixture.
#[test]
fn ct2_term_ctor_qualified_cross_module_resolves() {
let prelude = Module {
schema: SCHEMA.into(),
name: "p".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Type(TypeDef {
name: "Ordering".into(),
vars: vec![],
ctors: vec![
Ctor { name: "LT".into(), fields: vec![] },
Ctor { name: "EQ".into(), fields: vec![] },
Ctor { name: "GT".into(), fields: vec![] },
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
})],
};
let consumer = Module {
schema: SCHEMA.into(),
name: "u".into(),
kernel: false,
imports: vec![Import { module: "p".into(), alias: None }],
defs: vec![fn_def(
"lt",
Type::Fn {
params: vec![],
ret: Box::new(Type::Con {
name: "p.Ordering".into(),
args: vec![],
}),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::Ctor {
type_name: "p.Ordering".into(),
ctor: "LT".into(),
args: vec![],
},
)],
};
let mut modules = BTreeMap::new();
modules.insert("p".into(), prelude);
modules.insert("u".into(), consumer);
let ws = Workspace {
entry: "u".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(diags.is_empty(), "expected green; got {diags:?}");
}
/// bare-name resolution falls through to free
/// fns of implicitly-imported modules. The consumer calls bare `dbl`,
/// declared in `prelude` (the singleton implicit import today). The
/// pre-fix behaviour is `unbound-var` because the `Term::Var` lookup
/// ladder consults locals → local globals → class_methods →
/// dot-qualified, but never the flat free-fn tables of implicit
/// imports.
#[test]
fn bare_name_resolves_through_implicit_import_to_free_fn() {
let prelude = Module {
schema: SCHEMA.into(),
name: "prelude".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"dbl",
Type::Fn {
params: vec![Type::int()],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec!["n"],
Term::Var { name: "n".into() },
)],
};
let consumer = Module {
schema: SCHEMA.into(),
name: "m".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"main",
Type::Fn {
params: vec![],
ret: Box::new(Type::int()),
effects: vec![],
param_modes: vec![],
ret_mode: ParamMode::Implicit,
},
vec![],
Term::App {
callee: Box::new(Term::Var { name: "dbl".into() }),
args: vec![Term::Lit { lit: Literal::Int { value: 5 } }],
tail: false,
},
)],
};
let mut modules = BTreeMap::new();
modules.insert("prelude".into(), prelude);
modules.insert("m".into(), consumer);
let ws = Workspace {
entry: "m".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.is_empty(),
"expected bare `dbl` to resolve through implicit prelude import; got {diags:?}"
);
}
/// `AmbiguousMethodResolution` is the new check-time
/// diagnostic for multi-candidate residuals that survive type-driven
/// filtering at a monomorphic call site. Verifies the variant is
/// constructible, its `code()` returns the structured-diagnostic key,
/// and the Display surface names the candidate classes.
#[test]
fn mq2_ambiguous_method_resolution_display_and_code() {
let err = CheckError::AmbiguousMethodResolution {
method: "show".to_string(),
at_type: "Int".to_string(),
candidate_classes: vec![
"prelude.Show".to_string(),
"userlib.Show".to_string(),
],
};
assert_eq!(err.code(), "ambiguous-method-resolution");
let rendered = format!("{}", err);
assert!(rendered.contains("show"), "Display must echo method, got: {rendered}");
assert!(rendered.contains("prelude.Show"), "Display must name candidate, got: {rendered}");
assert!(rendered.contains("userlib.Show"), "Display must name candidate, got: {rendered}");
}
/// `UnknownClass` is the new check-time diagnostic for an
/// explicit class qualifier in `Term::Var.name` that names a
/// qualified class not in the workspace.
#[test]
fn mq2_unknown_class_display_and_code() {
let err = CheckError::UnknownClass {
name: "unknownlib.Show".to_string(),
};
assert_eq!(err.code(), "unknown-class");
let rendered = format!("{}", err);
assert!(rendered.contains("unknownlib.Show"), "Display must echo the qualified name, got: {rendered}");
}
/// `NoInstance` carries an additive `candidate_classes`
/// list. When non-empty, the rendered ctx() carries the candidate
/// list; when empty, the ctx() shape is unchanged from pre-canonical-class-form
/// form (backwards compatible for single-class call sites).
#[test]
fn mq2_no_instance_with_candidate_classes_renders() {
let err = CheckError::NoInstance {
def: "f".to_string(),
class: "prelude.Show".to_string(),
method: "show".to_string(),
at_type: "MyType".to_string(),
candidate_classes: vec![
"prelude.Show".to_string(),
"userlib.Show".to_string(),
],
};
let rendered = format!("{}", err);
assert!(rendered.contains("show"), "Display must echo method, got: {rendered}");
assert!(rendered.contains("MyType"), "Display must echo type, got: {rendered}");
let ctx = err.ctx();
assert_eq!(ctx["candidate_classes"][0], "prelude.Show");
assert_eq!(ctx["candidate_classes"][1], "userlib.Show");
}
/// empty `candidate_classes` keeps the existing single-class
/// ctx() shape — no `candidate_classes` key in the JSON.
#[test]
fn mq2_no_instance_empty_candidates_back_compat() {
let err = CheckError::NoInstance {
def: "f".to_string(),
class: "prelude.Show".to_string(),
method: "show".to_string(),
at_type: "MyType".to_string(),
candidate_classes: vec![],
};
let rendered = format!("{}", err);
assert!(rendered.contains("prelude.Show"), "Display must echo class, got: {rendered}");
let ctx = err.ctx();
assert!(ctx.get("candidate_classes").is_none(),
"empty candidate_classes must not render in ctx; got: {ctx}");
}
/// `ResidualConstraint` carries an optional candidate-class
/// set for the multi-candidate dispatch path. `None` preserves the
/// pre-canonical-class-form single-class semantics (the `class` field is the
/// resolved class). `Some(...)` carries the candidate set; the
/// `class` field's content is a tentative value until discharge
/// resolves it.
#[test]
fn mq2_residual_constraint_candidates_field_exists() {
let single = ResidualConstraint {
class: "prelude.Eq".to_string(),
type_: Type::Con { name: "Int".to_string(), args: vec![] },
method: "eq".to_string(),
candidates: None,
};
assert!(single.candidates.is_none());
let mut multi_set = std::collections::BTreeSet::new();
multi_set.insert("prelude.Show".to_string());
multi_set.insert("userlib.Show".to_string());
let multi = ResidualConstraint {
class: "prelude.Show".to_string(),
type_: Type::Con { name: "Int".to_string(), args: vec![] },
method: "show".to_string(),
candidates: Some(multi_set.clone()),
};
assert_eq!(multi.candidates, Some(multi_set));
}
/// smoke test on `parse_method_qualifier` — the helper
/// underpinning the rewritten synth Var-arm. Bare names pass
/// through with `None` qualifier; dotted names split at the last
/// dot so the prefix is the (possibly-multi-dot) class qualifier.
#[test]
fn mq2_parse_method_qualifier_smoke() {
assert_eq!(parse_method_qualifier("show"), ("show", None));
assert_eq!(
parse_method_qualifier("prelude.Show.show"),
("show", Some("prelude.Show".to_string()))
);
assert_eq!(
parse_method_qualifier("std_list.length"),
("length", Some("std_list".to_string()))
);
}
/// a multi-candidate residual with a concrete `type_`
/// resolved post-unification to `Int` is filtered against the
/// registry. Single survivor → Resolved.
#[test]
fn mq2_discharge_multi_candidate_concrete_type_single_survivor() {
let mut candidates = BTreeSet::new();
candidates.insert("prelude.Show".to_string());
candidates.insert("userlib.Show".to_string());
let residual = ResidualConstraint {
class: "prelude.Show".to_string(), // tentative
type_: Type::Con { name: "Int".to_string(), args: vec![] },
method: "show".to_string(),
candidates: Some(candidates),
};
let mut registry: BTreeMap<(String, String), ()> = BTreeMap::new();
let int_h = ailang_core::canonical::type_hash(
&Type::Con { name: "Int".to_string(), args: vec![] }
);
registry.insert(("prelude.Show".to_string(), int_h), ());
let outcome = refine_multi_candidate_residual(
&residual,
/*declared_constraints*/ &[],
/*registry*/ &registry,
);
assert_eq!(outcome, RefineOutcome::Resolved("prelude.Show".to_string()));
}
/// zero registry survivors → NoInstance with the full
/// candidate-class set echoed back to the author.
#[test]
fn mq2_discharge_multi_candidate_concrete_type_zero_survivors_no_instance() {
let mut candidates = BTreeSet::new();
candidates.insert("prelude.Show".to_string());
candidates.insert("userlib.Show".to_string());
let residual = ResidualConstraint {
class: "prelude.Show".to_string(),
type_: Type::Con { name: "MyType".to_string(), args: vec![] },
method: "show".to_string(),
candidates: Some(candidates.clone()),
};
let registry: BTreeMap<(String, String), ()> = BTreeMap::new();
let outcome = refine_multi_candidate_residual(&residual, &[], &registry);
match outcome {
RefineOutcome::NoInstance { candidate_classes, .. } => {
assert_eq!(candidate_classes.len(), 2);
}
other => panic!("expected NoInstance, got {other:?}"),
}
}
/// multi survivors → AmbiguousMethodResolution.
#[test]
fn mq2_discharge_multi_candidate_concrete_type_multi_survivors_ambiguous() {
let mut candidates = BTreeSet::new();
candidates.insert("prelude.Show".to_string());
candidates.insert("userlib.Show".to_string());
let residual = ResidualConstraint {
class: "prelude.Show".to_string(),
type_: Type::Con { name: "Int".to_string(), args: vec![] },
method: "show".to_string(),
candidates: Some(candidates.clone()),
};
let mut registry: BTreeMap<(String, String), ()> = BTreeMap::new();
let int_h = ailang_core::canonical::type_hash(
&Type::Con { name: "Int".to_string(), args: vec![] }
);
registry.insert(("prelude.Show".to_string(), int_h.clone()), ());
registry.insert(("userlib.Show".to_string(), int_h), ());
let outcome = refine_multi_candidate_residual(&residual, &[], &registry);
match outcome {
RefineOutcome::Ambiguous { candidate_classes, .. } => {
assert_eq!(candidate_classes.len(), 2);
}
other => panic!("expected Ambiguous, got {other:?}"),
}
}
/// `Env` carries a workspace-flat
/// `method_to_candidate_classes: BTreeMap<String, BTreeSet<String>>`
/// inverse map of `class_methods`. Today's `MethodNameCollision`
/// invariant guarantees each set is singleton; post-canonical-class-form the
/// cardinality > 1 case becomes legal.
#[test]
fn mq2_env_method_to_candidate_classes_built() {
use ailang_core::ast::{ClassDef, ClassMethod, Module};
let m = Module {
schema: SCHEMA.into(),
name: "m".to_string(),
kernel: false,
imports: vec![],
defs: vec![Def::Class(ClassDef {
name: "MyShow".to_string(),
param: "a".to_string(),
superclass: None,
methods: vec![ClassMethod {
name: "myshow".to_string(),
ty: Type::Fn {
params: vec![Type::Var { name: "a".to_string() }],
param_modes: vec![ParamMode::Borrow],
ret: Box::new(Type::Con { name: "Str".to_string(), args: vec![] }),
effects: vec![],
ret_mode: ParamMode::Implicit,
},
default: None,
}],
doc: None,
})],
};
let mut modules = BTreeMap::new();
modules.insert("m".into(), m);
let ws = Workspace {
entry: "m".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let env = build_check_env(&ws);
let candidates = env.method_to_candidate_classes.get("myshow")
.expect("method_to_candidate_classes must contain `myshow`");
assert!(candidates.contains("m.MyShow"), "candidates: {candidates:?}");
assert_eq!(candidates.len(), 1, "MethodNameCollision invariant: singleton");
}
/// `Env` carries an `active_declared_constraints` field
/// holding the active fn's POST-superclass-expansion declared
/// constraints. Empty at workspace entry; populated by `check_fn`
/// before invoking `synth` on the fn body. Consumed by `synth`'s
/// Var-arm class-method branch when calling `resolve_method_dispatch`
/// (constraint-driven filter path).
#[test]
fn mq3_env_active_declared_constraints_field_exists() {
let env = Env::default();
assert_eq!(env.active_declared_constraints.len(), 0,
"active_declared_constraints empty at default-construction");
}
/// when synth's Var-arm resolves a name to a free fn
/// (locals / caller-module-fn / implicit-import fn) AND the same
/// method name has class-method candidates in the workspace, a
/// structured warning `class-method-shadowed-by-fn` is emitted
/// via the warnings out-parameter. The fn resolution proceeds;
/// the warning surfaces the shadow so the LLM-author can
/// disambiguate via explicit class-qualified call if the shadow
/// was unintentional.
#[test]
fn mq3_class_method_shadowed_by_fn_warning_fires() {
use ailang_core::ast::{ClassDef, ClassMethod, Module};
// Synthesise a workspace with `class Show { show: a -> Str }`
// in module `clsmod` and `fn show : (Int) -> Str` in module
// `fnmod`. Module `m` imports both implicitly; `synth` on
// `Term::Var { name: "show" }` should resolve to the fn AND
// emit the shadow warning.
let clsmod = Module {
schema: SCHEMA.into(),
name: "clsmod".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Class(ClassDef {
name: "Show".into(),
param: "a".into(),
superclass: None,
methods: vec![ClassMethod {
name: "show".into(),
ty: Type::Fn {
params: vec![Type::Var { name: "a".into() }],
param_modes: vec![ParamMode::Borrow],
ret: Box::new(Type::str_()),
effects: vec![],
ret_mode: ParamMode::Implicit,
},
default: None,
}],
doc: None,
})],
};
let show_fn_ty = Type::Fn {
params: vec![Type::int()],
param_modes: vec![ParamMode::Borrow],
ret: Box::new(Type::str_()),
effects: vec![],
ret_mode: ParamMode::Implicit,
};
let fnmod = Module {
schema: SCHEMA.into(),
name: "fnmod".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "show".into(),
ty: show_fn_ty.clone(),
params: vec!["x".into()],
body: Term::Lit { lit: Literal::Str { value: "_".into() } },
doc: None,
suppress: vec![],
export: None,
})],
};
let mut modules = BTreeMap::new();
modules.insert("clsmod".into(), clsmod);
modules.insert("fnmod".into(), fnmod);
// mq.tidy T3: post-tightening, the warning fires only when at
// least one candidate class has an instance in the workspace
// registry. Ship a `clsmod.Show Int` instance so the fixture
// continues to assert positive-fire behaviour under the
// post-tidy spec rule.
let mut registry = ailang_core::workspace::Registry::default();
let int_h = ailang_core::canonical::type_hash(&Type::int());
registry.entries.insert(
("clsmod.Show".into(), int_h),
ailang_core::workspace::RegistryEntry {
instance: ailang_core::ast::InstanceDef {
class: "clsmod.Show".into(),
type_: Type::int(),
methods: vec![],
doc: None,
},
defining_module: "clsmod".into(),
},
);
let ws = Workspace {
entry: "fnmod".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry,
};
let mut env = build_check_env(&ws);
// Treat both modules as implicitly imported by `env.imports`
// (the test-only equivalent of the prelude-injection convention).
env.imports.insert("clsmod".into(), "clsmod".into());
env.imports.insert("fnmod".into(), "fnmod".into());
env.current_module = "fnmod".into();
let term = Term::Var { name: "show".into() };
let mut locals: IndexMap<String, Type> = IndexMap::new();
// loop-recur iter 2: loop-free unit-test call site — fresh
// empty loop-stack.
let mut loop_stack: Vec<Vec<(String, Type)>> = Vec::new();
let mut effects: BTreeSet<String> = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
let mut residuals: Vec<ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
let mut warnings: Vec<crate::diagnostic::Diagnostic> = Vec::new();
let _ = synth(
&term,
&env,
&mut locals,
&mut loop_stack,
&mut effects,
"test_call_site",
&mut subst,
&mut counter,
&mut residuals,
&mut free_fn_calls,
&mut warnings,
)
.expect("synth must succeed (fn wins precedence)");
assert!(
warnings.iter().any(|d| d.code == "class-method-shadowed-by-fn"),
"expected at least one class-method-shadowed-by-fn warning, got: {warnings:?}",
);
}
/// `Env.class_methods` is keyed by `(QualifiedClassName,
/// MethodName)` tuple — post-canonical-class-form the workspace can carry multiple
/// classes sharing a method name, so the key must disambiguate.
/// O(1) lookup post-dispatch via `(resolved_class, method)`.
#[test]
fn mq3_env_class_methods_tuple_keyed() {
use ailang_core::ast::{ClassDef, ClassMethod, Module};
let m = Module {
schema: SCHEMA.into(),
name: "m".to_string(),
kernel: false,
imports: vec![],
defs: vec![Def::Class(ClassDef {
name: "MyCls".to_string(),
param: "a".to_string(),
superclass: None,
methods: vec![ClassMethod {
name: "mymethod".to_string(),
ty: Type::Fn {
params: vec![Type::Var { name: "a".to_string() }],
param_modes: vec![ParamMode::Borrow],
ret: Box::new(Type::Con { name: "Str".to_string(), args: vec![] }),
effects: vec![],
ret_mode: ParamMode::Implicit,
},
default: None,
}],
doc: None,
})],
};
let mut modules = BTreeMap::new();
modules.insert("m".into(), m);
let ws = Workspace {
entry: "m".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let env = build_check_env(&ws);
let key = ("m.MyCls".to_string(), "mymethod".to_string());
assert!(env.class_methods.contains_key(&key),
"env.class_methods must contain {key:?}");
}
/// mq.tidy T1: discharge-time rigid-var refinement must filter
/// declared constraints by BOTH class-name match AND
/// type-unification with the residual's `type_` (spec
/// §"Constraint-discharge refinement" lines 130-138). Two
/// same-class declared constraints on different typevars must
/// be discriminated by the residual's actual typevar identity.
#[test]
fn mq_tidy_rigid_var_filter_uses_type_unification() {
use ailang_core::ast::Constraint;
// Candidate set: two distinct classes both named "Show".
let mut candidates = BTreeSet::new();
candidates.insert("prelude.Show".to_string());
candidates.insert("userlib.Show".to_string());
// Residual on Var "a".
let residual = ResidualConstraint {
class: "prelude.Show".to_string(),
type_: Type::Var { name: "a".to_string() },
method: "show".to_string(),
candidates: Some(candidates),
};
// Declared: prelude.Show a (matches residual type),
// userlib.Show b (does NOT match residual type).
let declared = vec![
Constraint {
class: "prelude.Show".to_string(),
type_: Type::Var { name: "a".to_string() },
},
Constraint {
class: "userlib.Show".to_string(),
type_: Type::Var { name: "b".to_string() },
},
];
let registry: BTreeMap<(String, String), ()> = BTreeMap::new();
let outcome = refine_multi_candidate_residual(&residual, &declared, &registry);
assert_eq!(
outcome,
RefineOutcome::Resolved("prelude.Show".to_string()),
"type-unification leg must drop userlib.Show because its declared type (Var b) does not match the residual type (Var a)"
);
}
/// mq.tidy T2: the synth Var-arm's class-method dispatch entry
/// gates on a qualifier-shape predicate. The predicate must
/// accept three shapes — bare-method (None), bare-class
/// PascalCase qualifier (`"Show"`), module-qualified class
/// qualifier (`"prelude.Show"`) — and reject bare-fn
/// qualifiers (`"std_list"`, lowercase, no inner dot) which
/// belong to the cross-module-fn arm.
#[test]
fn mq_tidy_bare_class_qualifier_shape_accepted() {
assert!(qualifier_is_class_shape(&None));
assert!(qualifier_is_class_shape(&Some("Show".to_string())));
assert!(qualifier_is_class_shape(&Some("prelude.Show".to_string())));
// Bare fn qualifier (lowercase, no inner dot) — NOT class-shape.
assert!(!qualifier_is_class_shape(&Some("std_list".to_string())));
}
/// mq.tidy T3: the `class-method-shadowed-by-fn` warning fires
/// only when at least one candidate class has a registry
/// instance (any type) per spec §"Class-fn collisions" 161-162.
/// Without this conservative-tightening, the warning fires
/// unconditionally on `method_to_candidate_classes` presence,
/// including class methods with zero instances anywhere.
#[test]
fn mq_tidy_shadow_warning_suppressed_when_no_instance() {
let mut method_to_candidate_classes: BTreeMap<String, BTreeSet<String>> =
BTreeMap::new();
let mut foo_cands = BTreeSet::new();
foo_cands.insert("userlib.Foo".to_string());
method_to_candidate_classes.insert("foo".to_string(), foo_cands);
// Empty registry → no candidate class has an instance → false.
let empty_registry: BTreeMap<(String, String), ()> = BTreeMap::new();
assert!(!any_candidate_class_has_instance(
&method_to_candidate_classes,
&empty_registry,
"foo",
));
// Add one instance for userlib.Foo → true.
let mut registry_with_inst: BTreeMap<(String, String), ()> = BTreeMap::new();
registry_with_inst.insert(
("userlib.Foo".to_string(), "Int_hash".to_string()),
(),
);
assert!(any_candidate_class_has_instance(
&method_to_candidate_classes,
&registry_with_inst,
"foo",
));
}
/// prep.1 (kernel-extension-mechanics): a dot-qualified `Term::Var`
/// `<TypeName>.<member>` resolves to the type's home module when
/// `<TypeName>` is a known `TypeDef` in the workspace, regardless
/// of whether the consumer module imports the home module under
/// that name. Here `Maybe.from_maybe` from `consumer` must resolve
/// to `std_maybe.from_maybe` because `Maybe` is declared in
/// `std_maybe` and `consumer` does import `std_maybe`.
#[test]
fn type_scoped_member_resolves() {
let std_maybe: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "std_maybe",
"imports": [],
"defs": [
{"kind": "type", "name": "Maybe", "vars": ["a"], "ctors": [
{"name": "Nothing", "fields": []},
{"name": "Just", "fields": [{"k": "var", "name": "a"}]}
]},
{"kind": "fn", "name": "from_maybe",
"type": {"k": "forall", "vars": ["a"], "constraints": [], "body":
{"k": "fn", "params": [{"k": "var", "name": "a"},
{"k": "con", "name": "Maybe", "args": [{"k": "var", "name": "a"}]}],
"ret": {"k": "var", "name": "a"}, "effects": []}},
"params": ["default", "m"],
"body": {"t": "var", "name": "default"}}
]
})).unwrap();
// Consumer calls `Maybe.from_maybe` with arg types qualified to
// `std_maybe.Maybe` (post-resolution the type-scoped form
// resolves to `std_maybe.from_maybe`, but the ctor arg uses
// the qualified form so the bare-cross-module-type-validator
// is satisfied independently of Task 2's widening — Task 1's
// success criterion is only that the dot-qualified Var arm
// resolves through the TypeDef-first ladder).
let consumer: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "consumer",
"imports": [{"module": "std_maybe"}],
"defs": [
{"kind": "fn", "name": "f",
"type": {"k": "fn", "params": [{"k": "con", "name": "Int"}],
"ret": {"k": "con", "name": "Int"}, "effects": []},
"params": ["x"],
"body": {"t": "app",
"fn": {"t": "var", "name": "Maybe.from_maybe"},
"args": [{"t": "var", "name": "x"},
{"t": "ctor", "type": "std_maybe.Maybe",
"ctor": "Nothing", "args": []}]}}
]
})).unwrap();
let mut modules = BTreeMap::new();
modules.insert("std_maybe".to_string(), std_maybe);
modules.insert("consumer".to_string(), consumer);
let ws = Workspace {
entry: "consumer".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.is_empty(),
"type-scoped Maybe.from_maybe must resolve cleanly, got {diags:?}"
);
}
/// prep.1 (kernel-extension-mechanics): a dot-qualified `Term::Var`
/// `<TypeName>.<member>` where `<TypeName>` is a known `TypeDef`
/// but `<member>` is not a def in the type's home module fires
/// `TypeScopedMemberNotFound`.
#[test]
fn type_scoped_member_not_found() {
let std_maybe: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "std_maybe",
"imports": [],
"defs": [
{"kind": "type", "name": "Maybe", "vars": ["a"], "ctors": [
{"name": "Nothing", "fields": []},
{"name": "Just", "fields": [{"k": "var", "name": "a"}]}
]}
]
})).unwrap();
let consumer: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "consumer",
"imports": [{"module": "std_maybe"}],
"defs": [
{"kind": "fn", "name": "f",
"type": {"k": "fn", "params": [],
"ret": {"k": "con", "name": "Int"}, "effects": []},
"params": [],
"body": {"t": "var", "name": "Maybe.bogus"}}
]
})).unwrap();
let mut modules = BTreeMap::new();
modules.insert("std_maybe".to_string(), std_maybe);
modules.insert("consumer".to_string(), consumer);
let ws = Workspace {
entry: "consumer".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.iter().any(|d| d.code == "type-scoped-member-not-found"),
"expected diagnostic code `type-scoped-member-not-found`, got {diags:?}"
);
}
/// prep.1 (kernel-extension-mechanics): a dot-qualified `Term::Var`
/// whose receiver is neither a known `TypeDef` nor an imported
/// module fires `TypeScopedReceiverNotAType`.
#[test]
fn type_scoped_receiver_not_a_type() {
let consumer: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "consumer",
"imports": [],
"defs": [
{"kind": "fn", "name": "f",
"type": {"k": "fn", "params": [],
"ret": {"k": "con", "name": "Int"}, "effects": []},
"params": [],
"body": {"t": "var", "name": "SomethingRandom.x"}}
]
})).unwrap();
let mut modules = BTreeMap::new();
modules.insert("consumer".to_string(), consumer);
let ws = Workspace {
entry: "consumer".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.iter().any(|d| d.code == "type-scoped-receiver-not-a-type"),
"expected diagnostic code `type-scoped-receiver-not-a-type`, got {diags:?}"
);
}
/// prep.2 (kernel-extension-mechanics): the spec's worked example.
/// A `(new Counter 42)` call resolves to the home module's `new`
/// def, with `Counter` declared locally and `new : (Int) -> Counter`
/// constructing a `Counter` via `(term-ctor Counter MkCounter n)`.
/// Property: synth's Term::New arm walks the resolution + arity +
/// kind checks, substitutes type-vars (none here — `new` is
/// monomorphic), and unifies each value-arg against the
/// corresponding (substituted) param type.
#[test]
fn new_resolves_via_type_scope() {
let m: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "new_demo",
"imports": [],
"defs": [
{"kind": "type", "name": "Counter", "ctors": [
{"name": "MkCounter", "fields": [{"k": "con", "name": "Int"}]}
]},
{"kind": "fn", "name": "new",
"type": {"k": "fn",
"params": [{"k": "con", "name": "Int"}],
"ret": {"k": "con", "name": "Counter"},
"effects": []},
"params": ["n"],
"body": {"t": "ctor", "type": "Counter", "ctor": "MkCounter",
"args": [{"t": "var", "name": "n"}]}},
{"kind": "fn", "name": "main",
"type": {"k": "fn", "params": [],
"ret": {"k": "con", "name": "Counter"},
"effects": []},
"params": [],
"body": {"t": "new", "type": "Counter",
"args": [
{"kind": "value", "value":
{"t": "lit", "lit": {"kind": "int", "value": 42}}}
]}}
]
})).unwrap();
let mut modules = BTreeMap::new();
modules.insert("new_demo".to_string(), m);
let ws = Workspace {
entry: "new_demo".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.is_empty(),
"(new Counter 42) must check cleanly; got {diags:?}"
);
}
/// raw-buf.4: a `(new T arg)` where T's home module declares no
/// `new` def is rejected. The Term::New desugar (raw-buf.4)
/// rewrites `(new T …)` to `(app T.new …)` *before* check, so the
/// rejection now arrives through the type-scoped resolution ladder
/// as `type-scoped-member-not-found` ("type `T` has no member
/// `new`") rather than the prep.2 `new-type-not-constructible`
/// code that synth's now-bypassed Term::New arm produced. The
/// rejection condition is identical (no constructor for T) and the
/// new diagnostic carries strictly more context (type + member +
/// home_module).
#[test]
fn new_type_not_constructible() {
let m: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "no_new",
"imports": [],
"defs": [
{"kind": "type", "name": "T", "ctors": [
{"name": "MkT", "fields": []}
]},
// No `new` def for T.
{"kind": "fn", "name": "main",
"type": {"k": "fn", "params": [],
"ret": {"k": "con", "name": "T"},
"effects": []},
"params": [],
"body": {"t": "new", "type": "T",
"args": [
{"kind": "value", "value":
{"t": "lit", "lit": {"kind": "int", "value": 42}}}
]}}
]
})).unwrap();
let mut modules = BTreeMap::new();
modules.insert("no_new".to_string(), m);
let ws = Workspace {
entry: "no_new".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.iter().any(|d| d.code == "type-scoped-member-not-found"),
"expected the desugared `(app T.new …)` to be rejected with \
`type-scoped-member-not-found` (no `new` member on T), got {diags:?}"
);
}
/// raw-buf.4: a `(new T value)` against a polymorphic
/// `new : forall a. (a) -> T a` checks cleanly — the element type
/// `a` is recovered by inference from use (here the `main` return
/// `(con T (con Int))` fixes `a = Int`). This pins the desugar's
/// type-arg-dropping design: `(new T …)` rewrites to
/// `(app T.new …)` carrying only the value args, with no NewArg
/// kind distinction surviving into check. The prep.2
/// `new-arg-kind-mismatch` diagnostic is obsoleted by this design
/// (there are no longer type-args at a `new` site to mismatch);
/// the call shape that used to trip it is now the canonical,
/// accepted form.
#[test]
fn new_arg_kind_mismatch_value_where_type() {
let m: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "kind_mismatch",
"imports": [],
"defs": [
{"kind": "type", "name": "T", "vars": ["a"], "ctors": [
{"name": "MkT", "fields": [{"k": "var", "name": "a"}]}
]},
// `new : forall a. (a) -> T a`. The new-site at `main`
// wrongly supplies a single Value-arg where the Forall
// expects one Type-arg (then a Value-arg).
{"kind": "fn", "name": "new",
"type": {"k": "forall", "vars": ["a"], "constraints": [],
"body": {"k": "fn",
"params": [{"k": "var", "name": "a"}],
"ret": {"k": "con", "name": "T",
"args": [{"k": "var", "name": "a"}]},
"effects": []}},
"params": ["x"],
"body": {"t": "ctor", "type": "T", "ctor": "MkT",
"args": [{"t": "var", "name": "x"}]}},
{"kind": "fn", "name": "main",
"type": {"k": "fn", "params": [],
"ret": {"k": "con", "name": "T",
"args": [{"k": "con", "name": "Int"}]},
"effects": []},
"params": [],
// Wrong: only one NewArg::Value supplied for a sig
// that needs 1 Type-arg + 1 Value-arg.
"body": {"t": "new", "type": "T", "args": [
{"kind": "value", "value":
{"t": "lit", "lit": {"kind": "int", "value": 42}}}
]}}
]
})).unwrap();
let mut modules = BTreeMap::new();
modules.insert("kind_mismatch".to_string(), m);
let ws = Workspace {
entry: "kind_mismatch".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.is_empty(),
"(new T 42) against `forall a. (a) -> T a` must check cleanly — \
the desugar drops type-args and `a` is inferred from use; got {diags:?}"
);
}
/// prep.3 (kernel-extension-mechanics): `param-in` enforcement
/// rejects a `Type::Con` whose positional arg's outermost
/// type-name is not in the allowed set. Property: a TypeDef
/// carrying `param-in = {"a": {"Int", "Float"}}` referenced as
/// `(con StubT (con Str))` fires `ParamNotInRestrictedSet` with
/// the right type-name, var, found, and allowed-set payload.
#[test]
fn param_in_rejects_disallowed_type() {
let m: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "k",
"defs": [
{"kind": "type", "name": "StubT", "vars": ["a"],
"ctors": [{"name": "Stub", "fields": [{"k": "var", "name": "a"}]}],
"param-in": {"a": ["Int", "Float"]}},
// Reference `(con StubT (con Str))` in a fn return
// type — well-formedness check walks the return type.
{"kind": "fn", "name": "bad",
"type": {"k": "fn", "params": [],
"ret": {"k": "con", "name": "StubT",
"args": [{"k": "con", "name": "Str"}]},
"effects": []},
"params": [],
"body": {"t": "lit", "lit": {"kind": "unit"}}}
]
})).unwrap();
let mut modules = BTreeMap::new();
modules.insert("k".to_string(), m);
let ws = Workspace {
entry: "k".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.iter().any(|d| d.code == "param-not-in-restricted-set"),
"expected diagnostic code `param-not-in-restricted-set`, got {diags:?}"
);
}
/// fieldtest B3 (raw-buf, #7): the rendered `param-not-in-restricted-set`
/// message must name the *allowed set*, not only the offending type.
/// Property per design/models/0007-kernel-extensions.md §4
/// ("ParamNotInRestrictedSet names the offending type AND the allowed
/// set"): a downstream author rejected for `(con StubT (con Str))`
/// under `param-in = {"a": {"Int", "Float"}}` must be told `Int` and
/// `Float` are the permitted choices, so the message is actionable.
#[test]
fn param_in_reject_message_names_allowed_set() {
let m: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "k",
"defs": [
{"kind": "type", "name": "StubT", "vars": ["a"],
"ctors": [{"name": "Stub", "fields": [{"k": "var", "name": "a"}]}],
"param-in": {"a": ["Int", "Float"]}},
{"kind": "fn", "name": "bad",
"type": {"k": "fn", "params": [],
"ret": {"k": "con", "name": "StubT",
"args": [{"k": "con", "name": "Str"}]},
"effects": []},
"params": [],
"body": {"t": "lit", "lit": {"kind": "unit"}}}
]
})).unwrap();
let mut modules = BTreeMap::new();
modules.insert("k".to_string(), m);
let ws = Workspace {
entry: "k".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
let d = diags
.iter()
.find(|d| d.code == "param-not-in-restricted-set")
.unwrap_or_else(|| panic!("expected param-not-in-restricted-set, got {diags:?}"));
assert!(
d.message.contains("Int") && d.message.contains("Float"),
"message must name the allowed set {{Int, Float}}, got: {:?}",
d.message
);
}
/// prep.3 (kernel-extension-mechanics): `param-in` enforcement
/// accepts a type-arg inside the allowed set. Same TypeDef as
/// the RED test, but `(con StubT (con Int))` — Int is in
/// {Int, Float}, so the check passes.
#[test]
fn param_in_accepts_allowed_type() {
let m: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "k",
"defs": [
{"kind": "type", "name": "StubT", "vars": ["a"],
"ctors": [{"name": "Stub", "fields": [{"k": "var", "name": "a"}]}],
"param-in": {"a": ["Int", "Float"]}},
{"kind": "fn", "name": "good",
"type": {"k": "fn", "params": [],
"ret": {"k": "con", "name": "StubT",
"args": [{"k": "con", "name": "Int"}]},
"effects": []},
"params": [],
"body": {"t": "lit", "lit": {"kind": "unit"}}}
]
})).unwrap();
let mut modules = BTreeMap::new();
modules.insert("k".to_string(), m);
let ws = Workspace {
entry: "k".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
!diags.iter().any(|d| d.code == "param-not-in-restricted-set"),
"expected NO param-not-in-restricted-set diagnostic, got {diags:?}"
);
}
/// Fieldtest F1 (kernel-extension-mechanics, 2026-05-28):
/// a type-scoped call `<Type>.<member>` made from inside `<Type>`'s
/// own home module must check cleanly. The receiver `value` is a
/// `Def::Fn` in the same module as `Counter`; calling it via
/// `(app Counter.value c)` is the canonical form per
/// `docs/specs/0048-kernel-extension-mechanics.md` § "Iteration
/// prep.1 — Canonical form decision", which does NOT carve out
/// same-module sites as forbidden. Today this rejects with
/// `[type-mismatch] expected kem.Counter, got Counter` because the
/// dot-qualified arm at `synth` qualifies the resolved fn's param
/// type to `<this_module>.Counter` via `qualify_local_types`, while
/// the local `Term::Ctor` synth (`Term::Ctor` arm in `synth_term`)
/// returns the bare `Counter` form for the same-module type — the
/// two halves of the resolver disagree on whether
/// `<this_module>.T` and bare `T` are the same type.
#[test]
fn type_scoped_call_in_same_module_resolves() {
// Exact shape of examples/fieldtest/kem_2b_min_repro.ail —
// local Counter ADT with a `value` projector, called from
// `main` via `(app Counter.value c)` where `c` is built by
// `(term-ctor Counter MkCounter 41)`.
let m: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "kem",
"imports": [],
"defs": [
{"kind": "type", "name": "Counter", "ctors": [
{"name": "MkCounter", "fields": [{"k": "con", "name": "Int"}]}
]},
// `value` projects a Counter to Int. Body is a
// constant — the bug is at the call site, the body
// shape is irrelevant.
{"kind": "fn", "name": "value",
"type": {"k": "fn",
"params": [{"k": "con", "name": "Counter"}],
"ret": {"k": "con", "name": "Int"},
"effects": []},
"params": ["c"],
"body": {"t": "lit", "lit": {"kind": "int", "value": 0}}},
// `main` builds a Counter locally via term-ctor and
// calls `Counter.value` on it from the same module.
// Per spec § prep.1 "Canonical form decision" this
// is the canonical form and must check.
{"kind": "fn", "name": "main",
"type": {"k": "fn", "params": [],
"ret": {"k": "con", "name": "Int"},
"effects": []},
"params": [],
"body": {"t": "let", "name": "c",
"value": {"t": "ctor", "type": "Counter",
"ctor": "MkCounter",
"args": [{"t": "lit",
"lit": {"kind": "int", "value": 41}}]},
"body": {"t": "app",
"fn": {"t": "var", "name": "Counter.value"},
"args": [{"t": "var", "name": "c"}]}}}
]
})).unwrap();
let mut modules = BTreeMap::new();
modules.insert("kem".to_string(), m);
let ws = Workspace {
entry: "kem".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.is_empty(),
"same-module type-scoped call `Counter.value c` must check \
cleanly (the canonical-form rule does not carve out \
same-module sites); got {diags:?}"
);
}
/// Fieldtest F3 (kernel-extension-mechanics, 2026-05-28):
/// a `(con StubT (con Int))` reference in a consumer's type
/// signature, where `StubT` lives in a kernel-tier module
/// (`kernel: true`) and the consumer has NO explicit
/// `(import kernel_stub)`, must check cleanly. Spec §"Iteration
/// prep.3" promises kernel-tier types are accessible bare in
/// type position. The workspace pre-pass `qualify_workspace_types`
/// rewrites bare `StubT` to qualified `kernel_stub.StubT`; the
/// type-validity check at `synth_type` (line ~1968) then rejects
/// `kernel_stub` because only `prelude` is force-injected into
/// `env.imports` / `env.module_imports` (lines 1667–1671 and
/// 1797–1800) — kernel-tier modules OTHER than prelude are not
/// added to the per-module import map, so the qualifier they
/// receive from the pre-pass is unresolvable.
#[test]
fn kernel_tier_module_qualifier_resolves_without_explicit_import() {
let kernel_stub: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "kernel_stub",
"kernel": true,
"imports": [],
"defs": [
{"kind": "type", "name": "StubT", "vars": ["a"],
"ctors": [{"name": "Stub", "fields": [{"k": "var", "name": "a"}]}]}
]
})).unwrap();
// Consumer references `StubT` bare in a type signature — no
// `(import kernel_stub)` declaration. Per spec § prep.3 the
// kernel-tier flag should make this resolve.
let consumer: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "consumer",
"imports": [],
"defs": [
// The bug fires in the type-validity check on the
// declared param type `(con StubT (con Int))` — the
// body shape is irrelevant. A trivial Int-returning
// body keeps the test focused on the qualifier-
// resolution path.
{"kind": "fn", "name": "unwrap_int",
"type": {"k": "fn",
"params": [{"k": "con", "name": "StubT",
"args": [{"k": "con", "name": "Int"}]}],
"ret": {"k": "con", "name": "Int"},
"effects": []},
"params": ["s"],
"body": {"t": "lit", "lit": {"kind": "int", "value": 0}}}
]
})).unwrap();
let mut modules = BTreeMap::new();
modules.insert("kernel_stub".to_string(), kernel_stub);
modules.insert("consumer".to_string(), consumer);
let ws = Workspace {
entry: "consumer".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.is_empty(),
"kernel-tier `StubT` referenced bare in a consumer type \
signature must resolve without an explicit \
`(import kernel_stub)` declaration; got {diags:?}"
);
}
}
Reference in New Issue View Git Blame Copy Permalink