Totality checker thinks simple function is total when it's not

[wizeman]

Steps to Reproduce

Create a file called Bug.idr with the following contents:

module Bug

%default total

data MNat : Type where
  MZ : MNat
  MS : MNat -> MNat

minus : (n, m : MNat) -> MNat
minus MZ MZ = MZ
minus n MZ = n
minus (MS k) (MS j) = minus k j

Then run:

$ idris Bug.idr

*Bug> minus (MS MZ) MZ
MS MZ : MNat

*Bug> minus MZ (MS MZ)
minus MZ (MS MZ) : MNat

Expected Behavior

*Bug> :total Bug.minus
Bug.minus is not total as there are missing cases

Observed Behavior

*Bug> :total Bug.minus
Bug.minus is Total

I'm using Idris 1.3.2. The changelog of Idris 1.3.3 doesn't mention anything related to this problem, so I assume the bug is still present.

Bug.idr.gz

[wizeman]

Idris 2 correctly reports the missing cases and has the expected output:

1/1: Building Bug (Bug.idr)
Bug.idr:9:1--10:1:minus is not covering. Missing cases:
        minus MZ (MS _)

Bug> :total Bug.minus
Bug.minus is not covering all cases