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]

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

Example:

  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]

  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.

  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.

  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.

  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, #1264, #1292.

Termination checking

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

  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

  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... ;-)

  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
Issue #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:

  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

2.4.2.1.md 6.3 KB Permalink History Raw