[SOLVED] Using rewrite in the REPL

Using rewrite in the REPL

For one of the exercises in Type-Driven Development with Idris, I wrote the following:

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m = rewrite plusZeroRightNeutral m in Refl
myPlusCommutes (S n) m =
    rewrite myPlusCommutes n m in
      rewrite plusSuccRightSucc m n in Refl

Then I wanted to play around with rewrite in the REPL, so I could "see" what was happening behind the scenes. I thought the following might work, but it didn't.

λΠ> :let m : Nat
defined
λΠ> :let s : (plus 0 m = plus m 0)
defined
λΠ> rewrite plusZeroRightNeutral m in s
rewriting plus m 0 to m did not change type iType

Is it possible to see what rewrite is doing using the REPL?

Solution

rewrite x in y does not change the type of y to match the expected type, it change the expected type to match y. Idris does not know what the expected type is because you have not provided it.