Agda forgets parameter names in function types

[pvdstel]

Hi! I'm currently working on macros in Agda, and it appears that the names of parameters in function types are lost in some cases. This observation was made when using Agda interactively.

The code below defines a macro that prints the normalised type of the hole it acts on, and then returns a message indicates the macro has finished. Loading the file, placing the cursor in the holes, and triggering the Elaborate and Give command to execute the macro results in the following output to the debug buffer:

• (z : ℕ) → ℕ for the first two holes.
• (a : ℕ) → ℕ for the last hole.

It appears that the name is erased from the first type, (a : ℕ) → ℕ. The second type does not specify a name for the parameter, so I assume Agda automatically fills it in. The third type retains the parameter name.

Is this intentional behavior, a bug, or something else? If desired, I also have a version that demonstrates the issue without the debug buffer 🙂

Information
Agda version: 2.6.2
Platform: Ubuntu 20.04 on WSL2, Windows 10 x64

{-# OPTIONS -v dbg:50 #-}

open import Data.Bool
open import Data.List
open import Data.Nat
open import Data.Unit
open import Function
open import Reflection
open import Reflection.TypeChecking.Monad

macro
  printType : Term → TC ⊤
  printType hole = 
    do
      t1 ← withNormalisation true $ inferType hole
      debugPrint "attic" 0 [ termErr t1 ]
      typeError [ strErr "Print test executed to end." ]

-- Test with a type alias.
ℕ-func = (a : ℕ) → ℕ

testIntro1 : (a : ℕ) → ℕ
testIntro1 = {! printType  !}
testIntro2 : ℕ → ℕ
testIntro2 = {! printType  !}
testIntro3 : ℕ-func
testIntro3 = {! printType  !}

[jespercockx]

Thanks for reporting! I can reproduce the problem on my system. Here's a minimized version that doesn't depend on the standard library, for testing purposes:

open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.Unit
open import Agda.Builtin.Reflection

macro
  printType : Term → TC ⊤
  printType hole = bindTC (inferType hole) λ t → typeError (termErr t ∷ [])

test1 : (a : Nat) → Nat
test1 = {! printType  !}

test2 : (a : Bool) → Bool
test2 = {! printType  !}

Two interesting things to note:

• You only get the wrong name for the argument when running the macro in interactive mode using C-c C-m, when you use C-c C-space instead you get the right one.
• The name that Agda generates seems to depend on the type of the argument: in test1 you get the type (n : Nat) → Nat but in test2 you get (b : Bool) → Bool

This is quite an interesting one.

[jespercockx]

Actually when you just load the file without running any macros, you can already see that something is wrong:

?0 : Nat → Nat
?1 : Bool → Bool

Agda seems to have forgotten the name that was used in the function type.

EDIT: Although that doesn't explain the difference between C-c C-m and C-c C-space.

[andreasabel]

Agda seems to have forgotten the name that was used in the function type.

Not really, but it decides to print Pi-types as non-dependent if they are non-dependent:

agda/src/full/Agda/Syntax/Translation/InternalToAbstract.hs

Lines 529 to 531 in 756ac77

	I.Pi a b -> case b of
	NoAbs _ b'
	| visible a -> uncurry (A.Fun $ noExprInfo) <$> reify (a, b')

[jespercockx]

Right, you are correct. The fact remains that you should be able to access the name that the user gave from the reflection API even if it is not shown when printing the type. (On a side note, perhaps we should print the type as the user gave it instead of discarding the name annotation??)