Value set size should be compile-time known

[hackedy]

The size argument to a value set should be a nat/int by the time it reaches the typed AST. So the typechecker should do that compile-time evaluation.

[hackedy]

@MollyDream