[Bug] de Bruijn index is not in scope in the context

[ana-pantilie]

On #14 (commit 11ad0f5), when deriving Show for the CoC' type I'm getting:

/home/ana/Workspace/IOG/plutus/plutus-metatheory/src/VerifiedCompilation.lagda.md:236,1-258,8
de Bruijn index 5 is not in scope in the context
{t : Term} {t₁ : Term}
(z
 : Pointwise (Translation' CoC')
   (VerifiedCompilation.con1-1 (VerifiedCompilation.con1-0 t))
   (VerifiedCompilation.con1-1 (VerifiedCompilation.con1-0 t₁)))
(_
 : Pointwise (Translation' CoC') (VerifiedCompilation.con1-1 t₁)
   (VerifiedCompilation.con1-1 t))

The code is the following:

data Term : Set where
  con0 : Term
  con1 : Term -> L.List Term → Term

Relation' = Term → Term → Set₁

data Translation' (R : Relation') : Term → Term → Set₁ where
  constr'
    : {xs xs' : L.List Term}
    → (x x' : Term)
    → Pointwise (Translation' R) xs xs'
    → Translation' R (con1 x xs) (con1 x' xs')
  isTranslation' : {ast ast' : Term} → R ast ast' → Translation' R ast ast'

data CoC' : Relation' where
  isCoC'
    : (ft ft' tt tt' : L.List (Term))
    → Pointwise (Translation' CoC') ft ft'
    → Pointwise (Translation' CoC') tt tt'
    → CoC' (con1 (con1 con0 ft) tt') (con1 (con1 con0 ft') tt)

unquoteDecl
    Show-CoC
  =
    derive-Show 
      ((quote CoC' S., Show-CoC)
      L.∷ L.[]
      )

One hint might be that it starts failing after adding the second Pointwise argument (Pointwise (Translation' CoC') tt tt') to isCoC'.

[WhatisRT]

Smaller example:

  data Tm : Set where
    con : Tm -> Tm → Tm

  unquoteDecl Show-Tm = derive-Show [ (quote Tm , Show-Tm) ]

  data CoC : Tm → Set where
    isCoC : (ft tt : Tm) → CoC (con ft tt)

  unquoteDecl Show-CoC = derive-Show ((quote CoC , Show-CoC) ∷ [])

[ana-pantilie]

Adding {-# OPTIONS --no-forcing #-} as you suggested gets rid of the original error, but I am now running into a type error, similar to the following:

data Term : Set where
  con0 : Term

Relation' = Term → Term → Set₁

data Translation' (R : Relation') : Term → Term → Set₁ where
  constr'
    : (x x' : Term)
    → Translation' R x x'

data CoC' : Relation' where
  isCoC'
    : (t1 t2 : Term)
    → Translation' CoC' t1 t2
    → CoC' con0 con0

unquoteDecl
    Show-CoC
  =
    derive-Show 
      ((quote CoC' S., Show-CoC)
      L.∷ L.[]
      )

results in:

Emacs v2.7.0
Error
/home/ana/Workspace/IOG/plutus/plutus-metatheory/src/VerifiedCompilation.lagda.md:232,1-255,8
Term → Term → Set₁ !=< Set _ℓ_322
when checking that the inferred type of an application
  Term → Term → Set₁
matches the expected type
  Set _ℓ_322