fix(slim_check): do not crash when binders contain a function type (#…

…11231)

Previously
```lean
import Mathlib

open scoped BigOperators in
example (n : ℕ) : ∑ f : Unit → Fin (n + 1), f () = 0 := by slim_check
```
failed with
```
application type mismatch
  SlimCheck.NamedBinder "a._@._hyg.23" (Unit → Fin (n + 1))
argument
  Unit → Fin (n + 1)
has type
  Type : Type 1
but is expected to have type
  Prop : Type
```

Mathlib/Testing/SlimCheck/Testable.lean

@@ -509,8 +509,8 @@ open Lean
 quantifiers and add `NamedBinder` annotations next to them. -/
 partial def addDecorations (e : Expr) : MetaM Expr :=
   Meta.transform e fun expr => do
-    if not (← Meta.inferType e).isProp then
-      return .continue
+    if not (← Meta.inferType expr).isProp then
+      return .done expr
     else if let Expr.forallE name type body data := expr then
       let newType ← addDecorations type
       let newBody ← Meta.withLocalDecl name data type fun fvar => do

test/slim_check.lean

@@ -413,6 +413,21 @@ issue: ⋯ does not hold
     exact test_sorry
   trivial
 
+open scoped BigOperators in
+example (n : ℕ) : true := by
+  have : ∑ f : Unit → Fin (n + 1), f () = 0 := by
+    success_if_fail_with_msg "
+===================
+Found problems!
+n := 1
+issue: 1 = 0 does not hold
+(0 shrinks)
+-------------------
+"
+      slim_check (config := { randomSeed := some 257 })
+    exact test_sorry
+  trivial
+
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/slim_check.20question/near/412709012
 open scoped BigOperators in
 /--