Agda v2.6.3 Release Notes

Highlights
β Added support for Erased Cubical Agda, a variant of Cubical Agda that is supported by the GHC backend, under the flag
erasedcubical
.β Added a new flag
cubicalcompatible
to turn on generation of Cubical Agdaspecific support code (previously this behaviour was part ofwithoutK
).
Since
cubicalcompatible
mode implies that functions should work with the preliminary support for indexed inductive types in Cubical Agda, many pattern matching functions will now emit anUnsupportedIndexedMatch
warning, indicating that the function will not compute when applied to transports (fromcubical
code).This warning can be disabled with
WnoUnsupportedIndexedMatch
, which can be used either in anOPTIONS
pragma or in youragdalib
file. The latter is recommended if your project is onlycubicalcompatible
, or if it is already making extensive use of indexed types.π New primitives
declareData
,defineData
, andunquoteDecl data
for generating new data types have been added to the reflection API.π Thanks to a number of performance improvements, Agda 2.6.3 is about 30% faster than Agda 2.6.2.2 at typechecking the standard library with the
withoutK
flag, and 10% faster when using with the (new)cubicalcompatible
flag instead (some details can be found here).
Installation and infrastructure
π Agda supports GHC versions 8.0.2 to 9.4.3.
Erasure
 The new option
erasedcubical
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
erasedcubical
if the toplevel module uses this flag.This feature is experimental.
 The parameter arguments of constructors and record fields are now
