Revert "fix: reenable structure eta during tc search"

The fix is blocked by slow defeq checks for TC instances; see issues
1986 and 2055.  Enabling it right now causes lots of timeouts in
mathlib4.
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/bump.20to.202023-02-06/near/326223768

This reverts commit 15a045ee66.

src/Lean/Meta/SynthInstance.lean

@@ -668,13 +668,13 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
   let opts ← getOptions
   let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
   /-
-  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
+    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
   -/
   withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
-                                          foApprox := true, ctxApprox := true, constApprox := false }) do
+                                          foApprox := true, ctxApprox := true, constApprox := false,
+                                          etaStruct := .notClasses }) do
     let type ← instantiateMVars type
     let type ← preprocess type
     let s ← get

tests/lean/run/2074.lean

@@ -1,66 +0,0 @@
-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

tests/lean/run/tc_eta_struct_issue.lean

@@ -1,5 +1,3 @@
--- 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
@@ -15,14 +13,10 @@ variable {F} [Applicative F]
 instance : Applicative (Op1 F) where
   pure := pure (f := F)
   seq f x := ((λ x f => f x) <$> x () <*> 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)
+  map := Functor.map (f := F)
 
 variable [LawfulApplicative F]
+
 instance : LawfulApplicative (Op1 F) := by
   constructor
   repeat sorry