Release notes for Agda version 2.6.0
====================================

Highlights
----------

* Added support for [Cubical
  Agda](https://agda.readthedocs.io/en/v2.6.0/language/cubical.html)
  which adds new features such as univalence and higher inductive
  types to Agda.

* Added support for ML-style [automatic generalization of
  variables](https://agda.readthedocs.io/en/v2.6.0/language/generalization-of-declared-variables.html).

* Added a new sort ``Prop`` of [definitionally proof-irrelevant
  propositions](https://agda.readthedocs.io/en/v2.6.0/language/prop.html).

* The implementation of [instance
  search](https://agda.readthedocs.io/en/v2.6.0/language/instance-arguments.html)
  got a major overhaul and no longer supports overlapping instances
  (unless enabled by a flag).

Installation and infrastructure
-------------------------------

* Added support for GHC 8.6.4.

* Interface files for all builtin and primitive files are now
  re-generated each time Agda is installed.

Syntax
------

* Agda now supports implicit generalization of declared
  variables. Variables to be generalized can declared with the new
  keyword `variable`.  For example:

  ```agda
    postulate
      Con : Set

    variable
      Γ Δ θ : Con
  ```

  Declared variables are automatically generalized in type signatures,
  module telescopes and data type and record parameters and indices:

  ```agda
    postulate
      Sub : Con → Con → Set

      id  : Sub Γ Γ
   -- -- equivalent to
   -- id  : {Γ : Con} → Sub Γ Γ

      _∘_ : Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
   -- -- equivalent to
   -- _∘_ : {Γ Δ Θ : Con} → Sub Θ Δ → Sub Γ Θ → Sub Γ Δ
  ```

  See the [user manual](https://agda.readthedocs.io/en/v2.6.0/language/generalization-of-declared-variables.html)
  for more details.

* Data type and record definitions separated from their type signatures can no
  longer repeat the types of the parameters, but can bind implicit parameters
  by name [Issue [#1886](https://github.com/agda/agda/issues/1886)].

  This is now allowed
  ```agda
    data D {a b} (A : Set a) (B : Set b) : Set (a ⊔ lsuc b)
    data D {b = b} A B where
      mkD : (A → Set b) → D A B
  ```
  but this is not
  ```agda
    data I (A : Set) : Set
    data I (A : Set) where
  ```

* The label used for named implicit arguments can now be different from the
  name of the bound variable [Issue [#952](https://github.com/agda/agda/issues/952)].

  Example,
  ```agda
    id₁ : {A = X : Set} → X → X
    id₁ x = x

    id₂ : ∀ {B = X} → X → X
    id₂ {B = X} x = id₁ {A = X} x

    test : Nat
    test = id₁ {A = Nat} 5 + id₂ {B = Nat} 6
  ```
  Only implicit and instance arguments can have a label and either or both of
  the label and bound variable can be `_`. Labeled bindings with a type
  signature can only bind a single variable. For instance, the type `Set` has
  to be repeated here:
  ```agda
    const : {A = X : Set} {B = Y : Set} → X → Y → X
    const x _ = x
  ```

* The rules for parsing of patterns have changed slightly [Issue
  [#3400](https://github.com/agda/agda/issues/3400)].

  Now projections are treated similarly to constructors: In a pattern
  name parts coming from projections can only be used as part of
  projections, constructors or pattern synonyms. They cannot be used
  as variables, or as part of the name of the defined value.

  Examples:

  * The following code used to be syntactically ambiguous, but is now
    parsed, because A can no longer be used as a variable:
    ```agda
    record R : Set₂ where
      field
        _A : Set₁

    open R

    r : R
    r A = Set
    ```

  * On the other hand the following code is no longer parsed:
    ```agda
    record R : Set₁ where
      field
        ⟨_+_⟩ : Set

    open R

    + : Set → Set
    + A = A
    ```


Type checking
-------------

* Agda now supports a cubical mode which adds new features from
  [Cubical Type Theory](https://arxiv.org/abs/1611.02108), including
  univalence and higher inductive types. Option `--cubical` enables
  the cubical mode, and cubical primitives are defined in the module
  `Agda.Primitive.Cubical`.  See the [user
  manual](https://agda.readthedocs.io/en/v2.6.0/language/cubical.html)
  for more info.

* Agda now supports the new sort ``Prop`` of [definitionally
  proof-irrelevant propositions](https://hal.inria.fr/hal-01859964).
  Option `--prop` enables the `Prop` universe but is off by default.
  Option `--no-prop` disables the `Prop` universe.  See the [user
  manual](https://agda.readthedocs.io/en/v2.6.0/language/prop.html)
  for more details.

  In the absense of `Prop`, the sort `Set` is the lowest sort, thus,
  the sort annotation `: Set` can be ommitted if the sort is
  constrained to be weakly below `Set`.  For instance:

  ```agda
  {-# OPTIONS --no-prop #-}

  data Wrap A : Set where
    wrap : A → Wrap A
  ```

  In contrast, when `--prop` is enabled the sort of `A` could be
  either `Set` or `Prop` so this code no longer typechecks.

* Agda now allows omitting absurd clauses in case one of the pattern
  variable inhabits an obviously empty type
  [Issue [#1086](https://github.com/agda/agda/issues/1086)].
  For example:
  ```agda
  f : Fin 1 → Nat
  f zero = 0
  -- f (suc ())   -- this clause is no longer required
  ```
  Absurd clauses are still required in case deep pattern matching is
  needed to expose the absurd variable, or if there are no non-absurd
  clauses.

  Due to the changes to the coverage checker required for this new
  feature, Agda will now sometimes construct a different case tree when
  there are multiple valid splitting orders. In some cases this may
  impact the constraints that Agda is able to solve (for example, see
  [#673](https://github.com/agda/agda-stdlib/pull/673) on the
  standard library).

* Since Agda 2.5.3, the hiding is considered part of the name in the
  insertion of implicit arguments.  Until Agda 2.5.2, the following
  code was rejected:
  ```agda
    test : {{X : Set}} {X : Set} → Set
    test {X = X} = X
  ```
  The rationale was that named argument `X` is given with the wrong hiding.
  The new rationale is that the hiding is considered part of the name,
  distinguishing `{{X}}` from `{X}`.
  This language change was accidential and has not been documented in
  the 2.5.3 release notes.

* Agda no longer allows case splitting on irrelevant arguments of
  record types (see Issue
  [#3056](https://github.com/agda/agda/issues/3056)).

* Metavariables in module telescopes are now sometimes frozen later
  [Issue [#1063](https://github.com/agda/agda/issues/1063)].

  Metavariables created in the types of module parameters used to be
  frozen right after the module's first mutual block had been
  type-checked (unless, perhaps, if the module itself was contained in
  a mutual block). Now they are instead frozen at the end of the
  module (with a similar caveat regarding an outer mutual block).

* When `--without-K` is enabled, Agda no longer allows datatypes with
  large indices. For example, the following definition of equality is
  now forbidden when `--without-K` is enabled:
  ```agda
    data _≡₀_ {ℓ} {A : Set ℓ} (x : A) : A → Set where
      refl : x ≡₀ x
  ```

* The termination checker now also looks for recursive calls in the type of definitions.
  This fixes an issue where Agda allowed very dependent types
  [Issue [#1556](https://github.com/agda/agda/issues/1556)].

  This change affects induction-induction, e.g.
  ```agda
    mutual
      data Cxt : Set where
        ε    :  Cxt
        _,_  :  (Γ : Cxt) (A : Ty Γ) → Cxt

      data Ty : (Γ : Cxt) → Set where
        u  :  ∀ Γ → Ty Γ
        Π  :  ∀ Γ (A : Ty Γ) (B : Ty (Γ , A)) → Ty Γ

    mutual
      f : Cxt → Cxt
      f ε        =  ε
      f (Γ , T)  =  (f Γ , g Γ T)

      g : ∀ Γ → Ty Γ → Ty (f Γ)
      g Γ (u .Γ)      =  u (f Γ)
      g Γ (Π .Γ A B)  =  Π (f Γ) (g Γ A) (g (Γ , A) B)

  ```
  The type of `g` contains a call `g Γ _ --> f Γ` which is now taken
  into account during termination checking.

Instance search
---------------

* Instance argument resolution now also applies when there are
  unconstrained metavariables in the type of the argument. For
  example, if there is a single instance `eqBool : Eq Bool` in scope,
  then an instance argument `{{eq : Eq _}}` will be solved to
  `eqBool`, setting the value of the metavariable `_` to `Bool` in the
  process.

* By default, Agda no longer allows overlapping instances. Two
  instances are defined to overlap if they could both solve the
  instance goal when given appropriate solutions for their recursive
  (instance) arguments. Agda used to choose between undecidable
  instances based on the result of recursive instance search, but this
  lead to an exponential slowdown in instance resolution. Overlapping
  instances can be enabled with the flag `--overlapping-instances`.

* Explicit arguments are no longer automatically turned into instance
  arguments for the purpose of recursive instance search. Instead,
  explicit arguments are left unresolved and will thus never be used
  for instance search.

  If an instance is declared which has explicit arguments, Agda will
  raise a warning that this instance will never be considered by
  instance search.

* Instance arguments that are already solved by conversion checking
  are no longer ignored by instance search. Thus the constructor of
  the unit type must now be explicitly be declared as an instance in
  order to be considered by instance search:
  ```agda
    record ⊤ : Set where
      instance constructor tt
  ```

* Instances are now (correctly) required to be in scope to be eligible
  (see Issue [#1913](https://github.com/agda/agda/issues/1913)
   and Issue [#2489](https://github.com/agda/agda/issues/2489)
  ).
  This means that you can no longer import instances from parameterised modules by
  ```agda
    import Some.Module Arg₁ Arg2
  ```
  without opening or naming the module.

Reflection
----------

* New TC primitive `noConstraints` [Issue
  [#2351](https://github.com/agda/agda/issues/2351)]:

  ```agda
    noConstraints : ∀ {a} {A : Set a} → TC A → TC A
  ```

  The computation `noConstraints m` fails if `m` gives rise to new,
  unsolved
  ["blocking"](https://github.com/agda/agda/blob/4900ef5fc61776381f3a5e9c94ef776375e9e1f1/src/full/Agda/TypeChecking/Monad/Constraints.hs#L160-L174)
  constraints.

* New TC primitive `runSpeculative` [Issue
  [#3346](https://github.com/agda/agda/issues/3346)]:

  ```
    runSpeculative : ∀ {a} {A : Set a} → TC (Σ A λ _ → Bool) → TC A
  ```

  The computation `runSpeculative m` runs `m` and either keeps the new
  TC state (if the second component is `true`) or resets to the old TC
  state (if it is `false`).


Interaction and error reporting
-------------------------------

* A new command `agda2-elaborate-give` (C-c C-m) normalizes a goal input
  (it respects the C-u prefixes), type checks, and inserts the normalized
  term into the goal.

* 'Solve constraints' (C-c C-s) now turns unsolved metavariables into new
  interaction holes (see Issue [#2273](https://github.com/agda/agda/issues/2273)).

* Out-of-scope identifiers are no longer prefixed by a '.' dot [Issue
  [#3127](https://github.com/agda/agda/issues/3127)].  This notation
  could be confused with dot patterns, postfix projections, and
  irrelevance. Now Agda will do its best to make up fresh names for
  out-of-scope identifiers that do not conflict with any existing
  names. In addition, these names are marked as "(out of scope)" when
  printing the context.

  The change affects the printing of terms, e.g. in error messages and
  interaction, and the parsing of out-of-scope variables for
  case splitting (`C-c C-c` in emacs).

* Shadowed local variables are now assigned fresh names in error
  messages and interactive goals [Issue
  [#572](https://github.com/agda/agda/issues/572)]. For example,
  consider the following piece of code:
  ```agda
    postulate P : Set -> Set

    test : (B : Set) -> P B -> P B
    test = λ p p -> {!!}
  ```
  When asking for the goal type, Agda will now print the following:
  ```
    Goal: P p₁
    ————————————————————————————————————————————————————————————
    p      : P p₁
    p = p₁ : Set  (not in scope)
  ```
  Shadowed top-level identifiers are printed using the qualified name,
  for example in
  ```agda
    module M where

      postulate A : Set

      test : Set → A
      test A = {!!}
  ```
  Agda will now show the goal type as
  ```
    Goal: M.A
    ————————————————————————————————————————————————————————————
    A : Set
  ```

* When case splitting (`C-c C-c` in emacs), Agda will now filter out
  impossible cases (i.e. ones where at least one of the variables
  could be replaced by an absurd pattern `()`). If all the clauses
  produced by a case split are impossible, Agda will not filter out
  any of them.

Pragmas and options
-------------------

* Consistency checking of options used.

  Agda now checks that options used in imported modules are consistent
  with each other, e.g. a module using `--safe`, `--without-K`,
  `--no-universe-polymorphism` or `--no-sized-types` may only import
  modules with the same option, and modules using `--cubical` or
  `--prop` must in turn use the same option. If an interface file has
  been generated using different options compared to the current ones,
  Agda will now re-typecheck the file.
  [Issue [#2487](https://github.com/agda/agda/issues/2487)].

* New option `--cubical` to enable Cubical Agda.

* New option `--prop` to enable the ``Prop`` sort, and `--no-prop` to
  disable it (default).

* New options `--guardedness` and `--no-guardedness` [Issue
  [#1209](https://github.com/agda/agda/issues/1209)].

  Constructor-based guarded corecursion is now only (meant to be)
  allowed if the `--guardedness` option is active. This option is
  active by default. The combination of constructor-based guarded
  corecursion and sized types is not allowed if `--safe` is used,
  and activating `--safe` turns off both `--guardedness` and
  `--sized-types` (because this combination is known to be
  inconsistent in the current implementation). If you want to use
  either constructor-based guarded corecursion or sized types in
  safe mode, then you can use `--safe --guardedness` or `--safe
  --sized-types` respectively (in this order).

  The option `--no-guardedness` turns off constructor-based guarded
  corecursion.

* Option `--irrelevant-projections` is now off by default and
  not considered `--safe` any longer.
  Reason: There are consistency issues that may be systemic
  [Issue [#2170](https://github.com/agda/agda/issues/2170)].

* New option `--no-syntactic-equality` disables the syntactic equality
  shortcut used by the conversion checker. This will slow down
  typechecking in most cases, but makes the performance more
  predictable and stable under minor changes.

* New option `--overlapping-instances` enables overlapping instances
  by performing recursive instance search during pruning of instance
  candidates (this used to be the default behaviour). Overlapping
  instances can be disabled with `--no-overlapping-instances`
  (default).

* Option (and experimental feature)
  `--guardedness-preserving-type-constructors`
  has been removed.
  [Issue [#3180](https://github.com/agda/agda/issues/3180)].

* Deprecated options `--sharing` and `--no-sharing` now raise an error.

* New primitive `primErase`. It takes a proof of equality and returns a proof of
  the same equality. `primErase eq` reduces to `refl` on the diagonal. `trustMe`
  is not a primitive anymore, it is implemented using `primErase`.

  The primitive is declared in `Agda.Builtin.Equality.Erase`.

* The `REWRITE` builtin is now bound to the builtin equality type from
  `Agda.Builtin.Equality` in `Agda.Builtin.Equality.Rewrite` [Issue
  [#3318](https://github.com/agda/agda/issues/3318)].

* New primitives `primCharToNatInjective` and `primStringToListInjective`
  internalising the fact that `primCharToNat` and `primStringtoList` are
  injective functions. They are respectively bound in `Agda.Builtin.Char.Properties`
  and `Agda.Builtin.String.Properties`.

* The option `--only-scope-checking` is now allowed together with `--safe`.

* The option `--ignore-interfaces` no longer ignores the interfaces of
  builtin and primitive modules. For experts, there is the option
  `--ignore-all-interfaces` which also rechecks builtin and primitive
  files.

* The following deprecated compiler pragmas have been removed:

  ```
    {-# COMPILED f e #-}
    {-# COMPILED_TYPE A T #-}
    {-# COMPILED_DATA A D C1 .. CN #-}
    {-# COMPILED_DECLARE_DATA #-}
    {-# COMPILED_EXPORT f g #-}
    {-# IMPORT M #-}
    {-# HASKELL code #-}
    {-# COMPILED_UHC f e #-}
    {-# COMPILED_DATA_UHC A D C1 .. CN #-}
    {-# IMPORT_UHC M #-}
    {-# COMPILED_JS f e #-}
  ```

  See the [user manual](https://agda.readthedocs.io/en/v2.6.0/language/foreign-function-interface.html)
  for how to use the `COMPILE` and `FOREIGN` pragmas that replaced these in Agda 2.5.

### New warnings

* A declaration of the form `f : A` without an accompanying definition
  is no longer an error, but instead raises a warning.

* A clause that has both an absurd pattern and a right-hand side is no
  longer an error, but instead raises a warning.

* An import statement for `M` that mentions names not exported by `M`
  (in either `using`, `hiding`, or `renaming`) is no longer an
  error. Instead, Agda will raise a warning and ignore the names.

* Pragma, primitive, module or import statements in a mutual block
  are no longer errors. Instead, Agda will raise a warning and ignore
  these statements.

### Pragmas and options concerning universes

* New pragma `{-# NO_UNIVERSE_CHECK #-}`.

  The pragma `{-# NO_UNIVERSE_CHECK #-}` can be put in front of a data
  or record type to disable universe consistency checking locally.
  Example:
  ```agda
    {-# NO_UNIVERSE_CHECK #-}
    data U : Set where
      el : Set → U
  ```
  Like the similar pragmas for disabling termination and positivity
  checking, `{-# NO_UNIVERSE_CHECK #-}` cannot be used with `--safe`.

* New builtin `SETOMEGA`.

  Agda's top sort `Setω` is now defined as a builtin in `Agda.Primitive`
  and can be renamed when importing that module.

* New option `--omega-in-omega`.

  The option `--omega-in-omega` enables the typing rule `Setω : Setω`.
  Example:
  ```agda
  {-# OPTIONS --omega-in-omega #-}
  open import Agda.Primitive

  data Type : Setω where
    el : ∀ {ℓ} → Set ℓ → Type
  ```
  Like `--type-in-type`, this makes Agda inconsistent. However, code
  written using `--omega-in-omega` is still compatible with normal
  universe-polymorphic code and can be used in such files.

Emacs mode
----------

* Jump-to-definition now works for record field names in record expressions
  and patterns. [Issue [#3120](https://github.com/agda/agda/issues/3120)]
  ```agda
    record R : Set₂ where
      field f : Set₁

    exp : R
    exp = record { f = Set }

    pat : R → R
    pat r@record { f = X } = record r { f = X }
  ```
  Jump-to-definition (`M-.` or middle-click) on any of these `f`s
  now jumps to the field declaration.

* Commas "ʻ،⸲⸴⹁⹉、︐︑﹐﹑，､" and semi-colons "؛⁏፤꛶；︔﹔⍮⸵;" added
  to the input mode.

* It is now possible to customise the highlighting of more text in
  pragmas [Issue [#2452](https://github.com/agda/agda/issues/2452)].

  Some text was already highlighted. Now there is a specific face for
  the remaining text (`agda2-highlight-pragma-face`).

LaTeX backend
-------------

* The code environment has two new options, `inline` and `inline*`.

  These options are for typesetting inline code. The implementation of
  these options is a bit of a hack. Only use these options for
  typesetting a single line of code without multiple consecutive
  whitespace characters (except at the beginning of the line).

  When the option `inline*` is used space (`\AgdaSpace{}`) is added at
  the end of the code, and when `inline` is used space is not added.

* Now highlighting commands for things like "this is an unsolved
  meta-variable" are applied on the outside of highlighting commands
  for things like "this is a postulate" [Issue
  [#2474](https://github.com/agda/agda/issues/2474)].

  Example: Instead of generating
  `\AgdaPostulate{\AgdaUnsolvedMeta{F}}` Agda now generates
  `\AgdaUnsolvedMeta{\AgdaPostulate{F}}`.

* The package `agda.sty` no longer selects any fonts, and no longer
  changes the input or font encodings [Issue
  [#3224](https://github.com/agda/agda/issues/3224)].

  The new behaviour is the same as the old behaviour with the options
  `nofontsetup` and `noinputencodingsetup`. These options have been
  removed.

  One reason for this change is that several persons have received
  complaints from reviewers because they have unwittingly used
  non-standard fonts in submitted papers. Another is that the `utf8x`
  option to `inputenc` is now deprecated.

  Note that Agda code is now less likely to typeset properly out of
  the box. See the documentation for some hints about what to do if
  this affects you.

* Some text was by default typeset in math mode when LuaLaTeX or
  XeLaTeX were used, and in text mode when pdfLaTeX was used. Now text
  mode is the default for all of these engines.

* Typesetting of pragmas should now work better [Issue
  [#2452](https://github.com/agda/agda/issues/2452)].

  The `\AgdaOption` command and `AgdaOption` colour have been replaced
  by `\AgdaPragma` and `AgdaPragma`. The `\AgdaPragma` command is used
  where `\AgdaOption` used to be used (for certain options), but also
  in other cases (for other options and certain other text in
  pragmas).

* There is no longer any special treatment of the character `-` [Issue
  [#2452](https://github.com/agda/agda/issues/2452)].

  This might, depending on things like what font your are using, mean
  that the token `--` is typeset like an en dash (–). However, this is
  not the case for at least one common monospace font (in at least one
  setting).

* The default value of `\AgdaEmptySkip` has been changed from
  `\baselineskip` to `\abovedisplayskip`. This could mean that less
  vertical space is used to render empty lines in code blocks.

HTML backend
------------

* New option `--html-highlight=[code,all,auto]`.

  The option `--html-highlight=code` makes the HTML-backend generate
  files with:

  0. No HTML footer/header
  1. Agda codes highlighted
  2. Non-Agda code parts as-is
  3. Output file extension as-is (i.e. `.lagda.md` becomes `.md`)
  4. For ReStructuredText, a `.. raw:: html\n` will be inserted
     before every code blocks

  This makes it possible to use an ordinary Markdown/ReStructuredText
  processor to render the generated HTML.

  This will affect all the files involved in one compilation, making
  pure Agda code files rendered without HTML footer/header as well.
  To use `code` with literate Agda files and `all` with pure Agda
  files, use `--html-highlight=auto`, which means auto-detection.

  The old and default behaviour is still `--html-highlight=all`.

List of all closed issues
-------------------------

For 2.6.0, the following issues have been closed
(see [bug tracker](https://github.com/agda/agda/issues)):

  -  [#572](https://github.com/agda/agda/issues/572): Shadowed identifiers should be preceded by a dot when printed
  -  [#723](https://github.com/agda/agda/issues/723): Instance search needs to know whether a meta must be a function type
  -  [#758](https://github.com/agda/agda/issues/758): No highlighting for syntax declarations
  -  [#887](https://github.com/agda/agda/issues/887): Case-split causes problems for coverage checker
  -  [#952](https://github.com/agda/agda/issues/952): Parse named implicit pi {x = y : A} -> B
  -  [#1003](https://github.com/agda/agda/issues/1003): No highlighting for ambiguous instance argument
  -  [#1063](https://github.com/agda/agda/issues/1063): Freeze metas in module telescope after checking the module?
  -  [#1086](https://github.com/agda/agda/issues/1086): Make absurd patterns not needed at toplevel
  -  [#1209](https://github.com/agda/agda/issues/1209): Guardedness checker inconsistency with copatterns
  -  [#1581](https://github.com/agda/agda/issues/1581): Fields of opened records sometimes highlighted, sometimes not
  -  [#1602](https://github.com/agda/agda/issues/1602): NonStrict arguments should be allowed to occur relevantly in the type
  -  [#1706](https://github.com/agda/agda/issues/1706): Feature request: ML-style forall-generalization
  -  [#1764](https://github.com/agda/agda/issues/1764): Type in type and universe polymorphism
  -  [#1886](https://github.com/agda/agda/issues/1886): Second copies of telescopes not checked?
  -  [#1909](https://github.com/agda/agda/issues/1909): parameters are not dropped from reflected pattern lambda
  -  [#1913](https://github.com/agda/agda/issues/1913): Names that are not in scope can sometimes be candidates for instance resolution
  -  [#1995](https://github.com/agda/agda/issues/1995): Correct names in goal types after multiple renaming imports.
  -  [#2044](https://github.com/agda/agda/issues/2044): Better diagnosis for failed instance search
  -  [#2089](https://github.com/agda/agda/issues/2089): ''No such module'' is a rude error message for private modules
  -  [#2153](https://github.com/agda/agda/issues/2153): PDF version of Language Documentation on readthedocs lacks most Unicode characters
  -  [#2273](https://github.com/agda/agda/issues/2273): C-c C-s should put new goals instead of underscores for unknown subterms
  -  [#2351](https://github.com/agda/agda/issues/2351): expose noConstraints to reflection framework
  -  [#2452](https://github.com/agda/agda/issues/2452): The LaTeX backend does not handle options very well
  -  [#2473](https://github.com/agda/agda/issues/2473): Don't reread the source code without checking that it is unchanged
  -  [#2487](https://github.com/agda/agda/issues/2487): Options used for different modules must be consistent with each other, and options used when loading an interface must be consistent with those used when the interface was created
  -  [#2489](https://github.com/agda/agda/issues/2489): Where clauses in functions leak instances to global instance search
  -  [#2490](https://github.com/agda/agda/issues/2490): possible non-terminating inference of instance arguments?
  -  [#2513](https://github.com/agda/agda/issues/2513): Extensible syntax for function space annotations
  -  [#2548](https://github.com/agda/agda/issues/2548): Move the "Old Reference Manual" to the current documentation
  -  [#2563](https://github.com/agda/agda/issues/2563): Improve documentation and error reporting related to instance resolution (especially unconstrained metavariables)
  -  [#2579](https://github.com/agda/agda/issues/2579): Import statements with module instantiation should not trigger an error message
  -  [#2618](https://github.com/agda/agda/issues/2618): Reflection and pattern-matching lambdas
  -  [#2670](https://github.com/agda/agda/issues/2670): Instance arguments and multi-sorted algebras
  -  [#2757](https://github.com/agda/agda/issues/2757): Proposal: split non-strict relevance into shape-irrelevance, parametricity, and runtime-irrelevance
  -  [#2760](https://github.com/agda/agda/issues/2760): Relax instance search restriction on unconstrained metas
  -  [#2774](https://github.com/agda/agda/issues/2774): Internal error with sized types
  -  [#2783](https://github.com/agda/agda/issues/2783): Make more primitive/builtin modules safe?
  -  [#2789](https://github.com/agda/agda/issues/2789): Narrow and broad options
  -  [#2791](https://github.com/agda/agda/issues/2791): More illtyped meta solutions
  -  [#2797](https://github.com/agda/agda/issues/2797): Relevance check missed for overloaded projection
  -  [#2833](https://github.com/agda/agda/issues/2833): Coverage checker splits on result too eagerly
  -  [#2837](https://github.com/agda/agda/issues/2837): The Emacs mode only handles LaTeX-based literate Agda
  -  [#2872](https://github.com/agda/agda/issues/2872): Case splitting adds a dot in front of pattern matches on Chars
  -  [#2880](https://github.com/agda/agda/issues/2880): Disallow FFI binding for defined functions when --safe is used
  -  [#2892](https://github.com/agda/agda/issues/2892): 'With' should also abstract over the type of stripped dot patterns
  -  [#2893](https://github.com/agda/agda/issues/2893): Display warnings also when an error is encountered
  -  [#2899](https://github.com/agda/agda/issues/2899): Add a warning for infix notations without corresponding fixity declaration
  -  [#2929](https://github.com/agda/agda/issues/2929): Turn "missing definition" into a warning
  -  [#2936](https://github.com/agda/agda/issues/2936): Sort warning flags alphabetically in user manual
  -  [#2939](https://github.com/agda/agda/issues/2939): make install-bin on a Mac can fail to install text-icu
  -  [#2964](https://github.com/agda/agda/issues/2964): Mismatch between order of matching in clauses and case tree; subject reduction broken
  -  [#2969](https://github.com/agda/agda/issues/2969): Module parameter is erased from dot pattern
  -  [#2979](https://github.com/agda/agda/issues/2979): Rewriting matching does not respect eta rules
  -  [#2993](https://github.com/agda/agda/issues/2993): Quadratic (failing) instance search
  -  [#3010](https://github.com/agda/agda/issues/3010): Field of opened record does not get highlighted
  -  [#3032](https://github.com/agda/agda/issues/3032): spurious meta in dot pattern
  -  [#3056](https://github.com/agda/agda/issues/3056): Matching on irrelevant variable of dependent record type should not be allowed
  -  [#3057](https://github.com/agda/agda/issues/3057): A module can export two definitions with the same name
  -  [#3068](https://github.com/agda/agda/issues/3068): Add option to turn off syntactic equality check
  -  [#3095](https://github.com/agda/agda/issues/3095): Would like to make hidden variable visible but it is created ambiguous
  -  [#3102](https://github.com/agda/agda/issues/3102): Performance regression: very slow reduction in the presence of many module parameters
  -  [#3114](https://github.com/agda/agda/issues/3114): Missing alpha-renaming when printing constraints
  -  [#3120](https://github.com/agda/agda/issues/3120): No tooltips for record field names in record expressions
  -  [#3122](https://github.com/agda/agda/issues/3122): Hidden record fields are not picked up from module in record expression
  -  [#3124](https://github.com/agda/agda/issues/3124): De Bruijn index in lhs checking error message
  -  [#3125](https://github.com/agda/agda/issues/3125): Internal error in InstanceArguments.hs:292
  -  [#3127](https://github.com/agda/agda/issues/3127): Notation for out-of-scope variables conflicts with notation for irrelevance
  -  [#3128](https://github.com/agda/agda/issues/3128): Sigma builtin not added to setup, agdai file missing.
  -  [#3130](https://github.com/agda/agda/issues/3130): Conflict between dot pattern and postfix projection
  -  [#3137](https://github.com/agda/agda/issues/3137): Preserve Markdown as-is when outputting HTML
  -  [#3138](https://github.com/agda/agda/issues/3138): Result splitter introduces pattern variable that conflicts with constructor
  -  [#3139](https://github.com/agda/agda/issues/3139): Internal error in parser
  -  [#3147](https://github.com/agda/agda/issues/3147): Non-linear as-patterns
  -  [#3152](https://github.com/agda/agda/issues/3152): `give` in a do-block inserts spurious parentheses
  -  [#3153](https://github.com/agda/agda/issues/3153): Type checker fails to infer missing signature of module parameter.
  -  [#3161](https://github.com/agda/agda/issues/3161): Case splitter produces end-of-comment
  -  [#3169](https://github.com/agda/agda/issues/3169): Doc for rewriting
  -  [#3170](https://github.com/agda/agda/issues/3170): UnicodeDeclare fails with pdflatex from TeX Live 2018
  -  [#3175](https://github.com/agda/agda/issues/3175): Instance resolution fails with defined method
  -  [#3176](https://github.com/agda/agda/issues/3176): Empty lambdas are sometimes considered definitionally equal, other times not
  -  [#3180](https://github.com/agda/agda/issues/3180): Remove feature `--guardedness-preserving-type-constructors`
  -  [#3188](https://github.com/agda/agda/issues/3188): Warnings disappear when fatal error is encountered
  -  [#3195](https://github.com/agda/agda/issues/3195): Internal error at Auto/Typecheck.hs:373
  -  [#3196](https://github.com/agda/agda/issues/3196): Turning MissingDefinition into a warning
  -  [#3200](https://github.com/agda/agda/issues/3200): Function marked as irrelevant when it isn't
  -  [#3201](https://github.com/agda/agda/issues/3201): [ warning ] AbsurdPatternRequiresNoRHS
  -  [#3205](https://github.com/agda/agda/issues/3205): [ cleanup + warning ] ModuleDoesntExport can be recovered from
  -  [#3224](https://github.com/agda/agda/issues/3224): Switch from utf8x to utf8? Make agda.sty easier to maintain?
  -  [#3235](https://github.com/agda/agda/issues/3235): Cannot pass backend flags via emacs variable `agda2-program-args`
  -  [#3247](https://github.com/agda/agda/issues/3247): Support cabal-install >= 2.4.1.0 in the Makefile
  -  [#3248](https://github.com/agda/agda/issues/3248): Max of two sizes less than i
  -  [#3253](https://github.com/agda/agda/issues/3253): [ fix ] ignore duplicate declarations of libraries
  -  [#3254](https://github.com/agda/agda/issues/3254): `cpphs` doesn't build with GHC 8.6.*
  -  [#3256](https://github.com/agda/agda/issues/3256): Internal error at src/full/Agda/TypeChecking/Reduce.hs:148
  -  [#3257](https://github.com/agda/agda/issues/3257): Anonymous top-level modules can have names with multiple components
  -  [#3258](https://github.com/agda/agda/issues/3258): Ordering the constructor names at Definition.
  -  [#3262](https://github.com/agda/agda/issues/3262): Suboptimal placement of "missing with-clauses" error
  -  [#3264](https://github.com/agda/agda/issues/3264): When refine leads to a termination error it should say so rather than "cannot refine"
  -  [#3268](https://github.com/agda/agda/issues/3268): [ haddock ] Fix haddock formatting
  -  [#3285](https://github.com/agda/agda/issues/3285): Internal error for syntax declaration
  -  [#3302](https://github.com/agda/agda/issues/3302): Multiple definitions called _ are sometimes allowed, sometimes not
  -  [#3307](https://github.com/agda/agda/issues/3307): `--no-unicode` bug: case splitting inside a pattern matching lambda still produces unicode arrows
  -  [#3309](https://github.com/agda/agda/issues/3309): Use of irrelevant arguments with copatterns and irrelevant fields
  -  [#3313](https://github.com/agda/agda/issues/3313): Add --html-highlight support for the HTML backend
  -  [#3315](https://github.com/agda/agda/issues/3315): The primErase primitive is not safe
  -  [#3318](https://github.com/agda/agda/issues/3318): Lots of primitives and builtins are not declared in the primitive/builtin modules
  -  [#3320](https://github.com/agda/agda/issues/3320): Extra indentation when code is hidden
  -  [#3323](https://github.com/agda/agda/issues/3323): Internal error with inconsistent irrelevance info between declaration and definition of data type
  -  [#3338](https://github.com/agda/agda/issues/3338): Missing Definitions not recognised in instance search
  -  [#3342](https://github.com/agda/agda/issues/3342): GHC panic on stack and GHC 7.10.3
  -  [#3344](https://github.com/agda/agda/issues/3344): Disable compilation with GHC 8.6.1
  -  [#3356](https://github.com/agda/agda/issues/3356): C-c C-s prints postfix projections by default
  -  [#3363](https://github.com/agda/agda/issues/3363): The wiki should support HTTPS
  -  [#3364](https://github.com/agda/agda/issues/3364): Funny scope error when trying to import as qualified
  -  [#3366](https://github.com/agda/agda/issues/3366): Add a command line flag to change the extension of the files generated by the HTML backend
  -  [#3368](https://github.com/agda/agda/issues/3368): Support GHC 8.6.2
  -  [#3370](https://github.com/agda/agda/issues/3370): [ fix ] < and > need to be in math mode in latex
  -  [#3371](https://github.com/agda/agda/issues/3371): Document common LaTeX backend pitfalls
  -  [#3372](https://github.com/agda/agda/issues/3372): Provide some simple LaTeX backend templates
  -  [#3373](https://github.com/agda/agda/issues/3373): Wrap HTML in `raw` directive when working with ReStructuredText
  -  [#3379](https://github.com/agda/agda/issues/3379): Adding a tutorial set in the readthedocs frontpage
  -  [#3380](https://github.com/agda/agda/issues/3380): Too much erasure in strict backends
  -  [#3394](https://github.com/agda/agda/issues/3394): Internal error in mutual block with unsolved implicit argument in termination checker
  -  [#3400](https://github.com/agda/agda/issues/3400): Obscure parse error with copattern and infix field
  -  [#3403](https://github.com/agda/agda/issues/3403): Internal error in Agda.TypeChecking.Rules.Term
  -  [#3404](https://github.com/agda/agda/issues/3404): Positivity checker marks postulates as constant in mutual block
  -  [#3407](https://github.com/agda/agda/issues/3407): Internal error at "src/full/Agda/TypeChecking/Reduce/Fast.hs:1338"
  -  [#3409](https://github.com/agda/agda/issues/3409): No error if mapping the empty type to non-empty Haskell type
  -  [#3410](https://github.com/agda/agda/issues/3410): ghc backend generates program that segfaults
  -  [#3419](https://github.com/agda/agda/issues/3419): Allow unconstrained instances & disallow overlapping instances
  -  [#3420](https://github.com/agda/agda/issues/3420): Inductive definitions live in a larger set --without-K
  -  [#3425](https://github.com/agda/agda/issues/3425): Internal error at src/full/Agda/Termination/Monad.hs:177
  -  [#3426](https://github.com/agda/agda/issues/3426): Termination checking false positive when using "where"
  -  [#3428](https://github.com/agda/agda/issues/3428): Another interal error in Substitute:72 when filling a hole
  -  [#3431](https://github.com/agda/agda/issues/3431): Rewrite rule doesn't fire during conversion checking
  -  [#3434](https://github.com/agda/agda/issues/3434): Regression related to instance resolution
  -  [#3435](https://github.com/agda/agda/issues/3435): Performance regression
  -  [#3439](https://github.com/agda/agda/issues/3439): Setω doesn’t respect --type-in-type
  -  [#3441](https://github.com/agda/agda/issues/3441): Generate Level expressions with fewer parentheses
  -  [#3442](https://github.com/agda/agda/issues/3442): Support GHC 8.6.3
  -  [#3443](https://github.com/agda/agda/issues/3443): "internal error" in Agda of December 7, 2018
  -  [#3444](https://github.com/agda/agda/issues/3444): `Setup.hs` is not generating the interface files
  -  [#3445](https://github.com/agda/agda/issues/3445): case splitting attempts to shadow constructor
  -  [#3451](https://github.com/agda/agda/issues/3451): The --no-sized-types option is broken
  -  [#3452](https://github.com/agda/agda/issues/3452): Case split on irrelevant argument goes through but is later rejected
  -  [#3454](https://github.com/agda/agda/issues/3454): Highlighting for incomplete pattern matching should be above highliting for non-exact split
  -  [#3456](https://github.com/agda/agda/issues/3456): [ new ] Injectivity of prim(NatToChar/StringToList)
  -  [#3461](https://github.com/agda/agda/issues/3461): Macro loop
  -  [#3463](https://github.com/agda/agda/issues/3463): Impossible to give certain instance arguments by name?
  -  [#3466](https://github.com/agda/agda/issues/3466): two definitionally equal terms are not equal
  -  [#3471](https://github.com/agda/agda/issues/3471): Can't install via cabal-install on current Haskell Platform
  -  [#3480](https://github.com/agda/agda/issues/3480): Parse error at EOF should be reported before EOF (especially if there is a long comment before EOF)
  -  [#3483](https://github.com/agda/agda/issues/3483): Internal error at TypeChecking/Monad/Signature.hs:732
  -  [#3485](https://github.com/agda/agda/issues/3485): [ warnings ] for empty primitive blocks
  -  [#3491](https://github.com/agda/agda/issues/3491): Internal error src/full/Agda/TypeChecking/Rules/LHS.hs:294 after pattern matching
  -  [#3498](https://github.com/agda/agda/issues/3498): Internal error in activateLoadedFileCache
  -  [#3501](https://github.com/agda/agda/issues/3501): Case split in let clause causes internal error
  -  [#3503](https://github.com/agda/agda/issues/3503): Internal error in BasicOps
  -  [#3514](https://github.com/agda/agda/issues/3514): Accidential language change in 2.5.3: hiding is now part of name when resolving hidden argument insertion
  -  [#3517](https://github.com/agda/agda/issues/3517): Option consistency checking bug
  -  [#3518](https://github.com/agda/agda/issues/3518): Performance regression
  -  [#3521](https://github.com/agda/agda/issues/3521): Documentation: fixes a plural issue in copatterns
  -  [#3526](https://github.com/agda/agda/issues/3526): Do not generate trivially impossible clause when case-splitting
  -  [#3533](https://github.com/agda/agda/issues/3533): [ fix #3526 ] Remove trivially impossible clauses from case-split
  -  [#3534](https://github.com/agda/agda/issues/3534): Problem finding higher-order instances
  -  [#3536](https://github.com/agda/agda/issues/3536): Patternmatching on coinductive record fields breaks
  -  [#3544](https://github.com/agda/agda/issues/3544): internal error @ TypeChecking/Forcing.hs:227
  -  [#3548](https://github.com/agda/agda/issues/3548): [ new ] Add support for compiling literate Org documents
  -  [#3554](https://github.com/agda/agda/issues/3554): Type checker explosion
  -  [#3561](https://github.com/agda/agda/issues/3561): fix typo: "FreBSD" => "FreeBSD"
  -  [#3566](https://github.com/agda/agda/issues/3566): Missing name when printing type of definition of a record
  -  [#3578](https://github.com/agda/agda/issues/3578): Pattern matching unifier normalizes too much
  -  [#3586](https://github.com/agda/agda/issues/3586): Internal error in ConcreteToAbstract.hs:2217
  -  [#3590](https://github.com/agda/agda/issues/3590): Superlinear time required for simple code
  -  [#3597](https://github.com/agda/agda/issues/3597): Agda loops on simple code with a record and a hole
  -  [#3600](https://github.com/agda/agda/issues/3600): Size solver complains, explicit sizes work
  -  [#3610](https://github.com/agda/agda/issues/3610): Support GHC 8.6.4
  -  [#3621](https://github.com/agda/agda/issues/3621): performance problem
  -  [#3631](https://github.com/agda/agda/issues/3631): Performance with --no-universe-polymorphism
  -  [#3638](https://github.com/agda/agda/issues/3638): Rewrite rules do not fire in goal normalization in parametrized module
  -  [#3639](https://github.com/agda/agda/issues/3639): Argument to function created by tactic is lost
  -  [#3640](https://github.com/agda/agda/issues/3640): Polarity: Size index check crashes due to wrong parameter number calculation
  -  [#3641](https://github.com/agda/agda/issues/3641): Remove old compiler pragmas
  -  [#3648](https://github.com/agda/agda/issues/3648): Agda could fail to build if a .agda-lib file exists in a parent directory
  -  [#3651](https://github.com/agda/agda/issues/3651): internal error ghc backend
  -  [#3657](https://github.com/agda/agda/issues/3657): Disable compilation with Windows and GHC 8.6.3
  -  [#3678](https://github.com/agda/agda/issues/3678): Two out-of-scope variables are given the same name
  -  [#3687](https://github.com/agda/agda/issues/3687): Show module contents (C-c C-o) prints garbled names in clause