cubicaltt crashes when replacing an 'undefined' with a 'hole'.

[xekoukou]

Replacing an undefined with a hole here results in a cubicaltt crash with error :

Hole at (52,46) in lecture4:

A : U
--------------------------------------------------------------------------------
(x : Sigma A (\(x : A) -> (y : A) -> PathP (<!0> A) x y)) -> (y : Sigma A (\(x0 : A) -> (y : A) -> PathP (<!0> A) x0 y)) -> PathP (<!0> Sigma A (\(x0 : A) -> (y0 : A) -> PathP (<!0> A) x0 y0)) x y

Checking: isPropIsEquiv
cubical: inferType: not neutral ? (A = (Sigma A ((\(x : A) -> Path B y (f x)) (A = A, B = B, f = f, y = y))))
CallStack (from HasCallStack):
  error, called at ./Eval.hs:289:8 in main:Eval

Process cubical exited abnormally with code 1