Unhelpful error message when trying to use a keyword as a variable

[bkomuves]

If a function argument name coincides with a keyword, for example:

fun : a -> a
fun proof = proof

the compiler gives the rather unhelpful error message "Couldn't parse declaration", pointing at fun. (to compare, GHC also gives a parse error in such a case, but at least it points to the right source location.)

This can be confusing especially for newcomers. There are several keywords I would normally use as variable names without a second thought (for example "proof", "prefix", "total", maybe "parameters", etc).

Personally I ran into this twice in two days, so I can imagine other people running into it too.

[eayus]

I've also ran into this issue when trying to shadow a primitive type. For example, the declaration

String : Type

also gives a confusing error message, as the parser seems to handle these internal types specifically (which doesn't seem ideal for reasons like this).

Unfortnately I'd imagine this is quite a difficult fix. Perhaps the most pragmatic direction for issues like this is to put extra effort into ensuring that all popular editors are syntax highlighting keywords differently to normal identifiers.