spill: change default of bound var visibility for to-prop functions

[gares]

The new algorithm:

• walks backward until it finds an application of type X1 -> .. XN -> prop
• eta expand
• attach the spill (under the lambdas)
• sigma quantify spilled variables

once finished

• remove toplevel sigmas

[lweqx]

I'm trying to understand the changes, so first of all sorry if what I'm saying is irrelevant/off the mark.

Wouldn't it be better to systematically transform a spill {f x1 ... xn} occurring inside a (potentially partial) application f y1 ... {f x1 ... xn} ... yn of f: Y1 -> ... -> YN -> Z1 -> ... ZM -> prop into:

% transformation of `f y1 ... {f x1 ... xn} ... yn`
(z1\ ... zm\ sigma Spilled\
  f x1 ... xn Spilled,
  f y1 ... Spilled ... yn z1 ... zm)

(idea stolen from Cyril). Basically, eta-expanding and then "limiting the scope" of the spill unification variable.

This way we would keep spills inside partial applications possible (which is a nice feature in my opinion) and doing things like this would work, as one might intuitively expect:

pred f i:int, o:int.
f X X.

main :-
  std.forall [1, 2] (x\
    x = {f x}
  ).

where prior to this PR crashed with the "Unification problem outside the pattern fragment." error and with this PR unification fails.