predicate-typed-0.7.4.4: src/Predicate/Data/Either.hs

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE EmptyDataDeriving #-}
-- | promoted 'Either' functions
module Predicate.Data.Either (

 -- ** predicates
    IsLeft
  , IsRight

 -- ** constructors
  , MkLeft
  , MkLeft'
  , MkRight
  , MkRight'

 -- ** get rid of Either
  , Left'
  , Right'
  , LeftDef
  , LeftFail
  , RightDef
  , RightFail
  , EitherBool
  , PartitionEithers

 -- ** miscellaneous
  , type (|||)
  , type (+++)
  , EitherIn
  , EitherId
  , LeftDef'
  , RightDef'

 -- ** type families
  , EitherInT
 ) where
import Predicate.Core
import Predicate.Misc
import Predicate.Util
import GHC.TypeLits (ErrorMessage((:$$:),(:<>:)))
import qualified GHC.TypeLits as GL
import Data.Proxy (Proxy(Proxy))
import Data.Kind (Type)
import Data.Either (isLeft, isRight, partitionEithers)

-- $setup
-- >>> :set -XDataKinds
-- >>> :set -XTypeApplications
-- >>> :set -XTypeOperators
-- >>> :set -XOverloadedStrings
-- >>> import qualified Data.Text as T
-- >>> import Predicate.Prelude
-- >>> import qualified Data.Semigroup as SG

