fix: reenable structure eta during tc search

gebner · gebner · commit 09cde790c353 · 2023-02-05T10:36:11.000-08:00
Fixes #2074.
diff --git a/src/Lean/Meta/SynthInstance.lean b/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 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
   -/
   withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
-                                          foApprox := true, ctxApprox := true, constApprox := false,
-                                          etaStruct := .notClasses }) do
+                                          foApprox := true, ctxApprox := true, constApprox := false }) 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
@@ -0,0 +1,66 @@
+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
diff --git a/tests/lean/run/tc_eta_struct_issue.lean b/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)
 
-variable [LawfulApplicative 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
