Agda 2.7.0 → 2.7.0.1

raw patch · 15 files changed

+297/−576 lines, 15 filesdep ~basesetup-changedPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• Agda.cabal +2/−6
• CHANGELOG.md +47/−417
• Setup.hs +85/−27
• src/data/emacs-mode/agda2-mode-pkg.el +1/−1
• src/data/emacs-mode/agda2-mode.el +1/−1
• src/data/latex/agda.sty +1/−1
• src/full/Agda/Interaction/Imports.hs +39/−41
• src/full/Agda/Interaction/Options/Base.hs +1/−1
• src/full/Agda/Mimer/Mimer.hs +55/−51
• src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs +5/−2
• src/full/Agda/TypeChecking/DeadCode.hs +18/−10
• src/full/Agda/TypeChecking/DisplayForm.hs +21/−6
• src/full/Agda/TypeChecking/Empty.hs +1/−1
• src/full/Agda/TypeChecking/Monad/Base.hs +12/−0
• src/full/Agda/TypeChecking/Records.hs +8/−11

@@ -1,6 +1,6 @@ cabal-version:   2.4 name:            Agda-version:         2.7.0+version:         2.7.0.1 build-type:      Custom license:         MIT license-file:    LICENSE@@ -29,10 +29,6 @@     This package includes both a command-line program (agda) and an     Emacs mode. If you want to use the Emacs mode you can set it up by     running @agda-mode setup@ (see the README).-    .-    Note that the Agda package does not follow the package versioning-    policy, because it is not intended to be used by third-party-    packages.  tested-with:     GHC == 9.10.1@@ -160,7 +156,7 @@ source-repository this   type:     git   location: https://github.com/agda/agda.git-  tag:      v2.7.0+  tag:      v2.7.0.1  -- Build flags ---------------------------------------------------------------------------

