[Agda] TC: `freshName`s are not in scope

[Musa Al-hassy]

Dear Agda Community,

When I attempt to unquote a declaration where a `Name` is not provided, but
instead created using `freshName`,
the resulting function is not in scope. I want to create functions based on
lists of terms, so the option of passing
in names is not ideal.

Here is the current scenerario ---a minimal example is below, and attached.

{- Works, but is undesirable }
unquoteDecl identity = ⋯make the identity function⋯

{- Desirable but "identity" is not in scope. -}
unquoteDecl = do η ← freshName "identity"
                 ⋯make the identity function⋯

Moreover, regarding reflection is it possible to unquote a datatype or a
record declaration?
Does anyone have any documentation on how to use the /current/,
or a /recent/, version of Agda's reflection mechanism.
( My personal notes can be found here:
   https://github.com/alhassy/gentle-intro-to-reflection )

Best regards,

Musa Al-hassy

------------------------------------------------------------------------
module tangled where

open import Relation.Binary.PropositionalEquality hiding ([_])
open import Data.List as List
open import Reflection
open import Data.Nat
open import Data.Unit

_>>=_        : ∀ {a b} {A : Set a} {B : Set b} → TC A → (A → TC B) → TC B
_>>=_ = bindTC
_>>_        : ∀ {a b} {A : Set a} {B : Set b} → TC A → TC B → TC B
_>>_  = λ p q → p >>= (λ _ → q)

{- 𝓋isible 𝓇elevant 𝒶rgument -}
𝓋𝓇𝒶 : {A : Set} → A → Arg A
𝓋𝓇𝒶 = arg (arg-info visible relevant)

unquoteDecl
  = do η ← freshName "identity"
       τ ← quoteTC (∀ {A : Set} → A → A)
       declareDef (𝓋𝓇𝒶 η) τ
       defineFun η [ clause [ 𝓋𝓇𝒶 (var "x") ] (var 0 []) ]

{-
-- “identity” is not in scope!?
_ : ∀ {x : ℕ}  →  identity x  ≡  x
_ = refl
-}
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190516/58411270/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: tangled.agda
Type: application/octet-stream
Size: 897 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190516/58411270/attachment.obj>