====================================
Highlights
----------
Installation
------------
* Dropped support for GHC 8.6.
* Agda supports GHC versions 8.8.4 to 9.10.1.
* **Breaking**: Custom `Setup.hs` has been removed.
Agda will no longer build the `.agdai` files for the primitive and builtin modules
as part of the installation.
So if you do a system-wide installation where the installation location
is not writeable by the Agda users, you need to manually generate these files,
e.g. using these shell commands:
sh
cd "$(agda --print-agda-data-dir)/lib/prim"
find . -name "*.agda" -exec agda {} \;
Binary distributions of Agda should come equipped with these files.
So, if you are a packager, please include this step in your packaging routine.
* Added cabal build flag `dump-core` to save the optimised GHC Core code during
compilation of Agda. This can be useful for people working on improving the
performance of the Agda implementation.
Pragmas and options
-------------------
* Option `--local-interfaces` and warning `DuplicateInterfaceFiles` have been removed.
* New warning `InvalidDisplayForm` instead of hard error
when a display form is illegal (and thus ignored).
* New warning `UnusedVariablesInDisplayForm` when DISPLAY pragma
binds variables that are not used.
Example:
agda
{- DISPLAY List (Fin n) = ListFin -}
Since pattern variable `n` is not used on the right hand side `ListFin`,
Agda throws a warning and recommeds to rewrite it as:
agda
{- DISPLAY List (Fin _) = ListFin -}
* New warning `WithClauseProjectionFixityMismatch` instead of hard error
when in a with-clause a projection is used in a different fixity
(prefix vs. postfix) than in its parent clause.
* New error warning `TooManyArgumentsToSort` instead of hard error.
* New warning `EmptyPolarityPragma` for POLARITY pragma without polarities.
E.g. triggered by `{- POLARITY F -}`.
* Warning `AbsurdPatternRequiresNoRHS` has been renamed to
`AbsurdPatternRequiresAbsentRHS`.
* New option `--js-es6` for generating JavaScript with ES6 module syntax.
* DISPLAY pragmas can now define display forms that match on defined names
beyond constructors ([issue 7533](https://github.com/agda/agda/issues/7533)).
Example:
agda
{- DISPLAY Irrelevant Empty = ⊥ -}
`Empty` used to be interpreted as a pattern variable, effectively installing
the display form `Irrelevant _ = ⊥`.
Now `Empty` is treated as a matchable name, as one would intuitively expect
from a display form.
As a consequence, only `Irrelevant Empty` is displayed as `⊥`, not just any
`Irrelevant A`.
Polarity
--------
* Support for polarity annotations can be enabled by the feature flag
`--polarity`.
This flag is infective.
Uses of variables bound with polarity annotations are checked through modal
typing rules, and the positivity checker has been expanded to take annotations
into account. This means that the following is now definable:
agda
{- OPTIONS --polarity -}
data Mu (F : ++ Set → Set) : Set where
fix : F (Mu F) → Mu F
Syntax
------
Additions to the Agda syntax.
* Add new literate agda: forester, see [7403](https://github.com/agda/agda/pull/7403)
* Records can now be created using module-like syntax in place of curly braces
and semicolons.
agda
p : Pair Nat Nat
p = record where
fst = 2
snd = 3
In a `record where` block, definitions have the semantics of let-bindings: they
can refer to earlier bindings and may include other definitions than the fields
of the record, including opening of modules. For instance,
agda
p₁ : Pair Nat Nat
p₁ = record where
open Pair p using (fst)
n = fst * 2
snd = n * n
The syntax also works for record updates
agda
p₂ : Pair Nat Nat
p₂ = record p₁ where
snd = snd p₁ + 1
See [4275](https://github.com/agda/agda/issues/4275) for the proposal.
* It is now always possible to refer to the name of a record type's
constructor, even if a name was not explicitly specified. This is done
using the new `(Record name).constructor` syntax; See [issue
6964](https://github.com/agda/agda/issues/6964) for the motivation.
* The *left-hand-sides* of functions bound in a `let` expression can now
contain the same types of patterns that are allowed in lambda
expressions, in dependent function types, and in other `let` bindings.
This means that
agda
let
f : A → B → C
f p1 p2 = ...
in ...
should be accepted exactly when, and have the same meaning as,
agda
let
f : A → B → C
f = λ p1 p2 → ...
See [7572](https://github.com/agda/agda/pull/7572).
Language
--------
Changes to type checker and other components defining the Agda language.
* **BREAKING**: The primitive "cubical identity type", previously
exported from `Agda.Builtin.Cubical.Id`, has been removed. Its
computational behaviour is exactly replicated by the user-definable
identity type, which is also exported from `Agda.Builtin.Equality`.
See [agda/cubical1005](https://github.com/agda/cubical/pull/1005) for
the PR removing it from the library, and
[7652](https://github.com/agda/agda/pull/7652) for the compiler.
Reflection
----------
Changes to the meta-programming facilities.
* New reflection primitive: `checkFromStringTC : String → Type → TC Term`
Parse and type check the given string against the given type, returning
the resulting term (when successful).
Library management
------------------
* **BREAKING**: Agda no longer accepts several `.agda-lib` files in the root
of an Agda project.
(Previously, it allowed this and took the union of their contents.)
Interaction and emacs mode
--------------------------
* Agda's error messages now follow the [GNU standard](https://www.gnu.org/prep/standards/html_node/Errors.html).
To comply with this policy, line and column are now separated by a dot instead of comma.
The format of regular errors and error warnings follows this template:
> _sourcefile_:_line1_._column1_-_line2_._column2_: error: [_ErrorName_]
> ...
> _error message_
> ...
> when _error context_
_line2_ or even _column2_ can be missing, in some cases even the entire error location.
Internal errors might follow a different format.
Warnings are printed in a similar format:
> _sourcefile_:_line1_._column1_-_line2_._column2_: warning: -W[no]_WarningName_
> ...
> _warning text_
> ...
> when _warning context_
* Emacs: new face `agda2-highlight-cosmetic-problem-face`
for highlighting the new aspect `CosmeticProblem`.
* Emacs: new face `agda2-highlight-instance-problem-face`
for highlighting the new aspect `InstanceProblem`.
Backends
--------
* New `backendInteractTop/backendInteractHole` fields for providing backend-specific interaction commands (run with keyboard shortcut `C-c C-i`).
Other issues closed
-------------------
For 2.8.0, the following issues were also
[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.8.0+is%3Aclosed)
(see [bug tracker](https://github.com/agda/agda/issues)):
NOTE: This section will be filled by output produced with `closed-issues-for-milestone 2.8.0`.