Macro generates variable with out-of-scope name

[jespercockx]

I'm using some simple macros to generate parts of my agda2hs code. However, I noticed this can lead to terms being generated that refer to unbound variables. Here is a minimal example:

open import Haskell.Prelude
open import Agda.Builtin.Reflection

macro
  solve : Term → TC ⊤
  solve = unify (var 0 [])

test : Int → Int
test _ = solve

{-# COMPILE AGDA2HS test #-}

This is accepted by agda2hs and produces the following illegal Haskell code:

test :: Int -> Int
test _ = x

We should enforce that a variable with an unusable name such as _ is not used in any part of the generated Haskell code.