Compiler is not checking usage of erased arguments

[elmattic]

Here is a minimal code sample to reproduce the error:

foo<size: Nat>(dummy: Word(size)): Word(size)
  Word.zero(size)

Main: IO(Unit)
  do IO {
    let x = 7
    let w = Word.from_bits(4, Nat.to_bits(x)) :: Word(4);
    let z = foo<_>(w)
    let nat = Nat.show(Word.to_nat<_>(z))
    IO.print("Hello, Formality! " | nat)
  }

Error:

Compilation error.
ReferenceError: _size$1 is not defined

[elmattic]

I am adding another sample code:

// TAKE

Nat.min.left_zero(a: Nat): 0 == Nat.min(a, 0)
  case a {
    zero: refl
    succ: refl
  }!

Word.take(size: Nat)(len: Nat, word: Word(size)): Word(Nat.min(size, len))
  case len {
    zero: Word.e :: rewrite x in Word(x) with Nat.min.left_zero(size)
    succ: case word {
      e: Word.e,
      o: Word.o!(Word.take<word.size>(len.pred, word.pred)),
      i: Word.i!(Word.take<word.size>(len.pred, word.pred))
    }!
  }!

// MAIN

Main: IO(Unit)
  do IO {
    let x = 7

    let w = Word.from_bits(4, Nat.to_bits(x)) :: Word(4);
    let z = Word.take<_>(1, w) // should be 1 :: Word(1)
    let nat = Nat.show(Word.to_nat<_>(z))

    IO.print("Hello World! " | nat)
  }

Error:

base$ kind Main --run
Compilation error.
ReferenceError: _word$size$5 is not defined

Note that putting parens doesn't help as a workaround.

[algebraic-dev]

Closed because the repository now only contains the code for the Kind2 language.