{-# OPTIONS_HADDOCK show-extensions #-}
{-# OPTIONS_GHC -Wwarn #-}
{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE PatternSynonyms, ViewPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

-- Only for SetMember below, when emulating Monad Transformers
{-# LANGUAGE FunctionalDependencies, UndecidableInstances #-}

-- | Open unions (type-indexed co-products) for extensible effects
-- All operations are constant-time, and there is no Typeable constraint
--
-- This is a variation of OpenUion5.hs, which relies on overlapping
-- instances instead of closed type families. Closed type families
-- have their problems: overlapping instances can resolve even
-- for unground types, but closed type families are subject to a
-- strict apartness condition.
--
-- This implementation is very similar to OpenUnion1.hs, but without
-- the annoying Typeable constraint. We sort of emulate it:
--
-- Our list r of open union components is a small Universe.
-- Therefore, we can use the Typeable-like evidence in that
-- universe. We hence can define
--
-- @
-- data Union r v where
--   Union :: t v -> TRep t r -> Union r v -- t is existential
-- @
-- where
--
-- @
-- data TRep t r where
--   T0 :: TRep t (t ': r)
--   TS :: TRep t r -> TRep (any ': r)
-- @
-- Then Member is a type class that produces TRep
-- Taken literally it doesn't seem much better than
-- OpenUinion41.hs. However, we can cheat and use the index of the
-- type t in the list r as the TRep. (We will need UnsafeCoerce then).
--
-- The interface is the same as of other OpenUnion*.hs
module Data.OpenUnion ( Union
                      , inj
                      , prj, pattern U0'
                      , decomp, pattern U0, pattern U1
                      , Member
                      , SetMember
                      , type(<::)
                      , weaken
                      ) where

import Unsafe.Coerce(unsafeCoerce)

import Data.Kind (Constraint)
import GHC.TypeLits

-- | The data constructors of Union are not exported
--
-- Strong Sum (Existential with the evidence) is an open union
-- t is can be a GADT and hence not necessarily a Functor.
-- Int is the index of t in the list r; that is, the index of t in the
-- universe r
data Union (r :: [ * -> * ]) v where
  Union :: {-# UNPACK #-} !Int -> t v -> Union r v

{-# INLINE prj' #-}
{-# INLINE inj' #-}
inj' :: Int -> t v -> Union r v
inj' = Union

prj' :: Int -> Union r v -> Maybe (t v)
prj' n (Union n' x) | n == n'   = Just (unsafeCoerce x)
                    | otherwise = Nothing

newtype P t r = P{unP :: Int}

-- | Typeclass that asserts that effect @t@ is contained inside the effect-list
-- @r@.
--
-- The @FindElem@ typeclass is an implementation detail and not required for
-- using the effect list or implementing custom effects.
class (FindElem t r) => Member (t :: * -> *) r where
  inj :: t v -> Union r v
  prj :: Union r v -> Maybe (t v)

-- | Pattern synonym to project the union onto the effect @t@.
pattern U0' :: Member t r => t v -> Union r v
pattern U0' h <- (prj -> Just h) where
  U0' h = inj h

-- | Explicit type-level equality condition is a dirty
-- hack to eliminate the type annotation in the trivial case,
-- such as @run (runReader () get)@.
--
-- There is no ambiguity when finding instances for
-- @Member t (a ': b ': r)@, which the second instance is selected.
--
-- The only case we have to concerned about is  @Member t '[s]@.
-- But, in this case, values of definition is the same (if present),
-- and the first one is chosen according to GHC User Manual, since
-- the latter one is incoherent. This is the optimal choice.
instance {-# OVERLAPPING #-} t ~ s => Member t '[s] where
   {-# INLINE inj #-}
   {-# INLINE prj #-}
   inj x           = Union 0 x
   prj (Union _ x) = Just (unsafeCoerce x)
-- Note that if it weren't for us wanting to use the specialized instance above
-- we wouldn't need the INCOHERENT pragma below
-- TODO: consider impact of disabling specialization
instance {-# INCOHERENT #-}  (FindElem t r) => Member t r where
  {-# INLINE inj #-}
  {-# INLINE prj #-}
  inj = inj' (unP $ (elemNo :: P t r))
  prj = prj' (unP $ (elemNo :: P t r))

-- | A useful operator for reducing boilerplate in signatures.
--
-- The following lines are equivalent.
--
-- @
-- (Member (Exc e) r, Member (State s) r) => ...
-- [ Exc e, State s ] <:: r => ...
-- @
type family (<::) (ms :: [* -> *]) r where
  (<::) '[] r = (() :: Constraint)
  (<::) (m ': ms) r = (Member m r, (<::) ms r)

{-# INLINE [2] decomp #-}
-- | Orthogonal decomposition of the union: head and the rest.
decomp :: Union (t ': r) v -> Either (Union r v) (t v)
decomp (Union 0 v) = Right $ unsafeCoerce v
decomp (Union n v) = Left  $ Union (n-1) v

-- | Some helpful pattern synonyms.
-- U0 : the first element of the union
pattern U0 :: t v -> Union (t ': r) v
pattern U0 h <- (decomp -> Right h) where
  U0 h = inj h
-- | U1 : everything excluding the first element of the union.
pattern U1 t <- (decomp -> Left t) where
  U1 t = weaken t
{-# COMPLETE U0, U1 #-}

-- Specialized version
{-# RULES "decomp/singleton"  decomp = decomp0 #-}
{-# INLINE decomp0 #-}
decomp0 :: Union '[t] v -> Either (Union '[] v) (t v)
decomp0 (Union _ v) = Right $ unsafeCoerce v
-- No other case is possible

weaken :: Union r w -> Union (any ': r) w
weaken (Union n v) = Union (n+1) v

-- | Find the index of an element in a type-level list.
-- The element must exist
-- This is essentially a compile-time computation.
-- Using overlapping instances here is OK since this class is private to this
-- module
class FindElem (t :: * -> *) r where
  elemNo :: P t r

instance FindElem t (t ': r) where
  elemNo = P 0
instance {-# OVERLAPPABLE #-} FindElem t r => FindElem t (t' ': r) where
  elemNo = P $ 1 + (unP $ (elemNo :: P t r))
instance TypeError ('Text "Cannot unify effect types." ':$$:
                    'Text "Unhandled effect: " ':<>: 'ShowType t ':$$:
                    'Text "Perhaps check the type of effectful computation and the sequence of handlers for concordance?")
  => FindElem t '[] where
  elemNo = error "unreachable"

-- | Using overlapping instances here is OK since this class is private to this
-- module
class EQU (a :: k) (b :: k) p | a b -> p
instance EQU a a 'True
instance {-# OVERLAPPABLE #-} (p ~ 'False) => EQU a b p

-- | This class is used for emulating monad transformers
class Member t r => SetMember (tag :: k -> * -> *) (t :: * -> *) r | tag r -> t
instance (EQU t1 t2 p, MemberU' p tag t1 (t2 ': r)) => SetMember tag t1 (t2 ': r)

class Member t r =>
      MemberU' (f::Bool) (tag :: k -> * -> *) (t :: * -> *) r | tag r -> t
instance MemberU' 'True tag (tag e) (tag e ': r)
instance (Member t (t' ': r), SetMember tag t r) =>
           MemberU' 'False tag t (t' ': r)