This program should be rejected by the type checker

[athas]

let main [n] (xs: [n]i32) (ys: [n]i32) =
  loop (xs,ys) for i < 10 do
  let zs = filter (>0) (map2 (+) xs ys)
  in (xs, zs)

Something is (unsurprisingly) wrong with the size inference for loops.