Correctness of implicit lifting
haskell, types
Solution
If `m :: Monad m => m A`, then `m` must be equivalent to `return x` for some `x :: A`, because the only ways you have to get anything `:: m x` are `return` and `(>>=)`. But in order to use `(>>=)` you must be able to produce some `m y`, which you can either do with `return` or with another application of `(>>=)`. Either way you have to use `return` eventually, and the monad laws guarantee that the whole expression will be equivalent to `return x`.
(If `m` is completely polymorphic over the monad, then you must able to use it at `m ~ Identity`, so it can't use any fancy monad tricks, unless you pass it an argument. This sort of trick is used e.g. here and here.)
Given that `m = return x`, we know by the monad transformer laws (`lift . return = return`) that `lift m = m`.
Of course, this is only true for this particular type. If you have, say, `m :: MonadState S m => m A`, then `m` could easily be different from `lift m` -- for example, with a type like `StateT A (State A) A`, `get` and `lift get` will be different.
(And of course all of this is ignoring ⊥. Then again, if you don't, most monads don't obey the laws anyway.)
Problem
Imagine that I have a value that is generic over the monad: ``` m :: (Monad m) => m A -- 'A' is some concrete type ``` Now let's say that I specialize this value to a concrete monad transformer stack in two separate ways: ``` m1 :: T M A m1 = m m2 :: T M A m2 = lift m ``` ... where `M` and `T M` are monads, and `T` is a monad transformer: ``` instance Monad M where ... instance (Monad m) => Monad (T m) where ... instance MonadTrans T where ... ``` ... and those instances obey the monad laws and monad transformer laws. Can we deduce that: ``` m1 = m2 ``` ... knowing nothing about `m` other than its type? This is just a long-winded way of asking if `lift m` is a valid substitution for `m`, assuming that both type-check. It is a little bit difficult to phrase the question because it requires `m` type-checking as two separate monads before and after the substitution. As far as I can tell, the only way such a substitution would type-check is if `m` is generic over the monad. My vague intuition is that the substitution should always be correct, but I'm not sure that my intuition is correct, or how to prove it if it is correct.