From 59f528e678676e6472470c558da54197e853c668 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 18 Jul 2022 11:19:54 +0200
Subject: [PATCH] fix: support empty inductives in json derive

---
 src/Lean/Elab/Deriving/FromToJson.lean           | 6 +++---
 tests/lean/derivingRpcEncoding.lean              | 3 +++
 tests/lean/derivingRpcEncoding.lean.expected.out | 1 +
 3 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean
index 32872a1207..a0c1f61b49 100644
--- a/src/Lean/Elab/Deriving/FromToJson.lean
+++ b/src/Lean/Elab/Deriving/FromToJson.lean
@@ -30,7 +30,7 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
           let (isOptField, nm) := mkJsonField field
           if isOptField then ``(opt $nm $(mkIdent <| header.targetNames[0]! ++ field))
           else ``([($nm, toJson $(mkIdent <| header.targetNames[0]! ++ field))])
-        let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]!):ident $header.binders:bracketedBinder* :=
+        let cmd ← `(private def $(mkIdent ctx.auxFunNames[0]!):ident $header.binders:bracketedBinder* : Json :=
           mkObj <| List.join [$fields,*])
         return #[cmd] ++ (← mkInstanceCmds ctx ``ToJson declNames)
       cmds.forM elabCommand
@@ -63,9 +63,9 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
           if ctx.usePartial then
             let letDecls ← mkLocalInstanceLetDecls ctx ``ToJson header.argNames
             let auxTerm ← mkLet letDecls auxTerm
-            `(private partial def $toJsonFuncId:ident $header.binders:bracketedBinder* := $auxTerm)
+            `(private partial def $toJsonFuncId:ident $header.binders:bracketedBinder* : Json := $auxTerm)
           else
-            `(private def $toJsonFuncId:ident $header.binders:bracketedBinder* := $auxTerm)
+            `(private def $toJsonFuncId:ident $header.binders:bracketedBinder* : Json := $auxTerm)
         return #[auxCmd] ++ (← mkInstanceCmds ctx ``ToJson declNames)
       cmds.forM elabCommand
       return true
diff --git a/tests/lean/derivingRpcEncoding.lean b/tests/lean/derivingRpcEncoding.lean
index 8569210861..b971098f5d 100644
--- a/tests/lean/derivingRpcEncoding.lean
+++ b/tests/lean/derivingRpcEncoding.lean
@@ -111,3 +111,6 @@ structure UnusedStruct (α : Type)
 #print UnusedStruct.RpcEncodingPacket
 #check instRpcEncodingUnusedStruct
 #eval test (UnusedStruct NoRpcEncoding) default
+
+deriving instance Repr, RpcEncoding for Empty
+#eval M.run do rpcDecode (α := Empty) (← fromJson? .null)
diff --git a/tests/lean/derivingRpcEncoding.lean.expected.out b/tests/lean/derivingRpcEncoding.lean.expected.out
index a93276d439..197745270a 100644
--- a/tests/lean/derivingRpcEncoding.lean.expected.out
+++ b/tests/lean/derivingRpcEncoding.lean.expected.out
@@ -53,3 +53,4 @@ constructors:
 UnusedStruct.RpcEncodingPacket.mk : UnusedStruct.RpcEncodingPacket
 instRpcEncodingUnusedStruct : (α : Type) → RpcEncoding (UnusedStruct α) UnusedStruct.RpcEncodingPacket
 ok: {}
+Except.error "no inductive constructor matched"