diff --git a/examples/Propa.myc b/examples/Propa.myc new file mode 100644 index 0000000..c672556 --- /dev/null +++ b/examples/Propa.myc @@ -0,0 +1,11 @@ + +(do + (def last (fn [s] (s 0))) + + (def f (fn [n] n)) + + (def r (series 5)) + (push r 4) + + [(last f) (last r)] +) diff --git a/src/ast/compiler/type_checker.rs b/src/ast/compiler/type_checker.rs index ff55265..d713c0c 100644 --- a/src/ast/compiler/type_checker.rs +++ b/src/ast/compiler/type_checker.rs @@ -95,7 +95,7 @@ impl TypeInferenceAccess for TypeChecker { } fn bind_typevar(&self, id: u32, ty: StaticType) { - self.subst.borrow_mut().insert(id, ty); + self.bind_var(id, ty); } fn apply_subst_ty(&self, ty: StaticType) -> StaticType { @@ -174,6 +174,17 @@ pub struct TypeChecker { /// Global substitution map: TypeVar ID → resolved StaticType. /// Shared across all scopes within a single type-checking pass. subst: std::cell::RefCell>, + /// Index-call constraints: callee_var → result_var. + /// + /// When a `TypeVar` is used as a callable with a single `Int` argument — + /// the series lookback pattern `(s 0)` — we record the pairing here instead + /// of eagerly unifying `TypeVar = Series(elem)`. The constraint is evaluated + /// lazily in `bind_var`: only when the callee TypeVar is bound to `Series(inner)` + /// is the result TypeVar also bound to `inner`. + /// + /// **Extension point**: other indexable types (e.g. `Stream`, future `Map`) + /// can participate by being matched in `bind_var`'s propagation arm. + index_constraints: std::cell::RefCell>, /// Type-inference and finalization hooks keyed by global slot index. /// Populated from the frozen RTL snapshot; empty for non-RTL call sites. call_hooks: Rc>, @@ -188,6 +199,7 @@ impl TypeChecker { root_types, var_counter: Cell::new(0), subst: std::cell::RefCell::new(HashMap::new()), + index_constraints: std::cell::RefCell::new(HashMap::new()), call_hooks, } } @@ -199,6 +211,28 @@ impl TypeChecker { StaticType::TypeVar(id) } + /// Binds a TypeVar to a concrete type in the substitution, then propagates + /// any pending index-call constraints registered by Step 9. + /// + /// When `ty` is `Series(inner)` and `index_constraints[id]` is set, the + /// result TypeVar is also bound to `inner` — connecting the callee TypeVar + /// to its element type without the eager over-constraint of unification. + /// + /// To add support for another indexable type (e.g. `Stream`), extend the + /// `match &ty` arm in the propagation block below. + fn bind_var(&self, id: u32, ty: StaticType) { + self.subst.borrow_mut().insert(id, ty.clone()); + let ret_id = self.index_constraints.borrow().get(&id).copied(); + if let Some(ret_id) = ret_id { + match &ty { + StaticType::Series(inner) => { + self.subst.borrow_mut().insert(ret_id, *inner.clone()); + } + _ => {} + } + } + } + /// Recursively applies the substitution map to a type, replacing all /// resolved `TypeVar`s with their concrete types. fn apply_subst(ty: StaticType, subst: &HashMap) -> StaticType { @@ -227,6 +261,13 @@ impl TypeChecker { StaticType::Tuple(elems) => { StaticType::Tuple(elems.into_iter().map(|t| Self::apply_subst(t, subst)).collect()) } + // Substitute into the body but skip over the bound vars: they are local to + // this schema and must not be replaced by the global substitution. + StaticType::Forall(vars, body) => { + let filtered: HashMap = + subst.iter().filter(|(k, _)| !vars.contains(k)).map(|(k, v)| (*k, v.clone())).collect(); + StaticType::Forall(vars, Box::new(Self::apply_subst(*body, &filtered))) + } other => other, } } @@ -254,6 +295,10 @@ impl TypeChecker { || Self::occurs(var_id, &sig.ret, subst) } StaticType::Tuple(elems) => elems.iter().any(|t| Self::occurs(var_id, t, subst)), + // A bound var inside Forall does not count as a free occurrence. + StaticType::Forall(vars, body) => { + !vars.contains(&var_id) && Self::occurs(var_id, body, subst) + } _ => false, } } @@ -262,7 +307,7 @@ impl TypeChecker { /// On success, the substitution is extended so that `ty1` and `ty2` become equal. /// On failure (type mismatch or occurs check), a diagnostic error is emitted. fn unify(&self, ty1: StaticType, ty2: StaticType, diag: &mut Diagnostics) { - let mut subst = self.subst.borrow_mut(); + let subst = self.subst.borrow_mut(); let ty1 = Self::apply_subst(ty1, &subst); let ty2 = Self::apply_subst(ty2, &subst); @@ -273,7 +318,10 @@ impl TypeChecker { diag.push_error(format!("Infinite type: ?{} = {}", n, ty), None); return; } - subst.insert(n, ty); + // Release the borrow before routing through bind_var so that + // constraint propagation can re-borrow subst without a panic. + drop(subst); + self.bind_var(n, ty); } (StaticType::Series(a), StaticType::Series(b)) => { drop(subst); @@ -296,9 +344,30 @@ impl TypeChecker { self.unify(ta, tb, diag); } } + // A homogeneous Vector is assignable from a Tuple — unify each element + // with the vector's inner type. Mirrors the `is_assignable_from` coercion. + (StaticType::Tuple(elems), StaticType::Vector(inner, len)) + | (StaticType::Vector(inner, len), StaticType::Tuple(elems)) => { + if elems.len() != len { + diag.push_error( + format!("Type mismatch: expected tuple of length {}, got {}", len, elems.len()), + None, + ); + return; + } + drop(subst); + for e in elems { + self.unify(e, (*inner).clone(), diag); + } + } // Any and Error are already handled by is_assignable_from — silently succeed (StaticType::Any, _) | (_, StaticType::Any) => {} (StaticType::Error, _) | (_, StaticType::Error) => {} + // Forall should be instantiated before unification; delegate to the body. + (StaticType::Forall(_, body), other) | (other, StaticType::Forall(_, body)) => { + drop(subst); + self.unify(*body, other, diag); + } (a, b) => { diag.push_error(format!("Type mismatch: expected {}, got {}", a, b), None); } @@ -357,11 +426,17 @@ impl TypeChecker { } } - /// Returns true if `ty` (or any element of a Tuple) contains a TypeVar. + /// Returns true if `ty` contains a TypeVar anywhere in its structure. fn has_typevar_component(ty: &StaticType) -> bool { match ty { StaticType::TypeVar(_) => true, - StaticType::Tuple(elems) => elems.iter().any(|e| matches!(e, StaticType::TypeVar(_))), + StaticType::Tuple(elems) => elems.iter().any(Self::has_typevar_component), + StaticType::Series(inner) | StaticType::Stream(inner) | StaticType::Optional(inner) => { + Self::has_typevar_component(inner) + } + StaticType::Function(sig) => { + Self::has_typevar_component(&sig.params) || Self::has_typevar_component(&sig.ret) + } _ => false, } } @@ -410,6 +485,117 @@ impl TypeChecker { Some(StaticType::Record(RecordLayout::get_or_create(promoted_fields))) } + /// Collects all free TypeVar IDs that appear in `ty`, following the substitution + /// chain and skipping variables bound by `Forall`. Deduplicates via `out`. + fn collect_free_tvars(ty: &StaticType, subst: &HashMap, out: &mut Vec) { + match ty { + StaticType::TypeVar(n) => { + if let Some(resolved) = subst.get(n) { + Self::collect_free_tvars(resolved, subst, out); + } else if !out.contains(n) { + out.push(*n); + } + } + StaticType::Series(inner) | StaticType::Stream(inner) | StaticType::Optional(inner) => { + Self::collect_free_tvars(inner, subst, out); + } + StaticType::Function(sig) => { + Self::collect_free_tvars(&sig.params, subst, out); + Self::collect_free_tvars(&sig.ret, subst, out); + } + StaticType::Tuple(elems) => { + for e in elems { + Self::collect_free_tvars(e, subst, out); + } + } + // Recurse into the body but skip the locally bound vars. + StaticType::Forall(vars, body) => { + let mut body_free = Vec::new(); + Self::collect_free_tvars(body, subst, &mut body_free); + for v in body_free { + if !vars.contains(&v) && !out.contains(&v) { + out.push(v); + } + } + } + _ => {} + } + } + + /// Collects all free TypeVar IDs that are currently visible in `ctx`. + /// Used by `generalize` to avoid quantifying TypeVars that are still shared + /// with other live bindings (series, scalars, outer function params). + fn ctx_free_tvars(ctx: &TypeContext, subst: &HashMap) -> Vec { + let mut out = Vec::new(); + for ty in ctx.slots.values() { + Self::collect_free_tvars(ty, subst, &mut out); + } + for ty in &ctx.upvalue_types { + Self::collect_free_tvars(ty, subst, &mut out); + } + for ty in ctx.root_types.borrow().iter() { + Self::collect_free_tvars(ty, subst, &mut out); + } + out + } + + /// Generalizes a type at a `def` boundary (Algorithm W `gen` step). + /// Wraps all TypeVars that are free in `ty` but NOT free in `ctx` into a + /// `Forall`. Value restriction: only call this for `Function`-typed values. + fn generalize(&self, ty: StaticType, ctx: &TypeContext) -> StaticType { + let subst = self.subst.borrow(); + let resolved = Self::apply_subst(ty, &subst); + let mut tvars_in_ty = Vec::new(); + Self::collect_free_tvars(&resolved, &subst, &mut tvars_in_ty); + let ctx_tvars = Self::ctx_free_tvars(ctx, &subst); + let quantified: Vec = tvars_in_ty.into_iter() + .filter(|v| !ctx_tvars.contains(v)) + .collect(); + if quantified.is_empty() { + resolved + } else { + StaticType::Forall(quantified, Box::new(resolved)) + } + } + + /// Instantiates a `Forall` type by replacing each bound TypeVar with a + /// fresh one (Algorithm W `inst` step). No-op for non-`Forall` types. + /// + /// Also remaps any index-call constraints: if `index_constraints[old] = ret` + /// and both `old` and `ret` are bound vars, the fresh copies inherit the + /// same pairing so that `bind_var` propagation keeps working at each call site. + fn instantiate(&self, ty: StaticType) -> StaticType { + let StaticType::Forall(vars, body) = ty else { return ty }; + let mut local_subst: HashMap = HashMap::new(); + let mut var_mapping: HashMap = HashMap::new(); + for v in &vars { + let fresh = self.fresh_var(); + if let StaticType::TypeVar(fresh_id) = &fresh { + var_mapping.insert(*v, *fresh_id); + } + local_subst.insert(*v, fresh); + } + // Copy index-call constraints for the freshly created TypeVars. + // Both the callee-var and its result-var must be in vars for the + // mapping to apply; partial remaps are dropped (they can't occur in + // a well-formed Forall, but the guard is cheap insurance). + let new_constraints: Vec<(u32, u32)> = { + let constraints = self.index_constraints.borrow(); + vars.iter() + .filter_map(|v| { + let new_v = *var_mapping.get(v)?; + let old_ret = *constraints.get(v)?; + let new_ret = *var_mapping.get(&old_ret)?; + Some((new_v, new_ret)) + }) + .collect() + }; + for (new_v, new_ret) in new_constraints { + self.index_constraints.borrow_mut().insert(new_v, new_ret); + } + Self::apply_subst(*body, &local_subst) + } + /// Walks the typed AST, applies the HM substitution to every type annotation, /// and dispatches finalization hooks (e.g. schema injection for `series`). fn finalize_node(&self, node: TypedNode, subst: &HashMap) -> TypedNode { @@ -881,13 +1067,20 @@ impl TypeChecker { let val_typed = self.check_node(value, ctx, diag); let ty = val_typed.ty.clone(); - // Extract addr from pattern to register the type + // Extract addr from pattern to register the type. + // Value restriction: only Function-typed values are generalized to Forall. + // Mutable state (Series, scalars) must remain monomorphic. if let NodeKind::Identifier { binding: IdentifierBinding::Declaration { addr, .. }, .. } = &pattern.kind { - ctx.set_type(*addr, ty.clone()); + let stored_ty = if matches!(ty, StaticType::Function(..)) { + self.generalize(ty.clone(), ctx) + } else { + ty.clone() + }; + ctx.set_type(*addr, stored_ty); } // For destructuring defs, check params on the pattern @@ -949,7 +1142,10 @@ impl TypeChecker { // Apply the current HM substitution so that TypeVars resolved in // nested scopes (e.g. inside a `while` body) are visible here even // when ctx.set_type could not propagate back through an upvalue address. + // Instantiate Forall types: each use site gets fresh TypeVars so that + // calls with different argument types remain independent. let ty = Self::apply_subst(ctx.get_type(*addr), &self.subst.borrow()); + let ty = self.instantiate(ty); ( NodeKind::Identifier { symbol: symbol.clone(), @@ -1225,6 +1421,42 @@ impl TypeChecker { // e.g. `(+ Float TypeVar(1))` resolves TypeVar(1) = Float. self.unify_matched_overload(&callee_typed.ty, &args_typed.ty, diag); + // HM step 9: when a TypeVar is called with a single Int argument + // (series lookback indexing pattern), record a lazy index-call constraint + // instead of eagerly unifying `TypeVar = Series(elem)`. + // + // The constraint pair (callee_var → result_var) is stored in + // `index_constraints`. When `bind_var` later resolves callee_var to + // `Series(inner)`, it automatically binds result_var to `inner`. + // + // This avoids over-constraining the function to Series-only: passing + // any other callable (e.g. a Function) simply leaves result_var + // unresolved and the call returns `Any` — no spurious type error. + if let StaticType::TypeVar(n) = &callee_typed.ty { + let is_index_call = matches!(&args_typed.ty, + StaticType::Tuple(elems) if elems.len() == 1 + && matches!(&elems[0], StaticType::Int) + ); + if is_index_call && matches!(ret_ty, StaticType::Any) { + let elem_var = self.fresh_var(); + let StaticType::TypeVar(elem_id) = &elem_var else { unreachable!() }; + self.index_constraints.borrow_mut().insert(*n, *elem_id); + ret_ty = elem_var; + } + } + + // HM step 10: unify Function parameter types with actual argument types, + // but only when the signature still contains TypeVars to resolve. + // Skip for fully concrete signatures (e.g. fn([any any])) to avoid + // false conflicts between Tuple and Vector representations. + if let StaticType::Function(sig) = &callee_typed.ty + && Self::has_typevar_component(&sig.params) + { + let params = sig.params.clone(); + self.unify(params, args_typed.ty.clone(), diag); + ret_ty = Self::apply_subst(ret_ty, &self.subst.borrow()); + } + // Dispatch post-call hooks registered by the RTL (keyed by global slot index). // Hooks handle type-inference extensions such as: // - series: inject a fresh TypeVar for the element type diff --git a/src/ast/types.rs b/src/ast/types.rs index 4bc4969..4b65cc4 100644 --- a/src/ast/types.rs +++ b/src/ast/types.rs @@ -376,6 +376,12 @@ pub enum StaticType { /// An unresolved type variable used during Hindley-Milner type inference. /// The `u32` is a unique ID assigned by the type checker. Resolved via substitution. TypeVar(u32), + /// A universally quantified type (let-polymorphism / HM generalization). + /// Created at `def` boundaries for function values; instantiated with fresh TypeVars + /// at each use site so calls with different types remain independent. + /// Value restriction: only `Function`-typed defs are generalized — mutable state + /// (series, scalars) must remain monomorphic. + Forall(Vec, Box), /// A diagnostic poison type, allowing type-checking to continue after an error. Error, } @@ -436,6 +442,14 @@ impl fmt::Display for StaticType { StaticType::Object(name) => write!(f, "{}", name), StaticType::PolymorphicFn { .. } => write!(f, ""), StaticType::TypeVar(n) => write!(f, "?{}", n), + StaticType::Forall(vars, body) => { + write!(f, "∀")?; + for (i, v) in vars.iter().enumerate() { + if i > 0 { write!(f, ",")?; } + write!(f, "?{}", v)?; + } + write!(f, ". {}", body) + } StaticType::Error => write!(f, ""), } } @@ -485,6 +499,8 @@ impl StaticType { || matches!(other, StaticType::Error) || matches!(self, StaticType::TypeVar(_)) || matches!(other, StaticType::TypeVar(_)) + || matches!(self, StaticType::Forall(..)) + || matches!(other, StaticType::Forall(..)) { return true; } @@ -599,6 +615,9 @@ impl StaticType { .map(|sig| sig.ret.clone()), StaticType::PolymorphicFn { resolve_return, .. } => resolve_return(args_ty), StaticType::TypeVar(_) => Some(StaticType::Any), + // Forall should be instantiated before resolve_call is reached. + // This fallback delegates to the body as a safety net. + StaticType::Forall(_, body) => body.resolve_call(args_ty), // Lookback indexing: (my-series 0) → element type StaticType::Series(inner) => { let is_int = matches!( diff --git a/tests/hm_poly.rs b/tests/hm_poly.rs index 4b5dc8d..c2bffac 100644 --- a/tests/hm_poly.rs +++ b/tests/hm_poly.rs @@ -189,3 +189,29 @@ fn test_let_poly_generic_return_used_in_field_series() { other => panic!("Expected Float(42.0), got {:?}", other), } } + +/// Regression test: passing a non-series callable to a generic `last` function +/// must NOT produce a type error. Before the index-constraint fix, Step 9 would +/// eagerly unify `TypeVar = Series(elem)`, making `last` Series-only and causing +/// a spurious conflict when a Function-typed variable was passed. +/// +/// After the fix, `last` is inferred as `∀α β. fn(α) → β` with a lazy constraint: +/// only when `α` resolves to `Series(inner)` does `β` also resolve to `inner`. +/// For any other callable, `β` stays unbound and the return type is `Any`. +#[test] +fn test_let_poly_non_series_callable_no_false_positive() { + let env = Environment::new(); + let source = r#" + (do + (def f (fn [n] (n))) + (def last (fn [s] (s 0))) + (last f) + ) + "#; + let result = env.compile(source); + assert!( + !result.diagnostics.has_errors(), + "Passing a non-series callable to a generic function must not produce a type error: {}", + result.diagnostics.format_errors() + ); +}