Unnamed variables in error messages

[valis]

An unnamed variable (i.e., _) can be given a name in an error message. For example, consider the following code:

\func foo {A : \Type} (B : A -> \Type) (f : \Pi (a : A) -> B a) => 0

\func bar {A : \Type} (a : A) (B : A -> \Type) (b : B a) => foo B (\lam _ => b)

It produces the following error, which is confusing because the first 'a' is actually '_'

[ERROR] test.ard:37:79: Type mismatch
  Expected type: B a
    Actual type: B a

It is better to choose a name which clearly indicates that the variable was unnamed, like '_unnamed'. It is also unlikely that such a name will cause a clash of names as in the example above.

[ice1000]

This is what I see:

Is that because you've fixed it?

[ice1000]

[valis]

Fixed the code