Changelog of @hackage/Agda 2.6.1

Release notes for Agda version 2.6.1

General

Agda now has an official logo: (https://github.com/agda/agda/blob/master/doc/user-manual/agda.svg). The logo was chosen by the Agda community from a list of candidates. The winning design was submitted by Miëtek Bak. The list of candidates and the outcome of the poll can be consulted here.

Installation and infrastructure

Added support for GHC 8.8.2 [Issue #4285].
Removed support for GHC 7.10.3.
Interface files are now written in directory _build/VERSION/agda/ at the project root (the closest enclosing directory where an .agda-lib file is present). If there is no project root then the interface file is written alongside the module it corresponds to. The flag --local-interfaces forces Agda to revert back to storing interface files alongside module files no matter what.
Agda now uses the default RTS options -M3.5G -I0. If you run Agda on a 32-bit system or a system with less than 8GB of RAM, it is recommended to set the RTS options explicitly to a lower value by running agda with option +RTS -M1.2G -RTS (for example) or by setting the GHCRTS enviroment variable. See the GHC User's Guide for more information.
If Agda is compiled using GHC 8.4 or later, then one can expect to see substantially lower memory consumption [Issues #4457 and #4316].

This is due to the use of "compact regions".
The CHANGELOG.md was split. Changes to previous versions of Agda are in the directory doc/release-notes.

Pragmas and options

New pragma WARNING_ON_IMPORT to let module authors raise a warning when a module is imported. This can be use to tell users deprecations.
New option --confluence-check (off by default) enables confluence checking of user-defined rewrite rules (this only has an effect when --rewriting is also enabled).
New option --no-projection-like to turn off the analysis whether a type signature likens that of a projection. Projection-likeness is an optimization that reduces the size of terms by dropping parameter-like reconstructible function arguments. Thus, it is advisable to leave this optimization on, the flag is meant for debugging Agda.
Option --no-forcing is now a pragma option, i.e., the forcing analysis can be switched off on a per-file basis via
```
{-# OPTIONS --no-forcing #-}
```
at the beginning of the file [Issue #3872].
New pragma option --no-flat-split disables pattern matching on @♭ arguments.
New pragma option --allow-incomplete-matches. It is similar to --allow-unsolved-metas: modules containing partial function definitions can be imported. Its local equivalent is the NON_COVERING pragma to be placed before the function (or the block of mutually defined functions) which the user knows to be partial.
Option --interaction-json now brings more information about goals, unsolved metas, warnings, errors. It also displays pretty-printed terms.
New pragma option --keep-pattern-variables to prevent case splitting from replacing variables with dot patterns.
Pragma {-# ETA <record name> #-} is no longer considered --safe. See [Issue #4450].
New pragma options --subtyping and --no-subtyping (default) to turn on/off subtyping rules globally [see Issue_#4474]. Currently, this includes subtyping for irrelevance, erasure, and flat modalities. Additionally, --subtyping is implied by --cumulativity (see below). --subtyping is currently NOT implied by --sized-types, and subtyping for sized types is used even when --subtyping is not enabled.
New profiling options to measure time spent per module or top-level definition.
- -v profile.modules:10 prints a breakdown per top-level module
- -v profile.definitions:10 prints a breakdown per top-level definition

Language

Syntax

Fractional precedence levels are now supported, see Issue #3991. Example:
```
infix 3.14 _<_
```
Note that this includes a respective change in the reflected Agda syntax.
Fixities can now be changed during import in a renaming directive, see Issue #1346. Example:
```
open M using (_∙_)
open M renaming (_∙_ to infixl 10 _*_)
```
After this, _∙_ is in scope with its original fixity, and as _*_ as left associative operator of precedence 10.
Implicit non-dependent function spaces {A} → B and {{A}} → B are now supported.
Idiom brackets

Idiom brackets can accommodate none or multiple applications separated by a vertical bar | if there are two additional operations
```
empty : ∀ {A} → F A
_<|>_ : ∀ {A} → F A → F A → F A
```
i.e. an Alternative type class in Haskell. As usual, the new idiom brackets desugar before scope checking.

Idiom brackets with multiple applications
```
(| e₁ a₁ .. aₙ | e₂ a₁ .. aₘ | .. | eₖ a₁ .. aₗ |)
```
expand to (assuming right associative _<|>_)
```
(pure e₁ <*> a₁ <*> .. <*> aₙ) <|> ((pure e₂ <*> a₁ <*> .. <*> aₘ) <|> (pure eₖ <*> a₁ <*> .. <*> aₗ))
```
Idiom brackets with no application (|) or ⦇⦈ are equivalent to empty.
Irrefutable With

Users can now match on irrefutable patterns on the LHS using a pattern-matching with. An expression of the form:
```
f xs with p1 <- e1 | ... | pn <- en
     with q1 <- f1 | ... | qm <- fm = rhs
```
is translated to nested with clauses, essentially equivalent to:
```
f xs with e1 | ... | en
... | p1 | ... | pn
     with f1 | ... | fm
... | q1 | ... | qm = rhs
```
Record patterns in telescopes

Users can now use record patterns in telescope and lambda abstractions. The type of the second projection from a dependent pair is the prototypical example It can be defined as follows:
```
snd : ((a , _) : Σ A B) → B a
```
And this second projection can be implemented with a lamba-abstraction using one of these irrefutable patterns:
```
snd = λ (a , b) → b
```
Using an as-pattern, users can get a name for the value as well as for its subparts. We can for instance prove that any pair is equal to the pairing of its first and second projections:
```
eta : (p@(a , b) : Σ A B) → p ≡ (a , b)
eta p = refl
```
Absurd match in a do block The last expression in a do block can now also be an absurd match () <- f.

Named where modules are now in scope in the rhs of the clause (see Issue #4050). Example:

record Wrap : Set₂ where
  field wrapped : Set₁

test : Wrap
test = record { M }
  module M where
    wrapped : Set₁
    wrapped = Set

{{- is now lexed as { {- rather than {{ -, see Issue #3962.
Syntax for large numbers: you can now separate groups of 3 digits using _. e.g. write 1_000_000 instead of 1000000.
quoteGoal and quoteContext are no longer keywords.
Record constructors can no longer be qualified by the record module. (See Issue #4189.)
```
record Foo : Set where
  constructor foo

works = foo
fails = Foo.foo
```
codata definitions have been removed from the concrete syntax Previously they got accepted syntactically, but resulted in errors.
Imports can now be anonymous. (See Issue_#3727.) For example, the following will not bring Agda.Builtin.Unit into scope:
```
open import Agda.Builtin.Unit as _
blah :: ⊤
blah = tt
```

Type checking

Type inference for record expressions no longer considers record types from modules that have not been imported (Issue #4267).

For instance,

-- A.agda
module A where
  record R : Set₁ where
    field f : Set

-- B.agda
module B where
  import A

-- C.agda
module C where
  import B
  fails : Set → _
  fails X = record {f = X}  -- import A required to infer record type R

The fix of issue #3903 changes the algorithm computing the order of case splits, which in some cases may lead to unsolved metavariables in previously working code. See issue #4353.

Modalities

New Flat Modality

New modality @♭/@flat (previously only available in the branch "flat"). An idempotent comonadic modality modeled after spatial/crisp type theory. See Flat Modality in the documentation for more.
New run-time erasure modality (@0 / @erased). Terms marked as erased cannot influence computations and are erased at run time [Issue #3855]. See Run-time Irrelevance in the documentation for more information.

Note that this feature can cause previously solved metavariables to become unsolved even in code that doesn't use run-time erasure (see issue #4174).
Subtyping rules for modalities are by default no longer used (see Issue_#4390). For example, if f : .A → A, Agda no longer accepts f at type A → A. Instead, Agda accepts λ x → f x : A → A. The same holds for erasure (@0) and flat (@♭) modalities. Consequently, it may be required to eta-expand certain functions in order to make old code work with Agda 2.6.1. Alternatively, enabling the new --subtyping flag will restore the old behaviour but might negatively impact typechecking performance.

Universe levels

New (experimental) option --cumulativity

When the --cumulativity flag is enabled, Agda uses the subtyping rule Set i =< Set j whenever i =< j. For example, in addition to its usual type Set, Nat also has the type Set₁ and even Set i for any i : Level. More information about this new option can be found in section Cumulativity of the user manual.

Termination checking

The "with inlining" feature of the termination checker has been removed. As a consequence, some functions defined using with are no longer accepted as terminating. See Issue #59 for why this feature was originally introduced and #3604 for why it had to be removed.

The easiest way to fix termination problems caused by with is to abstract over the offending recursive call before any other withs. For example

data D : Set where
  [_] : Nat → D

fails : D → Nat
fails [ zero  ] = zero
fails [ suc n ] with some-stuff
... | _ = fails [ n ]

This fails termination because the relation between [ suc n ] and [ n ] is lost since the generated with-function only gets passed n. To fix it we can abstract over the recursive call:

fixed : D → Nat
fixed [ zero  ] = zero
fixed [ suc n ] with fixed [ n ] | some-stuff
... | rec | _ = rec

If the function takes more arguments you might need to abstract over a partial application to just the structurally recursive argument. For instance,

fails : Nat → D → Nat
fails _ [ zero  ] = zero
fails _ [ suc n ] with some-stuff
... | m = fails m [ n ]

fixed : Nat → D → Nat
fixed _ [ zero  ] = zero
fixed _ [ suc n ] with (λ m → fixed m [ n ]) | some-stuff
... | rec | m = rec m

A possible complication is that later with-abstractions might change the type of the abstracted recursive call:

T      : D → Set
suc-T  : ∀ {n} → T [ n ] → T [ suc n ]
zero-T : T [ zero ]

fails : (d : D) → T d
fails [ zero  ] = zero-T
fails [ suc n ] with some-stuff
... | _ with [ n ]
...   | z = suc-T (fails [ n ])

still-fails : (d : D) → T d
still-fails [ zero ] = zero-T
still-fails [ suc n ] with still-fails [ n ] | some-stuff
... | rec | _ with [ n ]
...   | z = suc-T rec -- Type error because rec : T z

To solve this problem you can add rec to the with-abstraction messing up its type. This will prevent it from having its type changed:

fixed : (d : D) → T d
fixed [ zero ] = zero-T
fixed [ suc n ] with fixed [ n ] | some-stuff
... | rec | _ with rec | [ n ]
...   | _ | z = suc-T rec

The termination checker will now try to dispose of recursive calls by reducing with the non-recursive function clauses. This eliminates false positives common for definitions by copatterns using dependent types, see Issue #906.

For example, consider the following example using a dependent coinductive record Tree:
```
data Fin : Nat → Set where
  fzero : ∀ n → Fin (suc n)
  fsuc  : ∀ n (i : Fin n) → Fin (suc n)

toNat : ∀ n → Fin n → Nat
toNat .(suc n) (fzero n)  = zero
toNat .(suc n) (fsuc n i) = suc (toNat n i)

record Tree : Set where
  coinductive
  field label : Nat
        child : Fin label → Tree
open Tree

tree : Nat → Tree
tree n .label   = n
tree n .child i = tree (n + toNat _ i)
```
Agda solves the underscore by tree n .label, which is a corecursive call in a non-guarded position, violating the guardedness criterion. This lead to a complaint of the termination checker. Now this call is reduced to n first using the non-recursive clause tree n .label = n, which leaves us only with the guarded call tree (n + toNat n i), and the termination checker is happy.

Note: Similar false positives arose already for non-recursive dependent records, e.g., when trying to define an inhabitant of the Σ-type by copattern matching on the projects. See Issue_#2068 for a non-recursive example.

Irrelevance and Prop

Agda will no longer reduce irrelevant definitions and definitions with a type in Prop. This does not have an effect on the semantics, but should lead to improved performance (see Issues #4115, #4118, #4120, #4122).
Terms of a type in Prop are now printed as _. To show the actual term, you can use the --show-irrelevant flag (see Issue #3337.

Rewrite rules

Rewrite rules (option --rewriting) with data or record types as the head symbol are no longer allowed (see Issue #3846).

Tactics & Reflection

Implicit arguments solved by user-defined tactics

You can declare tactics to be used to solve a particular implicit argument using the following syntax:
```
example : {@(tactic f) x : A} → B
```
where f : Term → TC ⊤. At calls to example, f is called on the metavariable inserted for x. f can be an arbitrary term and may depend on previous arguments to the function. For instance,
```
example₂ : (depth : Nat) {@(tactic search depth) x : A} → B
```
Record fields can also be annotated with a tactic, allowing them to be omitted in constructor applications, record constructions and co-pattern matches:
```
record Example : Set where
  constructor mkExample
  field x : A
        @(tactic solveP x) {y} : P x
```
where solveP : (x : A) → Term → TC ⊤ is a tactic that tries to prove P x [Issue #4124].
The legacy reflection framework using quoteGoal and quoteContext has been removed.

Builtins

New primitives

primWord64ToNatInjective    : ∀ a b → primWord64ToNat a ≡ primWord64ToNat b → a ≡ b

primFloatToWord64           : Float → Word64
primFloatToWord64Injective  : ∀ a b → primFloatToWord64 a ≡ primFloatToWord64 b → a ≡ b

primMetaToNat               : Meta → Nat
primMetaToNatInjective      : ∀ a b → primMetaToNat a ≡ primMetaToNat b → a ≡ b

primQNameToWord64s          : Name → Word64 × Word64
primQNameToWord64sInjective : ∀ a b → primQNameToWord64s a ≡ primQNameToWord64s b → a ≡ b

These can be used to define safe decidable propositional equality, see Issue agda-stdlib#698.

New Primitive for showing Natural numbers:
```
primShowNat : Nat → String
```
placed in Agda.Builtin.String.
The builtin IO has been declared strictly positive in both its level and type argument.

Warnings

New warning for a variable shadowing another in a telescope. If the two variables are introduced in different telescopes then the warning is not raised.
```
f : {a : Level} {A : Set a} (a : A) → A   -- warning raised: repeated a
g : {a : Level} {A : Set a} → (a : A) → A -- warning not raised: two distinct telescopes
```
Note that this warning is turned off by default (you can use -WShadowingInTelescope or --warning ShadowingInTelescope to turn it on, -Wall would also naturally work).

Emacs mode

Agda input method: new key bindings \ G h and \ G H for η and H (capital η) [Issue #3856].
Syntax highlighting: in literate modes, the pure texts (other than Agda code and the code-text separators) are no longer highlighted (it was highlighted as comments before). This somehow provides more information about how Agda lexes literate files.
Agda now also displays the values of let-bound variables in the context instead of just their types [Issue #4199].
Agda will now try to preserve the ellipsis (...) during case splitting when possible. To manually expand the ellipsis, you may ask Agda to case split on the special identifier ..

Agda will now also show variables named _ in the context if they are instance arguments (see #4307). Instance arguments are now also marked as (instance) in the context. Example:

f : {{_ : A}} → A
f = ?

Agda will now display the goal as follows:

Goal: A
————————————————————————————————————————————————————————————
_ : A   (instance)

It is now possible to ask Agda to terminate itself after any previously invoked commands have completed, by giving a prefix argument to agda2-term.
The command agda2-measure-load-time has been removed.

GHC Backend

Types which have a COMPILE GHC pragma are no longer erased [Issue #3732].
```
data I : Set where
  bar : I

{-# FOREIGN GHC data I = Bar     #-}
{-# COMPILE GHC I = data I (Bar) #-}

data S : Set where
  foo :  I → S

{-# FOREIGN GHC data S = Foo I #-}
{-# COMPILE GHC S = data S (Foo) #-}
```
Previously [Issue #2921], the last binding was incorrect, since the argument of singleton type I was erased from the constructor foo during compilation. The required shape of S was previously
```
{-# FOREIGN GHC data S = Foo #-}
```
i.e., constructor Foo had to have no arguments.

For the sake of transparency, Haskell constructors bound to Agda constructors now take the same arguments. This is especially important if Haskell bindings are to be produced automatically by third party tool.

LaTeX backend

Now the code environment complains if it is given unrecognised options.

It is also possible to write, say, hide=true instead of hide, and hide=false means that the hide option should not be used. Furthermore the same option can be given multiple times, in which case later choices take precedence over earlier ones.
The code environment has a new option, number.

When the option number is used an equation number is generated for the code listing. The number is set to the right, centered vertically. By default the number is set in parentheses, but this can be changed by redefining \AgdaFormatCodeNumber.

The option can optionally be given an argument: when number=l is used a label l, referring to the code listing, is generated. It is possible to use this option several times with different labels.

The option has no effect if used together with hide, inline or inline*.

API

Removed module Agda.Utils.HashMap. It only re-exported Data.HashMap.Strict from the package unordered-containers. Use Data.HashMap.Strict instead.
Removed module Agda.Utils.Char. It used to provide functions converting a Char in base 8, 10, and 16 to the corresponding Int. Use digitToInt in Data.Char instead. The rest of module was about Unicode test which was not used.
Agda.Utils.List no longer provides headMaybe. Use listToMaybe in Data.Maybe instead.
Agda.Utils.Either no longer provides mapEither. Use bimap in Data.Bifunctor instead.
Agda.Utils.Map no longer provides unionWithM, insertWithKeyM, allWithKey, unzip, and unzip3.

Other issues

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

#470: Constraint solving in heterogenous situations
#471: Emacs command to show goal with constraints on it
#500: Allow creation of implicit parameters in with blocks
#543: Irrelevant projections are inconsistent
#760: Warning for open public in an abstract block
#1073: Solve C-c C-s inserts variables that are not in scope
#1097: Allow record patterns in lambda-bound positions
#1182: Request: allowing the use of patterns in syntax-bound variables
#1381: Termination checker rejects function with with-clause
#1445: Lack of subject reduction with REWRITE
#1820: Case splitting should preserve existing names
#2068: Copattern matching: Hyvernat termination would succeed
#2148: Option to use use stack exec for GHC backend
#2170: Two equal irrelevant definitions: one is type checked, the other is not
#2284: Disallow duplicate bound variable in lambda and pi
#2414: Case splitting loses as-patterns
#2498: Resolution of unnamed instances
#2512: Propose: Split the changelog
#2530: --ignore-interfaces should not recompile Primitive.agda
#2535: Expose name id in reflection API
#2589: Preserve the ellipsis (dots) when case splitting "with" arguments
#2610: Avoid rechecking by storing interfaces in separate directories?
#2619: Feature request: link to renaming clause
#2902: Case-splitting should not generate patterns containing pattern synonyms
#3034: Pattern matching without K seemingly illogical for the inductive family of squares
#3073: type-in-type and spurious levels
#3081: Termination problem: copatterns and without-K
#3089: Nicer syntax for implicit @-patterns
#3095: Would like to make hidden variable visible but it is created ambiguous
#3136: Spurious module parameters printed in extended lambda in termination error
#3189: No information about which warnings are enabled by default
#3233: Type declarations not accompanied by a definition should be highlighted in the emacs mode
#3238: Printing of inserted hidden lambdas
#3293: Absurd match in a do block
#3295: Allow import of files with incomplete pattern matching
#3353: Case splitting turns named arguments into positional arguments
#3383: Document the DISPLAY pragma
#3417: No highlighting for code that fails termination checking when an error is encountered
#3423: Implicit arguments with custom macro for resolution
#3432: Highlighting does not work for pattern synonyms in import lists
#3493: Impossible to normalize elements in a proposition
#3525: Rewrite rules with non-linear patterns do not work in presence of Prop
#3545: JavaScript backend: mapping a function that returns Set fails
#3574: Support precedent rebind / changing the precedents in builtin library
#3582: Error message referring to Set instead of Prop
#3594: Occurs check throws error when a solution is possible by eta expansion
#3599: Bad performance on pathToEquiv
#3606: Do not create/display superfluous metas and show constraints in a readable way
#3654: Show non-blocked constraints first in list of unsolved constraints
#3695: Generalisation introduces multiple explicit arguments for one generalisable variable
#3698: Remove primComp?
#3712: Sigma not listed in Built-ins documentation
#3724: Internal error with Prop and inductive-inductive type
#3725: Support GHC 8.8.1
#3730: Internal error resulting from unused implicit argument
#3735: Incorrect context when generalisable variable is used
#3736: Safe decidability equality support for Name and Meta
#3745: Update user manual on built-ins
#3749: Inconsistency: Rounding op differentiates NaNs
#3759: Change the default RTS options?
#3774: de Bruijn index out of scope with rewrite rules
#3776: Conversion check fails too quickly when type could be eta unit type
#3779: Incorrectly ordered generalised variables
#3785: Comparison of blocked terms doesn't respect eta
#3791: Asking Agda to solve a constraint inside a macro
#3803: Parse empty field lists
#3805: Agda prelude: Internal error at src/full/Agda/TypeChecking/Reduce/Fast.hs:1347
#3807: Internal error related to generalisable variables
#3812: Rewriting projected symbols leads to loss of subject reduction
#3813: Destructuring leads to invalid premises
#3818: For open import M, Agda should remember that M is an external module
#3824: rewrite drops named where module
#3825: record{M} syntax reports unsolved metas in module M instead of in record expression
#3828: Internal error in Agda/TypeChecking/Coverage.hs:467
#3829: Case-split: don't generate pattern covered by unreachable clause
#3830: primShow(Char/String) display spurious square brackets
#3831: Wrong de Bruijn indices for reflected variables inside an extended context
#3843: Internal error with-clause and unification
#3851: C-c C-h should default to AsIs rather than Simplified
#3866: --no-unicode option producing unicode variable names
#3878: Case splitting should respect existing input
#3879: Only unqualified pattern synonyms should be used for resugaring
#3882: de Bruijn index out of scope
#3892: Internal error with data .. where definitions
#3898: Forcing analysis sensitive to normalization
#3900: Abstract constructor not usable in function definition involving "with"
#3901: Unnamed implicit non-dependent function space {A} -> B and {{A}} -> B
#3912: Generalisable variables generate unknown and explicit parameters
#3919: Case splitting fails in parameterized module
#3927: import … hiding … should be documented
#3928: The error message Hiding … has no effect should be improved
#3930: BUILTIN NATURAL internal error at Forcing.hs:232
#3932: Internal error when mixing implicit and explicit mutual blocks
#3937: Internal error at "ConcreteToAbstract:1372"
#3940: Weird error with piSort and generalization
#3943: Print also hidden problematic unification terms
#3955: Document module keyword in using/hiding/renaming
#3956: Duplicate name in environment buffer with @-pattern
#3964: Agda overwrites user-written dotted pattern
#3965: Wrong indication of unreachable clauses
#3966: All clauses marked when one clause has unification error
#3972: Unreachable clause leads to internal error at Serialise/Instances/Internal.hs:94 (MetaV)
#3974: Range for unexpected implicit argument on lhs too big
#3983: TERMINATING accepted with --safe if hidden in a block
#3989: Warn about duplicate bindings in a single telescope
#4000: How to get Agda to ignore ~/.agda?
#4006: Internal error related to abstract and variable
#4007: Cannot give pattern-matching lambda in abstract setting
#4010: unquoteDef fails in abstract block
#4012: Internal error when accessing abstract definitions created by unquoteDef/Decl
#4020: Rewriting incorrectly considers level variables under lambdas as unbound in the LHS
#4032: Loss of subject reduction involving --rewriting even when --confluence-check is on and everything passes the confluence checker
#4038: Rewriting sometimes fails to rewrite in the presence of unsolved metas
#4044: Equality checking uses too much memory in 2.6.0 (compared to 2.5.4)
#4046: Remove (deprecated) codata keyword
#4048: Rewriting rule fails to trigger
#4049: Internal error with sized types if the target type of a constructor is an alias
#4051: Internal error when importing a module with a hole in a type
#4053: Emacs-mode: Case split leaves part of old line behind
#4059: Two variants of irrefutable with?
#4066: Regression related to instance resolution
#4116: Internal error Forcing.hs:232
#4121: Pattern synonyms cannot be made private
#4125: Type checker normalizes too much
#4134: Internal error triggered by missing check for irrelevant meta dependencies
#4136: Overzealous pruning of metavariable with irrelevant argument
#4141: Printing of DontCare should not use dot syntax
#4142: defCopatternLHS needs to be set when record expression were translated to copatterns
#4148: Internal error related to records and type-level indices
#4152: Variables in Prop position should not raise hard error in occurs check
#4154: Renaming declarations within a module may cause name clash
#4158: Double check failure (unaware of rewrite rule)
#4163: pattern matching in parametrized module leads to ill-typed definitions in where modules.
#4170: Tactic causes Agda to enter into an infinite loop
#4179: Coverage check false positive
#4185: Agda uses η-equality for record types defined with no-eta-equality
#4205: Internal error in connection with with, copatterns, and open record
#4211: Cannot add as-pattern on literal pattern
#4214: with abstraction fails with HIT constructors in the goal
#4215: Case splitting should respect Nat literals
#4255: Hole filler accepted, but type check error on reload
#4261: Order of arguments affects lambda pattern matching
#4268: Give failure with large quantification
#4269: Universe levels are not solved
#4283: DeBruijn issue(?) in standard library tests
#4289: datatype scope and import guidelines
#4297: Missing documentation: NO_UNIVERSE_CHECK pragma
#4310: Anonymous .. binder should not lead to a parse error
#4314: Internal error with generalize
#4320: Path constructor overloading
#4323: Internal error (Rewriting.hs:395) with generalize and rewrite rules
#4330: Equations for cubical subtypes
#4348: Seemingly needless repetition of highlighting of warnings
#4360: Missing warning for declaring constructor instances for records with explicit fields
#4361: Inconsistent highlighting of BUILTING EQUALITY/REWRITE
#4371: Inconsistency with rewrite rules and assumptions in Prop
#4373: Non-imported instances are used for instance resolution
#4375: Internal error in Agda/TypeChecking/Monad/Context.hs:120
#4380: Parse error with instance constructor and end of file
#4382: Rewriting and records with eta
#4387: Less responsive Emacs mode in v2.6.1 release candidate 1
#4390: Unification finds solution with bound variable used at wrong modality
#4391: Termination checking failed with guardedness
#4399: Case split on unnamed argument produces non-sensical code
#4401: Missing check on context variables leads to Set:Set with --cumulativity
#4404: Disambiguation fails in Cubical Agda
#4410: Rewrite rule matching does not respect Prop
#4447: Positivity: internal error with projection in constructor type
#4451: Highlighting: use several lookups rather than merging hash-maps?
#4452: Compiler error when using REWRITE
#4469: The warning machinery does not work correctly when interface files are involved

The following previously closed issues were reopened:

#1556: Agda allows "very dependent" types