[SOLVED] Agda: Could not parse the application

Agda: Could not parse the application

when I try to load this example from the Programming Language Foundations in Agda it fails:

module Test where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _∎; _≡⟨⟩_)

data Nat : Set where
    zero : Nat
    suc : Nat → Nat

{-# BUILTIN NATURAL Nat #-}

_+_ : Nat → Nat → Nat
(suc m) + n  = suc (m + n)
zero + n = n

_ : 2 + 3 ≡ 5
_ =
  begin
    2 + 3
  ≡⟨⟩    -- is shorthand for
    (suc (suc zero)) + (suc (suc (suc zero)))
  ≡⟨⟩    -- inductive case
    suc ((suc zero) + (suc (suc (suc zero))))
  ≡⟨⟩    -- inductive case
    suc (suc (zero + (suc (suc (suc zero)))))
  ≡⟨⟩    -- base case
    suc (suc (suc (suc (suc zero))))
  ≡⟨⟩    -- is longhand for
    5
  ∎

First warning:

warning: -W[no]ModuleDoesntExport
The module Eq.≡-Reasoning doesn't export the following:
  _≡⟨⟩_
when scope checking the declaration
  open Eq.≡-Reasoning using (begin_; _∎; _≡⟨⟩_)

Second error:

Could not parse the application
begin 2 + 3 ≡ (suc (suc zero)) + (suc (suc (suc zero))) ≡ suc
((suc zero) + (suc (suc (suc zero)))) ≡ suc
(suc (zero + (suc (suc (suc zero))))) ≡ suc
(suc (suc (suc (suc zero)))) ≡ 5 ∎
Operators used in the grammar:
  +     (infix operator, level 20)  [_+_ (C:\Users\user\Documents\Agda\VSC\Test.agda:12,1-4)]                                                                            
  ∎     (postfix operator, level 3) [_∎ (C:\cabal\agda-stdlib-2.0\src\Relation\Binary\Reasoning\Syntax.agda:442,3-5)]                                                     
  ≡     (infix operator, level 4)   [_≡_ (C:\cabal\store\ghc-9.4.8\Agda-2.6.4.1-e51cf1324caf3a56d7db642f01cda06d05fc0698\share\lib\prim\Agda\Builtin\Equality.agda:6,6-9)]
  begin (prefix operator, level 1)  [begin_ (C:\cabal\agda-stdlib-2.0\src\Relation\Binary\Reasoning\Syntax.agda:51,3-9)]                                                  
when scope checking
begin 2 + 3 ≡ (suc (suc zero)) + (suc (suc (suc zero))) ≡ suc
((suc zero) + (suc (suc (suc zero)))) ≡ suc
(suc (zero + (suc (suc (suc zero))))) ≡ suc
(suc (suc (suc (suc zero)))) ≡ 5 ∎

I'm using Agda standard library 2.0 and I noticed the operator ≡⟨⟩ is not in Relation.Binary.PropositionalEquality anymore (compared with 1.7.2), but I couldn't find any replacement. Also I'm not sure what the operator "≡⟨⟩" means or hoagw can it be replaced, but also I'm not sure if that's actually the reason why it fails to load.

Solution

This is an issue with standard lib v2.0:

I just looked into this. The underlying issue isn't that ≡⟨⟩ has been removed, but that it's now declared as a syntax for a different name, which breaks opening the ≡-Reasoning module with only some names as PLFA instructs. I agree this is unfortunate.

In the meantime, you can replace open Eq.≡-Reasoning using (begin_; ≡⟨⟩; ∎) with open Eq.≡-Reasoning using (begin; step-≡-∣; _∎). The convention in stdlib is to not use a using clause on the various Reasoning modules, which is why we hadn't noticed until now.

The solution is to use standard lib 1.7.3 or wait for a fix.