Internal bug: TypeChecking/Sort

[txa]

An internal error has occurred. Please report this as a bug.
Location of the error: IMPOSSIBLE, called at src/full/Agda/TypeChecking/Sort.hs:211:36 in Agda-2.6.3-AGOdYf8ESdVHo914L0TbhF:Agda.TypeChecking.Sort

Here is the file
https://agda.zulipchat.com/user_uploads/23881/mz_RZr2xy0DPK73zgM48t2WX/Shallow.agda

We are a bit stuck on this in the moment :-(

[jespercockx]

Thanks for reporting. Here's the file contents for easy reference:

{-# OPTIONS --type-in-type --rewriting #-}
open import Data.Unit
open import Data.Product
open import Relation.Binary.PropositionalEquality

coe : {A B : Set} → A ≡ B → A → B
coe refl x = x

{-# BUILTIN REWRITE _≡_ #-}

Tel = Set
U = Set

variable
  Δ : Tel
  A B : Δ → U
  δ₀ δ₁ : Δ

postulate
  IdTel : (Δ : Tel)(δ₀ δ₁ : Δ) → Tel
  Id : (A : Δ → U){δ₀ δ₁ : Δ}(δ₂ : IdTel Δ δ₀ δ₁) → A δ₀ → A δ₁ → U
  ap : {A : Δ → U}(a : (δ : Δ) → A δ)
       → {δ₀ δ₁ : Δ}(δ₂ : IdTel Δ δ₀ δ₁) → Id A δ₂ (a δ₀) (a δ₁)

  idTel-unit : IdTel ⊤ tt tt ≡ ⊤
  idTel-sigma : {a₀ : A δ₀}{a₁ : A δ₁}
                → IdTel (Σ Δ A) (δ₀ , a₀) (δ₁ , a₁)
                  ≡ Σ (IdTel Δ δ₀ δ₁) (λ δ₂ → Id A δ₂ a₀ a₁)
  {-# REWRITE idTel-unit  idTel-sigma #-}

  id-u : {A₀ A₁ : U}{δ₂ : IdTel Δ δ₀ δ₁}
         → Id {Δ = Δ}(λ _ → U) δ₂ A₀ A₁ ≡ (A₀ → A₁ → U)

  {-# REWRITE id-u #-}

  id-ap : {δ₂ : IdTel Δ δ₀ δ₁}{a₀ : A δ₀}{a₁ : A δ₁}
          → Id A δ₂ a₀ a₁ ≡ ap {A = λ _ → U} A δ₂ a₀ a₁

  ap-sigma : {δ₂ : IdTel Δ δ₀ δ₁}{a₀ : A δ₀}{a₁ : A δ₁}
             {B : (δ : Δ) → A δ → U}
             {b₀ : B δ₀ a₀}{b₁ : B δ₁ a₁}→
             ap {Δ = Δ}{A = λ _ → U} (λ δ → Σ (A δ) (B δ))
                δ₂ (a₀ , b₀) (a₁ , b₁) ≡
                Σ (Id A δ₂ a₀ a₁) λ a₂ → Id {Δ = Σ Δ A} (λ (δ , a) → B δ a) (δ₂ , a₂) b₀ b₁

  {-# REWRITE ap-sigma #-}
  {-# REWRITE id-ap #-}

  ap-proj₁ : {δ₂ : IdTel Δ δ₀ δ₁}
             {B : (δ : Δ) → A δ → U}
             {ab : (δ : Δ) → Σ (A δ) (B δ)}
             → ap {Δ = Δ}{A = A}(λ δ → proj₁ (ab δ)) δ₂
               ≡ proj₁ (ap ab δ₂)

[gallais]

Replacing the last line in the type of ap-proj1 with

             → ? ≡ proj₁ (ap ab δ₂)`

leads to a different error:

src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs:168:7-51: Non-exhaustive patterns in Pi a b

The partially applied LHS:

             → ap {Δ = Δ} {A = A} (λ δ → proj₁ (ab δ)) {δ₀} {δ₁} ≡ {!!}

does show that the hole on the RHS has a pi type but as soon as you apply the LHS (even to a hole)
you get the internal error.

[jespercockx]

The root cause seems to be a non-confluence in the rewrite rules: the type Id {Δ} (λ _ → Set) {δ₀} {δ₁} δ₂ A₀ A₁ is rewritten using the rule id-ap to ap {Δ} {λ _ → U} (λ _ → Set) {δ₀} {δ₁} δ₂ A₀ A₁ (which is not a pi type) while it could also be rewritten using the rule id-u to A₀ → A₁ → U (which is a pi type). This breaks some internal assumption of the Agda typechecker and causes the internal error. The following variant works:

{-# OPTIONS --type-in-type --rewriting --confluence-check #-}
open import Data.Unit
open import Data.Product
open import Relation.Binary.PropositionalEquality

coe : {A B : Set} → A ≡ B → A → B
coe refl x = x

{-# BUILTIN REWRITE _≡_ #-}

Tel = Set
U = Set
{-# INLINE Tel #-}
{-# INLINE U #-}

variable
  Δ : Tel
  A B : Δ → U
  δ₀ δ₁ : Δ

postulate
  IdTel : (Δ : Tel)(δ₀ δ₁ : Δ) → Tel
  Id : (A : Δ → U){δ₀ δ₁ : Δ}(δ₂ : IdTel Δ δ₀ δ₁) → A δ₀ → A δ₁ → U
  ap : {A : Δ → U}(a : (δ : Δ) → A δ)
       → {δ₀ δ₁ : Δ}(δ₂ : IdTel Δ δ₀ δ₁) → Id A δ₂ (a δ₀) (a δ₁)

  idTel-unit : IdTel ⊤ tt tt ≡ ⊤
  idTel-sigma : {a₀ : A δ₀}{a₁ : A δ₁}
                → IdTel (Σ Δ A) (δ₀ , a₀) (δ₁ , a₁)
                  ≡ Σ (IdTel Δ δ₀ δ₁) (λ δ₂ → Id A δ₂ a₀ a₁)
  {-# REWRITE idTel-unit  idTel-sigma #-}

  id-u : {A₀ A₁ : U}{δ₂ : IdTel Δ δ₀ δ₁}
         → Id {Δ = Δ}(λ _ → U) δ₂ A₀ A₁ ≡ (A₀ → A₁ → U)

  {-# REWRITE id-u #-}

  id-ap : {δ₂ : IdTel Δ δ₀ δ₁}{a₀ : A δ₀}{a₁ : A δ₁}
          → Id A δ₂ a₀ a₁ ≡ ap {A = λ _ → U} A δ₂ a₀ a₁

  ap-u : {A₀ A₁ : U} {δ₂ : IdTel Δ δ₀ δ₁}
         → ap {Δ = Δ} {A = λ _ → U} (λ _ → Set) {δ₀} {δ₁} δ₂ A₀ A₁ ≡ (A₀ → A₁ → U)

  {-# REWRITE ap-u #-}

  ap-sigma : {δ₂ : IdTel Δ δ₀ δ₁}{a₀ : A δ₀}{a₁ : A δ₁}
             {B : (δ : Δ) → A δ → U}
             {b₀ : B δ₀ a₀}{b₁ : B δ₁ a₁}→
             ap {Δ = Δ}{A = λ _ → U} (λ δ → Σ (A δ) (B δ))
                δ₂ (a₀ , b₀) (a₁ , b₁) ≡
                Σ (Id A δ₂ a₀ a₁) λ a₂ → Id {Δ = Σ Δ A} (λ (δ , a) → B δ a) (δ₂ , a₂) b₀ b₁

  {-# REWRITE ap-sigma #-}
  {-# REWRITE id-ap #-}

  ap-proj₁ : {δ₂ : IdTel Δ δ₀ δ₁}
             {B : (δ : Δ) → A δ → U}
             {ab : (δ : Δ) → Σ (A δ) (B δ)}
             → ap {Δ = Δ}{A = A}(λ δ → proj₁ (ab δ)) δ₂
               ≡ proj₁ (ap ab δ₂)

Note that I added a rule ap-u and also added INLINE pragmas for Tel and U (this seems to be needed to make the confluence checker happy).

Of course Agda should not throw an internal error even if confluence is broken, but at least this hopefully helps to work around the problem.

[jespercockx]

Related: #5396

[txa]

Hi Jasper,

Thank you very much. Now I have the strange situation that a file that didn’t terminate terminates when adding the –confluence-check but not without it?!

Cheers,
Thorsten

{-# OPTIONS --rewriting --confluence-check #-}
--{-# OPTIONS --rewriting #-}

open import Data.Unit
open import Data.Product
open import Relation.Binary.PropositionalEquality

coe : {A B : Set} → A ≡ B → A → B
coe refl x = x

{-# BUILTIN REWRITE _≡_ #-}

data Tel : Set
-- Tel = Set
ElT : Tel → Set

{-# NO_UNIVERSE_CHECK #-}
{-# NO_POSITIVITY_CHECK #-}
{-
record U : Set where
  constructor code
  field
    El : Set
open U
-}

data U : Set
El : U → Set
data U  where
  u : U
  ΣU : (A : U) → (El A → U) → U
  ΠU : (A : U) → (El A → U) → U

infixr 5 _⇒_
_⇒_ : U → U → U
A ⇒ B = ΠU A (λ _ → B)

El u = U
El (ΣU A B) = Σ (El A) λ a → El (B a)
El (ΠU A B) = (a : El A) → El (B a)

data Tel where
  ⊤T : Tel
  _+_ : (Δ : Tel)(A : ElT Δ → U) → Tel

ElT ⊤T = ⊤
ElT (Δ + A) = Σ (ElT Δ) (λ δ → El (A δ))


variable
  Δ : Tel
  A B : ElT Δ → U
  δ₀ δ₁ : ElT Δ

postulate

  IdTel : (Δ : Tel)(δ₀ δ₁ : ElT Δ) → Tel
  Id : (A : ElT Δ → U){δ₀ δ₁ : ElT Δ}(δ₂ : ElT (IdTel Δ δ₀ δ₁)) → El (A δ₀) → El (A δ₁) → U


postulate
  ap : {A : ElT Δ → U}(a : (δ : ElT Δ) → El (A δ))
       → {δ₀ δ₁ : ElT Δ}(δ₂ : ElT (IdTel Δ δ₀ δ₁)) → El (Id A δ₂ (a δ₀) (a δ₁))


  idTel-unit : IdTel ⊤T tt tt ≡ ⊤T
  idTel-sigma : {δ₀ δ₁ : ElT Δ}{a₀ : El (A δ₀)}{a₁ : El (A δ₁)}
                → IdTel (Δ + A) (δ₀ , a₀) (δ₁ , a₁)
                  ≡ (IdTel Δ δ₀ δ₁) + (λ δ₂ → Id A δ₂ a₀ a₁)
  {-# REWRITE idTel-unit  idTel-sigma #-}

postulate
  id-u : {A₀ A₁ : U}{δ₀ δ₁ : ElT Δ}{δ₂ : ElT (IdTel Δ δ₀ δ₁)}
           → Id {Δ = Δ}(λ _ → u) δ₂ A₀ A₁ ≡ A₀ ⇒ A₁ ⇒ u

  {-# REWRITE id-u #-}


postulate

  id-ap-u : {A₀ A₁ : U}{δ₀ δ₁ : ElT Δ}{δ₂ : ElT (IdTel Δ δ₀ δ₁)}
         → ap {Δ = Δ}{A = λ _ → u} (λ _ → u) δ₂ A₀ A₁ ≡ A₀ ⇒ A₁ ⇒ u 

  {-# REWRITE id-ap-u #-}


  id-ap : {δ₀ δ₁ : ElT Δ}{δ₂ : ElT (IdTel Δ δ₀ δ₁)}{A : ElT Δ → U}{a₀ : El (A δ₀)}{a₁ : El (A δ₁)}
          → Id {Δ = Δ} A δ₂ a₀ a₁ ≡ ap {Δ = Δ} {A = λ _ → u} A δ₂ a₀ a₁

  {-# REWRITE id-ap #-}

{-
  Id-sigma : {δ₀ δ₁ : ElT Δ}{δ₂ : ElT (IdTel Δ δ₀ δ₁)}{A : ElT Δ → U}{a₀ : El (A δ₀)}{a₁ : El (A δ₁)}
             {B : (δ : ElT Δ) → El (A δ) → U}
             {b₀ : El (B δ₀ a₀)}{b₁ : El (B δ₁ a₁)} →
             Id {Δ = Δ} (λ δ → ΣU (A δ) (B δ))
                     δ₂ (a₀ , b₀) (a₁ , b₁) ≡
             ΣU (Id {Δ = Δ} A δ₂ a₀ a₁) λ a₂ → Id {Δ = Δ + A} (λ (δ , a) → B δ a) (δ₂ , a₂) b₀ b₁


  {-# REWRITE Id-sigma #-}  
-}

  ap-sigma : {δ₀ δ₁ : ElT Δ}{δ₂ : ElT (IdTel Δ δ₀ δ₁)}{A : ElT Δ → U}{a₀ : El (A δ₀)}{a₁ : El (A δ₁)}
             {B : (δ : ElT Δ) → El (A δ) → U}
             {b₀ : El (B δ₀ a₀)}{b₁ : El (B δ₁ a₁)} →
             ap {Δ = Δ} (λ δ → ΣU (A δ) (B δ))
                     δ₂ (a₀ , b₀) (a₁ , b₁) ≡
             ΣU (ap {Δ = Δ} A δ₂ a₀ a₁) λ a₂ → ap {Δ = Δ + A} (λ (δ , a) → B δ a) (δ₂ , a₂) b₀ b₁


  {-# REWRITE ap-sigma #-}  

{-
  ap-proj₁ : {δ₀ δ₁ : ElT Δ}{δ₂ : ElT (IdTel Δ δ₀ δ₁)}
             {A : ElT Δ → U}{B : (δ : ElT Δ) → El (A δ) → U}
             {ab : (δ : ElT Δ) → El (ΣU (A δ) (B δ))}
             → ap {Δ = Δ}{A = A}(λ δ → proj₁ (ab δ)) δ₂
               ≡ proj₁ (ap {Δ = Δ}{A = λ δ → ΣU (A δ) (B δ)} ab δ₂)
-}
  ap-proj₁ : {δ₀ δ₁ : ElT Δ}{δ₂ : ElT (IdTel Δ δ₀ δ₁)}
             {A : ElT Δ → U}{B : (δ : ElT Δ) → El (A δ) → U}
             {ab : (δ : ElT Δ) → El (ΣU (A δ) (B δ))}
             → proj₁ (ap {Δ = Δ}{A = λ δ → ΣU (A δ) (B δ)} ab δ₂)
               ≡ ap {Δ = Δ}{A = A}(λ δ → proj₁ (ab δ)) δ₂

  {-# REWRITE ap-proj₁ #-}


    

[jespercockx]

That's strange, I can't reproduce the problem here: it terminates with or without --confluence-check.

[andreasabel]

Cherry-picked onto maint-2.6.2, scheduled for 2.6.2.1.