(Phantom-)typed quotation

open import Prelude
open import Builtin.Reflection
open import Tactic.Reflection.Quote

data TTerm {a} (A : Set a) : Set where
  typed : Term → TTerm A

mkTyped : ∀ {a} {A : Set a} → A → Term → TTerm A
mkTyped _ t = typed t

macro
  quote-typed : Term → Term
  quote-typed t = def (quote mkTyped) (vArg t ∷ vArg (` t) ∷ [])

foo : TTerm Nat
foo = quote-typed (5 ofType Nat)

macro
  unquote-typed : Term → Term
  unquote-typed (con (quote typed) (_ ∷ _ ∷ vArg t ∷ [])) = unquote-term t []
  unquote-typed _ = unknown

bar : Nat
bar = unquote-typed foo