What is the proper why to generate an instance from Lean4 GetElm class type?

Question

Trigger

I am writing an exercise in Functional Programming in Lean. The example shows a way to generate an instance for GetElem' (NonEmptyList α) Nat α .. with a bound. I explain it as to implement the general typle class GetElem in specific user defined NonEmptyList with using n:Nat number to visit.

My Question

I fail to run the example in the book.

Type def and abbre copy&paste from the textbook. (no error)

structure NonEmptyList (α : Type) : Type where
  head : α
  tail : List α

def idahoSpiders : NonEmptyList String := {
  head := "Banded Garden Spider",
  tail := [
    "Long-legged Sac Spider",
    "Wolf Spider",
    "Hobo Spider",
    "Cat-faced Spider"
  ]
}


def NonEmptyList.get? {α : Type} : NonEmptyList α → Nat → Option α
  | xs, 0 => some xs.head
  | xs, n+1 => xs.tail.get? n
abbrev NonEmptyList.inBounds (xs : NonEmptyList α) (i : Nat) : Prop :=
  i ≤ xs.tail.length

theorem atLeastThreeSpiders : idahoSpiders.inBounds 2 := by decide
theorem notSixSpiders : ¬idahoSpiders.inBounds 5 := by decide
def NonEmptyList.get {α : Type} (xs : NonEmptyList α) (i : Nat) (ok : xs.inBounds i) : α :=
  match i with
  | 0 => xs.head
  | n+1 => xs.tail[n]

When try to get an instance of GetElem class. (Use ' tail to different from GetElem existed in prelude)

class GetElem' (coll : Type) (idx : Type) (item : outParam Type) (inBounds : outParam (coll → idx → Prop)) where
  getElem' : (c : coll) → (i : idx) → inBounds c i → item
instance : GetElem' (NonEmptyList α) Nat α NonEmptyList.inBounds where
  getElem' := NonEmptyList.get

with an error message

application type mismatch
  GetElem' (NonEmptyList α) Nat α NonEmptyList.inBounds
argument
  NonEmptyList.inBounds
has type
  Nat → Prop : Type
but is expected to have type
  outParam (NonEmptyList α → Nat → Prop) : Type

So I change my instance to solve the type mismatch problem.

class GetElem' (coll : Type) (idx : Type) (item : outParam Type) (inBounds : outParam (coll → idx → Prop)) where
  getElem : (c : coll) → (i : idx) → inBounds c i → item
instance : GetElem' (NonEmptyList α) Nat α (λ coll idx => coll.inBounds idx) where
  getElem := NonEmptyList.get

The final tests also pass.

#eval GetElem'.getElem idahoSpiders 0 (by decide)
#eval GetElem'.getElem idahoSpiders 1 (by decide)

So why the code on the textbook not work. Could anyone kindly explain what changed since I rewrite the inBounds with an (λ ..) function to me?