synth `DecidableRel (α := ℚ≥0) (· ≤ ·)` fails

Stream: mathlib4

[Yuyang Zhao]

import Mathlib

#check instDecidableRelLe
#check instDecidableLe_mathlib

#synth DecidableRel (α := ℚ≥0) (· ≤ ·)

attribute [-instance] instDecidableRelLe

#synth DecidableRel (α := ℚ≥0) (· ≤ ·)

For some reason lean doesn't try docs#instDecidableLe_mathlib after trying docs#instDecidableRelLe.

[Kim Morrison]

I'm not sure what is going on there.

In any case, FirstOrder.Language.instDecidableRelLeOfRelMapLeSymbVecConsVecEmpty certainly shouldn't be a global instance.

[Yury G. Kudryashov]

Should docs#instDecidableRelLe be an instance? Does Lean try to apply it to any LE and Ord instances, then try to unify them?

[Yuyang Zhao]

It usually synthesizes successfully for other types, but lean still tries this instance.

import Mathlib

set_option trace.Meta.synthInstance true in
#synth DecidableRel (α := PNat) (· ≤ ·)
/-
[Meta.synthInstance] ✅️ DecidableRel fun x1 x2 => x1 ≤ x2 ▼
  [] new goal (a b : ℕ+) → Decidable ((fun x1 x2 => x1 ≤ x2) a b) ▶
  [] ❌️ apply FirstOrder.Language.instDecidableRelLeOfRelMapLeSymbVecConsVecEmpty to (a b : ℕ+) →
      Decidable ((fun x1 x2 => x1 ≤ x2) a b) ▶
  [] ❌️ apply @instDecidableRelLe to (a b : ℕ+) → Decidable ((fun x1 x2 => x1 ≤ x2) a b) ▶
  [] ✅️ apply @instDecidableLe_mathlib to (a b : ℕ+) → Decidable ((fun x1 x2 => x1 ≤ x2) a b) ▶
  [] result instDecidableLe_mathlib
-/

[Kim Morrison]

Anyone have a theory why there's a difference in behaviour between NNRat and PNat here? In both cases there are highly suspicious metavariables in trace, but for PNat that just causes the search branch to fail, while for NNRat it blows up and stops the search.

[Kim Morrison]

Kim Morrison said:

In any case, FirstOrder.Language.instDecidableRelLeOfRelMapLeSymbVecConsVecEmpty certainly shouldn't be a global instance.

#17271

[Eric Wieser]

What makes those instances bad but docs#instDecidableRelLe ok?

[Eric Wieser]

I thought it was fine to have these kinds of instances about other non-instances, because they never actually match unless you're working with the non-instance they are about

[Yury G. Kudryashov]

They don't match but they aren't rejected by the discrimination tree, and sometimes (not for these instances, but I saw a discussion about some Fintype non-instances) take a long time to fail defeq test.

[Yury G. Kudryashov]

E.g., if you're working with a large finite type and Lean tries to unfold everything to verify if they're defeq.