The reflection machinery does not treat the module telescope consistently

[nad]

The reflection primitives getType and getDefinition return definitions that include the module telescope. However, the quoting machinery does not in general return definitions that have been lifted to the top-level. Here is one example:

{-# OPTIONS -vdbg:5 #-}

module Bad (A : Set) where

open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

f : A → A
f x = x

macro

  m : Term → TC ⊤
  m goal =
    bindTC (getType (quote f)) λ type →
    bindTC (debugPrint "dbg" 5
              (strErr "Type of f: " ∷ termErr type ∷ [])) λ _ →
    bindTC (inferType goal) λ type →
    bindTC (quoteTC type) λ type →
    bindTC (debugPrint "dbg" 5
              (strErr "Goal type: " ∷ termErr type ∷ [])) λ _ →
    unify goal (con (quote refl) [])

_ : f ≡ f
_ = m

Output:

Type of f: (A₁ : Set₀) (z : A₁) → A₁
Goal type: def (quote _≡_)
           (arg (arg-info hidden (modality relevant quantity-ω))
            (def (quote Agda.Primitive.lzero) [])
            ∷
            arg (arg-info hidden (modality relevant quantity-ω))
            (pi
             (arg (arg-info visible (modality relevant quantity-ω)) (var 0 []))
             (abs "_" (var 1 [])))
            ∷
            arg (arg-info visible (modality relevant quantity-ω))
            (def (quote f) [])
            ∷
            arg (arg-info visible (modality relevant quantity-ω))
            (def (quote f) [])
            ∷ [])

Note that the type of f includes the module parameter, but f is not applied to the module parameter in the quoted representation of the goal type.

I think that the reflection machinery should be consistent, and always treat the module telescope in the same way. Internally f is presumably already applied to the module parameter, so I guess an active decision was taken to remove module parameters when quoting terms:

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

Lines 286 to 288 in aed62b9

	n <- getDefFreeVars x
	def !@! quoteName x
	@@ list (drop n $ conOrProjPars ++ map (quoteArg quoteTerm) ts)

Can someone explain why the reflection machinery is set up in this way? Wouldn't it make more sense to always work on the top-level, like Agda does internally?

[jespercockx]

Yes, this would be good to have a better semantics of reflection in parametrized modules. Since this is not really critical and has been a problem for a while already, I am bumping this to 2.6.4.

[andreasabel]

Considered for 2.6.3 since we already have a PR dated March 2022 that adresses this:

• Fix the reflection primitive getType ignoring module parameters #5858