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

Release notes for Agda version 2.6.3

Highlights

Added support for Erased Cubical Agda, a variant of Cubical Agda that is supported by the GHC backend, under the flag --erased-cubical.
Added a new flag --cubical-compatible to turn on generation of Cubical Agda-specific support code (previously this behaviour was part of --without-K).

Since --cubical-compatible mode implies that functions should work with the preliminary support for indexed inductive types in Cubical Agda, many pattern matching functions will now emit an UnsupportedIndexedMatch warning, indicating that the function will not compute when applied to transports (from --cubical code).

This warning can be disabled with -WnoUnsupportedIndexedMatch, which can be used either in an OPTIONS pragma or in your agda-lib file.
The latter is recommended if your project is only --cubical-compatible, or if it is already making extensive use of indexed types.

Note that code that uses (only) --without-K can no longer be imported from code that uses --cubical. Thus it may make sense to
replace --without-K with --cubical-compatible in library code, if possible.

Note also that Agda tends to be quite a bit faster if --without-K is used instead of --cubical-compatible.
Agda 2.6.3 seems to type-check one variant of the standard library about 30% faster than Agda 2.6.2.2 (on one system; the library was changed in a small way between the tests to accommodate changes to Agda). In that test the standard library did not use the new flag --cubical-compatible. With that flag enabled in all the files that used to use --without-K (and the warning UnsupportedIndexedMatch turned off) Agda 2.6.3 was still about 10% faster.
New primitives declareData, defineData, and unquoteDecl data for generating new data types have been added to the reflection API.

Installation and infrastructure

Agda supports GHC versions 8.0.2 to 9.4.4.

Erasure

