From 0c4030137f24f2371db85469de2f627eccbb1703 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jan 2020 22:08:42 -0800
Subject: [PATCH] feat: simplify `Coe` again

Users may add the expensive instances if they want.
The goal is to make sure the default configuration is solid, and
covers all examples we really want to support.

cc @kha @dselsam
---
 src/Init/Coe.lean          | 55 +++++++++++++++++---------------------
 tests/lean/run/CoeNew.lean |  2 +-
 2 files changed, 26 insertions(+), 31 deletions(-)

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 :=