diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/TypeSimplifier.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/TypeSimplifier.scala
index 40cca3394..9011b3058 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/bbml/TypeSimplifier.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/TypeSimplifier.scala
@@ -28,7 +28,7 @@ class TypeSimplifier(tl: TraceLogger):
         tv.state.upperBounds = tv.state.upperBounds.map(goType)
       tv
     def goType(ty: Type): Type =
-    trace[Type](s"simplifyStructure($ty)", r => s"= $r"):
+    trace[Type](s"simplifyStructure(${ty.showDbg})", r => s"= ${r.showDbg}"):
       ty match
       case tv: InfVar => goTV(tv)
       case _ =>
@@ -72,7 +72,7 @@ class TypeSimplifier(tl: TraceLogger):
       }
       
       override def apply(pol: Bool)(ty: GeneralType): Unit =
-        trace(s"Analyse[${printPol(pol)}] $ty  [${curPath.reverseIterator.mkString(" ~> ")}]"):
+        trace(s"Analyse[${printPol(pol)}] ${ty.showDbg}  [${curPath.reverseIterator.mkString(" ~> ")}]"):
           ty match
             case ty if ty.lvl <= lvl =>
               log(s"Level is < $lvl")
@@ -84,7 +84,7 @@ class TypeSimplifier(tl: TraceLogger):
               if curPath.exists(_ is tv) then // TODO opt
                 traversedTVs += tv
                 val recPrefix = curPath.takeWhile(_ isnt tv)
-                log(s"UNIFYING $tv with ${recPrefix.mkString(", ")}")
+                log(s"UNIFYING ${tv.showDbg} with ${recPrefix.mkString(", ")}")
                 recPrefix.foreach: tv2 =>
                   if tv2 isnt tv then
                     traversedTVs += tv2
@@ -99,9 +99,9 @@ class TypeSimplifier(tl: TraceLogger):
                       else if tvRepr.lvl > lvl && !varSubst.contains(tvRepr) then varSubst += tvRepr -> tv
                 continue = false
               // TODO else??
-              if traversedTVs.contains(tv) then log(s"Now already traversed $tv")
+              if traversedTVs.contains(tv) then log(s"Now already traversed ${tv.showDbg}")
               else if pastPathsSet.contains(tv) then
-                log(s"REC $tv")
+                log(s"REC ${tv.showDbg}")
                 recVars += tv
                 continue = false
               if continue then
@@ -128,7 +128,7 @@ class TypeSimplifier(tl: TraceLogger):
               pastPathsSet --= oldPath
               ()
     
-    trace(s"Simplifying type $ty"):
+    trace(s"Simplifying type ${ty.showDbg}"):
       Analysis(pol)(ty)
     
     log("Unif-pre: " + Analysis.varSubst)
@@ -145,12 +145,12 @@ class TypeSimplifier(tl: TraceLogger):
     val traversed: MutSet[IV] = MutSet.empty
     val transformed: MutMap[IV, Type] = MutMap.empty
     
-    def subst(ty: GeneralType): GeneralType = trace[GeneralType](s"subst($ty)", r => s"= $r"):
+    def subst(ty: GeneralType): GeneralType = trace[GeneralType](s"subst(${ty.showDbg})", r => s"= ${r.showDbg}"):
       ty match
         case ty if ty.lvl <= lvl => ty // TODO NOPE
         case _tv: IV =>
           val tv = Analysis.getRepr(_tv)
