Asynchronous exception used to circumvent parser logic

[GoogleCodeExporter]

postulate
  F    : (Set → Set) → Set
  !_   : Set → Set
  !_,_ : Set → Set → Set
  X    : Set

syntax F (λ X → A) = X , A

infix 1 F
infix 2 !_

Foo : Set
Foo = ! X , X

-- This expression can be parsed in exactly one way. However, Agda
-- rejects it:
--
--   Expected variable name in binding position
--
-- The error is thrown from pure code in rebuildBinding, and this
-- action circumvents the parser logic.
--
-- The error was introduced in the fix for Issue 1129, and the problem
-- raised in Issue 1129 was introduced in a fix for Issue 1108
-- ("Operator parser performance").

Original issue reported on code.google.com by nils.anders.danielsson on 4 Mar 2015 at 1:55

[GoogleCodeExporter]

Fixed (on the master branch):

  https://github.com/agda/agda/commit/0c6f8395b1d2825be984aefcbff2e016d1088ba2

Original comment by nils.anders.danielsson on 4 Mar 2015 at 7:16

• Changed state: Fixed