Odd behavior when defining a instance

Stream: new members

[Nicolas Rolland]

Any reason why the first definition fails while the others don't ?

inductive Pos : Type where
  | one : Pos
  | succ : Pos → Pos

instance : Add Pos where
  add n m := match m with
           | Pos.one => Pos.succ n
           | Pos.succ m' => Pos.succ (n + m') -- failed to synthesize instance HAdd Pos Pos ?m.250

instance : Add Pos where
  add n -- : Pos -> Pos
  | Pos.one      => Pos.succ n
  | (Pos.succ m) => Pos.succ (n + m) -- OK !


instance : Add Pos where
  add -- : Pos -> Pos -> Pos
  | Pos.one   => Pos.succ
  | (Pos.succ n) => Pos.succ ∘ (n + .) -- OK

instance : Add Pos where
  add := fun
    | (Pos.one) => Pos.succ
    | (Pos.succ n)  => Pos.succ ∘ (n + .) -- OK

I tried on stable and nightly-2023-10-31

[Alex J. Best]

The others only succeed because of the first one.
When you write n+m' for two elements of Pos lean goes looking for a typeclass Add Pos, when you are defining the first one it doesn't find any so it fails (gracefully enough that the instance is still added to the environment with a sorried out term).

[Alex J. Best]

You can either make a separate Pos.add function that can call itself recursively or do something like

instance : Add Pos := {add}
where
  add n m := match m with
           | Pos.one => Pos.succ n
           | Pos.succ m' => Pos.succ (add n m') -- failed to synthesize instance HAdd Pos Pos ?m.250

[Alex J. Best]

Where all your variants probably work there

[Nicolas Rolland]

Ah, good to know ! Thank you for spotting this and your solution