merge fails, why?

InsertionSort.agda

module InsertionSort where

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 -> 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'

deal : {X : Set} (xs : List X) -> List X × List X
deal nil = nil , nil
deal (y ∷ nil) = y ∷ nil , nil
deal (y ∷ (y' ∷ y0)) with deal y0
deal (y' ∷ (y1 ∷ y0)) | proj₁ , y = y' ∷ proj₁ , y1 ∷ y

sort : List ℕ -> List ℕ
sort xs with deal xs
sort xs | proj₁ , nil = proj₁
sort xs | proj₁ , y ∷ y' = merge (sort proj₁) (sort (y ∷ y'))