From 97bb5e71fd0e0ba0b37f06244ab9ef4d79952ab4 Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 11 May 2026 09:21:36 +0200 Subject: [PATCH] iter ct.2.3: Term::Ctor synth direct lookup; delete imports-fallback + dead AmbiguousType --- crates/ailang-check/src/lib.rs | 371 ++++++++++++--------------------- 1 file changed, 135 insertions(+), 236 deletions(-) diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 4095b2d..2b609c7 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -434,18 +434,6 @@ pub enum CheckError { #[error("call marked `tail` is not in tail position")] TailCallNotInTailPosition, - /// Iter 23.1.3: a bare `Term::Ctor.type_name` did not resolve - /// against the current module's local `env.types` and resolved - /// against type defs in two or more imported modules. The author - /// must qualify the type-name (e.g. write `std_maybe.Maybe` instead - /// of bare `Maybe`). Code: `ambiguous-type`. - /// `ctx`: `{"type_name": "", "candidates": ["m1.T", "m2.T"]}`. - #[error("ambiguous type `{type_name}`: declared in {candidates:?}")] - AmbiguousType { - type_name: String, - candidates: Vec, - }, - /// 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 @@ -544,7 +532,6 @@ impl CheckError { CheckError::UnknownImport { .. } => "unknown-import", CheckError::InvalidDefName { .. } => "invalid-def-name", CheckError::TailCallNotInTailPosition => "tail-call-not-in-tail-position", - CheckError::AmbiguousType { .. } => "ambiguous-type", CheckError::ReuseAsNonAllocatingBody { .. } => "reuse-as-non-allocating-body", CheckError::MissingConstraint { .. } => "missing-constraint", CheckError::NoInstance { .. } => "no-instance", @@ -583,9 +570,6 @@ impl CheckError { CheckError::InvalidDefName { name } => { serde_json::json!({"name": name, "reason": "contains-dot"}) } - CheckError::AmbiguousType { type_name, candidates } => { - serde_json::json!({"type_name": type_name, "candidates": candidates}) - } CheckError::ReuseAsNonAllocatingBody { got, .. } => { serde_json::json!({"got": got}) } @@ -1947,10 +1931,11 @@ pub(crate) fn synth( Ok(sig.ret) } Term::Ctor { type_name, ctor, args } => { - // Iter 15a: a qualified `type_name` (`module.Type`) resolves - // through the import map; the ctor name stays bare and is - // looked up inside the resolved TypeDef. The bare-name path - // is the original Iter 13 behaviour. + // 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 @@ -1961,12 +1946,7 @@ pub(crate) fn synth( // (and any other locally-named cross-module type-cons) are // qualified before substitution / unification. let owning_module: Option; - // Iter 23.1.3: the name embedded in the result `Type::Con`. - // Defaults to the user-written `type_name` (qualified form - // for the `module.Type` branch, bare for the local branch), - // and is upgraded to `imp.Type` when the bare-name - // imports-fallback resolves through an imported module. - let mut result_type_name: String = type_name.clone(); + 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) { @@ -1985,52 +1965,10 @@ pub(crate) fn synth( owning_module = Some(target_module); td } else if let Some(td) = env.types.get(type_name) { - // Local hit: original Iter 13 behaviour. owning_module = None; td.clone() } else { - // Iter 23.1.3: bare type-name not present locally — - // scan imported modules for a type by this name. - // Symmetric to the Iter 15a imports-fallback applied - // to `Pattern::Ctor` resolution (search this file for - // "Iter 15a: try local ctor_index first" to find the - // canonical comment). Required so an LLM author can - // write `(con Ordering LT)` against a prelude type - // without qualifying it as `prelude.Ordering`. The - // result `Type::Con` carries the qualified name so - // that downstream `Pattern::Ctor` resolution (which - // already produces qualified names from its own - // imports-fallback) lines up against the scrutinee. - let mut hits: Vec<(String, String, TypeDef)> = Vec::new(); - for imp in env.imports.values() { - if let Some(tys) = env.module_types.get(imp) { - if let Some(td) = tys.get(type_name) { - hits.push(( - format!("{imp}.{type_name}"), - imp.clone(), - td.clone(), - )); - } - } - } - match hits.len() { - 0 => { - return Err(CheckError::UnknownType(type_name.clone())); - } - 1 => { - let (qname, owner, td) = - hits.into_iter().next().expect("len == 1"); - owning_module = Some(owner); - result_type_name = qname; - td - } - _ => { - return Err(CheckError::AmbiguousType { - type_name: type_name.clone(), - candidates: hits.into_iter().map(|(q, _, _)| q).collect(), - }); - } - } + return Err(CheckError::UnknownType(type_name.clone())); }; let cdef = td .ctors @@ -3696,173 +3634,6 @@ mod tests { assert!(diags.is_empty(), "expected green; got {diags:?}"); } - /// Iter 23.1: the new bare-type-name imports-fallback in - /// `Term::Ctor` synth (symmetric to `Pattern::Ctor`'s Iter-15a - /// fallback) must report `ambiguous-type` when two imported - /// modules each declare a type with the same bare name, so that - /// a future fixture importing two prelude-shaped modules cannot - /// silently resolve to one of them. - #[test] - fn cross_module_term_ctor_ambiguous_type_errors() { - // Two different libs, each declaring a type `T` (intentional clash) - // with a single ctor each. - let lib_a = Module { - schema: SCHEMA.into(), - name: "lib_a".into(), - imports: vec![], - defs: vec![Def::Type(TypeDef { - name: "T".into(), - vars: vec![], - ctors: vec![Ctor { name: "MkA".into(), fields: vec![] }], - doc: None, - drop_iterative: false, - })], - }; - let lib_b = Module { - schema: SCHEMA.into(), - name: "lib_b".into(), - imports: vec![], - defs: vec![Def::Type(TypeDef { - name: "T".into(), - vars: vec![], - ctors: vec![Ctor { name: "MkB".into(), fields: vec![] }], - doc: None, - drop_iterative: false, - })], - }; - let consumer = Module { - schema: SCHEMA.into(), - name: "use_both".into(), - imports: vec![ - Import { module: "lib_a".into(), alias: None }, - Import { module: "lib_b".into(), alias: None }, - ], - defs: vec![fn_def( - "f", - Type::Fn { - params: vec![], - ret: Box::new(Type::int()), - effects: vec![], - param_modes: vec![], - ret_mode: ParamMode::Implicit, - }, - vec![], - // Bare type_name `T` — both lib_a and lib_b match. - Term::Match { - scrutinee: Box::new(Term::Ctor { - type_name: "T".into(), - ctor: "MkA".into(), - args: vec![], - }), - arms: vec![Arm { - pat: Pattern::Wild, - body: Term::Lit { lit: Literal::Int { value: 0 } }, - }], - }, - )], - }; - let mut modules = BTreeMap::new(); - modules.insert("lib_a".into(), lib_a); - modules.insert("lib_b".into(), lib_b); - modules.insert("use_both".into(), consumer); - let ws = Workspace { - entry: "use_both".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 == "ambiguous-type"), - "expected ambiguous-type diagnostic; got {diags:?}" - ); - } - - /// Iter 23.1: the prelude module is implicitly imported into - /// every user module. A user module that pattern-matches on - /// `LT` / `EQ` / `GT` without an explicit - /// `import { module: "prelude" }` must typecheck cleanly. - #[test] - fn user_module_can_pattern_match_on_prelude_ordering_bare() { - let prelude = Module { - schema: SCHEMA.into(), - name: "prelude".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: "user".into(), - imports: vec![], - defs: vec![fn_def( - "from_lt", - 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::Ctor { - type_name: "Ordering".into(), - ctor: "LT".into(), - args: vec![], - }), - 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("prelude".into(), prelude); - modules.insert("user".into(), consumer); - let ws = Workspace { - entry: "user".into(), - modules, - root_dir: std::path::PathBuf::from("."), - registry: ailang_core::workspace::Registry::default(), - }; - let diags = check_workspace(&ws); - assert!( - diags.is_empty(), - "user module must typecheck bare-LT without explicit prelude import; 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 @@ -5036,4 +4807,132 @@ mod tests { 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:?}"); + } }