predicate-typed 0.7.2.0 → 0.7.3.0

raw patch · 38 files changed

+16410/−12825 lines, 38 filesdep +aeson-prettydep +string-conversionsPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: aeson-pretty, string-conversions

API changes (from Hackage documentation)

Files

• predicate-typed.cabal +50/−2
• src/Predicate/Core.hs +2389/−885
• src/Predicate/Data/Char.hs +472/−0
• src/Predicate/Data/Condition.hs +921/−0
• src/Predicate/Data/DateTime.hs +599/−0
• src/Predicate/Data/Either.hs +644/−0
• src/Predicate/Data/Enum.hs +512/−0
• src/Predicate/Data/Extra.hs +1053/−0
• src/Predicate/Data/Foldable.hs +531/−0
• src/Predicate/Data/IO.hs +326/−0
• src/Predicate/Data/Index.hs +534/−0
• src/Predicate/Data/Iterator.hs +594/−0
• src/Predicate/Data/Json.hs +198/−0
• src/Predicate/Data/List.hs +1885/−0
• src/Predicate/Data/Maybe.hs +487/−0
• src/Predicate/Data/Monoid.hs +314/−0
• src/Predicate/Data/Numeric.hs +1068/−0
• src/Predicate/Data/Ordering.hs +598/−0
• src/Predicate/Data/ReadShow.hs +412/−0
• src/Predicate/Data/Regex.hs +602/−0
• src/Predicate/Data/String.hs +429/−0
• src/Predicate/Data/These.hs +1029/−0
• src/Predicate/Data/Tuple.hs +324/−0
• src/Predicate/Examples/Common.hs +38/−2
• src/Predicate/Examples/Refined1.hs +2/−2
• src/Predicate/Examples/Refined2.hs +40/−1
• src/Predicate/Examples/Refined3.hs +49/−12
• src/Predicate/Prelude.hs +51/−11111
• src/Predicate/Refined.hs +12/−13
• src/Predicate/Refined1.hs +17/−17
• src/Predicate/Refined2.hs +18/−15
• src/Predicate/Refined3.hs +41/−23
• src/Predicate/Util.hs +151/−32
• src/Predicate/Util_TH.hs +2/−2
• test/TestJson.hs +1/−1
• test/TestPredicate.hs +5/−695
• test/TestRefined2.hs +8/−8
• test/TestRefined3.hs +4/−4

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 6b4766366591bfcedbf8b3452314ca1261917f6b3261789d01dca0eebe6b6b8d+-- hash: aa2ab78d68dcddef601cdef424ad1d3c3bb857cb5afc594647e650913558a4a1  name:           predicate-typed-version:        0.7.2.0+version:        0.7.3.0 synopsis:       Predicates, Refinement types and Dsl description:    Please see the README on GitHub at <https://github.com/gbwey/predicate-typed#readme> category:       Data@@ -28,6 +28,27 @@   exposed-modules:       Predicate       Predicate.Core+      Predicate.Data.Char+      Predicate.Data.Condition+      Predicate.Data.DateTime+      Predicate.Data.Either+      Predicate.Data.Enum+      Predicate.Data.Extra+      Predicate.Data.Foldable+      Predicate.Data.Index+      Predicate.Data.IO+      Predicate.Data.Iterator+      Predicate.Data.Json+      Predicate.Data.List+      Predicate.Data.Maybe+      Predicate.Data.Monoid+      Predicate.Data.Numeric+      Predicate.Data.Ordering+      Predicate.Data.ReadShow+      Predicate.Data.Regex+      Predicate.Data.String+      Predicate.Data.These+      Predicate.Data.Tuple       Predicate.Examples.Common       Predicate.Examples.Refined1       Predicate.Examples.Refined2@@ -48,6 +69,7 @@   build-depends:       QuickCheck     , aeson+    , aeson-pretty     , base >=4.7 && <5     , binary     , bytestring@@ -63,6 +85,7 @@     , pretty     , pretty-terminal >=0.1.0.0     , safe+    , string-conversions     , template-haskell     , text     , th-lift@@ -79,6 +102,27 @@   other-modules:       Predicate       Predicate.Core+      Predicate.Data.Char+      Predicate.Data.Condition+      Predicate.Data.DateTime+      Predicate.Data.Either+      Predicate.Data.Enum+      Predicate.Data.Extra+      Predicate.Data.Foldable+      Predicate.Data.Index+      Predicate.Data.IO+      Predicate.Data.Iterator+      Predicate.Data.Json+      Predicate.Data.List+      Predicate.Data.Maybe+      Predicate.Data.Monoid+      Predicate.Data.Numeric+      Predicate.Data.Ordering+      Predicate.Data.ReadShow+      Predicate.Data.Regex+      Predicate.Data.String+      Predicate.Data.These+      Predicate.Data.Tuple       Predicate.Examples.Common       Predicate.Examples.Refined1       Predicate.Examples.Refined2@@ -99,6 +143,7 @@   build-depends:       QuickCheck     , aeson+    , aeson-pretty     , base     , binary     , bytestring@@ -116,6 +161,7 @@     , pretty     , pretty-terminal >=0.1.0.0     , safe+    , string-conversions     , template-haskell     , text     , th-lift@@ -143,6 +189,7 @@   build-depends:       QuickCheck     , aeson+    , aeson-pretty     , base     , binary     , bytestring@@ -160,6 +207,7 @@     , pretty-terminal >=0.1.0.0     , safe     , stm+    , string-conversions     , tasty     , tasty-hunit     , tasty-quickcheck

