Another de Bruijn error in rewriting

[mikeshulman]

I've done all the minimization I can manage for now. I'm sorry it's still kind of long.

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

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.Equality.Rewrite

infixl 40 _∙_
infixr 30 _,_ Σ _⇒_ Π

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (a : A) → B a → Σ A B
syntax Σ A (λ x → B) = （ x ⦂ A ）× B

fst : {A : Set} {B : A → Set} → Σ A B → A
fst (a , _) = a

snd : {A : Set} {B : A → Set} (u : Σ A B) → B (fst u)
snd (_ , b) = b

postulate
  Π : (A : Set) (B : A → Set) → Set
  𝛌 : {A : Set} {B : A → Set} (f : (x : A) → B x) → Π A B
syntax Π A (λ x → B) = （ x ⦂ A ）⇒ B

postulate
  _∙_ : {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
{-# REWRITE Πβ #-}

_⇒_ : Set → Set → Set
A ⇒ B = （ _ ⦂ A ）⇒ B

postulate
  _＝_ : {A : Set} → A → A → Set
  refl' : {A : Set} (a : A) → (a ＝ a)
  Id : {A : Set} (B : A → Set) {a₀ a₁ : A} (a₂ : a₀ ＝ a₁) (b₀ : B a₀) (b₁ : B a₁) → Set
  Id-const : (A B : Set) {a₀ a₁ : A} (a₂ : a₀ ＝ a₁) → Id {A} (λ _ → B) a₂ ≡ _＝_ {B}
  ap : {A : Set} {B : A → Set} (f : (x : A) → B x) {a₀ a₁ : A} (a₂ : a₀ ＝ a₁) → Id B a₂ (f a₀) (f a₁)
  ＝-⊤ : (u v : ⊤) → (u ＝ v) ≡ ⊤
  ＝-Σ : {A : Set} {B : A → Set} (u v : Σ A B) → (u ＝ v) ≡ （ p ⦂ fst u ＝ fst v ）× Id B p (snd u) (snd v)
{-# REWRITE Id-const ＝-⊤ ＝-Σ #-}

postulate
  Id-Π : {Δ : Set} {A : Δ → Set} {B : (x : Δ) → A x → Set}
    {δ₀ δ₁ : Δ} (δ₂ : δ₀ ＝ δ₁)
    (f₀ : Π (A δ₀) (B δ₀)) (f₁ : Π (A δ₁) (B δ₁)) →
    Id (λ x → Π (A x) (B x)) δ₂ f₀ f₁ ≡ 
    （ aₓ ⦂ （ a₀ ⦂ A δ₀ ）× （ a₁ ⦂ A δ₁ ）× Id A δ₂ a₀ a₁ ）⇒
      Id {Σ Δ A} (λ u → B (fst u) (snd u)) {δ₀ , fst aₓ} {δ₁ , fst (snd aₓ)} (δ₂ , snd (snd aₓ))
        (f₀ ∙ fst aₓ) (f₁ ∙ fst (snd aₓ))
{-# REWRITE Id-Π #-}

data Σ⁵ (A B : Set) (C : A → B → Set) (D : A → Set) (E : B → Set) : Set where
  _⸴_⸴_⸴_⸴_ : (a : A) (b : B) (c : C a b) (d : D a) (e : E b) → Σ⁵ A B C D E
open Σ⁵

module _ {A B : Set} {C : A → B → Set} {D : A → Set} {E : B → Set} where
  _!₀ : Σ⁵ A B C D E → A
  (a ⸴ b ⸴ c ⸴ d ⸴ e) !₀ = a

  _!₁ : Σ⁵ A B C D E → B
  (a ⸴ b ⸴ c ⸴ d ⸴ e) !₁ = b

  _!₂ : (u : Σ⁵ A B C D E) → C (u !₀) (u !₁)
  (a ⸴ b ⸴ c ⸴ d ⸴ e) !₂ = c

  _!⁰ : (u : Σ⁵ A B C D E) → D (u !₀)
  (a ⸴ b ⸴ c ⸴ d ⸴ e) !⁰ = d

  _!¹ : (u : Σ⁵ A B C D E) → E (u !₁)
  (a ⸴ b ⸴ c ⸴ d ⸴ e) !¹ = e

∂ : (n : Nat) (A : Set) → Set

Cube : (n : Nat) (A : Set) → ∂ n A ⇒ Set

∂ zero A = ⊤
∂ (suc n) A = Σ⁵ (∂ n A) (∂ n A) (_＝_ {∂ n A}) (Cube n A ∙_) (Cube n A ∙_)

Cube zero A = 𝛌 λ _ → A
Cube (suc n) A = 𝛌 λ a → Id (Cube n A ∙_) {a !₀} {a !₁} (a !₂) (a !⁰) (a !¹)

CUBE : (n : Nat) (A : Set) → Set
CUBE n A = Σ (∂ n A) (Cube n A ∙_)

data _≊_ (A B : Set) : Set where
  ≊[_] : (A ⇒ B ⇒ Set) → A ≊ B
open _≊_

ext : {A B : Set} (e : A ≊ B) → A → B → Set
ext ≊[ rel ] a b = rel ∙ a ∙ b

Kan : (n : Nat) → ∂ n Set ⇒ Set
Kan zero = 𝛌 λ _ → ⊤
Kan (suc zero) = 𝛌 λ A → ((A !⁰) ≊ (A !¹))
Kan (suc (suc n)) = {!!}

postulate
  kan : {n : Nat} (A : CUBE n Set) → Kan n ∙ fst A

postulate
  refl↓ : (A : Set) → ext (kan ((tt ⸴ tt ⸴ tt ⸴ A ⸴ A) , refl' A)) ≡ _＝_ {A}
  Id-∙ : {Δ : Set} {A : Δ → Set} (f : (δ : Δ) → A δ ⇒ Set)
    (a : (δ : Δ) → A δ) {δ₀ δ₁ : Δ} (δ₂ : δ₀ ＝ δ₁)
    (x₀ : f δ₀ ∙ a δ₀) (x₁ : f δ₁ ∙ a δ₁) →
    Id (λ δ → f δ ∙ a δ) δ₂ x₀ x₁ ≡ ext (kan {suc zero} ((tt ⸴ tt ⸴ tt ⸴ _ ⸴ _) , ap f δ₂ ∙ (a δ₀ , a δ₁ , ap a δ₂))) x₀ x₁
{-# REWRITE refl↓ Id-∙ #-}

frob-ap-kan : {n : Nat} {Δ : Set} {δ₀ δ₁ : Δ} (δ₂ : δ₀ ＝ δ₁)
  (A : Δ → CUBE n Set) {Ω : Δ → Set} (ω : (λ δ → Kan n ∙ fst (A δ)) ≡ Ω) →
  Id (λ δ → Kan n ∙ fst (A δ)) δ₂ (kan (A δ₀)) (kan (A δ₁))
frob-ap-kan {n} {Δ} {δ₀} {δ₁} δ₂ A refl = {!!}

The error is

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

[mikeshulman]

Here is a slightly shorter version:

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

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.Equality.Rewrite

infixl 40 _∙_
infixr 30 _,_

data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (a : A) → B a → Σ A B

fst : {A : Set} {B : A → Set} → Σ A B → A
fst (a , _) = a

snd : {A : Set} {B : A → Set} (u : Σ A B) → B (fst u)
snd (_ , b) = b

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} → A → A → Set
  refl' : {A : Set} (a : A) → (a ＝ a)
  Id : {A : Set} (B : A → Set) {a₀ a₁ : A} (a₂ : a₀ ＝ a₁) (b₀ : B a₀) (b₁ : B a₁) → Set
  Id-const : (A B : Set) {a₀ a₁ : A} (a₂ : a₀ ＝ a₁) → Id {A} (λ _ → B) a₂ ≡ _＝_ {B}
  ap : {A : Set} {B : A → Set} (f : (x : A) → B x) {a₀ a₁ : A} (a₂ : a₀ ＝ a₁) → Id B a₂ (f a₀) (f a₁)
  ＝-⊤ : (u v : ⊤) → (u ＝ v) ≡ ⊤
  ＝-Σ : {A : Set} {B : A → Set} (u v : Σ A B) → (u ＝ v) ≡ Σ (fst u ＝ fst v) (λ p → Id B p (snd u) (snd v))
{-# REWRITE Πβ Id-const ＝-⊤ ＝-Σ #-}

postulate
  Id-Π : {Δ : Set} {A : Δ → Set} {B : (x : Δ) → A x → Set}
    {δ₀ δ₁ : Δ} (δ₂ : δ₀ ＝ δ₁)
    (f₀ : Π (A δ₀) (B δ₀)) (f₁ : Π (A δ₁) (B δ₁)) →
    Id (λ x → Π (A x) (B x)) δ₂ f₀ f₁ ≡ 
    Π (Σ (A δ₀) (λ a₀ → Σ (A δ₁) (λ a₁ → Id A δ₂ a₀ a₁))) (λ aₓ →
      Id {Σ Δ A} (λ u → B (fst u) (snd u)) {δ₀ , fst aₓ} {δ₁ , fst (snd aₓ)} (δ₂ , snd (snd aₓ))
        (f₀ ∙ fst aₓ) (f₁ ∙ fst (snd aₓ)))
{-# REWRITE Id-Π #-}

data Σ⁵ (A B : Set) (C : A → B → Set) (D : A → Set) (E : B → Set) : Set where
  _⸴_⸴_⸴_⸴_ : (a : A) (b : B) (c : C a b) (d : D a) (e : E b) → Σ⁵ A B C D E
open Σ⁵

module _ {A B : Set} {C : A → B → Set} {D : A → Set} {E : B → Set} where
  _!₀ : Σ⁵ A B C D E → A
  (a ⸴ b ⸴ c ⸴ d ⸴ e) !₀ = a

  _!₁ : Σ⁵ A B C D E → B
  (a ⸴ b ⸴ c ⸴ d ⸴ e) !₁ = b

  _!₂ : (u : Σ⁵ A B C D E) → C (u !₀) (u !₁)
  (a ⸴ b ⸴ c ⸴ d ⸴ e) !₂ = c

  _!⁰ : (u : Σ⁵ A B C D E) → D (u !₀)
  (a ⸴ b ⸴ c ⸴ d ⸴ e) !⁰ = d

  _!¹ : (u : Σ⁵ A B C D E) → E (u !₁)
  (a ⸴ b ⸴ c ⸴ d ⸴ e) !¹ = e

∂ : (n : Nat) → Set

Cube : (n : Nat) → ∂ n → Set

∂ zero = ⊤
∂ (suc n) = Σ⁵ (∂ n) (∂ n) (_＝_ {∂ n}) (Cube n) (Cube n)

Cube zero _ = Set
Cube (suc n) a = Id (Cube n) {a !₀} {a !₁} (a !₂) (a !⁰) (a !¹)

data _≊_ (A B : Set) : Set where
  ≊[_] : (Π A (λ _ → Π B (λ _ → Set))) → A ≊ B

ext : {A B : Set} (e : A ≊ B) → A → B → Set
ext ≊[ rel ] a b = rel ∙ a ∙ b

Kan : (n : Nat) → Π (∂ n) (λ _ → Set)
Kan zero = {!!}
Kan (suc zero) = 𝛌 λ A → ((A !⁰) ≊ (A !¹))
Kan (suc (suc n)) = {!!}

postulate
  kan : {n : Nat} (A : Σ (∂ n) (Cube n)) → Kan n ∙ fst A

postulate
  refl↓ : (A : Set) → ext (kan ((tt ⸴ tt ⸴ tt ⸴ A ⸴ A) , refl' A)) ≡ _＝_ {A}
  Id-∙ : {Δ : Set} {A : Δ → Set} (f : (δ : Δ) → Π (A δ) (λ _ → Set))
    (a : (δ : Δ) → A δ) {δ₀ δ₁ : Δ} (δ₂ : δ₀ ＝ δ₁)
    (x₀ : f δ₀ ∙ a δ₀) (x₁ : f δ₁ ∙ a δ₁) →
    Id (λ δ → f δ ∙ a δ) δ₂ x₀ x₁ ≡ ext (kan {suc zero} ((tt ⸴ tt ⸴ tt ⸴ _ ⸴ _) , ap f δ₂ ∙ (a δ₀ , a δ₁ , ap a δ₂))) x₀ x₁
{-# REWRITE refl↓ Id-∙ #-}

frob-ap-kan : {n : Nat} {Δ : Set} {δ₀ δ₁ : Δ} (δ₂ : δ₀ ＝ δ₁) (A : Δ → Σ (∂ n) (Cube n)) (ω : A ≡ A) →
  Id (λ δ → Kan n ∙ fst (A δ)) δ₂ (kan (A δ₀)) (kan (A δ₁))
frob-ap-kan {n} {Δ} {δ₀} {δ₁} δ₂ A refl = {!!}

While trying to shrink the example, I also noticed two interesting things:

1. If I don't try to pattern-match on the equality, replacing the refl in the last line with a variable name like e, the error goes away. But,
2. If I remove the argument ω in the type declaration of frob-ap-kan, but leave the final argument on the LHS of its definition (which is thus now incorrect, with too many arguments), the error doesn't go away.

[jespercockx]

Here is a minimized test case:

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

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

postulate
  F : Set → Set → Set
  G : (Set → Set) → Set → Set → Set
  rewF : (A : Set) → F A A ≡ Set
  rewG : (A : Set → Set) (X Y : Set) → G A X Y ≡ F (A X) (A Y)
{-# REWRITE rewF rewG #-}

test : (A : Set → Set) → G A _ _
test A x = {!!}

It seems like this has something to do with the non-linearity of the rule.

[mikeshulman]

Wow, the difference between your minimizing something and my "minimizing" it is night and day. (-:O

[jespercockx]

I use a relatively mechanical technique for minimization that doesn't require a lot of actual understanding of the code (which can be a bit slower but usually still faster than actually trying to understand the code). Basically it is a heuristically guided application of the following steps:

• Enable --type-in-type, --no-termination-check, --no-positivity-check, --no-projection-like, --no-fast-reduce
• Disable unused flags
• Remove unused imports
• Copy definitions from imported modules (other than Agda.Builtin modules)
• Delete unused definitions
• Turn functions into postulates
• Inline functions
• Remove clauses from definitions
• Replace patterns by _ if they are not used
• Replace types by Set
• Delete unused arguments to functions or constructors
• Remove dependencies from types
• Replace (sub)terms by w/e where w/e : ∀ {ℓ} {A : Set ℓ} → A is a postulate
• Make implicit arguments explicit
• Replace wildcards _ in terms by their solution

There's probably more things depending on the test case, but here these were sufficient to get to the minimized example I gave. Perhaps I should write down a proper guide on how to minimize test cases somewhere :)

[sattlerc]

A lot of these heuristic transformation could probably be implemented programmatically. Maybe an idea for a student project?

[andreasabel]

I think I do everything but this step:

• Enable --type-in-type, --no-termination-check, --no-positivity-check, --no-projection-like, --no-fast-reduce

Usually levels can be removed without resorting to the hammer Type:Type.

{-# OPTIONS --rewriting #-}

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

postulate
  S : Set
  F : Set → Set → Set
  G : (Set → Set) → Set → Set → Set
  rewF : (A : Set) → F A A ≡ S
  rewG : (A : Set → Set) (X Y : Set) → G A X Y ≡ F (A X) (A Y)
{-# REWRITE rewF rewG #-}

test : (A : Set → Set) → G A _ _
test A x = {!!}

But --no-projection-like, --no-fast-reduce could be a good heuristics to start...

[jespercockx]

Ok, I have a fix for the minimized test case I posted, but this did not yet fix the OP. Here is a new minimized example that seems to be triggering a slightly different bug:

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

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

postulate
  Id : (Set → Set) → Set → Set → Set
  ext : Set → Set → Set
  refl↓ : (A : Set) → ext A A ≡ Set
  Id-∙ : (A : Set → Set) (X Y : Set) → Id A X Y ≡ ext (A X) (A Y)
{-# REWRITE refl↓ Id-∙ #-}

frob-ap-kan : (A : Set → Set) → Set ≡ Set → Id A _ _
frob-ap-kan A refl = {!!}

[nad]

A lot of these heuristic transformation could probably be implemented programmatically. Maybe an idea for a student project?

I think it would be great if we had a tool which helped us with test case shrinking. However, note that it is not always trivial to know if a piece of code is handled correctly or not. When I shrink test cases for regressions I sometimes test the code using both the development version and the most recent release, and if I get the same result from both, then I backtrack.

[mikeshulman]

Thanks! This also fixes my original unminimized code.

I had thought of some of those transformations myself, but not all. A proper guide to minimization would be great, but even just that list is helpful to have. Maybe it could be made more available somewhere, like in (or linked from) the instructions for submitting a github issue?

[andreasabel]

OP worked in 2.6.0, fails in 2.6.1 and 2.6.2.