feat: allow interpolation of fvars, with a warning

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 []

Qq/Macro.lean

@@ -253,8 +253,12 @@ 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 _ ← 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))

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