Interpreter crash

[athas]

def f [n] (reps:[n]i64) : ?[m].[m]i64 =
  iota (reduce (+) 0 reps)

entry main arr = length (f (map (\x -> x) arr))

[athas]

This is because while map (\x -> x) arr) does end up occurring in a size expression, and has bindings which we do not allow, it is not itself a size - in fact, it is not even scalar. Thus replacing it with an unknown size is not sensible. We should replace the entire size expression where it occurs with an unknown size.

[athas]

Another reason this happens is that the return type ascription is ignored for some reason, and this more precise type is inferred:

def f [n] (reps:[n]i64) : [reduce (+) 0 reps]i64 =
  iota (reduce (+) 0 reps)

entry main arr = length (f (map (\x -> x) arr))

[athas]

Actually, maybe this is fine, and we just need to change our conception of "unknown size" to "unknown value", and the interpreter shouldn't assume it's an i64. The compiler handles it fine already.