Release notes for Agda version 2.5.2
====================================

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

* Modular support for literate programming

  Literate programming support has been moved out of the lexer and into the
  `Agda.Syntax.Parser.Literate` module.

  Files ending in `.lagda` are still interpreted as literate TeX.
  The extension `.lagda.tex` may now also be used for literate TeX files.

  Support for more literate code formats and extensions can be added
  modularly.

  By default, `.lagda.*` files are opened in the Emacs mode
  corresponding to their last extension.  One may switch to and from
  Agda mode manually.

* reStructuredText

  Literate Agda code can now be written in reStructuredText format, using
  the `.lagda.rst` extension.

  As a general rule, Agda will parse code following a line ending in `::`,
  as long as that line does not start with `..`. The module name must
  match the path of the file in the documentation, and must be given
  explicitly.  Several files have been converted already, for instance:

  - `language/mixfix-operators.lagda.rst`
  - `tools/compilers.lagda.rst`

  Note that:

  - Code blocks inside an rST comment block will be type-checked by Agda,
    but not rendered in the documentation.
  - Code blocks delimited by `.. code-block:: agda` will be rendered in
    the final documenation, but not type-checked by Agda.
  - All lines inside a codeblock must be further indented than the first line
    of the code block.
  - Indentation must be consistent between code blocks. In other
    words, the file as a whole must be a valid Agda file if all the
    literate text is replaced by white space.

* Documentation testing

  All documentation files in the `doc/user-manual` directory that end
  in `.lagda.rst` can be typechecked by running `make
  user-manual-test`, and also as part of the general test suite.

