If you don't mind deferring the definition of "correct" to the interpreter writer then that intentional choice is captured by
(MonadWriter Log m, MonadExcept m) => m a
throwError e >> m == throwError e
So how do we specify what additional laws are needed to cut down the free product of the effectful languages? Dunno, that's a hard one. You could clearly do it using dependent types, but that's still today very expensive.
But given that we literally lack proper information to make a choice it's very important that all of those choices are allowable. It's my position that there is no meaningful default. It's also my position that the `mtl` style free products are perfectly acceptable.