chore: add inhabited instance for RpcEncoding

This allows us to define RpcEncodings as partial defs.

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

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]