Infinite loop in type checker

[athas]

def f [n] (dmax: i64) (depth: [n]i64) (value: [n]i32) (parent: [n]i64) : []i32 =
  loop value for d in dmax..dmax-1...1 do
    reduce_by_index
    (copy value)
    (+)
    0i32
    (map (\i -> if depth[i] == d then parent[i] else -1) (iota (length value)))
    value

Probably in loop size analysis, which runs a convergence loop. This program is not well typed, so we should definitely report a type error.

[athas]

This program has the same problem, although for arbitrary reasons the type checker doesn't go into an infinite loop, but does complain about it in a late sanity check:

entry main (xs: []i32) = zip (iota (length xs)) xs

The problem is that xs gets inferred as having type [length xs]i32. Similarly, in the first program above, the loop parameter value is inferred as having size length value. That's of course not sensible.