content: {-# 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 = 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 n (Union n' x)
    | n == n'   = Just (unsafeCoerce x)
    | otherwise = Nothing
  {-# INLINE unsafePrj #-}
  
  -- | Represents position of element @t :: * -> *@ in a type list
  -- @r :: [* -> *]@.
  newtype P t r = P {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 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 $ 1 + unP (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 = unsafeInj $ unP (elemNo :: P t r)
    {-# INLINE inj #-}
  
    prj = unsafePrj $ unP (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 0 a) = Right $ unsafeCoerce a
  decomp (Union n a) = Left  $ Union (n - 1) 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 _ a) = Right $ unsafeCoerce 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 _ a) = unsafeCoerce 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 n a) = Union (n + 1) 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 = id
    {-# INLINE weakens #-}
  
  instance Weakens xs => Weakens (x ': xs) where
    weakens u = weaken (weakens @xs u)
    {-# INLINEABLE weakens #-}
  