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

-- This module was copied from polysemy-zoo:
-- https://hackage.haskell.org/package/polysemy-zoo-0.8.2.0/docs/src/Polysemy.ConstraintAbsorber.html

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 (Constraint, Type)
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.
absorbWithSem ::
  forall
    -- Constraint to be absorbed
    (p :: (Type -> Type) -> Constraint)
    -- Wrapper to avoid orphan instances
    (x :: (Type -> Type) -> Type -> Type -> Type)
    d
    r
    a.
  -- | Reified dictionary
  d ->
  -- | This parameter should always be @'Sub' 'Dict'@
  (forall s. R.Reifies s d :- p (x (Sem r) s)) ->
  (p (Sem r) => Sem r a) ->
  Sem r a
absorbWithSem :: forall (p :: (* -> *) -> Constraint) (x :: (* -> *) -> * -> * -> *)
       d (r :: EffectRow) a.
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)) ->
  Sem r a
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
      (p (x m s) :- p m
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 #-}