Why does Idris' Refl sometimes not type-check?

Question

I'm working through the Idris book, and I'm doing the first exercises on proof.

With the exercise to prove same_lists, I'm able to implement it like this, as matching Refl forces x and y to unify:

total same_lists : {xs : List a} -> {ys : List a} ->
    x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = Refl

However, when I try to prove something else in the same manner, I get mismatches. For example:

total allSame2 : (x, y : Nat) -> x = y -> S x = S y
allSame2 x y Refl = Refl

The compiler says:

Type mismatch between
   y = y (Type of Refl)
and
   x = y (Expected type)

If I case-match after the =, either explicitly or with a lambda, it works as expected:

total allSame2 : (x : Nat) -> (y : Nat) -> x = y -> S x = S y
allSame2 x y = \Refl => Refl

What's the difference here?

Another modification that works is making the problematic arguments implicit:

total allSame2 : {x : Nat} -> {y : Nat} -> x = y -> S x = S y
allSame2 Refl = Refl

erisco erisco · Accepted Answer · 2017-04-28T13:04:54

I do not know all the details, but I can give you a rough idea. In Idris, the parameter lists of named functions are special in that it is part of dependent pattern matching. When you pattern match it also rewrites the other parameters.

same_lists x y Refl = Refl is not valid, I roughly guess, because Idris is rewriting x and y to be the same, and you are not allowed to then give different names to this single value — I hope someone can give a better explanation of this mechanism. Instead you may use same_lists x x Refl = Refl — and note that the name x is not important, just that the same name is used in both sites.

A lambda parameter is apart from the named parameter list. Therefore, since you are doing the matching in the lambda, Idris is only going to rewrite the other parameters at that point. The key is that with the first example Idris wants to do it all at once because it is part of the same parameter list.

With the final example the only change is that you did not give distinct names to the parameters. It would have also been valid to use all_same _ _ Refl = Refl. When the parameters are implicit, Idris will fill them in correctly for you.

Finally you can consider same_lists = \x, y, Refl => Refl which also works. This is because Idris does not rewrite in unnamed parameter lists (i.e. lambda parameters).

Why does Idris' Refl sometimes not type-check?

1 Answers