diff --git a/src/Lean/Server/Rpc/Basic.lean b/src/Lean/Server/Rpc/Basic.lean
index 17c61fb665..b0e4510481 100644
--- a/src/Lean/Server/Rpc/Basic.lean
+++ b/src/Lean/Server/Rpc/Basic.lean
@@ -46,8 +46,8 @@ class RpcEncoding (α : Type) (β : outParam Type) where
   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 : Nonempty (RpcEncoding α β) :=
+  ⟨{ rpcEncode := fun _ => throw "unreachable", rpcDecode := fun _ => throw "unreachable" }⟩
 
 instance [FromJson α] [ToJson α] : RpcEncoding α α where
   rpcEncode := pure
diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean
index 20671c76c0..13b7dc5f50 100644
--- a/src/Lean/Server/Rpc/Deriving.lean
+++ b/src/Lean/Server/Rpc/Deriving.lean
@@ -25,7 +25,9 @@ private def deriveWithRefInstance (typeNm : Name) : CommandElabM Bool := do
       rpcDecode := WithRpcRef.decodeUnsafeAs $typeId:ident $(quote typeNm)
 
     @[implementedBy unsafeInst]
-    instance : RpcEncoding (WithRpcRef $typeId:ident) Lsp.RpcRef := default
+    opaque inst : RpcEncoding (WithRpcRef $typeId) Lsp.RpcRef
+
+    instance : RpcEncoding (WithRpcRef $typeId) Lsp.RpcRef := inst
   )
   elabCommand cmds
   return true