Release notes for Agda version 2.4.2.1
======================================

Pragmas and options
-------------------

* New pragma `{-# TERMINATING #-}` replacing
  `{-# NO_TERMINATION_CHECK #-}`

  Complements the existing pragma `{-# NON_TERMINATING #-}`.  Skips
  termination check for the associated definitions and marks them as
  terminating.  Thus, it is a replacement for `{-#
  NO_TERMINATION_CHECK #-}` with the same semantics.

  You can no longer use pragma `{-# NO_TERMINATION_CHECK #-}` to skip
  the termination check, but must label your definitions as either
  `{-# TERMINATING #-}` or `{-# NON_TERMINATING #-}` instead.

  Note: `{-# OPTION --no-termination-check #-}` labels all your
  definitions as `{-# TERMINATING #-}`, putting you in the danger zone
  of a loop in the type checker.

Language
--------

* Referring to a local variable shadowed by module opening is now an
  error.  Previous behavior was preferring the local over the imported
  definitions. [Issue [#1266](https://github.com/agda/agda/issues/1266)]

  Note that module parameters are locals as well as variables bound by
  λ, dependent function type, patterns, and let.

  Example:

  ```agda
  module M where
    A = Set1

  test : (A : Set) → let open M in A
  ```

  The last `A` produces an error, since it could refer to the local
  variable `A` or to the definition imported from module `M`.

* `with` on a variable bound by a module telescope or a pattern of a
  parent function is now forbidden.
  [Issue [#1342](https://github.com/agda/agda/issues/1342)]

  ```agda
  data Unit : Set where
    unit : Unit

  id : (A : Set) → A → A
  id A a = a

  module M (x : Unit) where

    dx : Unit → Unit
    dx unit = x

    g : ∀ u → x ≡ dx u
    g with x
    g | unit  = id (∀ u → unit ≡ dx u) ?
  ```

  Even though this code looks right, Agda complains about the type
  expression `∀ u → unit ≡ dx u`.  If you ask Agda what should go
  there instead, it happily tells you that it wants `∀ u → unit ≡ dx
  u`. In fact what you do not see and Agda will never show you is that
  the two expressions actually differ in the invisible first argument
  to `dx`, which is visible only outside module `M`.  What Agda wants
  is an invisible `unit` after `dx`, but all you can write is an
  invisible `x` (which is inserted behind the scenes).

  To avoid those kinds of paradoxes, `with` is now outlawed on module
  parameters.  This should ensure that the invisible arguments are
  always exactly the module parameters.

  Since a `where` block is desugared as module with pattern variables
  of the parent clause as module parameters, the same strikes you for
  uses of `with` on pattern variables of the parent function.

  ```agda
  f : Unit → Unit
  f x = unit
    where
      dx : Unit → Unit
      dx unit = x

      g : ∀ u → x ≡ dx u
      g with x
      g | unit  = id ((u : Unit) → unit ≡ dx u) ?
  ```

  The `with` on pattern variable `x` of the parent clause `f x = unit`
  is outlawed now.

Type checking
-------------

* Termination check failure is now a proper error.

  We no longer continue type checking after termination check
  failures.  Use pragmas `{-# NON_TERMINATING #-}` and `{-#
  NO_TERMINATION_CHECK #-}` near the offending definitions if you want
  to do so.  Or switch off the termination checker altogether with
  `{-# OPTIONS --no-termination-check #-}` (at your own risk!).

* (Since Agda 2.4.2): Termination checking `--without-K` restricts
  structural descent to arguments ending in data types or `Size`.
  Likewise, guardedness is only tracked when result type is data or
  record type.

  ```agda
  mutual
    data WOne : Set where wrap : FOne → WOne
    FOne = ⊥ → WOne

  noo : (X : Set) → (WOne ≡ X) → X → ⊥
  noo .WOne refl (wrap f) = noo FOne iso f
  ```

  `noo` is rejected since at type `X` the structural descent
  `f < wrap f` is discounted `--without-K`.

  ```agda
  data Pandora : Set where
    C : ∞ ⊥ → Pandora

  loop : (A : Set) → A ≡ Pandora → A
  loop .Pandora refl = C (♯ (loop ⊥ foo))
  ```

  `loop` is rejected since guardedness is not tracked at type `A`
  `--without-K`.

  See issues [#1023](https://github.com/agda/agda/issues/1023),
  [#1264](https://github.com/agda/agda/issues/1264),
  [#1292](https://github.com/agda/agda/issues/1292).

Termination checking
--------------------

* The termination checker can now recognize simple subterms in dot
  patterns.

  ```agda
  data Subst : (d : Nat) → Set where
    c₁ : ∀ {d} → Subst d → Subst d
    c₂ : ∀ {d₁ d₂} → Subst d₁ → Subst d₂ → Subst (suc d₁ + d₂)

  postulate
    comp : ∀ {d₁ d₂} → Subst d₁ → Subst d₂ → Subst (d₁ + d₂)

  lookup : ∀ d → Nat → Subst d → Set₁
  lookup d             zero    (c₁ ρ)             = Set
  lookup d             (suc v) (c₁ ρ)             = lookup d v ρ
  lookup .(suc d₁ + d₂) v      (c₂ {d₁} {d₂} ρ σ) = lookup (d₁ + d₂) v (comp ρ σ)
  ```

  The dot pattern here is actually normalized, so it is

  ```agda
  suc (d₁ + d₂)
  ```

  and the corresponding recursive call argument is `(d₁ + d₂)`.  In
  such simple cases, Agda can now recognize that the pattern is
  constructor applied to call argument, which is valid descent.

  Note however, that Agda only looks for syntactic equality when
  identifying subterms, since it is not allowed to normalize terms on
  the rhs during termination checking.

  Actually writing the dot pattern has no effect, this works as well,
  and looks pretty magical... ;-)

  ```agda
  hidden : ∀{d} → Nat → Subst d → Set₁
  hidden zero    (c₁ ρ)   = Set
  hidden (suc v) (c₁ ρ)   = hidden v ρ
  hidden v       (c₂ ρ σ) = hidden v (comp ρ σ)
  ```

Tools
-----

### LaTeX-backend

* Fixed the issue of identifiers containing operators being typeset with
  excessive math spacing.

Bug fixes
---------

* Issue [#1194](https://github.com/agda/agda/issues/1194)

* Issue [#836](https://github.com/agda/agda/issues/836): Fields and
  constructors can be qualified by the record/data *type* as well as
  by their record/data module.  This now works also for record/data
  type imported from parametrized modules:

  ```agda
  module M (_ : Set₁) where

    record R : Set₁ where
      field
        X : Set

  open M Set using (R)  -- rather than using (module R)

  X : R → Set
  X = R.X
  ```