feat: add instance from CoeSort to CoeTail

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

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 ()) ()