Release notes for Agda version 2.6.4 ==================================== Highlights ---------- * Cubical Agda now displays boundary conditions in interactive mode (PR [#6529](https://github.com/agda/agda/pull/6529)). * An inconsistency in the treatment of large indices has been fixed (Issue [#6654](https://github.com/agda/agda/issues/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.2. 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](https://agda.readthedocs.io/en/v2.6.4/tools/command-line-options.html#cmdoption-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](https://github.com/agda/agda/issues/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-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](https://github.com/agda/agda/pull/6682)). For example, this translation allows the `nats` function to pass termination checking: ```agda 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: ```agda 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](#language) 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. 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](https://github.com/agda/agda/issues/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 ```elisp (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](https://github.com/agda/agda/issues/2271)) and neither over generalized `variable`s (see [#6689](https://github.com/agda/agda/pull/6689)). * New Agda input mode prefix `box` for APL boxed operators, e.g. `\box=` for ⌸; see PR [#6510](https://github.com/agda/agda/pull/6510/files) 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](https://github.com/agda/agda/pull/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](https://github.com/agda/agda/issues/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](https://github.com/agda/agda/issues/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}) → …`. 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](https://github.com/agda/agda/issues/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](https://agda.readthedocs.io/en/v2.6.4/language/opaque-definitions.html), 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: ```agda 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](https://github.com/agda/agda/pull/6634)). * New sorts `Propω`, `Propω₁`, etc., in analogy to `Setω`, `Setω₁` etc. Requires option `--prop`. Example: ```agda {-# 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](https://github.com/agda/agda/issues/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](https://github.com/agda/agda/issues/4786)), with one exception: for indexed data types this only happens if the `--with-K` flag is active ([#6297](https://github.com/agda/agda/issues/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`: ```agda {-# 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](https://github.com/agda/agda/issues/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](https://github.com/agda/agda/issues/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: ```agda 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: ```agda 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](https://github.com/agda/agda/issues/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: ```agda 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: ```agda 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: ```agda 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: ```agda pragmaForeign : String → String → TC ⊤ pragmaCompile : String → Name → String → TC ⊤ ``` * Add 4 reflection primitives of the form `ask*` and `with*`: ```agda 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 ```agda withReconstructed : ∀ {a} {A : Set a} → TC A → TC A ``` to ```agda 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: ```agda 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](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.4+is%3Aclosed) (see [bug tracker](https://github.com/agda/agda/issues)): - [#1181](https://github.com/agda/agda/issues/1181): Display of let-bound variables in goals and error messages - [#3437](https://github.com/agda/agda/issues/3437): Add Propω - [#3605](https://github.com/agda/agda/issues/3605): Improve constraint reporting for cubical - [#3690](https://github.com/agda/agda/issues/3690): Cubical interaction: Display inferred type with interval variables instantiated - [#5900](https://github.com/agda/agda/issues/5900): De Bruijn fail in Cubical (Was: Garbled boundary contexts & naming eta expansion.) - [#6124](https://github.com/agda/agda/issues/6124): Reflection: cannot reduce type because variable is erased - [#6140](https://github.com/agda/agda/issues/6140): Unapplied `List` and `Maybe` are sometimes translated to `[AgdaAny]` and `Maybe AgdaAny` by GHC backend - [#6229](https://github.com/agda/agda/issues/6229): Print warning name along with warning text - [#6271](https://github.com/agda/agda/issues/6271): Cubical: should generated code corresponding to erased constructors be erased? - [#6272](https://github.com/agda/agda/issues/6272): Put Level type in a different sort - [#6309](https://github.com/agda/agda/issues/6309): Drop support for GHC 8.0, 8.2, and 8.4 - [#6325](https://github.com/agda/agda/issues/6325): Hidden argument puns - [#6333](https://github.com/agda/agda/issues/6333): Misleading file path in "Unrecognised option" error - [#6336](https://github.com/agda/agda/issues/6336): Paradoxical self-reference in endpoints for path constructors - [#6364](https://github.com/agda/agda/issues/6364): Instance candidates filtered out by type errors - [#6371](https://github.com/agda/agda/issues/6371): Preserve metavariable name suggestion when eta-expanding - [#6374](https://github.com/agda/agda/issues/6374): Refine does not work for overloaded record constructors - [#6380](https://github.com/agda/agda/issues/6380): Confusing warning about turning instances into instances - [#6395](https://github.com/agda/agda/issues/6395): `dataXXX` identifiers mis-parsed by {-# COMPILE GHC #-} - [#6407](https://github.com/agda/agda/issues/6407): Agsy produces clauses with out of scope variables - [#6413](https://github.com/agda/agda/issues/6413): Miscompilation of nested patterns in erased fields - [#6415](https://github.com/agda/agda/issues/6415): Apparent infinite loop in cubical with --lossy-unification - [#6418](https://github.com/agda/agda/issues/6418): Bug in rewriting with cubical primitives - [#6434](https://github.com/agda/agda/issues/6434): Option to increase performance: do not filter out absurd clauses automatically - [#6448](https://github.com/agda/agda/issues/6448): Don't define dependencies for elisp files included in the agda2-mode package - [#6506](https://github.com/agda/agda/issues/6506): Cubical: `with` abstraction failing to type check - [#6521](https://github.com/agda/agda/issues/6521): Support GHC 9.6 with cabal - [#6523](https://github.com/agda/agda/issues/6523): Soundness bug: Tick constraints not properly propogated in Guarded Cubical - [#6524](https://github.com/agda/agda/issues/6524): Ignore Unicode byte order mark - [#6525](https://github.com/agda/agda/issues/6525): Recent Emacs's escape character handling improvement leads to an error when loading agda-mode - [#6528](https://github.com/agda/agda/issues/6528): Guarded can block on solved metas - [#6530](https://github.com/agda/agda/issues/6530): Miscompilation of case split RHS lambdas - [#6541](https://github.com/agda/agda/issues/6541): Internal error in Agda.TypeChecking.Reduce.Fast - [#6551](https://github.com/agda/agda/issues/6551): Doc: the keywords `hiding`,`public`, `renaming`, and `using` are always reserved - [#6573](https://github.com/agda/agda/issues/6573): Check on presence of `--erasure` in `--erase-record-parameters` comes too early - [#6581](https://github.com/agda/agda/issues/6581): Cubical: no canonicity for record types without η-equality - [#6605](https://github.com/agda/agda/issues/6605): Doc: comments in "libraries" file - [#6621](https://github.com/agda/agda/issues/6621): Enable K also for SSetω (like for SSet) - [#6622](https://github.com/agda/agda/issues/6622): Bad error for `mutual` in implicit mutual block - [#6624](https://github.com/agda/agda/issues/6624): Suffix not working for SSet - [#6627](https://github.com/agda/agda/issues/6627): CheckArguments call exposes dummy checkArguments return type - [#6632](https://github.com/agda/agda/issues/6632): hcompU eta rule in conversion checker loses solution - [#6633](https://github.com/agda/agda/issues/6633): Bad interaction of Type:Type and SSet - [#6648](https://github.com/agda/agda/issues/6648): `--level-universe` not respected when solving funSort `_->_ : ? -> Set -> SetOmega` - [#6651](https://github.com/agda/agda/issues/6651): Agda fails on `univSort ? = SetOmega` even when `SizeUniv` is a solution - [#6654](https://github.com/agda/agda/issues/6654): Forcing analysis is inconsistent for large indices - [#6660](https://github.com/agda/agda/issues/6660): `{-# INLINE #-}` for copattern constructors - [#6662](https://github.com/agda/agda/issues/6662): Error message for unsafe option combinations has wrong pluralization - [#6677](https://github.com/agda/agda/issues/6677): Helper function type includes generalized parameters - [#6687](https://github.com/agda/agda/issues/6687): Termination checker bug with CATCHALL - [#6702](https://github.com/agda/agda/issues/6702): Inlining constructors to copattern should give warning with `--exact-split` - [#6706](https://github.com/agda/agda/issues/6706): Shape-irrelevant variables marked as irrelevant in human-readable context - [#6711](https://github.com/agda/agda/issues/6711): IMPOSSIBLE internal error on primStringUncons when no builtin Sigma provided - [#6714](https://github.com/agda/agda/issues/6714): Compiling Agda HEAD with Emacs 29+ reports docstring error - [#6715](https://github.com/agda/agda/issues/6715): Type checking loops on certain pattern match in cubical - [#6720](https://github.com/agda/agda/issues/6720): Cubical: IMPOSSIBLE in Sort.hs during checking with cubical - [#6725](https://github.com/agda/agda/issues/6725): Cubical: IMPOSSIBLE in Reduce.hs