NonEmptyList example crashes Lean

Stream: new members

[Lars Ericson]

Reading the textbook on non-empty lists:, I type in the example code which is about checking for array out of bounds. The code, which typechecks, crashes the Lean server:

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? : 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 simp

theorem notSixSpiders : ¬idahoSpiders.inBounds 5 := by simp

def NonEmptyList.get (xs : NonEmptyList α) (i : Nat) (_ : xs.inBounds i) : α :=
  match i with
  | 0 => xs.head
  | n + 1 => xs.tail[n]

#eval idahoSpiders.get? 2

#eval idahoSpiders.get? 2

class GetElem1 (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

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)

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

instance : HAdd Nat Pos Pos where
  hAdd := addNatPos

def Pos.toNat : Pos → Nat
  | Pos.succ n => n + 1

instance : GetElem (List α) Pos α (fun list n => list.length > n.toNat) where
  getElem (xs : List α) (i : Pos) ok := xs[i.toNat]

#eval idahoSpiders[6] -- "Server process for file:///home/catskills/mathlib4/test/hw_lists.lean crashed, likely due to a stack overflow or a bug."

[Mauricio Collares]

lean4#2252