`flip filter` fails to unify: where do the constraints go?

[chenzizhao]

flip filter and flip map used to work (at least in January) and now it throws a type error:

:t (flip filter)
Type error:
Expected: (a -> b -> c)
  Actual: ((d -> Bool) -> (Ix e) ?=> (e => d) -> List d)
(Solving for: [a, b, c, d, e])

If I define two functions and the only difference is where I explicitly place the constraint, flipping them gives different errors:

def myfunc {n} (x:Bool) [Ix n] (y:n=>Bool) : Unit = todo
def myfunc2 {n} [Ix n] (x:Bool)(y:n=>Bool) : Unit = todo

:t flip myfunc -- gives the same (surprising) error as flip filter
Type error: 
Expected: (a -> b -> c)
  Actual: (Bool -> (Ix d) ?=> (d => Bool) -> Unit)
(Solving for: [a, b, c, d])

:t flip myfunc2 -- gives a less surprising error
Type error:Ambiguous type variable

I can certainly avoid using flip, but thought this is a good opportunity to ask where should the constraints go in the function signature (functionally and aesthetically)?

[dougalm]

Thanks for the bug! This looks like an unintended consequence of the recent change that added implicit quantification (https://github.com/google-research/dex-lang/pull/699). One fix would be to avoid interleaving the Ix n constraints when we add them implicitly. That's not always possible, because they might mention earlier binders, but we could just abandon implicit quantification in that case. It's only meant as a convenience feature.

As a workaround, let's add the Ix constraints to filter and map explicitly in the usual order: implicit args ({..}) followed by constraints ([..]), followed by ordinary args.

[chenzizhao]

That's super clear @dougalm thank you for the reply! I'll close this issue as it seems much easier to address in the userspace.

[apaszke]

I think we should still keep it open, because it's certainly not an intended consequence of automatic quantification. I think a good fix here would be to try to hoist the quantified constraints as high up as possible, which would leave us with the usual ordering of binders suggested by Dougal.