Agda prints hidden function type in hidden argument as `{{...` and then fails to parse it

[andreasabel]

Agda prints hidden function type in hidden argument as {{... and then fails to parse it. Example: f {{x : A} -> B}.

This is dual to the existing problem f {record {x = a}} for which we have already workaround: https://github.com/agda/agda/blob/32724f0da322c6bdcca9811a179ab6f7e88b5376/src/full/Agda/Syntax/Parser/Parser.y#L426-L440

Rant about the syntax for instance arguments:

In hindsight, we shouldn't have allowed syntax {{...}} for instance arguments, as it necessitates these parser hacks. Except for parsing, the other conceptual shortcoming is that the lack of visible instance metas, because we tie instanceness in with hiding. This is issue #2172. After having introduced attributes, we could now untangle instanceness from hiding and support (@instance x : A) -> B and {@instance x : A} -> B, deprecating {{x : A}} -> B.

[andreasabel]

I tried to duplicate the DoubleCloseBrace trick into a symmetric DoubleOpenBrace, but it does not work, due to the bias in LR parser (left-to-right). Consider (1) f {{x y}} vs f {{x y : A} -> B}. If the parse stack looks like Id '{' '{' Id Id after y we can never reduce (1) correctly, but if it looks Id DoubleOpenBrace Id Id we fail to parse (2). (LR parsers cannot reduce inside the stack, only the top of the stack.)

So a systematic solution would be to drop both DoubleCloseBrace and DoubleOpenBrace from the parser and do the construction of instance arguments and instance abstractions in a post-processing step. The parser would then only make sure that bracketing{...} is balanced.

More radically, simplify Parser.y drastically so that e.g. -> and : are just expression constructors, and then have a post-parse step that constructs the dependent function space.