Why not equality with the minus typecheck in Idris?

Question

Why the following typecheck will not look:

minusReduces : (n : Nat) -> n `minus` Z = n
minusReduces n = Refl

But it will look great:

plusReduces : (n : Nat) -> Z `plus` n = n
plusReduces n = Refl

Answer 1

minus ndoes not decrease, because it minus is determined with the coincidence of patterns in the first argument:

total minus : Nat -> Nat -> Nat
minus Z        right     = Z
minus left     Z         = left
minus (S left) (S right) = minus left right

So you need to separate your cases Zand S n:

minusReduces : (n : Nat) -> n `minus` Z = n
minusReduces Z = Refl
minusReduces (S k) = Refl