diff --git a/crates/ail/tests/typeclass_22b2.rs b/crates/ail/tests/typeclass_22b2.rs index e864395..b2c03b4 100644 --- a/crates/ail/tests/typeclass_22b2.rs +++ b/crates/ail/tests/typeclass_22b2.rs @@ -169,3 +169,46 @@ fn fn_with_correct_constraint_typechecks_green() { diagnostics ); } + +/// Property protected: superclass-walk in `expand_declared_constraints` +/// covers the residual class produced by calling a superclass's method +/// from within a function constrained on the subclass. Concretely: the +/// fn declares `Ord a =>` and calls `eq` (an `Eq` method); the residual +/// `(Eq, a)` is satisfied because `Ord` extends `Eq`, so the expanded +/// declared set must include `(Eq, a)`. Without the superclass walk the +/// fn would spuriously fire `missing-constraint`. This is the positive +/// fixture for Decision 11's one-step superclass closure. +#[test] +fn fn_calling_superclass_method_via_subclass_constraint_typechecks_green() { + let entry = examples_dir() + .join("test_22b2_constraint_declared_via_superclass.ail.json"); + let ws = ailang_core::workspace::load_workspace(&entry) + .expect("workspace loads"); + let diagnostics = ailang_check::check_workspace(&ws); + assert!( + diagnostics.is_empty(), + "expected no diagnostics; superclass walk should have covered Eq via Ord; got: {:?}", + diagnostics + ); +} + +/// Property protected: the superclass walk goes from subclass to +/// superclass only — never the other direction. A fn that declares +/// `Eq a =>` and calls `lt` (an `Ord` method) must still fire +/// `missing-constraint` because `Ord` is a *sub*class of `Eq`, not a +/// superclass; the declared `(Eq, a)` does not cover the residual +/// `(Ord, a)`. Without this asymmetry, declaring the superclass would +/// spuriously satisfy any subclass residual. +#[test] +fn fn_with_superclass_constraint_calling_subclass_method_fires_missing_constraint() { + let entry = examples_dir() + .join("test_22b2_missing_constraint_subclass.ail.json"); + let ws = ailang_core::workspace::load_workspace(&entry) + .expect("workspace loads"); + let diagnostics = ailang_check::check_workspace(&ws); + assert!( + diagnostics.iter().any(|d| d.code == "missing-constraint"), + "expected missing-constraint; superclass walk should NOT cover sub-direction; got: {:?}", + diagnostics.iter().map(|d| &d.code).collect::>() + ); +} diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 19da231..2c5b1b8 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -1139,14 +1139,13 @@ fn check_in_workspace( } } env.class_methods = class_methods; - let mut class_superclasses: BTreeMap> = BTreeMap::new(); + let mut class_superclasses: BTreeMap = BTreeMap::new(); for module in ws.modules.values() { for def in &module.defs { if let Def::Class(cd) = def { - class_superclasses.insert( - cd.name.clone(), - cd.superclass.as_ref().map(|s| s.class.clone()), - ); + if let Some(sc) = &cd.superclass { + class_superclasses.insert(cd.name.clone(), sc.class.clone()); + } } } } @@ -1321,10 +1320,9 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> { let mut effects = BTreeSet::new(); let mut subst = Subst::default(); let mut counter: u32 = 0; - // Iter 22b.2 (Task 9): per-fn residual class constraints. Every - // call to a class method inside the body pushes a - // [`ResidualConstraint`] here; after the body finishes, we - // compare against the expanded declared set. + // Per-fn residual class constraints. Every call to a class method + // inside the body pushes a [`ResidualConstraint`] here; after the + // body finishes, we compare against the expanded declared set. let mut residuals: Vec = Vec::new(); let body_ty = synth(&f.body, &env, &mut locals, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals)?; unify(&ret_ty, &body_ty, &mut subst)?; @@ -1407,11 +1405,11 @@ pub(crate) struct ResidualConstraint { /// residual is satisfied. fn expand_declared_constraints( declared: &[Constraint], - class_superclasses: &BTreeMap>, + class_superclasses: &BTreeMap, ) -> Vec { let mut out: Vec = declared.to_vec(); for c in declared { - if let Some(Some(sc)) = class_superclasses.get(&c.class) { + if let Some(sc) = class_superclasses.get(&c.class) { out.push(Constraint { class: sc.clone(), type_: c.type_.clone(), @@ -2413,11 +2411,13 @@ pub struct Env { /// safe (no overwrites). Read in [`synth`]'s `Term::Var` arm. pub class_methods: BTreeMap, /// Iter 22b.2 (Task 9): one-step superclass expansion table. - /// Maps each class name to its (optional) superclass class name. - /// Used by [`check_fn`] to expand `Forall.constraints` for the - /// missing-constraint check (Decision 11: max one step). The - /// schema permits at most one superclass per class. - pub class_superclasses: BTreeMap>, + /// Maps each class name to its superclass class name. Absence from + /// the map means the class has no superclass — populated only for + /// classes that declare one. Used by [`check_fn`] to expand + /// `Forall.constraints` for the missing-constraint check + /// (Decision 11: max one step). The schema permits at most one + /// superclass per class. + pub class_superclasses: BTreeMap, } /// Back-pointer from a ctor name to the ADT that declared it. Stored diff --git a/examples/test_22b2_constraint_declared_via_superclass.ail.json b/examples/test_22b2_constraint_declared_via_superclass.ail.json new file mode 100644 index 0000000..4331304 --- /dev/null +++ b/examples/test_22b2_constraint_declared_via_superclass.ail.json @@ -0,0 +1,53 @@ +{ + "schema": "ailang/v0", + "name": "test_22b2_constraint_declared_via_superclass", + "imports": [], + "defs": [ + { + "kind": "class", "name": "Eq", "param": "a", + "methods": [{ + "name": "eq", + "type": { + "k": "fn", + "params": [{ "k": "var", "name": "a" }, { "k": "var", "name": "a" }], + "ret": { "k": "con", "name": "Bool" }, "effects": [] + } + }] + }, + { + "kind": "class", "name": "Ord", "param": "a", + "superclass": { "class": "Eq", "type": "a" }, + "methods": [{ + "name": "lt", + "type": { + "k": "fn", + "params": [{ "k": "var", "name": "a" }, { "k": "var", "name": "a" }], + "ret": { "k": "con", "name": "Bool" }, "effects": [] + } + }] + }, + { + "kind": "fn", + "name": "uses_eq_via_ord", + "type": { + "k": "forall", + "vars": ["a"], + "constraints": [ + { "class": "Ord", "type": { "k": "var", "name": "a" } } + ], + "body": { + "k": "fn", + "params": [{ "k": "var", "name": "a" }, { "k": "var", "name": "a" }], + "ret": { "k": "con", "name": "Bool" }, + "effects": [] + } + }, + "params": ["x", "y"], + "body": { + "t": "app", + "fn": { "t": "var", "name": "eq" }, + "args": [{ "t": "var", "name": "x" }, { "t": "var", "name": "y" }] + } + } + ] +} diff --git a/examples/test_22b2_missing_constraint_subclass.ail.json b/examples/test_22b2_missing_constraint_subclass.ail.json new file mode 100644 index 0000000..0dc38a0 --- /dev/null +++ b/examples/test_22b2_missing_constraint_subclass.ail.json @@ -0,0 +1,53 @@ +{ + "schema": "ailang/v0", + "name": "test_22b2_missing_constraint_subclass", + "imports": [], + "defs": [ + { + "kind": "class", "name": "Eq", "param": "a", + "methods": [{ + "name": "eq", + "type": { + "k": "fn", + "params": [{ "k": "var", "name": "a" }, { "k": "var", "name": "a" }], + "ret": { "k": "con", "name": "Bool" }, "effects": [] + } + }] + }, + { + "kind": "class", "name": "Ord", "param": "a", + "superclass": { "class": "Eq", "type": "a" }, + "methods": [{ + "name": "lt", + "type": { + "k": "fn", + "params": [{ "k": "var", "name": "a" }, { "k": "var", "name": "a" }], + "ret": { "k": "con", "name": "Bool" }, "effects": [] + } + }] + }, + { + "kind": "fn", + "name": "needs_ord_but_only_has_eq", + "type": { + "k": "forall", + "vars": ["a"], + "constraints": [ + { "class": "Eq", "type": { "k": "var", "name": "a" } } + ], + "body": { + "k": "fn", + "params": [{ "k": "var", "name": "a" }, { "k": "var", "name": "a" }], + "ret": { "k": "con", "name": "Bool" }, + "effects": [] + } + }, + "params": ["x", "y"], + "body": { + "t": "app", + "fn": { "t": "var", "name": "lt" }, + "args": [{ "t": "var", "name": "x" }, { "t": "var", "name": "y" }] + } + } + ] +}