Small and reasonably grounded example of -XQuantifiedConstraints

QuantifiedConstraintsExample.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE QuantifiedConstraints #-}
module QuantifiedConstraintsExample
  ( Stuff(..)
  , Things
  , getThingsIO
  , getThings
  ) where

import Control.Monad.IO.Class (MonadIO(..))
import Data.Monoid (Sum(..))
import Prelude

newtype Stuff = Stuff
  { unStuff :: Int
  }

-- | Dummy type that has a 'Monoid' instance.
newtype Things = Things
  { unThings :: Sum Int
  } deriving (Semigroup, Monoid) via (Sum Int)

-- | Given a bunch of 'Stuff', get a bunch of (combined) 'Things' in 'IO'. This
-- leverages the facts that the type 'Things' has a 'Monoid' instance and that
-- there is also a @Monoid a => Monoid (IO a)@ instance.
getThingsIO :: [Stuff] -> IO Things
getThingsIO stuffs = do
  fmap Things $ flip foldMap stuffs \stuff ->
    pure $ Sum $ unStuff stuff

-- | But when we try to generalize this function, we get a compiler error:
--
-- > getThings :: (MonadIO m) => [Stuff] -> m Things
-- > getThings stuffs = do
-- >   fmap Things $ flip foldMap stuffs \stuff ->
-- >     pure $ Sum $ unStuff stuff
--
-- > • Could not deduce (Monoid (m (Sum Int)))
-- >     arising from a use of ‘foldMap’
-- >   from the context: MonadIO m
-- >     bound by the type signature for:
-- >                getThings :: forall (m :: * -> *). MonadIO m => [Stuff] -> m Things
--
-- We don't want to directly put this missing constraint as GHC reports it into
-- our type signature, as that would leak the underlying type 'Things' wraps to
-- the user.
--
-- Instead, we can use the 'QuantifiedConstraints' extension to express the
-- requirement that @m a@ has a 'Monoid' instance.
getThings
  :: (MonadIO m, forall x. Monoid x => Monoid (m x))
  => [Stuff]
  -> m Things
getThings stuffs = do
  fmap Things $ flip foldMap stuffs \stuff ->
    pure $ Sum $ unStuff stuff