Wrong de Bruijn indices for reflected variables inside an extended context

[L-TChen]

Consider the following macro.

module _ where

open import Agda.Builtin.Reflection
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Primitive

open import Data.Nat.Show -- from the standard library

_>>=_  = bindTC
return = returnTC

macro
  test : List Nat → Term → TC _
  test n _ = do
    extendContext (arg (arg-info visible relevant) (quoteTerm Nat)) do
      var i [] ← quoteTC n
        where _ → typeError (strErr "impossible1" ∷ [])
      var j [] ← unquoteTC {A = Nat} (var 0 []) >>= quoteTC 
        where _ → typeError (strErr "impossible2" ∷ [])
      typeError (strErr (show i) ∷ strErr (show j) ∷ [])

If we execute the above code in Emacs by normalising

\ n -> test n

then we will get the following message

1,7-13
0 0
when checking that the expression unquote (test t) has type
_40 (t = t)

showing that the de Bruijn indices i and j are both 0. However, i should be 1.

[nad]

Shouldn't i be 2?

[L-TChen]

The last argument to a macro does not get into the context, as getContext shows only two variables inside the extended context.

If the last argument should be inside the context, then we shall open another issue for it.

[UlfNorell]

The arguments to the macro doesn't matter, it's the context of the call site that's relevant. So you'd expect:

λ a b c → test a  -- 3 0
λ a b c → test b  -- 2 0
λ a b c → test c  -- 1 0

[nad]

The arguments to the macro doesn't matter, it's the context of the call site that's relevant.

Right, of course.

[L-TChen]

I'd like to fix this myself. If I understand it correctly, I shall start from the following function, right?

agda/src/full/Agda/TypeChecking/Unquote.hs

Lines 635 to 636 in af3c1cf

	tcQuoteTerm :: Term -> UnquoteM Term
	tcQuoteTerm v = liftTCM $ quoteTerm =<< process v

[UlfNorell]

Yes.

[mefff]

Do you think this bug is related to the following issue? Here, we are extending the context with a Set, and then with an element of the set (i.e., var 0). But when we try to unquote the element (again, var 0), we get an error from de Bruijn indices. From our understanding, it seems that the elements in the context are not being lifted to acomodate to the new variable, is that correct?

Macro:

macro
  fail : Term → TC ⊤
  fail hole = do
    st ← quoteTC Set
    t ← extendContext (vArg st) (do
      v ← unquoteTC {A = Set} $ var₀ zero
      extendContext (vArg (var₀ zero)) (do
        unquoteTC {A = v} $ var₀ zero
        returnTC tt
        )
      )
    u ← quoteTC {A = ⊤} t
    unifyTC hole u

When normalizing fail, it fails with

1,1-5
_ !=< _ of type Set
(because one has de Bruijn index 1 and the other 0)
when checking that the expression _ has type _

[L-TChen]

Yes. If you observe the de Bruijn index for v by debugPrint or typeError, then you will find that it is 0 instead of 1.

The problem is that the de Bruijn index is assigned and fixed when Agda transforms the reflected or abstract syntaxes to the internal syntax, and quoteTC just returns the index in the internal syntax.

It is not obvious to me how this can be fixed without changing Term. It looks like reflected syntax shall contain the context so that a variable is always valid (since inContext can empty the current context). Does it make sense, @UlfNorell?

I will check contextual modal type theory as well ...

[mefff]

Now that I think of it, wouldn't it suffice to just lift the indices of the continuation by 1?

[mefff]

