Consider the following program using effect polymorphism (due to @thwfhk):
effect reader<s>
fun ask() : s
fun test( p : () -> <reader<int>, reader<int>|e> a ) : e a
with handler
fun ask() 100
with handler
fun ask() 42
p()
pub fun main(): console ()
with test
println(mask<reader<int>>(ask) : int)
As expected, it completes with output 100 and hovering over the call to ask we get the correct instantiation fun ask : () -> <reader<int>,console/console> int.
However, Koka surprisingly also accepts:
pub fun main(): console ()
with test
println(mask<reader<int>>(ask()) : int) // notice the call to ask
Hovering over ask again, we get the wrong instantiation fun ask : () -> <reader<() -> <console/console,reader<int>> int>|_e> (() -> <console/console,reader<int>> int). This program is accepted by the type checker but segfaults at runtime.
Consider the following program using effect polymorphism (due to @thwfhk):
As expected, it completes with output
100and hovering over the call toaskwe get the correct instantiationfun ask : () -> <reader<int>,console/console> int.However, Koka surprisingly also accepts:
Hovering over
askagain, we get the wrong instantiationfun ask : () -> <reader<() -> <console/console,reader<int>> int>|_e> (() -> <console/console,reader<int>> int). This program is accepted by the type checker but segfaults at runtime.