adding imports breaks class inference?

Stream: mathlib4

[Filippo A. E. Nuccio]

I really do not understand what is going on here: this first bit works perfectly

import Mathlib.RingTheory.DiscreteValuationRing.Basic

lemma foo (A : Type _) [CommRing A] [IsDomain A] [DiscreteValuationRing A] : IsNoetherianRing A := by
  infer_instance

Suppose now that I have a valuation ring, that I assume to be a DVR, is noetherian: I can import Mathlib.RingTheory.Valuation.ValuationSubring and then

import Mathlib.RingTheory.DiscreteValuationRing.Basic
import Mathlib.RingTheory.Valuation.ValuationSubring

lemma bar (L Γ: Type _) [Field L] [LinearOrderedCommGroupWithZero Γ] {w : Valuation L Γ}
  [DiscreteValuationRing w.valuationSubring] : IsNoetherianRing w.valuationSubring := by
  infer_instance

is also OK. But if I am importing Mathlib.RingTheory.DedekindDomain.AdicValuation as well, the second code breaks:

import Mathlib.RingTheory.DiscreteValuationRing.Basic
import Mathlib.RingTheory.DedekindDomain.AdicValuation
import Mathlib.RingTheory.Valuation.ValuationSubring

lemma bar (L Γ: Type _) [Field L] [LinearOrderedCommGroupWithZero Γ] {w : Valuation L Γ}
  [DiscreteValuationRing w.valuationSubring] : IsNoetherianRing w.valuationSubring := by
  infer_instance
-- failed to synthesize
--  IsNoetherian (↥Valuation.valuationSubring w) (↥Valuation.valuationSubring w)
-- (deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

(and I have tried all the $6=\vert\mathfrak{S}_3\vert$ permutations of the import with the same result). Nevertheless, the first still works, and therefore I can make do with the following

import Mathlib.RingTheory.Valuation.ValuationSubring
import Mathlib.RingTheory.DiscreteValuationRing.Basic
import Mathlib.RingTheory.DedekindDomain.AdicValuation

lemma foo (A : Type _) [CommRing A] [IsDomain A] [DiscreteValuationRing A] : IsNoetherianRing A := by
  infer_instance --this is still OK

lemma bar (L Γ: Type _) [Field L] [LinearOrderedCommGroupWithZero Γ] {w : Valuation L Γ}
  [DiscreteValuationRing w.valuationSubring] : IsNoetherianRing w.valuationSubring := by
  apply foo -- it works!

So I am mainly puzzled by three things:

1. Adding an import breaks an infer_instance;
2. Adding this import breaks the inference that the valuation subring is Noetherian, but here the noetherianity is just a consequence of the assumption that w.valuationSubring be a DVR (and should really have nothing to do about the fact that it is a valuation subring, rather than an arbitrary CommRing that is a DVR), and for such a ring foo works;
3. The lemma foo does nothing but applying an instance, yet apply foo is able to close bar, but infer_instance is not.

[Kevin Buzzard]

Adding the import just makes typeclass inference time out because it goes on a wild goose chase. You can fix it with set_option synthInstance.maxHeartbeats 200000 in.

[Adam Topaz]

What’s the trace? Is there something we need to fix?

[Kevin Buzzard]

                [] [5.874236s] ✅ apply @SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing to IsDomain
                      (↥Valuation.valuationSubring w) ▶

is what it finds with the extra import.

[Kevin Buzzard]

It's one of these again:

                      [] [2.918449s] ✅ CommSemiring.toSemiring =?= Ring.toSemiring ▼
                        [] [2.918426s] ✅ Ring.toSemiring =?= Ring.toSemiring ▼
                          [delta] [2.918418s] ✅ Ring.toSemiring =?= Ring.toSemiring ▼
                            [] [2.918405s] ✅ CommRing.toRing =?= SubringClass.toRing (Valuation.valuationSubring w) ▼
                              [] [2.918349s] ✅ CommRing.toRing =?= Function.Injective.ring Subtype.val _ _ _ _ _ _ _ _ _ _ _ _ ▼
                                [] [2.918273s] ✅ CommRing.toRing =?= let src := Function.Injective.mulZeroClass Subtype.val _ _ _;
                                    let src_1 := Function.Injective.addGroupWithOne Subtype.val _ _ _ _ _ _ _ _ _ _;
                                    let src_2 := Function.Injective.addCommGroup Subtype.val _ _ _ _ _ _ _;
                                    let src_3 := Function.Injective.monoid Subtype.val _ _ _ _;
                                    let src_4 := Function.Injective.distrib Subtype.val _ _ _;
                                    Ring.mk AddGroupWithOne.zsmul _ ▶

[Kevin Buzzard]

                                     [] [2.918170s] ✅ Ring.mk Ring.zsmul _ =?= Ring.mk AddGroupWithOne.zsmul _ ▼
                                        [] [0.347698s] ✅ Ring.zsmul =?= AddGroupWithOne.zsmul ▶
                                        [] [1.561553s] ✅ Ring.toSemiring =?= Semiring.mk _ _ Monoid.npow ▼
                                          [] [1.561492s] ✅ (Function.Injective.ring Subtype.val _ _ _ _ _ _ _ _ _ _ _ _).1 =?= Semiring.mk _ _ Monoid.npow ▼
                                            [] [1.561451s] ✅ Semiring.mk _ _ Monoid.npow =?= Semiring.mk _ _ Monoid.npow ▼
                                              [] [0.276237s] ✅ Monoid.npow =?= Monoid.npow ▶
                                              [] [0.616143s] ✅ NonUnitalSemiring.mk _ =?= NonUnitalSemiring.mk _ ▶
                                              [] [0.337922s] ✅ AddMonoidWithOne.toOne =?= AddMonoidWithOne.toOne ▶
                                              [] [0.330563s] ✅ AddMonoidWithOne.toNatCast =?= AddMonoidWithOne.toNatCast ▶
                                        [] [0.336362s] ✅ Ring.toNeg =?= AddGroupWithOne.toNeg ▶
                                        [] [0.338485s] ✅ Ring.toSub =?= AddGroupWithOne.toSub ▶
                                        [] [0.333761s] ✅ Ring.toIntCast =?= AddGroupWithOne.toIntCast ▶

etc

[Filippo A. E. Nuccio]

Kevin Buzzard said:

                [] [5.874236s] ✅ apply @SubringClass.instIsDomainSubtypeMemInstMembershipToSemiringToRing to IsDomain
                      (↥Valuation.valuationSubring w) ▶

is what it finds with the extra import.

Ah, so it tries to understand that it is a domain as a subring of a domain instead of just seeing that it is a DVR?