Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

simpa type mismatch error message could be improved #4101

Closed
kmill opened this issue May 7, 2024 · 0 comments · Fixed by #5648
Closed

simpa type mismatch error message could be improved #4101

kmill opened this issue May 7, 2024 · 0 comments · Fixed by #5648
Labels
bug Something isn't working P-medium We may work on this issue if we find the time

Comments

@kmill
Copy link
Collaborator

kmill commented May 7, 2024

Description

When doing simpa using e, if the simplified type of e is not defeq to the simplified type of the target, then the error message is obscure, saying that h✝ has a type mismatch.

Context

This came up on Zulip

Steps to Reproduce

Here is an example:

example (p q : Prop) (hp : p ∧ True) : p ∧ q ∧ True := by
  simpa using hp
/-
type mismatch
  h✝
has type
  p : Prop
but is expected to have type
  p ∧ q : Prop
-/

The expected behavior is that the error message explains that the simplified type of hp is p and the simplified target is p ∧ q, and that it doesn't mention the inaccessible variable created by simpa to process the using expression.

Versions

4.8.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.
@kmill kmill added the bug Something isn't working label May 7, 2024
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Aug 23, 2024
@kmill kmill mentioned this issue Oct 8, 2024
Merged
github-merge-queue bot pushed a commit that referenced this issue Oct 8, 2024
@kmill
fix: have simpa ... using ... do exact-like checks (#5648)
15bb8a2 
Closes #5634. Before assigning the simplified `using` clause expression
to the goal, this adds a check that the expression has no new
metavariables. It also adjusts how new hypotheses are added to the goal
to prevent spurious "don't know how to synthesize placeholder" errors on
that goal metavariable. We also throw in an occurs check immediately
after elaboration to avoid some counterintuitive behavior when
simplifying such a term closes the goal.

Closes #4101. This also improves the type mismatch error message,
showing the elaborated `using` clause rather than `h✝`:
```lean
example : False := by
  simpa using (fun x : True => x)
/-
error: type mismatch, term
  fun x => x
after simplification has type
  True : Prop
but is expected to have type
  False : Prop
-/
```
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working P-medium We may work on this issue if we find the time
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

fix: have simpa ... using ... do exact-like checks kmill/lean4
2 participants
@kmill @leanprover-bot