[Agda] How to engage coverage checking

[Jim Apple]

The following compiles (and loads into the interactive mode) fine with v2.1.2:

module Cover where

data Nat : Set where
     Z : Nat
     S : Nat -> Nat

sum : Nat -> Nat -> Nat
sum Z m = m

How do I ask Agda to check if sum is total?

Jim