Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

iter ct.2.3: Term::Ctor synth direct lookup; delete imports-fallback + dead AmbiguousType

Browse Source
This commit is contained in:
Brummel
2026-05-11 09:21:36 +02:00
parent edb694fdce
commit 97bb5e71fd
1 changed files with 135 additions and 236 deletions
Download Patch File Download Diff File Expand all files Collapse all files
crates/ailang-check/src/lib.rs
+135 -236
View File
@@ -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": "<n>", "candidates": ["m1.T", "m2.T"]}`.
#[error("ambiguous type `{type_name}`: declared in {candidates:?}")]
AmbiguousType {
type_name: String,
candidates: Vec<String>,
},
/// 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<String>;
// 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:?}");
}
}