Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

Argument to partially applied function moved outside parentheses in idiom brackets

Open joelberkeley opened this issue 3 years ago • 1 comments

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.

joelberkeley avatar May 23 '22 13:05 joelberkeley

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

stefan-hoeck avatar May 23 '22 13:05 stefan-hoeck