CHANGELOG.md

Release notes for Agda version 2.6.4

Reflection

• FOREIGN and COMPILE pragmas can now be generated using two new reflection primitives:

  pragmaForeign : String → String → TC ⊤
  pragmaCompile : String → Name → String → TC ⊤

Erasure

• [Breaking] The new flag --erasure turns on support for erasure (#6349).

  This flag is infective.

  Unless this flag is active the following things are prohibited:

  • Use of the annotations @0 and @erased.
  • Use of names defined in Cubical Agda in Erased Cubical Agda.
  • Use of the flag --erase-record-parameters.

  When --erasure is used the parameter arguments of constructors and projections are marked as erased (#4786), with one exception: for indexed data types this only happens if the --with-K flag is active (#6297).

  For instance, the type of the constructor c below is {@0 A : Set} → D A, and the type of the projection R.f is {@0 A : Set} → R A → A:

  {-# OPTIONS --erasure #-}
  
  data D (A : Set) : Set where
    c : D A
  
  record R (A : Set) : Set where
    field
      f : A

• [Breaking] Unless the new flag --erased-matches is used matching is not allowed in erased positions for single-constructor data types or record types without η-equality (#6349).

  This flag is infective and implied by --with-K.

• [Breaking] Added a hard compile-time mode (see #4743).

  When the hard compile-time mode is used all definitions are treated as erased. The hard compile-time mode is entered when an erased definition is checked (including an erased data or record type or module), but not when (for instance) a type-signature is checked.

  Previously the following code was rejected:

  open import Agda.Builtin.Bool
  
  @0 f : @0 Bool → Bool
  f = λ where
    true  → false
    false → true

  Now this code is accepted (if --erasure is used). On the other hand, the following code which used to be accepted is now rejected (if --erasure is used), because the pattern-matching lambda is treated as erased:

  open import Agda.Builtin.Equality
  
  data Unit : Set where
    unit : Unit
  
  mutual
  
    f : Unit → Unit
    f = _
  
    @0 f≡ : f ≡ λ { unit → unit }
    f≡ = refl

• One can now mark data and record types and modules as erased (see #4743).

  If a data type is marked as erased, then it can only be used in erased settings, and its constructors are erased. A data type is marked as erased by writing @0 or @erased right after the data keyword of the data type's declaration:

  data @0 D₁ : Set where
    c : D₁
  
  data @0 D₂ : Set
  
  data D₂ where
    c : D₁ → D₂
  
  interleaved mutual
  
    data @0 D₃ : Set where
  
    data D₃ where
      c : D₃

  If a record type is marked as erased, then it can only be used in erased settings, its constructors and fields are erased, and definitions in the record module are erased. A record type is marked as erased by writing @0 or @erased right after the record keyword of the record type's declaration:

  record @0 R₁ : Set where
    field
      x : D₁
  
  record @0 R₂ : Set
  
  record R₂ where
    field
      x : R₁

  If a module is marked as erased, then all definitions inside the module (and in the module's telescope) are erased. A module is marked as erased by writing @0 or @erased right after the module keyword:

  module @0 _ where
  
    F : @0 Set → Set
    F A = A
  
  module M (A : Set) where
  
    record R : Set where
      field
        @0 x : A
  
  module @0 N (@0 A : Set) = M A
  
  G : (@0 A : Set) → let module @0 M₂ = M A in Set
  G A = M.R B
    module @0 _ where
      B : Set
      B = A

  If an erased module is defined by a module application, then erased names can be used in the application, as in the definition of N above.

Syntax

• If the new option --hidden-argument-puns is used, then the pattern {x} is interpreted as {x = x}, and the pattern ⦃ x ⦄ is interpreted as ⦃ x = x ⦄ (see #6325). Here x must be an unqualified name that does not refer to a constructor that is in scope: if x is qualified, then the pattern is not interpreted as a pun, and if x is unqualified and refers to a constructor that is in scope, then the code is rejected.

  This feature can be turned off using --no-hidden-argument-puns.

  Note that {(x)} and ⦃ (x) ⦄ are not interpreted as puns.

  Note also that {x} is not interpreted as a pun in λ {x} → … or syntax f {x} = …. However, {x} is interpreted as a pun in λ (c {x}) → ….

Instance arguments

• [Breaking] The algorithm for resolution of instance arguments has been simplified. It will now only rely on the type of instances to determine which candidate it should use, and no longer on their values.

Pragmas and options

• New command-line option --trace-imports to switch on notification messages on the end of compilation of an imported module or on access to an interface file during the type-checking.

  See --trace-imports in the documentation for more.

• New option --no-infer-absurd-clauses to simplify coverage checking and case splitting: Agda will then no longer attempt to automatically eliminate absurd clauses which can be a costly operation. This means that these absurd clauses have to be written out in the Agda text. Try this option if you experience type checking performance degradation with omitted absurd clauses.

  Opposite: --infer-absurd-clauses.

• Benign warnings are now printed together with their warning name, to give a hint how they can be disabled (see #6229).

Library management

• [Breaking] One can no longer have .agda-lib files that are located below the "project root", on the path to the file that is being type-checked (see #6465).

  For instance, if you have a module called A.B.C in the directory Root/A/B, then an error is raised if there are .agda-lib files in Root/A or Root/A/B.

  Previously such .agda-lib files were ignored.

Emacs mode

• Helper function (C-c C-h) does not abstract over module parameters anymore (see #2271).