iter 22b.2.1: add Constraint struct, Type::Forall.constraints
This commit is contained in:
@@ -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() }),
|
||||
},
|
||||
);
|
||||
|
||||
@@ -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<String, Type>) -> 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<String, Type> = mapping
|
||||
.iter()
|
||||
@@ -145,6 +146,7 @@ fn substitute_rigids(t: &Type, mapping: &BTreeMap<String, Type>) -> 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<String>, 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<Stri
|
||||
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(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()],
|
||||
|
||||
@@ -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<String, Type>) -> Type {
|
||||
param_modes: vec![],
|
||||
ret_mode: ParamMode::Implicit,
|
||||
},
|
||||
Type::Forall { vars, body } => {
|
||||
Type::Forall { vars, constraints, body } => {
|
||||
let inner: BTreeMap<String, Type> = mapping
|
||||
.iter()
|
||||
.filter(|(k, _)| !vars.contains(k))
|
||||
@@ -875,6 +876,7 @@ fn substitute_rigids_local(t: &Type, mapping: &BTreeMap<String, Type>) -> Type {
|
||||
.collect();
|
||||
Type::Forall {
|
||||
vars: vars.clone(),
|
||||
constraints: constraints.clone(),
|
||||
body: Box::new(substitute_rigids_local(body, &inner)),
|
||||
}
|
||||
}
|
||||
|
||||
@@ -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<Type> = args
|
||||
.iter()
|
||||
.map(|a| self.synth_with_extras(a, extras))
|
||||
|
||||
@@ -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<String, Type>) -> 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<String, Type> = subst
|
||||
.iter()
|
||||
@@ -225,6 +226,7 @@ pub(crate) fn apply_subst_to_type(t: &Type, subst: &BTreeMap<String, Type>) -> T
|
||||
.collect();
|
||||
Type::Forall {
|
||||
vars: vars.clone(),
|
||||
constraints: constraints.clone(),
|
||||
body: Box::new(apply_subst_to_type(body, &inner)),
|
||||
}
|
||||
}
|
||||
|
||||
@@ -83,6 +83,7 @@ pub(crate) fn builtin_ail_type(name: &str) -> Option<Type> {
|
||||
// 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<Type> {
|
||||
// (`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,
|
||||
|
||||
@@ -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<String>,
|
||||
/// 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<Constraint>,
|
||||
body: Box<Type>,
|
||||
},
|
||||
}
|
||||
@@ -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,
|
||||
}
|
||||
}
|
||||
|
||||
@@ -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() }),
|
||||
|
||||
@@ -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}"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
@@ -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))
|
||||
}
|
||||
}
|
||||
|
||||
@@ -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() }),
|
||||
},
|
||||
),
|
||||
|
||||
@@ -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> a");
|
||||
|
||||
@@ -858,6 +858,7 @@ impl<'a> Parser<'a> {
|
||||
self.expect_rparen("forall-type")?;
|
||||
Ok(Type::Forall {
|
||||
vars,
|
||||
constraints: vec![],
|
||||
body: Box::new(body),
|
||||
})
|
||||
}
|
||||
|
||||
@@ -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(' ');
|
||||
|
||||
Reference in New Issue
Block a user