Panic: Pattern match failure with Setω and --without-K

[flupe]

There seem to be a regression in the current master of Agda.

The following code (where we define the equality type at Setω)

{-# OPTIONS --without-K #-}

open import Agda.Builtin.Equality
open import Agda.Primitive using (Setω)

data _≡ω_ {A : Setω} (x : A) : A → Setω where
  refl : x ≡ω x

congω : {A : Set} {B : Setω} (f : A → B)
      → ∀ {x y} → x ≡ y → f x ≡ω f y
congω f refl = refl

fails with the following message:

cong.agda:11,1-20
Panic: Pattern match failure in do expression at
src/full/Agda/TypeChecking/Primitive/Cubical.hs:2310:7-21
when checking the definition of congω

Can confirm this typechecks fine with the latest release (2.6.2.2) and with --with-K.

[flupe]

Just noticed the code fails at the same place as #6001. I also logged the types passed to toLType, giving:

toLType @14 ≡ @11 @0
toLType @14 ≡ @11 @0
toLType @13 ≡ @10 @0
toLType @13 ≡ @10 @0
toLType @11 @10 ≡ω @11 @9

As expected, the code fails because toLType does not handle things that live in Setω, just as for Prop (See #5816 and the fix #5897). I tried checking the example with the fix from #5897 and it no longer fails, so we can consider this issue to also be fixed by #5897.

[andreasabel]

Current error (after #5730 has been improved) is more benign:

Cannot generate inferred clause for congω. Case to handle:
  congω f
    (Agda.Primitive.Cubical.primHComp {.Agda.Primitive.lzero}
       {.(_ ≡ _)}
       {φ = φ}
       u
       a)
Cannot compose with type family: f x ≡ω f y.
when checking the definition of congω

[plt-amy]

Part of #6049, still an internal error to be fixed