Very confusing error in simple code, Coq-like style

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

The following code (admittedly in Coq/SF style) produces the error, "unknown variable _f_1". Confusing at best.

inductive bvar : Type
| mk (n : ℕ)

def bvar_eq : bvar → bvar → bool
| (bvar.mk n1) (bvar.mk n2) := n1=n2

inductive bExpr : Type
| BLit (b: bool)
| BVar (v: bvar)

def benv := bvar → bool

def bEval : bExpr → benv → bool
| (bExpr.BLit b) i := b
| (bExpr.BVar v) i := i v

def init_benv : benv := λ v, ff

def update_benv : benv → bvar → bool → benv
| i v b := λ v2, if (bvar_eq v v2) then b else (i v2)

inductive bCmd : Type
| bAssm (v : bvar) (e : bExpr)
| bSeq (c1 c2 : bCmd)

def cEval : benv → bCmd → benv
| i0 c :=   match c with
            | (bCmd.bAssm v e) := update_benv i0 v (bEval e i0)
            | (bCmd.bSeq c1 c2) :=
                let i1 := (cEval i0 c1) in (cEval i1 c2)
            end

def myFirstProg := bCmd.bAssm (bvar.mk 0) (bExpr.BLit ff)

def newEnv := cEval init_benv myFirstProg

eval newEnv (bvar.mk 0)

Steps to Reproduce

1. Elaborate the code

Expected behavior:

No error or reasonable error message.

Actual behavior: [What actually happens]

Confusing error message, apparently revealing internal details.

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

Reliably reproduces.

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Windows. Current version of Lean.

Start by reproducing the supplied code and checking the reported error with the current Lean version. Trace the compiler path that produces the “unknown variable _f_1” message. Done means the same input produces no error or a clear, user-facing diagnostic instead of an internal variable name.