Proper flow between result and answer type

[phischu]

Fixes #604

[phischu]

Consider our classical rule for handlers:

G |- s : T1    x: Char, k: Bool -> T2 |- t : T3
--------------------------------------------------
G |- try { s } with E { (x, k) => t } : T0

This should evoke the following flows:

T1 ~> T0
T3 ~> T0
T1 ~> T2

and nothing more. For now, and this is what this PR attempts to do, we can just unify T1 and T2.

[b-studios]

Conceptually, I don't think this is ok.

Shouldn't T3 also flow into T2?

For example, if we would allow subtyping in the source (since you argue with flows), T1 could be Int and T3 could be Bool. Now T2 cannot assume anymore that it is an Int, since also Bool flows into it. T3 would need to assume Int | Bool.

Don't get me wrong, I don't like this potentially "cyclic" flow.

[phischu]

Thank you for the concrete example. Consider the following program:

try { s; 123 } with { (x, k) => val y = k('a'); even(y) }

Under my proposal this should type check with T0 = Any, T1 = Int, T2 = Int, T3 = Bool.

Not let us consider what happens at runtime.

0: the effect operation is not used: this is fine.
1: the effect operation is used once: this is fine.
2: the effect operation is used twice: this is bad, because indeed the answer of the handler implementation also flows into the call-site of the resumption.

You are right and the flows should be:

T1 ~> T0
T3 ~> T0
T1 ~> T2
T3 ~> T2

Now the following type checks:

try { s; 123 } with { (x, k) => val _ = k('a'); false }

With T0 = Any, T1 = Int, T2 = Any, T3 = Bool.

Luckily this is not cyclic.

[b-studios]

Luckily this is not cyclic.

Not immediately. The moment the continuation is called (for instance in tail position), it will be cyclic. But maybe that's not a problem per se.