idris-lang
Using syntax rules should require fewer parentheses
Syntax rules using symbols as separators require more parentheses than syntax rules using keywords as separators. Tested with Idris 0.9.19.
module SyntaxProblem
helper : () -> () -> ()
helper _ _ = ()
syntax rule [a] keyword [b] = helper a b
syntax brokenRule [a] "+++" [b] = helper a b
example : ()
example = rule helper () () keyword helper () ()
brokenExample : ()
brokenExample = brokenRule helper () () +++ helper () ()
./SyntaxProblem.idr:13:17: error: unexpected
reserved
identifier, expected: dependent type signature
brokenExample = brokenRule helper () () +++ helper () ()
^
Adding more parentheses helps, but partially defeats the purpose of using syntax rules.
brokenExampleWorkaround : ()
brokenExampleWorkaround = brokenRule (helper () ()) +++ helper () ()
Related to #2566 and #2567 by way of error message.
I unfortunately wouldn't expected that this gets fixed, but I will still tag it if someone else wants to look at this. It is inherently a hard problem to give good error messages with so expressive syntax extensions.
Note that my complaint is primarily about the behaviour of the parser, and not the error message.
Related example:
typeApply : (a : Type) -> (a -> b) -> (a -> b) -- does work
typeApply _ f = f
infixl 10 @@
syntax [f] "@@" [a] = typeApply a f
t : String -> Int
-- t = id . const 3 @@ String -- broken
t = (id . const 3) @@ String -- works
On top of that the error message is really confusing:
Type checking ./TypeApplication.idr
TypeApplication.idr:8:3:When checking right hand side of t with expected type
String -> Int
When checking an application of function Prelude.Basics..:
No such variable @@
@gallais Your issue seems particularly weird, since "@@" is not a legal variable.
I unfortunately still do not have any idea how to improve syntax extensions in Idris in a usable and backwards compatible fashion. Ideas are welcome on how to solve the issue.
I don't know much about these things but I suspect that short of implementing a full parser for arbitrary mixfix expressions à la Agda, it'll always fall short of advanced users' expectations?