diff --git a/examples/matching.lean b/examples/matching.lean
index a97fc97..c38bff1 100644
--- a/examples/matching.lean
+++ b/examples/matching.lean
@@ -58,4 +58,4 @@ def pairLit (u : Lean.Level) (α : Q(Type u)) (a : Q($α)) : MetaM Q($α × $α)
   | 0, ~q(Int), z => return q(($z, $z))
   | _, _, _ => failure
 
-#eval do guard <| (←pairLit 0 q(Nat) q(2)) == q((2, 2))
+#eval show MetaM Unit from do guard <| (←pairLit _ _ q(2)) == q((2, 2))
diff --git a/lean-toolchain b/lean-toolchain
index f0a6d66..f90f8ec 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4-pr-releases:pr-release-3060