@@ -1,442 +1,72 @@-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.+Release notes for Agda version 2.7.0.1+====================================== -* User-facing options `--exact-split`, `--keep-pattern-variables`, and `--postfix-projections`-  are now on by default.+This is a minor release of Agda fixing some bugs and regressions.  Installation ------------ -* Agda versioning scheme switches to the [Haskell Package Versioning Policy](https://pvp.haskell.org/)-  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, ...--* When the creation of the Agda library interface files fails during installation,-  a warning is emitted rather than aborting installation.-  The absence of these interface files is not a problem if the Agda installation-  resides in user space; they will be created on the fly then.-  Yet for system-wide installations in root space or packaging,-  the interface files should be created.-  This can be achieved by a manual invocation of Agda on the library source files-  (i.e., primitive and builtin modules `Agda.*`).-  (See [Issue #7401](https://github.com/agda/agda/issues/7401) and [PR #7404](https://github.com/agda/agda/pull/7404).)+* During installation, Agda type-checks its built-in modules and installs the generated `.agdai` files.+  (This step is now skipped when the Agda executable is not installed, e.g. `cabal install --lib Agda`.)+  Should the generation for (some of) these files fail, the names of the missing ones are now printed,+  but installation continues nevertheless ([PR #7465](https://github.com/agda/agda/pull/7465)).+  Rationale: installation of these files is only crucial when installing Agda in super-user mode.  * 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-...`.--* Option `--rewriting` is now considered infective.-  This means that if a module has this flag 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`](https://agda.readthedocs.io/en/v2.7.0/tools/command-line-options.html#cmdoption-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`](https://agda.readthedocs.io/en/v2.7.0/pragmas.html#injective-for-inference-pragma)-  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:-  ```agda-  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](https://agda.readthedocs.io/en/v2.7.0/with-abstraction.html#left-hand-side-let-bindings):-  `using x ← e`-  ([PR #7078](https://github.com/agda/agda/pull/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-  `with`s that share some expressions. Something like--  ```agda-  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](https://github.com/agda/agda/pull/7173)).-  Example:-  ```agda-  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.-  ```agda-  f : D → D-  f (p {{d = x}}) = p {{d = x}}-  ```--  We cannot create new instance arguments this way, though.-  The following is rejected:-  ```agda-  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](https://github.com/agda/agda/pull/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:--  ```agda-    -- 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:-  ```agda-  macro-    testM : Term → TC ⊤-    testM hole = bindTC (getType (quote _,_)) (λ t → workOnTypes (unify hole t))--  typeOfComma = testM-  ```--Interaction and emacs mode-----------------------------* [**Breaking**] [The Auto command](https://agda.readthedocs.io/en/v2.7.0/tools/auto.html)-  _Agsy_ has been replaced by an entirely new implementation _Mimer_-  ([PR #6410](https://github.com/agda/agda/pull/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](https://github.com/agda/agda/pull/7162)).-  The motivation for `KwRange` is to distinguish such ranges from ranges for whole subtrees,-  e.g. in data type `Agda.Syntax.Concrete.Declaration`.+* The release notes of 2.7.0 claimed that the option `--exact-split` was now on by default+  ([Issue #7443](https://github.com/agda/agda/issues/7443)).+  This is actually not the case, the documentation has been suitably reverted. -  API:-  ```haskell-  module Agda.Syntax.Common.KeywordRange where+* Default option `--save-metas` has been reverted to `--no-save-metas` because of performance regressions+  ([Issue #7452](https://github.com/agda/agda/issues/7452)). -  type KwRange+Bug fixes+--------- -  -- From Range to KwRange-  kwRange :: HasRange a => a -> KwRange+* Fixed an internal error related to interface files+  ([Issue #7436](https://github.com/agda/agda/issues/7436)). -  -- From KwRange to Range-  instance HasRange KwRange where-    getRange :: KwRange -> Range-  ```+* Fixed two internal errors in Mimer:+  ([Issue #7402](https://github.com/agda/agda/issues/7402) and+  [Issue #7484](https://github.com/agda/agda/issues/7484)). -* New hook in ``Agda.Compiler.ToTreeless`` to enable custom pipelines in compiler backends-  ([PR #7273](https://github.com/agda/agda/pull/7273)).+* Fixed a regression causing needless re-checking of files+  ([Issue #7199](https://github.com/agda/agda/issues/7199)). +* Improved printing of terms by fixing a display form bug+  ([PR #7480](https://github.com/agda/agda/issues/7480)).  List of closed issues --------------------- -For 2.7.0, the following issues were-[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.7.0+is%3Aclosed)+For 2.7.0.1, the following issues were+[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.7.0.1+is%3Aclosed) (see [bug tracker](https://github.com/agda/agda/issues)): -- [Issue #2492](https://github.com/agda/agda/issues/2492): Limit the size of terms agsy is allowed to insert-- [Issue #2853](https://github.com/agda/agda/issues/2853): Auto does not work well with record types-- [Issue #4594](https://github.com/agda/agda/issues/4594): Improve the blocking primitive-- [Issue #4777](https://github.com/agda/agda/issues/4777): Interaction between tactics and instance search-- [Issue #6101](https://github.com/agda/agda/issues/6101): Agsy gives up when no HIT is present-- [Issue #6124](https://github.com/agda/agda/issues/6124): Reflection: cannot reduce type because variable is erased-- [Issue #6181](https://github.com/agda/agda/issues/6181): Agda incorrectly reports type error when an identity function is not properly hidden from the termination checker-- [Issue #6270](https://github.com/agda/agda/issues/6270): Irrelevance in the type of a record module definition-- [Issue #6292](https://github.com/agda/agda/issues/6292): Document interaction between reflection and erasure-- [Issue #6335](https://github.com/agda/agda/issues/6335): Error message for non-canonical value when using Show instances is confusing-- [Issue #6361](https://github.com/agda/agda/issues/6361): Agsy ignores --postfix-projections-- [Issue #6406](https://github.com/agda/agda/issues/6406): Subject reduction problem related to projections with non-erased parameter arguments-- [Issue #6433](https://github.com/agda/agda/issues/6433): Add unicode character BALLOT X as \crossmark to Agda input mode-- [Issue #6509](https://github.com/agda/agda/issues/6509): Agda seems to be very slow at typechecking records with many fields-- [Issue #6584](https://github.com/agda/agda/issues/6584): Case splitting on record renames top-level function-- [Issue #6643](https://github.com/agda/agda/issues/6643): Rewrite rules are allowed in implicit mutual blocks-- [Issue #6663](https://github.com/agda/agda/issues/6663): Function arguments are nonvariant more often than they should be-- [Issue #6667](https://github.com/agda/agda/issues/6667): An internal error occurrs when (mis)using syntax declarations-- [Issue #6744](https://github.com/agda/agda/issues/6744): Alias in constructor index foils the forcing analysis-- [Issue #6768](https://github.com/agda/agda/issues/6768): auto: not implemented HITs error on non-cubical code-- [Issue #6783](https://github.com/agda/agda/issues/6783): `@tactic` does not kick in for lambdas-- [Issue #6806](https://github.com/agda/agda/issues/6806): Remove `GenericWarning`-- [Issue #6841](https://github.com/agda/agda/issues/6841): Uncaught pattern violation when using `with...in...` instead of old-school inspect-- [Issue #6866](https://github.com/agda/agda/issues/6866): User Manual: Make Installation as Easy as Possible-- [Issue #6867](https://github.com/agda/agda/issues/6867): Agda rejects identity function on indexed datatype with erased index-- [Issue #6919](https://github.com/agda/agda/issues/6919): improving formatting of warnings/errors-- [Issue #6943](https://github.com/agda/agda/issues/6943): Making `--exact-split` and `--postfix-projections` default?-- [Issue #6945](https://github.com/agda/agda/issues/6945): Missing warning for non-empty but effectless `private` blocks-- [Issue #6976](https://github.com/agda/agda/issues/6976): Unexpected failure of instance resolution-- [Issue #7017](https://github.com/agda/agda/issues/7017): Document instance projections-- [Issue #7058](https://github.com/agda/agda/issues/7058): Unclear specification and correctness of TypeChecking/DeadCode-- [Issue #7090](https://github.com/agda/agda/issues/7090): REWRITE rule with confluence, inconsistencies with documentation and error messages-- [Issue #7123](https://github.com/agda/agda/issues/7123): Citation.cff-- [Issue #7136](https://github.com/agda/agda/issues/7136): Pattern synonyms with named arguments can be defined but not used-- [Issue #7146](https://github.com/agda/agda/issues/7146): Misprinted domain-free parameters with cohesion attribute-- [Issue #7158](https://github.com/agda/agda/issues/7158): Non-sensical error since 2.5.4 when applying a non-function-- [Issue #7167](https://github.com/agda/agda/issues/7167): Underapplied pattern synonyms expand to lambdas with wrong hiding in expressions-- [Issue #7170](https://github.com/agda/agda/issues/7170): Confusing error "Unused variable in pattern synonym"-- [Issue #7176](https://github.com/agda/agda/issues/7176): Instanceness is lost when expanding absurd pattern in pattern synonym expression-- [Issue #7177](https://github.com/agda/agda/issues/7177): No scope info for underscores inserted by pattern synonym expansion-- [Issue #7181](https://github.com/agda/agda/issues/7181): Forcing translation prevents reduction within function definition-- [Issue #7182](https://github.com/agda/agda/issues/7182): `getDefinition` gives wrong constructor for record from applied parameterised module-- [Issue #7187](https://github.com/agda/agda/issues/7187): Sort metas produce ill-typed reflected terms when quoted-- [Issue #7191](https://github.com/agda/agda/issues/7191): `show` does not respect `abstract`/`opaque` when normalising a term in a hole-- [Issue #7192](https://github.com/agda/agda/issues/7192): GHC 9.10-- [Issue #7193](https://github.com/agda/agda/issues/7193): Agda always has irrelevant projections-- [Issue #7196](https://github.com/agda/agda/issues/7196): Regression when giving instances with visible arguments-- [Issue #7202](https://github.com/agda/agda/issues/7202): `ModuleDoesntExport` has imprecise deadcode highlighting-- [Issue #7208](https://github.com/agda/agda/issues/7208): Importing module with wrong namespace causes internal error instead of user-friendly error.-- [Issue #7218](https://github.com/agda/agda/issues/7218): Internal error in opaque block when case splitting when just given extended lambda-- [Issue #7219](https://github.com/agda/agda/issues/7219): Only warn about unknown warnings, don't fail hard-- [Issue #7227](https://github.com/agda/agda/issues/7227): Save-metas causes OOM during macro execution-- [Issue #7236](https://github.com/agda/agda/issues/7236): Expected a hidden argument, but found a visible argument in with-abstraction when using REWRITE-- [Issue #7262](https://github.com/agda/agda/issues/7262): Error "This clause has target type ... which is not usable" highlights pattern instead of clause-- [Issue #7266](https://github.com/agda/agda/issues/7266): Internal error at Agda/TypeChecking/Substitute.hs:140:33-- [Issue #7286](https://github.com/agda/agda/issues/7286): Hard error on `instance` definition with unsolved type-- [Issue #7301](https://github.com/agda/agda/issues/7301): Agda >=2.6.3 hangs on conflicting record directives-- [Issue #7318](https://github.com/agda/agda/issues/7318): `--postfix-projections` do not make use of mixfix syntax-- [Issue #7326](https://github.com/agda/agda/issues/7326): Internal error on pattern lambda with no clauses-- [Issue #7329](https://github.com/agda/agda/issues/7329): wrong type for unnamed record constructor-- [Issue #7331](https://github.com/agda/agda/issues/7331): Search for project root crashes when (parent) directory lacks permissions-- [Issue #7332](https://github.com/agda/agda/issues/7332): quoteTerm loops on dependent copattern lambda-- [Issue #7337](https://github.com/agda/agda/issues/7337): Caching loses reflection-generated pragmas-- [Issue #7346](https://github.com/agda/agda/issues/7346): Proof of ⊥ using HIT-indexed type-- [Issue #7380](https://github.com/agda/agda/issues/7380): MAlonzo bug: `unreachable code reached`-- [Issue #7382](https://github.com/agda/agda/issues/7382): Agda 2.7.0-rc1 crashes when run twice, probably serialization issue-- [Issue #7401](https://github.com/agda/agda/issues/7401): Cabal 3.12.1.0 install failure for lib:Agda - dist/build/agda/agda does not exist+- [Issue #7199](https://github.com/agda/agda/issues/7199): Agda re-checks a file with an up-to-date interface file+- [Issue #7402](https://github.com/agda/agda/issues/7402): Mimer internal error in hole with constraint+- [Issue #7436](https://github.com/agda/agda/issues/7436): Code only reachable from display forms not serialised in Agda 2.7.0+- [Issue #7442](https://github.com/agda/agda/issues/7442): Regression: emptiness check fails when erased constructors are involved+- [Issue #7443](https://github.com/agda/agda/issues/7443): `--exact-split` is not default in 2.7.0, contrary to claims+- [Issue #7452](https://github.com/agda/agda/issues/7452): Performance regression caused by making `--save-metas` the default+- [Issue #7455](https://github.com/agda/agda/issues/7455): Both stack and cabal fail to install Agda+- [Issue #7484](https://github.com/agda/agda/issues/7484): Internal error using Mimer in where block -These (relevant) pull requests were merged for 2.7.0:+These pull requests were merged for 2.7.0.1: -- [PR #6410](https://github.com/agda/agda/issues/6410): Mimer: a drop-in replacement for Agsy-- [PR #6569](https://github.com/agda/agda/issues/6569): Do final checks before freezing metas-- [PR #6570](https://github.com/agda/agda/issues/6570): Coerce `unquote` applications-- [PR #6640](https://github.com/agda/agda/issues/6640): Add `INJECTIVE_FOR_INFERENCE` pragma-- [PR #6674](https://github.com/agda/agda/issues/6674): Testcase for fixed #6542-- [PR #6769](https://github.com/agda/agda/issues/6769): Various symbol additions to agda-input-- [PR #6870](https://github.com/agda/agda/issues/6870): [ fix #6867 ] Only consider arguments with @0 for forcing if --erasure is on-- [PR #6978](https://github.com/agda/agda/issues/6978): [ fix #6976 ] Add constraint for resolving the head of an instance-- [PR #7055](https://github.com/agda/agda/issues/7055): Unspine system projections when they have display forms-- [PR #7071](https://github.com/agda/agda/issues/7071): Eta-expand mismatched cubical primitives-- [PR #7078](https://github.com/agda/agda/issues/7078): Left-hand side `let`-- [PR #7109](https://github.com/agda/agda/issues/7109): Discrimination trees for instance search-- [PR #7115](https://github.com/agda/agda/issues/7115): Flake improvements-- [PR #7119](https://github.com/agda/agda/issues/7119): Split GenericWarning into individual warnings-- [PR #7121](https://github.com/agda/agda/issues/7121): Update installation.rst-- [PR #7138](https://github.com/agda/agda/issues/7138): Fix #7136: proper error when pattern definition has unsupported arguments-- [PR #7142](https://github.com/agda/agda/issues/7142): Fix #6783: error for @tactic on lambda-- [PR #7144](https://github.com/agda/agda/issues/7144): Add reference to Cornelis in the documentation-- [PR #7147](https://github.com/agda/agda/issues/7147): Fix #7146: printing of cohesion and lock attributes-- [PR #7149](https://github.com/agda/agda/issues/7149): Fix mutual information not being set properly by the positivity checker-- [PR #7155](https://github.com/agda/agda/issues/7155): Fix #6866: User Manual: Make Installation as Easy as Possible-- [PR #7159](https://github.com/agda/agda/issues/7159): Fix #7158: Application: check for sufficient arity before checking target-- [PR #7160](https://github.com/agda/agda/issues/7160): Fix #6667: case not `__IMPOSSIBLE__` for nullary syntax-- [PR #7161](https://github.com/agda/agda/issues/7161): Fix #6945: warn about useless private even in absense of nice decls-- [PR #7162](https://github.com/agda/agda/issues/7162): Blocks in Concrete syntax: store Range of block keyword-- [PR #7168](https://github.com/agda/agda/issues/7168): Fix #7167: type checking underapplied pattern synonyms-- [PR #7169](https://github.com/agda/agda/issues/7169): Trigger and improve error UnusedVariableInPatternSynonym-- [PR #7173](https://github.com/agda/agda/issues/7173): Part of #2829: Allow instance arguments in pattern synonyms that are such in the pattern already-- [PR #7179](https://github.com/agda/agda/issues/7179): Fix #7177: only setScope when scope is not null-- [PR #7180](https://github.com/agda/agda/issues/7180): Use compareAs for assignE even in compareAtom-- [PR #7183](https://github.com/agda/agda/issues/7183): Instance overlap pragmas-- [PR #7185](https://github.com/agda/agda/issues/7185): Fix #7176: turn absurd pattern in instance position to instance meta-- [PR #7197](https://github.com/agda/agda/issues/7197): Re. #7196: Only prune instances in serialised iface-- [PR #7203](https://github.com/agda/agda/issues/7203): Fix incorrectly quoted sorts-- [PR #7204](https://github.com/agda/agda/issues/7204): Fix #7202: ModuleDoesntExport: only highlight missing names-- [PR #7209](https://github.com/agda/agda/issues/7209): Fix #7208: restore missing check for OverlappingProjects-- [PR #7210](https://github.com/agda/agda/issues/7210): Fix range for deprecated module import warning when applied-- [PR #7211](https://github.com/agda/agda/issues/7211): Fix #7181: Allow matching to continue when stuck on lazy pattern-- [PR #7222](https://github.com/agda/agda/issues/7222): Fix #7219: only warn about problems with warning options-- [PR #7231](https://github.com/agda/agda/issues/7231): Instantiate terms before traversing them in tcExtendContext-- [PR #7237](https://github.com/agda/agda/issues/7237): Fix #7236: use context rather than telescope for lambda-bound variables in rewrite patterns-- [PR #7238](https://github.com/agda/agda/issues/7238): Build with GHC 9.10-- [PR #7241](https://github.com/agda/agda/issues/7241): Drop time-compat dependency and Stack LTS for GHC 8.6-- [PR #7243](https://github.com/agda/agda/issues/7243): re. 7218: Saturate opaque blocks after Give commands-- [PR #7248](https://github.com/agda/agda/issues/7248): Overhaul dead code elimination, make --save-metas the default-- [PR #7249](https://github.com/agda/agda/issues/7249): docs/installation: point new wiki-- [PR #7251](https://github.com/agda/agda/issues/7251): re. 7250: copy instanceinfo-- [PR #7252](https://github.com/agda/agda/issues/7252): Fix #7193: persistently remember what is a projection-- [PR #7260](https://github.com/agda/agda/issues/7260): Reflection primitive to solve instances-- [PR #7273](https://github.com/agda/agda/issues/7273): ToTreeless: allow backends to define custom pipelines-- [PR #7274](https://github.com/agda/agda/issues/7274): #7182: copied records should refer to the copied constructor and fields-- [PR #7276](https://github.com/agda/agda/issues/7276): #7191: respect abstract mode when using show function-- [PR #7283](https://github.com/agda/agda/issues/7283): agdaLatex  documentation-- [PR #7292](https://github.com/agda/agda/issues/7292): New error warning `ConstructorDoesNotFitInData` instead of hard error.-- [PR #7298](https://github.com/agda/agda/issues/7298): Remove fiddly attempt at instance postponement-- [PR #7300](https://github.com/agda/agda/issues/7300): New deadcode warning CoinductiveEtaRecord instead of GenericError-- [PR #7302](https://github.com/agda/agda/issues/7302): Fix #7301 (loop in parser): move verifyRecordDirectives to scope checker-- [PR #7305](https://github.com/agda/agda/issues/7305): Fix #7286: don't fail hard when there are instances with unresolved types-- [PR #7307](https://github.com/agda/agda/issues/7307): fix #7017: document instance projections-- [PR #7310](https://github.com/agda/agda/issues/7310): Add `workOnTypes` reflection primitive-- [PR #7311](https://github.com/agda/agda/issues/7311): [ #6406 ] Add test cases from discussion on this issue-- [PR #7313](https://github.com/agda/agda/issues/7313): Update universe-levels.lagda.rst-- [PR #7314](https://github.com/agda/agda/issues/7314): Add constructors for custom backend warning/errors-- [PR #7315](https://github.com/agda/agda/issues/7315): same shadowing logic for record patterns as for constructor patterns in absToCon-- [PR #7316](https://github.com/agda/agda/issues/7316): add \crossmark to emacs input mode-- [PR #7317](https://github.com/agda/agda/issues/7317): Don't mark eta unit records as irrelevant-- [PR #7319](https://github.com/agda/agda/issues/7319): Make --postfix-projections the default-- [PR #7320](https://github.com/agda/agda/issues/7320): Turn on --exact-split by default-- [PR #7322](https://github.com/agda/agda/issues/7322): Expose constructor erasure in reflection interface-- [PR #7325](https://github.com/agda/agda/issues/7325): add CSS rule for macro names-- [PR #7327](https://github.com/agda/agda/issues/7327): proper error instead of impossible for clauseless pat-lam-- [PR #7330](https://github.com/agda/agda/issues/7330): [#7329] Correct module name in module applications-- [PR #7333](https://github.com/agda/agda/issues/7333): [#7332] don't loop when quoting dependent copattern lambdas-- [PR #7334](https://github.com/agda/agda/issues/7334): Fix #7331: handle permission error in search for project file-- [PR #7336](https://github.com/agda/agda/issues/7336): Remove duplicate imports and pragmas in MAlonzo-- [PR #7338](https://github.com/agda/agda/issues/7338): (#7337) foreign code needs to go in post-scope state-- [PR #7343](https://github.com/agda/agda/issues/7343): Turn illegal rewrite rules into an error warning-- [PR #7347](https://github.com/agda/agda/issues/7347): [ fix #7266 ] Check that constructor names match before projecting in `matchPattern`-- [PR #7349](https://github.com/agda/agda/issues/7349): Fix #7346 by not considering HIT-constructor arguments forced-- [PR #7350](https://github.com/agda/agda/issues/7350): Fix #6744 by reducing during forcing analysis.-- [PR #7352](https://github.com/agda/agda/issues/7352): Fix issue 7262: Range of the lhs modality check-- [PR #7353](https://github.com/agda/agda/issues/7353): Update installation docs (e.g. re #7163: document installation problems with `executable-dynamic`)-- [PR #7355](https://github.com/agda/agda/issues/7355): Make `--keep-pattern-variables` the default-- [PR #7356](https://github.com/agda/agda/issues/7356): Add --save-metas default to CHANGELOG-- [PR #7358](https://github.com/agda/agda/issues/7358): [ doc ] Document `--termination-depth` in user manual-- [PR #7359](https://github.com/agda/agda/issues/7359): Fix #7354 by making types of live metas live in DeadCode-- [PR #7360](https://github.com/agda/agda/issues/7360): Fix for issue #6841 and related changes-- [PR #7362](https://github.com/agda/agda/issues/7362): Fix #6919: separate warnings by empty line-- [PR #7364](https://github.com/agda/agda/issues/7364): Resolve instance overlap for irrelevant metas-- [PR #7367](https://github.com/agda/agda/issues/7367): Minor fixes to instance overlap + constraint postponement-- [PR #7383](https://github.com/agda/agda/issues/7383): Fix #7382: make all module param sections live in DeadCode-- [PR #7386](https://github.com/agda/agda/issues/7386): Testcase for #7382 (completes PR #7383)-- [PR #7404](https://github.com/agda/agda/issues/7404): Fix #7401: do not fail hard in Setup.hs if library interface files cannot be built-- [PR #7410](https://github.com/agda/agda/issues/7410): Fixup #7404 and test agdai-generation in cabal-install workflow-- [PR #7419](https://github.com/agda/agda/issues/7419): #7380: add clauses to generalizedTel projections-- [PR #7423](https://github.com/agda/agda/issues/7423): Fixup #7265: restore passing arguments from goal to Mimer+- [PR #7427](https://github.com/agda/agda/issues/7427): #7402: mimer failing on higher order goal+- [PR #7444](https://github.com/agda/agda/issues/7444): Fix #7436: make display forms of imported names DeadCode roots+- [PR #7445](https://github.com/agda/agda/issues/7445): Remove disclaimer that Agda would not follow the Haskell PVP+- [PR #7454](https://github.com/agda/agda/issues/7454): Fixed #7199+- [PR #7456](https://github.com/agda/agda/issues/7456): Actually, --exact-split is not really on by default+- [PR #7457](https://github.com/agda/agda/issues/7457): Revert default to `--no-save-metas`+- [PR #7465](https://github.com/agda/agda/issues/7465): Re #7455: Setup.hs: catch when Agda did not produce (all) agdai files+- [PR #7471](https://github.com/agda/agda/issues/7471): setup: Don't assume exe is built on --lib+- [PR #7475](https://github.com/agda/agda/issues/7475): Hotfix for #7442+- [PR #7476](https://github.com/agda/agda/issues/7476): Bump std-lib to latest (v2.1.1) and cubical to latest+- [PR #7480](https://github.com/agda/agda/issues/7480): Match display forms in the right context+- [PR #7487](https://github.com/agda/agda/issues/7487): Mimer shouldn't try to use existing pattern lambdas in solutions

@@ -1,7 +1,11 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} -import Data.List-import Data.Maybe+import Data.Functor ( (<&>) )+import Data.List    ( intercalate )+import Data.Maybe   ( catMaybes )  import Distribution.Simple import Distribution.Simple.LocalBuildInfo@@ -11,7 +15,7 @@ import Distribution.System ( buildPlatform )  import System.FilePath-import System.Directory (makeAbsolute, removeFile)+import System.Directory (doesFileExist, makeAbsolute, removeFile) import System.Environment (getEnvironment) import System.Process import System.Exit@@ -42,11 +46,13 @@ copyHook' pd lbi hooks flags = do   -- Copy library and executable etc.   copyHook simpleUserHooks pd lbi hooks flags-  unless (skipInterfaces lbi) $ do+  if wantInterfaces flags && not (skipInterfaces lbi) then do     -- Generate .agdai files.     success <- generateInterfaces pd lbi     -- Copy again, now including the .agdai files.     when success $ copyHook simpleUserHooks pd' lbi hooks flags+  else+    putStrLn "Skipping generation of Agda core library interface files"   where   pd' = pd     { dataFiles = concatMap (expandAgdaExt pd) $ dataFiles pd@@ -66,23 +72,54 @@     -- , extraDocFiles = []     } +-- We only want to write interfaces if installing the executable.+-- If we're installing *just* the library, the interface files are not needed+-- and, most importantly, the executable will not be available to be run (cabal#10235)+wantInterfaces :: CopyFlags -> Bool+wantInterfaces _flags = do+#if MIN_VERSION_Cabal(3,11,0)+    any isAgdaExe (copyArgs _flags)+      where+        isAgdaExe "exe:agda" = True+        isAgdaExe _ = False+#else+  True+#endif+ -- Used to add .agdai files to data-files expandAgdaExt :: PackageDescription -> FilePath -> [FilePath]-expandAgdaExt pd fp | takeExtension fp == ".agda" = [ fp, toIFile pd fp ]-                    | otherwise                   = [ fp ]+expandAgdaExt pd = \ fp ->+    -- N.B. using lambda here so that @expandAgdaExt pd@ can be partially evaluated.+    if takeExtension fp == ".agda" then [ fp, iFile fp ] else [ fp ]+  where+  iFile = toIFile pd  version :: PackageDescription -> String version = intercalate "." . map show . versionNumbers . pkgVersion . package +-- | This returns @lib/prim@.+-- projectRoot :: PackageDescription -> FilePath-projectRoot pd = takeDirectory agdaLibFile where+projectRoot pd = takeDirectory agdaLibFile+  where   [agdaLibFile] = filter ((".agda-lib" ==) . takeExtension) $ dataFiles pd -toIFile :: PackageDescription -> FilePath -> FilePath-toIFile pd file = buildDir </> fileName where+-- | Turns e.g. @lib/prim/Agda/Primitive.agda@+--   into @lib/prim/_build/2.7.0/agda/Agda/Primitive.agdai@.+--+--   An absolute path will be returned unchanged.+toIFile ::+     PackageDescription+  -> FilePath            -- ^ Should be a relative path.+  -> FilePath            -- ^ Then this is also a relative path.+toIFile pd = (buildDir </>) . fileName+  where   root = projectRoot pd+    -- e.g. root     = "lib/prim"   buildDir = root </> "_build" </> version pd </> "agda"-  fileName = makeRelative root $ replaceExtension file ".agdai"+    -- e.g. buildDir = "lib/prim/_build/2.7.0/agda"+  fileName file = makeRelative root $ replaceExtension file ".agdai"+    -- e.g. fileName "lib/prim/Agda/Primitive.agda" = "Agda/Primitive.agdai"  -- Andreas, 2019-10-21, issue #4151: -- skip the generation of interface files with program suffix "-quicker"@@ -94,6 +131,8 @@ generateInterfaces :: PackageDescription -> LocalBuildInfo -> IO Bool generateInterfaces pd lbi = do +  putStrLn "Generating Agda core library interface files..."+   -- for debugging, these are examples how you can inspect the flags...   -- print $ flagAssignment lbi   -- print $ fromPathTemplate $ progSuffix lbi@@ -102,24 +141,20 @@   let bdir = buildDir lbi       agda = bdir </> "agda" </> "agda" <.> agdaExeExtension +  -- We should be in the current directory root of the cabal package+  -- and data-files reside in src/data relative to this.+  --   ddir <- makeAbsolute $ "src" </> "data" -  -- assuming we want to type check all .agda files in data-files-  -- current directory root of the package.--  putStrLn "Generating Agda library interface files..."-   -- The Agda.Primitive* and Agda.Builtin* modules.   let builtins = filter ((== ".agda") . takeExtension) (dataFiles pd) -  -- Remove all existing .agdai files.-  forM_ builtins $ \fp -> do-    let fullpathi = toIFile pd (ddir </> fp)--        handleExists e | isDoesNotExistError e = return ()-                       | otherwise             = throwIO e+  -- The absolute filenames of their interfaces.+  let interfaces = map ((ddir </>) . toIFile pd) builtins -    removeFile fullpathi `catch` handleExists+  -- Remove all existing .agdai files.+  forM_ interfaces $ \ fp -> removeFile fp `catch` \ e ->+    unless (isDoesNotExistError e) $ throwIO e    -- Type-check all builtin modules (in a single Agda session to take   -- advantage of caching).@@ -151,19 +186,19 @@         , [ "EOF" ]         ]   let onIOError (e :: IOException) = False <$ do-        putStr $ unlines $ concat-          [ [ "*** Warning!"-            , "*** Could not generate Agda library interface files."+        warn $ concat+          [ [ "*** Could not generate Agda library interface files."             , "*** Reason:"             , show e             , "*** The attempted call to Agda was:"             ]           , callLines-          , [ "*** Ignoring error, continuing installation..." ]           ]   env <- getEnvironment   handle onIOError $ do-    True <$ readCreateProcess++    -- Generate interface files via a call to Agda.+    readCreateProcess       (proc agda agdaArgs)         { delegate_ctlc = True                           -- Make Agda look for data files in a@@ -171,6 +206,29 @@         , env           = Just ((agdaDirEnvVar, ddir) : env)         }       (unlines loadBuiltinCmds)++    -- Check whether all interface files have been generated.+    missing <- catMaybes <$> forM interfaces \ f ->+      doesFileExist f <&> \case+        True  -> Nothing+        False -> Just f++    -- Warn if not all interface files have been generated, but don't crash.+    -- This might help with issue #7455.+    let success = null missing+    unless success $ warn $ concat+      [ [ "*** Agda failed to generate the following library interface files:" ]+      , missing+      ]+    return success++warn :: [String] -> IO ()+warn msgs = putStr $ unlines $ concat+    [ [ "*** Warning!" ]+    , msgs+    , [ "*** Ignoring error, continuing installation..." ]+    ]+   agdaExeExtension :: String

@@ -1,3 +1,3 @@-(define-package "agda2-mode" "2.7.0"+(define-package "agda2-mode" "2.7.0.1"   "interactive development for Agda, a dependently typed functional programming language"   '((emacs "24.3"))) ;; dep defs for `annotation.el` and `eri.el` are not required if they are packaged together

@@ -28,7 +28,7 @@  ;;; Code: -(defvar agda2-version "2.7.0"+(defvar agda2-version "2.7.0.1"   "The version of the Agda mode. Note that the same version of the Agda executable must be used.") 

@@ -6,7 +6,7 @@ % !!! NOTE: when you make changes to this file, bump the date. !!! % !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! \ProvidesPackage{agda}-  [2021/07/14 version 2.7.0 Formatting LaTeX generated by Agda]+  [2021/07/14 version 2.7.0.1 Formatting LaTeX generated by Agda]  \RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,                 calc, environ, xparse, xkeyval}

@@ -635,39 +635,10 @@          reportSLn "import.iface" 5 $ concat ["  ", prettyShow x, " is up-to-date."] -  -- Check if we have cached the module.-  cachedE <- runExceptT $ maybeToExceptT "the interface has not been decoded" $ MaybeT $-      lift $ getDecodedModule x--  case cachedE of-    -- If it's cached ignoreInterfaces has no effect;-    -- to avoid typechecking a file more than once.-    Right mi -> do-      (ifile, hashes) <- getIFileHashesET--      let ifp = filePath $ intFilePath ifile-      let i = miInterface mi--      -- Make sure the hashes match.-      let cachedIfaceHash = iFullHash i-      let fileIfaceHash = snd hashes-      unless (cachedIfaceHash == fileIfaceHash) $ do-        lift $ dropDecodedModule x-        reportSLn "import.iface" 50 $ "  cached hash = " ++ show cachedIfaceHash-        reportSLn "import.iface" 50 $ "  stored hash = " ++ show fileIfaceHash-        reportSLn "import.iface" 5 $ "  file is newer, re-reading " ++ ifp-        throwError $ concat-          [ "the cached interface hash (", show cachedIfaceHash, ")"-          , " does not match interface file (", show fileIfaceHash, ")"-          ]--      Bench.billTo [Bench.Deserialization] $ do-        checkSourceHashET (iSourceHash i)--        reportSLn "import.iface" 5 $ "  using stored version of " ++ filePath (intFilePath ifile)-        loadDecodedModule file mi--    Left whyNotCached -> withExceptT (\e -> concat [whyNotCached, " and ", e]) $ do+  let+    -- Load or reload the interface file, if possible.+    loadInterfaceFile whyNotCached =+      withExceptT (\e -> concat [whyNotCached, " and ", e]) $ do       whenM ignoreAllInterfaces $         throwError "we're ignoring all interface files" @@ -705,6 +676,39 @@           , miMode = ModuleTypeChecked           } +  -- Check if we have cached the module.+  cachedE <- runExceptT $ maybeToExceptT "the interface has not been decoded" $ MaybeT $+      lift $ getDecodedModule x++  case cachedE of+    Left whyNotCached -> loadInterfaceFile whyNotCached++    -- If it's cached ignoreInterfaces has no effect;+    -- to avoid typechecking a file more than once.+    Right mi -> do+      (ifile, hashes) <- getIFileHashesET++      let ifp = filePath $ intFilePath ifile+      let i = miInterface mi++      -- Make sure the hashes match.+      let cachedIfaceHash = iFullHash i+      let fileIfaceHash = snd hashes+      if cachedIfaceHash /= fileIfaceHash then do+        lift $ dropDecodedModule x+        reportSLn "import.iface" 50 $ "  cached hash = " ++ show cachedIfaceHash+        reportSLn "import.iface" 50 $ "  stored hash = " ++ show fileIfaceHash+        reportSLn "import.iface" 5 $ "  file is newer, re-reading " ++ ifp+        loadInterfaceFile $ concat+          [ "the cached interface hash (", show cachedIfaceHash, ")"+          , " does not match interface file (", show fileIfaceHash, ")"+          ]+       else Bench.billTo [Bench.Deserialization] $ do+        checkSourceHashET (iSourceHash i)++        reportSLn "import.iface" 5 $ "  using stored version of " ++ filePath (intFilePath ifile)+        loadDecodedModule file mi+ -- | Report those given warnings that come from the given module.  reportWarningsForModule :: MonadDebug m => TopLevelModuleName -> [TCWarning] -> m ()@@ -1245,7 +1249,7 @@      let !scope = topLevelScope topLevel -    (!solvedMetas, !definitions) <- eliminateDeadCode scope+    (!solvedMetas, !definitions, !displayForms) <- eliminateDeadCode scope     !sig <- set sigDefinitions definitions <$> getSignature      -- Andreas, 2015-02-09 kill ranges in pattern synonyms before@@ -1253,12 +1257,6 @@     -- when expanding a pattern synonym.     !patsyns <- killRange <$> getPatternSyns -    -- Ulf, 2016-04-12:-    -- Non-closed display forms are not applicable outside the module anyway,-    -- and should be dead-code eliminated (#1928).-    !importedDisplayForms <--        HMap.filter (not . null) . HMap.map (filter isClosed) <$> useTC stImportsDisplayForms-     !userwarns   <- useTC stLocalUserWarnings     !importwarn  <- useTC stWarningOnImport     !syntaxInfo  <- useTC stSyntaxInfo@@ -1290,7 +1288,7 @@           , iInsideScope          = scope           , iSignature            = sig           , iMetaBindings         = solvedMetas-          , iDisplayForms         = importedDisplayForms+          , iDisplayForms         = displayForms           , iUserWarnings         = userwarns           , iImportWarning        = importwarn           , iBuiltin              = builtin

@@ -425,7 +425,7 @@       --   This is a stronger form of 'optImportSorts'.   , _optAllowExec                 :: WithDefault 'False       -- ^ Allow running external @executables@ from meta programs.-  , _optSaveMetas                 :: WithDefault 'True+  , _optSaveMetas                 :: WithDefault 'False       -- ^ Save meta-variables to interface files.   , _optShowIdentitySubstitutions :: WithDefault 'False       -- ^ Show identity substitutions when pretty-printing terms

@@ -469,56 +469,60 @@       Nothing -> True       Just defName -> defName /= qname && fmap ((defName `elem`)) (funMutual f) /= Just True -    go comps qname = do-      info <- getConstInfo qname-      typ <- typeOfConst qname-      scope <- getScope-      let addLevel  = qnameToComponent (costLevel   costs) qname <&> \ comp -> comps{hintLevel     = comp : hintLevel  comps}-          addAxiom  = qnameToComponent (costAxiom   costs) qname <&> \ comp -> comps{hintAxioms    = comp : hintAxioms comps}-          addThisFn = qnameToComponent (costRecCall costs) qname <&> \ comp -> comps{hintThisFn    = Just comp{ compRec = True }}-          addFn     = qnameToComponent (costFn      costs) qname <&> \ comp -> comps{hintFns       = comp : hintFns comps}-          addData   = qnameToComponent (costSet     costs) qname <&> \ comp -> comps{hintDataTypes = comp : hintDataTypes comps}-      case theDef info of-        Axiom{} | isToLevel typ    -> addLevel-                | shouldKeep scope -> addAxiom-                | otherwise        -> return comps-        -- TODO: Check if we want to use these-        DataOrRecSig{}   -> return comps-        GeneralizableVar -> return comps-        AbstractDefn{}   -> return comps-        -- If the function is in the same mutual block, do not include it.-        f@Function{}-          | Just qname == mDefName                  -> addThisFn-          | isToLevel typ && isNotMutual qname f    -> addLevel-          | isNotMutual qname f && shouldKeep scope -> addFn-          | otherwise                               -> return comps-        Datatype{} -> addData-        Record{} -> do-          projections <- mapM (qnameToComponent (costSpeculateProj costs)) =<< getRecordFields qname-          comp <- qnameToComponent (costSet costs) qname-          return comps{ hintRecordTypes = comp : hintRecordTypes comps-                      , hintProjections = projections ++ hintProjections comps }-        -- We look up constructors when we need them-        Constructor{} -> return comps-        -- TODO: special treatment for primitives?-        Primitive{} | isToLevel typ    -> addLevel-                    | shouldKeep scope -> addFn-                    | otherwise        -> return comps-        PrimitiveSort{} -> return comps-      where-        shouldKeep scope = or-          [ qname `elem` explicitHints-          , qname `elem` whereNames-          , case hintMode of-              Unqualified -> Scope.isNameInScopeUnqualified qname scope-              AllModules  -> True-              Module      -> Just (qnameModule qname) == mThisModule-              NoHints     -> False-          ]+    go comps qname = go' comps qname =<< getConstInfo qname -        -- TODO: There is probably a better way of finding the module name-        mThisModule = qnameModule <$> mDefName+    go' comps qname info+      | isExtendedLambda (theDef info) = return comps    -- We can't use pattern lambdas as components+      | isWithFunction   (theDef info) = return comps    -- or with functions+      | otherwise = do+        typ <- typeOfConst qname+        scope <- getScope+        let addLevel  = qnameToComponent (costLevel   costs) qname <&> \ comp -> comps{hintLevel     = comp : hintLevel  comps}+            addAxiom  = qnameToComponent (costAxiom   costs) qname <&> \ comp -> comps{hintAxioms    = comp : hintAxioms comps}+            addThisFn = qnameToComponent (costRecCall costs) qname <&> \ comp -> comps{hintThisFn    = Just comp{ compRec = True }}+            addFn     = qnameToComponent (costFn      costs) qname <&> \ comp -> comps{hintFns       = comp : hintFns comps}+            addData   = qnameToComponent (costSet     costs) qname <&> \ comp -> comps{hintDataTypes = comp : hintDataTypes comps}+        case theDef info of+          Axiom{} | isToLevel typ    -> addLevel+                  | shouldKeep scope -> addAxiom+                  | otherwise        -> return comps+          -- TODO: Check if we want to use these+          DataOrRecSig{}   -> return comps+          GeneralizableVar -> return comps+          AbstractDefn{}   -> return comps+          -- If the function is in the same mutual block, do not include it.+          f@Function{}+            | Just qname == mDefName                  -> addThisFn+            | isToLevel typ && isNotMutual qname f    -> addLevel+            | isNotMutual qname f && shouldKeep scope -> addFn+            | otherwise                               -> return comps+          Datatype{} -> addData+          Record{} -> do+            projections <- mapM (qnameToComponent (costSpeculateProj costs)) =<< getRecordFields qname+            comp <- qnameToComponent (costSet costs) qname+            return comps{ hintRecordTypes = comp : hintRecordTypes comps+                        , hintProjections = projections ++ hintProjections comps }+          -- We look up constructors when we need them+          Constructor{} -> return comps+          -- TODO: special treatment for primitives?+          Primitive{} | isToLevel typ    -> addLevel+                      | shouldKeep scope -> addFn+                      | otherwise        -> return comps+          PrimitiveSort{} -> return comps+        where+          shouldKeep scope = or+            [ qname `elem` explicitHints+            , qname `elem` whereNames+            , case hintMode of+                Unqualified -> Scope.isNameInScopeUnqualified qname scope+                AllModules  -> True+                Module      -> Just (qnameModule qname) == mThisModule+                NoHints     -> False+            ] +          -- TODO: There is probably a better way of finding the module name+          mThisModule = qnameModule <$> mDefName+     -- NOTE: We do not reduce the type before checking, so some user definitions     -- will not be included here.     isToLevel :: Type -> Bool@@ -614,7 +618,6 @@     IPNoClause -> makeOpen []     IPClause{ipcQName = fnName, ipcClauseNo = clauseNr} -> do       info <- getConstInfo fnName-      typ <- typeOfConst fnName       parCount <- liftTCM getCurrentModuleFreeVars       case theDef info of         fnDef@Function{} -> do@@ -724,7 +727,9 @@                                        , "with args" <+> pretty (instTel inst) ]        -- ctx <- getContextTelescope-      return metaIds+      -- #7402: still solve the top-level meta, because we don't have the correct contexts for the+      --        submetas+      return [metaId | not $ null metaIds]     OpenMeta UnificationMeta -> do       reportSLn "mimer.init" 20 "Interaction point not instantiated."       return [metaId]@@ -1123,7 +1128,6 @@ tryLamAbs goal goalType branch =   case unEl goalType of     Pi dom abs -> do-     e <- isEmptyType (unDom dom)      isEmptyType (unDom dom) >>= \case -- TODO: Is this the correct way of checking if absurd lambda is applicable?       True -> do         let argInf = defaultArgInfo{argInfoOrigin = Inserted} -- domInfo dom

@@ -2448,12 +2448,14 @@    forM xs $ \ x -> do     e <- toAbstract $ OldQName x Nothing     case e of-      A.Def x          -> return [ x ]+      A.Def' x NoSuffix -> return [ x ]+      A.Def' x Suffix{} -> genericError $ "REWRITE used on name with suffix"       A.Proj _ p | Just x <- getUnambiguous p -> return [ x ]       A.Proj _ x       -> genericError $ "REWRITE used on ambiguous name " ++ prettyShow x       A.Con c | Just x <- getUnambiguous c -> return [ x ]       A.Con x          -> genericError $ "REWRITE used on ambiguous name " ++ prettyShow x       A.Var x          -> genericError $ "REWRITE used on parameter " ++ prettyShow x ++ " instead of on a defined symbol"+      A.PatternSyn{}   -> genericError $ "REWRITE used on pattern synonym"       _       -> __IMPOSSIBLE__   toAbstract (C.ForeignPragma _ rb s) = [] <$ addForeignCode (rangedThing rb) s   toAbstract (C.CompilePragma _ rb x s) = do@@ -2463,7 +2465,8 @@       Just e  -> do         let err what = genericError $ "Cannot COMPILE " ++ what ++ " " ++ prettyShow x         y <- case e of-          A.Def x             -> return x+          A.Def' x NoSuffix   -> return x+          A.Def' x Suffix{}   -> err "name with suffix"           A.Proj _ p | Just x <- getUnambiguous p -> return x           A.Proj _ x          -> err "ambiguous projection"           A.Con c | Just x <- getUnambiguous c -> return x

@@ -2,7 +2,7 @@  module Agda.TypeChecking.DeadCode (eliminateDeadCode) where -import Control.Monad ((<$!>), filterM)+import Control.Monad (filterM) import Control.Monad.Trans  import Data.Maybe@@ -30,20 +30,21 @@ --   public interface. We do not compute reachable data precisely, because that --   would be very expensive, mainly because of rewrite rules. The following --   things are assumed to be "roots":---     - public names (for definitions and pattern synonyms)+--     - public definitions --     - definitions marked as primitive --     - definitions with COMPILE pragma---     - all parameter sections (because all sections go into interfaces!)+--     - all pattern synonyms (because currently all of them go into interfaces)+--     - all parameter sections (because currently all of them go into interfaces) --       (see also issues #6931 and #7382) --     - local builtins --     - all rewrite rules---   We only ever prune dead metavariables and definitions. The reachable ones---   are returned from this function.-eliminateDeadCode :: ScopeInfo -> TCM (RemoteMetaStore, Definitions)+--     - closed display forms+--   We only ever prune dead metavariables and definitions. We return the pruned metas,+--   pruned definitions and closed display forms.+eliminateDeadCode :: ScopeInfo -> TCM (RemoteMetaStore, Definitions, DisplayForms) eliminateDeadCode !scope = Bench.billTo [Bench.DeadCode] $ do   !sig <- getSignature   let !defs = sig ^. sigDefinitions-  !psyns <- getPatternSyns   !metas <- useR stSolvedMetaStore    -- #2921: Eliminating definitions with attached COMPILE pragmas results in@@ -63,12 +64,18 @@    let !pubModules = publicModules scope +    -- Ulf, 2016-04-12:+    -- Non-closed display forms are not applicable outside the module anyway,+    -- and should be dead-code eliminated (#1928).+  !rootDisplayForms <-+      HMap.filter (not . null) . HMap.map (filter isClosed) <$> useTC stImportsDisplayForms+   let !rootPubNames  = map anameName $ publicNamesOfModules pubModules   let !rootExtraDefs = mapMaybe extraRootsFilter $ HMap.toList defs   let !rootRewrites  = sig ^. sigRewriteRules-   let !rootModSections = sig ^. sigSections   !rootBuiltins <- useTC stLocalBuiltins+  !rootPatSyns  <- getPatternSyns    !seenNames <- liftIO HT.empty :: TCM (HashTable QName ())   !seenMetas <- liftIO HT.empty :: TCM (HashTable MetaId ())@@ -80,7 +87,6 @@         Nothing -> do           HT.insert seenNames x ()           go (HMap.lookup x defs)-          go (PSyn <$!> MapS.lookup x psyns)        goMeta :: MetaId -> IO ()       goMeta !m = HT.lookup seenMetas m >>= \case@@ -99,11 +105,13 @@       {-# INLINE go #-}    Bench.billTo [Bench.DeadCode, Bench.DeadCodeReachable] $ liftIO $ do+    go rootDisplayForms     foldMap goName rootPubNames     foldMap goName rootExtraDefs     go rootRewrites     go rootModSections     go rootBuiltins+    foldMap (go . PSyn) rootPatSyns    let filterMeta :: (MetaId, MetaVariable) -> IO (Maybe (MetaId, RemoteMetaVariable))       filterMeta (!i, !m) = HT.lookup seenMetas i >>= \case@@ -117,7 +125,7 @@    !metas <- liftIO $ HMap.fromList <$> mapMaybeM filterMeta (MapS.toList metas)   !defs  <- liftIO $ HMap.fromList <$> filterM filterDef (HMap.toList defs)-  pure (metas, defs)+  pure (metas, defs, rootDisplayForms)  -- | Returns the instantiation. --   Precondition: The instantiation must be of the form @'InstV' inst@.

@@ -114,13 +114,28 @@   | length ps > length es = mzero   | otherwise             = do       let (es0, es1) = splitAt (length ps) es-      mm <- match (Window 0 n) ps es0++      -- The 'Display' constructor acts as though it binds the pattern+      -- pattern variables up to 'n', so a match like+      --+      --   Display 1 [@1 @0] x =? [@0 _]+      --+      -- should work (it didn't; see LiftDisplayIntermediate). In+      -- effect, this is because the LHS patterns are in some context+      -- "Γ . @0", but the RHS term is only in context Γ.+      --+      -- Therefore, we should raise the RHS term by the number of+      -- pattern variables, to bring it into the context of the+      -- patterns.++      mm <- match (Window 0 n) ps (raise n es0)       us <- forM [0 .. n - 1] $ \ i -> do-              -- #5294: Fail if we don't have bindings for all variables. This can-              --        happen outside parameterised modules when some of the parameters-              --        are not used in the lhs.-              Just u <- return $ Map.lookup i mm-              return u+        -- #5294: Fail if we don't have bindings for all variables. This can+        --        happen outside parameterised modules when some of the parameters+        --        are not used in the lhs.+        Just u <- return $ Map.lookup i mm+        -- Note that the RHS terms are independent of the pattern variables.+        return (applySubst (strengthenS __IMPOSSIBLE__ n) <$> u)       return (d, substWithOrigin (parallelS $ map woThing us) us v `applyE` es1)  type MatchResult = Map Int (WithOrigin Term)

@@ -100,7 +100,7 @@      -- If t is a record type, see if any of the field types is empty     Right (r, pars, def) -> do-      ifNotM (isEtaRecordDef def) (return $ Left Fail) $+      if not (isEtaRecordDef def) then return $ Left Fail else          void <$> do checkEmptyTel range $ _recTel def `apply` pars  -- | Check whether one of the types in the given telescope is constructor-less

@@ -3092,6 +3092,18 @@     Function { funClauses = [] } -> True     _ -> False +isExtendedLambda :: Defn -> Bool+isExtendedLambda def =+  case def of+    Function { funExtLam = Just{} } -> True+    _ -> False++isWithFunction :: Defn -> Bool+isWithFunction def =+  case def of+    Function { funWith = Just{} } -> True+    _ -> False+ isCopatternLHS :: [Clause] -> Bool isCopatternLHS = List.any (List.any (isJust . A.isProjP) . namedClausePats) 

@@ -447,17 +447,14 @@ isEtaRecord :: HasConstInfo m => QName -> m Bool isEtaRecord r = do   isRecord r >>= \case-    Nothing -> return False-    Just r -> isEtaRecordDef r--isEtaRecordDef :: HasConstInfo m => RecordData -> m Bool-isEtaRecordDef r-  | _recEtaEquality r /= YesEta = return False-  | otherwise = do+    Just r | isEtaRecordDef r -> do      constructorQ <- getQuantity <$> getConstInfo (conName (_recConHead r))      currentQ     <- viewTC eQuantity      return $ constructorQ `moreQuantity` currentQ+    _ -> return False +isEtaRecordDef :: RecordData -> Bool+isEtaRecordDef r = _recEtaEquality r == YesEta  {-# SPECIALIZE isEtaCon :: QName -> TCM Bool #-} isEtaCon :: HasConstInfo m => QName -> m Bool@@ -467,7 +464,7 @@ isEtaOrCoinductiveRecordConstructor :: HasConstInfo m => QName -> m Bool isEtaOrCoinductiveRecordConstructor c =   caseMaybeM (isRecordConstructor c) (return False) $ \ (_, def) ->-    isEtaRecordDef def `or2M`+    pure (isEtaRecordDef def) `or2M`       return (_recInduction def /= Just Inductive)       -- If in doubt about coinductivity, then yes. @@ -500,7 +497,7 @@ isEtaRecordConstructor :: HasConstInfo m => QName -> m (Maybe (QName, RecordData)) isEtaRecordConstructor c = isRecordConstructor c >>= \case   Nothing -> return Nothing-  Just (d, def) -> ifM (isEtaRecordDef def) (return $ Just (d, def)) (return Nothing)+  Just (d, def) -> if isEtaRecordDef def then return $ Just (d, def) else return Nothing  -- | Turn off eta for unguarded recursive records. --   Projections do not preserve guardedness.@@ -576,7 +573,7 @@           " since its type " <+> prettyTCM a <+>           " is not a record type"         return Nothing-  caseMaybeM (isRecordType a) failure $ \ (r, pars, def) -> isEtaRecordDef def >>= \case+  caseMaybeM (isRecordType a) failure $ \ (r, pars, def) -> case isEtaRecordDef def of     False -> return Nothing     True  -> Just <$> do       -- Get the record fields @Γ₁ ⊢ tel@ (@tel = Γ'@).@@ -928,7 +925,7 @@         record :: m (Maybe Term)         record = runMaybeT $ do           (r, ps, def) <- MaybeT $ isRecordType t-          guardM $ isEtaRecordDef def+          guard $ isEtaRecordDef def           abstract tel <$> MaybeT (isSingletonRecord' regardIrrelevance r ps rs)          -- Slightly harder case: η for Sub {level} tA phi elt.