From 9bc07254a1da87d03497302e44fcf714a45d19df Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jan 2020 02:34:35 -0800
Subject: [PATCH] feat: add support for `CoeSort`

---
 src/Init/Coe.lean            |  4 +--
 src/Init/Lean/Elab/Term.lean | 63 ++++++++++++++++++++++++------------
 2 files changed, 44 insertions(+), 23 deletions(-)

diff --git a/src/Init/Coe.lean b/src/Init/Coe.lean
index c707321cec..4be141e461 100644
--- a/src/Init/Coe.lean
+++ b/src/Init/Coe.lean
@@ -59,8 +59,8 @@ abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β :=
 abbrev coeFun {α : Sort u} {γ : Sort v} (a : α) [CoeFun α a γ] : γ :=
 @CoeFun.coe α a γ _
 
-abbrev coeSort {α : Sort u} {γ : Sort v} (a : α) [CoeSort α a γ] : γ :=
-@CoeSort.coe α a γ _
+abbrev coeSort {α : Sort u} {β : Sort v} (a : α) [CoeSort α a β] : β :=
+@CoeSort.coe α a β _
 
 instance coeDepTrans {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α a β] [CoeDep β (coeTC a) δ] : CoeTC α a δ :=
 { coe := coeD (coeTC a : β) }
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 194fde9fe4..c6c468e9f3 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -261,6 +261,7 @@ fun ctx s =>
   | EStateM.Result.error ex newS => EStateM.Result.error (fromMetaException ctx ref ex) (fromMetaState ref ctx s newS oldTraceState)
 
 def ppGoal (ref : Syntax) (mvarId : MVarId) : TermElabM Format := liftMetaM ref $ Meta.ppGoal mvarId
+def isType (ref : Syntax) (e : Expr) : TermElabM Bool := liftMetaM ref $ Meta.isType e
 def isDefEq (ref : Syntax) (t s : Expr) : TermElabM Bool := liftMetaM ref $ Meta.approxDefEq $ Meta.isDefEq t s
 def inferType (ref : Syntax) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.inferType e
 def whnf (ref : Syntax) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.whnf e
@@ -507,27 +508,6 @@ fun stx expectedType? => do
   stx' ← exp stx;
   withMacroExpansion stx stx' $ elabTerm stx' expectedType?
 
-/--
-  Make sure `e` is a type by inferring its type and making sure it is a `Expr.sort`
-  or is unifiable with `Expr.sort`, or can be coerced into one. -/
-def ensureType (ref : Syntax) (e : Expr) : TermElabM Expr := do
-eType ← inferType ref e;
-eType ← whnf ref eType;
-if eType.isSort then
-  pure e
-else do
-  u ← mkFreshLevelMVar ref;
-  condM (isDefEq ref eType (mkSort u))
-    (pure e)
-    (do -- TODO try coercion to sort
-        throwError ref "type expected")
-
-/-- Elaborate `stx` and ensure result is a type. -/
-def elabType (stx : Syntax) : TermElabM Expr := do
-u ← mkFreshLevelMVar stx;
-type ← elabTerm stx (mkSort u);
-ensureType stx type
-
 @[inline] def withLCtx {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : TermElabM α) : TermElabM α :=
 adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := localInsts, .. ctx }) x
 
@@ -647,6 +627,47 @@ match expectedType? with
 | none => pure e
 | _    => do eType ← inferType ref e; ensureHasTypeAux ref expectedType? eType e
 
+/-
+  Relevant definitions:
+  ```
+  class CoeSort (α : Sort u) (a : α) (β : outParam (Sort v))
+  abbrev coeSort {α : Sort u} {β : Sort v} (a : α) [CoeSort α a β] : β :=
+  ``` -/
+private def tryCoeSort (ref : Syntax) (α : Expr) (a : Expr) : TermElabM Expr := do
+β ← mkFreshTypeMVar ref;
+u ← getLevel ref α;
+v ← getLevel ref β;
+let coeSortInstType := mkAppN (Lean.mkConst `CoeSort [u, v]) #[α, a, β];
+mvar ← mkFreshExprMVar ref coeSortInstType MetavarKind.synthetic;
+let mvarId := mvar.mvarId!;
+catch
+  (condM (synthesizeInstMVarCore ref mvarId)
+    (pure $ mkAppN (Lean.mkConst `coeSort [u, v]) #[α, β, a, mvar])
+    (throwError ref "type expected"))
+  (fun ex =>
+    match ex with
+    | Exception.ex (Elab.Exception.error errMsg) => throwError ref ("type expected" ++ Format.line ++ errMsg.data)
+    | _ => throwError ref "type expected")
+
+/--
+  Make sure `e` is a type by inferring its type and making sure it is a `Expr.sort`
+  or is unifiable with `Expr.sort`, or can be coerced into one. -/
+def ensureType (ref : Syntax) (e : Expr) : TermElabM Expr :=
+condM (isType ref e)
+  (pure e)
+  (do
+    eType ← inferType ref e;
+    u ← mkFreshLevelMVar ref;
+    condM (isDefEq ref eType (mkSort u))
+      (pure e)
+      (tryCoeSort ref eType e))
+
+/-- Elaborate `stx` and ensure result is a type. -/
+def elabType (stx : Syntax) : TermElabM Expr := do
+u ← mkFreshLevelMVar stx;
+type ← elabTerm stx (mkSort u);
+ensureType stx type
+
 /- =======================================
        Builtin elaboration functions
    ======================================= -/