From fedf235cba35ed8bf6bf571cf38e6d8536b904ac Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Jan 2023 17:21:38 -0800
Subject: [PATCH] fix: fixes #2011
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

In Lean 4, we have support for typing constraints of the form
```
(?m ...).1 =?= v
```
where the type of `?m ...` is a structure with a single field.
This kind of constraint is reduced to `?m ... =?= ⟨v⟩`

This feature is implemented by the function `isDefEqSingleton`.
As far as I remember, Lean 3 does not implement this feature.

This commit disables this feature if the structure is a class.
The goal is to avoid the generation of counterintuitive instances by
typing inference.

For example, in the example at issue #2011, the following weird
instance was being generated for `Zero (f x)`
```
(@Zero.mk (f x✝) ((@instZero I (fun i => f i) fun i => inst✝¹ i).1 x✝)
```
where `inst✝¹` is the local instance `[∀ i, Zero (f i)]`
Note that this instance is definitinally equal to the expected nicer
instance `inst✝¹ x✝`.
However, the nasty instance trigger nasty unification higher order
constraints later.

Note that a few tests broke because different error messages were
produced. The new error messages seem better. I do not expect this
change to affect Mathlib4 since Lean 3 does not have this feature.
---
 src/Lean/Meta/ExprDefEq.lean      | 18 ++++++++++++++++++
 tests/lean/1870.lean.expected.out | 29 ++++++++++++++---------------
 tests/lean/have.lean.expected.out | 10 ++++++----
 tests/lean/run/calcBug.lean       |  2 +-
 4 files changed, 39 insertions(+), 20 deletions(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 4ed5979357..6313f5178e 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1640,6 +1640,24 @@ private def isDefEqProj : Expr → Expr → MetaM Bool
 where
   /-- If `structName` is a structure with a single field and `(?m ...).1 =?= v`, then solve contraint as `?m ... =?= ⟨v⟩` -/
   isDefEqSingleton (structName : Name) (s : Expr) (v : Expr) : MetaM Bool := do
+    if isClass (← getEnv) structName then
+      /-
+      We disable this feature is `structName` is a class. See issue #2011.
+      The example at issue #2011, the following weird
+      instance was being generated for `Zero (f x)`
+      ```
+      (@Zero.mk (f x✝) ((@instZero I (fun i => f i) fun i => inst✝¹ i).1 x✝)
+      ```
+      where `inst✝¹` is the local instance `[∀ i, Zero (f i)]`
+      Note that this instance is definitinally equal to the expected nicer
+      instance `inst✝¹ x✝`.
+      However, the nasty instance trigger nasty unification higher order
+      constraints later.
+
+      We say this behavior is defensible because it is more reliable to use TC resolution to
+      assign `?m`.
+      -/
+      return false
     let ctorVal := getStructureCtor (← getEnv) structName
     if ctorVal.numFields != 1 then
       return false -- It is not a structure with a single field.
diff --git a/tests/lean/1870.lean.expected.out b/tests/lean/1870.lean.expected.out
index 8f5b51d420..d8ead1a047 100644
--- a/tests/lean/1870.lean.expected.out
+++ b/tests/lean/1870.lean.expected.out
@@ -1,17 +1,16 @@
-1870.lean:21:2-21:5: error: tactic 'rfl' failed, equality lhs
-  Zero.ofOfNat0
-is not definitionally equal to rhs
-  { zero := 1 }
-⊢ Zero.ofOfNat0 = { zero := 1 }
-1870.lean:26:2-26:11: error: tactic 'apply' failed, failed to unify
-  ?a = ?a
+1870.lean:20:2-20:35: error: type mismatch
+  congrArg (@OfNat.ofNat Nat 0) (congrArg (@Zero.toOfNat0 Nat) ?m)
+has type
+  OfNat.ofNat 0 = OfNat.ofNat 0 : Prop
+but is expected to have type
+  OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
+1870.lean:24:2-24:16: error: tactic 'apply' failed, failed to unify
+  ?f ?a₁ = ?f ?a₂
 with
-  Zero.ofOfNat0 = { zero := 1 }
-case h.h
-⊢ Zero.ofOfNat0 = { zero := 1 }
-1870.lean:31:2-31:11: error: tactic 'apply' failed, failed to unify
-  ?a = ?a
+  OfNat.ofNat 0 = OfNat.ofNat 1
+⊢ OfNat.ofNat 0 = OfNat.ofNat 1
+1870.lean:29:2-29:16: error: tactic 'apply' failed, failed to unify
+  ?f ?a₁ = ?f ?a₂
 with
-  Zero.ofOfNat0 = { zero := 1 }
-case h.h
-⊢ Zero.ofOfNat0 = { zero := 1 }
+  OfNat.ofNat 0 = OfNat.ofNat 1
+⊢ OfNat.ofNat 0 = OfNat.ofNat 1
diff --git a/tests/lean/have.lean.expected.out b/tests/lean/have.lean.expected.out
index c0980eb8c6..2265fae1b7 100644
--- a/tests/lean/have.lean.expected.out
+++ b/tests/lean/have.lean.expected.out
@@ -2,7 +2,9 @@ have.lean:4:0: error: expected term
 have.lean:2:18-2:19: error: don't know how to synthesize placeholder
 context:
 ⊢ False
-have.lean:6:15-6:16: error: synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
-  instOfNatNat 6
-inferred
-  { ofNat := 3 }
+have.lean:7:2-7:3: error: type mismatch
+  f
+has type
+  5 = 6 : Prop
+but is expected to have type
+  5 = 3 : Prop
diff --git a/tests/lean/run/calcBug.lean b/tests/lean/run/calcBug.lean
index f04caf586b..b60fca0a5e 100644
--- a/tests/lean/run/calcBug.lean
+++ b/tests/lean/run/calcBug.lean
@@ -5,7 +5,7 @@ open Nat
 theorem zero_add (n : Nat) : 0 + n = n :=
   Nat.recOn (motive := fun x => 0 + x = x)
    n
-   (show 0 + 0 = 0 from rfl)
+   rfl
    (fun (n : Nat) (ih : 0 + n = n) =>
     show 0 + succ n = succ n from
     calc