Open anfelor opened 2 months ago
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).