Idris-dev icon indicating copy to clipboard operation
Idris-dev copied to clipboard

Broken sections of custom operators starting with pipe '|', "expecting function name"

Open ulidtko opened this issue 5 years ago • 0 comments

Custom operators starting with the | symbol seem to have a parsing/scoping issue.

Spotted here: https://github.com/LorenzoPerticone/idris-NN/issues/1

Steps to Reproduce

module Foo

infixl 0 |??
(|??) : Num a => a -> a -> a
x |?? y = x * y

issue : Int -> Int -> Int
issue x = (|?? x)

Observed Behavior

$ idris --check Foo.idr
Foo.idr:8:16:
  |
8 | issue x = (|?? x)
  |                ^
unexpected 'x'
expecting function name

The error doesn't happen if:

  • something else is used instead of the pipe symbol;
  • the section is left i.e. (x |??), this works.

idris --version: 1.3.3-git:PRE

ulidtko avatar Jul 24 '20 11:07 ulidtko