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 ```