Some programs are valid but cannot be generated if necessary data has been erased from the runtime.
For example below cannot_copy() typechecks but it cannot be generated at runtime because n has been erased.
func cannot_copy(0 u64_t n, array_t(i32_t, n) xs) -> array_t(i32_t, n)
{
return xs;
}