Is mask behind necessary?

[TimWhiting]

This is more of a question: not a bug!!

Consider the following code:

effect final ctl throw_(e: string): a

fun main()
  with handler
    fun throw_(e: string)
      println("Error in outer")
  with handler
    fun throw_(e2: string)
      println("Error in inner")
      throw_("from inner to outer") 
  with mask behind<exn_>
  ...
  throw_("throw to inner")
  mask<exn_>
    // Error
     throw_("throw to outer")

What if instead of mask behind we desugared overrides like this:

fun main()
  with handler
    fun throw_(e: string)
      println("Error in outer")
  fun throw-fn(e2: string, evv: evv)
     println("Error in inner")
     throw_("from inner to outer") 
  val evv = current-evidence-vector
  with mask<exn_>
  with handler
    fun throw_(s) throw-fn(s, evv)
  ...
  throw_("throw to inner") 
  mask<exn_>
    // Error
     throw_("throw to outer")

I guess the motivation for keeping mask behind is that it allows for the user to do overriding themselves, or to use it in other contexts. It adds expressive power. So maybe I've answered my own question - it isn't necessary for overrides, but adds expressive power that could allow the developer to make this and other safe evidence adjustments. The desugaring I show here is correct with respect to overriding, but exposes low level adjustments that are not type-safe - so it isn't a true user-accessible desugaring that they could write out themselves in a type-safe manner, just a compiler transform.