Agda 2.6.2.1 → 2.6.2.2

raw patch · 131 files changed

+1290/−726 lines, 131 filesdep ~aesondep ~basedep ~bytestringPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: aeson, base, bytestring, template-haskell, transformers

API changes (from Hackage documentation)

Files

• Agda.cabal +20/−11
• CHANGELOG.md +74/−114
• LICENSE +1/−1
• doc/release-notes/2.6.2.1.md +149/−0
• 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/data/lib/prim/Agda/Builtin/Cubical/HCompU.agda +1/−1
• src/data/lib/prim/Agda/Builtin/Cubical/Id.agda +1/−1
• src/data/lib/prim/Agda/Builtin/Cubical/Path.agda +1/−1
• src/data/lib/prim/Agda/Builtin/Cubical/Sub.agda +1/−1
• src/data/lib/prim/Agda/Primitive/Cubical.agda +1/−1
• src/full/Agda/Auto/Auto.hs +2/−0
• src/full/Agda/Auto/CaseSplit.hs +6/−4
• src/full/Agda/Auto/Convert.hs +2/−0
• src/full/Agda/Auto/NarrowingSearch.hs +4/−1
• src/full/Agda/Compiler/Backend.hs +2/−1
• src/full/Agda/Compiler/CallCompiler.hs +15/−3
• src/full/Agda/Compiler/MAlonzo/Compiler.hs +37/−22
• src/full/Agda/Compiler/MAlonzo/Pretty.hs +9/−6
• src/full/Agda/Compiler/ToTreeless.hs +5/−2
• src/full/Agda/Compiler/Treeless/Simplify.hs +3/−2
• src/full/Agda/Interaction/AgdaTop.hs +5/−1
• src/full/Agda/Interaction/Base.hs +2/−0
• src/full/Agda/Interaction/BasicOps.hs +82/−64
• src/full/Agda/Interaction/CommandLine.hs +2/−0
• src/full/Agda/Interaction/EmacsTop.hs +6/−2
• src/full/Agda/Interaction/FindFile.hs +2/−1
• src/full/Agda/Interaction/Highlighting/Dot/Backend.hs +4/−3
• src/full/Agda/Interaction/Highlighting/Dot/Base.hs +4/−2
• src/full/Agda/Interaction/Highlighting/FromAbstract.hs +2/−1
• src/full/Agda/Interaction/Highlighting/LaTeX/Base.hs +4/−1
• src/full/Agda/Interaction/Imports.hs +5/−1
• src/full/Agda/Interaction/InteractionTop.hs +41/−44
• src/full/Agda/Interaction/JSONTop.hs +11/−9
• src/full/Agda/Interaction/Library.hs +13/−24
• src/full/Agda/Interaction/Library/Base.hs +1/−8
• src/full/Agda/Interaction/Library/Parse.hs +2/−1
• src/full/Agda/Interaction/MakeCase.hs +1/−1
• src/full/Agda/Interaction/Options/Base.hs +1/−1
• src/full/Agda/Interaction/Options/Lenses.hs +1/−1
• src/full/Agda/Interaction/Options/Warnings.hs +0/−8
• src/full/Agda/Main.hs +3/−1
• src/full/Agda/Syntax/Abstract/Pattern.hs +4/−3
• src/full/Agda/Syntax/Abstract/PatternSynonyms.hs +3/−2
• src/full/Agda/Syntax/Concrete/Definitions.hs +4/−2
• src/full/Agda/Syntax/Concrete/Definitions/Monad.hs +3/−2
• src/full/Agda/Syntax/Concrete/Pattern.hs +3/−1
• src/full/Agda/Syntax/Internal.hs +4/−1
• src/full/Agda/Syntax/Internal/Pattern.hs +3/−2
• src/full/Agda/Syntax/Parser.hs +2/−0
• src/full/Agda/Syntax/Parser/Lexer.x +2/−3
• src/full/Agda/Syntax/Scope/Monad.hs +14/−3
• src/full/Agda/Syntax/Translation/AbstractToConcrete.hs +5/−4
• src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs +15/−21
• src/full/Agda/Syntax/Translation/InternalToAbstract.hs +3/−3
• src/full/Agda/Syntax/Translation/ReflectedToAbstract.hs +16/−8
• src/full/Agda/Termination/Monad.hs +2/−0
• src/full/Agda/Termination/RecCheck.hs +1/−1
• src/full/Agda/Termination/TermCheck.hs +5/−5
• src/full/Agda/TypeChecking/CheckInternal.hs +3/−3
• src/full/Agda/TypeChecking/Constraints.hs +2/−0
• src/full/Agda/TypeChecking/Conversion.hs +6/−4
• src/full/Agda/TypeChecking/Coverage.hs +22/−11
• src/full/Agda/TypeChecking/Datatypes.hs +2/−1
• src/full/Agda/TypeChecking/Empty.hs +2/−1
• src/full/Agda/TypeChecking/Free/Lazy.hs +2/−2
• src/full/Agda/TypeChecking/Generalize.hs +8/−5
• src/full/Agda/TypeChecking/Implicit.hs +2/−1
• src/full/Agda/TypeChecking/InstanceArguments.hs +9/−7
• src/full/Agda/TypeChecking/Irrelevance.hs +3/−4
• src/full/Agda/TypeChecking/Level/Solve.hs +3/−4
• src/full/Agda/TypeChecking/Lock.hs +1/−1
• src/full/Agda/TypeChecking/MetaVars.hs +3/−2
• src/full/Agda/TypeChecking/MetaVars/Mention.hs +1/−0
• src/full/Agda/TypeChecking/Monad/Base.hs +46/−16
• src/full/Agda/TypeChecking/Monad/Base.hs-boot +13/−3
• src/full/Agda/TypeChecking/Monad/Builtin.hs +2/−0
• src/full/Agda/TypeChecking/Monad/Builtin.hs-boot +4/−2
• src/full/Agda/TypeChecking/Monad/Constraints.hs +1/−0
• src/full/Agda/TypeChecking/Monad/Context.hs +1/−0
• src/full/Agda/TypeChecking/Monad/Debug.hs +2/−0
• src/full/Agda/TypeChecking/Monad/Imports.hs +2/−3
• src/full/Agda/TypeChecking/Monad/MetaVars.hs +52/−49
• src/full/Agda/TypeChecking/Monad/Options.hs +99/−5
• src/full/Agda/TypeChecking/Monad/Options.hs-boot +9/−0
• src/full/Agda/TypeChecking/Monad/Signature.hs +29/−15
• src/full/Agda/TypeChecking/Monad/State.hs +1/−1
• src/full/Agda/TypeChecking/Names.hs +7/−4
• src/full/Agda/TypeChecking/Polarity.hs +2/−2
• src/full/Agda/TypeChecking/Positivity.hs +11/−8
• src/full/Agda/TypeChecking/Pretty/Constraint.hs +2/−0
• src/full/Agda/TypeChecking/Primitive.hs +1/−6
• src/full/Agda/TypeChecking/Primitive/Cubical.hs +64/−25
• src/full/Agda/TypeChecking/ProjectionLike.hs +7/−3
• src/full/Agda/TypeChecking/ReconstructParameters.hs +7/−11
• src/full/Agda/TypeChecking/RecordPatterns.hs +7/−4
• src/full/Agda/TypeChecking/Reduce.hs +65/−30
• src/full/Agda/TypeChecking/Reduce/Fast.hs +5/−3
• src/full/Agda/TypeChecking/Reduce/Monad.hs +1/−1
• src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs +4/−3
• src/full/Agda/TypeChecking/Rewriting/NonLinPattern.hs +2/−1
• src/full/Agda/TypeChecking/Rules/Application.hs +4/−2
• src/full/Agda/TypeChecking/Rules/Decl.hs +8/−6
• src/full/Agda/TypeChecking/Rules/Def.hs +2/−2
• src/full/Agda/TypeChecking/Rules/LHS.hs +1/−1
• src/full/Agda/TypeChecking/Rules/LHS/Problem.hs +3/−2
• src/full/Agda/TypeChecking/Rules/LHS/Unify.hs +2/−0
• src/full/Agda/TypeChecking/Rules/Term.hs +4/−2
• src/full/Agda/TypeChecking/Serialise.hs +22/−17
• src/full/Agda/TypeChecking/Serialise/Base.hs +1/−0
• src/full/Agda/TypeChecking/Serialise/Instances/Common.hs +5/−4
• src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs +0/−4
• src/full/Agda/TypeChecking/SizedTypes.hs +3/−2
• src/full/Agda/TypeChecking/Substitute.hs +1/−0
• src/full/Agda/TypeChecking/SyntacticEquality.hs +5/−3
• src/full/Agda/TypeChecking/Unquote.hs +27/−8
• src/full/Agda/Utils/Benchmark.hs +1/−0
• src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs +1/−1
• src/full/Agda/Utils/IO/Directory.hs +4/−1
• src/full/Agda/Utils/IO/UTF8.hs +10/−0
• src/full/Agda/Utils/ListT.hs +1/−0
• src/full/Agda/Utils/Monad.hs +4/−3
• src/full/Agda/Utils/Null.hs +9/−5
• src/full/Agda/Utils/Suffix.hs +17/−7
• src/full/Agda/Utils/Update.hs +2/−1
• stack-8.10.7.yaml +1/−1
• stack-9.0.1.yaml +4/−1
• stack-9.0.2.yaml +7/−0
• stack-9.2.1.yaml +2/−2
• stack-9.2.2.yaml +6/−0

@@ -1,10 +1,10 @@ name:            Agda-version:         2.6.2.1+version:         2.6.2.2 cabal-version:   >= 1.10 build-type:      Custom license:         OtherLicense license-file:    LICENSE-copyright:       (c) 2005-2021 The Agda Team.+copyright:       (c) 2005-2022 The Agda Team. author:          Ulf Norell and The Agda Team, see https://agda.readthedocs.io/en/latest/team.html maintainer:      The Agda Team homepage:        http://wiki.portal.chalmers.se/agda/@@ -24,7 +24,7 @@   theory, a foundational system for constructive mathematics developed   by the Swedish logician Per Martin-L&#xf6;f. It has many   similarities with other proof assistants based on dependent types,-  such as Coq, Epigram and NuPRL.+  such as Coq, Idris, Lean and NuPRL.   .   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@@ -41,10 +41,13 @@                     GHC == 8.8.4                     GHC == 8.10.7                     GHC == 9.0.1+                    GHC == 9.0.2                     GHC == 9.2.1+                    GHC == 9.2.2  extra-source-files: CHANGELOG.md                     README.md+                    doc/release-notes/2.6.2.1.md                     doc/release-notes/2.6.2.md                     doc/release-notes/2.6.1.3.md                     doc/release-notes/2.6.1.2.md@@ -88,7 +91,9 @@                     stack-8.8.4.yaml                     stack-8.10.7.yaml                     stack-9.0.1.yaml+                    stack-9.0.2.yaml                     stack-9.2.1.yaml+                    stack-9.2.2.yaml  data-dir:           src/data data-files:         emacs-mode/*.el@@ -143,7 +148,7 @@ source-repository this   type:     git   location: https://github.com/agda/agda.git-  tag:      v2.6.2.1+  tag:      v2.6.2.2  flag cpphs   default:     False@@ -219,7 +224,7 @@                 , deepseq >= 1.4.2.0 && < 1.5                 , directory >= 1.2.6.2 && < 1.4                 , edit-distance >= 0.2.1.2 && < 0.3-                , equivalence >= 0.3.2 && < 0.4+                , equivalence >= 0.3.2 && < 0.5                 -- exceptions-0.8 instead of 0.10 because of stack                 , exceptions >= 0.8 && < 0.11                 , filepath >= 1.4.1.0 && < 1.5@@ -237,11 +242,9 @@                 , haskeline >= 0.7.2.3 && < 0.9                 -- monad-control-1.0.1.0 is the first to contain liftThrough                 , monad-control >= 1.0.1.0 && < 1.1-                -- mtl-2.1 contains a severe bug.-                --                 -- mtl >= 2.2 && < 2.2.1 doesn't export Control.Monad.Except.                 -- Need mtl 2.2.2  for export of Control.Monad.IdentityT (ghc 8.2.2+)-                , mtl >= 2.2.1 && < 2.3+                , mtl >= 2.2.1 && < 2.4                 , murmur-hash >= 0.1 && < 0.2                 , parallel >= 3.2.2.0 && < 3.3                 , pretty >= 1.1.3.3 && < 1.2@@ -251,13 +254,19 @@                 , stm >= 2.4.4 && < 2.6                 , strict >= 0.3.2 && < 0.5                 , template-haskell >= 2.11.0.0 && < 2.19-                , text >= 1.2.3.0 && < 1.3+                , text >= 1.2.3.0 && < 2.1                 , time >= 1.6.0.1 && < 1.13                 , transformers >= 0.5 && < 0.7                 , unordered-containers >= 0.2.5.0 && < 0.3                 , uri-encode >= 1.5.0.4 && < 1.6                 , zlib == 0.6.* +  -- Andreas, 2022-02-02, issue #5659:+  -- Build failure with transformers-0.6.0.{0,1,2} and GHC 8.6.+  -- Transformers-0.6.0.3 might restored GHC 8.6 buildability.+  if impl(ghc == 8.6.*)+    build-depends: transformers < 0.6 || >= 0.6.0.3+   -- Andreas, 2021-03-10:   -- All packages we depend upon should be mentioned in an unconditional   -- build-depends field, but additional restrictions on their@@ -793,8 +802,8 @@                   -- GHC 8.2.1 RC1).                    -- Nothing is used from the following package,-                  -- except for the prelude.-                , base >= 4.9.0.0 && < 6+                  -- except for the Prelude.+                , base   default-language: Haskell2010   -- If someone installs Agda with the setuid bit set, then the   -- presence of +RTS may be a security problem (see GHC bug #3910).

