Constrained polymorphic effects

[TimWhiting]

This has come up a few times. In particular with implicits. For example: #335, though I'm not sold on this particular proposal entirely.

Sometimes we'd like to state conditionally that if a higher order function parameter has the divergence effect than the function does as well. (This is partially due to limitations of the divergence analysis).

Essentially we want something like this:

fun show(l: list<a>, ?show: (a) -> <?div> string): <?div> string ...

I don't think this poses issues to inference for the following reasons, and with the following restrictions.

1. Restrict so that just like for polymorphic effects <div|e>, if it occurs in the result type, it must also occur in the argument types (modulo masking).
2. When unifying at an application we need to resolve show to a specific overloaded function, so we can instantiate the application and unify it so it becomes concrete right away. In particular we don't allow conditional effects due to if statements or anything like that. If there is a conditional effect in the result type it must be tied to one or more parameter types.
3. Only allow unhandleable effects to be conditional. (This means there needs to be no change to compilation)
4. We could relax rule 3 a bit:

• It would require specializing the function to every combination of effects present, which would probably be too much unless we only generate the specialized functions as needed.
• Or we would need to require that no other effects are used except via calling the function parameters?
• Or we just cannot use the static offset optimization for looking up a handler in an evidence vector

I haven't thought through all of the rules that this could affect, but it seems like a tractable problem.