Release notes for Agda version 2.6.2.2

Highlights

• Agda 2.6.2.2 catches up to changes in the Haskell ecosystem (bytestring-0.11.2.0, mtl-2.3-rc3/4, text-icu-0.8.0.1, stackage lts-19.0 and nightly).

• Fixes inconsistency #5838 in --cubical.

• Fixes some regressions introduced in 2.6.1:

  • #5809: internal error with --irrelevant-projections.

• Fixes some regressions introduced in 2.6.2:

  • #5705 and #5706: inconsistency from universe level Int overflow.

  • #5784: primEraseEquality does not compute.

  • #5805: internal error involving holes and with.

  • #5819: internal error when reducing in termination checker.

• Other fixes and improvements (see below).

Installation and infrastructure

Agda supports GHC versions 8.0.2 to 9.2.2.

• UTF-8 encoding is now used for the libraries and executables configuration files (issue #5741).

Language

• macro definitions can now be used even when they are declared as erased (PR #5744). For example, this is now accepted:

  macro
    @0 trivial : Term → TC ⊤
    trivial = unify (con (quote refl) [])
  
  test : 42 ≡ 42
  test = trivial
  

• Fixed inconsistent --cubical reductions for transp: issue #5838.

• Fixed issues with reflection:

  • #5762: do not eagerly check existence of commands in executables file.

  • #5695: fix elaborate-and-give interaction command.

  • #5700: scope of metas created during macro expansion.

  • #5712: internal error with tactics on record fields of function type.

• Fixed issues with instance search:

  • #5583: constructor instances from parameterized modules.

  • #5787: erased instance arguments.

• Fixed issue #5683 with generalization in let.

Compiler backends

• .hs files generated by the GHC backend now switch off the warn-overlapping-patterns warning (issue #5758).

• The GHC backend now calls ghc with environment setting GHC_CHARENC=UTF-8 (issue #5742).

Performance

• Better caching of interfaces (issue #2767).

• Various performance improvements concerning meta-variables: issue #5388 and PR #5733.