@@ -1,149 +1,109 @@-Release notes for Agda version 2.6.2.1+Release notes for Agda version 2.6.2.2 ======================================  Highlights ---------- -* Agda 2.6.2.1 catches up to changes in the Haskell ecosystem-  (GHC 9.2.1, `aeson-2.0`, `hashable-1.4.`).+* Agda 2.6.2.2 catches up to changes in the Haskell ecosystem+  (`bytestring-0.11.2.0`, `mtl-2.3-rc3/4`, `text-icu-0.8.0.1`,+  stackage `lts-19.0` and `nightly`). +* Fixes inconsistency [#5838](https://github.com/agda/agda/issues/5838)+  in `--cubical`.+ * Fixes some regressions introduced in 2.6.1:-  [#5283](https://github.com/agda/agda/issues/5283)-  [#5506](https://github.com/agda/agda/issues/5506)-  [#5610](https://github.com/agda/agda/issues/5610) +  - [#5809](https://github.com/agda/agda/issues/5809):+    internal error with `--irrelevant-projections`.+ * Fixes some regressions introduced in 2.6.2:-  [#5508](https://github.com/agda/agda/issues/5508)-  [#5544](https://github.com/agda/agda/issues/5544)-  [#5565](https://github.com/agda/agda/issues/5565)-  [#5584](https://github.com/agda/agda/issues/5584)-  [#5620](https://github.com/agda/agda/issues/5620)-  [#5638](https://github.com/agda/agda/issues/5638)-  [#5657](https://github.com/agda/agda/issues/5657) -* Improvements to the compiler backends (see below).+  - [#5705](https://github.com/agda/agda/issues/5705) and+    [#5706](https://github.com/agda/agda/issues/5706):+    inconsistency from universe level `Int` overflow. -* Feature preview: `--ghc-strict`.+  - [#5784](https://github.com/agda/agda/issues/5784):+    `primEraseEquality` does not compute. -Installation and infrastructure--------------------------------+  - [#5805](https://github.com/agda/agda/issues/5805):+    internal error involving holes and `with`. -Agda 2.6.2.1 is expected to build with GHC versions 8.0 to 9.2.-It has been tested with the latest minor version releases of GHC for-each of these major versions:+  - [#5819](https://github.com/agda/agda/issues/5819):+    internal error when reducing in termination checker. -  - 8.0.2-  - 8.2.2-  - 8.4.4-  - 8.6.5-  - 8.8.4-  - 8.10.7: Issue [#5539](https://github.com/agda/agda/issues/5539).-  - 9.0.1-  - 9.2.1:-    Issue [#5442](https://github.com/agda/agda/issues/5442),-    stackage issue [#6318](https://github.com/commercialhaskell/stackage/pull/6318).+* Other+  [fixes](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.2.2+is%3Aclosed)+  and improvements (see below). -Agda 2.6.2.1 has been adapted to recent changes in the Haskell ecosystem, including:+Installation and infrastructure+------------------------------- -  - `Cabal-3.6.2`-  - `aeson-2.0`:-    Issue [#5593](https://github.com/agda/agda/issues/5593),-    stackage issue [#6217](https://github.com/commercialhaskell/stackage/issues/6217).-  - `hashable-1.4`:-    Stackage issue [#6268](https://github.com/commercialhaskell/stackage/issues/6268).-  - `transformers-0.6`+Agda supports GHC versions 8.0.2 to 9.2.2. -Compiler backends------------------+* UTF-8 encoding is now used for the `libraries` and `executables`+  configuration files (issue+  [#5741](https://github.com/agda/agda/issues/5741)). -* Both the GHC and JS backends now refuse to compile code that uses-  `--cubical`.+Language+-------- -* The new option `--ghc-strict-data`, which is inspired by the GHC-  language extension `StrictData`, makes the GHC backend compile-  inductive data and record constructors to constructors with strict-  arguments.+* `macro` definitions can now be used even when they are declared as erased+  (PR [#5744](https://github.com/agda/agda/pull/5744)).+  For example, this is now accepted:+  ```agda+  macro+    @0 trivial : Term → TC ⊤+    trivial = unify (con (quote refl) []) -  This does not apply to certain builtin types—lists, the maybe type,-  and some types related to reflection—and might not apply to types-  with `COMPILE GHC … = data …` pragmas.+  test : 42 ≡ 42+  test = trivial+  ``` -  This feature is experimental.+* Fixed inconsistent `--cubical` reductions for `transp`:+  issue [#5838](https://github.com/agda/agda/issues/5838). -* The new option `--ghc-strict`, which is inspired by the GHC language-  extension `Strict`, makes the GHC backend generate mostly strict-  code.+* Fixed issues with reflection: -  Functions might not be strict in unused arguments.+  - [#5762](https://github.com/agda/agda/issues/5762):+    do not eagerly check existence of commands in `executables` file. -  Function definitions coming from `COMPILE GHC` pragmas are not-  affected.+  - [#5695](https://github.com/agda/agda/issues/5695):+    fix `elaborate-and-give` interaction command. -  This flag implies `--ghc-strict-data`, and the exceptions of that-  flag applies to this flag as well.+  - [#5700](https://github.com/agda/agda/issues/5700):+    scope of metas created during macro expansion. -  Note that this option requires the use of GHC 9 or later.+  - [#5712](https://github.com/agda/agda/issues/5712):+    internal error with tactics on record fields of function type. -  This feature is experimental.+* Fixed issues with instance search: -* JS backend now uses the native `BigInt` instead of the-  [biginteger.js](https://github.com/silentmatt/javascript-biginteger).-  Fixes [#4878](https://github.com/agda/agda/issues/4878).+  - [#5583](https://github.com/agda/agda/issues/5583):+    constructor instances from parameterized modules. -LaTeX backend--------------+  - [#5787](https://github.com/agda/agda/issues/5787):+    erased instance arguments. -* Files `agda.sty` and `postprocess-latex.pl` are now found in the `latex/`-  subdirectory of the Agda data directory (`agda --print-agda-dir`).+* Fixed issue [#5683](https://github.com/agda/agda/issues/5683) with+  generalization in `let`. -* `agda.sty` is now versioned (printed to the `.log` file by `latex`)-  (see [#5473](https://github.com/agda/agda/issues/5473)).+Compiler backends+----------------- -* Italics correction (inserted by `\textit` e.g. in `\AgdaBound`) now works,-  thanks to moving the `\textcolor` wrapping to the outside in `agda.sty`-  (see [#5471](https://github.com/agda/agda/issues/5471)).+* `.hs` files generated by the GHC backend now switch off the+  `warn-overlapping-patterns` warning (issue+  [#5758](https://github.com/agda/agda/issues/5758)). -List of closed issues----------------------+* The GHC backend now calls `ghc` with environment setting+  `GHC_CHARENC=UTF-8` (issue+  [#5742](https://github.com/agda/agda/issues/5742)). -For 2.6.2.1, the following issues were-[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.2.1+is%3Aclosed)-(see [bug tracker](https://github.com/agda/agda/issues)):+Performance+----------- -  - [#4878](https://github.com/agda/agda/issues/4878): Replace biginteger.js with native BigInt-  - [#5283](https://github.com/agda/agda/issues/5283): Tactic command runs forever-  - [#5291](https://github.com/agda/agda/issues/5291): `match` doesn't work for non-prefix-free cases-  - [#5302](https://github.com/agda/agda/issues/5302): building tests with cabal-  - [#5396](https://github.com/agda/agda/issues/5396): Internal error for rewriting without --confluence-check-  - [#5398](https://github.com/agda/agda/issues/5398): Problem with LaTeX code for multi-line comments with blank lines-  - [#5420](https://github.com/agda/agda/issues/5420): The JS backend generates incorrect code for Agda code that uses reflection-  - [#5421](https://github.com/agda/agda/issues/5421): The GHC backend generates incorrect code for Agda code that uses reflection-  - [#5431](https://github.com/agda/agda/issues/5431): --ghc-strict-data and --ghc-strict-  - [#5433](https://github.com/agda/agda/issues/5433): The JS backend "installs" highlight-hover.js-  - [#5440](https://github.com/agda/agda/issues/5440): (Re)Documenting `catchfilebetweentags` method of building latex files with Agda-  - [#5442](https://github.com/agda/agda/issues/5442): Support GHC 9.2-  - [#5463](https://github.com/agda/agda/issues/5463): Hole in the middle of a record is malformed-  - [#5465](https://github.com/agda/agda/issues/5465): Compilation of Parser.y depends on the locale on Debian too-  - [#5469](https://github.com/agda/agda/issues/5469): `onlyReduceDefs` should not prevent evaluation of macros-  - [#5470](https://github.com/agda/agda/issues/5470): Internal error when using `REWRITE` in `private` block-  - [#5471](https://github.com/agda/agda/issues/5471): LaTeX backend: italics correction-  - [#5473](https://github.com/agda/agda/issues/5473): agda.sty has no version-  - [#5478](https://github.com/agda/agda/issues/5478): Open goal inside record causes internal error (eta-contraction)-  - [#5481](https://github.com/agda/agda/issues/5481): Pattern-matching on records in Prop allows eliminating into Set-  - [#5489](https://github.com/agda/agda/issues/5489): C-c C-x C-a (abort) does not communicate well-  - [#5490](https://github.com/agda/agda/issues/5490): Why does abort (C-c C-x C-a) remove highlighting from the buffer?-  - [#5506](https://github.com/agda/agda/issues/5506): Agda panic: Pattern match failure-  - [#5508](https://github.com/agda/agda/issues/5508): Internal error typechecking non-terminating function on case-insensitive filesystem-  - [#5514](https://github.com/agda/agda/issues/5514): Support GHC 8.10.6-  - [#5531](https://github.com/agda/agda/issues/5531): Internal bug: TypeChecking/Sort-  - [#5532](https://github.com/agda/agda/issues/5532): "The module was successfully compiled" should mention with which backend-  - [#5539](https://github.com/agda/agda/issues/5539): Support GHC 8.10.7-  - [#5544](https://github.com/agda/agda/issues/5544): Internal error caused by addition of `Checkpoints` to `OpenThing`-  - [#5557](https://github.com/agda/agda/issues/5557): Allow Agda to output data files-  - [#5565](https://github.com/agda/agda/issues/5565): Internal error in Agda.TypeChecking.MetaVars-  - [#5593](https://github.com/agda/agda/issues/5593): Compilation failure with `aeson-2`-  - [#5602](https://github.com/agda/agda/issues/5602): The JS backend does not reduce constructor type signatures-  - [#5610](https://github.com/agda/agda/issues/5610): Panic when checking pragma BUILTIN SHARP-  - [#5620](https://github.com/agda/agda/issues/5620): Seemingly incorrect warning for abstract definition without type signature-  - [#5633](https://github.com/agda/agda/issues/5633): Case splitting inserts one with pattern too much (regression in 2.6.2)-  - [#5657](https://github.com/agda/agda/issues/5657): Internal error with postfix projection+* Better caching of interfaces+  (issue [#2767](https://github.com/agda/agda/issues/2767)).++* Various performance improvements concerning meta-variables:+  issue [#5388](https://github.com/agda/agda/issues/5388)+  and PR [#5733](https://github.com/agda/agda/pull/5733).

@@ -1,4 +1,4 @@-Copyright (c) 2005-2021 remains with the authors.+Copyright (c) 2005-2022 remains with the authors. Agda 2 was originally written by Ulf Norell, partially based on code from Agda 1 by Catarina Coquand and Makoto Takeyama, and from Agdalight by Ulf Norell and Andreas Abel.

@@ -0,0 +1,149 @@+Release notes for Agda version 2.6.2.1+======================================++Highlights+----------++* Agda 2.6.2.1 catches up to changes in the Haskell ecosystem+  (GHC 9.2.1, `aeson-2.0`, `hashable-1.4.`).++* Fixes some regressions introduced in 2.6.1:+  [#5283](https://github.com/agda/agda/issues/5283)+  [#5506](https://github.com/agda/agda/issues/5506)+  [#5610](https://github.com/agda/agda/issues/5610)++* Fixes some regressions introduced in 2.6.2:+  [#5508](https://github.com/agda/agda/issues/5508)+  [#5544](https://github.com/agda/agda/issues/5544)+  [#5565](https://github.com/agda/agda/issues/5565)+  [#5584](https://github.com/agda/agda/issues/5584)+  [#5620](https://github.com/agda/agda/issues/5620)+  [#5638](https://github.com/agda/agda/issues/5638)+  [#5657](https://github.com/agda/agda/issues/5657)++* Improvements to the compiler backends (see below).++* Feature preview: `--ghc-strict`.++Installation and infrastructure+-------------------------------++Agda 2.6.2.1 is expected to build with GHC versions 8.0 to 9.2.+It has been tested with the latest minor version releases of GHC for+each of these major versions:++  - 8.0.2+  - 8.2.2+  - 8.4.4+  - 8.6.5+  - 8.8.4+  - 8.10.7: Issue [#5539](https://github.com/agda/agda/issues/5539).+  - 9.0.1+  - 9.2.1:+    Issue [#5442](https://github.com/agda/agda/issues/5442),+    stackage issue [#6318](https://github.com/commercialhaskell/stackage/pull/6318).++Agda 2.6.2.1 has been adapted to recent changes in the Haskell ecosystem, including:++  - `Cabal-3.6.2`+  - `aeson-2.0`:+    Issue [#5593](https://github.com/agda/agda/issues/5593),+    stackage issue [#6217](https://github.com/commercialhaskell/stackage/issues/6217).+  - `hashable-1.4`:+    Stackage issue [#6268](https://github.com/commercialhaskell/stackage/issues/6268).+  - `transformers-0.6`++Compiler backends+-----------------++* Both the GHC and JS backends now refuse to compile code that uses+  `--cubical`.++* The new option `--ghc-strict-data`, which is inspired by the GHC+  language extension `StrictData`, makes the GHC backend compile+  inductive data and record constructors to constructors with strict+  arguments.++  This does not apply to certain builtin types—lists, the maybe type,+  and some types related to reflection—and might not apply to types+  with `COMPILE GHC … = data …` pragmas.++  This feature is experimental.++* The new option `--ghc-strict`, which is inspired by the GHC language+  extension `Strict`, makes the GHC backend generate mostly strict+  code.++  Functions might not be strict in unused arguments.++  Function definitions coming from `COMPILE GHC` pragmas are not+  affected.++  This flag implies `--ghc-strict-data`, and the exceptions of that+  flag applies to this flag as well.++  Note that this option requires the use of GHC 9 or later.++  This feature is experimental.++* JS backend now uses the native `BigInt` instead of the+  [biginteger.js](https://github.com/silentmatt/javascript-biginteger).+  Fixes [#4878](https://github.com/agda/agda/issues/4878).++LaTeX backend+-------------++* Files `agda.sty` and `postprocess-latex.pl` are now found in the `latex/`+  subdirectory of the Agda data directory (`agda --print-agda-dir`).++* `agda.sty` is now versioned (printed to the `.log` file by `latex`)+  (see [#5473](https://github.com/agda/agda/issues/5473)).++* Italics correction (inserted by `\textit` e.g. in `\AgdaBound`) now works,+  thanks to moving the `\textcolor` wrapping to the outside in `agda.sty`+  (see [#5471](https://github.com/agda/agda/issues/5471)).++List of closed issues+---------------------++For 2.6.2.1, the following issues were+[closed](https://github.com/agda/agda/issues?q=is%3Aissue+milestone%3A2.6.2.1+is%3Aclosed)+(see [bug tracker](https://github.com/agda/agda/issues)):++  - [#4878](https://github.com/agda/agda/issues/4878): Replace biginteger.js with native BigInt+  - [#5283](https://github.com/agda/agda/issues/5283): Tactic command runs forever+  - [#5291](https://github.com/agda/agda/issues/5291): `match` doesn't work for non-prefix-free cases+  - [#5302](https://github.com/agda/agda/issues/5302): building tests with cabal+  - [#5396](https://github.com/agda/agda/issues/5396): Internal error for rewriting without --confluence-check+  - [#5398](https://github.com/agda/agda/issues/5398): Problem with LaTeX code for multi-line comments with blank lines+  - [#5420](https://github.com/agda/agda/issues/5420): The JS backend generates incorrect code for Agda code that uses reflection+  - [#5421](https://github.com/agda/agda/issues/5421): The GHC backend generates incorrect code for Agda code that uses reflection+  - [#5431](https://github.com/agda/agda/issues/5431): --ghc-strict-data and --ghc-strict+  - [#5433](https://github.com/agda/agda/issues/5433): The JS backend "installs" highlight-hover.js+  - [#5440](https://github.com/agda/agda/issues/5440): (Re)Documenting `catchfilebetweentags` method of building latex files with Agda+  - [#5442](https://github.com/agda/agda/issues/5442): Support GHC 9.2+  - [#5463](https://github.com/agda/agda/issues/5463): Hole in the middle of a record is malformed+  - [#5465](https://github.com/agda/agda/issues/5465): Compilation of Parser.y depends on the locale on Debian too+  - [#5469](https://github.com/agda/agda/issues/5469): `onlyReduceDefs` should not prevent evaluation of macros+  - [#5470](https://github.com/agda/agda/issues/5470): Internal error when using `REWRITE` in `private` block+  - [#5471](https://github.com/agda/agda/issues/5471): LaTeX backend: italics correction+  - [#5473](https://github.com/agda/agda/issues/5473): agda.sty has no version+  - [#5478](https://github.com/agda/agda/issues/5478): Open goal inside record causes internal error (eta-contraction)+  - [#5481](https://github.com/agda/agda/issues/5481): Pattern-matching on records in Prop allows eliminating into Set+  - [#5489](https://github.com/agda/agda/issues/5489): C-c C-x C-a (abort) does not communicate well+  - [#5490](https://github.com/agda/agda/issues/5490): Why does abort (C-c C-x C-a) remove highlighting from the buffer?+  - [#5506](https://github.com/agda/agda/issues/5506): Agda panic: Pattern match failure+  - [#5508](https://github.com/agda/agda/issues/5508): Internal error typechecking non-terminating function on case-insensitive filesystem+  - [#5514](https://github.com/agda/agda/issues/5514): Support GHC 8.10.6+  - [#5531](https://github.com/agda/agda/issues/5531): Internal bug: TypeChecking/Sort+  - [#5532](https://github.com/agda/agda/issues/5532): "The module was successfully compiled" should mention with which backend+  - [#5539](https://github.com/agda/agda/issues/5539): Support GHC 8.10.7+  - [#5544](https://github.com/agda/agda/issues/5544): Internal error caused by addition of `Checkpoints` to `OpenThing`+  - [#5557](https://github.com/agda/agda/issues/5557): Allow Agda to output data files+  - [#5565](https://github.com/agda/agda/issues/5565): Internal error in Agda.TypeChecking.MetaVars+  - [#5593](https://github.com/agda/agda/issues/5593): Compilation failure with `aeson-2`+  - [#5602](https://github.com/agda/agda/issues/5602): The JS backend does not reduce constructor type signatures+  - [#5610](https://github.com/agda/agda/issues/5610): Panic when checking pragma BUILTIN SHARP+  - [#5620](https://github.com/agda/agda/issues/5620): Seemingly incorrect warning for abstract definition without type signature+  - [#5633](https://github.com/agda/agda/issues/5633): Case splitting inserts one with pattern too much (regression in 2.6.2)+  - [#5657](https://github.com/agda/agda/issues/5657): Internal error with postfix projection

@@ -1,3 +1,3 @@-(define-package "agda2-mode" "2.6.2.1"+(define-package "agda2-mode" "2.6.2.2"   "interactive development for Agda, a dependently typed functional programming language"   '((emacs "24.3") (annotation "1.0") (eri "1.0")))

@@ -28,7 +28,7 @@  ;;; Code: -(defvar agda2-version "2.6.2.1"+(defvar agda2-version "2.6.2.2"   "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.6.2.1 Formatting LaTeX generated by Agda]+  [2021/07/14 version 2.6.2.2 Formatting LaTeX generated by Agda]  \RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,                 calc, environ, xparse, xkeyval}

@@ -1,4 +1,4 @@-{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness+{-# OPTIONS --erased-cubical --safe --no-sized-types --no-guardedness             --no-subtyping #-}  module Agda.Builtin.Cubical.HCompU where

@@ -1,4 +1,4 @@-{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness+{-# OPTIONS --erased-cubical --safe --no-sized-types --no-guardedness             --no-subtyping #-}  module Agda.Builtin.Cubical.Id where

@@ -1,4 +1,4 @@-{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness+{-# OPTIONS --erased-cubical --safe --no-sized-types --no-guardedness             --no-subtyping #-}  module Agda.Builtin.Cubical.Path where

@@ -1,4 +1,4 @@-{-# OPTIONS --cubical --safe --no-sized-types --no-guardedness+{-# OPTIONS --erased-cubical --safe --no-sized-types --no-guardedness             --no-subtyping #-}  module Agda.Builtin.Cubical.Sub where

@@ -1,4 +1,4 @@-{-# OPTIONS --cubical --no-subtyping #-}+{-# OPTIONS --erased-cubical --no-subtyping #-}  module Agda.Primitive.Cubical where 

@@ -7,7 +7,9 @@  import Prelude hiding (null) +import Control.Monad          ( filterM, forM, guard, join, when ) import Control.Monad.Except+import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.State  import qualified Data.List as List

@@ -1,6 +1,12 @@  module Agda.Auto.CaseSplit where +import Control.Monad.State as St hiding (lift)+import Control.Monad.Reader as Rd hiding (lift)+import qualified Control.Monad.State as St+import Control.Monad.IO.Class ( MonadIO(..) )++import Data.Function import Data.IORef import Data.Tuple (swap) import Data.List (elemIndex)@@ -8,10 +14,6 @@ import Data.Monoid ((<>), Sum(..)) import qualified Data.Set    as Set import qualified Data.IntMap as IntMap-import Control.Monad.State as St hiding (lift)-import Control.Monad.Reader as Rd hiding (lift)-import qualified Control.Monad.State as St-import Data.Function  import Agda.Syntax.Common (Hiding(..)) import Agda.Auto.NarrowingSearch

@@ -1,7 +1,9 @@  module Agda.Auto.Convert where +import Control.Monad          ( when ) import Control.Monad.Except+import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.State  import Data.Bifunctor (first)

@@ -1,9 +1,12 @@  module Agda.Auto.NarrowingSearch where +import Control.Monad       ( foldM, when )+import Control.Monad.State ( MonadState(..), modify, StateT, evalStateT, runStateT )+import Control.Monad.Trans ( lift )+ import Data.IORef hiding (writeIORef, modifyIORef) import qualified Data.IORef as NoUndo (writeIORef, modifyIORef)-import Control.Monad.State  import Agda.Utils.Impossible import Agda.Utils.Empty

@@ -22,7 +22,8 @@   ) where  import Control.DeepSeq-import Control.Monad.State+import Control.Monad              ( (<=<) )+import Control.Monad.Trans        ( lift ) import Control.Monad.Trans.Maybe  import qualified Data.List as List

@@ -32,10 +32,13 @@      -- ^ The path to the compiler   -> [String]      -- ^ Command-line arguments.+  -> Maybe TextEncoding+     -- ^ Use the given text encoding, if any, when reading the output+     -- from the process (stdout and stderr).   -> TCM ()-callCompiler doCall cmd args =+callCompiler doCall cmd args enc =   if doCall then do-    merrors <- callCompiler' cmd args+    merrors <- callCompiler' cmd args enc     case merrors of       Nothing     -> return ()       Just errors -> typeError (CompilationError errors)@@ -49,8 +52,11 @@      -- ^ The path to the compiler   -> [String]      -- ^ Command-line arguments.+  -> Maybe TextEncoding+     -- ^ Use the given text encoding, if any, when reading the output+     -- from the process (stdout and stderr).   -> TCM (Maybe String)-callCompiler' cmd args = do+callCompiler' cmd args enc = do   reportSLn "compile.cmd" 1 $ "Calling: " ++ unwords (cmd : args)   (_, out, err, p) <-     liftIO $ createProcess@@ -65,6 +71,9 @@     Just out -> forkTCM $ do       -- The handle should be in text mode.       liftIO $ hSetBinaryMode out False+      case enc of+        Nothing  -> return ()+        Just enc -> liftIO $ hSetEncoding out enc       progressInfo <- liftIO $ hGetContents out       mapM_ (reportSLn "compile.output" 1) $ lines progressInfo @@ -73,6 +82,9 @@     Just err -> do       -- The handle should be in text mode.       hSetBinaryMode err False+      case enc of+        Nothing  -> return ()+        Just enc -> liftIO $ hSetEncoding err enc       hGetContents err    exitcode <- liftIO $ do

@@ -3,9 +3,12 @@  import Control.Arrow (second) import Control.DeepSeq-import Control.Monad.Except (throwError)-import Control.Monad.Reader-import Control.Monad.Writer hiding ((<>))+import Control.Monad+import Control.Monad.Except   ( throwError )+import Control.Monad.IO.Class ( MonadIO(..) )+import Control.Monad.Reader   ( MonadReader(..), asks, ReaderT, runReaderT, withReaderT)+import Control.Monad.Trans    ( lift )+import Control.Monad.Writer   ( MonadWriter(..), WriterT, runWriterT )  import qualified Data.HashSet as HashSet import qualified Data.List as List@@ -24,7 +27,9 @@ import qualified Agda.Utils.Haskell.Syntax as HS  import System.Directory (createDirectoryIfMissing)+import System.Environment (setEnv) import System.FilePath hiding (normalise)+import System.IO (utf8)  import Agda.Compiler.CallCompiler import Agda.Compiler.Common@@ -68,6 +73,7 @@ import Agda.Utils.Maybe import Agda.Utils.Monad import Agda.Utils.Pretty (prettyShow, render)+import Agda.Utils.Singleton import qualified Agda.Utils.IO.UTF8 as UTF8 import Agda.Utils.String @@ -1207,7 +1213,16 @@   -- Note that GHC assumes that sources use ASCII or UTF-8.   out <- snd <$> outFileAndDir m   strict <- optGhcStrict <$> askGhcOpts-  let p = HS.LanguagePragma $ List.map HS.Ident $+  let languagePragmas =+        List.map (HS.LanguagePragma . singleton . HS.Ident) $+          List.sort $+            [ "QualifiedDo" | strict ] +++                -- If --ghc-strict is used, then the language extension+                -- QualifiedDo is activated. At the time of writing no+                -- code is generated that depends on this extension+                -- (except for the pragmas), but --ghc-strict is broken+                -- with at least some versions of GHC prior to version 9,+                -- and QualifiedDo was introduced with GHC 9.             [ "BangPatterns"             , "EmptyDataDecls"             , "EmptyCase"@@ -1217,22 +1232,23 @@             , "RankNTypes"             , "PatternSynonyms"             , "OverloadedStrings"-            ] ++-            -- If --ghc-strict is used, then the language extension-            -- QualifiedDo is activated. At the time of writing no-            -- code is generated that depends on this extension-            -- (except for the pragmas), but --ghc-strict is broken-            -- with at least some versions of GHC prior to version 9,-            -- and QualifiedDo was introduced with GHC 9.-            if strict-            then ["QualifiedDo"]-            else []+            ]+  let ghcOptions =+        List.map HS.OtherPragma+          [ ""  -- to separate from LANGUAGE pragmas+          , "{-# OPTIONS_GHC -Wno-overlapping-patterns #-}"+              -- Andreas, 2022-01-26, issue #5758:+              -- Place this in generated file rather than+              -- passing it only when calling GHC from within Agda.+              -- This will silence the warning for the Agda-generated .hs+              -- files while it can be on for other .hs files in the same+              -- project.  (E.g., when using cabal/stack to compile.)+          ]   liftIO $ UTF8.writeFile out $ (++ "\n") $ prettyPrint $     -- TODO: It might make sense to skip bang patterns for the unused     -- arguments of the "non-stripped" functions.-    (if strict then makeStrict else id) $-    HS.Module m (p : ps) imp ds-  where+    applyWhen strict makeStrict $+    HS.Module m (concat [languagePragmas, ghcOptions, ps]) imp ds  outFileAndDir :: MonadGHCIO m => HS.ModuleName -> m (FilePath, FilePath) outFileAndDir m = do@@ -1257,9 +1273,7 @@   opts    <- askGhcOpts   hsmod   <- prettyPrint <$> curHsMod   agdaMod <- curAgdaMod-  let outputName = case mnameToList agdaMod of-        [] -> __IMPOSSIBLE__-        m:ms -> last1 m ms+  let outputName = lastWithDefault __IMPOSSIBLE__ $ mnameToList agdaMod   (mdir, fp) <- curOutFileAndDir   let ghcopts = optGhcFlags opts @@ -1282,14 +1296,15 @@         [ fp         , "--make"         , "-fwarn-incomplete-patterns"-        , "-fno-warn-overlapping-patterns"         ]       args     = overridableArgs ++ ghcopts ++ otherArgs    let ghcBin = optGhcBin opts +  -- Make GHC use UTF-8 when writing to stdout and stderr.+  liftIO $ setEnv "GHC_CHARENC" "UTF-8"   -- Note: Some versions of GHC use stderr for progress reports. For   -- those versions of GHC we don't print any progress information   -- unless an error is encountered.   let doCall = optGhcCallGhc opts-  liftTCM $ callCompiler doCall ghcBin args+  liftTCM $ callCompiler doCall ghcBin args (Just utf8)

@@ -17,12 +17,15 @@  instance Pretty HS.Module where   pretty (HS.Module m pragmas imps decls) =-    vcat [ vcat $ map pretty pragmas-         , "module" <+> pretty m <+> "where"-         , ""-         , vcat $ map pretty imps-         , ""-         , vcat $ map pretty decls ]+    vcat $ concat+      [ map pretty pragmas+      , [ "" | not $ null pragmas ]+      , [ "module" <+> pretty m <+> "where" ]+      , [ "" ]+      , map pretty imps+      , [ "" ]+      , map pretty decls+      ]  instance Pretty HS.ModulePragma where   pretty (HS.LanguagePragma ps) =

@@ -4,8 +4,10 @@   , closedTermToTreeless   ) where -import Control.Arrow (first)-import Control.Monad.Reader+import Control.Arrow        ( first )+import Control.Monad        ( filterM, foldM, forM, zipWithM )+import Control.Monad.Reader ( MonadReader(..), asks, ReaderT, runReaderT )+import Control.Monad.Trans  ( lift )  import Data.Maybe import Data.Map (Map)@@ -479,6 +481,7 @@ recConFromProj :: QName -> TCM I.ConHead recConFromProj q = do   caseMaybeM (isProjection q) __IMPOSSIBLE__ $ \ proj -> do+    -- Get the record type name @d@ from the projection.     let d = unArg $ projFromType proj     getRecordConstructor d 

@@ -1,7 +1,8 @@ module Agda.Compiler.Treeless.Simplify (simplifyTTerm) where -import Control.Arrow (second, (***))-import Control.Monad.Reader+import Control.Arrow        ( (***), second )+import Control.Monad        ( (>=>), guard )+import Control.Monad.Reader ( MonadReader(..), asks, Reader, runReader ) import qualified Data.List as List  import Agda.Syntax.Treeless

@@ -2,7 +2,11 @@     ( repl     ) where -import Control.Monad.State+import Control.Monad                ( unless )+import Control.Monad.IO.Class       ( MonadIO(..) )+import Control.Monad.State          ( evalStateT, runStateT )+import Control.Monad.Trans          ( lift )+ import Data.Char import Data.Maybe import System.IO

@@ -5,6 +5,8 @@  import           Control.Concurrent.STM.TChan import           Control.Concurrent.STM.TVar++import           Control.Monad                ( mplus, liftM2, liftM4 ) import           Control.Monad.Except import           Control.Monad.Identity import           Control.Monad.State

@@ -6,7 +6,8 @@  import Prelude hiding (null) -import Control.Arrow (first)+import Control.Arrow          ( first )+import Control.Monad          ( (>=>), forM, guard ) import Control.Monad.Except import Control.Monad.Reader import Control.Monad.State@@ -112,63 +113,61 @@     withMetaInfo mi $       concreteToAbstract (clScope mi) e -giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM ()--- When translator from internal to abstract is given, this function might return--- the expression returned by the type checker.+-- Type check the given expression and assign its value to the meta+-- Precondition: we are in the context where the given meta was created.+giveExpr :: UseForce -> Maybe InteractionId -> MetaId -> Expr -> TCM Term giveExpr force mii mi e = do     mv <- lookupMeta mi-    -- In the context (incl. signature) of the meta variable,-    -- type check expression and assign meta-    withMetaInfo (getMetaInfo mv) $ do-      let t = case mvJudgement mv of-                IsSort{}    -> __IMPOSSIBLE__-                HasType _ _ t -> t-      reportSDoc "interaction.give" 20 $-        "give: meta type =" TP.<+> prettyTCM t-      -- Here, we must be in the same context where the meta was created.-      -- Thus, we can safely apply its type to the context variables.-      ctx <- getContextArgs-      t' <- t `piApplyM` permute (takeP (length ctx) $ mvPermutation mv) ctx-      traceCall (CheckExprCall CmpLeq e t') $ do-        reportSDoc "interaction.give" 20 $ do-          a <- asksTC envAbstractMode-          TP.hsep-            [ TP.text ("give(" ++ show a ++ "): instantiated meta type =")-            , prettyTCM t'-            ]-        -- Andreas, 2020-05-27 AIM XXXII, issue #4679-        -- Clear envMutualBlock since cubical only executes-        -- certain checks (checkIApplyConfluence) for an extended lambda-        -- when not in a mutual block.-        v <- locallyTC eMutualBlock (const Nothing) $-          checkExpr e t'-        case mvInstantiation mv of+    let t = case mvJudgement mv of+              IsSort{}    -> __IMPOSSIBLE__+              HasType _ _ t -> t+    reportSDoc "interaction.give" 20 $+      "give: meta type =" TP.<+> prettyTCM t+    -- Here, we must be in the same context where the meta was created.+    -- Thus, we can safely apply its type to the context variables.+    ctx <- getContextArgs+    t' <- t `piApplyM` permute (takeP (length ctx) $ mvPermutation mv) ctx+    traceCall (CheckExprCall CmpLeq e t') $ do+      reportSDoc "interaction.give" 20 $ do+        a <- asksTC envAbstractMode+        TP.hsep+          [ TP.text ("give(" ++ show a ++ "): instantiated meta type =")+          , prettyTCM t'+          ]+      -- Andreas, 2020-05-27 AIM XXXII, issue #4679+      -- Clear envMutualBlock since cubical only executes+      -- certain checks (checkIApplyConfluence) for an extended lambda+      -- when not in a mutual block.+      v <- locallyTC eMutualBlock (const Nothing) $+        checkExpr e t'+      case mvInstantiation mv of -          InstV{} -> unlessM ((Irrelevant ==) <$> asksTC getRelevance) $ do-            v' <- instantiate $ MetaV mi $ map Apply ctx-            reportSDoc "interaction.give" 20 $ TP.sep-              [ "meta was already set to value v' = " TP.<+> prettyTCM v'-              , "now comparing it to given value v = " TP.<+> prettyTCM v-              , "in context " TP.<+> inTopContext (prettyTCM ctx)-              ]-            equalTerm t' v v'+        InstV{} -> unlessM ((Irrelevant ==) <$> asksTC getRelevance) $ do+          v' <- instantiate $ MetaV mi $ map Apply ctx+          reportSDoc "interaction.give" 20 $ TP.sep+            [ "meta was already set to value v' = " TP.<+> prettyTCM v'+            , "now comparing it to given value v = " TP.<+> prettyTCM v+            , "in context " TP.<+> inTopContext (prettyTCM ctx)+            ]+          equalTerm t' v v' -          _ -> do -- updateMeta mi v-            reportSLn "interaction.give" 20 "give: meta unassigned, assigning..."-            args <- getContextArgs-            nowSolvingConstraints $ assign DirEq mi args v (AsTermsOf t')+        _ -> do -- updateMeta mi v+          reportSLn "interaction.give" 20 "give: meta unassigned, assigning..."+          args <- getContextArgs+          nowSolvingConstraints $ assign DirEq mi args v (AsTermsOf t') -        reportSDoc "interaction.give" 20 $ "give: meta variable updated!"-        unless (force == WithForce) $ redoChecks mii-        wakeupConstraints mi-        solveSizeConstraints DontDefaultToInfty-        cubical <- isJust . optCubical <$> pragmaOptions-        -- don't double check with cubical, because it gets in the way too often.-        unless (cubical || force == WithForce) $ do-          -- Double check.-          reportSDoc "interaction.give" 20 $ "give: double checking"-          vfull <- instantiateFull v-          checkInternal vfull CmpLeq t'+      reportSDoc "interaction.give" 20 $ "give: meta variable updated!"+      unless (force == WithForce) $ redoChecks mii+      wakeupConstraints mi+      solveSizeConstraints DontDefaultToInfty+      cubical <- isJust . optCubical <$> pragmaOptions+      -- don't double check with cubical, because it gets in the way too often.+      unless (cubical || force == WithForce) $ do+        -- Double check.+        reportSDoc "interaction.give" 20 $ "give: double checking"+        vfull <- instantiateFull v+        checkInternal vfull CmpLeq t'+      return v  -- | After a give, redo termination etc. checks for function which was complemented. redoChecks :: Maybe InteractionId -> TCM ()@@ -202,7 +201,8 @@   reportSDoc "interaction.give" 10 $ "giving expression" TP.<+> prettyTCM e   reportSDoc "interaction.give" 50 $ TP.text $ show $ deepUnscope e   -- Try to give mi := e-  do setMetaOccursCheck mi DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions.+  _ <- withInteractionId ii $ do+     setMetaOccursCheck mi DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions.      giveExpr force (Just ii) mi e     `catchError` \ case       -- Turn PatternErr into proper error:@@ -212,6 +212,32 @@   removeInteractionPoint ii   return e +-- | Try to fill hole by elaborated expression.+elaborate_give+  :: Rewrite        -- ^ Normalise result?+  -> UseForce       -- ^ Skip safety checks?+  -> InteractionId  -- ^ Hole.+  -> Maybe Range+  -> Expr           -- ^ The expression to give.+  -> TCM Expr       -- ^ If successful, return the elaborated expression.+elaborate_give norm force ii mr e = withInteractionId ii $ do+  -- if Range is given, update the range of the interaction meta+  mi  <- lookupInteractionId ii+  whenJust mr $ updateMetaVarRange mi+  reportSDoc "interaction.give" 10 $ "giving expression" TP.<+> prettyTCM e+  reportSDoc "interaction.give" 50 $ TP.text $ show $ deepUnscope e+  -- Try to give mi := e+  v <- withInteractionId ii $ do+     setMetaOccursCheck mi DontRunMetaOccursCheck -- #589, #2710: Allow giving recursive solutions.+     locallyTC eCurrentlyElaborating (const True) $+       giveExpr force (Just ii) mi e+    `catchError` \ case+      -- Turn PatternErr into proper error:+      PatternErr{} -> typeError . GenericDocError =<< do+        withInteractionId ii $ "Failed to give" TP.<+> prettyTCM e+      err -> throwError err+  nv <- normalForm norm v+  locallyTC ePrintMetasBare (const True) $ reify nv  -- | Try to refine hole by expression @e@. --@@ -454,6 +480,7 @@     reify (CheckMetaInst m) = do       t <- jMetaType . mvJudgement <$> lookupMeta m       OfType <$> reify (MetaV m []) <*> reify t+    reify (CheckType t) = JustType <$> reify t     reify (UsableAtModality mod t) = UsableAtMod mod <$> reify t  instance (Pretty a, Pretty b) => Pretty (OutputForm a b) where@@ -618,6 +645,7 @@         HasPTSRule a b             -> Nothing         UnquoteTactic{}            -> Nothing         CheckMetaInst{}            -> Nothing+        CheckType t                -> isMeta (unEl t)         CheckLockedVars t _ _ _    -> isMeta t         UsableAtModality _ t       -> isMeta t @@ -1002,16 +1030,6 @@         mi <- getMetaInfo <$> lookupMeta m         withMetaInfo mi $             typeInCurrent norm e--withInteractionId :: InteractionId -> TCM a -> TCM a-withInteractionId i ret = do-  m <- lookupInteractionId i-  withMetaId m ret--withMetaId :: MetaId -> TCM a -> TCM a-withMetaId m ret = do-  mv <- lookupMeta m-  withMetaInfo' mv ret  -- | The intro tactic. --

@@ -3,7 +3,9 @@   ( runInteractionLoop   ) where +import Control.Monad import Control.Monad.Except+import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.State import Control.Monad.Reader 

@@ -7,7 +7,11 @@     , prettyTypeOfMeta     ) where -import Control.Monad.State hiding (state)+import Control.Monad+import Control.Monad.IO.Class ( MonadIO(..) )+import Control.Monad.State    ( evalStateT )+import Control.Monad.Trans    ( lift )+ import qualified Data.List as List  import Agda.Syntax.Common@@ -194,7 +198,7 @@     Info_GoalSpecific ii kind -> lispifyGoalSpecificDisplayInfo ii kind  lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM [Lisp String]-lispifyGoalSpecificDisplayInfo ii kind = localTCState $ B.withInteractionId ii $+lispifyGoalSpecificDisplayInfo ii kind = localTCState $ withInteractionId ii $   case kind of     Goal_HelperFunction helperType -> do       doc <- inTopContext $ prettyATop helperType

@@ -39,7 +39,8 @@ import Agda.TypeChecking.Monad.Base import Agda.TypeChecking.Monad.Benchmark (billTo) import qualified Agda.TypeChecking.Monad.Benchmark as Bench-import Agda.TypeChecking.Monad.Options (getIncludeDirs, libToTCM)+import {-# SOURCE #-} Agda.TypeChecking.Monad.Options+  (getIncludeDirs, libToTCM) import Agda.TypeChecking.Warnings (runPM)  import Agda.Version ( version )

@@ -10,12 +10,13 @@   )  import Control.Monad.Except-  ( MonadIO-  , ExceptT+  ( ExceptT   , runExceptT   , MonadError(throwError)   )-+import Control.Monad.IO.Class+  ( MonadIO(..)+  ) import Control.DeepSeq  import Data.Map ( Map )

@@ -9,8 +9,10 @@   , Env(..)   ) where -import Control.Monad.Reader-import Control.Monad.State+import Control.Monad          (liftM2, when)+import Control.Monad.IO.Class (MonadIO(..))+import Control.Monad.Reader   (ReaderT, runReaderT, ask)+import Control.Monad.State    (State, execState, get, modify, put)  import qualified Data.Map as M import Data.Map(Map)

@@ -13,7 +13,8 @@ import Prelude hiding (null)  import Control.Applicative-import Control.Monad.Reader+import Control.Monad         ( (<=<) )+import Control.Monad.Reader  ( MonadReader(..), asks, Reader, runReader )  import qualified Data.Map      as Map import           Data.Maybe

@@ -29,10 +29,13 @@ import Control.Monad (forM_, mapM_, unless, when) import Control.Monad.Trans.Reader as R ( ReaderT(runReaderT)) import Control.Monad.RWS.Strict-  ( MonadIO(..), RWST(runRWST)+  ( RWST(runRWST)   , MonadReader(..), asks   , MonadState(..), gets, modify   , lift, tell+  )+import Control.Monad.IO.Class+  ( MonadIO(..)   )  import System.Directory

@@ -24,7 +24,9 @@  import Prelude hiding (null) +import Control.Monad               ( forM, forM_, void ) import Control.Monad.Except+import Control.Monad.IO.Class      ( MonadIO(..) ) import Control.Monad.State import Control.Monad.Trans.Maybe import qualified Control.Exception as E@@ -1194,7 +1196,9 @@     let builtin' = Map.mapWithKey (\ x b -> (x,) . primFunName <$> b) builtin     warnings <- getAllWarnings AllWarnings     reportSLn "import.iface" 7 "  instantiating all meta variables"-    i <- instantiateFull Interface+    -- Note that the meta-variables in the definitions in "sig" have+    -- already been instantiated (by eliminateDeadCode).+    i <- instantiateFullExceptForDefinitions Interface       { iSourceHash      = hashText source       , iSource          = source       , iFileType        = fileType

@@ -13,12 +13,16 @@ import Control.Concurrent.Async import Control.Concurrent.STM.TChan import Control.Concurrent.STM.TVar-import qualified Control.Exception as E-import Control.Monad.Except-import Control.Monad.Identity-import Control.Monad.Reader-import Control.Monad.State hiding (state)++import qualified Control.Exception  as E++import Control.Monad+import Control.Monad.Except         ( MonadError(..), ExceptT(..), runExceptT )+import Control.Monad.IO.Class       ( MonadIO(..) )+import Control.Monad.Fail           ( MonadFail )+import Control.Monad.State          ( MonadState(..), gets, modify, runStateT ) import Control.Monad.STM+import Control.Monad.Trans          ( lift )  import qualified Data.Char as Char import Data.Function@@ -662,7 +666,7 @@  interpret (Cmd_intro pmLambda ii rng _) = do   ss <- lift $ B.introTactic pmLambda ii-  liftCommandMT (B.withInteractionId ii) $ case ss of+  liftCommandMT (withInteractionId ii) $ case ss of     []    -> do       display_info $ Info_Intro_NotFound     [s]   -> give_gen WithoutForce ii rng s Intro@@ -728,27 +732,18 @@  interpret (Cmd_helper_function norm ii rng s) = do   -- Create type of application of new helper function that would solve the goal.-  helperType <- liftLocalState $ B.withInteractionId ii $ inTopContext $ B.metaHelperType norm ii rng s+  helperType <- liftLocalState $ withInteractionId ii $ inTopContext $ B.metaHelperType norm ii rng s   display_info $ Info_GoalSpecific ii (Goal_HelperFunction helperType)  interpret (Cmd_infer norm ii rng s) = do-  expr <- liftLocalState $ B.withInteractionId ii $ B.typeInMeta ii norm =<< B.parseExprIn ii rng s+  expr <- liftLocalState $ withInteractionId ii $ B.typeInMeta ii norm =<< B.parseExprIn ii rng s   display_info $ Info_GoalSpecific ii (Goal_InferredType expr)  interpret (Cmd_goal_type norm ii _ _) =   display_info $ Info_GoalSpecific ii (Goal_CurrentGoal norm) -interpret (Cmd_elaborate_give norm ii rng s) = do-  have <- liftLocalState $ B.withInteractionId ii $ do-    expr <- B.parseExprIn ii rng s-    goal <- B.typeOfMeta AsIs ii-    term <- case goal of-      OfType _ ty -> checkExpr expr =<< isType_ ty-      _           -> __IMPOSSIBLE__-    nf <- B.normalForm norm term-    txt <- localTC (\ e -> e { envPrintMetasBare = True }) (TCP.prettyTCM nf)-    return $ show txt-  give_gen WithoutForce ii rng have ElaborateGive+interpret (Cmd_elaborate_give norm ii rng s) =+  give_gen WithoutForce ii rng s $ ElaborateGive norm  interpret (Cmd_goal_type_context norm ii rng s) =   cmd_goal_type_context_and GoalOnly norm ii rng s@@ -761,13 +756,13 @@             then return GoalOnly             else do               typ <- liftLocalState-                    $ B.withInteractionId ii+                    $ withInteractionId ii                     $ B.typeInMeta ii norm =<< B.parseExprIn ii rng s               return (GoalAndHave typ)   cmd_goal_type_context_and aux norm ii rng s  interpret (Cmd_goal_type_context_check norm ii rng s) = do-  term <- liftLocalState $ B.withInteractionId ii $ do+  term <- liftLocalState $ withInteractionId ii $ do     expr <- B.parseExprIn ii rng s     goal <- B.typeOfMeta AsIs ii     term <- case goal of@@ -777,17 +772,17 @@   cmd_goal_type_context_and (GoalAndElaboration term) norm ii rng s  interpret (Cmd_show_module_contents norm ii rng s) =-  liftCommandMT (B.withInteractionId ii) $ showModuleContents norm rng s+  liftCommandMT (withInteractionId ii) $ showModuleContents norm rng s  interpret (Cmd_why_in_scope_toplevel s) =   atTopLevel $ whyInScope s  interpret (Cmd_why_in_scope ii _range s) =-  liftCommandMT (B.withInteractionId ii) $ whyInScope s+  liftCommandMT (withInteractionId ii) $ whyInScope s  interpret (Cmd_make_case ii rng s) = do   (f, casectxt, cs) <- lift $ makeCase ii rng s-  liftCommandMT (B.withInteractionId ii) $ do+  liftCommandMT (withInteractionId ii) $ do     tel <- lift $ lookupSection (qnameModule f) -- don't shadow the names in this telescope     unicode <- getsTC $ optUseUnicode . getPragmaOptions     pcs      :: [Doc]      <- lift $ inTopContext $ addContext tel $ mapM prettyA cs@@ -830,7 +825,7 @@ interpret (Cmd_compute cmode ii rng s) = do   expr <- liftLocalState $ do     e <- B.parseExprIn ii rng $ B.computeWrapInput cmode s-    B.withInteractionId ii $ applyWhen (B.computeIgnoreAbstract cmode) ignoreAbstractMode $ B.evalInCurrent cmode e+    withInteractionId ii $ applyWhen (B.computeIgnoreAbstract cmode) ignoreAbstractMode $ B.evalInCurrent cmode e   display_info $ Info_GoalSpecific ii (Goal_NormalForm cmode expr)  interpret Cmd_show_version = display_info Info_Version@@ -950,7 +945,7 @@ --------------------------------------------------------------------------- -- Giving, refining. -data GiveRefine = Give | Refine | Intro | ElaborateGive+data GiveRefine = Give | Refine | Intro | ElaborateGive Rewrite   deriving (Eq, Show)  -- | A "give"-like action (give, refine, etc).@@ -970,28 +965,28 @@   -> CommandM () give_gen force ii rng s0 giveRefine = do   let s = trim s0-  lift $ reportSLn "interaction.give" 20 $ "give_gen  " ++ s+  reportSLn "interaction.give" 20 $ "give_gen  " ++ s   -- Andreas, 2015-02-26 if string is empty do nothing rather   -- than giving a parse error.   unless (null s) $ do     let give_ref =           case giveRefine of-            Give          -> B.give-            Refine        -> B.refine-            Intro         -> B.refine-            ElaborateGive -> B.give+            Give               -> B.give+            Refine             -> B.refine+            Intro              -> B.refine+            ElaborateGive norm -> B.elaborate_give norm     -- save scope of the interaction point (for printing the given expr. later)-    scope     <- lift $ getInteractionScope ii+    scope     <- getInteractionScope ii     -- parse string and "give", obtaining an abstract expression     -- and newly created interaction points-    (time, (ae, ae0, iis)) <- maybeTimed $ lift $ do+    (time, (ae, ae0, iis)) <- maybeTimed $ do         -- Issue 3000: mark the current hole as solved before giving, to avoid confusing it with potential         -- new interaction points introduced by the give.         removeInteractionPoint ii         mis  <- getInteractionPoints         reportSLn "interaction.give" 30 $ "interaction points before = " ++ show mis-        given <- B.parseExprIn ii rng s-        ae    <- give_ref force ii Nothing given+        given <- lift $ B.parseExprIn ii rng s+        ae    <- lift $ give_ref force ii Nothing given         mis' <- getInteractionPoints         reportSLn "interaction.give" 30 $ "interaction points after = " ++ show mis'         return (ae, given, mis' List.\\ mis)@@ -999,11 +994,11 @@     insertOldInteractionScope ii scope     -- sort the new interaction points and put them into the state     -- in replacement of the old interaction point-    iis' <- lift $ sortInteractionPoints iis+    iis' <- sortInteractionPoints iis     modifyTheInteractionPoints $ replace ii iis'     -- print abstract expr-    ce        <- lift $ abstractToConcreteScope scope ae-    lift $ reportS "interaction.give" 30+    ce        <- abstractToConcreteScope scope ae+    reportS "interaction.give" 30       [ "ce = " ++ show ce       , "scopePrecedence = " ++ show (scope ^. scopePrecedence)       ]@@ -1016,22 +1011,22 @@     -- WRONG: let literally = (giveRefine == Give || null iis) && rng /= noRange     -- Ulf, 2015-03-30, if we're doing intro we can't do literal give since     -- there is nothing in the hole (issue 1892).-    let literally = giveRefine /= Intro && giveRefine /= ElaborateGive && ae == ae0 && rng /= noRange+    let literally = (giveRefine == Give || giveRefine == Refine) && ae == ae0 && rng /= noRange     -- Ulf, 2014-01-24: This works for give since we're highlighting the string     -- that's already in the buffer. Doing it before the give action means that     -- the highlighting is moved together with the text when the hole goes away.     -- To make it work for refine we'd have to adjust the ranges.-    when literally $ lift $ do+    when literally $ do       l <- asksTC envHighlightingLevel-      when (l /= None) $ do+      when (l /= None) $ lift $ do         printHighlightingInfo KeepHighlighting =<<           generateTokenInfoFromString rng s         highlightExpr ae     putResponse $ Resp_GiveAction ii $ mkNewTxt literally ce-    lift $ reportSLn "interaction.give" 30 $ "putResponse GiveAction passed"+    reportSLn "interaction.give" 30 $ "putResponse GiveAction passed"     -- display new goal set (if not measuring time)     maybe (interpret $ Cmd_metas AsIs) (display_info . Info_Time) time-    lift $ reportSLn "interaction.give" 30 $ "interpret Cmd_metas passed"+    reportSLn "interaction.give" 30 $ "interpret Cmd_metas passed"   where     -- Substitutes xs for x in ys.     replace x xs ys = concatMap (\ y -> if y == x then xs else [y]) ys@@ -1054,7 +1049,9 @@  -- | Sorts interaction points based on their ranges. -sortInteractionPoints :: [InteractionId] -> TCM [InteractionId]+sortInteractionPoints+  :: (MonadInteractionPoints m, MonadError TCErr m, MonadFail m)+  => [InteractionId] -> m [InteractionId] sortInteractionPoints is =   map fst . List.sortBy (compare `on` snd) <$> do     forM is $ \ i -> do

@@ -1,8 +1,10 @@ module Agda.Interaction.JSONTop     ( jsonREPL     ) where-import Control.Monad.State +import Control.Monad          ( (<=<), forM )+import Control.Monad.IO.Class ( MonadIO(..) )+ import Data.ByteString.Lazy (ByteString) import qualified Data.ByteString.Lazy.Char8 as BS import qualified Data.Text as T@@ -20,13 +22,13 @@ import Agda.Syntax.Common import qualified Agda.Syntax.Concrete as C import Agda.Syntax.Concrete.Name (NameInScope(..), Name)-import Agda.Syntax.Internal (telToList, Dom'(..), Dom, MetaId(..), ProblemId(..), Blocker(..))-import Agda.Syntax.Position (Range, rangeIntervals, Interval'(..), Position'(..))+import Agda.Syntax.Internal (telToList, Dom'(..), Dom, MetaId(..), ProblemId(..), Blocker(..), alwaysUnblock)+import Agda.Syntax.Position (Range, rangeIntervals, Interval'(..), Position'(..), noRange) import Agda.VersionCommit  import Agda.TypeChecking.Errors (getAllWarningsOfTCErr)-import Agda.TypeChecking.Monad (Comparison(..), inTopContext, TCM, TCErr, TCWarning, NamedMeta(..))-import Agda.TypeChecking.Monad.MetaVars (getInteractionRange, getMetaRange)+import Agda.TypeChecking.Monad (Comparison(..), inTopContext, TCM, TCErr, TCWarning, NamedMeta(..), withInteractionId)+import Agda.TypeChecking.Monad.MetaVars (getInteractionRange, getMetaRange, withMetaId) import Agda.TypeChecking.Pretty (PrettyTCM(..), prettyTCM) -- borrowed from EmacsTop, for temporarily serialising stuff import Agda.TypeChecking.Pretty.Warning (filterTCWarnings)@@ -113,7 +115,7 @@     , "range" #= intervalsTCM     ]     where-      nameTCM = encodeShow <$> B.withMetaId (nmid m) (prettyATop m)+      nameTCM = encodeShow <$> withMetaId (nmid m) (prettyATop m)       intervalsTCM = toJSON <$> getMetaRange (nmid m)  instance EncodeTCM GiveResult where@@ -241,7 +243,7 @@     [ "range"      @= range     , "problems"   @= problems     , "unblocker"  @= unblock-    , "constraint" #= encodeOC (pure . encodeShow) (pure . encodeShow) oc+    , "constraint" #= encodeOC (pure . encodePretty) (pure . encodePretty) oc     ]  instance EncodeTCM Blocker where@@ -260,7 +262,7 @@     [ "constraints"       #= forM constraints encodeTCM     ]   encodeTCM (Info_AllGoalsWarnings (vis, invis) wes) = kind "AllGoalsWarnings"-    [ "visibleGoals"      #= forM vis (encodeOC encodeTCM encodePrettyTCM)+    [ "visibleGoals"      #= forM vis (\i -> withInteractionId (B.outputFormId $ OutputForm noRange [] alwaysUnblock i) $ encodeOC encodeTCM encodePrettyTCM i)     , "invisibleGoals"    #= forM invis (encodeOC encodeTCM encodePrettyTCM)     , "warnings"          #= encodeTCM (filterTCWarnings (tcWarnings wes))     , "errors"            #= encodeTCM (filterTCWarnings (nonFatalErrors wes))@@ -323,7 +325,7 @@     ]   encodeTCM (Info_GoalSpecific ii info) = kind "GoalSpecific"     [ "interactionPoint"  @= ii-    , "goalInfo"          #= encodeGoalSpecific ii info+    , "goalInfo"          #= withInteractionId ii (encodeGoalSpecific ii info)     ]  instance EncodeTCM GoalTypeAux where

@@ -38,10 +38,12 @@   , findLib'   ) where -import Control.Arrow ( first , second )+import Control.Arrow          ( first , second )+import Control.Monad          ( filterM, forM ) import Control.Monad.Except import Control.Monad.State import Control.Monad.Writer+import Control.Monad.IO.Class ( MonadIO(..) )  import Data.Char import Data.Data ( Data )@@ -65,6 +67,7 @@ import Agda.Utils.FileName import Agda.Utils.Functor ( (<&>) ) import Agda.Utils.IO ( catchIO )+import qualified Agda.Utils.IO.UTF8 as UTF8 import Agda.Utils.List import Agda.Utils.List1 ( List1 ) import qualified Agda.Utils.List1 as List1@@ -257,7 +260,7 @@     agdaDir <- liftIO getAgdaAppDir     let file = agdaDir </> defaultsFile     ifNotM (liftIO $ doesFileExist file) (return []) $ {-else-} do-      ls <- liftIO $ map snd . stripCommentLines <$> readFile file+      ls <- liftIO $ map snd . stripCommentLines <$> UTF8.readFile file       return $ concatMap splitCommas ls   `catchIO` \ e -> do     raiseErrors' [ OtherError $ unlines ["Failed to read defaults file.", show e] ]@@ -301,7 +304,7 @@       Left err -> raiseErrors' [OtherError err] >> return []       Right file -> do         if not (lfExists file) then return [] else do-          ls    <- liftIO $ stripCommentLines <$> readFile (lfPath file)+          ls    <- liftIO $ stripCommentLines <$> UTF8.readFile (lfPath file)           files <- liftIO $ sequence [ (i, ) <$> expandEnvironmentVariables s | (i, s) <- ls ]           parseLibFiles (Just file) $ nubOn snd files   `catchIO` \ e -> do@@ -370,7 +373,7 @@ getTrustedExecutables = mkLibM [] $ do     file <- liftIO getExecutablesFile     if not (efExists file) then return Map.empty else do-      es    <- liftIO $ stripCommentLines <$> readFile (efPath file)+      es    <- liftIO $ stripCommentLines <$> UTF8.readFile (efPath file)       files <- liftIO $ sequence [ (i, ) <$> expandEnvironmentVariables s | (i, s) <- es ]       tmp   <- parseExecutablesFile file $ nubOn snd files       return tmp@@ -387,26 +390,12 @@ parseExecutablesFile ef files =   fmap (Map.fromList . catMaybes) . forM files $ \(ln, fp) -> do -    -- Check if the executable exists.-    fpExists <- liftIO $ doesFileExist fp-    if not fpExists-      then do warnings' [ExeNotFound ef fp]-              return Nothing-      else do--      -- Check if the executable is executable.-      fpPerms <- liftIO $ getPermissions fp-      if not (executable fpPerms)-        then do warnings' [ExeNotExecutable ef fp]-                return Nothing-        else do--        -- Compute canonical executable name and absolute filepath.-        let strExeName  = takeFileName fp-        let strExeName' = fromMaybe strExeName $ stripExtension exeExtension strExeName-        let txtExeName  = T.pack strExeName'-        exePath <- liftIO $ makeAbsolute fp-        return $ Just (txtExeName, exePath)+    -- Compute canonical executable name and absolute filepath.+    let strExeName  = takeFileName fp+    let strExeName' = fromMaybe strExeName $ stripExtension exeExtension strExeName+    let txtExeName  = T.pack strExeName'+    exePath <- liftIO $ makeAbsolute fp+    return $ Just (txtExeName, exePath)  ------------------------------------------------------------------------ -- * Resolving library names to include pathes

@@ -7,6 +7,7 @@ import Control.Monad.Except import Control.Monad.State import Control.Monad.Writer+import Control.Monad.IO.Class ( MonadIO(..) )  import Data.Char ( isDigit ) import Data.Data ( Data )@@ -124,18 +125,12 @@ -- | Library Warnings. data LibWarning'   = UnknownField String-  | ExeNotFound ExecutablesFile FilePath-      -- ^ Raised when a trusted executable can not be found.-  | ExeNotExecutable ExecutablesFile FilePath-      -- ^ Raised when a trusted executable does not have the executable permission.   deriving (Show, Data, Generic)  data LibError = LibError (Maybe LibPositionInfo) LibError'  libraryWarningName :: LibWarning -> WarningName libraryWarningName (LibWarning c (UnknownField{})) = LibUnknownField_-libraryWarningName (LibWarning c (ExeNotFound{})) = ExeNotFoundWarning_-libraryWarningName (LibWarning c (ExeNotExecutable{})) = ExeNotExecutableWarning_  -- | Collected errors while processing library files. --@@ -261,8 +256,6 @@  instance Pretty LibWarning' where   pretty (UnknownField s) = text $ "Unknown field '" ++ s ++ "'"-  pretty (ExeNotFound file exe) = text $ "Executable '" ++ exe ++ "' not found."-  pretty (ExeNotExecutable file exe) = text $ "Executable '" ++ exe ++ "' not executable."  ------------------------------------------------------------------------ -- NFData instances

@@ -41,6 +41,7 @@  import Agda.Utils.Applicative import Agda.Utils.IO ( catchIO )+import qualified Agda.Utils.IO.UTF8 as UTF8 import Agda.Utils.Lens import Agda.Utils.List   ( duplicates ) import Agda.Utils.String ( ltrim )@@ -109,7 +110,7 @@ -- parseLibFile :: FilePath -> IO (P AgdaLibFile) parseLibFile file =-  (fmap setPath . parseLib <$> readFile file) `catchIO` \e ->+  (fmap setPath . parseLib <$> UTF8.readFile file) `catchIO` \e ->     return $ throwError $ unlines       [ "Failed to read library file " ++ file ++ "."       , "Reason: " ++ show e

@@ -324,7 +324,7 @@     -- we need to print them postfix.     let postProjInExtLam = applyWhen (isJust casectxt) $           withPragmaOptions $ \ opt -> opt { optPostfixProjections = True }-    (piTel, sc) <- insertTrailingArgs $ clauseToSplitClause clause+    (piTel, sc) <- insertTrailingArgs False $ clauseToSplitClause clause     -- Andreas, 2015-05-05 If we introduced new function arguments     -- do not split on result.  This might be more what the user wants.     -- To split on result, he can then C-c C-c again.

@@ -91,6 +91,7 @@   , optInputFile             :: Maybe FilePath   , optIncludePaths          :: [FilePath]   , optAbsoluteIncludePaths  :: [AbsolutePath]+    -- ^ The list should not contain duplicates.   , optLibraries             :: [LibName]   , optOverrideLibrariesFile :: Maybe FilePath   -- ^ Use this (if Just) instead of .agda/libraries@@ -709,7 +710,6 @@ cubicalFlag   :: Cubical  -- ^ Which variant of Cubical Agda?   -> Flag PragmaOptions-cubicalFlag CErased _ = throwError "--erased-cubical is not available." cubicalFlag variant o = do   let withoutK = optWithoutK o   return $ o { optCubical  = Just variant

@@ -6,7 +6,7 @@  module Agda.Interaction.Options.Lenses where -import Control.Monad.State+import Control.Monad.IO.Class   ( MonadIO(..) )  import Data.Set (Set) import qualified Data.Set as Set

@@ -150,8 +150,6 @@   , RewriteMaybeNonConfluent_   , RewriteAmbiguousRules_   , RewriteMissingRule_-  , ExeNotFoundWarning_-  , ExeNotExecutableWarning_   ]  allWarnings :: Set WarningName@@ -268,9 +266,6 @@   -- Record field warnings   | DuplicateFieldsWarning_   | TooManyFieldsWarning_-  -- System call warnings-  | ExeNotFoundWarning_-  | ExeNotExecutableWarning_   deriving (Eq, Ord, Show, Read, Enum, Bounded, Generic)  instance NFData WarningName@@ -425,6 +420,3 @@   -- Record field warnings   DuplicateFieldsWarning_          -> "Record expression with duplicate field names."   TooManyFieldsWarning_            -> "Record expression with invalid field names."-  -- System call warnings-  ExeNotFoundWarning_              -> "Trusted executable cannot be found."-  ExeNotExecutableWarning_         -> "Trusted executable does not have permission to execute."

@@ -5,7 +5,9 @@  import Prelude hiding (null) -import Control.Monad.Except+import Control.Monad          ( void )+import Control.Monad.Except   ( MonadError(..), ExceptT(..), runExceptT )+import Control.Monad.IO.Class ( MonadIO(..) )  import qualified Data.List as List import Data.Maybe

@@ -7,9 +7,10 @@  import Prelude hiding (null) -import Control.Arrow ((***), second)-import Control.Monad.Identity-import Control.Applicative (liftA2)+import Control.Arrow           ( (***), second )+import Control.Monad           ( (>=>) )+import Control.Monad.Identity  ( Identity(..), runIdentity )+import Control.Applicative     ( liftA2 )   import Data.Maybe

@@ -8,8 +8,9 @@   , mergePatternSynDefs   ) where -import Control.Applicative ( Alternative(empty) )-import Control.Monad.Writer hiding (forM)+import Control.Applicative  ( Alternative(empty) )+import Control.Monad        ( foldM, guard, zipWithM, zipWithM_ )+import Control.Monad.Writer ( MonadWriter(..), WriterT, execWriterT )  import Data.Map (Map) import qualified Data.Map as Map

@@ -54,8 +54,10 @@  import Prelude hiding (null) -import Control.Monad.Except-import Control.Monad.State+import Control.Monad         ( forM, guard, unless, void, when )+import Control.Monad.Except  ( )+import Control.Monad.State   ( MonadState(..), gets, StateT, runStateT )+import Control.Monad.Trans   ( lift )  import Data.Bifunctor import Data.Data (Data)

@@ -1,7 +1,8 @@ module Agda.Syntax.Concrete.Definitions.Monad where -import Control.Monad.Except-import Control.Monad.State+import Control.Monad        ( unless )+import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )+import Control.Monad.State  ( MonadState(..), modify, State, runState )  import Data.Bifunctor (second) import Data.Map (Map)

@@ -5,8 +5,10 @@  import Control.Applicative ( liftA2 ) import Control.Arrow ( first )+import Control.Monad ( (>=>) ) import Control.Monad.Identity-import Control.Monad.Writer++import Data.Monoid ( Any(..), Endo(..), Sum(..) )  import Agda.Syntax.Common import Agda.Syntax.Concrete

@@ -221,7 +221,10 @@             --   The @String@ typically describes the location where we create this dummy,             --   but can contain other information as well.             --   The second field accumulates eliminations in case we-            --   apply a dummy term to more of them.+            --   apply a dummy term to more of them. Dummy terms should never be used in places+            --   where they can affect type checking, so syntactic checks are free to ignore the+            --   eliminators, which are only there to ease debugging when a dummy term incorrectly+            --   leaks into a relevant position.   deriving (Data, Show)  type ConInfo = ConOrigin

@@ -1,8 +1,9 @@  module Agda.Syntax.Internal.Pattern where -import Control.Arrow (second)-import Control.Monad.State+import Control.Arrow       ( second )+import Control.Monad       ( (>=>), forM )+import Control.Monad.State ( MonadState(..), State, evalState )  import Data.Maybe import Data.Monoid

@@ -24,8 +24,10 @@     ) where  import Control.Exception+import Control.Monad          ( forM_ ) import Control.Monad.Except import Control.Monad.State+import Control.Monad.IO.Class ( MonadIO(..) )  import Data.Bifunctor import qualified Data.List as List

@@ -37,9 +37,8 @@  } --- Unicode is not handled by the following regular expressions.--- Instead, unicode characters are translated to 7-bit ASCII--- by Agda.Syntax.Parser.LexActions.foolAlex in a preprocessing pass.+-- Note that the regular expressions should not use non-ASCII+-- characters, see Agda.Syntax.Parser.Alex.alexGetByte.  $digit       = 0-9 $hexdigit    = [ $digit a-f A-F ]

@@ -10,7 +10,6 @@ import Control.Arrow ((***)) import Control.Monad import Control.Monad.Except-import Control.Monad.Writer hiding ((<>)) import Control.Monad.State  import Data.Either ( partitionEithers )@@ -253,6 +252,18 @@   printLocals 10 "bound variables:"   modifyScope_ $ setVarsToBind [] +annotateDecls :: ReadTCState m => m [A.Declaration] -> m A.Declaration+annotateDecls m = do+  ds <- m+  s  <- getScope+  return $ A.ScopedDecl s ds++annotateExpr :: ReadTCState m => m A.Expr -> m A.Expr+annotateExpr m = do+  e <- m+  s <- getScope+  return $ A.ScopedExpr s e+ --------------------------------------------------------------------------- -- * Names ---------------------------------------------------------------------------@@ -387,8 +398,8 @@   fromConcreteSuffix = \case     Nothing              -> Nothing     Just C.Prime{}       -> Nothing-    Just (C.Index i)     -> Just $ A.Suffix $ toInteger i-    Just (C.Subscript i) -> Just $ A.Suffix $ toInteger i+    Just (C.Index i)     -> Just $ A.Suffix i+    Just (C.Subscript i) -> Just $ A.Suffix i  -- | Test if a given abstract name can appear with a suffix. Currently --   only true for the names of builtin sorts @Set@ and @Prop@.

@@ -26,10 +26,11 @@  import Prelude hiding (null) -import Control.Arrow ((&&&), first)-import Control.Monad.Except-import Control.Monad.Reader-import Control.Monad.State+import Control.Arrow        ( (&&&), first )+import Control.Monad        ( (<=<), forM, forM_, guard, liftM2 )+import Control.Monad.Except ( runExceptT )+import Control.Monad.Reader ( MonadReader(..), asks, runReaderT )+import Control.Monad.State  ( StateT(..), runStateT )  import qualified Control.Monad.Fail as Fail 

@@ -19,9 +19,9 @@  import Prelude hiding ( null ) -import Control.Applicative hiding ( empty )-import Control.Monad.Except-import Control.Monad.Reader+import Control.Monad        ( (<=<), foldM, forM, forM_, zipWithM, zipWithM_ )+import Control.Applicative  ( liftA2, liftA3 )+import Control.Monad.Except ( MonadError(..) )  import Data.Bifunctor import Data.Foldable (traverse_)@@ -126,18 +126,6 @@ --annotateDecl :: ScopeM A.Declaration -> ScopeM A.Declaration --annotateDecl m = annotateDecls $ (:[]) <$> m -annotateDecls :: ScopeM [A.Declaration] -> ScopeM A.Declaration-annotateDecls m = do-  ds <- m-  s  <- getScope-  return $ ScopedDecl s ds--annotateExpr :: ScopeM A.Expr -> ScopeM A.Expr-annotateExpr m = do-  e <- m-  s <- getScope-  return $ ScopedExpr s e- -- | Make sure that there are no dot patterns (called on pattern synonyms). noDotorEqPattern :: String -> A.Pattern' e -> ScopeM (A.Pattern' Void) noDotorEqPattern err = dot@@ -2102,13 +2090,19 @@ unGeneralized (A.ScopedExpr si e) = A.ScopedExpr si <$> unGeneralized e unGeneralized t = (mempty, t) +alreadyGeneralizing :: ScopeM Bool+alreadyGeneralizing = isJust <$> useTC stGeneralizedVars+ collectGeneralizables :: ScopeM a -> ScopeM (Set I.QName, a)-collectGeneralizables m = bracket_ open close $ do-    a <- m-    s <- useTC stGeneralizedVars-    case s of-        Nothing -> __IMPOSSIBLE__-        Just s -> return (s, a)+collectGeneralizables m =+  -- #5683: No nested generalization+  ifM alreadyGeneralizing ((Set.empty,) <$> m) $+  {-else-} bracket_ open close $ do+      a <- m+      s <- useTC stGeneralizedVars+      case s of+          Nothing -> __IMPOSSIBLE__+          Just s -> return (s, a)   where     open = do         gvs <- useTC stGeneralizedVars

@@ -23,9 +23,9 @@  import Prelude hiding (null) -import Control.Applicative (liftA2)-import Control.Arrow ((&&&))-import Control.Monad.State+import Control.Applicative ( liftA2 )+import Control.Arrow       ( (&&&) )+import Control.Monad       ( filterM, forM )  import qualified Data.List as List import qualified Data.Map as Map

@@ -2,9 +2,10 @@  module Agda.Syntax.Translation.ReflectedToAbstract where -import Control.Arrow ( (***) )-import Control.Monad.Except-import Control.Monad.Reader+import Control.Arrow        ( (***) )+import Control.Monad        ( foldM )+import Control.Monad.Except ( MonadError )+import Control.Monad.Reader ( MonadReader(..), asks, reader, runReaderT )  import Data.Maybe import Data.Set (Set)@@ -118,7 +119,7 @@   , HasConstInfo m   ) => r -> m (AbsOfRef r) toAbstractWithoutImplicit x = do-  xs <- getContextNames+  xs <- killRange <$> getContextNames   let ctx = zip xs $ repeat R.Unknown   runReaderT (toAbstract x) ctx @@ -190,10 +191,17 @@       return $ A.Pi exprNoRange (singleton a) b     R.Sort s   -> toAbstract s     R.Lit l    -> toAbstract l-    R.Meta x es    -> toAbstract (A.Underscore info, es)-      where info = emptyMetaInfo{ metaNumber = Just x }-    R.Unknown      -> return $ Underscore emptyMetaInfo+    R.Meta x es    -> do+      info <- mkMetaInfo+      let info' = info{ metaNumber = Just x }+      toAbstract (A.Underscore info', es)+    R.Unknown      -> Underscore <$> mkMetaInfo +mkMetaInfo :: ReadTCState m => m MetaInfo+mkMetaInfo = do+  scope <- getScope+  return $ emptyMetaInfo { metaScope = scope }+ mkDef :: HasConstInfo m => QName -> m A.Expr mkDef f =   ifM (isMacro . theDef <$> getConstInfo f)@@ -231,7 +239,7 @@       PropS x -> mkApp (A.Def propName) <$> toAbstract x       PropLitS x -> return $ A.Def' propName $ A.Suffix x       InfS x -> return $ A.Def' infName $ A.Suffix x-      UnknownS -> return $ mkApp (A.Def setName) $ Underscore emptyMetaInfo+      UnknownS -> mkApp (A.Def setName) . Underscore <$> mkMetaInfo  instance ToAbstract R.Pattern where   type AbsOfRef R.Pattern = A.Pattern

@@ -13,6 +13,8 @@  import qualified Control.Monad.Fail as Fail +import Control.Monad          ( forM )+import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.Except import Control.Monad.Reader 

@@ -57,7 +57,7 @@   let nonRec = mapMaybe (\case{ AcyclicSCC x -> Just x ; _ -> Nothing}) sccs   let recs   = mapMaybe (\case{ CyclicSCC xs -> Just xs; _ -> Nothing}) sccs -  reportSLn "rec.graph" 20 $ show graph+  reportSLn "rec.graph" 60 $ show graph    -- Mark all non-recursive functions and their clauses as such.   mapM_ markNonRecursive nonRec

@@ -18,8 +18,8 @@  import Prelude hiding ( null ) -import Control.Applicative (liftA2)-import Control.Monad.Reader+import Control.Applicative  ( liftA2 )+import Control.Monad        ( (<=<), filterM, forM, forM_, zipWithM )  import Data.Foldable (toList) import qualified Data.List as List@@ -549,7 +549,7 @@  termToDBP :: Term -> TerM DeBruijnPattern termToDBP t = ifNotM terGetUseDotPatterns (return unusedVar) $ {- else -} do-  termToPattern =<< do liftTCM $ stripAllProjections t+  termToPattern =<< do liftTCM $ stripAllProjections =<< normalise t  -- | Convert a term (from a dot pattern) to a pattern for the purposes of the termination checker. --@@ -570,7 +570,7 @@ --   termToPattern t = unnamed <$> termToPattern t  instance TermToPattern Term DeBruijnPattern where-  termToPattern t = liftTCM (reduce t >>= constructorForm) >>= \case+  termToPattern t = liftTCM (constructorForm t) >>= \case     -- Constructors.     Con c _ args -> ConP c noConPatternInfo . map (fmap unnamed) <$> termToPattern (fromMaybe __IMPOSSIBLE__ $ allApplyElims args)     Def s [Apply arg] -> do@@ -604,7 +604,7 @@     , nest 2 $ "ps  =" <+> do addContext tel $ prettyTCMPatternList ps     ]   forM' body $ \ v -> addContext tel $ do-    -- TODO: combine the following two traversals.+    -- TODO: combine the following two traversals, avoid full normalisation.     -- Parse dot patterns as patterns as far as possible.     ps <- postTraversePatternM parseDotP ps     -- Blank out coconstructors.

@@ -56,7 +56,7 @@  -- | Entry point for e.g. checking WithFunctionType. checkType :: (MonadCheckInternal m) => Type -> m ()-checkType t = do+checkType t = catchConstraint (CheckType t) $ do   inferred <- checkType' t   equalSort (getSort t) inferred @@ -343,8 +343,8 @@ -- | Infer possibly projection-like function application inferDef' :: (MonadCheckInternal m) => QName -> Arg Term -> Elims -> m Type inferDef' f a es = do-  isProj <- isProjection f-  case isProj of+  -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.+  isRelevantProjection f >>= \case     Just Projection{ projIndex = n } | n > 0 -> do       let self = unArg a       b <- infer self

@@ -32,6 +32,7 @@ import {-# SOURCE #-} Agda.TypeChecking.MetaVars import {-# SOURCE #-} Agda.TypeChecking.Empty import {-# SOURCE #-} Agda.TypeChecking.Lock+import {-# SOURCE #-} Agda.TypeChecking.CheckInternal ( checkType )  import Agda.Utils.CallStack ( withCurrentCallStack ) import Agda.Utils.Functor@@ -296,6 +297,7 @@ solveConstraint_ (HasBiggerSort a)      = hasBiggerSort a solveConstraint_ (HasPTSRule a b)       = hasPTSRule a b solveConstraint_ (CheckMetaInst m)      = checkMetaInst m+solveConstraint_ (CheckType t)          = checkType t solveConstraint_ (UsableAtModality mod t) = usableAtModality mod t  checkTypeCheckingProblem :: TypeCheckingProblem -> TCM Term

@@ -193,8 +193,10 @@         (Def f es, Def f' es') | f == f' ->           ifNotM (optFirstOrder <$> pragmaOptions) fallback $ {- else -} unlessSubtyping $ do           def <- getConstInfo f-          -- We do not shortcut projection-likes-          if isJust $ isProjection_ (theDef def) then fallback else do+          -- We do not shortcut projection-likes,+          -- Andreas, 2022-03-07, issue #5809:+          -- but irrelevant projections since they are applied to their parameters.+          if isJust $ isRelevantProjection_ def then fallback else do           pol <- getPolarity' cmp f           compareElims pol [] (defType def) (Def f []) es es' `orelse` fallback         _               -> fallback@@ -393,8 +395,8 @@   def <- getConstInfo f   -- To compute the type @a@ of a projection-like @f@,   -- we have to infer the type of its first argument.-  if projectionArgs (theDef def) <= 0 then return $ defType def else do-    -- Find an first argument to @f@.+  if projectionArgs def <= 0 then return $ defType def else do+    -- Find a first argument to @f@.     let arg = case (es, es') of               (Apply arg : _, _) -> arg               (_, Apply arg : _) -> arg

@@ -297,7 +297,7 @@       ]     ]   -- Jesper, 2019-10: introduce trailing arguments (see #3828)-  (_ , sc') <- insertTrailingArgs sc+  (_ , sc') <- insertTrailingArgs True sc   CoverResult { coverMissingClauses = missing } <- cover f cs sc'   return $ null missing  -- Andreas, 2019-08-08 and 2020-02-11@@ -517,16 +517,24 @@     -- blocked on arguments that are not yet introduced:      -- we must split on a variable so that the target type becomes a pi type-    trySplitRes (BlockedOnApply IsApply) finalSplit splitError cont-      | finalSplit = __IMPOSSIBLE__ -- already ruled out by lhs checker-      | otherwise  = cont+    trySplitRes (BlockedOnApply IsApply) finalSplit splitError cont = do+      -- Andreas, 2021-12-31, issue #5712.+      -- If there is a tactic to solve the clause, we might not have inserted+      -- trailing args (due to #5358).  Now we force it!+      (tel, sc') <- insertTrailingArgs True sc+      if null tel then+        if finalSplit then __IMPOSSIBLE__ -- already ruled out by lhs checker+        else cont+      else cover f cs sc'+     -- ...or it was an IApply pattern, so we might just need to introduce the variable now.     trySplitRes (BlockedOnApply IsIApply) finalSplit splitError cont        = do-         caseMaybeM (splitResultPath f sc) fallback $ (cover f cs . snd) <=< insertTrailingArgs+         caseMaybeM (splitResultPath f sc) fallback $ (cover f cs . snd) <=< insertTrailingArgs False       where         fallback | finalSplit = __IMPOSSIBLE__ -- already ruled out by lhs checker?                  | otherwise  = cont+     -- blocked on result but there are catchalls:     -- try regular splits if there are any, or else throw an error,     -- this is nicer than continuing and reporting unreachable clauses@@ -546,7 +554,7 @@         Right (Covering n scs) -> do           -- If result splitting was successful, continue coverage checking.           (projs, results) <- unzip <$> do-            mapM (traverseF $ cover f cs <=< (snd <.> insertTrailingArgs)) scs+            mapM (traverseF $ cover f cs <=< (snd <.> insertTrailingArgs False)) scs             -- OR:             -- forM scs $ \ (proj, sc') -> (proj,) <$> do             --   cover f cs =<< do@@ -970,11 +978,14 @@  -- | Add more patterns to split clause if the target type is a function type. --   Returns the domains of the function type (if any).-insertTrailingArgs :: SplitClause -> TCM (Telescope, SplitClause)-insertTrailingArgs sc@SClause{ scTel = sctel, scPats = ps, scSubst = sigma, scCheckpoints = cps, scTarget = target } = do+insertTrailingArgs+  :: Bool         -- ^ Force insertion even when there is a 'domTactic'?+  -> SplitClause+  -> TCM (Telescope, SplitClause)+insertTrailingArgs force sc@SClause{ scTel = sctel, scPats = ps, scSubst = sigma, scCheckpoints = cps, scTarget = target } = do   let fallback = return (empty, sc)   caseMaybe target fallback $ \ a -> do-    if isJust (domTactic a) then fallback else do+    if isJust (domTactic a) && not force then fallback else do     (TelV tel b) <- telViewUpTo (-1) $ unDom a     reportSDoc "tc.cover.target" 15 $ sep       [ "target type telescope: " <+> do@@ -990,7 +1001,7 @@         sctel'    = telFromList $ telToList (raise n sctel) ++ telToList tel         -- Dot patterns in @ps@ need to be raised!  (Issue 1298)         ps'       = applySubst (raiseS n) ps ++ xs-        newTarget = Just $ a $> b+        newTarget = Just $ (if not (null tel) then a{ domTactic = Nothing } else a) $> b         sc'       = SClause           { scTel    = sctel'           , scPats   = ps'@@ -1455,7 +1466,7 @@   ns <- case inserttrailing of     DontInsertTrailing -> return ns     DoInsertTrailing   -> lift $ forM ns $ \(con,sc) ->-      (con,) . snd <$> insertTrailingArgs sc+      (con,) . snd <$> insertTrailingArgs False sc    mHCompName <- getPrimitiveName' builtinHComp   withoutK   <- collapseDefault . optWithoutK <$> pragmaOptions

@@ -1,7 +1,8 @@  module Agda.TypeChecking.Datatypes where -import Control.Monad.Except+import Control.Monad        ( filterM )+import Control.Monad.Except ( MonadError(..), ExceptT(..), runExceptT )  import Data.Maybe (fromMaybe) 

@@ -6,7 +6,8 @@   , checkEmptyTel   ) where -import Control.Monad.Except+import Control.Monad        ( void )+import Control.Monad.Except ( MonadError(..) )  import Data.Semigroup import qualified Data.Set as Set

@@ -60,8 +60,8 @@ module Agda.TypeChecking.Free.Lazy where  import Control.Applicative hiding (empty)-import Control.Monad.Reader-+import Control.Monad        ( guard )+import Control.Monad.Reader ( MonadReader(..), asks, ReaderT, Reader, runReader )  import Data.IntMap (IntMap) import qualified Data.IntMap as IntMap

@@ -10,7 +10,7 @@ import Control.Monad import Control.Monad.Except -import Data.IntSet (IntSet)+import qualified Data.IntMap as IntMap import qualified Data.IntSet as IntSet import Data.Set (Set) import qualified Data.Set as Set@@ -127,7 +127,8 @@   return (genTelNames, t', userdata)  -- | Create metas for the generalizable variables and run the type check action.-createMetasAndTypeCheck :: Set QName -> TCM a -> TCM (a, Map MetaId QName, IntSet)+createMetasAndTypeCheck ::+  Set QName -> TCM a -> TCM (a, Map MetaId QName, MetaStore) createMetasAndTypeCheck s typecheckAction = do   ((namedMetas, x), allmetas) <- metasCreatedBy $ do     (metamap, genvals) <- createGenValues s@@ -150,13 +151,15 @@ --   generalized. Called in the context extended with the telescope record variable (whose type is --   the first argument). Returns the telescope of generalized variables and a substitution from --   this telescope to the current context.-computeGeneralization :: Type -> Map MetaId name -> IntSet -> TCM (Telescope, [Maybe name], Substitution)+computeGeneralization ::+  Type -> Map MetaId name -> MetaStore ->+  TCM (Telescope, [Maybe name], Substitution) computeGeneralization genRecMeta nameMap allmetas = postponeInstanceConstraints $ do    reportSDoc "tc.generalize" 10 $ "computing generalization for type" <+> prettyTCM genRecMeta    -- Pair metas with their metaInfo-  mvs <- mapM ((\ x -> (x,) <$> lookupMeta x) . MetaId) $ IntSet.toList allmetas+  mvs <- mapM ((\ x -> (x,) <$> lookupMeta x) . MetaId) $ IntMap.keys allmetas    -- Issue 4727: filter out metavariables that were created before the   -- current checkpoint, since they are too old to be generalized.@@ -317,7 +320,7 @@   -- Now we need to prune the unsolved metas to make sure they respect the new   -- dependencies (#3672). Also update interaction points to point to pruned metas.   let inscope (ii, InteractionPoint{ipMeta = Just x})-        | IntSet.member (metaId x) allmetas = Just (x, ii)+        | IntMap.member (metaId x) allmetas = Just (x, ii)       inscope _ = Nothing   ips <- Map.fromDistinctAscList . mapMaybe inscope . fst . BiMap.toDistinctAscendingLists <$> useTC stInteractionPoints   pruneUnsolvedMetas genRecName genRecCon genTel genRecFields ips shouldGeneralize allSortedMetas

@@ -120,7 +120,8 @@              return $ makeInstance info           (_, v) <- newMetaArg info' x CmpLeq a-          whenJust tac $ \ tac -> liftTCM $ unquoteTactic tac v a+          whenJust tac $ \ tac -> liftTCM $+            applyModalityToContext info $ unquoteTactic tac v a           let narg = Arg info (Named (Just $ WithOrigin Inserted $ unranged x) v)           mapFst (narg :) <$> implicitNamedArgs (n-1) expand (absApp b v)       _ -> return ([], t0')

@@ -7,9 +7,11 @@   , postponeInstanceConstraints   ) where -import Control.Monad.Except-import Control.Monad.Reader-import qualified Data.IntSet as IntSet+import Control.Monad        ( forM )+import Control.Monad.Except ( MonadError(..) )+import Control.Monad.Trans  ( lift )++import qualified Data.IntMap as IntMap import qualified Data.Map as Map import qualified Data.Set as Set import qualified Data.List as List@@ -84,7 +86,6 @@           vars = [ Candidate LocalCandidate x t (isOverlappable info)                  | (x, Dom{domInfo = info, unDom = (_, t)}) <- varsAndRaisedTypes                  , isInstance info-                 , usableModality info                  ]        -- {{}}-fields of variables are also candidates@@ -356,9 +357,9 @@ -- This is sufficient to reduce the list to a singleton should all be equal. dropSameCandidates :: MetaId -> [(Candidate, Term, a)] -> TCM [(Candidate, Term, a)] dropSameCandidates m cands0 = verboseBracket "tc.instance" 30 "dropSameCandidates" $ do-  metas <- getMetaVariableSet+  metas <- getMetaStore   -- Does `it` have any metas in the initial meta variable store?-  let freshMetas = getAny . allMetas (Any . (`IntSet.notMember` metas) . metaId)+  let freshMetas = getAny . allMetas (Any . (`IntMap.notMember` metas) . metaId)    -- Take overlappable candidates into account   let cands =@@ -582,7 +583,8 @@         Constructor {conPars = n} -> return $ Con c ci (map Apply $ drop n vs)         _ -> __IMPOSSIBLE__     Def f [] -> do-      mp <- isProjection f+      -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.+      mp <- isRelevantProjection f       case mp of         Just Projection{projIndex = n} -> do           case drop n vs of

@@ -118,13 +118,12 @@ --   as argument. workOnTypes' :: (MonadTCEnv m) => Bool -> m a -> m a workOnTypes' experimental-  = modifyContextInfo (mapRelevance f)+  = (if experimental+     then modifyContextInfo (mapRelevance irrToNonStrict)+     else id)   . applyQuantityToContext zeroQuantity   . typeLevelReductions   . localTC (\ e -> e { envWorkingOnTypes = True })-  where-    f | experimental = irrToNonStrict-      | otherwise    = id  -- | (Conditionally) wake up irrelevant variables and make them relevant. --   For instance,

@@ -5,8 +5,7 @@ import Control.Monad import Control.Monad.Except -import qualified Data.IntSet as IntSet-import Data.IntSet (IntSet)+import qualified Data.IntMap as IntMap import Data.Maybe  import Agda.Interaction.Options@@ -32,8 +31,8 @@   defaultLevelsToZero newMetas   return result -defaultLevelsToZero :: forall m. (PureTCM m, MonadMetaSolver m) => IntSet -> m ()-defaultLevelsToZero xs = loop =<< openLevelMetas (map MetaId $ IntSet.elems xs)+defaultLevelsToZero :: forall m. (PureTCM m, MonadMetaSolver m) => MetaStore -> m ()+defaultLevelsToZero xs = loop =<< openLevelMetas (map MetaId $ IntMap.keys xs)   where     loop :: [MetaId] -> m ()     loop xs = do