@@ -4,888 +4,2392 @@ {-# OPTIONS -Wincomplete-uni-patterns #-}
 {-# OPTIONS -Wredundant-constraints #-}
 {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE AllowAmbiguousTypes #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TypeApplications #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE NoStarIsType #-}
-{- |
-     Dsl for evaluating and displaying type level expressions
--}
-module Predicate.Core (
-
- -- ** basic types
-    I
-  , Id
-  , IdT
-  , W
-  , Msg
-  , Hide
-
-  -- ** display evaluation tree
-  , pan
-  , panv
-  , pa
-  , pu
-  , pab
-  , pub
-  , pav
-  , puv
-  , pl
-  , pz
-  , run
-  , runs
-
-  , P(..)
-
-  -- ** evaluation methods
-  , runPQ
-  , runPQBool
-  , evalBool
-  , evalBoolHide
-  , evalHide
-  , evalQuick
-  , prtTree
-  ) where
-import Predicate.Util
-import GHC.TypeLits (Symbol,Nat,KnownSymbol,KnownNat)
-import Control.Lens ((&), (^.), (.~))
-import Data.Proxy
-import Data.Typeable
-import Data.Kind (Type)
-import Data.These (These(..))
-import Data.Functor.Identity
--- $setup
--- >>> :set -XDataKinds
--- >>> :set -XTypeApplications
--- >>> :set -XTypeOperators
-
--- | This is the core class. Each instance of this class can be combined into a dsl using 'Predicate.Prelude.>>'
-class P p a where
-  type PP (p :: k) a :: Type -- PP is the output type
-  eval :: MonadEval m
-     => proxy p -- ^ proxy for the expression
-     -> POpts  -- ^ display options
-     -> a      -- ^ value
-     -> m (TT (PP p a)) -- ^ returns a tree of results
-
--- | A specialised form of 'eval' that works only on predicates
-evalBool :: ( MonadEval m
-            , P p a
-            , PP p a ~ Bool
-            ) => proxy p
-              -> POpts
-              -> a
-              -> m (TT (PP p a))
-evalBool p opts a = fixBoolT <$> eval p opts a
-
-evalQuick :: forall p i . P p i => i -> Either String (PP p i)
-evalQuick i = getValLRFromTT (runIdentity (eval (Proxy @p) (getOptT @OL) i))
-
--- | identity function
---
--- >>> pz @I 23
--- PresentT 23
-data I
-instance P I a where
-  type PP I a = a
-  eval _ opts a =
-    let msg0 = "I"
-    in pure $ mkNode opts (PresentT a) msg0 []
-
-
--- | identity function that displays the input unlike 'I'
---
--- even more constraints than 'I' so we might need to add explicit type signatures
---
--- >>> pz @Id 23
--- PresentT 23
-data Id
-instance Show a => P Id a where
-  type PP Id a = a
-  eval _ opts a =
-    let msg0 = "Id"
-    in pure $ mkNode opts (PresentT a) (msg0 <> " " <> showL opts a) []
-
-
--- even more constraints than 'Id' so we might need to explicitly add types (Typeable)
--- | identity function that also displays the type information for debugging
---
--- >>> pz @IdT 23
--- PresentT 23
-data IdT
-instance ( Typeable a
-         , Show a
-         ) => P IdT a where
-  type PP IdT a = a
-  eval _ opts a =
-    let msg0 = "IdT(" <> t <> ")"
-        t = showT @a
-    in pure $ mkNode opts (PresentT a) (msg0 <> " " <> showL opts a) []
-
--- | transparent predicate wrapper to make k of kind 'Type' so it can be in a promoted list (cant mix kinds) see 'Predicate.Core.Do'
---
--- >>> pz @'[W 123, Id] 99
--- PresentT [123,99]
---
--- >>> pz @'[W "abc", W "def", Id, Id] "ghi"
--- PresentT ["abc","def","ghi","ghi"]
---
-data W (p :: k)
-instance P p a => P (W p) a where
-  type PP (W p) a = PP p a
-  eval _ = eval (Proxy @(Msg "W " p))
-
--- | add a message to give more context to the evaluation tree
---
--- >>> pan @(Msg "[somemessage] " Id) 999
--- P [somemessage] Id 999
--- PresentT 999
---
--- >>> pan @(Msg Id 999) "info message:"
--- P info message:'999
--- PresentT 999
---
-data Msg prt p
-
-instance (P prt a
-        , PP prt a ~ String
-        , P p a
-        ) => P (Msg prt p) a where
-  type PP (Msg prt p) a = PP p a
-  eval _ opts a = do
-    pp <- eval (Proxy @prt) opts a
-    case getValueLR opts "Msg" pp [] of
-         Left e -> pure e
-         Right msg -> prefixMsg msg <$> eval (Proxy @p) opts a
-
--- | run the expression \'p\' but remove the subtrees
-data Hide p
--- type H p = Hide p -- doesnt work with %   -- unsaturated!
-
-instance P p x => P (Hide p) x where
-  type PP (Hide p) x = PP p x
-  eval _ opts x = do
-      tt <- eval (Proxy @p) opts x
-      pure $ tt & tForest .~ []
-
--- | 'const' () function
---
--- >>> pz @() "Asf"
--- PresentT ()
---
-instance P () a where
-  type PP () a = ()
-  eval _ opts _ =
-    let msg0 = "()"
-    in pure $ mkNode opts (PresentT ()) msg0 []
-
-instance P (Proxy t) a where
-  type PP (Proxy t) a = Proxy t
-  eval _ opts _ =
-    let msg0 = "Proxy"
-    in pure $ mkNode opts (PresentT Proxy) msg0 []
-
--- Start non-Type kinds
------------------------
-
--- | pulls the type level 'Bool' to the value level
---
--- >>> pz @'True "not used"
--- TrueT
---
--- >>> pz @'False ()
--- FalseT
-instance GetBool b => P (b :: Bool) a where
-  type PP b a = Bool
-  eval _ opts _ =
-    let b = getBool @b
-    in pure $ mkNodeB opts b ("'" <> show b) []
-
--- | pulls the type level 'Symbol' to the value level as a 'GHC.Base.String'
---
--- >>> pz @"hello world" ()
--- PresentT "hello world"
-instance KnownSymbol s => P (s :: Symbol) a where
-  type PP s a = String
-  eval _ opts _ =
-    let s = symb @s
-    in pure $ mkNode opts (PresentT s) ("'" <> litL opts ("\"" <> s <> "\"")) []
-
--- | run the predicates in a promoted 2-tuple; similar to 'Control.Arrow.&&&'
---
--- >>> pz @'(Id, 4) "hello"
--- PresentT ("hello",4)
---
-instance ( P p a
-         , P q a
---         , Show (PP p a)
---         , Show (PP q a)
-         ) => P '(p,q) a where
-  type PP '(p,q) a = (PP p a, PP q a)
-  eval _ opts a = do
-    let msg = "'(,)"
-    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
-    pure $ case lr of
-       Left e -> e
-       Right (p,q,pp,qq) ->
-         mkNode opts (PresentT (p,q)) msg [hh pp, hh qq]
---         mkNode opts (PresentT (p,q)) ("'(" <> showL opts p <> ", " <> showL opts q <> ")") [hh pp, hh qq]
-
--- | run the predicates in a promoted 3-tuple
---
--- >>> pz @'(4, Id, "goodbye") "hello"
--- PresentT (4,"hello","goodbye")
---
--- >>> pan @'( 'True, 'False, 123) True
--- P '(,,)
--- |
--- +- True 'True
--- |
--- +- False 'False
--- |
--- `- P '123
--- PresentT (True,False,123)
---
-instance (P p a
-        , P q a
-        , P r a
-        ) => P '(p,q,r) a where
-  type PP '(p,q,r) a = (PP p a, PP q a, PP r a)
-  eval _ opts a = do
-    let msg = "'(,,)"
-    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
-    case lr of
-      Left e -> pure e
-      Right (p,q,pp,qq) -> do
-         let hhs0 = [hh pp, hh qq]
-         rr <- eval (Proxy @r) opts a
-         pure $ case getValueLR opts msg rr hhs0 of
-           Left e -> e
-           Right r ->
-             let hhs1 = hhs0 <> [hh rr]
-             in mkNode opts (PresentT (p,q,r)) msg hhs1
-
--- | run the predicates in a promoted 4-tuple
---
--- >>> pz @'(4, Id, "inj", 999) "hello"
--- PresentT (4,"hello","inj",999)
---
-instance (P p a
-        , P q a
-        , P r a
-        , P s a
-        ) => P '(p,q,r,s) a where
-  type PP '(p,q,r,s) a = (PP p a, PP q a, PP r a, PP s a)
-  eval _ opts a = do
-    let msg = "'(,,,)"
-    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
-    case lr of
-      Left e -> pure e
-      Right (p,q,pp,qq) -> do
-        let hhs0 = [hh pp, hh qq]
-        lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
-        pure $ case lr1 of
-          Left e -> e
-          Right (r,s,rr,ss) ->
-            let hhs1 = hhs0 ++ [hh rr, hh ss]
-            in mkNode opts (PresentT (p,q,r,s)) msg hhs1
-
--- | run the predicates in a promoted 5-tuple
---
--- >>> pz @'(4, Id, "inj", 999, 'LT) "hello"
--- PresentT (4,"hello","inj",999,LT)
---
-instance (P p a
-        , P q a
-        , P r a
-        , P s a
-        , P t a
-        ) => P '(p,q,r,s,t) a where
-  type PP '(p,q,r,s,t) a = (PP p a, PP q a, PP r a, PP s a, PP t a)
-  eval _ opts a = do
-    let msg = "'(,,,,)"
-    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
-    case lr of
-      Left e -> pure e
-      Right (p,q,pp,qq) -> do
-        let hhs0 = [hh pp, hh qq]
-        lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
-        case lr1 of
-          Left e -> pure e
-          Right (r,s,rr,ss) -> do
-            let hhs1 = hhs0 ++ [hh rr, hh ss]
-            tt <- eval (Proxy @t) opts a
-            pure $ case getValueLR opts msg tt hhs1 of
-              Left e -> e
-              Right t ->
-                let hhs2 = hhs1 <> [hh tt]
-                in mkNode opts (PresentT (p,q,r,s,t)) msg hhs2
-
--- | run the predicates in a promoted 6-tuple
---
--- >>> pz @'(4, Id, "inj", 999, 'LT, 1) "hello"
--- PresentT (4,"hello","inj",999,LT,1)
---
-instance (P p a
-        , P q a
-        , P r a
-        , P s a
-        , P t a
-        , P u a
-        ) => P '(p,q,r,s,t,u) a where
-  type PP '(p,q,r,s,t,u) a = (PP p a, PP q a, PP r a, PP s a, PP t a, PP u a)
-  eval _ opts a = do
-    let msg = "'(,,,,,)"
-    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
-    case lr of
-      Left e -> pure e
-      Right (p,q,pp,qq) -> do
-        let hhs0 = [hh pp, hh qq]
-        lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
-        case lr1 of
-          Left e -> pure e
-          Right (r,s,rr,ss) -> do
-            let hhs1 = hhs0 ++ [hh rr, hh ss]
-            lr2 <- runPQ msg (Proxy @t) (Proxy @u) opts a hhs1
-            pure $ case lr2 of
-              Left e -> e
-              Right (t,u,tt,uu) ->
-                let hhs2 = hhs1 ++ [hh tt, hh uu]
-                in mkNode opts (PresentT (p,q,r,s,t,u)) msg hhs2
-
--- | run the predicates in a promoted 7-tuple
---
--- >>> pz @'(4, Id, "inj", 999, 'LT, 1, 2) "hello"
--- PresentT (4,"hello","inj",999,LT,1,2)
---
-instance (P p a
-        , P q a
-        , P r a
-        , P s a
-        , P t a
-        , P u a
-        , P v a
-        ) => P '(p,q,r,s,t,u,v) a where
-  type PP '(p,q,r,s,t,u,v) a = (PP p a, PP q a, PP r a, PP s a, PP t a, PP u a, PP v a)
-  eval _ opts a = do
-    let msg = "'(,,,,,,)"
-    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
-    case lr of
-      Left e -> pure e
-      Right (p,q,pp,qq) -> do
-        let hhs0 = [hh pp, hh qq]
-        lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
-        case lr1 of
-          Left e -> pure e
-          Right (r,s,rr,ss) -> do
-            let hhs1 = hhs0 ++ [hh rr, hh ss]
-            lr2 <- runPQ msg (Proxy @t) (Proxy @u) opts a hhs1
-            case lr2 of
-              Left e -> pure e
-              Right (t,u,tt,uu) -> do
-                vv <- eval (Proxy @v) opts a
-                let hhs2 = hhs1 ++ [hh tt, hh uu]
-                pure $ case getValueLR opts msg vv hhs2 of
-                  Left e -> e
-                  Right v ->
-                    let hhs3 = hhs2 ++ [hh vv]
-                    in mkNode opts (PresentT (p,q,r,s,t,u,v)) msg hhs3
-
--- | run the predicates in a promoted 8-tuple
---
--- >>> pz @'(4, Id, "inj", 999, 'LT, 1, 2, 3) "hello"
--- PresentT (4,"hello","inj",999,LT,1,2,3)
---
-instance (P p a
-        , P q a
-        , P r a
-        , P s a
-        , P t a
-        , P u a
-        , P v a
-        , P w a
-        ) => P '(p,q,r,s,t,u,v,w) a where
-  type PP '(p,q,r,s,t,u,v,w) a = (PP p a, PP q a, PP r a, PP s a, PP t a, PP u a, PP v a, PP w a)
-  eval _ opts a = do
-    let msg = "'(,,,,,,,)"
-    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
-    case lr of
-      Left e -> pure e
-      Right (p,q,pp,qq) -> do
-        let hhs0 = [hh pp, hh qq]
-        lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
-        case lr1 of
-          Left e -> pure e
-          Right (r,s,rr,ss) -> do
-            let hhs1 = hhs0 ++ [hh rr, hh ss]
-            lr2 <- runPQ msg (Proxy @t) (Proxy @u) opts a hhs1
-            case lr2 of
-              Left e -> pure e
-              Right (t,u,tt,uu) -> do
-                let hhs2 = hhs1 ++ [hh tt, hh uu]
-                lr3 <- runPQ msg (Proxy @v) (Proxy @w) opts a hhs2
-                pure $ case lr3 of
-                  Left e -> e
-                  Right (v,w,vv,ww) ->
-                     let hhs3 = hhs2 ++ [hh vv, hh ww]
-                     in mkNode opts (PresentT (p,q,r,s,t,u,v,w)) msg hhs3
-
-
--- | extracts the value level representation of the promoted 'Ordering'
---
--- >>> pz @'LT "not used"
--- PresentT LT
---
--- >>> pz @'EQ ()
--- PresentT EQ
-instance GetOrdering cmp => P (cmp :: Ordering) a where
-  type PP cmp a = Ordering
-  eval _ opts _a =
-    let cmp = getOrdering @cmp
-        msg = "'" <> show cmp
-    in pure $ mkNode opts (PresentT cmp) msg []
-
--- | extracts the value level representation of the type level 'Nat'
---
--- >>> pz @123 ()
--- PresentT 123
-instance KnownNat n => P (n :: Nat) a where
-  type PP n a = Int
-  eval _ opts _ =
-    let n = nat @n
-    in pure $ mkNode opts (PresentT n) ("'" <> show n) []
-
--- | extracts the value level representation of the type level '()
---
--- >>> pz @'() ()
--- PresentT ()
-instance P '() a where
-  type PP '() a = ()
-  eval _ opts _ = pure $ mkNode opts (PresentT ()) "'()" []
-
--- the type has to be [a] so we still need type PP '[p] a = [PP p a] to keep the types in line
-
--- | extracts the value level representation of the type level '[]
---
--- >>> pz @'[] False
--- PresentT []
-instance P ('[] :: [k]) a where
-  type PP ('[] :: [k]) a = [a]
-  eval _ opts _ = pure $ mkNode opts (PresentT mempty) "'[]" []
-
--- | runs each predicate in turn from the promoted list
---
--- >>> pz @'[1, 2, 3] 999
--- PresentT [1,2,3]
---
--- >>> pz @'[W 1, W 2, W 3, Id] 999
--- PresentT [1,2,3,999]
---
-instance ( Show (PP p a)
-         , Show a
-         , P p a
-         ) => P '[p] a where
-  type PP '[p] a = [PP p a]
-  eval _ opts a = do
-    pp <- eval (Proxy @p) opts a
-    let msg0 = ""
-    pure $ case getValueLR opts msg0 pp [] of
-       Left e -> e
-       Right b -> mkNode opts (PresentT [b]) ("'" <> showL opts [b] <> showVerbose opts " | " a) [hh pp]
-
-instance (Show (PP p a)
-        , Show a
-        , P (p1 ': ps) a
-        , PP (p1 ': ps) a ~ [PP p1 a]
-        , P p a
-        , PP p a ~ PP p1 a
-        ) => P (p ': p1 ': ps) a where
-  type PP (p ': p1 ': ps) a = [PP p a]
-  eval _ opts a = do
-    let msg0 = "'(p':q)"
-    pp <- eval (Proxy @p) opts a
-    case getValueLR opts msg0 pp [] of
-      Left e -> pure e
-      Right p -> do
-        qq <- eval (Proxy @(p1 ': ps)) opts a
-        pure $ case getValueLR opts msg0 qq [hh pp] of
-          Left e -> e
-          Right q ->
-            let ret = p:q
-            -- no gap between ' and ret!
-            in mkNode opts (PresentT ret) ("'" <> showL opts ret <> litVerbose opts " " (topMessage pp) <> showVerbose opts " | " a) ([hh pp | isVerbose opts] <> [hh qq])
-
--- | extracts the \'a\' from type level \'Maybe a\' if the value exists
---
--- >>> pz @('Just Id) (Just 123)
--- PresentT 123
---
--- >>> pz @('Just Id) (Just True)
--- PresentT True
---
--- >>> pz @('Just Id) Nothing
--- FailT "'Just found Nothing"
---
-instance (Show (PP p a)
-        , P p a
-        , Show a
-        ) => P ('Just p) (Maybe a) where
-  type PP ('Just p) (Maybe a) = PP p a
-  eval _ opts ma = do
-    let msg0 = "'Just"
-    case ma of
-      Just a -> do
-        pp <- eval (Proxy @p) opts a
-        pure $ case getValueLR opts msg0 pp [] of
-          Left e -> e
-          Right b -> mkNode opts (PresentT b) (show01 opts msg0 b ma) [hh pp]
-      Nothing -> pure $ mkNode opts (FailT (msg0 <> " found Nothing")) "" []
-
--- | expects Nothing otherwise it fails
--- if the value is Nothing then it returns \'Proxy a\' as this provides type information
---
--- >>> pz @'Nothing Nothing
--- PresentT Proxy
---
--- >>> pz @'Nothing (Just True)
--- FailT "'Nothing found Just"
---
-instance P 'Nothing (Maybe a) where
-  type PP 'Nothing (Maybe a) = Proxy a -- () gives us less information
-  eval _ opts ma =
-    let msg0 = "'Nothing"
-    in pure $ case ma of
-         Nothing -> mkNode opts (PresentT Proxy) msg0 []
-         Just _ -> mkNode opts (FailT (msg0 <> " found Just")) "" []
-
--- omitted Show x so we can have less ambiguity
--- | extracts the \'a\' from type level \'Either a b\' if the value exists
---
--- >>> pz @('Left Id) (Left 123)
--- PresentT 123
---
--- >>> pz @('Left Id) (Right "aaa")
--- FailT "'Left found Right"
---
-instance (Show a
-        , Show (PP p a)
-        , P p a
-        ) => P ('Left p) (Either a x) where
-  type PP ('Left p) (Either a x) = PP p a
-  eval _ opts lr =
-    let msg0 = "'Left"
-    in case lr of
-         Right _ -> pure $ mkNode opts (FailT (msg0 <> " found Right")) "" []
-         Left a -> do
-            pp <- eval (Proxy @p) opts a
-            pure $ case getValueLR opts msg0 pp [] of
-                 Left e -> e
-                 Right b -> mkNode opts (_tBool pp) (show01' opts msg0 b "Left " a) [hh pp]
-
--- | extracts the \'b\' from type level \'Either a b\' if the value exists
---
--- >>> pz @('Right Id) (Right 123)
--- PresentT 123
---
--- >>> pz @('Right Id) (Left "aaa")
--- FailT "'Right found Left"
---
-instance (Show a
-        , Show (PP p a)
-        , P p a
-        ) => P ('Right p) (Either x a) where
-  type PP ('Right p) (Either x a) = PP p a
-  eval _ opts lr = do
-    let msg0 = "'Right"
-    case lr of
-         Left _ -> pure $ mkNode opts (FailT (msg0 <> " found Left")) "" []
-         Right a -> do
-            pp <- eval (Proxy @p) opts a
-            pure $ case getValueLR opts msg0 pp [] of
-                 Left e -> e
-                 Right b -> mkNode opts (_tBool pp) (show01' opts msg0 b "Right " a) [hh pp]
-
--- removed Show x: else ambiguity errors in TestPredicate
-
--- | extracts the \'a\' from type level \'These a b\' if the value exists
---
--- >>> pz @('This Id) (This 123)
--- PresentT 123
---
--- >>> pz @('This Id) (That "aaa")
--- FailT "'This found That"
---
--- >>> pz @('This Id) (These 999 "aaa")
--- FailT "'This found These"
---
-instance (Show a
-        , Show (PP p a)
-        , P p a
-        ) => P ('This p) (These a x) where
-  type PP ('This p) (These a x) = PP p a
-  eval _ opts th = do
-    let msg0 = "'This"
-    case th of
-         This a -> do
-            pp <- eval (Proxy @p) opts a
-            pure $ case getValueLR opts msg0 pp [] of
-                 Left e -> e
-                 Right b -> mkNode opts (_tBool pp) (show01' opts msg0 b "This " a) [hh pp]
-         _ -> pure $ mkNode opts (FailT (msg0 <> " found " <> showThese th)) "" []
-
--- | extracts the \'b\' from type level \'These a b\' if the value exists
---
--- >>> pz @('That Id) (That 123)
--- PresentT 123
---
--- >>> pz @('That Id) (This "aaa")
--- FailT "'That found This"
---
--- >>> pz @('That Id) (These 44 "aaa")
--- FailT "'That found These"
---
-instance (Show a
-        , Show (PP p a)
-        , P p a
-        ) => P ('That p) (These x a) where
-  type PP ('That p) (These x a) = PP p a
-  eval _ opts th = do
-    let msg0 = "'That"
-    case th of
-         That a -> do
-            pp <- eval (Proxy @p) opts a
-            pure $ case getValueLR opts msg0 pp [] of
-                 Left e -> e
-                 Right b -> mkNode opts (_tBool pp) (show01' opts msg0 b "That " a) [hh pp]
-         _ -> pure $ mkNode opts (FailT (msg0 <> " found " <> showThese th)) "" []
-
-
--- | extracts the (a,b) from type level 'These a b' if the value exists
---
--- >>> pz @('These Id Id) (These 123 "abc")
--- PresentT (123,"abc")
---
--- >>> pz @('These Id 5) (These 123 "abcde")
--- PresentT (123,5)
---
--- >>> pz @('These Id Id) (This "aaa")
--- FailT "'These found This"
---
--- >>> pz @('These Id Id) (That "aaa")
--- FailT "'These found That"
---
-instance (Show a
-        , Show b
-        , P p a
-        , P q b
-        , Show (PP p a)
-        , Show (PP q b)
-        ) => P ('These p q) (These a b) where
-  type PP ('These p q) (These a b) = (PP p a, PP q b)
-  eval _ opts th = do
-    let msg0 = "'These"
-    case th of
-         These a b -> do
-            pp <- eval (Proxy @p) opts a
-            case getValueLR opts msg0 pp [] of
-               Left e -> pure e
-               Right p -> do
-                 qq <- eval (Proxy @q) opts b
-                 pure $ case getValueLR opts (msg0 <> " q failed p=" <> showL opts p) qq [hh pp] of
-                    Left e -> e
-                    Right q ->
-                      let ret =(p,q)
-                      in  mkNode opts (PresentT ret) (show01 opts msg0 ret (These a b)) [hh pp, hh qq]
-         _ -> pure $ mkNode opts (FailT (msg0 <> " found " <> showThese th)) "" []
-
--- | converts the value to the corresponding 'Proxy'
---
--- >>> pz @'Proxy 'x'
--- PresentT Proxy
---
-instance Show a => P 'Proxy a where
-  type PP 'Proxy a = Proxy a
-  eval _ opts a =
-    let b = Proxy @a
-    in pure $ mkNode opts (PresentT b) ("'Proxy" <> showVerbose opts " | " a) []
-
--- | typelevel 'BoolT'
---
--- >>> pz @'TrueT ()
--- TrueT
---
--- >>> pz @'FalseT ()
--- FalseT
---
--- >>> pz @('PresentT 123) ()
--- PresentT False
---
--- >>> pz @('FailT '[]) ()
--- FailT "'FailT _"
---
-instance GetBoolT x b => P (b :: BoolT x) a where
-  type PP b a = Bool
-  eval _ opts _ = do
-    let ret = getBoolT @x @b
-    pure $ case ret of
-      Left b -> mkNodeB opts b (if b then "'TrueT" else "'FalseT") []
-      Right True -> mkNode opts (PresentT False) "'PresentT _" []
-      Right False -> mkNode opts (FailT "'FailT _") "BoolT" []
-
-pan, panv, pa, pu, pl, pz, pab, pub, pav, puv
-  :: forall p a
-  . ( Show (PP p a)
-    , P p a
-    ) => a
-      -> IO (BoolT (PP p a))
--- | skips the evaluation tree and just displays the end result
-pz = run @OZ @p
--- | same as 'pz' but adds context to the end result
-pl = run @OL @p
--- | displays the evaluation tree in plain text without colors
-pan = run @OAN @p
--- | displays the evaluation tree in plain text without colors and verbose
-panv = run @OANV @p
--- | displays the evaluation tree using colors without background colors
-pa = run @OA @p
--- | displays the evaluation tree using background colors
-pab = run @OAB @p
--- | 'pa' and verbose
-pav = run @OAV @p
--- | display the evaluation tree using unicode and colors
--- @
---   pu @'(Id, "abc", 123) [1..4]
--- @
-pu = run @OU @p
--- | displays the evaluation tree using unicode and colors with background colors
-pub = run @OUB @p
--- | 'pu' and verbose
-puv = run @OUV @p
-
--- | evaluate a typelevel expression (use type applications to pass in the options and the expression)
---
--- >>> run @OZ @Id 123
--- PresentT 123
---
--- >>> run @('OMsg "field1" ':# OL) @('Left Id) (Right 123)
--- field1 >>> Error 'Left found Right
--- FailT "'Left found Right"
---
--- >>> run @(OptTT '[ 'OMsg "test", OU, 'OEmpty, OL, 'OMsg "field2"]) @('FailT '[]) ()
--- test | field2 >>> Error 'FailT _ (BoolT)
--- FailT "'FailT _"
---
-run :: forall opts p a
-        . ( OptTC opts
-          , Show (PP p a)
-          , P p a)
-        => a
-        -> IO (BoolT (PP p a))
-run a = do
-  let opts = getOptT @opts
-  pp <- eval (Proxy @p) opts a
-  let r = pp ^. tBool
-  putStr $ prtTree opts pp
-  return r
-
--- | run expression with multiple options in a list
---
--- >>> runs @'[ OL, 'OMsg "field2"] @'( 'True, 'False) ()
--- field2 >>> Present (True,False) ('(,))
--- PresentT (True,False)
---
--- >>> runs @'[ 'OMsg "test", OU, 'OEmpty, OL, 'OMsg "field2"] @('FailT '[]) ()
--- test | field2 >>> Error 'FailT _ (BoolT)
--- FailT "'FailT _"
---
-runs :: forall optss p a
-        . ( OptTC (OptTT optss)
-          , Show (PP p a)
-          , P p a)
-        => a
-        -> IO (BoolT (PP p a))
-runs = run @(OptTT optss) @p
-
-
-prtTree :: Show x => POpts -> TT x -> String
-prtTree opts pp =
-  let r = pp ^. tBool
-  in case oDebug opts of
-       DZero -> ""
-       DLite ->
-             formatOMsg opts " >>> "
-          <> colorBoolT opts r
-          <> " "
-          <> topMessage pp
-          <> "\n"
-       _ -> formatOMsg opts "\n"
-         <> prtTreePure opts (fromTT pp)
-
-runPQ :: ( P p a
-         , P q a
-         , MonadEval m)
-   => String
-   -> proxy1 p
-   -> proxy2 q
-   -> POpts
-   -> a
-   -> [Holder]
-   -> m (Either (TT x) (PP p a, PP q a, TT (PP p a), TT (PP q a)))
-runPQ msg0 proxyp proxyq opts a hhs = do
-    pp <- eval proxyp opts a
-    case getValueLR opts msg0 pp hhs of
-      Left e -> pure $ Left e
-      Right p -> do
-         qq <- eval proxyq opts a
-         pure $ case getValueLR opts msg0 qq (hhs <> [hh pp]) of
-           Left e -> Left e
-           Right q -> Right (p, q, pp, qq)
-
-runPQBool :: ( P p a
-             , PP p a ~ Bool
-             , P q a
-             , PP q a ~ Bool, MonadEval m)
-   => String
-   -> proxy1 p
-   -> proxy2 q
-   -> POpts
-   -> a
-   -> [Holder]
-   -> m (Either (TT x) (PP p a, PP q a, TT (PP p a), TT (PP q a)))
-runPQBool msg0 proxyp proxyq opts a hhs = do
-    pp <- evalBool proxyp opts a
-    case getValueLR opts msg0 pp hhs of
-      Left e -> pure $ Left e
-      Right p -> do
-         qq <- evalBool proxyq opts a
-         pure $ case getValueLR opts msg0 qq (hhs <> [hh pp]) of
-           Left e -> Left e
-           Right q -> Right (p, q, pp, qq)
-
-evalBoolHide :: forall m p a proxy
-  . (MonadEval m, P p a, PP p a ~ Bool)
-  => proxy p
-  -> POpts
-  -> a
-  -> m (TT (PP p a))
-evalBoolHide _ opts =
-  if isVerbose opts then evalBool (Proxy @p) opts
-  else evalBool (Proxy @(Hide p)) opts
-
-evalHide :: forall m p a proxy
-  . (MonadEval m, P p a)
-  => proxy p
-  -> POpts
-  -> a
-  -> m (TT (PP p a))
-evalHide _ opts =
-  if isVerbose opts then eval (Proxy @p) opts
-  else eval (Proxy @(Hide p)) opts+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE NoStarIsType #-}
+{- |
+     Dsl for evaluating and displaying type level expressions
+-}
+module Predicate.Core (
+
+ -- ** basic types
+    Id
+  , IdT
+  , I
+  , W
+  , Msg
+  , MsgI
+  , Hide
+  , Width
+  , Hole
+  , Unproxy
+  , Len
+  , Length
+  , Map
+  , Do
+  , Pure
+  , Coerce
+  , OneP
+  , type (>>)
+
+  -- ** tree evaluation
+  , pan
+  , panv
+  , pa
+  , pu
+  , pab
+  , pub
+  , pav
+  , puv
+  , pl
+  , pz
+  , run
+  , runs
+
+  , P(..)
+
+  -- ** evaluation methods
+  , runPQ
+  , runPQBool
+  , evalBool
+  , evalBoolHide
+  , evalHide
+  , evalQuick
+
+ -- ** wrap, unwrap expressions
+  , Unwrap
+  , Wrap
+  , Wrap'
+
+ -- ** failure expressions
+  , Fail
+  , Failp
+  , Failt
+  , FailS
+
+ -- ** tuple expressions
+  , Fst
+  , Snd
+  , Thd
+  , L1
+  , L2
+  , L3
+  , L4
+  , L5
+  , L6
+
+  -- ** boolean expressions
+  , type (&&)
+  , type (&&~)
+  , type (||)
+  , type (||~)
+  , type (~>)
+  , Not
+  , Between
+  , All
+  , Any
+  , IdBool
+
+ -- ** miscellaneous
+  , type (<..>)
+  , type (<<)
+  , Swap
+  , SwapC(..)
+  , type ($)
+  , type (&)
+
+  ) where
+import Predicate.Util
+import qualified GHC.TypeLits as GL
+import GHC.TypeLits (Symbol,Nat,KnownSymbol,KnownNat)
+import Control.Lens -- ((&), (^.), (.~))
+import Data.Foldable (toList)
+import Data.Proxy
+import Data.Typeable
+import Data.Kind (Type)
+import Data.These (These(..))
+import Control.Monad
+import Data.List
+import Data.Coerce
+-- $setup
+-- >>> :set -XDataKinds
+-- >>> :set -XTypeApplications
+-- >>> :set -XTypeOperators
+-- >>> import Predicate.Prelude
+-- >>> import qualified Data.Semigroup as SG
+-- >>> import Data.Time
+
+-- | This is the core class. Each instance of this class can be combined into a dsl using 'Predicate.Core.>>'
+class P p a where
+  type PP (p :: k) a :: Type -- PP is the output type
+  eval :: MonadEval m
+     => proxy p -- ^ proxy for the expression
+     -> POpts  -- ^ display options
+     -> a      -- ^ value
+     -> m (TT (PP p a)) -- ^ returns a tree of results
+
+-- | A specialised form of 'eval' that works only on predicates
+evalBool :: ( MonadEval m
+            , P p a
+            , PP p a ~ Bool
+            ) => proxy p
+              -> POpts
+              -> a
+              -> m (TT (PP p a))
+evalBool p opts a = fixBoolT <$> eval p opts a
+
+evalQuick :: forall p i . P p i => i -> Either String (PP p i)
+evalQuick i = getValLRFromTT (runIdentity (eval (Proxy @p) (getOptT @OL) i))
+
+-- | identity function without show instance of 'Id'
+--
+-- >>> pz @I 23
+-- PresentT 23
+--
+data I
+instance P I a where
+  type PP I a = a
+  eval _ opts a =
+    let msg0 = "I"
+    in pure $ mkNode opts (PresentT a) msg0 []
+
+
+-- | identity function
+--
+-- >>> pz @Id 23
+-- PresentT 23
+--
+data Id
+instance Show a => P Id a where
+  type PP Id a = a
+  eval _ opts a =
+    let msg0 = "Id"
+    in pure $ mkNode opts (PresentT a) (msg0 <> " " <> showL opts a) []
+
+-- | identity function that also displays the type information for debugging
+--
+-- >>> pz @IdT 23
+-- PresentT 23
+data IdT
+instance ( Typeable a
+         , Show a
+         ) => P IdT a where
+  type PP IdT a = a
+  eval _ opts a =
+    let msg0 = "IdT(" <> t <> ")"
+        t = showT @a
+    in pure $ mkNode opts (PresentT a) (msg0 <> " " <> showL opts a) []
+
+-- | transparent predicate wrapper to make k of kind 'Type' so it can be in a promoted list (cant mix kinds) see 'Predicate.Core.Do'
+--
+-- >>> pz @'[W 123, Id] 99
+-- PresentT [123,99]
+--
+-- >>> pz @'[W "abc", W "def", Id, Id] "ghi"
+-- PresentT ["abc","def","ghi","ghi"]
+--
+data W (p :: k)
+instance P p a => P (W p) a where
+  type PP (W p) a = PP p a
+  eval _ = eval (Proxy @(MsgI "W " p))
+
+-- | add a message to give more context to the evaluation tree
+--
+-- >>> pan @(Msg "[somemessage]" Id) 999
+-- P [somemessage] Id 999
+-- PresentT 999
+--
+-- >>> pan @(Msg Id 999) "info message:"
+-- P info message: '999
+-- PresentT 999
+--
+data Msg prt p
+
+instance (P prt a
+        , PP prt a ~ String
+        , P p a
+        ) => P (Msg prt p) a where
+  type PP (Msg prt p) a = PP p a
+  eval _ opts a = do
+    pp <- eval (Proxy @prt) opts a
+    case getValueLR opts "Msg" pp [] of
+         Left e -> pure e
+         Right msg -> prefixMsg (setOtherEffects opts msg <> " ") <$> eval (Proxy @p) opts a
+
+-- | add a message to give more context to the evaluation tree
+--
+-- >>> pan @(MsgI "[somemessage] " Id) 999
+-- P [somemessage] Id 999
+-- PresentT 999
+--
+-- >>> pan @(MsgI Id 999) "info message:"
+-- P info message:'999
+-- PresentT 999
+--
+data MsgI prt p
+
+instance (P prt a
+        , PP prt a ~ String
+        , P p a
+        ) => P (MsgI prt p) a where
+  type PP (MsgI prt p) a = PP p a
+  eval _ opts a = do
+    pp <- eval (Proxy @prt) opts a
+    case getValueLR opts "MsgI" pp [] of
+         Left e -> pure e
+         Right msg -> prefixMsg msg <$> eval (Proxy @p) opts a
+
+-- | run the expression \'p\' but remove the subtrees
+data Hide p
+-- type H p = Hide p -- doesnt work with %   -- unsaturated!
+
+instance P p x => P (Hide p) x where
+  type PP (Hide p) x = PP p x
+  eval _ opts x = do
+      tt <- eval (Proxy @p) opts x
+      pure $ tt & tForest .~ []
+
+data Hole (t :: Type)
+
+-- | Acts as a proxy in this dsl where you can explicitly set the Type.
+--
+--  It is passed around as an argument to help the type checker when needed.
+--
+instance Typeable t => P (Hole t) a where
+  type PP (Hole t) a = t -- can only be Type not Type -> Type (can use Proxy but then we go down the rabbithole)
+  eval _ opts _a =
+    let msg0 = "Hole(" <> showT @t <> ")"
+    in pure $ mkNode opts (FailT msg0) "you probably meant to get access to the type of PP only and not evaluate" []
+
+-- | override the display width for the expression \'p\'
+data Width (n :: Nat) p
+
+instance (KnownNat n
+        , P p a
+        ) => P (Width n p) a where
+  type PP (Width n p) a = PP p a
+  eval _ opts a = do
+    let opts' = opts { oWidth = nat @n }
+    eval (Proxy @p) opts' a
+
+-- | 'const' () function
+--
+-- >>> pz @() "Asf"
+-- PresentT ()
+--
+instance P () a where
+  type PP () a = ()
+  eval _ opts _ =
+    let msg0 = "()"
+    in pure $ mkNode opts (PresentT ()) msg0 []
+
+instance P (Proxy t) a where
+  type PP (Proxy t) a = Proxy t
+  eval _ opts _ =
+    let msg0 = "Proxy"
+    in pure $ mkNode opts (PresentT Proxy) msg0 []
+
+-- Start non-Type kinds
+-----------------------
+
+-- | pulls the type level 'Bool' to the value level
+--
+-- >>> pz @'True "not used"
+-- TrueT
+--
+-- >>> pz @'False ()
+-- FalseT
+instance GetBool b => P (b :: Bool) a where
+  type PP b a = Bool
+  eval _ opts _ =
+    let b = getBool @b
+    in pure $ mkNodeB opts b ("'" <> show b) []
+
+-- | pulls the type level 'GHC.TypeLits.Symbol' to the value level as a 'GHC.Base.String'
+--
+-- >>> pz @"hello world" ()
+-- PresentT "hello world"
+instance KnownSymbol s => P (s :: Symbol) a where
+  type PP s a = String
+  eval _ opts _ =
+    let s = symb @s
+    in pure $ mkNode opts (PresentT s) ("'" <> litL opts ("\"" <> s <> "\"")) []
+
+-- | run the predicates in a promoted 2-tuple; similar to 'Control.Arrow.&&&'
+--
+-- >>> pz @'(Id, 4) "hello"
+-- PresentT ("hello",4)
+--
+instance ( P p a
+         , P q a
+         , Show (PP p a)
+         , Show (PP q a)
+         ) => P '(p,q) a where
+  type PP '(p,q) a = (PP p a, PP q a)
+  eval _ opts a = do
+    let msg = "'(,)"
+    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
+    pure $ case lr of
+       Left e -> e
+       Right (p,q,pp,qq) ->
+--         mkNode opts (PresentT (p,q)) msg [hh pp, hh qq]
+         mkNode opts (PresentT (p,q)) ("'(" <> showL opts p <> "," <> showL opts q <> ")") [hh pp, hh qq]
+
+-- | run the predicates in a promoted 3-tuple
+--
+-- >>> pz @'(4, Id, "goodbye") "hello"
+-- PresentT (4,"hello","goodbye")
+--
+-- >>> pan @'( 'True, 'False, 123) True
+-- P '(,,)
+-- |
+-- +- True 'True
+-- |
+-- +- False 'False
+-- |
+-- `- P '123
+-- PresentT (True,False,123)
+--
+instance (P p a
+        , P q a
+        , P r a
+        ) => P '(p,q,r) a where
+  type PP '(p,q,r) a = (PP p a, PP q a, PP r a)
+  eval _ opts a = do
+    let msg = "'(,,)"
+    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
+    case lr of
+      Left e -> pure e
+      Right (p,q,pp,qq) -> do
+         let hhs0 = [hh pp, hh qq]
+         rr <- eval (Proxy @r) opts a
+         pure $ case getValueLR opts msg rr hhs0 of
+           Left e -> e
+           Right r ->
+             let hhs1 = hhs0 <> [hh rr]
+             in mkNode opts (PresentT (p,q,r)) msg hhs1
+
+-- | run the predicates in a promoted 4-tuple
+--
+-- >>> pz @'(4, Id, "inj", 999) "hello"
+-- PresentT (4,"hello","inj",999)
+--
+instance (P p a
+        , P q a
+        , P r a
+        , P s a
+        ) => P '(p,q,r,s) a where
+  type PP '(p,q,r,s) a = (PP p a, PP q a, PP r a, PP s a)
+  eval _ opts a = do
+    let msg = "'(,,,)"
+    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
+    case lr of
+      Left e -> pure e
+      Right (p,q,pp,qq) -> do
+        let hhs0 = [hh pp, hh qq]
+        lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
+        pure $ case lr1 of
+          Left e -> e
+          Right (r,s,rr,ss) ->
+            let hhs1 = hhs0 ++ [hh rr, hh ss]
+            in mkNode opts (PresentT (p,q,r,s)) msg hhs1
+
+-- | run the predicates in a promoted 5-tuple
+--
+-- >>> pz @'(4, Id, "inj", 999, 'LT) "hello"
+-- PresentT (4,"hello","inj",999,LT)
+--
+instance (P p a
+        , P q a
+        , P r a
+        , P s a
+        , P t a
+        ) => P '(p,q,r,s,t) a where
+  type PP '(p,q,r,s,t) a = (PP p a, PP q a, PP r a, PP s a, PP t a)
+  eval _ opts a = do
+    let msg = "'(,,,,)"
+    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
+    case lr of
+      Left e -> pure e
+      Right (p,q,pp,qq) -> do
+        let hhs0 = [hh pp, hh qq]
+        lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
+        case lr1 of
+          Left e -> pure e
+          Right (r,s,rr,ss) -> do
+            let hhs1 = hhs0 ++ [hh rr, hh ss]
+            tt <- eval (Proxy @t) opts a
+            pure $ case getValueLR opts msg tt hhs1 of
+              Left e -> e
+              Right t ->
+                let hhs2 = hhs1 <> [hh tt]
+                in mkNode opts (PresentT (p,q,r,s,t)) msg hhs2
+
+-- | run the predicates in a promoted 6-tuple
+--
+-- >>> pz @'(4, Id, "inj", 999, 'LT, 1) "hello"
+-- PresentT (4,"hello","inj",999,LT,1)
+--
+instance (P p a
+        , P q a
+        , P r a
+        , P s a
+        , P t a
+        , P u a
+        ) => P '(p,q,r,s,t,u) a where
+  type PP '(p,q,r,s,t,u) a = (PP p a, PP q a, PP r a, PP s a, PP t a, PP u a)
+  eval _ opts a = do
+    let msg = "'(,,,,,)"
+    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
+    case lr of
+      Left e -> pure e
+      Right (p,q,pp,qq) -> do
+        let hhs0 = [hh pp, hh qq]
+        lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
+        case lr1 of
+          Left e -> pure e
+          Right (r,s,rr,ss) -> do
+            let hhs1 = hhs0 ++ [hh rr, hh ss]
+            lr2 <- runPQ msg (Proxy @t) (Proxy @u) opts a hhs1
+            pure $ case lr2 of
+              Left e -> e
+              Right (t,u,tt,uu) ->
+                let hhs2 = hhs1 ++ [hh tt, hh uu]
+                in mkNode opts (PresentT (p,q,r,s,t,u)) msg hhs2
+
+-- | run the predicates in a promoted 7-tuple
+--
+-- >>> pz @'(4, Id, "inj", 999, 'LT, 1, 2) "hello"
+-- PresentT (4,"hello","inj",999,LT,1,2)
+--
+instance (P p a
+        , P q a
+        , P r a
+        , P s a
+        , P t a
+        , P u a
+        , P v a
+        ) => P '(p,q,r,s,t,u,v) a where
+  type PP '(p,q,r,s,t,u,v) a = (PP p a, PP q a, PP r a, PP s a, PP t a, PP u a, PP v a)
+  eval _ opts a = do
+    let msg = "'(,,,,,,)"
+    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
+    case lr of
+      Left e -> pure e
+      Right (p,q,pp,qq) -> do
+        let hhs0 = [hh pp, hh qq]
+        lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
+        case lr1 of
+          Left e -> pure e
+          Right (r,s,rr,ss) -> do
+            let hhs1 = hhs0 ++ [hh rr, hh ss]
+            lr2 <- runPQ msg (Proxy @t) (Proxy @u) opts a hhs1
+            case lr2 of
+              Left e -> pure e
+              Right (t,u,tt,uu) -> do
+                vv <- eval (Proxy @v) opts a
+                let hhs2 = hhs1 ++ [hh tt, hh uu]
+                pure $ case getValueLR opts msg vv hhs2 of
+                  Left e -> e
+                  Right v ->
+                    let hhs3 = hhs2 ++ [hh vv]
+                    in mkNode opts (PresentT (p,q,r,s,t,u,v)) msg hhs3
+
+-- | run the predicates in a promoted 8-tuple
+--
+-- >>> pz @'(4, Id, "inj", 999, 'LT, 1, 2, 3) "hello"
+-- PresentT (4,"hello","inj",999,LT,1,2,3)
+--
+instance (P p a
+        , P q a
+        , P r a
+        , P s a
+        , P t a
+        , P u a
+        , P v a
+        , P w a
+        ) => P '(p,q,r,s,t,u,v,w) a where
+  type PP '(p,q,r,s,t,u,v,w) a = (PP p a, PP q a, PP r a, PP s a, PP t a, PP u a, PP v a, PP w a)
+  eval _ opts a = do
+    let msg = "'(,,,,,,,)"
+    lr <- runPQ msg (Proxy @p) (Proxy @q) opts a []
+    case lr of
+      Left e -> pure e
+      Right (p,q,pp,qq) -> do
+        let hhs0 = [hh pp, hh qq]
+        lr1 <- runPQ msg (Proxy @r) (Proxy @s) opts a hhs0
+        case lr1 of
+          Left e -> pure e
+          Right (r,s,rr,ss) -> do
+            let hhs1 = hhs0 ++ [hh rr, hh ss]
+            lr2 <- runPQ msg (Proxy @t) (Proxy @u) opts a hhs1
+            case lr2 of
+              Left e -> pure e
+              Right (t,u,tt,uu) -> do
+                let hhs2 = hhs1 ++ [hh tt, hh uu]
+                lr3 <- runPQ msg (Proxy @v) (Proxy @w) opts a hhs2
+                pure $ case lr3 of
+                  Left e -> e
+                  Right (v,w,vv,ww) ->
+                     let hhs3 = hhs2 ++ [hh vv, hh ww]
+                     in mkNode opts (PresentT (p,q,r,s,t,u,v,w)) msg hhs3
+
+
+-- | extracts the value level representation of the promoted 'Ordering'
+--
+-- >>> pz @'LT "not used"
+-- PresentT LT
+--
+-- >>> pz @'EQ ()
+-- PresentT EQ
+instance GetOrdering cmp => P (cmp :: Ordering) a where
+  type PP cmp a = Ordering
+  eval _ opts _a =
+    let cmp = getOrdering @cmp
+        msg = "'" <> show cmp
+    in pure $ mkNode opts (PresentT cmp) msg []
+
+-- | extracts the value level representation of the type level 'Nat'
+--
+-- >>> pz @123 ()
+-- PresentT 123
+--
+instance KnownNat n => P (n :: Nat) a where
+  type PP n a = Int
+  eval _ opts _ =
+    let n = nat @n
+    in pure $ mkNode opts (PresentT n) ("'" <> show n) []
+
+-- | extracts the value level representation of the type level '()
+--
+-- >>> pz @'() ()
+-- PresentT ()
+instance P '() a where
+  type PP '() a = ()
+  eval _ opts _ = pure $ mkNode opts (PresentT ()) "'()" []
+
+-- the type has to be [a] so we still need type PP '[p] a = [PP p a] to keep the types in line
+
+-- | extracts the value level representation of the type level '[]
+--
+-- >>> pz @'[] False
+-- PresentT []
+instance P ('[] :: [k]) a where
+  type PP ('[] :: [k]) a = [a]
+  eval _ opts _ = pure $ mkNode opts (PresentT mempty) "'[]" []
+
+-- | runs each predicate in turn from the promoted list
+--
+-- >>> pz @'[1, 2, 3] 999
+-- PresentT [1,2,3]
+--
+-- >>> pz @'[W 1, W 2, W 3, Id] 999
+-- PresentT [1,2,3,999]
+--
+instance ( Show (PP p a)
+         , Show a
+         , P p a
+         ) => P '[p] a where
+  type PP '[p] a = [PP p a]
+  eval _ opts a = do
+    pp <- eval (Proxy @p) opts a
+    let msg0 = ""
+    pure $ case getValueLR opts msg0 pp [] of
+       Left e -> e
+       Right b -> mkNode opts (PresentT [b]) ("'" <> showL opts [b] <> showVerbose opts " | " a) [hh pp]
+
+instance (Show (PP p a)
+        , Show a
+        , P (p1 ': ps) a
+        , PP (p1 ': ps) a ~ [PP p1 a]
+        , P p a
+        , PP p a ~ PP p1 a
+        ) => P (p ': p1 ': ps) a where
+  type PP (p ': p1 ': ps) a = [PP p a]
+  eval _ opts a = do
+    let msg0 = "'(p':q)"
+    pp <- eval (Proxy @p) opts a
+    case getValueLR opts msg0 pp [] of
+      Left e -> pure e
+      Right p -> do
+        qq <- eval (Proxy @(p1 ': ps)) opts a
+        pure $ case getValueLR opts msg0 qq [hh pp] of
+          Left e -> e
+          Right q ->
+            let ret = p:q
+            -- no gap between ' and ret!
+            in mkNode opts (PresentT ret) ("'" <> showL opts ret <> litVerbose opts " " (topMessage pp) <> showVerbose opts " | " a) ([hh pp | isVerbose opts] <> [hh qq])
+
+-- | tries to extract @a@ from @Maybe a@ otherwise it fails: similar to 'Data.Maybe.fromJust'
+--
+-- >>> pz @('Just Id) (Just "abc")
+-- PresentT "abc"
+--
+-- >>> pl @('Just Id >> Id) (Just 123)
+-- Present 123 ((>>) 123 | {Id 123})
+-- PresentT 123
+--
+-- >>> pl @('Just Id) (Just [1,2,3])
+-- Present [1,2,3] ('Just [1,2,3] | Just [1,2,3])
+-- PresentT [1,2,3]
+--
+-- >>> pl @('Just Id) (Just 10)
+-- Present 10 ('Just 10 | Just 10)
+-- PresentT 10
+--
+-- >>> pl @('Just Id) Nothing
+-- Error 'Just(empty)
+-- FailT "'Just(empty)"
+--
+-- >>> pz @('Just (Fst Id)) (Just 123,'x')
+-- PresentT 123
+--
+instance (Show a
+        , PP p x ~ Maybe a
+        , P p x
+        ) => P ('Just p) x where
+  type PP ('Just p) x = MaybeT (PP p x)
+  eval _ opts x = do
+    let msg0 = "'Just"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        case p of
+          Nothing -> mkNode opts (FailT (msg0 <> "(empty)")) "" [hh pp]
+          Just d -> mkNode opts (PresentT d) (show01 opts msg0 d p) [hh pp]
+
+-- | expects Nothing otherwise it fails
+--   if the value is Nothing then it returns \'Proxy a\' as this provides type information
+--
+-- >>> pz @'Nothing Nothing
+-- PresentT Proxy
+--
+-- >>> pz @'Nothing (Just True)
+-- FailT "'Nothing found Just"
+--
+instance P 'Nothing (Maybe a) where
+  type PP 'Nothing (Maybe a) = Proxy a -- () gives us less information
+  eval _ opts ma =
+    let msg0 = "'Nothing"
+    in pure $ case ma of
+         Nothing -> mkNode opts (PresentT Proxy) msg0 []
+         Just _ -> mkNode opts (FailT (msg0 <> " found Just")) "" []
+
+-- omitted Show x so we can have less ambiguity
+-- | extracts the \'a\' from type level \'Either a b\' if the value exists
+--
+-- >>> pz @('Left Id) (Left 123)
+-- PresentT 123
+--
+-- >>> pz @('Left (Snd Id)) ('x', Left 123)
+-- PresentT 123
+--
+-- >>> pz @('Left Id) (Right "aaa")
+-- FailT "'Left found Right"
+--
+-- >>> pl @('Left Id) (Left 123)
+-- Present 123 (Left)
+-- PresentT 123
+--
+-- >>> pl @('Left Id) (Right 123)
+-- Error 'Left found Right
+-- FailT "'Left found Right"
+--
+
+instance ( PP p x ~ Either a b
+         , P p x)
+    => P ('Left p) x where
+  type PP ('Left p) x = LeftT (PP p x)
+  eval _ opts x = do
+    let msg0 = "'Left"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        case p of
+          Left a -> mkNode opts (PresentT a) "Left" [hh pp]
+          Right _b -> mkNode opts (FailT (msg0 <> " found Right")) "" [hh pp]
+
+-- | extracts the \'b\' from type level \'Either a b\' if the value exists
+--
+-- >>> pl @('Right Id) (Right 123)
+-- Present 123 (Right)
+-- PresentT 123
+--
+-- >>> pz @('Right Id >> Snd Id) (Right ('x',123))
+-- PresentT 123
+--
+-- >>> pz @('Right Id) (Left "aaa")
+-- FailT "'Right found Left"
+--
+-- >>> pl @('Right Id) (Left 123)
+-- Error 'Right found Left
+-- FailT "'Right found Left"
+--
+instance ( PP p x ~ Either a b
+         , P p x)
+    => P ('Right p) x where
+  type PP ('Right p) x = RightT (PP p x)
+  eval _ opts x = do
+    let msg0 = "'Right"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        case p of
+          Left _a -> mkNode opts (FailT (msg0 <> " found Left")) "" [hh pp]
+          Right b -> mkNode opts (PresentT b) "Right" [hh pp]
+
+
+-- removed Show x: else ambiguity errors in TestPredicate
+
+-- | extracts the \'a\' from type level \'These a b\' if the value exists
+--
+-- >>> pl @('This Id) (This 12)
+-- Present 12 (This)
+-- PresentT 12
+--
+-- >>> pz @('This Id) (That "aaa")
+-- FailT "'This found That"
+--
+-- >>> pz @('This Id) (These 999 "aaa")
+-- FailT "'This found These"
+--
+-- >>> pl @('This Id) (That 12)
+-- Error 'This found That
+-- FailT "'This found That"
+--
+
+instance ( PP p x ~ These a b
+         , P p x)
+    => P ('This p) x where
+  type PP ('This p) x = ThisT (PP p x)
+  eval _ opts x = do
+    let msg0 = "'This"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        case p of
+          This a -> mkNode opts (PresentT a) "This" [hh pp]
+          That _b -> mkNode opts (FailT (msg0 <> " found That")) "" [hh pp]
+          These _a _b -> mkNode opts (FailT (msg0 <> " found These")) "" [hh pp]
+
+-- | extracts the \'b\' from type level \'These a b\' if the value exists
+--
+-- >>> pz @('That Id) (That 123)
+-- PresentT 123
+--
+-- >>> pz @('That Id) (This "aaa")
+-- FailT "'That found This"
+--
+-- >>> pz @('That Id) (These 44 "aaa")
+-- FailT "'That found These"
+--
+
+instance ( PP p x ~ These a b
+         , P p x)
+    => P ('That p) x where
+  type PP ('That p) x = ThatT (PP p x)
+  eval _ opts x = do
+    let msg0 = "'That"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        case p of
+          This _a -> mkNode opts (FailT (msg0 <> " found This")) "" [hh pp]
+          That b -> mkNode opts (PresentT b) "That" [hh pp]
+          These _a _b -> mkNode opts (FailT (msg0 <> " found These")) "" [hh pp]
+
+
+-- | extracts the (a,b) from type level \'These a b\' if the value exists
+--
+-- >>> pz @('These Id Id) (These 123 "abc")
+-- PresentT (123,"abc")
+--
+-- >>> pz @('These Id 5) (These 123 "abcde")
+-- PresentT (123,5)
+--
+-- >>> pz @('These Id Id) (This "aaa")
+-- FailT "'These found This"
+--
+-- >>> pz @('These Id Id) (That "aaa")
+-- FailT "'These found That"
+--
+instance (Show a
+        , Show b
+        , P p a
+        , P q b
+        , Show (PP p a)
+        , Show (PP q b)
+        ) => P ('These p q) (These a b) where
+  type PP ('These p q) (These a b) = (PP p a, PP q b)
+  eval _ opts th = do
+    let msg0 = "'These"
+    case th of
+         These a b -> do
+            pp <- eval (Proxy @p) opts a
+            case getValueLR opts msg0 pp [] of
+               Left e -> pure e
+               Right p -> do
+                 qq <- eval (Proxy @q) opts b
+                 pure $ case getValueLR opts (msg0 <> " q failed p=" <> showL opts p) qq [hh pp] of
+                    Left e -> e
+                    Right q ->
+                      let ret =(p,q)
+                      in  mkNode opts (PresentT ret) (show01 opts msg0 ret (These a b)) [hh pp, hh qq]
+         _ -> pure $ mkNode opts (FailT (msg0 <> " found " <> showThese th)) "" []
+
+-- | converts the value to the corresponding 'Proxy'
+--
+-- >>> pz @'Proxy 'x'
+-- PresentT Proxy
+--
+instance Show a => P 'Proxy a where
+  type PP 'Proxy a = Proxy a
+  eval _ opts a =
+    let b = Proxy @a
+    in pure $ mkNode opts (PresentT b) ("'Proxy" <> showVerbose opts " | " a) []
+
+-- | typelevel 'BoolT'
+--
+-- >>> pz @'TrueT ()
+-- TrueT
+--
+-- >>> pz @'FalseT ()
+-- FalseT
+--
+-- >>> pz @('PresentT 123) ()
+-- PresentT False
+--
+-- >>> pz @('FailT '[]) ()
+-- FailT "'FailT _"
+--
+instance GetBoolT x b => P (b :: BoolT x) a where
+  type PP b a = Bool
+  eval _ opts _ = do
+    let ret = getBoolT @x @b
+    pure $ case ret of
+      Left b -> mkNodeB opts b (if b then "'TrueT" else "'FalseT") []
+      Right True -> mkNode opts (PresentT False) "'PresentT _" []
+      Right False -> mkNode opts (FailT "'FailT _") "BoolT" []
+
+pan, panv, pa, pu, pl, pz, pab, pub, pav, puv
+  :: forall p a
+  . ( Show (PP p a)
+    , P p a
+    ) => a
+      -> IO (BoolT (PP p a))
+-- | skips the evaluation tree and just displays the end result
+pz = run @OZ @p
+-- | same as 'pz' but adds context to the end result
+pl = run @OL @p
+-- | displays the evaluation tree in plain text without colors
+pan = run @OAN @p
+-- | displays the evaluation tree in plain text without colors and verbose
+panv = run @OANV @p
+-- | displays the evaluation tree using colors without background colors
+pa = run @OA @p
+-- | displays the evaluation tree using background colors
+pab = run @OAB @p
+-- | 'pa' and verbose
+pav = run @OAV @p
+-- | display the evaluation tree using unicode and colors
+-- @
+--   pu @'(Id, "abc", 123) [1..4]
+-- @
+pu = run @OU @p
+-- | displays the evaluation tree using unicode and colors with background colors
+pub = run @OUB @p
+-- | 'pu' and verbose
+puv = run @OUV @p
+
+-- | evaluate a typelevel expression (use type applications to pass in the options and the expression)
+--
+-- >>> run @OZ @Id 123
+-- PresentT 123
+--
+-- >>> run @('OMsg "field1" ':# OL) @('Left Id) (Right 123)
+-- field1 >>> Error 'Left found Right
+-- FailT "'Left found Right"
+--
+-- >>> run @(OptTT '[ 'OMsg "test", OU, 'OEmpty, OL, 'OMsg "field2"]) @('FailT '[]) ()
+-- test | field2 >>> Error 'FailT _ (BoolT)
+-- FailT "'FailT _"
+--
+run :: forall opts p a
+        . ( OptTC opts
+          , Show (PP p a)
+          , P p a)
+        => a
+        -> IO (BoolT (PP p a))
+run a = do
+  let opts = getOptT @opts
+  pp <- eval (Proxy @p) opts a
+  let r = pp ^. tBool
+  putStr $ prtTree opts pp
+  return r
+
+-- | run expression with multiple options in a list
+--
+-- >>> runs @'[ OL, 'OMsg "field2"] @'( 'True, 'False) ()
+-- field2 >>> Present (True,False) ('(True,False))
+-- PresentT (True,False)
+--
+-- >>> runs @'[ 'OMsg "test", OU, 'OEmpty, OL, 'OMsg "field2"] @('FailT '[]) ()
+-- test | field2 >>> Error 'FailT _ (BoolT)
+-- FailT "'FailT _"
+--
+runs :: forall optss p a
+        . ( OptTC (OptTT optss)
+          , Show (PP p a)
+          , P p a)
+        => a
+        -> IO (BoolT (PP p a))
+runs = run @(OptTT optss) @p
+
+-- | convenience method to evaluate two expressions using the same input and return the results
+runPQ :: ( P p a
+         , P q a
+         , MonadEval m)
+   => String
+   -> proxy1 p
+   -> proxy2 q
+   -> POpts
+   -> a
+   -> [Holder]
+   -> m (Either (TT x) (PP p a, PP q a, TT (PP p a), TT (PP q a)))
+runPQ msg0 proxyp proxyq opts a hhs = do
+    pp <- eval proxyp opts a
+    case getValueLR opts msg0 pp hhs of
+      Left e -> pure $ Left e
+      Right p -> do
+         qq <- eval proxyq opts a
+         pure $ case getValueLR opts msg0 qq (hhs <> [hh pp]) of
+           Left e -> Left e
+           Right q -> Right (p, q, pp, qq)
+
+-- | convenience method to evaluate two boolean expressions using the same input and return the results
+runPQBool :: ( P p a
+             , PP p a ~ Bool
+             , P q a
+             , PP q a ~ Bool, MonadEval m)
+   => String
+   -> proxy1 p
+   -> proxy2 q
+   -> POpts
+   -> a
+   -> [Holder]
+   -> m (Either (TT x) (PP p a, PP q a, TT (PP p a), TT (PP q a)))
+runPQBool msg0 proxyp proxyq opts a hhs = do
+    pp <- evalBool proxyp opts a
+    case getValueLR opts msg0 pp hhs of
+      Left e -> pure $ Left e
+      Right p -> do
+         qq <- evalBool proxyq opts a
+         pure $ case getValueLR opts msg0 qq (hhs <> [hh pp]) of
+           Left e -> Left e
+           Right q -> Right (p, q, pp, qq)
+
+-- | evaluate a boolean expressions but hide the results unless verbose
+evalBoolHide :: forall p a m
+  . (MonadEval m, P p a, PP p a ~ Bool)
+  => POpts
+  -> a
+  -> m (TT (PP p a))
+evalBoolHide opts =
+  if isVerbose opts then evalBool (Proxy @p) opts
+  else evalBool (Proxy @(Hide p)) opts
+
+-- | evaluate a expressions but hide the results unless verbose
+evalHide :: forall p a m
+  . (MonadEval m, P p a)
+  => POpts
+  -> a
+  -> m (TT (PP p a))
+evalHide opts =
+  if isVerbose opts then eval (Proxy @p) opts
+  else eval (Proxy @(Hide p)) opts
+
+
+-- advantage of (>>) over 'Do [k] is we can use different kinds for (>>) without having to wrap with 'W'
+
+-- | compose expressions
+--
+-- >>> pz @(Fst Id >> Snd Id) ((11,12),'x')
+-- PresentT 12
+--
+data p >> q
+infixr 1 >>
+
+instance (Show (PP p a)
+        , Show (PP q (PP p a))
+        , P p a
+        , P q (PP p a)
+        ) => P (p >> q) a where
+  type PP (p >> q) a = PP q (PP p a)
+  eval _ opts a = do
+    let msg0 = "(>>)"
+    pp <- eval (Proxy @p) opts a
+    case getValueLR opts "(>>) lhs failed" pp [] of
+      Left e -> pure e
+      Right p -> do
+        qq <- eval (Proxy @q) opts p
+        pure $ case getValueLR opts (show p <> " (>>) rhs failed") qq [hh pp] of
+          Left e -> e
+          Right q -> mkNode opts (_tBool qq) (lit01 opts msg0 q "" (topMessageEgregious qq)) [hh pp, hh qq]
+
+-- | flipped version of 'Predicate.Core.>>'
+data p << q
+type LeftArrowsT p q = q >> p
+infixr 1 <<
+
+instance P (LeftArrowsT p q) x => P (p << q) x where
+  type PP (p << q) x = PP (LeftArrowsT p q) x
+  eval _ = eval (Proxy @(LeftArrowsT p q))
+
+-- bearbeiten! only used by >>
+topMessageEgregious :: TT a -> String
+topMessageEgregious pp = innermost (pp ^. tString)
+  where innermost = ('{':) . reverse . ('}':) . takeWhile (/='{') . dropWhile (=='}') . reverse
+
+-- | unwraps a value (see '_Wrapped'')
+--
+-- >>> pz @(Unwrap Id) (SG.Sum (-13))
+-- PresentT (-13)
+--
+-- >>> pl @(Unwrap Id >> '(Id, 'True)) (SG.Sum 13)
+-- Present (13,True) ((>>) (13,True) | {'(13,True)})
+-- PresentT (13,True)
+--
+data Unwrap p
+
+instance (PP p x ~ s
+        , P p x
+        , Show s
+        , Show (Unwrapped s)
+        , Wrapped s
+        ) => P (Unwrap p) x where
+  type PP (Unwrap p) x = Unwrapped (PP p x)
+  eval _ opts x = do
+    let msg0 = "Unwrap"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let d = p ^. _Wrapped'
+        in mkNode opts (PresentT d) (show01 opts msg0 d p) [hh pp]
+
+data Wrap' t p
+
+instance (Show (PP p x)
+        , P p x
+        , Unwrapped (PP s x) ~ PP p x
+        , Wrapped (PP s x)
+        , Show (PP s x)
+        ) => P (Wrap' s p) x where
+  type PP (Wrap' s p) x = PP s x
+  eval _ opts x = do
+    let msg0 = "Wrap"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let d = p ^. _Unwrapped'
+        in mkNode opts (PresentT d) (show01 opts msg0 d p) [hh pp]
+
+-- | wraps a value (see '_Wrapped'' and '_Unwrapped'')
+--
+-- >>> pz @(Wrap (SG.Sum _) Id) (-13)
+-- PresentT (Sum {getSum = -13})
+--
+-- >>> pz @(Wrap SG.Any (Ge 4)) 13
+-- PresentT (Any {getAny = True})
+--
+-- >>> import Data.List.NonEmpty (NonEmpty(..))
+-- >>> pz @(Wrap (NonEmpty _) (Uncons >> 'Just Id)) "abcd"
+-- PresentT ('a' :| "bcd")
+--
+-- >>> pl @(Wrap (SG.Sum _) Id) 13
+-- Present Sum {getSum = 13} (Wrap Sum {getSum = 13} | 13)
+-- PresentT (Sum {getSum = 13})
+--
+-- >>> pl @(Wrap (SG.Sum _) Id >> STimes 4 Id) 13
+-- Present Sum {getSum = 52} ((>>) Sum {getSum = 52} | {getSum = 13})
+-- PresentT (Sum {getSum = 52})
+--
+-- >>> pl @(Wrap _ 13 <> Id) (SG.Sum @Int 12)
+-- Present Sum {getSum = 25} (Sum {getSum = 13} <> Sum {getSum = 12} = Sum {getSum = 25})
+-- PresentT (Sum {getSum = 25})
+--
+
+data Wrap (t :: Type) p
+type WrapT (t :: Type) p = Wrap' (Hole t) p
+
+instance P (WrapT t p) x => P (Wrap t p) x where
+  type PP (Wrap t p) x = PP (WrapT t p) x
+  eval _ = eval (Proxy @(WrapT t p))
+
+
+-- | used for type inference
+data Unproxy
+
+instance Typeable a => P Unproxy (Proxy (a :: Type)) where
+  type PP Unproxy (Proxy a) = a
+  eval _ opts _a =
+    let msg0 = "Unproxy(" <> showT @a <> ")"
+    in pure $ mkNode opts (FailT msg0) "you probably meant to get access to the type of PP only and not evaluate" []
+
+-- | similar to 'length'
+--
+-- >>> pz @Len [10,4,5,12,3,4]
+-- PresentT 6
+--
+-- >>> pz @Len []
+-- PresentT 0
+--
+data Len
+instance ( Show a
+         , as ~ [a]
+         ) => P Len as where
+  type PP Len as = Int
+  eval _ opts as =
+    let msg0 = "Len"
+        n = length as
+    in pure $ mkNode opts (PresentT n) (show01 opts msg0 n as) []
+
+-- | similar to 'length' for 'Foldable' instances
+--
+-- >>> pz @(Length Id) (Left "aa")
+-- PresentT 0
+--
+-- >>> pz @(Length Id) (Right "aa")
+-- PresentT 1
+--
+-- >>> pz @(Length Right') (Right "abcd")
+-- PresentT 4
+--
+-- >>> pz @(Length (Thd (Snd Id))) (True,(23,'x',[10,9,1,3,4,2]))
+-- PresentT 6
+--
+data Length p
+
+instance (PP p x ~ t a
+        , P p x
+        , Show (t a)
+        , Foldable t) => P (Length p) x where
+  type PP (Length p) x = Int
+  eval _ opts x = do
+    let msg0 = "Length"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+            let n = length p
+            in mkNode opts (PresentT n) (show01 opts msg0 n p) [hh pp]
+
+-- | 'not' function
+--
+-- >>> pz @(Not Id) False
+-- TrueT
+--
+-- >>> pz @(Not Id) True
+-- FalseT
+--
+-- >>> pz @(Not (Fst Id)) (True,22)
+-- FalseT
+--
+-- >>> pl @(Not (Lt 3)) 13
+-- True (Not (13 < 3))
+-- TrueT
+--
+-- >>> pl @(Not 'True) ()
+-- False (Not ('True))
+-- FalseT
+--
+data Not p
+
+instance ( PP p x ~ Bool
+         , P p x
+         ) => P (Not p) x where
+  type PP (Not p) x = Bool
+  eval _ opts x = do
+    let msg0 = "Not"
+    pp <- evalBool (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let b = not p
+        in mkNodeB opts b (msg0 <> litVerbose opts " " (topMessage pp)) [hh pp]
+
+-- | 'id' function on a boolean
+--
+-- >>> pz @(IdBool Id) False
+-- FalseT
+--
+-- >>> pz @(IdBool Id) True
+-- TrueT
+--
+-- >>> pz @(IdBool (Fst Id)) (True,22)
+-- TrueT
+--
+-- >>> pl @(IdBool (Lt 3)) 13
+-- False (IdBool (13 < 3))
+-- FalseT
+--
+data IdBool p
+
+instance ( PP p x ~ Bool
+         , P p x
+         ) => P (IdBool p) x where
+  type PP (IdBool p) x = Bool
+  eval _ opts x = do
+    let msg0 = "IdBool"
+    pp <- evalBool (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let b = p
+        in mkNodeB opts b (msg0 <> litVerbose opts " " (topMessage pp)) [hh pp]
+
+-- | Fails the computation with a message but allows you to set the output type
+--
+-- >>> pz @(Failt Int (PrintF "value=%03d" Id)) 99
+-- FailT "value=099"
+--
+-- >>> pz @('False || (Fail 'True "failed")) (99,"somedata")
+-- FailT "failed"
+--
+-- >>> pz @('False || (Fail (Hole Bool) "failed")) (99,"somedata")
+-- FailT "failed"
+--
+-- >>> pz @('False || (Fail (Hole _) "failed")) (99,"somedata")
+-- FailT "failed"
+--
+data Fail t prt
+
+instance (P prt a
+        , PP prt a ~ String
+        ) => P (Fail t prt) a where
+  type PP (Fail t prt) a = PP t a
+  eval _ opts a = do
+    let msg0 = "Fail"
+    pp <- eval (Proxy @prt) opts a
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right s -> mkNode opts (FailT s) (msg0 <> " " <> s) [hh pp | isVerbose opts]
+
+-- | Fails the computation with a message for simple failures: doesnt preserve types
+--
+-- >>> pz @(FailS (PrintT "value=%03d string=%s" Id)) (99,"somedata")
+-- FailT "value=099 string=somedata"
+--
+data FailS p
+instance P (Fail I p) x => P (FailS p) x where
+  type PP (FailS p) x = PP (Fail I p) x
+  eval _ = eval (Proxy @(Fail I p))
+
+-- | Fails the computation with a message (wraps the type in 'Hole')
+--
+-- >>> pz @(Failt Int (PrintF "value=%03d" Id)) 99
+-- FailT "value=099"
+--
+data Failt (t :: Type) p
+instance P (Fail (Hole t) p) x => P (Failt t p) x where
+  type PP (Failt t p) x = PP (Fail (Hole t) p) x
+  eval _ = eval (Proxy @(Fail (Hole t) p))
+
+-- | Fails the computation with a message where the input value is a Proxy
+--
+-- >>> pz @(Ix 3 (Failp "oops")) "abcd"
+-- PresentT 'd'
+--
+-- >>> pz @(Ix 3 (Failp "oops")) "abc"
+-- FailT "oops"
+--
+data Failp p
+instance P (Fail Unproxy p) x => P (Failp p) x where
+  type PP (Failp p) x = PP (Fail Unproxy p) x
+  eval _ = eval (Proxy @(Fail Unproxy p))
+
+-- | gets the singleton value from a foldable
+--
+-- >>> pl @(OneP Id) [10..15]
+-- Error OneP 6 elements (expected one element)
+-- FailT "OneP 6 elements"
+--
+-- >>> pl @(OneP Id) [10]
+-- Present 10 (OneP)
+-- PresentT 10
+--
+-- >>> pl @(OneP Id) []
+-- Error OneP empty (expected one element)
+-- FailT "OneP empty"
+--
+-- >>> pl @(OneP Id) (Just 10)
+-- Present 10 (OneP)
+-- PresentT 10
+--
+-- >>> pl @(OneP Id) Nothing
+-- Error OneP empty (expected one element)
+-- FailT "OneP empty"
+--
+-- >>> pl @(OneP Id) [12]
+-- Present 12 (OneP)
+-- PresentT 12
+--
+-- >>> pl @(OneP Id) [1..5]
+-- Error OneP 5 elements (expected one element)
+-- FailT "OneP 5 elements"
+--
+-- >>> pl @(OneP Id) ([] ::[()])
+-- Error OneP empty (expected one element)
+-- FailT "OneP empty"
+--
+
+data OneP p
+instance (Foldable t
+        , PP p x ~ t a
+        , P p x
+        ) => P (OneP p) x where
+  type PP (OneP p) x = ExtractAFromTA (PP p x)
+  eval _ opts x = do
+    let msg0 = "OneP"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p -> case toList p of
+                   [] -> mkNode opts (FailT (msg0 <> " empty")) "expected one element" [hh pp]
+                   [a] -> mkNode opts (PresentT a) msg0 [hh pp]
+                   as -> let n = length as
+                         in mkNode opts (FailT (msg0 <> " " <> show n <> " elements")) "expected one element" [hh pp]
+
+--type OneP = Guard "expected list of length 1" (Len == 1) >> Head Id
+--type OneP = Guard (PrintF "expected list of length 1 but found length=%d" Len) (Len == 1) >> Head Id
+
+-- | A predicate that determines if the value is between \'p\' and \'q\'
+--
+-- >>> pz @(Between 5 8 Len) [1,2,3,4,5,5,7]
+-- TrueT
+--
+-- >>> pl @(Between 5 8 Id) 9
+-- False (9 <= 8)
+-- FalseT
+--
+-- >>> pl @(Between (Fst Id >> Fst Id) (Fst Id >> Snd Id) (Snd Id)) ((1,4),3)
+-- True (1 <= 3 <= 4)
+-- TrueT
+--
+-- >>> pl @(Between (Fst Id >> Fst Id) (Fst Id >> Snd Id) (Snd Id)) ((1,4),10)
+-- False (10 <= 4)
+-- FalseT
+--
+data Between p q r -- reify as it is used a lot! nicer specific messages at the top level!
+
+instance (Ord (PP p x)
+       , Show (PP p x)
+       , PP r x ~ PP p x
+       , PP r x ~ PP q x
+       , P p x
+       , P q x
+       , P r x
+       ) => P (Between p q r) x where
+  type PP (Between p q r) x = Bool
+  eval _ opts x = do
+    let msg0 = "Between"
+    rr <- eval (Proxy @r) opts x
+    case getValueLR opts msg0 rr [] of
+      Left e -> pure e
+      Right r -> do
+        lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x [hh rr]
+        pure $ case lr of
+          Left e -> e
+          Right (p,q,pp,qq) ->
+            let hhs = [hh rr, hh pp, hh qq]
+            in if p <= r && r <= q then mkNodeB opts True (showL opts p <> " <= " <> showL opts r <> " <= " <> showL opts q) hhs
+               else if p > r then mkNodeB opts False (showL opts p <> " <= " <> showL opts r) hhs
+               else mkNodeB opts False (showL opts r <> " <= " <> showL opts q) hhs
+
+
+-- | A operator predicate that determines if the value is between \'p\' and \'q\'
+--
+-- >>> pz @(5 <..> 8) 6
+-- TrueT
+--
+-- >>> pz @(10 % 4 <..> 40 % 5) 4
+-- TrueT
+--
+-- >>> pz @(10 % 4 <..> 40 % 5) 33
+-- FalseT
+--
+data p <..> q
+infix 4 <..>
+
+type BetweenT p q = Between p q Id
+
+instance P (BetweenT p q) x => P (p <..> q) x where
+  type PP (p <..> q) x = PP (BetweenT p q) x
+  eval _ = evalBool (Proxy @(BetweenT p q))
+
+-- | similar to 'all'
+--
+-- >>> pl @(All (Between 1 8 Id) Id) [7,3,4,1,2,9,0,1]
+-- False (All(8) i=5 (9 <= 8))
+-- FalseT
+--
+-- >>> pz @(All Odd Id) [1,5,11,5,3]
+-- TrueT
+--
+-- >>> pz @(All Odd Id) []
+-- TrueT
+--
+-- >>> run @'OANV @(All Even Id) [1,5,11,5,3]
+-- False All(5) i=0 (1 == 0)
+-- |
+-- +- P Id [1,5,11,5,3]
+-- |
+-- +- False i=0: 1 == 0
+-- |  |
+-- |  +- P 1 `mod` 2 = 1
+-- |  |  |
+-- |  |  +- P I
+-- |  |  |
+-- |  |  `- P '2
+-- |  |
+-- |  `- P '0
+-- |
+-- +- False i=1: 1 == 0
+-- |  |
+-- |  +- P 5 `mod` 2 = 1
+-- |  |  |
+-- |  |  +- P I
+-- |  |  |
+-- |  |  `- P '2
+-- |  |
+-- |  `- P '0
+-- |
+-- +- False i=2: 1 == 0
+-- |  |
+-- |  +- P 11 `mod` 2 = 1
+-- |  |  |
+-- |  |  +- P I
+-- |  |  |
+-- |  |  `- P '2
+-- |  |
+-- |  `- P '0
+-- |
+-- +- False i=3: 1 == 0
+-- |  |
+-- |  +- P 5 `mod` 2 = 1
+-- |  |  |
+-- |  |  +- P I
+-- |  |  |
+-- |  |  `- P '2
+-- |  |
+-- |  `- P '0
+-- |
+-- `- False i=4: 1 == 0
+--    |
+--    +- P 3 `mod` 2 = 1
+--    |  |
+--    |  +- P I
+--    |  |
+--    |  `- P '2
+--    |
+--    `- P '0
+-- FalseT
+--
+-- >>> pl @(All (Gt 3) (Fst Id)) ([10,12,3,5],"ss")
+-- False (All(4) i=2 (3 > 3))
+-- FalseT
+--
+-- >>> pl @(All (Lt 3) Id) [1::Int .. 10]
+-- False (All(10) i=2 (3 < 3))
+-- FalseT
+--
+data All p q
+
+instance (P p a
+        , PP p a ~ Bool
+        , PP q x ~ f a
+        , P q x
+        , Show a
+        , Foldable f
+        ) => P (All p q) x where
+  type PP (All p q) x = Bool
+  eval _ opts x = do
+    let msg0 = "All"
+    qq <- eval (Proxy @q) opts x
+    case getValueLR opts msg0 qq [] of
+      Left e -> pure e
+      Right q ->
+        case chkSize opts msg0 q [hh qq] of
+          Left e -> pure e
+          Right () -> do
+            ts <- zipWithM (\i a -> ((i, a),) <$> evalBoolHide @p opts a) [0::Int ..] (toList q)
+            pure $ case splitAndAlign opts msg0 ts of
+                 Left e -> e
+                 Right abcs ->
+                   let hhs = hh qq : map (hh . fixit) ts
+                       msg1 = msg0 ++ "(" ++ show (length q) ++ ")"
+                   in case find (not . view _1) abcs of
+                        Nothing -> mkNodeB opts True msg1 hhs
+                        Just (_,(i,_),tt) ->
+                          mkNodeB opts False (msg1 <> " i=" ++ showIndex i ++ " " <> topMessage tt) hhs
+
+-- | similar to 'any'
+--
+-- >>> pl @(Any Even Id) [1,5,11,5,3]
+-- False (Any(5))
+-- FalseT
+--
+-- >>> pl @(Any Even Id) [1,5,112,5,3]
+-- True (Any(5) i=2 (0 == 0))
+-- TrueT
+--
+-- >>> pz @(Any Even Id) []
+-- FalseT
+--
+-- >>> pl @(Any (Gt 3) (Fst Id)) ([10,12,3,5],"ss")
+-- True (Any(4) i=0 (10 > 3))
+-- TrueT
+--
+-- >>> pl @(Any (Same 2) Id) [1,4,5]
+-- False (Any(3))
+-- FalseT
+--
+-- >>> pl @(Any (Same 2) Id) [1,4,5,2,1]
+-- True (Any(5) i=3 (2 == 2))
+-- TrueT
+--
+data Any p q
+
+instance (P p a
+        , PP p a ~ Bool
+        , PP q x ~ f a
+        , P q x
+        , Show a
+        , Foldable f
+        ) => P (Any p q) x where
+  type PP (Any p q) x = Bool
+  eval _ opts x = do
+    let msg0 = "Any"
+    qq <- eval (Proxy @q) opts x
+    case getValueLR opts msg0 qq [] of
+      Left e -> pure e
+      Right q ->
+        case chkSize opts msg0 q [hh qq] of
+          Left e -> pure e
+          Right () -> do
+            ts <- zipWithM (\i a -> ((i, a),) <$> evalBoolHide @p opts a) [0::Int ..] (toList q)
+            pure $ case splitAndAlign opts msg0 ts of
+                 Left e -> e
+                 Right abcs ->
+                   let hhs = hh qq : map (hh . fixit) ts
+                       msg1 = msg0 ++ "(" ++ show (length q) ++ ")"
+                   in case find (view _1) abcs of
+                        Nothing -> mkNodeB opts False msg1 hhs
+                        Just (_,(i,_),tt) ->
+                          mkNodeB opts True (msg1 <> " i=" ++ showIndex i ++ " " <> topMessage tt) hhs
+
+-- | similar to 'fst'
+--
+-- >>> pz @(Fst Id) (10,"Abc")
+-- PresentT 10
+--
+-- >>> pz @(Fst Id) (10,"Abc",'x')
+-- PresentT 10
+--
+-- >>> pz @(Fst Id) (10,"Abc",'x',False)
+-- PresentT 10
+--
+-- >>> pl @(Fst Id) (99,'a',False,1.3)
+-- Present 99 (Fst 99 | (99,'a',False,1.3))
+-- PresentT 99
+--
+data Fst p
+
+instance (Show (ExtractL1T (PP p x))
+        , ExtractL1C (PP p x)
+        , P p x
+        , Show (PP p x)
+        ) => P (Fst p) x where
+  type PP (Fst p) x = ExtractL1T (PP p x)
+  eval _ opts x = do
+    let msg0 = "Fst"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let b = extractL1C p
+        in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
+
+data L1 p
+type L1T p = Fst p
+
+instance P (L1T p) x => P (L1 p) x where
+  type PP (L1 p) x = PP (L1T p) x
+  eval _ = eval (Proxy @(L1T p))
+
+class ExtractL1C tp where
+  type ExtractL1T tp
+  extractL1C :: tp -> ExtractL1T tp
+instance ExtractL1C (a,b) where
+  type ExtractL1T (a,b) = a
+  extractL1C (a,_) = a
+instance ExtractL1C (a,b,c) where
+  type ExtractL1T (a,b,c) = a
+  extractL1C (a,_,_) = a
+instance ExtractL1C (a,b,c,d) where
+  type ExtractL1T (a,b,c,d) = a
+  extractL1C (a,_,_,_) = a
+instance ExtractL1C (a,b,c,d,e) where
+  type ExtractL1T (a,b,c,d,e) = a
+  extractL1C (a,_,_,_,_) = a
+instance ExtractL1C (a,b,c,d,e,f) where
+  type ExtractL1T (a,b,c,d,e,f) = a
+  extractL1C (a,_,_,_,_,_) = a
+
+-- | similar to 'snd'
+--
+-- >>> pz @(Snd Id) (10,"Abc")
+-- PresentT "Abc"
+--
+-- >>> pz @(Snd Id) (10,"Abc",True)
+-- PresentT "Abc"
+--
+-- >>> pl @(Snd Id) (99,'a',False,1.3)
+-- Present 'a' (Snd 'a' | (99,'a',False,1.3))
+-- PresentT 'a'
+--
+data Snd p
+
+instance (Show (ExtractL2T (PP p x))
+        , ExtractL2C (PP p x)
+        , P p x
+        , Show (PP p x)
+        ) => P (Snd p) x where
+  type PP (Snd p) x = ExtractL2T (PP p x)
+  eval _ opts x = do
+    let msg0 = "Snd"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let b = extractL2C p
+        in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
+
+data L2 p
+type L2T p = Snd p
+
+instance P (L2T p) x => P (L2 p) x where
+  type PP (L2 p) x = PP (L2T p) x
+  eval _ = eval (Proxy @(L2T p))
+
+class ExtractL2C tp where
+  type ExtractL2T tp
+  extractL2C :: tp -> ExtractL2T tp
+instance ExtractL2C (a,b) where
+  type ExtractL2T (a,b) = b
+  extractL2C (_,b) = b
+instance ExtractL2C (a,b,c) where
+  type ExtractL2T (a,b,c) = b
+  extractL2C (_,b,_) = b
+instance ExtractL2C (a,b,c,d) where
+  type ExtractL2T (a,b,c,d) = b
+  extractL2C (_,b,_,_) = b
+instance ExtractL2C (a,b,c,d,e) where
+  type ExtractL2T (a,b,c,d,e) = b
+  extractL2C (_,b,_,_,_) = b
+instance ExtractL2C (a,b,c,d,e,f) where
+  type ExtractL2T (a,b,c,d,e,f) = b
+  extractL2C (_,b,_,_,_,_) = b
+
+-- | similar to 3rd element in a n-tuple
+--
+-- >>> pz @(Thd Id) (10,"Abc",133)
+-- PresentT 133
+--
+-- >>> pz @(Thd Id) (10,"Abc",133,True)
+-- PresentT 133
+--
+-- >>> pl @(Thd Id) (99,'a',False,1.3)
+-- Present False (Thd False | (99,'a',False,1.3))
+-- PresentT False
+--
+data Thd p
+
+instance (Show (ExtractL3T (PP p x))
+        , ExtractL3C (PP p x)
+        , P p x
+        , Show (PP p x)
+        ) => P (Thd p) x where
+  type PP (Thd p) x = ExtractL3T (PP p x)
+  eval _ opts x = do
+    let msg0 = "Thd"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let b = extractL3C p
+        in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
+
+data L3 p
+type L3T p = Thd p
+
+instance P (L3T p) x => P (L3 p) x where
+  type PP (L3 p) x = PP (L3T p) x
+  eval _ = eval (Proxy @(L3T p))
+
+class ExtractL3C tp where
+  type ExtractL3T tp
+  extractL3C :: tp -> ExtractL3T tp
+instance ExtractL3C (a,b) where
+  type ExtractL3T (a,b) = GL.TypeError ('GL.Text "Thd doesn't work for 2-tuples")
+  extractL3C _ = errorInProgram "Thd doesn't work for 2-tuples"
+instance ExtractL3C (a,b,c) where
+  type ExtractL3T (a,b,c) = c
+  extractL3C (_,_,c) = c
+instance ExtractL3C (a,b,c,d) where
+  type ExtractL3T (a,b,c,d) = c
+  extractL3C (_,_,c,_) = c
+instance ExtractL3C (a,b,c,d,e) where
+  type ExtractL3T (a,b,c,d,e) = c
+  extractL3C (_,_,c,_,_) = c
+instance ExtractL3C (a,b,c,d,e,f) where
+  type ExtractL3T (a,b,c,d,e,f) = c
+  extractL3C (_,_,c,_,_,_) = c
+
+-- | similar to 4th element in a n-tuple
+--
+-- >>> pz @(L4 Id) (10,"Abc",'x',True)
+-- PresentT True
+--
+-- >>> pz @(L4 (Fst (Snd Id))) ('x',((10,"Abc",'x',999),"aa",1),9)
+-- PresentT 999
+--
+-- >>> pl @(L4 Id) (99,'a',False,"someval")
+-- Present "someval" (L4 "someval" | (99,'a',False,"someval"))
+-- PresentT "someval"
+--
+data L4 p
+
+instance (Show (ExtractL4T (PP p x))
+        , ExtractL4C (PP p x)
+        , P p x
+        , Show (PP p x)
+        ) => P (L4 p) x where
+  type PP (L4 p) x = ExtractL4T (PP p x)
+  eval _ opts x = do
+    let msg0 = "L4"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let b = extractL4C p
+        in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
+
+class ExtractL4C tp where
+  type ExtractL4T tp
+  extractL4C :: tp -> ExtractL4T tp
+instance ExtractL4C (a,b) where
+  type ExtractL4T (a,b) = GL.TypeError ('GL.Text "L4 doesn't work for 2-tuples")
+  extractL4C _ = errorInProgram "L4 doesn't work for 2-tuples"
+instance ExtractL4C (a,b,c) where
+  type ExtractL4T (a,b,c) = GL.TypeError ('GL.Text "L4 doesn't work for 3-tuples")
+  extractL4C _ = errorInProgram "L4 doesn't work for 3-tuples"
+instance ExtractL4C (a,b,c,d) where
+  type ExtractL4T (a,b,c,d) = d
+  extractL4C (_,_,_,d) = d
+instance ExtractL4C (a,b,c,d,e) where
+  type ExtractL4T (a,b,c,d,e) = d
+  extractL4C (_,_,_,d,_) = d
+instance ExtractL4C (a,b,c,d,e,f) where
+  type ExtractL4T (a,b,c,d,e,f) = d
+  extractL4C (_,_,_,d,_,_) = d
+
+-- | similar to 5th element in a n-tuple
+--
+-- >>> pz @(L5 Id) (10,"Abc",'x',True,1)
+-- PresentT 1
+--
+data L5 p
+
+instance (Show (ExtractL5T (PP p x))
+        , ExtractL5C (PP p x)
+        , P p x
+        , Show (PP p x)
+        ) => P (L5 p) x where
+  type PP (L5 p) x = ExtractL5T (PP p x)
+  eval _ opts x = do
+    let msg0 = "L5"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let b = extractL5C p
+        in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
+
+class ExtractL5C tp where
+  type ExtractL5T tp
+  extractL5C :: tp -> ExtractL5T tp
+instance ExtractL5C (a,b) where
+  type ExtractL5T (a,b) = GL.TypeError ('GL.Text "L5 doesn't work for 2-tuples")
+  extractL5C _ = errorInProgram "L5 doesn't work for 2-tuples"
+instance ExtractL5C (a,b,c) where
+  type ExtractL5T (a,b,c) = GL.TypeError ('GL.Text "L5 doesn't work for 3-tuples")
+  extractL5C _ = errorInProgram "L5 doesn't work for 3-tuples"
+instance ExtractL5C (a,b,c,d) where
+  type ExtractL5T (a,b,c,d) = GL.TypeError ('GL.Text "L5 doesn't work for 4-tuples")
+  extractL5C _ = errorInProgram "L5 doesn't work for 4-tuples"
+instance ExtractL5C (a,b,c,d,e) where
+  type ExtractL5T (a,b,c,d,e) = e
+  extractL5C (_,_,_,_,e) = e
+instance ExtractL5C (a,b,c,d,e,f) where
+  type ExtractL5T (a,b,c,d,e,f) = e
+  extractL5C (_,_,_,_,e,_) = e
+
+
+-- | similar to 6th element in a n-tuple
+--
+-- >>> pz @(L6 Id) (10,"Abc",'x',True,1,99)
+-- PresentT 99
+--
+data L6 p
+
+instance (Show (ExtractL6T (PP p x))
+        , ExtractL6C (PP p x)
+        , P p x
+        , Show (PP p x)
+        ) => P (L6 p) x where
+  type PP (L6 p) x = ExtractL6T (PP p x)
+  eval _ opts x = do
+    let msg0 = "L6"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let b = extractL6C p
+        in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
+
+class ExtractL6C tp where
+  type ExtractL6T tp
+  extractL6C :: tp -> ExtractL6T tp
+instance ExtractL6C (a,b) where
+  type ExtractL6T (a,b) = GL.TypeError ('GL.Text "L6 doesn't work for 2-tuples")
+  extractL6C _ = errorInProgram "L6 doesn't work for 2-tuples"
+instance ExtractL6C (a,b,c) where
+  type ExtractL6T (a,b,c) = GL.TypeError ('GL.Text "L6 doesn't work for 3-tuples")
+  extractL6C _ = errorInProgram "L6 doesn't work for 3-tuples"
+instance ExtractL6C (a,b,c,d) where
+  type ExtractL6T (a,b,c,d) = GL.TypeError ('GL.Text "L6 doesn't work for 4-tuples")
+  extractL6C _ = errorInProgram "L6 doesn't work for 4-tuples"
+instance ExtractL6C (a,b,c,d,e) where
+  type ExtractL6T (a,b,c,d,e) = GL.TypeError ('GL.Text "L6 doesn't work for 5-tuples")
+  extractL6C _ = errorInProgram "L6 doesn't work for 5-tuples"
+instance ExtractL6C (a,b,c,d,e,f) where
+  type ExtractL6T (a,b,c,d,e,f) = f
+  extractL6C (_,_,_,_,_,f) = f
+
+-- | applies \'p\' to the first and second slot of an n-tuple
+--
+-- >>> pl @(Both Len (Fst Id)) (("abc",[10..17],1,2,3),True)
+-- Present (3,8) (Both)
+-- PresentT (3,8)
+--
+-- >>> pl @(Both (Pred Id) $ Fst Id) ((12,'z',[10..17]),True)
+-- Present (11,'y') (Both)
+-- PresentT (11,'y')
+--
+-- >>> pl @(Both (Succ Id) Id) (4,'a')
+-- Present (5,'b') (Both)
+-- PresentT (5,'b')
+--
+-- >>> pl @(Both Len (Fst Id)) (("abc",[10..17]),True)
+-- Present (3,8) (Both)
+-- PresentT (3,8)
+--
+-- >>> pl @(Both (ReadP Day Id) Id) ("1999-01-01","2001-02-12")
+-- Present (1999-01-01,2001-02-12) (Both)
+-- PresentT (1999-01-01,2001-02-12)
+--
+data Both p q
+instance ( ExtractL1C (PP q x)
+         , ExtractL2C (PP q x)
+         , P p (ExtractL1T (PP q x))
+         , P p (ExtractL2T (PP q x))
+         , P q x
+   ) => P (Both p q) x where
+  type PP (Both p q) x = (PP p (ExtractL1T (PP q x)), PP p (ExtractL2T (PP q x)))
+  eval _ opts x = do
+    let msg0 = "Both"
+    qq <- eval (Proxy @q) opts x
+    case getValueLR opts msg0 qq [] of
+      Left e -> pure e
+      Right q -> do
+        let (a,a') = (extractL1C q, extractL2C q)
+        pp <- eval (Proxy @p) opts a
+        case getValueLR opts msg0 pp [hh qq] of
+          Left e -> pure e
+          Right b -> do
+            pp' <- eval (Proxy @p) opts a'
+            pure $ case getValueLR opts msg0 pp' [hh qq, hh pp] of
+              Left e -> e
+              Right b' ->
+                mkNode opts (PresentT (b,b')) msg0 [hh qq, hh pp, hh pp']
+
+-- | similar to 'map'
+--
+-- >>> pz @(Map (Pred Id) Id) [1..5]
+-- PresentT [0,1,2,3,4]
+--
+data Map p q
+
+instance (Show (PP p a)
+        , P p a
+        , PP q x ~ f a
+        , P q x
+        , Show a
+        , Show (f a)
+        , Foldable f
+        ) => P (Map p q) x where
+  type PP (Map p q) x = [PP p (ExtractAFromTA (PP q x))]
+  eval _ opts x = do
+    let msg0 = "Map"
+    qq <- eval (Proxy @q) opts x
+    case getValueLR opts msg0 qq [] of
+      Left e -> pure e
+      Right q -> do
+        ts <- zipWithM (\i a -> ((i, a),) <$> evalHide @p opts a) [0::Int ..] (toList q)
+        pure $ case splitAndAlign opts msg0 ts of
+             Left e -> e
+             Right abcs ->
+               let vals = map (view _1) abcs
+               in mkNode opts (PresentT vals) (show01 opts msg0 vals q) (hh qq : map (hh . fixit) ts)
+
+-- | processes a type level list predicates running each in sequence: see 'Predicate.>>'
+--
+-- >>> pz @(Do [Pred Id, ShowP Id, Id &&& Len]) 9876543
+-- PresentT ("9876542",7)
+--
+-- >>> pz @(Do '[W 123, W "xyz", Len &&& Id, Pred Id *** Id<>Id]) ()
+-- PresentT (2,"xyzxyz")
+--
+-- >>> pl @(Do '[Succ Id,Id,ShowP Id,Ones Id,Map (ReadBase Int 8 Id) Id]) 1239
+-- Present [1,2,4,0] ((>>) [1,2,4,0] | {Map [1,2,4,0] | ["1","2","4","0"]})
+-- PresentT [1,2,4,0]
+--
+-- >>> pl @(Do '[Pred Id,Id,ShowP Id,Ones Id,Map (ReadBase Int 8 Id) Id]) 1239
+-- Error invalid base 8 (1238 (>>) rhs failed)
+-- FailT "invalid base 8"
+--
+-- >>> pl @(Do '[4,5,6]) ()
+-- Present 6 ((>>) 6 | {'6})
+-- PresentT 6
+--
+-- >>> pl @(Do '["abc", "Def", "ggg", "hhhhh"]) ()
+-- Present "hhhhh" ((>>) "hhhhh" | {'"hhhhh"})
+-- PresentT "hhhhh"
+--
+-- >>> pl @(Do '[ 'LT, 'EQ, 'GT ]) ()
+-- Present GT ((>>) GT | {'GT})
+-- PresentT GT
+--
+-- >>> pl @(Do '[4 % 4,22 % 1 ,12 -% 4]) ()
+-- Present (-3) % 1 ((>>) (-3) % 1 | {Negate (-3) % 1 | 3 % 1})
+-- PresentT ((-3) % 1)
+--
+-- >>> pl @(Do '[ W ('PresentT I), W 'FalseT, Not Id]) False
+-- True ((>>) True | {Not (Id False)})
+-- TrueT
+--
+-- >>> pl @(Do '[W ('PresentT Id), W 'FalseT]) True -- have to wrap them cos BoolT a vs BoolT Bool ie different types
+-- False ((>>) False | {W 'FalseT})
+-- FalseT
+--
+-- >>> pl @(Do '[1,2,3]) ()
+-- Present 3 ((>>) 3 | {'3})
+-- PresentT 3
+--
+
+data Do (ps :: [k])
+
+instance (P (DoExpandT ps) a) => P (Do ps) a where
+  type PP (Do ps) a = PP (DoExpandT ps) a
+  eval _ = eval (Proxy @(DoExpandT ps))
+
+type family DoExpandT (ps :: [k]) :: Type where
+  DoExpandT '[] = GL.TypeError ('GL.Text "'[] invalid: requires at least one predicate in the list")
+  DoExpandT '[p] = Id >> p -- need this else fails cos 1 is nat and would mean that the result is nat not Type!
+  -- if p >> Id then turns TrueT to PresentT True
+  DoExpandT (p ': p1 ': ps) = p >> DoExpandT (p1 ': ps)
+
+-- | similar to 'Prelude.&&'
+--
+-- >>> pz @(Fst Id && Snd Id) (True, True)
+-- TrueT
+--
+-- >>> pz @(Id > 15 && Id < 17) 16
+-- TrueT
+--
+-- >>> pz @(Id > 15 && Id < 17) 30
+-- FalseT
+--
+-- >>> pz @(Fst Id && (Length (Snd Id) >= 4)) (True,[11,12,13,14])
+-- TrueT
+--
+-- >>> pz @(Fst Id && (Length (Snd Id) == 4)) (True,[12,11,12,13,14])
+-- FalseT
+--
+data p && q
+infixr 3 &&
+
+instance (P p a
+        , P q a
+        , PP p a ~ Bool
+        , PP q a ~ Bool
+        ) => P (p && q) a where
+  type PP (p && q) a = Bool
+  eval _ opts a = do
+    let msg0 = "&&"
+    lr <- runPQBool msg0 (Proxy @p) (Proxy @q) opts a []
+    pure $ case lr of
+      Left e -> e
+      Right (p,q,pp,qq) ->
+        let zz = case (p,q) of
+                  (True, True) -> ""
+                  (False, True) -> topMessage pp
+                  (True, False) -> topMessage qq
+                  (False, False) -> topMessage pp <> " " <> msg0 <> " " <> topMessage qq
+        in mkNodeB opts (p&&q) (showL opts p <> " " <> msg0 <> " " <> showL opts q <> (if null zz then zz else " | " <> zz)) [hh pp, hh qq]
+
+-- | short circuit version of boolean And
+--
+-- >>> pl @(Id > 10 &&~ Failt _ "ss") 9
+-- False (False &&~ _ | (9 > 10))
+-- FalseT
+--
+-- >>> pl @(Id > 10 &&~ Id == 12) 11
+-- False (True &&~ False | (11 == 12))
+-- FalseT
+--
+-- >>> pl @(Id > 10 &&~ Id == 11) 11
+-- True (True &&~ True)
+-- TrueT
+--
+data p &&~ q
+infixr 3 &&~
+
+instance (P p a
+        , P q a
+        , PP p a ~ Bool
+        , PP q a ~ Bool
+        ) => P (p &&~ q) a where
+  type PP (p &&~ q) a = Bool
+  eval _ opts a = do
+    let msg0 = "&&~"
+    pp <- eval (Proxy @p) opts a
+    case getValueLR opts msg0 pp [] of
+      Left e -> pure e
+      Right False ->
+        pure $ mkNodeB opts False ("False " <> msg0 <> " _" <> litVerbose opts " | " (topMessage pp)) [hh pp]
+      Right True -> do
+        qq <- eval (Proxy @q) opts a
+        pure $ case getValueLR opts msg0 qq [hh pp] of
+          Left e -> e
+          Right q ->
+            let zz = if q then ""
+                     else " | " <> topMessage qq
+            in mkNodeB opts q ("True " <> msg0 <> " " <> showL opts q <> litVerbose opts "" zz) [hh pp, hh qq]
+
+-- | similar to 'Prelude.||'
+--
+-- >>> pz @(Fst Id || (Length (Snd Id) >= 4)) (False,[11,12,13,14])
+-- TrueT
+--
+-- >>> pz @(Not (Fst Id) || (Length (Snd Id) == 4)) (True,[12,11,12,13,14])
+-- FalseT
+--
+data p || q
+infixr 2 ||
+
+instance (P p a
+        , P q a
+        , PP p a ~ Bool
+        , PP q a ~ Bool
+        ) => P (p || q) a where
+  type PP (p || q) a = Bool
+  eval _ opts a = do
+    let msg0 = "||"
+    lr <- runPQBool msg0 (Proxy @p) (Proxy @q) opts a []
+    pure $ case lr of
+      Left e -> e
+      Right (p,q,pp,qq) ->
+        let zz = case (p,q) of
+                  (False,False) -> " | " <> topMessage pp <> " " <> msg0 <> " " <> topMessage qq
+                  _ -> ""
+        in mkNodeB opts (p||q) (showL opts p <> " " <> msg0 <> " " <> showL opts q <> zz) [hh pp, hh qq]
+
+-- | short circuit version of boolean Or
+--
+-- >>> pl @(Id > 10 ||~ Failt _ "ss") 11
+-- True (True ||~ _ | (11 > 10))
+-- TrueT
+--
+-- >>> pz @(Id > 10 ||~ Id == 9) 9
+-- TrueT
+--
+-- >>> pl @(Id > 10 ||~ Id > 9) 9
+-- False (False ||~ False | (9 > 10) ||~ (9 > 9))
+-- FalseT
+--
+data p ||~ q
+infixr 2 ||~
+
+instance (P p a
+        , P q a
+        , PP p a ~ Bool
+        , PP q a ~ Bool
+        ) => P (p ||~ q) a where
+  type PP (p ||~ q) a = Bool
+  eval _ opts a = do
+    let msg0 = "||~"
+    pp <- eval (Proxy @p) opts a
+    case getValueLR opts msg0 pp [] of
+      Left e -> pure e
+      Right False -> do
+        qq <- eval (Proxy @q) opts a
+        pure $ case getValueLR opts msg0 qq [hh pp] of
+          Left e -> e
+          Right q ->
+            let zz = if q then ""
+                     else " | " <> topMessage pp <> " " <> msg0 <> " " <> topMessage qq
+            in mkNodeB opts q ("False " <> msg0 <> " " <> showL opts q <> litVerbose opts "" zz) [hh pp, hh qq]
+      Right True ->
+        pure $ mkNodeB opts True ("True " <> msg0 <> " _" <> litVerbose opts " | " (topMessage pp)) [hh pp]
+
+-- | boolean implication
+--
+-- >>> pz @(Fst Id ~> (Length (Snd Id) >= 4)) (True,[11,12,13,14])
+-- TrueT
+--
+-- >>> pz @(Fst Id ~> (Length (Snd Id) == 4)) (True,[12,11,12,13,14])
+-- FalseT
+--
+-- >>> pz @(Fst Id ~> (Length (Snd Id) == 4)) (False,[12,11,12,13,14])
+-- TrueT
+--
+-- >>> pz @(Fst Id ~> (Length (Snd Id) >= 4)) (False,[11,12,13,14])
+-- TrueT
+--
+data p ~> q
+infixr 1 ~>
+
+instance (P p a
+        , P q a
+        , PP p a ~ Bool
+        , PP q a ~ Bool
+        ) => P (p ~> q) a where
+  type PP (p ~> q) a = Bool
+  eval _ opts a = do
+    let msg0 = "~>"
+    lr <- runPQBool msg0 (Proxy @p) (Proxy @q) opts a []
+    pure $ case lr of
+      Left e -> e
+      Right (p,q,pp,qq) ->
+        let zz = case (p,q) of
+                  (True,False) -> topMessage pp <> " " <> msg0 <> " " <> topMessage qq
+                  _ -> ""
+        in mkNodeB opts (p~>q) (showL opts p <> " " <> msg0 <> " " <> showL opts q <> (if null zz then zz else " | " <> zz)) [hh pp, hh qq]
+
+
+-- | swaps using 'SwapC'
+--
+-- >>> pz @Swap (Left 123)
+-- PresentT (Right 123)
+--
+-- >>> pz @Swap (Right 123)
+-- PresentT (Left 123)
+--
+-- >>> pz @Swap (These 'x' 123)
+-- PresentT (These 123 'x')
+--
+-- >>> pz @Swap (This 'x')
+-- PresentT (That 'x')
+--
+-- >>> pz @Swap (That 123)
+-- PresentT (This 123)
+--
+-- >>> pz @Swap (123,'x')
+-- PresentT ('x',123)
+--
+-- >>> pz @Swap (Left "abc")
+-- PresentT (Right "abc")
+--
+-- >>> pz @Swap (Right 123)
+-- PresentT (Left 123)
+--
+-- >>> pl @Swap (Right "asfd")
+-- Present Left "asfd" (Swap Left "asfd" | Right "asfd")
+-- PresentT (Left "asfd")
+--
+-- >>> pl @Swap (12,"asfd")
+-- Present ("asfd",12) (Swap ("asfd",12) | (12,"asfd"))
+-- PresentT ("asfd",12)
+--
+
+data Swap
+
+class Bifunctor p => SwapC p where -- (p :: Type -> Type -> Type) where
+  swapC :: p a b -> p b a
+instance SwapC Either where
+  swapC (Left a) = Right a
+  swapC (Right a) = Left a
+instance SwapC These where
+  swapC (This a) = That a
+  swapC (That b) = This b
+  swapC (These a b) = These b a
+instance SwapC (,) where
+  swapC (a,b) = (b,a)
+
+instance (Show (p a b)
+        , SwapC p
+        , Show (p b a)
+        ) => P Swap (p a b) where
+  type PP Swap (p a b) = p b a
+  eval _ opts pabx =
+    let msg0 = "Swap"
+        d = swapC pabx
+    in pure $ mkNode opts (PresentT d) (show01 opts msg0 d pabx) []
+
+-- | like 'GHC.Base.$' for expressions
+--
+-- >>> pl @(Fst $ Snd $ Id) ((1,2),(3,4))
+-- Present 3 (Fst 3 | (3,4))
+-- PresentT 3
+--
+-- >>> pl @((<=) 4 $ Fst $ Snd $ Id) ((1,2),(3,4))
+-- False (4 <= 3)
+-- FalseT
+--
+data (p :: k -> k1) $ (q :: k)
+infixr 0 $
+
+instance P (p q) a => P (p $ q) a where
+  type PP (p $ q) a = PP (p q) a
+  eval _  = eval (Proxy @(p q))
+
+-- | similar to 'Control.Lens.&'
+--
+-- >>> pl @(Id & Fst & Singleton & Length) (13,"xyzw")
+-- Present 1 (Length 1 | [13])
+-- PresentT 1
+--
+-- >>> pl @(2 & (&&&) "abc") ()
+-- Present ("abc",2) (W '("abc",2))
+-- PresentT ("abc",2)
+--
+-- >>> pl @(2 & '(,) "abc") ()
+-- Present ("abc",2) ('("abc",2))
+-- PresentT ("abc",2)
+--
+-- >>> pl @('(,) 4 $ '(,) 7 $ "aa") ()
+-- Present (4,(7,"aa")) ('(4,(7,"aa")))
+-- PresentT (4,(7,"aa"))
+--
+-- >>> pl @(Thd $ Snd $ Fst Id) ((1,("W",9,'a')),(3,4))
+-- Present 'a' (Thd 'a' | ("W",9,'a'))
+-- PresentT 'a'
+--
+data (q :: k) & (p :: k -> k1)
+infixl 1 &
+
+instance P (p q) a => P (q & p) a where
+  type PP (q & p) a = PP (p q) a
+  eval _ = eval (Proxy @(p q))
+
+-- | similar to 'pure'
+--
+-- >>> pz @(Pure Maybe Id) 4
+-- PresentT (Just 4)
+--
+-- >>> pz @(Pure [] Id) 4
+-- PresentT [4]
+--
+-- >>> pz @(Pure (Either String) (Fst Id)) (13,True)
+-- PresentT (Right 13)
+--
+-- >>> pl @(Pure Maybe Id) 'x'
+-- Present Just 'x' (Pure Just 'x' | 'x')
+-- PresentT (Just 'x')
+--
+-- >>> pl @(Pure (Either _) Id) 'x'
+-- Present Right 'x' (Pure Right 'x' | 'x')
+-- PresentT (Right 'x')
+--
+-- >>> pl @(Pure (Either _) Id >> Swap) 'x'
+-- Present Left 'x' ((>>) Left 'x' | {Swap Left 'x' | Right 'x'})
+-- PresentT (Left 'x')
+--
+-- >>> pl @(Pure (Either ()) Id >> Swap) 'x'
+-- Present Left 'x' ((>>) Left 'x' | {Swap Left 'x' | Right 'x'})
+-- PresentT (Left 'x')
+--
+-- >>> pl @(Pure (Either String) Id >> Swap) 123
+-- Present Left 123 ((>>) Left 123 | {Swap Left 123 | Right 123})
+-- PresentT (Left 123)
+--
+data Pure (t :: Type -> Type) p
+instance (P p x
+        , Show (PP p x)
+        , Show (t (PP p x))
+        , Applicative t
+        ) => P (Pure t p) x where
+  type PP (Pure t p) x = t (PP p x)
+  eval _ opts x = do
+    let msg0 = "Pure"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right a ->
+        let b = pure a
+        in mkNode opts (PresentT b) (show01 opts msg0 b a) [hh pp]
+
+-- | similar to 'coerce'
+--
+-- >>> pz @(Coerce (SG.Sum Integer)) (Identity (-13))
+-- PresentT (Sum {getSum = -13})
+--
+-- >>> pl @(Coerce SG.Any) True
+-- Present Any {getAny = True} (Coerce Any {getAny = True} | True)
+-- PresentT (Any {getAny = True})
+--
+-- >>> pl @(Coerce Bool) (SG.Any True)
+-- Present True (Coerce True | Any {getAny = True})
+-- PresentT True
+--
+data Coerce (t :: k)
+
+instance (Show a
+        , Show t
+        , Coercible t a
+        ) => P (Coerce t) a where
+  type PP (Coerce t) a = t
+  eval _ opts a =
+    let msg0 = "Coerce"
+        d = a ^. coerced
+    in pure $ mkNode opts (PresentT d) (show01 opts msg0 d a) []
+
+

@@ -0,0 +1,472 @@+{-# OPTIONS -Wall #-}
+{-# OPTIONS -Wno-compat #-}
+{-# OPTIONS -Wincomplete-record-updates #-}
+{-# OPTIONS -Wincomplete-uni-patterns #-}
+{-# OPTIONS -Wredundant-constraints #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE NoOverloadedLists #-}
+{-# LANGUAGE NoStarIsType #-}
+{- |
+     promoted character functions
+-}
+module Predicate.Data.Char (
+ -- ** constructor
+    Char1
+
+ -- ** character predicates
+  , IsLower
+  , IsUpper
+  , IsDigit
+  , IsSpace
+  , IsPunctuation
+  , IsControl
+  , IsHexDigit
+  , IsOctDigit
+  , IsSeparator
+  , IsLatin1
+
+ -- ** string predicates
+  , IsLowerAll
+  , IsUpperAll
+  , IsDigitAll
+  , IsSpaceAll
+  , IsPunctuationAll
+  , IsControlAll
+  , IsHexDigitAll
+  , IsOctDigitAll
+  , IsSeparatorAll
+  , IsLatin1All
+ -- ** change case
+  , ToTitle
+  , ToUpper
+  , ToLower
+ ) where
+import Predicate.Core
+import Predicate.Util
+import Control.Lens hiding (iall)
+import qualified Data.Text.Lens as DTL
+import GHC.TypeLits (Symbol, KnownSymbol)
+import qualified GHC.TypeLits as GL
+import Data.Proxy
+import Data.Char
+
+-- $setup
+-- >>> :set -XDataKinds
+-- >>> :set -XTypeApplications
+-- >>> :set -XTypeOperators
+-- >>> :set -XOverloadedStrings
+-- >>> :set -XNoOverloadedLists
+-- >>> import qualified Data.Text as T
+-- >>> import Predicate.Prelude
+
+-- | extracts the first character from a non empty 'GHC.TypeLits.Symbol'
+--
+-- >>> pz @(Char1 "aBc") ()
+-- PresentT 'a'
+--
+data Char1 (s :: Symbol)  -- gets the first char from the Symbol [requires that Symbol is not empty]
+instance ( KnownSymbol s
+         , GL.CmpSymbol s "" ~ 'GT
+         ) => P (Char1 s) a where
+  type PP (Char1 s) a = Char
+  eval _ opts _ =
+     case symb @s of
+       [] -> errorInProgram "Char1: found empty Symbol/string"
+       c:_ -> pure $ mkNode opts (PresentT c) ("Char1 " <> showL opts c) []
+
+
+-- | a predicate for determining if a character belongs to the given character set
+--
+-- >>> pz @(Map '(IsControl, IsLatin1, IsHexDigit, IsOctDigit, IsDigit, IsPunctuation, IsSeparator, IsSpace) Id) "abc134"
+-- PresentT [(False,True,True,False,False,False,False,False),(False,True,True,False,False,False,False,False),(False,True,True,False,False,False,False,False),(False,True,True,True,True,False,False,False),(False,True,True,True,True,False,False,False),(False,True,True,True,True,False,False,False)]
+--
+data IsCharSet (cs :: CharSet)
+
+instance ( x ~ Char
+         , GetCharSet cs
+         ) => P (IsCharSet cs) x where
+  type PP (IsCharSet cs) x = Bool
+  eval _ opts c =
+    let msg0 = "Is" ++ drop 1 (show cs)
+        (cs,f) = getCharSet @cs
+        b = f c
+    in pure $ mkNodeB opts b (msg0 <> showVerbose opts " | " [c]) []
+
+-- | predicate similar to 'Data.Char.isLower'
+--
+-- >>> pz @IsLower 'X'
+-- FalseT
+--
+-- >>> pz @IsLower '1'
+-- FalseT
+--
+-- >>> pz @IsLower 'a'
+-- TrueT
+--
+
+data IsLower
+type IsLowerT = IsCharSet 'CLower
+
+instance P IsLowerT x => P IsLower x where
+  type PP IsLower x = PP IsLowerT x
+  eval _ = evalBool (Proxy @IsLowerT)
+
+-- | predicate similar to 'Data.Char.isUpper'
+--
+data IsUpper
+type IsUpperT = IsCharSet 'CUpper
+
+instance P IsUpperT x => P IsUpper x where
+  type PP IsUpper x = PP IsUpperT x
+  eval _ = evalBool (Proxy @IsUpperT)
+
+-- | predicate similar to 'Data.Char.isDigit'
+--
+-- >>> pz @IsDigit 'g'
+-- FalseT
+--
+-- >>> pz @IsDigit '9'
+-- TrueT
+--
+data IsDigit
+type IsDigitT = IsCharSet 'CNumber
+instance P IsDigitT x => P IsDigit x where
+  type PP IsDigit x = Bool
+  eval _ = evalBool (Proxy @IsDigitT)
+
+-- | predicate similar to 'Data.Char.isSpace'
+--
+-- >>> pz @IsSpace '\t'
+-- TrueT
+--
+-- >>> pz @IsSpace ' '
+-- TrueT
+--
+-- >>> pz @IsSpace 'x'
+-- FalseT
+--
+data IsSpace
+type IsSpaceT = IsCharSet 'CSpace
+instance P IsSpaceT x => P IsSpace x where
+  type PP IsSpace x = Bool
+  eval _ = evalBool (Proxy @IsSpaceT)
+
+-- | predicate similar to 'Data.Char.isPunctuation'
+--
+data IsPunctuation
+type IsPunctuationT = IsCharSet 'CPunctuation
+instance P IsPunctuationT x => P IsPunctuation x where
+  type PP IsPunctuation x = Bool
+  eval _ = evalBool (Proxy @IsPunctuationT)
+
+-- | predicate similar to 'Data.Char.isControl'
+--
+data IsControl
+type IsControlT = IsCharSet 'CControl
+instance P IsControlT x => P IsControl x where
+  type PP IsControl x = Bool
+  eval _ = evalBool (Proxy @IsControlT)
+
+-- | predicate similar to 'Data.Char.isHexDigit'
+--
+-- >>> pz @IsHexDigit 'A'
+-- TrueT
+--
+-- >>> pz @IsHexDigit 'g'
+-- FalseT
+--
+data IsHexDigit
+type IsHexDigitT = IsCharSet 'CHexDigit
+instance P IsHexDigitT x => P IsHexDigit x where
+  type PP IsHexDigit x = Bool
+  eval _ = evalBool (Proxy @IsHexDigitT)
+
+-- | predicate similar to 'Data.Char.isOctDigit'
+--
+data IsOctDigit
+type IsOctDigitT = IsCharSet 'COctDigit
+instance P IsOctDigitT x => P IsOctDigit x where
+  type PP IsOctDigit x = Bool
+  eval _ = evalBool (Proxy @IsOctDigitT)
+
+-- | predicate similar to 'Data.Char.isSeparator'
+--
+data IsSeparator
+type IsSeparatorT = IsCharSet 'CSeparator
+instance P IsSeparatorT x => P IsSeparator x where
+  type PP IsSeparator x = Bool
+  eval _ = evalBool (Proxy @IsSeparatorT)
+
+-- | predicate similar to 'Data.Char.isLatin1'
+--
+data IsLatin1
+type IsLatin1T = IsCharSet 'CLatin1
+instance P IsLatin1T x => P IsLatin1 x where
+  type PP IsLatin1 x = Bool
+  eval _ = evalBool (Proxy @IsLatin1T)
+
+
+-- | a predicate for determining if a string 'Data.Text.IsText' belongs to the given character set
+--
+-- >>> pl @('Just Uncons >> IsUpper &* IsLowerAll) "AbcdE"
+-- False ((>>) False | {True (&*) False | (IsLowerAll | "bcdE")})
+-- FalseT
+--
+-- >>> pl @('Just Uncons >> IsUpper &* IsLowerAll) "Abcde"
+-- True ((>>) True | {True (&*) True})
+-- TrueT
+--
+-- >>> pl @('Just Uncons >> IsUpper &* IsLowerAll) "xbcde"
+-- False ((>>) False | {False (&*) True | (IsUpper | "x")})
+-- FalseT
+--
+-- >>> pl @('Just Uncons >> IsUpper &* IsLowerAll) "X"
+-- True ((>>) True | {True (&*) True})
+-- TrueT
+--
+-- >>> pz @( '(IsControlAll, IsLatin1All , IsHexDigitAll , IsOctDigitAll , IsDigitAll , IsPunctuationAll , IsSeparatorAll , IsSpaceAll)) "abc134"
+-- PresentT (False,True,True,False,False,False,False,False)
+--
+-- >>> pl @(SplitAts [1,2,10] Id >> Para '[IsLowerAll, IsDigitAll, IsUpperAll]) "abdefghi"
+-- Present [True,False,False] ((>>) [True,False,False] | {Para(0) [True,False,False] | ["a","bd","efghi"]})
+-- PresentT [True,False,False]
+--
+-- >>> pl @(SplitAts [1,2,10] Id >> BoolsQuick "" '[IsLowerAll, IsDigitAll, IsUpperAll]) "a98efghi"
+-- False ((>>) False | {Bool(2) [] (IsUpperAll | "efghi")})
+-- FalseT
+--
+-- >>> pl @(SplitAts [1,2,10] Id >> BoolsQuick "" '[IsLowerAll, IsDigitAll, IsUpperAll || IsLowerAll]) "a98efghi"
+-- True ((>>) True | {Bools})
+-- TrueT
+--
+-- >>> pl @(SplitAts [1,2,10] Id >> BoolsQuick "" '[IsLowerAll, IsDigitAll, IsUpperAll || IsLowerAll]) "a98efgHi"
+-- False ((>>) False | {Bool(2) [] (False || False | (IsUpperAll | "efgHi") || (IsLowerAll | "efgHi"))})
+-- FalseT
+--
+data IsCharSetAll (cs :: CharSet)
+
+instance (GetCharSet cs
+        , Show a
+        , DTL.IsText a
+        ) => P (IsCharSetAll cs) a where
+  type PP (IsCharSetAll cs) a = Bool
+  eval _ opts as =
+    let b = allOf DTL.text f as
+        msg0 = "Is" ++ drop 1 (show cs) ++ "All"
+        (cs,f) = getCharSet @cs
+    in pure $ mkNodeB opts b (msg0 <> showVerbose opts " | " as) []
+
+data CharSet = CLower
+             | CUpper
+             | CNumber
+             | CSpace
+             | CPunctuation
+             | CControl
+             | CHexDigit
+             | COctDigit
+             | CSeparator
+             | CLatin1
+             deriving Show
+
+class GetCharSet (cs :: CharSet) where
+  getCharSet :: (CharSet, Char -> Bool)
+instance GetCharSet 'CLower where
+  getCharSet = (CLower, isLower)
+instance GetCharSet 'CUpper where
+  getCharSet = (CUpper, isUpper)
+instance GetCharSet 'CNumber where
+  getCharSet = (CNumber, isNumber)
+instance GetCharSet 'CSpace where
+  getCharSet = (CSpace, isSpace)
+instance GetCharSet 'CPunctuation where
+  getCharSet = (CPunctuation, isPunctuation)
+instance GetCharSet 'CControl where
+  getCharSet = (CControl, isControl)
+instance GetCharSet 'CHexDigit where
+  getCharSet = (CHexDigit, isHexDigit)
+instance GetCharSet 'COctDigit where
+  getCharSet = (COctDigit, isOctDigit)
+instance GetCharSet 'CSeparator where
+  getCharSet = (CSeparator, isSeparator)
+instance GetCharSet 'CLatin1 where
+  getCharSet = (CLatin1, isLatin1)
+
+-- | predicate for determining if a string is all lowercase
+--
+-- >>> pz @IsLowerAll "abc"
+-- TrueT
+--
+-- >>> pz @IsLowerAll "abcX"
+-- FalseT
+--
+-- >>> pz @IsLowerAll (T.pack "abcX")
+-- FalseT
+--
+-- >>> pz @IsLowerAll "abcdef213"
+-- FalseT
+--
+-- >>> pz @IsLowerAll ""
+-- TrueT
+--
+data IsLowerAll
+type IsLowerAllT = IsCharSetAll 'CLower
+
+instance P IsLowerAllT x => P IsLowerAll x where
+  type PP IsLowerAll x = PP IsLowerAllT x
+  eval _ = evalBool (Proxy @IsLowerAllT)
+
+data IsUpperAll
+type IsUpperAllT = IsCharSetAll 'CUpper
+
+instance P IsUpperAllT x => P IsUpperAll x where
+  type PP IsUpperAll x = PP IsUpperAllT x
+  eval _ = evalBool (Proxy @IsUpperAllT)
+
+-- | predicate for determining if the string is all digits
+--
+-- >>> pz @IsDigitAll "213G"
+-- FalseT
+--
+-- >>> pz @IsDigitAll "929"
+-- TrueT
+--
+data IsDigitAll
+type IsDigitAllT = IsCharSetAll 'CNumber
+instance P IsDigitAllT x => P IsDigitAll x where
+  type PP IsDigitAll x = Bool
+  eval _ = evalBool (Proxy @IsDigitAllT)
+
+-- | predicate for determining if the string is all spaces
+--
+-- >>> pz @IsSpaceAll "213G"
+-- FalseT
+--
+-- >>> pz @IsSpaceAll "    "
+-- TrueT
+--
+-- >>> pz @IsSpaceAll ""
+-- TrueT
+--
+data IsSpaceAll
+type IsSpaceAllT = IsCharSetAll 'CSpace
+instance P IsSpaceAllT x => P IsSpaceAll x where
+  type PP IsSpaceAll x = Bool
+  eval _ = evalBool (Proxy @IsSpaceAllT)
+
+data IsPunctuationAll
+type IsPunctuationAllT = IsCharSetAll 'CPunctuation
+instance P IsPunctuationAllT x => P IsPunctuationAll x where
+  type PP IsPunctuationAll x = Bool
+  eval _ = evalBool (Proxy @IsPunctuationAllT)
+
+data IsControlAll
+type IsControlAllT = IsCharSetAll 'CControl
+instance P IsControlAllT x => P IsControlAll x where
+  type PP IsControlAll x = Bool
+  eval _ = evalBool (Proxy @IsControlAllT)
+
+-- | predicate for determining if the string is all hex digits
+--
+-- >>> pz @IsHexDigitAll "01efA"
+-- TrueT
+--
+-- >>> pz @IsHexDigitAll "01egfA"
+-- FalseT
+--
+data IsHexDigitAll
+type IsHexDigitAllT = IsCharSetAll 'CHexDigit
+instance P IsHexDigitAllT x => P IsHexDigitAll x where
+  type PP IsHexDigitAll x = Bool
+  eval _ = evalBool (Proxy @IsHexDigitAllT)
+
+data IsOctDigitAll
+type IsOctDigitAllT = IsCharSetAll 'COctDigit
+instance P IsOctDigitAllT x => P IsOctDigitAll x where
+  type PP IsOctDigitAll x = Bool
+  eval _ = evalBool (Proxy @IsOctDigitAllT)
+
+data IsSeparatorAll
+type IsSeparatorAllT = IsCharSetAll 'CSeparator
+instance P IsSeparatorAllT x => P IsSeparatorAll x where
+  type PP IsSeparatorAll x = Bool
+  eval _ = evalBool (Proxy @IsSeparatorAllT)
+
+data IsLatin1All
+type IsLatin1AllT = IsCharSetAll 'CLatin1
+instance P IsLatin1AllT x => P IsLatin1All x where
+  type PP IsLatin1All x = Bool
+  eval _ = evalBool (Proxy @IsLatin1AllT)
+
+
+-- | converts a string 'Data.Text.Lens.IsText' value to lower case
+--
+-- >>> pz @ToLower "HeLlO wOrld!"
+-- PresentT "hello world!"
+--
+data ToLower
+
+instance ( Show a
+         , DTL.IsText a
+         ) => P ToLower a where
+  type PP ToLower a = a
+  eval _ opts as =
+    let msg0 = "ToLower"
+        xs = as & DTL.text %~ toLower
+    in pure $ mkNode opts (PresentT xs) (show01 opts msg0 xs as) []
+
+-- | converts a string 'Data.Text.Lens.IsText' value to upper case
+--
+-- >>> pz @ToUpper "HeLlO wOrld!"
+-- PresentT "HELLO WORLD!"
+--
+data ToUpper
+
+instance ( Show a
+         , DTL.IsText a
+         ) => P ToUpper a where
+  type PP ToUpper a = a
+  eval _ opts as =
+    let msg0 = "ToUpper"
+        xs = as & DTL.text %~ toUpper
+    in pure $ mkNode opts (PresentT xs) (show01 opts msg0 xs as) []
+
+
+-- | converts a string 'Data.Text.Lens.IsText' value to title case
+--
+-- >>> pz @ToTitle "HeLlO wOrld!"
+-- PresentT "Hello world!"
+--
+-- >>> data Color = Red | White | Blue | Green | Black deriving (Show,Eq,Enum,Bounded,Read)
+-- >>> pz @(ToTitle >> ReadP Color Id) "red"
+-- PresentT Red
+--
+data ToTitle
+
+instance ( Show a
+         , DTL.IsText a
+         ) => P ToTitle a where
+  type PP ToTitle a = a
+  eval _ opts as =
+    let msg0 = "ToTitle"
+        xs = toTitleAll (as ^. DTL.unpacked) ^. DTL.packed
+    in pure $ mkNode opts (PresentT xs) (show01 opts msg0 xs as) []
+
+
+toTitleAll :: String -> String
+toTitleAll (x:xs) = toUpper x : map toLower xs
+toTitleAll [] = []
+

@@ -0,0 +1,921 @@+{-# OPTIONS -Wall #-}
+{-# OPTIONS -Wno-compat #-}
+{-# OPTIONS -Wincomplete-record-updates #-}
+{-# OPTIONS -Wincomplete-uni-patterns #-}
+{-# OPTIONS -Wredundant-constraints #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE NoOverloadedLists #-}
+{-# LANGUAGE NoStarIsType #-}
+{- |
+     promoted conditional functions
+-}
+module Predicate.Data.Condition (
+  -- ** conditional expressions
+    If
+  , Case
+  , Case'
+  , Case''
+  , Guards
+  , GuardsQuick
+  , Guard
+  , ExitWhen
+  , GuardSimple
+  , GuardsN
+  , GuardsDetail
+
+  , Bools
+  , BoolsQuick
+  , BoolsN
+
+ ) where
+import Predicate.Core
+import Predicate.Util
+import Predicate.Data.ReadShow (PrintT)
+import GHC.TypeLits (Nat,KnownNat,ErrorMessage((:<>:)))
+import qualified GHC.TypeLits as GL
+import Control.Lens hiding (iall)
+import Data.Proxy
+import Data.Kind (Type)
+import Data.Void
+import qualified Data.Type.Equality as DE
+
+-- $setup
+-- >>> import Predicate.Prelude
+-- >>> :set -XDataKinds
+-- >>> :set -XTypeApplications
+-- >>> :set -XTypeOperators
+-- >>> :set -XAllowAmbiguousTypes
+-- >>> :set -XOverloadedStrings
+-- >>> :set -XNoOverloadedLists
+-- >>> :set -XFlexibleContexts
+-- >>> import qualified Data.Text as T
+
+
+-- | similar to an if statement: if \'p\' then run \'q\' else run \'r\'
+--
+-- >>> pz @(If (Gt 4) "greater than 4" "less than or equal to 4") 10
+-- PresentT "greater than 4"
+--
+-- >>> pz @(If (Gt 4) "greater than 4" "less than or equal to 4") 0
+-- PresentT "less than or equal to 4"
+--
+-- >>> pz @(If (Snd Id == "a") '("xxx",Fst Id + 13) (If (Snd Id == "b") '("yyy",Fst Id + 7) (Failt _ "oops"))) (99,"b")
+-- PresentT ("yyy",106)
+--
+-- >>> pl @(If (Len > 2) (Map (Succ Id) Id) (FailS "someval")) [12,15,16]
+-- Present [13,16,17] (If (true cond))
+-- PresentT [13,16,17]
+--
+-- >>> pl @(Map (If (Lt 3) 'True (Failt _ "err")) Id) [1..10]
+-- Error err(8) (Map(i=2, a=3) excnt=8)
+-- FailT "err(8)"
+--
+-- >>> pl @(Map (If (Lt 3) 'True (Failt _ "someval")) Id) [1..10]
+-- Error someval(8) (Map(i=2, a=3) excnt=8)
+-- FailT "someval(8)"
+--
+-- >>> pl @(Map (If (Lt 3) 'True 'False) Id) [1..5]
+-- Present [True,True,False,False,False] (Map [True,True,False,False,False] | [1,2,3,4,5])
+-- PresentT [True,True,False,False,False]
+--
+-- >>> pl @(If (Gt 4) (Fail (Hole _) (PrintF "failing with %d" Id)) ()) 45
+-- Error failing with 45 (If [True])
+-- FailT "failing with 45"
+--
+-- >>> pl @(If (Gt 4) (Fail (Hole _) (PrintF "failing with %d" Id)) (Id * 7)) 3
+-- Present 21 (If (false cond) 21)
+-- PresentT 21
+--
+-- >>> pl @(If (Gt 4) (Fail (Hole _) (PrintF "failing with %d" Id)) (Id * 7 >> ShowP Id >> Ones Id)) 3
+-- Present ["2","1"] (If (false cond) ["2","1"])
+-- PresentT ["2","1"]
+--
+-- >>> pl @(If (Gt 4) (Fail (Hole _) (PrintF "failing with %d" Id)) (ShowP (Id * 7) >> Ones Id)) 19
+-- Error failing with 19 (If [True])
+-- FailT "failing with 19"
+--
+data If p q r
+
+instance (Show (PP r a)
+        , P p a
+        , PP p a ~ Bool
+        , P q a
+        , P r a
+        , PP q a ~ PP r a
+        ) => P (If p q r) a where
+  type PP (If p q r) a = PP q a
+  eval _ opts a = do
+    let msg0 = "If"
+    pp <- evalBool (Proxy @p) opts a
+    case getValueLR opts (msg0 <> " condition failed") pp [] of
+      Left e -> pure e
+      Right b -> do
+        qqrr <- if b
+              then eval (Proxy @q) opts a
+              else eval (Proxy @r) opts a
+        pure $ case getValueLR opts (msg0 <> " [" <> show b <> "]") qqrr [hh pp, hh qqrr] of
+          Left e -> e
+          Right ret -> mkNode opts (_tBool qqrr) (msg0 <> " " <> if b then "(true cond)" else "(false cond) " <> showL opts ret) [hh pp, hh qqrr]
+
+type family GuardsT (ps :: [k]) where
+  GuardsT '[] = '[]
+  GuardsT (p ': ps) = Guard "fromGuardsT" p ': GuardsT ps
+
+--type Guards' (ps :: [k]) = Para (GuardsT ps)
+
+--type ToGuards (prt :: k) (os :: [k1]) = Proxy (Guards (ToGuardsT prt os))
+
+type family ToGuardsT (prt :: k) (os :: [k1]) :: [(k,k1)] where
+  ToGuardsT prt '[] = GL.TypeError ('GL.Text "ToGuardsT cannot be empty")
+  ToGuardsT prt '[p] = '(prt,p) : '[]
+  ToGuardsT prt (p ': ps) = '(prt,p) ': ToGuardsT prt ps
+
+-- | tries each predicate ps and on the first match runs the corresponding qs but if there is no match on ps then runs the fail case e
+--
+-- >>> pz @(Case (Failt _ "asdf") '[Lt 4,Lt 10,Same 50] '[PrintF "%d is lt4" Id, PrintF "%d is lt10" Id, PrintF "%d is same50" Id] Id) 50
+-- PresentT "50 is same50"
+--
+-- >>> pz @(Case (Failt _ "asdf") '[Lt 4,Lt 10,Same 50] '[PrintF "%d is lt4" Id, PrintF "%d is lt10" Id, PrintF "%d is same50" Id] Id) 9
+-- PresentT "9 is lt10"
+--
+-- >>> pz @(Case (Failt _ "asdf") '[Lt 4,Lt 10,Same 50] '[PrintF "%d is lt4" Id, PrintF "%d is lt10" Id, PrintF "%d is same50" Id] Id) 3
+-- PresentT "3 is lt4"
+--
+-- >>> pz @(Case (Failt _ "asdf") '[Lt 4,Lt 10,Same 50] '[PrintF "%d is lt4" Id, PrintF "%d is lt10" Id, PrintF "%d is same50" Id] Id) 99
+-- FailT "asdf"
+--
+-- >>> pz @(Case (FailS "asdf" >> Snd Id >> Unproxy) '[Lt 4,Lt 10,Same 50] '[PrintF "%d is lt4" Id, PrintF "%d is lt10" Id, PrintF "%d is same50" Id] Id) 99
+-- FailT "asdf"
+--
+-- >>> pz @(Case (Failt _ "x") '[Same "a",Same "b"] '["hey","there"] Id) "b"
+-- PresentT "there"
+--
+-- >>> pz @(Case (Failt _ "x") '[Id == "a",Id == "b"] '["hey","there"] Id) "a"
+-- PresentT "hey"
+--
+-- >>> pz @(Case (Failt _ "x") '[Same "a",Same "b"] '["hey","there"] Id) "c"
+-- FailT "x"
+--
+data CaseImpl (n :: Nat) (e :: k0) (ps :: [k]) (qs :: [k1]) (r :: k2)
+-- ps = conditions
+-- qs = what to do [one to one with ps]
+-- r = the value
+-- e = otherwise  -- leave til later
+
+-- | tries to match the value \'r\' with a condition in \'ps\' and if there is a match calls the associated \'qs\' entry else run \'e\'
+--
+-- >>> pl @(Case (Snd Id >> Failp "xx") '[Gt 3, Lt 2, Same 3] '["gt3","lt2","eq3"] Id) 15
+-- Present "gt3" (Case(0 of 3) "gt3" | 15)
+-- PresentT "gt3"
+--
+-- >>> pl @(Case (Snd Id >> Failp "xx") '[Gt 3, Lt 2, Same 3] '["gt3","lt2","eq3"] Id) 1
+-- Present "lt2" (Case(0) "lt2" | 1)
+-- PresentT "lt2"
+--
+-- >>> pl @(Case (Snd Id >> Failp "xx") '[Gt 3, Lt 2, Same 3] '["gt3","lt2","eq3"] Id) 3
+-- Present "eq3" (Case(0) "eq3" | 3)
+-- PresentT "eq3"
+--
+-- >>> pl @(Case (Snd Id >> Failp "no match") '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 15
+-- Error no match (Case(0) failed rhs)
+-- FailT "no match"
+--
+-- >>> pl @(Case (Fail (Snd Id >> Unproxy) (PrintF "no match for %03d" (Fst Id))) '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 15
+-- Error no match for 015 (Case(0) failed rhs)
+-- FailT "no match for 015"
+--
+-- >>> pl @(Case "other" '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 15
+-- Present "other" (Case(0) "other" | 15)
+-- PresentT "other"
+--
+-- >>> pl @(Case (ShowP (Fst Id) >> Id <> Id <> Id) '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 15
+-- Present "151515" (Case(0) "151515" | 15)
+-- PresentT "151515"
+--
+data Case (e :: k0) (ps :: [k]) (qs :: [k1]) (r :: k2)
+
+-- | like 'Case' but uses a generic error message (skips the \'e\' parameter)
+--
+-- >>> pl @(Case' '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 15
+-- Error Case:no match (Case(0) failed rhs)
+-- FailT "Case:no match"
+--
+data Case' (ps :: [k]) (qs :: [k1]) (r :: k2)
+
+-- | like 'Case' but allows you to use the value in the error message
+--
+-- >>> pl @(Case'' (PrintF "no match for %03d" Id) '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 15
+-- Error no match for 015 (Case(0) failed rhs)
+-- FailT "no match for 015"
+--
+-- >>> pl @(Case'' (PrintF "no match for %03d" Id) '[Same 1, Same 2, Same 3] '["eq1","eq2","eq3"] Id) 15
+-- Error no match for 015 (Case(0) failed rhs)
+-- FailT "no match for 015"
+--
+-- >>> pl @(Case'' (PrintF "no match for %04d" Id) '[Between 0 5 Id, Same 6, Between 7 10 Id] '[ 'LT, 'EQ, 'GT] Id) (-12)
+-- Error no match for -012 (Case(0) failed rhs)
+-- FailT "no match for -012"
+--
+data Case'' s (ps :: [k]) (qs :: [k1]) (r :: k2)
+
+type CaseT' (ps :: [k]) (qs :: [k1]) (r :: k2) = Case (Snd Id >> Failp "Case:no match") ps qs r
+type CaseT'' s (ps :: [k]) (qs :: [k1]) (r :: k2) = Case (FailCaseT s) ps qs r -- eg s= PrintF "%s" (ShowP Id)
+
+instance P (CaseT'' s ps qs r) x => P (Case'' s ps qs r) x where
+  type PP (Case'' s ps qs r) x = PP (CaseT'' s ps qs r) x
+  eval _ = eval (Proxy @(CaseT'' s ps qs r))
+
+instance P (CaseT' ps qs r) x => P (Case' ps qs r) x where
+  type PP (Case' ps qs r) x = PP (CaseT' ps qs r) x
+  eval _ = eval (Proxy @(CaseT' ps qs r))
+
+type FailCaseT p = Fail (Snd Id >> Unproxy) (Fst Id >> p)
+
+type CaseImplT e ps qs r = CaseImpl (LenT ps) e ps qs r
+
+-- passthru but adds the length of ps (replaces LenT in the type synonym to avoid type synonyms being expanded out
+instance (FailUnlessT (LenT ps DE.== LenT qs)
+                  ('GL.Text "lengths are not the same "
+                   ':<>: 'GL.ShowType (LenT ps)
+                   ':<>: 'GL.Text " vs "
+                   ':<>: 'GL.ShowType (LenT qs))
+        , P (CaseImplT e ps qs r) x
+        ) => P (Case e ps qs r) x where
+  type PP (Case e ps qs r) x = PP (CaseImplT e ps qs r) x
+  eval _ = eval (Proxy @(CaseImplT e ps qs r))
+
+-- only allow non empty lists!
+instance (GL.TypeError ('GL.Text "CaseImpl '[] invalid: lhs requires at least one value in the list"))
+   => P (CaseImpl n e ('[] :: [k]) (q ': qs) r) x where
+  type PP (CaseImpl n e ('[] :: [k]) (q ': qs) r) x = Void
+  eval _ _ _ = errorInProgram "CaseImpl lhs empty"
+
+instance (GL.TypeError ('GL.Text "CaseImpl '[] invalid: rhs requires at least one value in the list"))
+   => P (CaseImpl n e (p ': ps) ('[] :: [k1]) r) x where
+  type PP (CaseImpl n e (p ': ps) ('[] :: [k1]) r) x = Void
+  eval _ _ _ = errorInProgram "CaseImpl rhs empty"
+
+instance (GL.TypeError ('GL.Text "CaseImpl '[] invalid: lists are both empty"))
+   => P (CaseImpl n e ('[] :: [k]) ('[] :: [k1]) r) x where
+  type PP (CaseImpl n e ('[] :: [k]) ('[] :: [k1]) r) x = Void
+  eval _ _ _ = errorInProgram "CaseImpl both lists empty"
+
+instance (P r x
+        , P q (PP r x)
+        , Show (PP q (PP r x))
+        , P p (PP r x)
+        , PP p (PP r x) ~ Bool
+        , KnownNat n
+        , Show (PP r x)
+        , P e (PP r x, Proxy (PP q (PP r x)))
+        , PP e (PP r x, Proxy (PP q (PP r x))) ~ PP q (PP r x)
+        ) => P (CaseImpl n e '[p] '[q] r) x where
+  type PP (CaseImpl n e '[p] '[q] r) x = PP q (PP r x)
+  eval _ opts z = do
+    let msgbase0 = "Case(" <> show n <> ")"
+        n :: Int = nat @n
+    rr <- eval (Proxy @r) opts z
+    case getValueLR opts msgbase0 rr [] of
+      Left e -> pure e
+      Right a -> do
+        pp <- evalBool (Proxy @p) opts a
+        case getValueLR opts msgbase0 pp [hh rr] of
+          Left e -> pure e
+          Right True -> do
+            qq <- eval (Proxy @q) opts a
+            pure $ case getValueLR opts msgbase0 qq [hh rr, hh pp] of
+              Left e -> e
+              Right b -> mkNode opts (PresentT b) (show01 opts msgbase0 b a) (hh rr : hh pp : [hh qq | isVerbose opts])
+          Right False -> do
+            ee <- eval (Proxy @e) opts (a, Proxy @(PP q (PP r x)))
+            pure $ case getValueLR opts (msgbase0 <> "  otherwise failed") ee [hh rr, hh pp] of
+              Left e -> e
+              Right b -> mkNode opts (PresentT b) (show01 opts msgbase0 b a) [hh rr, hh pp, hh ee]
+
+instance (KnownNat n
+        , GetLen ps
+        , P r x
+        , P p (PP r x)
+        , P q (PP r x)
+        , PP p (PP r x) ~ Bool
+        , Show (PP q (PP r x))
+        , Show (PP r x)
+        , P (CaseImpl n e (p1 ': ps) (q1 ': qs) r) x
+        , PP (CaseImpl n e (p1 ': ps) (q1 ': qs) r) x ~ PP q (PP r x)
+        )
+     => P (CaseImpl n e (p ': p1 ': ps) (q ': q1 ': qs) r) x where
+  type PP (CaseImpl n e (p ': p1 ': ps) (q ': q1 ': qs) r) x = PP q (PP r x)
+  eval _ opts z = do
+    let cpos = n-pos-1
+        msgbase0 = msgbase2 <> "(" <> showIndex cpos <> " of " <> show n <> ")"
+        msgbase1 = msgbase2 <> "(" <> showIndex cpos <> ")"
+        msgbase2 = "Case"
+        n = nat @n
+        pos = 1 + getLen @ps -- cos p1!
+    rr <- eval (Proxy @r) opts z
+    case getValueLR opts msgbase0 rr [] of
+      Left e -> pure e
+      Right a -> do
+        pp <- evalBool (Proxy @p) opts a
+        case getValueLR opts msgbase0 pp [hh rr] of
+          Left e -> pure e
+          Right True -> do
+            qq <- eval (Proxy @q) opts a
+            pure $ case getValueLR opts msgbase0 qq [hh pp, hh rr] of
+              Left e -> e
+              Right b -> mkNode opts (PresentT b) (show01 opts msgbase0 b a) (hh rr : hh pp : [hh qq | isVerbose opts])
+          Right False -> do
+            ww <- eval (Proxy @(CaseImpl n e (p1 ': ps) (q1 ': qs) r)) opts z
+            pure $ case getValueLR opts (msgbase1 <> " failed rhs") ww [hh rr, hh pp] of
+              Left e -> e
+              Right b -> mkNode opts (PresentT b) (show01 opts msgbase1 b a) [hh rr, hh pp, hh ww]
+
+
+data GuardsImpl (n :: Nat) (os :: [(k,k1)])
+
+-- isbn 10 tests (dont need first guard as Zip enforces same length: handles case insensitive \'x\' as check digit)
+
+
+-- | Guards contain a type level list of tuples the action to run on failure of the predicate and the predicate itself
+--   Each tuple validating against the corresponding value in a value list
+--
+-- \'prt\' receives (Int,a) as input which is the position and value if there is a failure
+--
+-- >>> pz @(Guards '[ '("arg1 failed",Gt 4), '("arg2 failed", Same 4)]) [17,4]
+-- PresentT [17,4]
+--
+-- >>> pz @(Guards '[ '("arg1 failed",Gt 4), '("arg2 failed", Same 5)]) [17,4]
+-- FailT "arg2 failed"
+--
+-- >>> pz @(Guards '[ '("arg1 failed",Gt 99), '("arg2 failed", Same 4)]) [17,4]
+-- FailT "arg1 failed"
+--
+-- >>> pz @(Guards '[ '(PrintT "arg %d failed with value %d" Id,Gt 4), '(PrintT "%d %d" Id, Same 4)]) [17,3]
+-- FailT "1 3"
+--
+-- >>> pz @(Msg "isbn10" (Resplit "-" Id) >> Concat Id >> 'Just Unsnoc >> Map (ReadP Int (Singleton Id)) Id *** If (Singleton Id ==~ "X") 10 (ReadP Int (Singleton Id)) >> Zip (1...10 >> Reverse) (Fst Id +: Snd Id) >> Map (Fst Id * Snd Id) Id >> Sum >> Guard ("mod 0 oops") (Id `Mod` 11 == 0)) "0-306-40614-X"
+-- FailT "mod 0 oops"
+--
+-- >>> pz @(Resplit "-" Id >> Concat Id >> 'Just Unsnoc >> Map (ReadP Int (Singleton Id)) Id *** If (Singleton Id ==~ "X") 10 (ReadP Int (Singleton Id)) >> Zip (1...10 >> Reverse) (Fst Id +: Snd Id) >> Map (Fst Id * Snd Id) Id >> Sum >> Guard ("mod 0 oops") (Id `Mod` 11 == 0)) "0-306-40611-X"
+-- PresentT 132
+--
+-- >>> pz @(Msg "isbn13" (Resplit "-" Id) >> Concat Id >> Map (ReadP Int (Singleton Id)) Id >> Zip (Cycle 13 [1,3] >> Reverse) Id >> Map (Fst Id * Snd Id) Id >> Sum >> '(Id,Id `Mod` 10) >> Guard (PrintT "sum=%d mod 10=%d" Id) (Snd Id == 0)) "978-0-306-40615-7"
+-- PresentT (100,0)
+--
+-- >>> pz @(Resplit "-" Id >> Concat Id >> Map (ReadP Int (Singleton Id)) Id >> Zip (Cycle 13 [1,3] >> Reverse) Id >> Map (Fst Id * Snd Id) Id >> Sum >> '(Id,Id `Mod` 10) >> Guard (PrintT "sum=%d mod 10=%d" Id) (Snd Id == 0)) "978-0-306-40615-8"
+-- FailT "sum=101 mod 10=1"
+--
+-- >>> pz @(Do '[Resplit "-" Id, Concat Id, Zip (Cycle 13 [1,3]) (Map (ReadP Int (Singleton Id)) Id), Map (Fst Id * Snd Id) Id, Sum, Guard (PrintF "%d is not evenly divisible by 10" Id) (Id `Mod` 10 == 0)]) "978-0-7167-0344-9"
+-- FailT "109 is not evenly divisible by 10"
+--
+-- >>> pz @(Do '[Resplit "-" Id, Concat Id, Zip (Cycle 13 [1,3]) (Map (ReadP Int (Singleton Id)) Id), Map (Fst Id * Snd Id) Id, Sum, Guard (PrintF "%d is not evenly divisible by 10" Id) (Id `Mod` 10 == 0)]) "978-0-7167-0344-0"
+-- PresentT 100
+--
+data Guards (ps :: [(k,k1)])
+
+instance ( [a] ~ x
+         , GetLen ps
+         , P (GuardsImpl (LenT ps) ps) x
+         ) => P (Guards ps) x where
+  type PP (Guards ps) x = PP (GuardsImpl (LenT ps) ps) x
+  eval _ opts as = do
+    let msg0 = "Guards"
+        n = getLen @ps
+    if n /= length as then
+       let msg1 = msg0 <> badLength as n
+       in pure $ mkNode opts (FailT msg1) "" []
+    else eval (Proxy @(GuardsImpl (LenT ps) ps)) opts as
+
+instance ( [a] ~ x
+         , Show a
+         ) => P (GuardsImpl n ('[] :: [(k,k1)])) x where
+  type PP (GuardsImpl n ('[] :: [(k,k1)])) x = x
+  eval _ opts as =
+    let msg0 = "Guards"
+    in if not (null as) then errorInProgram $ "GuardsImpl base case has extra data " ++ show as
+       else pure $ mkNode opts (PresentT as) (msg0 <> " no data") []
+
+instance (PP prt (Int, a) ~ String
+        , P prt (Int, a)
+        , KnownNat n
+        , GetLen ps
+        , P p a
+        , PP p a ~ Bool
+        , P (GuardsImpl n ps) [a]
+        , PP (GuardsImpl n ps) [a] ~ [a]
+        , Show a
+        , [a] ~ x
+        ) => P (GuardsImpl n ('(prt,p) ': ps)) x where
+  type PP (GuardsImpl n ('(prt,p) ': ps)) x = x
+  eval _ opts as' = do
+     let cpos = n-pos-1
+         msgbase1 = "Guard(" <> show cpos <> ")"
+         msgbase2 = "Guards"
+         n :: Int
+         n = nat @n
+         pos = getLen @ps
+     case as' of
+         a:as -> do
+            pp <- evalBoolHide @p opts a
+            case getValueLR opts (msgbase1 <> " p failed") pp [] of
+                 Left e -> pure e
+                 Right False -> do
+                   qq <- eval (Proxy @prt) opts (cpos,a) -- only run prt when predicate is False
+                   pure $ case getValueLR opts (msgbase2 <> " False predicate and prt failed") qq [hh pp] of
+                      Left e -> e
+                      Right msgx -> mkNode opts (FailT msgx) (msgbase1 <> " failed [" <> msgx <> "] " <> showL opts a) (hh pp : [hh qq | isVerbose opts])
+                 Right True ->
+                   if pos == 0 then -- we are at the bottom of the tree
+                      pure $ mkNode opts (PresentT [a]) msgbase2 [hh pp]
+                   else do
+                     ss <- eval (Proxy @(GuardsImpl n ps)) opts as
+                     pure $ case getValueLR opts (msgbase1 <> " ok | rhs failed") ss [hh pp] of
+                       Left e -> e -- shortcut else we get too compounding errors with the pp tree being added each time!
+                       Right zs -> (ss & tForest %~ \x -> fromTT pp : x) & tBool .~ PresentT (a:zs)
+         _ -> errorInProgram "GuardsImpl n+1 case has no data"
+
+-- | GuardsQuick contain a type level list of conditions and one of matching values: on no match will fail using the first parameter
+--
+-- >>> pz @(GuardsQuick (PrintT "arg %d failed with value %d" Id) '[Gt 4, Ge 3, Same 4]) [17,3,5]
+-- FailT "arg 2 failed with value 5"
+--
+-- >>> pz @(GuardsQuick (PrintT "arg %d failed with value %d" Id) '[Gt 4, Ge 3, Same 4]) [17,3,5,99]
+-- FailT "Guards:invalid length(4) expected 3"
+--
+-- >>> pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 0 11 Id, Between 1 4 Id,Between 3 5 Id]) [10::Int,2,5]
+-- Present [10,2,5] (Guards)
+-- PresentT [10,2,5]
+--
+-- >>> pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31 Id, Between 1 12 Id, Between 1990 2050 Id]) [31,11,1999::Int]
+-- Present [31,11,1999] (Guards)
+-- PresentT [31,11,1999]
+--
+-- >>> pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31 Id, Between 1 12 Id, Between 1990 2050 Id]) [31,11::Int]
+-- Error Guards:invalid length(2) expected 3
+-- FailT "Guards:invalid length(2) expected 3"
+--
+-- >>> pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31 Id, Between 1 12 Id, Between 1990 2050 Id]) [31,13,1999::Int]
+-- Error guard(1) 13 is out of range (Guard(0) ok | rhs failed)
+-- FailT "guard(1) 13 is out of range"
+--
+-- >>> pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31 Id, Between 1 12 Id, Between 1990 2050 Id]) [0,44,1999::Int]
+-- Error guard(0) 0 is out of range (Guard(0) failed [guard(0) 0 is out of range] 0)
+-- FailT "guard(0) 0 is out of range"
+--
+-- >>> pl @(GuardsQuick (PrintT "guard(%d) %d is out of range" Id) '[Between 1 31 Id, Between 1 12 Id, Between 1990 2050 Id]) [31,11,2000,1,2::Int]
+-- Error Guards:invalid length(5) expected 3
+-- FailT "Guards:invalid length(5) expected 3"
+--
+-- >>> pl @(GuardsQuick (PrintT "guard(%d) err %03d" Id) '[W 'True, Ge 12, W 'False, Lt 2]) [1,2,-99,-999]
+-- Error guard(1) err 002 (Guard(0) ok | rhs failed)
+-- FailT "guard(1) err 002"
+--
+-- >>> pl @(GuardsQuick (PrintT "guard(%d) err %03d" Id) '[W 'True, Ge 12, W 'False, Lt 2]) [1,2,-99]
+-- Error Guards:invalid length(3) expected 4
+-- FailT "Guards:invalid length(3) expected 4"
+--
+-- >>> pl @(GuardsQuick (PrintT "guard(%d) err %03d" Id) '[W 'True, Ge 12, W 'True, Lt 2]) [1,22,-99,-999,1,1,2]
+-- Error Guards:invalid length(7) expected 4
+-- FailT "Guards:invalid length(7) expected 4"
+--
+data GuardsQuick (prt :: k) (ps :: [k1])
+type GuardsQuickT (prt :: k) (ps :: [k1]) = Guards (ToGuardsT prt ps)
+
+instance P (GuardsQuickT prt ps) x => P (GuardsQuick prt ps) x where
+  type PP (GuardsQuick prt ps) x = PP (GuardsQuickT prt ps) x
+  eval _ = eval (Proxy @(GuardsQuickT prt ps))
+
+-- prefer 'Bools' as 'BoolsQuick' doesnt give much added value: passes in the index and the value to prt but you already have the index in the message
+-- pulls the top message from the tree if a predicate is false
+
+-- | boolean guard which checks a given a list of predicates against the list of values
+--
+-- >>> pl @(Bools '[ '(W "hh",Between 0 23 Id), '(W "mm",Between 0 59 Id), '(PrintT "<<<%d %d>>>" Id,Between 0 59 Id) ]) [12,93,14]
+-- False (Bool(1) [mm] (93 <= 59))
+-- FalseT
+--
+-- >>> pl @(Bools '[ '(W "hh",Between 0 23 Id), '(W "mm",Between 0 59 Id), '(PrintT "<<<%d %d>>>" Id,Between 0 59 Id) ]) [12,13,94]
+-- False (Bool(2) [<<<2 94>>>] (94 <= 59))
+-- FalseT
+--
+-- >>> pl @(Bools '[ '(W "hh",Between 0 23 Id), '(W "mm",Between 0 59 Id), '(PrintT "<<<%d %d>>>" Id,Between 0 59 Id) ]) [12,13,14]
+-- True (Bools)
+-- TrueT
+--
+-- >>> pl @(BoolsQuick "abc" '[Between 0 23 Id, Between 0 59 Id, Between 0 59 Id]) [12,13,14]
+-- True (Bools)
+-- TrueT
+--
+-- >>> pl @(BoolsQuick (PrintT "id=%d val=%d" Id) '[Between 0 23 Id, Between 0 59 Id, Between 0 59 Id]) [12,13,14]
+-- True (Bools)
+-- TrueT
+--
+-- >>> pl @(BoolsQuick (PrintT "id=%d val=%d" Id) '[Between 0 23 Id, Between 0 59 Id, Between 0 59 Id]) [12,13,99]
+-- False (Bool(2) [id=2 val=99] (99 <= 59))
+-- FalseT
+--
+-- >>> pl @(Bools '[ '("hours",Between 0 23 Id), '("minutes",Between 0 59 Id), '("seconds",Between 0 59 Id)]) [12,13,14]
+-- True (Bools)
+-- TrueT
+--
+-- >>> pl @(Bools '[ '("hours",Between 0 23 Id), '("minutes",Between 0 59 Id), '("seconds",Between 0 59 Id)]) [12,60,14]
+-- False (Bool(1) [minutes] (60 <= 59))
+-- FalseT
+--
+-- >>> pl @(Bools '[ '("hours",Between 0 23 Id), '("minutes",Between 0 59 Id), '("seconds",Between 0 59 Id)]) [12,60,14,20]
+-- False (Bools:invalid length(4) expected 3)
+-- FalseT
+--
+data Bools (ps :: [(k,k1)])
+
+instance ([a] ~ x
+        , GetLen ps
+        , P (BoolsImpl (LenT ps) ps) x
+        , PP (BoolsImpl (LenT ps) ps) x ~ Bool
+        ) => P (Bools ps) x where
+  type PP (Bools ps) x = Bool
+  eval _ opts as = do
+    let msg0 = "Bools"
+        msg1 = "Bool("++show n++")"
+        n = getLen @ps
+    case chkSize opts msg1 as [] of
+      Left e -> pure e
+      Right () ->
+        if n /= length as then
+           let msg2 = msg0 <> badLength as n
+           in pure $ mkNodeB opts False msg2 [] -- was FailT but now just FalseT
+        else evalBool (Proxy @(BoolsImpl (LenT ps) ps)) opts as
+
+data BoolsImpl (n :: Nat) (os :: [(k,k1)])
+
+instance (KnownNat n
+        , Show a
+        , [a] ~ x
+        ) => P (BoolsImpl n ('[] :: [(k,k1)])) x where
+  type PP (BoolsImpl n ('[] :: [(k,k1)])) x = Bool
+  eval _ opts as =
+    let msg0 = "Bool(" <> show n <> ")"
+        n :: Int = nat @n
+    in if not (null as) then errorInProgram $ "BoolsImpl base case has extra data " ++ show as
+       else pure $ mkNodeB opts True (msg0 <> " empty") []
+
+instance (PP prt (Int, a) ~ String
+        , P prt (Int, a)
+        , KnownNat n
+        , GetLen ps
+        , P p a
+        , PP p a ~ Bool
+        , P (BoolsImpl n ps) x
+        , PP (BoolsImpl n ps) [a] ~ Bool
+--        , Show a
+        , [a] ~ x
+        ) => P (BoolsImpl n ('(prt,p) ': ps)) x where
+  type PP (BoolsImpl n ('(prt,p) ': ps)) x = Bool
+  eval _ opts as' = do
+     let cpos = n-pos-1
+         msgbase1 = "Bool(" <> showIndex cpos <> ")"
+         msgbase2 = "Bools"
+         n :: Int = nat @n
+         pos = getLen @ps
+     case as' of
+         a:as -> do
+            pp <- evalBoolHide @p opts a
+            case getValueLR opts (msgbase1 <> " p failed") pp [] of
+                 Left e -> pure e
+                 Right False -> do
+                   qq <- eval (Proxy @prt) opts (cpos,a) -- only run prt when predicate is False
+                   pure $ case getValueLR opts (msgbase2 <> " False predicate and prt failed") qq [hh pp] of
+                      Left e -> e
+                      Right msgx -> mkNodeB opts False (msgbase1 <> " [" <> msgx <> "] " <> topMessage pp) (hh pp : [hh qq | isVerbose opts])
+                 Right True ->
+                   if pos == 0 then -- we are at the bottom of the tree
+                      pure $ mkNodeB opts True msgbase2 [hh pp]
+                   else do
+                     ss <- evalBool (Proxy @(BoolsImpl n ps)) opts as
+                     pure $ case getValueLR opts (msgbase1 <> " ok | rhs failed") ss [hh pp] of
+                       Left e -> e -- shortcut else we get too compounding errors with the pp tree being added each time!
+                       Right _ ->  ss & tForest %~ \x -> fromTT pp : x
+         _ -> errorInProgram "BoolsImpl n+1 case has no data"
+
+data BoolsQuick (prt :: k) (ps :: [k1])
+type BoolsQuickT (prt :: k) (ps :: [k1]) = Bools (ToGuardsT prt ps)
+
+-- why do we need this? when BoolsN works without [use the x ~ [a] trick in BoolsN]
+instance (PP (Bools (ToGuardsT prt ps)) x ~ Bool
+        , P (BoolsQuickT prt ps) x
+          ) => P (BoolsQuick prt ps) x where
+  type PP (BoolsQuick prt ps) x = PP (BoolsQuickT prt ps) x
+  eval _ = evalBool (Proxy @(BoolsQuickT prt ps))
+
+-- | leverages 'RepeatT' for repeating predicates (passthrough method)
+--
+-- >>> pl @(BoolsN (PrintT "id=%d must be between 0 and 255, found %d" Id) 4 (Between 0 255 Id)) [121,33,7,256]
+-- False (Bool(3) [id=3 must be between 0 and 255, found 256] (256 <= 255))
+-- FalseT
+--
+-- >>> pl @(BoolsN (PrintT "id=%d must be between 0 and 255, found %d" Id) 4 (Between 0 255 Id)) [121,33,7,44]
+-- True (Bools)
+-- TrueT
+--
+data BoolsN prt (n :: Nat) (p :: k1)
+type BoolsNT prt (n :: Nat) (p :: k1) = Bools (ToGuardsT prt (RepeatT n p))
+
+instance ( x ~ [a]
+         , P (BoolsNT prt n p) x
+         ) => P (BoolsN prt n p) x where
+  type PP (BoolsN prt n p) x = PP (BoolsNT prt n p) x
+  eval _ = evalBool (Proxy @(BoolsNT prt n p))
+
+-- | if a predicate fails then then the corresponding symbol and value will be passed to the print function
+--
+-- >>> pz @(GuardsDetail "%s invalid: found %d" '[ '("hours", Between 0 23 Id),'("minutes",Between 0 59 Id),'("seconds",Between 0 59 Id)]) [13,59,61]
+-- FailT "seconds invalid: found 61"
+--
+-- >>> pz @(GuardsDetail "%s invalid: found %d" '[ '("hours", Between 0 23 Id),'("minutes",Between 0 59 Id),'("seconds",Between 0 59 Id)]) [27,59,12]
+-- FailT "hours invalid: found 27"
+--
+-- >>> pz @(GuardsDetail "%s invalid: found %d" '[ '("hours", Between 0 23 Id),'("minutes",Between 0 59 Id),'("seconds",Between 0 59 Id)]) [23,59,12]
+-- PresentT [23,59,12]
+--
+data GuardsDetailImpl (ps :: [(k,k1)])
+
+instance ([a] ~ x
+        , GetLen ps
+        , P (GuardsImplX (LenT ps) ps) x
+        ) => P (GuardsDetailImpl ps) x where
+  type PP (GuardsDetailImpl ps) x = PP (GuardsImplX (LenT ps) ps) x
+  eval _ opts as = do
+    let msg0 = "Guards"
+        n = getLen @ps
+    if n /= length as then
+       let msg1 = msg0 <> badLength as n
+       in pure $ mkNode opts (FailT msg1) "" []
+    else eval (Proxy @(GuardsImplX (LenT ps) ps)) opts as
+
+data GuardsImplX (n :: Nat) (os :: [(k,k1)])
+
+instance ( [a] ~ x
+         , Show a
+         ) => P (GuardsImplX n ('[] :: [(k,k1)])) x where
+  type PP (GuardsImplX n ('[] :: [(k,k1)])) x = x
+  eval _ opts as =
+    let msg0 = "Guards"
+        -- n :: Int = nat @n
+    in if not (null as) then errorInProgram $ "GuardsImplX base case has extra data " ++ show as
+       else pure $ mkNode opts (PresentT as) msg0 []
+
+instance (PP prt a ~ String
+        , P prt a
+        , KnownNat n
+        , GetLen ps
+        , P p a
+        , PP p a ~ Bool
+        , P (GuardsImplX n ps) [a]
+        , PP (GuardsImplX n ps) [a] ~ [a]
+        , Show a
+        , [a] ~ x
+        ) => P (GuardsImplX n ('(prt,p) ': ps)) x where
+  type PP (GuardsImplX n ('(prt,p) ': ps)) x = x
+  eval _ opts as' = do
+     let cpos = n-pos-1
+         msgbase1 = "Guard(" <> showIndex cpos <> ")"
+         msgbase2 = "Guards"
+         n :: Int = nat @n
+         pos = getLen @ps
+     case as' of
+         a:as -> do
+            pp <- evalBoolHide @p opts a
+            case getValueLR opts (msgbase1 <> " p failed") pp [] of
+                 Left e -> pure e
+                 Right False -> do
+                   qq <- eval (Proxy @prt) opts a -- only run prt when predicate is False
+                   pure $ case getValueLR opts (msgbase2 <> " False predicate and prt failed") qq [hh pp] of
+                      Left e -> e
+                      Right msgx -> mkNode opts (FailT msgx) (msgbase1 <> " failed [" <> msgx <> "] " <> showL opts a) (hh pp : [hh qq | isVerbose opts])
+                 Right True -> do
+                   ss <- eval (Proxy @(GuardsImplX n ps)) opts as
+                   pure $ case getValueLR opts (msgbase1 <> " ok | rhs failed") ss [hh pp] of
+                     Left e -> e -- shortcut else we get too compounding errors with the pp tree being added each time!
+                     Right zs -> mkNode opts (PresentT (a:zs)) (msgbase1 <> " " <> showL opts a) [hh pp, hh ss]
+         _ -> errorInProgram "GuardsImplX n+1 case has no data"
+
+data GuardsDetail prt (ps :: [(k0,k1)])
+type GuardsDetailT prt (ps :: [(k0,k1)]) = GuardsDetailImpl (ToGuardsDetailT prt ps)
+
+instance P (GuardsDetailT prt ps) x => P (GuardsDetail prt ps) x where
+  type PP (GuardsDetail prt ps) x = PP (GuardsDetailT prt ps) x
+  eval _ = eval (Proxy @(GuardsDetailT prt ps))
+
+type family ToGuardsDetailT (prt :: k1) (os :: [(k2,k3)]) :: [(Type,k3)] where
+  ToGuardsDetailT prt '[ '(s,p) ] = '(PrintT prt '(s,Id), p) : '[]
+  ToGuardsDetailT prt ( '(s,p) ': ps) = '(PrintT prt '(s,Id), p) ': ToGuardsDetailT prt ps
+  ToGuardsDetailT prt '[] = GL.TypeError ('GL.Text "ToGuardsDetailT cannot be empty")
+
+-- | leverages 'RepeatT' for repeating predicates (passthrough method)
+--
+-- >>> pz @(GuardsN (PrintT "id=%d must be between 0 and 255, found %d" Id) 4 (Between 0 255 Id)) [121,33,7,256]
+-- FailT "id=3 must be between 0 and 255, found 256"
+--
+-- >>> pz @(GuardsN (PrintT "id=%d must be between 0 and 255, found %d" Id) 4 (Between 0 255 Id)) [121,33,7,44]
+-- PresentT [121,33,7,44]
+--
+-- >>> pl @(GuardsN (PrintT "guard(%d) %d is out of range" Id) 4 (Between 0 255 Id)) [1,2,3,4::Int]
+-- Present [1,2,3,4] (Guards)
+-- PresentT [1,2,3,4]
+--
+-- >>> pl @(GuardsN (PrintT "guard(%d) %d is out of range" Id) 4 (Between 0 255 Id)) [1,2,3,4,5::Int]
+-- Error Guards:invalid length(5) expected 4
+-- FailT "Guards:invalid length(5) expected 4"
+--
+-- >>> pl @(GuardsN (PrintT "guard(%d) %d is out of range" Id) 4 (Between 0 255 Id)) [1,2,3::Int]
+-- Error Guards:invalid length(3) expected 4
+-- FailT "Guards:invalid length(3) expected 4"
+--
+data GuardsN prt (n :: Nat) p
+type GuardsNT prt (n :: Nat) p = Guards (ToGuardsT prt (RepeatT n p))
+
+instance ( x ~ [a]
+         , P (GuardsNT prt n p) x
+         ) => P (GuardsN prt n p) x where
+  type PP (GuardsN prt n p) x = PP (GuardsNT prt n p) x
+  eval _ = eval (Proxy @(GuardsNT prt n p))
+
+-- | \'p\' is the predicate and on failure of the predicate runs \'prt\'
+--
+-- >>> pz @(Guard "expected > 3" (Gt 3)) 17
+-- PresentT 17
+--
+-- >>> pz @(Guard "expected > 3" (Gt 3)) 1
+-- FailT "expected > 3"
+--
+-- >>> pz @(Guard (PrintF "%d not > 3" Id) (Gt 3)) (-99)
+-- FailT "-99 not > 3"
+--
+-- >>> pl @(Map (Guard "someval" (Lt 3) >> 'True) Id) [1::Int ..10]
+-- Error someval(8) (Map(i=2, a=3) excnt=8)
+-- FailT "someval(8)"
+--
+-- >>> pl @(Guard "someval" (Len == 2) >> (ShowP Id &&& Id)) ([] :: [Int])
+-- Error someval ((>>) lhs failed)
+-- FailT "someval"
+--
+-- >>> pl @(Guard "someval" (Len == 2) >> (Id &&& ShowP Id)) [2,3]
+-- Present ([2,3],"[2,3]") ((>>) ([2,3],"[2,3]") | {W '([2,3],"[2,3]")})
+-- PresentT ([2,3],"[2,3]")
+--
+-- >>> pl @(Guard "someval" (Len == 2) >> (ShowP Id &&& Id)) [2,3,4]
+-- Error someval ((>>) lhs failed)
+-- FailT "someval"
+--
+-- >>> pl @(Map (Guard "someval" (Lt 3) >> 'True) Id) [1::Int ..10]
+-- Error someval(8) (Map(i=2, a=3) excnt=8)
+-- FailT "someval(8)"
+--
+-- >>> pl @(Guard "oops" (Len > 2) >> Map (Succ Id) Id) [12,15,16]
+-- Present [13,16,17] ((>>) [13,16,17] | {Map [13,16,17] | [12,15,16]})
+-- PresentT [13,16,17]
+--
+-- >>> pl @(Guard "err" (Len > 2) >> Map (Succ Id) Id) [12]
+-- Error err ((>>) lhs failed)
+-- FailT "err"
+--
+-- >>> pl @(Guard (PrintF "err found len=%d" Len) (Len > 5) >> Map (Succ Id) Id) [12,15,16]
+-- Error err found len=3 ((>>) lhs failed)
+-- FailT "err found len=3"
+--
+data Guard prt p
+
+
+instance (Show a
+        , P prt a
+        , PP prt a ~ String
+        , P p a
+        , PP p a ~ Bool
+        ) => P (Guard prt p) a where
+  type PP (Guard prt p) a = a
+  eval _ opts a = do
+    let msg0 = "Guard"
+    pp <- evalBool (Proxy @p) opts a
+    case getValueLR opts msg0 pp [] of
+      Left e -> pure e
+      Right False -> do
+        qq <- eval (Proxy @prt) opts a
+        pure $ case getValueLR opts (msg0 <> " Msg") qq [hh pp] of
+          Left e -> e
+          Right ee -> mkNode opts (FailT ee) (msg0 <> " | " <> showL opts a) (hh pp : [hh qq | isVerbose opts])
+      Right True -> pure $ mkNode opts (PresentT a) (msg0 <> "(ok) | " <> showL opts a) [hh pp]  -- dont show the guard message if successful
+
+-- | uses 'Guard' but negates \'p\'
+--
+-- >>> pl @(HeadFail "failedn" Id &&& (Len == 1 >> ExitWhen "ExitWhen" Id) >> Fst Id) [3]
+-- Error ExitWhen ((>>) lhs failed)
+-- FailT "ExitWhen"
+--
+-- >>> pl @(Head Id &&& (Len == 1 >> Not Id >> ExitWhen "ExitWhen" Id) >> Fst Id) [3]
+-- Present 3 ((>>) 3 | {Fst 3 | (3,False)})
+-- PresentT 3
+--
+-- >>> pl @(Head Id &&& (Len == 1 >> ExitWhen "ExitWhen" (Not Id)) >> Fst Id) [3]
+-- Present 3 ((>>) 3 | {Fst 3 | (3,True)})
+-- PresentT 3
+--
+-- >>> pl @(ExitWhen "ExitWhen" (Len /= 1) >> Head Id) [3,1]
+-- Error ExitWhen ((>>) lhs failed)
+-- FailT "ExitWhen"
+--
+-- >>> pl @(ExitWhen "ExitWhen" (Len /= 1) >> Head Id) [3]
+-- Present 3 ((>>) 3 | {Head 3 | [3]})
+-- PresentT 3
+--
+-- >>> pl @(ExitWhen "ExitWhen" (Len /= 1) >> Head Id >> Gt (20 -% 1)) [3]
+-- True ((>>) True | {3 % 1 > (-20) % 1})
+-- TrueT
+--
+-- >>> pl @(ExitWhen "ExitWhen" (Len /= 1) >> Head Id >> Gt (20 -% 1)) [-23]
+-- False ((>>) False | {(-23) % 1 > (-20) % 1})
+-- FalseT
+--
+-- >>> pl @(Map (ExitWhen "ExitWhen" (Gt 10) >> Gt 2) Id) [1..5]
+-- Present [False,False,True,True,True] (Map [False,False,True,True,True] | [1,2,3,4,5])
+-- PresentT [False,False,True,True,True]
+--
+-- >>> pl @(ExitWhen "err" (Len > 2) >> Map (Succ Id) Id) [12,15,16]
+-- Error err ((>>) lhs failed)
+-- FailT "err"
+--
+-- >>> pl @(ExitWhen "err" (Len > 2) >> Map (Succ Id) Id) [12]
+-- Present [13] ((>>) [13] | {Map [13] | [12]})
+-- PresentT [13]
+--
+
+data ExitWhen prt p
+type ExitWhenT prt p = Guard prt (Not p)
+
+instance P (ExitWhenT prt p) x => P (ExitWhen prt p) x where
+  type PP (ExitWhen prt p) x = PP (ExitWhenT prt p) x
+  eval _ = eval (Proxy @(ExitWhenT prt p))
+
+-- | similar to 'Guard' but uses the root message of the False predicate case as the failure message
+--
+-- most uses of GuardSimple can be replaced by a boolean predicate unless you require a failure message instead of true/false
+--
+-- >>> pz @(GuardSimple (Luhn Id)) [1..4]
+-- FailT "(Luhn map=[4,6,2,2] sum=14 ret=4 | [1,2,3,4])"
+--
+-- >>> pl @(Luhn Id) [1..4]
+-- False (Luhn map=[4,6,2,2] sum=14 ret=4 | [1,2,3,4])
+-- FalseT
+--
+-- >>> pz @(GuardSimple (Luhn Id)) [1,2,3,0]
+-- PresentT [1,2,3,0]
+--
+-- >>> pz @(GuardSimple (Len > 30)) [1,2,3,0]
+-- FailT "(4 > 30)"
+--
+-- >>> pl @(Map (GuardSimple (Lt 3) >> 'True) Id) [1::Int .. 10]
+-- Error (3 < 3) | (4 < 3) | (5 < 3) | (6 < 3) | (7 < 3) | (8 < 3) | (9 < 3) | (10 < 3) (Map(i=2, a=3) excnt=8)
+-- FailT "(3 < 3) | (4 < 3) | (5 < 3) | (6 < 3) | (7 < 3) | (8 < 3) | (9 < 3) | (10 < 3)"
+--
+-- >>> pl @(Map (GuardSimple (Ge 1) >> 'True) Id) [1::Int .. 10]
+-- Present [True,True,True,True,True,True,True,True,True,True] (Map [True,True,True,True,True,True,True,True,True,True] | [1,2,3,4,5,6,7,8,9,10])
+-- PresentT [True,True,True,True,True,True,True,True,True,True]
+--
+-- >>> pl @(Map (GuardSimple (Lt 3) >> 'True) Id) [1::Int .. 10]
+-- Error (3 < 3) | (4 < 3) | (5 < 3) | (6 < 3) | (7 < 3) | (8 < 3) | (9 < 3) | (10 < 3) (Map(i=2, a=3) excnt=8)
+-- FailT "(3 < 3) | (4 < 3) | (5 < 3) | (6 < 3) | (7 < 3) | (8 < 3) | (9 < 3) | (10 < 3)"
+--
+-- >>> pl @(Map (GuardSimple (Ge 1) >> 'True) Id) [1::Int .. 10]
+-- Present [True,True,True,True,True,True,True,True,True,True] (Map [True,True,True,True,True,True,True,True,True,True] | [1,2,3,4,5,6,7,8,9,10])
+-- PresentT [True,True,True,True,True,True,True,True,True,True]
+--
+data GuardSimple p
+
+instance (Show a
+        , P p a
+        , PP p a ~ Bool
+        ) => P (GuardSimple p) a where
+  type PP (GuardSimple p) a = a
+  eval _ opts a = do
+    let msg0 = "GuardSimple"
+    pp <- evalBool (Proxy @p) (subopts opts) a -- temporarily lift DZero to DLite so as not to lose the failure message
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right False ->
+        let msgx = topMessage pp
+        in mkNode opts (FailT msgx) (msg0 <> " | " <> showL opts a) [hh pp]
+      Right True ->
+        mkNode opts (PresentT a) (msg0 <> "(ok) | " <> showL opts a) [hh pp]

@@ -0,0 +1,599 @@+{-# OPTIONS -Wall #-}
+{-# OPTIONS -Wno-compat #-}
+{-# OPTIONS -Wincomplete-record-updates #-}
+{-# OPTIONS -Wincomplete-uni-patterns #-}
+{-# OPTIONS -Wredundant-constraints #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE NoOverloadedLists #-}
+{-# LANGUAGE NoStarIsType #-}
+{- |
+     promoted date time functions
+-}
+module Predicate.Data.DateTime (
+
+  -- ** format
+    FormatTimeP
+
+  -- ** constructors
+  , ParseTimeP
+  , ParseTimeP'
+  , ParseTimes
+  , ParseTimes'
+  , MkDay
+  , MkDay'
+  , MkDayExtra
+  , MkDayExtra'
+  , MkTime
+  , MkTime'
+  , PosixToUTCTime
+
+ -- ** destructors
+  , UnMkDay
+  , ToWeekDate
+  , ToWeekYear
+  , ToDay
+  , ToTime
+  , UnMkTime
+  , UTCTimeToPosix
+
+ ) where
+import Predicate.Core
+import Predicate.Util
+import Control.Lens hiding (iall)
+import Data.Proxy
+import Data.Typeable
+import Data.Kind (Type)
+import Data.Maybe
+import Data.Time
+import Data.Time.Calendar.WeekDate
+import qualified Data.Time.Clock.System as CP
+import qualified Data.Time.Clock.POSIX as P
+-- $setup
+-- >>> :set -XDataKinds
+-- >>> :set -XTypeApplications
+-- >>> :set -XTypeOperators
+-- >>> :set -XOverloadedStrings
+-- >>> :set -XNoOverloadedLists
+-- >>> import qualified Data.Text as T
+-- >>> import Predicate.Prelude
+-- >>> import Safe (readNote)
+
+-- | type level expression representing a formatted time
+-- similar to 'Data.Time.formatTime' using a type level 'GHC.TypeLits.Symbol' to get the formatting string
+--
+-- >>> pz @(FormatTimeP "%F %T" Id) (readNote @LocalTime "invalid localtime" "2019-05-24 05:19:59")
+-- PresentT "2019-05-24 05:19:59"
+--
+-- >>> pz @(FormatTimeP (Fst Id) (Snd Id)) ("the date is %d/%m/%Y", readNote @Day "invalid day" "2019-05-24")
+-- PresentT "the date is 24/05/2019"
+--
+-- >>> pl @(FormatTimeP "%Y-%m-%d" Id) (readNote @Day "invalid day" "2019-08-17")
+-- Present "2019-08-17" (FormatTimeP (%Y-%m-%d) 2019-08-17 | 2019-08-17)
+-- PresentT "2019-08-17"
+--
+data FormatTimeP p q
+
+instance (PP p x ~ String
+        , FormatTime (PP q x)
+        , P p x
+        , Show (PP q x)
+        , P q x
+        ) => P (FormatTimeP p q) x where
+  type PP (FormatTimeP p q) x = String
+  eval _ opts x = do
+    let msg0 = "FormatTimeP"
+    lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
+    pure $ case lr of
+      Left e -> e
+      Right (p,q,pp,qq) ->
+        let msg1 = msg0 <> " (" <> p <> ")"
+            b = formatTime defaultTimeLocale p q
+        in mkNode opts (PresentT b) (msg1 <> " " <> litL opts b <> showVerbose opts " | " q) [hh pp, hh qq]
+
+-- | similar to 'Data.Time.parseTimeM' where \'t\' is the 'Data.Time.ParseTime' type, \'p\' is the datetime format and \'q\' points to the content to parse
+--
+-- >>> pz @(ParseTimeP LocalTime "%F %T" Id) "2019-05-24 05:19:59"
+-- PresentT 2019-05-24 05:19:59
+--
+-- >>> pz @(ParseTimeP LocalTime "%F %T" "2019-05-24 05:19:59") (Right "never used")
+-- PresentT 2019-05-24 05:19:59
+--
+-- keeping \'q\' as we might want to extract from a tuple
+data ParseTimeP' t p q
+
+instance (ParseTime (PP t a)
+        , Typeable (PP t a)
+        , Show (PP t a)
+        , P p a
+        , P q a
+        , PP p a ~ String
+        , PP q a ~ String
+        ) => P (ParseTimeP' t p q) a where
+  type PP (ParseTimeP' t p q) a = PP t a
+  eval _ opts a = do
+    let msg0 = "ParseTimeP " <> t
+        t = showT @(PP t a)
+    lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
+    pure $ case lr of
+      Left e -> e
+      Right (p,q,pp,qq) ->
+        let msg1 = msg0 <> " (" <> p <> ")"
+            hhs = [hh pp, hh qq]
+        in case parseTimeM @Maybe @(PP t a) True defaultTimeLocale p q of
+             Just b -> mkNode opts (PresentT b) (lit01 opts msg1 b "fmt=" p <> showVerbose opts " | " q) hhs
+             Nothing -> mkNode opts (FailT (msg1 <> " failed to parse")) "" hhs
+-- | similar to 'Date.Time.parseTimeM'
+--
+-- >>> pl @(ParseTimeP TimeOfDay "%H:%M%S" Id) "14:04:61"
+-- Error ParseTimeP TimeOfDay (%H:%M%S) failed to parse
+-- FailT "ParseTimeP TimeOfDay (%H:%M%S) failed to parse"
+--
+-- >>> pl @(ParseTimeP UTCTime "%F %T" Id) "1999-01-01 12:12:12"
+-- Present 1999-01-01 12:12:12 UTC (ParseTimeP UTCTime (%F %T) 1999-01-01 12:12:12 UTC | fmt=%F %T | "1999-01-01 12:12:12")
+-- PresentT 1999-01-01 12:12:12 UTC
+--
+
+data ParseTimeP (t :: Type) p q
+type ParseTimePT (t :: Type) p q = ParseTimeP' (Hole t) p q
+
+instance P (ParseTimePT t p q) x => P (ParseTimeP t p q) x where
+  type PP (ParseTimeP t p q) x = PP (ParseTimePT t p q) x
+  eval _ = eval (Proxy @(ParseTimePT t p q))
+
+-- | A convenience method to match against many different datetime formats to find the first match
+data ParseTimes' t p q
+
+instance (ParseTime (PP t a)
+        , Typeable (PP t a)
+        , Show (PP t a)
+        , P p a
+        , P q a
+        , PP p a ~ [String]
+        , PP q a ~ String
+        ) => P (ParseTimes' t p q) a where
+  type PP (ParseTimes' t p q) a = PP t a
+  eval _ opts a = do
+    let msg0 = "ParseTimes " <> t
+        t = showT @(PP t a)
+    lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts a []
+    pure $ case lr of
+      Left e -> e
+      Right (p,q,pp,qq) ->
+        let hhs = [hh pp, hh qq]
+            zs = map (\d -> (d,) <$> parseTimeM @Maybe @(PP t a) True defaultTimeLocale d q) p
+        in case catMaybes zs of
+             [] -> mkNode opts (FailT ("no match on (" ++ q ++ ")")) msg0 hhs
+             (d,b):_ -> mkNode opts (PresentT b) (lit01 opts msg0 b "fmt=" d <> showVerbose opts " | " q) hhs
+
+-- | A convenience method to match against many different datetime formats to find the first match
+--
+-- >>> pz @(ParseTimes LocalTime '["%Y-%m-%d %H:%M:%S", "%m/%d/%y %H:%M:%S", "%B %d %Y %H:%M:%S", "%Y-%m-%dT%H:%M:%S"] "03/11/19 01:22:33") ()
+-- PresentT 2019-03-11 01:22:33
+--
+-- >>> pz @(ParseTimes LocalTime (Fst Id) (Snd Id)) (["%Y-%m-%d %H:%M:%S", "%m/%d/%y %H:%M:%S", "%B %d %Y %H:%M:%S", "%Y-%m-%dT%H:%M:%S"], "03/11/19 01:22:33")
+-- PresentT 2019-03-11 01:22:33
+--
+-- >>> pl @(Map (ParseTimes Day '["%Y-%m-%d", "%m/%d/%y", "%b %d %Y"] Id) Id) ["2001-01-01", "Jan 24 2009", "03/29/0x7"]
+-- Error no match on (03/29/0x7) (Map(i=2, a="03/29/0x7") excnt=1)
+-- FailT "no match on (03/29/0x7)"
+--
+-- >>> pl @(Map (ParseTimes Day '["%Y-%m-%d", "%m/%d/%y", "%b %d %Y"] Id) Id) ["2001-01-01", "Jan 24 2009", "03/29/07"]
+-- Present [2001-01-01,2009-01-24,2007-03-29] (Map [2001-01-01,2009-01-24,2007-03-29] | ["2001-01-01","Jan 24 2009","03/29/07"])
+-- PresentT [2001-01-01,2009-01-24,2007-03-29]
+--
+data ParseTimes (t :: Type) p q
+type ParseTimesT (t :: Type) p q = ParseTimes' (Hole t) p q
+
+instance P (ParseTimesT t p q) x => P (ParseTimes t p q) x where
+  type PP (ParseTimes t p q) x = PP (ParseTimesT t p q) x
+  eval _ = eval (Proxy @(ParseTimesT t p q))
+
+-- | create a 'Day' from three int values passed in as year month and day
+--
+-- >>> pz @(MkDay' (Fst Id) (Snd Id) (Thd Id)) (2019,99,99999)
+-- PresentT Nothing
+--
+data MkDay' p q r
+
+instance (P p x
+        , P q x
+        , P r x
+        , PP p x ~ Int
+        , PP q x ~ Int
+        , PP r x ~ Int
+        ) => P (MkDay' p q r) x where
+  type PP (MkDay' p q r) x = Maybe Day
+  eval _ opts x = do
+    let msg0 = "MkDay"
+    lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
+    case lr of
+      Left e -> pure e
+      Right (p,q,pp,qq) -> do
+        let hhs = [hh pp, hh qq]
+        rr <- eval (Proxy @r) opts x
+        pure $ case getValueLR opts msg0 rr hhs of
+          Left e -> e
+          Right r ->
+            let mday = fromGregorianValid (fromIntegral p) q r
+            in mkNode opts (PresentT mday) (show01' opts msg0 mday "(y,m,d)=" (p,q,r)) (hhs <> [hh rr])
+
+-- | create a 'Day' from three int values passed in as year month and day
+--
+-- >>> pz @(MkDay '(1,2,3) >> 'Just Id) ()
+-- PresentT 0001-02-03
+--
+-- >>> pz @(Just (MkDay '(1,2,3))) 1
+-- PresentT 0001-02-03
+--
+-- >>> pz @(MkDay Id) (2019,12,30)
+-- PresentT (Just 2019-12-30)
+--
+-- >>> pz @(MkDay Id) (1999,3,13)
+-- PresentT (Just 1999-03-13)
+--
+data MkDay p
+type MkDayT p = MkDay' (Fst p) (Snd p) (Thd p)
+
+instance P (MkDayT p) x => P (MkDay p) x where
+  type PP (MkDay p) x = PP (MkDayT p) x
+  eval _ = eval (Proxy @(MkDayT p))
+
+-- | uncreate a 'Day' returning year month and day
+--
+-- >>> pz @(UnMkDay Id) (readNote "invalid day" "2019-12-30")
+-- PresentT (2019,12,30)
+--
+data UnMkDay p
+
+instance ( PP p x ~ Day
+         , P p x
+         ) => P (UnMkDay p) x where
+  type PP (UnMkDay p) x = (Int, Int, Int)
+  eval _ opts x = do
+    let msg0 = "UnMkDay"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let (fromIntegral -> y, m, d) = toGregorian p
+            b = (y, m, d)
+        in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
+
+
+-- | create a 'Day', week number, and the day of the week from three numbers passed in as year month and day
+--
+-- >>> pz @(MkDayExtra' (Fst Id) (Snd Id) (Thd Id)) (2019,99,99999)
+-- PresentT Nothing
+--
+data MkDayExtra' p q r
+
+instance (P p x
+        , P q x
+        , P r x
+        , PP p x ~ Int
+        , PP q x ~ Int
+        , PP r x ~ Int
+        ) => P (MkDayExtra' p q r) x where
+  type PP (MkDayExtra' p q r) x = Maybe (Day, Int, Int)
+  eval _ opts x = do
+    let msg0 = "MkDayExtra"
+    lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
+    case lr of
+      Left e -> pure e
+      Right (p,q,pp,qq) -> do
+        let hhs = [hh pp, hh qq]
+        rr <- eval (Proxy @r) opts x
+        pure $ case getValueLR opts msg0 rr hhs of
+          Left e -> e
+          Right r ->
+            let mday = fromGregorianValid (fromIntegral p) q r
+                b = mday <&> \day ->
+                      let (_, week, dow) = toWeekDate day
+                      in (day, week, dow)
+            in mkNode opts (PresentT b) (show01' opts msg0 b "(y,m,d)=" (p,q,r)) (hhs <> [hh rr])
+
+-- | create a 'Day', week number, and the day of the week from three numbers passed in as year month and day
+--
+-- >>> pz @(MkDayExtra '(1,2,3) >> 'Just Id >> Fst Id) ()
+-- PresentT 0001-02-03
+--
+-- >>> pz @(Fst (Just (MkDayExtra '(1,2,3)))) 1
+-- PresentT 0001-02-03
+--
+-- >>> pz @(MkDayExtra Id) (2019,12,30)
+-- PresentT (Just (2019-12-30,1,1))
+--
+-- >>> pz @(MkDayExtra Id) (1999,3,13)
+-- PresentT (Just (1999-03-13,10,6))
+--
+data MkDayExtra p
+type MkDayExtraT p = MkDayExtra' (Fst p) (Snd p) (Thd p)
+
+instance P (MkDayExtraT p) x => P (MkDayExtra p) x where
+  type PP (MkDayExtra p) x = PP (MkDayExtraT p) x
+  eval _ = eval (Proxy @(MkDayExtraT p))
+
+-- | get the day of the week
+--
+-- >>> pz @(Just (MkDay '(2020,7,11)) >> '(UnMkDay Id, ToWeekYear Id,ToWeekDate Id)) ()
+-- PresentT ((2020,7,11),28,(6,"Saturday"))
+--
+data ToWeekDate p
+
+instance ( P p x
+         , PP p x ~ Day
+         ) => P (ToWeekDate p) x where
+  type PP (ToWeekDate p) x = (Int, String)
+  eval _ opts x = do
+    let msg0 = "ToWeekDate"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let (_, _week, dow) = toWeekDate p
+            dowString =
+              case dow of
+                 1 -> "Monday"
+                 2 -> "Tuesday"
+                 3 -> "Wednesday"
+                 4 -> "Thursday"
+                 5 -> "Friday"
+                 6 -> "Saturday"
+                 7 -> "Sunday"
+                 _ -> error $ "oops: ToWeekDate invalid " ++ show dow
+        in mkNode opts (PresentT (dow,dowString)) (show01 opts msg0 dow p) [hh pp]
+
+-- | get week number of the year
+--
+-- >>> pz @(Just (MkDay '(2020,7,11)) >> ToWeekYear Id) ()
+-- PresentT 28
+--
+data ToWeekYear p
+
+instance ( P p x
+         , PP p x ~ Day
+         ) => P (ToWeekYear p) x where
+  type PP (ToWeekYear p) x = Int
+  eval _ opts x = do
+    let msg0 = "ToWeekYear"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let (_, week, _dow) = toWeekDate p
+        in mkNode opts (PresentT week) (show01 opts msg0 week p) [hh pp]
+
+class ToDayC a where
+  getDay :: a -> Day
+instance ToDayC UTCTime where
+  getDay = utctDay
+instance ToDayC ZonedTime where
+  getDay = getDay . zonedTimeToLocalTime
+instance ToDayC LocalTime where
+  getDay = localDay
+instance ToDayC Day where
+  getDay = id
+instance ToDayC Rational where
+  getDay = getDay . P.posixSecondsToUTCTime . fromRational
+instance ToDayC CP.SystemTime where
+  getDay = getDay . CP.systemToUTCTime
+
+class ToTimeC a where
+  getTime :: a -> TimeOfDay
+instance ToTimeC UTCTime where
+  getTime = getTime . utctDayTime
+instance ToTimeC ZonedTime where
+  getTime = getTime . zonedTimeToLocalTime
+instance ToTimeC LocalTime where
+  getTime = localTimeOfDay
+instance ToTimeC TimeOfDay where
+  getTime = id
+instance ToTimeC DiffTime where
+  getTime = timeToTimeOfDay
+instance ToTimeC Rational where
+  getTime = getTime . P.posixSecondsToUTCTime . fromRational
+instance ToTimeC CP.SystemTime where
+  getTime = getTime . CP.systemToUTCTime
+
+-- | extract 'Day' from a DateTime
+--
+-- >>> pz @(ReadP UTCTime Id >> ToDay Id) "2020-07-06 12:11:13Z"
+-- PresentT 2020-07-06
+--
+data ToDay p
+
+instance ( P p x
+         , Show (PP p x)
+         , ToDayC (PP p x)
+         ) => P (ToDay p) x where
+  type PP (ToDay p) x = Day
+  eval _ opts x = do
+    let msg0 = "ToDay"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let ret = getDay p
+        in mkNode opts (PresentT ret) (show01 opts msg0 ret p) [hh pp]
+
+-- | extract 'TimeOfDay' from DateTime
+--
+-- >>> pz @(ReadP UTCTime Id >> ToDay Id) "2020-07-06 12:11:13Z"
+-- PresentT 2020-07-06
+--
+data ToTime p
+
+instance ( P p x
+         , Show (PP p x)
+         , ToTimeC (PP p x)
+         ) => P (ToTime p) x where
+  type PP (ToTime p) x = TimeOfDay
+  eval _ opts x = do
+    let msg0 = "ToTime"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let ret = getTime p
+        in mkNode opts (PresentT ret) (show01 opts msg0 ret p) [hh pp]
+
+
+-- | create a 'TimeOfDay' from three int values passed in as year month and day
+--
+-- >>> pz @(MkTime' (Fst Id) (Snd Id) (Thd Id)) (13,99,99999)
+-- PresentT 13:99:99999
+--
+data MkTime' p q r
+
+instance (P p x
+        , P q x
+        , P r x
+        , PP p x ~ Int
+        , PP q x ~ Int
+        , PP r x ~ Rational
+        ) => P (MkTime' p q r) x where
+  type PP (MkTime' p q r) x = TimeOfDay
+  eval _ opts x = do
+    let msg0 = "MkTime"
+    lr <- runPQ msg0 (Proxy @p) (Proxy @q) opts x []
+    case lr of
+      Left e -> pure e
+      Right (p,q,pp,qq) -> do
+        let hhs = [hh pp, hh qq]
+        rr <- eval (Proxy @r) opts x
+        pure $ case getValueLR opts msg0 rr hhs of
+          Left e -> e
+          Right r ->
+            let mtime = TimeOfDay p q (fromRational r)
+            in mkNode opts (PresentT mtime) (show01' opts msg0 mtime "(h,m,s)=" (p,q,r)) (hhs <> [hh rr])
+
+-- | create a 'TimeOfDay' from a three-tuple of year month and day
+--
+-- >>> pz @(MkTime '(1,2,3 % 12345)) ()
+-- PresentT 01:02:00.000243013365
+--
+-- >>> pz @(MkTime Id) (12,13,65)
+-- PresentT 12:13:65
+--
+-- >>> pz @(MkTime Id) (17,3,13)
+-- PresentT 17:03:13
+--
+data MkTime p
+type MkTimeT p = MkTime' (Fst p) (Snd p) (Thd p)
+
+instance P (MkTimeT p) x => P (MkTime p) x where
+  type PP (MkTime p) x = PP (MkTimeT p) x
+  eval _ = eval (Proxy @(MkTimeT p))
+
+
+-- | uncreate a 'TimeOfDay' returning hour minute seconds picoseconds
+--
+-- >>> pz @(ReadP UTCTime "2019-01-01 12:13:14.1234Z" >> ToTime Id >> UnMkTime Id) ()
+-- PresentT (12,13,70617 % 5000)
+--
+-- >>> pz @(ReadP UTCTime Id >> ToTime Id >> UnMkTime Id) "2020-07-22 08:01:14.127Z"
+-- PresentT (8,1,14127 % 1000)
+--
+-- >>> pz @(ReadP ZonedTime Id >> '(UnMkDay (ToDay Id), UnMkTime (ToTime Id))) "2020-07-11 11:41:12.333 CET"
+-- PresentT ((2020,7,11),(11,41,12333 % 1000))
+--
+data UnMkTime p
+
+instance ( PP p x ~ TimeOfDay
+         , P p x
+         ) => P (UnMkTime p) x where
+  type PP (UnMkTime p) x = (Int, Int, Rational)
+  eval _ opts x = do
+    let msg0 = "UnMkTime"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let TimeOfDay h m s = p
+            b = (h, m, toRational s)
+        in mkNode opts (PresentT b) (show01 opts msg0 b p) [hh pp]
+
+
+-- microsoft json date is x*1000 ie milliseconds
+
+-- | convert posix time (seconds since 01-01-1970) to 'UTCTime'
+--
+-- >>> pl @(PosixToUTCTime Id) 1593384312
+-- Present 2020-06-28 22:45:12 UTC (PosixToUTCTime 2020-06-28 22:45:12 UTC | 1593384312 % 1)
+-- PresentT 2020-06-28 22:45:12 UTC
+--
+-- >>> pl @(PosixToUTCTime Id >> UTCTimeToPosix Id) 1593384312
+-- Present 1593384312 % 1 ((>>) 1593384312 % 1 | {UTCTimeToPosix 1593384312 % 1 | 2020-06-28 22:45:12 UTC})
+-- PresentT (1593384312 % 1)
+--
+-- >>> pl @(PosixToUTCTime (Id % 1000)) 1593384312000
+-- Present 2020-06-28 22:45:12 UTC (PosixToUTCTime 2020-06-28 22:45:12 UTC | 1593384312 % 1)
+-- PresentT 2020-06-28 22:45:12 UTC
+--
+-- >>> pl @(PosixToUTCTime Id) (3600*4+60*7+12)
+-- Present 1970-01-01 04:07:12 UTC (PosixToUTCTime 1970-01-01 04:07:12 UTC | 14832 % 1)
+-- PresentT 1970-01-01 04:07:12 UTC
+--
+-- >>> pz @(Rescan "^Date\\((\\d+)([^\\)]+)\\)" Id >> Head Id >> Snd Id >> ReadP Integer (Id !! 0) >> PosixToUTCTime (Id % 1000)) "Date(1530144000000+0530)"
+-- PresentT 2018-06-28 00:00:00 UTC
+--
+data PosixToUTCTime p
+
+instance ( PP p x ~ Rational
+         , P p x
+         ) => P (PosixToUTCTime p) x where
+  type PP (PosixToUTCTime p) x = UTCTime
+  eval _ opts x = do
+    let msg0 = "PosixToUTCTime"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let d = P.posixSecondsToUTCTime (fromRational p)
+        in mkNode opts (PresentT d) (show01 opts msg0 d p) [hh pp]
+
+-- | convert 'UTCTime' to posix time (seconds since 01-01-1970)
+--
+-- >>> pl @(ReadP UTCTime Id >> UTCTimeToPosix Id) "2020-06-28 22:45:12 UTC"
+-- Present 1593384312 % 1 ((>>) 1593384312 % 1 | {UTCTimeToPosix 1593384312 % 1 | 2020-06-28 22:45:12 UTC})
+-- PresentT (1593384312 % 1)
+--
+-- >>> pz @(Rescan "^Date\\((\\d+)([^\\)]+)\\)" Id >> Head Id >> Snd Id >> ((ReadP Integer (Id !! 0) >> PosixToUTCTime (Id % 1000)) &&& ReadP TimeZone (Id !! 1))) "Date(1530144000000+0530)"
+-- PresentT (2018-06-28 00:00:00 UTC,+0530)
+--
+-- not so useful: instead use ParseTimeP FormatTimeP with %s %q %z etc
+--
+-- >>> pz @(ParseTimeP ZonedTime "%s%Q%z" Id)  "153014400.000+0530"
+-- PresentT 1974-11-07 05:30:00 +0530
+--
+data UTCTimeToPosix p
+
+instance ( PP p x ~ UTCTime
+         , P p x
+         ) => P (UTCTimeToPosix p) x where
+  type PP (UTCTimeToPosix p) x = Rational
+  eval _ opts x = do
+    let msg0 = "UTCTimeToPosix"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let d = toRational $ P.utcTimeToPOSIXSeconds p
+        in mkNode opts (PresentT d) (show01 opts msg0 d p) [hh pp]
+

@@ -0,0 +1,644 @@+{-# OPTIONS -Wall #-}
+{-# OPTIONS -Wno-compat #-}
+{-# OPTIONS -Wincomplete-record-updates #-}
+{-# OPTIONS -Wincomplete-uni-patterns #-}
+{-# OPTIONS -Wredundant-constraints #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE NoOverloadedLists #-}
+{-# LANGUAGE NoStarIsType #-}
+{- |
+     promoted 'Either' functions
+-}
+module Predicate.Data.Either (
+
+ -- ** boolean predicates
+    IsLeft
+  , IsRight
+
+ -- ** constructors
+  , MkLeft
+  , MkLeft'
+  , MkRight
+  , MkRight'
+
+ -- ** get rid of Either
+  , Left'
+  , Right'
+  , LeftDef
+  , LeftFail
+  , RightDef
+  , RightFail
+  , EitherBool
+  , EitherIn
+  , PartitionEithers
+
+ -- ** miscellaneous
+  , type (|||)
+  , type (+++)
+
+ ) where
+import Predicate.Core
+import Predicate.Util
+import GHC.TypeLits (ErrorMessage((:$$:),(:<>:)))
+import qualified GHC.TypeLits as GL
+import Data.Proxy
+import Data.Kind (Type)
+import Data.Either
+
+-- $setup
+-- >>> :set -XDataKinds
+-- >>> :set -XTypeApplications
+-- >>> :set -XTypeOperators
+-- >>> :set -XOverloadedStrings
+-- >>> :set -XNoOverloadedLists
+-- >>> 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 Id) (Left 20)
+-- PresentT 21
+--
+-- >>> pz @(Left' >> Succ Id) (Right 'a')
+-- FailT "Left' found Right"
+--
+data Left'
+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 (FailT (msg0 <> " found Right")) "" []
+         Left a -> mkNode opts (PresentT a) (msg0 <> " " <> showL opts a) []
+
+-- | extracts the right value from an 'Either'
+--
+-- >>> pz @(Right' >> Succ Id) (Right 20)
+-- PresentT 21
+--
+-- >>> pz @(Right' >> Succ Id) (Left 'a')
+-- FailT "Right' found Left"
+--
+data Right'
+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 (FailT (msg0 <> " found Left")) "" []
+         Right a -> mkNode opts (PresentT a) (msg0 <> " " <> showL opts a) []
+
+-- | similar 'Control.Arrow.|||'
+--
+-- >>> pz @(Pred Id ||| Id) (Left 13)
+-- PresentT 12
+--
+-- >>> pz @(ShowP Id ||| Id) (Right "hello")
+-- PresentT "hello"
+--
+-- >>> pl @('True ||| 'False) (Left "someval")
+-- True ((|||) Left True | "someval")
+-- TrueT
+--
+-- >>> pl @('True ||| 'False) (Right "someval")
+-- False ((|||) Right False | "someval")
+-- FalseT
+--
+-- >>> pl @(ShowP (Succ Id) ||| ShowP Id) (Left 123)
+-- Present "124" ((|||) Left "124" | 123)
+-- PresentT "124"
+--
+-- >>> pl @(ShowP (Succ Id) ||| ShowP Id) (Right True)
+-- Present "True" ((|||) Right "True" | True)
+-- PresentT "True"
+--
+-- >>> pl @(EitherIn (Not Id) Id) (Right True)
+-- Present True ((|||) Right True | True)
+-- PresentT True
+--
+-- >>> pl @(EitherIn (Not Id) Id) (Left True)
+-- False ((|||) Left False | True)
+-- FalseT
+--
+data p ||| q
+infixr 2 |||
+type EitherIn p q = p ||| q
+
+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 opts msg0 pp [] of
+          Left e -> e
+          Right a1 -> let msg1 = msg0 ++ " Left"
+                      in mkNode opts (_tBool pp) (show01 opts msg1 a1 a) [hh pp]
+      Right a -> do
+        qq <- eval (Proxy @q) opts a
+        pure $ case getValueLR opts msg0 qq [] of
+          Left e -> e
+          Right a1 ->
+            let msg1 = msg0 ++ " Right"
+            in mkNode opts (_tBool qq) (show01 opts msg1 a1 a) [hh qq]
+
+-- | similar to 'isLeft'
+--
+-- >>> pz @(IsLeft Id) (Right 123)
+-- FalseT
+--
+-- >>> pz @(IsLeft Id) (Left 'a')
+-- TrueT
+--
+data IsLeft p
+
+instance ( P p x
+         , PP p x ~ Either a b
+         ) => P (IsLeft p) x where
+  type PP (IsLeft p) x = Bool
+  eval _ opts x = do
+    let msg0 = "IsLeft"
+    pp <- eval (Proxy @p) opts x
+    let hhs = [hh pp]
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right (Left _) -> mkNodeB opts True msg0 hhs
+      Right (Right _) -> mkNodeB opts False msg0 hhs
+
+-- | similar to 'isRight'
+--
+-- >>> pz @(IsRight Id) (Right 123)
+-- TrueT
+--
+-- >>> pz @(IsRight Id) (Left "aa")
+-- FalseT
+--
+data IsRight p
+
+instance ( P p x
+         , PP p x ~ Either a b
+         ) => P (IsRight p) x where
+  type PP (IsRight p) x = Bool
+  eval _ opts x = do
+    let msg0 = "IsRight"
+    pp <- eval (Proxy @p) opts x
+    let hhs = [hh pp]
+    pure $ case getValueLR opts msg0 pp [] of
+      Left e -> e
+      Right (Left _) -> mkNodeB opts False msg0 hhs
+      Right (Right _) -> mkNodeB opts True msg0 hhs
+
+
+-- | similar 'Control.Arrow.+++'
+--
+-- >>> pz @(Pred Id +++ Id) (Left 13)
+-- PresentT (Left 12)
+--
+-- >>> pz @(ShowP Id +++ Reverse) (Right "hello")
+-- PresentT (Right "olleh")
+--
+-- >>> pl @(HeadDef 'False Id +++ Id) (Right @[Bool] 1) -- need @[Bool] cos we said 'False!
+-- Present Right 1 ((+++) Right 1 | 1)
+-- PresentT (Right 1)
+--
+-- >>> pl @(HeadDef 'False Id +++ Id) (Left [True,False]) -- need @[Bool] cos we said 'False!
+-- Present Left True ((+++) Left True | [True,False])
+-- PresentT (Left True)
+--
+-- >>> pl @(Not Id +++ Id) (Right True)
+-- Present Right True ((+++) Right True | True)
+-- PresentT (Right True)
+--
+-- >>> pl @(Not Id +++ Id) (Right 12)
+-- Present Right 12 ((+++) Right 12 | 12)
+-- PresentT (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)
+-- PresentT (Right 1)
+--
+-- >>> pl @(HeadDef () Id +++ Id) (Right @[()] 1) -- this breaks! cos Left doesnt have a type
+-- Present Right 1 ((+++) Right 1 | 1)
+-- PresentT (Right 1)
+--
+-- >>> pl @(Not Id +++ Id) (Right @Bool 12)
+-- Present Right 12 ((+++) Right 12 | 12)
+-- PresentT (Right 12)
+--
+data p +++ q
+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 opts msg0 pp [] of
+          Left e -> e
+          Right a1 ->
+            let msg1 = msg0 ++ " Left"
+            in mkNode opts (PresentT (Left a1)) (msg1 <> " " <> showL opts a1 <> showVerbose opts " | " a) [hh pp]
+      Right a -> do
+        qq <- eval (Proxy @q) opts a
+        pure $ case getValueLR opts msg0 qq [] of
+          Left e -> e
+          Right a1 ->
+            let msg1 = msg0 ++ " Right"
+            in mkNode opts (PresentT (Right a1)) (msg1 <> " " <> showL opts a1 <> showVerbose opts " | " a) [hh qq]
+
+-- | similar to 'partitionEithers'
+--
+-- >>> pz @PartitionEithers [Left 'a',Right 2,Left 'c',Right 4,Right 99]
+-- PresentT ("ac",[2,4,99])
+--
+-- >>> pz @PartitionEithers [Right 2,Right 4,Right 99]
+-- PresentT ([],[2,4,99])
+--
+-- >>> pz @PartitionEithers [Left 'a',Left 'c']
+-- PresentT ("ac",[])
+--
+-- >>> pz @PartitionEithers ([] :: [Either () Int])
+-- PresentT ([],[])
+--
+-- >>> 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])
+-- PresentT ([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])
+-- PresentT ("xabz",[1,10])
+--
+data PartitionEithers
+
+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 (PresentT b) (show01 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 Id > 4) (Snd Id >> Fst Id) (Snd Id >> Snd Id)) (24,(-1,999))
+-- PresentT (Right 999)
+--
+-- >>> pz @(EitherBool (Fst Id > 4) (Fst (Snd Id)) (Snd (Snd Id))) (1,(-1,999))
+-- PresentT (Left (-1))
+--
+-- >>> pl @(EitherBool (Fst Id > 10) (Snd Id >> Fst Id) (Snd Id >> Snd Id)) (7,('x',99))
+-- Present Left 'x' (EitherBool(False) Left 'x')
+-- PresentT (Left 'x')
+--
+-- >>> pl @(EitherBool (Fst Id > 10) (Snd Id >> Fst Id) (Snd Id >> Snd Id)) (11,('x',99))
+-- Present Right 99 (EitherBool(True) Right 99)
+-- PresentT (Right 99)
+--
+-- >>> pl @(EitherBool (Gt 10) "found left" 99) 12
+-- Present Right 99 (EitherBool(True) Right 99)
+-- PresentT (Right 99)
+--
+-- >>> pl @(EitherBool (Gt 10) "found left" 99) 7
+-- Present Left "found left" (EitherBool(False) Left "found left")
+-- PresentT (Left "found left")
+--
+data EitherBool b p q
+
+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 opts (msg0 <> " b failed") bb [] of
+      Left e -> pure e
+      Right False -> do
+        pp <- eval (Proxy @p) opts z
+        pure $ case getValueLR opts (msg0 <> " p failed") pp [hh bb] of
+          Left e -> e
+          Right p -> mkNode opts (PresentT (Left p)) (msg0 <> "(False) Left " <> showL opts p) [hh bb, hh pp]
+      Right True -> do
+        qq <- eval (Proxy @q) opts z
+        pure $ case getValueLR opts (msg0 <> " q failed") qq [hh bb] of
+          Left e -> e
+          Right q -> mkNode opts (PresentT (Right q)) (msg0 <> "(True) Right " <> showL opts q) [hh bb, hh qq]
+
+-- | similar to 'Control.Arrow.|||' but additionally gives \'p\' and \'q\' the original input
+--
+-- >>> pz @(EitherX (ShowP (Fst (Fst Id) + Snd Id)) (ShowP Id) (Snd Id)) (9,Left 123)
+-- PresentT "132"
+--
+-- >>> pz @(EitherX (ShowP (Fst (Fst Id) + Snd Id)) (ShowP Id) (Snd Id)) (9,Right 'x')
+-- PresentT "((9,Right 'x'),'x')"
+--
+-- >>> pz @(EitherX (ShowP Id) (ShowP (Second (Succ Id))) (Snd Id)) (9,Right 'x')
+-- PresentT "((9,Right 'x'),'y')"
+--
+data EitherX p q r
+instance (P r x
+        , P p (x,a)
+        , P q (x,b)
+        , PP r x ~ Either a b
+        , PP p (x,a) ~ c
+        , PP q (x,b) ~ c
+        ) => P (EitherX p q r) x where
+  type PP (EitherX p q r) x = EitherXT (PP r x) x p
+  eval _ opts x = do
+    let msg0 = "EitherX"
+    rr <- eval (Proxy @r) opts x
+    case getValueLR opts msg0 rr [] of
+      Left e -> pure e
+      Right (Left a) -> do
+        let msg1 = msg0 <> "(Left)"
+        pp <- eval (Proxy @p) opts (x,a)
+        pure $ case getValueLR opts msg1 pp [hh rr] of
+          Left e -> e
+          Right _ -> mkNode opts (_tBool pp) msg1 [hh rr, hh pp]
+      Right (Right b) -> do
+        let msg1 = msg0 <> "(Right)"
+        qq <- eval (Proxy @q) opts (x,b)
+        pure $ case getValueLR opts msg1 qq [hh rr] of
+          Left e -> e
+          Right _ -> mkNode opts (_tBool qq) msg1 [hh rr, hh qq]
+
+type family EitherXT lr x p where
+  EitherXT (Either a b) x p = PP p (x,a)
+  EitherXT o _ _ = GL.TypeError (
+      'GL.Text "EitherXT: expected 'Either a b' "
+      ':$$: 'GL.Text "o = "
+      ':<>: 'GL.ShowType o)
+
+-- | 'Data.Either.Left' constructor
+data MkLeft' t p
+
+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 opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let d = Left p
+        in mkNode opts (PresentT d) (msg0 <> " Left " <> showL opts p) [hh pp]
+
+-- | 'Data.Either.Left' constructor
+--
+-- >>> pz @(MkLeft _ Id) 44
+-- PresentT (Left 44)
+--
+data MkLeft (t :: Type) p
+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
+
+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 opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let d = Right p
+        in mkNode opts (PresentT d) (msg0 <> " Right " <> showL opts p) [hh pp]
+
+-- | 'Data.Either.Right' constructor
+--
+-- >>> pz @(MkRight _ Id) 44
+-- PresentT (Right 44)
+--
+data MkRight (t :: Type) p
+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)
+-- PresentT (102 % 5)
+--
+-- >>> pz @(LeftDef (1 % 4) Id) (Right "aa")
+-- PresentT (1 % 4)
+--
+-- >>> pz @(LeftDef (PrintT "found right=%s fst=%d" '(Fst Id,Fst (Snd Id))) (Snd Id)) (123,Right "xy")
+-- PresentT "found right=xy fst=123"
+--
+-- >>> pz @(LeftDef (MEmptyT _) Id) (Right 222)
+-- PresentT ()
+--
+-- >>> pz @(LeftDef (MEmptyT (SG.Sum _)) Id) (Right 222)
+-- PresentT (Sum {getSum = 0})
+--
+data LeftDef p q
+
+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 opts msg0 qq [] of
+      Left e -> pure e
+      Right q ->
+        case q of
+          Left a -> pure $ mkNode opts (PresentT a) (msg0 <> " Left") [hh qq]
+          Right b -> do
+            pp <- eval (Proxy @p) opts (b,x)
+            pure $ case getValueLR opts msg0 pp [hh qq] of
+              Left e -> e
+              Right p -> mkNode opts (PresentT p) (msg0 <> " Right") [hh qq, hh pp]
+
+-- | 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)
+-- PresentT (102 % 5)
+--
+-- >>> pz @(RightDef (1 % 4) Id) (Left "aa")
+-- PresentT (1 % 4)
+--
+-- >>> pz @(RightDef (PrintT "found left=%s fst=%d" '(Fst Id,Fst (Snd Id))) (Snd Id)) (123,Left "xy")
+-- PresentT "found left=xy fst=123"
+--
+-- >>> pz @(RightDef (MEmptyT _) Id) (Left 222)
+-- PresentT ()
+--
+-- >>> pz @(RightDef (MEmptyT (SG.Sum _)) Id) (Left 222)
+-- PresentT (Sum {getSum = 0})
+--
+data RightDef p q
+
+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 opts msg0 qq [] of
+      Left e -> pure e
+      Right q ->
+        case q of
+          Right b -> pure $ mkNode opts (PresentT b) (msg0 <> " Right") [hh qq]
+          Left a -> do
+            pp <- eval (Proxy @p) opts (a,x)
+            pure $ case getValueLR opts msg0 pp [hh qq] of
+              Left e -> e
+              Right p -> mkNode opts (PresentT p) (msg0 <> " Left") [hh qq, hh pp]
+
+
+-- | 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)
+-- PresentT 20.4
+--
+-- >>> pz @(LeftFail "oops" Id) (Right "aa")
+-- FailT "oops"
+--
+-- >>> pz @(LeftFail (PrintT "found right=%s fst=%d" '(Fst Id,Fst (Snd Id))) (Snd Id)) (123,Right "xy")
+-- FailT "found right=xy fst=123"
+--
+-- >>> pz @(LeftFail (MEmptyT _) Id) (Right 222)
+-- FailT ""
+--
+-- >>> pl @(LeftFail (PrintF "someval=%d" (Fst (Snd Id))) (Snd Id)) (13::Int,Right @(SG.Sum Int) "abc")
+-- Error someval=13 (LeftFail Right)
+-- FailT "someval=13"
+--
+-- >>> pl @(LeftFail (PrintF "someval=%s" (Fst Id)) Id) (Right @(SG.Sum Int) ("abc" :: String))
+-- Error someval=abc (LeftFail Right)
+-- FailT "someval=abc"
+--
+-- >>> pl @(LeftFail (PrintF "found rhs=%d" (Fst Id)) Id) (Right @String @Int 10)
+-- Error found rhs=10 (LeftFail Right)
+-- FailT "found rhs=10"
+--
+-- >>> pl @(LeftFail (PrintF "found rhs=%d" (Snd Id >> Snd Id >> Snd Id)) (Snd Id >> Fst Id)) ('x',(Right 10,23::Int))
+-- Error found rhs=23 (LeftFail Right)
+-- FailT "found rhs=23"
+--
+-- >>> pl @(LeftFail (PrintF "found rhs=%d" (Snd (Snd (Snd Id)))) (Fst (Snd Id))) ('x',(Left "abc",23::Int))
+-- Present "abc" (Left)
+-- PresentT "abc"
+--
+data LeftFail p q
+
+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 opts msg0 qq [] of
+      Left e -> pure e
+      Right q ->
+        case q of
+          Left a -> pure $ mkNode opts (PresentT a) "Left" [hh qq]
+          Right b -> do
+            pp <- eval (Proxy @p) opts (b,x)
+            pure $ case getValueLR opts msg0 pp [hh qq] of
+              Left e -> e
+              Right p -> mkNode opts (FailT 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)
+-- PresentT 20.4
+--
+-- >>> pz @(RightFail "oops" Id) (Left "aa")
+-- FailT "oops"
+--
+-- >>> pz @(RightFail (PrintT "found left=%s fst=%d" '(Fst Id,Fst (Snd Id))) (Snd Id)) (123,Left "xy")
+-- FailT "found left=xy fst=123"
+--
+-- >>> pz @(RightFail (MEmptyT _) Id) (Left 222)
+-- FailT ""
+--
+data RightFail p q
+
+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 opts msg0 qq [] of
+      Left e -> pure e
+      Right q ->
+        case q of
+          Right b -> pure $ mkNode opts (PresentT b) "Right" [hh qq]
+          Left a -> do
+            pp <- eval (Proxy @p) opts (a,x)
+            pure $ case getValueLR opts msg0 pp [hh qq] of
+              Left e -> e
+              Right p -> mkNode opts (FailT p) (msg0 <> " Left") [hh qq, hh pp]