Changelog for Agda-2.7.20250510

Release notes for Agda version 2.8.0

Highlights

Agda is now a self-contained single binary.
Build all Agda files reachable from paths in the .agda-lib file with new flag --build-library.
Experimental support for polarity annotations with new flag --polarity.
Compile to JavaScript with ES6 module syntax with new flag --js-es6.
Errors now have an identifier and follow the GNU standard.

Installation

Dropped support for GHC 8.6, added support for GHC 9.12.
Agda supports GHC versions 8.8.4 to 9.12.2.
The agda binary now contains everything to set itself up, it need not be shipped with additional files.
1. The functionality of the agda-mode executable has been replicated under the new option --emacs-mode. The agda-mode executable is now deprecated. References to agda-mode in your .emacs file should be replaced by agda --emacs-mode.
2. Agda now contains all its data files, like primitive and builtin modules, supplements for the HTML and LaTeX backends, the runtimes for the JS and GHC backends, and the emacs mode.
  
  These will be written to ${Agda_datadir}/${VERSION} on the first invocation of agda or an invocation of agda --setup, agda --emacs-mode setup, or agda --emacs-mode compile. Herein, ${VERSION} is the Agda version and ${Agda_datadir} the Agda data directory, on Unix-like systems defaulting to ${HOME}/.local/share/agda.
The Cabal/Stack custom installation Setup.hs has been removed that previously generated the .agdai files for the builtin and primitive modules. These will now be generated by Agda whenever they are needed, just as for ordinary modules.

This change is breaking for packagers of Agda as the packaging routines might need to be updated (but should become simpler).
Added cabal build flag dump-core to save the optimised GHC Core code during compilation of Agda. This can be useful for people working on improving the performance of the Agda implementation.

Pragmas and options

