Relevance check in reflection

[L-TChen]

While erased variables cannot be used during computation, they can be used to type-check. In particular, it should be fine to be referred to in a context. However, consider the following macro m:

extend*Context : Telescope → TC A → TC A
extend*Context []              m = m
extend*Context ((s , a) ∷ tel) m = extendContext s a (extend*Context tel m)

macro
  m : Term → TC _
  m hole = extend*Context
    (("ℓ" , arg (arg-info visible (modality relevant quantity-0))  (def₀ (quote Level)))
    ∷ ("A" , vArg (agda-sort (set (var₀ 0)))) ∷ [])
    (return tt)

When extending the context with the second variable A in the above telescope (("ℓ" , arg (arg-info visible (modality relevant quantity-0)) (def₀ (quote Level))) ∷ ("A" , vArg (agda-sort (set (var₀ 0)))) ∷ []), Agda throws an error

Variable ℓ is declared erased, so it cannot be used here
when checking that the expression ℓ has type Level

The type checker should be in the compile-time mode, in this case, so the modality should be ignored. The question is, how this can be fixed systematically?

[jespercockx]

I'd say the solution is just to add a call to workOnTypes to the line

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

Line 787 in 60e2c7a

a <- unquote a

Or is there are reason this would not be fixing the issue "systematically"?

[L-TChen]

In this particular case, it seems fine to call workOnTypes. In general, a term itself is not sufficient to determine which mode the type checker should use, so it is not clear how other primitives should interact with modalities.

By the way, we should add workOnTypes to

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

Line 780 in 015759c

extendCxt :: Arg R.Type -> UnquoteM a -> UnquoteM a

instead, right? Both of inContext and extendContext should be allowed to add types involving erased variables…

[nad]

One approach would be to let the reflection machinery generate code without any restrictions, and then check the generated code. I guess this is not how things are set up.

[L-TChen]

One approach would be to let the reflection machinery generate code without any restrictions, and then check the generated code. I guess this is not how things are set up.

It might be useful to have an operation checking a term in run-time mode, although I don't have any concrete application.

[jespercockx]

One approach would be to let the reflection machinery generate code without any restrictions, and then check the generated code. I guess this is not how things are set up.

The problem is not so much that there are restrictions on the generated code, but that arguments to built-in primitives such as extendContext need to be well-formed, lest they break internal invariants of Agda. You don't have to use these primitives if you don't want to; you can just write pure functions generating terms without any TC primitives and only unquote it at the very end.

[nad]

If code generated by macros were not trusted but checked, then it would presumably be safe to allow unrestricted use of erased definitions in macros. If the generated code satisfies all typing rules, then it does not matter if some erased name is used as part of the (compile-time) computation that generates the code. It might still be nice to catch errors early, though.

[jespercockx]

I'm not sure I understand what you are saying. Code generated by macros is already not trusted, as it always passes through the typechecker when it is unquoted. The only time you get an error "early" in the macro is when you use one of the TC primitives that take a term as input, but there it is really necessary to check that the input is well-formed because otherwise it could violate internal invariants of Agda.

[jespercockx]

Perhaps what you are saying is that we could allow the definition of a macro itself to be erased? This seems true to me and would be a good idea, but it's unrelated on whether the generated code is trusted or checked.

Edit: See #5744

[nad]

Code generated by macros is already not trusted, as it always passes through the typechecker when it is unquoted.

My understanding is that the unquoting code is trusted: if you make a mistake in the wrong part of Agda.TypeChecking.Unquote, then that could make Agda (more) inconsistent. That is perhaps to some degree unavoidable, but it appears to me as if we have not tried to make the trusted part of Agda.TypeChecking.Unquote as small as possible. Did I get that right? If not, why do you suggest using workOnTypes somewhere in Agda.TypeChecking.Unquote, instead of leaving the decision of when to switch to the "working on types" mode to the type-checker?

Perhaps what you are saying is that we could allow the definition of a macro itself to be erased? This seems true to me and would be a good idea, but it's unrelated on whether the generated code is trusted or checked.

Yes, the definition of a macro can be erased, as long as Agda checks that the generated code satisfies all typing rules (including rules related to erasure).

[jespercockx]

Ah yes, you are correct that the code in the implementation of Agda responsible for unquoting needs to be correct. In principle it just constructs the abstract syntax by running the user macro and then passes this to the typechecker, so there is not much that can go wrong, but it calls the typechecker in the wrong way (e.g. by wrapping it in a workOnTypes where it shouldn't) then that means the resulting internal syntax will be wrong. In theory there is nothing that even prevents this code from just bypassing the typechecker completely and just producing unchecked internal syntax directly, so in that sense Unquote.hs is really part of the trusted core of Agda.

Perhaps what you are imagining is that we would have a small core part of Agda that only exports the type of internal syntax as an abstract type, so it would be guaranteed that all syntax of this type is well-typed as long as this small core is correct. This is how some proof checkers are set up, but for Agda this is currently not the case.

[nad]

In theory there is nothing that even prevents this code from just bypassing the typechecker completely and just producing unchecked internal syntax directly, so in that sense Unquote.hs is really part of the trusted core of Agda.

It is for reasons like this one that I wrote "That is perhaps to some degree unavoidable" above. Even with a fully verified type-checker, if you don't call the type-checker at all, or if you manipulate the source code incorrectly before you send it to the type-checker, then you can get incorrect results.

[jespercockx]

Yes, this is a problem that cannot be solved by verifying the typechecker, but it can in principle be solved by a much more strict separation between trusted and untrusted parts of the typechecker than we have now.

[jespercockx]

Seems to me that the main issue was fixed in 5485ecf, feel free to open a new issue if there is still a problem.