{-# LANGUAGE AllowAmbiguousTypes         #-}
{-# LANGUAGE ConstraintKinds             #-}

module Polysemy.ConstraintAbsorber
  ( -- * Absorb builder
    absorbWithSem

    -- * Re-exports
  , Reifies
  , (:-) (Sub)
  , Dict (Dict)
  , reflect
  , Proxy (Proxy)
  ) where

import           Data.Constraint (Dict(Dict), (:-)(Sub), (\\))
import qualified Data.Constraint as C
import qualified Data.Constraint.Unsafe as C
import           Data.Kind (Type, Constraint)
import           Data.Proxy (Proxy (..))
import           Data.Reflection (Reifies, reflect)
import qualified Data.Reflection as R
import           Polysemy

------------------------------------------------------------------------------
-- | This function can be used to locally introduce typeclass instances for
-- 'Sem'. See 'Polysemy.ConstraintAbsorber.MonadState' for an example of how to
-- use it.
--
-- @since 0.3.0.0
absorbWithSem
    :: forall -- Constraint to be absorbed
              (p :: (Type -> Type) -> Constraint)
              -- Wrapper to avoid orphan instances
              (x :: (Type -> Type) -> Type -> Type -> Type)
              d r a
     . d  -- ^ Reified dictionary
    -> (forall s. R.Reifies s d :- p (x (Sem r) s))  -- ^ This parameter should always be @'Sub' 'Dict'@
    -> (p (Sem r) => Sem r a)
    -> Sem r a
absorbWithSem :: d
-> (forall s. Reifies s d :- p (x (Sem r) s))
-> (p (Sem r) => Sem r a)
-> Sem r a
absorbWithSem d
d forall s. Reifies s d :- p (x (Sem r) s)
i p (Sem r) => Sem r a
m =  d -> (forall s. Reifies s d => Proxy s -> Sem r a) -> Sem r a
forall a r. a -> (forall s. Reifies s a => Proxy s -> r) -> r
R.reify d
d ((forall s. Reifies s d => Proxy s -> Sem r a) -> Sem r a)
-> (forall s. Reifies s d => Proxy s -> Sem r a) -> Sem r a
forall a b. (a -> b) -> a -> b
$ \(Proxy s
_ :: Proxy (s :: Type)) -> p (Sem r) => Sem r a
m (p (Sem r) => Sem r a) -> (Reifies s d :- p (Sem r)) -> Sem r a
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (p (x (Sem r) s) :- p (Sem r))
-> (Reifies s d :- p (x (Sem r) s)) -> Reifies s d :- p (Sem r)
forall (b :: Constraint) (c :: Constraint) (a :: Constraint).
(b :- c) -> (a :- b) -> a :- c
C.trans
  (forall (a :: Constraint) (b :: Constraint). a :- b
forall (m :: * -> *). p (x m s) :- p m
C.unsafeCoerceConstraint :: ((p (x m s) :- p m))) Reifies s d :- p (x (Sem r) s)
forall s. Reifies s d :- p (x (Sem r) s)
i
{-# INLINEABLE absorbWithSem #-}