Inconsistency in sizes going out of scope

[athas]

This does not work:

def takefrom 't (xs: []t) (i: i64) : [i+1]t = take (i+1) xs

entry main n (xs: []i32) =
  n |> takefrom xs

Cannot apply "|>" to "takefrom xs" (invalid type).
Expected: a₂ -> b₃
Actual:   (i: i64) -> [i + 1]i32

Parameter(s) "i" used as size(s) would go out of scope.

But it works if we use this definition of takefrom:

def takefrom 't (xs: []t) (i: i64) : [i]t = take i xs

In this case the size that goes out of scope is just turned into an existential. I suspect the code that detects this case does not handle nontrivial expressions properly. I see no reason not to always decay to an existential in such cases.