From de4cf47179fdd112d2524d3ac362a137aa2acbae Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20Christiansen=20S=C3=B8rby?= Date: Fri, 1 May 2026 17:38:36 +0200 Subject: [PATCH] fix(type): resolve type variable scoping in constrained instances - Collect type variables from constraints, instance args, and class constructor params before type checking, filtering out known names - Wrap impl types with forall bindings for proper polymorphism - Remove circular HAdd/Add constraint from Add class definition - Add pre-commit hooks for cargo test and monad test suite --- core/src/eval/type.rs | 73 ++++++++++++++++++++++++++++++++++++++--- core/src/term/module.rs | 4 +-- devenv.nix | 16 +++++++++ init/prelude.mo | 14 +++++--- 4 files changed, 95 insertions(+), 12 deletions(-) diff --git a/core/src/eval/type.rs b/core/src/eval/type.rs index bd2a1be..b8739ab 100644 --- a/core/src/eval/type.rs +++ b/core/src/eval/type.rs @@ -4,7 +4,7 @@ use crate::{ Map, Set, empty_set, set_of, term::{ Ann, ClassDefRef, Decl, Def, Identifier, Inductive, InductiveVariant, Instance, InstanceKey, - Literal, NameRef, Named, NumSuffix, SourceContext, + Literal, ModulePath, NameRef, Named, NumSuffix, SourceContext, Term::{Forall, Hole, Pi}, TypeConstraint, Typed, TypedTerm, VarRef, app, bvar, ctx, def, forall, lam_par, module::{LoadedModules, names_of_decls}, @@ -15,6 +15,14 @@ use crate::{ use super::*; +use crate::term::module::Scope; + +fn is_known_type_name(name: &ModulePath, scope: &Scope) -> bool { + scope.find_inductive(name).is_ok() + || scope.global().find_ref(name).is_some() + || scope.global().find_class_def(name).is_some() +} + #[derive(Debug, Clone, PartialEq)] pub enum TypeError { MismatchingBranches(Term, Term), @@ -226,8 +234,48 @@ pub fn type_check_instance<'a>( Err(Generic("wrong class name".into()))?; } + // Collect type variables from constraints and instance args FIRST + let mut type_vars: crate::Map = crate::Map::new(); + let default_type = Term::Type { universe: 0 }; + for constraint in &instance.constraints { + for var in constraint.vars() { + type_vars.insert(var.clone(), default_type.clone()); + } + } + for arg in &instance.args { + if let Term::Var { name } = arg { + if let Some(id) = name.as_id() { + let path = id.clone().to_path(); + if !is_known_type_name(&path, scope) { + type_vars.entry(id.clone()).or_insert(default_type.clone()); + } + } + } + } + + // Also collect free type variables from class constructor param types + let cons = class + .constructors + .first() + .expect("Class needs to have at least one constructor"); + for param in &cons.params { + let param_typ = param.typ(); + for fv in free_vars(param_typ, &empty_set()) { + let path = fv.clone().to_path(); + if !is_known_type_name(&path, scope) { + type_vars.entry(fv).or_insert(default_type.clone()); + } + } + } + + // Add type variables to scope BEFORE type checking args + let mut scope = scope.clone(); + for (var, typ) in &type_vars { + scope = scope.with_forall(var, typ); + } + for (param, arg) in class.params.iter().zip(instance.args.iter()) { - type_check(arg.clone(), *param.typ.clone(), scope)?; + type_check(arg.clone(), *param.typ.clone(), &scope)?; } let cons = class @@ -238,10 +286,11 @@ pub fn type_check_instance<'a>( for param in class_defs { if let Some(impl_def) = instance.impls_map.get_mut(¶m.name) { let class_def_type = param.typ(); - let typ = match_resolve_type(class_def_type, &impl_def.typ, scope)?; - let (term, _) = type_check(impl_def.term.clone(), typ.clone(), scope)?.to_tuple(); + let typ = match_resolve_type(class_def_type, &impl_def.typ, &scope)?; + let (term, _) = type_check(impl_def.term.clone(), typ.clone(), &scope)?.to_tuple(); impl_def.term = term; - impl_def.typ = typ; + // Wrap type with forall bindings for type variables + impl_def.typ = wrap_with_foralls(typ, &type_vars); } else { Err(MissingImplementation(param.name.clone()))?; } @@ -249,6 +298,20 @@ pub fn type_check_instance<'a>( Ok(instance) } +/// Wrap a type with forall bindings for the given type variables. +fn wrap_with_foralls(typ: Term, vars: &crate::Map) -> Term { + use crate::term::Term::Forall; + let mut result = typ; + for (name, param_typ) in vars { + result = Forall { + name: name.clone(), + typ: Box::new(param_typ.clone()), + body: Box::new(result), + }; + } + result +} + pub fn join_many_results(list: Vec>) -> (Vec, Vec) { let mut oks = Vec::new(); let mut errs = Vec::new(); diff --git a/core/src/term/module.rs b/core/src/term/module.rs index c509d71..1a0faac 100644 --- a/core/src/term/module.rs +++ b/core/src/term/module.rs @@ -947,13 +947,13 @@ impl<'a> GlobalScope<'a> { .impls_map .iter() .map(|(name, imp)| { - let name = instance + let full_name = instance .name .clone() .extend(ModulePath::single(name.clone())); DefRef { - name, + name: full_name, typ: &imp.typ, term: &imp.term, module, diff --git a/devenv.nix b/devenv.nix index ff8002a..77bb832 100644 --- a/devenv.nix +++ b/devenv.nix @@ -50,6 +50,22 @@ git-hooks.hooks = { rustfmt.enable = true; clippy.enable = true; + rust-tests = { + enable = true; + entry = '' + cargo test + ''; + pass_filenames = false; + files = "\\.(rs|mo)$"; + }; + monad-tests = { + enable = true; + entry = '' + cargo run -- test init/tests.mo + ''; + pass_filenames = false; + files = "\\.(rs|mo)$"; + }; }; # See full reference at https://devenv.sh/reference/options/ diff --git a/init/prelude.mo b/init/prelude.mo index bd8543c..e8cf2c8 100644 --- a/init/prelude.mo +++ b/init/prelude.mo @@ -18,14 +18,18 @@ class HAdd A B C { } /// Homogenous addition -class [HAdd A A A] Add A { +class Add A { def add : A -> A -> A } -// TODO: Fix scoping of type variables in constrained instances -// instance [Add A] HAdd A A A { -// def add (a b : A) : A := Add.add a b -// } +// TODO: Circular instances - Add/HAdd bridging is handled by concrete instances in number.mo + // instance [HAdd A A A] Add A { + // def add (a b : A) : A := HAdd.add a b + // } + + // instance [Add A] HAdd A A A { + // def add (a b : A) : A := Add.add a b + // } /// Heterogeneous multiplication class HMul A B C { -- 2.51.2