Decidable vs decidable_rel

Stream: general

[Eric Wieser]

What's going on here?

import algebra.order.group.instances

 -- change to `linear_order α` and everything works
variables {α : Type*} [linear_ordered_add_comm_group α]

--ok
example (a b : α) : decidable (a < b) := by apply_instance
--fail
example : Π (a b : α), decidable (a < b) := by apply_instance
example : decidable_rel ((<) : α → α → Prop) := by apply_instance
example : decidable_rel ((<) : α → α → Prop) :=
by { dunfold decidable_rel, apply_instance }
-- ok
example : decidable_rel ((<) : α → α → Prop) := λ a b, by apply_instance

It seems that somehow apply_instance can't see through the binders, even though the above works fine with docs#linear_order instead of docs#linear_ordered_add_comm_group

[Eric Wieser]

attribute [instance] linear_ordered_add_comm_group.decidable_lt

also seems to fix it, cc @Joseph Myers who did that (but only locally) in #17657

[Eric Wieser]

Ah, this was discussed before at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/type.20class.20inference.20issues/near/276937942