Release notes for Agda version 2.5.1
====================================

Documentation
-------------

* There is now an official Agda User Manual:
  https://agda.readthedocs.io/

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

* Builtins and primitives are now defined in a new set of modules available to
  all users, independent of any particular library. The modules are

  ```agda
  Agda.Builtin.Bool
  Agda.Builtin.Char
  Agda.Builtin.Coinduction
  Agda.Builtin.Equality
  Agda.Builtin.Float
  Agda.Builtin.FromNat
  Agda.Builtin.FromNeg
  Agda.Builtin.FromString
  Agda.Builtin.IO
  Agda.Builtin.Int
  Agda.Builtin.List
  Agda.Builtin.Nat
  Agda.Builtin.Reflection
  Agda.Builtin.Size
  Agda.Builtin.Strict
  Agda.Builtin.String
  Agda.Builtin.TrustMe
  Agda.Builtin.Unit
  ```

  The standard library reexports the primitives from the new modules.

  The `Agda.Builtin` modules are installed in the same way as
  `Agda.Primitive`, but unlike `Agda.Primitive` they are not loaded
  automatically.

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

* Library management

  There is a new 'library' concept for managing include paths. A library
  consists of
    - a name,
    - a set of libraries it depends on, and
    - a set of include paths.

  A library is defined in a `.agda-lib` file using the following
  format:

  ```
  name: LIBRARY-NAME  -- Comment
  depend: LIB1 LIB2
    LIB3
    LIB4
  include: PATH1
    PATH2
    PATH3
  ```

  Dependencies are library names, not paths to `.agda-lib` files, and
  include paths are relative to the location of the library-file.

  To be useable, a library file has to be listed (with its full path)
  in `AGDA_DIR/libraries` (or `AGDA_DIR/libraries-VERSION`, for a
  given Agda version). `AGDA_DIR` defaults to `~/.agda` on Unix-like
  systems and `C:/Users/USERNAME/AppData/Roaming/agda` or similar on
  Windows, and can be overridden by setting the `AGDA_DIR` environment
  variable.

  Environment variables in the paths (of the form `$VAR` or `${VAR}`)
  are expanded. The location of the libraries file used can be
  overridden using the `--library-file=FILE` flag, although this is
  not expected to be very useful.

  You can find out the precise location of the 'libraries' file by
  calling `agda -l fjdsk Dummy.agda` and looking at the error message
  (assuming you don't have a library called fjdsk installed).

  There are three ways a library gets used:

    - You supply the `--library=LIB` (or `-l LIB`) option to
      Agda. This is equivalent to adding a `-iPATH` for each of the
      include paths of `LIB` and its (transitive) dependencies.

    - No explicit `--library` flag is given, and the current project
      root (of the Agda file that is being loaded) or one of its
      parent directories contains a `.agda-lib` file defining a
      library `LIB`. This library is used as if a `--librarary=LIB`
      option had been given, except that it is not necessary for the
      library to be listed in the `AGDA_DIR/libraries` file.

    - No explicit `--library` flag, and no `.agda-lib` file in the
      project root. In this case the file `AGDA_DIR/defaults` is read
      and all libraries listed are added to the path. The defaults
      file should contain a list of library names, each on a separate
      line. In this case the current directory is also added to the
      path.

      To disable default libraries, you can give the flag
      `--no-default-libraries`.

  Library names can end with a version number (for instance,
  `mylib-1.2.3`). When resolving a library name (given in a `--library`
  flag, or listed as a default library or library dependency) the
  following rules are followed:

    - If you don't give a version number, any version will do.

    - If you give a version number an exact match is required.

    - When there are multiple matches an exact match is preferred, and
      otherwise the latest matching version is chosen.

  For example, suppose you have the following libraries installed:
  `mylib`, `mylib-1.0`, `otherlib-2.1`, and `otherlib-2.3`. In this
  case, aside from the exact matches you can also say
  `--library=otherlib` to get `otherlib-2.3`.

* New Pragma `COMPILED_DECLARE_DATA` for binding recursively defined
  Haskell data types to recursively defined Agda data types.

  If you have a Haskell type like

  ```haskell
  {-# LANGUAGE GADTs #-}

  module Issue223 where

  data A where
    BA :: B -> A

  data B where
    AB :: A -> B
    BB :: B
  ```

  You can now bind it to corresponding mutual Agda inductive data
  types as follows:

  ```agda
  {-# IMPORT Issue223 #-}

  data A : Set
  {-# COMPILED_DECLARE_DATA A Issue223.A #-}
  data B : Set
  {-# COMPILED_DECLARE_DATA B Issue223.B #-}

  data A where
    BA : B → A

  {-# COMPILED_DATA A Issue223.A Issue223.BA #-}
  data B where
    AB : A → B
    BB : B

  {-# COMPILED_DATA B Issue223.B Issue223.AB Issue223.BB #-}
  ```

  This fixes Issue [#223](https://github.com/agda/agda/issues/223).

* New pragma `HASKELL` for adding inline Haskell code (GHC backend only)

  Arbitrary Haskell code can be added to a module using the `HASKELL`
  pragma. For instance,

  ```agda
  {-# HASKELL
    echo :: IO ()
    echo = getLine >>= putStrLn
  #-}

  postulate echo : IO ⊤
  {-# COMPILED echo echo #-}
  ```

* New option `--exact-split`.

  The `--exact-split` flag causes Agda to raise an error whenever a
  clause in a definition by pattern matching cannot be made to hold
  definitionally (i.e. as a reduction rule). Specific clauses can be
  excluded from this check by means of the `{-# CATCHALL #-}` pragma.

  For instance, the following definition will be rejected as the second clause
  cannot be made to hold definitionally:

  ```agda
  min : Nat → Nat → Nat
  min zero    y       = zero
  min x       zero    = zero
  min (suc x) (suc y) = suc (min x y
  ```

  Catchall clauses have to be marked as such, for instance:

  ```agda
  eq : Nat → Nat → Bool
  eq zero    zero    = true
  eq (suc m) (suc n) = eq m n
  {-# CATCHALL #-}
  eq _       _       = false
  ```

* New option: `--no-exact-split`.

  This option can be used to override a global `--exact-split` in a
  file, by adding a pragma `{-# OPTIONS --no-exact-split #-}`.

* New options: `--sharing` and `--no-sharing`.

  These options are used to enable/disable sharing and call-by-need
  evaluation.  The default is `--no-sharing`.

  Note that they cannot appear in an `OPTIONS` pragma, but have to be
  given as command line arguments or added to the Agda Program Args
  from Emacs with `M-x customize-group agda2`.

* New pragma `DISPLAY`.

  ```agda
  {-# DISPLAY f e1 .. en = e #-}
  ```

  This causes `f e1 .. en` to be printed in the same way as `e`, where
  `ei` can bind variables used in `e`. The expressions `ei` and `e`
  are scope checked, but not type checked.

  For example this can be used to print overloaded (instance) functions with
  the overloaded name:

  ```agda
  instance
    NumNat : Num Nat
    NumNat = record { ..; _+_ = natPlus }

  {-# DISPLAY natPlus a b = a + b #-}
  ```

  Limitations

  - Left-hand sides are restricted to variables, constructors, defined
    functions or types, and literals. In particular, lambdas are not
    allowed in left-hand sides.

  - Since `DISPLAY` pragmas are not type checked implicit argument
    insertion may not work properly if the type of `f` computes to an
    implicit function space after pattern matching.

* Removed pragma `{-# ETA R #-}`

  The pragma `{-# ETA R #-}` is replaced by the `eta-equality` directive
  inside record declarations.

* New option `--no-eta-equality`.

  The `--no-eta-equality` flag disables eta rules for declared record
  types.  It has the same effect as `no-eta-equality` inside each
  declaration of a record type `R`.

  If used with the `OPTIONS` pragma it will not affect records defined
  in other modules.

* The semantics of `{-# REWRITE r #-}` pragmas in parametrized modules
  has changed (see
  Issue [#1652](https://github.com/agda/agda/issues/1652)).

  Rewrite rules are no longer lifted to the top context. Instead, they
  now only apply to terms in (extensions of) the module context. If
  you want the old behaviour, you should put the `{-# REWRITE r #-}`
  pragma outside of the module (i.e. unindent it).

* New pragma `{-# INLINE f #-}` causes `f` to be inlined during
  compilation.

* The `STATIC` pragma is now taken into account during compilation.

  Calls to a function marked `STATIC` are normalised before
  compilation. The typical use case for this is to mark the
  interpreter of an embedded language as `STATIC`.

* Option `--type-in-type` no longer implies
  `--no-universe-polymorphism`, thus, it can be used with explicit
  universe
  levels. [Issue [#1764](https://github.com/agda/agda/issues/1764)] It
  simply turns off error reporting for any level mismatch now.
  Examples:

  ```agda
  {-# OPTIONS --type-in-type #-}

  Type : Set
  Type = Set

  data D {α} (A : Set α) : Set where
    d : A → D A

  data E α β : Set β where
    e : Set α → E α β
  ```

* New `NO_POSITIVITY_CHECK` pragma to switch off the positivity checker
  for data/record definitions and mutual blocks.

  The pragma must precede a data/record definition or a mutual block.

  The pragma cannot be used in `--safe` mode.

  Examples (see `Issue1614*.agda` and `Issue1760*.agda` in
  `test/Succeed/`):

  1. Skipping a single data definition.

     ```agda
     {-# NO_POSITIVITY_CHECK #-}
     data D : Set where
       lam : (D → D) → D
     ```

  2. Skipping a single record definition.

     ```agda
     {-# NO_POSITIVITY_CHECK #-}
     record U : Set where
       field ap : U → U
     ```

  3. Skipping an old-style mutual block: Somewhere within a `mutual`
     block before a data/record definition.

     ```agda
     mutual
       data D : Set where
         lam : (D → D) → D

       {-# NO_POSITIVITY_CHECK #-}
       record U : Set where
         field ap : U → U
     ```

  4. Skipping an old-style mutual block: Before the `mutual` keyword.

     ```agda
     {-# NO_POSITIVITY_CHECK #-}
     mutual
       data D : Set where
         lam : (D → D) → D

       record U : Set where
         field ap : U → U
     ```

  5. Skipping a new-style mutual block: Anywhere before the
     declaration or the definition of data/record in the block.

     ```agda
     record U : Set
     data D   : Set

     record U where
       field ap : U → U

     {-# NO_POSITIVITY_CHECK #-}
     data D where
       lam : (D → D) → D
     ```

* Removed `--no-coverage-check`
  option. [Issue [#1918](https://github.com/agda/agda/issues/1918)]

Language
--------

### Operator syntax

* The default fixity for syntax declarations has changed from -666 to 20.

* Sections.

  Operators can be sectioned by replacing arguments with underscores.
  There must not be any whitespace between these underscores and the
  adjacent nameparts. Examples:

  ```agda
  pred : ℕ → ℕ
  pred = _∸ 1

  T : Bool → Set
  T = if_then ⊤ else ⊥

  if : {A : Set} (b : Bool) → A → A → A
  if b = if b then_else_
  ```

  Sections are translated into lambda expressions. Examples:

  ```agda
  _∸ 1              ↦  λ section → section ∸ 1

  if_then ⊤ else ⊥  ↦  λ section → if section then ⊤ else ⊥

  if b then_else_   ↦  λ section section₁ →
                           if b then section else section₁
  ```

  Operator sections have the same fixity as the underlying operator
  (except in cases like `if b then_else_`, in which the section is
  "closed", but the operator is not).

  Operator sections are not supported in patterns (with the exception
  of dot patterns), and notations coming from syntax declarations
  cannot be sectioned.

* A long-standing operator fixity bug has been fixed. As a consequence
  some programs that used to parse no longer do.

  Previously each precedence level was (incorrectly) split up into
  five separate ones, ordered as follows, with the earlier ones
  binding less tightly than the later ones:

    - Non-associative operators.

    - Left associative operators.

    - Right associative operators.

    - Prefix operators.

    - Postfix operators.

  Now this problem has been addressed. It is no longer possible to mix
  operators of a given precedence level but different associativity.
  However, prefix and right associative operators are seen as having
  the same associativity, and similarly for postfix and left
  associative operators.

  Examples
  --------

  The following code is no longer accepted:

  ```agda
  infixl 6 _+_
  infix  6 _∸_

  rejected : ℕ
  rejected = 1 + 0 ∸ 1
  ```

  However, the following previously rejected code is accepted:

  ```agda
  infixr 4 _,_
  infix  4 ,_

  ,_ : {A : Set} {B : A → Set} {x : A} → B x → Σ A B
  , y = _ , y

  accepted : Σ ℕ λ i → Σ ℕ λ j → Σ (i ≡ j) λ _ → Σ ℕ λ k → j ≡ k
  accepted = 5 , , refl , , refl
  ```

* The classification of notations with binders into the categories
  infix, prefix, postfix or closed has
  changed. [Issue [#1450](https://github.com/agda/agda/issues/1450)]

  The difference is that, when classifying the notation, only
  *regular* holes are taken into account, not *binding* ones.

  Example: The notation

  ```agda
  syntax m >>= (λ x → f) = x <- m , f
  ```

  was previously treated as infix, but is now treated as prefix.

* Notation can now include wildcard binders.

  Example: `syntax Σ A (λ _ → B) = A × B`

* If an overloaded operator is in scope with several distinct
  precedence levels, then several instances of this operator will be
  included in the operator grammar, possibly leading to ambiguity.
  Previously the operator was given the default fixity
  [Issue [#1436](https://github.com/agda/agda/issues/1436)].

  There is an exception to this rule: If there are multiple precedences,
  but at most one is explicitly declared, then only one instance will be
  included in the grammar. If there are no explicitly declared
  precedences, then this instance will get the default precedence, and
  otherwise it will get the declared precedence.

  If multiple occurrences of an operator are "merged" in the grammar,
  and they have distinct associativities, then they are treated as
  being non-associative.

  The three paragraphs above also apply to identical notations (coming
  from syntax declarations) for a given overloaded name.

  Examples:

  ```agda
  module A where

    infixr 5 _∷_
    infixr 5 _∙_
    infixl 3 _+_
    infix  1 bind

    syntax bind c (λ x → d) = x ← c , d

  module B where

    infix  5 _∷_
    infixr 4 _∙_
    -- No fixity declaration for _+_.
    infixl 2 bind

    syntax bind c d = c ∙ d

  module C where

    infixr 2 bind

    syntax bind c d = c ∙ d

  open A
  open B
  open C

  -- _∷_ is infix 5.
  -- _∙_ has two fixities: infixr 4 and infixr 5.
  -- _+_ is infixl 3.
  -- A.bind's notation is infix 1.
  -- B.bind and C.bind's notations are infix 2.

  -- There is one instance of "_ ∷ _" in the grammar, and one
  -- instance of "_ + _".

  -- There are three instances of "_ ∙ _" in the grammar, one
  -- corresponding to A._∙_, one corresponding to B._∙_, and one
  -- corresponding to both B.bind and C.bind.
  ```

### Reflection

* The reflection framework has received a massive overhaul.

  A new type of reflected type checking computations supplants most of
  the old reflection primitives. The `quoteGoal`, `quoteContext` and
  tactic primitives are deprecated and will be removed in the future,
  and the `unquoteDecl` and `unquote` primitives have changed
  behaviour. Furthermore the following primitive functions have been
  replaced by builtin type checking computations:

  ```agda
  - primQNameType              --> AGDATCMGETTYPE
  - primQNameDefinition        --> AGDATCMGETDEFINITION
  - primDataConstructors       --> subsumed by AGDATCMGETDEFINITION
  - primDataNumberOfParameters --> subsumed by AGDATCMGETDEFINITION
  ```

  See below for details.

* Types are no longer packaged with a sort.

  The `AGDATYPE` and `AGDATYPEEL` built-ins have been
  removed. Reflected types are now simply terms.

* Reflected definitions have more information.

  The type for reflected definitions has changed to

  ```agda
  data Definition : Set where
    fun-def     : List Clause  → Definition
    data-type   : Nat → List Name → Definition -- parameters and constructors
    record-type : Name → Definition            -- name of the data/record type
    data-con    : Name → Definition            -- name of the constructor
    axiom       : Definition
    prim-fun    : Definition
  ```

  Correspondingly the built-ins for function, data and record
  definitions (`AGDAFUNDEF`, `AGDAFUNDEFCON`, `AGDADATADEF`,
  `AGDARECORDDEF`) have been removed.

* Reflected type checking computations.

  There is a primitive `TC` monad representing type checking
  computations. The `unquote`, `unquoteDecl`, and the new `unquoteDef`
  all expect computations in this monad (see below). The interface to
  the monad is the following

  ```agda
  -- Error messages can contain embedded names and terms.
  data ErrorPart : Set where
    strErr  : String → ErrorPart
    termErr : Term → ErrorPart
    nameErr : Name → ErrorPart

  {-# BUILTIN AGDAERRORPART       ErrorPart #-}
  {-# BUILTIN AGDAERRORPARTSTRING strErr    #-}
  {-# BUILTIN AGDAERRORPARTTERM   termErr   #-}
  {-# BUILTIN AGDAERRORPARTNAME   nameErr   #-}

  postulate
    TC         : ∀ {a} → Set a → Set a
    returnTC   : ∀ {a} {A : Set a} → A → TC A
    bindTC     : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B

    -- Unify two terms, potentially solving metavariables in the process.
    unify      : Term → Term → TC ⊤

    -- Throw a type error. Can be caught by catchTC.
    typeError  : ∀ {a} {A : Set a} → List ErrorPart → TC A

    -- Block a type checking computation on a metavariable. This will abort
    -- the computation and restart it (from the beginning) when the
    -- metavariable is solved.
    blockOnMeta : ∀ {a} {A : Set a} → Meta → TC A

    -- Backtrack and try the second argument if the first argument throws a
    -- type error.
    catchTC    : ∀ {a} {A : Set a} → TC A → TC A → TC A

    -- Infer the type of a given term
    inferType  : Term → TC Type

    -- Check a term against a given type. This may resolve implicit arguments
    -- in the term, so a new refined term is returned. Can be used to create
    -- new metavariables: newMeta t = checkType unknown t
    checkType  : Term → Type → TC Term

    -- Compute the normal form of a term.
    normalise  : Term → TC Term

    -- Get the current context.
    getContext : TC (List (Arg Type))

    -- Extend the current context with a variable of the given type.
    extendContext : ∀ {a} {A : Set a} → Arg Type → TC A → TC A

    -- Set the current context.
    inContext     : ∀ {a} {A : Set a} → List (Arg Type) → TC A → TC A

    -- Quote a value, returning the corresponding Term.
    quoteTC : ∀ {a} {A : Set a} → A → TC Term

    -- Unquote a Term, returning the corresponding value.
    unquoteTC : ∀ {a} {A : Set a} → Term → TC A

    -- Create a fresh name.
    freshName  : String → TC QName

    -- Declare a new function of the given type. The function must be defined
    -- later using 'defineFun'. Takes an Arg Name to allow declaring instances
    -- and irrelevant functions. The Visibility of the Arg must not be hidden.
    declareDef : Arg QName → Type → TC ⊤

    -- Define a declared function. The function may have been declared using
    -- 'declareDef' or with an explicit type signature in the program.
    defineFun  : QName → List Clause → TC ⊤

    -- Get the type of a defined name. Replaces 'primQNameType'.
    getType    : QName → TC Type

    -- Get the definition of a defined name. Replaces 'primQNameDefinition'.
    getDefinition : QName → TC Definition

  {-# BUILTIN AGDATCM                   TC                 #-}
  {-# BUILTIN AGDATCMRETURN             returnTC           #-}
  {-# BUILTIN AGDATCMBIND               bindTC             #-}
  {-# BUILTIN AGDATCMUNIFY              unify              #-}
  {-# BUILTIN AGDATCMNEWMETA            newMeta            #-}
  {-# BUILTIN AGDATCMTYPEERROR          typeError          #-}
  {-# BUILTIN AGDATCMBLOCKONMETA        blockOnMeta        #-}
  {-# BUILTIN AGDATCMCATCHERROR         catchTC            #-}
  {-# BUILTIN AGDATCMINFERTYPE          inferType          #-}
  {-# BUILTIN AGDATCMCHECKTYPE          checkType          #-}
  {-# BUILTIN AGDATCMNORMALISE          normalise          #-}
  {-# BUILTIN AGDATCMGETCONTEXT         getContext         #-}
  {-# BUILTIN AGDATCMEXTENDCONTEXT      extendContext      #-}
  {-# BUILTIN AGDATCMINCONTEXT          inContext          #-}
  {-# BUILTIN AGDATCMQUOTETERM          quoteTC            #-}
  {-# BUILTIN AGDATCMUNQUOTETERM        unquoteTC          #-}
  {-# BUILTIN AGDATCMFRESHNAME          freshName          #-}
  {-# BUILTIN AGDATCMDECLAREDEF         declareDef         #-}
  {-# BUILTIN AGDATCMDEFINEFUN          defineFun          #-}
  {-# BUILTIN AGDATCMGETTYPE            getType            #-}
  {-# BUILTIN AGDATCMGETDEFINITION      getDefinition      #-}
  ```

* Builtin type for metavariables

  There is a new builtin type for metavariables used by the new reflection
  framework. It is declared as follows and comes with primitive equality,
  ordering and show.

  ```agda
  postulate Meta : Set
  {-# BUILTIN AGDAMETA Meta #-}
  primitive primMetaEquality : Meta → Meta → Bool
  primitive primMetaLess : Meta → Meta → Bool
  primitive primShowMeta : Meta → String
  ```

  There are corresponding new constructors in the `Term` and `Literal`
  data types:

  ```agda
  data Term : Set where
    ...
    meta : Meta → List (Arg Term) → Term

  {-# BUILTIN AGDATERMMETA meta #-}

  data Literal : Set where
    ...
    meta : Meta → Literal

  {-# BUILTIN AGDALITMETA meta #-}
  ```

* Builtin unit type

  The type checker needs to know about the unit type, which you can
  allow by

  ```agda
  record ⊤ : Set where
  {-# BUILTIN UNIT ⊤ #-}
  ```

* Changed behaviour of `unquote`

  The `unquote` primitive now expects a type checking computation
  instead of a pure term. In particular `unquote e` requires

  ```agda
  e : Term → TC ⊤
  ```

  where the argument is the representation of the hole in which the
  result should go. The old `unquote` behaviour (where `unquote`
  expected a `Term` argument) can be recovered by

  ```agda
  OLD: unquote v
  NEW: unquote λ hole → unify hole v
  ```

* Changed behaviour of `unquoteDecl`

  The `unquoteDecl` primitive now expects a type checking computation
  instead of a pure function definition. It is possible to define
  multiple (mutually recursive) functions at the same time. More
  specifically

  ```agda
  unquoteDecl x₁ .. xₙ = m
  ```

  requires `m : TC ⊤` and that `x₁ .. xₙ` are defined (using
  `declareDef` and `defineFun`) after executing `m`. As before `x₁
  .. xₙ : QName` in `m`, but have their declared types outside the
  `unquoteDecl`.

* New primitive `unquoteDef`

  There is a new declaration

  ```agda
  unquoteDef x₁ .. xₙ = m
  ```

  This works exactly as `unquoteDecl` (see above) with the exception
  that `x₁ ..  xₙ` are required to already be declared.

  The main advantage of `unquoteDef` over `unquoteDecl` is that
  `unquoteDef` is allowed in mutual blocks, allowing mutually
  recursion between generated definitions and hand-written
  definitions.

* The reflection interface now exposes the name hint (as a string)
  for variables. As before, the actual binding structure is with
  de Bruijn indices. The String value is just a hint used as a prefix
  to help display the variable. The type `Abs` is a new builtin type used
  for the constructors `Term.lam`, `Term.pi`, `Pattern.var`
  (bultins `AGDATERMLAM`, `AGDATERMPI` and `AGDAPATVAR`).

  ```agda
  data Abs (A : Set) : Set where
    abs : (s : String) (x : A) → Abs A
  {-# BUILTIN ABS    Abs #-}
  {-# BUILTIN ABSABS abs #-}
  ```

  Updated constructor types:

  ```agda
  Term.lam    : Hiding   → Abs Term → Term
  Term.pi     : Arg Type → Abs Type → Term
  Pattern.var : String   → Pattern
  ```

* Reflection-based macros

  Macros are functions of type `t1 → t2 → .. → Term → TC ⊤` that are
  defined in a `macro` block. Macro application is guided by the type
  of the macro, where `Term` arguments desugar into the `quoteTerm`
  syntax and `Name` arguments into the `quote` syntax. Arguments of
  any other type are preserved as-is. The last `Term` argument is the
  hole term given to `unquote` computation (see above).

  For example, the macro application `f u v w` where the macro `f` has
  the type `Term → Name → Bool → Term → TC ⊤` desugars into `unquote
  (f (quoteTerm u) (quote v) w)`

  Limitations:

    - Macros cannot be recursive. This can be worked around by defining the
      recursive function outside the macro block and have the macro call the
      recursive function.

  Silly example:

  ```agda
  macro
    plus-to-times : Term → Term → TC ⊤
    plus-to-times (def (quote _+_) (a ∷ b ∷ [])) hole = unify hole (def (quote _*_) (a ∷ b ∷ []))
    plus-to-times v hole = unify hole v

  thm : (a b : Nat) → plus-to-times (a + b) ≡ a * b
  thm a b = refl
  ```

  Macros are most useful when writing tactics, since they let you hide the
  reflection machinery. For instance, suppose you have a solver

  ```agda
  magic : Type → Term
  ```

  that takes a reflected goal and outputs a proof (when successful). You can
  then define the following macro

  ```agda
  macro
    by-magic : Term → TC ⊤
    by-magic hole =
      bindTC (inferType hole) λ goal →
      unify hole (magic goal)
  ```

  This lets you apply the magic tactic without any syntactic noise at all:

  ```agda
  thm : ¬ P ≡ NP
  thm = by-magic
  ```

### Literals and built-ins

* Overloaded number literals.

  You can now overload natural number literals using the new builtin
  `FROMNAT`:

  ```agda
  {-# BUILTIN FROMNAT fromNat #-}
  ```

  The target of the builtin should be a defined name. Typically you would do
  something like

  ```agda
  record Number (A : Set) : Set where
    field fromNat : Nat → A

  open Number {{...}} public

  {-# BUILTIN FROMNAT fromNat #-}
  ```

  This will cause number literals `n` to be desugared to `fromNat n`
  before type checking.

* Negative number literals.

  Number literals can now be negative. For floating point literals it
  works as expected. For integer literals there is a new builtin
  `FROMNEG` that enables negative integer literals:

  ```agda
  {-# BUILTIN FROMNEG fromNeg #-}
  ```

  This causes negative literals `-n` to be desugared to `fromNeg n`.

* Overloaded string literals.

  String literals can be overladed using the `FROMSTRING` builtin:

  ```agda
  {-# BUILTIN FROMSTRING fromString #-}
  ```

  The will cause string literals `s` to be desugared to `fromString s`
  before type checking.

* Change to builtin integers.

  The `INTEGER` builtin now needs to be bound to a datatype with two
  constructors that should be bound to the new builtins `INTEGERPOS`
  and `INTEGERNEGSUC` as follows:

  ```agda
  data Int : Set where
    pos    : Nat -> Int
    negsuc : Nat -> Int
  {-# BUILTIN INTEGER       Int    #-}
  {-# BUILTIN INTEGERPOS    pos    #-}
  {-# BUILTIN INTEGERNEGSUC negsuc #-}
  ```

  where `negsuc n` represents the integer `-n - 1`. For instance, `-5`
  is represented as `negsuc 4`. All primitive functions on integers
  except `primShowInteger` have been removed, since these can be
  defined without too much trouble on the above representation using
  the corresponding functions on natural numbers.

  The primitives that have been removed are

  ```agda
  primIntegerPlus
  primIntegerMinus
  primIntegerTimes
  primIntegerDiv
  primIntegerMod
  primIntegerEquality
  primIntegerLess
  primIntegerAbs
  primNatToInteger
  ```

* New primitives for strict evaluation

  ```agda
  primitive
    primForce      : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → (∀ x → B x) → B x
    primForceLemma : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) (f : ∀ x → B x) → primForce x f ≡ f x
  ```

  `primForce x f` evaluates to `f x` if x is in weak head normal form,
  and `primForceLemma x f` evaluates to `refl` in the same
  situation. The following values are considered to be in weak head
  normal form:

    - constructor applications
    - literals
    - lambda abstractions
    - type constructor (data/record types) applications
    - function types
    - Set a

### Modules

* Modules in import directives

  When you use `using`/`hiding`/`renaming` on a name it now
  automatically applies to any module of the same name, unless you
  explicitly mention the module. For instance,

  ```agda
  open M using (D)
  ```

  is equivalent to

  ```agda
  open M using (D; module D)
  ```

  if `M` defines a module `D`. This is most useful for record and data
  types where you always get a module of the same name as the type.

  With this feature there is no longer useful to be able to qualify a
  constructor (or field) by the name of the data type even when it
  differs from the name of the corresponding module. The follow
  (weird) code used to work, but doesn't work anymore:

  ```agda
  module M where
    data D where
      c : D
  open M using (D) renaming (module D to MD)
  foo : D
  foo = D.c
  ```

  If you want to import only the type name and not the module you have to hide
  it explicitly:

  ```agda
  open M using (D) hiding (module D)
  ```

  See discussion on
  Issue [#836](https://github.com/agda/agda/issues/836).

* Private definitions of a module are no longer in scope at the Emacs
  mode top-level.

  The reason for this change is that `.agdai-files` are stripped of
  unused private definitions (which can yield significant performance
  improvements for module-heavy code).

  To test private definitions you can create a hole at the bottom of
  the module, in which private definitions will be visible.

### Records

* New record directives `eta-equality`/`no-eta-equality`

  The keywords `eta-equality`/`no-eta-equality` enable/disable eta
  rules for the (inductive) record type being declared.

  ```agda
  record Σ (A : Set) (B : A -> Set) : Set where
    no-eta-equality
    constructor _,_
    field
      fst : A
      snd : B fst
  open Σ

  -- fail : ∀ {A : Set}{B : A -> Set} → (x : Σ A B) → x ≡ (fst x , snd x)
  -- fail x = refl
  --
  -- x != fst x , snd x of type Σ .A .B
  -- when checking that the expression refl has type x ≡ (fst x , snd x)
  ```

* Building records from modules.

  The `record { <fields> }` syntax is now extended to accept module
  names as well. Fields are thus defined using the corresponding
  definitions from the given module.

  For instance assuming this record type `R` and module `M`:

  ```agda
  record R : Set where
    field
      x : X
      y : Y
      z : Z

  module M where
    x = {! ... !}
    y = {! ... !}

  r : R
  r = record { M; z = {! ... !} }
  ```

  Previously one had to write `record { x = M.x; y = M.y; z = {! ... !} }`.

  More precisely this construction now supports any combination of explicit
  field definitions and applied modules.

  If a field is both given explicitly and available in one of the modules,
  then the explicit one takes precedence.

  If a field is available in more than one module then this is ambiguous
  and therefore rejected. As a consequence the order of assignments does
  not matter.

  The modules can be both applied to arguments and have import directives
  such as `hiding`, `using`, and `renaming`. In particular this construct
  subsumes the record update construction.

  Here is an example of record update:

  ```agda
  -- Record update. Same as: record r { y = {! ... !} }
  r2 : R
  r2 = record { R r; y = {! ... !} }
  ```

  A contrived example showing the use of `hiding`/`renaming`:

  ```agda
  module M2 (a : A) where
    w = {! ... !}
    z = {! ... !}

  r3 : A → R
  r3 a = record { M hiding (y); M2 a renaming (w to y) }
  ```

* Record patterns are now accepted.

  Examples:

  ```agda
  swap : {A B : Set} (p : A × B) → B × A
  swap record{ proj₁ = a; proj₂ = b } = record{ proj₁ = b; proj₂ = a }

  thd3 : ...
  thd3 record{ proj₂ = record { proj₂ = c }} = c
  ```

* Record modules now properly hide all their parameters
  [Issue [#1759](https://github.com/agda/agda/issues/1759)]

  Previously parameters to parent modules were not hidden in the record
  module, resulting in different behaviour between

  ```agda
  module M (A : Set) where
    record R (B : Set) : Set where
  ```

  and

  ```agda
  module M where
    record R (A B : Set) : Set where
  ```

  where in the former case, `A` would be an explicit argument to the module
  `M.R`, but implicit in the latter case. Now `A` is implicit in both cases.

### Instance search

* Performance has been improved, recursive instance search which was
  previously exponential in the depth is now only quadratic.

* Constructors of records and datatypes are not anymore automatically
  considered as instances, you have to do so explicitely, for
  instance:

  ```agda
  -- only [b] is an instance of D
  data D : Set where
    a : D
    instance
      b : D
    c : D

  -- the constructor is now an instance
  record tt : Set where
    instance constructor tt
  ```

* Lambda-bound variables are no longer automatically considered
  instances.

  Lambda-bound variables need to be bound as instance arguments to be
  considered for instance search. For example,

  ```agda
  _==_ : {A : Set} {{_ : Eq A}} → A → A → Bool

  fails : {A : Set} → Eq A → A → Bool
  fails eqA x = x == x

  works : {A : Set} {{_ : Eq A}} → A → Bool
  works x = x == x
  ```

* Let-bound variables are no longer automatically considered
  instances.

  To make a let-bound variable available as an instance it needs to be
  declared with the `instance` keyword, just like top-level
  instances. For example,

  ```agda
  mkEq : {A : Set} → (A → A → Bool) → Eq A

  fails : {A : Set} → (A → A → Bool) → A → Bool
  fails eq x = let eqA = mkEq eq in x == x

  works : {A : Set} → (A → A → Bool) → A → Bool
  works eq x = let instance eqA = mkEq eq in x == x
  ```

* Record fields can be declared instances.

  For example,

  ```agda
  record EqSet : Set₁ where
    field
      set : Set
      instance eq : Eq set
  ```

  This causes the projection function `eq : (E : EqSet) → Eq (set E)`
  to be considered for instance search.

* Instance search can now find arguments in variable types (but such
  candidates can only be lambda-bound variables, they can’t be
  declared as instances)

  ```agda
  module _ {A : Set} (P : A → Set) where

    postulate
      bla : {x : A} {{_ : P x}} → Set → Set

    -- Works, the instance argument is found in the context
    test :  {x : A} {{_ : P x}} → Set → Set
    test B = bla B

    -- Still forbidden, because [P] could be instantiated later to anything
    instance
     postulate
      forbidden : {x : A} → P x
  ```

* Instance search now refuses to solve constraints with unconstrained
  metavariables, since this can lead to non-termination.

  See [Issue [#1532](https://github.com/agda/agda/issues/1523)] for an
  example.

* Top-level instances are now only considered if they are in
  scope. [Issue [#1913](https://github.com/agda/agda/issues/1913)]

  Note that lambda-bound instances need not be in scope.

### Other changes

* Unicode ellipsis character is allowed for the ellipsis token `...`
  in `with` expressions.

* `Prop` is no longer a reserved word.

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

* Large indices.

  Force constructor arguments no longer count towards the size of a datatype.
  For instance, the definition of equality below is accepted.

  ```agda
  data _≡_ {a} {A : Set a} : A → A → Set where
    refl : ∀ x → x ≡ x
  ```

  This gets rid of the asymmetry that the version of equality which indexes
  only on the second argument could be small, but not the version above which
  indexes on both arguments.

* Detection of datatypes that satisfy K (i.e. sets)

  Agda will now try to detect datatypes that satisfy K when
  `--without-K` is enabled. A datatype satisfies K when it follows
  these three rules:

  - The types of all non-recursive constructor arguments should satisfy K.

  - All recursive constructor arguments should be first-order.

  - The types of all indices should satisfy K.

  For example, the types `Nat`, `List Nat`, and `x ≡ x` (where `x :
  Nat`) are all recognized by Agda as satisfying K.

* New unifier for case splitting

  The unifier used by Agda for case splitting has been completely
  rewritten. The new unifier takes a much more type-directed approach
  in order to avoid the problems in issues
  [#1406](https://github.com/agda/agda/issues/1406),
  [#1408](https://github.com/agda/agda/issues/1408),
  [#1427](https://github.com/agda/agda/issues/1427), and
  [#1435](https://github.com/agda/agda/issues/1435).

  The new unifier also has eta-equality for record types
  built-in. This should avoid unnecessary case splitting on record
  constructors and improve the performance of Agda on code that
  contains deeply nested record patterns (see issues
  [#473](https://github.com/agda/agda/issues/473),
  [#635](https://github.com/agda/agda/issues/635),
  [#1575](https://github.com/agda/agda/issues/1575),
  [#1603](https://github.com/agda/agda/issues/1603),
  [#1613](https://github.com/agda/agda/issues/1613), and
  [#1645](https://github.com/agda/agda/issues/1645)).

  In some cases, the locations of the dot patterns computed by the
  unifier did not correspond to the locations given by the user (see
  Issue [#1608](https://github.com/agda/agda/issues/1608)). This has
  now been fixed by adding an extra step after case splitting that
  checks whether the user-written patterns are compatible with the
  computed ones.

  In some rare cases, the new unifier is still too restrictive when
  `--without-K` is enabled because it cannot generalize over the
  datatype indices (yet). For example, the following code is rejected:

  ```agda
  data Bar : Set₁ where
    bar : Bar
    baz : (A : Set) → Bar

  data Foo : Bar → Set where
    foo : Foo bar

  test : foo ≡ foo → Set₁
  test refl = Set
  ```

* The aggressive behaviour of `with` introduced in 2.4.2.5 has been
  rolled back
  [Issue [#1692](https://github.com/agda/agda/issues/1692)]. With no
  longer abstracts in the types of variables appearing in the
  with-expressions. [Issue [#745](https://github.com/agda/agda/issues/745)]

  This means that the following example no longer works:

  ```agda
  fails : (f : (x : A) → a ≡ x) (b : A) → b ≡ a
  fails f b with a | f b
  fails f b | .b | refl = f b
  ```

  The `with` no longer abstracts the type of `f` over `a`, since `f`
  appears in the second with-expression `f b`. You can use a nested
  `with` to make this example work.

  This example does work again:

  ```agda
  test : ∀{A : Set}{a : A}{f : A → A} (p : f a ≡ a) → f (f a) ≡ a
  test p rewrite p = p
  ```

  After `rewrite p` the goal has changed to `f a ≡ a`, but the type
  of `p` has not been rewritten, thus, the final `p` solves the goal.

  The following, which worked in 2.4.2.5, no longer works:

  ```agda
  fails : (f : (x : A) → a ≡ x) (b : A) → b ≡ a
  fails f b rewrite f b = f b
  ```

  The rewrite with `f b : a ≡ b` is not applied to `f` as
  the latter is part of the rewrite expression `f b`.  Thus,
  the type of `f` remains untouched, and the changed goal
  `b ≡ b` is not solved by `f b`.

* When using `rewrite` on a term `eq` of type `lhs ≡ rhs`, the `lhs`
  is no longer abstracted in `rhs`
  [Issue [#520](https://github.com/agda/agda/issues/520)].  This means
  that

  ```agda
  f pats rewrite eq = body
  ```

  is more than syntactic sugar for

  ```agda
  f pats with lhs | eq
  f pats | _ | refl = body
  ```

  In particular, the following application of `rewrite` is now
  possible

  ```agda
  id : Bool → Bool
  id true  = true
  id false = false

  is-id : ∀ x → x ≡ id x
  is-id true  = refl
  is-id false = refl

  postulate
    P : Bool → Set
    b : Bool
    p : P (id b)

  proof : P b
  proof rewrite is-id b = p
  ```

  Previously, this was desugared to

  ```agda
  proof with b | is-id b
  proof | _ | refl = p
  ```

  which did not type check as `refl` does not have type `b ≡ id b`.
  Now, Agda gets the task of checking `refl : _ ≡ id b` leading to
  instantiation of `_` to `id b`.

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

* Major Bug Fixes:

  - Function clauses with different arities are now always compiled
    correctly by the GHC/UHC
    backends. (Issue [#727](https://github.com/agda/agda/issues/727))

* Co-patterns

  - The GHC/UHC backends now support co-patterns. (Issues
    [#1567](https://github.com/agda/agda/issues/1567),
    [#1632](https://github.com/agda/agda/issues/1632))

* Optimizations

  - Builtin naturals are now represented as arbitrary-precision
    Integers. See the user manual, section
    "Agda Compilers -> Optimizations" for details.

* GHC Haskell backend (MAlonzo)

  - Pragmas

    Since builtin naturals are compiled to `Integer` you can no longer
    give a `{-# COMPILED_DATA #-}` pragma for `Nat`. The same goes for
    builtin booleans, integers, floats, characters and strings which
    are now hard-wired to appropriate Haskell types.

* UHC compiler backend

  A new backend targeting the Utrecht Haskell Compiler (UHC) is
  available.  It targets the UHC Core language, and it's design is
  inspired by the Epic backend. See the user manual, section "Agda
  Compilers -> UHC Backend" for installation instructions.

  - FFI

    The UHC backend has a FFI to Haskell similar to MAlonzo's. The
    target Haskell code also needs to be compilable using UHC, which
    does not support the Haskell base library version 4.*.

    FFI pragmas for the UHC backend are not checked in any way. If the
    pragmas are wrong, bad things will happen.

  - Imports

    Additional Haskell modules can be brought into scope with the
    `IMPORT_UHC` pragma:

    ```agda
    {-# IMPORT_UHC Data.Char #-}
    ```

    The Haskell modules `UHC.Base` and `UHC.Agda.Builtins` are always in
    scope and don't need to be imported explicitly.

  - Datatypes

    Agda datatypes can be bound to Haskell datatypes as follows:

    Haskell:
    ```haskell
    data HsData a = HsCon1 | HsCon2 (HsData a)
    ```

    Agda:
    ```agda
    data AgdaData (A : Set) : Set where
      AgdaCon1 : AgdaData A
      AgdaCon2 : AgdaData A -> AgdaData A
    {-# COMPILED_DATA_UHC AgdaData HsData HsCon1 HsCon2 #-}
    ```

    The mapping has to cover all constructors of the used Haskell
    datatype, else runtime behavior is undefined!

    There are special reserved names to bind Agda datatypes to certain
    Haskell datatypes. For example, this binds an Agda datatype to
    Haskell's list datatype:

    Agda:
    ```agda
    data AgdaList (A : Set) : Set where
      Nil : AgdaList A
      Cons : A -> AgdaList A -> AgdaList A
    {-# COMPILED_DATA_UHC AgdaList __LIST__ __NIL__ __CONS__ #-}
    ```

    The following "magic" datatypes are available:

    ```
    HS Datatype | Datatype Pragma | HS Constructor | Constructor Pragma
    ()            __UNIT__          ()               __UNIT__
    List          __LIST__          (:)              __CONS__
                                    []               __NIL__
    Bool          __BOOL__          True             __TRUE__
                                    False            __FALSE__
    ```

  - Functions

    Agda postulates can be bound to Haskell functions. Similar as in
    MAlonzo, all arguments of type `Set` need to be dropped before
    calling Haskell functions. An example calling the return function:

    Agda:
    ```agda
    postulate hs-return : {A : Set} -> A -> IO A
    {-# COMPILED_UHC hs-return (\_ -> UHC.Agda.Builtins.primReturn) #-}
    ```

Emacs mode and interaction
--------------------------

* Module contents (`C-c C-o`) now also works for
  records. [See Issue [#1926](https://github.com/agda/agda/issues/1926) ]
  If you have an inferable expression of record type in an interaction
  point, you can invoke `C-c C-o` to see its fields and types.
  Example

  ```agda
  record R : Set where
    field f : A

  test : R → R
  test r = {!r!}  -- C-c C-o here
  ```

* Less aggressive error notification.

  Previously Emacs could jump to the position of an error even if the
  type-checking process was not initiated in the current buffer. Now
  this no longer happens: If the type-checking process was initiated
  in another buffer, then the cursor is moved to the position of the
  error in the buffer visiting the file (if any) and in every window
  displaying the file, but focus should not change from one file to
  another.

  In the cases where focus does change from one file to another, one
  can now use the go-back functionality to return to the previous
  position.

* Removed the `agda-include-dirs` customization parameter.

  Use `agda-program-args` with `-iDIR` or `-lLIB` instead, or add
  libraries to `~/.agda/defaults`
  (`C:/Users/USERNAME/AppData/Roaming/agda/defaults` or similar on
  Windows). See Library management, above, for more information.

Tools
-----

### LaTeX-backend

* The default font has been changed to XITS (which is part of TeX Live):

    http://www.ctan.org/tex-archive/fonts/xits/

  This font is more complete with respect to Unicode.

### agda-ghc-names

* New tool: The command

  ```
  agda-ghc-names fixprof <compile-dir> <ProgName>.prof
  ```

  converts `*.prof` files obtained from profiling runs of
  MAlonzo-compiled code to `*.agdaIdents.prof`, with the original Agda
  identifiers replacing the MAlonzo-generated Haskell identifiers.

  For usage and more details, see `src/agda-ghc-names/README.txt`.

Highlighting and textual backends
---------------------------------

* Names in import directives are now highlighted and are clickable.
  [Issue [#1714](https://github.com/agda/agda/issues/1714)] This leads
  also to nicer printing in the LaTeX and html backends.

Fixed issues
------------

See
[bug tracker (milestone 2.5.1)](https://github.com/agda/agda/issues?q=milestone%3A2.5.1+is%3Aclosed)