# 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?