RFC: type class synthesis order when `outParam` has multiple possible values

Proposal

Classes such as MonadState, MonadExcept, MonadReader have an outParam, and they also come with a version with a semiOutParam, namely MonadStateOf, MonadExceptOf and MonadReaderOf. The value that gets picked for the outParam depends on the order in which instances are applied during type class resolution. This can be influenced by setting priorities on the instances, but this is not currently done. The convention for monad transformers tends to be that the outermost transformer is the one that gives the outParam instance and programmers rely on this a lot.

Bad instance example

example (e : ε) : ExceptT ε MetaM Unit := throw e -- error

gives an error, because the instance generated for MonadExcept is the one that comes from the CoreM instance. So, we could increase the priority of the instance MonadExcept ε (ExceptT ε). This would make it much more convenient to use ExceptT in this scenario.

Similarly, I propose to give a high instance priority to MonadState σ (StateT σ), MonadReader ρ (ReaderT ρ) etc.. These won't have any direct effect as far as I know of, but will make sure that no future instances will accidentally mess with the expected behaviour of these classes.

Original discussion

Original discussion on Zulip. This topic came up when I found a use of the MonadStore1 type class where it should be used with a semiOutParam, but it has an outParam. This class should be refactored to have a version MonadStore1Of with the semiOutParam, following the design of the aforementioned type classes. And for this we also want the instance priorities to be set properly.

leanprover / lean4