Hi, cafe. Imagine that we are writing an operating system FooOS which uses spinlocks (mutexes, critical sections) to guard shared resources and we want the typesystem to prevent application from re-locking the spinlock which have already been locked by the current thread. Below is the code which does it by explicitly defining MonadSpinlockLess class. Unfortunately, it requires tons of boilerplate instances because we need _any_ monad except SpinlockT to be an instance of MonadSpinlockLess. Is there a better way of doing it? Maybe GADTs? Basically, it would be sufficient to rewrite lock function as lock :: (! MonadSpinlock m) => Spinlock -> SpinlockT m a -> m a but afaik we can't use negations on a typelevel, can we? Thanks, Sergey --- {-# LANGUAGE GeneralizedNewtypeDeriving #-} import Data.IORef newtype Spinlock = SL (IORef Int) newtype SpinlockT m a = SpinlockT { unSpinlock :: m a } deriving(Monad) class (Monad m) => MonadSpinlockLess m instance MonadSpinlockLess IO instance MonadSpinlockLess m => MonadSpinlockLess (ReaderT r m) instance MonadSpinlockLess m => MonadSpinlockLess (WriterT r m) instance MonadSpinlockLess m => MonadSpinlockLess (StateT s m) -- .... lots of instances class (Monad m) => MonadSpinlock m instance Monad m => MonadSpinlock (SpinlockT m) lock :: (MonadSpinlockLess m) => Spinlock -> SpinlockT m a -> m a lock (SL r) h = {- atomicModifyIORef (+1) r (doesn't matter) >> -} unSpinlock h process :: Spinlock -> IO () process sl = handler_a where handler_a = do lock sl handler_b handler_b = do lock sl handler_c {- ^^^^ Second lock, should fail to typecheck -} handler_c = do {- do something -} return ()