Changelog of @hackage/Agda 2.6.2.2

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.