How Agda determines a type is impossible

Question

So I'm trying to understand why this code gives yellow highlighting around the ()

data sometype : List ℕ → Set where
  constr : (l1 l2 : List ℕ)(n : ℕ) → sometype (l1 ++ (n ∷ l2))

somef : sometype [] → ⊥
somef ()

But this does not

data sometype : List ℕ → Set where
  constr : (l1 l2 : List ℕ)(n : ℕ) → sometype (n ∷ (l1 ++ l2))

somef : sometype [] → ⊥
somef ()

Both seem to such that sometype [] is empty, but Agda can't figure the first one out? Why? What is the code behind this doing? And Can I define somef in a way to make the first definition work?

András Kovács András Kovács · Accepted Answer · 2016-02-12T20:12:07

Agda can't assume anything about arbitrary functions like ++. Suppose we defined ++ the following way:

_++_ : {A : Set} → List A → List A → List A
xs ++ ys = []

In this case, sometype [] → ⊥ isn't provable, and accepting the () absurd pattern would be an error.

In your second example, the index of sometype must be of the form n ∷ (l1 ++ l2), which is a constructor expression, since _∷_ is a list constructor. Agda can safely infer that a _∷_-constructed list can never be equal to []. In general, distinct constructors can be seen as impossible to unify.

What Agda can do with function applications is reducing them as far as possible. In some cases reduction yields constructor expressions, in other cases it doesn't, and we need to write additional proofs.

To prove sometype [] → ⊥, we should do some generalization first. We can't pattern match on a value of sometype [] (because of the ++ in the type index), but we can match on sometype xs for some abstracted xs. So, our lemma says the following:

someF' : ∀ xs → sometype xs → xs ≡ [] → ⊥
someF' .(n  ∷ l2)           (constr [] l2 n) ()
someF' .(n' ∷ l1 ++ n ∷ l2) (constr (n' ∷ l1) l2 n) ()

In other words, ∀ xs → sometype xs → xs ≢ []. We can derive the desired proof from this:

someF : sometype [] → ⊥
someF p = someF' [] p refl

How Agda determines a type is impossible

1 Answers