[OpenCB Project Fix] Fixes #26018: Surface diverging implicit error from nested summonInline#26024
Draft
soronpo wants to merge 1 commit into
Draft
[OpenCB Project Fix] Fixes #26018: Surface diverging implicit error from nested summonInline#26024soronpo wants to merge 1 commit into
soronpo wants to merge 1 commit into
Conversation
92 tasks
…nInline
When an inline given's body contains a `summonInline[T]` that triggers a
recursive implicit search of the same type, divergence is correctly
detected at the inner search but the buffered error gets wrapped by
`typedImplicit` as a `MismatchedImplicit` failure ("does not match
type"), which is misleading because the displayed candidate would in
fact match.
Detect the buffered divergence via a new `isDivergingImplicit` predicate
on `MissingImplicitArgument` and propagate as `DivergingImplicit` so the
user sees "produces a diverging implicit search" instead.
560f6cc to
f360f92
Compare
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
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.
When an inline given's body contains a
summonInline[T]that triggers a recursive implicit search of the same type, divergence is correctly detected at the inner search but the buffered error gets wrapped bytypedImplicitas aMismatchedImplicitfailure ("does not match type"), which is misleading because the displayed candidate would in fact match.Detect the buffered divergence via a new
isDivergingImplicitpredicate onMissingImplicitArgumentand propagate asDivergingImplicitso the user sees "produces a diverging implicit search" instead.Fixes #26018
How much have you relied on LLM-based tools in this contribution?
Extensively, but it's a small fix.
How was the solution tested?
New automated tests (including the issue's reproducer, if applicable)