How exactly does rewrite work in Idris?

Question

I wrote the following proposition in Idris:

total
plusOneCommutes : (n : Nat) -> (m : Nat) -> (n + S m = S n + m)
plusOneCommutes Z     k     = Refl
plusOneCommutes (S k) j     = 
 let inductiveHypothesis = plusOneCommutes k j in
   rewrite inductiveHypothesis in Refl

Using inspiration from the Prelude.Nat source code, I understand why it makes sense to use the recursive call (in the second case) as an induction hypothesis in order to prove the case. However, going through the details of the rewriting with holes, I don't really grok what's going on and why this works.

If I write:

plusOneCommutes (S k) j     = ?hole

I get the following from the compiler:

- + HolyGrail.hole [P]
 `--               k : Nat
                   j : Nat
     ------------------------------------------------------
      HolyGrail.hole : S (plus k (S j)) = S (S (plus k j))

which does not really seem right. According to the signature of plusOneCommutes this hole should have type (plus (S k) (S j)) = (plus (S (S k)) j).

Going one step further and introducing induction hypothesis, if I write:

plusOneCommutes (S k) j     = 
 let inductiveHypothesis = plusOneCommutes k j in
   ?hole

then type of hole becomes:

 - + HolyGrail.hole [P]
  `--                    k : Nat
                         j : Nat
       inductiveHypothesis : k + S j = S k + j
      -------------------------------------------------------------------------
       HolyGrail.hole : S (plus k (S j))  = S (S (plus k j))

then using the rewrite rule given by inductiveHypothesis

 - + HolyGrail.hole [P]
  `--                    k : Nat
                         j : Nat
       inductiveHypothesis : k + S j = S k + j
             _rewrite_rule : k + S j = S k + j
      -------------------------------------------------------------------------
       HolyGrail.hole : (\replaced => S replaced = S (S (plus k j))) (S k + j)

which leads to S (plus (S k) j) = S (S (plus k j)) which is the expected type, and Idris can complete the proof automatically replacing ?hole with Refl.

What's puzzling me then is the unexpected difference in types between what I infer from the signature and what the compiler infers from the hole. If I introduce voluntarily an error:

I get the following message:

 - + Errors (1)
  `-- HolyGrail.idr line 121 col 16:
      When checking right hand side of plusOneCommutes with expected type
              S k + S j = S (S k) + j

      Type mismatch between
              S (S (plus k j)) = S (S (plus k j)) (Type of Refl)
      and
              S (plus k (S j)) = S (S (plus k j)) (Expected type)

      Specifically:
              Type mismatch between
                      S (plus k j)
              and
                      plus k (S j)

The Type mismatch... part is consistent with the above steps but not the When checking ... part which gives the type I would expect.

Answer 1

The following from compiler actually makes sense:

- + HolyGrail.hole [P]
 `--               k : Nat
                   j : Nat
     ------------------------------------------------------
      HolyGrail.hole : S (plus k (S j)) = S (S (plus k j))

In the left side of = in type you have n + S m. After pattern matching on n you have (S k) and should have S k + S j in type which is plus (S k) (S j). In this question I explained one important point: from the fact how plus function is written and fact that compiler can perform pattern matching in types you're seeing S (plus k (S j)) which is just applying plus to (S k) and (S j). Similar situation with S n + m.

Now to rewrite. In Agda programming language rewrite is just syntax sugar for pattern matching on Refl. And sometimes you can replace rewrite with pattern matching in Idris but not in this case.

We can try to do something similar. Consider next:

total
plusOneCommutes : (n : Nat) -> (m : Nat) -> (n + S m = S n + m)
plusOneCommutes Z     k     = Refl
plusOneCommutes (S k) j     = case plusOneCommutes k j of
    prf => ?hole

Compiler says next very reasonable things:

- + HolyGrail.hole [P]
 `--               k : Nat
                   j : Nat
                 prf : k + S j = S k + j
     ------------------------------------------------------
      HolyGrail.hole : S (plus k (S j)) = S (S (plus k j))

prf is something that proves k + S j = S k + j which makes sense. And after using rewrite:

plusOneCommutes (S k) j     = case plusOneCommutes k j of
    prf => rewrite prf in ?hole

We got:

- + HolyGrail.hole [P]
 `--               k : Nat
                   j : Nat
                 prf : k + S j = S k + j
       _rewrite_rule : k + S j = S k + j
     -------------------------------------------------------------------------
      HolyGrail.hole : (\replaced => S replaced = S (S (plus k j))) (S k + j)

rewrite in Idris behaves in the following way:

1. Takes Refl : left = right object and expr : t.
2. Searches left in t.
3. Replaces all occurrences of left with right in t.

In our case:

1. t is S (plus k (S j)) = S (S (plus k j))
2. Refl : plus k (S j) = plus (S k) j
   • left is plus k (S j)
   • right is plus (S k) j
3. Idris replaces plus k (S j) (left) with plus (S k) j (right) in t and we get S (plus (S k) j) = S (S (plus k j)). Idris can perform pattern matching which it does. And S (plus (S k) j) naturally becomes S (S (plus k j)).