From d7b83654cd9982f081647a7c956243a27e38d769 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Tue, 2 Apr 2024 23:42:32 +0100
Subject: [PATCH] fix: workaround leanprover/lean4#3827 (#41)

Once it lands in a release, the change in leanprover/lean4#3820 to detect accidental do lifting misfires on quotations.
To avoid breakage later, we manually lift out this expression.
---
 Qq/Match.lean | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

diff --git a/Qq/Match.lean b/Qq/Match.lean
index c7199cd..abe4cfc 100644
--- a/Qq/Match.lean
+++ b/Qq/Match.lean
@@ -110,18 +110,20 @@ def makeMatchCode {γ : Q(Type)} {m : Q(Type → Type v)} (_instLift : Q(MonadLi
     decls.map fun decl => { decl with ty := decl.ty.map fun e => replaceTempExprsByQVars decls e }
   let next ← withLocalDeclD (← mkFreshBinderName) (mkIsDefEqType decls) fun fv => do
     let fv : Q($(mkIsDefEqType decls)) := fv
+    -- note: cannot inline into `$body` due to leanprover/lean4#3827
+    let body ← mkQqLets nextDecls fv do
+      have pat : Q(Quoted $ty) := replaceTempExprsByQVars decls pat
+      let (_, s) ← unquoteLCtx.run { mayPostpone := (← read).mayPostpone }
+      let _discr' ← (unquoteExpr discr).run' s
+      let _pat' ← (unquoteExpr pat).run' s
+      withLocalDeclDQ (← mkFreshUserName `match_eq) q(QuotedDefEq $discr $pat) fun h => do
+        let res ← k expectedType
+        let res : Q($m $γ) ← instantiateMVars res
+        let res : Q($m $γ) := (← res.abstractM #[h]).instantiate #[q(⟨⟩ : QuotedDefEq $discr $pat)]
+        return res
     let next : Q($m $γ) :=
       q(if $(mkIsDefEqResultVal decls fv) then
-          $(← mkQqLets nextDecls fv do
-            have pat : Q(Quoted $ty) := replaceTempExprsByQVars decls pat
-            let (_, s) ← unquoteLCtx.run { mayPostpone := (← read).mayPostpone }
-            let _discr' ← (unquoteExpr discr).run' s
-            let _pat' ← (unquoteExpr pat).run' s
-            withLocalDeclDQ (← mkFreshUserName `match_eq) q(QuotedDefEq $discr $pat) fun h => do
-              let res ← k expectedType
-              let res : Q($m $γ) ← instantiateMVars res
-              let res : Q($m $γ) := (← res.abstractM #[h]).instantiate #[q(⟨⟩ : QuotedDefEq $discr $pat)]
-              return res)
+          $body
         else
           $alt)
     return show Q($(mkIsDefEqType decls) → $m $γ) from