de Bruijn index out of scope when rewriting

[mikeshulman]

I'm sorry that this example is so long; I wasn't able to remove any parts of it and still reproduce the error.

{-# OPTIONS --type-in-type --rewriting #-}

infix 10 _≡_
infix 35 _＝_
infixl 40 _∙_
infixl 30 _∷_
infix 40 _⊘_
infixl 30 _▸_ _▹_

data _≡_ {A : Set} (a : A) : A → Set where
  reflᵉ : a ≡ a

{-# BUILTIN REWRITE _≡_ #-}

postulate
  _＝_ : {A : Set} → A → A → Set
  refl : {A : Set} (a : A) → (a ＝ a)

record ⊤ᵉ : Set where
  constructor []
open ⊤ᵉ

data Tel : Set

el : Tel → Set

postulate
  ℿ : (Δ : Tel) (T : el Δ → Set) → Set
  Λ : {Δ : Tel} {T : el Δ → Set} → ((x : el Δ) → T x) → ℿ Δ T

postulate
  _⊘_ : {Δ : Tel} {T : el Δ → Set} (f : ℿ Δ (λ x → T x)) (a : el Δ) → T a
  ℿβ : {Δ : Tel} {T : el Δ → Set} (f : (x : el Δ) → T x) (a : el Δ) → (Λ {Δ} f) ⊘ a ≡ f a
  ℿη : {Δ : Tel} {T : el Δ → Set} (f : ℿ Δ (λ x → T x)) → Λ (λ x → f ⊘ x) ≡ f 

{-# REWRITE ℿβ ℿη #-}

_⇨_ : Tel → Set → Set
Δ ⇨ T = ℿ Δ (λ _ → T)

postulate
  _▹_ : (Δ : Tel) (B : Δ ⇨ Set) → Set
  _∷_ : {Δ : Tel} {B : Δ ⇨ Set} (x : el Δ) → B ⊘ x → Δ ▹ B
  pop : {Δ : Tel} {B : Δ ⇨ Set} → Δ ▹ B → el Δ
  top : {Δ : Tel} {B : Δ ⇨ Set} (δ : Δ ▹ B) → B ⊘ (pop δ)
  popβ : {Δ : Tel} {B : Δ ⇨ Set} (δ : el Δ) (b : B ⊘ δ) → pop {Δ} {B} (δ ∷ b) ≡ δ

{-# REWRITE popβ #-}

postulate
  topβ : {Δ : Tel} {B : Δ ⇨ Set} (δ : el Δ) (b : B ⊘ δ) → top {Δ} {B} (δ ∷ b) ≡ b

{-# REWRITE topβ #-}

data Tel where
  ε : Tel
  _▸_ : (Δ : Tel) (A : Δ ⇨ Set) → Tel

el ε = ⊤ᵉ
el (Δ ▸ A) = Δ ▹ A

postulate
  ID : Tel → Tel
  IDε : ID ε ≡ ε
  ID▸ⁿᵈ : (Δ : Tel) (A : Set) →
    ID (Δ ▸ (Λ λ _ → A)) ≡
    ID Δ ▸ (Λ λ _ → A) ▸ (Λ λ _ → A) ▸ (Λ λ x → top (pop x) ＝ top x)
  _₀ : {Δ : Tel} → el (ID Δ) → el Δ
  _₁ : {Δ : Tel} → el (ID Δ) → el Δ

{-# REWRITE IDε ID▸ⁿᵈ #-}

postulate
  ε▸₀ⁿᵈ : (A : Set) (a₀ a₁ : A) (a₂ : a₀ ＝ a₁) →
    (_₀ {ε ▸ (Λ λ _ → A)} ([] ∷ a₀ ∷ a₁ ∷ a₂)) ≡ ([] ∷ a₀)
  ε▸₁ⁿᵈ : (A : Set) (a₀ a₁ : A) (a₂ : a₀ ＝ a₁) →
    (_₁ {ε ▸ (Λ λ _ → A)} ([] ∷ a₀ ∷ a₁ ∷ a₂)) ≡ ([] ∷ a₁)

{-# REWRITE ε▸₀ⁿᵈ ε▸₁ⁿᵈ #-}

postulate
  ＝⇨ : (Δ : Tel) (T : Set) (f g : Δ ⇨ T) →
    (f ＝ g) ≡ ℿ (ID Δ) (λ x → f ⊘ (x ₀) ＝ g ⊘ (x ₁))

{-# REWRITE ＝⇨ #-}

postulate
  reflΛⁿᵈ-const : (Δ : Tel) (T : Set) (t : T) →
    refl {ℿ Δ (λ _ → T)} (Λ λ _ → t) ≡ Λ λ _ → refl t

{-# REWRITE reflΛⁿᵈ-const #-}

postulate
  Π : (A : Set) (B : A → Set) → Set
  ƛ : {A : Set} {B : A → Set} (f : (x : A) → B x) → Π A B
  _∙_ : {A : Set} {B : A → Set} (f : Π A B) (a : A) → B a
  Πβ : {A : Set} {B : A → Set} (f : (x : A) → B x) (a : A) → (ƛ f ∙ a) ≡ f a
  Πη : {A : Set} {B : A → Set} (f : Π A B) → (ƛ (λ x → f ∙ x)) ≡ f

{-# REWRITE Πβ Πη #-}

postulate
  ＝⇒ : (A B : Set) (f g : Π A (λ _ → B)) →
    (f ＝ g) ≡ Π A (λ a₀ → Π A (λ a₁ → Π (a₀ ＝ a₁) (λ a₂ → f ∙ a₀ ＝ g ∙ a₁)))

{-# REWRITE ＝⇒ #-}

postulate
  reflƛⁿᵈ : (A B : Set) (f : Π A (λ _ → B)) →
    refl f ≡ (ƛ λ a₀ → ƛ λ a₁ → ƛ λ a₂ →
      refl {ℿ (ε ▸ (Λ λ _ → A)) (λ _ → B)} (Λ λ x → f ∙ top x) ⊘ ([] ∷ a₀ ∷ a₁ ∷ a₂))

{-# REWRITE reflƛⁿᵈ #-}

postulate
  Σ : (A : Set) (B : A → Set) → Set
  _,_ : {A : Set} {B : A → Set} (a : A) → B a → Σ A B
  fst : {A : Set} {B : A → Set} → Σ A B → A
  snd : {A : Set} {B : A → Set} (u : Σ A B) → B (fst u)
  fstβ : {A : Set} {B : A → Set} (a : A) (b : B a) → fst {A} {B} (a , b) ≡ a

{-# REWRITE fstβ #-}

record _＝U_ (A B : Set) : Set where
  field
    _//_~_ : (a : A) (b : B) → Set
open _＝U_

postulate
  ＝U : (A B : Set) → (A ＝ B) ≡ (A ＝U B)

{-# REWRITE ＝U #-}

postulate
  ＝∙ : (A : Set) (B : Π A (λ _ → Set)) (a : A) (b₀ b₁ : B ∙ a) →
    (b₀ ＝ b₁) ≡ refl B ∙ a ∙ a ∙ refl a // b₀ ~ b₁

{-# REWRITE ＝∙ #-}

postulate
  ＝Σ : (A : Set) (B : A → Set) (u v : Σ A B) →
    (u ＝ v) ≡ Σ (fst u ＝ fst v) (λ p → (refl (ƛ B) ∙ fst u ∙ fst v ∙ p // snd u ~ snd v))

{-# REWRITE ＝Σ #-}

postulate
  refl-fst : (A : Set) (B : A → Set) (u : Σ A B) → refl (fst u) ≡ fst (refl u)

{-# REWRITE refl-fst #-}

frob-refl-snd : {A : Set} (B : Π A (λ _ → Set)) (u : Σ A (λ x → B ∙ x)) → snd u ＝ snd u
frob-refl-snd B u = {!!}

In Agda 2.6.3-5d2d77a this produces

de Bruijn index out of scope: 5 in context [a₂, a₁, x, x]
CallStack (from HasCallStack):
  error, called at src/full/Agda/TypeChecking/Monad/Base.hs:4098:10 in Agda-2.6.3-K939Rz0lK6d4Qhz5rVu9uS:Agda.TypeChecking.Monad.Base

[mikeshulman]

I got a similar error elsewhere in my code:

de Bruijn index out of scope: 9 in context [x, x, x, x, x, x]
CallStack (from HasCallStack):
  error, called at src/full/Agda/TypeChecking/Monad/Base.hs:4098:10 in Agda-2.6.3-K939Rz0lK6d4Qhz5rVu9uS:Agda.TypeChecking.Monad.Base

It seems reasonably likely that this has the same or similar cause, since it cites the same line of the Agda source. If it would be helpful to have another example, let me know and I can post the second one. (It will start out with the same long setup, but the error is triggered by something different.)

(I am aware that I'm doing terrible things to subject reduction. But I would assume that even this shouldn't cause de Bruijn indices to go out of scope.)

[mikeshulman]

Would it be helpful in fixing this if I were able to make the test case smaller? (Sorry if this is a dumb question, I don't really have any idea whether the size of the triggering code affects the difficulty of tracking down a bug like this.)

[andreasabel]

Would it be helpful in fixing this if I were able to make the test case smaller?

Yes, this always helps, because focusing the trigger will usually give some idea where the bug could reside (helps understanding the test case), and, trivially, there will be less clutter if debug-printing is turned on.

[mikeshulman]

Fantastic! Thanks for fixing this, even with such a long test case. As I expected, the fix has also fixed the other similar error.

[andreasabel]

Agda 2.6.0 still said correctly:

Unsolved interaction metas at the following locations:
  /Users/abel/play/agda/bugs/Issue6003.agda:154,21-25