From 8b9c7ebf431dca0b254f3ddb670f11779f83c360 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sun, 17 Jul 2022 15:55:43 +0200
Subject: [PATCH] chore: simplify deriveWithRefInstance

---
 src/Lean/Server/Rpc/Deriving.lean | 26 +++++++-------------------
 1 file changed, 7 insertions(+), 19 deletions(-)

diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean
index c106b84d07..482b84585a 100644
--- a/src/Lean/Server/Rpc/Deriving.lean
+++ b/src/Lean/Server/Rpc/Deriving.lean
@@ -20,26 +20,14 @@ private def deriveWithRefInstance (typeNm : Name) : CommandElabM Bool := do
   -- TODO(WN): check that `typeNm` is not a scalar type
   let typeId := mkIdent typeNm
   let cmds ← `(
-    section
-    variable {m : Type → Type}
-    unsafe def encodeUnsafe [Monad m] [MonadRpcSession m] (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef :=
-      WithRpcRef.encodeUnsafe $(quote typeNm) r
+    unsafe def unsafeInst : RpcEncoding (WithRpcRef $typeId:ident) Lsp.RpcRef where
+      rpcEncode := WithRpcRef.encodeUnsafe $(quote typeNm)
+      rpcDecode := WithRpcRef.decodeUnsafeAs $typeId:ident $(quote typeNm)
 
-    @[implementedBy encodeUnsafe]
-    opaque encode [Monad m] [MonadRpcSession m] (r : WithRpcRef $typeId:ident) : m Lsp.RpcRef :=
-      pure ⟨0⟩
-
-    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]
-    opaque decode [Monad m] [MonadRpcSession m] (r : Lsp.RpcRef) : ExceptT String m (WithRpcRef $typeId:ident) :=
-      throw "unreachable"
-
-    instance : RpcEncoding (WithRpcRef $typeId:ident) Lsp.RpcRef :=
-      { rpcEncode := encode
-        rpcDecode := decode }
-    end
+    @[implementedBy unsafeInst]
+    instance : RpcEncoding (WithRpcRef $typeId:ident) Lsp.RpcRef where
+      rpcEncode r := pure ⟨0⟩
+      rpcDecode r := throw "unreachable"
   )
   elabCommand cmds
   return true