Brummel
2e6a4ca200
Installs the dispatch infrastructure for type-driven method resolution without retiring MethodNameCollision yet. The new multi-candidate path is exercised exclusively by 15 unit tests; real workspaces continue producing single-class residuals (candidates: None) and every pre-mq.2 fixture typechecks unchanged. Three new CheckError variants: - AmbiguousMethodResolution (multi-candidate after type-driven filter) - UnknownClass (explicit qualifier names a class not in registry) - NoInstance gains additive candidate_classes field (Vec<String>) Schema/Env additions: - Env.method_to_candidate_classes: BTreeMap<String, BTreeSet<String>> workspace-flat inverse of class_methods, built in build_check_env. - ResidualConstraint.candidates: Option<BTreeSet<String>> — None preserves pre-mq.2 single-class semantics; Some(set) carries the multi-candidate residual that discharge refines. - ResidualConstraint visibility bumped pub(crate) → pub for unit-test crate access. New helpers: - MethodDispatchOutcome enum + pure resolve_method_dispatch implementing the spec's 5-step rule (qualifier → singleton → type-driven filter → constraint-driven filter → Multi for discharge-time refinement). - parse_method_qualifier splits Term::Var.name into (method_name, optional_qualifier_prefix) at the last dot. - RefineOutcome enum + refine_multi_candidate_residual for discharge-time refinement. - resolve_residual_class_for_mono wires the refinement into mono's collect_residuals_ordered residual-to-target mapping. Synth Var-arm class-method branch rewritten via parse_method_qualifier with inner-dot gate (qualifier must be <module>.<Class>; single-dot names fall through to the existing qualified-fn path). Constraint-discharge in check_fn uses expanded (post-superclass- expansion) constraints for the rigid-var path — sounder than raw declared_constraints. Plan-invented format_type_for_display replaced with the existing ailang_core::pretty::type_to_string (one less duplicate). Synth-time declared_constraints: &[] is a deliberate gap documented as known debt — load-bearing only post-mq.3 for the rigid-var fallback (env-plumbing the active fn's constraints into the Var arm is a ~10-line edit slated for mq.3). 9/9 tasks, 539 tests green (was 520 pre-mq.2; +15 mq.2 unit tests + 4 pre-existing). bench/compile_check.py + cross_lang.py clean; bench/check.py 1 regression (latency noise — runtime cannot be touched by a typecheck-side iter).
6020 lines
252 KiB
Rust
6020 lines
252 KiB
Rust
//! 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, ret, effects, .. } => Type::Fn {
|
|
params: params.iter().map(|p| substitute_rigids(p, mapping)).collect(),
|
|
ret: Box::new(substitute_rigids(ret, mapping)),
|
|
effects: effects.clone(),
|
|
param_modes: vec![],
|
|
ret_mode: ParamMode::Implicit,
|
|
},
|
|
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)),
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
/// Iter 23.4: 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)),
|
|
},
|
|
}
|
|
}
|
|
|
|
/// 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>),
|
|
|
|
/// 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-ct.2): 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 },
|
|
|
|
/// Iter 14e: 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 Decision 8.
|
|
#[error("call marked `tail` is not in tail position")]
|
|
TailCallNotInTailPosition,
|
|
|
|
/// Iter 18d.1: 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 },
|
|
|
|
/// Iter 22b.2 (Task 9): 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,
|
|
},
|
|
|
|
/// Iter 22b.2 (Task 10): 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,
|
|
/// mq.2: additive candidate-class list. Empty on residuals from
|
|
/// the single-class dispatch path (pre-mq.2 shape preserved).
|
|
/// Non-empty when the diagnostic originated from the
|
|
/// multi-candidate refinement path with zero registry survivors.
|
|
candidate_classes: Vec<String>,
|
|
},
|
|
|
|
/// mq.2: 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>,
|
|
},
|
|
|
|
/// mq.2: 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,
|
|
},
|
|
|
|
/// Iter 22b.3: 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::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::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 })
|
|
}
|
|
_ => 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);
|
|
}
|
|
// Iter 18d.1: 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(),
|
|
);
|
|
}
|
|
// Iter 23.5: Float-aware addendum on `NoInstance`. When the
|
|
// unresolved class is `Eq` or `Ord` AND the type is `Float`,
|
|
// append a cross-reference to DESIGN.md §"Float semantics" 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() {
|
|
// mq.1: `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); see DESIGN.md §\"Float semantics\".",
|
|
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> {
|
|
// Iter 16a: 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("."),
|
|
// Iter 22b.1: 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.
|
|
///
|
|
/// 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;
|
|
}
|
|
}
|
|
// Iter 16a: 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).
|
|
let ws_owned = Workspace {
|
|
entry: ws.entry.clone(),
|
|
modules: ws
|
|
.modules
|
|
.iter()
|
|
.map(|(k, m)| (k.clone(), ailang_core::desugar::desugar_module(m)))
|
|
.collect(),
|
|
root_dir: ws.root_dir.clone(),
|
|
// Iter 22b.1: pass the registry 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 desugared modules.
|
|
registry: ws.registry.clone(),
|
|
};
|
|
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];
|
|
let typecheck_errors = check_in_workspace(m, ws, &module_globals);
|
|
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());
|
|
}
|
|
// Iter 18c.2: 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 {
|
|
// Iter 23.5: 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));
|
|
// Iter 18d.2: 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));
|
|
}
|
|
// Iter 19b: 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)?;
|
|
// Iter 16a: 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("."),
|
|
// Iter 22b.1: 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`.
|
|
if let Some(first) = check_in_workspace(m, &ws, &module_globals).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![],
|
|
},
|
|
// Iter 22b.1: 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 })
|
|
}
|
|
|
|
/// Iter 16b.3: 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))
|
|
}
|
|
|
|
/// Iter 15a: 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
|
|
}
|
|
|
|
/// Iter 22b.2: 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>,
|
|
/// Class-method names, by method name. Populated in
|
|
/// [`build_module_globals`] from `Def::Class` entries; consulted by
|
|
/// the 22b.2 `missing-constraint` / `no-instance` arms (Tasks 9 / 10).
|
|
/// `IndexMap` matches the sibling [`Self::fns`] channel and preserves
|
|
/// definition order — Tasks 9 / 10 may surface diagnostics in source
|
|
/// order, and downstream consumers should not depend on a sorted
|
|
/// iteration order they did not ask for.
|
|
pub class_methods: IndexMap<String, ClassMethodEntry>,
|
|
}
|
|
|
|
impl ModuleGlobals {
|
|
/// True if `name` is a class method declared in this module.
|
|
pub fn has_class_method(&self, name: &str) -> bool {
|
|
self.class_methods.contains_key(name)
|
|
}
|
|
|
|
/// The class that declared the method `name`, or `None` if `name`
|
|
/// is not a class method in this module.
|
|
pub fn class_method_class(&self, name: &str) -> Option<&str> {
|
|
self.class_methods
|
|
.get(name)
|
|
.map(|e| e.class_name.as_str())
|
|
}
|
|
|
|
/// The full [`ClassMethodEntry`] for method `name`, or `None` if
|
|
/// `name` is not a class method in this module. Tasks 9 / 10 use
|
|
/// this to read `method_ty` and `defining_module` together; the
|
|
/// narrower `has_class_method` / `class_method_class` accessors
|
|
/// stay for callers that only need a yes/no or the class name.
|
|
pub fn class_method(&self, name: &str) -> Option<&ClassMethodEntry> {
|
|
self.class_methods.get(name)
|
|
}
|
|
}
|
|
|
|
/// Iter 22b.2: 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`).
|
|
///
|
|
/// mq.1: 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.
|
|
///
|
|
/// Iter 22b.2 (Task 8): 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();
|
|
// mq.1: 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(),
|
|
}),
|
|
));
|
|
}
|
|
// Iter 22b.2: 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) => {
|
|
// Iter 22b.2 (Task 8): 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.
|
|
//
|
|
// mq.1: 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(
|
|
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 (n, e) in &g.class_methods {
|
|
env.class_methods.insert(n.clone(), e.clone());
|
|
// mq.2: build the inverse method → candidate-class set in
|
|
// the same loop. `e.class_name` already carries the
|
|
// qualified form (mq.1 invariant), so the set is keyed on
|
|
// workspace-flat qualified class names directly.
|
|
env.method_to_candidate_classes
|
|
.entry(n.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`.
|
|
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());
|
|
}
|
|
// Iter 23.1: the prelude module is implicitly imported into
|
|
// every non-prelude module. A user-declared explicit
|
|
// `import { module: "prelude" }` would already place
|
|
// "prelude" in the map above (idempotent insert via entry).
|
|
// The prelude module itself does not import itself.
|
|
if m.name != "prelude" {
|
|
import_map
|
|
.entry("prelude".to_string())
|
|
.or_insert_with(|| "prelude".to_string());
|
|
}
|
|
env.module_imports.insert(m.name.clone(), import_map);
|
|
}
|
|
|
|
// env.class_superclasses — walk every module's Def::Class.
|
|
//
|
|
// mq.1: 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-mq.1), 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>,
|
|
) -> 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 (ct.2.2).
|
|
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());
|
|
}
|
|
// Iter 23.1: the prelude module is implicitly imported into
|
|
// every non-prelude module's body-check env. The wiring here
|
|
// populates `env.imports` (the active per-module table the
|
|
// body-check pass reads); the sibling block in `build_check_env`
|
|
// populates `env.module_imports` (the workspace-wide table
|
|
// referenced when resolving qualified names across modules).
|
|
// Both fields need the prelude-injection rule applied, and they
|
|
// are populated from different code paths — hence the apparent
|
|
// duplication. The prelude itself does not import itself.
|
|
if m.name != "prelude" {
|
|
import_map
|
|
.entry("prelude".to_string())
|
|
.or_insert_with(|| "prelude".to_string());
|
|
}
|
|
env.imports = import_map;
|
|
env.current_module = m.name.clone();
|
|
|
|
for def in &m.defs {
|
|
if let Err(e) = check_def(def, &env) {
|
|
errors.push(CheckError::Def(def.name().to_string(), Box::new(e)));
|
|
}
|
|
}
|
|
errors
|
|
}
|
|
|
|
fn check_def(def: &Def, env: &Env) -> Result<()> {
|
|
match def {
|
|
Def::Fn(f) => check_fn(f, env),
|
|
Def::Const(c) => check_const(c, env),
|
|
Def::Type(td) => check_type_def(td, env),
|
|
// Iter 22b.1: schema-only landing for class/instance defs.
|
|
// Class-schema validation (InvalidSuperclassParam,
|
|
// ConstraintReferencesUnboundTypeVar) and instance-body
|
|
// typechecking (with class-method substitution) land in 22b.2.
|
|
// ctt.3: KindMismatch retired — the malformed-class-param
|
|
// shape now fires BareCrossModuleTypeRef from the canonical-
|
|
// form validator instead.
|
|
// Workspace-load coherence checks (Orphan / Duplicate /
|
|
// MissingMethod) already fire from `workspace::build_registry`,
|
|
// so a malformed instance never reaches this point.
|
|
Def::Class(_) | Def::Instance(_) => Ok(()),
|
|
}
|
|
}
|
|
|
|
fn check_type_def(td: &TypeDef, env: &Env) -> Result<()> {
|
|
// Iter 13a: 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(());
|
|
}
|
|
// Iter 15a: a qualified type name `module.Type` resolves
|
|
// through the import map and the per-module type table. The
|
|
// bare-name path is unchanged.
|
|
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 {
|
|
env.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()
|
|
)));
|
|
}
|
|
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()))
|
|
}
|
|
}
|
|
}
|
|
|
|
fn check_fn(f: &FnDef, env: &Env) -> 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());
|
|
}
|
|
|
|
// Iter 13a: 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 ¶m_tys {
|
|
check_type_well_formed(p, &env)?;
|
|
}
|
|
check_type_well_formed(&ret_ty, &env)?;
|
|
|
|
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 body_ty = synth(&f.body, &env, &mut locals, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls)?;
|
|
unify(&ret_ty, &body_ty, &mut subst)?;
|
|
|
|
// Iter 14e: tail-position verification (Decision 8). 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)?;
|
|
|
|
let declared: BTreeSet<String> = declared_effs.into_iter().collect();
|
|
for e in &effects {
|
|
if !declared.contains(e) {
|
|
return Err(CheckError::UndeclaredEffect(e.clone()));
|
|
}
|
|
}
|
|
|
|
// Iter 22b.2 (Task 9): missing-constraint check. Build the expanded
|
|
// declared-constraint set (declared + one-step superclass per
|
|
// Decision 11) and compare against residuals. Var-shaped residuals
|
|
// not covered by the expanded set fire `MissingConstraint`. Concrete
|
|
// residuals are deferred to Task 10's `no-instance` arm.
|
|
//
|
|
// mq.1: 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 comparing
|
|
// against residuals — residuals always carry qualified `class`
|
|
// because they come from `ClassMethodEntry.class_name` which is
|
|
// qualified post-mq.1.
|
|
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(),
|
|
};
|
|
let expanded = expand_declared_constraints(&declared_constraints, &env.class_superclasses);
|
|
for r in &residuals {
|
|
let r_ty = subst.apply(&r.type_);
|
|
|
|
// mq.2: 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 mq.3.
|
|
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,
|
|
®istry_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) {
|
|
// Iter 22b.2 (Task 10): 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 (Decision 11).
|
|
}
|
|
Ok(())
|
|
}
|
|
|
|
/// Iter 22b.2 (Task 10): 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),
|
|
}
|
|
}
|
|
|
|
/// Iter 22b.2 (Task 9): 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,
|
|
/// mq.2: candidate-class set for the multi-candidate dispatch
|
|
/// path. `None` ⇒ single-class semantics (pre-mq.2 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-mq.3), real workspaces only ever construct `None`-candidate
|
|
/// residuals; the `Some`-path is exercised exclusively by unit
|
|
/// tests until mq.3 retires the workaround.
|
|
pub candidates: Option<BTreeSet<String>>,
|
|
}
|
|
|
|
/// mq.2: 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>,
|
|
},
|
|
}
|
|
|
|
/// mq.2: 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-mq.3
|
|
// path. Returns immediately so the post-mq.3 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(),
|
|
}
|
|
}
|
|
|
|
/// mq.2: 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>,
|
|
},
|
|
}
|
|
|
|
/// mq.2: 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-mq.2.
|
|
///
|
|
/// 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.
|
|
let survivors: Vec<String> = candidates
|
|
.iter()
|
|
.filter(|c| declared_constraints.iter().any(|dc| &dc.class == *c))
|
|
.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(),
|
|
},
|
|
}
|
|
}
|
|
|
|
/// Iter 23.4: 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>,
|
|
}
|
|
|
|
/// mq.1: 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}")
|
|
}
|
|
}
|
|
|
|
/// mq.2: 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"))`
|
|
/// - `"std_list.length"` → `("length", Some("std_list"))`
|
|
///
|
|
/// Callers gate on the qualifier shape: a class qualifier is always
|
|
/// qualified per mq.1's canonical-form rule, so a single-segment
|
|
/// prefix (no dot) is structurally a module name and the caller falls
|
|
/// through to the cross-module-fn path. A multi-segment prefix
|
|
/// (`<module>.<Class>`) signals an explicit class qualifier on a
|
|
/// class-method call site.
|
|
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)
|
|
}
|
|
}
|
|
|
|
/// Iter 22b.2 (Task 9): expand a list of declared class constraints
|
|
/// with their one-step superclass closure (Decision 11). For every
|
|
/// declared `(C, t)`, append `(S, t)` if class `C` has a superclass
|
|
/// `S`. Only one step — Decision 11 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
|
|
}
|
|
|
|
/// Iter 22b.2 (Task 9): 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,
|
|
}
|
|
}
|
|
|
|
/// Iter 14e: verifies that every `Term::App { tail: true, .. }` and
|
|
/// `Term::Do { tail: true, .. }` actually sits in tail position, per
|
|
/// Decision 8.
|
|
///
|
|
/// `is_tail` is the tail-context flag for the term currently being
|
|
/// visited. The propagation rules (from DESIGN.md Decision 8):
|
|
///
|
|
/// - 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, .. } => {
|
|
// Iter 16b.3: `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 } => {
|
|
// Iter 18c.1: 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 } => {
|
|
// Iter 18d.1: 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)
|
|
}
|
|
}
|
|
}
|
|
|
|
fn check_const(c: &ConstDef, env: &Env) -> 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;
|
|
// Iter 22b.2 (Task 9): 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 v = synth(&c.value, env, &mut locals, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls)?;
|
|
unify(&c.ty, &v, &mut subst)?;
|
|
if !effects.is_empty() {
|
|
return Err(CheckError::ConstHasEffects(
|
|
c.name.clone(),
|
|
effects.into_iter().collect(),
|
|
));
|
|
}
|
|
Ok(())
|
|
}
|
|
|
|
pub(crate) fn synth(
|
|
t: &Term,
|
|
env: &Env,
|
|
locals: &mut IndexMap<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>,
|
|
) -> 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.
|
|
//
|
|
// Iter 22b.2 (Task 9): 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`.
|
|
// Iter 23.4: 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
|
|
// `std_list.length`, 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.
|
|
let (raw, free_fn_owner): (Type, Option<(String, String)>) = if let Some(t) = locals.get(name) {
|
|
(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()));
|
|
(t.clone(), owner)
|
|
} else if {
|
|
// mq.2 dispatch entry: the Var arm matches a class
|
|
// method either bare (`"show"`) or qualified
|
|
// (`"prelude.Show.show"`). `parse_method_qualifier`
|
|
// splits at the last dot; a `Some(qualifier)` with no
|
|
// inner dot is a 1-dot name (`std_list.length`) —
|
|
// structurally a cross-module-fn call per mq.1's
|
|
// canonical-form rule (class qualifiers are always
|
|
// `<module>.<Class>`), so we fall through to the
|
|
// qualified-fn arm below in that case.
|
|
let (method_name, qualifier_opt) = parse_method_qualifier(name);
|
|
let qualifier_is_class_shape = match &qualifier_opt {
|
|
None => true,
|
|
Some(q) => q.contains('.'),
|
|
};
|
|
qualifier_is_class_shape
|
|
&& env.method_to_candidate_classes.contains_key(method_name)
|
|
} {
|
|
// mq.2: 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-mq.3),
|
|
// real workspaces never reach the `Multi` branch — the
|
|
// candidate set is always singleton. The branch is
|
|
// installed here for mq.3 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*/ &[],
|
|
/*registry*/ ®istry_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,
|
|
});
|
|
}
|
|
};
|
|
|
|
// Look up the `ClassMethodEntry` by method name —
|
|
// workspace-flat. The `MethodNameCollision` invariant
|
|
// (pre-mq.3) guarantees the lookup is unambiguous. Post-
|
|
// mq.3, the class_methods table is keyed by
|
|
// `(class, method)` and this `.get(method_name)` will
|
|
// need to be reworked alongside the table.
|
|
let cm = env.class_methods.get(method_name).expect(
|
|
"method_to_candidate_classes invariant: 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 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())))
|
|
})
|
|
{
|
|
// Iter 23.4-prep: 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 at this file's
|
|
// ~1170 / ~1285), 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.
|
|
//
|
|
// 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())))
|
|
} else if name.matches('.').count() == 1 {
|
|
let (prefix, suffix) = 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 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(|| {
|
|
CheckError::UnknownImport {
|
|
module: target_module.clone(),
|
|
name: suffix.to_string(),
|
|
}
|
|
})?;
|
|
// Iter 15a: 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.
|
|
let owner_types = env
|
|
.module_types
|
|
.get(&target_module)
|
|
.cloned()
|
|
.unwrap_or_default();
|
|
let qualified = qualify_local_types(&raw_ty, &target_module, &owner_types);
|
|
// Dot-qualified `prefix.suffix`: the unqualified name in
|
|
// the owner module is `suffix`.
|
|
(qualified, Some((target_module, suffix.to_string())))
|
|
} else {
|
|
return Err(CheckError::UnknownIdent(name.clone()));
|
|
};
|
|
// Iter 23.4: 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))) =
|
|
(&raw, &free_fn_owner)
|
|
{
|
|
let (metas, inst) = instantiate(vars, body, counter);
|
|
free_fn_calls.push(FreeFnCall {
|
|
name: unqualified_name.clone(),
|
|
owner_module: owner.clone(),
|
|
forall_vars: vars.clone(),
|
|
metas: metas.clone(),
|
|
});
|
|
return Ok(inst);
|
|
}
|
|
Ok(maybe_instantiate(raw, counter))
|
|
}
|
|
Term::App { callee, args, .. } => {
|
|
let cty = synth(callee, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
|
|
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, effects, in_def, subst, counter, residuals, free_fn_calls)?;
|
|
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, effects, in_def, subst, counter, residuals, free_fn_calls)?;
|
|
let prev = locals.insert(name.clone(), v);
|
|
let r = synth(body, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
|
|
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, effects, in_def, subst, counter, residuals, free_fn_calls)?;
|
|
unify(&Type::bool_(), &c, subst)?;
|
|
let t1 = synth(then, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
|
|
let t2 = synth(else_, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)?;
|
|
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, effects, in_def, subst, counter, residuals, free_fn_calls)?;
|
|
unify(exp, &actual, subst)?;
|
|
}
|
|
effects.insert(sig.effect.clone());
|
|
Ok(sig.ret)
|
|
}
|
|
Term::Ctor { type_name, ctor, args } => {
|
|
// ct.2 Task 3: Term::Ctor lookup is direct post-ct.1.
|
|
// Canonical type_name: bare = local TypeDef, qualified =
|
|
// explicit cross-module. The imports-fallback (iter
|
|
// 23.1.3) is gone — bare cross-module refs are rejected
|
|
// upstream by the workspace validator (ct.1).
|
|
//
|
|
// Iter 15b: 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 = type_name.clone();
|
|
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);
|
|
td
|
|
} else if let Some(td) = env.types.get(type_name) {
|
|
owning_module = None;
|
|
td.clone()
|
|
} 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(),
|
|
});
|
|
}
|
|
// Iter 15b: 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(),
|
|
};
|
|
// Iter 13a: 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, effects, in_def, subst, counter, residuals, free_fn_calls)?;
|
|
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, effects, in_def, subst, counter, residuals, free_fn_calls)?;
|
|
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, effects, in_def, subst, counter, residuals, free_fn_calls)?;
|
|
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 {
|
|
// Iter 15a: 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, effects, in_def, subst, counter, residuals, free_fn_calls)?;
|
|
unify(&Type::unit(), <y, subst)?;
|
|
synth(rhs, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls)
|
|
}
|
|
Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => {
|
|
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, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls);
|
|
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 } => {
|
|
// Iter 16b.3: 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 ¶m_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, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls);
|
|
|
|
// 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, effects, in_def, subst, counter, residuals, free_fn_calls);
|
|
match prev_in {
|
|
Some(p) => {
|
|
locals.insert(name.clone(), p);
|
|
}
|
|
None => {
|
|
locals.shift_remove(name);
|
|
}
|
|
}
|
|
in_ty
|
|
}
|
|
Term::Clone { value } => {
|
|
// Iter 18c.1: `(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, effects, in_def, subst, counter, residuals, free_fn_calls)
|
|
}
|
|
Term::ReuseAs { source, body } => {
|
|
// Iter 18d.1: `(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, effects, in_def, subst, counter, residuals, free_fn_calls)?;
|
|
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::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, effects, in_def, subst, counter, residuals, free_fn_calls)
|
|
}
|
|
}
|
|
}
|
|
|
|
/// 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
|
|
}
|
|
}
|
|
|
|
/// Iter 15a: 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 } => {
|
|
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(),
|
|
}
|
|
}
|
|
|
|
/// 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, <)?;
|
|
Ok(vec![])
|
|
}
|
|
Pattern::Ctor { ctor, fields } => {
|
|
// Iter 16a: 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"
|
|
);
|
|
}
|
|
}
|
|
}
|
|
// ct.2 Task 2: Pattern::Ctor lookup is type-driven post-ct.1.
|
|
// 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(),
|
|
});
|
|
}
|
|
// Iter 13a: 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`).
|
|
//
|
|
// Iter 15b: 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>>,
|
|
/// Iter 15a: 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,
|
|
/// 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>,
|
|
/// Iter 22b.2 (Task 9): workspace-wide class-method table. Merged
|
|
/// from every module's [`ModuleGlobals::class_methods`] so that a
|
|
/// `Term::Var { name: "show" }` in any module resolves to the
|
|
/// declaring class's [`ClassMethodEntry`]. Method-name uniqueness
|
|
/// is enforced earlier by `workspace::build_registry`'s
|
|
/// method-name-collision check (Iter 22b.2.6), so the merge is
|
|
/// safe (no overwrites). Read in [`synth`]'s `Term::Var` arm.
|
|
pub class_methods: BTreeMap<String, ClassMethodEntry>,
|
|
/// mq.2: workspace-flat inverse of [`Self::class_methods`] — for
|
|
/// each method name, the set of qualified class names that declare
|
|
/// it. Pre-mq.3, the `MethodNameCollision` invariant guarantees
|
|
/// each set is singleton; mq.3 lifts the invariant and cardinality
|
|
/// > 1 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>>,
|
|
/// Iter 22b.2 (Task 9): 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
|
|
/// (Decision 11: max one step). The schema permits at most one
|
|
/// superclass per class.
|
|
pub class_superclasses: BTreeMap<String, String>,
|
|
/// Iter 22b.2 (Task 10): 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;
|
|
|
|
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,
|
|
})
|
|
}
|
|
|
|
#[test]
|
|
fn checks_simple_arithmetic_fn() {
|
|
let m = Module {
|
|
schema: SCHEMA.into(),
|
|
name: "t".into(),
|
|
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(),
|
|
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(),
|
|
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_int".into(),
|
|
args: vec![Term::Lit {
|
|
lit: Literal::Int { value: 1 },
|
|
}],
|
|
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(),
|
|
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(),
|
|
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,
|
|
}),
|
|
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(),
|
|
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,
|
|
}),
|
|
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(),
|
|
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"));
|
|
}
|
|
|
|
/// Iter 12a: 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(),
|
|
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");
|
|
}
|
|
|
|
/// Iter 12a: `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(),
|
|
imports: vec![],
|
|
defs: vec![id_def, use_int, use_bool],
|
|
};
|
|
check(&m).expect("two distinct id instantiations should typecheck");
|
|
}
|
|
|
|
/// Iter 12a: 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(),
|
|
imports: vec![],
|
|
defs: vec![id_def, bad],
|
|
};
|
|
let err = check(&m).unwrap_err();
|
|
let msg = format!("{err}");
|
|
assert!(msg.contains("type mismatch"), "got: {msg}");
|
|
}
|
|
|
|
/// Iter 12a: 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(),
|
|
imports: vec![],
|
|
defs: vec![apply_def, succ, use_apply],
|
|
};
|
|
check(&m).expect("apply instantiation should typecheck");
|
|
}
|
|
|
|
/// Iter 13a: 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,
|
|
});
|
|
// 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(),
|
|
imports: vec![],
|
|
defs: vec![box_def, make],
|
|
};
|
|
check(&m).expect("Box<Int> ctor should typecheck");
|
|
}
|
|
|
|
/// Iter 13a: 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,
|
|
});
|
|
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,
|
|
});
|
|
// 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(),
|
|
imports: vec![],
|
|
defs: vec![box_def, unbox, use_int, use_bool],
|
|
};
|
|
check(&m).expect("polymorphic Box should typecheck at both instantiations");
|
|
}
|
|
|
|
/// Iter 13a: 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,
|
|
});
|
|
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(),
|
|
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}");
|
|
}
|
|
|
|
/// Iter 10: `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(),
|
|
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}");
|
|
}
|
|
|
|
/// Iter 14e: 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(),
|
|
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,
|
|
}),
|
|
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(),
|
|
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,
|
|
})],
|
|
};
|
|
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(),
|
|
}
|
|
}
|
|
|
|
/// Iter 15a, path 1: 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(),
|
|
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:?}");
|
|
}
|
|
|
|
/// Iter 15a, path 2: 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(),
|
|
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:?}");
|
|
}
|
|
|
|
/// Iter 15a (post-ct.2): 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-ct.2 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(),
|
|
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:?}");
|
|
}
|
|
|
|
/// Iter 15b: 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(),
|
|
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,
|
|
})],
|
|
};
|
|
// 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(),
|
|
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:?}");
|
|
}
|
|
|
|
/// ct.2 Task 1: 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-ct.1 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-ct.1 (bare = local to defining module).
|
|
let prelude = Module {
|
|
schema: SCHEMA.into(),
|
|
name: "p".into(),
|
|
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,
|
|
}),
|
|
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(),
|
|
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
|
|
);
|
|
}
|
|
|
|
/// ct.2 Task 1: `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 ct.1.5a-followup 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,
|
|
});
|
|
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),
|
|
}
|
|
}
|
|
|
|
/// Iter 14e: 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(),
|
|
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,
|
|
}),
|
|
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_int".into(),
|
|
args: vec![Term::Var { name: "h".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");
|
|
}
|
|
|
|
/// Iter 16b.3: a `Term::LetRec` that captures a `Term::Let`-bound
|
|
/// name (whose type is known only after typecheck) reaches `synth`
|
|
/// because the desugar pass leaves it in place. The new typing
|
|
/// rule for `Term::LetRec` accepts it: extends locals with `name`
|
|
/// and the params, synths the body, unifies against the declared
|
|
/// return type, then synths the in-clause.
|
|
#[test]
|
|
fn letrec_with_let_binding_capture_typechecks() {
|
|
// fn outer : (Int) -> Int = \n.
|
|
// let threshold = + 5 5
|
|
// in let-rec loop : (Int) -> Int = \i.
|
|
// if (>= i threshold) then 0 else loop (+ i 1)
|
|
// in loop 0
|
|
let body = Term::Let {
|
|
name: "threshold".into(),
|
|
value: Box::new(Term::App {
|
|
callee: Box::new(Term::Var { name: "+".into() }),
|
|
args: vec![
|
|
Term::Lit { lit: Literal::Int { value: 5 } },
|
|
Term::Lit { lit: Literal::Int { value: 5 } },
|
|
],
|
|
tail: false,
|
|
}),
|
|
body: Box::new(Term::LetRec {
|
|
name: "loop".into(),
|
|
ty: Type::Fn {
|
|
params: vec![Type::int()],
|
|
ret: Box::new(Type::int()),
|
|
effects: vec![],
|
|
param_modes: vec![],
|
|
ret_mode: ParamMode::Implicit,
|
|
},
|
|
params: vec!["i".into()],
|
|
body: Box::new(Term::If {
|
|
cond: Box::new(Term::App {
|
|
callee: Box::new(Term::Var { name: ">=".into() }),
|
|
args: vec![
|
|
Term::Var { name: "i".into() },
|
|
Term::Var { name: "threshold".into() },
|
|
],
|
|
tail: false,
|
|
}),
|
|
then: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
|
|
else_: Box::new(Term::App {
|
|
callee: Box::new(Term::Var { name: "loop".into() }),
|
|
args: vec![Term::App {
|
|
callee: Box::new(Term::Var { name: "+".into() }),
|
|
args: vec![
|
|
Term::Var { name: "i".into() },
|
|
Term::Lit { lit: Literal::Int { value: 1 } },
|
|
],
|
|
tail: false,
|
|
}],
|
|
tail: false,
|
|
}),
|
|
}),
|
|
in_term: Box::new(Term::App {
|
|
callee: Box::new(Term::Var { name: "loop".into() }),
|
|
args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
|
|
tail: false,
|
|
}),
|
|
}),
|
|
};
|
|
let m = Module {
|
|
schema: SCHEMA.into(),
|
|
name: "t".into(),
|
|
imports: vec![],
|
|
defs: vec![fn_def(
|
|
"outer",
|
|
Type::Fn {
|
|
params: vec![Type::int()],
|
|
ret: Box::new(Type::int()),
|
|
effects: vec![],
|
|
param_modes: vec![],
|
|
ret_mode: ParamMode::Implicit,
|
|
},
|
|
vec!["n"],
|
|
body,
|
|
)],
|
|
};
|
|
check(&m).expect("LetRec with Let-binding capture should typecheck");
|
|
}
|
|
|
|
/// Iter 16b.3: 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(),
|
|
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}"
|
|
);
|
|
}
|
|
|
|
/// Iter 16b.3: `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(),
|
|
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:?}"),
|
|
}
|
|
}
|
|
|
|
/// Iter 16b.4: 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,
|
|
};
|
|
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(),
|
|
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()]);
|
|
}
|
|
|
|
/// Iter 16b.6: post-typecheck `lift_letrecs` lifts a deferred
|
|
/// LetRec inside a polymorphic enclosing fn into a `Forall`-typed
|
|
/// synthetic top-level fn, mirroring the enclosing fn's type
|
|
/// vars. Property protected:
|
|
///
|
|
/// 1. The fast-path desugar lift handles the `KnownType`-only
|
|
/// case end-to-end (see desugar's
|
|
/// `let_rec_capture_under_polymorphic_enclosing_fn_lifts_to_forall_fn`).
|
|
/// 2. The defer path (some capture is `Term::Let`-bound) goes
|
|
/// through `lift_letrecs`. This test forces that path by
|
|
/// introducing a `Term::Let { z = 7 }` inside the body and
|
|
/// capturing `z`. The lifted fn must still be `Forall(a). Fn(...)`,
|
|
/// even though the lift happens post-typecheck rather than
|
|
/// in desugar.
|
|
///
|
|
/// Without 16b.6, lift_letrecs would have panicked on the
|
|
/// `Type::Forall` match arm at lift-construction time.
|
|
#[test]
|
|
fn lift_letrecs_under_polymorphic_enclosing_fn_produces_forall_fn() {
|
|
// fn outer : Forall(a). (a) -> a = \x.
|
|
// let z = 7
|
|
// in let-rec helper : (Int) -> a = \k. if k == 0 then x else helper(k-1) + z (impossible — types don't match)
|
|
//
|
|
// Simpler shape: capture z (Let-bound, Int) in a polymorphic
|
|
// enclosing fn, with a body that returns x (the polymorphic
|
|
// capture).
|
|
//
|
|
// fn outer : Forall(a). (a) -> a = \x.
|
|
// let z = 7
|
|
// in let-rec helper : (Int) -> a = \k.
|
|
// if k == 0 then x else helper(k - z)
|
|
// in helper 1
|
|
let m = Module {
|
|
schema: SCHEMA.into(),
|
|
name: "t".into(),
|
|
imports: vec![],
|
|
defs: vec![fn_def(
|
|
"outer",
|
|
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".into()],
|
|
Term::Let {
|
|
name: "z".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::Var { name: "a".into() }),
|
|
effects: vec![],
|
|
param_modes: vec![],
|
|
ret_mode: ParamMode::Implicit,
|
|
},
|
|
params: vec!["k".into()],
|
|
body: Box::new(Term::If {
|
|
cond: Box::new(Term::App {
|
|
callee: Box::new(Term::Var { name: "==".into() }),
|
|
args: vec![
|
|
Term::Var { name: "k".into() },
|
|
Term::Lit { lit: Literal::Int { value: 0 } },
|
|
],
|
|
tail: false,
|
|
}),
|
|
then: Box::new(Term::Var { name: "x".into() }),
|
|
else_: Box::new(Term::App {
|
|
callee: Box::new(Term::Var { name: "helper".into() }),
|
|
args: vec![Term::App {
|
|
callee: Box::new(Term::Var { name: "-".into() }),
|
|
args: vec![
|
|
Term::Var { name: "k".into() },
|
|
Term::Var { name: "z".into() },
|
|
],
|
|
tail: false,
|
|
}],
|
|
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 succeeds.
|
|
check(&m).expect("typecheck before lift");
|
|
let desugared = ailang_core::desugar::desugar_module(&m);
|
|
// After desugar the LetRec should still be present (the
|
|
// capture set is `{x: KnownType, z: LetBound}` and any
|
|
// LetBound forces deferral).
|
|
let lifted = lift_letrecs(&desugared).expect("lift_letrecs");
|
|
assert_eq!(
|
|
lifted.defs.len(),
|
|
2,
|
|
"expected one synthetic fn appended; got {:?}",
|
|
lifted.defs.iter().map(|d| d.name()).collect::<Vec<_>>()
|
|
);
|
|
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
|
|
);
|
|
// Lifted ty must be Forall(a). Fn(Int, a, Int) -> a.
|
|
// Original LetRec params: [Int]; captures (BTreeSet order):
|
|
// x: a then z: Int (alphabetical). Ret: a.
|
|
match &synth.ty {
|
|
Type::Forall { vars, constraints: _, body } => {
|
|
assert_eq!(
|
|
vars,
|
|
&vec!["a".to_string()],
|
|
"Forall vars must mirror enclosing fn's vars; got {:?}",
|
|
vars
|
|
);
|
|
match body.as_ref() {
|
|
Type::Fn { params, ret, .. } => {
|
|
assert_eq!(params.len(), 3, "expected k + x + z params");
|
|
assert!(
|
|
matches!(¶ms[0], Type::Con { name, .. } if name == "Int"),
|
|
"first param: original k:Int; got {:?}",
|
|
params[0]
|
|
);
|
|
// Captures are in BTreeSet order, so x (a-typed) comes before z (Int).
|
|
assert!(
|
|
matches!(¶ms[1], Type::Var { name } if name == "a"),
|
|
"second param: x: a; got {:?}",
|
|
params[1]
|
|
);
|
|
assert!(
|
|
matches!(¶ms[2], Type::Con { name, .. } if name == "Int"),
|
|
"third param: z: Int; got {:?}",
|
|
params[2]
|
|
);
|
|
assert!(
|
|
matches!(ret.as_ref(), Type::Var { name } if name == "a"),
|
|
"ret: a; got {:?}",
|
|
ret
|
|
);
|
|
}
|
|
other => panic!("Forall body must be Fn; got {:?}", other),
|
|
}
|
|
}
|
|
other => panic!(
|
|
"lifted type must be Forall (mirroring enclosing); got {:?}",
|
|
other
|
|
),
|
|
}
|
|
assert_eq!(
|
|
synth.params,
|
|
vec!["k".to_string(), "x".to_string(), "z".to_string()]
|
|
);
|
|
}
|
|
|
|
/// Iter 16e: helper that wraps `body` in a fn whose return type is
|
|
/// `Bool`, runs `check`, and returns the diagnostics. Used by the
|
|
/// polymorphic-`==` typecheck tests below.
|
|
fn check_eq_body_returns_bool(body: Term) -> Vec<Diagnostic> {
|
|
let m = Module {
|
|
schema: SCHEMA.into(),
|
|
name: "t".into(),
|
|
imports: vec![],
|
|
defs: vec![fn_def(
|
|
"f",
|
|
Type::Fn {
|
|
params: vec![],
|
|
ret: Box::new(Type::bool_()),
|
|
effects: vec![],
|
|
param_modes: vec![],
|
|
ret_mode: ParamMode::Implicit,
|
|
},
|
|
vec![],
|
|
body,
|
|
)],
|
|
};
|
|
check_module(&m)
|
|
}
|
|
|
|
fn eq_app(a: Term, b: Term) -> Term {
|
|
Term::App {
|
|
callee: Box::new(Term::Var { name: "==".into() }),
|
|
args: vec![a, b],
|
|
tail: false,
|
|
}
|
|
}
|
|
|
|
/// Iter 16e: `==` accepts Int args (regression — the pre-16e
|
|
/// behaviour stays identical).
|
|
#[test]
|
|
fn eq_typechecks_at_int() {
|
|
let body = eq_app(
|
|
Term::Lit { lit: Literal::Int { value: 1 } },
|
|
Term::Lit { lit: Literal::Int { value: 2 } },
|
|
);
|
|
assert!(check_eq_body_returns_bool(body).is_empty());
|
|
}
|
|
|
|
/// Iter 16e: `==` accepts Bool args. Pre-16e this was a typecheck
|
|
/// error because `==` was declared `(Int, Int) -> Bool`.
|
|
#[test]
|
|
fn eq_typechecks_at_bool() {
|
|
let body = eq_app(
|
|
Term::Lit { lit: Literal::Bool { value: true } },
|
|
Term::Lit { lit: Literal::Bool { value: false } },
|
|
);
|
|
assert!(check_eq_body_returns_bool(body).is_empty());
|
|
}
|
|
|
|
/// Iter 16e: `==` accepts Str args. Same story as Bool.
|
|
#[test]
|
|
fn eq_typechecks_at_str() {
|
|
let body = eq_app(
|
|
Term::Lit { lit: Literal::Str { value: "hi".into() } },
|
|
Term::Lit { lit: Literal::Str { value: "ho".into() } },
|
|
);
|
|
assert!(check_eq_body_returns_bool(body).is_empty());
|
|
}
|
|
|
|
/// Iter 16e: `==` accepts Unit args.
|
|
#[test]
|
|
fn eq_typechecks_at_unit() {
|
|
let body = eq_app(
|
|
Term::Lit { lit: Literal::Unit },
|
|
Term::Lit { lit: Literal::Unit },
|
|
);
|
|
assert!(check_eq_body_returns_bool(body).is_empty());
|
|
}
|
|
|
|
/// Iter 16e: `==`'s type still demands the two sides to agree —
|
|
/// `(== 1 true)` must fail to unify the second arg's `Bool`
|
|
/// against the metavar already pinned to `Int` by the first.
|
|
#[test]
|
|
fn eq_rejects_mixed_int_bool() {
|
|
let body = eq_app(
|
|
Term::Lit { lit: Literal::Int { value: 1 } },
|
|
Term::Lit { lit: Literal::Bool { value: true } },
|
|
);
|
|
let diags = check_eq_body_returns_bool(body);
|
|
assert!(
|
|
!diags.is_empty(),
|
|
"(== 1 true) must fail to typecheck; got no diagnostics"
|
|
);
|
|
}
|
|
|
|
/// Iter 18d.1: 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(),
|
|
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.md §"Float
|
|
/// semantics" — 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(),
|
|
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:?}"
|
|
);
|
|
}
|
|
|
|
/// ct.2 Task 2: 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(),
|
|
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,
|
|
})],
|
|
};
|
|
let consumer = Module {
|
|
schema: SCHEMA.into(),
|
|
name: "use_lib".into(),
|
|
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:?}");
|
|
}
|
|
|
|
/// ct.2 Task 2: 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-ct.1 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(),
|
|
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"
|
|
);
|
|
}
|
|
|
|
/// ct.2 Task 3: a bare `Term::Ctor.type_name` that does not resolve
|
|
/// to a local TypeDef must error with `UnknownType` (or
|
|
/// `UnknownCtor`, depending on which check fires first). The
|
|
/// imports-fallback that previously synthesised a qualified result
|
|
/// from an arbitrary imported module is gone. The
|
|
/// post-ct.1 validator catches this shape at load time for
|
|
/// canonical inputs; this test pins the residual runtime guard
|
|
/// against constructed (non-loaded) AST.
|
|
#[test]
|
|
fn ct2_term_ctor_bare_cross_module_fails_closed() {
|
|
let prelude = Module {
|
|
schema: SCHEMA.into(),
|
|
name: "p".into(),
|
|
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,
|
|
})],
|
|
};
|
|
// Consumer imports prelude but writes BARE `Ordering` in
|
|
// Term::Ctor — this is a stale-canonical-form construction.
|
|
let consumer = Module {
|
|
schema: SCHEMA.into(),
|
|
name: "u".into(),
|
|
imports: vec![Import { module: "p".into(), alias: None }],
|
|
defs: vec![fn_def(
|
|
"stale",
|
|
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(), 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.iter().any(|d| d.code == "unknown-type"),
|
|
"expected unknown-type diagnostic for bare cross-module \
|
|
Term::Ctor; got {diags:?}"
|
|
);
|
|
}
|
|
|
|
/// ct.2 Task 3: a qualified `Term::Ctor.type_name`
|
|
/// (`p.Ordering` / `LT`) continues to resolve cleanly through the
|
|
/// qualified branch. This is the canonical form post-ct.1 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(),
|
|
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,
|
|
})],
|
|
};
|
|
let consumer = Module {
|
|
schema: SCHEMA.into(),
|
|
name: "u".into(),
|
|
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:?}");
|
|
}
|
|
|
|
/// Iter 23.4-prep Task 2: 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(),
|
|
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(),
|
|
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:?}"
|
|
);
|
|
}
|
|
|
|
/// mq.2.1: `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}");
|
|
}
|
|
|
|
/// mq.2.1: `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}");
|
|
}
|
|
|
|
/// mq.2.2: `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-mq.2
|
|
/// 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");
|
|
}
|
|
|
|
/// mq.2.2: 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}");
|
|
}
|
|
|
|
/// mq.2.3: `ResidualConstraint` carries an optional candidate-class
|
|
/// set for the multi-candidate dispatch path. `None` preserves the
|
|
/// pre-mq.2 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));
|
|
}
|
|
|
|
/// mq.2.5: 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()))
|
|
);
|
|
}
|
|
|
|
/// mq.2.7: 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*/ ®istry,
|
|
);
|
|
assert_eq!(outcome, RefineOutcome::Resolved("prelude.Show".to_string()));
|
|
}
|
|
|
|
/// mq.2.7: 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, &[], ®istry);
|
|
match outcome {
|
|
RefineOutcome::NoInstance { candidate_classes, .. } => {
|
|
assert_eq!(candidate_classes.len(), 2);
|
|
}
|
|
other => panic!("expected NoInstance, got {other:?}"),
|
|
}
|
|
}
|
|
|
|
/// mq.2.7: 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, &[], ®istry);
|
|
match outcome {
|
|
RefineOutcome::Ambiguous { candidate_classes, .. } => {
|
|
assert_eq!(candidate_classes.len(), 2);
|
|
}
|
|
other => panic!("expected Ambiguous, got {other:?}"),
|
|
}
|
|
}
|
|
|
|
/// mq.2.4: `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-mq.3 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(),
|
|
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");
|
|
}
|
|
}
|