iter 22b.2.10: no-instance per-fn diagnostic

crates/ail/tests/typeclass_22b2.rs

@@ -212,3 +212,26 @@ fn fn_with_superclass_constraint_calling_subclass_method_fires_missing_constrain
         diagnostics.iter().map(|d| &d.code).collect::<Vec<_>>()
     );
 }
+
+/// Property protected: a (monomorphic) fn that calls a class method at a
+/// fully-concrete type for which no `instance C T` exists in the workspace
+/// MUST receive a `no-instance` diagnostic. This is the dual of
+/// `missing-constraint`: when the residual class constraint resolves to a
+/// concrete type, the fn cannot push the obligation to a caller via a
+/// `Forall.constraints` annotation — it can only be discharged by an
+/// existing instance. Without this check, monomorphisation in 22b.3 would
+/// have nothing to specialise to. Fixture: `main` calls `show 42` (so the
+/// residual is `(Show, Int)`) without any `instance Show Int` declared in
+/// the workspace.
+#[test]
+fn fn_calling_class_method_at_type_without_instance_fires_no_instance() {
+    let entry = examples_dir().join("test_22b2_no_instance.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 == "no-instance"),
+        "expected no-instance; got: {:?}",
+        diagnostics.iter().map(|d| &d.code).collect::<Vec<_>>()
+    );
+}

crates/ailang-check/src/diagnostic.rs

@@ -69,6 +69,14 @@
 //!   not include the residual class constraint. `ctx`:
 //!   `{"class": "<C>", "method": "<m>", "at_type": "<a>"}`. Concrete-
 //!   type residuals are deferred to the `no-instance` diagnostic.
+//! - `no-instance` (Iter 22b.2) — `severity: error`. Emitted by the
+//!   per-fn typecheck arm when a class-method call resolves the class
+//!   param to a fully-concrete type that has no matching entry in the
+//!   workspace instance registry (`(class, canonical-type-hash)`).
+//!   Dual of `missing-constraint`: when the residual is concrete, the
+//!   fn cannot push the obligation to a caller, so an existing
+//!   instance is the only way to discharge it. `ctx`:
+//!   `{"class": "<C>", "method": "<m>", "at_type": "<T>"}`.
 
 use serde::Serialize;
 

crates/ailang-check/src/lib.rs

@@ -464,6 +464,27 @@ pub enum CheckError {
         class: String,
         at_type: String,
     },
+
+    /// Iter 22b.2 (Task 10): a `FnDef` calls a class method at a
+    /// fully-concrete type (e.g. `show 42` resolves the residual class
+    /// param to `Int`), but the workspace registry has no
+    /// `instance class at_type` entry. This is the dual of
+    /// `MissingConstraint`: when the residual type is concrete, the fn
+    /// cannot push the obligation to a caller via `Forall.constraints`
+    /// — it can only be discharged by an existing instance. Without a
+    /// matching registry entry, monomorphisation (22b.3) would have no
+    /// dictionary to substitute. Code: `no-instance`. `ctx`:
+    /// `{"class": "<C>", "method": "<m>", "at_type": "<T>"}`.
+    #[error(
+        "fn `{def}` calls `{method}` requiring `instance {class} {at_type}`, \
+        but no such instance exists in the workspace"
+    )]
+    NoInstance {
+        def: String,
+        method: String,
+        class: String,
+        at_type: String,
+    },
 }
 
 pub(crate) type Result<T> = std::result::Result<T, CheckError>;
@@ -503,6 +524,7 @@ impl CheckError {
             CheckError::AmbiguousCtor { .. } => "ambiguous-ctor",
             CheckError::ReuseAsNonAllocatingBody { .. } => "reuse-as-non-allocating-body",
             CheckError::MissingConstraint { .. } => "missing-constraint",
+            CheckError::NoInstance { .. } => "no-instance",
         }
     }
 
@@ -546,6 +568,9 @@ impl CheckError {
             CheckError::MissingConstraint { class, method, at_type, .. } => {
                 serde_json::json!({"class": class, "method": method, "at_type": at_type})
             }
+            CheckError::NoInstance { class, method, at_type, .. } => {
+                serde_json::json!({"class": class, "method": method, "at_type": at_type})
+            }
             _ => serde_json::Value::Object(serde_json::Map::new()),
         }
     }
@@ -1150,9 +1175,13 @@ fn check_in_workspace(
         }
     }
     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.
