Why is this Idris function not total and what could be done to make it check total?

Question

This Idris function does not successfully check for totality, however in my mind it seems that all cases are covered. This is my merge function in a merge sort.

Using Idris version 1.3.3

Error.

*d:/home/projects/testidris/test> :total merge2
Main.merge2 is possibly not total due to:
    Main.case block in case block in merge2 at d:\home\projects\testidris\test.idr:11:22-47 at d:\home\projects\testidris\test.idr:12:22-31, which is not total as there are missing cases

Idris.

module Main

record Mergeable where
    constructor MkMergeable
    left : List Nat
    right : List Nat

merge2 : Mergeable -> List Nat
merge2 (MkMergeable [] right) = right
merge2 (MkMergeable left []) = left
merge2 (input) = let MkMergeable (left) (right) = input;
                     (a1 :: a2) = left;
                     (b1 :: b2) = right in
                 if a1 < b1 then a1 :: merge2 (MkMergeable a2 right)
                 else b1 :: merge2 (MkMergeable left b2)