Decidable (Eq, LE,...) requirement in definition

Stream: mathlib4

[Weiyi Wang]

In #27055, @Kevin Buzzard brought up a good point about requiring Decidability for definition (and also recommended me creating this thread). My original code looked like

def coeff {G: Type*} [PartialOrder G] (c i : G) := open Classical in if c ≤ i then 0 else ...

and the suggestion was to remove open Classical in and adding [DecidableLE G], because for some G this could be decidable and we don't want to use the classical instance on them. This makes sense to me. I'd like to understand a more general guideline similar to this, as there are other existing definitions that doesn't seem to follow this logic (e.g. HahnSeries.single).

My current understanding is: if the if condition involves generic types that could make it decidable, then the decidability should be put in parameters and let downstream user decide whether to use classical or provide decidable types. If the if condition involves a more concrete type that is not likely going to be decidable in most cases, then one should open classical in the definition. Does this sound about right?

And perhaps we can add related guideline in https://leanprover-community.github.io/contribute/style.html ?

[Kevin Buzzard]

Just to say that I am not confident that open Classical in will cause problems, but my instinct is that [DecidableLE] will not cause problems in the definition; it will however cause problems for mathemtical users of the definition in that they'll have to supply some mathematically spurious hypothesis.