From 842df380a40948295837558888b3a0701c7b63ab Mon Sep 17 00:00:00 2001 From: Brummel Date: Sun, 10 May 2026 21:24:16 +0200 Subject: [PATCH] iter 23.1.3: implicit prelude import + symmetric bare-type-name imports-fallback in Term::Ctor synth --- crates/ailang-check/src/lib.rs | 177 +++++++++++++++++- .../tests/env_construction_pin.rs | 8 +- 2 files changed, 178 insertions(+), 7 deletions(-) diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index c34dad5..5990123 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -443,6 +443,18 @@ pub enum CheckError { candidates: Vec, }, + /// 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 @@ -542,6 +554,7 @@ impl CheckError { CheckError::InvalidDefName { .. } => "invalid-def-name", CheckError::TailCallNotInTailPosition => "tail-call-not-in-tail-position", CheckError::AmbiguousCtor { .. } => "ambiguous-ctor", + CheckError::AmbiguousType { .. } => "ambiguous-type", CheckError::ReuseAsNonAllocatingBody { .. } => "reuse-as-non-allocating-body", CheckError::MissingConstraint { .. } => "missing-constraint", CheckError::NoInstance { .. } => "no-instance", @@ -583,6 +596,9 @@ impl CheckError { CheckError::AmbiguousCtor { ctor, candidates } => { serde_json::json!({"ctor": ctor, "candidates": candidates}) } + CheckError::AmbiguousType { type_name, candidates } => { + serde_json::json!({"type_name": type_name, "candidates": candidates}) + } CheckError::ReuseAsNonAllocatingBody { got, .. } => { serde_json::json!({"got": got}) } @@ -1179,6 +1195,16 @@ pub fn build_check_env(ws: &Workspace) -> Env { 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); } @@ -1271,6 +1297,15 @@ fn check_in_workspace( 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. Mirrors the + // workspace-flat overlay in `build_check_env`. 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(); @@ -1913,6 +1948,12 @@ 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 td = if type_name.matches('.').count() == 1 { let (prefix, suffix) = type_name.split_once('.').expect("checked"); let target_module = match env.imports.get(prefix) { @@ -1930,12 +1971,51 @@ pub(crate) fn synth( .ok_or_else(|| CheckError::UnknownType(type_name.clone()))?; owning_module = Some(target_module); td - } else { + } else if let Some(td) = env.types.get(type_name) { + // Local hit: original Iter 13 behaviour. owning_module = None; - env.types - .get(type_name) - .ok_or_else(|| CheckError::UnknownType(type_name.clone()))? - .clone() + td.clone() + } else { + // Iter 23.1.3: bare type-name not present locally — + // scan imported modules for a type by this name. + // Symmetric to `Pattern::Ctor`'s fallback at this + // file's ~lib.rs:2453; 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(), + }); + } + } }; let cdef = td .ctors @@ -1990,7 +2070,7 @@ pub(crate) fn synth( unify(&exp_inst, &actual, subst)?; } Ok(Type::Con { - name: type_name.clone(), + name: result_type_name, args: type_args, }) } @@ -3713,6 +3793,91 @@ mod tests { assert!(diags.is_empty(), "expected green; 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 + ); + } + /// 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. diff --git a/crates/ailang-check/tests/env_construction_pin.rs b/crates/ailang-check/tests/env_construction_pin.rs index 09a6f9a..b3c1dad 100644 --- a/crates/ailang-check/tests/env_construction_pin.rs +++ b/crates/ailang-check/tests/env_construction_pin.rs @@ -72,13 +72,19 @@ fn build_env_inline_pre_refactor(ws: &ailang_core::workspace::Workspace) -> Env } env.module_types = module_types; - // env.module_imports — per-module alias map. + // env.module_imports — per-module alias map. Iter 23.1: every + // non-prelude module implicitly imports the prelude module. for m in ws.modules.values() { let mut import_map: BTreeMap = 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()); } + 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); }