Inconsistent sizes when having both polymorphic and unknown sizes

[catvayor]

This program should not type, but it does (the compiler even manage to produce code):

let foo [n] = (iota n, filter (>5) (iota n))

entry main (n:i64) =
    let t1 = iota n
    let (f1f, f1s) = foo
    let r11 = zip f1f t1

    let t2 = iota (2*n)
    let (f2f, f2s) = foo
    let r12 = zip f2f t2

    in ((r11 ++ r12), zip f2s f1s)

I think the problem comes from the fact that foo don't have explicit arguments, and so consider that the size it produce should be global, even if it in fact depends of the polymorphic argument n, then f1s and f2s are wrongly considered of same size...

This can be easily seen in the typing production:

def foo [n] : ?[d₄][d₄].([n]i64, [d₄]i64) =
  (iota n, filter (> 5) (iota n))

entry main ((n: i64): i64) : (*[n + 2 * n](i64, i64), *[d₄](i64, i64)) =
  let (t1: [n]i64) =
    iota n
  let ((f1f: [n]i64), (f1s: [d₄]i64)) = foo
  let (r11: [n](i64, i64)) =
    zip f1f t1

  let (t2: [2 * n]i64) =
    iota (2 * n)
  let ((f2f: [2 * n]i64), (f2s: [d₄]i64)) = foo
  let (r12: [2 * n](i64, i64)) =
    zip f2f t2

  in ((r11 ++ r12), zip f2s f1s)

version commit:

. futhark --version
Futhark 0.26.0 (prerelease - include info below when reporting bugs)
git: 00d8d95 (Sun Jul 23 23:12:10 2023 +0200

[athas]

Yes, we've had other bugs related to the fact that polymorphic bindings are essentially functions.

How do we fix this? One problem is that we don't have anywhere to plug in unknown sizes that are produced by polymorphic instantiation. Specifically, a Var is not an AppExp. It could become one, of course.

We could also simply ban polymorphic values from having an existential type. It's probably not useful. I want to keep both polymorphic values and existential values, but they are on their own somewhat rare features, and their combination is highly unusual.

[catvayor]

Maybe we can consider the size parameters as parameters for the checking of adding the unknown or not ?
If Apply was not requiring a NE.NonEmpty of arguments, we could then have done a case of variable typing so that if a variable is polymorphic with existential type, it is converted to function application with 0 argument. Else I don't really know how to deal with these.

Making Var an AppExp sounds like a bit too much for such a specific (and contrived) case, I don't think its the right thing to do. Or, if it is done, it should probably be the case for every construction, which lead to deep reworking of typing and internalisation, so should probably not be done just for this reason.

Note that formalisation forbid this, even if we could have authorized them, as every construction act like AppExp in it.

[athas]

The most principled solution is to make Var an AppExp. The easiest solution is to forbid the definition of foo. Sometimes it's better to impose a somewhat ad-hoc restriction in order to keep the implementation simpler.