Mask is ignored when adding exn effect

[anfelor]

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).

[TimWhiting]

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.