Case analysis in Idris proofs

Question

So I have wirtten the following type to prove some properties of Integers:

data Number : Type where
    PosN : Nat -> Number
    Zero : Number
    NegN : Nat -> Number

plusPosNeg : Nat -> Nat -> Number
plusPosNeg n m with (cmp n m)
    plusPosNeg (k + S d) k  | CmpGT d = PosN d
    plusPosNeg k k          | CmpEQ = Zero
    plusPosNeg k (k + S d)  | CmpLT d = NegN d

plus : Number -> Number -> Number
plus Zero y = y
plus x Zero = x
plus (PosN k) (PosN j) = PosN (k + j)
plus (NegN k) (NegN j) = NegN (k + j)
plus (PosN k) (NegN j) = plusPosNeg k j
plus (NegN k) (PosN j) = plusPosNeg j k

Now I'd like to prove that Zero is the neutral element of addition, which is quite obvious from the definition of plus. And indeed, Idris accepts the following proof:

plusRZeroNeutral : {l : Number} -> plus l Zero = l
plusRZeroNeutral {l = Zero} = Refl
plusRZeroNeutral {l = PosN _} = Refl
plusRZeroNeutral {l = NegN _} = Refl

But rejects a shorter version I have first come up with:

plusRZeroNeutral : {l : Number} -> plus l Zero = l
plusRZeroNeutral {l} = Refl

My question is why is that so? Looking at the definition of plus it would seem the compiler should know that the constructor passed as right argument to plus does not matter as long as the left argument is Zero (and vice versa). Perhaps it's a bug, or am I missing something?

Answer 1

If all you know about l is that it is, well, l (i.e. some arbitrary parameter), then you cannot reduce plus l Zero any further since you are stuck on which branch of plus to take.

When you pattern match on e.g. l = Zero, the right-hand side's type is now refined to plus Zero Zero = Zero, which can be reduced (via the definition of plus) to Zero = Zero. The constructor Refl's type unifies readily with this refined result type, and so the clause plusRZeroNeutral {l = Zero} = Refl typechecks.

The other branches are handled similarly by the other clauses of your first definition of plusRZeroNeutral.