From d6084a71fb085cb91cdadc8376196e76d52418e3 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sat, 9 May 2026 20:41:45 +0200 Subject: [PATCH] =?UTF-8?q?iter=2022b.3.4:=20synthesise=5Fmono=5Ffn=20?= =?UTF-8?q?=E2=80=94=20instance=20body=20+=20class=20default=20fallback?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- crates/ail/tests/typeclass_22b3.rs | 124 +++++++++++++++++++++++++++++ crates/ailang-check/src/lib.rs | 10 ++- crates/ailang-check/src/mono.rs | 101 ++++++++++++++++++++++- 3 files changed, 232 insertions(+), 3 deletions(-) diff --git a/crates/ail/tests/typeclass_22b3.rs b/crates/ail/tests/typeclass_22b3.rs index 909d9a6..b414219 100644 --- a/crates/ail/tests/typeclass_22b3.rs +++ b/crates/ail/tests/typeclass_22b3.rs @@ -183,3 +183,127 @@ fn mono_symbol_compound_type_uses_hash_suffix() { let again = ailang_check::mono::mono_symbol("show", &pair_ty); assert_eq!(name, again, "mono_symbol must be deterministic"); } + +/// Property: synthesise_mono_fn copies the matching instance method's +/// body verbatim and produces a fully-concrete `FnDef` whose name uses +/// the `mono_symbol` form, whose `ty` is the class method's declared +/// type with the class param substituted to the target type, and whose +/// `params` / `body` come from the instance's `Term::Lam`. +#[test] +fn synthesise_mono_fn_uses_instance_body_lam() { + use ailang_check::mono::{synthesise_mono_fn, MonoTarget}; + use ailang_core::ast::{ClassDef, ClassMethod, InstanceDef, InstanceMethod, Term}; + + let class_def = ClassDef { + name: "Foo".into(), + param: "a".into(), + superclass: None, + methods: vec![ClassMethod { + name: "bar".into(), + ty: Type::Fn { + params: vec![Type::Var { name: "a".into() }], + ret: Box::new(Type::int()), + effects: vec![], + param_modes: vec![], + ret_mode: ailang_core::ast::ParamMode::Implicit, + }, + default: None, + }], + doc: None, + }; + let instance = InstanceDef { + class: "Foo".into(), + type_: Type::int(), + methods: vec![InstanceMethod { + name: "bar".into(), + body: Term::Lam { + params: vec!["i".into()], + param_tys: vec![Type::Var { name: "a".into() }], + ret_ty: Box::new(Type::int()), + effects: vec![], + body: Box::new(Term::Var { name: "i".into() }), + }, + }], + doc: None, + }; + let target = MonoTarget { + class: "Foo".into(), + method: "bar".into(), + type_: Type::int(), + defining_module: "m".into(), + }; + + let f = synthesise_mono_fn(&target, &class_def, &instance).expect("synth"); + assert_eq!(f.name, "bar#Int"); + assert!( + matches!( + &f.ty, + Type::Fn { params, ret, .. } + if params.len() == 1 + && matches!(¶ms[0], Type::Con { name, args } if name == "Int" && args.is_empty()) + && matches!(ret.as_ref(), Type::Con { name, args } if name == "Int" && args.is_empty()) + ), + "ty = {:?}", + f.ty + ); + assert_eq!(f.params, vec!["i".to_string()]); + assert!( + matches!(&f.body, Term::Var { name } if name == "i"), + "body = {:?}", + f.body + ); +} + +/// Property: when the instance omits a method that has a class-level +/// `default` body, synthesise_mono_fn falls back to that default and +/// uses its params/body verbatim — registry-build's `MissingMethod` +/// has already enforced that one of the two is present. +#[test] +fn synthesise_mono_fn_falls_back_to_class_default() { + use ailang_check::mono::{synthesise_mono_fn, MonoTarget}; + use ailang_core::ast::{ClassDef, ClassMethod, InstanceDef, Literal, Term}; + + let class_def = ClassDef { + name: "Greet".into(), + param: "a".into(), + superclass: None, + methods: vec![ClassMethod { + name: "hello".into(), + ty: Type::Fn { + params: vec![Type::Var { name: "a".into() }], + ret: Box::new(Type::str_()), + effects: vec![], + param_modes: vec![], + ret_mode: ailang_core::ast::ParamMode::Implicit, + }, + default: Some(Term::Lam { + params: vec!["_x".into()], + param_tys: vec![Type::Var { name: "a".into() }], + ret_ty: Box::new(Type::str_()), + effects: vec![], + body: Box::new(Term::Lit { + lit: Literal::Str { value: "hi".into() }, + }), + }), + }], + doc: None, + }; + // Instance carries no `hello` body — must fall back to default. + let instance = InstanceDef { + class: "Greet".into(), + type_: Type::int(), + methods: vec![], + doc: None, + }; + let target = MonoTarget { + class: "Greet".into(), + method: "hello".into(), + type_: Type::int(), + defining_module: "m".into(), + }; + + let f = synthesise_mono_fn(&target, &class_def, &instance).expect("synth"); + assert_eq!(f.name, "hello#Int"); + assert_eq!(f.params, vec!["_x".to_string()]); + assert!(matches!(&f.body, Term::Lit { .. }), "body = {:?}", f.body); +} diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 5727081..295bb8b 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -123,7 +123,7 @@ fn instantiate(forall_vars: &[String], body: &Type, counter: &mut u32) -> (Vec) -> Type { +pub(crate) fn substitute_rigids(t: &Type, mapping: &BTreeMap) -> Type { match t { Type::Var { name } => mapping.get(name).cloned().unwrap_or_else(|| t.clone()), Type::Con { name, args } => Type::Con { @@ -487,6 +487,13 @@ pub enum CheckError { class: String, at_type: String, }, + + /// Iter 22b.3: an internal invariant in the typechecker / mono pass + /// was violated — surfaced as an error so callers can propagate + /// rather than abort, but in well-formed inputs (typecheck has + /// succeeded) it must never fire. Code: `internal`. + #[error("internal: {0}")] + Internal(String), } pub(crate) type Result = std::result::Result; @@ -527,6 +534,7 @@ impl CheckError { CheckError::ReuseAsNonAllocatingBody { .. } => "reuse-as-non-allocating-body", CheckError::MissingConstraint { .. } => "missing-constraint", CheckError::NoInstance { .. } => "no-instance", + CheckError::Internal(_) => "internal", } } diff --git a/crates/ailang-check/src/mono.rs b/crates/ailang-check/src/mono.rs index 66ed426..d5d899e 100644 --- a/crates/ailang-check/src/mono.rs +++ b/crates/ailang-check/src/mono.rs @@ -51,11 +51,11 @@ //! the implementation so the constraint is visible to anyone //! extending the skeleton. -use ailang_core::ast::{Def, FnDef as AstFnDef, Type}; +use ailang_core::ast::{ClassDef, Def, FnDef as AstFnDef, InstanceDef, Term, Type}; use ailang_core::workspace::Workspace; use crate::Result; use indexmap::IndexMap; -use std::collections::BTreeSet; +use std::collections::{BTreeMap, BTreeSet}; /// Iter 22b.3: workspace-wide monomorphisation pass entry. See the /// module-level doc for the architecture and contract. @@ -287,3 +287,100 @@ pub fn collect_mono_targets( } Ok(out) } + +/// Iter 22b.3: produce a `FnDef` for a single (target, class, +/// instance) triple. The synthesised fn: +/// +/// 1. has name [`mono_symbol`]`(target.method, target.type_)`, +/// 2. has type = the class's method type with the class param +/// substituted to `target.type_` (rigid-var substitution via +/// [`crate::substitute_rigids`]); the result is a plain +/// `Type::Fn` with no `Forall`, +/// 3. has params + body taken from the instance's matching +/// `InstanceMethod.body` if present and Lam-shaped; from the +/// class's `default` body if the instance omits the method; +/// or directly from the body if the method has no params +/// (zero-arg method types). +/// +/// Errors (all [`crate::CheckError::Internal`] — caller-contract +/// violations that cannot occur after typecheck has succeeded): +/// +/// - The instance omits the method AND the class has no `default` +/// — unreachable in practice because +/// `workspace::build_registry`'s `MissingMethod` check fires at +/// load. +/// - The class itself has no method by that name — also caught at +/// load. +/// - The method type is `(args) -> ret` with `args` non-empty but +/// the resolved body is not [`Term::Lam`] — schema-shape +/// mismatch enforced by 22b.2's instance-method check. +pub fn synthesise_mono_fn( + target: &MonoTarget, + class_def: &ClassDef, + instance: &InstanceDef, +) -> Result { + // Locate the class method declaration. + let class_method = class_def + .methods + .iter() + .find(|m| m.name == target.method) + .ok_or_else(|| { + crate::CheckError::Internal(format!( + "synthesise_mono_fn: class `{}` has no method `{}`", + class_def.name, target.method + )) + })?; + + // Build the substitution `param := target.type_` and apply it + // to the method type. The result is a concrete `Type::Fn` (no + // `Forall`). + let mut mapping: BTreeMap = BTreeMap::new(); + mapping.insert(class_def.param.clone(), target.type_.clone()); + let concrete_method_ty = crate::substitute_rigids(&class_method.ty, &mapping); + + // Resolve the body — instance override first, then class default. + let body_term: Term = match instance.methods.iter().find(|im| im.name == target.method) { + Some(im) => im.body.clone(), + None => class_method.default.clone().ok_or_else(|| { + crate::CheckError::Internal(format!( + "synthesise_mono_fn: instance `{} {}` omits method `{}` and class has no \ + default (registry-build should have rejected this)", + target.class, + ailang_core::pretty::type_to_string(&target.type_), + target.method, + )) + })?, + }; + + // Decide the (params, body) shape based on whether the method + // type takes positional args. + let method_has_params = matches!( + &class_method.ty, + Type::Fn { params, .. } if !params.is_empty() + ); + let (params, body): (Vec, Term) = if method_has_params { + // Method has positional params — body must be a Lam. + match body_term { + Term::Lam { params, body, .. } => (params, *body), + other => { + return Err(crate::CheckError::Internal(format!( + "synthesise_mono_fn: method `{}` has positional params but body is not \ + a Lam: {:?}", + target.method, other + ))); + } + } + } else { + // Zero-arg method — body is the value directly. + (Vec::new(), body_term) + }; + + Ok(AstFnDef { + name: mono_symbol(&target.method, &target.type_), + ty: concrete_method_ty, + params, + body, + doc: None, + suppress: Vec::new(), + }) +}