idris-lang / Idris2

A purely functional programming language with first class types
https://idris-lang.org/
Other
2.54k stars 380 forks source link

Argument to partially applied function moved outside parentheses in idiom brackets #2498

Open joelberkeley opened 2 years ago

joelberkeley commented 2 years ago

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.

stefan-hoeck commented 2 years ago

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