Stage c/228 qualified type effect path#309
Closed
hyperpolymath wants to merge 2 commits into
Closed
Conversation
…tor (Refs #228) The type/effect grammar had no module-qualified path production, so `Externs.Res` / `prelude.Option` / any `Pkg.Type` in type or effect position failed `parse error` at the `.` — contradicting ADR-011 (real modules with qualified paths). This adds full, SOUND module-qualified paths in type and effect position, with `.` as the canonical separator (`::` stays value/import per ADR-011); decision recorded as ADR-014. Resolution is by sound module-scoped member lookup, never flat scope: load module `[A;B]` through the loader, resolve+typecheck it as an import would, then look the member up *inside that module's own resolved symbols*, requiring Public/PubCrate and the right kind (SKType / SKEffect). Unknown/wrong module, missing member, private member, or wrong-kind member is a resolution error at the use-site span — never a parse error and never silently accepted. - lib/ast.ml: `ident` gains `modpath : string list` ([]=unqualified); add `mk_ident` helper so synthetic idents set the field in one place. - lib/parser.mly: `mk_qualified_ident`; `path_seg`/`module_prefix`/ `qualified_type_path` helpers; qualified bare/[args]/<args> forms for types and bare/[args] for effects. Module-prefix segments accept lower OR upper case (stdlib modules are `prelude`/`option` as well as `Network`/`Http`); member segment is upper_ident. - lib/typecheck.ml: `lower_type_expr`/`lower_effect_expr` validate the qualified case via a loader-backed `qualified_member_check` threaded into the context; `Qualified_path_error` -> `QualifiedPathError` at the check_program boundary (same pattern as Effect_validation_error). A validated qualified effect's name is admitted as a declared effect (issue #59) so a sibling module's public effect is usable like a local one. Resolved representation is the canonical nominal type/effect — identical to the bare/imported form; the validation, not the representation, is the soundness gate. Typecheck/codegen otherwise unchanged. - lib/resolve.ml: `make_qualified_member_check` built where the loader lives, inside the `resolve_and_typecheck_module` recursive group so transitively-qualified stdlib paths resolve too. - bin/main.ml: thread the validator into the 6 patterned check_program calls (via the type_ctx returned by resolve_program_with_loader). - Fixed ~10 internal direct `ident` record literals (trait/codegen_gc/ borrow/verilog) to route through `Ast.mk_ident`. - docs/specs/SETTLED-DECISIONS.adoc + .machine_readable/6a2/META.a2ml: ADR-014 (full stanza, same shape as ADR-011/012/013). - tests/conformance/qualified-paths/{valid,invalid}: 5 conformance fixtures wired into the e2e gate (valid qualified type+effect; unknown module; private member; absent member). Parser-conflict delta: ZERO. menhir --explain summary is byte-identical to the pre-change parser — 21 shift/reduce states, 1 reduce/reduce state, 68 s/r + 7 r/r arbitrarily resolved. The `upper_ident` vs `upper_ident DOT ...` decision is the expected benign DOT shift (Menhir shifts, disclosed per ADR-012); no new unexplained conflict. Test gate: 258 -> 263 (5 new #228 cases), zero regressions. Adding `modpath` to `ident` reflows every golden .expected AST dump; regenerated — the span-normalised golden harness confirms no structural change. STAGE-C peer of #225 (typed-wasm Http) and #160 (C-spine). Language decision is human-gated (ISSUE-CLOSURE): Refs #228, not Closes. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…ture limitation - .machine_readable/6a2/STATE.a2ml: bump last-updated; add session-note-2026-05-18 recording #228/ADR-014/PR#231 (machine state/progress convention was stale). - docs/specs/SETTLED-DECISIONS.adoc (ADR-014): add 'Known limitation' paragraph — qualified-effect positive fixture is harness-only (no public stdlib effect for a self-contained positive); bare-oracle audits must exclude it. - tests/conformance/qualified-paths/valid/qualified_effect.affine: header now states the harness-search-path dependency explicitly. Turns a silent landmine into a stated limitation. No code change. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Owner
Author
|
Superseded — closing as duplicate / stale re-open. This PR's head (
PR #241 merged to No salvageable content — closing without rebase. Refs #228, #231, #241. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.