Odd GND failure/success
There's currently a discussion about whether to change the definition of MonadTrans
to use QuantifiedConstraints
:
class (forall m. Monad m => Monad (t m)) => MonadTrans t where
lift :: m a -> t m a
I wondered if this works with GND. As it turns out, the answer is yes:
newtype B t (m :: Type -> Type) a => B (t m a)
deriving (Functor, Applicative, Monad)
-- StandaloneDeriving just to be sure the constraints is
-- what I expect.
deriving instance MonadTrans t => MonadTrans (B t)
compiles just fine. But a conceptually very similar idea does not:
class MonadTrans t where
lift :: m a -> t m a
liftMonad :: Monad m => Proxy (t m) -> (Monad (t m) => r) -> r
This one produces an error,
Lift.hs:9:42: error:
• Occurs check: cannot construct the infinite type: t ~ B t
arising from the coercion of the method ‘liftMonad’
from type ‘forall (m :: * -> *) r.
Monad m =>
Proxy (t m) -> (Monad (t m) => r) -> r’
to type ‘forall (m :: * -> *) r.
Monad m =>
Proxy (B t m) -> (Monad (B t m) => r) -> r’
• When deriving the instance for (MonadTrans (B t))
Why does one work and not the other? Is there a good reason for that, or should they both succeed or both fail?