Clear `._hyg` in `.mvarId!.getType`

Stream: metaprogramming / tactics

[nrs]

In the following, how would I clear the ._hyg in the output to get back the original type information, for debugging what's happening inside MetaM? I know this is probably related to hygienic macros, any tips on what I can read to figure out how this works? (Lens.problembResolutiona is the name of the current file)

import Mathlib
open Lean Meta Elab Term

namespace myNamespace

class Signature where
  symbols : Type
  arity : symbols -> Nat

inductive Ext (sig : Signature) (α : Type _)
| mk : (s : sig.symbols) -> (Fin2 (sig.arity s) -> α) -> Ext sig α

inductive W (sig : Signature)
| sup : Ext sig (W sig) -> W sig

class SubSig (siga : Signature) (sigb : outParam Signature) where
  inj : Ext siga α -> Ext sigb α

instance NatTyE : Signature := ⟨Unit, fun _ => 0⟩

def myCore : CoreM Unit := do
  let axiom_stx : Syntax := <- `({sig : Signature} -> [inst : SubSig NatTyE sig] -> W sig -> Type _)
  let _ <- MetaM.run' (α := Unit) (do
    let goal <- mkFreshExprMVar (<- TermElabM.run' (do elabTerm axiom_stx (Expr.sort levelOne)))
    dbg_trace (<- goal.mvarId!.getType)
  )

#eval myCore

/-
forall {sig._@.Lens.problembResolutiona._hyg.467 : myNamespace.Signature} [inst._@.Lens.problembResolutiona._hyg.467 : myNamespace.SubSig.{?_uniq.2346} myNamespace.NatTyE sig._@.Lens.problembResolutiona._hyg.467], (myNamespace.W sig._@.Lens.problembResolutiona._hyg.467) -> Type.{?_uniq.2351}
-/

[Kyle Miller]

Use logInfo instead of dbg_trace

[Kyle Miller]

Output like what you see is from not using the pretty printer

[nrs]

I see! thanks a lot!!

[Kyle Miller]

You should also be able to do logInfo m!"{goal.mvarId!}" to see the entire goal pretty printed, if you want. The m!"{...}" wrapper is likely optional, but that way you can add in extra text.

[nrs]

ah yes nice, this is significantly easier to read, ty