chore: add option to enable structure eta in tc search

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

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