Why doesn't Idris Ref sometimes check the type?
I am working on Idris's book and I am doing my first proof exercises.
With an exercise to prove same_lists
, I can implement it this way, since conformance Refl
forces x
and y
unifies:
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 way, I get inconsistencies. 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 give the case argument after =
, 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 makes implicit problematic arguments:
total allSame2 : {x : Nat} -> {y : Nat} -> x = y -> S x = S y
allSame2 Refl = Refl
source to share
I don't know all the details, but I can give you a rough idea. In Idris, named function parameter lists are special in that they are part of dependent pattern matching. When you match a pattern, it also overwrites other parameters.
same_lists x y Refl = Refl
unacceptable, I think roughly, because Idris rewrites x
both y
as the same thing and you are not allowed to give different names to this single meaning - I hope someone can provide a better explanation of this mechanism. You can use instead same_lists x x Refl = Refl
- and note that the name is x
not important, it is just that the same name is used on both sites.
The lambda parameter is different from the named parameter list name. Therefore, since you are doing the matching in the lambda, Idris is only going to overwrite the other parameters at this point. The key is that in the first example, Idris wants to do it all at once, because it is part of the same parameter list.
In the last example, the only change is that you have not specified various parameters. It would also be helpful to use all_same _ _ Refl = Refl
. When the parameters are implicit, Idris will fill them in correctly for you.
Finally, you may want to consider same_lists = \x, y, Refl => Refl
which also works. This is because Idris does not rewrite lists of unnamed parameters (i.e. lambda parameters).
source to share