Release notes for Agda 2 version 2.2.6
======================================
Language
--------
* Universe polymorphism (experimental extension).
To enable universe polymorphism give the flag
`--universe-polymorphism` on the command line or (recommended) as an
`OPTIONS` pragma.
When universe polymorphism is enabled `Set` takes an argument which is
the universe level. For instance, the type of universe polymorphic
identity is
```agda
id : {a : Level} {A : Set a} → A → A.
```
The type Level is isomorphic to the unary natural numbers and should
be specified using the BUILTINs `LEVEL`, `LEVELZERO`, and
`LEVELSUC`:
```agda
data Level : Set where
zero : Level
suc : Level → Level
{-# BUILTIN LEVEL Level #-}
{-# BUILTIN LEVELZERO zero #-}
{-# BUILTIN LEVELSUC suc #-}
```
There is an additional BUILTIN `LEVELMAX` for taking the maximum of two
levels:
```agda
max : Level → Level → Level
max zero m = m
max (suc n) zero = suc n
max (suc n) (suc m) = suc (max n m)
{-# BUILTIN LEVELMAX max #-}
```
The non-polymorphic universe levels `Set`, `Set₁` and so on are
sugar for `Set zero`, `Set (suc zero)`, etc.
At present there is no automatic lifting of types from one level to
another. It can still be done (rather clumsily) by defining types
like the following one:
```agda
data Lifted {a} (A : Set a) : Set (suc a) where
lift : A → Lifted A
```
However, it is likely that automatic lifting is introduced at some
point in the future.
* Multiple constructors, record fields, postulates or primitives can
be declared using a single type signature:
```agda
data Bool : Set where
false true : Bool
postulate
A B : Set
```
* Record fields can be implicit:
```agda
record R : Set₁ where
field
{A} : Set
f : A → A
{B C} D {E} : Set
g : B → C → E
```
By default implicit fields are not printed.
* Record constructors can be defined:
```agda
record Σ (A : Set) (B : A → Set) : Set where
constructor _,_
field
proj₁ : A
proj₂ : B proj₁
```
In this example `_,_` gets the type
```agda
(proj₁ : A) → B proj₁ → Σ A B.
```
For implicit fields the corresponding constructor arguments become
implicit.
Note that the constructor is defined in the *outer* scope, so any
fixity declaration has to be given outside the record definition.
The constructor is not in scope inside the record module.
Note also that pattern matching for records has not been implemented
yet.
* BUILTIN hooks for equality.
The data type
```agda
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
```
can be specified as the builtin equality type using the following
pragmas:
```agda
{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}
```
The builtin equality is used for the new rewrite construct and
the `primTrustMe` primitive described below.
* New `rewrite` construct.
If `eqn : a ≡ b`, where `_≡_` is the builtin equality (see above) you
can now write
```agda
f ps rewrite eqn = rhs
```
instead of
```agda
f ps with a | eqn
... | ._ | refl = rhs
```
The `rewrite` construct has the effect of rewriting the goal and the
context by the given equation (left to right).
You can rewrite using several equations (in sequence) by separating
them with vertical bars (|):
```agda
f ps rewrite eqn₁ | eqn₂ | … = rhs
```
It is also possible to add `with`-clauses after rewriting:
```agda
f ps rewrite eqns with e
... | p = rhs
```
Note that pattern matching happens before rewriting—if you want to
rewrite and then do pattern matching you can use a with after the
rewrite.
See `test/Succeed/Rewrite.agda` for some examples.
* A new primitive, `primTrustMe`, has been added:
```agda
primTrustMe : {A : Set} {x y : A} → x ≡ y
```
Here `_≡_` is the builtin equality (see BUILTIN hooks for equality,
above).
If `x` and `y` are definitionally equal, then
`primTrustMe {x = x} {y = y}` reduces to `refl`.
Note that the compiler replaces all uses of `primTrustMe` with the
`REFL` builtin, without any check for definitional
equality. Incorrect uses of `primTrustMe` can potentially lead to
segfaults or similar problems.
For an example of the use of `primTrustMe`, see `Data.String` in
version 0.3 of the standard library, where it is used to implement
decidable equality on strings using the primitive boolean equality.
* Changes to the syntax and semantics of IMPORT pragmas, which are
used by the Haskell FFI. Such pragmas must now have the following
form:
```agda
{-# IMPORT <module name> #-}
```
These pragmas are interpreted as *qualified* imports, so Haskell
names need to be given qualified (unless they come from the Haskell
prelude).
* The horizontal tab character (U+0009) is no longer treated as white
space.
* Line pragmas are no longer supported.
* The `--include-path` flag can no longer be used as a pragma.
* The experimental and incomplete support for proof irrelevance has
been disabled.
Tools
-----
* New `intro` command in the Emacs mode. When there is a canonical way
of building something of the goal type (for instance, if the goal
type is a pair), the goal can be refined in this way. The command
works for the following goal types:
- A data type where only one of its constructors can be used to
construct an element of the goal type. (For instance, if the
goal is a non-empty vector, a `cons` will be introduced.)
- A record type. A record value will be introduced. Implicit
fields will not be included unless showing of implicit arguments
is switched on.
- A function type. A lambda binding as many variables as possible
will be introduced. The variable names will be chosen from the
goal type if its normal form is a dependent function type,
otherwise they will be variations on `x`. Implicit lambdas will
only be inserted if showing of implicit arguments is switched
on.
This command can be invoked by using the `refine` command
(`C-c C-r`) when the goal is empty. (The old behaviour of the refine
command in this situation was to ask for an expression using the
minibuffer.)
* The Emacs mode displays `Checked` in the mode line if the current
file type checked successfully without any warnings.
* If a file `F` is loaded, and this file defines the module `M`, it is
an error if `F` is not the file which defines `M` according to the
include path.
Note that the command-line tool and the Emacs mode define the
meaning of relative include paths differently: the command-line tool
interprets them relative to the current working directory, whereas
the Emacs mode interprets them relative to the root directory of the
current project. (As an example, if the module `A.B.C` is loaded
from the file `<some-path>/A/B/C.agda`, then the root directory is
`<some-path>`.)
* It is an error if there are several files on the include path which
match a given module name.
* Interface files are relocatable. You can move around source trees as
long as the include path is updated in a corresponding way. Note
that a module `M` may be re-typechecked if its time stamp is
strictly newer than that of the corresponding interface file
(`M.agdai`).
* Type-checking is no longer done when an up-to-date interface exists.
(Previously the initial module was always type-checked.)
* Syntax highlighting files for Emacs (`.agda.el`) are no longer used.
The `--emacs` flag has been removed. (Syntax highlighting
information is cached in the interface files.)
* The Agate and Alonzo compilers have been retired. The options
`--agate`, `--alonzo` and `--malonzo` have been removed.
* The default directory for MAlonzo output is the project's root
directory. The `--malonzo-dir` flag has been renamed to
`--compile-dir`.
* Emacs mode: `C-c C-x C-d` no longer resets the type checking state.
`C-c C-x C-r` can be used for a more complete reset. `C-c C-x C-s`
(which used to reload the syntax highlighting information) has been
removed. `C-c C-l` can be used instead.
* The Emacs mode used to define some "abbrevs", unless the user
explicitly turned this feature off. The new default is *not* to add
any abbrevs. The old default can be obtained by customising
`agda2-mode-abbrevs-use-defaults` (a customisation buffer can be
obtained by typing `M-x customize-group agda2 RET` after an Agda
file has been loaded).