From b0319462f18ee8c8c432fd99879a45f0a11d711b Mon Sep 17 00:00:00 2001
From: Henrik <hargonix@gmail.com>
Date: Sat, 9 Sep 2023 23:56:21 +0200
Subject: [PATCH] feat: print nameless instances properly

---
 DocGen4/Output/Module.lean    |  5 ++++-
 DocGen4/Process/Base.lean     |  6 ++++--
 DocGen4/Process/NameInfo.lean | 11 +++++++----
 3 files changed, 15 insertions(+), 7 deletions(-)

diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 03c0fdc..b14b6da 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -30,7 +30,10 @@ def argToHtml (arg : Arg) : HtmlM Html := do
   | BinderInfo.implicit => ("{", "}", true)
   | BinderInfo.strictImplicit => ("⦃", "⦄", true)
   | BinderInfo.instImplicit => ("[", "]", true)
-  let mut nodes := #[Html.text s!"{l}{arg.name.toString} : "]
+  let mut nodes :=
+    match arg.name with
+    | some name => #[Html.text s!"{l}{name.toString} : "]
+    | none => #[Html.text s!"{l}"]
   nodes := nodes.append (← infoFormatToHtml arg.type)
   nodes := nodes.push r
   let inner := <span class="fn">[nodes]</span>
diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean
index c5908ce..cf3df3a 100644
--- a/DocGen4/Process/Base.lean
+++ b/DocGen4/Process/Base.lean
@@ -27,14 +27,16 @@ structure NameInfo where
   doc : Option String
   deriving Inhabited
 
+
 /--
 An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`.
 -/
 structure Arg where
   /--
-  The name of the argument.
+  The name of the argument. For auto generated argument names like `[Monad α]`
+  this is none
   -/
-  name : Name
+  name : Option Name
   /--
   The pretty printed type of the argument.
   -/
diff --git a/DocGen4/Process/NameInfo.lean b/DocGen4/Process/NameInfo.lean
index cb082bb..f567fe5 100644
--- a/DocGen4/Process/NameInfo.lean
+++ b/DocGen4/Process/NameInfo.lean
@@ -15,17 +15,20 @@ def NameInfo.ofTypedName (n : Name) (t : Expr) : MetaM NameInfo := do
   let env ← getEnv
   return { name := n, type := ← prettyPrintTerm t, doc := ← findDocString? env n}
 
-partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × Expr) :=
+partial def typeToArgsType (e : Expr) : (Array ((Option Name) × Expr × BinderInfo) × Expr) :=
   let helper := fun name type body data =>
     -- Once we hit a name with a macro scope we stop traversing the expression
     -- and print what is left after the : instead. The only exception
     -- to this is instances since these almost never have a name
     -- but should still be printed as arguments instead of after the :.
-    if name.hasMacroScopes && !data.isInstImplicit then
+    if data.isInstImplicit then
+      let arg := (none, type, data)
+      let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
+      (#[arg] ++ args, final)
+    else if name.hasMacroScopes then
       (#[], e)
     else
-      let name := name.eraseMacroScopes
-      let arg := (name, type, data)
+      let arg := (some name, type, data)
       let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩))
       (#[arg] ++ args, final)
   match e.consumeMData with