idris-lang / Idris2

A purely functional programming language with first class types

https://idris-lang.org/

Other

2.46k stars 368 forks source link

Regression in #3234, backticked infix operators are printed incorrectly #3249

Closed buzden closed 3 months ago

buzden commented 3 months ago

Steps to Reproduce

Typecheck the following module:

import Language.Reflection

%default total
%language ElabReflection

export infix 6 `op`

%runElab logSugaredTerm "debug" 0 "term with infix" `(a `op` b)

Expected Behavior

Prints

LOG debug:0: term with infix: a `op` b

Observed Behavior

Prints

LOG debug:0: term with infix: a op b

Pinging @andrevidela as the author of the original PR #3234

andrevidela commented 3 months ago

Nice catch! I'll see if I can fix it this afternoon

something something bidirectional parsing would have caught it etc etc