internal error in Agda, perhaps related to --rewriting

[jsiek]

To reproduce the bug, go to the following repository:
https://github.com/jsiek/abstract-binding-trees
and checkout at the tag
agda-bug
Then process the file
src/rewriting/examples/Lambda.agda
which will produces the following error:

An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE_VERBOSE__, called at src/full/Agda/TypeChecking/Monad/Signature.hs:703:32 in Agd-2.6.2-17c972f8:Agda.TypeChecking.Monad.Signature

The error goes away if a small change is made to the ABTPredicate.agda file. See the comment in that file.

[andreasabel]

Thanks to the report @jsiek ! Which Agda version does this apply to?
Please try whether this is fixed by the release candidate for 2.6.3: https://hackage.haskell.org/package/Agda-2.6.2.2.20221106/candidate

[jsiek]

This applies to version 2.6.2.
I'll give it a try with 2.6.3 and report back.

[jsiek]

So I'll need to install that version... I tried the following but failed.
What's the recommended way to install the release candidate on a Mac?

jsiek@sice-mbp-986171 abstract-binding-trees % cabal update
Downloading the latest package list from hackage.haskell.org
Package list of hackage.haskell.org is up to date at index-state 2022-11-17T13:58:44Z
jsiek@sice-mbp-986171 abstract-binding-trees % cabal install Agda-2.6.2.2.20221106
Resolving dependencies...
cabal: Could not resolve dependencies:
[__0] next goal: Agda (user goal)
[__0] rejecting: Agda-2.6.2.2, Agda-2.6.2.1, Agda-2.6.2, Agda-2.6.1.3,
Agda-2.6.0.1, Agda-2.5.4.2, Agda-2.5.3, Agda-2.5.2, Agda-2.5.1.2,
Agda-2.4.2.5, Agda-2.4.2.4, Agda-2.4.2.3, Agda-2.4.2.2, Agda-2.4.2.1,
Agda-2.4.2, Agda-2.4.0.2, Agda-2.4.0.1, Agda-2.4.0, Agda-2.3.2.2,
Agda-2.3.2.1, Agda-2.3.2, Agda-2.3.0.1, Agda-2.3.0, Agda-2.2.10, Agda-2.2.8,
Agda-2.2.6, Agda-2.2.4, Agda-2.2.2, Agda-2.2.0, Agda-2.6.1.2, Agda-2.6.1.1,
Agda-2.6.1, Agda-2.6.0, Agda-2.5.4.1, Agda-2.5.4, Agda-2.5.1.1, Agda-2.5.1
(constraint from user target requires ==2.6.2.2.20221106)
[__0] fail (backjumping, conflict set: Agda)
After searching the rest of the dependency tree exhaustively, these were the
goals I've had most trouble fulfilling: Agda

[fredrikNordvallForsberg]

From the announcement of the release candidate on the mailing list:

# Installation

Agda 2.6.3 RC1 can be installed using cabal-install or stack:

* Getting the release candidate

    $ cabal get
https://hackage.haskell.org/package/Agda-2.6.2.2.20221106/candidate/Agda-2.6.2.2.20221106.tar.gz
    $ cd Agda-2.6.2.2.20221106

* Using cabal-install

    $ cabal install

* Using stack

    $ stack --stack-yaml stack-a.b.c.yaml install

replacing `a.b.c` with your version of GHC.

[jsiek]

Thanks! (I'm not on the mailing list.)

[jsiek]

With the release candidate, I'm getting a regular error from a different place in the code... it looks like the rewriting behavior has changed. I'll try to fix that other error...

[jsiek]

How do I update my emacs agda-mode? I thought the cabal install for the agda release would also install a new agda-mode, but that doesn't seem to be the case.

[asr]

Oops! Due to an involuntary errror, the agda-mode program wasn't include in the release candidate.

[jsiek]

Ok, then I'll wait for a fixed release candidate.

[asr]

I didn't get any error running Agda 2.6.3 RC1 on Lambda.agda:

$ cd src/rewriting/examples/
$ agda Lambda.agda

[jsiek]

Good!

[asr]

Ok, then I'll wait for a fixed release candidate.

At the moment, you can use this temporal fix: In the file agda2-mode.el localized in the directory pointed by running agda-mode locate replace

(defvar agda2-version "2.6.2.2"

with

(defvar agda2-version "2.6.2.2.20221106"

[jsiek]

Thanks! I can confirm that its working with 2.6.2.2.20221106.