New main mode of operation --build-library (issue #4338). Invoking agda --build-library will look for an .agda-lib file starting in the current directory. It will then extract the include directories of this library, collect all Agda files in these directories and their subdirectories, and check all these files.
New option --setup that writes out the Agda data files (see above) and can be used to regenerate them.
New option --emacs-mode to administer the Emacs mode as previously done by the agda-mode executable.
Option --local-interfaces and warning DuplicateInterfaceFiles have been removed.
New option --js-es6 for generating JavaScript with ES6 module syntax.
DISPLAY pragmas can now define display forms that match on defined names beyond constructors (issue #7533). Example:
```
{-# DISPLAY Irrelevant Empty = ⊥ #-}
```
Empty used to be interpreted as a pattern variable, effectively installing the display form Irrelevant _ = ⊥. Now Empty is treated as a matchable name, as one would intuitively expect from a display form. As a consequence, only Irrelevant Empty is displayed as ⊥, not just any Irrelevant A.

Warnings

New deadcode warnings FixingCohesion, FixingPolarity and FixingRelevance when wrong user-written attribute was corrected automatically by Agda.
New deadcode warning InvalidDisplayForm instead of hard error when a display form is illegal (and thus ignored).
New warning UnusedVariablesInDisplayForm when DISPLAY pragma binds variables that are not used. Example:
```
{-# DISPLAY List (Fin n) = ListFin #-}
```
Since pattern variable n is not used on the right hand side ListFin, Agda throws a warning and recommeds to rewrite it as:
```
{-# DISPLAY List (Fin _) = ListFin #-}
```
Unused CATCHALL pragmas now trigger UselessPragma warnings.
New deadcode warning EmptyPolarityPragma for POLARITY pragma without polarities. E.g. triggered by {-# POLARITY F #-}.
New deadcode warning TooManyPolarities instead of hard error when a POLARITY pragma gives polarities that exceed the known arity of the postulate.
New deadcode warning UselessTactic when a @tactic attribute has no effect, typically when it is attached to a non-hidden or instance argument.
New warning WithClauseProjectionFixityMismatch instead of hard error when in a with-clause a projection is used in a different fixity (prefix vs. postfix) than in its parent clause.
New error warning TooManyArgumentsToSort instead of hard error.
Warning AbsurdPatternRequiresNoRHS has been renamed to AbsurdPatternRequiresAbsentRHS.
Warnings OpenPublicAbstract and OpenPublicPrivate have been replaced by new warnings OpenImportAbstract and OpenImportPrivate.
Warning NoGuardednessFlag has been removed. Instead Agda gives a hint when --guardedness would help with termination checking, unless options --sized-types or --no-guardedness are set.

Polarity

Support for polarity annotations can be enabled by the feature flag --polarity.

This flag is infective.

Uses of variables bound with polarity annotations are checked through modal typing rules, and the positivity checker has been expanded to take annotations into account. This means that the following is now definable:
```
{-# OPTIONS --polarity #-}

data Mu (F : @++ Set → Set) : Set where
  fix : F (Mu F) → Mu F
```

Syntax

Additions to the Agda syntax.

Add new literate agda: forester, see #7403
It is now always possible to refer to the name of a record type's constructor, even if a name was not explicitly specified. This is done using the new (Record name).constructor syntax; See issue #6964 for the motivation.
The left-hand-sides of functions bound in a let expression can now contain the same types of patterns that are allowed in lambda expressions, in dependent function types, and in other let bindings.

This means that
```
let
  f : A → B → C
  f p1 p2 = ...
in ...
```
should be accepted exactly when, and have the same meaning as,
```
let
  f : A → B → C
  f = λ p1 p2 → ...
```
See #7572.

Language

Changes to type checker and other components defining the Agda language.

BREAKING: The primitive "cubical identity type", previously exported from Agda.Builtin.Cubical.Id, has been removed. Its computational behaviour is exactly replicated by the user-definable identity type, which is also exported from Agda.Builtin.Equality.

See agda/cubical#1005 for the PR removing it from the library, and #7652 for the compiler.
Inlining constructors no longer happens on the right-hand-sides of INLINE functions. This allows using INLINE functions to define "smart constructors" for record types which have the same reduction behaviour as using the actual constructor would. Small example:
```
triple : Nat → Nat → Nat → Nat × Nat × Nat
{-# INLINE triple #-}
triple x y z = record { fst = x ; snd = y , z }

ex = triple 1 2 3
```
Here, constructor inlining happens on the right hand side of ex rather than of triple.

Reflection

Changes to the meta-programming facilities.

New reflection primitive: checkFromStringTC : String → Type → TC Term

Parse and type check the given string against the given type, returning the resulting term (when successful).

Library management

BREAKING: Agda no longer accepts several .agda-lib files in the root of an Agda project. (Previously, it allowed this and took the union of their contents.)

Interaction and emacs mode

Agda's error messages now follow the GNU standard. To comply with this policy, line and column are now separated by a dot instead of comma. The format of regular errors and error warnings follows this template:

sourcefile:line1.column1-line2.column2: error: [ErrorName] ... error message ... when error context

line2 or even column2 can be missing, in some cases even the entire error location. Internal errors might follow a different format.

Warnings are printed in a similar format:

sourcefile:line1.column1-line2.column2: warning: -W[no]WarningName ... warning text ... when warning context
Emacs: new face agda2-highlight-cosmetic-problem-face for highlighting the new aspect CosmeticProblem.
Emacs: new face agda2-highlight-instance-problem-face for highlighting the new aspect InstanceProblem.
When generating clauses after case splitting on a datatype defined in a parameterised module, Agda now prints constructor names without a module prefix rather than fully qualified (see issue #3209). This is only a surface-level fix, since Agda might still fail to find the properly qualified name for the constructor in scope, but should at least make more sense in most situations.
New bindings for unicode 'tacks' (⟘⟙⟛⟝⟞⫫⫪) via \tack (as well as specialised names for each of them)

Backends

New backendInteractTop/backendInteractHole fields for providing backend-specific interaction commands (run with keyboard shortcut C-c C-i).

Issues closed

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

Issues for closed for milestone 2.8.0

Issue #570: Explicit polarity annotation
Issue #2004: DISPLAY should be more pragmatic
Issue #4100: GHC backend produces code that is wrongly compiled by GHC 8.4.* and 8.6.*
Issue #4338: Add mechanism to type check entire Agda libraries
Issue #5793: [JS backend] add option for AMD-style and/or native JS modules support
Issue #6320: Parse strings to terms as reflection operation
Issue #6657: Turn --guardedness warning into an error-hint
Issue #6781: Making @tactic arguments visible leads to unsolved constraints
Issue #6916: Internal error at Agda/TypeChecking/Sort.hs:224:21
Issue #6964: Allow referring to unnamed record constructors
Issue #6994: Warnings are turned off, but code is still highlighted
Issue #7057: Document let-bindings in telescopes
Issue #7066: Documentation for anonymous modules
Issue #7157: Future: cabal build-type Setup will be phased out in favor of Hooks
Issue #7163: cabal install Agda fails with executable-dynamic
Issue #7321: No warning about useless {-# CATCHALL #-} pragma
Issue #7375: The specification of --safe misses the pragmas
Issue #7381: Our error messages do not follow the GNU standard
Issue #7392: Pattern matching unifier does not preserve instances
Issue #7434: Range printed twice for "Parse error"
Issue #7440: Unexpected hidden argument in nested records/modules
Issue #7495: Catchall clauses with less arguments are considered exact
Issue #7503: Cumulativity Prop <= Set loses canonicity
Issue #7508: Unused-arg optimization breaks function call
Issue #7517: quoteTerm accepts hidden arguments
Issue #7529: Strange problem with --level-universe and --cubical
Issue #7530: Generalized variable blocks projection-likeness
Issue #7531: JS backend crashes on big case split
Issue #7533: DISPLAY pragmas should treat any defined name as matchable
Issue #7535: Regression in 2.6.4: Agda thinks large propositions can be transported
Issue #7537: Type checking a definition with higher inductive type fails to terminate
Issue #7546: Why do we allow empty POLARITY pragmas?
Issue #7574: Support GHC 9.12
Issue #7576: impossible error: parameter overflow in declareData
Issue #7580: Our Setup.hs does not build with Cabal-3.14
Issue #7585: Happy-2.1.1 causes Agda build to fail
Issue #7587: Mimer takes an absurd lambda as the solution of the original goal rather than the current (sub)goal
Issue #7618: De Bruijn index out of scope in the presence of rewrite rules and records
Issue #7624: Internal error when interactively checking expression with new meta-variables
Issue #7639: Internal error in Agda/TypeChecking/Monad/Context.hs using Mimer
Issue #7641: No error highlighting when "fits in" test fails
Issue #7642: Better not claim "Level should be a function type"
Issue #7643: Panic: uncaught pattern violation
Issue #7650: Internal error when utilizing Emacs case splits and with .. in ..
Issue #7655: haskell/cabal#10235 can still occur with Agda-2.7.0.1
Issue #7659: Using auto leads to __IMPOSSIBLE__ when Σ and case_of_ are both present
Issue #7660: Add a warning for unresolved constructor name
Issue #7662: Using Auto with a goal involving musical coinduction ♭ produces incorrect projection
Issue #7668: Inductive identity allowed in negative position, inconsistent in Cubical Agda
Issue #7669: Positivity checker doesn't respect definitional equality
Issue #7673: nix build skips "generation of Agda core library interface files"
Issue #7675: toIFile logic from #6988 leads to scattering of .agdai files
Issue #7678: Order of agda-lib files in a directory affects flag settings
Issue #7692: Option to completely disable generation of dot patterns
Issue #7696: Panic: de Bruijn index out of scope
Issue #7707: ConstructorDoesNotFitInData error for record in Prop with Set fields
Issue #7709: Slow typecheck when importing a module with instances
Issue #7712: Embed data files using file-embed
Issue #7722: Exponential behavior in pattern operator parser
Issue #7730: emacs-mode files fail to build with "file has no lexical-binding directive"
Issue #7738: Rewriting by a constructor
Issue #7751: Application of module with datatype fools the termination checker
Issue #7753: Coverage checker internal error with copatterns and dot patterns
Issue #7759: Internal error for ellipsis without with-patterns
Issue #7761: Propω is not actually proof irrelevant
Issue #7765: Supply reason with UselessPublic warning
Issue #7766: .lagda.org: {-1} outside agda code block messes up hole detection
Issue #7769: The warning OpenPublicAbstract is wrongly formulated
Issue #7777: Parse error when using tactic and irrelevance
Issue #7788: TooManyPatternsInWithClause when nesting hidden with
Issue #7792: Inlining happens at most twice
Issue #7795: Polarity annotation ignored by positivity checker?
Issue #7796: Distinguish --no-guardedness from default value in termination hints?
Issue #7799: Potential regression related to instance resolution
Issue #7811: Internal error with Path and with-abstraction II
Issue #7815: Missing highlighting in module telescopes
Issue #7823: DISPLAY matches pattern with wrong amount of arguments
Issue #7825: DISPLAY form on irrelevant projection drops arguments
Issue #7829: Fields with signature not highlighted in record where
Issue #7832: Recursive function over inductive record treats arguments as irrelevant
Issue #7851: Error TooManyPolarities is too eager
Issue #7853: Subject reduction failure with instance constructors in parameterised modules
Issue #7856: Strange interaction between opaque and extended lambdas
Issue #7863: Internal error when calling MakeCase on target __

PRs for closed for milestone 2.8.0

PR #6629: Reflection primitive for parsing surface level syntax from string.
PR #7010: [new] backend-end specific interaction
PR #7287: Temporary fix for reflection of partial elements.
PR #7366: Handle symlinks correctly when computing interface file locations
PR #7374: New warning WithClauseProjectionFixityMismatch instead of GenericError
PR #7377: New warning RecursiveDisplayForm instead of hard error
PR #7379: Print error name with error message
PR #7385: New error group GHCBackendError instead of GenericError
PR #7387: Factor out give_ and remove PatternErr handler
PR #7388: GenericError crusade, continued
PR #7391: New error NeedOptionAllowExec etc. instead of GenericError
PR #7394: New error group InteractionError
PR #7395: Get rid of some MonadFail in favor of IMPOSSIBLE
PR #7396: instance warning
PR #7403: New literate programming backend forester, *.lagda.tree
PR #7409: GenericError crusade goes on: NeedOptionSizedTypes etc.
PR #7412: pattern in path lambda
PR #7414: Replace interaction Cmd_no_metas by Cmd_load_no_metas
PR #7415: Error refactoring: use of Exception, generic errors
PR #7418: New errors CannotGenerate{HComp,Transport}Clause
PR #7425: GenericError replacements
PR #7426: #7371: add Mimer tests for -s and -l
PR #7430: Warnings instead of GenericError for ill-formed pragmas
PR #7435: Print warning name on same line as location
PR #7437: Reform printing of parse error
PR #7447: Add new error InvalidModalTelescopeUse and add reproducer.
PR #7451: New warning FixingRelevance instead of GenericError
PR #7453: New error NotAllowedInDotPatterns instead of GenericError
PR #7458: Add ZuriHac Video to tutorial-list
PR #7459: NotAValidLet{Expression,Binding} instead of GenericError
PR #7462: Naming generic syntax errors (GenericError quest)
PR #7473: Re #6919: also separate compilation warnings by newlines
PR #7478: Store warnings in a set rather than a list
PR #7481: Named Backend errors instead of GenericError
PR #7483: Some named scope errors replacing GenericError
PR #7488: Named scope errors instead of GenericError
PR #7491: ES6 modules
PR #7492: Correctly print ParserWarning range, remove mdo
PR #7496: Fix #7495: Check extra split clause patterns are trivial for exactness
PR #7498: Add Left Multimap (⟜) to agda-input.el
PR #7500: Fix & test primShowNat
PR #7501: handle ProjPs in DISPLAY pragmas
PR #7502: Make termination checking more permissive wrt non-exact clause reduction
PR #7504: [ fix #7503 ] Use principal sort of datatype for checking if split is ok
PR #7509: Fix #7508: remove unused-arg optimization from the JS backend
PR #7510: Expose the names of generated record constructors (reopen #6975)
PR #7511: Fix #7381: comply to GNU error standard: use dot instead of comma in ranges
PR #7512: GenericError crusade
PR #7513: Reconcile PR #7510 with commit ac2888a7ad: add Maybe Induction to scopeRecords
PR #7516: New error CannotQuote instead of GenericError
PR #7518: OccursCheckErrors
PR #7520: Drop GHC 8.6
PR #7534: Fix #7529: treat LevelUniv in Cubical Agda
PR #7536: Re #7533: warn when DISPLAY form binds variables unused on the rhs
PR #7539: Fix #7413: Cubical: a GenericError is actually __IMPOSSIBLE__
PR #7543: DISPLAY: match on defined names
PR #7545: Fix #7531: Preserve let bindings in the JS backend
PR #7550: Fix #7546: warn about empty POLARITY pragmas
PR #7555: Some error housekeeping
PR #7556: unquote errors
PR #7557: kill GenericError in instance search
PR #7559: Fix compilation of serialisation code on 32 bit platforms
PR #7566: Make dangling hidden/instance args into a warning
PR #7570: Optimize concrete name scopeLookup
PR #7572: Improvements to let desugaring
PR #7577: chore: remove uses of genericError
PR #7581: don't add generalizedTel definitions to mutual blocks
PR #7583: Implement conversion to JS BigInt
PR #7586: Support Happy 2.1.1
PR #7589: Fix #7575: Check if variables are generalizable in builtin pragmas
PR #7591: Fix #7588: Remove overlapping branches when simplifying chained cases
PR #7593: Fix #7576
PR #7604: REPL: fix printing of result of :typeOf
PR #7613: Correct parameters to wrapper modules created in module telescopes
PR #7617: Fix de Bruijn indices in Treeless primitive translation
PR #7622: [ fix #7618 ] Use underAbstraction_ for going under lambda in reduceAndEtaContract
PR #7640: [ emacs ] adding su(b/p)(sim/approx) to input method
PR #7645: Fix #7642: new error CannotApply that mentions also term, not only type
PR #7648: Fix #7641: Range for ConstructorDoesNotFit warning (anon. rec. con.)
PR #7651: Fix #7650: Throw CaseSplitError when splitting on with-abstraction equality
PR #7652: remove the cubical identity type
PR #7653: Print point-ranges as such (line.col rather than line:col-col)
PR #7657: Setup: unconditionally check if we want interfaces
PR #7670: Fix typo COMPILED
PR #7672: Fix #7643: coverage: handle blocked sort in isFibrant
PR #7674: Fix #7669: positivity checker: compute function arity up to def. eq.
PR #7676: Remove --local-interfaces and warning DuplicateInterfaceFiles
PR #7677: Setup: fix wantInterfaces check
PR #7679: Disallow several .agda-lib files in the project root (#7678)
PR #7682: New main mode --build-library
PR #7685: Add dump-core cabal flag
PR #7686: Monomorphise unifyIndices
PR #7687: Make toTerm return a monadic function
PR #7688: Add some links to lecture notes and videos on Agda
PR #7697: Fix #7696: Add missing addContext when splitting on literals
PR #7699: Remove custom Setup.hs
PR #7700: Never generate dot patterns under --keep-pattern-variables
PR #7704: Speed up nix build
PR #7719: Embed data files into Agda binary
PR #7726: Compare overlapping instances in the right context
PR #7727: Fix #7722: in pattern parser only consider pattern-relevant operators
PR #7728: Improvements to instance search performance
PR #7729: Let Agda perform several of --help, --version etc. if the user requests so
PR #7732: Duplicate agda-mode as agda --emacs-mode
PR #7734: Doc: executable-dynamic no longer a problem on Linux
PR #7739: Fix #7738: Allow rewrite rule defined with constructor or primitive
PR #7742: Fix #7741: Fix printing inserted binder from operator section
PR #7743: Re-enable dot-pattern termination for Cubical Agda
PR #7745: Limit depth of constructed discrimination tree
PR #7746: Compute occurrences in trX “constructors”
PR #7750: Support GHC 9.12.2
PR #7752: Fix #7751: Consider datatype clauses generated from module application in recursion checker
PR #7758: Fix #7753: a possible __IMPOSSIBLE__
PR #7763: Fix #7761: Include large Prop in checks whether something is a Prop
PR #7764: Fixed #7730
PR #7767: Fix #7766: emacs org mode: fix code block end detection
PR #7768: Reason for UselessPublic; private useless in where blocks
PR #7771: Fix #7769: replace warning OpenPublic{Abstract,Private}
PR #7772: Fix #7707: wording of warning ConstructorDoesNotFitInData
PR #7773: Fix #7662: Mimer: special case for printing ♭
PR #7774: Fix #7321: warn about unused CATCHALL pragmas
PR #7775: Fix #6994: highlighting only for enabled warnings
PR #7776: Fix #7624 by reifying Term before wrapping it in GoalAndElaboration
PR #7778: Fix #6657: termination checker hints at missing --guardedness flag
PR #7782: re #3209: print out-of-scope names unqualified in case splits
PR #7783: Don't inline constructors into inline functions
PR #7785: Fix #7777: parse both attributes and irrelevance markers
PR #7786: New warning UselessTactic for tactic attribute on non-hidden binder
PR #7787: Small fixes for parsing and printing attributes
PR #7789: Fix issues #7759 and #7788: wrong counting of with-patterns in nested with
PR #7791: [ new ] unicode symbols for various 'tacks'
PR #7793: re #7792: keep inlining after inlining a copy
PR #7800: Fix #7796: don't hint towards --guardedness when --no-guardedness
PR #7802: Remove broken AbsurdLam heuristics from Mimer
PR #7812: Fix #7803 fix #7811: new error PathAbstractionFailed instead of crash
PR #7814: Fix #7660: new DisambiguateConstructor postponed tc problem
PR #7816: re #7815: propagate range into wrapper modules
PR #7817: Add documentation for telescopes and some related things
PR #7819: [ fix #7392 ] Ensure wildcards and variable instances are kept
PR #7822: Fix issue #7537
PR #7826: Fix #7825 by using droppedPars instead of hand-knitted code
PR #7830: Disregard qualified names when assigning clauses to functions in the nicifier
PR #7831: Fix #7829 by reactivating my own fix of #1618
PR #7834: fix #7795: Use occurrences from type for defs
PR #7840: Document which pragmas are unsafe
PR #7849: Fix for #7639
PR #7850: Re #7225: new error DatatypeIndexPolarity instead of GenericError
PR #7852: Turn TooManyPolarities error into warning (fixes #7851)
PR #7854: Modality warnings for constructors and fields
PR #7855: Re #7225 name error CubicalNotErasure
PR #7857: Forget opacity when checking signatures
PR #7858: Fix for #7659
PR #7859: Fix #7853: don't drop parameters of constructor in the same module
PR #7860: [ re #7587 ] Properly reintroduce absurd lambdas to Mimer
PR #7865: Fix #7863: properly parse names before case-splitting
PR #7867: Fix #7832 by placing properlyMatching in monad to have isEtaRecordConstructor