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

iter ct.2.1: qualify_local_types on class-method channel + Forall constraints recursion

Browse Source
This commit is contained in:
Brummel
2026-05-11 09:00:06 +02:00
parent e9aae3e9fb
commit 78ccbcee9c
1 changed files with 229 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files
crates/ailang-check/src/lib.rs
+229 -2
View File
@@ -1806,10 +1806,24 @@ pub(crate) fn synth(
// a fresh metavar; the body's unification at the call
// site fills it in, and the residual is the class
// constraint we owe at this use site.
//
// ct.2 Task 1: a class method's declared type lives in
// its defining module's bare-local namespace.
// qualify_local_types runs symmetrically with the
// Term::Var qualified path below so the consumer's
// typecheck context sees the method's return /
// parameter Type::Cons fully qualified.
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(&cm.method_ty, &mapping);
let inst_ty = substitute_rigids(&qualified_method_ty, &mapping);
residuals.push(ResidualConstraint {
class: cm.class_name.clone(),
type_: fresh,
@@ -2417,7 +2431,13 @@ fn qualify_local_types(t: &Type, owner_module: &str, local_types: &IndexMap<Stri
},
Type::Forall { vars, constraints, body } => Type::Forall {
vars: vars.clone(),
constraints: constraints.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(),
@@ -3969,6 +3989,213 @@ mod tests {
);
}
/// 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.