marked as erased
(#4786), with one
exception: for indexed data types this only happens if the
withK
flag is active (#6297).
For instance, the type of the constructor
c
below is now{@0 A : Set} β D A
, and the type of the record fieldR.f
is{@0 A : Set} β R A β A
:data D (A : Set) : Set where c : D A record R (A : Set) : Set where field f : A
 β Added an option
eraserecordparameters
that additionally marks parameters to definitions in a record module as erased (#5770). For example:
{# OPTIONS eraserecordparameters #} postulate A : Set postulate a : A record R (x : A) : Set where y : A y = a f : (@0 x : A) β R x β A f x r = R.y {x} r
Cubical Agda
 π₯ [Breaking] The generation of Cubical Agdaspecific support code was removed
from
withoutK
and transferred to its own flag,cubicalcompatible
(see #5843 and #6049 for the rationale).
Note that code that uses (only)
withoutK
can no longer be imported from code that usescubical
. Thus it may make sense to replacewithoutK
withcubicalcompatible
in library code, if possible.Note also that Agda tends to be quite a bit faster if
withoutK
is used instead ofcubicalcompatible
.Note finally that when
withoutK
is used it might not be safe to compile and run programs that postulate erased univalence (but we are currently not aware of a program that would go wrong).π 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 thanSSet
. ForJ : IUniv
andA : J β Set l
, we have(j : J) β A j : Set l
, that is, the type of functions from a type inIUniv
to a fibrant type is fibrant.The option
experimentalirrelevance
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
experimentalirrelevance
cannot be used together withsafe
. A new builtin constructor
REFLID
was added to the cubical identity types. This is definitionally equal to the reflexivity identification built withconid
, with the difference being that matching onREFLID
is allowed.
symId : β {a} {A : Set a} {x y : A} β Id x y β Id y x symId reflId = reflId
Definitions which pattern match on higherinductive 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 flagnoflatsplit
has been removed, and the flagflatsplit
is now infective (see #6238 and #6263).
Matching can be enabled using the
flatsplit
flag. Note that in Cubical Agda functions that match on an argument marked with@flat
trigger theUnsupportedIndexedMatch
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
anddefineDef
. The construct
unquoteDecl
is extended with the ability of bringing a datatyped
and its constructorscβ ... cβ
given by aTC
computationm
into scope by the following syntax:
unquoteDecl data x constructor cβ .. cβ = m
A new reflection primitive
getInstances : Meta β TC (List Term)
was added toAgda.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 [email protected](meta m _) = do (cand β· _) β getInstances m where [] > typeError (strErr "No candidates!" β· []) unify hole cand pickWhatever _ = typeError (strErr "Already solved!" β· [])
π₯ [Breaking] The reflection primitives
getContext
andinContext
use a nominal contextList (Ξ£ String Ξ» _ β Arg Type)
instead ofList (Arg Type)
for printing type information better. Similarly,extendContext
takes an extra argument of typeString
.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 lambdabound variables anywhere in the righthand 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`. ```agda 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 returnMaybe Word64
. (See #6093.)
The new type is
primFloatToWord64 : Float β Maybe Word64
and it returns
nothing
forNaN
.π₯ [Breaking] The type expected by the builtin
EQUIVPROOF
has been changed to properly encode the condition thatEQUVIFUN
is an equivalence. (#5661, #6032)π₯ [Breaking] The primitive
primIdJ
has been removed (#6032) in favour of matching on the cubical identity type.π₯ [Breaking] The builtin
SUBIN
is now exported fromAgda.Builtin.Cubical.Sub
asinS
rather thaninc
. Similarly, the internal modules refer toprimSubOut
asoutS
. (#6032)
Pragmas and options
 It is now possible to declare several
BUILTIN REWRITE
relations. Example: ```agda {# OPTIONS rewriting #}
open import Agda.Builtin.Equality open import Agda.Builtin.Equality.Rewrite  1st rewrite relation
postulate R : (A : Set) β A β A β Set A : Set a b c : A foo : R A a b  using 2nd rewrite relation bar : b β‘ c  using 1st rewrite relation
{# BUILTIN REWRITE R #}  2nd rewrite relation {# REWRITE foo bar #}
test : a β‘ c test = refl
* π₯ [**Breaking**] Option `experimentallossyunification` that turns on (the incomplete) firstorder unification has been renamed to `lossyunification`. ([#1625](https://github.com/agda/agda/issues/1625)) * The new option `noloadprimitives` complements `noimportsorts` by foregoing loading of the primitive modules altogether. This option leaves Agda in a very fragile state, as the builtin sorts are used extensively throughout the implementation. It is intended to be used by Literate Agda projects which want to bind `BUILTIN TYPE` (and other primitives) in their own literate files. * If `interactionexitonerror` is used, then Agda exits with a nonzero exit code if `interaction` or `interactionjson` are used and a type error is encountered. The option also makes Agda exit with exit code 113 if Agda fails to parse a command. This option might for instance be used if Agda is controlled from a script. * Add a `NOT_PROJECTION_LIKE` pragma, which marks a function as not suitable for projectionlikeness. Projectionlike functions have some of their arguments erased, which can cause confusing behaviour when they are printed instantiated (see [#6203](https://github.com/agda/agda/issues/6203)). * π₯ [**Breaking**] The options `subtyping` and `nosubtyping` have been removed (see [#5427](https://github.com/agda/agda/issues/5427)). π Profiling and performance  * π New verbosity `v debug.time:100` adds time stamps to debugging output. * π₯ [**Breaking**] Profiling options are now turned on with a new `profile` flag instead of abusing the debug verbosity option. (See [#5781](https://github.com/agda/agda/issues/5781).) * The new profiling option `profile=conversion` collects statistics on how often various steps of the conversion algorithm are used (reduction, etaexpansion, syntactic equality, etc). * Metavariables can now be saved in `.agdai` files, instead of being expanded. This can affect performance. (See [#5731](https://github.com/agda/agda/issues/5731).) Metavariables are saved if the pragma option `savemetas` is used. This option can be overridden by `nosavemetas`. * The new option `syntacticequality[=FUEL]` can be used to limit how many times the syntactic equality shortcut is allowed to fail (see [#5801](https://github.com/agda/agda/issues/5801)). If `FUEL` is omitted, then the syntactic equality shortcut is enabled without any restrictions. If `FUEL` is given, then the syntactic equality shortcut is given `FUEL` units of fuel. The exact meaning of this is implementationdependent, but successful uses of the shortcut do not affect the amount of fuel. Currently the fuel is decreased in the failure continuations of the implementation of the syntactic equality shortcut. When a failure continuation completes the fuel is restored to its previous amount. The idea for this option comes from AndrΓ‘s KovΓ‘cs' [smalltt](https://github.com/AndrasKovacs/smalltt/blob/989b020309686e04374f1ab7844f468386d2eb2f/README.md#approximateconversionchecking). Note that this option is experimental and subject to change. Library management  * Library files below the "project root" are now ignored (see [#5644](https://github.com/agda/agda/issues/5644)). For instance, if you have a module called `A.B.C` in the directory `Root/A/B`, then `.agdalib` files in `Root/A` or `Root/A/B` do not affect what options are used to typecheck `A.B.C`: `.agdalib` files for `A.B.C` have to reside in `Root`, or further up the directory hierarchy. Interaction  * β Agsy ([automatic proof search](https://agda.readthedocs.io/en/latest/tools/auto.html)) can now be invoked in the righthandsides of copattern matching clauses. ([#5827](https://github.com/agda/agda/pull/5827)) Compiler backends  * π₯ [**Breaking**] Both the GHC and JS backends now refuse to compile code that uses `cubical`. Note that support for compiling code that uses `erasedcubical` has been added to the GHC backend (see above). * If the GHC backend is invoked when `interaction` or `interactionjson` is active (for instance when the Emacs mode is used), then GHC is now invoked from the directory containing the `MAlonzo` directory (see [#6194](https://github.com/agda/agda/issues/6194)). Before GHC was invoked from the Agda process's current working directory, and that is still the case if `interaction` and `interactionjson` are not used. DOT backend  * The new option `dependencygraphinclude=LIBRARY` can be used to restrict the dependency graph to modules from one or more libraries (see [#5634](https://github.com/agda/agda/issues/5634)). Note that the module given on the command line might not be included. * The generated graphs no longer contain "redundant" edges: if a module is imported both directly and indirectly, then the edge corresponding to the direct import is omitted. JSON API  * π₯ [**Breaking**] The JSON API now represents metavariables differently, using objects containing two keys, `id` and `module`, both with values that are (natural) numbers. See [#5731](https://github.com/agda/agda/issues/5731). Other issues closed  π For 2.6.3, the following issues were also closed (see [bug tracker](https://github.com/agda/agda/issues)):  [#3986](https://github.com/agda/agda/issues/3986): Subtyping .A > B <= A > B leads to wrong ArgInfo  [#4103](https://github.com/agda/agda/issues/4103): Rewrite rule rejected because of projection likeness  [#4506](https://github.com/agda/agda/issues/4506): Lack of unicode support in locale may result in uncaught IOException  [#4725](https://github.com/agda/agda/issues/4725): Cubical Agda: Program rejected by termination checker due to moved dot pattern  [#4755](https://github.com/agda/agda/issues/4755): Rewrite rule on constructor uses wrong type for matching  [#4763](https://github.com/agda/agda/issues/4763): Cubical Agda: Unquote anonymous copattern involving path  [#5191](https://github.com/agda/agda/issues/5191): Unifier can use erased variables in nonerased data parameters  [#5257](https://github.com/agda/agda/issues/5257): Internal error when matching on user syntax with binding  [#5378](https://github.com/agda/agda/issues/5378): Internal error with tactic on record field  [#5448](https://github.com/agda/agda/issues/5448): Should the predicate be erasable in the subst rule (withoutK)  [#5462](https://github.com/agda/agda/issues/5462): Internal error caused by a REWRITE on a projectionlike function  [#5468](https://github.com/agda/agda/issues/5468): Disallow certain forms of pattern matching when an index is erased  [#5525](https://github.com/agda/agda/issues/5525): Duplicate entries in `executables` file lead to undefined behavior  [#5548](https://github.com/agda/agda/issues/5548): Agda infers an incorrect type with subtyping on  [#5551](https://github.com/agda/agda/issues/5551): Panic when showing module contents with pattern synonym  [#5563](https://github.com/agda/agda/issues/5563): Allow erased names in the type signatures of letbound definitions  [#5577](https://github.com/agda/agda/issues/5577): The "Could not generate equivalence" warning is not always emitted  [#5581](https://github.com/agda/agda/issues/5581): Lexical error with tab character in literate Agda text  [#5589](https://github.com/agda/agda/issues/5589): Internal error with REWRITE of function from path  [#5681](https://github.com/agda/agda/issues/5681): Panic on record declaration with unknown sort  [#5702](https://github.com/agda/agda/issues/5702): Can't case split an `HitInt` with some already existing cases  [#5715](https://github.com/agda/agda/issues/5715): Reflection: Use `Telescope` for `getContext`, `inContext`, and `extendContext`  [#5727](https://github.com/agda/agda/issues/5727): Reducing universe levels before checking is not sufficient  [#5728](https://github.com/agda/agda/issues/5728): Internal error when pattern matching on `...` in with statement without providing a pattern match  [#5734](https://github.com/agda/agda/issues/5734): Relevance check in reflection  [#5751](https://github.com/agda/agda/issues/5751): json interaction produces Haskell output for SolveAll  [#5754](https://github.com/agda/agda/issues/5754): Internal error when compiling program with quoted metavariable  [#5760](https://github.com/agda/agda/issues/5760): Some code related to Cubical Agda runs also when the K rule is on  [#5763](https://github.com/agda/agda/issues/5763): Internal parser error using syntax rules  [#5765](https://github.com/agda/agda/issues/5765): Erasure check failure when pattern matching on refl in erased definition  [#5775](https://github.com/agda/agda/issues/5775): JSON interaction produces fully qualified terms  [#5794](https://github.com/agda/agda/issues/5794): Agsy/Auto crashes with `Prelude.!!: index too large`  [#5823](https://github.com/agda/agda/issues/5823): Singleton check loops on recursive eta record  [#5828](https://github.com/agda/agda/issues/5828): Agsy/Auto panics with `r` in the presence of a pattern synonym  [#5845](https://github.com/agda/agda/issues/5845): Internal error caused by abstracting `variables`  [#5848](https://github.com/agda/agda/issues/5848): Internal error with `confluencecheck`  [#5850](https://github.com/agda/agda/issues/5850): Warn about useless hiding in `variable` declaration  [#5856](https://github.com/agda/agda/issues/5856): Lambda with irrefutable pattern is not rejected when used on Path  [#5868](https://github.com/agda/agda/issues/5868): Document twolevel  [#5875](https://github.com/agda/agda/issues/5875): Instance Search breaks Termination Highlighting  [#5891](https://github.com/agda/agda/issues/5891): SizeUniv : SizeUniv is inconsistent  [#5901](https://github.com/agda/agda/issues/5901): Use emacs batch mode in agdamode setup  [#5920](https://github.com/agda/agda/issues/5920): Erased constructors skipped in modality check  [#5922](https://github.com/agda/agda/issues/5922): Failure of termination checking for reflectiongenerated code due to data projections  [#5923](https://github.com/agda/agda/issues/5923): Internal error in rewriting  [#5944](https://github.com/agda/agda/issues/5944): Internal error in rewriting with twolevel  [#5953](https://github.com/agda/agda/issues/5953): Recursor of inductiveinductive type does not pass termination check in Cubical Agda  [#5955](https://github.com/agda/agda/issues/5955): Composition of Glue Type Causes Infinite Loop  [#5956](https://github.com/agda/agda/issues/5956): Cubical Agda crashes when printing empty system  [#5966](https://github.com/agda/agda/issues/5966): Improved performance by switching to `vectorhashtables`  [#5989](https://github.com/agda/agda/issues/5989): Deadcode elimination crashes function with private tactic argument  [#6003](https://github.com/agda/agda/issues/6003): de Bruijn index out of scope when rewriting  [#6006](https://github.com/agda/agda/issues/6006): Internal error rewriting with holes  [#6015](https://github.com/agda/agda/issues/6015): Pi types and Partial types should not be considered interconvertible  [#6022](https://github.com/agda/agda/issues/6022): Private bindings in imported modules defeat check for binding of primIdFace/primIdPath  [#6042](https://github.com/agda/agda/issues/6042): De Bruijn index out of scope when rewriting withoutK  [#6043](https://github.com/agda/agda/issues/6043): de Bruijn error on unexpected implicit argument  [#6059](https://github.com/agda/agda/issues/6059): Nonterminating function over tuples passed with `terminationdepth=2`  [#6066](https://github.com/agda/agda/issues/6066): Document the meaning of `pattern` without `noetaequality`  [#6067](https://github.com/agda/agda/issues/6067): Another de Bruijn error in rewriting  [#6073](https://github.com/agda/agda/issues/6073): Constraint solving does not honour singleton types  [#6074](https://github.com/agda/agda/issues/6074): piSort/funSort of IUniv should be blocked on the codomain  [#6076](https://github.com/agda/agda/issues/6076): Agda input mode (emacs): Minibuffer display for `\;` is strange  [#6080](https://github.com/agda/agda/issues/6080): A space leak due to absName  [#6082](https://github.com/agda/agda/issues/6082): Elaborateandgive does not respect postfixprojections  [#6095](https://github.com/agda/agda/issues/6095): Ambiguous pattern synonyms broken with anonymous module  [#6112](https://github.com/agda/agda/issues/6112): Internal error: nonconfluent rewriting to singletons  [#6200](https://github.com/agda/agda/issues/6200): The reflection machinery does not treat the module telescope consistently  [#6203](https://github.com/agda/agda/issues/6203): Projectionlikeness and instance arguments  [#6205](https://github.com/agda/agda/issues/6205): Internal error with `withReconstructed`  [#6244](https://github.com/agda/agda/issues/6244): Make `noloadprimitives` not `safe`  [#6250](https://github.com/agda/agda/issues/6250): Documentation says `sizedtypes` is the default when it isn't  [#6257](https://github.com/agda/agda/issues/6257): Document options `prop`, `guarded`, and `twolevel`.  [#6265](https://github.com/agda/agda/issues/6265): Some options should be listed in `restartOptions`  [#6273](https://github.com/agda/agda/issues/6273): Missing highlighting when interleaved mutual is used  [#6276](https://github.com/agda/agda/issues/6276): LaTeX/HTML generation doesn't properly render parameters of predeclared records  [#6281](https://github.com/agda/agda/issues/6281): Special treatment of attribute followed by underscore in prettyprinter  [#6285](https://github.com/agda/agda/issues/6285): Bump to GHC 9.4.3  [#6337](https://github.com/agda/agda/issues/6337): lossyunification in Agda 2.6.3  [#6338](https://github.com/agda/agda/issues/6338): internal error in Agda, perhaps related to rewriting