Regression/bug in the pattern compiler?

[robdockins]

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

There appears to have been a regression in the pattern compiler sometime in the last few weeks. Pulling a recent lean caused me to start seeing an error produced in code that previously (modulo some syntactic changes) would be accepted.

Steps to Reproduce

1. Compile the attached bugmin.lean file via:

LEAN_PATH=/usr/local/lib/lean/library:. /usr/local/bin/lean --make bugmin.lean

Expected behavior:

File should compile without errors.

Actual behavior:

Lean complains:

bugmin.lean:37:4: error: unknown free variable: _fresh.4.2315

Reproduces how often:
100% reproducible. However, the error is very fragile under code changes; removing apparently-redundant pattern matches or monadic binds, or even changing the constant nat value in the affected pattern matches can cause the problem to disappear.

Versions

$ lean --version
Lean (version 4.0.0, commit 4b49aa4b5040, Release)

macOS 10.14.6.

Additional Information

Github doesn't accept .lean files, so rename...
bugmin.lean.txt