Curly braces are allowed nested in patterns

[janmasrovira]

Fixes #1337.

[lukaszcz]

Compiling:

module braces;

f : {A : Type} -> A -> A;
f {Do you wanna stack trace?} x := x;

end;

results in:

juvix: constructor expected on the left of a pattern application
CallStack (from HasCallStack):
  error, called at src/Juvix/Prelude/Base.hs:264:9 in juvix-0.2.1-CZT06Rzh5GNEZIQRWHpfSc:Juvix.Prelude.Base
  error, called at src/Juvix/Translation/ScopedToAbstract.hs:382:11 in juvix-0.2.1-CZT06Rzh5GNEZIQRWHpfSc:Juvix.Translation.ScopedToAbstract

Should be a user-level error message.

[lukaszcz]

Maybe I'll just open the above as a separate issue. It fails also for explicit arguments in ordinary braces.

[lukaszcz]

Maybe it's fine to leave it as it is for now in the current PR, but I think ultimately PatternBraces should be removed from the scoped concrete syntax. It's not a kind of pattern, but an indication that the argument is implicit. The information on which patterns (arguments) are implicit should perhaps be kept in FunctionClause? Analogously, you don't have PatternParens in the scoped concrete syntax, PatternAtomParens seems to be removed at scoping.

[janmasrovira]

Maybe it's fine to leave it as it is for now in the current PR, but I think ultimately PatternBraces should be removed from the scoped concrete syntax. It's not a kind of pattern, but an indication that the argument is implicit. The information on which patterns (arguments) are implicit should perhaps be kept in FunctionClause? Analogously, you don't have PatternParens in the scoped concrete syntax, PatternAtomParens seems to be removed at scoping.

Good point. I think it is better if I remove PatternBraces from scoped syntax in this PR

[janmasrovira]

Maybe it's fine to leave it as it is for now in the current PR, but I think ultimately PatternBraces should be removed from the scoped concrete syntax. It's not a kind of pattern, but an indication that the argument is implicit. The information on which patterns (arguments) are implicit should perhaps be kept in FunctionClause? Analogously, you don't have PatternParens in the scoped concrete syntax, PatternAtomParens seems to be removed at scoping.

Good point. I think it is better if I remove PatternBraces from scoped syntax in this PR

Done in 1108b7f

[lukaszcz]

Do you intend to fix "proper error messages" in another commit to this PR, or should this be done in another issue?

[janmasrovira]

Do you intend to fix "proper error messages" in another commit to this PR, or should this be done in another issue?

Let's do it in a separate pr.
I have already started working on it, but I think it would be a good idea for you to join me to get familiar with creating new errors

[lukaszcz]

Do you intend to fix "proper error messages" in another commit to this PR, or should this be done in another issue?

Let's do it in a separate pr. I have already started working on it, but I think it would be a good idea for you to join me to get familiar with creating new errors

Okay, I'll approve this PR then.