Decide whether pi is large based on original codomain sort - #8870

Since this is supposed to go on 2.9.0, I asked Claude for a review, and it found two regressions, one internal error, and one case with with. I paste the review here. This should be investigated before merging, and the reproducers should go into the testsuite to guard against regressions.

Regression 1: internal error with rewrite rules in a parameterised module. Master accepts this file; the PR dies with __IMPOSSIBLE__ at Reduce.hs:488.

{-# OPTIONS --rewriting #-}
open import Agda.Primitive
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

postulate
  I : Set
  g : Level → I → Level

module _ (a : Level) where
  postulate p : ∀ {i} → g a i ≡ lzero
  {-# REWRITE p #-}

  postulate
    F : (b : Level) (i : I) → Set (g b i)
    G : (b : Level) (X Y : (i : I) → Set (g b i)) → Set

  test : (b : Level) → G b (F b) (F b) ≡ G b (F b) (λ i → F b i)
  test b = refl

Cause: inLargeEnoughContext uses inTopContext, which drops the module checkpoints. Inside the dummy context moduleParamsToApply then returns no arguments (see its comment about #4383), so the rule is used uninstantiated as g ?a i ↦ lzero and rewrites g b i. In the real context the rule is instantiated to g a i and does not fire. So the old codomain sort comes out NotFree while the current one is MaybeFree, which the code asserts cannot happen. The same dummy-context trick also loses local rewrite rules (--local-rewriting) and let-bindings, so the "old" dependency check can disagree with the real context in the other direction too. I could not turn the local-rewriting case into a user-visible failure, but it is the same root cause.

Regression 2: with on a term whose type went through substitution. Master accepts this; the PR rejects it.

open import Agda.Primitive

postulate
  I : Set
  F : (o : I → Level) (i : I) → Set (o i)

test : Set₁
test with F (λ _ → lzero)
... | _ = Set

error: [UnequalTypes]
The types Set₂ and Setω are not equal
when checking that the type ((i : I) → Set) → Set₁ of the generated
with function is well-formed

The same happens with module M (o : I → Level) where postulate F : (i : I) → Set (o i) followed by open M (λ _ → lzero) and with F. Cause: after piApply, the type of F (λ _ → lzero) keeps PiSort (CodomainSortOld (Set (lsuc (o i)))), which now reduces to Setω by design. But sortOf (used by checkType on the with-function type, checkSolutionSort, checkInternal) recomputes sorts from the term and gets Set₁. The debug output shows exactly this: "checking if sort Set₂ of pi type ((i : I) → Set) → Set₁ fits in given sort Setω". So stored sorts and recomputed sorts are no longer consistent, and every place that compares them with CmpEq can fail. with is the one I could trigger; --double-check and reflection's checkType are candidates for the same mismatch.

Smaller remarks

• simplify' for sorts does not instantiate metas before piSortB', so a CodomainSortOld holding an instantiated sort meta while the current codomain is already Setω would hit the (_, Right LargeSort{}) impossible case in piSortB''. I did not find a trigger; it is reachable only via interactive "simplified" normalisation.
• Derived Eq/SynEq on PiSort now compares the stored old sort, so two otherwise identical PiSorts fail syntactic equality and get postponed in piSortEquals until their blockers clear. Harmless in all tests, but it is extra constraint churn.
• Several traversals (Free, Occurs, positivity, termination) deliberately skip the old sort. That is fine as long as nothing interprets it in a real context, which currently holds.

That should be both regressions fixed.

I am less convinced by Claude's "smaller remarks":

• I don't see how the current codomain sort could ever become a large sort if the original codomain sort was dependent (and therefore not large)
• We definitely cannot ignore the blocked dependency check in while checking syntactic equality: the blocked dependency check can determine whether the pi reduces to a large or small sort, and these are not equal!
• Skipping the codomain sort in those traversals is intentional

There definitely could be bugs somewhere related to these things which I have missed, and obviously the reproducers were useful, but I'm not convinced sending LLM generated comments like these without validation is helpful... I spent quite a while thinking about the first remark before deciding it wasn't a bug

Thanks!

Well, you are the expert on your PR. You can ignore the speculations if you find they have no substance. I am in a worse position to judge whether there is anything to it or not.