Add Forall type for polymorphism

Introduce `StaticType::Forall` to represent universally quantified
types. This enables Hindley-Milner's let-polymorphism, allowing
functions to be generalized and reused with different concrete types.

- **Generalization at `def`:** Function values are now generalized using
  `self.generalize` when they are defined, wrapping their type in
  `Forall`. This occurs at `def` boundaries.
- **Instantiation at use:** Function types are instantiated with fresh
  type variables at each call site using `self.instantiate`. This
  ensures that different uses of the same polymorphic function do not
  interfere with each other's type inference.
- **Value restriction:** Only function-typed definitions are
  generalized. Mutable state like series and scalars remain monomorphic
  to prevent unexpected behavior.
- **Type context awareness:** The `generalize` function considers the
  current type context to avoid quantifying type variables that are
  still in use elsewhere.
  Feat: Add Forall type for polymorphism

Introduces the `Forall` type to support polymorphic functions and enable
let-polymorphism.

- `Forall(vars, body)`: Represents a universally quantified type where
  `vars` are the type variables bound by this quantification, and `body`
  is the type itself.
- `TypeChecker::generalize`: Wraps a type in `Forall` when a `def`
  boundary is encountered for function-typed values. This ensures that
  each use site of a polymorphic function gets its own instantiation.
- `TypeChecker::instantiate`: Replaces the type variables within a
  `Forall` type with fresh ones. This is performed at each call site of
  a polymorphic function.
- Updates `TypeChecker::unify` and `TypeChecker::apply_subst` to
  correctly handle `Forall` types, ensuring that bound variables within
  a `Forall` are not affected by global substitutions and that `Forall`
  types are instantiated before unification.
- Adds a new example script `examples/Propa.myc` to demonstrate basic
  usage.
- Includes a regression test
  `test_let_poly_non_series_callable_no_false_positive` to ensure that
  passing non-series callables to generic functions does not lead to
  type errors.
- Introduces `TypeChecker::bind_var` to handle lazy propagation of
  index-call constraints, crucial for correctly typing series lookups
  like `(s 0)`.
This commit is contained in:
2026-03-28 22:49:44 +01:00
parent bf12755905
commit 84abbd9721
4 changed files with 295 additions and 7 deletions
+19
View File
@@ -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<u32>, Box<StaticType>),
/// 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, "<polymorphic-fn>"),
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, "<error>"),
}
}
@@ -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!(