From b636b883a3c80bfc4735eddb79d5f9fb4103c1d7 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sat, 9 May 2026 17:34:39 +0200 Subject: [PATCH] iter 22b.2.1: add Constraint struct, Type::Forall.constraints --- crates/ailang-check/src/builtins.rs | 2 ++ crates/ailang-check/src/lib.rs | 23 ++++++++++++++------ crates/ailang-check/src/lift.rs | 4 +++- crates/ailang-codegen/src/lib.rs | 4 ++-- crates/ailang-codegen/src/subst.rs | 6 ++++-- crates/ailang-codegen/src/synth.rs | 2 ++ crates/ailang-core/src/ast.rs | 27 ++++++++++++++++++++--- crates/ailang-core/src/desugar.rs | 5 ++++- crates/ailang-core/src/hash.rs | 30 ++++++++++++++++++++++++++ crates/ailang-core/src/pretty.rs | 2 +- crates/ailang-core/tests/spec_drift.rs | 1 + crates/ailang-prose/src/lib.rs | 5 +++-- crates/ailang-surface/src/parse.rs | 1 + crates/ailang-surface/src/print.rs | 2 +- 14 files changed, 94 insertions(+), 20 deletions(-) diff --git a/crates/ailang-check/src/builtins.rs b/crates/ailang-check/src/builtins.rs index 74476c5..c1687ad 100644 --- a/crates/ailang-check/src/builtins.rs +++ b/crates/ailang-check/src/builtins.rs @@ -79,6 +79,7 @@ pub fn install(env: &mut crate::Env) { "==".into(), Type::Forall { vars: vec!["a".into()], + constraints: vec![], body: Box::new(Type::Fn { params: vec![ Type::Var { name: "a".into() }, @@ -112,6 +113,7 @@ pub fn install(env: &mut crate::Env) { "__unreachable__".into(), Type::Forall { vars: vec!["a".into()], + constraints: vec![], body: Box::new(Type::Var { name: "a".into() }), }, ); diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 74d2ef4..4a91e23 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -96,8 +96,9 @@ impl Subst { param_modes: vec![], ret_mode: ParamMode::Implicit, }, - Type::Forall { vars, body } => Type::Forall { + Type::Forall { vars, constraints, body } => Type::Forall { vars: vars.clone(), + constraints: constraints.clone(), body: Box::new(self.apply(body)), }, } @@ -136,7 +137,7 @@ fn substitute_rigids(t: &Type, mapping: &BTreeMap) -> Type { param_modes: vec![], ret_mode: ParamMode::Implicit, }, - Type::Forall { vars, body } => { + Type::Forall { vars, constraints, body } => { // Inner forall shadows: only substitute vars not re-bound here. let inner: BTreeMap = mapping .iter() @@ -145,6 +146,7 @@ fn substitute_rigids(t: &Type, mapping: &BTreeMap) -> Type { .collect(); Type::Forall { vars: vars.clone(), + constraints: constraints.clone(), body: Box::new(substitute_rigids(body, &inner)), } } @@ -1082,7 +1084,7 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> { // with themselves. An empty `vars` list (vacuously polymorphic) // gets normalised to a non-polymorphic body. let (rigids, inner_ty): (Vec, Type) = match &f.ty { - Type::Forall { vars, body } => (vars.clone(), (**body).clone()), + Type::Forall { vars, constraints: _, body } => (vars.clone(), (**body).clone()), other => (vec![], other.clone()), }; @@ -1337,7 +1339,7 @@ pub(crate) fn synth( Type::Fn { params, ret, effects: fx, .. } => { (params.clone(), (**ret).clone(), fx.clone()) } - Type::Forall { vars, body } => { + Type::Forall { vars, constraints: _, body } => { // Defensive — Var should already have instantiated. let (_, body) = instantiate(vars, body, counter); match &body { @@ -1797,7 +1799,7 @@ pub(crate) fn synth( /// If `t` is a `Forall`, instantiate it with fresh metavars; otherwise /// pass through unchanged. Used at every var-resolution site. fn maybe_instantiate(t: Type, counter: &mut u32) -> Type { - if let Type::Forall { vars, body } = &t { + if let Type::Forall { vars, constraints: _, body } = &t { let (_, inst) = instantiate(vars, body, counter); inst } else { @@ -1845,8 +1847,9 @@ fn qualify_local_types(t: &Type, owner_module: &str, local_types: &IndexMap Type::Forall { + Type::Forall { vars, constraints, body } => Type::Forall { vars: vars.clone(), + constraints: constraints.clone(), body: Box::new(qualify_local_types(body, owner_module, local_types)), }, Type::Var { .. } => t.clone(), @@ -2380,6 +2383,7 @@ mod tests { "id", Type::Forall { vars: vec!["a".into()], + constraints: vec![], body: Box::new(Type::Fn { params: vec![Type::Var { name: "a".into() }], ret: Box::new(Type::Var { name: "a".into() }), @@ -2405,6 +2409,7 @@ mod tests { "id", Type::Forall { vars: vec!["a".into()], + constraints: vec![], body: Box::new(Type::Fn { params: vec![Type::Var { name: "a".into() }], ret: Box::new(Type::Var { name: "a".into() }), @@ -2468,6 +2473,7 @@ mod tests { "id", Type::Forall { vars: vec!["a".into()], + constraints: vec![], body: Box::new(Type::Fn { params: vec![Type::Var { name: "a".into() }], ret: Box::new(Type::Var { name: "a".into() }), @@ -2516,6 +2522,7 @@ mod tests { "apply", Type::Forall { vars: vec!["a".into(), "b".into()], + constraints: vec![], body: Box::new(Type::Fn { params: vec![ Type::Fn { @@ -2649,6 +2656,7 @@ mod tests { name: "unbox".into(), ty: Type::Forall { vars: vec!["a".into()], + constraints: vec![], body: Box::new(Type::Fn { params: vec![Type::Con { name: "Box".into(), @@ -3708,6 +3716,7 @@ mod tests { "outer", Type::Forall { vars: vec!["a".into()], + constraints: vec![], body: Box::new(Type::Fn { params: vec![Type::Var { name: "a".into() }], ret: Box::new(Type::Var { name: "a".into() }), @@ -3788,7 +3797,7 @@ mod tests { // Original LetRec params: [Int]; captures (BTreeSet order): // x: a then z: Int (alphabetical). Ret: a. match &synth.ty { - Type::Forall { vars, body } => { + Type::Forall { vars, constraints: _, body } => { assert_eq!( vars, &vec!["a".to_string()], diff --git a/crates/ailang-check/src/lift.rs b/crates/ailang-check/src/lift.rs index 2c0d86b..4dabba0 100644 --- a/crates/ailang-check/src/lift.rs +++ b/crates/ailang-check/src/lift.rs @@ -558,6 +558,7 @@ impl<'a> Lifter<'a> { } else { Type::Forall { vars: self.current_def_forall_vars.clone(), + constraints: vec![], body: Box::new(inner_augmented_ty), } }; @@ -867,7 +868,7 @@ fn substitute_rigids_local(t: &Type, mapping: &BTreeMap) -> Type { param_modes: vec![], ret_mode: ParamMode::Implicit, }, - Type::Forall { vars, body } => { + Type::Forall { vars, constraints, body } => { let inner: BTreeMap = mapping .iter() .filter(|(k, _)| !vars.contains(k)) @@ -875,6 +876,7 @@ fn substitute_rigids_local(t: &Type, mapping: &BTreeMap) -> Type { .collect(); Type::Forall { vars: vars.clone(), + constraints: constraints.clone(), body: Box::new(substitute_rigids_local(body, &inner)), } } diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs index 2cf3fae..ee6f4fb 100644 --- a/crates/ailang-codegen/src/lib.rs +++ b/crates/ailang-codegen/src/lib.rs @@ -1845,7 +1845,7 @@ impl<'a> Emitter<'a> { )) })?; let (forall_vars, params, ret) = match &fdef.ty { - Type::Forall { vars, body } => match body.as_ref() { + Type::Forall { vars, constraints: _, body } => match body.as_ref() { Type::Fn { params, ret, .. } => { (vars.clone(), params.clone(), (**ret).clone()) } @@ -2434,7 +2434,7 @@ impl<'a> Emitter<'a> { let cty = self.synth_with_extras(callee, extras)?; match cty { Type::Fn { ret, .. } => Ok(*ret), - Type::Forall { vars, body } => { + Type::Forall { vars, constraints: _, body } => { let arg_tys: Vec = args .iter() .map(|a| self.synth_with_extras(a, extras)) diff --git a/crates/ailang-codegen/src/subst.rs b/crates/ailang-codegen/src/subst.rs index b502b7c..bbdcfe9 100644 --- a/crates/ailang-codegen/src/subst.rs +++ b/crates/ailang-codegen/src/subst.rs @@ -191,8 +191,9 @@ pub(crate) fn qualify_local_types_codegen( param_modes: vec![], ret_mode: ParamMode::Implicit, }, - Type::Forall { vars, body } => Type::Forall { + Type::Forall { vars, constraints, body } => Type::Forall { vars: vars.clone(), + constraints: constraints.clone(), body: Box::new(qualify_local_types_codegen(body, owner_module, owner_local_types)), }, Type::Var { .. } => t.clone(), @@ -216,7 +217,7 @@ pub(crate) fn apply_subst_to_type(t: &Type, subst: &BTreeMap) -> T param_modes: vec![], ret_mode: ParamMode::Implicit, }, - Type::Forall { vars, body } => { + Type::Forall { vars, constraints, body } => { // Inner forall shadows: don't substitute re-bound names. let inner: BTreeMap = subst .iter() @@ -225,6 +226,7 @@ pub(crate) fn apply_subst_to_type(t: &Type, subst: &BTreeMap) -> T .collect(); Type::Forall { vars: vars.clone(), + constraints: constraints.clone(), body: Box::new(apply_subst_to_type(body, &inner)), } } diff --git a/crates/ailang-codegen/src/synth.rs b/crates/ailang-codegen/src/synth.rs index 16b94ad..c3b5485 100644 --- a/crates/ailang-codegen/src/synth.rs +++ b/crates/ailang-codegen/src/synth.rs @@ -83,6 +83,7 @@ pub(crate) fn builtin_ail_type(name: &str) -> Option { // constant i1 1) on those resolved types. "==" => Type::Forall { vars: vec!["a".into()], + constraints: vec![], body: Box::new(Type::Fn { params: vec![ Type::Var { name: "a".into() }, @@ -105,6 +106,7 @@ pub(crate) fn builtin_ail_type(name: &str) -> Option { // (`forall a. a`). Mirrors the typechecker's `builtins::install`. "__unreachable__" => Type::Forall { vars: vec!["a".into()], + constraints: vec![], body: Box::new(Type::Var { name: "a".into() }), }, _ => return None, diff --git a/crates/ailang-core/src/ast.rs b/crates/ailang-core/src/ast.rs index 6356c5c..84032ad 100644 --- a/crates/ailang-core/src/ast.rs +++ b/crates/ailang-core/src/ast.rs @@ -331,6 +331,21 @@ pub struct InstanceMethod { pub body: Term, } +/// Iter 22b.2: a class constraint on a polymorphic function (Decision +/// 11). `(class, type)` pair where `class` is a class name and `type` +/// is a `Type` expression — typically a single `Type::Var` (e.g. +/// `(Eq, a)` for `Eq a => ...`). Concrete-type constraints are legal +/// schema-wise but fired as `no-instance` at typecheck time if no +/// matching registry entry exists. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct Constraint { + /// Class name. + pub class: String, + /// Type the class is applied to. + #[serde(rename = "type")] + pub type_: Type, +} + /// A constant (top-level binding to a value). /// /// Differs from a zero-arg [`FnDef`] in that it is evaluated once and @@ -588,6 +603,12 @@ pub enum Type { /// names, instantiated fresh at each use site. Forall { vars: Vec, + /// Iter 22b.2: class constraints quantified together with + /// `vars`. Empty for pre-22b.2 polymorphic types; serialised + /// with `skip_serializing_if = "Vec::is_empty"` so existing + /// canonical-JSON bytes stay bit-identical. + #[serde(default, skip_serializing_if = "Vec::is_empty")] + constraints: Vec, body: Box, }, } @@ -742,9 +763,9 @@ impl PartialEq for Type { } (Type::Var { name: a }, Type::Var { name: b }) => a == b, ( - Type::Forall { vars: a, body: ab }, - Type::Forall { vars: b, body: bb }, - ) => a == b && ab == bb, + Type::Forall { vars: a, constraints: ac, body: ab }, + Type::Forall { vars: b, constraints: bc, body: bb }, + ) => a == b && ac == bc && ab == bb, _ => false, } } diff --git a/crates/ailang-core/src/desugar.rs b/crates/ailang-core/src/desugar.rs index 9077cfa..b0eea34 100644 --- a/crates/ailang-core/src/desugar.rs +++ b/crates/ailang-core/src/desugar.rs @@ -774,6 +774,7 @@ impl Desugarer { } else { Type::Forall { vars: self.current_def_forall_vars.clone(), + constraints: vec![], body: Box::new(inner_augmented_ty), } }; @@ -2307,6 +2308,7 @@ mod tests { name: "rec_id".into(), ty: Type::Forall { vars: vec!["a".into()], + constraints: vec![], body: Box::new(Type::Fn { params: vec![Type::Var { name: "a".into() }], ret: Box::new(Type::Var { name: "a".into() }), @@ -2339,7 +2341,7 @@ mod tests { ); // Lifted type must be Forall(a). Fn(Int, a) -> a (k + x capture). match &lifted.ty { - Type::Forall { vars, body } => { + Type::Forall { vars, constraints: _, body } => { assert_eq!(vars, &vec!["a".to_string()], "Forall vars must mirror enclosing"); match body.as_ref() { Type::Fn { params, ret, .. } => { @@ -2409,6 +2411,7 @@ mod tests { name: "outer".into(), ty: Type::Forall { vars: vec!["a".into()], + constraints: vec![], body: Box::new(Type::Fn { params: vec![Type::Var { name: "a".into() }], ret: Box::new(Type::Var { name: "a".into() }), diff --git a/crates/ailang-core/src/hash.rs b/crates/ailang-core/src/hash.rs index 1070817..403daba 100644 --- a/crates/ailang-core/src/hash.rs +++ b/crates/ailang-core/src/hash.rs @@ -237,4 +237,34 @@ mod tests { "ClassDef with elided optionals must hash identically to construction with explicit None" ); } + + /// Iter 22b.2: adding `constraints` to [`crate::ast::Type::Forall`] + /// must NOT alter canonical-JSON bytes of any pre-22b.2 polymorphic + /// type. The `#[serde(default, skip_serializing_if = "Vec::is_empty")]` + /// attribute on the field is what enforces this; if it is wrong, + /// every existing fixture's hash drifts and workspace dedup keys + /// based on the canonical bytes break. + /// + /// Property: a `Type::Forall` constructed without specifying + /// `constraints` (i.e. empty vec) must serialise with no + /// `constraints` key in the canonical JSON. + #[test] + fn forall_without_constraints_hashes_bit_identical_to_pre_22b2() { + use crate::ast::Type; + let t = Type::Forall { + vars: vec!["a".into()], + constraints: vec![], + body: Box::new(Type::fn_implicit( + vec![Type::Var { name: "a".into() }], + Type::Var { name: "a".into() }, + vec![], + )), + }; + let bytes = crate::canonical::to_bytes(&t); + let s = std::str::from_utf8(&bytes).unwrap(); + assert!( + !s.contains("constraints"), + "Type::Forall serialised must omit `constraints` when empty; got: {s}" + ); + } } diff --git a/crates/ailang-core/src/pretty.rs b/crates/ailang-core/src/pretty.rs index 61bdbc8..c2e9562 100644 --- a/crates/ailang-core/src/pretty.rs +++ b/crates/ailang-core/src/pretty.rs @@ -154,7 +154,7 @@ pub fn type_to_string(t: &Type) -> String { }; format!("({p}) -> {ret}{eff}", ret = type_to_string(ret)) } - Type::Forall { vars, body } => { + Type::Forall { vars, constraints: _, body } => { format!("forall {}. {}", vars.join(" "), type_to_string(body)) } } diff --git a/crates/ailang-core/tests/spec_drift.rs b/crates/ailang-core/tests/spec_drift.rs index 7635e35..6e4f56d 100644 --- a/crates/ailang-core/tests/spec_drift.rs +++ b/crates/ailang-core/tests/spec_drift.rs @@ -190,6 +190,7 @@ fn spec_mentions_every_type_variant() { "(forall", Type::Forall { vars: vec!["a".into()], + constraints: vec![], body: Box::new(Type::Var { name: "a".into() }), }, ), diff --git a/crates/ailang-prose/src/lib.rs b/crates/ailang-prose/src/lib.rs index 11bd649..0ce8195 100644 --- a/crates/ailang-prose/src/lib.rs +++ b/crates/ailang-prose/src/lib.rs @@ -259,7 +259,7 @@ fn write_fn_def(out: &mut String, fd: &FnDef, level: usize) { // we render the forall on the line above and then the inner fn // signature. let (forall_vars, fn_ty) = match &fd.ty { - Type::Forall { vars, body } => (Some(vars.clone()), body.as_ref()), + Type::Forall { vars, constraints: _, body } => (Some(vars.clone()), body.as_ref()), other => (None, other), }; @@ -405,7 +405,7 @@ fn write_type(out: &mut String, t: &Type) { } } } - Type::Forall { vars, body } => { + Type::Forall { vars, constraints: _, body } => { out.push_str("forall<"); for (i, v) in vars.iter().enumerate() { if i > 0 { @@ -1445,6 +1445,7 @@ mod tests { fn type_forall_renders_with_angle_vars() { let t = Type::Forall { vars: vec!["a".into()], + constraints: vec![], body: Box::new(Type::Var { name: "a".into() }), }; assert_eq!(render_type(&t), "forall a"); diff --git a/crates/ailang-surface/src/parse.rs b/crates/ailang-surface/src/parse.rs index b4d9d1d..708cfbd 100644 --- a/crates/ailang-surface/src/parse.rs +++ b/crates/ailang-surface/src/parse.rs @@ -858,6 +858,7 @@ impl<'a> Parser<'a> { self.expect_rparen("forall-type")?; Ok(Type::Forall { vars, + constraints: vec![], body: Box::new(body), }) } diff --git a/crates/ailang-surface/src/print.rs b/crates/ailang-surface/src/print.rs index 647f28e..d41c268 100644 --- a/crates/ailang-surface/src/print.rs +++ b/crates/ailang-surface/src/print.rs @@ -296,7 +296,7 @@ fn write_type(out: &mut String, t: &Type) { } out.push(')'); } - Type::Forall { vars, body } => { + Type::Forall { vars, constraints: _, body } => { out.push_str("(forall (vars"); for v in vars { out.push(' ');