Skip to content

Elaborate bare Grammar-v1 Frame types exactly - #491

Merged
abiggerhammer merged 3 commits into
mainfrom
phase1-surf-008-bare-frame-type-elaboration
Sep 1, 2026
Merged

Elaborate bare Grammar-v1 Frame types exactly#491
abiggerhammer merged 3 commits into
mainfrom
phase1-surf-008-bare-frame-type-elaboration

Conversation

@abiggerhammer

Copy link
Copy Markdown
Owner

Summary

Continue Matrix SURF-008 / ledger PHIL-SURFACE-ELAB-001 with exact source-to-Core routing for Grammar-v1 Frame[...] types whose grammar reference is unspecialized.

Contract

  • a bare or qualified unspecialized Grammar-v1 grammar reference preserves its source-qualified spelling exactly as Core GrammarId inside TyFrame;
  • this follows the established surface elaborator contract (Frame[Hello] -> TyFrame (GrammarId "Hello")) without introducing a new semantic category;
  • specialized grammar references fail closed because Core GrammarId has no carrier for static arguments and flattening them would erase semantically relevant source information;
  • non-Frame types remain outside this bridge;
  • grammar existence, category competence, and any later specialization semantics remain competent semantic-checker responsibilities.

Executable pressure

Phase1GrammarV1BareFrameTypeElaborationMain.hs parses Frame[Hello] and Frame[Wire.Codec] and requires exact Core grammar identity. Frame[Wire.Codec[U32]] and a non-Frame type are negative pressure and must remain unresolved.

This is the fifteenth bounded SURF-008 slice after #462, #464, #466, #468, #471, #474, #477, #478, #481, #482, #485, #486, #488, and #489; full Grammar-v1 elaboration correspondence remains open.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant