Can not eliminate [type blocked on meta] forces very silly extended lambdas

[plt-amy]

The setup is anything that uses (e.g.) instance search to build a function type ending in a record, e.g. this silly reduction of some 1lab helpers:

postulate A B : Set

record R : Set₁ where field f1 : Set
open R

record S (A : Set) : Set₂ where field T : Set₁
open S

postulate fun : (X : Set) ⦃ t : S X ⦄ → t .T → X

instance
  S-A : ∀ {X} ⦃ _ : S X ⦄ → S (A → X)
  S-A ⦃ i ⦄ = record { T = A → i .T }

  S-B : S B
  S-B = record { T = R }

The problem is trying to use fun with an extended lambda (at type A → R) to build an A → B. This works:

_ : A → B
_ = fun (A → B) λ a → λ where
  .f1 → {!   !}

This fails, because the "can not eliminate" check is too eager to fail hard:

_ : A → B
_ = fun (A → B) λ where
  a .f1 → {!   !}

{-
/home/amelia/default/Projects/agda/Test291.agda:22.5-8: error: [CannotEliminateWithProjection]
Cannot eliminate type  (_22 .T)  with projection  f1
when checking the clause left hand side
.extendedlambda0 a .f1
-}

[andreasabel]

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, as it computes also type information.)

[andreasabel]

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