Park projection equality #54

New issue

Open

opened 2026-07-27 12:33:10 +02:00 by st · 0 comments

st commented

2026-07-27 12:33:10 +02:00

Owner

The declared generic consumer already works end-to-end, over every collection and generic in the element:

forall
  C, S, E: Num,
  I: Iterate[C, S],
  I.Elem = E,
fn total(xs: C): E
  let mut s = Num.zero
  for x in xs do
    s := s + x
  end
  s
end

total([1, 2, 3])      -- 6   (S improved to Iterator[i64] from C)
total(Array(40, 50))  -- 90
total(0..4)           -- 6

Call sites already solve the C→S relation — only C is ground, and dispatch improves S from the unique matching instance. What fails is dropping the forall: fn total(xs) gives cannot unify Iterate[?, ?].Elem with …, and still fails with the element pinned (let mut s: i64 = 0). So the blocker is not the relation but the projection: x : Iterate[?C, ?S].Elem meets a required type through plain unification while the participants are still variables, and an unreduced projection unifies with nothing. The declared I.Elem = E given hands the reducer exactly that equality, which is why the annotated form succeeds.

Two pieces are needed, both in this arc's territory:

1. Park the projection equality — Iterate[?C, ?S].Elem ~ τ in value position becomes a wanted Proj equation awaiting the fixpoint, instead of an eager unify failure. (OutsideIn: wanted equalities are quantified into the context; GHC infers this signature with type families.)
2. Promote the inferred Iterate[?C, ?S] obligation through generalization, quantifying S — a participant appearing only in the constraint. The scheme side already anticipates this (generalize_group, lib/infer.ml:3953, whose retained equations "determine a constraint-only participant's element types in the caller"); the promotion path doesn't yet produce it.

Acceptance example when both land: fn total(xs) infers forall C, S, E: Num, Iterate[C, S], Elem = E. fn(C) -> E — composing parked projections, inferred-MPTC promotion, and given-driven dispatch in one five-line function.

``` The declared generic consumer already works end-to-end, over every collection and generic in the element: forall C, S, E: Num, I: Iterate[C, S], I.Elem = E, fn total(xs: C): E let mut s = Num.zero for x in xs do s := s + x end s end total([1, 2, 3]) -- 6 (S improved to Iterator[i64] from C) total(Array(40, 50)) -- 90 total(0..4) -- 6 Call sites already solve the C→S relation — only C is ground, and dispatch improves S from the unique matching instance. What fails is dropping the forall: fn total(xs) gives cannot unify Iterate[?, ?].Elem with …, and still fails with the element pinned (let mut s: i64 = 0). So the blocker is not the relation but the projection: x : Iterate[?C, ?S].Elem meets a required type through plain unification while the participants are still variables, and an unreduced projection unifies with nothing. The declared I.Elem = E given hands the reducer exactly that equality, which is why the annotated form succeeds. Two pieces are needed, both in this arc's territory: 1. Park the projection equality — Iterate[?C, ?S].Elem ~ τ in value position becomes a wanted Proj equation awaiting the fixpoint, instead of an eager unify failure. (OutsideIn: wanted equalities are quantified into the context; GHC infers this signature with type families.) 2. Promote the inferred Iterate[?C, ?S] obligation through generalization, quantifying S — a participant appearing only in the constraint. The scheme side already anticipates this (generalize_group, lib/infer.ml:3953, whose retained equations "determine a constraint-only participant's element types in the caller"); the promotion path doesn't yet produce it. Acceptance example when both land: fn total(xs) infers forall C, S, E: Num, Iterate[C, S], Elem = E. fn(C) -> E — composing parked projections, inferred-MPTC promotion, and given-driven dispatch in one five-line function. ```