Release notes for Agda 2 version 2.3.2
======================================
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.
```agda
{-# NO_TERMINATION_CHECK #-}
a : A
a = a
```
2. Skipping a single definition: before first clause.
```agda
b : A
{-# NO_TERMINATION_CHECK #-}
b = b
```
3. Skipping an old-style mutual block: Before `mutual` keyword.
```agda
{-# 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
```agda
i : A
j : A
i = j
{-# NO_TERMINATION_CHECK #-}
j = i
```
The pragma cannot be used in `--safe` mode.
Language
--------
* Let binding record patterns
```agda
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
```agda
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:
```agda
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:
```agda
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
```agda
import Data.Nat as Nat
import Data.Bool as Bool
two = Bool.if true then 1 Nat.+ 1 else 0
```
* Sections [Issue [#735](https://github.com/agda/agda/issues/735)].
Agda now parses anonymous modules as sections:
```agda
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
```agda
module _ parameters where
declarations
```
is accepted and has the same effect as
```agda
private
module M parameters where
declarations
open M public
```
for a fresh name `M`.
* Instantiating a module in an open import statement
[Issue [#481](https://github.com/agda/agda/issues/481)]. Now
accepted:
```agda
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:
```agda
import Path.Module args [using/hiding/renaming (...)]
```
You can give a private name `M` to the instantiated module via
```agda
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:
```agda
open import as as as as as as
```
* Implicit module parameters can be given by name. E.g.
```agda
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.
```agda
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](https://github.com/agda/agda/issues/526)]
* Agda expands identifiers in anonymous modules when printing. Should
make some goals nicer to read.
[Issue [#721](https://github.com/agda/agda/issues/721)]
* When a module identifier is ambiguous, Agda tells you if one of them
is a data type module.
[Issues [#318](https://github.com/agda/agda/issues/318),
[#705](https://github.com/agda/agda/issues/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:
```agda
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
```agda
[] !! ()
```
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:
```agda
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](https://github.com/agda/agda/issues/456)]
Agda now solves meta-variables that are applied to record patterns.
A typical (but here, artificial) case is:
```agda
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](https://github.com/agda/agda/issues/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.
```agda
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](https://github.com/agda/agda/issues/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
```agda
test : {A : Set} -> Set
test = \ {A} -> A
```
because internally, the hidden argument `{A : Set}` was added to the
left-hand side, yielding
```agda
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
```agda
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
```agda
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:
```agda
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
```agda
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.
```agda
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](https://github.com/agda/agda/issues/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](https://github.com/agda/agda/issues/691),
solves also Issue [#44](https://github.com/agda/agda/issues/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:
```agda
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:
```agda
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:
```agda
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`.
```agda
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](https://github.com/agda/agda/issues/747)] For
instance, the following now also works:
```agda
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:
```agda
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:
```agda
_==_ : Bool → Bool → Bool
b₁ == b₂ = {!!}
```
If you split on `b₁ b₂`, then you get the following code:
```agda
_==_ : Bool → Bool → Bool
true == true = {!!}
true == false = {!!}
false == true = {!!}
false == false = {!!}
```
The order of the variables matters. Consider the following code:
```agda
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:
```agda
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:
```agda
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:
```latex
\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:
```agda
\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.