fix: make elabTermEnsuringType respect errToSorry when there is a type mismatch
#3633
Conversation
This file contains 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
leodemoura
approved these changes
Mar 7, 2024
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
… type mismatch Floris van Doorn [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/have.20tactic.20error.20recovery/near/425283053) that it is confusing that the `have : T := e` tactic completely fails if the body `e` is not of type `T`. This is in contrast to `have : T := by exact e`, which does not completely fail when `e` fails to have type `T`. This ends up being caused by `elabTermEnsuringType` throwing an error when it fails inserting a coercion. Now, it detects this case, and it checks the `errToSorry` flag to decide whether to throw the error or to log the error and insert a `sorry`. This is justified by `elabTermEnsuringType` being a frontend to `elabTerm`, which inserts `sorry` on error. An alternative would be to make `ensureType` respect `errToSorry`, but there exists code that catch errors from this function.
kmill
force-pushed
the
elabTermEnsuringType
branch
from
49e1e04
to
738d34b
Compare
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 7, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Mar 7, 2024
leanprover-community-mathlib4-bot
added
the
builds-mathlib
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Mar 7, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Mar 7, 2024
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.
Floris van Doorn reported on Zulip that it is confusing that the
have : T := etactic completely fails if the bodyeis not of typeT. This is in contrast tohave : T := by exact e, which does not completely fail wheneis not of typeT.This ends up being caused by
elabTermEnsuringTypethrowing an error when it fails to insert a coercion. Now, it detects this case, and it checks theerrToSorryflag to decide whether to throw the error or to log the error and insert asorry.This is justified by
elabTermEnsuringTypebeing a frontend toelabTerm, which insertssorryon error.An alternative would be to make
ensureTyperespecterrToSorry, but there exists code that expects being able to catch whenensureTypefails. Making such code manipulateerrToSorryseems error prone, and this function is not a main entry point to the term elaborator, unlikeelabTermEnsuringType.