Release notes for Agda version 2.4.2.4
======================================
Installation and infrastructure
-------------------------------
* Removed support for GHC 7.4.2.
Pragmas and options
-------------------
* Option `--copatterns` is now on by default. To switch off
parsing of copatterns, use:
```agda
{-# OPTIONS --no-copatterns #-}
```
* Option `--rewriting` is now needed to use `REWRITE` pragmas and
rewriting during reduction. Rewriting is not `--safe`.
To use rewriting, first specify a relation symbol `R` that will
later be used to add rewrite rules. A canonical candidate would be
propositional equality
```agda
{-# BUILTIN REWRITE _≡_ #-}
```
but any symbol `R` of type `Δ → A → A → Set i` for some `A` and `i`
is accepted. Then symbols `q` can be added to rewriting provided
their type is of the form `Γ → R ds l r`. This will add a rewrite
rule
```
Γ ⊢ l ↦ r : A[ds/Δ]
```
to the signature, which fires whenever a term is an instance of `l`.
For example, if
```agda
plus0 : ∀ x → x + 0 ≡ x
```
(ideally, there is a proof for `plus0`, but it could be a
postulate), then
```agda
{-# REWRITE plus0 #-}
```
will prompt Agda to rewrite any well-typed term of the form `t + 0`
to `t`.
Some caveats: Agda accepts and applies rewrite rules naively, it is
very easy to break consistency and termination of type checking.
Some examples of rewrite rules that should *not* be added:
```agda
refl : ∀ x → x ≡ x -- Agda loops
plus-sym : ∀ x y → x + y ≡ y + x -- Agda loops
absurd : true ≡ false -- Breaks consistency
```
Adding only proven equations should at least preserve consistency,
but this is only a conjecture, so know what you are doing! Using
rewriting, you are entering into the wilderness, where you are on
your own!
Language
--------
* `forall` / `∀` now parses like `λ`, i.e., the following parses now
[Issue [#1583](https://github.com/agda/agda/issues/1538)]:
```agda
⊤ × ∀ (B : Set) → B → B
```
* The underscore pattern `_` can now also stand for an inaccessible
pattern (dot pattern). This alleviates the need for writing `._`.
[Issue #[1605](https://github.com/agda/agda/issues/1605)] Instead of
```agda
transVOld : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
transVOld _ ._ ._ refl refl = refl
```
one can now write
```agda
transVNew : ∀{A : Set} (a b c : A) → a ≡ b → b ≡ c → a ≡ c
transVNew _ _ _ refl refl = refl
```
and let Agda decide where to put the dots. This was always possible
by using hidden arguments
```agda
transH : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
transH refl refl = refl
```
which is now equivalent to
```agda
transHNew : ∀{A : Set}{a b c : A} → a ≡ b → b ≡ c → a ≡ c
transHNew {a = _}{b = _}{c = _} refl refl = refl
```
Before, underscore `_` stood for an unnamed variable that could not
be instantiated by an inaccessible pattern. If one no wants to
prevent Agda from instantiating, one needs to use a variable name
other than underscore (however, in practice this situation seems
unlikely).
Type checking
-------------
* Polarity of phantom arguments to data and record types has
changed. [Issue [#1596](https://github.com/agda/agda/issues/1596)]
Polarity of size arguments is Nonvariant (both monotone and
antitone). Polarity of other arguments is Covariant (monotone).
Both were Invariant before (neither monotone nor antitone).
The following example type-checks now:
```agda
open import Common.Size
-- List should be monotone in both arguments
-- (even when `cons' is missing).
data List (i : Size) (A : Set) : Set where
[] : List i A
castLL : ∀{i A} → List i (List i A) → List ∞ (List ∞ A)
castLL x = x
-- Stream should be antitone in the first and monotone in the second argument
-- (even with field `tail' missing).
record Stream (i : Size) (A : Set) : Set where
coinductive
field
head : A
castSS : ∀{i A} → Stream ∞ (Stream ∞ A) → Stream i (Stream i A)
castSS x = x
```
* `SIZELT` lambdas must be consistent
[Issue [#1523](https://github.com/agda/agda/issues/1523), see Abel
and Pientka, ICFP 2013]. When lambda-abstracting over type (`Size<
size`) then `size` must be non-zero, for any valid instantiation of
size variables.
- The good:
```agda
data Nat (i : Size) : Set where
zero : ∀ (j : Size< i) → Nat i
suc : ∀ (j : Size< i) → Nat j → Nat i
{-# TERMINATING #-}
-- This definition is fine, the termination checker is too strict at the moment.
fix : ∀ {C : Size → Set}
→ (∀ i → (∀ (j : Size< i) → Nat j -> C j) → Nat i → C i)
→ ∀ i → Nat i → C i
fix t i (zero j) = t i (λ (k : Size< i) → fix t k) (zero j)
fix t i (suc j n) = t i (λ (k : Size< i) → fix t k) (suc j n)
```
The `λ (k : Size< i)` is fine in both cases, as context
```agda
i : Size, j : Size< i
```
guarantees that `i` is non-zero.
- The bad:
```agda
record Stream {i : Size} (A : Set) : Set where
coinductive
constructor _∷ˢ_
field
head : A
tail : ∀ {j : Size< i} → Stream {j} A
open Stream public
_++ˢ_ : ∀ {i A} → List A → Stream {i} A → Stream {i} A
[] ++ˢ s = s
(a ∷ as) ++ˢ s = a ∷ˢ (as ++ˢ s)
```
This fails, maybe unjustified, at
```agda
i : Size, s : Stream {i} A
⊢
a ∷ˢ (λ {j : Size< i} → as ++ˢ s)
```
Fixed by defining the constructor by copattern matching:
```agda
record Stream {i : Size} (A : Set) : Set where
coinductive
field
head : A
tail : ∀ {j : Size< i} → Stream {j} A
open Stream public
_∷ˢ_ : ∀ {i A} → A → Stream {i} A → Stream {↑ i} A
head (a ∷ˢ as) = a
tail (a ∷ˢ as) = as
_++ˢ_ : ∀ {i A} → List A → Stream {i} A → Stream {i} A
[] ++ˢ s = s
(a ∷ as) ++ˢ s = a ∷ˢ (as ++ˢ s)
```
- The ugly:
```agda
fix : ∀ {C : Size → Set}
→ (∀ i → (∀ (j : Size< i) → C j) → C i)
→ ∀ i → C i
fix t i = t i λ (j : Size< i) → fix t j
```
For `i=0`, there is no such `j` at runtime, leading to looping
behavior.
Interaction
-----------
* Issue [#635](https://github.com/agda/agda/issues/635) has been
fixed. Case splitting does not spit out implicit record patterns
any more.
```agda
record Cont : Set₁ where
constructor _◃_
field
Sh : Set
Pos : Sh → Set
open Cont
data W (C : Cont) : Set where
sup : (s : Sh C) (k : Pos C s → W C) → W C
bogus : {C : Cont} → W C → Set
bogus w = {!w!}
```
Case splitting on `w` yielded, since the fix of
Issue [#473](https://github.com/agda/agda/issues/473),
```agda
bogus {Sh ◃ Pos} (sup s k) = ?
```
Now it gives, as expected,
```agda
bogus (sup s k) = ?
```
Performance
-----------
* As one result of the 21st Agda Implementor's Meeting (AIM XXI),
serialization of the standard library is 50% faster (time reduced by
a third), without using additional disk space for the interface
files.
Bug fixes
---------
Issues fixed (see [bug tracker](https://github.com/agda/agda/issues)):
[#1546](https://github.com/agda/agda/issues/1546) (copattern matching
and with-clauses)
[#1560](https://github.com/agda/agda/issues/1560) (positivity checker
inefficiency)
[#1584](https://github.com/agda/agda/issues/1548) (let pattern with
trailing implicit)