diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index bbe8220..3e1365c 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -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 = 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 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{Ord a}. Fn[..]` carries the + /// constraint type `Type::Var { name: "a" }` — fine — but a + /// hypothetical `Forall{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 = 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.