From 0595e8a78a3b0a4bf2f194ddcec7c22ff60f90af Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 27 Mar 2020 11:20:43 -0700
Subject: [PATCH] feat: add `tryPureCoe`

@Kha It seems to work reasonably well. It didn't break any test.
---
 src/Init/Lean/Elab/Term.lean   | 24 +++++++++++++++++++++++-
 tests/lean/run/tryPureCoe.lean | 28 ++++++++++++++++++++++++++++
 2 files changed, 51 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/tryPureCoe.lean

diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index c9fde4400e..921896caab 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -524,6 +524,18 @@ match result with
 | LOption.undef    => throwError ref ("failed to synthesize instance" ++ indentExpr type)
 | LOption.none     => throwError ref ("failed to synthesize instance" ++ indentExpr type)
 
+/--
+  Try to coerce `a : α` into `m β` by first coercing `a : α` into ‵β`, and then using `pure`.
+  The method is only applied if the head of `α` nor ‵β` is not a metavariable. -/
+private def tryPureCoe? (ref : Syntax) (m β α a : Expr) : TermElabM (Option Expr) :=
+if β.getAppFn.isMVar || α.getAppFn.isMVar then pure none
+else catch
+ (do
+   aNew ← tryCoe ref β α a none;
+   aNew ← liftMetaM ref $ Meta.mkPure m aNew;
+   pure $ some aNew)
+ (fun _ => pure none)
+
 /-
 Try coercions and monad lifts to make sure `e` has type `expectedType`.
 
@@ -532,7 +544,11 @@ Otherwise, we just use the basic `tryCoe`.
 
 Extensions for monads.
 
-Given an expected type of the form `n β` and a given type `eType` is of the form `m α`. We use the following approaches.
+Given an expected type of the form `n β`, if `eType` is of the form `α`
+
+1 - Try to coerce ‵α` into ‵β`, and use `pure` to lift it to `n α`.
+
+If `eType` is of the form `m α`. We use the following approaches.
 
 1- Try to unify `n` and `m`. If it succeeds, then we rely on `tryCoe`, and
    the instances
@@ -578,7 +594,13 @@ since this goal does not contain any metavariables. And then, we
 convert `g x` into `liftM $ g x`.
 -/
 def tryLiftAndCoe (ref : Syntax) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr) : TermElabM Expr := do
+eType ← instantiateMVars ref eType;
 some ⟨n, β, monadInst⟩ ← isMonad? ref expectedType | tryCoe ref expectedType eType e f?;
+β ← instantiateMVars ref β;
+eNew? ← tryPureCoe? ref n β eType e;
+match eNew? with
+| some eNew => pure eNew
+| none      => do
 some (m, α) ← isTypeApp? ref eType | tryCoe ref expectedType eType e f?;
 condM (isDefEq ref m n) (tryCoe ref expectedType eType e f?) $
   catch
diff --git a/tests/lean/run/tryPureCoe.lean b/tests/lean/run/tryPureCoe.lean
new file mode 100644
index 0000000000..bd46d63ab3
--- /dev/null
+++ b/tests/lean/run/tryPureCoe.lean
@@ -0,0 +1,28 @@
+new_frontend
+def m1 : IO Bool :=
+pure true
+
+def p (x : Nat) : Bool :=
+x > 0
+
+def tst1 : IO Bool :=
+true <&&> m1
+
+def tst2 (x : Nat) : IO Bool :=
+x = 0 <&&> m1
+
+def tst3 (x : Nat) : IO Unit :=
+whenM (m1 <&&> x > 0) $
+  throw $ IO.userError "test"
+
+def tst4 (x : Nat) : IO Unit :=
+whenM (x > 0 <&&> m1) $
+  throw $ IO.userError "test"
+
+def tst5 (x : Nat) : IO Unit :=
+whenM (p x <&&> m1) $
+  throw $ IO.userError "test"
+
+def tst6 (x : Nat) : IO Unit :=
+whenM (p x <&&> id m1) $
+  throw $ IO.userError "test"