Release notes for Agda version 2.5.3
====================================
Installation and infrastructure
-------------------------------
* Added support for GHC 8.0.2 and 8.2.1.
* Removed support for GHC 7.6.3.
* Markdown support for literate Agda
\[PR [#2357](https://github.com/agda/agda/pull/2357)].
Files ending in `.lagda.md` will be parsed as literate Markdown files.
+ Code blocks start with ```` ``` ```` or ```` ```agda ```` in its own line, and end with
```` ``` ````, also in its own line.
+ Code blocks which should be type-checked by Agda but should not be visible
when the Markdown is rendered may be enclosed in HTML comment delimiters
(`<!--` and `-->`).
+ Code blocks which should be ignored by Agda, but rendered in the final
document may be indented by four spaces.
+ Note that inline code fragments are not supported due to the difficulty of
interpreting their indentation level with respect to the rest of the file.
Language
--------
### Pattern matching
* Dot patterns.
The dot in front of an inaccessible pattern can now be skipped if the
pattern consists entirely of constructors or literals. For example:
```agda
open import Agda.Builtin.Bool
data D : Bool → Set where
c : D true
f : (x : Bool) → D x → Bool
f true c = true
```
Before this change, you had to write `f .true c = true`.
* With-clause patterns can be replaced by _
[Issue [#2363](https://github.com/agda/agda/issues/2363)].
Example:
```agda
test : Nat → Set
test zero with zero
test _ | _ = Nat
test (suc x) with zero
test _ | _ = Nat
```
We do not have to spell out the pattern of the parent clause
(`zero` / `suc x`) in the with-clause if we do not need the
pattern variables. Note that `x` is not in scope in the
with-clause!
A more elaborate example, which cannot be reduced to
an ellipsis `...`:
```agda
record R : Set where
coinductive -- disallow matching
field f : Bool
n : Nat
data P (r : R) : Nat → Set where
fTrue : R.f r ≡ true → P r zero
nSuc : P r (suc (R.n r))
data Q : (b : Bool) (n : Nat) → Set where
true! : Q true zero
suc! : ∀{b n} → Q b (suc n)
test : (r : R) {n : Nat} (p : P r n) → Q (R.f r) n
test r nSuc = suc!
test r (fTrue p) with R.f r
test _ (fTrue ()) | false
test _ _ | true = true! -- underscore instead of (isTrue _)
```
* Pattern matching lambdas (also known as extended lambdas) can now be
nullary, mirroring the behaviour for ordinary function definitions.
[Issue [#2671](https://github.com/agda/agda/issues/2671)]
This is useful for case splitting on the result inside an
expression: given
```agda
record _×_ (A B : Set) : Set where
field
π₁ : A
π₂ : B
open _×_
```
one may case split on the result (C-c C-c RET) in a hole
```agda
λ { → {!!}}
```
of type A × B to produce
```agda
λ { .π₁ → {!!} ; .π₂ → {!!}}
```
* Records with a field of an empty type are now recognized as empty by Agda.
In particular, they can be matched against with an absurd pattern ().
For example:
```agda
data ⊥ : Set where
record Empty : Set where
field absurdity : ⊥
magic : Empty → ⊥
magic ()
```
* Injective pragmas.
Injective pragmas can be used to mark a definition as injective for the
pattern matching unifier. This can be used as a version of
`--injective-type-constructors` that only applies to specific datatypes.
For example:
```agda
open import Agda.Builtin.Equality
data Fin : Nat → Set where
zero : {n : Nat} → Fin (suc n)
suc : {n : Nat} → Fin n → Fin (suc n)
{-# INJECTIVE Fin #-}
Fin-injective : {m n : Nat} → Fin m ≡ Fin n → m ≡ n
Fin-injective refl = refl
```
Aside from datatypes, this pragma can also be used to mark other definitions
as being injective (for example postulates).
* Metavariables can no longer be instantiated during case splitting. This means
Agda will refuse to split instead of taking the first constructor it finds.
For example:
```agda
open import Agda.Builtin.Nat
data Vec (A : Set) : Nat → Set where
nil : Vec A 0
cons : {n : Nat} → A → Vec A n → Vec A (suc n)
foo : Vec Nat _ → Nat
foo x = {!x!}
```
In Agda 2.5.2, case splitting on `x` produced the single clause
`foo nil = {!!}`, but now Agda refuses to split.
### Reflection
* New TC primitive: `debugPrint`.
```agda
debugPrint : String → Nat → List ErrorPart → TC ⊤
```
This maps to the internal function `reportSDoc`. Debug output is enabled with
the `-v` flag at the command line, or in an `OPTIONS` pragma. For instance,
giving `-v a.b.c:10` enables printing from `debugPrint "a.b.c.d" 10 msg`. In the
Emacs mode, debug output ends up in the `*Agda debug*` buffer.
### Built-ins
* BUILTIN REFL is now superfluous, subsumed by BUILTIN EQUALITY
[Issue [#2389](https://github.com/agda/agda/issues/2389)].
* BUILTIN EQUALITY is now more liberal
[Issue [#2386](https://github.com/agda/agda/issues/2386)].
It accepts, among others, the following new definitions of equality:
```agda
-- Non-universe polymorphic:
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
-- ... with explicit argument to refl;
data _≡_ {A : Set} : (x y : A) → Set where
refl : {x : A} → x ≡ x
-- ... even visible
data _≡_ {A : Set} : (x y : A) → Set where
refl : (x : A) → x ≡ x
-- Equality in a different universe than domain:
-- (also with explicit argument to refl)
data _≡_ {a} {A : Set a} (x : A) : A → Set where
refl : x ≡ x
```
The standard definition is still:
```agda
-- Equality in same universe as domain:
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
```
### Miscellaneous
* Rule change for omitted top-level module headers.
[Issue [#1077](https://github.com/agda/agda/issues/1077)]
If your file is named `Bla.agda`, then the following content
is rejected.
```agda
foo = Set
module Bla where
bar = Set
```
Before the fix of this issue, Agda would add the missing module
header `module Bla where` at the top of the file.
However, in this particular case it is more likely the user
put the declaration `foo = Set` before the module start in error.
Now you get the error
```
Illegal declaration(s) before top-level module
```
if the following conditions are met:
1. There is at least one non-import declaration or non-toplevel pragma
before the start of the first module.
2. The module has the same name as the file.
3. The module is the only module at this level
(may have submodules, of course).
If you should see this error, insert a top-level module
before the illegal declarations, or move them inside the
existing module.
Emacs mode
----------
* New warnings:
- Unreachable clauses give rise to a simple warning. They are
highlighted in gray.
- Incomplete patterns are non-fatal warnings: it is possible
to keep interacting with the file (the reduction will simply
be stuck on arguments not matching any pattern).
The definition with incomplete patterns are highlighted in
wheat.
* Clauses which do not hold definitionally are now highlighted in white smoke.
* Fewer commands have the side effect that the buffer is saved.
* Aborting commands.
Now one can (try to) abort an Agda command by using `C-c C-x C-a` or
a menu entry. The effect is similar to that of restarting Agda (`C-c
C-x C-r`), but some state is preserved, which could mean that it
takes less time to reload the module.
Warning: If a command is aborted while it is writing data to disk
(for instance `.agdai` files or Haskell files generated by the GHC
backend), then the resulting files may be corrupted. Note also that
external commands (like GHC) are not aborted, and their output may
continue to be sent to the Emacs mode.
* New bindings for the Agda input method:
- All the bold digits are now available. The naming scheme is `\Bx` for digit `x`.
- Typing `\:` you can now get a whole slew of colons.
(The Agda input method originally only bound the standard unicode colon,
which looks deceptively like the normal colon.)
* Case splitting now preserves underscores.
[Issue [#819](https://github.com/agda/agda/issues/819)]
```agda
data ⊥ : Set where
test : {A B : Set} → A → ⊥ → B
test _ x = {! x !}
```
Splitting on `x` yields
```agda
test _ ()
```
* Interactively expanding ellipsis.
[Issue [#2589](https://github.com/agda/agda/issues/2589)]
An ellipsis in a with-clause can be expanded by splitting on "variable" "." (dot).
```agda
test0 : Nat → Nat
test0 x with zero
... | q = {! . !} -- C-c C-c
```
Splitting on dot here yields:
```agda
test0 x | q = ?
```
* New command to check an expression against the type of the hole
it is in and see what it elaborates to.
[Issue [#2700](https://github.com/agda/agda/issues/2700)]
This is useful to determine e.g. what solution typeclass resolution yields.
The command is bound to `C-c C-;` and respects the `C-u` modifier.
```agda
record Pointed (A : Set) : Set where
field point : A
it : ∀ {A : Set} {{x : A}} → A
it {{x}} = x
instance _ = record { point = 3 - 4 }
_ : Pointed Nat
_ = {! it !} -- C-u C-u C-c C-;
```
yields
```agda
Goal: Pointed Nat
Elaborates to: record { point = 0 }
```
* If `agda2-give` is called with a prefix, then giving is forced,
i.e., the safety checks are skipped,
including positivity, termination, and double type-checking.
[Issue [#2730](https://github.com/agda/agda/issues/2730)]
Invoke forced giving with key sequence `C-u C-c C-SPC`.
Library management
------------------
* The `name` field in an `.agda-lib` file is now optional.
[Issue [#2708](https://github.com/agda/agda/issues/2708)]
This feature is convenient if you just want to specify the dependencies
and include pathes for your local project in an `.agda-lib` file.
Naturally, libraries without names cannot be depended on.
Compiler backends
-----------------
* Unified compiler pragmas
The compiler pragmas (`COMPILED`, `COMPILED_DATA`, etc.) have been unified across
backends into two new pragmas:
```
{-# COMPILE <Backend> <Name> <Text> #-}
{-# FOREIGN <Backend> <Text> #-}
```
The old pragmas still work, but will emit a warning if used. They will be
removed completely in Agda 2.6.
The translation of old pragmas into new ones is as follows:
Old | New
--- | ---
`{-# COMPILED f e #-}` | `{-# COMPILE GHC f = e #-}`
`{-# COMPILED_TYPE A T #-}` | `{-# COMPILE GHC A = type T #-}`
`{-# COMPILED_DATA A D C1 .. CN #-}` | `{-# COMPILE GHC A = data D (C1 \| .. \| CN) #-}`
`{-# COMPILED_DECLARE_DATA #-}` | obsolete, removed
`{-# COMPILED_EXPORT f g #-}` | `{-# COMPILE GHC f as g #-}`
`{-# IMPORT M #-}` | `{-# FOREIGN GHC import qualified M #-}`
`{-# HASKELL code #-}` | `{-# FOREIGN GHC code #-}`
`{-# COMPILED_UHC f e #-}` | `{-# COMPILE UHC f = e #-}`
`{-# COMPILED_DATA_UHC A D C1 .. CN #-}` | `{-# COMPILE UHC A = data D (C1 \| .. \| CN) #-}`
`{-# IMPORT_UHC M #-}` | `{-# FOREIGN UHC __IMPORT__ M #-}`
`{-# COMPILED_JS f e #-}` | `{-# COMPILE JS f = e #-}`
* GHC Haskell backend
The COMPILED pragma (and the corresponding COMPILE GHC pragma) is now also
allowed for functions. This makes it possible to have both an Agda
implementation and a native Haskell runtime implementation.
The GHC file header pragmas `LANGUAGE`, `OPTIONS_GHC`, and `INCLUDE`
inside a `FOREIGN GHC` pragma are recognized and printed correctly
at the top of the generated Haskell file.
[Issue [#2712](https://github.com/agda/agda/issues/2712)]
* UHC compiler backend
The UHC backend has been moved to its own repository
[https://github.com/agda/agda-uhc] and is no longer part of the Agda
distribution.
* Haskell imports are no longer transitively inherited from imported modules.
The (now deprecated) IMPORT and IMPORT_UHC pragmas no longer cause import
statements in modules importing the module containing the pragma.
The same is true for the corresponding FOREIGN pragmas.
* Support for stand-alone backends.
There is a new API in `Agda.Compiler.Backend` for creating stand-alone
backends using Agda as a library. This allows prospective backend writers to
experiment with new backends without having to change the Agda code base.
HTML backend
------------
* Anchors for identifiers (excluding bound variables) are now the
identifiers themselves rather than just the file position
[Issue [#2604](https://github.com/agda/agda/issues/2604)].
Symbolic anchors look like
```html
<a id="test1">
<a id="M.bla">
```
while other anchors just give the character position in the file:
```html
<a id="42">
```
Top-level module names do not get a symbolic anchor, since the position of
a top-level module is defined to be the beginning of the file.
Example:
```agda
module Issue2604 where -- Character position anchor
test1 : Set₁ -- Issue2604.html#test1
test1 = bla
where
bla = Set -- Character position anchor
test2 : Set₁ -- Issue2604.html#test2
test2 = bla
where
bla = Set -- Character position anchor
test3 : Set₁ -- Issue2604.html#test3
test3 = bla
module M where -- Issue2604.html#M
bla = Set -- Issue2604.html#M.bla
module NamedModule where -- Issue2604.html#NamedModule
test4 : Set₁ -- Issue2604.html#NamedModule.test4
test4 = M.bla
module _ where -- Character position anchor
test5 : Set₁ -- Character position anchor
test5 = M.bla
```
* Some generated HTML files now have different file names [Issue
[#2725](https://github.com/agda/agda/issues/2725)].
Agda now uses an encoding that amounts to first converting the
module names to UTF-8, and then percent-encoding the resulting
bytes. For instance, HTML for the module `Σ` is placed in
`%CE%A3.html`.
LaTeX backend
-------------
* The LaTeX backend now handles indentation in a different way [Issue
[#1832](https://github.com/agda/agda/issues/1832)].
A constraint on the indentation of the first token *t* on a line is
determined as follows:
* Let *T* be the set containing every previous token (in any code
block) that is either the initial token on its line or preceded by
at least one whitespace character.
* Let *S* be the set containing all tokens in *T* that are not
*shadowed* by other tokens in *T*. A token *t₁* is shadowed by
*t₂* if *t₂* is further down than *t₁* and does not start to the
right of *t₁*.
* Let *L* be the set containing all tokens in *S* that start to the
left of *t*, and *E* be the set containing all tokens in *S* that
start in the same column as *t*.
* The constraint is that *t* must be indented further than every
token in *L*, and aligned with every token in *E*.
Note that if any token in *L* or *E* belongs to a previous code
block, then the constraint may not be satisfied unless (say) the
`AgdaAlign` environment is used in an appropriate way.
If custom settings are used, for instance if `\AgdaIndent` is
redefined, then the constraint discussed above may not be satisfied.
(Note that the meaning of the `\AgdaIndent` command's argument has
changed, and that the command is now used in a different way in the
generated LaTeX files.)
Examples:
* Here `C` is indented further than `B`:
```agda
postulate
A B
C : Set
```
* Here `C` is not (necessarily) indented further than `B`, because
`X` shadows `B`:
```agda
postulate
A B : Set
X
C : Set
```
The new rule is inspired by, but not identical to, the one used by
lhs2TeX's poly mode (see Section 8.4 of the [manual for lhs2TeX
version 1.17](https://www.andres-loeh.de/lhs2tex/Guide2-1.17.pdf)).
* Some spacing issues
[[#2353](https://github.com/agda/agda/issues/2353),
[#2441](https://github.com/agda/agda/issues/2441),
[#2733](https://github.com/agda/agda/issues/2733),
[#2740](https://github.com/agda/agda/issues/2740)] have been fixed.
* The user can now control the typesetting of (certain) individual tokens
by redefining the `\AgdaFormat` command. Example:
```latex
\usepackage{ifthen}
% Insert extra space before some tokens.
\DeclareRobustCommand{\AgdaFormat}[2]{%
\ifthenelse{
\equal{#1}{≡⟨} \OR
\equal{#1}{≡⟨⟩} \OR
\equal{#1}{∎}
}{\ }{}#2}
```
Note the use of `\DeclareRobustCommand`. The first argument to
`\AgdaFormat` is the token, and the second argument the thing to
be typeset.
* One can now instruct the agda package not to select any fonts.
If the `nofontsetup` option is used, then some font packages are
loaded, but specific fonts are not selected:
```latex
\usepackage[nofontsetup]{agda}
```
* The height of empty lines is now configurable
[[#2734](https://github.com/agda/agda/issues/2734)].
The height is controlled by the length `\AgdaEmptySkip`, which by
default is `\baselineskip`.
* The alignment feature regards the string `+̲`, containing `+` and a
combining character, as having length two. However, it seems more
reasonable to treat it as having length one, as it occupies a single
column, if displayed "properly" using a monospace font. The new flag
`--count-clusters` is an attempt at fixing this. When this flag is
enabled the backend counts ["extended grapheme
clusters"](http://www.unicode.org/reports/tr29/#Grapheme_Cluster_Boundaries)
rather than code points.
Note that this fix is not perfect: a single extended grapheme
cluster might be displayed in different ways by different programs,
and might, in some cases, occupy more than one column. Here are some
examples of extended grapheme clusters, all of which are treated as
a single character by the alignment algorithm:
```
│ │
│+̲│
│Ö̂│
│நி│
│ᄀힰᇹ│
│ᄀᄀᄀᄀᄀᄀힰᇹᇹᇹᇹᇹᇹ│
│ │
```
Note also that the layout machinery does not count extended grapheme
clusters, but code points. The following code is syntactically
correct, but if `--count-clusters` is used, then the LaTeX backend
does not align the two `field` keywords:
```agda
record +̲ : Set₁ where field A : Set
field B : Set
```
The `--count-clusters` flag is not enabled in all builds of Agda,
because the implementation depends on the
[ICU](http://site.icu-project.org) library, the installation of
which could cause extra trouble for some users. The presence of this
flag is controlled by the Cabal flag `enable-cluster-counting`.
* A faster variant of the LaTeX backend: QuickLaTeX.
When this variant of the backend is used the top-level module is not
type-checked, only scope-checked. This implies that some
highlighting information is not available. For instance, overloaded
constructors are not resolved.
QuickLaTeX can be invoked from the Emacs mode, or using `agda
--latex --only-scope-checking`. If the module has already been
type-checked successfully, then this information is reused; in this
case QuickLaTeX behaves like the regular LaTeX backend.
The `--only-scope-checking` flag can also be used independently, but
it is perhaps unclear what purpose that would serve. (The flag can
currently not be combined with `--html`, `--dependency-graph` or
`--vim`.) The flag is not allowed in safe mode.
Pragmas and options
-------------------
* The `--safe` option is now a valid pragma.
This makes it possible to declare a module as being part of the safe
subset of the language by stating `{-# OPTIONS --safe #-}` at the top
of the corresponding file. Incompatibilities between the `--safe` option
and other options or language constructs are non-fatal errors.
* The `--no-main` option is now a valid pragma.
One can now suppress the compiler warning about a missing main function by
putting
```agda
{-# OPTIONS --no-main #-}
```
on top of the file.
* New command-line option and pragma `--warning=MODE` (or `-W MODE`) for
setting the warning mode. Current options are
- `warn` for displaying warnings (default)
- `error` for turning warnings into errors
- `ignore` for not displaying warnings
List of fixed issues
--------------------
For 2.5.3, the following issues have been fixed
(see [bug tracker](https://github.com/agda/agda/issues)):
- [#142](https://github.com/agda/agda/issues/142): Inherited dot patterns in with functions are not checked
- [#623](https://github.com/agda/agda/issues/623): Error message points to importing module rather than imported module
- [#657](https://github.com/agda/agda/issues/657): Yet another display form problem
- [#668](https://github.com/agda/agda/issues/668): Ability to stop, or restart, typechecking somehow
- [#705](https://github.com/agda/agda/issues/705): confusing error message for ambiguous datatype module name
- [#719](https://github.com/agda/agda/issues/719): Error message for duplicate module definition points to external module instead of internal module
- [#776](https://github.com/agda/agda/issues/776): Unsolvable constraints should give error
- [#819](https://github.com/agda/agda/issues/819): Case-splitting doesn't preserve underscores
- [#883](https://github.com/agda/agda/issues/883): Rewrite loses type information
- [#899](https://github.com/agda/agda/issues/899): Instance search fails if there are several definitionally equal values in scope
- [#1077](https://github.com/agda/agda/issues/1077): problem with module syntax, with parametric module import
- [#1126](https://github.com/agda/agda/issues/1126): Port optimizations from the Epic backend
- [#1175](https://github.com/agda/agda/issues/1175): Internal Error in Auto
- [#1544](https://github.com/agda/agda/issues/1544): Positivity polymorphism needed for compositional positivity analysis
- [#1611](https://github.com/agda/agda/issues/1611): Interactive splitting instantiates meta
- [#1664](https://github.com/agda/agda/issues/1664): Add Reflection primitives to expose precedence and fixity
- [#1817](https://github.com/agda/agda/issues/1817): Solvable size constraints reported as unsolvable
- [#1832](https://github.com/agda/agda/issues/1832): Insufficient indentation in LaTeX-rendered Agda code
- [#1834](https://github.com/agda/agda/issues/1834): Copattern matching: order of clauses should not matter here
- [#1886](https://github.com/agda/agda/issues/1886): Second copies of telescopes not checked?
- [#1899](https://github.com/agda/agda/issues/1899): Positivity checker does not treat datatypes and record types in the same way
- [#1975](https://github.com/agda/agda/issues/1975): Type-incorrect instantiated overloaded constructor accepted in pattern
- [#1976](https://github.com/agda/agda/issues/1976): Type-incorrect instantiated projection accepted in pattern
- [#2035](https://github.com/agda/agda/issues/2035): Matching on string causes solver to fail with internal error
- [#2146](https://github.com/agda/agda/issues/2146): Unicode syntax for instance arguments
- [#2217](https://github.com/agda/agda/issues/2217): Abort Agda without losing state
- [#2229](https://github.com/agda/agda/issues/2229): Absence or presence of top-level module header affects scope
- [#2253](https://github.com/agda/agda/issues/2253): Wrong scope error for abstract constructors
- [#2261](https://github.com/agda/agda/issues/2261): Internal error in Auto/CaseSplit.hs:284
- [#2270](https://github.com/agda/agda/issues/2270): Printer does not use sections.
- [#2329](https://github.com/agda/agda/issues/2329): Size solver does not use type `Size< i` to gain the necessary information
- [#2354](https://github.com/agda/agda/issues/2354): Interaction between instance search, size solver, and ordinary constraint solver.
- [#2355](https://github.com/agda/agda/issues/2355): Literate Agda parser does not recognize TeX comments
- [#2360](https://github.com/agda/agda/issues/2360): With clause stripping chokes on ambiguous projection
- [#2362](https://github.com/agda/agda/issues/2362): Printing of parent patterns when with-clause does not match
- [#2363](https://github.com/agda/agda/issues/2363): Allow underscore in with-clause patterns
- [#2366](https://github.com/agda/agda/issues/2366): With-clause patterns renamed in error message
- [#2368](https://github.com/agda/agda/issues/2368): Internal error after refining a tactic @ MetaVars.hs:267
- [#2371](https://github.com/agda/agda/issues/2371): Shadowed module parameter crashes interaction
- [#2372](https://github.com/agda/agda/issues/2372): problems when instances are declared with inferred types
- [#2374](https://github.com/agda/agda/issues/2374): Ambiguous projection pattern could be disambiguated by visibility
- [#2376](https://github.com/agda/agda/issues/2376): Termination checking interacts badly with eta-contraction
- [#2377](https://github.com/agda/agda/issues/2377): open public is useless before module header
- [#2381](https://github.com/agda/agda/issues/2381): Search (`C-c C-z`) panics on pattern synonyms
- [#2386](https://github.com/agda/agda/issues/2386): Relax requirements of BUILTIN EQUALITY
- [#2389](https://github.com/agda/agda/issues/2389): BUILTIN REFL not needed
- [#2400](https://github.com/agda/agda/issues/2400): LaTeX backend error on LaTeX comments
- [#2402](https://github.com/agda/agda/issues/2402): Parameters not dropped when reporting incomplete patterns
- [#2403](https://github.com/agda/agda/issues/2403): Termination checker should reduce arguments in structural order check
- [#2405](https://github.com/agda/agda/issues/2405): instance search failing in parameterized module
- [#2408](https://github.com/agda/agda/issues/2408): DLub sorts are not serialized
- [#2412](https://github.com/agda/agda/issues/2412): Problem with checking with sized types
- [#2413](https://github.com/agda/agda/issues/2413): Agda crashes on x@y pattern
- [#2415](https://github.com/agda/agda/issues/2415): Size solver reports "inconsistent upper bound" even though there is a solution
- [#2416](https://github.com/agda/agda/issues/2416): Cannot give size as computed by solver
- [#2422](https://github.com/agda/agda/issues/2422): Overloaded inherited projections don't resolve
- [#2423](https://github.com/agda/agda/issues/2423): Inherited projection on lhs
- [#2426](https://github.com/agda/agda/issues/2426): On just warning about missing cases
- [#2429](https://github.com/agda/agda/issues/2429): Irrelevant lambda should be accepted when relevant lambda is expected
- [#2430](https://github.com/agda/agda/issues/2430): Another regression related to parameter refinement?
- [#2433](https://github.com/agda/agda/issues/2433): rebindLocalRewriteRules re-adds global rewrite rules
- [#2434](https://github.com/agda/agda/issues/2434): Exact split analysis is too strict when matching on eta record constructor
- [#2441](https://github.com/agda/agda/issues/2441): Incorrect alignement in latex using the new ACM format
- [#2444](https://github.com/agda/agda/issues/2444): Generalising compiler pragmas
- [#2445](https://github.com/agda/agda/issues/2445): The LaTeX backend is slow
- [#2447](https://github.com/agda/agda/issues/2447): Cache loaded interfaces even if a type error is encountered
- [#2449](https://github.com/agda/agda/issues/2449): Agda depends on additional C library icu
- [#2451](https://github.com/agda/agda/issues/2451): Agda panics when attempting to rewrite a typeclass Eq
- [#2456](https://github.com/agda/agda/issues/2456): Internal error when postulating instance
- [#2458](https://github.com/agda/agda/issues/2458): Regression: Agda-2.5.3 loops where Agda-2.5.2 passes
- [#2462](https://github.com/agda/agda/issues/2462): Overloaded postfix projection does not resolve
- [#2464](https://github.com/agda/agda/issues/2464): Eta contraction for irrelevant functions breaks subject reduction
- [#2466](https://github.com/agda/agda/issues/2466): Case split to make hidden variable visible does not work
- [#2467](https://github.com/agda/agda/issues/2467): REWRITE without BUILTIN REWRITE crashes
- [#2469](https://github.com/agda/agda/issues/2469): "Partial" pattern match causes segfault at runtime
- [#2472](https://github.com/agda/agda/issues/2472): Regression related to the auto command
- [#2477](https://github.com/agda/agda/issues/2477): Sized data type analysis brittle, does not reduce size
- [#2478](https://github.com/agda/agda/issues/2478): Multiply defined labels on the user manual (pdf)
- [#2479](https://github.com/agda/agda/issues/2479): "Occurs check" error in generated Haskell code
- [#2480](https://github.com/agda/agda/issues/2480): Agda accepts incorrect (?) code, subject reduction broken
- [#2482](https://github.com/agda/agda/issues/2482): Wrong counting of data parameters with new-style mutual blocks
- [#2483](https://github.com/agda/agda/issues/2483): Files are sometimes truncated to a size of 201 bytes
- [#2486](https://github.com/agda/agda/issues/2486): Imports via FOREIGN are not transitively inherited anymore
- [#2488](https://github.com/agda/agda/issues/2488): Instance search inhibits holes for instance fields
- [#2493](https://github.com/agda/agda/issues/2493): Regression: Agda seems to loop when expression is given
- [#2494](https://github.com/agda/agda/issues/2494): Instance fields sometimes have incorrect goal types
- [#2495](https://github.com/agda/agda/issues/2495): Regression: termination checker of Agda-2.5.3 seemingly loops where Agda-2.5.2 passes
- [#2500](https://github.com/agda/agda/issues/2500): Adding fields to a record can cause Agda to reject previous definitions
- [#2510](https://github.com/agda/agda/issues/2510): Wrong error with --no-pattern-matching
- [#2517](https://github.com/agda/agda/issues/2517): "Not a variable error"
- [#2518](https://github.com/agda/agda/issues/2518): CopatternReductions in TreeLess
- [#2523](https://github.com/agda/agda/issues/2523): The documentation of `--without-K` is outdated
- [#2529](https://github.com/agda/agda/issues/2529): Unable to install Agda on Windows.
- [#2537](https://github.com/agda/agda/issues/2537): case splitting with 'with' creates {_} instead of replicating the arguments it found.
- [#2538](https://github.com/agda/agda/issues/2538): Internal error when parsing as-pattern
- [#2543](https://github.com/agda/agda/issues/2543): Case splitting with ellipsis produces spurious parentheses
- [#2545](https://github.com/agda/agda/issues/2545): Race condition in api tests
- [#2549](https://github.com/agda/agda/issues/2549): Rewrite rule for higher path constructor does not fire
- [#2550](https://github.com/agda/agda/issues/2550): Internal error in Agda.TypeChecking.Substitute
- [#2552](https://github.com/agda/agda/issues/2552): Let bindings in module telescopes crash Agda.Interaction.BasicOps
- [#2553](https://github.com/agda/agda/issues/2553): Internal error in Agda.TypeChecking.CheckInternal
- [#2554](https://github.com/agda/agda/issues/2554): More flexible size-assignment in successor style
- [#2555](https://github.com/agda/agda/issues/2555): Why does the positivity checker care about non-recursive occurrences?
- [#2558](https://github.com/agda/agda/issues/2558): Internal error in Warshall Solver
- [#2560](https://github.com/agda/agda/issues/2560): Internal Error in Reduce.Fast
- [#2564](https://github.com/agda/agda/issues/2564): Non-exact-split highlighting makes other highlighting disappear
- [#2568](https://github.com/agda/agda/issues/2568): agda2-infer-type-maybe-toplevel (in hole) does not respect "single-solution" requirement of instance resolution
- [#2571](https://github.com/agda/agda/issues/2571): Record pattern translation does not eta contract
- [#2573](https://github.com/agda/agda/issues/2573): Rewrite rules fail depending on unrelated changes
- [#2574](https://github.com/agda/agda/issues/2574): No link attached to module without toplevel name
- [#2575](https://github.com/agda/agda/issues/2575): Internal error, related to caching
- [#2577](https://github.com/agda/agda/issues/2577): deBruijn fail for higher order instance problem
- [#2578](https://github.com/agda/agda/issues/2578): Catch-all clause face used incorrectly for parent with pattern
- [#2579](https://github.com/agda/agda/issues/2579): Import statements with module instantiation should not trigger an error message
- [#2580](https://github.com/agda/agda/issues/2580): Implicit absurd match is NonVariant, explicit not
- [#2583](https://github.com/agda/agda/issues/2583): Wrong de Bruijn index introduced by absurd pattern
- [#2584](https://github.com/agda/agda/issues/2584): Duplicate warning printing
- [#2585](https://github.com/agda/agda/issues/2585): Definition by copatterns not modulo eta
- [#2586](https://github.com/agda/agda/issues/2586): "λ where" with single absurd clause not parsed
- [#2588](https://github.com/agda/agda/issues/2588): `agda --latex` produces invalid LaTeX when there are block comments
- [#2592](https://github.com/agda/agda/issues/2592): Internal Error in Agda/TypeChecking/Serialise/Instances/Common.hs
- [#2597](https://github.com/agda/agda/issues/2597): Inline record definitions confuse the reflection API
- [#2602](https://github.com/agda/agda/issues/2602): Debug output messes up AgdaInfo buffer
- [#2603](https://github.com/agda/agda/issues/2603): Internal error in MetaVars.hs
- [#2604](https://github.com/agda/agda/issues/2604): Use QNames as anchors in generated HTML
- [#2605](https://github.com/agda/agda/issues/2605): HTML backend generates anchors for whitespace
- [#2606](https://github.com/agda/agda/issues/2606): Check that LHS of a rewrite rule doesn't reduce is too strict
- [#2612](https://github.com/agda/agda/issues/2612): `exact-split` documentation is outdated and incomplete
- [#2613](https://github.com/agda/agda/issues/2613): Parametrised modules, with-abstraction and termination
- [#2620](https://github.com/agda/agda/issues/2620): Internal error in auto.
- [#2621](https://github.com/agda/agda/issues/2621): Case splitting instantiates meta
- [#2626](https://github.com/agda/agda/issues/2626): triggered internal error with sized types in MetaVars module
- [#2629](https://github.com/agda/agda/issues/2629): Exact splitting should not complain about absurd clauses
- [#2631](https://github.com/agda/agda/issues/2631): docs for auto aren't clear on how to use flags/options
- [#2632](https://github.com/agda/agda/issues/2632): some flags to auto dont seem to work in current agda 2.5.2
- [#2637](https://github.com/agda/agda/issues/2637): Internal error in Agda.TypeChecking.Pretty, possibly related to sized types
- [#2639](https://github.com/agda/agda/issues/2639): Performance regression, possibly related to the size solver
- [#2641](https://github.com/agda/agda/issues/2641): Required instance of FromNat when compiling imported files
- [#2642](https://github.com/agda/agda/issues/2642): Records with duplicate fields
- [#2644](https://github.com/agda/agda/issues/2644): Wrong substitution in expandRecordVar
- [#2645](https://github.com/agda/agda/issues/2645): Agda accepts postulated fields in a record
- [#2646](https://github.com/agda/agda/issues/2646): Only warn if fixities for undefined symbols are given
- [#2649](https://github.com/agda/agda/issues/2649): Empty list of "previous definition" in duplicate definition error
- [#2652](https://github.com/agda/agda/issues/2652): Added a new variant of the colon to the Agda input method
- [#2653](https://github.com/agda/agda/issues/2653): agda-mode: "cannot refine" inside instance argument even though term to be refined typechecks there
- [#2654](https://github.com/agda/agda/issues/2654): Internal error on result splitting without --postfix-projections
- [#2664](https://github.com/agda/agda/issues/2664): Segmentation fault with compiled programs using mutual record
- [#2665](https://github.com/agda/agda/issues/2665): Documentation: Record update syntax in wrong location
- [#2666](https://github.com/agda/agda/issues/2666): Internal error at Agda/Syntax/Abstract/Name.hs:113
- [#2667](https://github.com/agda/agda/issues/2667): Panic error on unbound variable.
- [#2669](https://github.com/agda/agda/issues/2669): Interaction: incorrect field variable name generation
- [#2671](https://github.com/agda/agda/issues/2671): Feature request: nullary pattern matching lambdas
- [#2679](https://github.com/agda/agda/issues/2679): Internal error at "Typechecking/Abstract.hs:133" and "TypeChecking/Telescope.hs:68"
- [#2682](https://github.com/agda/agda/issues/2682): What are the rules for projections of abstract records?
- [#2684](https://github.com/agda/agda/issues/2684): Bad error message for abstract constructor
- [#2686](https://github.com/agda/agda/issues/2686): Abstract constructors should be ignored when resolving overloading
- [#2690](https://github.com/agda/agda/issues/2690): [regression?] Agda engages in deep search instead of immediately failing
- [#2700](https://github.com/agda/agda/issues/2700): Add a command to check against goal type (and normalise)
- [#2703](https://github.com/agda/agda/issues/2703): Regression: Internal error for underapplied indexed constructor
- [#2705](https://github.com/agda/agda/issues/2705): The GHC backend might diverge in infinite file creation
- [#2708](https://github.com/agda/agda/issues/2708): Why is the `name` field in .agda-lib files mandatory?
- [#2710](https://github.com/agda/agda/issues/2710): Type checker hangs
- [#2712](https://github.com/agda/agda/issues/2712): Compiler Pragma for headers
- [#2714](https://github.com/agda/agda/issues/2714): Option --no-main should be allowed as file-local option
- [#2717](https://github.com/agda/agda/issues/2717): internal error at DisplayForm.hs:197
- [#2718](https://github.com/agda/agda/issues/2718): Interactive 'give' doesn't insert enough parenthesis
- [#2721](https://github.com/agda/agda/issues/2721): Without-K doesn't prevent heterogeneous conflict between literals
- [#2723](https://github.com/agda/agda/issues/2723): Unreachable clauses in definition by copattern matching trip clause compiler
- [#2725](https://github.com/agda/agda/issues/2725): File names for generated HTML files
- [#2726](https://github.com/agda/agda/issues/2726): Old regression related to with
- [#2727](https://github.com/agda/agda/issues/2727): Internal errors related to rewrite
- [#2729](https://github.com/agda/agda/issues/2729): Regression: case splitting uses variable name variants instead of the unused original names
- [#2730](https://github.com/agda/agda/issues/2730): Command to give in spite of termination errors
- [#2731](https://github.com/agda/agda/issues/2731): Agda fails to build with happy 1.19.6
- [#2733](https://github.com/agda/agda/issues/2733): Avoid some uses of \AgdaIndent?
- [#2734](https://github.com/agda/agda/issues/2734): Make height of empty lines configurable
- [#2736](https://github.com/agda/agda/issues/2736): Segfault using Alex 3.2.2 and cpphs
- [#2740](https://github.com/agda/agda/issues/2740): Indenting every line of code should be a no-op