de Bruijn index out of scope

[ecavallo]

I am getting the error

de Bruijn index out of scope: 17 in context [s, v, u, b, a, s, x₀, φ, p, r, n₁, n₀, ψ, φ, Γ]
CallStack (from HasCallStack):
  error, called at src/full/Agda/TypeChecking/Monad/Base.hs:3417:10 in Agda-2.6.1-9OYRc5L5C8uKq1UrNAib4P:Agda.TypeChecking.Monad.Base

with this code: https://gist.github.com/ecavallo/9f8a54554093aed0a2360194d0b89ad4. It seems related to rewrite rules, but I have not isolated very successfully.

agda --version
Agda version 2.6.1-4e989c1

[andreasabel]

Thanks for reporting. Could you shrink this down a bit? E.g. by uses of

postulate ANY : forall {a} {A : Set a} -> A

and step-wise eliminating code that does not contribute to the error?

[ecavallo]

I've done a bit of that already, but I'll go over again and see if I can improve.

[ecavallo]

Here's where I'm at now: https://gist.github.com/ecavallo/7d79f8898ffceb3a9d4db6524dcb6068

[asr]

Removed whitespace issue in the title (detected when running the closed-issues-for-milestone).