Why typeclass synthesis doesn't automatcially work?

Stream: general

[Hyunwoo Lee]

I recently suffered from Lean4's typeclass synthesis problem. It doesn't work in seemingly obvious case.

Here's the minimal reproducing example.

def down {T : Type} [LE T] (A B : T) : Prop :=
  A <= B

def down2 {T : Type} [Ord T] (A B : T) : Prop :=
  down A B

Definition down2 fails because it cannot synthesize LE T. However, it's obvious that if there's an order on type T, then you can compare which one is less than or equal to other. Actually I find such thing is already implemented.

https://leanprover-community.github.io/mathlib4_docs/Init/Data/Ord.html#Ord.toLE

How can I make Lean know the fact that Ord T includes LE T ?

[Robin Arnez]

Ord does not include LE automatically, you need to explicitly tell it to use Ord.toLE:

def down {T : Type u} [LE T] (A B : T) : Prop :=
  A <= B

def down2 {T : Type u} [Ord T] (A B : T) : Prop :=
  letI : LE T := leOfOrd
  down A B

Specifically, typeclass search will only search through instances; but Ord.toLE and leOfOrd are defs

[Hyunwoo Lee]

Thank you. Now I understand def and instance are different. Then is it possible to define this if I only want to use LE instance generated from Ord instance?

instance leFromOrd {α : Type} [Ord α] : LE α where
  le := leOfOrd.le

[Ruben Van de Velde]

For a general type, that seems like a bad idea

[Sébastien Gouëzel]

Maybe you want to use directly [PartialOrder α] or [LinearOrder α].

[Robin Arnez]

you can also attribute [local instance] leOfOrd in files where you need it to make sure this doesn't become an instance when it shouldn't be

[Hyunwoo Lee]

@Sébastien Gouëzel You are right. I was confused between Ord α and LinearOrder α. Thank you!