Internal error with --confluence-check

[xekoukou]

An internal error has occurred. Please report this as a bug.

Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Rewriting/NonLinPattern.hs:320:28 in Agda-2.6.3-JzcsF0w6Ok8pSpuaNaFFz:Agda.TypeChecking.Rewriting.NonLinPattern

{-# OPTIONS  --confluence-check --cubical #-}

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.HLevels
open import Cubical.HITs.SetQuotients as Sq

module Test (ℓ : Level) where

private
  variable
    A B : Type ℓ
    T : A → A → Type ℓ


E : (T : A → A → Type ℓ) → (B → A) → (B → A) → Type ℓ
E T f1 f2 = ∀ x → T (f1 x) (f2 x)

dd : (B → A) / (E T) → B → A / T
dd {T = T} f = Sq.rec (isSetΠ λ _ → squash/) (λ g x → [ g x ]) l1 f where
  l1 : (a b : _ → _) → E T a b → (λ x → [ a x ]) ≡ (λ x → [ b x ])
  l1 a b r i = ?

[andreasabel]

The internal error is raised here:

agda/src/full/Agda/TypeChecking/Rewriting/NonLinPattern.hs

Lines 319 to 320 in d8ec8dd

	instance GetMatchables Term where
	getMatchables = getDefs' __IMPOSSIBLE__ singleton

[andreasabel]

Would be interesting to see whether this is a regression. @xekoukou , could you shrink your test case so that it does not use the cubical library, only the Agda.Builtin.* modules?

[xekoukou]

{-# OPTIONS  --confluence-check --cubical #-}

open import Agda.Builtin.Cubical.Path

module Test where

l1 : PathP ? ? ?
l1 i = ?

[andreasabel]

Thanks @xekoukou !
For this minimal test, 2.6.3 and 2.6.2 have the same location of the internal error. 2.6.1 has a different one, and 2.6.0 does not know about --confluence-check. So, it is not a regression.