Agda-2.6.2: doc/release-notes/2.6.1.md
Release notes for Agda version 2.6.1
====================================
General
-------
* Agda now has an official logo: [](https://github.com/agda/agda/blob/master/doc/user-manual/agda.svg). The
logo was chosen by the Agda community from a list of candidates. The
winning design was submitted by Miëtek Bak. The list of candidates
and the outcome of the poll can be consulted
[here](https://civs.cs.cornell.edu/cgi-bin/results.pl?id=E_ce6fe5e2a518ac98).
Installation and infrastructure
-------------------------------
* Added support for GHC 8.8.2
[Issue [#4285](https://github.com/agda/agda/issues/4285)].
* Removed support for GHC 7.10.3.
* Interface files are now written in directory `_build/VERSION/agda/` at
the project root (the closest enclosing directory where an `.agda-lib`
file is present). If there is no project root then the interface file
is written alongside the module it corresponds to.
The flag `--local-interfaces` forces Agda to revert back to storing
interface files alongside module files no matter what.
* Agda now uses the default RTS options `-M3.5G -I0`. If
you run Agda on a 32-bit system or a system with less than 8GB of
RAM, it is recommended to set the RTS options explicitly to a lower
value by running `agda` with option `+RTS -M1.2G -RTS`
(for example) or by setting the GHCRTS enviroment variable. See the
[GHC User's Guide](https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/runtime_control.html#setting-rts-options)
for more information.
* If Agda is compiled using GHC 8.4 or later, then one can expect to
see substantially lower memory consumption
[Issues [#4457](https://github.com/agda/agda/issues/4457)
and [#4316](https://github.com/agda/agda/issues/4316)].
This is due to the use of ["compact
regions"](https://hackage.haskell.org/package/ghc-compact-0.1.0.0/docs/GHC-Compact.html).
* The `CHANGELOG.md` was split. Changes to previous versions of Agda
are in the directory `doc/release-notes`.
Pragmas and options
-------------------
* New pragma `WARNING_ON_IMPORT` to let module authors raise a warning
when a module is imported. This can be use to tell users deprecations.
* New option `--confluence-check` (off by default) enables confluence
checking of user-defined rewrite rules (this only has an effect when
`--rewriting` is also enabled).
* New option `--no-projection-like` to turn off the analysis whether a
type signature likens that of a projection.
Projection-likeness is an optimization that reduces the size of
terms by dropping parameter-like reconstructible function arguments.
Thus, it is advisable to leave this optimization on, the flag is
meant for debugging Agda.
* Option `--no-forcing` is now a pragma option, i.e., the forcing analysis
can be switched off on a per-file basis via
```agda
{-# OPTIONS --no-forcing #-}
```
at the beginning of the file
[Issue [#3872](https://github.com/agda/agda/issues/3872)].
* New pragma option `--no-flat-split` disables pattern matching on `@♭` arguments.
* New pragma option `--allow-incomplete-matches`. It is similar to
`--allow-unsolved-metas`: modules containing partial function definitions
can be imported. Its local equivalent is the `NON_COVERING` pragma to
be placed before the function (or the block of mutually defined functions)
which the user knows to be partial.
* Option `--interaction-json` now brings more information about goals,
unsolved metas, warnings, errors.
It also displays pretty-printed terms.
* New pragma option `--keep-pattern-variables` to prevent case
splitting from replacing variables with dot patterns.
* Pragma `{-# ETA <record name> #-}` is no longer considered `--safe`.
See [Issue [#4450](https://github.com/agda/agda/issues/4450)].
* New pragma options `--subtyping` and `--no-subtyping` (default) to
turn on/off subtyping rules globally [see
Issue_[#4474](https://github.com/agda/agda/issues/4474)]. Currently,
this includes subtyping for irrelevance, erasure, and flat
modalities. Additionally, `--subtyping` is implied by
`--cumulativity` (see below). `--subtyping` is currently NOT implied
by `--sized-types`, and subtyping for sized types is used even when
`--subtyping` is not enabled.
* New profiling options to measure time spent per module or top-level
definition.
- `-v profile.modules:10` prints a breakdown per top-level module
- `-v profile.definitions:10` prints a breakdown per top-level
definition
Language
--------
### Syntax
* Fractional precedence levels are now supported, see
Issue [#3991](https://github.com/agda/agda/issues/3991). Example:
```agda
infix 3.14 _<_
```
Note that this includes a respective change in the reflected Agda syntax.
* Fixities can now be changed during import in a `renaming` directive,
see
Issue [#1346](https://github.com/agda/agda/issues/1346). Example:
```agda
open M using (_∙_)
open M renaming (_∙_ to infixl 10 _*_)
```
After this, `_∙_` is in scope with its original fixity, and as `_*_` as left
associative operator of precedence 10.
* Implicit non-dependent function spaces `{A} → B` and `{{A}} → B` are now supported.
* Idiom brackets
Idiom brackets can accommodate none or multiple applications separated by a vertical bar `|`
if there are two additional operations
```agda
empty : ∀ {A} → F A
_<|>_ : ∀ {A} → F A → F A → F A
```
i.e. an Alternative type class in Haskell.
As usual, the new idiom brackets desugar before scope checking.
Idiom brackets with multiple applications
```agda
(| e₁ a₁ .. aₙ | e₂ a₁ .. aₘ | .. | eₖ a₁ .. aₗ |)
```
expand to (assuming right associative `_<|>_`)
```agda
(pure e₁ <*> a₁ <*> .. <*> aₙ) <|> ((pure e₂ <*> a₁ <*> .. <*> aₘ) <|> (pure eₖ <*> a₁ <*> .. <*> aₗ))
```
Idiom brackets with no application `(|)` or `⦇⦈` are equivalent to `empty`.
* Irrefutable With
Users can now match on irrefutable patterns on the LHS using a
pattern-matching `with`. An expression of the form:
```agda
f xs with p1 <- e1 | ... | pn <- en
with q1 <- f1 | ... | qm <- fm = rhs
```
is translated to nested `with` clauses, essentially equivalent to:
```agda
f xs with e1 | ... | en
... | p1 | ... | pn
with f1 | ... | fm
... | q1 | ... | qm = rhs
```
* Record patterns in telescopes
Users can now use record patterns in telescope and lambda abstractions.
The type of the second projection from a dependent pair is the prototypical
example It can be defined as follows:
```agda
snd : ((a , _) : Σ A B) → B a
```
And this second projection can be implemented with a lamba-abstraction using
one of these irrefutable patterns:
```agda
snd = λ (a , b) → b
```
Using an as-pattern, users can get a name for the value as well as for its
subparts. We can for instance prove that any pair is equal to the pairing
of its first and second projections:
```agda
eta : (p@(a , b) : Σ A B) → p ≡ (a , b)
eta p = refl
```
* Absurd match in a do block
The last expression in a do block can now also be an absurd match `() <- f`.
* Named `where` modules are now in scope in the rhs of the clause (see
Issue [#4050](https://github.com/agda/agda/issues/4050)). Example:
```agda
record Wrap : Set₂ where
field wrapped : Set₁
test : Wrap
test = record { M }
module M where
wrapped : Set₁
wrapped = Set
```
* `{{-` is now lexed as `{ {-` rather than `{{ -`,
see Issue [#3962](https://github.com/agda/agda/issues/3962).
* Syntax for large numbers: you can now separate groups of 3 digits using `_`.
e.g. write `1_000_000` instead of `1000000`.
* `quoteGoal` and `quoteContext` are no longer keywords.
* Record constructors can no longer be qualified by the record module.
(See Issue [#4189](https://github.com/agda/agda/issues/4189).)
```agda
record Foo : Set where
constructor foo
works = foo
fails = Foo.foo
```
* `codata` definitions have been removed from the concrete syntax
Previously they got accepted syntactically, but resulted in errors.
* Imports can now be anonymous.
(See Issue_[#3727](https://github.com/agda/agda/issues/3727).)
For example, the following will **not** bring `Agda.Builtin.Unit` into scope:
```agda
open import Agda.Builtin.Unit as _
blah :: ⊤
blah = tt
```
### Type checking
* Type inference for record expressions no longer considers record types from
modules that have not been imported (Issue [#4267](https://github.com/agda/agda/issues/4267)).
For instance,
```agda
-- A.agda
module A where
record R : Set₁ where
field f : Set
```
```agda
-- B.agda
module B where
import A
```
```agda
-- C.agda
module C where
import B
fails : Set → _
fails X = record {f = X} -- import A required to infer record type R
```
* The fix of issue [#3903](https://github.com/agda/agda/issues/3903) changes
the algorithm computing the order of case splits, which in some cases may
lead to unsolved metavariables in previously working code. See issue
[#4353](https://github.com/agda/agda/issues/4353).
### Modalities
* New Flat Modality
New modality `@♭/@flat` (previously only available in the branch "flat").
An idempotent comonadic modality modeled after spatial/crisp type theory.
See [Flat Modality](https://agda.readthedocs.io/en/v2.6.1/language/flat.html)
in the documentation for more.
* New run-time erasure modality (`@0` / `@erased`).
Terms marked as erased cannot influence computations and are erased
at run time
[Issue [#3855](https://github.com/agda/agda/issues/3855)]. See
[Run-time
Irrelevance](https://agda.readthedocs.io/en/v2.6.1/language/runtime-irrelevance.html)
in the documentation for more information.
Note that this feature can cause previously solved metavariables to become
unsolved even in code that doesn't use run-time erasure (see issue
[#4174](https://github.com/agda/agda/issues/4174)).
* Subtyping rules for modalities are by default no longer used (see
Issue_[#4390](https://github.com/agda/agda/issues/4390)). For
example, if `f : .A → A`, Agda no longer accepts `f` at type `A →
A`. Instead, Agda accepts `λ x → f x : A → A`. The same holds for
erasure (`@0`) and flat (`@♭`) modalities. Consequently, it may be
required to eta-expand certain functions in order to make old code
work with Agda 2.6.1. Alternatively, enabling the new `--subtyping`
flag will restore the old behaviour but might negatively impact
typechecking performance.
### Universe levels
* New (experimental) option `--cumulativity`
When the ``--cumulativity`` flag is enabled, Agda uses the subtyping
rule ``Set i =< Set j`` whenever ``i =< j``. For example, in
addition to its usual type ``Set``, ``Nat`` also has the type
``Set₁`` and even ``Set i`` for any ``i : Level``. More information
about this new option can be found in section
[Cumulativity](https://agda.readthedocs.io/en/v2.6.1/language/cumulativity.html)
of the user manual.
### Termination checking
* The "with inlining" feature of the termination checker has been
removed. As a consequence, some functions defined using `with` are
no longer accepted as terminating. See
Issue [#59](https://github.com/agda/agda/issues/59) for why this
feature was originally introduced and
[#3604](https://github.com/agda/agda/issues/3604) for why it had to
be removed.
The easiest way to fix termination problems caused by `with` is to abstract
over the offending recursive call before any other `with`s. For example
```agda
data D : Set where
[_] : Nat → D
fails : D → Nat
fails [ zero ] = zero
fails [ suc n ] with some-stuff
... | _ = fails [ n ]
```
This fails termination because the relation between `[ suc n ]` and `[ n ]`
is lost since the generated with-function only gets passed `n`. To fix it we
can abstract over the recursive call:
```agda
fixed : D → Nat
fixed [ zero ] = zero
fixed [ suc n ] with fixed [ n ] | some-stuff
... | rec | _ = rec
```
If the function takes more arguments you might need to abstract over a
partial application to just the structurally recursive argument. For instance,
```agda
fails : Nat → D → Nat
fails _ [ zero ] = zero
fails _ [ suc n ] with some-stuff
... | m = fails m [ n ]
fixed : Nat → D → Nat
fixed _ [ zero ] = zero
fixed _ [ suc n ] with (λ m → fixed m [ n ]) | some-stuff
... | rec | m = rec m
```
A possible complication is that later `with`-abstractions might change the
type of the abstracted recursive call:
```agda
T : D → Set
suc-T : ∀ {n} → T [ n ] → T [ suc n ]
zero-T : T [ zero ]
fails : (d : D) → T d
fails [ zero ] = zero-T
fails [ suc n ] with some-stuff
... | _ with [ n ]
... | z = suc-T (fails [ n ])
still-fails : (d : D) → T d
still-fails [ zero ] = zero-T
still-fails [ suc n ] with still-fails [ n ] | some-stuff
... | rec | _ with [ n ]
... | z = suc-T rec -- Type error because rec : T z
```
To solve this problem you can add `rec` to the with-abstraction messing up
its type. This will prevent it from having its type changed:
```agda
fixed : (d : D) → T d
fixed [ zero ] = zero-T
fixed [ suc n ] with fixed [ n ] | some-stuff
... | rec | _ with rec | [ n ]
... | _ | z = suc-T rec
```
* The termination checker will now try to dispose of recursive calls
by reducing with the non-recursive function clauses.
This eliminates false positives common for definitions by copatterns
using dependent types,
see Issue [#906](https://github.com/agda/agda/issues/906).
For example, consider the following example using a dependent
coinductive record `Tree`:
```agda
data Fin : Nat → Set where
fzero : ∀ n → Fin (suc n)
fsuc : ∀ n (i : Fin n) → Fin (suc n)
toNat : ∀ n → Fin n → Nat
toNat .(suc n) (fzero n) = zero
toNat .(suc n) (fsuc n i) = suc (toNat n i)
record Tree : Set where
coinductive
field label : Nat
child : Fin label → Tree
open Tree
tree : Nat → Tree
tree n .label = n
tree n .child i = tree (n + toNat _ i)
```
Agda solves the underscore by `tree n .label`, which is a corecursive
call in a non-guarded position, violating the guardedness criterion.
This lead to a complaint of the termination checker.
Now this call is reduced to `n` first using the non-recursive clause
`tree n .label = n`, which leaves us only with the guarded call
`tree (n + toNat n i)`, and the termination checker is happy.
Note: Similar false positives arose already for non-recursive dependent
records, e.g., when trying to define an inhabitant of the Σ-type by
copattern matching on the projects.
See Issue_[#2068](https://github.com/agda/agda/issues/2068) for a
non-recursive example.
### Irrelevance and Prop
* Agda will no longer reduce irrelevant definitions and definitions
with a type in `Prop`. This does not have an effect on the
semantics, but should lead to improved performance (see Issues
[#4115](https://github.com/agda/agda/issues/4115),
[#4118](https://github.com/agda/agda/issues/4118),
[#4120](https://github.com/agda/agda/issues/4120),
[#4122](https://github.com/agda/agda/issues/4122)).
* Terms of a type in `Prop` are now printed as `_`. To show the actual
term, you can use the `--show-irrelevant` flag (see
Issue [#3337](https://github.com/agda/agda/issues/3337).
### Rewrite rules
* Rewrite rules (option `--rewriting`) with data or record types as
the head symbol are no longer allowed (see
Issue [#3846](https://github.com/agda/agda/issues/3846)).
### Tactics & Reflection
* Implicit arguments solved by user-defined tactics
You can declare tactics to be used to solve a particular implicit argument
using the following syntax:
```agda
example : {@(tactic f) x : A} → B
```
where `f : Term → TC ⊤`. At calls to `example`, `f` is called on the
metavariable inserted for `x`. `f` can be an arbitrary term and may depend on
previous arguments to the function. For instance,
```agda
example₂ : (depth : Nat) {@(tactic search depth) x : A} → B
```
Record fields can also be annotated with a tactic, allowing them to be
omitted in constructor applications, record constructions and co-pattern
matches:
```agda
record Example : Set where
constructor mkExample
field x : A
@(tactic solveP x) {y} : P x
```
where `solveP : (x : A) → Term → TC ⊤` is a tactic that tries to
prove `P x`
[Issue [#4124](https://github.com/agda/agda/issues/4124)].
* The legacy reflection framework using `quoteGoal` and `quoteContext` has been
removed.
### Builtins
* New primitives
```agda
primWord64ToNatInjective : ∀ a b → primWord64ToNat a ≡ primWord64ToNat b → a ≡ b
primFloatToWord64 : Float → Word64
primFloatToWord64Injective : ∀ a b → primFloatToWord64 a ≡ primFloatToWord64 b → a ≡ b
primMetaToNat : Meta → Nat
primMetaToNatInjective : ∀ a b → primMetaToNat a ≡ primMetaToNat b → a ≡ b
primQNameToWord64s : Name → Word64 × Word64
primQNameToWord64sInjective : ∀ a b → primQNameToWord64s a ≡ primQNameToWord64s b → a ≡ b
```
These can be used to define safe decidable propositional equality, see Issue [agda-stdlib#698](https://github.com/agda/agda-stdlib/issues/698).
* New Primitive for showing Natural numbers:
```agda
primShowNat : Nat → String
```
placed in Agda.Builtin.String.
* The builtin `IO` has been declared strictly positive in both its
level and type argument.
### Warnings
* New warning for a variable shadowing another in a telescope. If the two
variables are introduced in different telescopes then the warning is not
raised.
```agda
f : {a : Level} {A : Set a} (a : A) → A -- warning raised: repeated a
g : {a : Level} {A : Set a} → (a : A) → A -- warning not raised: two distinct telescopes
```
Note that this warning is turned off by default (you can use
`-WShadowingInTelescope` or `--warning ShadowingInTelescope` to turn
it on, `-Wall` would also naturally work).
Emacs mode
----------
* Agda input method: new key bindings `\ G h` and `\ G H` for `η` and
`H` (capital η)
[Issue [#3856](https://github.com/agda/agda/issues/3856)].
* Syntax highlighting: in literate modes, the pure texts
(other than Agda code and the code-text separators) are no longer highlighted
(it was highlighted as comments before).
This somehow provides more information about how Agda lexes literate files.
* Agda now also displays the values of let-bound variables in the
context instead of just their types
[Issue [#4199](https://github.com/agda/agda/issues/4199)].
* Agda will now try to preserve the ellipsis (`...`) during case
splitting when possible. To manually expand the ellipsis, you may
ask Agda to case split on the special identifier `.`.
[Issue [#2589](https://github.com/agda/agda/issues/2589)]
* Agda will now also show variables named `_` in the context if they
are instance arguments (see
[#4307](https://github.com/agda/agda/issues/4307)). Instance
arguments are now also marked as `(instance)` in the context. Example:
```agda
f : {{_ : A}} → A
f = ?
```
Agda will now display the goal as follows:
```
Goal: A
————————————————————————————————————————————————————————————
_ : A (instance)
```
* It is now possible to ask Agda to terminate itself after any
previously invoked commands have completed, by giving a prefix
argument to `agda2-term`.
* The command `agda2-measure-load-time` has been removed.
GHC Backend
-----------
* Types which have a COMPILE GHC pragma are no longer erased
[Issue [#3732](https://github.com/agda/agda/issues/3732)].
```agda
data I : Set where
bar : I
{-# FOREIGN GHC data I = Bar #-}
{-# COMPILE GHC I = data I (Bar) #-}
data S : Set where
foo : I → S
{-# FOREIGN GHC data S = Foo I #-}
{-# COMPILE GHC S = data S (Foo) #-}
```
Previously [Issue [#2921](https://github.com/agda/agda/issues/2921)],
the last binding was incorrect, since the argument of
singleton type `I` was erased from the constructor `foo` during
compilation. The required shape of `S` was previously
```
{-# FOREIGN GHC data S = Foo #-}
```
i.e., constructor `Foo` had to have no arguments.
For the sake of transparency, Haskell constructors bound to
Agda constructors now take the same arguments.
This is especially important if Haskell bindings are to be
produced automatically by third party tool.
LaTeX backend
-------------
* Now the code environment complains if it is given unrecognised options.
It is also possible to write, say, `hide=true` instead of `hide`,
and `hide=false` means that the `hide` option should not be used.
Furthermore the same option can be given multiple times, in which
case later choices take precedence over earlier ones.
* The code environment has a new option, `number`.
When the option `number` is used an equation number is generated for
the code listing. The number is set to the right, centered
vertically. By default the number is set in parentheses, but this
can be changed by redefining `\AgdaFormatCodeNumber`.
The option can optionally be given an argument: when `number=l` is
used a label `l`, referring to the code listing, is generated. It is
possible to use this option several times with different labels.
The option has no effect if used together with `hide`, `inline` or
`inline*`.
API
----
* Removed module `Agda.Utils.HashMap`. It only re-exported `Data.HashMap.Strict`
from the package `unordered-containers`. Use `Data.HashMap.Strict` instead.
* Removed module `Agda.Utils.Char`. It used to provide functions converting a
`Char` in base 8, 10, and 16 to the corresponding `Int`. Use `digitToInt` in
`Data.Char` instead. The rest of module was about Unicode test which was not
used.
* `Agda.Utils.List` no longer provides `headMaybe`.
Use `listToMaybe` in `Data.Maybe` instead.
* `Agda.Utils.Either` no longer provides `mapEither`. Use `bimap` in
`Data.Bifunctor` instead.
* `Agda.Utils.Map` no longer provides `unionWithM`, `insertWithKeyM`,
`allWithKey`, `unzip`, and `unzip3`.
Other issues
------------
For 2.6.1, the following issues were also closed (see [bug
tracker](https://github.com/agda/agda/issues)):
- [#470](https://github.com/agda/agda/issues/470): Constraint solving in heterogenous situations
- [#471](https://github.com/agda/agda/issues/471): Emacs command to show goal with constraints on it
- [#500](https://github.com/agda/agda/issues/500): Allow creation of implicit parameters in with blocks
- [#543](https://github.com/agda/agda/issues/543): Irrelevant projections are inconsistent
- [#760](https://github.com/agda/agda/issues/760): Warning for open public in an abstract block
- [#1073](https://github.com/agda/agda/issues/1073): Solve C-c C-s inserts variables that are not in scope
- [#1097](https://github.com/agda/agda/issues/1097): Allow record patterns in lambda-bound positions
- [#1182](https://github.com/agda/agda/issues/1182): Request: allowing the use of patterns in syntax-bound variables
- [#1381](https://github.com/agda/agda/issues/1381): Termination checker rejects function with with-clause
- [#1445](https://github.com/agda/agda/issues/1445): Lack of subject reduction with REWRITE
- [#1820](https://github.com/agda/agda/issues/1820): Case splitting should preserve existing names
- [#2068](https://github.com/agda/agda/issues/2068): Copattern matching: Hyvernat termination would succeed
- [#2148](https://github.com/agda/agda/issues/2148): Option to use use `stack exec` for GHC backend
- [#2170](https://github.com/agda/agda/issues/2170): Two equal irrelevant definitions: one is type checked, the other is not
- [#2284](https://github.com/agda/agda/issues/2284): Disallow duplicate bound variable in lambda and pi
- [#2414](https://github.com/agda/agda/issues/2414): Case splitting loses as-patterns
- [#2498](https://github.com/agda/agda/issues/2498): Resolution of unnamed instances
- [#2512](https://github.com/agda/agda/issues/2512): Propose: Split the changelog
- [#2530](https://github.com/agda/agda/issues/2530): --ignore-interfaces should not recompile Primitive.agda
- [#2535](https://github.com/agda/agda/issues/2535): Expose name id in reflection API
- [#2589](https://github.com/agda/agda/issues/2589): Preserve the ellipsis (dots) when case splitting "with" arguments
- [#2610](https://github.com/agda/agda/issues/2610): Avoid rechecking by storing interfaces in separate directories?
- [#2619](https://github.com/agda/agda/issues/2619): Feature request: link to `renaming` clause
- [#2902](https://github.com/agda/agda/issues/2902): Case-splitting should not generate patterns containing pattern synonyms
- [#3034](https://github.com/agda/agda/issues/3034): Pattern matching without K seemingly illogical for the inductive family of squares
- [#3073](https://github.com/agda/agda/issues/3073): type-in-type and spurious levels
- [#3081](https://github.com/agda/agda/issues/3081): Termination problem: copatterns and without-K
- [#3089](https://github.com/agda/agda/issues/3089): Nicer syntax for implicit @-patterns
- [#3095](https://github.com/agda/agda/issues/3095): Would like to make hidden variable visible but it is created ambiguous
- [#3136](https://github.com/agda/agda/issues/3136): Spurious module parameters printed in extended lambda in termination error
- [#3189](https://github.com/agda/agda/issues/3189): No information about which warnings are enabled by default
- [#3233](https://github.com/agda/agda/issues/3233): Type declarations not accompanied by a definition should be highlighted in the emacs mode
- [#3238](https://github.com/agda/agda/issues/3238): Printing of inserted hidden lambdas
- [#3293](https://github.com/agda/agda/issues/3293): Absurd match in a do block
- [#3295](https://github.com/agda/agda/issues/3295): Allow import of files with incomplete pattern matching
- [#3353](https://github.com/agda/agda/issues/3353): Case splitting turns named arguments into positional arguments
- [#3383](https://github.com/agda/agda/issues/3383): Document the DISPLAY pragma
- [#3417](https://github.com/agda/agda/issues/3417): No highlighting for code that fails termination checking when an error is encountered
- [#3423](https://github.com/agda/agda/issues/3423): Implicit arguments with custom macro for resolution
- [#3432](https://github.com/agda/agda/issues/3432): Highlighting does not work for pattern synonyms in import lists
- [#3493](https://github.com/agda/agda/issues/3493): Impossible to normalize elements in a proposition
- [#3525](https://github.com/agda/agda/issues/3525): Rewrite rules with non-linear patterns do not work in presence of Prop
- [#3545](https://github.com/agda/agda/issues/3545): JavaScript backend: mapping a function that returns Set fails
- [#3574](https://github.com/agda/agda/issues/3574): Support precedent rebind / changing the precedents in builtin library
- [#3582](https://github.com/agda/agda/issues/3582): Error message referring to Set instead of Prop
- [#3594](https://github.com/agda/agda/issues/3594): Occurs check throws error when a solution is possible by eta expansion
- [#3599](https://github.com/agda/agda/issues/3599): Bad performance on pathToEquiv
- [#3606](https://github.com/agda/agda/issues/3606): Do not create/display superfluous metas and show constraints in a readable way
- [#3654](https://github.com/agda/agda/issues/3654): Show non-blocked constraints first in list of unsolved constraints
- [#3695](https://github.com/agda/agda/issues/3695): Generalisation introduces multiple explicit arguments for one generalisable variable
- [#3698](https://github.com/agda/agda/issues/3698): Remove primComp?
- [#3712](https://github.com/agda/agda/issues/3712): Sigma not listed in Built-ins documentation
- [#3724](https://github.com/agda/agda/issues/3724): Internal error with Prop and inductive-inductive type
- [#3725](https://github.com/agda/agda/issues/3725): Support GHC 8.8.1
- [#3730](https://github.com/agda/agda/issues/3730): Internal error resulting from unused implicit argument
- [#3735](https://github.com/agda/agda/issues/3735): Incorrect context when generalisable variable is used
- [#3736](https://github.com/agda/agda/issues/3736): Safe decidability equality support for Name and Meta
- [#3745](https://github.com/agda/agda/issues/3745): Update user manual on built-ins
- [#3749](https://github.com/agda/agda/issues/3749): Inconsistency: Rounding op differentiates NaNs
- [#3759](https://github.com/agda/agda/issues/3759): Change the default RTS options?
- [#3774](https://github.com/agda/agda/issues/3774): de Bruijn index out of scope with rewrite rules
- [#3776](https://github.com/agda/agda/issues/3776): Conversion check fails too quickly when type could be eta unit type
- [#3779](https://github.com/agda/agda/issues/3779): Incorrectly ordered generalised variables
- [#3785](https://github.com/agda/agda/issues/3785): Comparison of blocked terms doesn't respect eta
- [#3791](https://github.com/agda/agda/issues/3791): Asking Agda to solve a constraint inside a macro
- [#3803](https://github.com/agda/agda/issues/3803): Parse empty field lists
- [#3805](https://github.com/agda/agda/issues/3805): Agda prelude: Internal error at src/full/Agda/TypeChecking/Reduce/Fast.hs:1347
- [#3807](https://github.com/agda/agda/issues/3807): Internal error related to generalisable variables
- [#3812](https://github.com/agda/agda/issues/3812): Rewriting projected symbols leads to loss of subject reduction
- [#3813](https://github.com/agda/agda/issues/3813): Destructuring leads to invalid premises
- [#3818](https://github.com/agda/agda/issues/3818): For open import M, Agda should remember that M is an external module
- [#3824](https://github.com/agda/agda/issues/3824): rewrite drops named where module
- [#3825](https://github.com/agda/agda/issues/3825): record{M} syntax reports unsolved metas in module M instead of in record expression
- [#3828](https://github.com/agda/agda/issues/3828): Internal error in Agda/TypeChecking/Coverage.hs:467
- [#3829](https://github.com/agda/agda/issues/3829): Case-split: don't generate pattern covered by unreachable clause
- [#3830](https://github.com/agda/agda/issues/3830): primShow(Char/String) display spurious square brackets
- [#3831](https://github.com/agda/agda/issues/3831): Wrong de Bruijn indices for reflected variables inside an extended context
- [#3843](https://github.com/agda/agda/issues/3843): Internal error with-clause and unification
- [#3851](https://github.com/agda/agda/issues/3851): C-c C-h should default to AsIs rather than Simplified
- [#3866](https://github.com/agda/agda/issues/3866): `--no-unicode` option producing unicode variable names
- [#3878](https://github.com/agda/agda/issues/3878): Case splitting should respect existing input
- [#3879](https://github.com/agda/agda/issues/3879): Only unqualified pattern synonyms should be used for resugaring
- [#3882](https://github.com/agda/agda/issues/3882): de Bruijn index out of scope
- [#3892](https://github.com/agda/agda/issues/3892): Internal error with `data .. where` definitions
- [#3898](https://github.com/agda/agda/issues/3898): Forcing analysis sensitive to normalization
- [#3900](https://github.com/agda/agda/issues/3900): Abstract constructor not usable in function definition involving "with"
- [#3901](https://github.com/agda/agda/issues/3901): Unnamed implicit non-dependent function space {A} -> B and {{A}} -> B
- [#3912](https://github.com/agda/agda/issues/3912): Generalisable variables generate unknown and explicit parameters
- [#3919](https://github.com/agda/agda/issues/3919): Case splitting fails in parameterized module
- [#3927](https://github.com/agda/agda/issues/3927): `import … hiding …` should be documented
- [#3928](https://github.com/agda/agda/issues/3928): The error message `Hiding … has no effect` should be improved
- [#3930](https://github.com/agda/agda/issues/3930): BUILTIN NATURAL internal error at Forcing.hs:232
- [#3932](https://github.com/agda/agda/issues/3932): Internal error when mixing implicit and explicit mutual blocks
- [#3937](https://github.com/agda/agda/issues/3937): Internal error at "ConcreteToAbstract:1372"
- [#3940](https://github.com/agda/agda/issues/3940): Weird error with piSort and generalization
- [#3943](https://github.com/agda/agda/issues/3943): Print also hidden problematic unification terms
- [#3955](https://github.com/agda/agda/issues/3955): Document module keyword in using/hiding/renaming
- [#3956](https://github.com/agda/agda/issues/3956): Duplicate name in environment buffer with @-pattern
- [#3964](https://github.com/agda/agda/issues/3964): Agda overwrites user-written dotted pattern
- [#3965](https://github.com/agda/agda/issues/3965): Wrong indication of unreachable clauses
- [#3966](https://github.com/agda/agda/issues/3966): All clauses marked when one clause has unification error
- [#3972](https://github.com/agda/agda/issues/3972): Unreachable clause leads to internal error at Serialise/Instances/Internal.hs:94 (MetaV)
- [#3974](https://github.com/agda/agda/issues/3974): Range for unexpected implicit argument on lhs too big
- [#3983](https://github.com/agda/agda/issues/3983): TERMINATING accepted with --safe if hidden in a block
- [#3989](https://github.com/agda/agda/issues/3989): Warn about duplicate bindings in a single telescope
- [#4000](https://github.com/agda/agda/issues/4000): How to get Agda to ignore `~/.agda`?
- [#4006](https://github.com/agda/agda/issues/4006): Internal error related to abstract and variable
- [#4007](https://github.com/agda/agda/issues/4007): Cannot give pattern-matching lambda in abstract setting
- [#4010](https://github.com/agda/agda/issues/4010): unquoteDef fails in abstract block
- [#4012](https://github.com/agda/agda/issues/4012): Internal error when accessing abstract definitions created by unquoteDef/Decl
- [#4020](https://github.com/agda/agda/issues/4020): Rewriting incorrectly considers level variables under lambdas as unbound in the LHS
- [#4032](https://github.com/agda/agda/issues/4032): Loss of subject reduction involving --rewriting even when --confluence-check is on and everything passes the confluence checker
- [#4038](https://github.com/agda/agda/issues/4038): Rewriting sometimes fails to rewrite in the presence of unsolved metas
- [#4044](https://github.com/agda/agda/issues/4044): Equality checking uses too much memory in 2.6.0 (compared to 2.5.4)
- [#4046](https://github.com/agda/agda/issues/4046): Remove (deprecated) codata keyword
- [#4048](https://github.com/agda/agda/issues/4048): Rewriting rule fails to trigger
- [#4049](https://github.com/agda/agda/issues/4049): Internal error with sized types if the target type of a constructor is an alias
- [#4051](https://github.com/agda/agda/issues/4051): Internal error when importing a module with a hole in a type
- [#4053](https://github.com/agda/agda/issues/4053): Emacs-mode: Case split leaves part of old line behind
- [#4059](https://github.com/agda/agda/issues/4059): Two variants of irrefutable with?
- [#4066](https://github.com/agda/agda/issues/4066): Regression related to instance resolution
- [#4116](https://github.com/agda/agda/issues/4116): Internal error Forcing.hs:232
- [#4121](https://github.com/agda/agda/issues/4121): Pattern synonyms cannot be made private
- [#4125](https://github.com/agda/agda/issues/4125): Type checker normalizes too much
- [#4134](https://github.com/agda/agda/issues/4134): Internal error triggered by missing check for irrelevant meta dependencies
- [#4136](https://github.com/agda/agda/issues/4136): Overzealous pruning of metavariable with irrelevant argument
- [#4141](https://github.com/agda/agda/issues/4141): Printing of DontCare should not use dot syntax
- [#4142](https://github.com/agda/agda/issues/4142): defCopatternLHS needs to be set when record expression were translated to copatterns
- [#4148](https://github.com/agda/agda/issues/4148): Internal error related to records and type-level indices
- [#4152](https://github.com/agda/agda/issues/4152): Variables in Prop position should not raise hard error in occurs check
- [#4154](https://github.com/agda/agda/issues/4154): Renaming declarations within a module may cause name clash
- [#4158](https://github.com/agda/agda/issues/4158): Double check failure (unaware of rewrite rule)
- [#4163](https://github.com/agda/agda/issues/4163): pattern matching in parametrized module leads to ill-typed definitions in where modules.
- [#4170](https://github.com/agda/agda/issues/4170): Tactic causes Agda to enter into an infinite loop
- [#4179](https://github.com/agda/agda/issues/4179): Coverage check false positive
- [#4185](https://github.com/agda/agda/issues/4185): Agda uses η-equality for record types defined with no-eta-equality
- [#4205](https://github.com/agda/agda/issues/4205): Internal error in connection with with, copatterns, and open record
- [#4211](https://github.com/agda/agda/issues/4211): Cannot add as-pattern on literal pattern
- [#4214](https://github.com/agda/agda/issues/4214): `with` abstraction fails with HIT constructors in the goal
- [#4215](https://github.com/agda/agda/issues/4215): Case splitting should respect Nat literals
- [#4255](https://github.com/agda/agda/issues/4255): Hole filler accepted, but type check error on reload
- [#4261](https://github.com/agda/agda/issues/4261): Order of arguments affects lambda pattern matching
- [#4268](https://github.com/agda/agda/issues/4268): Give failure with large quantification
- [#4269](https://github.com/agda/agda/issues/4269): Universe levels are not solved
- [#4283](https://github.com/agda/agda/issues/4283): DeBruijn issue(?) in standard library tests
- [#4289](https://github.com/agda/agda/issues/4289): datatype scope and import guidelines
- [#4297](https://github.com/agda/agda/issues/4297): Missing documentation: NO_UNIVERSE_CHECK pragma
- [#4310](https://github.com/agda/agda/issues/4310): Anonymous .. binder should not lead to a parse error
- [#4314](https://github.com/agda/agda/issues/4314): Internal error with generalize
- [#4320](https://github.com/agda/agda/issues/4320): Path constructor overloading
- [#4323](https://github.com/agda/agda/issues/4323): Internal error (Rewriting.hs:395) with generalize and rewrite rules
- [#4330](https://github.com/agda/agda/issues/4330): Equations for cubical subtypes
- [#4348](https://github.com/agda/agda/issues/4348): Seemingly needless repetition of highlighting of warnings
- [#4360](https://github.com/agda/agda/issues/4360): Missing warning for declaring constructor instances for records with explicit fields
- [#4361](https://github.com/agda/agda/issues/4361): Inconsistent highlighting of BUILTING EQUALITY/REWRITE
- [#4371](https://github.com/agda/agda/issues/4371): Inconsistency with rewrite rules and assumptions in Prop
- [#4373](https://github.com/agda/agda/issues/4373): Non-imported instances are used for instance resolution
- [#4375](https://github.com/agda/agda/issues/4375): Internal error in Agda/TypeChecking/Monad/Context.hs:120
- [#4380](https://github.com/agda/agda/issues/4380): Parse error with instance constructor and end of file
- [#4382](https://github.com/agda/agda/issues/4382): Rewriting and records with eta
- [#4387](https://github.com/agda/agda/issues/4387): Less responsive Emacs mode in v2.6.1 release candidate 1
- [#4390](https://github.com/agda/agda/issues/4390): Unification finds solution with bound variable used at wrong modality
- [#4391](https://github.com/agda/agda/issues/4391): Termination checking failed with guardedness
- [#4399](https://github.com/agda/agda/issues/4399): Case split on unnamed argument produces non-sensical code
- [#4401](https://github.com/agda/agda/issues/4401): Missing check on context variables leads to Set:Set with --cumulativity
- [#4404](https://github.com/agda/agda/issues/4404): Disambiguation fails in Cubical Agda
- [#4410](https://github.com/agda/agda/issues/4410): Rewrite rule matching does not respect Prop
- [#4447](https://github.com/agda/agda/issues/4447): Positivity: internal error with projection in constructor type
- [#4451](https://github.com/agda/agda/issues/4451): Highlighting: use several lookups rather than merging hash-maps?
- [#4452](https://github.com/agda/agda/issues/4452): Compiler error when using REWRITE
- [#4469](https://github.com/agda/agda/issues/4469): The warning machinery does not work correctly when interface files are involved
The following previously closed issues were reopened:
- [#1556](https://github.com/agda/agda/issues/1556): Agda allows "very dependent" types