silent overflow with large integers

[kbuzzard]

Prerequisites

• [X ] 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.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

For large integers in a certain range (possibly system dependent), lean can fail to produce any error at all when overflow issues occur.

Steps to Reproduce

$ lean --version
Lean (version 3.3.1, nightly-2018-04-06, commit 8f55ec4c5037, Release)
$ more wrong.lean 
example : 1000 * 1000 = 123456 := rfl -- no error reported
$ lean -t0 wrong.lean 
$

Expected behavior: [What you expect to happen]

Some indication that the assertion has not been proved, e.g.

type mismatch, term
  rfl
has type
  ?m_2 = ?m_2
but is expected to have type
  1000 * 1000 = 123456

or

deep recursion was detected at 'replace' (potential solution: increase stack space in your system)

Actual behavior: [What actually happens]

No error reported.

Reproduces how often: [What percentage of the time does it reproduce?]

For me, 100%, although @gebner reported that he had to use larger numbers to reproduce the problem e.g. example : 1000*1000*100 + 0 = 1000*1000*100 + 1 := rfl

Versions

Nightly of 6th April 2018, Ubuntu 16.04.

Additional Information

Let it be clear that Lean is not proving 1000 * 1000 = 123456 here. It is catching the error but simply failing to report it. Any attempt to name the false statement, somehow add it to the local context, or to try to use it in any way (e.g. theorem X : 1000 * 1000 = 123456 := rfl) correctly reports an error.

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/silent.20overflow contains a little more information about what is going on.