Question on subtyping of handlers in "An Effect System for Algebraic Effects and Handlers"
I'm surprised we don't get this question more often, for Andrej and I have considered adding this rule for quite some time and believed to have proven its correctness. But in the end, it turned out to be false, at least in a call-by-value setting (I have heard it plays out nicer in call-by-push-value).

Consider the state handler, described on top of page 24 of the same paper, which takes a stateful computation of type $B$ on state $A$ and transforms it into a pure function from $A$ to $B$. Its type is $$B!\{\mathtt{lookup},\mathtt{update}\} \Rightarrow (A \to B ! \emptyset) ! \emptyset$$ Note the two empty sets on the right hand side. The first states that the resulting function is pure, the second one that there no effects occur when producing this function.

Now assume that we apply the handler to a computation that may call some other effects $\Delta$ besides $\mathtt{lookup}$ and $\mathtt{update}$. Applying the suggested rule, you would get the type $$B!(\{\mathtt{lookup},\mathtt{update}\} \cup \Delta) \Rightarrow (A \to B ! \emptyset) ! \Delta$$
but in fact, the correct type is 
$$B!(\{\mathtt{lookup},\mathtt{update}\} \cup \Delta) \Rightarrow (A \to B ! \Delta) ! \Delta$$
as the unhandled effects $\Delta$ may occur before producing the function or after calling it.