Release notes for Agda version 2.4.2
====================================

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

* New option: `--with-K`

  This can be used to override a global `--without-K` in a file, by
  adding a pragma `{-# OPTIONS --with-K #-}`.

* New pragma `{-# NON_TERMINATING #-}`

  This is a safer version of `NO_TERMINATION_CHECK` which doesn't
  treat the affected functions as terminating. This means that
  `NON_TERMINATING` functions do not reduce during type checking. They
  do reduce at run-time and when invoking `C-c C-n` at top-level (but
  not in a hole).

Language
--------

* Instance search is now more efficient and recursive (see
  Issue [#938](https://github.com/agda/agda/issues/938)) (but without
  termination check yet).

  A new keyword `instance` has been introduced (in the style of
  `abstract` and `private`) which must now be used for every
  definition/postulate that has to be taken into account during
  instance resolution. For example:

  ```agda
  record RawMonoid (A : Set) : Set where
    field
      nil  : A
      _++_ : A -> A -> A

  open RawMonoid {{...}}

  instance
    rawMonoidList : {A : Set} -> RawMonoid (List A)
    rawMonoidList = record { nil = []; _++_ = List._++_ }

    rawMonoidMaybe : {A : Set} {{m : RawMonoid A}} -> RawMonoid (Maybe A)
    rawMonoidMaybe {A} = record { nil = nothing ; _++_ = catMaybe }
      where
        catMaybe : Maybe A -> Maybe A -> Maybe A
        catMaybe nothing mb = mb
        catMaybe ma nothing = ma
        catMaybe (just a) (just b) = just (a ++ b)
  ```

  Moreover, each type of an instance must end in (something that reduces
  to) a named type (e.g. a record, a datatype or a postulate). This
  allows us to build a simple index structure

  ```
  data/record name  -->  possible instances
  ```

  that speeds up instance search.

  Instance search takes into account all local bindings and all global
  `instance` bindings and the search is recursive. For instance,
  searching for

  ```agda
  ? : RawMonoid (Maybe (List A))
  ```

  will consider the candidates {`rawMonoidList`, `rawMonoidMaybe`}, fail to
  unify the first one, succeeding with the second one

  ```agda
  ? = rawMonoidMaybe {A = List A} {{m = ?m}} : RawMonoid (Maybe (List A))
  ```

  and continue with goal

  ```agda
  ?m : RawMonoid (List A)
  ```

  This will then find

  ```agda
  ?m = rawMonoidList {A = A}
  ```

  and putting together we have the solution.

  Be careful that there is no termination check for now, you can
  easily make Agda loop by declaring the identity function as an
  instance. But it shouldn’t be possible to make Agda loop by only
  declaring structurally recursive instances (whatever that means).

  Additionally:

  - Uniqueness of instances is up to definitional equality (see
    Issue [#899](https://github.com/agda/agda/issues/899)).

  - Instances of the following form are allowed:

    ```agda
    EqSigma : {A : Set} {B : A → Set} {{EqA : Eq A}}
              {{EqB : {a : A} → Eq (B a)}}
              → Eq (Σ A B)
    ```

    When searching recursively for an instance of type `{a : A} → Eq
    (B a)`, a lambda will automatically be introduced and instance
    search will search for something of type `Eq (B a)` in the context
    extended by `a : A`. When searching for an instance, the `a`
    argument does not have to be implicit, but in the definition of
    `EqSigma`, instance search will only be able to use `EqB` if `a`
    is implicit.

  - There is no longer any attempt to solve irrelevant metas by instance
    search.

  - Constructors of records and datatypes are automatically added to the
    instance table.

* You can now use `quote` in patterns.

  For instance, here is a function that unquotes a (closed) natural
  number term.

  ```agda
  unquoteNat : Term → Maybe Nat
  unquoteNat (con (quote Nat.zero) [])            = just zero
  unquoteNat (con (quote Nat.suc) (arg _ n ∷ [])) = fmap suc (unquoteNat n)
  unquoteNat _                                    = nothing
  ```

* The builtin constructors `AGDATERMUNSUPPORTED` and
  `AGDASORTUNSUPPORTED` are now translated to meta variables when
  unquoting.

* New syntactic sugar `tactic e` and `tactic e | e1 | .. | en`.

  It desugars as follows and makes it less unwieldy to call
  reflection-based tactics.

  ```agda
  tactic e                --> quoteGoal g in unquote (e g)
  tactic e | e1 | .. | en --> quoteGoal g in unquote (e g) e1 .. en
  ```

  Note that in the second form the tactic function should generate a
  function from a number of new subgoals to the original goal. The
  type of `e` should be `Term -> Term` in both cases.

* New reflection builtins for literals.

  The term data type `AGDATERM` now needs an additional constructor
   `AGDATERMLIT` taking a reflected literal defined as follows (with
   appropriate builtin bindings for the types `Nat`, `Float`, etc).

  ```agda
  data Literal : Set where
    nat    : Nat    → Literal
    float  : Float  → Literal
    char   : Char   → Literal
    string : String → Literal
    qname  : QName  → Literal

  {-# BUILTIN AGDALITERAL   Literal #-}
  {-# BUILTIN AGDALITNAT    nat     #-}
  {-# BUILTIN AGDALITFLOAT  float   #-}
  {-# BUILTIN AGDALITCHAR   char    #-}
  {-# BUILTIN AGDALITSTRING string  #-}
  {-# BUILTIN AGDALITQNAME  qname   #-}
  ```

  When quoting (`quoteGoal` or `quoteTerm`) literals will be mapped to
  the `AGDATERMLIT` constructor. Previously natural number literals
  were quoted to `suc`/`zero` application and other literals were
  quoted to `AGDATERMUNSUPPORTED`.

* New reflection builtins for function definitions.

  `AGDAFUNDEF` should now map to a data type defined as follows

  (with
  ```agda
  {-# BUILTIN QNAME       QName   #-}
  {-# BUILTIN ARG         Arg     #-}
  {-# BUILTIN AGDATERM    Term    #-}
  {-# BUILTIN AGDATYPE    Type    #-}
  {-# BUILTIN AGDALITERAL Literal #-}
  ```
  ).

  ```agda
  data Pattern : Set where
    con    : QName → List (Arg Pattern) → Pattern
    dot    : Pattern
    var    : Pattern
    lit    : Literal → Pattern
    proj   : QName → Pattern
    absurd : Pattern

  {-# BUILTIN AGDAPATTERN   Pattern #-}
  {-# BUILTIN AGDAPATCON    con     #-}
  {-# BUILTIN AGDAPATDOT    dot     #-}
  {-# BUILTIN AGDAPATVAR    var     #-}
  {-# BUILTIN AGDAPATLIT    lit     #-}
  {-# BUILTIN AGDAPATPROJ   proj    #-}
  {-# BUILTIN AGDAPATABSURD absurd  #-}

  data Clause : Set where
    clause        : List (Arg Pattern) → Term → Clause
    absurd-clause : List (Arg Pattern) → Clause

  {-# BUILTIN AGDACLAUSE       Clause        #-}
  {-# BUILTIN AGDACLAUSECLAUSE clause        #-}
  {-# BUILTIN AGDACLAUSEABSURD absurd-clause #-}

  data FunDef : Set where
    fun-def : Type → List Clause → FunDef

  {-# BUILTIN AGDAFUNDEF    FunDef  #-}
  {-# BUILTIN AGDAFUNDEFCON fun-def #-}
  ```

* New reflection builtins for extended (pattern-matching) lambda.

  The `AGDATERM` data type has been augmented with a constructor

  ```agda
  AGDATERMEXTLAM : List AGDACLAUSE → List (ARG AGDATERM) → AGDATERM
  ```

  Absurd lambdas (`λ ()`) are quoted to extended lambdas with an
  absurd clause.

* Unquoting declarations.

  You can now define (recursive) functions by reflection using the new
  `unquoteDecl` declaration

  ```agda
  unquoteDecl x = e
  ```

  Here e should have type `AGDAFUNDEF` and evaluate to a closed
  value. This value is then spliced in as the definition of `x`. In
  the body `e`, `x` has type `QNAME` which lets you splice in
  recursive definitions.

  Standard modifiers, such as fixity declarations, can be applied to `x` as
  expected.

* Quoted levels

  Universe levels are now quoted properly instead of being quoted to
  `AGDASORTUNSUPPORTED`. `Setω` still gets an unsupported sort,
  however.

* Module applicants can now be operator applications.

  Example:

  ```agda
  postulate
    [_] : A -> B

  module M (b : B) where

  module N (a : A) = M [ a ]
  ```

  [See Issue [#1245](https://github.com/agda/agda/issues/1245)]

* Minor change in module application
  semantics. [Issue [#892](https://github.com/agda/agda/issues/892)]

  Previously re-exported functions were not redefined when
  instantiating a module. For instance

  ```agda
  module A where f = ...
  module B (X : Set) where
    open A public
  module C = B Nat
  ```

  In this example `C.f` would be an alias for `A.f`, so if both `A`
  and `C` were opened `f` would not be ambiguous. However, this
  behaviour is not correct when `A` and `B` share some module
  parameters
  (Issue [#892](https://github.com/agda/agda/issues/892)). To fix this
  `C` now defines its own copy of `f` (which evaluates to `A.f`),
  which means that opening `A` and `C` results in an ambiguous `f`.

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

* Recursive records need to be declared as either `inductive` or
  `coinductive`.  `inductive` is no longer default for recursive
  records. Examples:

  ```agda
  record _×_ (A B : Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B

  record Tree (A : Set) : Set where
    inductive
    constructor tree
    field
      elem     : A
      subtrees : List (Tree A)

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

  If you are using old-style (musical) coinduction, a record may have
  to be declared as inductive, paradoxically.

  ```agda
  record Stream (A : Set) : Set where
    inductive -- YES, THIS IS INTENDED !
    constructor _∷_
    field
      head : A
      tail : ∞ (Stream A)
  ```

  This is because the "coinduction" happens in the use of `∞` and not
  in the use of `record`.

Tools
-----

### Emacs mode

* A new menu option `Display` can be used to display the version of
  the running Agda process.

### LaTeX-backend

* New experimental option `references` has been added. When specified,
  i.e.:

  ```latex
  \usepackage[references]{agda}
  ```

  a new command called `\AgdaRef` is provided, which lets you
  reference previously typeset commands, e.g.:

  Let us postulate `\AgdaRef{apa}`.

  ```agda
  \begin{code}
  postulate
    apa : Set
  \end{code}
  ```

  Above `apa` will be typeset (highlighted) the same in the text as in
  the code, provided that the LaTeX output is post-processed using
  `src/data/postprocess-latex.pl`, e.g.:

  ```
  cp $(dirname $(dirname $(agda-mode locate)))/postprocess-latex.pl .
  agda -i. --latex Example.lagda
  cd latex/
  perl ../postprocess-latex.pl Example.tex > Example.processed
  mv Example.processed Example.tex
  xelatex Example.tex
  ```

  Mix-fix and Unicode should work as expected (Unicode requires
  XeLaTeX/LuaLaTeX), but there are limitations:

  - Overloading identifiers should be avoided, if multiples exist
    `\AgdaRef` will typeset according to the first it finds.

  - Only the current module is used, should you need to reference
    identifiers in other modules then you need to specify which other
    module manually, i.e. `\AgdaRef[module]{identifier}`.