diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index 616d40fe25..a97ca477ec 100644
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@@ -12,12 +12,9 @@ universes u v w w'
 class Coe (α : Sort u) (β : Sort v) :=
 (coe : α → β)
 
-class CoeDep (α : Sort u) (a : α) (β : Sort v) :=
-(coe : β)
-
-/-- Auxiliary class that contains the transitive closure of `Coe` and `CoeDep`. -/
-class CoeTC (α : Sort u) (a : α) (β : Sort v) :=
-(coe : β)
+/-- Auxiliary class that contains the transitive closure of `Coe`. -/
+class CoeTC (α : Sort u) (β : Sort v) :=
+(coe : α → β)
 
 /- Expensive coercion that can only appear at the beggining of a sequence of coercions. -/
 class CoeHead (α : Sort u) (β : Sort v) :=
@@ -27,7 +24,10 @@ class CoeHead (α : Sort u) (β : Sort v) :=
 class CoeTail (α : Sort u) (β : Sort v) :=
 (coe : α → β)
 
-/- CoeHead + CoeTC + CoeTail -/
+class CoeDep (α : Sort u) (a : α) (β : Sort v) :=
+(coe : β)
+
+/- Combines CoeHead, CoeTC, CoeTail, CoeDep -/
 class CoeT (α : Sort u) (a : α) (β : Sort v) :=
 (coe : β)
 
@@ -37,20 +37,20 @@ class CoeFun (α : Sort u) (γ : outParam (α → outParam (Sort v))) :=
 class CoeSort (α : Sort u) (β : outParam (Sort v)) :=
 (coe : α → β)
 
-abbrev coeB {α : Sort u} {β : Sort v} (a : α) [Coe α β] : β :=
+abbrev coeB {α : Sort u} {β : Sort v} [Coe α β] (a : α) : β :=
 @Coe.coe α β _ a
 
-abbrev coeHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : β :=
+abbrev coeHead {α : Sort u} {β : Sort v} [CoeHead α β] (a : α) : β :=
 @CoeHead.coe α β _ a
 
-abbrev coeTail {α : Sort u} {β : Sort v} (a : α) [CoeTail α β] : β :=
+abbrev coeTail {α : Sort u} {β : Sort v} [CoeTail α β] (a : α) : β :=
 @CoeTail.coe α β _ a
 
 abbrev coeD {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : β :=
 @CoeDep.coe α a β _
 
-abbrev coeTC {α : Sort u} {β : Sort v} (a : α) [CoeTC α a β] : β :=
-@CoeTC.coe α a β _
+abbrev coeTC {α : Sort u} {β : Sort v} [CoeTC α β] (a : α) : β :=
+@CoeTC.coe α β _ a
 
 /-- Apply coercion manually. -/
 abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β :=
@@ -62,27 +62,19 @@ abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
 abbrev coeSort {α : Sort u} {β : Sort v} (a : α) [CoeSort α β] : β :=
 @CoeSort.coe α β _ a
 
-instance coeDepTrans {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α a β] [CoeDep β (coeTC a) δ] : CoeTC α a δ :=
-{ coe := coeD (coeTC a : β) }
+instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [CoeTC α β] [Coe β δ] : CoeTC α δ :=
+{ coe := fun a => coeB (coeTC a : β) }
 
-instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α a β] [Coe β δ] : CoeTC α a δ :=
-{ coe := coeB (coeTC a : β) }
+instance coeBase {α : Sort u} {β : Sort v} [Coe α β] : CoeTC α β :=
+{ coe := fun a => coeB a }
 
-instance coeBase {α : Sort u} {β : Sort v} (a : α) [Coe α β] : CoeTC α a β :=
-{ coe := coeB a }
-
-instance coeDepBase {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : CoeTC α a β :=
-{ coe := coeD a }
-
-@[inferTCGoalsLR]
-instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeHead α β] [CoeTail δ γ] [CoeTC β (coeHead a) δ] : CoeT α a γ :=
+instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeTC β δ] [CoeTail δ γ] [CoeHead α β] : CoeT α a γ :=
 { coe := coeTail (coeTC (coeHead a : β) : δ) }
 
-@[inferTCGoalsLR]
-instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeHead α β] [CoeTC β (coeHead a) δ] : CoeT α a δ  :=
+instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC β δ] [CoeHead α β] : CoeT α a δ  :=
 { coe := coeTC (coeHead a : β) }
 
-instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α a β] [CoeTail β δ] : CoeT α a δ :=
+instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α β] [CoeTail β δ] : CoeT α a δ :=
 { coe := coeTail (coeTC a : β) }
 
 instance coeOfHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : CoeT α a β :=
@@ -91,13 +83,16 @@ instance coeOfHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : CoeT 
 instance coeOfTail {α : Sort u} {β : Sort v} (a : α) [CoeTail α β] : CoeT α a β :=
 { coe := coeTail a }
 
-instance coeOfTC {α : Sort u} {β : Sort v} (a : α) [CoeTC α a β] : CoeT α a β :=
+instance coeOfTC {α : Sort u} {β : Sort v} (a : α) [CoeTC α β] : CoeT α a β :=
 { coe := coeTC a }
 
-instance coeFunTrans {α : Sort u} {β : Sort v} {γ : β → Sort w} [Coe α β] [CoeFun β γ] : CoeFun α (fun a => γ (coe a)) :=
+instance coeOfDep {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : CoeT α a β :=
+{ coe := coeD a }
+
+instance coeFunTrans {α : Sort u} {β : Sort v} {γ : β → Sort w} [CoeFun β γ] [Coe α β] : CoeFun α (fun a => γ (coe a)) :=
 { coe := fun a => coeFun (coeB a : β) }
 
-instance coeSortTrans {α : Sort u} {β : Sort v} {δ : Sort w} [Coe α β] [CoeSort β δ] : CoeSort α δ :=
+instance coeSortTrans {α : Sort u} {β : Sort v} {δ : Sort w} [CoeSort β δ] [Coe α β] : CoeSort α δ :=
 { coe := fun a => coeSort (coeB a : β) }
 
 /- Basic instances -/
diff --git a/tests/lean/run/CoeNew.lean b/tests/lean/run/CoeNew.lean
index 93c777f97f..fe7efaa974 100644
--- a/tests/lean/run/CoeNew.lean
+++ b/tests/lean/run/CoeNew.lean
@@ -22,7 +22,7 @@ set_option pp.implicit true
 #synth CoeT { x : Nat // x > 0 } ⟨1, sorryAx _⟩ Bool
 #synth CoeT Nat 0 (Option Nat)
 #synth CoeT Bool true (Option Nat)
-#synth CoeT Prop (0 = 1) Nat
+#synth CoeT Prop (0 = 1) Bool
 #synth CoeT Bool true (Option Nat)
 
 def f (c : ConstantFunction Nat Nat) : Nat :=