[Agda] New user question. Why does Agda reject my program.

[Jesper Louis Andersen]

Hi Agda users.

I am trying to work myself through "Why Dependent types matter" by
Altenkirch, McBride and McKinna. The code is in Epigram, but I have
enough spare neurons in my brain to attempt a translation. However, I
run into trouble early on, for the general code:

module MergeSort where

open import Function
open import Data.Nat
open import Data.Product

data Order : Set where
  le : Order
  ge : Order

data List (X : Set) : Set where
  nil : List X
  _∷_ : (x : X) -> (xs : List X) -> List X

order : (x : ℕ) (y : ℕ) -> Order
order zero y = le
order (suc n) zero = ge
order (suc n) (suc n') = order n n'

merge : List ℕ -> List ℕ -> List ℕ
merge nil ys = ys
merge xs nil = xs
merge (x ∷ xs') (y ∷ ys') with order x y
merge (x ∷ xs') (y ∷ ys') | le = x ∷ merge xs' (y ∷ ys')
merge (x ∷ xs') (y ∷ ys') | ge = y ∷ merge (x ∷ xs') ys'

Agda 2.2.10's Emacs mode places a big fat red sticker on the 'merge'
definition, but I can't see why it does so. My question is thus: Why?
How can I query Agda-mode for what is going on here? I'd like some
more hint than "You are wrong, and it is grave!"


-- 
J.