fix: make sure isDefEqSingleton rule checks types
#6421
Conversation
This PR fixes an issue where the `isDefEqSingleton` rule could apply in inappropriate situations. In particular, if `S` is a one-field structure with field `f`, then `S.f ?m =?= v` was being reduced to `?m =?= { f := v }` even if `{ f := v }` was type-incorrect.
Closes leanprover#6420
kmill
added
awaiting-review
github-actions
bot
added
the
toolchain-available
leanprover-community-bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
leanprover-community-bot
added
builds-mathlib
|
@leodemoura I made this PR to validate the explanation of #6420. I don't know the isDefEq code well enough to know if there is a better way to implement this — perhaps you would want to implement it differently. The bug is low priority. There were two places where mathlib was somehow taking advantage of this bug, but neither looked intentional. |
| else | ||
| if !(← isAssignable sFn) then | ||
| return false | ||
| let ctor := mkAppN (mkConst ctorVal.name sTypeFn.constLevels!) sType.getAppArgs |
There was a problem hiding this comment.
Could you please add a comment explaining this change? It can be based on the PR description.
Additional requests regarding coding convetion:
let Expr.forallE _ ty ...=>let .forallE _ ty ...unless ← isDefEq ty (← inferType v) do=>unless (← isDefEq ty (← inferType v)) do
There was a problem hiding this comment.
Done.
General question about isDefEq that came up in a Zulip discussion: some users believe that you are not supposed to use isDefEq on terms if you have not already ensured isDefEq for their inferred types. Is that the case?
If so, then this PR is not necessary, but it would raise a bunch of questions for me (I don't recall seeing any meta code that specifically ensured isDefEq on inferred types).
There was a problem hiding this comment.
I don't have time to context switch to this module right now. Moreover, I feel like this is going to be a really long thread. Let's create one at the Lean FRO Zulip.
BTW, I want to minimize as much as possible changes to ExprDefEq.lean, and do it in batches whenever we decide to the context switch.
That said, at first sight, this PR is consistent with the current design. We already have functions such as checkTypesAndAssign.
There was a problem hiding this comment.
BTW, were you able to trigger the bug without meta-programming? If not, I prefer to put this PR on hold.
There was a problem hiding this comment.
No problem, it's low-priority. I'll let you know if I manage to trigger it without meta-programming.
There was a problem hiding this comment.
Just to let you know, I pushed a simple example that uses just the have and exact tactics. (Please feel free to keep this PR on hold.)
This PR fixes an issue where the
isDefEqSingletonrule could apply in inappropriate situations. In particular, ifSis a one-field structure with fieldf, thenS.f ?m =?= vwas being reduced to?m =?= { f := v }even if{ f := v }was type-incorrect.Closes #6420