From e102cd4f4202b33adb303cae8aa2fdb5b3e4e512 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Jan 2021 11:59:58 -0800
Subject: [PATCH] fix: `checkAssignment` must be at `assignConst`

Example of issue fixed by this commit: the variables `xs` may have references to `mvar`.
---
 src/Lean/Meta/ExprDefEq.lean | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 59b9aef713..0b7b9e9785 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -846,17 +846,18 @@ private def assignConst (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool :=
       pure false
     else
       let some v ← mkLambdaFVarsWithLetDeps xs v | pure false
-      trace[Meta.isDefEq.constApprox]! "{mvar} := {v}"
-      checkTypesAndAssign mvar v
+      match (← checkAssignment mvar.mvarId! #[] v) with
+      | none   => pure false
+      | some v =>
+        trace[Meta.isDefEq.constApprox]! "{mvar} := {v}"
+        checkTypesAndAssign mvar v
 
 private def processConstApprox (mvar : Expr) (numArgs : Nat) (v : Expr) : MetaM Bool := do
   let cfg ← getConfig
   let mvarId := mvar.mvarId!
   let mvarDecl ← getMVarDecl mvarId
   if mvarDecl.numScopeArgs == numArgs || cfg.constApprox then
-    match (← checkAssignment mvarId #[] v) with
-    | none   => pure false
-    | some v => assignConst mvar numArgs v
+    assignConst mvar numArgs v
   else
     pure false