diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index f4382de448..1186e93c1b 100644
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@@ -100,6 +100,9 @@ instance coeOfDep {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : CoeT 
 instance coeId {α : Sort u} (a : α) : CoeT α a α where
   coe := a
 
+instance coeSortToCoeTail [inst : CoeSort α β] : CoeTail α β where
+  coe := inst.coe
+
 /- Basic instances -/
 
 @[inline] instance boolToProp : Coe Bool Prop where
diff --git a/tests/lean/run/mathport_issue16.lean b/tests/lean/run/mathport_issue16.lean
index 3d86a94bfd..b332353c51 100644
--- a/tests/lean/run/mathport_issue16.lean
+++ b/tests/lean/run/mathport_issue16.lean
@@ -3,7 +3,4 @@ class Foo (α : Type) where x : α
 instance : CoeSort (Foo α) Type where
   coe _ := α
 
-instance coeSortToCoe [inst : CoeSort α β] : Coe α β where
-  coe := inst.coe
-
 #check @id (Foo.mk ()) ()