Default instance with strange behavior

Stream: general

[DSB]

I'm using the @[default_instance], and I'm getting a different result for the output type, which, if I understood correctly, should be the same. I mean, in the code below, I have HPlus.hPlus (2 : Pos) 2 and HPlus.hPlus (2 : Pos) (2 :Nat), which are defaulting to different instances, despite the fact that the last argument is a natural number in both cases.

inductive Pos : Type where
  | one : Pos
  | succ (p : Pos)

def addNatPos : Nat → Pos → Pos
  | 0, p => p
  | n + 1, p => Pos.succ (addNatPos n p)

def addPosNat : Pos → Nat → Pos
  | p, 0 => p
  | p, n + 1 => Pos.succ (addPosNat p n)

class HPlus (α : Type) (β : Type) (γ : outParam Type) where
  hPlus : α → β → γ
instance {n : Nat} : OfNat Pos (n + 1) where
  ofNat :=
    let rec natPlusOne : Nat → Pos
      | 0 => Pos.one
      | k + 1 => Pos.succ (natPlusOne k)
    natPlusOne n

@[default_instance]
instance : HPlus Pos Nat String where
  hPlus := fun x y => "ok"

instance : HPlus Pos Nat Pos where
  hPlus := addPosNat

#check HPlus.hPlus (2 : Pos)

#eval HPlus.hPlus (2 : Pos) 2 -- Outputs "ok"
#eval HPlus.hPlus (2 : Pos) (2 :Nat) -- Output the Pos value

[Edward van de Meent]

could you make sure the code snippet you post works on live.lean-lang.org ?

[Edward van de Meent]

because right now it complains it doesn't know what Pos is supposed to be, and a search for addPosNat didn't illuminate what type you would be referring to.

[DSB]

Edward van de Meent said:

could you make sure the code snippet you post works on live.lean-lang.org ?

Sorry for that. I've updated it!