fix(Testing/SlimCheck/Testable): do not call inferType on an expres…

…sion with `bvar`s (leanprover-community#9722)

Fixes a bug reported twice on Zulip:
* https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/slim_check.20question/near/412709012
* https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/slim_check.20giving.20wrong.20counterexamples.3F/near/420008365

Both test-cases are included

Mathlib/Testing/SlimCheck/Testable.lean

@@ -512,11 +512,11 @@ partial def addDecorations (e : Expr) : MetaM Expr :=
     if not (← Meta.inferType e).isProp then
       return .continue
     else if let Expr.forallE name type body data := expr then
-      let n := name.toString
       let newType ← addDecorations type
-      let newBody ← addDecorations body
+      let newBody ← Meta.withLocalDecl name data type fun fvar => do
+        return (← addDecorations (body.instantiate1 fvar)).abstract #[fvar]
       let rest := Expr.forallE name newType newBody data
-      return .done <| (← Meta.mkAppM `SlimCheck.NamedBinder #[mkStrLit n, rest])
+      return .done <| (← Meta.mkAppM `SlimCheck.NamedBinder #[mkStrLit name.toString, rest])
     else
       return .continue
 

test/slim_check.lean

@@ -410,3 +410,28 @@ issue: ⋯ does not hold
     slim_check (config := { randomSeed := some 257 })
   admit
   trivial
+
+-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/slim_check.20question/near/412709012
+open scoped BigOperators in
+/--
+info: Success
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+example (q : ℕ) : q = 0 ∨ q ≥ 2 ∨
+    8 = ∑ k in Finset.range 2, 5 ^ k * Nat.choose (2 * q + 1) (2 * k + 1) := by
+  slim_check
+
+-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/slim_check.20giving.20wrong.20counterexamples.3F/near/420008365
+open Nat in
+/--
+info: Success
+---
+warning: declaration uses 'sorry'
+-/
+#guard_msgs in
+theorem testBit_pred :
+    testBit (pred x) i = (decide (0 < x) &&
+      (Bool.xor ((List.range i).all fun j => ! testBit x j) (testBit x i))) := by
+  slim_check