fix: deriving RpcEncoding

src/Lean/Server/Rpc/Basic.lean

@@ -76,6 +76,9 @@ instance [RpcEncoding α α'] [RpcEncoding β β']  : RpcEncoding (α × β) (α
     let b ← rpcDecode b'
     return (a, b)
 
+structure RpcEncoding.DerivingParams where
+  withRef : Bool := false
+
 /-- Marks fields to encode as opaque references in LSP packets. -/
 structure WithRpcRef (α : Type u) where
   val : α

src/Lean/Server/Rpc/Deriving.lean

@@ -13,9 +13,6 @@ import Lean.Server.Rpc.Basic
 
 namespace Lean.Server.RpcEncoding
 
-structure DerivingParams where
-  withRef : Bool := false
-
 open Meta Elab Command Term
 
 private def deriveWithRefInstance (typeNm : Name) : CommandElabM Bool := do
@@ -24,22 +21,24 @@ private def deriveWithRefInstance (typeNm : Name) : CommandElabM Bool := do
   let typeId := mkIdent typeNm
   let cmds ← `(
     namespace $typeId:ident
-    variable {m : Type → Type} [Monad m] [MonadRpcSession m]
-    private unsafe def encodeUnsafe (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef :=
+    variable {m : Type → Type}
+    private unsafe def encodeUnsafe [Monad m] [MonadRpcSession m] (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef :=
       WithRpcRef.encodeUnsafe $(quote typeNm) r
 
     @[implementedBy encodeUnsafe]
-    private constant encode (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef
+    private constant encode [Monad m] [MonadRpcSession m] (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef :=
+      pure ⟨0⟩
 
-    private unsafe def decodeUnsafe (r : Lsp.RpcRef) : m (WithRpcRef $typeId:ident) :=
+    private unsafe def decodeUnsafe [Monad m] [MonadRpcSession m] (r : Lsp.RpcRef) : ExceptT String m (WithRpcRef $typeId:ident) :=
       WithRpcRef.decodeUnsafeAs $typeId:ident $(quote typeNm) r
 
     @[implementedBy decodeUnsafe]
-    private constant decode (r : Lsp.RpcRef) : m (WithRpcRef $typeId:ident)
+    private constant decode [Monad m] [MonadRpcSession m] (r : Lsp.RpcRef) : ExceptT String m (WithRpcRef $typeId:ident) :=
+      throw "unreachable"
 
     instance : RpcEncoding (WithRpcRef $typeId:ident) Lsp.RpcRef where
-      lspEncode a := encode a
-      lspDecode a := decode a
+      rpcEncode a := encode a
+      rpcDecode a := decode a
     end $typeId:ident
   )
   elabCommand cmds
@@ -101,11 +100,11 @@ private def deriveInstance (typeName : Name) : CommandElabM Bool := do
           deriving $(mkIdent ``Lean.FromJson), $(mkIdent ``Lean.ToJson)
 
         instance : RpcEncoding $typeId:ident RpcEncodingPacket where
-          lspEncode a := do
+          rpcEncode a := do
             return {
               $[$encFields]*
             }
-          lspDecode a := do
+          rpcDecode a := do
             return {
               $[$decFields]*
             }

tests/lean/run/derivingRpcEncoding.lean

@@ -1,10 +1,10 @@
-import Lean.Server.FileWorker.LspEncoding
+import Lean.Server.Rpc.Basic
 
 open Lean Server
 
 structure FooRef where
   a : Array Nat
-  deriving LspEncoding with { withRef := true }
+  deriving RpcEncoding with { withRef := true }
 
 structure FooJson where
   s : String
@@ -13,12 +13,12 @@ structure FooJson where
 structure Bar where
   fooRef : WithRpcRef FooRef
   fooJson : FooJson
-  deriving LspEncoding
+  deriving RpcEncoding
 
 structure BarTrans where
   bar : Bar
-  deriving LspEncoding
+  deriving RpcEncoding
 
 structure Baz where
   arr : Array String -- non-constant field
-  deriving LspEncoding
+  deriving RpcEncoding