{-# LANGUAGE AllowAmbiguousTypes, FunctionalDependencies #-}
module Control.Effect.Internal.Reflection
  ( Reifies (..)
  , Tagged(..)
  , unproxy
  , reify
  , reifyTagged
  ) where

import Unsafe.Coerce
import Data.Proxy

newtype Tagged s a = Tagged { Tagged s a -> a
getTagged :: a }

unproxy :: (Proxy s -> a) -> Tagged s a
unproxy :: (Proxy s -> a) -> Tagged s a
unproxy Proxy s -> a
f = a -> Tagged s a
forall k (s :: k) a. a -> Tagged s a
Tagged (Proxy s -> a
f Proxy s
forall k (t :: k). Proxy t
Proxy)
{-# INLINE unproxy #-}

class Reifies s a | s -> a where
  reflect :: a

data Skolem

newtype Magic a r = Magic (Reifies Skolem a => Tagged Skolem r)


reifyTagged :: forall a r. a -> (forall (s :: *). Reifies s a => Tagged s r) -> r
reifyTagged :: a -> (forall s. Reifies s a => Tagged s r) -> r
reifyTagged a
a forall s. Reifies s a => Tagged s r
k = Magic a r -> a -> r
forall a b. a -> b
unsafeCoerce ((Reifies Skolem a => Tagged Skolem r) -> Magic a r
forall a r. (Reifies Skolem a => Tagged Skolem r) -> Magic a r
Magic Reifies Skolem a => Tagged Skolem r
forall s. Reifies s a => Tagged s r
k :: Magic a r) a
a
{-# INLINE reifyTagged #-}

reify :: forall a r. a -> (forall (s :: *) pr. (pr ~ Proxy, Reifies s a) => pr s -> r) -> r
reify :: a
-> (forall s (pr :: * -> *).
    (pr ~ Proxy, Reifies s a) =>
    pr s -> r)
-> r
reify a
a forall s (pr :: * -> *). (pr ~ Proxy, Reifies s a) => pr s -> r
k = a -> (forall s. Reifies s a => Tagged s r) -> r
forall a r. a -> (forall s. Reifies s a => Tagged s r) -> r
reifyTagged a
a ((Proxy s -> r) -> Tagged s r
forall k (s :: k) a. (Proxy s -> a) -> Tagged s a
unproxy Proxy s -> r
forall s (pr :: * -> *). (pr ~ Proxy, Reifies s a) => pr s -> r
k)
{-# INLINE reify #-}