algebraic data type vm check failed is_closure

[joehendrix]

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

I'm getting the following error on the file below, which was minimized from a larger module.

42:1: vm check failed: is_closure(o) (possibly due to incorrect axioms, or sorry)

Steps to Reproduce

Run lean on the following file

inductive type
| bv  : ℕ → type
| bit : type

open type

-- This is a "parameterized list" where `plist f types` contains
-- an element of type `f tp` for each corresponding element `tp ∈ types`.
inductive plist (f : type → Type) : list type → Type
| nil {} : plist []
| cons {h:type} {r:list type} : f h → plist r → plist (h::r)

-- Operations on values; the first argument contains the types of
-- inputs, and the second for the return type.
inductive op : list type → type → Type
| neq (tp:type) : op [tp, tp] bit
| mul (w:ℕ) : op [bv w, bv w] (bv w)

-- Denotes expressions that evaluate to a number given a memory state and register to value map.
inductive value : type → Type
| const (w:ℕ) : value (bv w)
| op {args:list type} {tp:type} : op args tp → plist value args → value tp

--- This creates a plist (borrowed from the list notation).
notation `[[[` l:(foldr `,` (h t, plist.cons h t) plist.nil) `]]]` := l

open value

-- This works
#eval value.op (op.mul 32) [[[ const 32, const 32 ]]]

-- This also works
instance bv_has_mul (w:ℕ) : has_mul (value (bv w)) := ⟨λx y, value.op (op.mul w) [[[x, y]]]⟩
#eval const 32 * const 32

-- This works
#eval value.op (op.neq (bv 32)) [[[ const 32, const 32 ]]]

-- This returns the VM check error
def neq {tp:type} (x y : value tp) : value bit := value.op (op.neq tp) [[[x, y]]]
#eval neq (const 32) (const 32)

Expected behavior: No errors or an error message explaining what definition is wrong.

Actual behavior: The vm check error above Reproduces how often: 100%

Versions

Lean (version 3.4.2, commit ceacfa744595, Release) on OSX 10.13.5.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.

[Kha]

Fixed in b13ac12. This turned out to be a pretty fundamental bug in the compiler with no practicable workaround.

[joehendrix]

Thanks, this fixed the immediate issue.

It turns out the definition still isn't quite what I'm looking for since the recursor value.rec doesn't seem to let one recursively visit the values inside plist. I think I'll need to build up a recursive value directly, and that seems to work.