* Support installation through Stack

  The Agda sources now also include a configuration for the stack install tool
  (tested through continuous integration).

  It should hence be possible to repeatably build any future Agda version
  (including unreleased commits) from source by checking out that version and
  running `stack install` from the checkout directory.
  By using repeatable builds, this should keep selecting the same dependencies
  in the face of new releases on Hackage.

  For further motivation, see
  Issue [#2005](https://github.com/agda/agda/issues/2005).

* Removed the `--test` command-line option

  This option ran the internal test-suite. This test-suite was
  implemented using Cabal supports for
  test-suites. [Issue [#2083](https://github.com/agda/agda/issues/2083)].

* The `--no-default-libraries` flag has been split into two flags
  [Issue [#1937](https://github.com/agda/agda/issues/1937)]

  - `--no-default-libraries`: Ignore the defaults file but still look for local
    `.agda-lib` files
  - `--no-libraries`: Don't use any `.agda-lib` files (the previous behaviour
    of `--no-default-libraries`).

* If `agda` was built inside `git` repository, then the `--version` flag
  will display the hash of the commit used, and whether the tree was
  `-dirty` (i.e. there were uncommited changes in the working directory).
  Otherwise, only the version number is shown.

Language
--------

* Dot patterns are now optional

  Consider the following program

  ```agda
  data Vec (A : Set) : Nat → Set where
    []   : Vec A zero
    cons : ∀ n → A → Vec A n → Vec A (suc n)

  vmap : ∀ {A B} n → (A → B) → Vec A n → Vec B n
  vmap .zero    f []            = []
  vmap .(suc m) f (cons m x xs) = cons m (f x) (vmap m f xs)
  ```

  If we don't care about the dot patterns they can (and could previously) be
  replaced by wildcards:

  ```agda
  vmap : ∀ {A B} n → (A → B) → Vec A n → Vec B n
  vmap _ f []            = []
  vmap _ f (cons m x xs) = cons m (f x) (vmap m f xs)
  ```

  Now it is also allowed to give a variable pattern in place of the dot
  pattern. In this case the variable will be bound to the value of the dot
  pattern. For our example:

  ```agda
  vmap : ∀ {A B} n → (A → B) → Vec A n → Vec B n
  vmap n f []            = []
  vmap n f (cons m x xs) = cons m (f x) (vmap m f xs)
  ```

  In the first clause `n` reduces to `zero` and in the second clause
  `n` reduces to `suc m`.

* Module parameters can now be refined by pattern matching

  Previously, pattern matches that would refine a variable outside the
  current left-hand side was disallowed. For instance, the following
  would give an error, since matching on the vector would
  instantiate `n`.

  ```agda
  module _ {A : Set} {n : Nat} where
    f : Vec A n → Vec A n
    f []       = []
    f (x ∷ xs) = x ∷ xs
  ```

  Now this is no longer disallowed. Instead `n` is bound to the
  appropriate value in each clause.

* With-abstraction now abstracts also in module parameters

  The change that allows pattern matching to refine module parameters also
  allows with-abstraction to abstract in them. For instance,

  ```agda
  module _ (n : Nat) (xs : Vec Nat (n + n)) where
    f : Nat
    f with n + n
    f    | nn = ? -- xs : Vec Nat nn
  ```

  Note: Any function argument or lambda-bound variable bound outside a given
  function counts as a module parameter.

  To prevent abstraction in a parameter you can hide it inside a definition. In
  the above example,

  ```agda
  module _ (n : Nat) (xs : Vec Nat (n + n)) where

    ys : Vec Nat (n + n)
    ys = xs

    f : Nat
    f with n + n
    f    | nn = ? -- xs : Vec Nat nn, ys : Vec Nat (n + n)
  ```

* As-patterns [Issue [#78](https://github.com/agda/agda/issues/78)].

  As-patterns (`@`-patterns) are finally working and can be used to name a
  pattern. The name has the same scope as normal pattern variables (i.e. the
  right-hand side, where clause, and dot patterns). The name reduces to the
  value of the named pattern. For example::

  ```agda
  module _ {A : Set} (_<_ : A → A → Bool) where
    merge : List A → List A → List A
    merge xs [] = xs
    merge [] ys = ys
    merge xs@(x ∷ xs₁) ys@(y ∷ ys₁) =
      if x < y then x ∷ merge xs₁ ys
               else y ∷ merge xs ys₁
  ```

* Idiom brackets.

  There is new syntactic sugar for idiom brackets:

    `(| e a1 .. an |)` expands to

    `pure e <*> a1 <*> .. <*> an`

  The desugaring takes place before scope checking and only requires names
  `pure` and `_<*>_` in scope. Idiom brackets work well with operators, for
  instance

    `(| if a then b else c |)` desugars to

    `pure if_then_else_ <*> a <*> b <*> c`

  Limitations:

    - The top-level application inside idiom brackets cannot include
      implicit applications, so `(| foo {x = e} a b |)` is illegal. In
      the case `e` is pure you can write `(| (foo {x = e}) a b |)`
      which desugars to

        `pure (foo {x = e}) <*> a <*> b`

    - Binding syntax and operator sections cannot appear immediately inside
      idiom brackets.

* Layout for pattern matching lambdas.

  You can now write pattern matching lambdas using the syntax

  ```agda
  λ where false → true
          true  → false
  ```

  avoiding the need for explicit curly braces and semicolons.

* Overloaded projections
  [Issue [#1944](https://github.com/agda/agda/issues/1944)].

  Ambiguous projections are no longer a scope error.  Instead they get
  resolved based on the type of the record value they are
  eliminating.  This corresponds to constructors, which can be
  overloaded and get disambiguated based on the type they are
  introducing.  Example:

  ```agda
  module _ (A : Set) (a : A) where

  record R B : Set where
    field f : B
  open R public

  record S B : Set where
    field f : B
  open S public
  ```

  Exporting `f` twice from both `R` and `S` is now allowed.  Then,

  ```agda
  r : R A
  f r = a

  s : S A
  f s = f r
  ```

  disambiguates to:

  ```agda
  r : R A
  R.f r = a

  s : S A
  S.f s = R.f r
  ```

  If the type of the projection is known, it can also be disambiguated
  unapplied.

  ```agda
  unapplied : R A -> A
  unapplied = f
  ```

* Postfix projections
  [Issue [#1963](https://github.com/agda/agda/issues/1963)].

  Agda now supports a postfix syntax for projection application.
  This style is more in harmony with copatterns.  For example:

  ```agda
  record Stream (A : Set) : Set where
    coinductive
    field head : A
          tail : Stream A

  open Stream

  repeat : ∀{A} (a : A) → Stream A
  repeat a .head = a
  repeat a .tail = repeat a

  zipWith : ∀{A B C} (f : A → B → C) (s : Stream A) (t : Stream B) → Stream C
  zipWith f s t .head = f (s .head) (t .head)
  zipWith f s t .tail = zipWith f (s .tail) (t .tail)

  module Fib (Nat : Set) (zero one : Nat) (plus : Nat → Nat → Nat) where

    {-# TERMINATING #-}
    fib : Stream Nat
    fib .head = zero
    fib .tail .head = one
    fib .tail .tail = zipWith plus fib (fib .tail)
  ```

  The thing we eliminate with projection now is visibly the head,
  i.e., the left-most expression of the sequence (e.g. `repeat` in
  `repeat a .tail`).

  The syntax overlaps with dot patterns, but for type correct left
  hand sides there is no confusion: Dot patterns eliminate function
  types, while (postfix) projection patterns eliminate record types.

  By default, Agda prints system-generated projections (such as by
  eta-expansion or case splitting) prefix.  This can be changed with
  the new option:

  ```agda
  {-# OPTIONS --postfix-projections #-}
  ```

  Result splitting in extended lambdas (aka pattern lambdas) always
  produces postfix projections, as prefix projection pattern do not
  work here: a prefix projection needs to go left of the head, but the
  head is omitted in extended lambdas.

  ```agda
  dup : ∀{A : Set}(a : A) → A × A
  dup = λ{ a → ? }
  ```

  Result splitting (`C-c C-c RET`) here will yield:

  ```agda
  dup = λ{ a .proj₁ → ? ; a .proj₂ → ? }
  ```

* Projection parameters
  [Issue [#1954](https://github.com/agda/agda/issues/1954)].

  When copying a module, projection parameters will now stay hidden
  arguments, even if the module parameters are visible.
  This matches the situation we had for constructors since long.
  Example:

  ```agda
  module P (A : Set) where
    record R : Set where
      field f : A

  open module Q A = P A
  ```

  Parameter `A` is now hidden in `R.f`:

  ```agda
  test : ∀{A} → R A → A
  test r = R.f r
  ```

  Note that a module parameter that corresponds to the record value
  argument of a projection will not be hidden.

  ```agda
  module M (A : Set) (r : R A) where
    open R A r public

  test' : ∀{A} → R A → A
  test' r = M.f r
  ```

* Eager insertion of implicit arguments
  [Issue [#2001](https://github.com/agda/agda/issues/2001)]

  Implicit arguments are now (again) eagerly inserted in left-hand sides. The
  previous behaviour of inserting implicits for where blocks, but not
  right-hand sides was not type safe.

* Module applications can now be eta expanded/contracted without
  changing their behaviour
  [Issue #[1985](https://github.com/agda/agda/issues/1985)]

  Previously definitions exported using `open public` got the
  incorrect type for underapplied module applications.

  Example:

  ```agda
  module A where
    postulate A : Set

  module B (X : Set) where
    open A public

  module C₁ = B
  module C₂ (X : Set) = B X
  ```

  Here both `C₁.A` and `C₂.A` have type `(X : Set) → Set`.

* Polarity pragmas.

  Polarity pragmas can be attached to postulates. The polarities express
  how the postulate's arguments are used. The following polarities
  are available:

  `_`:  Unused.

  `++`: Strictly positive.

  `+`:  Positive.

  `-`:  Negative.

  `*`:  Unknown/mixed.

  Polarity pragmas have the form

  ```
  {-# POLARITY name <zero or more polarities> #-}
  ```

  and can be given wherever fixity declarations can be given. The
  listed polarities apply to the given postulate's arguments
  (explicit/implicit/instance), from left to right. Polarities
  currently cannot be given for module parameters. If the postulate
  takes n arguments (excluding module parameters), then the number of
  polarities given must be between 0 and n (inclusive).

  Polarity pragmas make it possible to use postulated type formers in
  recursive types in the following way:

  ```agda
  postulate
    ∥_∥ : Set → Set

  {-# POLARITY ∥_∥ ++ #-}

  data D : Set where
    c : ∥ D ∥ → D
  ```

  Note that one can use postulates that may seem benign, together with
  polarity pragmas, to prove that the empty type is inhabited:

  ```agda
  postulate
    _⇒_    : Set → Set → Set
    lambda : {A B : Set} → (A → B) → A ⇒ B
    apply  : {A B : Set} → A ⇒ B → A → B

  {-# POLARITY _⇒_ ++ #-}

  data ⊥ : Set where

  data D : Set where
    c : D ⇒ ⊥ → D

  not-inhabited : D → ⊥
  not-inhabited (c f) = apply f (c f)

  inhabited : D
  inhabited = c (lambda not-inhabited)

  bad : ⊥
  bad = not-inhabited inhabited
  ```

  Polarity pragmas are not allowed in safe mode.

* Declarations in a `where`-block are now
  private. [Issue [#2101](https://github.com/agda/agda/issues/2101)]
  This means that

  ```agda
  f ps = body where
    decls
  ```

  is now equivalent to

  ```agda
  f ps = body where
    private
      decls
  ```

  This changes little, since the `decls` were anyway not in scope
  outside `body`.  However, it makes a difference for abstract
  definitions, because private type signatures can see through
  abstract definitions.  Consider:

  ```agda
  record Wrap (A : Set) : Set where
    field unwrap : A

  postulate
    P : ∀{A : Set} → A → Set

  abstract

    unnamedWhere : (A : Set) → Set
    unnamedWhere A = A
      where  -- the following definitions are private!
      B : Set
      B = Wrap A

      postulate
        b : B
        test : P (Wrap.unwrap b)  -- succeeds
  ```

  The `abstract` is inherited in `where`-blocks from the parent (here:
  function `unnamedWhere`).  Thus, the definition of `B` is opaque and
  the type equation `B = Wrap A` cannot be used to check type
  signatures, not even of abstract definitions.  Thus, checking the
  type  `P (Wrap.unwrap b)` would fail.  However, if `test` is
  private, abstract definitions are translucent in its type, and
  checking succeeds.  With the implemented change, all
  `where`-definitions are private, in this case `B`, `b`, and `test`,
  and the example succeeds.

  Nothing changes for the named forms of `where`,

  ```agda
  module M where
  module _ where
  ```

  For instance, this still fails:

  ```agda
  abstract

    unnamedWhere : (A : Set) → Set
    unnamedWhere A = A
      module M where
      B : Set
      B = Wrap A

      postulate
        b : B
        test : P (Wrap.unwrap b)  -- fails
  ```

* Private anonymous modules now work as expected
  [Issue [#2199](https://github.com/agda/agda/issues/2199)]

  Previously the `private` was ignored for anonymous modules causing
  its definitions to be visible outside the module containing the
  anonymous module.  This is no longer the case. For instance,

  ```agda
  module M where
    private
      module _ (A : Set) where
        Id : Set
        Id = A

    foo : Set → Set
    foo = Id

  open M

  bar : Set → Set
  bar = Id -- Id is no longer in scope here
  ```

* Pattern synonyms are now expanded on left hand sides of DISPLAY
  pragmas [Issue [#2132](https://github.com/agda/agda/issues/2132)].
  Example:

  ```agda
  data D : Set where
    C c : D
    g : D → D

  pattern C′ = C

  {-# DISPLAY C′ = C′ #-}
  {-# DISPLAY g C′ = c #-}
  ```

  This now behaves as:

  ```agda
  {-# DISPLAY C = C′ #-}
  {-# DISPLAY g C = c #-}
  ```

  Expected error for

  ```agda
  test : C ≡ g C
  test = refl
  ```

  is thus:

  ```
  C′ != c of type D
  ```

* The built-in floats have new semantics to fix inconsistencies
  and to improve cross-platform portability.

  - Float equality has been split into two primitives.
    ``primFloatEquality`` is designed to establish
    decidable propositional equality while
    ``primFloatNumericalEquality`` is intended for numerical
    computations. They behave as follows:

    ```
    primFloatEquality NaN NaN = True
    primFloatEquality 0.0 -0.0 = False

    primFloatNumericalEquality NaN NaN = False
    primFloatNumericalEquality 0.0 -0.0 = True
    ```

    This change fixes an inconsistency, see [Issue [#2169](https://github.com/agda/agda/issues/2169)].
    For further detail see the [user manual](http://agda.readthedocs.io/en/v2.5.2/language/built-ins.html#floats).

  - Floats now have only one `NaN` value. This is necessary
    for proper Float support in the JavaScript backend,
    as JavaScript (and some other platforms) only support
    one `NaN` value.

  - The primitive function `primFloatLess` was renamed
    `primFloatNumericalLess`.

* Added new primitives to built-in floats:

  - `primFloatNegate : Float → Float`
    [Issue [#2194](https://github.com/agda/agda/issues/2194)]

  - Trigonometric primitives
    [Issue [#2200](https://github.com/agda/agda/issues/2200)]:

    ```agda
    primCos   : Float → Float
    primTan   : Float → Float
    primASin  : Float → Float
    primACos  : Float → Float
    primATan  : Float → Float
    primATan2 : Float → Float → Float
    ```

* Anonymous declarations
  [Issue [#1465](https://github.com/agda/agda/issues/1465)].

  A module can contain an arbitrary number of declarations
  named `_` which will scoped-checked and type-checked but
  won't be made available in the scope (nor exported). They
  cannot introduce arguments on the LHS (but one can use
  lambda-abstractions on the RHS) and they cannot be defined
  by recursion.

  ```agda
  _ : Set → Set
  _ = λ x → x
  ```

### Rewriting

* The REWRITE pragma can now handle several names.  E.g.:
  ```agda
  {-# REWRITE eq1 eq2 #-}
  ```

### Reflection

* You can now use macros in reflected terms
  [Issue [#2130](https://github.com/agda/agda/issues/2130)].

  For instance, given a macro

  ```agda
  macro
    some-tactic : Term → TC ⊤
    some-tactic = ...
  ```

  the term `def (quote some-tactic) []` represents a call to the
  macro. This makes it a lot easier to compose tactics.

* The reflection machinery now uses normalisation less often:

  * Macros no longer normalise the (automatically quoted) term
    arguments.

  * The TC primitives `inferType`, `checkType` and `quoteTC` no longer
    normalise their arguments.

  * The following deprecated constructions may also have been changed:
    `quoteGoal`, `quoteTerm`, `quoteContext` and `tactic`.

* New TC primitive: `withNormalisation`.

  To recover the old normalising behaviour of `inferType`, `checkType`,
  `quoteTC` and `getContext`, you can wrap them inside a call to
  `withNormalisation true`:

  ```agda
    withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A
  ```

* New TC primitive: `reduce`.

  ```agda
  reduce : Term → TC Term
  ```

  Reduces its argument to weak head normal form.

* Added new TC primitive: `isMacro`
  [Issue [#2182](https://github.com/agda/agda/issues/2182)]

  ```agda
  isMacro : Name → TC Bool
  ```

  Returns `true` if the name refers to a macro, otherwise `false`.

* The `record-type` constructor now has an extra argument containing
  information about the record type's fields:
  ```agda
    data Definition : Set where
      …
      record-type : (c : Name) (fs : List (Arg Name)) → Definition
      …
  ```

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

* Files with open metas can be imported now
  [Issue [#964](https://github.com/agda/agda/issues/964)].  This
  should make simultaneous interactive development on several modules
  more pleasant.

  Requires option: `--allow-unsolved-metas`

  Internally, before serialization, open metas are turned into postulates named

  ```
    unsolved#meta.<nnn>
  ```

  where `<nnn>` is the internal meta variable number.

* The performance of the compile-time evaluator has been greatly improved.

  - Fixed a memory leak in evaluator
    (Issue [#2147](https://github.com/agda/agda/issues/2147)).

  - Reduction speed improved by an order of magnitude and is now
    comparable to the performance of GHCi. Still call-by-name though.

* The detection of types that satisfy K added in Agda 2.5.1 has been
  rolled back (see
  Issue [#2003](https://github.com/agda/agda/issues/2003)).

* Eta-equality for record types is now only on after the positivity
  checker has confirmed it is safe to have it.  Eta-equality for
  unguarded inductive records previously lead to looping of the type
  checker.
  [See Issue [#2197](https://github.com/agda/agda/issues/2197)]

  ```agda
  record R : Set where
    inductive
    field r : R

    loops : R
    loops = ?
  ```

  As a consequence of this change, the following example does not
  type-check any more:

  ```agda
  mutual
    record ⊤ : Set where

    test : ∀ {x y : ⊤} → x ≡ y
    test = refl
  ```

  It fails because the positivity checker is only run after the mutual
  block, thus, eta-equality for `⊤` is not available when checking
  test.

  One can declare eta-equality explicitly, though, to make this
  example work.

  ```agda
  mutual
    record ⊤ : Set where
      eta-equality

    test : ∀ {x y : ⊤} → x ≡ y
    test = refl
  ```

* Records with instance fields are now eta expanded before instance search.

  For instance, assuming `Eq` and `Ord` with boolean functions `_==_` and `_<_`
  respectively,

  ```agda
    record EqAndOrd (A : Set) : Set where
      field {{eq}}  : Eq A
            {{ord}} : Ord A


    leq : {A : Set} {{_ : EqAndOrd A}} → A → A → Bool
    leq x y = x == y || x < y
  ```

  Here the `EqAndOrd` record is automatically unpacked before instance search,
  revealing the component `Eq` and `Ord` instances.

  This can be used to simulate superclass dependencies.

* Overlappable record instance fields.

  Instance fields in records can be marked as overlappable using the new
  `overlap` keyword:

  ```agda
    record Ord (A : Set) : Set where
      field
        _<_ : A → A → Bool
        overlap {{eqA}} : Eq A
  ```

  When instance search finds multiple candidates for a given instance goal and
  they are **all** overlappable it will pick the left-most candidate instead of
  refusing to solve the instance goal.

  This can be use to solve the problem arising from shared "superclass"
  dependencies. For instance, if you have, in addition to `Ord` above, a `Num`
  record that also has an `Eq` field and want to write a function requiring
  both `Ord` and `Num`, any `Eq` constraint will be solved by the `Eq` instance
  from whichever argument that comes first.

  ```agda
    record Num (A : Set) : Set where
      field
        fromNat : Nat → A
        overlap {{eqA}} : Eq A

    lessOrEqualFive : {A : Set} {{NumA : Num A}} {{OrdA : Ord A}} → A → Bool
    lessOrEqualFive x = x == fromNat 5 || x < fromNat 5
  ```

  In this example the call to `_==_` will use the `eqA` field from `NumA`
  rather than the one from `OrdA`. Note that these may well be different.

* Instance fields can be left out of copattern matches
  [Issue [#2288](https://github.com/agda/agda/issues/2288)]

  Missing cases for instance fields (marked `{{` `}}`) in copattern matches
  will be solved using instance search. This makes defining instances with
  superclass fields much nicer. For instance, we can define `Nat` instances of
  `Eq`, `Ord` and `Num` from above as follows:

  ```agda
    instance
      EqNat : Eq Nat
      _==_ {{EqNat}} n m = eqNat n m

      OrdNat : Ord Nat
      _<_ {{OrdNat}} n m = lessNat n m

      NumNat : Num Nat
      fromNat {{NumNat}} n = n
  ```

  The `eqA` fields of `Ord` and `Num` are filled in using instance search (with
  `EqNat` in this case).

* Limited instance search depth
  [Issue [#2269](https://github.com/agda/agda/issues/2269)]

  To prevent instance search from looping on bad instances
  (see [Issue #1743](https://github.com/agda/agda/issues/1743)) the search
  depth of instance search is now limited. The maximum depth can be set with
  the `--instance-search-depth` flag and the default value is `500`.

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

* New command `C-u C-u C-c C-n`: Use `show` to display the result of
  normalisation.

  Calling `C-u C-u C-c C-n` on an expression `e` (in a hole or at top level)
  normalises `show e` and prints the resulting string, or an error message if
  the expression does not normalise to a literal string.

  This is useful when working with complex data structures for which you have
  defined a nice `Show` instance.

  Note that the name `show` is hardwired into the command.

* Changed feature: Interactively split result.

  Make-case (`C-c C-c`) with no variables will now *either* introduce
  function arguments *or* do a copattern split (or fail).

  This is as before:

  ```agda
  test : {A B : Set} (a : A) (b : B) → A × B
  test a b = ?

  -- expected:
  -- proj₁ (test a b) = {!!}
  -- proj₂ (test a b) = {!!}

  testFun : {A B : Set} (a : A) (b : B) → A × B
  testFun = ?

  -- expected:
  -- testFun a b = {!!}
  ```

  This is has changed:

  ```agda
  record FunRec A : Set where
    field funField : A → A
  open FunRec

  testFunRec : ∀{A} → FunRec A
  testFunRec = ?

  -- expected (since 2016-05-03):
  -- funField testFunRec = {!!}

  -- used to be:
  -- funField testFunRec x = {!!}
  ```

* Changed feature: Split on hidden variables.

  Make-case (`C-c C-c`) will no longer split on the given hidden
  variables, but only make them visible. (Splitting can then be
  performed in a second go.)

  ```agda
  test : ∀{N M : Nat} → Nat → Nat → Nat
  test N M = {!.N N .M!}
  ```

  Invoking splitting will result in:

  ```agda
  test {N} {M} zero M₁ = ?
  test {N} {M} (suc N₁) M₁ = ?
  ```

  The hidden `.N` and `.M` have been brought into scope, the
  visible `N` has been split upon.

* Non-fatal errors/warnings.

  Non-fatal errors and warnings are now displayed in the info buffer
  and do not interrupt the typechecking of the file.

  Currently termination errors, unsolved metavariables, unsolved
  constraints, positivity errors, deprecated BUILTINs, and empty
  REWRITING pragmas are non-fatal errors.

* Highlighting for positivity check failures

  Negative occurences of a datatype in its definition are now
  highlighted in a way similar to termination errors.

* The abbrev for codata was replaced by an abbrev for code
  environments.

  If you type `c C-x '` (on a suitably standard setup), then Emacs
  will insert the following text:

  ```agda
  \begin{code}<newline>  <cursor><newline>\end{code}<newline>.
  ```

* The LaTeX backend can now be invoked from the Emacs mode.

  Using the compilation command (`C-c C-x C-c`).

  The flag `--latex-dir` can be used to set the output directory (by
  default: `latex`). Note that if this directory is a relative path,
  then it is interpreted relative to the "project root". (When the
  LaTeX backend is invoked from the command line the path is
  interpreted relative to the current working directory.) Example: If
  the module `A.B.C` is located in the file `/foo/A/B/C.agda`, then
  the project root is `/foo/`, and the default output directory is
  `/foo/latex/`.

* The compilation command (`C-c C-x C-c`) now by default asks for a
  backend.

  To avoid this question, set the customisation variable
  `agda2-backend` to an appropriate value.

* The command `agda2-measure-load-time` no longer "touches" the file,
  and the optional argument `DONT-TOUCH` has been removed.

* New command `C-u (C-u) C-c C-s`: Simplify or normalise the solution `C-c C-s` produces

  When writing examples, it is nice to have the hole filled in with
  a normalised version of the solution. Calling `C-c C-s` on

  ```agda
  _ : reverse (0 ∷ 1 ∷ []) ≡ ?
  _ = refl
  ```

  used to yield the non informative `reverse (0 ∷ 1 ∷ [])` when we would
  have hopped to get `1 ∷ 0 ∷ []` instead. We can now control finely the
  degree to which the solution is simplified.

* Changed feature: Solving the hole at point

  Calling `C-c C-s` inside a specific goal does not solve *all* the goals
  already instantiated internally anymore: it only solves the one at hand
  (if possible).

* New bindings: All the blackboard bold letters are now available
  [Pull Request [#2305](https://github.com/agda/agda/pull/2305)]

  The Agda input method only bound a handful of the blackboard bold letters
  but programmers were actually using more than these. They are now all
  available: lowercase and uppercase. Some previous bindings had to be
  modified for consistency. The naming scheme is as follows:

  * `\bx` for lowercase blackboard bold
  * `\bX` for uppercase blackboard bold
  * `\bGx` for lowercase greek blackboard bold (similar to `\Gx` for
    greeks)
  * `\bGX` for uppercase greek blackboard bold (similar to `\GX` for
    uppercase greeks)

* Replaced binding for go back

  Use `M-,` (instead of `M-*`) for go back in Emacs ≥ 25.1 (and
  continue using `M-*` with previous versions of Emacs).

Compiler backends
-----------------

* JS compiler backend

  The JavaScript backend has been (partially) rewritten. The
  JavaScript backend now supports most Agda features, notably
  copatterns can now be compiled to JavaScript. Furthermore, the
  existing optimizations from the other backends now apply to the
  JavaScript backend as well.

* GHC, JS and UHC compiler backends

  Added new primitives to built-in floats
  [Issues [#2194](https://github.com/agda/agda/issues/2194) and
  [#2200](https://github.com/agda/agda/issues/2200)]:

  ```agda
  primFloatNegate : Float → Float
  primCos         : Float → Float
  primTan         : Float → Float
  primASin        : Float → Float
  primACos        : Float → Float
  primATan        : Float → Float
  primATan2       : Float → Float → Float
  ```

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

* Code blocks are now (by default) surrounded by vertical space.
  [Issue [#2198](https://github.com/agda/agda/issues/2198)]

  Use `\AgdaNoSpaceAroundCode{}` to avoid this vertical space, and
  `\AgdaSpaceAroundCode{}` to reenable it.

  Note that, if `\AgdaNoSpaceAroundCode{}` is used, then empty lines
  before or after a code block will not necessarily lead to empty
  lines in the generated document. However, empty lines *inside* the
  code block do (by default) lead to empty lines in the output.

  If you prefer the previous behaviour, then you can use the `agda.sty`
  file that came with the previous version of Agda.

* `\AgdaHide{...}` now eats trailing spaces (using `\ignorespaces`).

* New environments: `AgdaAlign`, `AgdaSuppressSpace` and
  `AgdaMultiCode`.

  Sometimes one might want to break up a code block into multiple
  pieces, but keep code in different blocks aligned with respect to
  each other. Then one can use the `AgdaAlign` environment. Example
  usage:
  ```latex
    \begin{AgdaAlign}
    \begin{code}
      code
        code  (more code)
    \end{code}
    Explanation...
    \begin{code}
      aligned with "code"
        code  (aligned with (more code))
    \end{code}
    \end{AgdaAlign}
  ```
  Note that `AgdaAlign` environments should not be nested.

  Sometimes one might also want to hide code in the middle of a code
  block. This can be accomplished in the following way:
  ```latex
    \begin{AgdaAlign}
    \begin{code}
      visible
    \end{code}
    \AgdaHide{
    \begin{code}
      hidden
    \end{code}}
    \begin{code}
      visible
    \end{code}
    \end{AgdaAlign}
  ```
  However, the result may be ugly: extra space is perhaps inserted
  around the code blocks.

  The `AgdaSuppressSpace` environment ensures that extra space is only
  inserted before the first code block, and after the last one (but
  not if `\AgdaNoSpaceAroundCode{}` is used).

  The environment takes one argument, the number of wrapped code
  blocks (excluding hidden ones). Example usage:
  ```latex
    \begin{AgdaAlign}
    \begin{code}
      code
        more code
    \end{code}
    Explanation...
    \begin{AgdaSuppressSpace}{2}
    \begin{code}
      aligned with "code"
        aligned with "more code"
    \end{code}
    \AgdaHide{
    \begin{code}
      hidden code
    \end{code}}
    \begin{code}
        also aligned with "more code"
    \end{code}
    \end{AgdaSuppressSpace}
    \end{AgdaAlign}
  ```

  Note that `AgdaSuppressSpace` environments should not be nested.

  There is also a combined environment, `AgdaMultiCode`, that combines
  the effects of `AgdaAlign` and `AgdaSuppressSpace`.

Tools
-----

### agda-ghc-names

The `agda-ghc-names` now has its own repository at

  https://github.com/agda/agda-ghc-names

and is no longer distributed with Agda.