2.6.2.2.md

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](https://github.com/agda/agda/issues/5838)
  in `--cubical`.

* Fixes some regressions introduced in 2.6.1:

  - [#5809](https://github.com/agda/agda/issues/5809):
    internal error with `--irrelevant-projections`.

* Fixes some regressions introduced in 2.6.2:

  - [#5705](https://github.com/agda/agda/issues/5705) and
    [#5706](https://github.com/agda/agda/issues/5706):
    inconsistency from universe level `Int` overflow.

  - [#5784](https://github.com/agda/agda/issues/5784):
    `primEraseEquality` does not compute.

  - [#5805](https://github.com/agda/agda/issues/5805):
    internal error involving holes and `with`.

  - [#5819](https://github.com/agda/agda/issues/5819):
    internal error when reducing in termination checker.

* Other
  [fixes](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.2.2+is%3Aclosed)
  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](https://github.com/agda/agda/issues/5741)).

Language
--------

* `macro` definitions can now be used even when they are declared as erased
  (PR [#5744](https://github.com/agda/agda/pull/5744)).
  For example, this is now accepted:
  ```agda
  macro
    @0 trivial : Term → TC ⊤
    trivial = unify (con (quote refl) [])

  test : 42 ≡ 42
  test = trivial
  ```

* Fixed inconsistent `--cubical` reductions for `transp`:
  issue [#5838](https://github.com/agda/agda/issues/5838).

* Fixed issues with reflection:

  - [#5762](https://github.com/agda/agda/issues/5762):
    do not eagerly check existence of commands in `executables` file.

  - [#5695](https://github.com/agda/agda/issues/5695):
    fix `elaborate-and-give` interaction command.

  - [#5700](https://github.com/agda/agda/issues/5700):
    scope of metas created during macro expansion.

  - [#5712](https://github.com/agda/agda/issues/5712):
    internal error with tactics on record fields of function type.

* Fixed issues with instance search:

  - [#5583](https://github.com/agda/agda/issues/5583):
    constructor instances from parameterized modules.

  - [#5787](https://github.com/agda/agda/issues/5787):
    erased instance arguments.

* Fixed issue [#5683](https://github.com/agda/agda/issues/5683) with
  generalization in `let`.

Compiler backends
-----------------

* `.hs` files generated by the GHC backend now switch off the
  `warn-overlapping-patterns` warning (issue
  [#5758](https://github.com/agda/agda/issues/5758)).

* The GHC backend now calls `ghc` with environment setting
  `GHC_CHARENC=UTF-8` (issue
  [#5742](https://github.com/agda/agda/issues/5742)).

Performance
-----------

* Better caching of interfaces
  (issue [#2767](https://github.com/agda/agda/issues/2767)).

* Various performance improvements concerning meta-variables:
  issue [#5388](https://github.com/agda/agda/issues/5388)
  and PR [#5733](https://github.com/agda/agda/pull/5733).