diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 21a409481f..6b479c8080 100644 --- 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 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 diff --git a/tests/lean/run/2074.lean b/tests/lean/run/2074.lean deleted file mode 100644 index 7d81ea356c..0000000000 --- a/tests/lean/run/2074.lean +++ /dev/null @@ -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 diff --git a/tests/lean/run/tc_eta_struct_issue.lean b/tests/lean/run/tc_eta_struct_issue.lean index 9d5902d808..d4b085bfbd 100644 --- a/tests/lean/run/tc_eta_struct_issue.lean +++ b/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