Bitten by same problem as RingOfIntegers

Stream: mathlib4

[Kevin Buzzard]

I made an abbrev ZHat : Type := (_ : Subring (some explicit product of concrete groups)), i.e. I defined it as a subring but, because of problems with slowdowns in docs#NumberField.RingOfIntegers, I then coerced it to a type. But it doesn't solve the RingOfIntegers slowdown problem; once the theory of normed fields is imported, typeclass search can't get NonUnitalCommRing ZHat from CommRing ZHat without timing out, because it keeps going down rabbitholes like

      [] [0.647223] ❌ apply @Subalgebra.seminormedCommRing to SeminormedCommRing ZHat2 ▼
        [tryResolve] [0.647166] ❌ SeminormedCommRing ZHat2 ≟ SeminormedCommRing ↥?m.5971 ▼
          [isDefEq] [0.647150] ❌ SeminormedCommRing ZHat2 =?= SeminormedCommRing ↥?m.5971 ▼
            [] [0.647106] ❌ ZHat2 =?= ↥?m.5971 ▼
              [] [0.647081] ❌ ↥{ carrier := {f | ∀ (D N : ℕ+) (h : ↑D ∣ ↑N), (ZMod.castHom h (ZMod ↑D)) (f N) = f D},
                      mul_mem' := @ZHat2.proof_2, one_mem' := ZHat2.proof_3, add_mem' := @ZHat2.proof_4,
                      zero_mem' := ZHat2.proof_5, neg_mem' := @ZHat2.proof_6 } =?= ↥?m.5971 ▶

and then

 [] [0.900950] ❌ apply @Subalgebra.normedCommRing to NormedCommRing ZHat2

with the same sort of trace, and you're usually in trouble if the ring structure explodes. I've had to fix it with def ZHat... instead of abbrev ZHat. Here's some code which indicates the problem.

import Mathlib.Data.ZMod.Basic
import Mathlib.RingTheory.Polynomial.Basic
--next import makes `#synth NonUnitalCommRing ZHat2` overflow
-- import Mathlib.Analysis.Normed.Field.Basic

def ZHat1 : Type :=
({
  carrier := { f : Π M : ℕ+, ZMod M | ∀ (D N : ℕ+) (h : (D : ℕ) ∣ N),
    ZMod.castHom h (ZMod D) (f N) = f D },
  zero_mem' := sorry
  neg_mem' := sorry
  add_mem' := sorry
  one_mem' := sorry
  mul_mem' := sorry
} : Subring (Π n : ℕ+, ZMod n))

-- works great
instance : CommRing ZHat1 := by unfold ZHat1; infer_instance

-- works great, even with `import Mathlib`
#synth NonUnitalCommRing ZHat1

-- now try with abbrev not def
abbrev ZHat2 : Type :=
({
  carrier := { f : Π M : ℕ+, ZMod M | ∀ (D N : ℕ+) (h : (D : ℕ) ∣ N),
    ZMod.castHom h (ZMod D) (f N) = f D },
  zero_mem' := sorry
  neg_mem' := sorry
  add_mem' := sorry
  one_mem' := sorry
  mul_mem' := sorry
} : Subring (Π n : ℕ+, ZMod n))

-- works great
instance commRing2 : CommRing ZHat2 := by infer_instance

-- but this is too slow with the normed field import
--set_option synthInstance.maxHeartbeats 40000 in
#synth NonUnitalCommRing ZHat2

For any kind of type coerced from a term, the algebra hierarchy is currently very fragile because of things like this (and of course, more imports make it worse)

[Eric Wieser]

I think the whole point in the "type not subring" trick was to also make the type semireducible

[Eric Wieser]

If you make it reducible (an abbrev), then the choice of type vs subring has no performance impact

[Eric Wieser]

As an aside, note that ({ a := _ } : A) can be written a little more concisely as { a := _ : A }

[Michael Stoll]

Kevin Buzzard said:

because it keeps going down rabbitholes like

I'm playing around with instance priorities in #12680, maybe this helps here?