Release notes for Agda version 2.6.4

Highlights

• Cubical Agda now displays boundary conditions in interactive mode (PR #6529).

• An inconsistency in the treatment of large indices has been fixed (Issue #6654).

• Unfolding of definitions can now be fine-controlled via opaque definitions.

• Additions to the sort system: LevelUniv and Propω.

• New flag --erasure with several improvements to erasure (declared run-time irrelevance).

• New reflection primitives for meta-programming.

Installation

• Removed the cabal flag cpphs that enabled building Agda with cpphs instead of the default C preprocessor.

• Agda supports GHC versions 8.6.5 to 9.6.3.

Pragmas and options

• New command-line option --numeric-version to just print the version number of Agda.

• Option --version now also prints the cabal flags active in this build of Agda (e.g. whether Agda was built with -f enable-cluster-counting).

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

• New option --level-universe to make Level inhabit its own universe LevelUniv: When this option is turned on, Level can now only depend on terms of type Level.

  Note: While compatible with the --cubical option, this option is currently not compatible with cubical builtin files, and an error will be raised when trying to import them in a file using --level-universe.

  Opposite: --no-level-universe.

• Most boolean options now have their opposite, e.g., --allow-unsolved-metas is complemented by --no-allow-unsolved-metas. With the opposite one can override a previously given option. Options given on the command line are overwritten by options given in the .agda-lib file, which in turn get overwritten by options given in the individual .agda file.

  New options (all on by default):

  • --no-allow-exec
  • --no-allow-incomplete-matches
  • --no-allow-unsolved-metas
  • --no-call-by-name
  • --no-cohesion
  • --no-count-clusters
  • --no-erased-matches
  • --no-erasure
  • --no-experimental-irrelevance
  • --no-flat-split
  • --no-guarded
  • --no-injective-type-constructors
  • --no-keep-covering-clauses
  • --no-lossy-unification
  • --no-keep-pattern-variables
  • --no-omega-in-omega
  • --no-postfix-projections
  • --no-rewriting
  • --no-show-identity-substitutions
  • --no-show-implicit
  • --no-show-irrelevant
  • --no-two-level
  • --no-type-in-type
  • --eta-equality
  • --fast-reduce
  • --forcing
  • --import-sorts
  • --load-primitives
  • --main
  • --pattern-matching
  • --positivity-check
  • --print-pattern-synonyms
  • --projection-like
  • --termination-check
  • --unicode

• Option --flat-split again implies --cohesion. Reverts change introduced in Agda 2.6.3 where --cohesion was a prerequisite for --flat-split.

• Pragma INLINE may now be applied to constructors of types supporting co-pattern matching. It enables translation of right-hand-side constructor applications to left-hand-side co-pattern splits (see PR #6682). For example, this translation allows the nats function to pass termination checking:

    record Stream (A : Set) : Set where
      coinductive; constructor _∷_
      field head : A
            tail : Stream A
    open Stream
    {-# INLINE _∷_ #-}
  
    nats : Nat → Stream Nat
    nats n = n ∷ nats (1 + n)
  

  Inlining transforms the definition of nats to the following definition by copattern matching:

    nats n .head = n
    nats n .tail = nats (1 + n)
  

  This form is accepted by the termination checker; unlike the form before inlining, it does not admit any infinite reduction sequences.

  If option --exact-split is on, the inlining will trigger a InlineNoExactSplit warning for nats. This warning can be disabled as usual, with -WnoInlineNoExactSplit.

• New option --large-indices, controlling whether constructors of indexed data types are allowed to refer to data that would be “too large” to fit in their declared sort. Large indices are disallowed by default; see the language changes for details.

• New option --forced-argument-recursion, on by default, controlling whether forced constructor arguments are usable for termination checking. This flag may be necessary for Agda to accept nontrivial uses of induction-induction.

• The suffix Warning has been dropped from the warning names DuplicateFieldsWarning and TooManyFieldsWarning.

• The warning GenericUseless has been split into the three warnings UselessPragma, FaceConstraintCannotBeHidden and FaceConstraintCannotBeNamed.

• New warning PatternShadowsConstructor which used to be an error.

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.

Interaction and emacs mode

• Agda now supports reading files with extension .lagda.typ, and use the parser for markdown files to parse them. To edit such files in Emacs with Agda support, one needs to add the line

  (add-to-list 'auto-mode-alist '("\\.lagda.typ\\'" . agda2-mode))
  

  to .emacs.

  Generation for highlighted code like HTML is unsupported for Typst. One may generate HTML with typst input, but that makes little sense, and markdown is recommended instead when HTML export is desired.

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

• New Agda input mode prefix box for APL boxed operators, e.g. \box= for ⌸; see PR #6510 for full list of bindings.

• Cubical Agda will now report boundary information for interaction points which are not at the top-level of their respective clauses. This includes bodies of Path-typed values, the faces of a partial element, arguments to functions returning paths, etc.

  Since this information is available in a structured way during interaction, the “goal type, context, and inferred type” command will also display the value of the expression at each relevant face.

  See also PR #6529 for a deeper explanation and a demo video.

Syntax

• Agda now skips the UTF8 byte order mark (BOM) at beginning of files (see #6524). Previously, the BOM caused a parse error.

• 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}) → ….

• postulate blocks may now contain private declarations (see #1702).

Language

• [Breaking] Constructor arguments are no longer allowed to store values of a type larger than their own sort, even when these values are forced by the indices of a constructor.

  This fixes a particular instance of the incompatibility between structural recursion and impredicativity, which could previously be exploited through the use of large data-type indices. (see #6654).

  This behaviour can be controlled with the flag --large-indices. Note that, when --large-indices is enabled, forced constructor arguments should not be used for termination checking. The flag --[no-]forced-argument-recursion makes the termination checker skip these arguments entirely. When --safe is given, --large-indices is incompatible with --without-K and incompatible with --forced-argument-recursion.

• Added opaque definitions, a mechanism for finer-grained control of unfolding. Unlike abstract definitions, which can never be unfolded outside of (a child module of) the defining module, opacity can be toggled at use-sites:

  opaque
    foo : Set
    foo = Nat
  
  opaque
    unfolding foo
  
    _ : foo
    _ = 123
  

• Unless --no-import-sorts is given, Set is in scope as before, but Prop is only in scope when --prop is active. Additionally SSet is now in scope when --two-level is active (see #6634).

• New sorts Propω, Propω₁, etc., in analogy to Setω, Setω₁ etc. Requires option --prop.

  Example:

  {-# OPTIONS --prop --large-indices #-}
  
  open Agda.Primitive
  
  variable
    ℓ : Level
    A : Set ℓ
  
  -- Lists of elements of types at any finite level.
  
  data HList : Setω where
    []  : HList
    _∷_ : A → HList → HList
  
  variable
    x  : A
    xs : HList
  
  -- Predicate stating that all elements satisfy a given property.
  
  data All (P : ∀{ℓ} {A : Set ℓ} → A → Prop ℓ) : HList → Propω where
    []  : All P []
    _∷_ : P x → All P xs → All P (x ∷ xs)
  

• [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.

Erasure

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

  This flag is infective. It is implied by --erase-record-parameters and --erased-matches.

  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.

  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. If it is given explicitly, it implies --erasure.

• [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.

• Equivalence primitives no longer require full --cubical mode, --erased-cubical suffices. Equivalence definition is moved out of Agda.Builtin.Cubical.Glue into its own module Agda.Builtin.Cubical.Equiv, the former reexports the latter.

Reflection

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

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

• Add 4 reflection primitives of the form ask* and with*:

  withNormalisation : ∀ {a} {A : Set a} → Bool → TC A → TC A
  askNormalisation  : TC Bool
  
  withExpandLast : ∀ {a} {A : Set a} → Bool → TC A → TC A
  askExpandLast  : TC Bool
  
  withReduceDefs : ∀ {a} {A : Set a} → (Σ Bool λ _ → List Name) → TC A → TC A
  askReduceDefs  : TC (Σ Bool λ _ → List Name)
  
  askReconstructed  : TC Bool
  

  to change the behaviour of inferType, checkType, quoteTC, getContext.

• [Breaking] The type of withReconstructed has been changed from

  withReconstructed : ∀ {a} {A : Set a} →        TC A → TC A
  
  

  to

  withReconstructed : ∀ {a} {A : Set a} → Bool → TC A → TC A
  

  to match the type of primitives of the form with*.

• Two primitives onlyReduceDefs and dontReduceDefs are removed but re-implemented using the new family of primitives with* and ask* for backward compatibility.

• Blocking the type-checking monad can now be done with more precision by using the Blocker type, and the blockTC primitive:

  data Blocker : Set where
    blockerAny  : List Blocker → Blocker
    blockerAll  : List Blocker → Blocker
    blockerMeta : Meta → Blocker
  

  When blocking on a value of this type, the TCM computation will only be retried when any (resp. all) of the mentioned metavariables have been solved. This can avoid getting into loops where a macro blocks on a meta, gets unblocked, traverses some term again, and then blocks on a meta that was already present.

  The blockOnMeta builtin has been deprecated, and an implementation in terms of blockTC is given for backwards compatibility.

Other issues closed

For 2.6.4, the following issues were also closed (see bug tracker):

• #1181: Display of let-bound variables in goals and error messages
• #2271: Helper function abstracts over module parameters, with sometimes disastrous consequences for printing
• #3437: Add Propω
• #3605: Improve constraint reporting for cubical
• #3690: Cubical interaction: Display inferred type with interval variables instantiated
• #5900: De Bruijn fail in Cubical (Was: Garbled boundary contexts & naming eta expansion.)
• #6124: Reflection: cannot reduce type because variable is erased
• #6140: Unapplied List and Maybe are sometimes translated to [AgdaAny] and Maybe AgdaAny by GHC backend
• #6229: Print warning name along with warning text
• #6269: Documentation is missing for --keep-covering-clauses and --lossy-unification
• #6271: Cubical: should generated code corresponding to erased constructors be erased?
• #6272: Put Level type in a different sort
• #6309: Drop support for GHC 8.0, 8.2, and 8.4
• #6325: Hidden argument puns
• #6333: Misleading file path in “Unrecognised option” error
• #6336: Paradoxical self-reference in endpoints for path constructors
• #6364: Instance candidates filtered out by type errors
• #6371: Preserve metavariable name suggestion when eta-expanding
• #6374: Refine does not work for overloaded record constructors
• #6380: Confusing warning about turning instances into instances
• #6395: dataXXX identifiers mis-parsed by {-# COMPILE GHC #-}
• #6407: Agsy produces clauses with out of scope variables
• #6413: Miscompilation of nested patterns in erased fields
• #6415: Apparent infinite loop in cubical with –lossy-unification
• #6418: Bug in rewriting with cubical primitives
• #6434: Option to increase performance: do not filter out absurd clauses automatically
• #6448: Don’t define dependencies for elisp files included in the agda2-mode package
• #6506: Cubical: with abstraction failing to type check
• #6521: Support GHC 9.6 with cabal
• #6523: Soundness bug: Tick constraints not properly propogated in Guarded Cubical
• #6524: Ignore Unicode byte order mark
• #6525: Recent Emacs’s escape character handling improvement leads to an error when loading agda-mode
• #6528: Guarded can block on solved metas
• #6530: Miscompilation of case split RHS lambdas
• #6541: Internal error in Agda.TypeChecking.Reduce.Fast
• #6551: Doc: the keywords hiding,public, renaming, and using are always reserved
• #6573: Check on presence of --erasure in --erase-record-parameters comes too early
• #6581: Cubical: no canonicity for record types without η-equality
• #6605: Doc: comments in “libraries” file
• #6621: Enable K also for SSetω (like for SSet)
• #6622: Bad error for mutual in implicit mutual block
• #6624: Suffix not working for SSet
• #6627: CheckArguments call exposes dummy checkArguments return type
• #6632: hcompU eta rule in conversion checker loses solution
• #6633: Bad interaction of Type:Type and SSet
• #6648: --level-universe not respected when solving funSort _->_ : ? -> Set -> SetOmega
• #6651: Agda fails on univSort ? = SetOmega even when SizeUniv is a solution
• #6654: Forcing analysis is inconsistent for large indices
• #6660: {-# INLINE #-} for copattern constructors
• #6662: Error message for unsafe option combinations has wrong pluralization
• #6677: Helper function type includes generalized parameters
• #6687: Termination checker bug with CATCHALL
• #6702: Inlining constructors to copattern should give warning with --exact-split
• #6706: Shape-irrelevant variables marked as irrelevant in human-readable context
• #6711: Internal error on primStringUncons when no builtin Sigma provided
• #6714: Docstring error with Emacs 29+ due to changed escape rules for single quote
• #6715: Type checking loops on certain pattern match in cubical (regression in 2.6.3)
• #6720: Cubical: internal error in Sort.hs
• #6725: Cubical: internal error in Reduce.hs (regression in 2.6.3)
• #6750: Order of deserialization depends on build of Agda (version of hashable)
• #6757: Incorrect InteractionMetaBoundaries warning
• #6767: Internal error related to forcing on literals
• #6786: Missing “when checking parameters of module M” in error message
• #6787: Refine doesn’t find proof of refl=refl without K
• #6794: Safe Agda accepts {-# TERMINATING #-} pragma in interleaved mutual block
• #6795: Missing warning about discarded {-# TERMINATING #-} pragma in where block inside interleaved mutual block
• #6823: Suboptimal error location for missing definition before mutual block
• #6868: With-abstraction fails for trailing instance argument