Lean: newtype test fails

[protoben]

The newtype Lean test fails with the following message:

error: ././././Out.lean:99:2: invalid match-expression, pattern contains metavariables
  C w
error: Lean exited with code 1

[ineol]

@bacam How does Coq deal with this?

It seems that it boils down to this, with n being unconnected to the constructor C, and a quick test with jsCoq online didn't work...

Inductive constrained {n : nat} (*member_Z_list n [32; 64]*) :=
| C : nat -> constrained.
Arguments constrained : clear implicits.


Definition main '(tt : unit) : unit :=
   let z := C 32 in
   match z with | C w => tt end.

For completeness, the input program is the following:

newtype wrapper = Wrapper : bits(5)

newtype constrained('n), 'n in {32, 64} = C : int('n)

function main() -> unit = {
  let x = Wrapper(0b00100);
  match x {
    Wrapper(y) => print_bits("y = ", y)
  };
  let z = C(32);
  match z {
    C(w) => print_int("w = ", w)
  }
}

[bacam]

It's currently an expected failure (BTW, there are reasons for expected failures in test/c/run_tests.py). Really, we only need one of the type-level and term-level integers to appear in the translation, a bit like the merging we do for functions.