From b7ff0165ea59352853cb00c1e7bb26cb26cdbcc1 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 2 Nov 2024 14:13:21 +0000
Subject: [PATCH 1/2] =?UTF-8?q?style:=20replace=20`=E2=86=90=20pure`=20wit?=
 =?UTF-8?q?h=20`:=3D`=20in=20matches?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Qq/ForLean/ReduceEval.lean | 2 +-
 Qq/Macro.lean              | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Qq/ForLean/ReduceEval.lean b/Qq/ForLean/ReduceEval.lean
index 97f8577..fe14353 100644
--- a/Qq/ForLean/ReduceEval.lean
+++ b/Qq/ForLean/ReduceEval.lean
@@ -8,7 +8,7 @@ def throwFailedToEval (e : Expr) : MetaM α :=
 
 private partial def evalList [ReduceEval α] (e : Expr) : MetaM (List α) := do
   let e ← whnf e
-  let .const c _ ← pure e.getAppFn | throwFailedToEval e
+  let .const c _ := e.getAppFn | throwFailedToEval e
   let nargs := e.getAppNumArgs
   match c, nargs with
     | ``List.nil, 1 => pure []
diff --git a/Qq/Macro.lean b/Qq/Macro.lean
index 4c52ba7..4f1a5ea 100644
--- a/Qq/Macro.lean
+++ b/Qq/Macro.lean
@@ -254,7 +254,7 @@ partial def unquoteExpr (e : Expr) : UnquoteM Expr := do
     }
     return fv
   let e ← whnf e
-  let .const c _ ← pure e.getAppFn | throwError "unquoteExpr: {e} : {eTy}"
+  let .const c _ := e.getAppFn | throwError "unquoteExpr: {e} : {eTy}"
   let nargs := e.getAppNumArgs
   match c, nargs with
     | ``betaRev', 2 => return betaRev' (← unquoteExpr (e.getArg! 0)) (← unquoteExprList (e.getArg! 1))

From f95d85e967f194416e8801e9ebdc7fd59ce29203 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 2 Nov 2024 14:46:40 +0000
Subject: [PATCH 2/2] feat: allow interpolation of fvars, with a warning

---
 Qq/Macro.lean                    |  4 ++++
 examples/unquoteExprWarning.lean | 31 +++++++++++++++++++++++++++++++
 2 files changed, 35 insertions(+)
 create mode 100644 examples/unquoteExprWarning.lean

diff --git a/Qq/Macro.lean b/Qq/Macro.lean
index 4f1a5ea..d7ce920 100644
--- a/Qq/Macro.lean
+++ b/Qq/Macro.lean
@@ -253,6 +253,10 @@ partial def unquoteExpr (e : Expr) : UnquoteM Expr := do
       abstractedFVars := s.abstractedFVars.push fvarId
     }
     return fv
+  if let .fvar _ := e then
+    Lean.logWarning m!"Interpolated variable `{e}` should have type `Q(_)` not `{eTy}`. \
+      Adding `have {e} : Q(_) := {e}` may fix this."
+    return e
   let e ← whnf e
   let .const c _ := e.getAppFn | throwError "unquoteExpr: {e} : {eTy}"
   let nargs := e.getAppNumArgs
diff --git a/examples/unquoteExprWarning.lean b/examples/unquoteExprWarning.lean
new file mode 100644
index 0000000..d993386
--- /dev/null
+++ b/examples/unquoteExprWarning.lean
@@ -0,0 +1,31 @@
+import Lean
+import Qq.Macro
+
+open Qq
+open Lean Meta Elab Tactic Command
+
+elab "iff_constructor" : tactic => do
+  let mvarId ← getMainGoal
+  let goalType ← getMainTarget
+
+  let_expr Iff a b := goalType
+    | throwError "Goal type is not of the form `a ↔ b`"
+
+  let a : Q(Prop) := a
+  let b : Q(Prop) := b
+
+  let mvarId1 ← mkFreshExprMVar q($a → $b) (userName := `mp)
+  let mvarId2 ← mkFreshExprMVar q($b → $a) (userName := `mpr)
+
+  let mvarId1 : Q($a → $b) := mvarId1
+  let mvarId2 : Q($b → $a) := mvarId2
+
+  mvarId.assign q(@Iff.intro $a $b $mvarId1 $mvarId2)
+
+  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }
+
+example (p q : Prop) (h1 : p → q) (h2 : q → p) : p ↔ q := by
+  iff_constructor
+
+  case mp => assumption
+  case mpr => assumption