From fc404af645af2fdaa0fd1bfae4293b5466e51c56 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 12 Feb 2020 13:21:56 -0800
Subject: [PATCH] =?UTF-8?q?feat:=20solve=20`=3Fm=20t=20=3D=3F=3D=20c`=20ev?=
 =?UTF-8?q?en=20when=20constApprox=20is=20disabled?=

---
 src/Init/Lean/Meta/ExprDefEq.lean |  2 +-
 tests/lean/run/newfrontend1.lean  | 11 +++++++++--
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean
index b370077c8c..632ae6c234 100644
--- a/src/Init/Lean/Meta/ExprDefEq.lean
+++ b/src/Init/Lean/Meta/ExprDefEq.lean
@@ -611,7 +611,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
     arg ← simpAssignmentArg arg;
     let args := args.set ⟨i, h⟩ arg;
     let useConstApprox : Unit → MetaM Bool := fun _ =>
-      if cfg.constApprox then
+      if cfg.constApprox || (not args.isEmpty && not v.isApp) then
         processConstApprox mvar args.size v
       else
         pure false;
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index 1fe6c162ff..f7cb3d4302 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -224,8 +224,6 @@ set_option pp.all true
 def g1 {α} (a₁ a₂ : α) {β} (b : β) : α × α × β :=
 (a₁, a₂, b)
 
-#check @(g1 true)
-
 def id1 : {α : Type} → α → α :=
 fun x => x
 
@@ -244,6 +242,15 @@ fun x => id1 x
 def id5 : {α : Type} → α → α :=
 @(fun α x => id1 x)
 
+def id6 : {α : Type} → α → α :=
+fun {α} x => id1 x
+
+def id7 : {α : Type} → α → α :=
+fun {α} x => @id α x
+
+def id8 : {α : Type} → α → α :=
+fun {α} x => id (@id α x)
+
 def altTst1 {m σ} [Alternative m] [Monad m] : Alternative (StateT σ m) :=
 ⟨StateT.failure, StateT.orelse⟩