Idris2
Idris2 copied to clipboard
Argument to partially applied function moved outside parentheses in idiom brackets
Steps to Reproduce
Given
export
interface Primitive dtype => LiteralPrimitiveRW dtype ty where
set : Literal -> List Nat -> ty -> IO ()
get : Literal -> List Nat -> ty
this compiles
sequence_ [| (\idxs => set {dtype} literal idxs) indexed xs |]
but this doesn't
sequence_ [| (set {dtype} literal) indexed xs |]
Inspecting the generated TTImp with elab-util's pretty printer gives
Language.Reflection.Pretty> :exec putPretty `([| (set {dtype} literal) indexed xs |])
IApp. IVar <*>
$ (IApp. IVar <*>
$ (IApp. IVar <*>
$ (IApp. IVar pure $ (INamedApp. IVar set $ IVar dtype))
$ IVar literal)
$ IVar indexed)
$ IVar xs
The same happens with [| (get {dtype} literal) indexed |].
Expected Behavior
Both forms should compile: literal should remain inside the brackets.
Here is a minimal example: During desugaring of the idiom bracket, the argument to f has escaped the parens:
Language.Reflection.Pretty> :exec putPretty `([| (f a) y |])
IApp. IVar <*>
$ (IApp. IVar <*> $ (IApp. IVar pure $ IVar f) $ IVar a)
$ IVar y