From d7d7e16f961641a8dbcd9814a7ae46fe005d86b3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Oct 2020 09:55:19 -0700
Subject: [PATCH] chore: `Id` missing instances

---
 src/Init/Control/Id.lean    | 16 ++++++++++------
 src/Init/Data/Repr.lean     |  4 ++++
 src/Init/Data/ToString.lean |  6 +++++-
 3 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/src/Init/Control/Id.lean b/src/Init/Control/Id.lean
index 20107fd0bd..322231ff65 100644
--- a/src/Init/Control/Id.lean
+++ b/src/Init/Control/Id.lean
@@ -13,23 +13,27 @@ universe u
 
 def Id (type : Type u) : Type u := type
 
-@[inline] def Id.pure {α : Type u} (x : α) : Id α :=
+namespace Id
+
+@[inline] protected def pure {α : Type u} (x : α) : Id α :=
 x
 
-@[inline] def Id.bind {α β : Type u} (x : Id α) (f : α → Id β) : Id β :=
+@[inline] protected def bind {α β : Type u} (x : Id α) (f : α → Id β) : Id β :=
 f x
 
-@[inline] def Id.map {α β : Type u} (f : α → β) (x : Id α) : Id β :=
+@[inline] protected def map {α β : Type u} (f : α → β) (x : Id α) : Id β :=
 f x
 
-instance Id.hasBind : HasBind Id :=
+instance : HasBind Id :=
 { bind := @Id.bind }
 
-instance Id.monad : Monad Id :=
+instance : Monad Id :=
 { pure := @Id.pure, bind := @Id.bind, map := @Id.map }
 
-@[inline] def Id.run {α : Type u} (x : Id α) : α :=
+@[inline] protected def run {α : Type u} (x : Id α) : α :=
 x
 
 instance : MonadRun id Id :=
 ⟨@Id.run⟩
+
+end Id
diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index a38a7e1990..3114e37062 100644
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@@ -7,6 +7,7 @@ prelude
 import Init.Data.String.Basic
 import Init.Data.UInt
 import Init.Data.Nat.Div
+import Init.Control.Id
 open Sum Subtype Nat
 
 universes u v
@@ -23,6 +24,9 @@ inferInstanceAs (HasRepr α)
 instance : HasRepr Bool :=
 ⟨fun b => cond b "true" "false"⟩
 
+instance {α} [HasRepr α] : HasRepr (Id α) :=
+inferInstanceAs (HasRepr α)
+
 instance {p : Prop} : HasRepr (Decidable p) :=
 ⟨fun h => match h with
   | Decidable.isTrue _  => "true"
diff --git a/src/Init/Data/ToString.lean b/src/Init/Data/ToString.lean
index a24b120bec..77c858f8f1 100644
--- a/src/Init/Data/ToString.lean
+++ b/src/Init/Data/ToString.lean
@@ -8,6 +8,7 @@ import Init.Data.String.Basic
 import Init.Data.UInt
 import Init.Data.Nat.Div
 import Init.Data.Repr
+import Init.Control.Id
 open Sum Subtype Nat
 
 universes u v
@@ -18,7 +19,10 @@ class HasToString (α : Type u) :=
 export HasToString (toString)
 
 -- This instance is needed because `id` is not reducible
-instance {α : Type u} [HasToString α] : HasToString (id α) :=
+instance {α} [HasToString α] : HasToString (id α) :=
+inferInstanceAs (HasToString α)
+
+instance {α} [HasToString α] : HasToString (Id α) :=
 inferInstanceAs (HasToString α)
 
 instance : HasToString String :=