Why can't I move a partial box definition into a local binding?

As a followup to this, I realized I need to use a heterogeneous composition to make a lid for a partial box. Here I have removed all the unnecessary cruft:

{-# OPTIONS --cubical #-}

module _ where

open import Cubical.Core.Everything
open import Cubical.Foundations.Everything

postulate
  A : Type

  P : A → Type
  PIsProp : ∀ x → isProp (P x)

  prove : ∀ x → P x

  x y : A
  q : x ≡ y

a = prove x
b = prove y

prf : PathP (λ i → P (q i)) a b
prf = p
  where
    b′ : P y
    b′ = subst P q a

    r : PathP _ a b′
    r = transport-filler (λ i → P (q i)) a

    --        a            b
    --        ^            ^
    --        |            |
    --   refl |            | PIsProp y _ _
    --        |            |
    ---       a ---------> b′
    --               r

    p-faces : (i j : I) → Partial (i ∨ ~ i) (P (q i))
    p-faces i j (i = i0) = a
    p-faces i j (i = i1) = PIsProp y b′ b j

    p : PathP (λ i → P (q i)) a b
    p i = comp (λ j → P (q i)) ? (r i)

So here the only remaining hole is in the defintion of p. I'd like to fill it with p-faces i, of course, because that is the reason I defined it. However, this leads to a universe level error:

    p : PathP (λ i → P (q i)) a b
    p i = comp (λ j → P (q i)) (p-faces i) (r i)

Agda.Primitive.SSet ℓ-zero != Agda.Primitive.SSetω

when checking that the expression p-faces i has type

(i₁ : I) → Partial (i ∨ ~ i) (P (q i))

However, if I inline the definition of p-faces into p, it typechecks; note that this also includes typechecking the definition of p-faces (I don't need to remove it), it is only the usage of p-faces that causes this type error:

    p : PathP (λ i → P (q i)) a b
    p i = comp (λ j → P (q i)) (λ { j (i = i0) → a; j (i = i1) → PIsProp y b′ b j }) (r i)

What is the issue with using p-faces in the definition of p? To my untrained eyes, it looks like a normal definition never going above Type₀

I see you are using agda/master!

The following would have also worked

p i = comp (λ j → P (q i)) (\ j -> p-faces i j) (r i)

with the introduction of --two-level the types of comp and transp trigger a problem with sort assignment for universe polymorphism, so some eta expansion is needed here to let Agda check the lambda at the sort it wants.

Hopefully we'll find a better solution soon.