-- | extracts the left value from an 'Either'
--
-- >>> pz @(Left' >> Succ) (Left 20)
-- Val 21
--
-- >>> pz @(Left' >> Succ) (Right 'a')
-- Fail "Left' found Right"
--
data Left' deriving Show
instance Show a => P Left' (Either a x) where
  type PP Left' (Either a x) = a
  eval _ opts lr =
    let msg0 = "Left'"
    in pure $ case lr of
         Right _ -> mkNode opts (Fail (msg0 <> " found Right")) "" []
         Left a -> mkNode opts (Val a) (msg0 <> " " <> showL opts a) []

-- | extracts the right value from an 'Either'
--
-- >>> pz @(Right' >> Succ) (Right 20)
-- Val 21
--
-- >>> pz @(Right' >> Succ) (Left 'a')
-- Fail "Right' found Left"
--
data Right' deriving Show
instance Show a => P Right' (Either x a) where
  type PP Right' (Either x a) = a
  eval _ opts lr =
    let msg0 = "Right'"
    in pure $ case lr of
         Left _ -> mkNode opts (Fail (msg0 <> " found Left")) "" []
         Right a -> mkNode opts (Val a) (msg0 <> " " <> showL opts a) []

-- | similar 'Control.Arrow.|||'
--
-- >>> pz @(Pred ||| Id) (Left 13)
-- Val 12
--
-- >>> pz @(ShowP Id ||| Id) (Right "hello")
-- Val "hello"
--
-- >>> pl @('True ||| 'False) (Left "someval")
-- True ((|||) Left True | "someval")
-- Val True
--
-- >>> pl @('True ||| 'False) (Right "someval")
-- False ((|||) Right False | "someval")
-- Val False
--
-- >>> pl @(ShowP Succ ||| ShowP Id) (Left 123)
-- Present "124" ((|||) Left "124" | 123)
-- Val "124"
--
-- >>> pl @(ShowP Succ ||| ShowP Id) (Right True)
-- Present "True" ((|||) Right "True" | True)
-- Val "True"
--
-- >>> pl @(Not Id ||| Id) (Right True)
-- Present True ((|||) Right True | True)
-- Val True
--
-- >>> pl @(Not Id ||| Id) (Left True)
-- False ((|||) Left False | True)
-- Val False
--
data p ||| q deriving Show
infixr 2 |||

instance ( Show (PP p a)
         , P p a
         , P q b
         , PP p a ~ PP q b
         , Show a
         , Show b
         ) => P (p ||| q) (Either a b) where
  type PP (p ||| q) (Either a b) = PP p a
  eval _ opts lr = do
    let msg0 = "(|||)"
    case lr of
      Left a -> do
        pp <- eval (Proxy @p) opts a
        pure $ case getValueLR NoInline opts msg0 pp [] of
          Left e -> e
          Right a1 -> let msg1 = msg0 ++ " Left"
                      in mkNodeCopy opts pp (show3 opts msg1 a1 a) []
      Right a -> do
        qq <- eval (Proxy @q) opts a
        pure $ case getValueLR NoInline opts msg0 qq [] of
          Left e -> e
          Right a1 ->
            let msg1 = msg0 ++ " Right"
            in mkNodeCopy opts qq (show3 opts msg1 a1 a) []

-- | similar to 'isLeft'
--
-- >>> pz @IsLeft (Right 123)
-- Val False
--
-- >>> pz @IsLeft (Left 'a')
-- Val True
--
data IsLeft deriving Show

instance x ~ Either a b
       => P IsLeft x where
  type PP IsLeft x = Bool
  eval _ opts x = pure $ mkNodeB opts (isLeft x) "IsLeft" []

-- | similar to 'isRight'
--
-- >>> pz @IsRight (Right 123)
-- Val True
--
-- >>> pz @IsRight (Left "aa")
-- Val False
--
data IsRight deriving Show

instance x ~ Either a b
         => P IsRight x where
  type PP IsRight x = Bool
  eval _ opts x = pure $ mkNodeB opts (isRight x) "IsRight" []


-- | similar 'Control.Arrow.+++'
--
-- >>> pz @(Pred +++ Id) (Left 13)
-- Val (Left 12)
--
-- >>> pz @(ShowP Id +++ Reverse) (Right "hello")
-- Val (Right "olleh")
--
-- >>> pl @(HeadDef 'False Id +++ Id) (Right @[Bool] 1) -- need @[Bool] to match with 'False
-- Present Right 1 ((+++) Right 1 | 1)
-- Val (Right 1)
--
-- >>> pl @(HeadDef 'False Id +++ Id) (Left [True,False]) -- need @[Bool] to match with 'False!
-- Present Left True ((+++) Left True | [True,False])
-- Val (Left True)
--
-- >>> pl @(Not Id +++ Id) (Right True)
-- Present Right True ((+++) Right True | True)
-- Val (Right True)
--
-- >>> pl @(Not Id +++ Id) (Right 12)
-- Present Right 12 ((+++) Right 12 | 12)
-- Val (Right 12)
--
-- >>> pl @(HeadDef () Id +++ Id) (Right @[()] 1) -- breaks otherwise: Id says () -> () so has to be a list of [()]
-- Present Right 1 ((+++) Right 1 | 1)
-- Val (Right 1)
--
-- >>> pl @(HeadDef () Id +++ Id) (Right @[()] 1) -- this breaks! as Left doesnt have a type
-- Present Right 1 ((+++) Right 1 | 1)
-- Val (Right 1)
--
-- >>> pl @(Not Id +++ Id) (Right @Bool 12)
-- Present Right 12 ((+++) Right 12 | 12)
-- Val (Right 12)
--
data p +++ q deriving Show
infixr 2 +++

instance ( Show (PP p a)
         , Show (PP q b)
         , P p a
         , P q b
         , Show a
         , Show b
         ) => P (p +++ q) (Either a b) where
  type PP (p +++ q) (Either a b) = Either (PP p a) (PP q b)
  eval _ opts lr = do
    let msg0 = "(+++)"
    case lr of
      Left a -> do
        pp <- eval (Proxy @p) opts a
        pure $ case getValueLR NoInline opts msg0 pp [] of
          Left e -> e
          Right p ->
            let msg1 = msg0 ++ " Left"
            in mkNode opts (Val (Left p)) (msg1 <> " " <> showL opts p <> showVerbose opts " | " a) [hh pp]
      Right a -> do
        qq <- eval (Proxy @q) opts a
        pure $ case getValueLR NoInline opts msg0 qq [] of
          Left e -> e
          Right q ->
            let msg1 = msg0 ++ " Right"
            in mkNode opts (Val (Right q)) (msg1 <> " " <> showL opts q <> showVerbose opts " | " a) [hh qq]

-- | similar to 'partitionEithers'
--
-- >>> pz @PartitionEithers [Left 'a',Right 2,Left 'c',Right 4,Right 99]
-- Val ("ac",[2,4,99])
--
-- >>> pz @PartitionEithers [Right 2,Right 4,Right 99]
-- Val ([],[2,4,99])
--
-- >>> pz @PartitionEithers [Left 'a',Left 'c']
-- Val ("ac",[])
--
-- >>> pz @PartitionEithers ([] :: [Either () Int])
-- Val ([],[])
--
-- >>> pl @PartitionEithers [Left 4, Right 'x', Right 'y',Left 99]
-- Present ([4,99],"xy") (PartitionEithers ([4,99],"xy") | [Left 4,Right 'x',Right 'y',Left 99])
-- Val ([4,99],"xy")
--
-- >>> pl @PartitionEithers [Left 'x', Right 1,Left 'a', Left 'b',Left 'z', Right 10]
-- Present ("xabz",[1,10]) (PartitionEithers ("xabz",[1,10]) | [Left 'x',Right 1,Left 'a',Left 'b',Left 'z',Right 10])
-- Val ("xabz",[1,10])
--
data PartitionEithers deriving Show

instance ( Show a
         , Show b
         ) => P PartitionEithers [Either a b] where
  type PP PartitionEithers [Either a b] = ([a], [b])
  eval _ opts as =
    let msg0 = "PartitionEithers"
        b = partitionEithers as
    in pure $ mkNode opts (Val b) (show3 opts msg0 b as) []

-- | Convenient method to convert a @p@ or @q@ to a 'Either' based on a predicate @b@
--   if @b@ then Right @p@ else Left @q@
--
-- >>> pz @(EitherBool (Fst > 4) L21 L22) (24,(-1,999))
-- Val (Right 999)
--
-- >>> pz @(EitherBool (Fst > 4) L21 L22) (1,(-1,999))
-- Val (Left (-1))
--
-- >>> pl @(EitherBool (Fst > 10) L21 L22) (7,('x',99))
-- Present Left 'x' (EitherBool(False) Left 'x')
-- Val (Left 'x')
--
-- >>> pl @(EitherBool (Fst > 10) L21 L22) (11,('x',99))
-- Present Right 99 (EitherBool(True) Right 99)
-- Val (Right 99)
--
-- >>> pl @(EitherBool (Gt 10) "found left" 99) 12
-- Present Right 99 (EitherBool(True) Right 99)
-- Val (Right 99)
--
-- >>> pl @(EitherBool (Gt 10) "found left" 99) 7
-- Present Left "found left" (EitherBool(False) Left "found left")
-- Val (Left "found left")
--
data EitherBool b p q deriving Show

instance ( Show (PP p a)
         , P p a
         , Show (PP q a)
         , P q a
         , P b a
         , PP b a ~ Bool
         ) => P (EitherBool b p q) a where
  type PP (EitherBool b p q) a = Either (PP p a) (PP q a)
  eval _ opts z = do
    let msg0 = "EitherBool"
    bb <- evalBool (Proxy @b) opts z
    case getValueLR NoInline opts (msg0 <> " b failed") bb [] of
      Left e -> pure e
      Right False -> do
        pp <- eval (Proxy @p) opts z
        pure $ case getValueLR NoInline opts (msg0 <> " p failed") pp [hh bb] of
          Left e -> e
          Right p -> mkNode opts (Val (Left p)) (msg0 <> "(False) Left " <> showL opts p) [hh bb, hh pp]
      Right True -> do
        qq <- eval (Proxy @q) opts z
        pure $ case getValueLR NoInline opts (msg0 <> " q failed") qq [hh bb] of
          Left e -> e
          Right q -> mkNode opts (Val (Right q)) (msg0 <> "(True) Right " <> showL opts q) [hh bb, hh qq]

-- | 'Data.Either.Left' constructor
data MkLeft' t p deriving Show

instance ( Show (PP p x)
         , P p x
         ) => P (MkLeft' t p) x where
  type PP (MkLeft' t p) x = Either (PP p x) (PP t x)
  eval _ opts x = do
    let msg0 = "MkLeft"
    pp <- eval (Proxy @p) opts x
    pure $ case getValueLR NoInline opts msg0 pp [] of
      Left e -> e
      Right p ->
        let d = Left p
        in mkNode opts (Val d) (msg0 <> " Left " <> showL opts p) [hh pp]

-- | 'Data.Either.Left' constructor
--
-- >>> pz @(MkLeft _ Id) 44
-- Val (Left 44)
--
data MkLeft (t :: Type) p deriving Show
type MkLeftT (t :: Type) p = MkLeft' (Hole t) p

instance P (MkLeftT t p) x => P (MkLeft t p) x where
  type PP (MkLeft t p) x = PP (MkLeftT t p) x
  eval _ = eval (Proxy @(MkLeftT t p))

-- | 'Data.Either.Right' constructor
data MkRight' t p deriving Show

instance ( Show (PP p x)
         , P p x
         ) => P (MkRight' t p) x where
  type PP (MkRight' t p) x = Either (PP t x) (PP p x)
  eval _ opts x = do
    let msg0 = "MkRight"
    pp <- eval (Proxy @p) opts x
    pure $ case getValueLR NoInline opts msg0 pp [] of
      Left e -> e
      Right p ->
        let d = Right p
        in mkNode opts (Val d) (msg0 <> " Right " <> showL opts p) [hh pp]

-- | 'Data.Either.Right' constructor
--
-- >>> pz @(MkRight _ Id) 44
-- Val (Right 44)
--
data MkRight (t :: Type) p deriving Show
type MkRightT (t :: Type) p = MkRight' (Hole t) p

instance P (MkRightT t p) x => P (MkRight t p) x where
  type PP (MkRight t p) x = PP (MkRightT t p) x
  eval _ = eval (Proxy @(MkRightT t p))

-- | extract the Left value from an 'Either' otherwise use the default value: similar to 'Data.Either.fromLeft'
--
-- if there is no Left value then @p@ is passed the Right value and the whole context
--
-- >>> pz @(LeftDef (1 % 4) Id) (Left 20.4)
-- Val (102 % 5)
--
-- >>> pz @(LeftDef (1 % 4) Id) (Right "aa")
-- Val (1 % 4)
--
-- >>> pz @(LeftDef (PrintT "found right=%s fst=%d" '(Fst,L21)) Snd) (123,Right "xy")
-- Val "found right=xy fst=123"
--
-- >>> pz @(LeftDef (MEmptyT _) Id) (Right 222)
-- Val ()
--
-- >>> pz @(LeftDef (MEmptyT (SG.Sum _)) Id) (Right 222)
-- Val (Sum {getSum = 0})
--
data LeftDef p q deriving Show

instance ( PP q x ~ Either a b
         , PP p (b,x) ~ a
         , P q x
         , P p (b,x)
    ) => P (LeftDef p q) x where
  type PP (LeftDef p q) x = LeftT (PP q x)
  eval _ opts x = do
    let msg0 = "LeftDef"
    qq <- eval (Proxy @q) opts x
    case getValueLR NoInline opts msg0 qq [] of
      Left e -> pure e
      Right q ->
        case q of
          Left a -> pure $ mkNode opts (Val a) (msg0 <> " Left") [hh qq]
          Right b -> do
            pp <- eval (Proxy @p) opts (b,x)
            pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
              Left e -> e
              Right _ -> mkNodeCopy opts pp (msg0 <> " Right") [hh qq]

-- | extract the Right value from an 'Either': similar to 'Data.Either.fromRight'
--
-- if there is no Right value then @p@ is passed the Left value and the whole context
--
-- >>> pz @(RightDef (1 % 4) Id) (Right 20.4)
-- Val (102 % 5)
--
-- >>> pz @(RightDef (1 % 4) Id) (Left "aa")
-- Val (1 % 4)
--
-- >>> pz @(RightDef (PrintT "found left=%s fst=%d" '(Fst,L21)) Snd) (123,Left "xy")
-- Val "found left=xy fst=123"
--
-- >>> pz @(RightDef (MEmptyT _) Id) (Left 222)
-- Val ()
--
-- >>> pz @(RightDef (MEmptyT (SG.Sum _)) Id) (Left 222)
-- Val (Sum {getSum = 0})
--
data RightDef p q deriving Show

instance ( PP q x ~ Either a b
         , PP p (a,x) ~ b
         , P q x
         , P p (a,x)
    ) => P (RightDef p q) x where
  type PP (RightDef p q) x = RightT (PP q x)
  eval _ opts x = do
    let msg0 = "RightDef"
    qq <- eval (Proxy @q) opts x
    case getValueLR NoInline opts msg0 qq [] of
      Left e -> pure e
      Right q ->
        case q of
          Right b -> pure $ mkNode opts (Val b) (msg0 <> " Right") [hh qq]
          Left a -> do
            pp <- eval (Proxy @p) opts (a,x)
            pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
              Left e -> e
              Right _ -> mkNodeCopy opts pp (msg0 <> " Left") [hh qq]

-- | extract the Left value from an 'Either' otherwise fail with a message
--
-- if there is no Left value then @p@ is passed the Right value and the whole context
--
-- >>> pz @(LeftFail "oops" Id) (Left 20.4)
-- Val 20.4
--
-- >>> pz @(LeftFail "oops" Id) (Right "aa")
-- Fail "oops"
--
-- >>> pz @(LeftFail (PrintT "found right=%s fst=%d" '(Fst,L21)) Snd) (123,Right "xy")
-- Fail "found right=xy fst=123"
--
-- >>> pz @(LeftFail (MEmptyT _) Id) (Right 222)
-- Fail ""
--
-- >>> pl @(LeftFail (PrintF "someval=%d" L21) Snd) (13::Int,Right @(SG.Sum Int) "abc")
-- Error someval=13 (LeftFail Right)
-- Fail "someval=13"
--
-- >>> pl @(LeftFail (PrintF "someval=%s" Fst) Id) (Right @(SG.Sum Int) "abc")
-- Error someval=abc (LeftFail Right)
-- Fail "someval=abc"
--
-- >>> pl @(LeftFail (PrintF "found rhs=%d" Fst) Id) (Right @String @Int 10)
-- Error found rhs=10 (LeftFail Right)
-- Fail "found rhs=10"
--
-- >>> pl @(LeftFail (PrintF "found rhs=%d" (Snd >> L22)) L21) ('x',(Right 10,23))
-- Error found rhs=23 (LeftFail Right)
-- Fail "found rhs=23"
--
-- >>> pl @(LeftFail (PrintF "found rhs=%d" (L2 L22)) L21) ('x',(Left "abc",23))
-- Present "abc" (Left)
-- Val "abc"
--
data LeftFail p q deriving Show

instance ( PP p (b,x) ~ String
         , PP q x ~ Either a b
         , P p (b,x)
         , P q x
         )
    => P (LeftFail p q) x where
  type PP (LeftFail p q) x = LeftT (PP q x)
  eval _ opts x = do
    let msg0 = "LeftFail"
    qq <- eval (Proxy @q) opts x
    case getValueLR NoInline opts msg0 qq [] of
      Left e -> pure e
      Right q ->
        case q of
          Left a -> pure $ mkNode opts (Val a) "Left" [hh qq]
          Right b -> do
            pp <- eval (Proxy @p) opts (b,x)
            pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
              Left e -> e
              Right p -> mkNode opts (Fail p) (msg0 <> " Right") [hh qq, hh pp]


-- | extract the Right value from an 'Either' otherwise fail with a message
--
-- if there is no Right value then @p@ is passed the Left value and the whole context
--
-- >>> pz @(RightFail "oops" Id) (Right 20.4)
-- Val 20.4
--
-- >>> pz @(RightFail "oops" Id) (Left "aa")
-- Fail "oops"
--
-- >>> pz @(RightFail (PrintT "found left=%s fst=%d" '(Fst,L21)) Snd) (123,Left "xy")
-- Fail "found left=xy fst=123"
--
-- >>> pz @(RightFail (MEmptyT _) Id) (Left 222)
-- Fail ""
--
data RightFail p q deriving Show

instance ( PP p (a,x) ~ String
         , PP q x ~ Either a b
         , P p (a,x)
         , P q x
         )
    => P (RightFail p q) x where
  type PP (RightFail p q) x = RightT (PP q x)
  eval _ opts x = do
    let msg0 = "RightFail"
    qq <- eval (Proxy @q) opts x
    case getValueLR NoInline opts msg0 qq [] of
      Left e -> pure e
      Right q ->
        case q of
          Right b -> pure $ mkNode opts (Val b) "Right" [hh qq]
          Left a -> do
            pp <- eval (Proxy @p) opts (a,x)
            pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
              Left e -> e
              Right p -> mkNode opts (Fail p) (msg0 <> " Left") [hh qq, hh pp]


-- | destructor for Either (similar to 'Control.Arrow.|||' but with an extra environment @s@)
--   @p@ @Left a@ receives @(PP t x,a)@
--   @q@ @Right b@ receives @(PP t x,b)@
--   @s@ points to the environment you want to pass in
--   @t@ points to the Either value
--
-- >>> pz @(EitherIn (ShowP (Fst + Snd)) (ShowP Id) Fst Snd) (9,Left 123)
-- Val "132"
--
-- >>> pz @(EitherIn (ShowP (Fst + Snd)) (ShowP Id) Fst Snd) (9,Right 'x')
-- Val "(9,'x')"
--
-- >>> pz @(EitherIn (ShowP Id) (ShowP (Second Succ)) Fst Snd) (9,Right 'x')
-- Val "(9,'y')"
--
-- >>> pz @(EitherIn (FailT _ (PrintF ("found left=%d") Snd)) (Second Succ) Fst Snd) (9,Right 'x')
-- Val (9,'y')
--
-- >>> pz @(EitherIn (FailT _ (PrintF ("found left=%d") Snd)) (Second Succ) Fst Snd) (9,Left 13)
-- Fail "found left=13"
--
data EitherIn p q s t deriving Show

instance ( Show a
         , Show b
         , Show (PP q (y,b))
         , P p (y,a)
         , P q (y,b)
         , PP p (y,a) ~ PP q (y,b)
         , P s x
         , P t x
         , PP s x ~ y
         , PP t x ~ Either a b
         )  => P (EitherIn p q s t) x where
  type PP (EitherIn p q s t) x = EitherInT p (PP s x) (PP t x)
  eval _ opts x = do
    let msg0 = "EitherIn"
    lr <- runPQ NoInline msg0 (Proxy @s) (Proxy @t) opts x []
    case lr of
      Left e -> pure e
      Right (s,t,ss,tt) -> do
         let hhs = [hh ss, hh tt]
         case t of
            Left a -> do
              let msg1 = msg0 <> "(Left)"
              pp <- eval (Proxy @p) opts (s,a)
              pure $ case getValueLR NoInline opts (msg1 <> " p failed") pp hhs of
                   Left e -> e
                   Right c -> mkNodeCopy opts pp (show3 opts msg1 c a) hhs
            Right b -> do
              let msg1 = msg0 <> "(Right)"
              qq <- eval (Proxy @q) opts (s,b)
              pure $ case getValueLR NoInline opts (msg1 <> " q failed") qq hhs of
                   Left e -> e
                   Right c -> mkNodeCopy opts qq (show3 opts msg1 c b) hhs

type family EitherInT (p :: k) (y :: Type) (lr :: Type) where
  EitherInT p y (Either a _) = PP p (y,a)
  EitherInT _ _ o = GL.TypeError (
      'GL.Text "EitherInT: expected 'Either a b' "
      ':$$: 'GL.Text "o = "
      ':<>: 'GL.ShowType o)

-- | simple version of 'EitherIn' with Id as the Either value and the environment set to ()
--
-- >>> pz @(EitherId '(Id,"fromleft") '(888,Id)) (Right "ok")
-- Val (888,"ok")
--
-- >>> pz @(EitherId '(Id,"fromleft") '(888,Id)) (Left 123)
-- Val (123,"fromleft")
--
data EitherId p q deriving Show
type EitherIdT p q = EitherIn (Snd >> p) (Snd >> q) () Id

instance P (EitherIdT p q) x => P (EitherId p q) x where
  type PP (EitherId p q) x = PP (EitherIdT p q) x
  eval _ = eval (Proxy @(EitherIdT p q))


-- | get Left or use the default value @p@: @q@ is the environment and @r@ is the Elr value
--
-- >>> pz @(LeftDef' 999 () Id) (Right "sdf")
-- Val 999
--
-- >>> pz @(LeftDef' 999 () Id) (Left 1)
-- Val 1
--
data LeftDef' p q r deriving Show

type LeftDefT' p q r = EitherIn Snd (Fst >> p) q r

instance P (LeftDefT' p q r) x => P (LeftDef' p q r) x where
  type PP (LeftDef' p q r) x = PP (LeftDefT' p q r) x
  eval _ = eval (Proxy @(LeftDefT' p q r))

-- | get Right or use the default value @p@: @q@ is the environment and @r@ is the Elr value
--
-- >>> pz @(RightDef' 999 () Id) (Left "sdf")
-- Val 999
--
-- >>> pz @(RightDef' 999 Fst Snd) (999,Right 1)
-- Val 1
--
data RightDef' p q r deriving Show

type RightDefT' p q r = EitherIn (Fst >> p) Snd q r

instance P (RightDefT' p q r) x => P (RightDef' p q r) x where
  type PP (RightDef' p q r) x = PP (RightDefT' p q r) x
  eval _ = eval (Proxy @(RightDefT' p q r))