Incorrect usage of underscore in names breaks parsing

[isovector]

module Bug where

data Bug : Set where
  var_x : Bug

bug : Bug → Bug
bug x = {! !}

produces the error message

Could not parse the left-hand side bug x
Operators used in the grammar:
  None
when scope checking the left-hand side bug x in the definition of
bug

Removing x, and then attempting to refine the hole instead gives this error:

1,5-6
Could not parse the left-hand side .extendedlambda0 x
Operators used in the grammar:
  None
when scope checking the left-hand side .extendedlambda0 x in the
definition of .extendedlambda0

[andreasabel]

Well, x is part of a mixfix constructor, so it cannot be used as a pattern variable here. But I agree there is something off here, because Agda claims:

Operators used in the grammar:
  None

Maybe I expect to see:

Operators used in the grammar:
  var_x (closed operator)

This is what you get if you also include var on the lhs, e.g.:

bug : Bug → Bug
var bug x = {! !}

[nad]

The grammar only includes operators for which, roughly speaking, all name parts are present in the expression/pattern that is parsed.

[andreasabel]

The grammar only includes operators for which, roughly speaking, all name parts are present in the expression/pattern that is parsed.

But if this is the case, what is the reason that parsing would fail?

[isovector]

I actually hadn't noticed that my variable name x was part of the mixfix var_x, which makes this behavior more scrutable. However, I think a better error message here would go a very long way!

[nad]

But if this is the case, what is the reason that parsing would fail?

https://github.com/agda/agda/blob/2816605bfdc24c93d8801016d31beeed7608ad02/src/full/Agda/Syntax/Concrete/Operators.hs#L299-L301

In this case var and x are part of conParts (because x is mentioned in the pattern), but not conNames. Perhaps the error message could include an explanation of which things are allowed as "atoms".

[andreasabel]

Perhaps the error message could include an explanation of which things are allowed as "atoms".

Yes, please. Should be easy since all the information is on the table already.

[isovector]

One other confounding issue here is that make case and refinement were both automatically choosing the name x for my variable in bug.

[andreasabel]

automatically choosing the name x for my variable in bug.

x is the default if no other name is suggested. You can give a name to the argument of bug, and then this one will be used:

bug : (philosantos : Bug) -> Bug

The default chosen name for the first argument of bug is then philosantos.

Unfortunately, if that chosen name isn't valid as pattern variable, then Agda doesn't try another one, but errors out, as you report. Agda doesn't maintain a set of names that mustn't be shadowed by a pattern variable, unfortunately. Those are the names of constructors that are in scope or could easily come into scope, or (apparently), parts of those.