DecidablePred failing with lexicographic ordering

Stream: general

[Praneeth Kolichala]

I'm running into an issue where instance search is failing to synthesize instances for the decidability of the predicate, even when it can find the decidability of the specialization of the predicate. This seems to only happen when the predicate has something to do with lexicographic ordering:

import Mathlib.Order.Basic
import Mathlib.Data.Prod.Lex

variable {n : ℕ}

-- For each particular `n`, deciding if (0, 1) <= (n, 0) is decidable
#synth Decidable (LE.le (α := ℕ ×ₗ ℤ) (0, 1) (n, 0)) -- succeeds
-- But we can't show that this is actually a decidable predicate!
#synth DecidablePred (fun n : ℕ => LE.le (α := ℕ ×ₗ ℤ) (0, 1) (n, 0)) -- fails

If we replace the lexicographic ordering with the product partial order, then it succeeds. Similarly other minor variations succeed:

#synth Decidable ((0, 1) ≤ (n, 0))  -- succeeds
#synth DecidablePred (fun n : ℕ => (0, 1) ≤ (n, 0))  -- also succeeds
#synth DecidablePred (fun n : ℕ => LE.le (α := ℕ ×ₗ ℤ) (0, 1) (1, 0)) -- fails
#synth DecidablePred (fun n : ℕ => True → LE.le (α := ℕ ×ₗ ℤ) (0, 1) (1, 0)) -- succeeds?!

Can anyone explain this?

[Gabriel Ebner]

Type aliases are evil. That's why we're moving them to structures where easily possible, or at least add functions like toLex : α → Lex α that do not break the abstraction. In your example, the defeq α = Lex α leaks and Lean tries to synthesize an instance of LinearOrder (Nat × Nat) which of course breaks.

[Gabriel Ebner]

The reason it leaks is because (0, 1) has the type Nat × Nat, and not Lex (Nat × Nat).

[Gabriel Ebner]

It works if you use toLex:

#synth DecidablePred fun n => toLex (0, 1) ≤ toLex (n, 0) -- succeeds