Type inference incorrectly unifies flexible effect variables in recursive functions

[samo-novak]

For certain recursive functions that have both a flexible effect variable, and an operation label occuring in a different effect row, the two effect variables get unified, even though the flexible one should be instantiated as a fresh rigid var.

Two minimal examples:

sig g : (a) -%f-> Comp((), {Op:(a) {}-> ()|e})
#           ^^^^^
fun g(x)() {
  g(x)()
}

g = fun : (a) {Op:(a) {}-> ()|b}~> Comp ((),{Op:(a) {}-> ()|b})
#             ^^^^^^^^^^^^^^^^^^            ^^^^^^^^^^^^^^^^^^


sig g' : (a) -%f-> () {Op:(a) {}-> ()|e}~> ()
#            ^^^^^
fun g'(x)() {
  g'(x)()
}

g' = fun : (a) {Op:(a) {}-> ()|b}~> () {Op:(a) {}-> ()|b}~> ()
#              ^^^^^^^^^^^^^^^^^^      ^^^^^^^^^^^^^^^^^^

As you can see above, %f incorrectly unified with e. However, we would expect %f to be instantiated to some fresh variable, so that is it different from e - this is also the type that gets inferred if the signature is omitted.

fun g'(x)() {
  do Op(x);
  g'(x)()
}

g' = fun : (a) -> () {Op:(a) {}-> ()|_}~> _::Any
#              ^^                   ^^^ these are different!

(Note that in the above example, I changed this definition of g' so that the operation Op would be inferred).

More details:

• This happens in cases with and without type aliases containing effects (such as Comp).
• The declared operations do not need to be invoked from within the function.
• It seems this only happens with recursive functions (at least I have not yet managed to replicate it with a non-recursive function).
• This occurs on master, independent of effect sugar.

---

For a more elaborate example, I first noticed this in examples/handlers/fringe.links, when I placed a flexible variable on the arrow in walkTree, as follows:

sig walkTree : (Tree(a)) -%f-> Comp((), {Yield:(a) {}-> ()|_})
fun walkTree(tree)() {
  switch (tree) {
    case Leaf(v)   -> yield(v)
    case Node(l,r) -> walkTree(l)(); walkTree(r)()
  }
}

(placing flexible variables here is motivated by #1032)