feat(laurel): user-level polymorphism — generic composites, procedures, datatypes, type aliases by fabiomadge · Pull Request #1394 · strata-org/Strata

fabiomadge · 2026-06-19T00:17:15Z

What

User-level polymorphism for Laurel: generic composites, polymorphic procedures/functions, and generic datatypes. Verified end-to-end through Core/SMT.

Three mechanisms

The SMT wall (composites erase to one Core type; no sort quantification) rules out a uniform approach:

Generic composites → monomorphize (one per instantiation).
Value T → Core HM freshening (per call site).
Generic datatypes → native Core parametric datatypes (no monomorphization).

Covers generic fields, methods, inheritance (incl. Box<T> extends Base<T>), remap-aware upcasting, new C<τ>, polymorphic procedures, and recursive/nested generic datatypes.

Follow-up work (commits on top of the original squash)

Five commits extend the original landing. Each is individually built + lake test-green; soundness is pinned by paired must-fail twins (a .verifies case is matched with a _wrong case that must fail).

Cleanups (chore): stale-comment rewords; dead-code (parseOpaqueType) deletion; a comesBefore pin (monomorphize → heap-parameterization, load-enforced); a numVCs > 0 vacuity guard on the .verifies test oracle; a cosmetic resolveOutputParameter dup-check (a $heap-named user output now fails loud with Duplicate definition instead of a type-mismatch — both already rejected, so not a soundness change).
Map/Set-typed composite fields now heap-box (reading/writing a Map-typed field works; was a fail-loud limitation). Implemented as a 1:1 mirror of the generic-datatype tag; distinct (K,V) stay distinct boxes (no coalescing — corpus-pinned).
Generic is/as operands: x is Box<int> / x as Box<int> now parse, resolve, and verify (operand was a bare Ident). Also fixes a pre-existing emit bug (.Applied is/as operands were serialized as the literal "Unknown").
Type aliases type Name = Target, including generic aliases type Foo<T> = … (Map/primitive and composite targets; transitive/chained; param-order-preserving). Cyclic aliases fail loud.
Test hardening: matchTypeArg base-name self-guard (monomorphizer is now self-guarding, not trusting an upstream gate); a polymorphic program added to the differential cross-check; value-coupled twins; an optional diagnostic-kind assertion on .rejected corpus cases.

Note on scope: the Map-field, generic-is/as, and type-alias features are sound and corpus-tested but currently have no frontend emitter — they are carried on speculation. A reviewer may reasonably ask to defer them behind a consumer; the branch is linear, so they can be dropped cleanly.

Soundness

Anything unsupported fails loud (translated=false + diagnostic, or a type error) — no silent unsoundness, verified by execution.

An adversarial whole-diff review found 0 soundness findings, 0 wrong-accepts — scoped to the original squash. The five follow-up commits added soundness-relevant surface (the type-consistency relation isConsistent/TypeLattice.unfold, the monomorphizer's matchTypeArg, resolveOutputParameter, and new grammar/parse) that this review did not cover. That surface is instead backed by: paired must-fail twins per feature, a no-coalescing pair for Map-field boxing, a cross-spelling-reject twin for generic aliases (Box<bool> into a Foo<int> param rejects), and full lake test green. (A separate adversarial pass over the follow-up diff found no live wrong-accept either, but it is not the same "comprehensive whole-diff" review the original got.)

Tests

PolymorphismCorpusTest (the feature corpus — every feature paired with a must-fail twin), VerifyMetricsCorpusTest (+ a polymorphic differential cross-check), VerifyMetricsTest, MatchTypeArgTest, and an AbstractToConcreteTreeTranslatorTest round-trip case (incl. generic aliases). Full build and lake test pass locally (only the pre-existing ion-java JAR fixture is absent); CI in progress.

Pipeline ordering

liftInstanceProceduresPass runs at position 0 (must precede monomorphization). Type-alias elimination runs before monomorphization (so an alias of a generic-composite instantiation unfolds to the real .Applied the monomorphizer rewrites). The monomorphize → heap-parameterization order is enforced by a load-time comesBefore constraint.

Known debt (non-blocking)

CallElimCorrect is execution-guarded — its correctness theorem is stated over value/store semantics and quantifies over no types, so per-call-site type freshening is outside its scope (and that proof file is standalone, imported nowhere). A Strata-team conversation, not a code gap.

The shipped .TSet arms are unreachable (no Set surface syntax yet) and kept only for symmetry with .TMap.

A recent upstream commit notes an impending repository split — flagging in case this PR should retarget.

Migration note (breaking changes to `HighType` / `CompositeType`)

Two AST changes affect anyone who pattern-matches on HighType or constructs CompositeType:

New constructor HighType.TVar (a type variable). Non-exhaustive match HighType now needs a .TVar arm (Lean fills a missing arm with sorry, which compiles but aborts at evaluation — see the StrataPython fix in this PR for the pattern).
CompositeType.extending : List Identifier → List HighTypeMd (a composite may now extend a generic parent Base<T>). Constructors passing bare names wrap each as ⟨.UserDefined name, none⟩.

In-repo consumers (incl. the Python→Laurel translator) are updated here; the separate Java→Laurel translator will need the same two one-line changes.

(Follow-up surface changes — is/as grammar operand Ident→LaurelType, TypeAlias.typeArgs, TypeLattice.unfoldMap shape — are internal or have defaults, so they are not breaking for external pattern-matchers.)

Post-review fixes (found while building dynamic dispatch on top of this work)

Building method dispatch on top of these polymorphism primitives stress-tested them and
surfaced five issues in this PR's own code. They are folded in here (squashed into one
fix(laurel) commit) rather than shipped as a follow-up, since this PR has not merged.
All are verified by execution; the fail-loud invariant still holds everywhere.

