lower instance priority on Prop implying Prop

Stream: mathlib4

[Yakov Pechersky]

In #18382, I provide/generalize the following instances:

-- See note [lower instance priority]
instance (priority := 100) _root_.PrincipalIdealRing.isNoetherianRing [IsPrincipalIdealRing R] :
    IsNoetherianRing R where
  noetherian S := (IsPrincipalIdealRing.principal S).FG

-- See note [lower instance priority]
instance (priority := 100) _root_.IsPrincipalIdealRing.of_isNoetherianRing_of_isBezout
    [IsNoetherianRing R] [IsBezout R] : IsPrincipalIdealRing R where
  principal S := IsBezout.isPrincipal_of_FG S (IsNoetherian.noetherian S)

In a comment, @Andrew Yang guided me to make sure that I lower the priorities, according to our library note. Initially, I did not have lower priorities, thinking that for such "Prop implies Prop" instances, the lean4 TC system will resolve loops. The library note discusses forgetful instances (data carrying), which I think is like "you get Noetherian when you have PIR". But how about "PIR when you have Noetherian and Bezout"? What's the general guidance for instance priorities on such "prop implies prop" classes?

[Andrew Yang]

I might have not made myself clear in my comment on the PR, but the point is that result type (the thing after :) is too generic and will trigger a (often non-necessary) extensive search and it has little to do about loops and data.

[Yakov Pechersky]

And, if I understand correctly, since in the context of lemmas about some PIR, we're more likely to have that as an "explicit" instance argument, it's better to lower the priority on these so that they don't override? I'm not sure I understand the line that is drawn about what counts as "too generic".

[Kyle Miller]

I guess one thing here that's suboptimal is that together these mean that if you're looking for IsNoetherianRing R, then it will look for IsBezout R unnecessarily. Not sure if there's anything that can be done about that.

[Andrew Yang]

By too generic I meant that the result type is MyClass X where X is a variable and not some complex terms.