diff --git a/crates/ail/tests/typeclass_22b2.rs b/crates/ail/tests/typeclass_22b2.rs index b2c03b4..a283fcd 100644 --- a/crates/ail/tests/typeclass_22b2.rs +++ b/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::>() ); } + +/// 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::>() + ); +} diff --git a/crates/ailang-check/src/diagnostic.rs b/crates/ailang-check/src/diagnostic.rs index 906238b..dbba755 100644 --- a/crates/ailang-check/src/diagnostic.rs +++ b/crates/ailang-check/src/diagnostic.rs @@ -69,6 +69,14 @@ //! not include the residual class constraint. `ctx`: //! `{"class": "", "method": "", "at_type": ""}`. 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": "", "method": "", "at_type": ""}`. use serde::Serialize; diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 2c5b1b8..6280d3a 100644 --- a/crates/ailang-check/src/lib.rs +++ b/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": "", "method": "", "at_type": ""}`. + #[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 = std::result::Result; @@ -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, + /// 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 diff --git a/examples/test_22b2_no_instance.ail.json b/examples/test_22b2_no_instance.ail.json new file mode 100644 index 0000000..2c5005e --- /dev/null +++ b/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 } }] + } + } + ] +}