Repository navigation
M3 kind gate: expression-level kinds, polykind instantiation, row-function kinds #100
Description
Part of #77 (Phase 4). The M3 kind gate is at 27/48. The remaining 21 files split cleanly: 13 are blocked only on a missing library module and 8 need real kind features.
Library-blocked (13) — resolved by Phase 3 + #83
failing/3453.purs, 3549.purs, CoercibleKindMismatch.purs, FoldableInstance1-3.purs, InvalidDerivedInstance3.purs, NewtypeInstance6.purs, PASTrumpsKDNU1.purs, PASTrumpsKDNU7.purs, RowConstructors1-3.purs.
These import Prelude, Data.Foldable, Data.Newtype, Effect.Console, or Safe.Coerce. They do not need new kind code. Note that PASTrumpsKDNU1/7 are cases where purs deliberately chooses PartiallyAppliedSynonym over KindsDoNotUnify; the comment in the file says so, and the choice must be reproduced, not improved on.
Real gaps (8)
| File | Expected | Needs |
|---|---|---|
3077.purs |
KindsDoNotUnify |
Kind checking in an expression (put (SProxy :: SProxy "apple") where TProxy expects Type but SProxy "apple" :: Symbol) |
StandaloneKindSignatures1.purs |
KindsDoNotUnify |
Standalone kind signature on a data type plus kinded application (Pair :: Pair Int "foo") |
StandaloneKindSignatures4.purs |
KindsDoNotUnify |
As above |
PolykindInstantiation.purs |
KindsDoNotUnify |
A polykinded data type whose parameter kind is inferred at instantiation |
PolykindInstantiatedInstance.purs |
KindsDoNotUnify |
As above, through an instance head |
3765-kinds.purs |
KindsDoNotUnify |
A kind that is a function over a row: data Tricky :: forall r. {a :: Int | r} -> {b :: Int | r} -> Type |
2542.purs |
UndefinedTypeVariable |
A free type variable in a local where signature (bar :: Array a) |
DiffKindsSameName.purs |
KindsDoNotUnify |
A shared cross-module kind environment where two modules define the same local kind name |
Acceptance
M3 reaches 48/48, and FE-11 moves from "complete cross-module environments, rows in kinds, and expression-level cases" to a concrete remaining gap.
Activity
Correct the first-stage blocker decomposition and close out Phase 2
biuld commentedon Oct 22, 2026
L3 is 50/50: all original kind cases and both quantified-kind/type codes agree. Passing-program kind gaps remain separately tracked.
Verified by PR #164 (41a16e2): formatting, default Clippy, full workspace (2331 passed, zero failed), five separately executed frontend boards, all 22 official purs differential tests, and the complete serial runtime board (297/340; 25 FFI exclusions; every agreeing exit zero). Required Wasmtime CI execution check 119961920075 completed successfully. The three losses versus the older board reproduce on the unmodified starting HEAD; BigFunction remains an explicit incomplete compiler verdict.
Evidence: Phase 4 acceptance review.