iter 22b.2.9: missing-constraint per-fn diagnostic

crates/ailang-check/src/diagnostic.rs

@@ -62,6 +62,13 @@
 //!   the build refuses it. Note that an invalid suppression does NOT
 //!   suppress its target diagnostic — the original still fires
 //!   alongside this error.
+//! - `missing-constraint` (Iter 22b.2) — `severity: error`. Emitted
+//!   by the per-fn typecheck arm when a polymorphic `FnDef` calls a
+//!   class method (e.g. `show x` where `x: a`) but its declared
+//!   `Forall.constraints` (after one-step superclass expansion) does
+//!   not include the residual class constraint. `ctx`:
+//!   `{"class": "<C>", "method": "<m>", "at_type": "<a>"}`. Concrete-
+//!   type residuals are deferred to the `no-instance` diagnostic.
 
 use serde::Serialize;
 

crates/ailang-check/src/lib.rs

@@ -442,6 +442,28 @@ pub enum CheckError {
     /// can attach a `SuggestedRewrite` that drops the wrapper.
     #[error("reuse-as body must be an allocating term (Term::Ctor or Term::Lam), got {got}")]
     ReuseAsNonAllocatingBody { got: String, body_form_a: String },
+
+    /// Iter 22b.2 (Task 9): a polymorphic `FnDef` calls a class method
+    /// (e.g. `show x` where `x: a`), producing a residual class
+    /// constraint `(class, a)` at the call site, but the fn's declared
+    /// `Forall.constraints` does not list that constraint (and the
+    /// one-step superclass-expansion of the declared set still does
+    /// not cover it). Without an in-scope constraint, monomorphisation
+    /// (22b.3) would have no dictionary to thread, so this is a hard
+    /// soundness error. Code: `missing-constraint`. `ctx`:
+    /// `{"class": "<C>", "method": "<m>", "at_type": "<a>"}`.
+    /// Concrete-type residuals (`Type::Con`) are deferred to Task 10's
+    /// `no-instance` diagnostic.
+    #[error(
+        "fn `{def}` calls class method `{method}` (class `{class}`) at type `{at_type}`, \
+        but its declared constraints do not include `{class} {at_type}`"
+    )]
+    MissingConstraint {
+        def: String,
+        method: String,
+        class: String,
+        at_type: String,
+    },
 }
 
 pub(crate) type Result<T> = std::result::Result<T, CheckError>;
@@ -480,6 +502,7 @@ impl CheckError {
             CheckError::TailCallNotInTailPosition => "tail-call-not-in-tail-position",
             CheckError::AmbiguousCtor { .. } => "ambiguous-ctor",
             CheckError::ReuseAsNonAllocatingBody { .. } => "reuse-as-non-allocating-body",
+            CheckError::MissingConstraint { .. } => "missing-constraint",
         }
     }
 
@@ -520,6 +543,9 @@ impl CheckError {
             CheckError::ReuseAsNonAllocatingBody { got, .. } => {
                 serde_json::json!({"got": got})
             }
+            CheckError::MissingConstraint { class, method, at_type, .. } => {
+                serde_json::json!({"class": class, "method": method, "at_type": at_type})
+            }
             _ => serde_json::Value::Object(serde_json::Map::new()),
         }
     }
@@ -1100,6 +1126,31 @@ fn check_in_workspace(
         .collect();
     env.module_types = build_module_types(ws);
     env.current_module = m.name.clone();
+    // Iter 22b.2 (Task 9): merge per-module class-method tables into a
+    // single workspace-wide map for [`synth`]'s `Term::Var` arm. Method
+    // names are unique workspace-wide (enforced by
+    // `workspace::build_registry`'s method-name-collision check), so
+    // the merge has no overwrites. Also walk every module's
+    // `Def::Class` to build the one-step superclass expansion table.
+    let mut class_methods: BTreeMap<String, ClassMethodEntry> = BTreeMap::new();
+    for g in module_globals.values() {
+        for (n, e) in &g.class_methods {
+            class_methods.insert(n.clone(), e.clone());
+        }
+    }
+    env.class_methods = class_methods;
+    let mut class_superclasses: BTreeMap<String, Option<String>> = 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()),
+                );
+            }
+        }
+    }
+    env.class_superclasses = class_superclasses;
     // Workspace isn't directly needed in the env; cross-module lookup uses
     // only `module_globals`. But we keep the ws reference in the
     // comment as a reminder, in case cross-module ADTs are added later.
