You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Consider the following example, where we use two different handlers to catch two abort effects.
effect abort
ctl abort() : a
fun catch'(f : () -> <abort|e> a, h : () -> e a) : e a
with ctl abort() { h() }
f()
fun maybe(f : () -> <abort|e> a) : e maybe<a>
with ctl abort() { Nothing }
Just(f())
type abc { A; B; C }
fun show(abc : abc)
match abc
A -> "A"
B -> "B"
C -> "C"
fun abortA(abc : abc)
match abc
A -> abort()
_ -> abc
fun abortB(abc : abc)
match abc
B -> abort()
_ -> abc
fun distinct(abc : abc) : <abort,abort> abc
val n = mask<abort>
abortA(abc)
abortB(n)
fun main() : <console> ()
println(maybe(fn() catch'(fn() distinct(A), fn() C)))
println(maybe(fn() catch'(fn() distinct(B), fn() C)))
println(maybe(fn() catch'(fn() distinct(C), fn() C)))
This program runs as expected, where abortA() is caught by the maybe handler and abortB() is caught by the catch' handler. The output thus is:
Nothing
Just(C)
Just(C)
However, if we merely change the type signature to fun main() : <console, exn> (), we obtain:
Just(C)
Just(C)
Just(C)
where now abortA() is also caught by the catch' handler (and the mask is seemingly ignored).
The text was updated successfully, but these errors were encountered:
So it looks like there is a bug in Simplify.hs when there are duplicate labels:
I'm seeing the following:
(fn<<abort,abort,console/console,exn>>(){
(std/core/hnd/@open1(
(std/core/vector/unvlist(
// Here is the problem
(std/core/types/Cons((std/core/types/@make-ssize_t(0)),
(std/core/types/Cons((std/core/types/@make-ssize_t(0)),
std/core/types/Nil)))))), (fn<<abort,abort>>(abc: abc){
val x@1@10064 : hnd/ev-index
= (std/core/hnd/@evv-index(scratch/test/@tag-abort));
(match ((std/core/hnd/yielding())) {
((std/core/types/True() : bool ) as @pat@2: bool)
-> std/core/hnd/yield-extend((fn<<abort,abort>>(@y-x10014: hnd/ev-index){
(scratch/test/@mlift-main@10034(abc, @y-x10014));
}));
((@skip std/core/types/False() : bool ) as @pat@0@1: bool)
-> scratch/test/@mlift-main@10034(abc, x@1@10064);
});
}), scratch/test/A));
In particular in the open1() call it creates a vector with two indices being identical. There is a correct abort type at that offset, but it corresponds to the wrong evidence.
Even without the issue in Simplify.hs, I believe the code in OpenResolve.hs and hnd.kk does not handle this correctly, because it just searches by handler tag, without keeping track of duplicate labels.
Consider the following example, where we use two different handlers to catch two
abort
effects.This program runs as expected, where
abortA()
is caught by themaybe
handler andabortB()
is caught by thecatch'
handler. The output thus is:However, if we merely change the type signature to
fun main() : <console, exn> ()
, we obtain:where now
abortA()
is also caught by thecatch'
handler (and the mask is seemingly ignored).The text was updated successfully, but these errors were encountered: