Agda 2.9.0 release candidate 2 [wasm] - #8879

…8852)

* Fix #8851 by checking whether meta-program actually defined names in unquoteDecl

<details>
<summary>Claude interaction </summary>

Prompt
======

Local test/Fail/Issue8851 panics (issue #8851).
Instead, we want a proper error that `bang` was not actually defined by the meta-program passed to `unquoteDecl`.

Please investigate the source of this error and a fix.
While doing this also address the following:
- In `unquoteTop`, what is the point of `tell xs`?  Please document the `Writer` component of the UnquoteM monad.
- Why does `unquoteTop` return a list of `QName` when every invokation just ignores it?   What does this list actually contain?
- I suppose `checkUnquoteDecl` and `checkUnquoteDef` should both check that the names that are supposed to be defined by the meta program are actually defined.  The error should mention the names that were not defined.

Answer
======

`test/Fail/Issue8851` now fails with a proper error instead of panicking:

```
Issue8851.agda:13.1-29: error: [Unquote.MissingDefinition]
Missing definition for bang
```

The full `Succeed`/`Fail` suites pass, apart from the `CubicalSucceed` tests, which fail only because the cubical library isn't checked out. Nothing is committed yet.

Cause of the panic
------------------

`unquoteTop` ran `tell xs`, which put the names bound by `unquoteDecl` into the same list as the names the meta-program declares. After the run, `runUnquoteM` called `getConstInfo` on every name in that list to check it had been defined. `doNothing` never declares `bang`, so the lookup failed with `Unbound name`.

The same panic had two other triggers, and both are fixed too:
- **`unquoteDecl data D constructor c`** where the meta-program never declares `c`.
- **A name declared inside `runSpeculative` that is then rolled back.** The rollback restored the signature, but the name stayed in the list.

Your three questions
--------------------

**What `tell xs` is for.** The `Writer` part of `UnquoteM` collects the names the meta-program declares (via `declareDef`, `declarePostulate` and `declareData`). Each of these must be defined by the end. `tell xs` misused that list so the names bound by `unquoteDecl` also got checked. I removed it, and the `Writer` is now documented on the `UnquoteM` type.

**Why `unquoteTop` returned `[QName]`.** It returned that list: the bound names plus everything the meta-program declared. Every caller ignored it, so `unquoteTop` now returns `()`.

**Checking in `checkUnquoteDecl` and `checkUnquoteDef`.** Both go through `unquoteTop`, so I put the check in one place. `runUnquoteM` now takes the names the meta-program is expected to define as an argument. After the run it checks those names together with the ones the meta-program declared (duplicates removed). A name counts as missing if it isn't in the signature at all, or if it is a function with no clauses. All missing names are reported in one error. Tactics pass an empty list, so they behave as before.

Changes
-------

- **`Unquote.hs`:**
  - The `UnquoteM` documentation.
  - The new `runUnquoteM` check, which uses `getConstInfo'` so a missing name no longer panics.
  - `tcRunSpeculative` now drops the names it declared when it rolls back.
- **`Base.hs` / `Errors.hs`:** `MissingDefinition` now holds a non-empty list of names and prints them comma-separated, e.g. `Missing definition for f, h`. The error's name is unchanged, so existing `.err` files still match.
- **`Decl.hs` / `Term.hs`:** callers updated, and the unused `tell` import removed.
- **New tests:**
  - `test/Fail/Issue8851` (added an issue header).
  - `test/Fail/Issue8851-data`: an undeclared constructor, reported as `Missing definition for c`.
  - `test/Succeed/Issue8851-speculative`: the rollback case.

**Decision for you:** I first also treated a declared but undefined data type as missing. That broke `test/Succeed/Issue7576b`, which deliberately allows a bare data signature from reflection (#7576), so I reverted it and noted the reason in a comment. If you'd rather make that an error, it's a one-line change in `isUndefined`, but `Issue7576b` would then need to move to `Fail`.

</details>

* Re #8851: also require data definitions be given by unquoteDecl

I think allowing DataSigs created by reflection without accompanying
DataDefs was not attended, but just slipped through and was then made
explicit in #7576 to fix the internal error.
Now we simply do not allow them.

This partially reverts 4d79e4b.
Coded by Claude. (No memorable content from its summary to be preserved here.)

This case was deemed impossible but it ain't.
Implemented by Claude.

Closes #8853.

* Fix doc typo

* Restore doc hyperlinks to Cabal option docs

* Repair dangling reference

Otherwise `-v mimer:10` or even `-v 10` will turn this on by accident.

…aint

`tryLamAbs` needs to catch errors so that just Mimer does not report
them but simply fails the search instead.

Now `refine` catches errors from `tryLamAbs` and discards the branch.

Test: Mimer-LamAbsFail (previously: [UnequalTerms], now: No solution found).

New error `WrongNamedArgumentInLHS` which contains names of possible arguments as hint.

Coded by Claude, test case polishing by me.

Closes #8739.

* [wasm] Fix flake by switching dev environment to ghc912

* happy + alex: fetch packages from hpkgs

This reverts commit 6ed875c.

* Fix #8875: warning to show dependency version conflicts

* Files are clickable

* Restore markdown-ref like printing

* Warning also interactively

* Warning rendering cosmetics

* Review

* Shorten changelog

* Generalize tree printing to Data.Tree

* New PiSort field

* I am going insane

* Stuff

* Subject reduction fix?

* Update reduction for PiSort

* Fixes

* Fixes

* Optimisations

* Small fix

* Clean up context handling

* Micro-optimisation

* Cleanup

* Comments/cleanup

* Relax double checking of pi sorts

* Disable rewrite rules when checking old pi codom

---------

Co-authored-by: Andreas Abel <andreas.abel@ifi.lmu.de>

…in goal type

<details>
<summary>Claude interaction</summary>

The fix builds and works: Agda now accepts the module from issue #8866.

**Verdict:** the regression was an intended side effect of #8367, but it exposed a real bug in overlap resolution that 2.8.0 already had. 2.8.0 also rejects the same example with the binder's type written out, `op tt (λ (x : X) → g)`. 2.8.0 only accepted the original because the unsolved type of `x` happened to make instance search wait. #8367 deliberately removed that wait, as its CHANGELOG entry says.

**The bug:** in `checkCandidateForMeta` (`src/full/Agda/TypeChecking/InstanceArguments.hs`), a candidate counts as safe for overlap resolution if checking it leaves no constraints blocked on the goal's metas. `spec : C Z` against the goal `C ?B` simply sets `?B := Z` and leaves no constraint, so it counts as safe. It then knocks out `gen` as strictly more specific, and Agda commits to `?B := Z` too early. The same happens with `OVERLAPPING` instead of `INCOHERENT`.

**The fix:** a candidate also stops counting as safe if checking it sets a goal meta to anything other than another meta. Then both `gen` and `spec` stay candidates, the constraint waits until `?B := Y` is known, and only `gen` fits. It's about 15 lines in `checkCandidateForMeta`. Someone added a type signature to `stillFlexible` while I was working, and I kept it.

**New test:** `test/Succeed/Issue8866.agda` passes. It covers the issue's example, the variant with `(x : X)`, and a check that overlap is still resolved when the goal type is known.

**Remaining risk:** code whose goal type is never determined used to get the more specific instance. It will now be left with an unsolved instance constraint. The library ecosystem is the place to find out whether anything relies on that.

</details>

* agda-mode: Rebind mouse-2 to 'agda2-goto-definition-mouse'

As discussed in #8762, rebinding mouse-2 to
xref-find-definitions-at-mouse means that you cannot paste the primary
selection if there is no identifier on point.  We therefore revert the
change, un-deprecate 'agda2-goto-definition-mouse' and adjust it to
use Xref.

* Further work on issue #8762.

* agad2-mode: Don't reset point after clicking on definition

---------

Co-authored-by: Nils Anders Danielsson <nad@cse.gu.se>
Co-authored-by: Andreas Abel <andreas.abel@ifi.lmu.de>

`a ≤ b₁ ⊔ ... ⊔ bₙ` and `bᵢ ≤ a` for all `i` give `a = b₁ ⊔ ... ⊔ bₙ`.

Implemented by Claude.

Closes #8881.

When splitting x :^μ on c : (y :^ν C) → D, the new variable y has
modality μ∘ν in the context, but the pattern c y^ν has to carry the
field's own modality ν, as in Coverage.  checkLHS used the composed
modality for the pattern as well, and patternToTerm copied it into the
term c y that replaces x, e.g. in as-patterns and types.

Such ill-annotated terms were rejected by CheckInternal, i.e. by
--double-check and also by with-abstraction without --double-check:
- cohesion, polarity: __IMPOSSIBLE__ in checkModality
- erasure: spurious QuantityMismatch

Fix by Claude Opus 5.5.

Closes #8888.