idris-lang / Idris2

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

Postfix functions are parsed as if inside unquote when are right after unquote #3251

Closed buzden closed 6 months ago

buzden commented 7 months ago

Steps to Reproduce

Consider the following code:

import Language.Reflection

(.fun) : Nat -> Nat

x : TTImp

f : Nat -> TTImp

useX : TTImp
useX = `(g (~x).fun)

useX' : TTImp
useX' = `(g ~x.fun)

useFX : TTImp
useFX = `(g (~(f 5)).fun)

useFX' : TTImp
useFX' = `(g ~(f 5).fun)

Expected Behavior

All use* function typecheck successfully, primed and un-primed variants having the same meaning.

Observed Behavior

Primed versions do not typecheck:

Error: While processing right hand side of useX'. When unifying:
    TTImp
and:
    Nat
Mismatch between: TTImp and Nat.

X:13:14--13:15
 09 | useX : TTImp
 10 | useX = `(g (~x).fun)
 11 | 
 12 | useX' : TTImp
 13 | useX' = `(g ~x.fun)
                   ^
Error: While processing right hand side of useFX'. When unifying:
    TTImp
and:
    Nat
Mismatch between: TTImp and Nat.

X:19:16--19:19
 15 | useFX : TTImp
 16 | useFX = `(g (~(f 5)).fun)
 17 | 
 18 | useFX' : TTImp
 19 | useFX' = `(g ~(f 5).fun)
                     ^^^

Seems like (.fun) function was tried to be applied to the TTImp being unquoted, despite being outside the unquote brackets.

dunhamsteve commented 6 months ago

I believe this is fixed by #3253.