Defining the head of a list with a proof object

Question

I would like to define a head function for lists. In order to avoid trying to compute the head of an empty list one can either work with vectors of length greater than one (i.e., Vec (suc n)) or work with Lists, but pass a proof that the list is non-empty to head. (This is what "Dependent Types at Work" calls internal vs external programming logic, I believe.) I am interested in the latter approach. Note that there is a SO answer which addresses this, but I wanted a minimal approach. (For example, I would prefer not to use Instance Arguments unless they are required.) Below is my attempt, but I don't fully understand what is going on. For example:

1. It's not clear why I was able to skip the head [] case. Obviously it's related to the "proof" I pass in but I would have expected I would need some kind of case with () in it.
2. When I type check (C-c C-l) I seem to get two goals as output.
3. I would have liked to have seen tmp2 fail to type check.

Any insight would be very welcome. In particular, what is the "right" way(s) to do what I am trying to do?

data List (A : Set) : Set where
    [] : List A
    _::_ : A → List A → List A

{-
head1 : {A : Set} → (as : List A) → A
-- As expected, complains about missing case `head1 []`.
head1 (a :: aa) = a
-}

data ⊤ : Set where
    tt : ⊤

data ⊥ : Set where

isNonEmpty : {A : Set} → List A → Set
isNonEmpty [] = ⊥
isNonEmpty (_ :: _) = ⊤

head : {A : Set} → (as : List A) → {isNonEmpty as} → A
head (a :: _) = a

-- Define just enough to do some examples

data Nat : Set where
    zero : Nat
    suc : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

len1 : List Nat
len1 = 17 :: []

tmp : Nat
tmp = head len1

tmp1 : Nat
tmp1 = head len1 { tt }

len0 : List Nat
len0 = []

tmp2 : Nat
tmp2 = head len0 

Answer 1

1. The user manual on coverage checking in Agda explains that in certain situations absurd clauses can be left out completely:

In many common cases, absurd clauses may be omitted as long as the remaining clauses reveal sufficient information to indicate what arguments to case split on. [...] Absurd clauses may be omitted if removing the corresponding internal nodes from the case tree does not result in other internal nodes becoming childless.

Note that you can still write the absurd clause manually if you want and Agda will accept it.

2. What you are getting are not two unsolved holes but two unsolved metavariables. These metavariables were created by Agda to fill in the implicit argument to head in the definitions of tmp and tmp2 respectively, and Agda's constraint solver wasn't able to solve them. For the metavariable in tmp, this is because you defined ⊤ as a datatype instead of a record type, and Agda only applies eta-equality for record types. For the metavariable in tmp2, the type is ⊥ so there is no hope that Agda would be able to find a solution here.

3. When using Agda, you should see unsolved metavariables as a specific case of "failing to typecheck". They are not a hard type error because that would prevent you from continuing to use the interactive editing of Agda, and in many cases further filling in holes will actually solve the metavariables. However, they indicate "this program is not finished" just as much as an actual type error would.