fix: fixes #679

src/Lean/Data/Json/FromToJson.lean

@@ -69,9 +69,12 @@ instance [ToJson α] [ToJson β] : ToJson (α × β) where
 instance : FromJson Name where
   fromJson? j := do
     let s ← j.getStr?
-    let some n ← Syntax.decodeNameLit ("`" ++ s)
-      | throw s!"expected a `Name`, got '{j}'"
-    return n
+    if s == "[anonymous]" then
+      return Name.anonymous
+    else
+      let some n ← Syntax.decodeNameLit ("`" ++ s)
+        | throw s!"expected a `Name`, got '{j}'"
+      return n
 
 instance : ToJson Name where
   toJson n := toString n

tests/lean/679.lean

@@ -0,0 +1,8 @@
+import Lean
+open Lean
+
+def encodeDecode [ToJson α] [FromJson α] (x : α) : Except String α := do
+  let json ← toJson x
+  fromJson? json
+
+#eval encodeDecode Name.anonymous

tests/lean/679.lean.expected.out

@@ -0,0 +1 @@
+Except.ok Lean.Name.anonymous