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

[Jesper Cockx]

Hi Musa,

What you're trying to do is currently not possible because of limitations
of Agda's scope checker: it scope checks the *complete* file before any
typechecking can happen or any reflection code is run, so any names
generated through reflection appear 'too late' to be in scope.

For the same reason it's not possible to generate data/record types from
reflection directly, since the scope checker wouldn't know about the
constructor/field names. It is however already possible to generate the
*types* of the constructors or fields through reflection.

I've also been annoyed by the lack of a good reflection tutorial in the
past, but so far I haven't found the time yet to write something up. So the
best way to learn more about reflection is by reading the documentation and
looking at examples, e.g. my ataca <https://github.com/jespercockx/ataca>
library. I think there's definitely an audience for a good proper tutorial
like the one you're writing. Perhaps if you agree we could link to it from
the list of tutorials at
https://agda.readthedocs.io/en/v2.6.0/getting-started/tutorial-list.html
and/or from the reflection documentation.

-- Jesper

On Thu, May 16, 2019 at 10:10 PM Musa Al-hassy <alhassm at mcmaster.ca> wrote:

> 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
> -}
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190517/0f9b47fc/attachment.html>