Type checker does not detect size mismatch in loop

[athas]

This leads to a crash later in compilation.

def hide [m] (aoa_shp: [m]i32) : ?[n].[n]i32 =
  filter (!=0) aoa_shp

entry main [n] (iv : [n]bool) =
  loop (wrk, wrk_shp) = (iv,  [(i32.i64 n)]) for _i < 2 do
  let flags = hide wrk_shp
  let min = zip flags wrk -- There is no way 'wrk' can have the right shape here.
  in (wrk ++ wrk, wrk_shp ++ wrk_shp)

I remember fixing a similar bug about a year ago.

[athas]

Similar to #1565.

[athas]

The problem is that we take the existential size produced by hide and promote it to a loop-carried size, which is nonsensical. The type checker should check the binding level before doing that.