{-# OPTIONS_GHC -Wno-redundant-constraints #-} -- Due to use of TypeError.
{-# OPTIONS_HADDOCK not-home #-}

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module:       Data.OpenUnion.Internal
-- Description:  Open unions (type-indexed co-products) for extensible effects.
--
-- Copyright:    (c) 2016 Allele Dev; 2017 Ixperta Solutions s.r.o.; 2017 Alexis King
-- License:      BSD3
-- Maintainer:   Alexis King <lexi.lambda@gmail.com>
-- Stability:    experimental
-- Portability:  GHC specific language extensions.
--
-- These are internal definitions and should be used with caution. There are no
-- guarantees that the API of this module will be preserved between minor
-- versions of this package.
--
-- Open unions (type-indexed co-products, i.e. type-indexed sums) for
-- extensible effects All operations are constant-time.
--
-- Based on
-- <http://okmij.org/ftp/Haskell/extensible/OpenUnion51.hs OpenUnion51.hs>.
--
-- Type-list @r :: [* -> *]@ of open union components is a small Universe.
-- Therefore, we can use a @Typeable@-like evidence in that universe. In our
-- case a simple index of an element in the type-list is sufficient
-- substitution for @Typeable@.
module Data.OpenUnion.Internal where

import Data.Kind (Type)
import GHC.TypeLits (TypeError, ErrorMessage(..))
import Unsafe.Coerce (unsafeCoerce)

-- | Open union is a strong sum (existential with an evidence).
data Union (r :: [Type -> Type]) a where
  Union :: {-# UNPACK #-} !Word -> t a -> Union r a

-- | Takes a request of type @t :: * -> *@, and injects it into the 'Union'.
--
-- Summand is assigning a specified 'Word' value, which is a position in the
-- type-list @(t ': r) :: * -> *@.
--
-- __This function is unsafe.__
--
-- /O(1)/
unsafeInj :: Word -> t a -> Union r a
unsafeInj :: Word -> t a -> Union r a
unsafeInj = Word -> t a -> Union r a
forall k (t :: k -> *) (a :: k) (r :: [* -> *]).
Word -> t a -> Union r a
Union
{-# INLINE unsafeInj #-}

-- | Project a value of type @'Union' (t ': r) :: * -> *@ into a possible
-- summand of the type @t :: * -> *@. 'Nothing' means that @t :: * -> *@ is not
-- the value stored in the @'Union' (t ': r) :: * -> *@.
--
-- It is assumed that summand is stored in the 'Union' when the 'Word' value is
-- the same value as is stored in the 'Union'.
--
-- __This function is unsafe.__
--
-- /O(1)/
unsafePrj :: Word -> Union r a -> Maybe (t a)
unsafePrj :: Word -> Union r a -> Maybe (t a)
unsafePrj Word
n (Union Word
n' t a
x)
  | Word
n Word -> Word -> Bool
forall a. Eq a => a -> a -> Bool
== Word
n'   = t a -> Maybe (t a)
forall a. a -> Maybe a
Just (t a -> t a
forall a b. a -> b
unsafeCoerce t a
x)
  | Bool
otherwise = Maybe (t a)
forall a. Maybe a
Nothing
{-# INLINE unsafePrj #-}

-- | Represents position of element @t :: * -> *@ in a type list
-- @r :: [* -> *]@.
newtype P t r = P {P t r -> Word
unP :: Word}

-- | Find an index of an element @t :: * -> *@ in a type list @r :: [* -> *]@.
-- The element must exist. The @w :: [* -> *]@ type represents the entire list,
-- prior to recursion, and it is used to produce better type errors.
--
-- This is essentially a compile-time computation without run-time overhead.
class FindElem (t :: Type -> Type) (r :: [Type -> Type]) where
  -- | Position of the element @t :: * -> *@ in a type list @r :: [* -> *]@.
  --
  -- Position is computed during compilation, i.e. there is no run-time
  -- overhead.
  --
  -- /O(1)/
  elemNo :: P t r

-- | Base case; element is at the current position in the list.
instance FindElem t (t ': r) where
  elemNo :: P t (t : r)
elemNo = Word -> P t (t : r)
forall k k (t :: k) (r :: k). Word -> P t r
P Word
0

-- | Recursion; element is not at the current position, but is somewhere in the
-- list.
instance {-# OVERLAPPABLE #-} FindElem t r => FindElem t (t' ': r) where
  elemNo :: P t (t' : r)
elemNo = Word -> P t (t' : r)
forall k k (t :: k) (r :: k). Word -> P t r
P (Word -> P t (t' : r)) -> Word -> P t (t' : r)
forall a b. (a -> b) -> a -> b
$ Word
1 Word -> Word -> Word
forall a. Num a => a -> a -> a
+ P t r -> Word
forall k (t :: k) k (r :: k). P t r -> Word
unP (P t r
forall (t :: * -> *) (r :: [* -> *]). FindElem t r => P t r
elemNo :: P t r)

-- | Instance resolution for this class fails with a custom type error
-- if @t :: * -> *@ is not in the list @r :: [* -> *]@.
class IfNotFound (t :: Type -> Type) (r :: [Type -> Type]) (w :: [Type -> Type])

-- | If we reach an empty list, that’s a failure, since it means the type isn’t
-- in the list. For GHC >=8, we can render a custom type error that explicitly
-- states what went wrong.
instance TypeError ('Text "‘" ':<>: 'ShowType t
                    ':<>: 'Text "’ is not a member of the type-level list"
                    ':$$: 'Text "  ‘" ':<>: 'ShowType w ':<>: 'Text "’"
                    ':$$: 'Text "In the constraint ("
                    ':<>: 'ShowType (Member t w) ':<>: 'Text ")")
    => IfNotFound t '[] w

instance IfNotFound t (t ': r) w
instance {-# OVERLAPPABLE #-} IfNotFound t r w => IfNotFound t (t' ': r) w

-- | Pass if @r@ is uninstantiated. The incoherence here is safe, since picking
-- this instance doesn’t cause any variation in behavior, except possibly the
-- production of an inferior error message. For more information, see
-- lexi-lambda/freer-simple#3, which describes the motivation in more detail.
instance {-# INCOHERENT #-} IfNotFound t r w

-- | A constraint that requires that a particular effect, @eff@, is a member of
-- the type-level list @effs@. This is used to parameterize an
-- 'Control.Monad.Freer.Eff' computation over an arbitrary list of effects, so
-- long as @eff@ is /somewhere/ in the list.
--
-- For example, a computation that only needs access to a cell of mutable state
-- containing an 'Integer' would likely use the following type:
--
-- @
-- 'Member' ('Control.Monad.Freer.State.State' 'Integer') effs => 'Control.Monad.Freer.Eff' effs ()
-- @
class FindElem eff effs => Member (eff :: Type -> Type) effs where
  -- This type class is used for two following purposes:
  --
  -- * As a @Constraint@ it guarantees that @t :: * -> *@ is a member of a
  --   type-list @r :: [* -> *]@.
  --
  -- * Provides a way how to inject\/project @t :: * -> *@ into\/from a 'Union',
  --   respectively.
  --
  -- Following law has to hold:
  --
  -- @
  -- 'prj' . 'inj' === 'Just'
  -- @

  -- | Takes a request of type @t :: * -> *@, and injects it into the
  -- 'Union'.
  --
  -- /O(1)/
  inj :: eff a -> Union effs a

  -- | Project a value of type @'Union' (t ': r) :: * -> *@ into a possible
  -- summand of the type @t :: * -> *@. 'Nothing' means that @t :: * -> *@ is
  -- not the value stored in the @'Union' (t ': r) :: * -> *@.
  --
  -- /O(1)/
  prj :: Union effs a -> Maybe (eff a)

instance (FindElem t r, IfNotFound t r r) => Member t r where
  inj :: t a -> Union r a
inj = Word -> t a -> Union r a
forall k (t :: k -> *) (a :: k) (r :: [* -> *]).
Word -> t a -> Union r a
unsafeInj (Word -> t a -> Union r a) -> Word -> t a -> Union r a
forall a b. (a -> b) -> a -> b
$ P t r -> Word
forall k (t :: k) k (r :: k). P t r -> Word
unP (P t r
forall (t :: * -> *) (r :: [* -> *]). FindElem t r => P t r
elemNo :: P t r)
  {-# INLINE inj #-}

  prj :: Union r a -> Maybe (t a)
prj = Word -> Union r a -> Maybe (t a)
forall k (r :: [* -> *]) (a :: k) (t :: k -> *).
Word -> Union r a -> Maybe (t a)
unsafePrj (Word -> Union r a -> Maybe (t a))
-> Word -> Union r a -> Maybe (t a)
forall a b. (a -> b) -> a -> b
$ P t r -> Word
forall k (t :: k) k (r :: k). P t r -> Word
unP (P t r
forall (t :: * -> *) (r :: [* -> *]). FindElem t r => P t r
elemNo :: P t r)
  {-# INLINE prj #-}

-- | Orthogonal decomposition of a @'Union' (t ': r) :: * -> *@. 'Right' value
-- is returned if the @'Union' (t ': r) :: * -> *@ contains @t :: * -> *@, and
-- 'Left' when it doesn't. Notice that 'Left' value contains
-- @Union r :: * -> *@, i.e. it can not contain @t :: * -> *@.
--
-- /O(1)/
decomp :: Union (t ': r) a -> Either (Union r a) (t a)
decomp :: Union (t : r) a -> Either (Union r a) (t a)
decomp (Union Word
0 t a
a) = t a -> Either (Union r a) (t a)
forall a b. b -> Either a b
Right (t a -> Either (Union r a) (t a))
-> t a -> Either (Union r a) (t a)
forall a b. (a -> b) -> a -> b
$ t a -> t a
forall a b. a -> b
unsafeCoerce t a
a
decomp (Union Word
n t a
a) = Union r a -> Either (Union r a) (t a)
forall a b. a -> Either a b
Left  (Union r a -> Either (Union r a) (t a))
-> Union r a -> Either (Union r a) (t a)
forall a b. (a -> b) -> a -> b
$ Word -> t a -> Union r a
forall k (t :: k -> *) (a :: k) (r :: [* -> *]).
Word -> t a -> Union r a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
- Word
1) t a
a
{-# INLINE [2] decomp #-}

-- | Specialized version of 'decomp' for efficiency.
--
-- /O(1)/
--
-- TODO: Check that it actually adds on efficiency.
decomp0 :: Union '[t] a -> Either (Union '[] a) (t a)
decomp0 :: Union '[t] a -> Either (Union '[] a) (t a)
decomp0 (Union Word
_ t a
a) = t a -> Either (Union '[] a) (t a)
forall a b. b -> Either a b
Right (t a -> Either (Union '[] a) (t a))
-> t a -> Either (Union '[] a) (t a)
forall a b. (a -> b) -> a -> b
$ t a -> t a
forall a b. a -> b
unsafeCoerce t a
a
{-# INLINE decomp0 #-}
{-# RULES "decomp/singleton"  decomp = decomp0 #-}

-- | Specialised version of 'prj'\/'decomp' that works on an
-- @'Union' '[t] :: * -> *@ which contains only one specific summand. Hence the
-- absence of 'Maybe', and 'Either'.
--
-- /O(1)/
extract :: Union '[t] a -> t a
extract :: Union '[t] a -> t a
extract (Union Word
_ t a
a) = t a -> t a
forall a b. a -> b
unsafeCoerce t a
a
{-# INLINE extract #-}

-- | Inject whole @'Union' r@ into a weaker @'Union' (any ': r)@ that has one
-- more summand.
--
-- /O(1)/
weaken :: Union r a -> Union (any ': r) a
weaken :: Union r a -> Union (any : r) a
weaken (Union Word
n t a
a) = Word -> t a -> Union (any : r) a
forall k (t :: k -> *) (a :: k) (r :: [* -> *]).
Word -> t a -> Union r a
Union (Word
n Word -> Word -> Word
forall a. Num a => a -> a -> a
+ Word
1) t a
a
{-# INLINE weaken #-}

infixr 5 :++:
type family xs :++: ys where
  '[] :++: ys = ys
  (x ': xs) :++: ys = x ': (xs :++: ys)

class Weakens q where
  weakens :: Union r a -> Union (q :++: r) a

instance Weakens '[] where
  weakens :: Union r a -> Union ('[] :++: r) a
weakens = Union r a -> Union ('[] :++: r) a
forall a. a -> a
id
  {-# INLINE weakens #-}

instance Weakens xs => Weakens (x ': xs) where
  weakens :: Union r a -> Union ((x : xs) :++: r) a
weakens Union r a
u = Union (xs :++: r) a -> Union (x : (xs :++: r)) a
forall k (r :: [* -> *]) (a :: k) (any :: * -> *).
Union r a -> Union (any : r) a
weaken (Union r a -> Union (xs :++: r) a
forall (q :: [* -> *]) k (r :: [* -> *]) (a :: k).
Weakens q =>
Union r a -> Union (q :++: r) a
weakens @xs Union r a
u)
  {-# INLINEABLE weakens #-}