Coverage Checking

To ensure completeness of definitions by pattern matching, Agda performs a coverage check on each definition by pattern matching. This page explains how this coverage check works by starting from simple examples and building up to the general case.

Single match on a non-indexed datatype

When a function definition pattern matches on a single argument of a simple (i.e. non-indexed) datatype, there should be a clause for each constructor. For example:

data TrafficLight : Set where
  red yellow green : TrafficLight
go : TrafficLight → Bool
go red    = false
go yellow = false
go green  = true

Alternatively, one or more cases may be replaced by a catchall clause that uses a variable pattern or a wildcard pattern _. In this case, the catchall clause should be last.

go' : TrafficLight → Bool
go' green = true
go' _     = false

Note

When the –exact-split flag is enabled, catchall clauses should be marked explicitly by a catchall pragma ({-# CATCHALL #-}).

The coverage check can be turned off for an individual definition by putting a {-# NON_COVERING #-} pragma immediately in front of the type signature.

{-# NON_COVERING #-}
go'' : TrafficLight → Bool
go'' red   = false
go'' green = true

In the special case of a datatype with no constructors (i.e. an empty type), there should be a single absurd clause with an absurd pattern () and no right-hand side.

data ⊥ : Set where
  -- no constructors
magic : {A : Set} → ⊥ → A
magic ()

Matching on multiple arguments

If a function matches on several arguments, there should be a case for each possible combinations of constructors.

sameColor : TrafficLight → TrafficLight → Bool
sameColor red    red    = true
sameColor red    yellow = false
sameColor red    green  = false
sameColor yellow red    = false
sameColor yellow yellow = true
sameColor yellow green  = false
sameColor green  red    = false
sameColor green  yellow = false
sameColor green  green  = true

Again, one or more cases may be replaced by a catchall clause.

sameColor' : TrafficLight → TrafficLight → Bool
sameColor' red    red    = true
sameColor' yellow yellow = true
sameColor' green  green  = true
sameColor' _      _      = false

Copattern matching

Functions that return an element of a record type can use copatterns to give the individual fields. The coverage check will ensure that there is a single case for each field of the record type. For example:

record Person : Set where
  field
    name : String
    age  : Nat
open Person
bob : Person
name bob = "Bob"
age  bob = 25

Absurd copatterns or wildcard copatterns are not supported.

Matching on indexed datatypes

When a function definition matches on an argument of an indexed datatype, the following conditions should be satisfied:

• For each clause that matches on a constructor pattern c u₁ … uₙ, the indices of the type of the pattern should be unifiable with the indices of the datatype being matched on.

• For each constructor c that does not appear in a clause, unification of the indices of the type of the constructor with the indices of the datatype should end in a conflict.

For example, consider the definition of the head function on vectors:

data Vec (A : Set) : Nat → Set where
  []  : Vec A 0
  _∷_ : ∀ {n} → A → Vec A n → Vec A (suc n)
head : ∀ {A m} → Vec A (suc m) → A
head (x ∷ xs) = x

The type of the pattern x ∷ xs is Vec A (suc n), which is unifiable with the type Vec A (suc m). Meanwhile, unification of the type Vec A 0 of the constructor [] with the type Vec A (suc n) results in a conflict between 0 and suc n, so there is no case for [].

In case a function matches on several arguments and one or more of them are of indexed datatypes, only those combinations of arguments should be considered where the indices do not lead to a conflict. For example, consider the zipWith function on vectors:

zipWith : ∀ {A B C m} → (A → B → C) → Vec A m → Vec B m → Vec C m
zipWith f []       []       = []
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys

Since both input vectors have the same length m, there is are no cases for the combinations where one vector has length 0 and the other has length suc n.

In the special case where unification ends in a conflict for all constructors, there should be a single absurd clase (as for an empty type). For example:

data Fin : Nat → Set where
  zero : ∀ {n} → Fin (suc n)
  suc  : ∀ {n} → Fin n → Fin (suc n)
no-fin-zero : Fin 0 → ⊥
no-fin-zero ()

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. As an example, consider the definition of the lookup function for vectors:

lookup : ∀ {A} {n} → Vec A n → Fin n → A
lookup []       ()
lookup (x ∷ xs) zero    = x
lookup (x ∷ xs) (suc i) = lookup xs i

This definition pattern matches on both its (explicit) arguments in both the absurd clause and the two regular clauses. Hence it is allowed to leave out the absurd clause from the definition:

lookup' : ∀ {A} {n} → Vec A n → Fin n → A
lookup' (x ∷ xs) zero    = x
lookup' (x ∷ xs) (suc i) = lookup' xs i

Refer to the next section for a precise explanation of when an absurd clause may be omitted.

General case

In the general case, the coverage checker constructs a case tree from the definition given by the user. It then ensures that the following properties are satisfied:

• The non-absurd clauses of a definition should arise as the leaves of the case tree.

• The absurd clauses of a definition should arise as the internal nodes of the case tree that have no children.

• Absurd clauses may be omitted if removing the corresponding internal nodes from the case tree does not result in other internal nodes becoming childless.

• Non-absurd clauses may be replaced by catchall clauses if (1) the patterns of those catchall clauses are more general than the omitted clauses, (2) the added catchall clauses are not more general than any of the clauses that follow it, and (3) removing the leaves corresponding to the omitted clauses does not result in any internal nodes becoming childless.

As an example, consider the case tree for the definition of the lookup function defined above:

lookup xs i = case xs of
  []       → case i of {}
  (x ∷ xs) → case i of
    zero    → x
    (suc i) → lookup xs i

The absurd clause arises from the case split on i in the branch where xs = [], which leads to zero cases. The two normal clauses arise from the two leaves of the case tree. If the case [] → case i of {} is removed from the case tree, all the remaining internal nodes still have at least one child, hence the absurd clause may be left out of the definition.

For a full formal description of the algorithm that Agda uses to construct a case tree and check coverage of definitions by pattern matching, refer to the article Elaborating dependent (co)pattern matching: No pattern left behind.