fix: make sure isDefEqSingleton rule checks types

src/Lean/Meta/ExprDefEq.lean

@@ -1963,11 +1963,21 @@ 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
+    -- The constructor with all parameters applied. The field is the remaining argument.
+    let ctor := mkAppN (mkConst ctorVal.name sTypeFn.constLevels!) sType.getAppArgs
+    /-
+    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
 
 /--
   Given applications `t` and `s` that are in WHNF (modulo the current transparency setting),

tests/lean/run/6420.lean

@@ -0,0 +1,52 @@
+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?}"
+
+/-!
+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