Why do these declarations (for the same pattern) satisfy the type checker?

Question

I'm following along with the amazing TDDwI, writing a simple removeElem.

Four questions about it:

1. why can I write 3 declarations for the same pattern?

2. what's the difference between absurd and impossible?

3. in that 3rd case that returns [], [] is a value, therefore... proof that xs had an a to remove, and did... right?

4. if I remove all 3 of them, the function is still total, and I have an inexplicable tickle that something weird's going on. ?. (i think that's a question)

---

removeElem : (value : a)
          -> (xs : Vect (S n) a) 
          -> (prf : Elem value xs) 
          -> Vect n a
removeElem value (value :: ys) Here = ys
removeElem {n = Z} value (y :: []) (There later) = absurd later -- ??
removeElem {n = Z} value (y :: []) (There later) impossible     -- ??
removeElem {n = Z} value (y :: []) (There later) = []           -- ??
removeElem {n = (S k)} value (y :: ys) (There later) = 
  y :: removeElem value ys later

Answer 1

why can I write 3 declarations for the same pattern?

Because in this case (y :: []) you are dealing with a one-element vector. This means that later has type Elem value [], i.e. there is an element value in the empty list, which is absurd. Recall that absurd has type Uninhabited t => t -> a, which reads as "if a type t is uninhabited and you have an inhabitant of that type, then you can construct an inhabitant of an arbitrary type a". So, you just need Elem x [] to have an implementation of that interface (it's here). That's why absurd later works.

impossible works because Idris is capable of performing all the above reasoning on its own.

what's the difference between absurd and impossible?

The impossible keyword can be used to rule out a case that doesn’t type-check, while absurd is just a lemma, so everything must typecheck if you use it.

in that 3rd case that returns [], [] is a value, therefore... proof that xs had an a to remove, and did... right?

Yes, it is correct. removeElem takes a value, a vector of some positive length, a proof that the value belongs to the vector and returns a vector of the decremented-by-one length. If you take a one-element vector, you can just ignore the value and the proof and immediately return the empty vector. My point being you don't have to use the proof, it gives you additional guarantees but you are free to ignore them.

if I remove all 3 of them, the function is still total, and I have an inexplicable tickle that something weird's going on

Everything is fine here, the function still works -- Idris lets you omit impossible cases:

removeElem {n = Z} value (y :: []) (There later) impossible