DecidableRel for Option.lt issue

Stream: lean4

[Scott Kovach]

I came across the instance https://github.com/leanprover/lean4/blob/master/src/Init/Data/Option/Basic.lean#L70, which isn't working:

instance : DecidableRel (. < . : Option Nat -> Option Nat -> Prop) := inferInstance -- fails

I talked to @Kyle Miller about it, and he wrote this additional definition, which can derive the appropriate instance:

instance [t : LT α] [s : DecidableRel (LT.lt (α := α))] : DecidableRel (LT.lt (α := Option α)) :=
  by {
    simp [LT.lt];
    inferInstance
  }

[Kyle Miller]

Another example is that without this additional instance the following fails to find a Decidable instance.

def foo (x : Nat) : Bool := if some x < none then true else false