Why's `noncomputable linear_ordered` preferred over `orde...

Stream: general

[Junyan Xu]

• Lean's typeclass inference prefers docs#ordered_add_comm_group over docs#linear_ordered_add_comm_group, so it doesn't demand I mark test1 below noncomputable. (Or maybe it just finds the former before the latter.)
• A similar test shows it also prefers docs#ordered_ring over docs#linear_ordered_ring.
• However, it prefers docs#linear_ordered_comm_ring over docs#ordered_comm_ring, as test2 below shows (you may delete the first two instances when testing the last two).
• This is currently making docs#surreal.dyadic_map noncomputable in my surreal multiplication branch. I tried to lower the priority of the linear_ordered_comm_ring instance, but to no avail.

• What could be the cause of these behaviors? For reference:
  linear_ordered_add_comm_group extends ordered_add_comm_group α, linear_order α
linear_ordered_ring extends ordered_ring α, linear_order α, nontrivial α
linear_ordered_comm_ring extends linear_ordered_ring α, comm_monoid α

• Can we make Lean always prefer the computable instance when it's available?

import algebra.order.ring

instance : ordered_add_comm_group unit := sorry

noncomputable instance : linear_ordered_add_comm_group unit :=
{ le_total := sorry,
  decidable_le := classical.dec_rel _,
  .. unit.ordered_add_comm_group }

def test1 : bool := if () + () = () then tt else ff /- OK -/

instance : ordered_comm_ring unit := sorry

noncomputable instance : linear_ordered_comm_ring unit :=
{ le_total := sorry,
  decidable_le := classical.dec_rel _,
  .. unit.ordered_comm_ring }

def test2 : bool := if () + () = () then tt else ff
/- missing 'noncomputable' modifier, definition 'test'
depends on 'unit.linear_ordered_comm_ring' -/

[Eric Wieser]

Adding intermediate instances (like docs#comm_ring) would fix this

[Junyan Xu]

Adding docs#comm_ring doesn't fix it (tested for surreals), unfortuantely.

[Junyan Xu]

adding docs#add_comm_group does fix it though

[Eric Wieser]

You can find out exactly what instance you need by looking at the path from linear_ordered_comm_ring to has_add

[Eric Wieser]

And adding an instance for the last step that is still computable

[Eric Wieser]

We do this already for real and complex

[Junyan Xu]

Hmm, then docs#ordered_ring should also work, let me try

[Junyan Xu]

It's cumbersome to move those fields around, so maybe I'll not try it for surreals, since everything works right now. ordered_comm_ring is the largest class that remains computable, and it's a shame that we have to break it down further. docs#surreal.dyadic_map should only require add_zero_class for the add_monoid_hom, and here are the paths from docs#ordered_comm_ring to docs#add_zero_class:

ordered_comm_ring ->
  ordered_ring ->
    ring -> add_comm_group ->
      add_group -> sub_neg_monoid -> add_monoid -> add_zero_class
      add_comm_monoid -> add_monoid
    ordered_add_comm_group -> add_comm_group
  comm_ring -> ring

[Junyan Xu]

and from docs#linear_ordered_comm_ring:

linear_ordered_comm_ring -> linear_ordered_ring -> ordered_ring

[Junyan Xu]

It seems to me the chain from ordered_comm_ring is shorter, no idea why Lean first finds linear_ordered_comm_ring.

[Eric Wieser]

Lean starts from the right and works left; it takes the highest priority option at every step, breaking ties by recently. It doesn't optimize for depth in any way