Very confusing error in simple code, Coq-like style

[kevinsullivan]

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.

[Vtec234]

By the way, here's a working version of cEval:

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

The issue is that well-founded recursion is resolved in the top-level match statement | i0 c so you need to move match c with .. into that. But agreed that the error is confusing, so the issue is still valid.