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

fix: make sure isDefEqSingleton rule checks types #6421

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open

fix: make sure isDefEqSingleton rule checks types #6421

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ff36a1c
fix: make sure `isDefEqSingleton` rule checks types
kmill Dec 20, 2024
ac1ccc9
documentation
kmill Dec 20, 2024
ea99def
add metaprogramming-free example
kmill Dec 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 7 additions & 4 deletions src/Lean/Meta/ExprDefEq.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1963,11 +1963,14 @@ where
let sFn := s.getAppFn
if !sFn.isMVar then
return false
if (← isAssignable sFn) then
let ctorApp := mkApp (mkAppN (mkConst ctorVal.name sTypeFn.constLevels!) sType.getAppArgs) v
processAssignment' s ctorApp
else
if !(← isAssignable sFn) then
return false
let ctor := mkAppN (mkConst ctorVal.name sTypeFn.constLevels!) sType.getAppArgs
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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).

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BTW, were you able to trigger the bug without meta-programming? If not, I prefer to put this PR on hold.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No problem, it's low-priority. I'll let you know if I manage to trigger it without meta-programming.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.)

let Expr.forallE _ ty _ _ ← whnf (← inferType ctor) | return false
unless ← isDefEq ty (← inferType v) do
return false
let ctorApp := mkApp ctor v
processAssignment' s ctorApp

/--
Given applications `t` and `s` that are in WHNF (modulo the current transparency setting),
Expand Down
22 changes: 22 additions & 0 deletions tests/lean/run/6420.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
import Lean
/-!
# Testing fix to `isDefEqSingleton`
https://github.com/leanprover/lean4/issues/6420
-/

/-!
The following example used to print `unifiable? true`.
-/
open Lean

structure foo where
bar : Nat

/-- info: unifiable? false -/
#guard_msgs in
#eval show MetaM Unit from do
let lhs := Expr.const ``foo []
let m ← Meta.mkFreshExprMVar lhs
let rhs := Expr.app (.const ``foo.bar []) m
let defeq? ← Meta.isDefEq lhs rhs
logInfo m!"unifiable? {defeq?}"
Loading