+    // Iter 22b.2 (Task 10): thread the workspace-load-time instance
+    // registry into the env so `check_fn`'s concrete-residual path can
+    // look up `(class, type_hash)` keys for the no-instance check.
+    env.workspace_registry = ws.registry.clone();
+    // Workspace isn't otherwise needed in the env; cross-module lookup
+    // uses only `module_globals` / `module_types`. The ws reference is
+    // preserved in case cross-module ADTs are added later.
     let _ = ws;
 
     for def in &m.defs {
@@ -1371,11 +1400,52 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> {
                     at_type: name.clone(),
                 });
             }
+        } else if is_fully_concrete(&r_ty) {
+            // Iter 22b.2 (Task 10): fully-concrete residual — the class
+            // method was called at a concrete type, so the obligation
+            // can only be discharged by an existing workspace instance.
+            // Look up `(class, type_hash(r_ty))` in the registry; absence
+            // → no-instance. The hash uses `canonical::type_hash`, the
+            // same key shape `workspace::build_registry` writes with, so
+            // representation-equal types match deterministically.
+            let key = (
+                r.class.clone(),
+                ailang_core::canonical::type_hash(&r_ty),
+            );
+            if !env.workspace_registry.entries.contains_key(&key) {
+                return Err(CheckError::NoInstance {
+                    def: f.name.clone(),
+                    method: r.method.clone(),
+                    class: r.class.clone(),
+                    at_type: ailang_core::pretty::type_to_string(&r_ty),
+                });
+            }
         }
+        // Other shapes (unsolved metavars inside a `Type::Con`,
+        // `Type::Fn`, `Type::Forall`) are out of scope for the 22b.2
+        // diagnostics: metavars mean the body never connected the
+        // class param to anything observable, and `Fn`/`Forall` cannot
+        // appear as instance heads (Decision 11).
     }
     Ok(())
 }
 
+/// Iter 22b.2 (Task 10): true iff the type tree contains no `Type::Var`
+/// at any depth. A fully-concrete type is the only shape eligible for
+/// the no-instance lookup — anything carrying a metavar / rigid-var
+/// component is either covered by the missing-constraint check or
+/// genuinely under-specified at the call site.
+fn is_fully_concrete(t: &Type) -> bool {
+    match t {
+        Type::Con { args, .. } => args.iter().all(is_fully_concrete),
+        Type::Var { .. } => false,
+        Type::Fn { params, ret, .. } => {
+            params.iter().all(is_fully_concrete) && is_fully_concrete(ret)
+        }
+        Type::Forall { body, .. } => is_fully_concrete(body),
+    }
+}
+
 /// 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
@@ -2418,6 +2488,15 @@ pub struct Env {
     /// (Decision 11: max one step). The schema permits at most one
     /// superclass per class.
     pub class_superclasses: BTreeMap<String, String>,
+    /// Iter 22b.2 (Task 10): workspace-wide instance registry, threaded
+    /// through from [`Workspace::registry`]. Read by [`check_fn`] in the
+    /// concrete-residual path: when a class-method call at a fully-
+    /// concrete type produces a residual `(class, type_)` whose
+    /// `(class, type_hash(type_))` key is absent from `registry.entries`,
+    /// the fn fires `NoInstance`. Default-constructed (empty) for
+    /// the standalone [`check_module`] entry point — pre-22b fixtures
+    /// never invoke class methods, so the empty registry is harmless.
+    pub workspace_registry: ailang_core::workspace::Registry,
 }
 
 /// Back-pointer from a ctor name to the ADT that declared it. Stored

examples/test_22b2_no_instance.ail.json

@@ -0,0 +1,39 @@
+{
+  "schema": "ailang/v0",
+  "name": "test_22b2_no_instance",
+  "imports": [],
+  "defs": [
+    {
+      "kind": "class",
+      "name": "Show",
+      "param": "a",
+      "methods": [
+        {
+          "name": "show",
+          "type": {
+            "k": "fn",
+            "params": [{ "k": "var", "name": "a" }],
+            "ret": { "k": "con", "name": "Str" },
+            "effects": []
+          }
+        }
+      ]
+    },
+    {
+      "kind": "fn",
+      "name": "main",
+      "type": {
+        "k": "fn",
+        "params": [],
+        "ret": { "k": "con", "name": "Str" },
+        "effects": []
+      },
+      "params": [],
+      "body": {
+        "t": "app",
+        "fn": { "t": "var", "name": "show" },
+        "args": [{ "t": "lit", "lit": { "kind": "int", "value": 42 } }]
+      }
+    }
+  ]
+}