fix: reenable structure eta during tc search

Fixes #2074.

src/Lean/Meta/SynthInstance.lean

@@ -24,11 +24,6 @@ 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 :=
@@ -664,14 +659,13 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
   withTraceNode `Meta.synthInstance
     (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
   /-
-    We disable eta for structures that are not classes during TC resolution because it allows us to find unintended solutions.
-    See discussion at
-      https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60constructor.60.20and.20.60Applicative.60/near/279984801
+  We explicitly enable eta for structures because that is required to make
+  subobject projections and constructor applications commute (and we would get
+  non-defeq diamonds otherwise).
+  https://github.com/leanprover/lean4/issues/2074#issuecomment-1418198304
   -/
-  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 }) do
+                                          foApprox := true, ctxApprox := true, constApprox := false }) do
     let type ← instantiateMVars type
     let type ← preprocess type
     let s ← get

tests/lean/run/2074.lean

@@ -1,5 +1,3 @@
-set_option synthInstance.etaExperiment true -- TODO: make work by default
-
 class NonUnitalNonAssocSemiring (α : Type u)
 
 class NonUnitalSemiring (α : Type u) extends NonUnitalNonAssocSemiring α

tests/lean/run/tc_eta_struct_issue.lean

@@ -1,3 +1,5 @@
+-- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60constructor.60.20and.20.60Applicative.60/near/279949125
+
 def Op1 (F : Type u → Type v) α := F α
 
 namespace Op1
@@ -13,10 +15,14 @@ variable {F} [Applicative F]
 instance : Applicative (Op1 F) where
   pure := pure (f := F)
   seq f x := ((λ x f => f x) <$> x () <*> f : F _)
-  map := Functor.map (f := F)
+
+  -- The original version of this mwe did not specify the mapConst etc. instances,
+  -- causing a non-defeq diamond.  Non-defeq diamonds for classes like Functor
+  -- are not supported.
+
+  -- map := Functor.map (f := F)
 
 variable [LawfulApplicative F]
-
 instance : LawfulApplicative (Op1 F) := by
   constructor
   repeat sorry