Version-2–3−2

  ------------------------------------------------------------------------
  -- Release notes for Agda 2 version 2.3.2
  ------------------------------------------------------------------------

  Important changes since 2.3.0:

  Installation
  ============

  * The Agda-executable package has been removed.

    The executable is now provided as part of the Agda package.

  * The Emacs mode no longer depends on haskell-mode or GHCi.

  * Compilation of Emacs mode Lisp files.

    You can now compile the Emacs mode Lisp files by running “agda-mode
    compile”. This command is run by “make install”.

    Compilation can, in some cases, give a noticeable speedup.

    WARNING: If you reinstall the Agda mode without recompiling the
    Emacs Lisp files, then Emacs may continue using the old, compiled
    files.

  Pragmas and Options
  ===================

  * The --without-K check now reconstructs constructor parameters.

    New specification of --without-K:

    If the flag is activated, then Agda only accepts certain
    case-splits. If the type of the variable to be split is D pars ixs,
    where D is a data (or record) type, pars stands for the parameters,
    and ixs the indices, then the following requirements must be
    satisfied:

    * The indices ixs must be applications of constructors (or literals)
      to distinct variables. Constructors are usually not applied to
      parameters, but for the purposes of this check constructor
      parameters are treated as other arguments.

    * These distinct variables must not be free in pars.

  * Irrelevant arguments are printed as _ by default now.  To turn on
    printing of irrelevant arguments, use option

      --show-irrelevant

  * New: Pragma NO_TERMINATION_CHECK to switch off termination checker
    for individual function definitions and mutual blocks.

    The pragma must precede a function definition or a mutual block.
    Examples (see test/succeed/NoTerminationCheck.agda):

    1. Skipping a single definition: before type signature.

         {-# NO_TERMINATION_CHECK #-}
         a : A
         a = a

    2. Skipping a single definition: before first clause.

         b : A
         {-# NO_TERMINATION_CHECK #-}
         b = b

    3. Skipping an old-style mutual block: Before ‘mutual’ keyword.

         {-# NO_TERMINATION_CHECK #-}
         mutual
           c : A
           c = d

           d : A
           d = c

    4. Skipping a new-style mutual block: Anywhere before a type
       signature or first function clause in the block

         i : A
         j : A

         i = j
         {-# NO_TERMINATION_CHECK #-}
         j = i

    The pragma cannot be used in --safe mode.

  Language
  ========

  * Let binding record patterns

      record __ (A B : Set) : Set where
        constructor _,_
        field
          fst : A
          snd : B
      open __

      let (x , (y , z)) = t
      in  u

    will now be interpreted as

      let x = fst t
          y = fst (snd t)
          z = snd (snd t)
      in  u

    Note that the type of t needs to be inferable.  If you need to provide
    a type signature, you can write the following:

      let a : …
          a = t
          (x , (y , z)) = a
      in  u

  * Pattern synonyms

    A pattern synonym is a declaration that can be used on the left hand
    side (when pattern matching) as well as the right hand side (in
    expressions). For example:

    pattern z    = zero
    pattern ss x = suc (suc x)

    f : ℕ → ℕ
    f z       = z
    f (suc z) = ss z
    f (ss n)  = n

    Pattern synonyms are implemented by substitution on the abstract
    syntax, so definitions are scope-checked but not type-checked. They
    are particularly useful for universe constructions.

  * Qualified mixfix operators

    It is now possible to use a qualified mixfix operator by qualifying the first
    part of the name. For instance

      import Data.Nat as Nat
      import Data.Bool as Bool

      two = Bool.if true then 1 Nat.+ 1 else 0

  * Sections [Issue 735].  Agda now parses anonymous modules as sections:

      module _ {a} (A : Set a) where

        data List : Set a where
          []  : List
          _∷_ : (x : A) (xs : List) → List

      module _ {a} {A : Set a} where

        _++_ : List A → List A → List A
        []       ++ ys = ys
        (x ∷ xs) ++ ys = x ∷ (xs ++ ys)

      test : List Nat
      test = (5 ∷ []) ++ (3 ∷ [])

    In general, now the syntax

      module _ parameters where
        declarations

    is accepted and has the same effect as

      private
        module M parameters where
          declarations
      open M public

    for a fresh name M.

  * Instantiating a module in an open import statement [Issue 481].  Now accepted:

      open import Path.Module args [using/hiding/renaming (…)]

    This only brings the imported identifiers from Path.Module into scope,
    not the module itself!  Consequently, the following is pointless, and raises
    an error:

      import Path.Module args [using/hiding/renaming (…)]

    You can give a private name M to the instantiated module via

      import Path.Module args as M [using/hiding/renaming (…)]
      open import Path.Module args as M [using/hiding/renaming (…)]

    Try to avoid ‘as’ as part of the arguments.  ‘as’ is not a keyword;
    the following can be legal, although slightly obfuscated Agda code:

      open import as as as as as as

  * Implicit module parameters can be given by name. E.g.

      open M {namedArg = bla}

    This feature has been introduced in Agda 2.3.0 already.

  * Multiple type signatures sharing a same type can now be written as a single
    type signature.

      one two : ℕ
      one = suc zero
      two = suc one

  Goal and error display
  ======================

  * Meta-variables that were introduced by hidden argument `arg’ are now
    printed as _arg_number instead of just _number.  [Issue 526]

  * Agda expands identifiers in anonymous modules when printing.
    Should make some goals nicer to read. [Issue 721]

  * When a module identifier is ambiguous, Agda tells you if one
    of them is a data type module.  [Issues 318, 705]

  Type checking
  =============

  * Improved coverage checker.  The coverage checker splits on
    arguments that have constructor or literal pattern, committing
    to the left-most split that makes progress.
    Consider the lookup function for vectors:

      data Fin : Nat → Set where
        zero : {n : Nat} → Fin (suc n)
        suc  : {n : Nat} → Fin n → Fin (suc n)

      data Vec (A : Set) : Nat → Set where
        []  : Vec A zero
        _∷_ : {n : Nat} → A → Vec A n → Vec A (suc n)

      _!!_ : {A : Set}{n : Nat} → Vec A n → Fin n → A
      (x ∷ xs) !! zero  = x
      (x ∷ xs) !! suc i = xs !! i

    In Agda up to 2.3.0, this definition is rejected unless we add
    an absurd clause

      [] !! ()

    This is because the coverage checker committed on splitting
    on the vector argument, even though this inevitably lead to
    failed coverage, because a case for the empty vector [] is missing.

    The improvement to the coverage checker consists on committing
    only on splits that have a chance of covering, since all possible
    constructor patterns are present.  Thus, Agda will now split
    first on the Fin argument, since cases for both zero and suc are
    present.  Then, it can split on the Vec argument, since the
    empty vector is already ruled out by instantiating n to a suc _.

  * Instance arguments resolution will now consider candidates which
    still expect hidden arguments. For example:

      record Eq (A : Set) : Set where
        field eq : A → A → Bool

      open Eq {{…}}

      eqFin : {n : ℕ} → Eq (Fin n)
      eqFin = record { eq = primEqFin }

      testFin : Bool
      testFin = eq fin1 fin2

    The type-checker will now resolve the instance argument of the eq
    function to eqFin {_}. This is only done for hidden arguments, not
    instance arguments, so that the instance search stays non-recursive.

  * Constraint solving: Upgraded Miller patterns to record patterns. [Issue 456]

    Agda now solves meta-variables that are applied to record patterns.
    A typical (but here, artificial) case is:

      record Sigma (A : Set)(B : A → Set) : Set where
        constructor _,_
        field
          fst : A
          snd : B fst

      test : (A : Set)(B : A → Set) →
        let X : Sigma A B → Sigma A B
            X = _
        in  (x : A)(y : B x) → X (x , y) ≡ (x , y)
      test A B x y = refl

    This yields a constraint of the form

      _X A B (x , y) := t[x,y]

    (with t[x,y] = (x, y)) which is not a Miller pattern.
    However, Agda now solves this as

      _X A B z := t[fst z,snd z].

  * Changed: solving recursive constraints.  [Issue 585]

    Until 2.3.0, Agda sometimes inferred values that did not pass the
    termination checker later, or would even make Agda loop.  To prevent this,
    the occurs check now also looks into the definitions of the current mutual
    block, to avoid constructing recursive solutions.  As a consequence, also
    terminating recursive solutions are no longer found automatically.

    This effects a programming pattern where the recursively computed
    type of a recursive function is left to Agda to solve.

      mutual

        T : D → Set
        T pattern1 = _
        T pattern2 = _

        f : (d : D) → T d
        f pattern1 = rhs1
        f pattern2 = rhs2

    This might no longer work from now on.
    See examples test/fail/Issue585*.agda

  * Less eager introduction of implicit parameters.  [Issue 679]

    Until Agda 2.3.0, trailing hidden parameters were introduced eagerly
    on the left hand side of a definition.  For instance, one could not
    write

      test : {A : Set} → Set
      test = \ {A} → A

    because internally, the hidden argument {A : Set} was added to the
    left-hand side, yielding

      test {_} = \ {A} → A

    which raised a type error.  Now, Agda only introduces the trailing
    implicit parameters it has to, in order to maintain uniform function
    arity.  For instance, in

      test : Bool → {A B C : Set} → Set
      test true {A}      = A
      test false {B = B} = B

    Agda will introduce parameters A and B in all clauses, but not C,
    resulting in

      test : Bool → {A B C : Set} → Set
      test true  {A} {_}     = A
      test false {_} {B = B} = B

    Note that for checking where-clauses, still all hidden trailing
    parameters are in scope.  For instance:

      id : {i : Level}{A : Set i} → A → A
      id = myId
        where myId : forall {A} → A → A
              myId x = x

    To be able to fill in the meta variable _1 in

      myId : {A : Set _1} → A → A

    the hidden parameter {i : Level} needs to be in scope.

    As a result of this more lazy introduction of implicit parameters,
    the following code now passes.

      data Unit : Set where
        unit : Unit

      T : Unit → Set
      T unit = {u : Unit} → Unit

      test : (u : Unit) → T u
      test unit with unit
      … | _ = λ {v} → v

    Before, Agda would eagerly introduce the hidden parameter {v} as
    unnamed left-hand side parameter, leaving no way to refer to it.

    The related issue 655 has also been addressed.  It is now possible
    to make `synonym’ definitions

      name = expression

    even when the type of expression begins with a hidden quantifier.
    Simple example:

      id2 = id

    That resulted in unsolved metas until 2.3.0.

  * Agda detects unused arguments and ignores them during equality
    checking. [Issue 691, solves also issue 44.]

    Agda’s polarity checker now assigns ‘Nonvariant’ to arguments
    that are not actually used (except for absurd matches).  If
    f’s first argument is Nonvariant, then f x is definitionally equal
    to f y regardless of x and y.  It is similar to irrelevance, but
    does not require user annotation.

    For instance, unused module parameters do no longer get in the way:

      module M (x : Bool) where

        not : Bool → Bool
        not true  = false
        not false = true

      open M true
      open M false renaming (not to not′)

      test : (y : Bool) → not y ≡ not′ y
      test y = refl

    Matching against record or absurd patterns does not count as `use’,
    so we get some form of proof irrelevance:

      data ⊥ : Set where
      record ⊤ : Set where
        constructor trivial

      data Bool : Set where
        true false : Bool

      True : Bool → Set
      True true  = ⊤
      True false = ⊥

      fun : (b : Bool) → True b → Bool
      fun true  trivial = true
      fun false ()

      test : (b : Bool) → (x y : True b) → fun b x ≡ fun b y
      test b x y = refl

    More examples in test/succeed/NonvariantPolarity.agda.

    Phantom arguments:  Parameters of record and data types are considered
    `used’ even if they are not actually used.  Consider:

      False : Nat → Set
      False zero    = ⊥
      False (suc n) = False n

      module Invariant where
        record Bla (n : Nat)(p : False n) : Set where

      module Nonvariant where
        Bla : (n : Nat) → False n → Set
        Bla n p = ⊤

    Even though record Bla’ does not use its parameters n and p, they
    are considered as used, allowing “phantom type” techniques.

    In contrast, the arguments of function Bla’ are recognized as unused.
    The following code type-checks if we open Invariant but leaves unsolved
    metas if we open Nonvariant.

      drop-suc : {n : Nat}{p : False n} → Bla (suc n) p → Bla n p
      drop-suc _ = _

      bla : (n : Nat) → {p : False n} → Bla n p → ⊥
      bla zero {()} b
      bla (suc n) b = bla n (drop-suc b)

    If Bla’ is considered invariant, the hidden argument in the recursive
    call can be inferred to be `p’.  If it is considered non-variant, then
    Bla n X = Bla n p’ does not entail X = p’ and the hidden argument
    remains unsolved.  Since `bla’ does not actually use its hidden argument,
    its value is not important and it could be searched for.
    Unfortunately, polarity analysis of `bla’ happens only after type
    checking, thus, the information that `bla’ is non-variant in `p’ is
    not available yet when meta-variables are solved.
    (See test/fail/BrokenInferenceDueToNonvariantPolarity.agda)

  * Agda now expands simple definitions (one clause, terminating)
    to check whether a function is constructor headed. [Issue 747]
    For instance, the following now also works:

      MyPair : Set → Set → Set
      MyPair A B = Pair A B

      Vec : Set → Nat → Set
      Vec A zero    = Unit
      Vec A (suc n) = MyPair A (Vec A n)

    Here, Unit and Pair are data or record types.

  Compiler backends
  =================

  * -Werror is now overridable.

    To enable compilation of Haskell modules containing warnings, the
    -Werror flag for the MAlonzo backend has been made overridable. If,
    for example, --ghc-flag=-Wwarn is passed when compiling, one can get
    away with things like:

      data PartialBool : Set where
        true : PartialBool

      {-# COMPILED_DATA PartialBool Bool True #-}

    The default behavior remains as it used to be and rejects the above
    program.

  Tools
  =====

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

  * Asynchronous Emacs mode.

    One can now use Emacs while a buffer is type-checked. If the buffer
    is edited while the type-checker runs, then syntax highlighting will
    not be updated when type-checking is complete.

  * Interactive syntax highlighting.

    The syntax highlighting is updated while a buffer is type-checked:

     At first the buffer is highlighted in a somewhat crude way
      (without go-to-definition information for overloaded
      constructors).

     If the highlighting level is “interactive”, then the piece of code
      that is currently being type-checked is highlighted as such. (The
      default is “non-interactive”.)

     When a mutual block has been type-checked it is highlighted
      properly (this highlighting includes warnings for potential
      non-termination).

    The highlighting level can be controlled via the new configuration
    variable agda2-highlight-level.

  * Multiple case-splits can now be performed in one go.

    Consider the following example:

      _==_ : Bool → Bool → Bool
      b₁ == b₂ = {!!}

    If you split on “b₁ b₂”, then you get the following code:

      _==_ : Bool → Bool → Bool
      true == true = {!!}
      true == false = {!!}
      false == true = {!!}
      false == false = {!!}

    The order of the variables matters. Consider the following code:

      lookup : ∀ {a n} {A : Set a} → Vec A n → Fin n → A
      lookup xs i = {!!}

    If you split on “xs i”, then you get the following code:

      lookup : ∀ {a n} {A : Set a} → Vec A n → Fin n → A
      lookup [] ()
      lookup (x ∷ xs) zero = {!!}
      lookup (x ∷ xs) (suc i) = {!!}

    However, if you split on “i xs”, then you get the following code
    instead:

      lookup : ∀ {a n} {A : Set a} → Vec A n → Fin n → A
      lookup (x ∷ xs) zero = ?
      lookup (x ∷ xs) (suc i) = ?

    This code is rejected by Agda 2.3.0, but accepted by 2.3.2 thanks
    to improved coverage checking (see above).

  * The Emacs mode now presents information about which module is
    currently being type-checked.

  * New global menu entry: Information about the character at point.

    If this entry is selected, then information about the character at
    point is displayed, including (in many cases) information about how
    to type the character.

  * Commenting/uncommenting the rest of the buffer.

    One can now comment or uncomment the rest of the buffer by typing
    C-c C-x M-; or by selecting the menu entry “Comment/uncomment the
    rest of the buffer”.

  * The Emacs mode now uses the Agda executable instead of GHCi.

    The *ghci* buffer has been renamed to *agda2*.

    A new configuration variable has been introduced:
    agda2-program-name, the name of the Agda executable (by default
    agda).

    The variable agda2-ghci-options has been replaced by
    agda2-program-args: extra arguments given to the Agda executable (by
    default none).

    If you want to limit Agda’s memory consumption you can add some
    arguments to agda2-program-args, for instance +RTS -M1.5G -RTS.

  * The Emacs mode no longer depends on haskell-mode.

    Users who have customised certain haskell-mode variables (such as
    haskell-ghci-program-args) may want to update their configuration.

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

  An experimental LaTeX-backend which does precise highlighting a la the
  HTML-backend and code alignment a la lhs2TeX has been added.

  Here is a sample input literate Agda file:

    \documentclass{article}

    \usepackage{agda}

    \begin{document}

    The following module declaration will be hidden in the output.

    \AgdaHide{
    \begin{code}
    module M where
    \end{code}
    }

    Two or more spaces can be used to make the backend align stuff.

    \begin{code}
    data ℕ : Set where
      zero  : ℕ
      suc   : ℕ → ℕ

    _+_ : ℕ → ℕ → ℕ
    zero   + n = n
    suc m  + n = suc (m + n)
    \end{code}

    \end{document}

  To produce an output PDF issue the following commands:

    agda --latex -i . <file>.lagda
    pdflatex latex/<file>.tex

  Only the top-most module is processed, like with lhs2tex and unlike with
  the HTML-backend. If you want to process imported modules you have to
  call agda --latex manually on each of those modules.

  There are still issues related to formatting, see the bug tracker for
  more information:

    https://code.google.com/p/agda/issues/detail?id=697

  The default agda.sty might therefore change in backwards-incompatible
  ways, as work proceeds in trying to resolve those problems.


  Implemented features:

    * Two or more spaces can be used to force alignment of things, like
      with lhs2tex. See example above.

    * The highlighting information produced by the type checker is used to
      generate the output. For example, the data declaration in the example
      above, produces:

        \AgdaKeyword{data} \AgdaDatatype{ℕ} \AgdaSymbol{:}
            \AgdaPrimitiveType{Set} \AgdaKeyword{where}

      These latex commands are defined in agda.sty (which is imported by
      \usepackage{agda}) and cause the highlighting.

    * The latex-backend checks if agda.sty is found by the latex
      environment, if it isn’t a default agda.sty is copied from Agda’s
      data-dir into the working directory (and thus made available to the
      latex environment).

      If the default agda.sty isn’t satisfactory (colors, fonts, spacing,
      etc) then the user can modify it and make put it somewhere where the
      latex environment can find it. Hopefully most aspects should be
      modifiable via agda.sty rather than having to tweak the
      implementation.

    * --latex-dir can be used to change the default output directory.