2.4.2.4.md

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)