[Agda] How to show a Term?

[Roman]

Hi. `unquote` allows to print a Term, but it also performs type
checking. Is there a way to print a Term just like `unquote` does, but
without type checking it? I.e. something like `showTerm : Term ->
String`. It's hard to read plain Terms even with appropriate {-#
DISPLAY #-} pragmas and more importantly we could define a type class

record Quote {α} (A : Set α) : Set α where
  field deepQuote : A -> Term

  show : A -> String
  show = showTerm ∘ deepQuote
open Quote {{...}} public

instead of the Show type class and delegate pretty printing to the
built-in machinery therefore avoiding all the burden of dealing with
associativity, inserting parentheses and spaces etc.