why can't Lean generate this instance?

Stream: general

[Kenny Lau]

universes u

example {α β : Type u} [discrete_linear_ordered_field α] (f : β → α) (x : α) :
  decidable_pred (λ i, x < f i) :=
by apply_instance

why does this fail?

error state:

tactic.mk_instance failed to generate instance for
  decidable_pred (λ (i : β), x < f i)
state:
α β : Type u,
_inst_1 : discrete_linear_ordered_field α,
f : β → α,
x : α
⊢ decidable_pred (λ (i : β), x < f i)

[Yury G. Kudryashov]

Did you try to look at the trace?

[Kenny Lau]

yeah it keeps trying a billion things on the lambda thing

[Kenny Lau]

actually it substituted in the lambda so it's trying to prove some (_ : \a) < _ is decidable

[Kenny Lau]

but somehow it never finds the right instance

[Chris Hughes]

If you beta reduce it does it work?

[Kenny Lau]

so you mean intro?

[Yury G. Kudryashov]

If I put decidable_linear_order instead of discrete*, it works.

[Yury G. Kudryashov]

Doesn't work with decidable_linear_ordered_comm_group

[Kenny Lau]

can this be solved with some priority hacking?

[Yury G. Kudryashov]

It tries has_lt.lt.decidable but for some reason defeq fails.

[Yury G. Kudryashov]

@Gabriel Ebner ?

[Yury G. Kudryashov]

@Simon Hudon ?

[Gabriel Ebner]

The surprising thing is that the following works:

example {α β : Type u} [discrete_linear_ordered_field α] (f : β → α) (x : α) (i : β) :
  decidable (x < f i) :=
by apply_instance

[Yury G. Kudryashov]

I don't know how to debug this...

[Gabriel Ebner]

Problem seems to be in unification, because the type-class search creates higher-order patterns like ?x_123 a:

-- also fails
example {α β : Type u} [discrete_linear_ordered_field α] (f : β → α) (x : α) :
  ∀ i, decidable (x < f i) :=
by apply_instance

[Gabriel Ebner]

I haven't got a good explanation either, but here's a workaround:

instance foo {α} [discrete_linear_ordered_field α] (a b : α) : decidable (a < b) :=
by apply_instance