The new option --erased-cubical turns on a variant of Cubical Agda (see #4701).

When this variant of Cubical Agda is used glue (and some related builtins) may only be used in erased settings. One can import
regular Cubical Agda code from this variant of Cubical Agda, but names defined using Cubical Agda are (mostly) treated as if they had
been marked as erased. See the reference manual for more details.

The GHC backend can compile code that uses --erased-cubical if the top-level module uses this flag.

This feature is experimental.

Added an option --erase-record-parameters that marks parameters to record fields and definitions in a record module as erased (see #4786 and #5770). For example:

{-# OPTIONS --erase-record-parameters #-}

record R (A : Set) : Set where
  field
    f : A

test : {@0 A : Set} → R A → A
test = R.f

Cubical Agda

[Breaking] The generation of Cubical Agda-specific support code was removed from --without-K and transferred to its own flag, --cubical-compatible (see #5843 and #6049 for the rationale).
Cubical Agda now has experimental support for indexed inductive types (#3733).
See the user guide for caveats.
The cubical interval I now belongs to its own sort, IUniv, rather than SSet.
For J : IUniv and A : J → Set l, we have (j : J) → A j : Set l, that is, the type of functions from a type in IUniv to a fibrant type is fibrant.
The option --experimental-irrelevance is now perhaps incompatible with Cubical Agda and perhaps also postulated univalence (see #5611 and #5861).

This is not meant to imply that the option was not already incompatible with those things.
Note that --experimental-irrelevance cannot be used together with --safe.
A new built-in constructor REFLID was added to the cubical identity types.
This is definitionally equal to the reflexivity identification built with conid, with the difference being that matching on REFLID is allowed.
```
symId : ∀ {a} {A : Set a} {x y : A} → Id x y → Id y x
symId reflId = reflId
```
Definitions which pattern match on higher-inductive types are no longer considered for injectivity analysis.
(#6219)
[Breaking] Higher constructors are no longer considered as guarding in the productivity check.
(#6108)
Rewrite rules with interval arguments are now supported.
(#4384)

The flat modality

[Breaking] The @flat/@♭ modality is now by default disabled (see
#4927).

It can be enabled using the infective flag --cohesion.
[Breaking] Matching on @flat arguments is now disabled by default, the flag
--no-flat-split has been removed, and the flag --flat-split is
now infective (see #6238
and #6263).

Matching can be enabled using the --flat-split flag. Note that in
Cubical Agda functions that match on an argument marked with @flat
trigger the UnsupportedIndexedMatch warning, and the code might
not compute properly.

Reflection

Two new reflection primitives

declareData      : Name → Nat → Type → TC ⊤
defineData       : Name → List (Σ Name (λ _ → Type)) → TC ⊤

are added for declaring and defining datatypes, similar to
declareDef and defineDef.

The construct unquoteDecl is extended with the ability of bringing
a datatype d and its constructors c₁ ... cₙ given by a TC
computation m into scope by the following syntax:
```
unquoteDecl data x constructor c₁ .. cₙ = m
```
A new reflection primitive getInstances : Meta → TC (List Term)
was added to Agda.Builtin.Reflection. This operation returns the
list of all possibly valid instance candidates for a given
metavariable. For example, the following macro instantiates the goal
with the first instance candidate, even if there are several:
```
macro
  pickWhatever : Term → TC ⊤
  pickWhatever hole@(meta m _) = do
    (cand ∷ _) ← getInstances m
      where [] -> typeError (strErr "No candidates!" ∷ [])
    unify hole cand
  pickWhatever _ = typeError (strErr "Already solved!" ∷ [])
```
[Breaking] The reflection primitives getContext and inContext use a nominal context
List (Σ String λ _ → Arg Type) instead of List (Arg Type) for printing
type information better. Similarly, extendContext takes an extra argument
of type String.

macro definitions can now be used even when they are declared as erased.
For example, this is now accepted:

macro
  @0 trivial : Term → TC ⊤
  trivial = unify (con (quote refl) [])

test : 42 ≡ 42
test = trivial

A new reflection primitive formatErrorParts : List ErrorPart → TC String
is added. It takes a list of ErrorPart and return its formatted string.
[Breaking] A new constructor pattErr : Pattern → ErrorPart of ErrorPart for reflection
is added.
[Breaking] The reflection primitives getType and
getDefinition respect the module context they are invoked from
instead of returning information that would be expected in the top
context.
[Breaking] The reflection primitive inContext cannot step
outside of the context that the TC computation is invoked from
anymore. The telescope is now relative to that context instead.

Syntax

It is now OK to put lambda-bound variables anywhere in the
right-hand side of a syntax declaration. However, there must always
be at least one "identifier" between any two regular "holes". For
instance, the following syntax declaration is accepted because -
is between the holes B and D.
```
postulate
  F : (Set → Set) → (Set → Set) → Set

syntax F (λ A → B) (λ C → D) = B A C - D
```

Syntax can now use lambdas with multiple arguments
(#394).

Example:

postulate
  Σ₂ : (A : Set) → (A → A → Set) → Set

syntax Σ₂ A (λ x₁ x₂ → P) = [ x₁ x₂ ⦂ A ] × P

Builtins

[Breaking] Change primFloatToWord64 to return Maybe Word64.
(See #6093.)

The new type is
```
  primFloatToWord64 : Float → Maybe Word64
```
and it returns nothing for NaN.
[Breaking] The type expected by the builtin EQUIVPROOF has been changed to
properly encode the condition that EQUVIFUN is an equivalence.
(#5661,
#6032)
[**Breaking...

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Release notes for Agda version 2.6.4

Highlights

Installation

Pragmas and options

Library management

Interaction and emacs mode

Syntax

Language

Contributors

Uh oh!

Release notes for Agda version 2.6.3

Highlights

Installation and infrastructure

Erasure

Cubical Agda

The flat modality

Reflection

Syntax

Builtins

Contributors

Uh oh!

Releases: agda/agda

v2.6.4

Release notes for Agda version 2.6.4

Highlights

Installation

Pragmas and options

Library management

Interaction and emacs mode

Syntax

Language

Contributors

Uh oh!

v2.6.3

Release notes for Agda version 2.6.3

Highlights

Installation and infrastructure

Erasure

Cubical Agda

The flat modality

Reflection

Syntax

Builtins

Contributors

Uh oh!