<div dir="ltr">Hi everyone,<div><br></div><div>I&#39;m experimenting with the new reflection stuff in 2.5.1. These changes are quite exciting!</div><div><br></div><div>I noticed that all the unquoting operations (unquote/unquoteDecl/unquoteDef) take a TC ⊤, making it hard to return results of a computation in this monad. Let&#39;s say we want to count the number of constructors of a datatype:</div><div><br></div><div>---</div><div><div>open import Prelude<br></div><div>open import Builtin.Reflection</div><div><br></div><div>data Foo : Set where</div><div>  foo1 : Foo</div><div>  foo2 : Foo</div><div><br></div><div>countConstructors : Name → TC Nat</div><div>countConstructors dt = length &lt;$&gt; getConstructors dt</div></div><div>---</div><div><br></div><div>Now i believe in an ideal situation one would have a way to run this computation and return the result:</div><div><br></div><div>---</div><div><div>-- test-countConstructors : runquote (countConstructors (quote Foo)) ≡ 2</div><div>-- test-countConstructors = refl</div></div><div>---</div><div><br></div><div>As it turns out, it is possible to abuse the unify function to return arbitrary results by quoting them to a Term first. So we can define a function which takes a TC A and gives us a tactic which puts the value in the hole:</div><div><br></div><div>---</div><div><div>runTC : ∀ {a} {A : Set a} → TC A → Tactic</div><div>runTC c hole =</div><div>  do v ← c</div><div>  =| `v ← quoteTC v</div><div>  =| unify hole `v</div><div><br></div><div>test-countConstructors : unquote (runTC (countConstructors (quote Foo))) ≡ 2</div><div>test-countConstructors = refl</div></div><div>---</div><div><br></div><div>This is usable, but the notation is awkward. I used the new macro functionality to clean it up:</div><div><br></div><div>---</div><div><div>macro</div><div>  countConstructors′ : Name → Tactic</div><div>  countConstructors′ dt = runTC (countConstructors dt)</div><div><br></div><div>test-countConstructors′ : countConstructors′ Foo ≡ 2</div><div>test-countConstructors′ = refl</div></div><div>---</div><div><br></div><div>All of this took quite a while for me to figure out, so i thought it was worth sharing. But i also think this is a complicated solution to something which should be quite simple. Is this the right way to do it or am i missing something here?</div><div><br></div><div>Would it maybe make sense to have runTC as a built-in, and extend the macro&#39;s to allow result types of something else than TC ⊤ in which case runTC is used? I imagine something like this would be possible:</div><div><br></div><div>---</div><div><div>-- macro</div><div>--   countConstructors : Name → TC Nat</div><div>--   countConstructors dt = length &lt;$&gt; getConstructors dt</div><div><br></div><div>-- test-countConstructors : countConstructors Foo ≡ 2</div><div>-- test-countConstructors = refl</div></div><div>---</div><div><br></div><div>I would like to hear your opinions on this,</div><div><br></div><div>Yorick</div></div>