Release notes for Agda version 2.7.0

Highlights

• Mimer, a re-implementation of the "auto" term synthesizer, replaces Agsy.

• New syntax using x ← e to bind values on the left-hand-side of a function clause.

• Instance search is more performant thanks to a new indexing structure. Additionally, users can now control how instances should be selected in the case multiple candidates exist.

• User-facing options --exact-split, --keep-pattern-variables, and --postfix-projections are now on by default.

Installation

• Agda versioning scheme switches to the Haskell Package Versioning Policy so Agda can be more reliably used as a library. Major releases will now bump the second number in the version tuple: 2.7.0, 2.8.0, 2.9.0, ...

• Agda supports GHC versions 8.6.5 to 9.10.1.

Pragmas and options

• [Breaking] The option --overlapping-instances, which allows backtracking during instance search, has been renamed to --backtracking-instance-search.

• These options are now on by default:

  • --exact-split: Warn about clauses that are not definitional equalities.
  • --keep-pattern-variables: Do not introduce dot patterns in interactive splitting.
  • --postfix-projections: Print projections and projection patterns in postfix.
  • --save-metas: Try to not unfold metavariable solutions in interface files.

  To revert to the old behavior, use options --no-....

• The following options are now considered infective: (Issue #5264)

  • --allow-exec
  • --cumulativity
  • --experimental-irrelevance
  • --injective-type-constructors
  • --omega-in-omega
  • --rewriting
  • --type-in-type

  This means that if a module has one of these flags enabled, then all modules importing it must also have that flag enabled.

• New warnings:

  • CoinductiveEtaRecord if a record is declared both coinductive and having eta-equality. Used to be a hard error; now Agda continues, ignoring eta-equality.

  • ConflictingPragmaOptions if giving both --this and --that when --this implies --no-that (and analogous for --no-this implies --that, etc).

  • ConstructorDoesNotFitInData when a constructor parameter is too big (in the sense of universe level) for the target data type of the constructor. Error warning, used to be a hard error.

  • DuplicateRecordDirectives if e.g. a record is declared both inductive and coinductive, or declared inductive twice.

  • UselessMacro when a macro block does not contain any function definitions.

  • WarningProblem when trying to switch an unknown or non-benign warning with the -W option. Used to be a hard error.

• Rejected rewrite rules no longer cause a hard error but instead cause an error warning. The following warnings were added to document the various reasons for rejection:

  • RewriteLHSNotDefinitionOrConstructor
  • RewriteVariablesNotBoundByLHS
  • RewriteVariablesBoundMoreThanOnce
  • RewriteLHSReduces
  • RewriteHeadSymbolIsProjection
  • RewriteHeadSymbolIsProjectionLikeFunction
  • RewriteHeadSymbolIsTypeConstructor
  • RewriteHeadSymbolContainsMetas
  • RewriteConstructorParametersNotGeneral
  • RewriteContainsUnsolvedMetaVariables
  • RewriteBlockedOnProblems
  • RewriteRequiresDefinitions
  • RewriteDoesNotTargetRewriteRelation
  • RewriteBeforeFunctionDefinition
  • RewriteBeforeMutualFunctionDefinition

Lossy unification

• New option --require-unique-meta-solutions (turned on by default). Disabling it with --no-require-unique-meta-solutions allows the type checker to take advantage of INJECTIVE_FOR_INFERENCE pragmas (see below). The --lossy-unification flag implies --no-require-unique-meta-solutions.

• New pragma INJECTIVE_FOR_INFERENCE which treats functions as injective for inferring implicit arguments if --no-require-unique-meta-solutions is given. The --no-require-unique-meta-solutions flag needs to be given in the file where the function is used, and not necessarily in the file where it is defined. For example:

  postulate
    reverse-≡ : {l l' : List A} → reverse l ≡ reverse l' → reverse l ≡ reverse l'
  
  []≡[] : [] ≡ []
  []≡[] = reverse-≡ (refl {x = reverse []})
  

  does not work since Agda won't solve l and l' for [], even though it knows reverse l = reverse []. If reverse is marked as injective with {-# INJECTIVE_FOR_INFERENCE reverse #-} this example will work.

Syntax

Additions to the Agda syntax.

• Left-hand side let: using x ← e (PR #7078)

  This new construct can be use in left-hand sides together with with and rewrite to give names to subexpressions. It is the left-hand side counterpart of a let-binding and supports the same limited form of pattern matching on eta-expandable record values.

  It can be quite useful when you have a function doing a series of nested withs that share some expressions. Something like

  fun : A → B
  fun x using z ← e with foo z
  ... | p with bar z
  ...   | q = r
  

  Here the expression e doesn't have to be repeated in the two with-expressions.

  As in a with, multiple bindings can be separated by a |, and variables to the left are in scope in bindings to the right.

• Pattern synonyms can now expose existing instance arguments (PR 7173). Example:

  data D : Set where
    c : {{D}} → D
  
  pattern p {{d}} = c {{d}}
  

  This allows us to explicitly bind these argument in a pattern match and supply them explicitly when using the pattern synonym in an expression.

  f : D → D
  f (p {{d = x}}) = p {{d = x}}
  

  We cannot create new instance arguments this way, though. The following is rejected:

  data D : Set where
    c : D → D
  
  pattern p {{d}} = c d
  

Language

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

• Agda now uses discrimination trees to store and look up instance definitions, rather than linearly searching through all instances for a given "class" (PR #7109).

  This is a purely internal change, and should not result in any change to which programs are accepted or rejected. However, it significantly improves the performance of instance search, especially for the case of a "type class" indexed by a single type argument. The new lookup procedure should never be slower than the previous implementation.

Reflection

Changes to the meta-programming facilities.

• [Breaking] Erased constructors are now supported in reflection machinery. Quantity argument was added to data-cons. For erased constructors this argument has a value of quantity-0, otherwise it's quantity-ω. defineData now requires setting quantity for each constructor.

• Add new primitive to run instance search from reflection code:

    -- Try to solve open instance constraints. When wrapped in `noConstraints`,
    -- fails if there are unsolved instance constraints left over that originate
    -- from the current macro invokation. Outside constraints are still attempted,
    -- but failure to solve them are ignored by `noConstraints`.
    solveInstanceConstraints : TC ⊤
  

• A new reflection primitive workOnTypes : TC A → TC A was added to Agda.Builtin.Reflection. This runs the given computation at the type level, which enables the use of erased things. In particular, this is needed when working with (dependent) function types with erased arguments. For example, one can get the type of the tuple constructor _,_ (which now takes its type parameters as erased arguments, see above) and unify it with the current goal as follows:

  macro
    testM : Term → TC ⊤
    testM hole = bindTC (getType (quote _,_)) (λ t → workOnTypes (unify hole t))
  
  typeOfComma = testM
  

Interaction and emacs mode

• [Breaking] The Auto command Agsy has been replaced by an entirely new implementation Mimer (PR #6410). This fixes problems where Auto would fail in the presence of language features it did not know about, such as copatterns or anything cubical.

  The reimplementation does not support case splitting (-c), disproving (-d) or refining (-r).

• The Agda input method for Emacs has been extended by several character bindings. The list of changes can be obtained with a git diff on the sources:

  git diff v2.6.4.3 v2.7.0 -- src/data/emacs-mode/agda-input.el
  

API

Highlighting some changes to Agda as a library.

• New module Agda.Syntax.Common.KeywordRange providing type KwRange isomorphic to Range to indicate source positions that just span keywords (PR #7162). The motivation for KwRange is to distinguish such ranges from ranges for whole subtrees, e.g. in data type Agda.Syntax.Concrete.Declaration.

  API:

  module Agda.Syntax.Common.KeywordRange where
  
  type KwRange
  
  -- From Range to KwRange
  kwRange :: HasRange a => a -> KwRange
  
  -- From KwRange to Range
  instance HasRange KwRange where
    getRange :: KwRange -> Range
  

• New hook in Agda.Compiler.ToTreeless to enable custom pipelines in compiler backends (PR #7273).

List of closed issues

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

• Issue #2492: Limit the size of terms agsy is allowed to insert
• Issue #2853: Auto does not work well with record types
• Issue #4594: Improve the blocking primitive
• Issue #4777: Interaction between tactics and instance search
• Issue #5264: Should more flags be infective (or have coinfective negations)?
• Issue #6101: Agsy gives up when no HIT is present
• Issue #6124: Reflection: cannot reduce type because variable is erased
• Issue #6181: Agda incorrectly reports type error when an identity function is not properly hidden from the termination checker
• Issue #6270: Irrelevance in the type of a record module definition
• Issue #6292: Document interaction between reflection and erasure
• Issue #6335: Error message for non-canonical value when using Show instances is confusing
• Issue #6361: Agsy ignores --postfix-projections
• Issue #6406: Subject reduction problem related to projections with non-erased parameter arguments
• Issue #6433: Add unicode character BALLOT X as \crossmark to Agda input mode
• Issue #6509: Agda seems to be very slow at typechecking records with many fields
• Issue #6584: Case splitting on record renames top-level function
• Issue #6643: Rewrite rules are allowed in implicit mutual blocks
• Issue #6663: Function arguments are nonvariant more often than they should be
• Issue #6667: An internal error occurrs when (mis)using syntax declarations
• Issue #6744: Alias in constructor index foils the forcing analysis
• Issue #6768: auto: not implemented HITs error on non-cubical code
• Issue #6783: @tactic does not kick in for lambdas
• Issue #6806: Remove GenericWarning
• Issue #6841: Uncaught pattern violation when using with...in... instead of old-school inspect
• Issue #6866: User Manual: Make Installation as Easy as Possible
• Issue #6867: Agda rejects identity function on indexed datatype with erased index
• Issue #6919: improving formatting of warnings/errors
• Issue #6943: Making --exact-split and --postfix-projections default?
• Issue #6945: Missing warning for non-empty but effectless private blocks
• Issue #6976: Unexpected failure of instance resolution
• Issue #7017: Document instance projections
• Issue #7058: Unclear specification and correctness of TypeChecking/DeadCode
• Issue #7090: REWRITE rule with confluence, inconsistencies with documentation and error messages
• Issue #7123: Citation.cff
• Issue #7136: Pattern synonyms with named arguments can be defined but not used
• Issue #7146: Misprinted domain-free parameters with cohesion attribute
• Issue #7158: Non-sensical error since 2.5.4 when applying a non-function
• Issue #7167: Underapplied pattern synonyms expand to lambdas with wrong hiding in expressions
• Issue #7170: Confusing error "Unused variable in pattern synonym"
• Issue #7176: Instanceness is lost when expanding absurd pattern in pattern synonym expression
• Issue #7177: No scope info for underscores inserted by pattern synonym expansion
• Issue #7181: Forcing translation prevents reduction within function definition
• Issue #7182: getDefinition gives wrong constructor for record from applied parameterised module
• Issue #7187: Sort metas produce ill-typed reflected terms when quoted
• Issue #7191: show does not respect abstract/opaque when normalising a term in a hole
• Issue #7192: GHC 9.10
• Issue #7193: Agda always has irrelevant projections
• Issue #7196: Regression when giving instances with visible arguments
• Issue #7202: ModuleDoesntExport has imprecise deadcode highlighting
• Issue #7208: Importing module with wrong namespace causes internal error instead of user-friendly error.
• Issue #7218: Internal error in opaque block when case splitting when just given extended lambda
• Issue #7219: Only warn about unknown warnings, don't fail hard
• Issue #7227: Save-metas causes OOM during macro execution
• Issue #7236: Expected a hidden argument, but found a visible argument in with-abstraction when using REWRITE
• Issue #7262: Error "This clause has target type ... which is not usable" highlights pattern instead of clause
• Issue #7266: Internal error at Agda/TypeChecking/Substitute.hs:140:33
• Issue #7286: Hard error on instance definition with unsolved type
• Issue #7301: Agda >=2.6.3 hangs on conflicting record directives
• Issue #7318: --postfix-projections do not make use of mixfix syntax
• Issue #7326: Internal error on pattern lambda with no clauses
• Issue #7329: wrong type for unnamed record constructor
• Issue #7331: Search for project root crashes when (parent) directory lacks permissions
• Issue #7332: quoteTerm loops on dependent copattern lambda
• Issue #7337: Caching loses reflection-generated pragmas
• Issue #7346: Proof of ⊥ using HIT-indexed type

These (relevant) pull requests were merged for 2.7.0:

• PR #5267: Make more flags infective
• PR #6410: Mimer: a drop-in replacement for Agsy
• PR #6569: Do final checks before freezing metas
• PR #6570: Coerce unquote applications
• PR #6640: Add INJECTIVE_FOR_INFERENCE pragma
• PR #6674: Testcase for fixed #6542
• PR #6769: Various symbol additions to agda-input
• PR #6870: [ fix #6867 ] Only consider arguments with @0 for forcing if --erasure is on
• PR #6978: [ fix #6976 ] Add constraint for resolving the head of an instance
• PR #7055: Unspine system projections when they have display forms
• PR #7071: Eta-expand mismatched cubical primitives
• PR #7078: Left-hand side let
• PR #7103: [ re #5267 ] Add new infective options to user manual
• PR #7109: Discrimination trees for instance search
• PR #7115: Flake improvements
• PR #7119: Split GenericWarning into individual warnings
• PR #7121: Update installation.rst
• PR #7138: Fix #7136: proper error when pattern definition has unsupported arguments
• PR #7142: Fix #6783: error for @tactic on lambda
• PR #7144: Add reference to Cornelis in the documentation
• PR #7147: Fix #7146: printing of cohesion and lock attributes
• PR #7149: Fix mutual information not being set properly by the positivity checker
• PR #7155: Fix #6866: User Manual: Make Installation as Easy as Possible
• PR #7159: Fix #7158: Application: check for sufficient arity before checking target
• PR #7160: Fix #6667: case not __IMPOSSIBLE__ for nullary syntax
• PR #7161: Fix #6945: warn about useless private even in absense of nice decls
• PR #7162: Blocks in Concrete syntax: store Range of block keyword
• PR #7168: Fix #7167: type checking underapplied pattern synonyms
• PR #7169: Trigger and improve error UnusedVariableInPatternSynonym
• PR #7173: Part of #2829: Allow instance arguments in pattern synonyms that are such in the pattern already
• PR #7179: Fix #7177: only setScope when scope is not null
• PR #7180: Use compareAs for assignE even in compareAtom
• PR #7183: Instance overlap pragmas
• PR #7185: Fix #7176: turn absurd pattern in instance position to instance meta
• PR #7197: Re. #7196: Only prune instances in serialised iface
• PR #7203: Fix incorrectly quoted sorts
• PR #7204: Fix #7202: ModuleDoesntExport: only highlight missing names
• PR #7209: Fix #7208: restore missing check for OverlappingProjects
• PR #7210: Fix range for deprecated module import warning when applied
• PR #7211: Fix #7181: Allow matching to continue when stuck on lazy pattern
• PR #7222: Fix #7219: only warn about problems with warning options
• PR #7231: Instantiate terms before traversing them in tcExtendContext
• PR #7237: Fix #7236: use context rather than telescope for lambda-bound variables in rewrite patterns
• PR #7238: Build with GHC 9.10
• PR #7241: Drop time-compat dependency and Stack LTS for GHC 8.6
• PR #7243: re. 7218: Saturate opaque blocks after Give commands
• PR #7248: Overhaul dead code elimination, make --save-metas the default
• PR #7249: docs/installation: point new wiki
• PR #7251: re. 7250: copy instanceinfo
• PR #7252: Fix #7193: persistently remember what is a projection
• PR #7260: Reflection primitive to solve instances
• PR #7273: ToTreeless: allow backends to define custom pipelines
• PR #7274: #7182: copied records should refer to the copied constructor and fields
• PR #7276: #7191: respect abstract mode when using show function
• PR #7283: agdaLatex documentation
• PR #7292: New error warning ConstructorDoesNotFitInData instead of hard error.
• PR #7298: Remove fiddly attempt at instance postponement
• PR #7300: New deadcode warning CoinductiveEtaRecord instead of GenericError
• PR #7302: Fix #7301 (loop in parser): move verifyRecordDirectives to scope checker
• PR #7305: Fix #7286: don't fail hard when there are instances with unresolved types
• PR #7307: fix #7017: document instance projections
• PR #7310: Add workOnTypes reflection primitive
• PR #7311: [ #6406 ] Add test cases from discussion on this issue
• PR #7313: Update universe-levels.lagda.rst
• PR #7314: Add constructors for custom backend warning/errors
• PR #7315: same shadowing logic for record patterns as for constructor patterns in absToCon
• PR #7316: add \crossmark to emacs input mode
• PR #7317: Don't mark eta unit records as irrelevant
• PR #7319: Make --postfix-projections the default
• PR #7320: Turn on --exact-split by default
• PR #7322: Expose constructor erasure in reflection interface
• PR #7325: add CSS rule for macro names
• PR #7327: proper error instead of impossible for clauseless pat-lam
• PR #7330: [#7329] Correct module name in module applications
• PR #7333: [#7332] don't loop when quoting dependent copattern lambdas
• PR #7334: Fix #7331: handle permission error in search for project file
• PR #7336: Remove duplicate imports and pragmas in MAlonzo
• PR #7338: (#7337) foreign code needs to go in post-scope state
• PR #7343: Turn illegal rewrite rules into an error warning
• PR #7347: [ fix #7266 ] Check that constructor names match before projecting in matchPattern
• PR #7349: Fix #7346 by not considering HIT-constructor arguments forced
• PR #7350: Fix #6744 by reducing during forcing analysis.
• PR #7352: Fix issue 7262: Range of the lhs modality check
• PR #7353: Update installation docs (e.g. re #7163: document installation problems with executable-dynamic)
• PR #7355: Make --keep-pattern-variables the default
• PR #7356: Add --save-metas default to CHANGELOG
• PR #7358: [ doc ] Document --termination-depth in user manual
• PR #7359: Fix #7354 by making types of live metas live in DeadCode
• PR #7360: Fix for issue #6841 and related changes
• PR #7362: Fix #6919: separate warnings by empty line
• PR #7364: Resolve instance overlap for irrelevant metas
• PR #7367: Minor fixes to instance overlap + constraint postponement