From 6ccaf3573dc3a1c49ba103e69c6337bb3f468741 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 23 Mar 2024 10:50:22 +0000
Subject: [PATCH] fix(slim_check): do not crash when binders contain a function
 type (#11231)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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 |  4 ++--
 test/slim_check.lean                    | 15 +++++++++++++++
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Testing/SlimCheck/Testable.lean b/Mathlib/Testing/SlimCheck/Testable.lean
index 131283467919f7..7f84a6b567d169 100644
--- a/Mathlib/Testing/SlimCheck/Testable.lean
+++ b/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
diff --git a/test/slim_check.lean b/test/slim_check.lean
index bef7c77904b483..aa764cc89305fc 100644
--- a/test/slim_check.lean
+++ b/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
 /--