@@ -1270,7 +1321,12 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> {
     let mut effects = BTreeSet::new();
     let mut subst = Subst::default();
     let mut counter: u32 = 0;
-    let body_ty = synth(&f.body, &env, &mut locals, &mut effects, &f.name, &mut subst, &mut counter)?;
+    // 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.
+    let mut residuals: Vec<ResidualConstraint> = 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)?;
 
     // Iter 14e: tail-position verification (Decision 8). Runs after
@@ -1284,9 +1340,106 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> {
             return Err(CheckError::UndeclaredEffect(e.clone()));
         }
     }
+
+    // Iter 22b.2 (Task 9): missing-constraint check. Build the expanded
+    // declared-constraint set (declared + one-step superclass per
+    // Decision 11) and compare against residuals. Var-shaped residuals
+    // not covered by the expanded set fire `MissingConstraint`. Concrete
+    // residuals are deferred to Task 10's `no-instance` arm.
+    let declared_constraints: Vec<Constraint> = match &f.ty {
+        Type::Forall { constraints, .. } => constraints.clone(),
+        _ => Vec::new(),
+    };
+    let expanded = expand_declared_constraints(&declared_constraints, &env.class_superclasses);
+    for r in &residuals {
+        let r_ty = subst.apply(&r.type_);
+        if let Type::Var { name } = &r_ty {
+            // Skip residuals over metavars (`$mN`) — those mean the
+            // residual is over a value the body never connected to a
+            // rigid var; treat as concrete-uncovered, which Task 10
+            // will handle. Only rigid (source-level) vars participate
+            // in the missing-constraint check here.
+            if Subst::meta_id(name).is_some() {
+                continue;
+            }
+            let satisfied = expanded
+                .iter()
+                .any(|d| d.class == r.class && constraint_type_matches(&d.type_, &r_ty));
+            if !satisfied {
+                return Err(CheckError::MissingConstraint {
+                    def: f.name.clone(),
+                    method: r.method.clone(),
+                    class: r.class.clone(),
+                    at_type: name.clone(),
+                });
+            }
+        }
+    }
     Ok(())
 }
 
+/// Iter 22b.2 (Task 9): per-call-site residual class constraint
+/// recorded by [`synth`] when a `Term::Var` resolves to a class method.
+/// Carries the method name (for diagnostic rendering), the class, and
+/// the type the class is applied to at the call site. The type is
+/// typically a fresh metavar (which unification then ties to the
+/// argument's actual type) or, after `subst.apply`, a rigid var or a
+/// concrete `Type::Con`.
+#[derive(Debug, Clone)]
+pub(crate) struct ResidualConstraint {
+    /// Class name (e.g. `Show`).
+    pub class: String,
+    /// Class param's instance at this call site. Pre-substitution: the
+    /// fresh metavar inserted at the Var site. Post-substitution: the
+    /// solved type — rigid var, concrete con, or unsolved metavar.
+    pub type_: Type,
+    /// Method name (e.g. `show`); used by the missing-constraint
+    /// diagnostic to point the author at which call site triggered
+    /// the residual.
+    pub method: String,
+}
+
+/// Iter 22b.2 (Task 9): expand a list of declared class constraints
+/// with their one-step superclass closure (Decision 11). For every
+/// declared `(C, t)`, append `(S, t)` if class `C` has a superclass
+/// `S`. Only one step — Decision 11 forbids deeper chains. The
+/// expanded list is what [`check_fn`] uses to decide whether a
+/// residual is satisfied.
+fn expand_declared_constraints(
+    declared: &[Constraint],
+    class_superclasses: &BTreeMap<String, Option<String>>,
+) -> Vec<Constraint> {
+    let mut out: Vec<Constraint> = declared.to_vec();
+    for c in declared {
+        if let Some(Some(sc)) = class_superclasses.get(&c.class) {
+            out.push(Constraint {
+                class: sc.clone(),
+                type_: c.type_.clone(),
+            });
+        }
+    }
+    out
+}
+
+/// Iter 22b.2 (Task 9): equality of constraint types for the
+/// missing-constraint match. The residual type has been
+/// `subst.apply`-d, so two rigid vars match iff their names are equal;
+/// a `Type::Con` matches another `Type::Con` iff their head names and
+/// args agree. Conservative: anything outside `Var` / `Con` is rejected
+/// (the schema bounds Constraint.type_ to plain types, and Task 9 only
+/// fires on Var residuals anyway).
+fn constraint_type_matches(declared: &Type, residual: &Type) -> bool {
+    match (declared, residual) {
+        (Type::Var { name: a }, Type::Var { name: b }) => a == b,
+        (Type::Con { name: a, args: aa }, Type::Con { name: b, args: ba }) => {
+            a == b
+                && aa.len() == ba.len()
+                && aa.iter().zip(ba.iter()).all(|(x, y)| constraint_type_matches(x, y))
+        }
+        _ => false,
+    }
+}
+
 /// Iter 14e: verifies that every `Term::App { tail: true, .. }` and
 /// `Term::Do { tail: true, .. }` actually sits in tail position, per
 /// Decision 8.
