Agda fails to install on HEAD

(Continuing a discussion at head.hackage!210 (merged).)

Currently, Agda fails to install properly when built with GHC HEAD using head.hackage patches. The error arises when trying to run Agda's custom Setup.hs script during the copy phase. When building Agda-2.6.1.3, it will fail with this error, as seen here:

Could not parse the application primCharToNat a ≡ primCharToNat b
Operators used in the grammar:
  ≡ (infix operator, level 4) [_≡_ (/builds/ghc/head.hackage/ci/run/test-Agda-2.6.1.3/dist-newstyle/tmp/src-11665/Agda-2.6.1.3/src/data/lib/prim/Agda/Builtin/Equality.agda:7,6-9)]
when scope checking primCharToNat a ≡ primCharToNat b
Error: Failed to typecheck /builds/ghc/head.hackage/ci/run/test-Agda-2.6.1.3/dist-newstyle/tmp/src-11665/Agda-2.6.1.3/src/data/lib/prim/Agda/Builtin/Char/Properties.agda!
Generating Agda library interface files...
... /builds/ghc/head.hackage/ci/run/test-Agda-2.6.1.3/dist-newstyle/tmp/src-11665/Agda-2.6.1.3/src/data/lib/prim/Agda/Builtin/Bool.agda
... /builds/ghc/head.hackage/ci/run/test-Agda-2.6.1.3/dist-newstyle/tmp/src-11665/Agda-2.6.1.3/src/data/lib/prim/Agda/Builtin/Char.agda
... /builds/ghc/head.hackage/ci/run/test-Agda-2.6.1.3/dist-newstyle/tmp/src-11665/Agda-2.6.1.3/src/data/lib/prim/Agda/Builtin/Char/Properties.agda
cabal: Failed to build Agda-2.6.1.3 (which is required by test-Agda-1.0). See
the build log above for details.

And when building Agda-2.6.2.1, the most recent Hackage release, it will fail with this error, as seen here:

Importing module Agda.Builtin.Bool not using the --no-subtyping
flag from a module which does.
Error: Failed to typecheck /builds/ghc/head.hackage/ci/run/test-Agda-2.6.2.1/dist-newstyle/tmp/src-11770/Agda-2.6.2.1/src/data/lib/prim/Agda/Builtin/Bool.agda!
Generating Agda library interface files...
... /builds/ghc/head.hackage/ci/run/test-Agda-2.6.2.1/dist-newstyle/tmp/src-11770/Agda-2.6.2.1/src/data/lib/prim/Agda/Builtin/Bool.agda
cabal: Failed to build Agda-2.6.2.1 (which is required by test-Agda-1.0). See
the build log above for details.

Unfortunately, I have not yet figured out a way to minimize the issue yet. The only way I know how to reproduce the issue is:

1. Set up head.hackage.

2. Run:

   $ head.hackage/scripts/patch-tool unpack-patch Agda <AGDA_VER>

   where <AGDA_VER> is one of 2.6.1.3 or 2.6.2.1.

3. cabal build Agda

4. Run:

   Agda_datadir=<PREFIX>/packages/Agda-<AGDA_VER>/src/data <PREFIX>/dist-newstyle/build/x86_64-linux/ghc-<GHC_VER>/Agda-<AGDA_VER>/build/agda/agda --no-libraries --local-interfaces -Werror <PREFIX>/packages/Agda-<AGDA_VER>/src/data/lib/prim/Agda/Builtin/Char/Properties.agda -v0

   where <PREFIX> is the directory where you checked out head.hackage, <GHC_VER> is the version of HEAD you're using, and <AGDA_VER> is the same as in step (2).

Some notes:

• Bisecting reveals that commit 0e93023e (Tag inference work.) is the culprit.

• In the case of Agda-2.6.2.1, the issue seems to involve roundtripping through interface files. Despite the error message given above, Agda.Builtin.Bool does in fact enable --no-subtyping. In fact, when Agda first parses this module, it correctly recognizes the presence of --no-subtyping. It's only after Agda writes Agda.Builtin.Bool to an interface file and reads it back that Agda mistakenly believes that Agda.Builtin.Bool does not enable --no-subtyping.

  When Agda serializes a module to an interface file, it uses the zlib library to do so. Independently of this bug, I discovered that zlib's test suite segfaults on HEAD—see #21186 (closed). However, that issue predates the Tag inference work. commit (see #21186 (comment 413308)), so that may just be a coincidence.

I'm opening this issue as a reminder to continue minimizing the Agda failure into something more tractable. For the time being, I'll mark Agda as being allowed to fail on the HEAD CI job.