Release notes for Agda version 2.5.4
====================================
Installation and infrastructure
-------------------------------
* Added support for GHC 8.2.2 and GHC 8.4.3.
Note that GHC 8.4.* requires `cabal-install` ≥ 2.2.0.0.
* Removed support for GHC 7.8.4.
* Included user manual in PDF format in `doc/user-manual.pdf`.
Language
--------
* Call-by-need reduction.
Compile-time weak-head evaluation is now call-by-need, but each weak-head
reduction has a local heap, so sharing is not maintained between different
reductions.
The reduction machine has been rewritten from scratch and should be faster
than the old one in all cases, even those not exploiting laziness.
* Compile-time inlining.
Simple definitions (that don't do any pattern matching) marked as INLINE are
now also inlined at compile time, whereas before they were only inlined by
the compiler backends. Inlining only triggers in function bodies and not in
type signatures, to preserve goal types as far as possible.
* Automatic inlining.
Definitions satisfying the following criteria are now automatically inlined
(can be disabled using the new NOINLINE pragma):
- No pattern matching.
- Uses each argument at most once.
- Does not use all its arguments.
Automatic inlining can be turned off using the flag `--no-auto-inline`. This
can be useful when debugging tactics that may be affected by whether or not
a particular definition is being inlined.
### Syntax
* Do-notation.
There is now builtin do-notation syntax. This means that `do` is a reserved
keyword and cannot be used as an identifier.
Do-blocks support lets and pattern matching binds. If the pattern in a bind
is non-exhaustive the other patterns need to be handled in a `where`-clause
(see example below).
Example:
```agda
filter : {A : Set} → (A → Bool) → List A → List A
filter p xs = do
x ← xs
true ← return (p x)
where false → []
return x
```
Do-blocks desugar to `_>>=_` and `_>>_` before scope checking, so whatever
definitions of these two functions are in scope of the do-block will be used.
More precisely:
- Simple bind
```agda
do x ← m
m'
```
desugars to `m >>= λ x → m'`.
- Pattern bind
```agda
do p ← m where pᵢ → mᵢ
m'
```
desugars to `m >>= λ { p → m'; pᵢ → mᵢ }`, where `pᵢ → mᵢ` is an arbitrary
sequence of clauses and follows the usual layout rules for `where`. If `p`
is exhaustive the `where` clause can be omitted.
- Non-binding operation
```agda
do m
m'
```
desugars to `m >> m'`.
- Let
```agda
do let ds
m
```
desugars to `let ds in m`, where `ds` is an arbitrary sequence of valid let-declarations.
- The last statement in the do block must be a plain expression (no let or bind).
Bind statements can use either `←` or `<-`. Neither of these are reserved, so
code outside do-blocks can use identifiers with these names, but inside a
do-block they would need to be used qualified or under different names.
* Infix let declarations. [Issue [#917](https://github.com/agda/agda/issues/917)]
Let declarations can now be defined in infix (or mixfix) style. For instance:
```agda
f : Nat → Nat
f n = let _!_ : Nat → Nat → Nat
x ! y = 2 * x + y
in n ! n
```
* Overloaded pattern synonyms. [Issue [#2787](https://github.com/agda/agda/issues/2787)]
Pattern synonyms can now be overloaded if all candidates have the same
*shape*. Two pattern synonym definitions have the same shape if they are
equal up to variable and constructor names. Shapes are checked at resolution
time.
For instance, the following is accepted:
```agda
open import Agda.Builtin.Nat
data List (A : Set) : Set where
lnil : List A
lcons : A → List A → List A
data Vec (A : Set) : Nat → Set where
vnil : Vec A 0
vcons : ∀ {n} → A → Vec A n → Vec A (suc n)
pattern [] = lnil
pattern [] = vnil
pattern _∷_ x xs = lcons x xs
pattern _∷_ y ys = vcons y ys
lmap : ∀ {A B} → (A → B) → List A → List B
lmap f [] = []
lmap f (x ∷ xs) = f x ∷ lmap f xs
vmap : ∀ {A B n} → (A → B) → Vec A n → Vec B n
vmap f [] = []
vmap f (x ∷ xs) = f x ∷ vmap f xs
```
* If the file has no top-level module header, the first module
cannot have the same name as the file.
[Issues [#2808](https://github.com/agda/agda/issues/2808)
and [#1077](https://github.com/agda/agda/issues/1077)]
This means that the following file `File.agda` is rejected:
```agda
-- no module header
postulate A : Set
module File where -- inner module with the same name as the file
```
Agda reports `Illegal declarations(s) before top-level module`
at the `postulate`.
This is to avoid confusing scope errors in similar situations.
If a top-level module header is inserted manually, the file is accepted:
```agda
module _ where -- user written module header
postulate A : Set
module File where -- inner module with the same name as the file, ok
```
### Pattern matching
* Forced constructor patterns.
Constructor patterns can now be dotted to indicate that Agda should not case
split on them but rather their value is forced by the type of the other
patterns. The difference between this and a regular dot pattern is that
forced constructor patterns can still bind variables in their arguments.
For example,
```agda
open import Agda.Builtin.Nat
data Vec (A : Set) : Nat → Set where
nil : Vec A zero
cons : (n : Nat) → A → Vec A n → Vec A (suc n)
append : {A : Set} (m n : Nat) → Vec A m → Vec A n → Vec A (m + n)
append .zero n nil ys = ys
append (.suc m) n (cons .m x xs) ys = cons (m + n) x (append m n xs ys)
```
* Inferring the type of a function based on its patterns
Agda no longer infers the type of a function based on the patterns used in
its definition. [Issue [#2834](https://github.com/agda/agda/issues/2834)]
This means that the following Agda program is no longer accepted:
```agda
open import Agda.Builtin.Nat
f : _ → _
f zero = zero
f (suc n) = n
```
Agda now requires the type of the argument of `f` to be given explicitly.
* Improved constraint solving for pattern matching functions
Constraint solving for functions where each right-hand side has a distinct
rigid head has been extended to also cover the case where some clauses return
an argument of the function. A typical example is append on lists:
```agda
_++_ : {A : Set} → List A → List A → List A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
```
Agda can now solve constraints like `?X ++ ys == 1 ∷ ys` when `ys` is a
neutral term.
* Record expressions translated to copatterns
Definitions of the form
```agda
f ps = record { f₁ = e₁; ..; fₙ = eₙ }
```
are translated internally to use copatterns:
```agda
f ps .f₁ = e₁
...
f ps .fₙ = eₙ
```
This means that `f ps` does not reduce, but thanks to η-equality the two
definitions are equivalent.
The change should lead to fewer big record expressions showing up in goal
types, and potentially significant performance improvement in some cases.
This may have a minor impact on with-abstraction and code using `--rewriting`
since η-equality is not used in these cases.
* When using `with`, it is now allowed to replace any pattern from the parent
clause by a variable in the with clause. For example:
```agda
f : List ℕ → List ℕ
f [] = []
f (x ∷ xs) with x ≤? 10
f xs | p = {!!}
```
In the with clause, `xs` is treated as a let-bound variable with value
`.x ∷ .xs` (where `.x : ℕ` and `.xs : List ℕ` are out of scope) and
`p : Dec (.x ≤ 10)`.
Since with-abstraction may change the type of variables, instantiations
of variables in the with clause are type checked again after with-abstraction.
### Builtins
* Added support for built-in 64-bit machine words.
These are defined in `Agda.Builtin.Word` and come with two primitive
operations to convert to and from natural numbers.
```agda
Word64 : Set
primWord64ToNat : Word64 → Nat
primWord64FromNat : Nat → Word64
```
Converting to a natural number is the trivial embedding, and converting from a natural number
gives you the remainder modulo 2^64. The proofs of these theorems are not
primitive, but can be defined in a library using `primTrustMe`.
Basic arithmetic operations can be defined on `Word64` by converting to
natural numbers, peforming the corresponding operation, and then converting
back. The compiler will optimise these to use 64-bit arithmetic. For
instance,
```agda
addWord : Word64 → Word64 → Word64
addWord a b = primWord64FromNat (primWord64ToNat a + primWord64ToNat b)
subWord : Word64 → Word64 → Word64
subWord a b = primWord64FromNat (primWord64ToNat a + 18446744073709551616 - primWord64ToNat b)
```
These compiles (in the GHC backend) to addition and subtraction on
`Data.Word.Word64`.
* New primitive primFloatLess and changed semantics of primFloatNumericalLess.
`primFloatNumericalLess` now uses standard IEEE `<`, so for instance
`NaN < x = x < NaN = false`.
On the other hand `primFloatLess` provides a total order on `Float`, with
`-Inf < NaN < -1.0 < -0.0 < 0.0 < 1.0 < Inf`.
* The `SIZEINF` builtin is now given the name `∞` in
`Agda.Builtin.Size` [Issue
[#2931](https://github.com/agda/agda/issues/2931)].
Previously it was given the name `ω`.
### Reflection
* New TC primitive: `declarePostulate`. [Issue
[#2782](https://github.com/agda/agda/issues/2782)]
```agda
declarePostulate : Arg Name → Type → TC ⊤
```
This can be used to declare new postulates. The Visibility of the
Arg must not be hidden. This feature fails when executed with
`--safe` flag from command-line.
Pragmas and options
-------------------
* The `--caching` option is ON by default and is also a valid pragma.
Caching can (sometimes) speed up re-typechecking in `--interaction`
mode by reusing the result of the previous typechecking for the
prefix of the file that has not changed (with a granularity at the
level of declarations/mutual blocks).
It can be turned off by passing ```--no-caching``` to ```agda``` or
with the following at the top of your file.
```agda
{-# OPTIONS --no-caching #-}
```
* The `--sharing` and `--no-sharing` options have been deprecated and do
nothing.
Compile-time evaluation is now always call-by-need.
* BUILTIN pragmas can now appear before the top-level module header
and in parametrized modules.
[Issue [#2824](https://github.com/agda/agda/issues/2824)]
```agda
{-# OPTIONS --rewriting #-}
open import Agda.Builtin.Equality
{-# BUILTIN REWRITE _≡_ #-} -- here
module TopLevel (A : Set) where
{-# BUILTIN REWRITE _≡_ #-} -- or here
```
Note that it is still the case that built-ins cannot be bound if
they depend on module parameters from an enclosing module. For
instance, the following is illegal:
```agda
module _ {a} {A : Set a} where
data _≡_ (x : A) : A → Set a where
refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
```
* Builtin `NIL` and `CONS` have been merged with `LIST`.
When binding the `LIST` builtin, `NIL` and `CONS` are bound to
the appropriate constructors automatically. This means that instead
of writing
```agda
{-# BUILTIN LIST List #-}
{-# BUILTIN NIL [] #-}
{-# BUILTIN CONS _∷_ #-}
```
you just write
```agda
{-# BUILTIN LIST List #-}
```
Attempting to bind `NIL` or `CONS` results in a warning and has otherwise no
effect.
* The `--no-unicode` pragma prevents Agda from introducing unicode characters
when pretty printing a term. Lambda, Arrows and Forall quantifiers are all
replaced by their ascii only version. Instead of resorting to subscript
suffixes, Agda uses ascii digit characters.
* New option `--inversion-max-depth=N`.
The depth is used to avoid looping due to inverting pattern matching for
unsatisfiable constraints [Issue [#431](https://github.com/agda/agda/issues/431)].
This option is only expected to be necessary in pathological cases.
* New option `--no-print-pattern-synonyms`.
This disables the use of pattern synonyms in output from Agda.
See [Issue [#2902](https://github.com/agda/agda/issues/2902)] for situations
where this might be desirable.
* New fine-grained control over the warning machinery: ability to (en/dis)able
warnings on a one-by-one basis.
* The command line option `--help` now takes an optional argument which
allows the user to request more specific usage information about particular
topics. The only one added so far is `warning`.
* New pragma NOINLINE.
```agda
{-# NOINLINE f #-}
```
Disables automatic inlining of `f`.
* New pragma WARNING_ON_USAGE
```
{-# WARNING_ON_USAGE QName Message #}
```
Prints Message whenever QName is used.
Emacs mode
----------
* Banana brackets have been added to the Agda input method.
```
\(( #x2985 LEFT WHITE PARENTHESIS
\)) #x2986 RIGHT WHITE PARENTHESIS
```
* Result splitting will introduce the trailing hidden arguments,
if there is nothing else todo
[Issue [#2871](https://github.com/agda/agda/issues/2871)].
Example:
```agda
data Fun (A : Set) : Set where
mkFun : (A → A) → Fun A
test : {A : Set} → Fun A
test = ?
```
Splitting on the result here (`C-c C-c RET`) will append
`{A}` to the left hand side.
```agda
test {A} = ?
```
* Light highlighting is performed dynamically, even if the file is not
loaded [Issue [#2794](https://github.com/agda/agda/issues/2794)].
This light highlighting is based on the token stream generated by
Agda's lexer: the code is only highlighted if the file is lexically
correct. If the Agda backend is not busy with something else, then
the code is highlighted automatically in certain situations:
* When the file is saved.
* When Emacs has been idle, continuously, for a certain period of
time (by default 0.2 s) after the last modification of the file,
and the file has not been saved (or marked as being unmodified).
This functionality can be turned off, and the time period can be
customised.
* Highlighting of comments is no longer handled by Font Lock mode
[Issue [#2794](https://github.com/agda/agda/issues/2794)].
* The Emacs mode's syntax table has been changed.
Previously `_` was treated as punctuation. Now it is treated in the
same way as most other characters: if the standard syntax table
assigns it the syntax class "whitespace", "open parenthesis" or
"close parenthesis", then it gets that syntax class, and otherwise
it gets the syntax class "word constituent".
Compiler backends
-----------------
* The GHC backend now automatically compiles BUILTIN LIST to Haskell lists.
This means that it's no longer necessary to give a COMPILE GHC pragma for the
builtin list type. Indeed, doing so has no effect on the compilation and
results in a warning.
* The GHC backend performance improvements.
Generated Haskell code now contains approximate type signatures, which lets
GHC get rid of many of the `unsafeCoerce`s. This leads to performance
improvements of up to 50% of compiled code.
* The GHC backend now compiles the `INFINITY`, `SHARP` and `FLAT`
builtins in a different way [Issue
[#2909](https://github.com/agda/agda/issues/2909)].
Previously these were compiled to (basically) nothing. Now the
`INFINITY` builtin is compiled to `Infinity`, available from
`MAlonzo.RTE`:
```haskell
data Inf a = Sharp { flat :: a }
type Infinity level a = Inf a
```
The `SHARP` builtin is compiled to `Sharp`, and the `FLAT` builtin
is (by default) compiled to a corresponding destructor.
Note that code that interacts with Haskell libraries may have to be
updated. As an example, here is one way to print colists of
characters using the Haskell function `putStr`:
```agda
open import Agda.Builtin.Char
open import Agda.Builtin.Coinduction
open import Agda.Builtin.IO
open import Agda.Builtin.Unit
data Colist {a} (A : Set a) : Set a where
[] : Colist A
_∷_ : A → ∞ (Colist A) → Colist A
{-# FOREIGN GHC
data Colist a = Nil | Cons a (MAlonzo.RTE.Inf (Colist a))
type Colist' l a = Colist a
fromColist :: Colist a -> [a]
fromColist Nil = []
fromColist (Cons x xs) = x : fromColist (MAlonzo.RTE.flat xs)
#-}
{-# COMPILE GHC Colist = data Colist' (Nil | Cons) #-}
postulate
putStr : Colist Char → IO ⊤
{-# COMPILE GHC putStr = putStr . fromColist #-}
```
* `COMPILE GHC` pragmas have been included for the size primitives
[Issue [#2879](https://github.com/agda/agda/issues/2879)].
LaTeX backend
-------------
* The `code` environment can now take arguments [Issues
[#2744](https://github.com/agda/agda/issues/2744) and
[#2453](https://github.com/agda/agda/issues/2453)].
Everything from \begin{code} to the end of the line is preserved in
the generated LaTeX code, and not treated as Agda code.
The default implementation of the `code` environment recognises one
optional argument, `hide`, which can be used for code that should be
type-checked, but not typeset:
```latex
\begin{code}[hide]
open import Module
\end{code}
```
The `AgdaHide` macro has not been removed, but has been deprecated
in favour of `[hide]`.
* The `AgdaSuppressSpace` and `AgdaMultiCode` environments no longer
take an argument.
Instead some documents need to be compiled multiple times.
* The `--count-clusters` flag can now be given in `OPTIONS` pragmas.
* The `nofontsetup` option to the LaTeX package `agda` was broken, and
has (hopefully) been fixed
[Issue [#2773](https://github.com/agda/agda/issues/2773)].
Fewer packages than before are loaded when `nofontsetup` is used,
see `agda.sty` for details. Furthermore, if LuaLaTeX or XeLaTeX are
not used, then the font encoding is no longer changed.
* The new option `noinputencodingsetup` instructs the LaTeX package
`agda` to not change the input encoding, and to not load the `ucs`
package.
* Underscores are now typeset using `\AgdaUnderscore{}`.
The default implementation is `\_` (the command that was previously
generated for underscores). Note that it is possible to override
this implementation.
* OtherAspects (unsolved meta variables, catchall clauses, etc.) are
now correctly highlighted in the LaTeX backend (and the HTML one).
[Issue [#2474](https://github.com/agda/agda/issues/2474)]
* `postprocess-latex.pl` does not add extra spaces around tagged `\Agda*{}`
commands anymore.
HTML backend
------------
* An identifier (excluding bound variables),
gets the identifier itself as an anchor,
_in addition_ to the file position
[Issue [#2756](https://github.com/agda/agda/issues/2756)].
In Agda 2.5.3, the identifier anchor would _replace_ the file position anchor
[Issue [#2604](https://github.com/agda/agda/issues/2604)].
Symbolic anchors look like
```html
```
while file position anchors just give the character position in the file:
```html
```
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 -- Only character position anchor
test2 : Set₁ -- Issue2604.html#test2
test2 = bla
where
bla = Set -- Only 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 -- Only character position anchor
test5 : Set₁ -- Only character position anchor
test5 = M.bla
```
List of closed issues
---------------------
For 2.5.4, the following issues have been closed
(see [bug tracker](https://github.com/agda/agda/issues)):
- [#351](https://github.com/agda/agda/issues/351): Constraint solving for irrelevant metas
- [#421](https://github.com/agda/agda/issues/421): Higher order positivity
- [#431](https://github.com/agda/agda/issues/431): Constructor-headed function makes type-checker diverge
- [#437](https://github.com/agda/agda/issues/437): Detect when something cannot be a function type
- [#488](https://github.com/agda/agda/issues/488): Refining on user defined syntax mixes up the order of the subgoals
- [#681](https://github.com/agda/agda/issues/681): Lack of visual state indicators in new Emacs mode
- [#689](https://github.com/agda/agda/issues/689): Contradictory constraints should yield error
- [#708](https://github.com/agda/agda/issues/708): Coverage checker not taking literal patterns into account properly
- [#875](https://github.com/agda/agda/issues/875): Nonstrict irrelevance violated by implicit inference
- [#964](https://github.com/agda/agda/issues/964): Allow unsolved metas in imported files
- [#987](https://github.com/agda/agda/issues/987): --html anchors could be more informative
- [#1054](https://github.com/agda/agda/issues/1054): Inlined Agda code in LaTeX backend
- [#1131](https://github.com/agda/agda/issues/1131): Infix definitions not allowed in let definitions
- [#1169](https://github.com/agda/agda/issues/1169): Auto fails with non-terminating function
- [#1268](https://github.com/agda/agda/issues/1268): Hard to print type of variable if the type starts with an instance argument
- [#1384](https://github.com/agda/agda/issues/1384): Order of constructor arguments matters for coverage checker
- [#1425](https://github.com/agda/agda/issues/1425): Instances with relevant recursive instance arguments are not considered in irrelevant positions
- [#1548](https://github.com/agda/agda/issues/1548): Confusing error about ambiguous definition with parametrized modules
- [#1884](https://github.com/agda/agda/issues/1884): what is the format of the libraries and defaults files
- [#1906](https://github.com/agda/agda/issues/1906): Possible performance problem
- [#2056](https://github.com/agda/agda/issues/2056): Cannot instantiate meta to solution...: Pattern checking done too early in where block
- [#2067](https://github.com/agda/agda/issues/2067): Display forms in parameterised module too general
- [#2183](https://github.com/agda/agda/issues/2183): Allow splitting on dotted variables
- [#2226](https://github.com/agda/agda/issues/2226): open {{...}} gets hiding wrong
- [#2255](https://github.com/agda/agda/issues/2255): Performance issue with deeply-nested lambdas
- [#2306](https://github.com/agda/agda/issues/2306): Commands in the emacs-mode get confused if we add question marks to the file
- [#2384](https://github.com/agda/agda/issues/2384): More fine-grained blocking in constraint solver
- [#2401](https://github.com/agda/agda/issues/2401): LaTeX backend error
- [#2404](https://github.com/agda/agda/issues/2404): checkType doesn't accept a type-checking definition checked with the same type
- [#2420](https://github.com/agda/agda/issues/2420): Failed to solve level constraints in record type with hole
- [#2421](https://github.com/agda/agda/issues/2421): After emacs starts up, Agda does not process file without restart of Agda
- [#2436](https://github.com/agda/agda/issues/2436): Agda allows coinductive records with eta-equality
- [#2450](https://github.com/agda/agda/issues/2450): Irrelevant variables are pruned too eagerly
- [#2474](https://github.com/agda/agda/issues/2474): The LaTeX and HTML backends do not highlight (all) unsolved metas
- [#2484](https://github.com/agda/agda/issues/2484): Regression related to sized types
- [#2526](https://github.com/agda/agda/issues/2526): Better documentation of record modules
- [#2536](https://github.com/agda/agda/issues/2536): UTF8 parsed incorrectly for literate agda files
- [#2565](https://github.com/agda/agda/issues/2565): Options for the interaction action give to keep the overloaded literals and sections?
- [#2576](https://github.com/agda/agda/issues/2576): Shadowing data decl by data sig produces Missing type signature error
- [#2594](https://github.com/agda/agda/issues/2594): Valid partial cover rejected: "Cannot split on argument of non-datatype"
- [#2600](https://github.com/agda/agda/issues/2600): Stack complains about Agda.cabal
- [#2607](https://github.com/agda/agda/issues/2607): Instance search confused when an instance argument is sourced from a record
- [#2617](https://github.com/agda/agda/issues/2617): Installation instructions
- [#2623](https://github.com/agda/agda/issues/2623): Incorrect indentation when \AgdaHide is used
- [#2634](https://github.com/agda/agda/issues/2634): Fixity declaration ignored in definitions in record
- [#2636](https://github.com/agda/agda/issues/2636): The positivity checker complains when a new definition is added in the same where clause
- [#2640](https://github.com/agda/agda/issues/2640): Unifier dots the relevant pattern variables when it should dot the irrelevant ones
- [#2668](https://github.com/agda/agda/issues/2668): Changing the visibility of a module parameter breaks `with`
- [#2728](https://github.com/agda/agda/issues/2728): Bad interaction between caching and the warning machinery
- [#2738](https://github.com/agda/agda/issues/2738): Update Stackage LTS from 9.1 to version supporting Alex 3.2.3
- [#2744](https://github.com/agda/agda/issues/2744): It should be possible to give arguments to the code environment
- [#2745](https://github.com/agda/agda/issues/2745): Broken build with GHC 7.8.4 due to (new) version 1.2.2.0 of hashtables
- [#2749](https://github.com/agda/agda/issues/2749): Add --no-unicode cli option to Agda
- [#2751](https://github.com/agda/agda/issues/2751): Unsolved constraints, but no highlighting
- [#2752](https://github.com/agda/agda/issues/2752): Mutual blocks inside instance blocks
- [#2753](https://github.com/agda/agda/issues/2753): Unsolved constraint, related to instance arguments and sized types
- [#2756](https://github.com/agda/agda/issues/2756): HTML backend generates broken links
- [#2758](https://github.com/agda/agda/issues/2758): Relevant meta is instantiated with irrelevant solution
- [#2759](https://github.com/agda/agda/issues/2759): Empty mutual blocks should be warning rather than error
- [#2762](https://github.com/agda/agda/issues/2762): Automatically generate DISPLAY pragmas to fold pattern synonyms
- [#2763](https://github.com/agda/agda/issues/2763): Internal Error at "src/full/Agda/TypeChecking/Abstract.hs:138"
- [#2765](https://github.com/agda/agda/issues/2765): Inferred level expressions are often "reversed"
- [#2769](https://github.com/agda/agda/issues/2769): Agda prints ill-formed expression, record argument dropped
- [#2771](https://github.com/agda/agda/issues/2771): Erroneous 'with' error message
- [#2773](https://github.com/agda/agda/issues/2773): The nofontsetup option does not work as advertised
- [#2775](https://github.com/agda/agda/issues/2775): Irrelevance to be taken into account in 'with' abstraction.
- [#2776](https://github.com/agda/agda/issues/2776): Dotted variable in inferred type
- [#2780](https://github.com/agda/agda/issues/2780): Improve level constraint solving for groups of inequality constraints
- [#2782](https://github.com/agda/agda/issues/2782): Extending Agda reflection to introduce postulates
- [#2785](https://github.com/agda/agda/issues/2785): internal error @ ConcreteToAbstract.hs:721
- [#2787](https://github.com/agda/agda/issues/2787): Overloaded pattern synonyms
- [#2792](https://github.com/agda/agda/issues/2792): Safe modules can sometimes not be imported from unsafe modules
- [#2794](https://github.com/agda/agda/issues/2794): Using \texttt{-} destroys code coloring in literate file
- [#2796](https://github.com/agda/agda/issues/2796): Overloaded (inherited) projection resolution fails with parametrized record
- [#2798](https://github.com/agda/agda/issues/2798): The LaTeX backend ignores the "operator" aspect
- [#2802](https://github.com/agda/agda/issues/2802): Printing of overloaded functions broken due to eager normalization of projections
- [#2803](https://github.com/agda/agda/issues/2803): Case splitting loses names of hidden arguments
- [#2808](https://github.com/agda/agda/issues/2808): Confusing error when inserting declaration before top-level module
- [#2810](https://github.com/agda/agda/issues/2810): Make `--caching` a pragma option
- [#2811](https://github.com/agda/agda/issues/2811): OPTION --caching allowed in file (Issue #2810)
- [#2819](https://github.com/agda/agda/issues/2819): Forcing analysis doesn't consider relevance
- [#2821](https://github.com/agda/agda/issues/2821): BUILTIN BOOL gremlin
- [#2824](https://github.com/agda/agda/issues/2824): Allow {-# BUILTIN #-} in preamble and in parametrized modules
- [#2826](https://github.com/agda/agda/issues/2826): Case splitting on earlier variable uses duplicate variable name
- [#2827](https://github.com/agda/agda/issues/2827): Variables off in with-clauses. Parameter refinement?
- [#2831](https://github.com/agda/agda/issues/2831): NO_POSITIVITY_CHECK pragma can be written before a mutual block without data or record types
- [#2832](https://github.com/agda/agda/issues/2832): BUILTIN NIL and CONS are not needed
- [#2834](https://github.com/agda/agda/issues/2834): Disambiguation of type based on pattern leads to non-unique meta solution
- [#2836](https://github.com/agda/agda/issues/2836): The Emacs mode does not handle .lagda.tex files
- [#2840](https://github.com/agda/agda/issues/2840): Internal error in positivity with modules/datatype definitions
- [#2841](https://github.com/agda/agda/issues/2841): Opting out of idiom brackets
- [#2844](https://github.com/agda/agda/issues/2844): Root documentation URL redirects to version 2.5.2
- [#2849](https://github.com/agda/agda/issues/2849): Internal error at absurd pattern followed by `rewrite`
- [#2854](https://github.com/agda/agda/issues/2854): Agda worries about possibly empty type of sizes even when no builtins for size are active
- [#2855](https://github.com/agda/agda/issues/2855): Single-clause definition is both unreachable and incomplete
- [#2856](https://github.com/agda/agda/issues/2856): Panic: unbound variable
- [#2859](https://github.com/agda/agda/issues/2859): Error "pattern variable shadows constructor" caused by parameter refinement
- [#2862](https://github.com/agda/agda/issues/2862): inconsistency from a mutual datatype declaration and module definition
- [#2867](https://github.com/agda/agda/issues/2867): Give does not insert parenthesis for module parameters
- [#2868](https://github.com/agda/agda/issues/2868): With --postfix-projections, record fields are printed preceded by a dot when working within the record
- [#2870](https://github.com/agda/agda/issues/2870): Lexical error for \- (hyphen)
- [#2871](https://github.com/agda/agda/issues/2871): Introduce just trailing hidden arguments by result splitting
- [#2873](https://github.com/agda/agda/issues/2873): Refinement problem in presence of overloaded constructors
- [#2874](https://github.com/agda/agda/issues/2874): Internal error in src/full/Agda/TypeChecking/Coverage/Match.hs:312
- [#2878](https://github.com/agda/agda/issues/2878): Support for GHC 8.4.1
- [#2879](https://github.com/agda/agda/issues/2879): Include COMPILE GHC pragmas for size primitives
- [#2881](https://github.com/agda/agda/issues/2881): Internal error in BasicOps
- [#2883](https://github.com/agda/agda/issues/2883): "internal error in TypeChecking/Substitute.hs:379"
- [#2884](https://github.com/agda/agda/issues/2884): Missing PDF user manual in the tarball
- [#2888](https://github.com/agda/agda/issues/2888): Internal error caused by new forcing translation
- [#2894](https://github.com/agda/agda/issues/2894): Unifier tries to eta expand non-eta record
- [#2896](https://github.com/agda/agda/issues/2896): Unifier throws away pattern
- [#2897](https://github.com/agda/agda/issues/2897): Internal error for local modules with refined parameters
- [#2904](https://github.com/agda/agda/issues/2904): No tab completion for GHCNoMain
- [#2906](https://github.com/agda/agda/issues/2906): Confusing "cannot be translated to a Haskell type" error message
- [#2908](https://github.com/agda/agda/issues/2908): primForce is compiled away
- [#2909](https://github.com/agda/agda/issues/2909): Agda uses newtypes incorrectly, causing wellformed programs to loop
- [#2911](https://github.com/agda/agda/issues/2911): Inferring missing instance clause panics in refined context
- [#2912](https://github.com/agda/agda/issues/2912): Add fine-grained control over the displayed warnings
- [#2914](https://github.com/agda/agda/issues/2914): Slicing ignores as pragma?
- [#2916](https://github.com/agda/agda/issues/2916): The GHC backend generates code with an incorrect number of constructor arguments
- [#2917](https://github.com/agda/agda/issues/2917): Very slow due to unsolved size?
- [#2919](https://github.com/agda/agda/issues/2919): Internal error in Agda.TypeChecking.Forcing
- [#2921](https://github.com/agda/agda/issues/2921): COMPILE data for data types with erased constructor arguments
- [#2923](https://github.com/agda/agda/issues/2923): Word.agda not included as builtin
- [#2925](https://github.com/agda/agda/issues/2925): Allow adding the same rewrite rules multiple times
- [#2927](https://github.com/agda/agda/issues/2927): Panic related to sized types
- [#2928](https://github.com/agda/agda/issues/2928): Internal error in Agda.TypeChecking.Rules.LHS
- [#2931](https://github.com/agda/agda/issues/2931): Rename Agda.Builtin.Size.ω to ∞?
- [#2941](https://github.com/agda/agda/issues/2941): "coinductive" record inconsistent
- [#2944](https://github.com/agda/agda/issues/2944): Regression, seemingly related to record expressions
- [#2945](https://github.com/agda/agda/issues/2945): Inversion warning in code that used to be accepted
- [#2947](https://github.com/agda/agda/issues/2947): Internal error in Agda.TypeChecking.Forcing
- [#2952](https://github.com/agda/agda/issues/2952): Wrong compilation of pattern matching to Haskell
- [#2953](https://github.com/agda/agda/issues/2953): Generated Haskell code does not typecheck
- [#2954](https://github.com/agda/agda/issues/2954): Pattern matching on string gives unexpected unreachable clause
- [#2957](https://github.com/agda/agda/issues/2957): Support for async 2.2.1
- [#2958](https://github.com/agda/agda/issues/2958): `as` names being duplicated in buffer after `with`
- [#2959](https://github.com/agda/agda/issues/2959): Repeating a successful command after revert + reload fails with caching enabled
- [#2960](https://github.com/agda/agda/issues/2960): Uncommenting indented lines doesn't work
- [#2963](https://github.com/agda/agda/issues/2963): Extended lambdas bypass positivity checking in records
- [#2966](https://github.com/agda/agda/issues/2966): Internal error in Auto
- [#2968](https://github.com/agda/agda/issues/2968): Bad Interaction with copatterns and eta?, leads to ill-typed terms in error messages.
- [#2971](https://github.com/agda/agda/issues/2971): Copattern split with `--no-irrelevant-projections` panics
- [#2974](https://github.com/agda/agda/issues/2974): Copatterns break canonicity
- [#2975](https://github.com/agda/agda/issues/2975): Termination checker runs too early for definitions inside record (or: positivity checker runs too late)
- [#2976](https://github.com/agda/agda/issues/2976): Emacs mode reports errors in connection with highlighting comments
- [#2978](https://github.com/agda/agda/issues/2978): Double solving of meta
- [#2985](https://github.com/agda/agda/issues/2985): The termination checker accepts non-terminating code
- [#2989](https://github.com/agda/agda/issues/2989): Internal error when checking record match in let expr
- [#2990](https://github.com/agda/agda/issues/2990): Performance regression related to the abstract machine
- [#2994](https://github.com/agda/agda/issues/2994): Solution accepted in hole is subsequently rejected on reload
- [#2996](https://github.com/agda/agda/issues/2996): Internal error with -v tc.cover:20
- [#2997](https://github.com/agda/agda/issues/2997): Internal error in Agda.TypeChecking.Rules.LHS
- [#2998](https://github.com/agda/agda/issues/2998): Regression: With clause pattern x is not an instance of its parent pattern "eta expansion of x"
- [#3002](https://github.com/agda/agda/issues/3002): Spurious 1 after simplification
- [#3004](https://github.com/agda/agda/issues/3004): Agda hangs on extended lambda
- [#3007](https://github.com/agda/agda/issues/3007): Internal error in Parser
- [#3012](https://github.com/agda/agda/issues/3012): Internal Error at : "src/full/Agda/TypeChecking/Reduce/Fast.hs:1030"
- [#3014](https://github.com/agda/agda/issues/3014): Internal error in Rules.LHS
- [#3020](https://github.com/agda/agda/issues/3020): Missing highlighting in record modules
- [#3023](https://github.com/agda/agda/issues/3023): Support for GHC 8.4.2
- [#3024](https://github.com/agda/agda/issues/3024): Postfix projection patterns not highlighted correctly with agda --latex
- [#3030](https://github.com/agda/agda/issues/3030): [ warning ] user defined warnings
- [#3031](https://github.com/agda/agda/issues/3031): Eta failure for record meta with irrelevant fields
- [#3033](https://github.com/agda/agda/issues/3033): Giving and solving don't insert parenthesis for applications in dot pattern
- [#3044](https://github.com/agda/agda/issues/3044): Internal error in src/full/Agda/TypeChecking/Substitute/Class.hs:209
- [#3045](https://github.com/agda/agda/issues/3045): GHC backend generates type without enough arguments
- [#3046](https://github.com/agda/agda/issues/3046): do-notation causes parse errors in subsequent where clauses
- [#3049](https://github.com/agda/agda/issues/3049): Positivity unsoundness
- [#3050](https://github.com/agda/agda/issues/3050): We revert back to call-by-name during positivity checking
- [#3051](https://github.com/agda/agda/issues/3051): Pattern synonyms should be allowed in mutual blocks
- [#3052](https://github.com/agda/agda/issues/3052): Another recent inference change
- [#3062](https://github.com/agda/agda/issues/3062): Literal match does not respect first-match semantics
- [#3063](https://github.com/agda/agda/issues/3063): Internal error in Agda.TypeChecking.Forcing
- [#3064](https://github.com/agda/agda/issues/3064): Coverage checker bogus on literals combined with copatterns
- [#3065](https://github.com/agda/agda/issues/3065): Internal error in coverage checker triggered by literal dot pattern
- [#3067](https://github.com/agda/agda/issues/3067): checking hangs on invalid program
- [#3072](https://github.com/agda/agda/issues/3072): invalid section printing
- [#3074](https://github.com/agda/agda/issues/3074): Wrong hiding causes internal error in LHS checker
- [#3075](https://github.com/agda/agda/issues/3075): Automatic inlining and tactics
- [#3078](https://github.com/agda/agda/issues/3078): Error building with GHC 7.10.2: Missing transformers library
- [#3079](https://github.com/agda/agda/issues/3079): Wrong parameter hiding for instance open
- [#3080](https://github.com/agda/agda/issues/3080): Case splitting prints out-of-scope pattern synonyms
- [#3082](https://github.com/agda/agda/issues/3082): Emacs mode regression: a ? inserted before existing hole hijacks its interaction point
- [#3083](https://github.com/agda/agda/issues/3083): Wrong hiding in module application
- [#3084](https://github.com/agda/agda/issues/3084): Changes to mode line do not take effect immediately
- [#3085](https://github.com/agda/agda/issues/3085): Postpone checking a pattern let binding when type is blocked
- [#3090](https://github.com/agda/agda/issues/3090): Internal error in parser when using parentheses in BUILTIN pragma
- [#3096](https://github.com/agda/agda/issues/3096): Support GHC 8.4.3