@@ -1397,7 +1550,12 @@ fn check_const(c: &ConstDef, env: &Env) -> Result<()> {
     let mut effects = BTreeSet::new();
     let mut subst = Subst::default();
     let mut counter: u32 = 0;
-    let v = synth(&c.value, env, &mut locals, &mut effects, &c.name, &mut subst, &mut counter)?;
+    // Iter 22b.2 (Task 9): const bodies don't carry a `Forall.constraints`
+    // (rejected upstream), so any residual would have to be concrete —
+    // Task 10's no-instance arm will pick those up. We thread an
+    // accumulator only to keep `synth`'s signature uniform.
+    let mut residuals: Vec<ResidualConstraint> = Vec::new();
+    let v = synth(&c.value, env, &mut locals, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals)?;
     unify(&c.ty, &v, &mut subst)?;
     if !effects.is_empty() {
         return Err(CheckError::ConstHasEffects(
@@ -1416,6 +1574,7 @@ pub(crate) fn synth(
     in_def: &str,
     subst: &mut Subst,
     counter: &mut u32,
+    residuals: &mut Vec<ResidualConstraint>,
 ) -> Result<Type> {
     match t {
         Term::Lit { lit } => Ok(match lit {
@@ -1425,15 +1584,37 @@ pub(crate) fn synth(
             Literal::Unit => Type::unit(),
         }),
         Term::Var { name } => {
-            // Lookup precedence: locals → local globals → qualified
-            // cross-module ref. A `Forall` resolved at any of these
-            // levels is instantiated with fresh metavars at the use
-            // site (textbook ML rule); rigid vars and concrete types
-            // pass through unchanged.
+            // Lookup precedence: locals → local globals → class-method
+            // table → qualified cross-module ref. A `Forall` resolved at
+            // any of these levels is instantiated with fresh metavars at
+            // the use site (textbook ML rule); rigid vars and concrete
+            // types pass through unchanged.
+            //
+            // Iter 22b.2 (Task 9): the class-method channel sits between
+            // local globals and qualified cross-module ref. When a name
+            // resolves through `env.class_methods`, we substitute the
+            // class param with a fresh metavar and record a residual
+            // class constraint — `check_fn` later compares the residual
+            // set against the declared `Forall.constraints`.
             let raw = if let Some(t) = locals.get(name) {
                 t.clone()
             } else if let Some(t) = env.globals.get(name) {
                 t.clone()
+            } else if let Some(cm) = env.class_methods.get(name) {
+                // Iter 22b.2 (Task 9): instantiate the class param with
+                // 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.
+                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);
+                residuals.push(ResidualConstraint {
+                    class: cm.class_name.clone(),
+                    type_: fresh,
+                    method: name.clone(),
+                });
+                return Ok(inst_ty);
             } else if name.matches('.').count() == 1 {
                 let (prefix, suffix) = name.split_once('.').expect("checked");
                 let target_module = match env.imports.get(prefix) {
@@ -1472,7 +1653,7 @@ pub(crate) fn synth(
             Ok(maybe_instantiate(raw, counter))
         }
         Term::App { callee, args, .. } => {
-            let cty = synth(callee, env, locals, effects, in_def, subst, counter)?;
+            let cty = synth(callee, env, locals, effects, in_def, subst, counter, residuals)?;
             let cty = subst.apply(&cty);
             let (params, ret, fx) = match &cty {
                 Type::Fn { params, ret, effects: fx, .. } => {
@@ -1508,7 +1689,7 @@ pub(crate) fn synth(
                 });
             }
             for (a, exp) in args.iter().zip(params.iter()) {
-                let actual = synth(a, env, locals, effects, in_def, subst, counter)?;
+                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals)?;
                 unify(exp, &actual, subst)?;
             }
             for e in fx {
@@ -1517,9 +1698,9 @@ pub(crate) fn synth(
             Ok(subst.apply(&ret))
         }
         Term::Let { name, value, body } => {
-            let v = synth(value, env, locals, effects, in_def, subst, counter)?;
+            let v = synth(value, env, locals, effects, in_def, subst, counter, residuals)?;
             let prev = locals.insert(name.clone(), v);
-            let r = synth(body, env, locals, effects, in_def, subst, counter)?;
+            let r = synth(body, env, locals, effects, in_def, subst, counter, residuals)?;
             match prev {
                 Some(p) => {
                     locals.insert(name.clone(), p);
@@ -1531,10 +1712,10 @@ pub(crate) fn synth(
             Ok(r)
         }
         Term::If { cond, then, else_ } => {
-            let c = synth(cond, env, locals, effects, in_def, subst, counter)?;
+            let c = synth(cond, env, locals, effects, in_def, subst, counter, residuals)?;
             unify(&Type::bool_(), &c, subst)?;
-            let t1 = synth(then, env, locals, effects, in_def, subst, counter)?;
-            let t2 = synth(else_, env, locals, effects, in_def, subst, counter)?;
+            let t1 = synth(then, env, locals, effects, in_def, subst, counter, residuals)?;
+            let t2 = synth(else_, env, locals, effects, in_def, subst, counter, residuals)?;
             unify(&t1, &t2, subst)?;
             Ok(subst.apply(&t1))
         }
@@ -1552,7 +1733,7 @@ pub(crate) fn synth(
                 });
             }
             for (a, exp) in args.iter().zip(sig.params.iter()) {
-                let actual = synth(a, env, locals, effects, in_def, subst, counter)?;
+                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals)?;
                 unify(exp, &actual, subst)?;
             }
             effects.insert(sig.effect.clone());
@@ -1646,7 +1827,7 @@ pub(crate) fn synth(
             }
             for (a, exp) in args.iter().zip(qualified_fields.iter()) {
                 let exp_inst = substitute_rigids(exp, &mapping);
-                let actual = synth(a, env, locals, effects, in_def, subst, counter)?;
+                let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals)?;
                 unify(&exp_inst, &actual, subst)?;
             }
             Ok(Type::Con {
@@ -1655,7 +1836,7 @@ pub(crate) fn synth(
             })
         }
         Term::Match { scrutinee, arms } => {
-            let s_ty = synth(scrutinee, env, locals, effects, in_def, subst, counter)?;
+            let s_ty = synth(scrutinee, env, locals, effects, in_def, subst, counter, residuals)?;
             if arms.is_empty() {
                 return Err(CheckError::NonExhaustive {
                     ty: ailang_core::pretty::type_to_string(&s_ty),
@@ -1673,7 +1854,7 @@ pub(crate) fn synth(
                     let prev = locals.insert(n.clone(), t.clone());
                     pushed.push((n.clone(), prev));
                 }
-                let body_ty = synth(&arm.body, env, locals, effects, in_def, subst, counter)?;
+                let body_ty = synth(&arm.body, env, locals, effects, in_def, subst, counter, residuals)?;
                 for (n, prev) in pushed.into_iter().rev() {
                     match prev {
                         Some(p) => {
@@ -1748,9 +1929,9 @@ pub(crate) fn synth(
             Ok(subst.apply(&result_ty.expect("checked arms is non-empty")))
         }
         Term::Seq { lhs, rhs } => {
-            let lty = synth(lhs, env, locals, effects, in_def, subst, counter)?;
+            let lty = synth(lhs, env, locals, effects, in_def, subst, counter, residuals)?;
             unify(&Type::unit(), &lty, subst)?;
-            synth(rhs, env, locals, effects, in_def, subst, counter)
+            synth(rhs, env, locals, effects, in_def, subst, counter, residuals)
         }
         Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => {
             let mut pushed: Vec<(String, Option<Type>)> = Vec::new();
@@ -1759,7 +1940,7 @@ pub(crate) fn synth(
                 pushed.push((n.clone(), prev));
             }
             let mut body_effects: BTreeSet<String> = BTreeSet::new();
-            let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter);
+            let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter, residuals);
             for (n, prev) in pushed.into_iter().rev() {
                 match prev {
                     Some(p) => {
@@ -1847,7 +2028,7 @@ pub(crate) fn synth(
             // subset rule against `declared_effs` — exactly like
             // `Term::Lam`.
             let mut body_effects: BTreeSet<String> = BTreeSet::new();
-            let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter);
+            let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter, residuals);
 
             // Restore body-scope locals (params + name).
             for (n, prev) in pushed.into_iter().rev() {
@@ -1874,7 +2055,7 @@ pub(crate) fn synth(
             // scope (params are not visible here; only the recursive
             // binding is).
             let prev_in = locals.insert(name.clone(), ty.clone());
-            let in_ty = synth(in_term, env, locals, effects, in_def, subst, counter);
+            let in_ty = synth(in_term, env, locals, effects, in_def, subst, counter, residuals);
             match prev_in {
                 Some(p) => {
                     locals.insert(name.clone(), p);
@@ -1890,7 +2071,7 @@ pub(crate) fn synth(
             // No constraint generated, no environment change. The
             // wrapper records author intent for the future RC inc/dec
             // emission pass (18c.3); typing is pure passthrough.
-            synth(value, env, locals, effects, in_def, subst, counter)
+            synth(value, env, locals, effects, in_def, subst, counter, residuals)
         }
         Term::ReuseAs { source, body } => {
             // Iter 18d.1: `(reuse-as SRC NEW-CTOR)` requires `body` to
@@ -1904,7 +2085,7 @@ pub(crate) fn synth(
             // shape-compatibility check (18d.2 will add a
             // `reuse-as-shape-mismatch` diagnostic when codegen has
             // the actual size info).
-            let _ = synth(source, env, locals, effects, in_def, subst, counter)?;
+            let _ = synth(source, env, locals, effects, in_def, subst, counter, residuals)?;
             match body.as_ref() {
                 Term::Ctor { .. } | Term::Lam { .. } => {}
                 other => {
@@ -1930,7 +2111,7 @@ pub(crate) fn synth(
             }
             // Body's type is the result type of the whole reuse-as
             // expression.
-            synth(body, env, locals, effects, in_def, subst, counter)
+            synth(body, env, locals, effects, in_def, subst, counter, residuals)
         }
     }
 }
@@ -2223,6 +2404,20 @@ pub struct Env {
     /// these names are legal as `Type::Var { name }` and unify only
     /// with themselves.
     pub rigid_vars: BTreeSet<String>,
+    /// Iter 22b.2 (Task 9): workspace-wide class-method table. Merged
+    /// from every module's [`ModuleGlobals::class_methods`] so that a
+    /// `Term::Var { name: "show" }` in any module resolves to the
+    /// declaring class's [`ClassMethodEntry`]. Method-name uniqueness
+    /// is enforced earlier by `workspace::build_registry`'s
+    /// method-name-collision check (Iter 22b.2.6), so the merge is
+    /// safe (no overwrites). Read in [`synth`]'s `Term::Var` arm.
+    pub class_methods: BTreeMap<String, ClassMethodEntry>,
+    /// 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<String, Option<String>>,
 }
 
 /// Back-pointer from a ctor name to the ADT that declared it. Stored

crates/ailang-check/src/lift.rs

@@ -684,7 +684,14 @@ impl<'a> Lifter<'a> {
         let mut subst = Subst::default();
         let mut counter: u32 = 0;
         let mut effects: BTreeSet<String> = BTreeSet::new();
-        let ty = synth(t, &self.env, locals, &mut effects, in_def, &mut subst, &mut counter)?;
+        // Iter 22b.2 (Task 9): the lift pass does its own type
+        // synthesis to figure out free-var types for letrec captures.
+        // Class-method residuals collected here are discarded — the
+        // missing-constraint check has already run for the enclosing
+        // fn during `check_fn`. Threading the accumulator only keeps
+        // `synth`'s signature uniform.
+        let mut residuals: Vec<crate::ResidualConstraint> = Vec::new();
+        let ty = synth(t, &self.env, locals, &mut effects, in_def, &mut subst, &mut counter, &mut residuals)?;
         Ok(subst.apply(&ty))
     }
 }