Understanding noConfusion

Question

Data.List.getLast is defined as follows:

def getLast : ∀ (as : List α), as ≠ [] → α
  | [],       h => absurd rfl h
  | [a],      _ => a
  | _::b::as, _ => getLast (b::as) (fun h => List.noConfusion h)

I do not understand this definition, in particular the details around the recursive call.

1. Why is the last argument a lambda, when the signature seems to suggest a proof?
2. What is List.noConfusion, where is it defined, and how does it relate to the "No Confusion" rule in general?
3. Here's the type of List.noConfusion:

List.noConfusion.{u_1, u} {α : Type u} {P : Sort u_1} {v1 v2 : List α} (h12 : v1 = v2) : List.noConfusionType P v1 v2

How should I interpreter this? What is noConfusionType?

Answer 1

The "no confusion" in type theory is a characterizing property of constructors, say, if two terms of an inductive type are generated from different constructors, they should be unequal.

Why is the last argument a lambda, when the signature seems to suggest a proof?

They are the same. a ≠ b is usually defined as a = b → False, which you usually prove via introducing a lambda.

where is it (no confusion) defined

Seems like it's defined internally (correct me if I'm wrong).

The noConfusionType should be similar to something you generate in Haskell from deriving Eq, which is a two-arg pattern matching function that returns the unit type when v1 and v2 are of the same constructor and the empty type otherwise.