(@beta-ziliani talking here: I don't think CMTT is the answer...)

[L-TChen]

Huh, that was what I thought initially. Hope I am wrong.

Agda provides not only extendContext but also inContext which can set an arbitrary valid context, e.g., an empty context. Following the idea of lifting the indices, if we quoted a variable from the call site but in an empty context set by inContext, then the variable would not be quotable. Is this behaviour intended?

I am not familiar with semantics of type theory with elaborator reflection. If you know any reference on this, please let me know.

[beta-ziliani]

Sorry, I'm missing the point about inContext. Can you be more specific?

[L-TChen]

Okay, maybe a concrete macro. The question is what the intended behaviour of the following macro is.

postulate
  whatever : ∀ {a} {A : Set a} → A
  
macro
  f : Term → TC ⊤
  f hole = do
    extendContext (vArg (quoteTerm ℕ)) do
     x ← unquoteTC {A = ℕ} (var₀ 0)
     inContext [] do
       var₀ i ← quoteTC x -- what is `i` here?
         where _ → whatever
       typeError (strErr (show i) ∷ [])

For now, Agda shows 0 referring to the outer context containing solely ℕ. If it updates the index according to the context, then x will cause type checking error.

[beta-ziliani]

I would expect it to fail, but perhaps I'm missing some point here. @UlfNorell ?

[L-TChen]

Alright, I overthought the problem. I will just increase the index inside extendContext, i.e. indices in m.

agda/src/full/Agda/TypeChecking/Unquote.hs

Lines 665 to 668 in af3c1cf

	tcExtendContext :: Term -> Term -> UnquoteM Term
	tcExtendContext a m = do
	a <- unquote a
	extendCxt a (evalTCM m)

As for inContext, it seems to me that any variable in the original context shouldn't be quotable in the new context.

[gallais]

These days the interaction test case corresponding to this issue
contains an internal error.

https://github.com/agda/agda/blob/4a5bcdfe4b13a79fcb9bc5d5a9f2a44c969376c3/test/interaction/Issue3831.out

This does not appear to have been intended by the original commit and
was introduced by 27a1a2a (and then we have close to a dozen commits
dutifully updating the line number the internal error references 🤣).

So I'm reopening this issue.

[gallais]

Also, I am not sure why we have both __IMPOSSIBLE__ and __UNREACHABLE__.
The latter seems to only be used at the source of this internal error
in Agda.TypeChecking.Unquote.

[L-TChen]

This does not appear to have been intended by the original commit and
was introduced by 27a1a2a (and then we have close to a dozen commits
dutifully updating the line number the internal error references 🤣).

It looks like this __UNREACHABLE__ is actually intended, since the variable (de Bruijn index 0 referring to the variable introduced by Extendcontext) escapes its scope. Do you agree?

Also, I am not sure why we have both __IMPOSSIBLE__ and __UNREACHABLE__.

As far as I understand, __UNREACHABLE__ is not really a bug but a feature for reporting an incorrect de Bruijn index (or something similar).

[gallais]

If the error comes from a user mistake when writing code on the reflected
syntax then there is no point mentioning the source file and position of the
feature in Agda: we should mention the source file and position of the user's
mistake!

[L-TChen]

Agree! Make another PR to change the behaviour of __UNREACHABLE__?

[andreasabel]

I think the (now only) use of __UNREACHABLE__ in Unquote.hs is not what I intended when I added __UNREACHABLE__. My use pattern was:

verboseS "tc.foo" 10 $
  reportSLn "" 10 "Bar"
  __UNREACHABLE__

So, the idea was that I intend to trigger a crash with a certain verbosity setting when this program point is reached. The idea was that I wanted to make sure that a certain test case does not reach a certain program location.
Please do not change the behavior of __UNREACHABLE__, just do not use it in this case.

[L-TChen]

Please do not change the behavior of __UNREACHABLE__, just do not use it in this case.

Okay, so I will invent another kind of __IMPOSSIBLE__ to report the position.

[jespercockx]

Do we really need a test case that refers to a specific line in the Agda source code? It changes with practically every major commit, which makes it very hard to avoid conflicts when people are working on multiple branches at the same time.

[UlfNorell]

Indeed it should not report the position. The correct fix is to check the debruijn indices explicitly (rather than strengthen blindly), and issue a proper type error if they're bad.

[L-TChen]

Do we really need a test case that refers to a specific line in the Agda source code?

No, we don't. Based on the discussion with @gallais and @andreasabel, the fix will be the one suggested by @UlfNorell.

[ I just need to wait for my work laptop to arrive and work on it. I can't do this on my almost a decade old laptop. ]