@@ -7,7 +7,7 @@   ) where -import Control.Monad.Reader+import Control.Monad            ( filterM, forM, forM_ )  import qualified Data.IntMap as IMap import qualified Data.IntSet as ISet

@@ -5,8 +5,9 @@  import Prelude hiding (null) -import Control.Monad.Except-import Control.Monad.Reader+import Control.Monad        ( foldM, forM, forM_, liftM2, void )+import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )+import Control.Monad.Trans  ( lift )  import Data.Function import qualified Data.IntMap as IntMap

@@ -118,6 +118,7 @@     HasPTSRule a b      -> mm (a, b)     UnquoteTactic tac hole goal -> False     CheckMetaInst m     -> True   -- TODO+    CheckType t         -> mm t     CheckLockedVars a b c d -> mm ((a, b), (c, d))     UsableAtModality mod t -> mm t     where

@@ -15,14 +15,16 @@  import qualified Control.Monad.Fail as Fail +import Control.Monad                ( void ) import Control.Monad.Except-import Control.Monad.State-import Control.Monad.Reader-import Control.Monad.Writer hiding ((<>))+import Control.Monad.IO.Class       ( MonadIO(..) )+import Control.Monad.State          ( MonadState(..), modify, StateT(..), runStateT )+import Control.Monad.Reader         ( MonadReader(..), ReaderT(..), runReaderT )+import Control.Monad.Writer         ( WriterT ) import Control.Monad.Trans          ( MonadTrans(..), lift ) import Control.Monad.Trans.Control  ( MonadTransControl(..), liftThrough )-import Control.Monad.Trans.Identity-import Control.Monad.Trans.Maybe+import Control.Monad.Trans.Identity ( IdentityT(..), runIdentityT )+import Control.Monad.Trans.Maybe    ( MaybeT(..) )  import Control.Parallel             ( pseq ) @@ -1002,6 +1004,11 @@ iFullHash :: Interface -> Hash iFullHash i = combineHashes $ iSourceHash i : List.map snd (iImportedModules i) +-- | A lens for the 'iSignature' field of the 'Interface' type.++intSignature :: Lens' Signature Interface+intSignature f i = f (iSignature i) <&> \s -> i { iSignature = s }+ --------------------------------------------------------------------------- -- ** Closure ---------------------------------------------------------------------------@@ -1065,6 +1072,7 @@   | HasBiggerSort Sort   | HasPTSRule (Dom Type) (Abs Sort)   | CheckMetaInst MetaId+  | CheckType Type   | UnBlock MetaId     -- ^ Meta created for a term blocked by a postponed type checking problem or unsolved     --   constraints. The 'MetaInstantiation' for the meta (when unsolved) is either 'BlockedConst'@@ -1114,6 +1122,7 @@       CheckLockedVars a b c d -> freeVars' ((a,b),(c,d))       UnquoteTactic t h g   -> freeVars' (t, (h, g))       CheckMetaInst m       -> mempty+      CheckType t           -> freeVars' t       UsableAtModality mod t -> freeVars' t  instance TermLike Constraint where@@ -1133,6 +1142,7 @@       HasBiggerSort s        -> foldTerm f s       HasPTSRule a s         -> foldTerm f (a, Sort <$> s)       CheckMetaInst m        -> mempty+      CheckType t            -> foldTerm f t       UsableAtModality m t   -> foldTerm f t    traverseTermM f c = __IMPOSSIBLE__ -- Not yet implemented@@ -1280,7 +1290,10 @@                 , mvInstantiation :: MetaInstantiation                 , mvListeners     :: Set Listener -- ^ meta variables scheduled for eta-expansion but blocked by this one                 , mvFrozen        :: Frozen -- ^ are we past the point where we can instantiate this meta variable?-                , mvTwin          :: Maybe MetaId -- ^ @Just m@ means this meta will be equated to @m@ when the latter is unblocked. See @blockedTermOnProblem@.+                , mvTwin          :: Maybe MetaId+                  -- ^ @Just m@ means that this meta-variable will be+                  -- equated to @m@ when the latter is unblocked. See+                  -- 'Agda.TypeChecking.MetaVars.blockTermOnProblem'.                 }   deriving Generic @@ -2907,6 +2920,9 @@           , envConflComputingOverlap :: Bool                 -- ^ Are we currently computing the overlap between                 --   two rewrite rules for the purpose of confluence checking?+          , envCurrentlyElaborating :: Bool+                -- ^ Are we currently in the process of executing an+                --   elaborate-and-give interactive command?           }     deriving (Generic) @@ -2966,6 +2982,7 @@                 , envGeneralizedVars        = Map.empty                 , envActiveBackendName      = Nothing                 , envConflComputingOverlap  = False+                , envCurrentlyElaborating   = False                 }  class LensTCEnv a where@@ -3106,6 +3123,9 @@ ePrintDomainFreePi :: Lens' Bool TCEnv ePrintDomainFreePi f e = f (envPrintDomainFreePi e) <&> \ x -> e { envPrintDomainFreePi = x } +ePrintMetasBare :: Lens' Bool TCEnv+ePrintMetasBare f e = f (envPrintMetasBare e) <&> \ x -> e { envPrintMetasBare = x }+ eInsideDotPattern :: Lens' Bool TCEnv eInsideDotPattern f e = f (envInsideDotPattern e) <&> \ x -> e { envInsideDotPattern = x } @@ -3142,6 +3162,9 @@ eConflComputingOverlap :: Lens' Bool TCEnv eConflComputingOverlap f e = f (envConflComputingOverlap e) <&> \ x -> e { envConflComputingOverlap = x } +eCurrentlyElaborating :: Lens' Bool TCEnv+eCurrentlyElaborating f e = f (envCurrentlyElaborating e) <&> \ x -> e { envCurrentlyElaborating = x }+ --------------------------------------------------------------------------- -- ** Context ---------------------------------------------------------------------------@@ -4195,38 +4218,45 @@ -- [1] When compiled with -auto-all and run with -p: roughly 750% -- faster for one example. -returnTCMT :: MonadIO m => a -> TCMT m a-returnTCMT = \x -> TCM $ \_ _ -> return x+returnTCMT :: Applicative m => a -> TCMT m a+returnTCMT = \x -> TCM $ \_ _ -> pure x {-# INLINE returnTCMT #-} -bindTCMT :: MonadIO m => TCMT m a -> (a -> TCMT m b) -> TCMT m b+bindTCMT :: Monad m => TCMT m a -> (a -> TCMT m b) -> TCMT m b bindTCMT = \(TCM m) k -> TCM $ \r e -> m r e >>= \x -> unTCM (k x) r e {-# INLINE bindTCMT #-} -thenTCMT :: MonadIO m => TCMT m a -> TCMT m b -> TCMT m b-thenTCMT = \(TCM m1) (TCM m2) -> TCM $ \r e -> m1 r e >> m2 r e+thenTCMT :: Applicative m => TCMT m a -> TCMT m b -> TCMT m b+thenTCMT = \(TCM m1) (TCM m2) -> TCM $ \r e -> m1 r e *> m2 r e {-# INLINE thenTCMT #-} -instance MonadIO m => Functor (TCMT m) where+instance Functor m => Functor (TCMT m) where   fmap = fmapTCMT -fmapTCMT :: MonadIO m => (a -> b) -> TCMT m a -> TCMT m b+fmapTCMT :: Functor m => (a -> b) -> TCMT m a -> TCMT m b fmapTCMT = \f (TCM m) -> TCM $ \r e -> fmap f (m r e) {-# INLINE fmapTCMT #-} -instance MonadIO m => Applicative (TCMT m) where+instance Applicative m => Applicative (TCMT m) where   pure  = returnTCMT   (<*>) = apTCMT -apTCMT :: MonadIO m => TCMT m (a -> b) -> TCMT m a -> TCMT m b-apTCMT = \(TCM mf) (TCM m) -> TCM $ \r e -> ap (mf r e) (m r e)+apTCMT :: Applicative m => TCMT m (a -> b) -> TCMT m a -> TCMT m b+apTCMT = \(TCM mf) (TCM m) -> TCM $ \r e -> mf r e <*> m r e {-# INLINE apTCMT #-}  instance MonadTrans TCMT where     lift m = TCM $ \_ _ -> m  -- We want a special monad implementation of fail.+#if __GLASGOW_HASKELL__ < 808 instance MonadIO m => Monad (TCMT m) where+#else+-- Andreas, 2022-02-02, issue #5659:+-- @transformers-0.6@ requires exactly a @Monad@ superclass constraint here+-- if we want @instance MonadTrans TCMT@.+instance Monad m => Monad (TCMT m) where+#endif     return = pure     (>>=)  = bindTCMT     (>>)   = (*>)

@@ -1,3 +1,5 @@+{-# LANGUAGE CPP #-}+ module Agda.TypeChecking.Monad.Base where  import Control.Monad.IO.Class (MonadIO)@@ -26,10 +28,18 @@ data TCState newtype TCMT m a = TCM { unTCM :: IORef TCState -> TCEnv -> m a } -instance MonadIO m => Applicative (TCMT m)-instance MonadIO m => Functor (TCMT m)-instance MonadIO m => Monad (TCMT m)+instance Applicative m => Applicative (TCMT m)+instance Functor m => Functor (TCMT m) instance MonadIO m => MonadIO (TCMT m)++#if __GLASGOW_HASKELL__ < 808+instance MonadIO m => Monad (TCMT m) where+#else+-- Andreas, 2022-02-02, issue #5659:+-- @transformers-0.6@ requires exactly a @Monad@ superclass constraint here+-- if we want @instance MonadTrans TCMT@.+instance Monad m => Monad (TCMT m) where+#endif  type TCM = TCMT IO 

@@ -6,7 +6,9 @@  import qualified Control.Monad.Fail as Fail +import Control.Monad                ( liftM2, void ) import Control.Monad.Except+import Control.Monad.IO.Class       ( MonadIO(..) ) import Control.Monad.Reader import Control.Monad.State import Control.Monad.Trans.Identity (IdentityT)

@@ -1,9 +1,11 @@  module Agda.TypeChecking.Monad.Builtin where -import Control.Monad.Reader-import Control.Monad.State+import Control.Monad.IO.Class       ( MonadIO )+import Control.Monad.Reader         ( ReaderT )+import Control.Monad.State          ( StateT ) import Control.Monad.Trans.Identity ( IdentityT )+import Control.Monad.Trans          ( MonadTrans, lift )  import qualified Control.Monad.Fail as Fail 

@@ -210,6 +210,7 @@       CheckFunDef{}    -> True       UnquoteTactic{}  -> True       CheckMetaInst{}  -> True+      CheckType{}      -> True       CheckLockedVars{} -> True       UsableAtModality{} -> True 

@@ -1,6 +1,7 @@  module Agda.TypeChecking.Monad.Context where +import Control.Monad                ( (<=<), forM, when ) import Control.Monad.Except import Control.Monad.Reader import Control.Monad.State

@@ -6,6 +6,8 @@  import qualified Control.Exception as E import qualified Control.DeepSeq as DeepSeq (force)++import Control.Monad.IO.Class       ( MonadIO(..) ) import Control.Monad.Except import Control.Monad.Reader import Control.Monad.State

@@ -19,9 +19,8 @@   , withImportPath   ) where -import Control.Arrow ( (***) )-import Control.Monad.State-+import Control.Arrow   ( (***) )+import Control.Monad   ( when )  import Data.Set (Set) import qualified Data.Map as Map

@@ -4,6 +4,9 @@  import Prelude hiding (null) +import Control.DeepSeq++import Control.Monad                ( (<=<), guard ) import Control.Monad.Except import Control.Monad.State import Control.Monad.Trans.Identity ( IdentityT )@@ -127,12 +130,17 @@ modifyMetaStore f = stMetaStore `modifyTCLens` f  -- | Run a computation and record which new metas it created.-metasCreatedBy :: ReadTCState m => m a -> m (a, IntSet)+metasCreatedBy :: ReadTCState m => m a -> m (a, MetaStore) metasCreatedBy m = do-  before <- IntMap.keysSet <$> useTC stMetaStore-  a <- m-  after  <- IntMap.keysSet <$> useTC stMetaStore-  return (a, after IntSet.\\ before)+  -- Compute largestMeta strictly to avoid leaking memory.+  !largestMeta <- force . fmap fst . IntMap.lookupMax <$>+                    useTC stMetaStore+  a            <- m+  ms           <- useTC stMetaStore+  let createdMetas = case largestMeta of+        Nothing          -> ms+        Just largestMeta -> snd $ IntMap.split largestMeta ms+  return (a, createdMetas)  -- | Lookup a meta variable. lookupMeta' :: ReadTCState m => MetaId -> m (Maybe MetaVariable)@@ -272,6 +280,7 @@       HasBiggerSort{}          -> return mempty       HasPTSRule{}             -> return mempty       CheckMetaInst x          -> return mempty+      CheckType t              -> return $ allMetas Set.singleton t       CheckLockedVars a b c d  -> return $ allMetas Set.singleton (a, b, c, d)       UsableAtModality{}       -> return mempty   where@@ -518,33 +527,37 @@ getMetaRange :: (MonadFail m, ReadTCState m) => MetaId -> m Range getMetaRange = getRange <.> lookupMeta -getInteractionScope :: InteractionId -> TCM ScopeInfo+getInteractionScope+  :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m)+  => InteractionId -> m ScopeInfo getInteractionScope = getMetaScope <.> lookupMeta <=< lookupInteractionId -withMetaInfo' :: MetaVariable -> TCM a -> TCM a+withMetaInfo' :: (MonadTCEnv m, ReadTCState m, MonadTrace m) => MetaVariable -> m a -> m a withMetaInfo' mv = withMetaInfo (miClosRange $ mvInfo mv) -withMetaInfo :: Closure Range -> TCM a -> TCM a+withMetaInfo :: (MonadTCEnv m, ReadTCState m, MonadTrace m) => Closure Range -> m a -> m a withMetaInfo mI cont = enterClosure mI $ \ r ->   setCurrentRange r cont -getMetaVariableSet :: ReadTCState m => m IntSet-getMetaVariableSet = IntMap.keysSet <$> getMetaStore+withInteractionId+  :: (MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m, MonadTrace m)+  => InteractionId -> m a -> m a+withInteractionId i ret = do+  m <- lookupInteractionId i+  withMetaId m ret +withMetaId+  :: (MonadFail m, MonadTCEnv m, ReadTCState m, MonadTrace m)+  => MetaId -> m a -> m a+withMetaId m ret = do+  mv <- lookupMeta m+  withMetaInfo' mv ret+ getMetaVariables :: ReadTCState m => (MetaVariable -> Bool) -> m [MetaId] getMetaVariables p = do   store <- getMetaStore   return [ MetaId i | (i, mv) <- IntMap.assocs store, p mv ] -getInstantiatedMetas :: ReadTCState m => m [MetaId]-getInstantiatedMetas = getMetaVariables (isInst . mvInstantiation)-  where-    isInst Open                           = False-    isInst OpenInstance                   = False-    isInst BlockedConst{}                 = False-    isInst PostponedTypeCheckingProblem{} = False-    isInst InstV{}                        = True- getOpenMetas :: ReadTCState m => m [MetaId] getOpenMetas = getMetaVariables (isOpenMeta . mvInstantiation) @@ -578,41 +591,31 @@ -- * Freezing and unfreezing metas. --------------------------------------------------------------------------- --- | Freeze all so far unfrozen metas for the duration of the given computation.-withFreezeMetas :: TCM a -> TCM a-withFreezeMetas cont = do-  ms <- Set.fromList <$> freezeMetas-  x  <- cont-  unfreezeMetas' (`Set.member` ms)-  return x---- | Freeze all meta variables and return the list of metas that got frozen.-freezeMetas :: TCM [MetaId]-freezeMetas = freezeMetas' $ const True---- | Freeze some meta variables and return the list of metas that got frozen.-freezeMetas' :: (MetaId -> Bool) -> TCM [MetaId]-freezeMetas' p = execWriterT $ modifyTCLensM stMetaStore $ IntMap.traverseWithKey (freeze . MetaId)+-- | Freeze the given meta-variables and return those that were not+--   already frozen.+freezeMetas :: MetaStore -> TCM IntSet+freezeMetas ms =+  execWriterT $+  modifyTCLensM stMetaStore $+  execStateT (mapM_ freeze $ IntMap.keys ms)   where-  freeze :: Monad m => MetaId -> MetaVariable -> WriterT [MetaId] m MetaVariable-  freeze m mvar-    | p m && mvFrozen mvar /= Frozen = do-        tell [m]-        return $ mvar { mvFrozen = Frozen }-    | otherwise = return mvar+  freeze :: Monad m => Int -> StateT MetaStore (WriterT IntSet m) ()+  freeze m = do+    store <- get+    case IntMap.lookup m store of+      Just mvar+        | mvFrozen mvar /= Frozen -> do+          lift $ tell (IntSet.singleton m)+          put $ IntMap.insert m (mvar { mvFrozen = Frozen }) store+        | otherwise -> return ()+      Nothing -> __IMPOSSIBLE__  -- | Thaw all meta variables. unfreezeMetas :: TCM ()-unfreezeMetas = unfreezeMetas' $ const True---- | Thaw some metas, as indicated by the passed condition.-unfreezeMetas' :: (MetaId -> Bool) -> TCM ()-unfreezeMetas' cond = modifyMetaStore $ IntMap.mapWithKey $ unfreeze . MetaId+unfreezeMetas = modifyMetaStore $ IntMap.map unfreeze   where-  unfreeze :: MetaId -> MetaVariable -> MetaVariable-  unfreeze m mvar-    | cond m    = mvar { mvFrozen = Instantiable }-    | otherwise = mvar+  unfreeze :: MetaVariable -> MetaVariable+  unfreeze mvar = mvar { mvFrozen = Instantiable }  isFrozen :: (MonadFail m, ReadTCState m) => MetaId -> m Bool isFrozen x = do

@@ -1,30 +1,44 @@  module Agda.TypeChecking.Monad.Options where -import Control.Arrow ( (&&&) )+import Control.Arrow          ( (&&&) )+import Control.Monad          ( unless, when )+import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.Except import Control.Monad.Reader import Control.Monad.State import Control.Monad.Writer +import qualified Data.Graph as Graph+import Data.List (sort) import Data.Maybe+import Data.Map (Map)+import qualified Data.Map as Map  import System.Directory import System.FilePath  import Agda.Syntax.Common+import Agda.Syntax.Concrete (TopLevelModuleName)+import qualified Agda.Syntax.Concrete as C+import qualified Agda.Syntax.Abstract as A import Agda.TypeChecking.Monad.Debug (reportSDoc) import Agda.TypeChecking.Warnings import Agda.TypeChecking.Monad.Base+import Agda.TypeChecking.Monad.Imports import Agda.TypeChecking.Monad.State import Agda.TypeChecking.Monad.Benchmark+import Agda.Interaction.FindFile import Agda.Interaction.Options import qualified Agda.Interaction.Options.Lenses as Lens import Agda.Interaction.Library import Agda.Utils.FileName import Agda.Utils.Functor+import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as G+import Agda.Utils.List import Agda.Utils.Maybe import Agda.Utils.Pretty+import Agda.Utils.Tuple import Agda.Utils.WithDefault  import Agda.Utils.Impossible@@ -180,8 +194,9 @@ -- | Makes the given directories absolute and stores them as include -- directories. ----- If the include directories change, then the state is reset (completely,--- except for the include directories and 'stInteractionOutputCallback').+-- If the include directories change, then the state is reset+-- (completely, except for the include directories and some other+-- things). -- -- An empty list is interpreted as @["."]@. @@ -204,7 +219,7 @@       -- We add the default dir at the end, since it is then       -- printed last in error messages.       -- Might also be useful to overwrite default imports...-  incs <- return $ incs ++ [primdir]+  incs <- return $ nubOn id $ incs ++ [primdir]    reportSDoc "setIncludeDirs" 10 $ return $ vcat     [ "Old include directories:"@@ -226,18 +241,97 @@   -- up in a situation in which we use the contents of the file   -- "old-path/M.agda", when the user actually meant   -- "new-path/M.agda".-  when (oldIncs /= incs) $ do+  when (sort oldIncs /= sort incs) $ do     ho <- getInteractionOutputCallback     tcWarnings <- useTC stTCWarnings -- restore already generated warnings     projectConfs <- useTC stProjectConfigs  -- restore cached project configs & .agda-lib     agdaLibFiles <- useTC stAgdaLibFiles    -- files, since they use absolute paths+    decodedModules <- getDecodedModules+    (keptDecodedModules, modFile) <- modulesToKeep incs decodedModules     resetAllState     setTCLens stTCWarnings tcWarnings     setTCLens stProjectConfigs projectConfs     setTCLens stAgdaLibFiles agdaLibFiles     setInteractionOutputCallback ho+    setDecodedModules keptDecodedModules+    setTCLens stModuleToSource modFile    Lens.putAbsoluteIncludePaths incs+  where+  -- A decoded module is kept if its top-level module name is resolved+  -- to the same absolute path using the old and the new include+  -- directories, and the same applies to all dependencies.+  --+  -- File system accesses are cached using the ModuleToSource data+  -- structure: For the old include directories this should mean that+  -- the file system is not accessed, but the file system is accessed+  -- for the new include directories, and certain changes to the file+  -- system could lead to interfaces being discarded. A new+  -- ModuleToSource structure, constructed using the new include+  -- directories, is returned.+  modulesToKeep+    :: [AbsolutePath]  -- New include directories.+    -> DecodedModules  -- Old decoded modules.+    -> TCM (DecodedModules, ModuleToSource)+  modulesToKeep incs old = process Map.empty Map.empty modules+    where+    -- A graph with one node per module in old, and an edge from m to+    -- n if the module corresponding to m imports the module+    -- corresponding to n.+    dependencyGraph :: G.Graph A.ModuleName ()+    dependencyGraph =+      G.fromNodes+        [ iModuleName $ miInterface m+        | m <- Map.elems old+        ]+        `G.union`+      G.fromEdges+        [ G.Edge+            { source = iModuleName $ miInterface m+            , target = d+            , label = ()+            }+        | m      <- Map.elems old+        , (d, _) <- iImportedModules $ miInterface m+        ]++    -- All the modules from old, sorted so that all of a module's+    -- dependencies precede it in the list.+    modules :: [ModuleInfo]+    modules =+      map (\case+              Graph.CyclicSCC{} ->+                -- Agda does not allow cycles in the dependency graph.+                __IMPOSSIBLE__+              Graph.AcyclicSCC m ->+                case Map.lookup (A.toTopLevelModuleName m) old of+                  Just m  -> m+                  Nothing -> __IMPOSSIBLE__) $+      G.sccs' dependencyGraph++    process ::+      Map A.ModuleName ModuleInfo -> ModuleToSource -> [ModuleInfo] ->+      TCM (DecodedModules, ModuleToSource)+    process !keep !modFile [] = return+      ( Map.fromList $+        map (mapFst A.toTopLevelModuleName) $+        Map.toList keep+      , modFile+      )+    process keep modFile (m : ms) = do+      let deps     = map fst $ iImportedModules $ miInterface m+          depsKept = all (`Map.member` keep) deps+      (keep, modFile) <-+        if not depsKept then return (keep, modFile) else do+        let n = iModuleName $ miInterface m+            t = A.toTopLevelModuleName n+        oldF            <- findFile' t+        (newF, modFile) <- liftIO $ findFile'' incs t modFile+        return $ case (oldF, newF) of+          (Right f1, Right f2) | f1 == f2 ->+            (Map.insert n m keep, modFile)+          _ -> (keep, modFile)+      process keep modFile ms  isPropEnabled :: HasOptions m => m Bool isPropEnabled = optProp <$> pragmaOptions

@@ -0,0 +1,9 @@+module Agda.TypeChecking.Monad.Options where++import Agda.Interaction.Library.Base+import Agda.Interaction.Options.HasOptions+import Agda.TypeChecking.Monad.Base+import Agda.Utils.FileName++libToTCM       :: LibM a -> TCM a+getIncludeDirs :: HasOptions m => m [AbsolutePath]

@@ -6,13 +6,14 @@  import qualified Control.Monad.Fail as Fail -import Control.Arrow (first, second)-import Control.Monad.Except-import Control.Monad.State-import Control.Monad.Reader-import Control.Monad.Writer hiding ((<>))-import Control.Monad.Trans.Maybe-import Control.Monad.Trans.Identity+import Control.Arrow                 ( first, second )+import Control.Monad.Except          ( ExceptT )+import Control.Monad.State           ( StateT  )+import Control.Monad.Reader          ( ReaderT )+import Control.Monad.Writer          ( WriterT )+import Control.Monad.Trans.Maybe     ( MaybeT  )+import Control.Monad.Trans.Identity  ( IdentityT )+import Control.Monad.Trans           ( MonadTrans, lift )  import Data.Foldable (for_) import qualified Data.List as List@@ -265,8 +266,8 @@ addDisplayForms :: QName -> TCM () addDisplayForms x = do   reportSDoc "tc.display.section" 20 $ "Computing display forms for" <+> pretty x-  def <- theDef <$> getConstInfo x-  let v = case def of+  def <- getConstInfo x+  let v = case theDef def of              Constructor{conSrcCon = h} -> Con h{ conName = x } ConOSystem []              _                          -> Def x [] @@ -441,7 +442,10 @@           -- Issue1238: the copied def should be an 'instance' if the original           -- def is one. Skip constructors since the original constructor will           -- still work as an instance.-          unless isCon $ whenJust inst $ \ c -> addNamedInstance y c+          -- Issue5583: Don't skip constructures, because the original constructor doesn't always+          -- work. For instance if it's only available in an anonymous module generated by+          -- `open import M args`.+          whenJust inst $ \ c -> addNamedInstance y c           -- Set display form for the old name if it's not a constructor. {- BREAKS fail/Issue478           -- Andreas, 2012-10-20 and if we are not an anonymous module@@ -1221,7 +1225,7 @@     Axiom{}                  -> 0     DataOrRecSig{}           -> 0     GeneralizableVar{}       -> 0-    def@Function{}           -> projectionArgs def+    def@Function{}           -> projectionArgs d     Datatype  {dataPars = _} -> 0  -- not dropped     Record     {recPars = _} -> 0  -- not dropped     Constructor{conPars = n} -> n@@ -1240,6 +1244,15 @@     Function { funProjection = result } -> result     _                                   -> Nothing +-- | Is it the name of a non-irrelevant record projection?+{-# SPECIALIZE isProjection :: QName -> TCM (Maybe Projection) #-}+isRelevantProjection :: HasConstInfo m => QName -> m (Maybe Projection)+isRelevantProjection qn = isRelevantProjection_ <$> getConstInfo qn++isRelevantProjection_ :: Definition -> Maybe Projection+isRelevantProjection_ def =+  if isIrrelevant def then Nothing else isProjection_ $ theDef def+ -- | Is it a function marked STATIC? isStaticFun :: Defn -> Bool isStaticFun = (^. funStatic)@@ -1256,20 +1269,21 @@   (projIndex isP > 0) && isJust (projProper isP)  -- | Number of dropped initial arguments of a projection(-like) function.-projectionArgs :: Defn -> Int-projectionArgs = maybe 0 (max 0 . pred . projIndex) . isProjection_+projectionArgs :: Definition -> Int+projectionArgs = maybe 0 (max 0 . pred . projIndex) . isRelevantProjection_  -- | Check whether a definition uses copatterns. usesCopatterns :: (HasConstInfo m) => QName -> m Bool usesCopatterns q = defCopatternLHS <$> getConstInfo q  -- | Apply a function @f@ to its first argument, producing the proper---   postfix projection if @f@ is a projection.+--   postfix projection if @f@ is a projection which is not irrelevant. applyDef :: (HasConstInfo m)          => ProjOrigin -> QName -> Arg Term -> m Term applyDef o f a = do   let fallback = return $ Def f [Apply a]-  caseMaybeM (isProjection f) fallback $ \ isP -> do+  -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.+  caseMaybeM (isRelevantProjection f) fallback $ \ isP -> do     if projIndex isP <= 0 then fallback else do       -- Get the original projection, if existing.       if isNothing (projProper isP) then fallback else do

@@ -5,7 +5,7 @@  import qualified Control.Exception as E -import Control.Monad.State (void)+import Control.Monad       (void) import Control.Monad.Trans (MonadIO, liftIO)  import Data.Maybe

@@ -22,11 +22,14 @@ -- Control.Monad.Fail import is redundant since GHC 8.8.1 import Control.Monad.Fail (MonadFail) -import Control.Monad.Except-import Control.Monad.Reader-import Control.Monad.State+import Control.Monad          ( liftM2, unless )+import Control.Monad.Except   ( MonadError )+import Control.Monad.IO.Class ( MonadIO(..) )+import Control.Monad.Reader   ( MonadReader(..), ReaderT, runReaderT )+import Control.Monad.State    ( MonadState )+import Control.Monad.Trans    ( MonadTrans, lift ) -import Data.List (isSuffixOf)+import Data.List              ( isSuffixOf )  import Agda.Syntax.Common hiding (Nat) import Agda.Syntax.Internal

@@ -11,10 +11,10 @@   , polFromOcc   ) where -import Control.Monad.State+import Control.Monad  ( forM_, zipWithM )  import Data.Maybe-import Data.Semigroup (Semigroup(..))+import Data.Semigroup ( Semigroup(..) )  import Agda.Syntax.Abstract.Name import Agda.Syntax.Common

@@ -6,7 +6,8 @@  import Control.Applicative hiding (empty) import Control.DeepSeq-import Control.Monad.Reader+import Control.Monad        ( forM_, guard, liftM2 )+import Control.Monad.Reader ( MonadReader(..), asks, Reader, runReader )  import Data.Either import qualified Data.Foldable as Fold@@ -260,13 +261,15 @@  getDefArity :: Definition -> TCM Int getDefArity def = do-  let dropped = case theDef def of-        defn@Function{} -> projectionArgs defn-        _ -> 0-  -- TODO: instantiateFull followed by arity could perhaps be-  -- optimised, presumably the instantiation can be performed-  -- lazily.-  subtract dropped . arity <$> instantiateFull (defType def)+  subtract (projectionArgs def) <$> arity' (defType def)+  where+  -- A variant of "\t -> arity <$> instantiateFull t".+  arity' :: Type -> TCM Int+  arity' t = do+    t <- instantiate t+    case unEl t of+      Pi _ t -> succ <$> arity' (unAbs t)+      _      -> return 0  -- Computing occurrences -------------------------------------------------- 

@@ -132,6 +132,8 @@           case mvJudgement m of             HasType{ jMetaType = t } -> prettyTCM x <+> ":" <+> prettyTCM t             IsSort{} -> prettyTCM x <+> "is a sort"+        CheckType t ->+          prettyTCM t <+> "is a well-formed type"         CheckLockedVars t ty lk lk_ty -> do           "Lock" <+> prettyTCM lk <+> "|-" <+> prettyTCMCtx TopCtx t <+> ":" <+> prettyTCM ty         UsableAtModality mod t -> "Is usable at" <+> prettyTCM mod <+> ":" <+> prettyTCM t

@@ -547,12 +547,7 @@     -- and the conversion checker for eliminations does not     -- like this.     -- We can only do untyped equality, e.g., by normalisation.-    -- Jesper, 2020-04-04: We reduce rather than normalise for-    -- efficiency reasons. In general this is weaker but it is-    -- equivalent at base types. A stronger version of-    -- primEraseEquality (using type-directed conversion) may be-    -- implemented using --rewriting.-    (u', v') <- reduce' (u, v)+    (u', v') <- normalise' (u, v)     if u' == v' then redReturn $ refl u else       return $ NoReduction $ map notReduced ts 

@@ -461,6 +461,8 @@                   -> FamilyOrNot                        (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term)                   -> m Term+-- ...    |- psi, u0+-- ..., i |- la, lb, bA, phi, bT, e unglueTranspGlue psi u0 (IsFam (la, lb, bA, phi, bT, e)) = do       let         localUse = builtinTrans ++ " for " ++ builtinGlue@@ -496,21 +498,31 @@                           <@> (imax phi (ineg i))                           <@> u0         [psi,u0] <- mapM (open . unArg) [psi,u0]++        -- glue1 t a = glue la[i1/i] lb[i1/i] bA[i1/i] phi[i1/i] bT[i1/i] e[i1/i] t a         glue1 <- do           g <- open $ (tglue `apply`) . map ((setHiding Hidden) . (subst 0 io)) $ [la, lb, bA, phi, bT, e]           return $ \ t a -> g <@> t <@> a-        unglue0 <- do-          ug <- open $ (tunglue `apply`) . map ((setHiding Hidden) . (subst 0 iz)) $ [la, lb, bA, phi, bT, e]-          return $ \ a -> ug <@> a+         [la, lb, bA, phi, bT, e] <- mapM (\ a -> open . runNames [] $ lam "i" (const (pure $ unArg a))) [la, lb, bA, phi, bT, e]++        -- Andreas, 2022-03-24, fixing #5838+        -- Following the updated note+        --+        --   Simon Huber, A Cubical Type Theory for Higher Inductive Types+        --   https://simhu.github.io/misc/hcomp.pdf (February 2022)+        --+        -- See: https://github.com/agda/agda/issues/5755#issuecomment-1043797776++        -- unglue_u0 i = unglue la[i/i] lb[i/i] bA[i/i] phi[i/i] bT[i/i] e[i/i] u0+        let unglue_u0 i =+              foldl (<#>) (pure tunglue) (map (<@> i) [la, lb, bA, phi, bT, e]) <@> u0+         view <- intervalView' -        -- phi1 <- view <$> (reduce =<< (phi <@> pure io))-        -- if not $ (isIOne phi1) then return Nothing else Just <$> do         let           tf i o = transpFill lb (lam "i" $ \ i -> bT <@> i <..> o) psi u0 i           t1 o = tf (pure io) o-          a0 = unglue0 u0            -- compute "forall. phi"           forallphi = pure tForall <@> phi@@ -522,14 +534,14 @@                                              <@> psi                                              <@> forallphi                                              <@> ilam "o" (\ a -> bA <@> i)-                                             <@> ilam "o" (\ _ -> a0)+                                             <@> ilam "o" (\ _ -> unglue_u0 i)                                              <@> ilam "o" (\ o -> pure tEFun <#> (lb <@> i)                                                                                <#> (la <@> i)                                                                                <#> (bT <@> i <..> o)                                                                                <#> (bA <@> i)                                                                                <@> (e <@> i <..> o)                                                                                <@> (tf i o)))-                 a0+                 (unglue_u0 (pure iz))            max l l' = pure tLMax <@> l <@> l'           sigCon x y = pure (Con (sigmaCon kit) ConOSystem []) <@> x <@> y@@ -642,6 +654,9 @@         case tpos of           Head -> t1 (pure tItIsOne)           Eliminated -> a1++-- ...    |- psi, u0+-- ..., i |- la, lb, bA, phi, bT, e compGlue DoTransp psi Nothing u0 (IsFam (la, lb, bA, phi, bT, e)) tpos = do       let         localUse = builtinTrans ++ " for " ++ builtinGlue@@ -677,20 +692,32 @@                           <@> (imax phi (ineg i))                           <@> u0         [psi,u0] <- mapM (open . unArg) [psi,u0]++        -- glue1 t a = glue la[i1/i] lb[i1/i] bA[i1/i] phi[i1/i] bT[i1/i] e[i1/i] t a         glue1 <- do           g <- open $ (tglue `apply`) . map ((setHiding Hidden) . (subst 0 io)) $ [la, lb, bA, phi, bT, e]           return $ \ t a -> g <@> t <@> a-        unglue0 <- do-          ug <- open $ (tunglue `apply`) . map ((setHiding Hidden) . (subst 0 iz)) $ [la, lb, bA, phi, bT, e]-          return $ \ a -> ug <@> a+         [la, lb, bA, phi, bT, e] <- mapM (\ a -> open . runNames [] $ lam "i" (const (pure $ unArg a))) [la, lb, bA, phi, bT, e]++        -- Andreas, 2022-03-24, fixing #5838+        -- Following the updated note+        --+        --   Simon Huber, A Cubical Type Theory for Higher Inductive Types+        --   https://simhu.github.io/misc/hcomp.pdf (February 2022)+        --+        -- See: https://github.com/agda/agda/issues/5755#issuecomment-1043797776++        -- unglue_u0 i = unglue la[i/i] lb[i/i] bA[i/i] phi[i/i] bT[i/i] e[i/e] u0+        let unglue_u0 i =+              foldl (<#>) (pure tunglue) (map (<@> i) [la, lb, bA, phi, bT, e]) <@> u0+         view <- intervalView'          ifM (headStop tpos (phi <@> pure io)) (return Nothing) $ Just <$> do         let           tf i o = transpFill lb (lam "i" $ \ i -> bT <@> i <..> o) psi u0 i           t1 o = tf (pure io) o-          a0 = unglue0 u0            -- compute "forall. phi"           forallphi = pure tForall <@> phi@@ -701,15 +728,15 @@                  (lam "i" $ \ i -> pure tPOr <#> (la <@> i)                                              <@> psi                                              <@> forallphi-                                             <@> ilam "o" (\ a -> bA <@> i)-                                             <@> ilam "o" (\ _ -> a0)+                                             <@> ilam "o" (\ _ -> bA <@> i)+                                             <@> ilam "o" (\ _ -> unglue_u0 i)                                              <@> ilam "o" (\ o -> pure tEFun <#> (lb <@> i)                                                                                <#> (la <@> i)                                                                                <#> (bT <@> i <..> o)                                                                                <#> (bA <@> i)                                                                                <@> (e <@> i <..> o)                                                                                <@> (tf i o)))-                 a0+                 (unglue_u0 (pure iz))            max l l' = pure tLMax <@> l <@> l'           sigCon x y = pure (Con (sigmaCon kit) ConOSystem []) <@> x <@> y@@ -864,21 +891,33 @@           let bAS = pure tSubIn <#> (pure tLSuc <@> la) <#> (Sort . tmSort <$> la) <#> phi <@> bA           g <- (open =<<) $ pure tglue <#> la <#> phi <#> bT <#> bAS           return $ \ t a -> g <@> t <@> a-        unglue0 <- do-          tunglue <- cl $ getTermLocal builtin_unglueU-          [la, phi, bT, bA] <- mapM (open . unArg . subst 0 iz) $ [la, phi, bT, bA]-          let bAS = pure tSubIn <#> (pure tLSuc <@> la) <#> (Sort . tmSort <$> la) <#> phi <@> bA-          ug <- (open =<<) $ pure tunglue <#> la <#> phi <#> bT <#> bAS-          return $ \ a -> ug <@> a+         [la, phi, bT, bA] <- mapM (\ a -> open . runNames [] $ lam "i" (const (pure $ unArg a))) [la, phi, bT, bA] +        -- Andreas, 2022-03-25, issue #5838.+        -- Port the fix of @unglueTranspGlue@ and @compGlue DoTransp@+        -- also to @compHCompU DoTransp@, as suggested by Tom Jack and Anders Mörtberg.+        -- We define @unglue_u0 i@ that is first used with @i@ and then with @i0@.+        -- The original code used it only with @i0@.+        tunglue <- cl $ getTermLocal builtin_unglueU+        let bAS i =+              pure tSubIn  <#> (pure tLSuc <@> (la <@> i))+                           <#> (Sort . tmSort <$> (la <@> i))+                           <#> (phi <@> i)+                           <@> (bA <@> i)+        let unglue_u0 i =+              pure tunglue <#> (la <@> i)+                           <#> (phi <@> i)+                           <#> (bT <@> i)+                           <#> bAS i+                           <@> u0+         ifM (headStop tpos (phi <@> pure io)) (return Nothing) $ Just <$> do          let           lb = la           tf i o = transpFill lb (lam "i" $ \ i -> bT <@> i <@> pure io <..> o) psi u0 i           t1 o = tf (pure io) o-          a0 = unglue0 u0            -- compute "forall. phi"           forallphi = pure tForall <@> phi@@ -889,12 +928,12 @@                  (lam "i" $ \ i -> pure tPOr <#> (la <@> i)                                              <@> psi                                              <@> forallphi-                                             <@> ilam "o" (\ a -> bA <@> i)-                                             <@> ilam "o" (\ _ -> a0)+                                             <@> ilam "o" (\ _ -> bA <@> i)+                                             <@> ilam "o" (\ _ -> unglue_u0 i)                                              <@> ilam "o" (\ o -> transp (la <@> i)                                                                            (\ j -> bT <@> i <@> ineg j <..> o)                                                                            (tf i o)))-                 a0+                 (unglue_u0 (pure iz))            w i o = lam "x" $                   transp (la <@> i)

@@ -87,7 +87,7 @@  import Agda.Utils.Impossible --- | View for a @Def f (Apply a : es)@ where @isProjection f@.+-- | View for a @Def f (Apply a : es)@ where @isRelevantProjection f@. --   Used for projection-like @f@s. data ProjectionView   = ProjectionView@@ -117,7 +117,7 @@ projView v = do   let fallback = return $ NoProjection v   case v of-    Def f es -> caseMaybeM (isProjection f) fallback $ \ isP -> do+    Def f es -> caseMaybeM (isRelevantProjection f) fallback $ \ isP -> do       if projIndex isP <= 0 then fallback else do         case es of           []           -> return $ LoneProjectionLike f $ projArgInfo isP@@ -226,6 +226,8 @@ --         Thus, an application of @f@ waiting for a projection --         can be stuck even when the principal argument is a constructor. --+--      g. @f@ cannot be an irrelevant definition (Andreas, 2022-03-07, #5809),+--         as those are not reduced. -- -- For internal reasons: --@@ -247,7 +249,9 @@     [ "Checking for projection likeness "     , prettyTCM x <+> " : " <+> prettyTCM t     ]-  case theDef defn of+  if isIrrelevant defn then+    reportSDoc "tc.proj.like" 30 $ "  projection-like functions cannot be irrelevant"+  else case theDef defn of     Function{funClauses = cls}       | any (isNothing . clauseBody) cls ->         reportSLn "tc.proj.like" 30 $ "  projection-like functions cannot have absurd clauses"

@@ -24,6 +24,7 @@  import Agda.Utils.Size import Agda.Utils.Either+import Agda.Utils.Function (applyWhen)  import Agda.Utils.Impossible @@ -162,23 +163,18 @@     applyWithoutReversing _            _   = __IMPOSSIBLE__      mapHide (El _ (Pi a b)) (p:tl) =-      case argInfoHiding (domInfo a) of-        Hidden -> (hideAndRelParams p):(mapHide (unAbs b) tl)-        _      -> p:(mapHide (unAbs b) tl)+      applyWhen (getHiding a == Hidden) hideAndRelParams p : mapHide (unAbs b) tl     mapHide t l = l  dropParameters :: TermLike a => a -> TCM a-dropParameters = traverseTermM dropPars-  where-    dropPars v =-      case v of+dropParameters = traverseTermM $+    \case         Con c ci vs -> do           Constructor{ conData = d } <- theDef <$> getConstInfo (conName c)           Just n <- defParameters <$> getConstInfo d           return $ Con c ci $ drop n vs-        Def f vs -> do-          isProj <- isProjection f-          case isProj of+        v@(Def f vs) -> do+          isRelevantProjection f >>= \case             Nothing -> return v             Just pr -> return $ applyE (projDropPars pr ProjSystem) vs-        _        -> return v+        v -> return v

@@ -9,10 +9,13 @@   , recordPatternToProjections   ) where -import Control.Arrow (first, second)-import Control.Monad.Fix-import Control.Monad.Reader-import Control.Monad.State+import Control.Arrow          ( first, second )+import Control.Monad          ( forM, unless, when, zipWithM )+import Control.Monad.Fix      ( mfix )+import Control.Monad.IO.Class ( MonadIO(..) )+import Control.Monad.Reader   ( MonadReader(..), ReaderT(..), runReaderT )+import Control.Monad.State    ( MonadState(..), StateT(..), runStateT )+import Control.Monad.Trans    ( lift )  import qualified Data.List as List import Data.Maybe

@@ -2,7 +2,7 @@  module Agda.TypeChecking.Reduce where -import Control.Monad.Reader+import Control.Monad ( (>=>), void )  import Data.Maybe import Data.Map (Map)@@ -232,6 +232,7 @@     CheckLockedVars <$> instantiate' a <*> instantiate' b <*> instantiate' c <*> instantiate' d   instantiate' (UnquoteTactic t h g) = UnquoteTactic <$> instantiate' t <*> instantiate' h <*> instantiate' g   instantiate' c@CheckMetaInst{}    = return c+  instantiate' (CheckType t)        = CheckType <$> instantiate' t   instantiate' (UsableAtModality mod t) = UsableAtModality mod <$> instantiate' t  instance Instantiate CompareAs where@@ -555,12 +556,14 @@       -- (i.e., those that failed the termination check)       -- and delayed definitions       -- are not unfolded unless explicitly permitted.-      dontUnfold =-        (defNonterminating info && SmallSet.notMember NonTerminatingReductions allowed)-        || (defTerminationUnconfirmed info && SmallSet.notMember UnconfirmedReductions allowed)-        || (defDelayed info == Delayed && not unfoldDelayed)-        || prp == Right True || isIrrelevant (defArgInfo info)-        || not defOk+      dontUnfold = or+        [ defNonterminating info && SmallSet.notMember NonTerminatingReductions allowed+        , defTerminationUnconfirmed info && SmallSet.notMember UnconfirmedReductions allowed+        , defDelayed info == Delayed && not unfoldDelayed+        , prp == Right True+        , isIrrelevant info+        , not defOk+        ]       copatterns = defCopatternLHS info   case def of     Constructor{conSrcCon = c} -> do@@ -573,12 +576,20 @@                              cls (defCompiled info) rewr         else noReduction $ notBlocked v     PrimitiveSort{ primSort = s } -> yesReduction NoSimplification $ Sort s `applyE` es+     _  -> do-      if (RecursiveReductions `SmallSet.member` allowed) ||-         (isJust (isProjection_ def) && ProjectionReductions `SmallSet.member` allowed) || -- includes projection-like-         (isInlineFun def && InlineReductions `SmallSet.member` allowed) ||-         (definitelyNonRecursive_ def && copatterns && CopatternReductions `SmallSet.member` allowed) ||-         (definitelyNonRecursive_ def && FunctionReductions `SmallSet.member` allowed)+      if or+          [ RecursiveReductions `SmallSet.member` allowed+          , isJust (isProjection_ def) && ProjectionReductions `SmallSet.member` allowed+              -- Includes projection-like and irrelevant projections.+              -- Note: irrelevant projections lead to @dontUnfold@ and+              -- so are not actually unfolded.+          , isInlineFun def && InlineReductions `SmallSet.member` allowed+          , definitelyNonRecursive_ def && or+            [ copatterns && CopatternReductions `SmallSet.member` allowed+            , FunctionReductions `SmallSet.member` allowed+            ]+          ]         then           reduceNormalE v0 f (map notReduced es) dontUnfold                        (defClauses info) (defCompiled info) rewr@@ -830,6 +841,7 @@   reduce' (CheckLockedVars a b c d) =     CheckLockedVars <$> reduce' a <*> reduce' b <*> reduce' c <*> reduce' d   reduce' c@CheckMetaInst{}     = return c+  reduce' (CheckType t)         = CheckType <$> reduce' t   reduce' (UsableAtModality mod t) = UsableAtModality mod <$> reduce' t  instance Reduce CompareAs where@@ -994,6 +1006,7 @@   simplify' (CheckLockedVars a b c d) =     CheckLockedVars <$> simplify' a <*> simplify' b <*> simplify' c <*> simplify' d   simplify' c@CheckMetaInst{}     = return c+  simplify' (CheckType t)         = CheckType <$> simplify' t   simplify' (UsableAtModality mod t) = UsableAtModality mod <$> simplify' t  instance Simplify CompareAs where@@ -1173,6 +1186,7 @@   normalise' (CheckLockedVars a b c d) =     CheckLockedVars <$> normalise' a <*> normalise' b <*> normalise' c <*> normalise' d   normalise' c@CheckMetaInst{}     = return c+  normalise' (CheckType t)         = CheckType <$> normalise' t   normalise' (UsableAtModality mod t) = UsableAtModality mod <$> normalise' t  instance Normalise CompareAs where@@ -1405,6 +1419,7 @@     CheckLockedVars a b c d ->       CheckLockedVars <$> instantiateFull' a <*> instantiateFull' b <*> instantiateFull' c <*> instantiateFull' d     c@CheckMetaInst{}   -> return c+    CheckType t         -> CheckType <$> instantiateFull' t     UsableAtModality mod t -> UsableAtModality mod <$> instantiateFull' t  instance InstantiateFull CompareAs where@@ -1532,24 +1547,44 @@        <*> return ell  instance InstantiateFull Interface where-    instantiateFull' (Interface h s ft ms mod scope inside-                               sig display userwarn importwarn b foreignCode-                               highlighting libPragmas filePragmas usedOpts patsyns-                               warnings partialdefs) =-        Interface h s ft ms mod scope inside-            <$> instantiateFull' sig-            <*> instantiateFull' display-            <*> return userwarn-            <*> return importwarn-            <*> instantiateFull' b-            <*> return foreignCode-            <*> return highlighting-            <*> return libPragmas-            <*> return filePragmas-            <*> return usedOpts-            <*> return patsyns-            <*> return warnings-            <*> return partialdefs+  instantiateFull' i = do+    defs <- instantiateFull' (i ^. intSignature . sigDefinitions)+    instantiateFullExceptForDefinitions'+      (set (intSignature . sigDefinitions) defs i)++-- | Instantiates everything except for definitions in the signature.++instantiateFullExceptForDefinitions' :: Interface -> ReduceM Interface+instantiateFullExceptForDefinitions'+  (Interface h s ft ms mod scope inside sig display userwarn importwarn+     b foreignCode highlighting libPragmas filePragmas usedOpts patsyns+     warnings partialdefs) =+  Interface h s ft ms mod scope inside+    <$> ((\s r -> Sig { _sigSections     = s+                      , _sigDefinitions  = sig ^. sigDefinitions+                      , _sigRewriteRules = r+                      })+         <$> instantiateFull' (sig ^. sigSections)+         <*> instantiateFull' (sig ^. sigRewriteRules))+    <*> instantiateFull' display+    <*> return userwarn+    <*> return importwarn+    <*> instantiateFull' b+    <*> return foreignCode+    <*> return highlighting+    <*> return libPragmas+    <*> return filePragmas+    <*> return usedOpts+    <*> return patsyns+    <*> return warnings+    <*> return partialdefs++-- | Instantiates everything except for definitions in the signature.++instantiateFullExceptForDefinitions ::+  MonadReduce m => Interface -> m Interface+instantiateFullExceptForDefinitions =+  liftReduce . instantiateFullExceptForDefinitions'  instance InstantiateFull a => InstantiateFull (Builtin a) where     instantiateFull' (Builtin t) = Builtin <$> instantiateFull' t

@@ -502,9 +502,11 @@  -- | In most cases pointers that we dereference do not contain black holes. derefPointer_ :: Pointer s -> ST s (Closure s)-derefPointer_ ptr = do-  Thunk cl <- derefPointer ptr-  return cl+derefPointer_ ptr =+  derefPointer ptr <&> \case+    Thunk cl  -> cl+    BlackHole -> __IMPOSSIBLE__+  -- | Only use for debug printing! unsafeDerefPointer :: Pointer s -> Thunk (Closure s)

@@ -10,7 +10,7 @@  import Prelude hiding (null) -import Control.Monad.Reader+import Control.Monad         ( liftM2 )  import qualified Data.Map as Map import Data.Maybe

@@ -22,9 +22,10 @@  import Prelude hiding (null, sequence) -import Control.Applicative (Alternative)-import Control.Monad.Except-import Control.Monad.State+import Control.Applicative  ( Alternative )+import Control.Monad        ( void )+import Control.Monad.Except ( MonadError(..), ExceptT, runExceptT )+import Control.Monad.State  ( MonadState, StateT, runStateT )  import qualified Control.Monad.Fail as Fail 

@@ -6,7 +6,8 @@  module Agda.TypeChecking.Rewriting.NonLinPattern where -import Control.Monad.Reader+import Control.Monad        ( (>=>), forM )+import Control.Monad.Reader ( asks )  import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet

@@ -10,7 +10,8 @@  import Prelude hiding ( null ) -import Control.Applicative ((<|>))+import Control.Applicative        ( (<|>) )+import Control.Monad              ( forM, forM_, guard, liftM2 ) import Control.Monad.Except import Control.Monad.Trans import Control.Monad.Trans.Maybe@@ -262,7 +263,8 @@  inferHeadDef :: ProjOrigin -> QName -> TCM (Elims -> Term, Type) inferHeadDef o x = do-  proj <- isProjection x+  -- Andreas, 2022-03-07, issue #5809: don't drop parameters of irrelevant projections.+  proj <- isRelevantProjection x   rel  <- getRelevance . defArgInfo <$> getConstInfo x   let app =         case proj of

@@ -9,9 +9,10 @@  import Data.Either (partitionEithers) import qualified Data.Foldable as Fold+import qualified Data.IntMap as IntMap+import qualified Data.IntSet as IntSet import Data.Maybe import qualified Data.Set as Set-import qualified Data.IntSet as IntSet import Data.Set (Set)  import Agda.Interaction.Highlighting.Generate@@ -213,7 +214,7 @@             A.Generalize{} -> pure ()             _ -> do               reportSLn "tc.decl" 20 $ "Freezing all metas."-              void $ freezeMetas' $ \ (MetaId x) -> IntSet.member x metas+              void $ freezeMetas metas          theMutualChecks @@ -335,7 +336,8 @@   lzero <- primLevelZero   let vArg = defaultArg       hArg = setHiding Hidden . vArg-  m    <- checkExpr e $ El (mkType 0) $ apply tcm [hArg lzero, vArg unit]+  m    <- applyQuantityToContext zeroQuantity $+            checkExpr e $ El (mkType 0) $ apply tcm [hArg lzero, vArg unit]   res  <- runUnquoteM $ tell xs >> evalTCM m   case res of     Left err      -> typeError $ UnquoteFailed err@@ -522,10 +524,10 @@     (a, ms) <- metasCreatedBy m     reportSLn "tc.decl" 20 $ "Attempting to solve constraints before freezing."     wakeupConstraints_   -- solve emptiness and instance constraints-    xs <- freezeMetas' $ (`IntSet.member` ms) . metaId+    xs <- freezeMetas ms     reportSDoc "tc.decl.ax" 20 $ vcat-      [ "Abstract type signature produced new metas: " <+> sep (map prettyTCM $ IntSet.toList ms)-      , "We froze the following ones of these:       " <+> sep (map prettyTCM xs)+      [ "Abstract type signature produced new metas: " <+> sep (map prettyTCM $ IntMap.keys ms)+      , "We froze the following ones of these:       " <+> sep (map prettyTCM $ IntSet.toList xs)       ]     return a 

@@ -4,8 +4,8 @@  import Prelude hiding ( null ) -import Control.Monad.Except-import Control.Monad.State+import Control.Monad        ( forM, forM_ )+import Control.Monad.Except ( MonadError(..) )  import Data.Bifunctor import Data.Function

@@ -18,7 +18,7 @@ import Control.Monad import Control.Monad.Except import Control.Monad.Reader-import Control.Monad.Writer hiding ((<>))+import Control.Monad.Writer       ( MonadWriter(..), runWriterT ) import Control.Monad.Trans.Maybe  import Data.IntSet (IntSet)

@@ -11,8 +11,9 @@  import Prelude hiding (null) -import Control.Arrow ( (***) )-import Control.Monad.Writer hiding ((<>))+import Control.Arrow        ( (***) )+import Control.Monad        ( zipWithM )+import Control.Monad.Writer ( MonadWriter(..), Writer, runWriter )  import Data.Functor (($>)) import Data.IntMap (IntMap)

@@ -1206,10 +1206,12 @@   -- Jesper, Andreas, 2018-10-17: the quantity of the equation is morally   -- always @Quantity0@, since the indices of the data type are runtime erased.   -- Thus, we need not change the quantity of the solution.+  envmod <- viewTC eModality   let eqrel  = getRelevance dom       eqmod  = getModality dom       varmod = getModality dom'       mod    = applyUnless (NonStrict `moreRelevant` eqrel) (setRelevance eqrel)+             $ applyUnless (usableQuantity envmod) (setQuantity zeroQuantity)              $ varmod   reportSDoc "tc.lhs.unify" 65 $ text $ "Equation modality: " ++ show (getModality dom)   reportSDoc "tc.lhs.unify" 65 $ text $ "Variable modality: " ++ show varmod

@@ -4,6 +4,7 @@  import Prelude hiding ( null ) +import Control.Monad         ( (<=<), forM ) import Control.Monad.Except import Control.Monad.Reader @@ -1346,7 +1347,8 @@ -- | Unquote a TCM computation in a given hole. unquoteM :: A.Expr -> Term -> Type -> TCM () unquoteM tacA hole holeType = do-  tac <- checkExpr tacA =<< (el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit))+  tac <- applyQuantityToContext zeroQuantity $+    checkExpr tacA =<< (el primAgdaTerm --> el (primAgdaTCM <#> primLevelZero <@> primUnit))   inFreshModuleIfFreeParams $ unquoteTactic tac hole holeType  -- | Run a tactic `tac : Term → TC ⊤` in a hole (second argument) of the type@@ -1624,7 +1626,7 @@     -- #4131: Only DontExpandLast if no user written type signature     let check | getOrigin info == Inserted = checkDontExpandLast               | otherwise                  = checkExpr'-    t <- isType_ t+    t <- workOnTypes $ isType_ t     v <- applyModalityToContext info $ check CmpLeq e t     addLetBinding info (A.unBind x) v t ret 

@@ -23,6 +23,8 @@   )   where +import Prelude hiding ( null )+ import System.Directory ( createDirectoryIfMissing ) import System.FilePath ( takeDirectory ) @@ -31,12 +33,14 @@ import qualified Control.Exception as E import Control.Monad import Control.Monad.Except+import Control.Monad.IO.Class ( MonadIO(..) ) import Control.Monad.Reader import Control.Monad.State.Strict  import Data.Array.IArray import Data.Word-import qualified Data.ByteString.Builder as L+import Data.ByteString.Lazy    ( ByteString )+import Data.ByteString.Builder ( byteString, toLazyByteString ) import qualified Data.ByteString.Lazy as L import qualified Data.HashTable.IO as H import qualified Data.Map as Map@@ -66,6 +70,7 @@ import Agda.Utils.FileName (canonicalizeAbsolutePath) import Agda.Utils.Hash import Agda.Utils.IORef+import Agda.Utils.Null  import Agda.Utils.Impossible @@ -74,15 +79,15 @@ -- 32-bit machines). Word64 does not have these problems.  currentInterfaceVersion :: Word64-currentInterfaceVersion = 20210514 * 10 + 1+currentInterfaceVersion = 20220211 * 10 + 0  -- | The result of 'encode' and 'encodeInterface'.  data Encoded = Encoded-  { uncompressed :: L.ByteString+  { uncompressed :: ByteString     -- ^ The uncompressed bytestring, without hashes and the interface     -- version.-  , compressed :: L.ByteString+  , compressed :: ByteString     -- ^ The compressed bytestring.   } @@ -135,7 +140,7 @@           }     cbits <- Bench.billTo [ Bench.Serialization, Bench.Compress ] $       return $!! G.compressWith compressParams bits1-    let x = B.encode currentInterfaceVersion `L.append` cbits+    let x = B.encode currentInterfaceVersion <> cbits     return (Encoded { uncompressed = bits1, compressed = x })   where     l h = List.map fst . List.sortBy (compare `on` snd) <$> H.toList h@@ -152,7 +157,7 @@       tickN (kind ++ " (reused)") $ fromIntegral reused #endif --- encode :: EmbPrj a => a -> TCM L.ByteString+-- encode :: EmbPrj a => a -> TCM ByteString -- encode a = do --     fileMod <- sourceToModule --     (x, shared, total) <- liftIO $ do@@ -160,7 +165,7 @@ --       root <- runReaderT (icode a) newD --       nL <- l nD; sL <- l sD; iL <- l iD; dL <- l dD --       (shared, total) <- readIORef stats---       return (B.encode currentInterfaceVersion `L.append`+--       return (B.encode currentInterfaceVersion <> --               G.compress (B.encode (root, nL, sL, iL, dL)), shared, total) --     verboseS "profile.sharing" 10 $ do --       tickN "pointers (reused)" $ fromIntegral shared@@ -174,7 +179,7 @@ -- -- Returns 'Nothing' if a decoding error is encountered. -decode :: EmbPrj a => L.ByteString -> TCM (Maybe a)+decode :: EmbPrj a => ByteString -> TCM (Maybe a) decode s = do   mf   <- useTC stModuleToSource   incs <- getIncludeDirs@@ -186,7 +191,7 @@   (mf, r) <- liftIO $ E.handle (\(E.ErrorCall s) -> noResult s) $ do      ((r, nL, ltL, stL, bL, iL, dL), s, _) <- return $ runGetState B.get s 0-    if s /= L.empty+    if not (null s)      then noResult "Garbage at end."      else do @@ -226,9 +231,9 @@ encodeInterface :: Interface -> TCM Encoded encodeInterface i = do   r <- encode i-  return (r { compressed = L.append hashes (compressed r) })+  return r{ compressed = hashes <> compressed r }   where-    hashes :: L.ByteString+    hashes :: ByteString     hashes = B.runPut $ B.put (iSourceHash i) >> B.put (iFullHash i)  -- | Encodes an interface. To ensure relocatability file paths in@@ -237,7 +242,7 @@ -- An uncompressed bytestring corresponding to the encoded interface -- is returned. -encodeFile :: FilePath -> Interface -> TCM L.ByteString+encodeFile :: FilePath -> Interface -> TCM ByteString encodeFile f i = do   r <- encodeInterface i   liftIO $ createDirectoryIfMissing True (takeDirectory f)@@ -249,7 +254,7 @@ -- Returns 'Nothing' if the file does not start with the right magic -- number or some other decoding error is encountered. -decodeInterface :: L.ByteString -> TCM (Maybe Interface)+decodeInterface :: ByteString -> TCM (Maybe Interface) decodeInterface s = do    -- Note that runGetState and the decompression code below can raise@@ -264,10 +269,10 @@        if ver /= currentInterfaceVersion        then Left "Wrong interface version."        else Right $-            L.toLazyByteString $+            toLazyByteString $             Z.foldDecompressStreamWithInput-              (\s -> (L.byteString s <>))-              (\s -> if L.null s+              (\s -> (byteString s <>))+              (\s -> if null s                      then mempty                      else error "Garbage at end.")               (\err -> error (show err))@@ -281,7 +286,7 @@         "Error when decoding interface file: " ++ err       return Nothing -decodeHashes :: L.ByteString -> Maybe (Hash, Hash)+decodeHashes :: ByteString -> Maybe (Hash, Hash) decodeHashes s   | L.length s < 16 = Nothing   | otherwise       = Just $ B.runGet getH $ L.take 16 s

@@ -9,6 +9,7 @@  import Control.Monad.Catch (catchAll) import Control.Monad.Except+import Control.Monad.IO.Class     ( MonadIO(..) ) import Control.Monad.Reader import Control.Monad.State.Strict (StateT, gets) 

@@ -3,10 +3,11 @@  module Agda.TypeChecking.Serialise.Instances.Common (SerialisedRange(..)) where -import Control.Monad.Except-import Control.Monad.Reader-import Control.Monad.State.Strict (gets, modify)-+import Control.Monad              ( (<=<) )+import Control.Monad.IO.Class     ( MonadIO(..) )+import Control.Monad.Except       ( MonadError(..) )+import Control.Monad.Reader       ( MonadReader(..), asks )+import Control.Monad.State.Strict ( gets, modify )  import Data.Array.IArray import Data.Word

@@ -239,13 +239,9 @@ instance EmbPrj LibWarning' where   icod_ = \case     UnknownField     a   -> icodeN 0 UnknownField a-    ExeNotFound      a b -> icodeN 1 ExeNotFound a b-    ExeNotExecutable a b -> icodeN 2 ExeNotExecutable a b    value = vcase $ \case     [0, a]    -> valuN UnknownField a-    [1, a, b] -> valuN ExeNotFound a b-    [2, a, b] -> valuN ExeNotExecutable a b     _ -> malformed  instance EmbPrj ExecutablesFile where

@@ -4,8 +4,9 @@  import Prelude hiding (null) -import Control.Monad.Except-import Control.Monad.Writer+import Control.Monad+import Control.Monad.Except ( MonadError(..) )+import Control.Monad.Writer ( MonadWriter(..), WriterT(..), runWriterT )  import qualified Data.Foldable as Fold import qualified Data.List as List

@@ -993,6 +993,7 @@     CheckLockedVars a b c d  -> CheckLockedVars (rf a) (rf b) (rf c) (rf d)     UnquoteTactic t h g      -> UnquoteTactic (rf t) (rf h) (rf g)     CheckMetaInst m          -> CheckMetaInst m+    CheckType t              -> CheckType (rf t)     UsableAtModality mod m   -> UsableAtModality mod (rf m)     where       rf :: forall a. TermSubst a => a -> a

@@ -9,10 +9,12 @@  module Agda.TypeChecking.SyntacticEquality (SynEq, checkSyntacticEquality) where -import Control.Arrow ((***))-import Control.Monad.State+import Control.Arrow            ( (***) )+import Control.Monad            ( zipWithM )+import Control.Monad.State      ( MonadState(..), StateT, runStateT )+import Control.Monad.Trans      ( lift ) -import Agda.Interaction.Options (optSyntacticEquality)+import Agda.Interaction.Options ( optSyntacticEquality )  import Agda.Syntax.Common import Agda.Syntax.Internal

@@ -1,11 +1,14 @@  module Agda.TypeChecking.Unquote where -import Control.Arrow (first, second)-import Control.Monad.Except-import Control.Monad.Reader-import Control.Monad.State-import Control.Monad.Writer hiding ((<>))+import Control.Arrow          ( first, second, (&&&) )+import Control.Monad          ( (<=<) )+import Control.Monad.Except   ( MonadError(..), ExceptT(..), runExceptT )+import Control.Monad.IO.Class ( MonadIO(..) )+import Control.Monad.Reader   ( ReaderT(..), runReaderT )+import Control.Monad.State    ( gets, modify, StateT(..), runStateT )+import Control.Monad.Writer   ( MonadWriter(..), WriterT(..), runWriterT )+import Control.Monad.Trans    ( lift )  import Data.Char import Data.Map (Map)@@ -17,6 +20,7 @@ import qualified Data.Text as T import Data.Word +import System.Directory (doesFileExist, getPermissions, executable) import System.Process ( readProcessWithExitCode ) import System.Exit ( ExitCode(..) ) @@ -658,6 +662,8 @@      tcFreshName :: Text -> TCM Term     tcFreshName s = do+      whenM (viewTC eCurrentlyElaborating) $+        typeError $ GenericError "Not supported: declaring new names from an edit-time macro"       m <- currentModule       quoteName . qualify m <$> freshName_ (T.unpack s) @@ -963,8 +969,13 @@   requireAllowExec   exes <- optTrustedExecutables <$> commandLineOptions   case Map.lookup exe exes of-    Nothing -> raiseExeNotFound exe exes+    Nothing -> raiseExeNotTrusted exe exes     Just fp -> do+      -- Check that the executable exists.+      unlessM (liftIO $ doesFileExist fp) $ raiseExeNotFound exe fp+      -- Check that the executable is executable.+      unlessM (liftIO $ executable <$> getPermissions fp) $ raiseExeNotExecutable exe fp+       let strArgs    = T.unpack <$> args       let strStdIn   = T.unpack stdIn       (datExitCode, strStdOut, strStdErr) <- lift $ readProcessWithExitCode fp strArgs strStdIn@@ -976,8 +987,16 @@  -- | Raise an error if the trusted executable cannot be found. ---raiseExeNotFound :: ExeName -> Map ExeName FilePath -> TCM a-raiseExeNotFound exe exes = genericDocError =<< do+raiseExeNotTrusted :: ExeName -> Map ExeName FilePath -> TCM a+raiseExeNotTrusted exe exes = genericDocError =<< do   vcat . map pretty $     ("Could not find '" ++ T.unpack exe ++ "' in list of trusted executables:") :     [ "  - " ++ T.unpack exe | exe <- Map.keys exes ]++raiseExeNotFound :: ExeName -> FilePath -> TCM a+raiseExeNotFound exe fp = genericDocError =<< do+  text $ "Could not find file '" ++ fp ++ "' for trusted executable " ++ T.unpack exe++raiseExeNotExecutable :: ExeName -> FilePath -> TCM a+raiseExeNotExecutable exe fp = genericDocError =<< do+  text $ "File '" ++ fp ++ "' for trusted executable" ++ T.unpack exe ++ " does not have permission to execute"

@@ -12,6 +12,7 @@ import Control.Monad.Reader import Control.Monad.Writer import Control.Monad.State+import Control.Monad.IO.Class ( MonadIO(..) )   import Data.Function

@@ -377,7 +377,7 @@ -- occur in both graphs (labels from the first graph are given as the -- first argument to the function). ----- Time complexity: /O(n₁ log (n₂/n₁ + 1) + e₁ log e₂/, where /n₁/ is+-- Time complexity: /O(n₁ log (n₂/n₁ + 1) + e₁ log e₂)/, where /n₁/ is -- the number of nodes in the graph with the smallest number of nodes -- and /n₂/ is the number of nodes in the other graph, and /e₁/ is the -- number of edges in the graph with the smallest number of edges and

@@ -4,7 +4,10 @@ where  import Control.Monad-import Control.Monad.Writer+import Control.Monad.Writer ( WriterT, execWriterT, tell )+import Control.Monad.Trans  ( lift )++import Data.Monoid          ( Endo(Endo, appEndo) )  import System.Directory import System.FilePath

@@ -2,6 +2,7 @@  module Agda.Utils.IO.UTF8   ( readTextFile+  , Agda.Utils.IO.UTF8.readFile   , Agda.Utils.IO.UTF8.writeFile   , writeTextToFile   ) where@@ -40,6 +41,15 @@     IO.NewlineMode { IO.inputNL = IO.CRLF, IO.outputNL = IO.LF }   IO.hSetEncoding h IO.utf8   T.hGetContents h++-- | Reads a UTF8-encoded text file and converts many character+-- sequences which may be interpreted as line or paragraph separators+-- into '\n'.++readFile :: FilePath -> IO String+readFile f = do+  s <- readTextFile f+  return $ T.unpack s  -- | Writes a UTF8-encoded text file. The native convention for line -- endings is used.

@@ -15,6 +15,7 @@ import Control.Monad.Fail as Fail import Control.Monad.Reader import Control.Monad.State+import Control.Monad.IO.Class ( MonadIO(..) )  #if !(MIN_VERSION_base(4,11,0)) import Data.Semigroup (Semigroup(..))

@@ -7,9 +7,10 @@     )     where -import Control.Applicative  (liftA2)-import Control.Monad.Except-import Control.Monad.State+import Control.Applicative  ( liftA2 )+import Control.Monad        ( MonadPlus(..), guard, unless, when )+import Control.Monad.Except ( MonadError(catchError, throwError) )+import Control.Monad.State  ( MonadState(get, put) )  import Data.Traversable as Trav hiding (for, sequence) import Data.Foldable as Fold

@@ -11,8 +11,8 @@ import Control.Monad.Reader import Control.Monad.State -import Data.ByteString.Char8 (ByteString)-import qualified Data.ByteString.Char8 as ByteString+import qualified Data.ByteString.Char8 as ByteStringChar8+import qualified Data.ByteString.Lazy as ByteStringLazy  import Data.HashMap.Strict (HashMap) import qualified Data.HashMap.Strict as HashMap@@ -64,9 +64,13 @@   empty          = (empty, empty, empty, empty)   null (a,b,c,d) = null a && null b && null c && null d -instance Null ByteString where-  empty = ByteString.empty-  null  = ByteString.null+instance Null ByteStringChar8.ByteString where+  empty = ByteStringChar8.empty+  null  = ByteStringChar8.null++instance Null ByteStringLazy.ByteString where+  empty = ByteStringLazy.empty+  null  = ByteStringLazy.null  instance Null Text where   empty = Text.empty

@@ -2,6 +2,7 @@ module Agda.Utils.Suffix where  import Data.Char+import qualified Data.List as List  import Agda.Utils.Impossible @@ -37,12 +38,11 @@ -- | Classification of identifier variants.  data Suffix-  = Prime     Int  -- ^ Identifier ends in @Int@ many primes.-  | Index     Int  -- ^ Identifier ends in number @Int@ (ordinary digits).-  | Subscript Int  -- ^ Identifier ends in number @Int@ (subscript digits).+  = Prime     Integer  -- ^ Identifier ends in @Integer@ many primes.+  | Index     Integer  -- ^ Identifier ends in number @Integer@ (ordinary digits).+  | Subscript Integer  -- ^ Identifier ends in number @Integer@ (subscript digits). --- | Increase the suffix by one.  If no suffix yet, put a subscript @1@---   unless users do not want us to use any unicode.+-- | Increase the suffix by one.  nextSuffix :: Suffix -> Suffix nextSuffix (Prime i)     = Prime $ i + 1@@ -53,17 +53,27 @@  suffixView :: String -> (String, Maybe Suffix) suffixView s-    | (ps@(_:_), s') <- span (=='\'') rs         = (reverse s', Just $ Prime $ length ps)+    | (ps@(_:_), s') <- span (=='\'') rs         = (reverse s', Just $ Prime $ List.genericLength ps)     | (ns@(_:_), s') <- span isDigit rs          = (reverse s', Just $ Index $ read $ reverse ns)     | (ns@(_:_), s') <- span isSubscriptDigit rs = (reverse s', Just $ Subscript $ read $                                                       map fromSubscriptDigit $ reverse ns)     | otherwise                                  = (s, Nothing)     where rs = reverse s +-- Note: suffixView could be implemented using spanEnd, but the implementation using reverse+-- looks more efficient, since the reversal is only done once.+--+-- suffixView :: String -> (String, Maybe Suffix)+-- suffixView s+--     | (s', ps@(_:_)) <- spanEnd (=='\'') s         = (s', Just $ Prime $ length ps)+--     | (s', ns@(_:_)) <- spanEnd isDigit s          = (s', Just $ Index $ read ns)+--     | (s', ns@(_:_)) <- spanEnd isSubscriptDigit s = (s', Just $ Subscript $ read $ map fromSubscriptDigit ns)+--     | otherwise                                    = (s, Nothing)+ -- | Print suffix.  renderSuffix :: Suffix -> String-renderSuffix (Prime n)     = replicate n '\''+renderSuffix (Prime n)     = List.genericReplicate n '\'' renderSuffix (Index i)     = show i renderSuffix (Subscript i) = map toSubscriptDigit (show i) 

@@ -25,8 +25,9 @@ -- NB: Control.Monad.Trans.Identity is already exported by Control.Monad.Identity -- since version mtl 2.2.2, but this needs at least ghc 8.2.2 import Control.Monad.Trans.Identity-import Control.Monad.Writer.Strict+import Control.Monad.Writer.Strict ( MonadWriter(..), Writer, WriterT, mapWriterT, runWriterT ) +import Data.Monoid ( Any(..) )  import Agda.Utils.Tuple 

@@ -1,4 +1,4 @@-resolver: lts-18.10+resolver: lts-18.22 compiler: ghc-8.10.7 compiler-check: match-exact 

@@ -1,4 +1,4 @@-resolver: nightly-2021-11-12+resolver: nightly-2022-01-06 compiler: ghc-9.0.1 compiler-check: match-exact @@ -7,6 +7,9 @@ # happy-1.21.0 is deprecated, but currently in nightly # (commercialhaskell/stackage#6294) - happy-1.20.0+# Andreas, 2022-02-07+# On Windows, we install the latest ICU (v69), which is only supported from text-icu >= 0.8+- text-icu-0.8.0  flags:   transformers-compat:

@@ -0,0 +1,7 @@+resolver: lts-19.0+compiler: ghc-9.0.2+compiler-check: match-exact++# Local packages, usually specified by relative directory name+packages:+- '.'

@@ -71,7 +71,7 @@ - process-extras-0.7.4 - random-1.2.1 - regex-base-0.94.0.1-- regex-posix-0.96.0.0+- regex-posix-0.96.0.1 - regex-tdfa-1.3.1.1 - safe-0.3.19 - scientific-0.3.7.0@@ -89,7 +89,7 @@ - temporary-1.3 - test-framework-0.8.2.0 - test-framework-hunit-0.3.0.2-- text-icu-0.7.1.0+- text-icu-0.8.0.1 - text-short-0.1.4 - th-abstraction-0.4.3.0 - th-compat-0.1.3

@@ -0,0 +1,6 @@+resolver: nightly-2022-03-26+compiler: ghc-9.2.2+compiler-check: match-exact++packages:+- '.'