How Agda defines a type, impossible

Question

So, I'm trying to understand why this code gives a yellow highlight around ()

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

But it is not

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

Both seem like sometype [] is empty, but Agda cannot determine the first one? What for? What is this code? Can I define somef to do the work on the first definition?

Answer 1

Agda cannot accept anything about features like ++ . Suppose we define ++ as follows:

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

In this case, sometype [] → ⊥ not provable, and accepting an absurd pattern () will be a mistake.

In your second example, the sometype index should look like n ∷ (l1 ++ l2) , which is a constructor expression, since _∷_ is a list constructor. Agda can safely conclude that a _∷_ -built list can never be equal to [] . In general, various constructors can be considered impossible for unification.

What Agda can do with application applications reduces them as much as possible. In some cases, the abbreviation gives constructor expressions, in other cases it is not, and we need to write additional evidence.

To prove sometype [] → ⊥ , you first need to make some generalization. We cannot match the match by the value of sometype [] (due to ++ in the type index), but we can match on sometype xs for some abstract xs . So our lemma reads as follows:

 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 ≢ [] . From this we can obtain the required proof:

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