Chained field access through a generic-composite field — p#b#az where p : Pair<int,Z>
and field b has a type-variable (or .Applied) declared type was spuriously rejected
("'az' is not defined"). targetTypeName/resolveFieldRef dropped .TVar/.Applied field
types; fixed by threading the synthesized concrete holder type into resolveFieldRef.
(Completeness — rejected valid programs.)
$-name collision diagnostics + false comments — a user identifier colliding with a
generated monomorph name (e.g. a composite literally named Box$a1$int, or a $heap
output) was reported as an Internal error/.StrataBug, blaming the compiler for a user
mistake. Now a clean .UserError with a rename hint. Also corrected six comments asserting
"no source identifier can contain $" — factually false ($ is a legal identifier char;
the monomorph tag encoding is non-injective, with soundness enforced by the downstream
duplicate-definition net, not by the tag). (Diagnostic quality.)
as-cast in heap-neutral procedures — HeapParameterization only lowered as
(x as T → { assert (x is T); x }) in procedures that read/write the heap; a heap-neutral
procedure took an early return, leaving AsType un-lowered and hard-failing the Core
translator with NotYetImplemented. Now lowered in the heap-neutral branch too (only the
heap-independent AsType rewrite, not the heap-dependent ones). (Completeness.)
A non-generic composite extending a generic instantiation — composite IntBox extends Box<int> did not type-check (upcast rejected, inherited field unresolved). Three coordinated
fixes: the monomorphizer now seeds + rewrites extending-list references (Box<int> →
Box$a1$int); isSubtype gained a .UserDefined-child / .Applied-parent arm (remap-aware
via substitutedAncestors, args invariant — so IntBox <: Box<int> succeeds while
IntBox <: Box<bool> and the prior-bug remap-swap shape both still fail); and the final type
list is topo-sorted as a whole so a concrete child emitted after its monomorph parent.
(Feature gap. Soundness re-verified adversarially: ~30 wrong-upcast / false-twin programs,
none accepted.)
Re-resolution cascade suppression — when a program already has a non-warning error, a
"new" error at post-pass re-resolution is downstream cascade (the same error restated over
the rewritten types), not a genuine internal failure; it is now suppressed rather than
mislabeled .StrataBug. (Diagnostic quality. Also fixed a name-collision regression in the
whole-list topo-sort — it now tracks entries by list index so a user/monomorph name collision
is preserved and reported, not coalesced.)

Corpus: 14 new cases (generic_chained_field_*, user_heap_output_rejected,
user_name_collides_with_monomorph, as_*_downcast_heap_neutral, concrete_extends_geninst_*).
Full lake test green (only the pre-existing ion-java JAR failure).

Dynamic method dispatch (the feature that surfaced these) is a separate, stacked PR —
it is a distinct capability (behavioral-subtyping checking + runtime-tag dispatchers) and is
not needed to review or land this polymorphism work.

