Fix resolution errors during phases#1389
Merged
keyboardDrummer merged 13 commits intoJun 19, 2026
Merged
Conversation
keyboardDrummer
changed the base branch from
main
to
reviewed-kbd-will-merge-to-main
June 18, 2026 13:52
keyboardDrummer
marked this pull request as ready for review
June 18, 2026 14:30
keyboardDrummer
enabled auto-merge
June 18, 2026 14:30
keyboardDrummer
marked this pull request as draft
June 18, 2026 14:30
auto-merge was automatically disabled
June 18, 2026 14:30
Pull request was converted to draft
- Statement forms (Var-Declare, Exit, Return-*, While, Assert, Assume) are now synth rules (⇒ TVoid) instead of check rules (⇐ A) - Replace [⋄] Stmt / [⋄] Discard-Call with single [⋄] Synth-Discard rule - Remove TVoid <:_~ T premise from Return-None-Single - Procedure body is now synthesized, not checked against procedureBodyType - Update all index entries accordingly
…ules - Var-Declare, While, Exit, Return, Assert, Assume: ⇐ A → ⇒ TVoid - Check.statement (Discard): describe single synth-and-discard rule - Remove references to Discard-Call carve-out (no longer needed) - resolveBody: remove stale reference to expected type parameter - resolveProcedure: body is now synthesized, not checked against procedureBodyType - Return-None-Single: remove TVoid <:~ T subtype check from doc - Block: update non-last description to match synth-and-discard semantics - Overview section: rewrite statement-form explanation
keyboardDrummer
marked this pull request as ready for review
June 18, 2026 15:46
keyboardDrummer
enabled auto-merge
June 18, 2026 15:46
keyboardDrummer
requested review from
ssomayyajula
and removed request for
ssomayyajula
June 18, 2026 15:46
fabiomadge
approved these changes
Jun 18, 2026
kadirayk
approved these changes
Jun 19, 2026
kadirayk
left a comment
kadirayk
left a comment
Contributor
There was a problem hiding this comment.
LGTM. Reporting errors that were silently dropping after transformation steps. Giving each type a single consistent name (and grouping the related steps) is a nice clean up.
Merged
via the queue into
reviewed-kbd-will-merge-to-main
with commit Jun 19, 2026
81f20ab
20 checks passed
leo-leesco
reviewed
Jun 19, 2026
strata-git-sync Bot
pushed a commit
that referenced
this pull request
Jul 14, 2026
### Changes - Report resolution errors that occur after transformation passes during the compilation of Laurel to Core. This change triggers errors in existing tests that lead to the remainder of the changes in this PR. - Remove `.THeap` and `.TTypedField`. The usages have been replaced by `.UserDefinedType "Heap"` and `.UserDefinedType "Field"`, so that all references to the heap type use that form, preventing type equality errors. - Only re-resolve after HeapParam, TypeInference and ModifiesClauses passes all complete, since they are part of the same logical pass. In the future, we should refactor so they're actually one pass, but still three components, since TypeHierarchy and ModifiesClauses are features that built on top of Composite types. - Replace all reference types with `Composite` during the TypeInference pass. This also enables a slight simplification of LaurelToCoreTranslator. - Correct a source location usage in the lifting pass. Without this change, the reported location for an error would change, and this is detected during re-resolution. - In `Resolution.lean`, synth instead of void-check non-last block elements. This is required because some passes create non-void non-last block elements. In particular the `EliminateIncrDecr` pass creates them. This change also means that `Resolution.lean` no longer needs to special-case checking `| .StaticCall .. | .InstanceCall .. | .IncrDecr `. - Because of the previous change, `Resolution.lean` needs to support synthing for any StmtExpr, which it now does. - In the resolver, add special casing for calls to select/update/const. These are polymorphic procedures which we can't type check without special casing yet, since we don't support polymorphism yet. - Remove expecting the body of a function to correspond to its result type. This check failed for more complicated functions from `T3_ControlFlow` after they were lowered by some passes. Note that function will be removed entirely. In the test related to this removed check, I have changed the function into a procedure and the same diagnostic is reported then, although through a different mechanism. - Refactor TypeAliasElim so it uses a generic traversal to update types. This generic traversal was added a part of changes to TypeHierarchy ### Testing Added one test, but mostly this PR relies on the existing tests. --------- Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
fabiomadge
added a commit
to fabiomadge/Strata
that referenced
this pull request
Jul 15, 2026
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.
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
5 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.
Changes
.THeapand.TTypedField. The usages have been replaced by.UserDefinedType "Heap"and.UserDefinedType "Field", so that all references to the heap type use that form, preventing type equality errors.Compositeduring the TypeInference pass. This also enables a slight simplification of LaurelToCoreTranslator.Resolution.lean, synth instead of void-check non-last block elements. This is required because some passes create non-void non-last block elements. In particular theEliminateIncrDecrpass creates them. This change also means thatResolution.leanno longer needs to special-case checking| .StaticCall .. | .InstanceCall .. | .IncrDecr.Resolution.leanneeds to support synthing for any StmtExpr, which it now does.T3_ControlFlowafter they were lowered by some passes. Note that function will be removed entirely. In the test related to this removed check, I have changed the function into a procedure and the same diagnostic is reported then, although through a different mechanism.Testing
Added one test, but mostly this PR relies on the existing tests.