-          log(s"Repr: $tv")
+          log(s"Repr: ${tv.showDbg}")
           transformed.getOrElseUpdate(tv, {
             if Analysis.recVars.contains(tv) then
               log(s"It's recursive!")
diff --git a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala
index a1900570a..79f73a540 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/bbml/types.scala
@@ -183,7 +183,7 @@ sealed abstract class BasicType extends Type:
       if targs.isEmpty then s"${name.nme}" else s"${name.nme}[${targs.map(_.showDbg).mkString(", ")}]"
     case v @ InfVar(lvl, uid, _, isSkolem) =>
       val name = if v.hint.isEmpty then s"${v.sym.nme}" else s"${v.sym.nme}(${v.hint})"
-      if isSkolem then s"<${name}>_${lvl}" else s"${name}_${lvl}"
+      if isSkolem then s"<${name}${uid}>_${lvl}" else s"${name}${uid}_${lvl}"
     case FunType(arg :: Nil, ret, eff) => s"${arg.parenDbg} ->{${eff.showDbg}} ${ret.parenDbg}"
     case FunType(args, ret, eff) => s"(${args.map(_.showDbg).mkString(", ")}) ->{${eff.showDbg}} ${ret.parenDbg}"
     case ComposedType(lhs, rhs, pol) => s"${lhs.parenDbg} ${if pol then "∨" else "∧"} ${rhs.parenDbg}"
@@ -315,10 +315,10 @@ case class PolyType(tvs: Ls[InfVar], body: GeneralType) extends GeneralType:
         v.state.upperBounds = state.upperBounds.map(_.subst)
     body.subst
 
-  def skolemize(nextUid: => Uid[InfVar], lvl: Int)(tl: TL)(using State) =
+  def skolemize(nextUid: => Uid[InfVar], lvl: Int)(tl: TL) =
     // * Note that by this point, the state is supposed to be frozen/treated as immutable
     val map = tvs.map(v =>
-      val sk = InfVar(lvl, nextUid, new VarState(), true)(new RefSymbol(v.sym), v.hint)
+      val sk = InfVar(lvl, nextUid, new VarState(), true)(v.sym, v.hint)
       tl.log(s"skolemize ${v.showDbg} ~> ${sk.showDbg}")
       v.uid -> sk
     ).toMap
@@ -326,7 +326,7 @@ case class PolyType(tvs: Ls[InfVar], body: GeneralType) extends GeneralType:
   
   def instantiate(nextUid: => Uid[InfVar], lvl: Int)(tl: TL)(using State): GeneralType =
     val map = tvs.map(v =>
-      val nv = InfVar(lvl, nextUid, new VarState(), false)(new RefSymbol(v.sym), v.hint)
+      val nv = InfVar(lvl, nextUid, new VarState(), false)(new InstSymbol(v.sym), v.hint)
       tl.log(s"instantiate ${v.showDbg} ~> ${nv.showDbg}")
       v.uid -> nv
     ).toMap
diff --git a/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala b/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala
index ba1b0b13a..ab79e3a47 100644
--- a/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala
+++ b/hkmc2/shared/src/main/scala/hkmc2/semantics/Symbol.scala
@@ -80,7 +80,10 @@ class TempSymbol(val trm: Opt[Term], dbgNme: Str = "tmp")(using State) extends B
   override def toString: Str = s"$$${super.toString}"
 
 
-class RefSymbol(val origin: Symbol)(using State) extends LocalSymbol:
+// * When instantiating forall-qualified TVs, we need to duplicate the information
+// * for pretty-printing, but each instantiation should be different from each other
+// * i.e., UID should be different
+class InstSymbol(val origin: Symbol)(using State) extends LocalSymbol:
   override def nme: Str = origin.nme
   override def toLoc: Option[Loc] = origin.toLoc
   override def toString: Str = origin.toString
diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls
index af4449a76..d78b667b8 100644
--- a/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls
+++ b/hkmc2/shared/src/test/mlscript/bbml/bbBounds.mls
@@ -114,9 +114,9 @@ bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A
 //│ ╔══[ERROR] Cannot type non-function term SynthSel(Ref(globalThis:block#17),Ident(bazbaz)) as (<A>) ->{⊥} (forall B: B) ->{⊥} <A>
 //│ ║  l.113: 	bazbaz: [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A
 //│ ╙──       	^^^^^^
-//│ Type: forall A1: (A1) ->{⊥} (forall B: A1 -> A1) ->{⊥} A1
+//│ Type: forall A: (A) ->{⊥} (forall B: A -> A) ->{⊥} A
 //│ Where:
-//│   A1 <: Int
+//│   A <: Int
 
 
 (x => f => bazbaz(x)(f)): [A extends Int] -> A -> ([B extends A -> A restricts A -> A] -> B) -> A
diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls
index 11e356b21..c01bd9133 100644
--- a/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls
+++ b/hkmc2/shared/src/test/mlscript/bbml/bbCyclicExtrude.mls
@@ -27,7 +27,7 @@ f => (let g = x => f(x(x)) in g) : [A] -> A -> A
 //│ ╟── because: cannot constrain  <A>  <:  x
 //│ ╟── because: cannot constrain  <A>  <:  x
 //│ ╙── because: cannot constrain  <A>  <:  ¬(¬{x ->{eff1} app1})
-//│ Type: (⊥ -> ⊥) ->{⊥} forall A1: (A1) ->{⊥} A1
+//│ Type: (⊥ -> ⊥) ->{⊥} forall A: (A) ->{⊥} A
 
 f => (x => f(x(x)) : [A] -> A -> A)
 //│ Type: (app -> (⊤ -> ⊥)) ->{⊥} (x -> app) ->{⊥} forall A: (A) ->{⊥} A
diff --git a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls
index 10a29dc9b..cd0bc4567 100644
--- a/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls
+++ b/hkmc2/shared/src/test/mlscript/bbml/bbPoly.mls
@@ -31,7 +31,7 @@ id
 //│ ║  l.25: 	(x => x + 1): [A] -> A -> A
 //│ ║        	      ^^^^^
 //│ ╙── because: cannot constrain  Int  <:  <A>
-//│ Type: forall A1: (A1) ->{⊥} A1
+//│ Type: forall A: (A) ->{⊥} A
 
 
 (x => x): [A] -> A -> A