From ec7be1d801252ac5d9bec29334a6995ca41b9dd1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 11 Jan 2021 15:22:10 -0800
Subject: [PATCH] feat: add `processAssignment'`

---
 src/Lean/Meta/ExprDefEq.lean | 26 +++++++++++++++++++++++---
 1 file changed, 23 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index cc4a80fcf4..bf80ec3681 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -905,6 +905,27 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
               checkTypesAndAssign mvar v
     process 0 mvarApp.getAppArgs v
 
+/--
+  Similar to processAssignment, but if it fails, compute v's whnf and try again.
+  This helps to solve constraints such as `?m =?= { α := ?m, ... }.α`
+  Note this is not perfect solution since we still fail occurs check for constraints such as
+  ```lean
+    ?m =?= List { α := ?m, β := Nat }.β
+  ```
+-/
+private def processAssignment' (mvarApp : Expr) (v : Expr) : MetaM Bool := do
+  if (← processAssignment mvarApp v) then
+    return true
+  else
+    let vNew ← whnf v
+    if vNew != v then
+      if mvarApp == vNew then
+        return true
+      else
+        processAssignment mvarApp vNew
+    else
+      return false
+
 private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) :=
   match t.getAppFn with
   | Expr.const c _ _ => getConst? c
@@ -1218,11 +1239,10 @@ private partial def isDefEqQuickOther (t s : Expr) : MetaM LBool := do
       let sAssign? ← isAssignable sFn
       let assignableMsg (b : Bool) := if b then "[assignable]" else "[nonassignable]"
       trace[Meta.isDefEq]! "{t} {assignableMsg tAssign?} =?= {s} {assignableMsg sAssign?}"
-      let assign (t s : Expr) : MetaM LBool := toLBoolM $ processAssignment t s
       if tAssign? && !sAssign? then
-        toLBoolM $ processAssignment t s
+        toLBoolM <| processAssignment' t s
       else if !tAssign? && sAssign? then
-        toLBoolM $ processAssignment s t
+        toLBoolM <| processAssignment' s t
       else if !tAssign? && !sAssign? then
         if tFn.isMVar || sFn.isMVar then
           let ctx ← read