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).