polymorhic ability handlers can intercept requests of wrong type, violating static type safety

I was playing around with abilities in Unison and in particular trying to see if I could create an interface with an abstract ability. For example:

structural type Variable a e = { read' : '{e} a , write : a ->{e} () }
Variable.read var = !(Variable.read' var)

withLocalVarInefficient : a -> (forall abstractVariableEffect. Variable a abstractVariableEffect -> {abstractVariableEffect, e} b) -> {e} b
withLocalVarInefficient initVal f =
  Scope.run do
    innerRef = Scope.ref initVal
    f (Variable '(Ref.read innerRef) (Ref.write innerRef))

> withLocalVarInefficient 0 (x ->
    withLocalVarInefficient "Hello" (y ->
      withLocalVarInefficient 2 (z ->
        (Variable.read x, Variable.read y, Variable.read z)
      )
    )
)

This returns (0, "Hello", 2)

This has three Scope ability which can't be unified, but it works because the type system tracks each ability separately as it has no idea what the abilities are. What I was unsure of was whether Unison was actually sending every request to the correct handler or whether it happens to work with this builtin handler as any Scope.run can handle requests for any Ref. I tried a different implementation:

withLocalVarBad : a -> (forall abstractVariableEffect. Variable a abstractVariableEffect -> {abstractVariableEffect, e} b) -> {e} b
withLocalVarBad initVal f =
  Store.withInitialValue initVal do
    f (Variable '(Store.get) Store.put)

> withLocalVarBad 0 (x ->
    withLocalVarBad "Hello" (y ->
      withLocalVarBad 2 (z ->
        (0 + Variable.read x, Variable.read y, 0 + Variable.read z)
      )
    )
)

Expected: either same as above, or (2, "Hello", 2) Got: (2, 2, 2)

This is in conflict with the static type! A further variant:

> withLocalVarBad 0 (x ->
    withLocalVarBad "Hello" (y ->
      withLocalVarBad 2 (z ->
        (0 + Variable.read x, "" ++ Variable.read y, 0 + Variable.read z)
      )
    )
)

Got: Encountered exception: marshalToForeign: unhandled closure: DataU1 ( ReferenceBuiltin "Nat" ) 1310720 2 CallStack ( from HasCallStack ): error

I think it is more reasonable to change the runtime behavior than the type checker here, but it's not immediately obvious how the runtime behavior should be specified. I see two general options: 1) Requests go to topmost ability handler with fully matching type, in this case yielding (2, "Hello", 2). 2) Requests go to the ability handler the type system thinks they go to, in this case yielding (0, "Hello", 2). Effekt has something similar, but I don't know that it would be straightforward to apply their effect system to Unison. Also this is the bigger breaking change; it is plausible someone has working code in their codebase that the second approach would change. So focusing on option 1, one potential upside of this is the ability system would provide a way to do type specific overloading of a polymorphic function (e.g. by emitting a value of unknown type and handling it with both a Stream Nat and a Stream a handler). However it is less clear what should happen if you emit None when you have a Stream (Optional Nat) handler and a Stream (Optional a) handler. Likewise, if you go with approach 1 but I happen to want behavior 2, can I add an extra type variable like in the Scope s ability and ensure that only the intended handler is known to have a matching type? This would be a cool feature, akin to Koka's named scoped handlers.

unisonweb / unison

polymorhic ability handlers can intercept requests of wrong type, violating static type safety #4522