From adcca179918fcf1e30b150eb0fa3bad27a517bd0 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 21 Feb 2023 16:41:30 -0800
Subject: [PATCH] chore: add option to enable structure eta in tc search

---
 src/Lean/Meta/SynthInstance.lean |  8 +++-
 tests/lean/run/2074.lean         | 68 ++++++++++++++++++++++++++++++++
 2 files changed, 75 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/2074.lean

diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index 6b479c8080..b4311ef5d0 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -24,6 +24,11 @@ register_builtin_option synthInstance.maxSize : Nat := {
   descr := "maximum number of instances used to construct a solution in the type class instance synthesis procedure"
 }
 
+register_builtin_option synthInstance.etaExperiment : Bool := {
+  defValue := false
+  descr := "[DO NOT USE EXCEPT FOR TESTING] enable structure eta for type-classes during type-class search"
+}
+
 namespace SynthInstance
 
 def getMaxHeartbeats (opts : Options) : Nat :=
@@ -672,9 +677,10 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     See discussion at
       https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60constructor.60.20and.20.60Applicative.60/near/279984801
   -/
+  let etaStruct := if synthInstance.etaExperiment.get (← getOptions) then .all else .notClasses
   withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
                                           foApprox := true, ctxApprox := true, constApprox := false,
-                                          etaStruct := .notClasses }) do
+                                          etaStruct }) do
     let type ← instantiateMVars type
     let type ← preprocess type
     let s ← get
diff --git a/tests/lean/run/2074.lean b/tests/lean/run/2074.lean
new file mode 100644
index 0000000000..52d68f6e8c
--- /dev/null
+++ b/tests/lean/run/2074.lean
@@ -0,0 +1,68 @@
+set_option synthInstance.etaExperiment true -- TODO: make work by default
+
+class NonUnitalNonAssocSemiring (α : Type u)
+
+class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α
+
+class Semiring (α : Type u) extends NonUnitalSemiring α
+
+class NonUnitalCommSemiring (α : Type u) extends NonUnitalSemiring α
+
+class CommSemiring (R : Type u) extends Semiring R
+
+class NonUnitalNonAssocRing (α : Type u) extends NonUnitalNonAssocSemiring α
+
+class NonUnitalRing (α : Type _) extends NonUnitalNonAssocRing α, NonUnitalSemiring α
+
+class Ring (R : Type u) extends Semiring R
+
+class NonUnitalCommRing (α : Type u) extends NonUnitalRing α
+
+class CommRing (α : Type u) extends Ring α
+
+instance (priority := 100) NonUnitalCommRing.toNonUnitalCommSemiring [s : NonUnitalCommRing α] :
+    NonUnitalCommSemiring α :=
+  { s with }
+
+instance (priority := 100) CommRing.toCommSemiring [s : CommRing α] : CommSemiring α :=
+  { s with }
+
+instance (priority := 100) CommSemiring.toNonUnitalCommSemiring [s : CommSemiring α] :
+    NonUnitalCommSemiring α :=
+  { s with }
+
+instance (priority := 100) CommRing.toNonUnitalCommRing [s : CommRing α] : NonUnitalCommRing α :=
+  { s with }
+
+class StarRing' (R : Type _) [NonUnitalSemiring R]
+def starGizmo [CommSemiring R] [StarRing' R] : R → R := id
+theorem starGizmo_foo [CommRing R] [StarRing' R] (x : R) : starGizmo x = x := rfl
+
+namespace ReidMWE
+
+class A (α : Type u)
+
+class B (α : Type u) extends A α
+
+class C (α : Type u) extends B α
+
+class D (α : Type u) extends B α
+
+class E (α : Type u) extends C α, D α
+
+class F (α : Type u) extends A α
+
+class G (α : Type u) extends F α, B α
+
+class H (α : Type u) extends C α
+
+class I (α : Type u) extends G α, D α
+
+class J (α : Type u) extends H α, I α, E α
+
+class StarRing' (R : Type 0) [B R]
+def starGizmo [E R] [StarRing' R] : R → R := id
+
+theorem starGizmo_foo [J R] [StarRing' R] (x : R) : starGizmo x = x := rfl
+
+theorem T (i : J R) : (@D.toB.{0} R (@E.toD.{0} R (@J.toE.{0} R i))) = i.toB := rfl