Type error in Functional Programming In Lean

Stream: new members

[Lars Ericson]

@David Thrane Christiansen , the section "Controlling Instance Search" in Functional Programming in Lean appears to have
Screenshot-from-2023-07-16-11-05-42.png
a coding error in this example:

structure Pos where
  succ :: pred : Nat

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

The error is that Pos.succ takes a Nat but addNatPos n p is a Pos. Please also attached screenshot.

The following alternate definition of addNatPos works but requires a little more buildup:

structure Pos where
  succ :: pred : Nat

class Plus (α : Type) where
  plus : α → α → α

def Nat.plus : Nat → Nat → Nat
  | 0, k => k
  | n+1, k => (n.plus k) + 1

def Pos.plus : Pos → Pos → Pos
  | Pos.succ a, Pos.succ b => Pos.succ (a + b + 1)

instance : Plus Pos where
  plus := Pos.plus

instance : Add Pos where
  add := Pos.plus

def addNatPos : Nat → Pos → Pos
  | Nat.zero, p => p
  | Nat.succ n, p => Pos.plus (Pos.succ n) p

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

#check addPosNat (Pos.succ 1) (Nat.succ 0)

[David Thrane Christiansen]

The Pos.succ here is the one from this definition:

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

The structure that you have here is part of an exercise on other ways to do it, not the main one in the chapter.

How could this have been more clear?