#check issue with native_decide

[arthur-adjedj]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Using native_decide in #check can trick #check into believing something is well-typed when it shouldn't be, The following code doesn't raise any error:

#check show False by native_decide

See associated Zulip thread

Steps to Reproduce

Expected behavior:
#check should reject this and give an error

Actual behavior:
#check acts as if the term produced was well-formed, and prints this:

let_fun this := of_decide_eq_true (Lean.ofReduceBool _check._nativeDecide_1 true (Eq.refl true));
this : False

Reproduces how often:
100%

Versions

4.0.0-nightly-2023-01-16
Windows 11