From b7bcb1616a70d3f2aaa2663fef6e79c65e4d9037 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sun, 17 Jul 2022 18:19:59 +0200
Subject: [PATCH] chore: add inhabited instance for RpcEncoding

This allows us to define RpcEncodings as partial defs.
---
 src/Lean/Server/Rpc/Basic.lean           |  5 ++++-
 src/Lean/Server/Rpc/RequestHandling.lean | 14 ++++++++++++--
 2 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Server/Rpc/Basic.lean b/src/Lean/Server/Rpc/Basic.lean
index 1d1c5f93c0..17c61fb665 100644
--- a/src/Lean/Server/Rpc/Basic.lean
+++ b/src/Lean/Server/Rpc/Basic.lean
@@ -42,10 +42,13 @@ non-JSON-serializable fields can be auto-encoded in two ways:
 -- TODO(WN): for Lean.js, have third parameter defining the client-side structure;
 -- or, compile `WithRpcRef` to "opaque reference" on the client
 class RpcEncoding (α : Type) (β : outParam Type) where
-  rpcEncode {m : Type → Type} [Monad m] [MonadRpcSession m] : α → m β
+  rpcEncode {m : Type → Type} [Monad m] [MonadRpcSession m] : α → ExceptT String m β
   rpcDecode {m : Type → Type} [Monad m] [MonadRpcSession m] : β → ExceptT String m α
 export RpcEncoding (rpcEncode rpcDecode)
 
+instance : Inhabited (RpcEncoding α β) where
+  default := { rpcEncode := fun _ => throw "unreachable", rpcDecode := fun _ => throw "unreachable" }
+
 instance [FromJson α] [ToJson α] : RpcEncoding α α where
   rpcEncode := pure
   rpcDecode := pure
diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean
index 1da7da08fd..5ad94572cf 100644
--- a/src/Lean/Server/Rpc/RequestHandling.lean
+++ b/src/Lean/Server/Rpc/RequestHandling.lean
@@ -82,8 +82,18 @@ def wrapRpcProcedure (method : Name) paramType respType
     RequestM.mapTask t fun
       | Except.error e => throw e
       | Except.ok ret => do
-        let act := rpcEncode (α := respType) (β := respLspType) (m := StateM FileWorker.RpcSession) ret
-        return toJson (← seshRef.modifyGet act.run)⟩
+        let act : StateM FileWorker.RpcSession (Except String respLspType) := do
+          let s ← get
+          match ← rpcEncode (α := respType) (β := respLspType) (m := StateM FileWorker.RpcSession) ret with
+            | .ok x => return .ok x
+            | .error e => set s; return .error e
+        match ← seshRef.modifyGet act.run with
+          | .ok x => return toJson x
+          | .error e =>
+            throwThe RequestError {
+              code := JsonRpc.ErrorCode.invalidParams
+              message := s!"Cannot encode result of RPC call '{method}'\n{e}"
+            }⟩
 
 def registerBuiltinRpcProcedure (method : Name) paramType respType
     {paramLspType} [RpcEncoding paramType paramLspType] [FromJson paramLspType]