Can Dex actually allow question marks in array sizes?

[axch]

I tried to define a function specialized to a flat array with an anonymous (unknown) size, like so:

def fin_mean (xs: (Fin _)=>Float) : Float =
  mean xs

and I got this:

Not implemented:
Please report this at github.com/google-research/dex-lang/issues

Type inference of this program requires delayed interface resolution

def fin_mean (xs: (Fin _)=>Float) : Float =
                   ^^^^^^^^^^^^^

This doesn't block anything for me, because it's easy enough to just add the implicit Nat argument to serve as a name for the size, but the gap seems unaesthetic.

[apaszke]

Well, a type annotation is an expression, so whenever you say _ it means "this can be inferred". But in this case it can't, because there's nothing to provide the size of xs! I read your issue as expecting _ to automatically make the function polymorphic, but _ never introduces any more binders/polymorphism!

[axch]

Hm. Then "not implemented" is probably not a good error message.

[apaszke]

I agree it's not good. But putting an extra inference variable in there does hit a not implemented case in inference, so it's also true. We used to support this before safer names, but not anymore.