This modification type checks in Agda 2.6.4 RC2.

 S = Σ λ (x : X) → Σ λ (y : Y) → A x × B y
 T = (Σ λ (x : X) → A x) × (Σ λ (y : Y) → B y)

 fact : S ≅ T
 fact = f , g , gf , fg
  where
   f : S → T
   f (x , y , a , b) = ((x , a) , (y , b))
   g : _
   g ((x , a) , (y , b)) = x , y , a , b
   fg : f ∘ g ∼ id
   fg _ = refl
   gf : g ∘ f ∼ id
   gf _ = refl

So it seems to be a type inference problem. But instead of giving unsolved constraints it is giving an error as discussed in the previous comment (and Agda 2.6.3 can solve the constraints and doesn't give an error).

I "fixed" TypeTopology so that it now type checks with Agda 2.6.4 RC2. However, the above example shows that Agda 2.6.4 type-checks / type-infers fewer Agda files than 2.6.3.

Bisection run v2.6.3 - master reports:

Succeeds at:

• b86dd2b [ releases notes ] Removed mention to -fprof-auto.
• dc845d0 Also apply the change to getDefinition and add documentation
• 32599bc [ Release Agda 2.6.3 #6055, CHANGELOG ] Updated list of closed issues.
• dd60c64 [ workflows ] add cabal sdist to whitespace.yml CI

Internal error at:

• BLAMED: 536b73f [ re Regression related to Cubical Agda and generalisable variables #6211 ] Pull off the band-aid
• 590cede Reflection ffi pragmas (Reflection ffi pragmas #6366)
• 022a617 [ user-manual ] doc: use stack-x.y.z everywhere
• be4d058 [ workflows ] stack/test: fix cache-deletion step
• 791fb5e Bump CI from GHC 9.4.4 to 9.4.5 (except for Windows)
• RC1: v2.6.3.20230805

This bisect run only found the point where the result went from "good" to "internal error".

Looks like the OP went from accepted to rejected somewhere invisible due to a cover of "internal error" introduced by 536b73f.
@jespercockx , could you have a look please?

Turning on -v tc.lhs.top:10 triggers the following impossible:

I did a manual bisect now, patching away the __IMPOSSIBLE__ at each step. Result is:
f271f44 is the first bad commit (ping @jespercockx)

Date: Sun Sep 3 19:07:22 2023 +0200
[ fix #6758 ] Instantiate defBlocked in case of blocked definition

Here's my idea of what is going on during the type checking of the where block:

• First, Agda tries to type check the definitions of f and g, but is blocked by the metas in their type signatures.
• Then it tries to check the definitions of fg and gf. Checking refl at type f (g x) = x is blocked as well because the definitions of f and g are not yet known. Importantly, Agda blocks this problem on the meta it gets from the defBlocked fields of f and g, which point to the same metas that the definitions of f and g themselves are blocked on.
• Next, Agda checks the body of fact itself, which succeeds. In the process, it also learns about the types of f and g, instantiating the two metas from their types.
• This unblocks both the checking of the definitions of f and g, and the checking of both refls. Agda (arbitrarily) decides to check the refl first.
• Agda again tries to reduce f (g x) to whnf, which still doesn't work (as we still don't have a definition for f and g) but now there is also no longer any meta blocking the problem! Since nothing is blocking the problem, Agda assumes that f (g x) is the final whnf and throws an error because it is not equal to x.

To fix this problem, it seems like we should instead block the checking of the refl until the definitions of f and g have actually been checked and added to the signature. It seems we already have a constructor for this in the Blocker type for this: UnblockOnDef, but we are not using it here which is causing the problem.