…s, and datatypes Adds user-level polymorphism to Laurel, verified end-to-end through Core/SMT. Two mechanisms, forced by the "SMT wall" (every composite erases to one Core type): generic COMPOSITES monomorphize; generic DATATYPES map to native Core parametric datatypes (no monomorphization). Value-level `T` polymorphism rides Core HM freshening. Layers (each builds green on the prior): 1. Differential-verification harness — verifyToMetrics / corpus runner / cross-solution diff, plus the Core.verifyWithStats split (surfaces previously-discarded statistics). 2. Type-variable substrate — HighType.TVar, Procedure/CompositeType.typeArgs, ResolvedNode.typeVar, resolution scoping, translateType → .ftvar. 3. Polymorphic functions — Core HM instantiation; reference args via the uniform Composite. 4. Generic composites (monomorphization) — MonomorphizeComposites: per-instantiation emission across every type position, with a depth cap + fuel guard that fail LOUD. 5. Polymorphic procedures — CallElim per-call-site type-var freshening; the procedure↔composite monomorphization fixpoint; uncalled-poly-proc witness verification. 6. `new C<τ>` explicit-type-argument syntax — grammar → AST → resolution → monomorphize. 7. Gradual-checker .TVar arms (atop strata-org#1121) — polymorphic programs type-check and translate; soundness guarded both directions. 8. Generic composite methods — lifted to polymorphic procedures, reusing layer 5. 9. Generic composite inheritance — concrete parent and generic parent (`Box<T> extends Base<T>`), with remap-aware field inheritance and topological monomorph emission. 10. Remap-aware generic upcasting — substitutedAncestors; `C<args> <: P<remapped-args>`. 11. Generic-composite field-type concretization — reject-only; closes a field-write wildcard wrong-accept without touching the load-bearing .TVar consistency arm. 12. Generic datatypes — native Core parametric datatypes, including the heap-stored composite-field box wrapper; instantiations stay distinct sorts (cross-instantiation rejected). Recursive and nested generics round-trip. Invariant (verified by execution throughout): everything unsupported fails LOUD — translated=false with a diagnostic, or a thrown type error. No silent unsoundness. Reviewed pre-merge by a comprehensive adversarial whole-diff pass: 0 soundness findings, 0 wrong-accepts; the fail-loud invariant holds at every cross-feature seam. Tests: PolymorphismCorpusTest (the table-driven feature corpus — poly procedures, generic composites/methods/inheritance/upcast/field-tvar, generic datatypes), VerifyMetricsHarness (shared Case/checkCase machinery), VerifyMetricsCorpusTest (harness self-tests + monomorphic baseline), VerifyMetricsTest, MatchTypeArgTest, and AbstractToConcreteTreeTranslatorTest (AST→concrete→AST round-trips for the new generic emit productions; writing them surfaced and fixed a formatter bug where the `prec(80)` `appliedType`/`newTypeArgs` ops were parenthesized into non-re-parseable text — `(Box<int>)`, `new Box(<int>)` — corrected via `:0` annotations on the `typeAnnotation`/`new` references), and Core/Tests/PolyProcFreshenTest (Core-layer regression tests for CallElim per-call-site type-var freshening — multi-instantiation verifies, the soundness twin fails at the exact obligation, and the abort-masking ship-blocker is pinned by obligation label). Integrates strata-org#1381 (LiftInstanceProcedure ordering) — its T9_ValueReturningInstanceMethods test passes under the merged pass order (our lift sits at pipeline position 0, satisfying strata-org#1381's lift-before-eliminateValueInReturns requirement). Full build green; corpus green.

Five low-risk follow-ups from the polymorphism-PR backlog, all verified by ablation where they make a behavioral claim: - comesBefore pin (MonomorphizeComposites → HeapParameterization) at the pipeline-assembly site; load-enforced (ablation: a violated order throws at load when a consumer module builds). - numVCs > 0 added to the corpus `.verifies` oracle, closing the vacuous-pass hole (ablation: a 0-obligation translating program is now rejected; none of the existing ~45 .verifies cases regress). - resolveOutputParameter: thread a seen-outputs accumulator so a second same-name output routes to defineNameCheckDup. COSMETIC only — ablation showed the `$heap`-output case already fails loud (type mismatch); this just yields a cleaner "Duplicate definition" diagnostic. NOT a soundness fix (the claimed silent wrong-accept does not reproduce). Pinned by a fail-loud guard. - Reword two stale "Laurel doesn't support polymorphism yet" comments (CoreDefinitionsForLaurel, Resolution) — premise now false. - Delete dead parseOpaqueType (no grammar op, zero callers). lake test green (only the pre-existing ion-java JAR failure).

…rdening Implements the spike-verified follow-ups from the polymorphism backlog. All sound (false twins fail), full lake test green (only pre-existing ion-java). Features: - Item 1: Map/Set-typed composite fields heap-box. instTagCommon gains .TMap/.TSet arms (injective `Map$a2$k$v` tags, fail-loud on untaggable nested args); the three HeapParameterization box-name fns route .TMap/.TSet through appliedBoxTag. Reading/ writing a Map-typed field now round-trips (was boxDestructorNameError). Distinct (K,V) stay distinct boxes (no coalescing — corpus-pinned). Also lets `Box<Map int int>` monomorphize; the two former `untaggable_*` .rejected cases are now .verifies with value-coupled false twins (the rejects were un-implemented limitations, not soundness boundaries). - Item 7B: `is`/`as` operands widened Ident->LaurelType, so `x is Box<int>` / `x as Box<int>` parse, resolve, and verify (operand monomorphizes to the tag lowerIsType keys; `as` lowers via the HeapParam is-guard). Emit routes through highTypeToArg (fixes the .Applied->"Unknown" collapse). - Item 7C: `type Name = Target` surface form (grammar + parseTopLevel arm). Composite -typed aliases work via a transitive alias-unfold in resolveFieldInTypeScope (field resolution is name-keyed and runs before TypeAliasElim). Hardening: - Item 10C: matchTypeArg self-guards on the .Applied base name (Box<T> no longer structurally matches Pair<int>); MatchTypeArgTest case 7 pins it. - Item 10E: value-coupled twins for poly_proc_concrete_composite_param (now calls take + observes the field) and generic_datatype_recursive (reads back by equality). - Item 9+10B: runCrossCheck folds a polyCrossCheckCorpus (verify/fail/reject) so the post-monomorphize re-resolution fold is dual-path-checked. - Item 10D: Expect.rejected gains an optional DiagnosticType kind, checked via a 2nd verifyToDiagnosticModelsCapturing pass; representative cases tagged (.UserError / .NotYetImplemented) so a net<->clean diagnostic move fails loud.

Extends the monomorphic type aliases from 4131c09 with type parameters. All sound (false twins fail, wrong-arg rejects), full lake test green (only pre-existing ion-java). - Grammar/AST/parse: `Option TypeParams` on the `typeAlias` op + `typeArgs` on the `TypeAlias` AST; `target:0` so a Map/composite target emits without parens and re-parses. - Resolution: scope the alias's type params as `.typeVar` (mirrors .Datatype), so `A`/`B` in the target resolve to `.TVar`. - TypeAliasElim: parameterized substitution — `Foo<int>` binds the alias params to the args and substitutes into the target (via substTypeVars). Reordered BEFORE monomorphize so an alias of a generic-composite instantiation unfolds to the real `.Applied` the monomorphizer rewrites (mono is alias-agnostic). - TypeLattice.unfold: `unfoldMap` now carries (params, target); a new `.Applied`-alias arm substitutes args into the target, so isConsistent agrees with elimination at the initial resolve (fixes cross-spelling assignability, e.g. `var b: Foo<int> := new Box<int>` and passing `Box<int>` to a `Foo<int>` param). Unfold-then-compare stays strict, so `Box<bool>` into `Foo<int>` rejects. - Emit: AbstractToConcrete wraps the alias in `typeAliasCommand` and emits typeParams; round-trip test pins `type MyPair<A,B> = Map A B` / `type Foo<T> = Box<T>`. Corpus: generic alias to Map (+ param-order `Swapped<A,B> = Map B A`), to a generic composite (assign/param/wrong-arg/false twins), chained generic aliases, and arity-mismatch reject.

Review follow-ups on the poly test corpora: - GenericCompositeTest: fix the section-doc monomorph tag (Box$int → Box$a1$int, the actual instTagCommon arity-tagged form used everywhere else in the file); pin map_concrete_mismatch + generic_alias_wrong_arg to .rejected (some .UserError). - GenericDatatypeTest: pin generic_datatype_cross_instantiation_rejected to (some .UserError). - PolyProcedureTest: pin the 7 tc_* checker-not-weakened cases to (some .UserError) and the 2 divergent-generic cases to (some .NotYetImplemented) — bare .rejected can't distinguish a clean user error / depth-cap NYI from a StrataBug internal error. All kinds probed + build-confirmed present on THIS branch (user_heap left .StrataBug — its .UserError reclassification is a dispatch-branch change, absent here). Comment/outcome only.

An applied type at the wrong type-argument arity (`MyPair<int>` for a `type MyPair<A,B>`, or `Box<int,bool>` for a `composite Box<T>`) now reports a plain UserError from the resolver instead of surfacing as an internal StrataBug. - Resolution.resolveHighType's `.Applied` arm checks the argument count against the declared param count (unfoldMap for a generic alias, parentExprMap for a generic composite/datatype) and reports a clean user error on mismatch. Before, an arity-wrong alias resolved silently, then TypeAliasElim deleted the alias def while leaving the reference unfolded, so re-resolution reported the dangling name as an 'Internal error' StrataBug. - The pipeline's re-resolution net now fires only when the initial resolution was clean. It exists to police transforms that break an initially-VALID program; when the input was already user-rejected, a downstream dangling reference is just noise on top of the real error. - Pin generic_alias_arity_wrong to .rejected (some .UserError).

Test comments should describe what the mechanism IS, not narrate branch history. Drop 'previously fail-loud', 'spuriously over-rejected', 'was a crash', and the 'SUPERSEDES the runUnsupportedGates gate' narrative from GenericCompositeTest and PolyProcedureTest; keep the mechanism descriptions and what each case pins.

…cases The corpus's `.rejected (some kind)` asserts a diagnostic kind is PRESENT, not exclusive — a spurious extra diagnostic of another kind alongside it still passes. That gap let a cascade regression hide: a divergent generic correctly emits `.NotYetImplemented` (depth cap), but a broken re-resolution suppression folded three `.StrataBug` internal-errors on top, and the presence-only pin stayed green. Add `Expect.rejectedExactly (kind)`: !translated AND every non-Warning diagnostic is exactly `kind`. Pin poly_proc_chain_divergent and poly_proc_uncalled_divergent_witness with it. Verified by negative control: reintroducing the broken suppression makes the pin fail with 'got kinds #[NotYetImplemented, NotYetImplemented, StrataBug, StrataBug, StrataBug]', which the old presence-only pin passed.

Cut self-describing narration and a stale reference (PolymorphismCorpusTest, split into per-feature files) from LaurelCorpusHarness. Keep the load-bearing rationale: the .UserError-vs-.StrataBug kind distinction, why .rejected(some k) is presence-only, and what .rejectedExactly guards against. Comments only; -39/+21 lines.

Remove comments that restate a case's own `why` field, duplicate a section/module docstring, or carry stale external item-labels (7(B), 7(C), Item-5, gap-(ii), '(this commit)'). Keep all load-bearing mechanism/soundness rationale — e.g. the cross-instantiation-distinctness note, the remap-aware upcast reasoning, and the richer freshening-vacuity docstrings were deliberately left intact. Comments only.

…Test 'Pair' was used for three different shapes in one file. Rename the one-param wrapper `Pair<T> { b: Box<T> }` (nested_generic cases) to `Wrap<T>` — it holds one Box, not a pair — and give the `is`-operand `Pair<A,B>` its honest second field so every remaining `Pair` is the conventional two-param/two-field pair. No collision risk either way ('Pair' is not a reserved/prelude/internal name, unlike 'Box'); this is readability.

Five fixes to the polymorphism primitives in this PR, surfaced by building dynamic method dispatch on top of them. Folded back here (squashed) rather than shipped as a follow-up, since this PR has not merged. All verified by execution; the fail-loud soundness invariant holds throughout. 1. Chained field access through a generic-composite field (p#b#az where the intermediate field has a .TVar/.Applied type) was spuriously rejected; resolveFieldRef now threads the synthesized concrete holder type. (Completeness.) 2. A user identifier colliding with a generated monomorph name (e.g. a composite named Box$a1$int, or a $heap output) was reported as an internal StrataBug; now a clean UserError with a rename hint. Corrected six comments that falsely asserted no source identifier can contain '$' (it is a legal identifier char; the monomorph tag encoding is non-injective, with soundness enforced by the downstream duplicate-definition net). (Diagnostic quality.) 3. 'as'-casts in heap-neutral procedures were left un-lowered (the HeapParameterization early-return for heap-neutral procs skipped AsType), hard-failing the Core translator; now the heap-independent AsType rewrite is applied in that branch too. (Completeness.) 4. A non-generic composite extending a generic instantiation (composite IntBox extends Box<int>) did not type-check. Three coordinated fixes: the monomorphizer seeds + rewrites extending-list references; isSubtype gained a .UserDefined-child / .Applied-parent arm (remap-aware via substitutedAncestors, args invariant, so IntBox <: Box<int> succeeds while IntBox <: Box<bool> and the remap-swap shape both still fail); and the final type list is topo-sorted as a whole so a concrete child is emitted after its monomorph parent. (Feature gap; soundness re-verified adversarially.) 5. Re-resolution cascade suppression: a "new" error at post-pass re-resolution on an already-rejected program is downstream cascade, not an internal failure, and is no longer mislabeled StrataBug. Also fixes a name-collision regression introduced by fix 4 in the whole-list topo-sort, which now tracks entries by list index so a user/monomorph name collision is preserved and reported, not coalesced. (Diagnostic quality + regression fix.) Adds 14 corpus cases (generic_chained_field_*, user_heap_output_rejected, user_name_collides_with_monomorph, as_*_downcast_heap_neutral, concrete_extends_geninst_*).

- Rename the nested-generic composite Wrap<T> -> Nest<T>: 'Wrap' collided with the existing 'datatype Wrap' in the same file (two meanings, reader-confusing). Nest<T> is free and matches the 'nested generic' intent. - Inline genericBoxProgram/genericBoxMultiProgram: both single-use, hoisted for no reason while the other 64 cases inline their src. - Correct the user_heap_output_rejected comment: it described the pre-fix behavior ('expected Heap got int', 'either way !translated'); the actual diagnostic is one clean UserError 'Duplicate definition $heap' + rename hint (verified by execution). - Tighten the alias_composite_field comment (drop 'was wired'/'new grammar' history).

- The two byte-identical worklist-drain loops (main drain + post-witness drain) are extracted into a single `drainWorklist` helper. It recurses structurally on `fuel : Nat` (so it's provably terminating — no `partial`, no `mut fuel`, no `while`) and both call sites share it, so the drains can't drift. Behavior verified identical: divergent→[NYI], multi-inst→[NYI,NYI], normal→verifies. - Fix the module header: a monomorph is `Box$a1$int` (arity-tagged), not `Box$int` — the rest of the file already uses the $a1$ form.

…se recursion) Reviewing TypeAliasElim surfaced that a bare generic name in an annotation (var m: MyPair, for type MyPair<A,B>) reaches Core as a dangling ref -> StrataBug, unlike the clean UserError for MyPair<int>. Attempted to extend resolveHighType's arity check to the bare .UserDefined arm; it over-rejected. ROOT CAUSE (traced by instrumentation, not guessed): the .Applied arm recurses 'resolveHighType base', so the base 'Box' of any 'Box<int>' arrives at the .UserDefined arm as a bare zero-arg name — indistinguishable from a genuinely-complete bare 'Box'. A zero-args check there fires on every applied type's base and rejects 'Box<int>' itself (verified: new_box_int AND param_box_int both trigger it). Reverted; documented the residual gap + its true cause inline. The gap is fail-loud (a rejection, never a wrong-accept), so acceptable — just a less precise message. (An earlier draft of this note blamed the 'new C' constructor head; that was wrong — corrected here after tracing the actual trigger.)

The comments claimed all arity-wrong alias references are handled upstream. Only .Applied (Pair<int>) is — resolveHighType's .Applied arity check catches it. A bare generic alias at zero args (Pair for type Pair<A,B>) is NOT caught upstream (that check can't fire on a bare name — see the Resolution.lean NOTE) and falls through here unfolded, surfacing as a fail-loud StrataBug at re-resolution. Both cases stated once in the docstring; the two inline comments just tag their arm and defer. Rejection, never a wrong-accept.

The comment claimed 'a method's own typeArgs are empty in the surface syntax, so this is a pure addition' — false. Instance methods CAN declare their own type params (e.g. id2<U>(self: Box<T>)), which is exactly why the lifted proc's typeArgs are ct.typeArgs ++ proc.typeArgs, not just ct.typeArgs. Verified: method_own_U (id2<U>) translates only because proc.typeArgs=[U] is carried. Rewrote to state the real composite-then-method ordering (Box$id2<T,U>) and drop the false 'empty/pure' framing.

The comment claimed 'reference-kinded T is erased to a composite by an earlier pass, so it never reaches this arm as .TVar' — false, and it directly contradicts PolymorphicFunctionTest's comment (+ its executing poly_ref_fn case). There is NO erase-reference-T pass: a reference-kinded T reaches translateType as .TVar, lowers to .ftvar, and Core's HM unifies it with the single Composite sort — verified (ref_T_fn: a poly fn over a composite arg translates + verifies). The .ftvar lowering is kind- agnostic. Rewrote the comment to state the real mechanism; the code was already correct.

38 comment lines -> ~20 for the cascade-suppression + collision block. Cut: the three-way enumeration of cascade sources (one example makes the point), the strata-org#1389 'supersedes an earlier workaround' changelog history, the '$body' example, and the 'HeapParam/TypeHierarchy set needsResolves:=false' aside (a DUPLICATE — that rationale already lives inline at both pass definitions). Kept every load-bearing reason: why suppress, why fold-loud, the duplicate-can-only-be-a-user/generated-collision proof that justifies UserError, and the source-location TODO. Comments only; corpus green.

The appliedBoxTag docstring re-explained the non-injectivity caveat in full while also pointing to the canonical copy on instTagCommon — compressed to the mechanism + the pointer (12 lines -> 7). Also fixed a contradiction: the boxDestructorName arm called it 'the shared INJECTIVE tag' while the function's own doc (correctly) says NON-injective — reworded to 'named via appliedBoxTag'. Left the boxConstructorDef arm comment intact (it carries distinct load-bearing content: the box holds the FULL type so translateType picks the right Core sort). Comments only; builds.

…tionsForLaurel The rewritten docstring already explains the select/update/const stand-ins fully (external, filtered before Core, int placeholders inert because the polymorphism lives in the Core primitives). The inline comment above the functions repeated the same 'int placeholders ON PURPOSE / filtered before Core' point ~10 lines below the docstring — cut it, and tightened the docstring's placeholder clause. Verified while reviewing: the select/update/const RETURN type changed Box->int by the poly cleanup is inert (these are external + filtered), and the deleted 'datatype Box {MkBox()}' was vestigial — the heap 'Box' is SYNTHESIZED by HeapParameterization (line 648), a separate datatype. Comments only.

…ontractPass The mentionsTVar docstring and the mkTempAssignments docstring stated the SAME 4-clause rationale near-verbatim (poly callee param is T -> resolution treats T authoritative -> T unbound at Core -> type the temp from the argument's concrete type). The logic lives in mkTempAssignments, so it keeps the full rationale; mentionsTVar is now a one-line 'what it tests' + pointer. Verified while reviewing (with corpusMetricsOf, the correct numFailures measure — NOT a diag count): a contracted poly proc gates correctly across instantiations (false postcondition -> numFailures=1, violated precond via pos(-3,..) -> numFailures=1, multi-inst true -> 0). Comments only.

The extends comment restated that 'bare Base parses as compositeType, Base<T> as appliedType' — which is inherent to having both productions (already documented at appliedType). Cut that clause; kept the two load-bearing parts: WHY parents became LaurelTypes (generic parent instantiation) and the no-ambiguity-with-fields-block note. Left the new<>/lt and FieldPath/multiAssign comments intact (each documents a real disambiguation / anti-regression rationale). Verified all four disambiguation claims by PARSING the sensitive cases (bare-vs-applied, new<> vs '<', FieldPath vs multiAssign value, generic-parent extends) — all parse clean. Comment only.

This 6-line #load_dialect wrapper was buried under a ~25-line running changelog ('Then: ... Then: ...') narrating every past grammar change, scattered both between module/import and after 'end'. The current grammar is self-documented in LaurelGrammar.st (48 comment lines on the productions themselves), so the history here was pure redundancy. Replaced it with a tight header: the file's purpose + the one load-bearing note — the build system does NOT track the .st as an input, so you must touch this file to force a recompile after editing the grammar (verified: no .st dep in the lakefile). 46 -> 25 lines; dialect loads, corpus parses.

…rammar The translateFieldPath docstring re-argued WHY FieldPath is a dedicated category (the multiAssign-value parse collision) — but that is a GRAMMAR concern already stated in full in LaurelGrammar.st where the category is declared. Kept the translation-specific content (the two-arm mapping + the 'same .Var(.Field) chain a field read produces, so downstream lowering is uniform' insight, which the grammar does NOT cover) and replaced the parse re-argument with a pointer. Also fixed a stray-comma typo ('object,)'). Left the extends inline comment intact (it documents translation-routing, not the grammar's disambiguation). Verified while reviewing: every poly production translates faithfully (multi-arg Pair<int,bool>, new<>, is/as LaurelType, datatype/alias typeparams); the removed parseOpaqueType was dead (no 'opaqueType' production anywhere). Separately noted (NOT this file's bug): a generic alias of a generic DATATYPE (type Foo<T> = Opt<T>) translates fine but is rejected downstream ('expected Foo<int>, got Opt') — a real alias-consistency gap, out of scope here. Comments only.

A generic alias of a generic DATATYPE assigned from a constructor result was wrongly rejected: 'type Foo<T> = Opt<T>; var o: Foo<int> := Som(5)' gave "expected 'Foo<int>', got 'Opt'". Root cause: a datatype constructor synthesizes the BARE datatype type (Som(5) : Opt, no args), so the assign reaches isConsistent's bare-name~instantiation arm (LaurelAST.lean) as .UserDefined Opt vs .Applied Foo [int]; that arm compared RAW base names ('Opt' == 'Foo' -> false) without unfolding the alias. Fix: compare base names AFTER ctx.unfold (which already turns a generic-alias application Foo<int> into its target Opt<int>). Completeness only — a wrong-REJECT, never a wrong-accept; verified the guard: a DIFFERENT datatype's constructor into the same alias-typed var is still rejected (generic_datatype_alias_wrong). The alias-of-COMPOSITE sibling already worked (its RHS 'new Box<int>' carries args, routing through the .Applied/.Applied arm); this brings the datatype case to parity. 2 corpus cases; termination proof still discharges; full Laurel corpus green.

The .Applied emission comment narrated the old lossy behavior ('Previously this dropped the args (Base<int> -> bare Base)...') — changelog, not current state. Kept the mechanism (emit appliedType, peel base to Ident name, mirrors newTypeArgs/isType) and restated the round-trip point as a property of the current code. Verified: the dedicated round-trip test (AbstractToConcreteTreeTranslatorTest — already covers Box<T>, new Box<int>, generic extends, generic datatype, poly function) stays green. Comment only.

… poly hunks The comment-trim pass I should have run on these two densest files (missed earlier — I'd only accuracy-spot-checked them). MonomorphizeComposites: the 'fuel = coarse backstop / maxInstDepth = real guard' point was stated 4x — dropped the two redundant restatements (the step-3 trailing clause and the drainWorklist call-site comment, both covered by drainWorklist's docstring); kept the fixpoint-algorithm + FUEL-EXHAUSTION-guard blocks (each a distinct load-bearing point). Resolution: dropped two changelog parentheticals ('Was resolveRef over bare-name Identifiers', 'an earlier guard ... was removed') — kept the current-state rationale. Comments only; builds + corpus green.

…instead Reverts the over-rewrite in 8bf1ea5 that gutted this file's running 'Then: ...' grammar changelog. That log IS the file's mechanism: since the build system does not track the .st as an input, appending a line is how you trigger a recompile after a grammar edit — so the right update is one appended entry, not a rewrite. Restored the original verbatim and added a single 'Then:' line for this pass's .st comment trim. Builds; corpus parses.

…ecompile NOTE) Removes the running 'Then: ...' grammar changelog (noise) and the 'Last grammar change' bump line. Keeps only what is load-bearing: the file loads the dialect from LaurelGrammar.st, and the NOTE that the build system does not track the .st as an input (so edit this file to force a recompile). Undoes the over-eager revert in 33138db that restored the whole log. Builds; corpus parses.

… verbatim Delete ONLY the 'Then: ...'/'Grammar change:' changelog lines. The three original lines — 'loaded from LaurelGrammar.st' + the two-line NOTE ('not tracked by the build system; update this file (e.g. this comment) to trigger a recompile') — are preserved BYTE-FOR-BYTE, not paraphrased. That NOTE's 'update this file' line IS the recompile-trigger / last-grammar-change bump point. Supersedes my earlier churn on this file (rewrite -> revert -> paraphrase); the diff vs the original is now pure deletion, nothing added.

…grammar delta The NOTE says to bump 'this comment' to trigger a recompile, but there was no designated comment to bump. Add one 'Last grammar change (polymorphism): ...' line that summarizes ALL the grammar (.st) changes this PR makes — <T> binders, appliedType, new C<τ>, is/as over LaurelType, generic extends, the type-alias command, the FieldPath category — replacing the old running 'Then: ...' log with a single line that serves the log's purpose (record the latest grammar change + the point to bump). Builds; corpus parses.

…ination proof Replace `partial def` with a terminating `def`: match on `op.args.toList` (list patterns generate the match unfold-equations a well-founded def needs; the `#[...]` array literals do not) and discharge termination with an extracted reusable lemma `sizeOf_mem_args_lt` (an element of `op.args` is a strict subterm of the operation). This is the only `partial def` the polymorphism PR added to this file; the other five predate it and are unchanged. No behavior change: chained-field-write tests (T9_ChainedFieldAccess, T1_MutableFields, T9_OldHeapTwoState, GenericCompositeTest, AbstractToConcreteTreeTranslatorTest) all pass.

github-actions Bot added Laurel Core Git conflicts labels Jun 19, 2026

fabiomadge force-pushed the laurel-polymorphism-landing branch from bf29841 to 1776dc6 Compare June 19, 2026 00:30

github-actions Bot removed the Git conflicts label Jun 19, 2026

fabiomadge force-pushed the laurel-polymorphism-landing branch 7 times, most recently from 9917acf to 0b0acb5 Compare June 19, 2026 12:10

github-actions Bot added the Git conflicts label Jun 19, 2026

fabiomadge force-pushed the laurel-polymorphism-landing branch 4 times, most recently from 9c13d6e to bd4d182 Compare June 20, 2026 15:10

github-actions Bot removed the Git conflicts label Jun 20, 2026

fabiomadge force-pushed the laurel-polymorphism-landing branch 4 times, most recently from 2217644 to 0f75fea Compare June 22, 2026 11:33

fabiomadge changed the title ~~feat(laurel): user-level polymorphism — generic composites, procedures, and datatypes~~ feat(laurel): user-level polymorphism — generic composites, procedures, datatypes, type aliases Jun 22, 2026

fabiomadge mentioned this pull request Jun 23, 2026

feat(laurel): Seq<T> and Array<T> with bounds-checked subscript and diagnostics #1073

Open

github-actions Bot added the Git conflicts label Jun 25, 2026

fabiomadge mentioned this pull request Jun 25, 2026

feat(laurel): dynamic method dispatch + behavioral-subtyping (Liskov) checking fabiomadge/Strata#3

Draft

fabiomadge added 4 commits June 26, 2026 13:37

fabiomadge added 29 commits July 15, 2026 17:39

fabiomadge force-pushed the laurel-polymorphism-landing branch from b52136b to dcc9704 Compare July 17, 2026 20:46

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

feat(laurel): user-level polymorphism — generic composites, procedures, datatypes, type aliases#1394

feat(laurel): user-level polymorphism — generic composites, procedures, datatypes, type aliases#1394
fabiomadge wants to merge 47 commits into
strata-org:reviewed-kbd-will-merge-to-mainfrom
fabiomadge:laurel-polymorphism-landing

fabiomadge commented Jun 19, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

fabiomadge commented Jun 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What

Three mechanisms

Follow-up work (commits on top of the original squash)

Soundness

Tests

Pipeline ordering

Known debt (non-blocking)

Migration note (breaking changes to HighType / CompositeType)

Post-review fixes (found while building dynamic dispatch on top of this work)

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

fabiomadge commented Jun 19, 2026 •

edited

Loading

Migration note (breaking changes to `HighType` / `CompositeType`)