fix: renable some slim check tests and make them pass (#9021)

Previously `addDecorations` was creating ill-typed expressions that in the presence of function types placed a `Type` where a `Prop` was expected.

A few of the tests needed some minor fixes to make them pass.

Mathlib/Tactic/SlimCheck.lean

@@ -168,7 +168,7 @@ elab_rules : tactic | `(tactic| slim_check $[$cfg]?) => withMainContext do
   let cfg ← elabConfig (mkOptionalNode cfg)
   let (_, g) ← (← getMainGoal).revert ((← getLocalHyps).map (Expr.fvarId!))
   let tgt ← g.getType
-  let tgt' := addDecorations tgt
+  let tgt' ← addDecorations tgt
   let cfg := { cfg with
     traceDiscarded := cfg.traceDiscarded || (← isTracingEnabledFor `slim_check.discarded),
     traceSuccesses := cfg.traceSuccesses || (← isTracingEnabledFor `slim_check.success),

Mathlib/Testing/SlimCheck/Testable.lean

@@ -388,6 +388,20 @@ where
     let finalR := addInfo s!"{var} is irrelevant (unused)" id r
     pure $ imp (· $ Classical.ofNonempty) finalR (PSum.inr $ λ x _ => x)
 
+instance (priority := 2000) subtypeVarTestable {p : α → Prop} {β : α → Prop}
+    [∀ x, PrintableProp (p x)]
+    [∀ x, Testable (β x)]
+    [SampleableExt (Subtype p)] {var'} :
+    Testable (NamedBinder var $ Π x : α, NamedBinder var' $ p x → β x) where
+  run cfg min :=
+    letI (x : Subtype p) : Testable (β x) :=
+      { run := fun cfg min => do
+          let r ← Testable.runProp (β x.val) cfg min
+          pure $ addInfo s!"guard: {printProp (p x)} (by construction)" id r (PSum.inr id) }
+    do
+      let r ← @Testable.run (∀ x : Subtype p, β x.val) (@varTestable var _ _ _ _) cfg min
+      pure $ iff Subtype.forall' r
+
 instance (priority := low) decidableTestable {p : Prop} [PrintableProp p] [Decidable p] :
     Testable p where
   run := λ _ _ =>
@@ -493,16 +507,18 @@ open Lean
 
 /-- Traverse the syntax of a proposition to find universal quantifiers
 quantifiers and add `NamedBinder` annotations next to them. -/
-partial def addDecorations (e : Expr) : Expr :=
-  e.replace $ λ expr =>
-    match expr with
-    | Expr.forallE name type body data =>
+partial def addDecorations (e : Expr) : MetaM Expr :=
+  Meta.transform e $ fun expr => do
+    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 newType ← addDecorations type
+      let newBody ← addDecorations body
       let rest := Expr.forallE name newType newBody data
-      some $ mkApp2 (mkConst `SlimCheck.NamedBinder) (mkStrLit n) rest
-    | _ => none
+      return .done $ (← Meta.mkAppM `SlimCheck.NamedBinder #[mkStrLit n, rest])
+    else
+      return .continue
 
 /-- `DecorationsOf p` is used as a hint to `mk_decorations` to specify
 that the goal should be satisfied with a proposition equivalent to `p`
@@ -527,7 +543,7 @@ scoped elab "mk_decorations" : tactic => do
   let goal ← getMainGoal
   let goalType ← goal.getType
   if let .app (.const ``Decorations.DecorationsOf _) body := goalType then
-    closeMainGoal (addDecorations body)
+    closeMainGoal (← addDecorations body)
 
 end Decorations