From bca57afae77ec2489f9d372dcc722aaaa5367ad4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 7 May 2019 09:26:28 -0700
Subject: [PATCH] fix(library/init/io): `RefPointed` must "depend" on \alpha

---
 library/init/io.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/library/init/io.lean b/library/init/io.lean
index e10da8b333..714df896a2 100644
--- a/library/init/io.lean
+++ b/library/init/io.lean
@@ -185,10 +185,9 @@ end Proc
 
 
 /- References -/
-constant RefPointed : PointedType := default _
-def Ref (α : Type) : Type := RefPointed.type
-instance (α : Type) : Inhabited (Ref α) :=
-⟨RefPointed.val⟩
+constant RefPointed (α : Type) : PointedType := default _
+def Ref (α : Type) : Type := (RefPointed α).type
+instance (α : Type) : Inhabited (Ref α) := ⟨(RefPointed α).val⟩
 
 namespace Prim
 @[extern 3 cpp inline "lean::io_mk_ref(#2, #3)"]