Type alias quantification trick for semi-polymorphic effect stacks

Example.hs

{-# LANGUAGE AllowAmbiguousTypes, ConstraintKinds, DataKinds, FlexibleContexts,
  FlexibleInstances, FunctionalDependencies, InstanceSigs,
  MultiParamTypeClasses, RankNTypes, RecordWildCards, ScopedTypeVariables,
  StandaloneKindSignatures, TypeApplications, TypeFamilies,
  TypeFamilyDependencies #-}

import Control.Monad.Reader (MonadReader)
import Control.Monad.Trans (MonadTrans)
import Control.Monad.Trans.Except (ExceptT, runExceptT)
import Data.Kind (Constraint, Type)

-- | An abstract effect "stack" built around a concrete 'ExceptT' transformer.
--
-- The general pattern is to use type aliases which let us specify the concrete
-- effects that we might want to interpret out of an otherwise polymorphic
-- "effect stack".
type AbstractStack :: Constraint -> Type -> (Type -> Type) -> Type -> Type
type AbstractStack capabilities error m result =
  capabilities =>
  ExceptT error m result

-- | Constraint synonym for the set of capabilities that all 'StackM' operations
-- must provide.
--
-- In other words: when a 'StackM' is evaluated, its resulting environment
-- should /at a minimum/ provide the capabilities listed here.
type Capabilities :: (Type -> Type) -> Constraint
type Capabilities m = ()

-- | An "effect stack" whose environment is constrained by /at least/ the set of
-- capabilities defined in 'Capabilities'.
--
-- NOTE: It's possible to define additional capabilities here so long as the
-- callsite where 'StackM' is discharged can fulfill them.
type StackM :: Type -> (Type -> Type) -> Type -> Type
type StackM error m result =
  AbstractStack
    (Capabilities m, MonadReader () m)
    error
    m
    result

-- | Execute some 'StackM' action, "discharging" the concrete effects defined
-- by the underlying 'AbstractStack' environment in terms of an operational
-- environment which is shared with 'StackM' (i.e. @m@).
--
-- This is useful for situations where some 'StackM' environment might need to
-- work over a concrete 'Monad' @m@, rather than being fixed to /all/ 'Monad's.
--
-- For example, one could write @StackM SomeException IO ()@ which would provide
-- 'StackM' with the ability to execute 'IO' operations.
runStackM ::
  forall error result m.
  MonadReader () m =>
  StackM error m result ->
  m (Either error result)
runStackM action = runExceptT action

-- | A "concrete" effect stack, whose operational environment is fixed to the
-- set of capabilities outlined in 'StackM'.
type Stack error result = forall m. StackM error m result

-- | Execute some 'Stack' action, "discharging" the concrete effects defined
-- by the underlying 'AbstractStack' environment in terms of our own operational
-- environment (i.e. @m@).
--
-- This is distinct from 'StackM' in that the environment that 'Stack' executes
-- in is "sealed" off in a way that prevents us from "enriching" it with the
-- capabilities provided by another 'Monad'.
runStack ::
  forall error result m.
  MonadReader () m =>
  Stack error result ->
  m (Either error result)
runStack action = runExceptT action