Repository navigation

v2 infer: a parameter containing a type variable inside a constructor is matched and judged, not admitted - #13187

Merged

gunbai-bot[bot] merged 16 commits into

mainfrom

session/stern-swift-290-generic-formal

Oct 4, 2026

Commits on Oct 4, 2026
- v2 infer: a formal containing a type variable inside a constructor is matched and judged (WIP)
  
  gunbc-ci-auto-heal
  and
  claude
  committed
  c1ecbe6
- generic formal: failure-mode row; warm producers for the controls
  
  gunbc-ci-auto-heal
  and
  claude
  committed
  7e4cbc5
- floor_pure_producer_share: no annotation inside the roster body
  
  gunbc-ci-auto-heal
  and
  claude
  committed
  a326d12
- generic formal: exhaustive arms over node kinds (no closed-coproduct wildcard)
  
  gunbc-ci-auto-heal
  and
  claude
  committed
  8ce1880
- generic formal: unfold a type alias before comparing constructors; alias controls
  
  gunbc-ci-auto-heal
  and
  claude
  committed
  8331557
- probe (temporary): where the List alias is indexed
  gunbc-ci-auto-heal
  committed
  21dc371
- probe: alias view
  gunbc-ci-auto-heal
  committed
  5ac1713
- generic formal: compare the matched formal and the argument with aliases unfolded before the exact judge; drop probe
  
  gunbc-ci-auto-heal
  and
  claude
  committed
  8f9d4f7
- generic formal: fold (typed) instead of list_map in alias normalization
  
  gunbc-ci-auto-heal
  and
  claude
  committed
  eaaad40
- Merge remote-tracking branch 'origin/main' into session/stern-swift-290-generic-formal
  gunbc-ci-auto-heal
  committed
  342eaef
- Merge main (Bool de-fork: import Bool from std.types)
  
  gunbc-ci-auto-heal
  and
  claude
  committed
  9842103
- generic formal: a refined argument matches through its declared carrier (review 75350); refinement and record-wrapper controls
  
  gunbc-ci-auto-heal
  and
  claude
  committed
  f4f2b5f
- one alias rule: transparent aliases normalized by the obligation producer for both routes; refinements never unfold; generic shortcut and alias arms deleted (review 75435)
  
  gunbc-ci-auto-heal
  and
  claude
  committed
  9e73727
- one obligation constructor: declared, produced and refinement carrier all alias-normalized at every infer obligation
  
  gunbc-ci-auto-heal
  and
  claude
  committed
  764dc9d
- generic formal: the refinement carrier is matched alias-normalized, like the formal
  
  gunbc-ci-auto-heal
  and
  claude
  committed
  ba7a8d3
- Merge remote-tracking branch 'origin/main' into session/stern-swift-290-generic-formal
  gunbc-ci-auto-heal
  committed
  c9e2aa8

Navigation Menu

Repository navigation

v2 infer: a parameter containing a type variable inside a constructor is matched and judged, not admitted - #13187

v2 infer: a parameter containing a type variable inside a constructor is matched and judged, not admitted#13187
gunbai-bot[bot] merged 16 commits into
mainfrom
session/stern-swift-290-generic-formal

Commits on Oct 4, 2026

v2 infer: a formal containing a type variable inside a constructor is matched and judged (WIP)

generic formal: failure-mode row; warm producers for the controls

floor_pure_producer_share: no annotation inside the roster body

generic formal: exhaustive arms over node kinds (no closed-coproduct wildcard)

generic formal: unfold a type alias before comparing constructors; alias controls

probe (temporary): where the List alias is indexed

probe: alias view

generic formal: compare the matched formal and the argument with aliases unfolded before the exact judge; drop probe

generic formal: fold (typed) instead of list_map in alias normalization

Merge remote-tracking branch 'origin/main' into session/stern-swift-290-generic-formal

Merge main (Bool de-fork: import Bool from std.types)

generic formal: a refined argument matches through its declared carrier (review 75350); refinement and record-wrapper controls

one alias rule: transparent aliases normalized by the obligation producer for both routes; refinements never unfold; generic shortcut and alias arms deleted (review 75435)

one obligation constructor: declared, produced and refinement carrier all alias-normalized at every infer obligation

generic formal: the refinement carrier is matched alias-normalized, like the formal

Merge remote-tracking branch 'origin/main' into session/stern-swift-290-generic-formal