Andreas Abel

We are always too close to a release. :-D

> As the coordinator, cabal should probably recognize when another instance is already building a given package, and wait. (In variant #11329, a similar race occurs when creating the `.cabal/store`...

The crux seems to be the lack of postponing lhs checking, according to this comment: https://github.com/agda/agda/blob/af61c6ce8696d4a80cb48955d1a11f5966cfbe76/src/full/Agda/TypeChecking/Rules/LHS.hs#L1716-L1719 https://github.com/agda/agda/blob/af61c6ce8696d4a80cb48955d1a11f5966cfbe76/src/full/Agda/TypeChecking/Rules/LHS.hs#L1757-L1762 (Remark: the function is called `disambiguateProjection` but also called for non-ambiguous projection patterns,...

Discussing Agda dev 2025-10-15: maybe add `CannotEliminateWithProjection` to the errors caught by `catchIlltypedPatternBlockedOnMeta`.

Here is an example where refining `w` to `w@(wrap _)` for no-eta constructor `wrap` makes a previously checking expression fail: ```agda -- Transparent wrap (η) record Just (A : Set)...

Here is a continuation of the last example: ```agda module Works2 (t@(just w) : T) (let wrap a = w) where -- Also works if I match on w with...

If we want to turn off let-pattern matching in the absence of eta, we can make the `recordPatternsToProjections` translation require eta constructors: https://github.com/agda/agda/blob/841f323b07e49ae4ba812a9dc0a330cb95145bce/src/full/Agda/TypeChecking/Rules/Term.hs#L1575-L1576 https://github.com/agda/agda/blob/841f323b07e49ae4ba812a9dc0a330cb95145bce/src/full/Agda/TypeChecking/Rules/Term.hs#L1588-L1589 Whether something is a eta-constructor could...

Another small example: ```agda open import Agda.Builtin.Equality record Wrap (A : Set) : Set where constructor wrap; no-eta-equality; pattern field unwrap : A open Wrap postulate A : Set _==_∋_...

Reverted the push to master, new PR at: - https://github.com/agda/agda/pull/6848

Here is a fun exploit of this issue: ```agda module Issue7664a where open import Agda.Builtin.String open import Agda.Builtin.Equality typeOf : {A : Set} (a : A) → Set typeOf {A}...