From ff36a1cd88bfa339a1123c6fddcba20c190e2cfe Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 19 Dec 2024 18:40:41 -0800
Subject: [PATCH 1/3] fix: make sure `isDefEqSingleton` rule checks types

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 #6420
---
 src/Lean/Meta/ExprDefEq.lean | 11 +++++++----
 tests/lean/run/6420.lean     | 22 ++++++++++++++++++++++
 2 files changed, 29 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/6420.lean

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 71ef14f4d0f4..0cb63bc0cd4d 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -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
+    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),
diff --git a/tests/lean/run/6420.lean b/tests/lean/run/6420.lean
new file mode 100644
index 000000000000..7bb0e1b77070
--- /dev/null
+++ b/tests/lean/run/6420.lean
@@ -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?}"

From ac1ccc970802ba204f85479613c313a466dca825 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Fri, 20 Dec 2024 11:39:09 -0800
Subject: [PATCH 2/3] documentation

---
 src/Lean/Meta/ExprDefEq.lean | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 0cb63bc0cd4d..9d076052cd83 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1965,9 +1965,16 @@ where
       return false
     if !(← isAssignable sFn) then
       return false
+    -- The constructor with all parameters applied. The field is the remaining argument.
     let ctor := mkAppN (mkConst ctorVal.name sTypeFn.constLevels!) sType.getAppArgs
-    let Expr.forallE _ ty _ _ ← whnf (← inferType ctor) | return false
-    unless ← isDefEq ty (← inferType v) do
+    /-
+    We might not yet have ensured that `(?m ...).1` and `v` have defeq types, which is necessary for `⟨v⟩` to be type-correct.
+    By this point we have already done some of the work of `Lean.Meta.inferProjType`,
+    and from here getting the binding domain of `inferType ctor` is a reasonably efficient way to compute the type of `(?m ...).1`.
+    https://github.com/leanprover/lean4/issues/6420
+    -/
+    let .forallE _ ty _ _ ← whnf (← inferType ctor) | return false
+    unless (← isDefEq ty (← inferType v)) do
       return false
     let ctorApp := mkApp ctor v
     processAssignment' s ctorApp

From ea99def68397add4729c18c3a643f88890d0b96a Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sat, 21 Dec 2024 10:30:23 -0800
Subject: [PATCH 3/3] add metaprogramming-free example

---
 tests/lean/run/6420.lean | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/tests/lean/run/6420.lean b/tests/lean/run/6420.lean
index 7bb0e1b77070..f9431a20cf0b 100644
--- a/tests/lean/run/6420.lean
+++ b/tests/lean/run/6420.lean
@@ -20,3 +20,33 @@ structure foo where
   let rhs := Expr.app (.const ``foo.bar []) m
   let defeq? ← Meta.isDefEq lhs rhs
   logInfo m!"unifiable? {defeq?}"
+
+/-!
+The following example used to have the following error on 'example' due to creating a type-incorrect term:
+```
+application type mismatch
+  { t := Type }
+argument has type
+  Type 1
+but function has type
+  Type v → S
+```
+-/
+
+structure S.{u} where
+  t : Type u
+
+-- this error is on the first 'exact'
+/--
+error: type mismatch
+  m
+has type
+  S.t ?m : Type v
+but is expected to have type
+  Type : Type 1
+-/
+#guard_msgs in
+example (α : Type v) : Type := by
+  have m : (?m : S.{v}).t := ?n
+  exact m -- 'assumption' worked too
+  exact Nat