{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_HADDOCK not-home #-}
-- | Type-safe indexing for 'Effectful.Internal.Monad.Env'.
--
-- This module is intended for internal use only, and may change without warning
-- in subsequent releases.
module Effectful.Internal.Effect
  ( Effect
  , (:>)(..)
  , (:>>)
  , Subset(..)

  -- * Re-exports
  , Type
  ) where

import Data.Kind
import GHC.TypeLits

-- | The kind of effects.
type Effect = (Type -> Type) -> Type -> Type

-- | A constraint that requires that a particular effect @e@ is a member of the
-- type-level list @es@. This is used to parameterize an 'Effectful.Eff'
-- computation over an arbitrary list of effects, so long as @e@ is /somewhere/
-- in the list.
--
-- For example, a computation that only needs access to a mutable value of type
-- 'Integer' would have the following type:
--
-- @
-- 'Effectful.State.Static.Local.State' 'Integer' ':>' es => 'Effectful.Eff' es ()
-- @
class (e :: Effect) :> (es :: [Effect]) where
  -- | Get the position of @e@ in @es@.
  --
  -- /Note:/ GHC is kind enough to cache these values as they're top level CAFs,
  -- so the lookup is amortized @O(1)@ without any language level tricks.
  reifyIndex :: Int
  reifyIndex = -- Don't show "minimal complete definition" in haddock.
               [Char] -> Int
forall a. HasCallStack => [Char] -> a
error [Char]
"unimplemented"

instance TypeError
  ( Text "There is no handler for '" :<>: ShowType e :<>: Text "' in the context"
  ) => e :> '[] where
  reifyIndex :: Int
reifyIndex = [Char] -> Int
forall a. HasCallStack => [Char] -> a
error [Char]
"unreachable"

instance {-# OVERLAPPING #-} e :> (e : es) where
  reifyIndex :: Int
reifyIndex = Int
0

instance e :> es => e :> (x : es) where
  reifyIndex :: Int
reifyIndex = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ forall (e :: Effect) (es :: [Effect]). (e :> es) => Int
reifyIndex @e @es

----------------------------------------

-- | Convenience operator for expressing that a function uses multiple effects
-- in a more concise way than enumerating them all with '(:>)'.
--
-- @[E1, E2, ..., En] ':>>' es ≡ (E1 ':>' es, E2 ':>' es, ..., En :> es)@
type family xs :>> es :: Constraint where
  '[]      :>> es = ()
  (x : xs) :>> es = (x :> es, xs :>> es)

----------------------------------------

-- | Provide evidence that @xs@ is a subset of @es@.
class Subset (xs :: [Effect]) (es :: [Effect]) where
  reifyIndices :: [Int]
  reifyIndices = -- Don't show "minimal complete definition" in haddock.
                 [Char] -> [Int]
forall a. HasCallStack => [Char] -> a
error [Char]
"unimplemented"

instance Subset '[] es where
  reifyIndices :: [Int]
reifyIndices = []

instance (e :> es, Subset xs es) => Subset (e : xs) es where
  reifyIndices :: [Int]
reifyIndices = forall (e :: Effect) (es :: [Effect]). (e :> es) => Int
reifyIndex @e @es Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: forall (xs :: [Effect]) (es :: [Effect]). Subset xs es => [Int]
reifyIndices @xs @es