From 118567657dec5c2efb6c2fcaf9aeafdafff7d01d Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 5 Dec 2022 19:31:23 -0800
Subject: [PATCH] chore: remove dangerous instances in json-rpc

---
 src/Lean/Data/JsonRpc.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean
index 2121b62419..4d50da5214 100644
--- a/src/Lean/Data/JsonRpc.lean
+++ b/src/Lean/Data/JsonRpc.lean
@@ -127,7 +127,7 @@ structure Request (α : Type u) where
   param  : α
   deriving Inhabited, BEq
 
-instance [ToJson α] : Coe (Request α) Message :=
+instance [ToJson α] : CoeHead (Request α) Message :=
   ⟨fun r => Message.request r.id r.method (toStructured? r.param).toOption⟩
 
 /-- Generic version of `Message.notification`.
@@ -142,7 +142,7 @@ structure Notification (α : Type u) where
   param  : α
   deriving Inhabited, BEq
 
-instance [ToJson α] : Coe (Notification α) Message :=
+instance [ToJson α] : CoeHead (Notification α) Message :=
   ⟨fun r => Message.notification r.method (toStructured? r.param).toOption⟩
 
 /-- Generic version of `Message.response`.
@@ -161,7 +161,7 @@ structure Response (α : Type u) where
   result : α
   deriving Inhabited, BEq
 
-instance [ToJson α] : Coe (Response α) Message :=
+instance [ToJson α] : CoeHead (Response α) Message :=
   ⟨fun r => Message.response r.id (toJson r.result)⟩
 
 /-- Generic version of `Message.responseError`.
@@ -180,7 +180,7 @@ structure ResponseError (α : Type u) where
   data?   : Option α := none
   deriving Inhabited, BEq
 
-instance [ToJson α] : Coe (ResponseError α) Message :=
+instance [ToJson α] : CoeHead (ResponseError α) Message :=
   ⟨fun r => Message.responseError r.id r.code r.message (r.data?.map toJson)⟩
 
 instance : Coe String RequestID := ⟨RequestID.str⟩