bizarre `slim_check` bug`

Stream: mathlib4

[Eric Rodriguez]

import Mathlib.Tactic.SlimCheck

open Classical

theorem s (y z : ℕ) (hy : y ≤ 5) (hz : z ≤ 5) : y * 2 + z * 2 ≠ 1 := by slim_check
/-
failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.propDecidable', and it does not have executable code
-/

All of this is minimal as far as I can see; reducing the numbers seems to just give a normal error. I can see that probably using slim_check with Classical open is going to give weird results.

[Henrik Böving]

Without any debug work my guess is: TC synthesis gets changed by open classical which causes slim check to attempt to use noncomputable functionality for its fuzzing.

[Henrik Böving]

Its not quite clear to me how go fix this? Maybe we can lower the priority of the propDecidable instance such that it doesn't pick up on it? Or maybe we could even equip tc synthesis with a flag to explicitly ignore all non computable things for applications like this.

[Sébastien Gouëzel]

Or slim_check could complain if Classical is open (which is a bad move most of the time anyway).

[Henrik Böving]

But that only mitigates the issue. In general if you have any noncomputable instance related to decidability around, this will break slim_check.