predicate-typed 0.7.4.2 → 0.7.4.3

raw patch · 40 files changed

+3090/−1292 lines, 40 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• doctest/doctests.hs +0/−1
• predicate-typed.cabal +4/−2
• src/Predicate/Core.hs +227/−149
• src/Predicate/Data/Bits.hs +2/−4
• src/Predicate/Data/Char.hs +1/−0
• src/Predicate/Data/Condition.hs +79/−68
• src/Predicate/Data/DateTime.hs +5/−6
• src/Predicate/Data/Either.hs +127/−55
• src/Predicate/Data/Elr.hs +716/−0
• src/Predicate/Data/Enum.hs +10/−8
• src/Predicate/Data/Extra.hs +2/−3
• src/Predicate/Data/Foldable.hs +113/−51
• src/Predicate/Data/IO.hs +0/−1
• src/Predicate/Data/Index.hs +4/−3
• src/Predicate/Data/Iterator.hs +24/−12
• src/Predicate/Data/Json.hs +1/−0
• src/Predicate/Data/Lifted.hs +331/−65
• src/Predicate/Data/List.hs +96/−128
• src/Predicate/Data/Maybe.hs +150/−191
• src/Predicate/Data/Monoid.hs +10/−14
• src/Predicate/Data/Numeric.hs +18/−26
• src/Predicate/Data/Ordering.hs +2/−2
• src/Predicate/Data/Proxy.hs +25/−14
• src/Predicate/Data/ReadShow.hs +2/−1
• src/Predicate/Data/Regex.hs +19/−22
• src/Predicate/Data/String.hs +14/−8
• src/Predicate/Data/These.hs +276/−277
• src/Predicate/Data/Tuple.hs +190/−41
• src/Predicate/Elr.hs +343/−0
• src/Predicate/Misc.hs +145/−56
• src/Predicate/Prelude.hs +5/−1
• src/Predicate/Refined.hs +3/−2
• src/Predicate/Refined2.hs +5/−4
• src/Predicate/Refined3.hs +4/−3
• src/Predicate/Refined5.hs +5/−5
• src/Predicate/TH_Orphans.hs +3/−0
• src/Predicate/Util.hs +110/−62
• test/TestPredicate.hs +3/−5
• test/TestRefined.hs +15/−0
• test/TestRefined2.hs +1/−2

@@ -1,5 +1,4 @@ import Test.DocTest
--- main = doctest ["src", "--verbose"]
 main :: IO ()
 
 main = doctest ["src","-XNoStarIsType"]

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: 1cbf6c9b513c819809aea5c7ba639f8270876d5ac8734ba14595ede9fbbc5a41+-- hash: ce998dc318ca06d53f625b8ae47f833c8bfabd675847d56a78cfa35f25fd9d2b  name:           predicate-typed-version:        0.7.4.2+version:        0.7.4.3 synopsis:       Predicates, Refinement types and Dsl description:    Please see the README on GitHub at <https://github.com/gbwey/predicate-typed#readme> category:       Data@@ -33,6 +33,7 @@       Predicate.Data.Condition       Predicate.Data.DateTime       Predicate.Data.Either+      Predicate.Data.Elr       Predicate.Data.Enum       Predicate.Data.Extra       Predicate.Data.Foldable@@ -52,6 +53,7 @@       Predicate.Data.String       Predicate.Data.These       Predicate.Data.Tuple+      Predicate.Elr       Predicate.Examples.Common       Predicate.Examples.Refined2       Predicate.Examples.Refined3

@@ -31,10 +31,9 @@   , Map'
   , Map
   , Do
-  , Pure
-  , Coerce
   , OneP
   , Swap
+  , Arg'
 
   -- ** impure evaluation
   , pan
@@ -118,11 +117,16 @@  -- ** core class
   , P(..)
 
+ -- ** type families
+  , DoExpandT
+  , DoExpandLT
+  , ArgT
   ) where
 import Predicate.Misc
 import Predicate.Util
+import Predicate.Elr
 import qualified GHC.TypeLits as GL
-import GHC.TypeLits (Symbol,Nat,KnownSymbol,KnownNat)
+import GHC.TypeLits (Symbol,Nat,KnownSymbol,KnownNat,ErrorMessage((:$$:),(:<>:)))
 import Control.Lens
 import Data.Foldable (toList)
 import Data.Proxy (Proxy(..))
@@ -134,10 +138,10 @@ import Data.List (find)
 import Data.Maybe (fromMaybe)
 import Data.Tree (Tree)
-import Data.Coerce (Coercible)
 import Data.Tree.Lens (root)
 import qualified Text.Regex.PCRE.Heavy as RH
 import GHC.Stack (HasCallStack)
+import qualified Data.Semigroup as SG
 -- $setup
 -- >>> :set -XDataKinds
 -- >>> :set -XTypeApplications
@@ -941,7 +945,7 @@ pav = run @OAV @p
 -- | display the evaluation tree using unicode and colors
 -- @
---   pu @'(Id, "abc", 123) [1..4]
+--   pu @'(Id, "abc", 'True) [1..4]
 -- @
 pu = run @OU @p
 -- | displays the evaluation tree using unicode and colors with background colors
@@ -1114,7 +1118,7 @@                     if anyOf (ttForest . folded . root . peValP) (has _FailP) qq
                     then qq & ttForest %~ (hh pp:) -- we still need pp for context
                     else e
-          Right q -> mkNodeCopy opts qq (lit3 opts msg0 q "" (topMessageEgregious (qq ^. ttString))) [hh pp, hh qq]
+          Right q -> mkNodeCopy opts qq (lit3 opts msg0 q "" (topMessageEgregious (qq ^. ttString))) [hh pp]
 
 -- | infixl version of 'Predicate.Core.>>'
 data p >>> q deriving Show
@@ -1230,8 +1234,16 @@     let msg0 = "UnproxyT(" <> showT @t <> ")"
     in pure $ mkNode opts (Fail msg0) "you probably meant to get access to the type of PP only and not evaluate (see Pop0)" []
 
--- | similar to 'length'
+-- | similar to 'Length' but displays the input value and works only for lists
 --
+-- >>> pl @Len "abcd"
+-- Present 4 (Len 4 | "abcd")
+-- Val 4
+--
+-- >>> pl @Len [1..3000]
+-- Present 3000 (Len 3000 | [1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,7...)
+-- Val 3000
+--
 -- >>> pz @Len [10,4,5,12,3,4]
 -- Val 6
 --
@@ -1242,17 +1254,23 @@ -- Val True
 --
 data Len deriving Show
-instance ( Show a
-         , x ~ [a]
+
+instance ( x ~ [a]
+         , Show a
          ) => P Len x where
   type PP Len x = Int
-  eval _ opts as =
+  eval _ opts as' =
     let msg0 = "Len"
-        n = length as
-    in pure $ mkNode opts (Val n) (show3 opts msg0 n as) []
+    in pure $ case chkSize opts { oLarge = True } msg0 as' [] of
+         Left e -> e
+         Right (asLen,_) ->
+           mkNode opts (Val asLen) (show3 opts msg0 asLen as') []
 
 -- | similar to 'length' for 'Foldable' instances
 --
+-- >>> pz @(Length Snd) (123,"abcdefg") -- if this breaks then get rid of Show a!
+-- Val 7
+--
 -- >>> pz @(Length Id) (Left "aa")
 -- Val 0
 --
@@ -1269,7 +1287,6 @@ 
 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
@@ -1278,9 +1295,11 @@     pp <- eval (Proxy @p) opts x
     pure $ case getValueLR NoInline opts msg0 pp [] of
       Left e -> e
-      Right p ->
-            let n = length p
-            in mkNode opts (Val n) (show3 opts msg0 n p) [hh pp]
+      Right p' ->
+        case chkSize opts { oLarge = True } msg0 p' [] of
+          Left e -> e
+          Right (pLen,_) ->
+            mkNode opts (Val pLen) (msg0 <> " " <> show pLen) [hh pp]
 
 -- | 'not' function
 --
@@ -1434,6 +1453,7 @@ -- Fail "OneP:expected one element(empty)"
 --
 data OneP deriving Show
+
 instance ( Foldable t
          , x ~ t a
          ) => P OneP x where
@@ -1443,8 +1463,10 @@     pure $ case toList x of
       [] -> mkNode opts (Fail (msg0 <> ":expected one element(empty)")) "" []
       [a] -> mkNode opts (Val a) msg0 []
-      as -> let n = length as
-            in mkNode opts (Fail (msg0 <> ":expected one element(" <> show n <> ")")) "" []
+      as' -> case chkSize opts msg0 as' [] of
+               Left e -> e
+               Right (asLen,_) ->
+                 mkNode opts (Fail (msg0 <> ":expected one element(" <> show asLen <> ")")) "" []
 
 --type OneP = Guard "expected list of length 1" (Len == 1) >> Head
 --type OneP = Guard (PrintF "expected list of length 1 but found length=%d" Len) (Len == 1) >> Head
@@ -1608,13 +1630,13 @@     let msg0 = "All"
     case chkSize opts msg0 x [] of
       Left e -> pure e
-      Right xs -> do
+      Right (xsLen,xs) -> do
         ts <- zipWithM (\i a -> ((i, a),) <$> evalBoolHide @p opts a) [0::Int ..] xs
         pure $ case splitAndAlign opts msg0 ts of
              Left e -> e
              Right abcs ->
                let hhs = map (hh . prefixNumberToTT) ts
-                   msg1 = msg0 ++ "(" ++ showL opts (length x) ++ ")"
+                   msg1 = msg0 ++ "(" ++ showL opts xsLen ++ ")"
                in case find (not . view _1) abcs of
                     Nothing -> mkNodeB opts True msg1 hhs
                     Just (_,(i,_),tt) ->
@@ -1657,13 +1679,13 @@     let msg0 = "Any"
     case chkSize opts msg0 x [] of
       Left e -> pure e
-      Right xs -> do
+      Right (xsLen,xs) -> do
         ts <- zipWithM (\i a -> ((i, a),) <$> evalBoolHide @p opts a) [0::Int ..] xs
         pure $ case splitAndAlign opts msg0 ts of
              Left e -> e
              Right abcs ->
                let hhs = map (hh . prefixNumberToTT) ts
-                   msg1 = msg0 ++ "(" ++ showL opts (length xs) ++ ")"
+                   msg1 = msg0 ++ "(" ++ showL opts xsLen ++ ")"
                in case find (view _1) abcs of
                     Nothing -> mkNodeB opts False msg1 hhs
                     Just (_,(i,_),tt) ->
@@ -1902,7 +1924,7 @@         let b = extractL8C p
         in mkNode opts (Val b) (show3 opts msg0 b p) [hh pp]
 
--- | similar to 'map' for foldable
+-- | similar to 'map' for Foldable types
 --
 -- >>> pz @(Map' Pred Id) [1..5]
 -- Val [0,1,2,3,4]
@@ -1926,7 +1948,7 @@       Right q -> do
         case chkSize opts msg0 q [hh qq] of
           Left e -> pure e
-          Right xs -> do
+          Right (_,xs) -> do
             ts <- zipWithM (\i a -> ((i, a),) <$> evalHide @p opts a) [0::Int ..] xs
             pure $ case splitAndAlign opts msg0 ts of
                  Left e -> e
@@ -1951,7 +1973,7 @@     let msg0 = "Map"
     case chkSize opts msg0 x [] of
       Left e -> pure e
-      Right xs -> do
+      Right (_,xs) -> do
         ts <- zipWithM (\i a -> ((i, a),) <$> evalHide @p opts a) [0::Int ..] xs
         pure $ case splitAndAlign opts msg0 ts of
              Left e -> e
@@ -2050,6 +2072,12 @@ -- >>> pz @(Fst && (Length Snd == 4)) (True,[12,11,12,13,14])
 -- Val False
 --
+-- >>> pz @(Uncurry (+:)) ([2..5],1)
+-- Val [2,3,4,5,1]
+--
+-- >>> pz @(Uncurry (==!)) ('x','y')
+-- Val LT
+--
 data p && q deriving Show
 infixr 3 &&
 
@@ -2070,7 +2098,7 @@                   (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 <> nullIf " | " zz) [hh pp, hh qq]
+        in mkNodeB opts (p&&q) (showL opts p <> " " <> msg0 <> " " <> joinStrings (showL opts q) zz) [hh pp, hh qq]
 
 -- | short circuit version of boolean And
 --
@@ -2209,7 +2237,7 @@         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 <> nullIf " | " zz) [hh pp, hh qq]
+        in mkNodeB opts (p~>q) (showL opts p <> " " <> msg0 <> " " <> joinStrings (showL opts q) zz) [hh pp, hh qq]
 
 
 -- | swaps using 'SwapC'
@@ -2261,7 +2289,7 @@         d = swapC pabx
     in pure $ mkNode opts (Val d) (show3 opts msg0 d pabx) []
 
--- | like 'GHC.Base.$' for expressions taking exactly on argument
+-- | like 'GHC.Base.$' for expressions taking exactly on argument (similar is 'Predicate.Misc.%%')
 -- ie this doesnt work: pz @('(,) $ 4 $ 'True) ()
 --
 -- >>> pl @(L1 $ L2 $ Id) ((1,2),(3,4))
@@ -2275,6 +2303,9 @@ -- >>> pz @('(,) 4 $ 'True) ()
 -- Val (4,True)
 --
+-- >>> pz @('(,) %% 'True %% 'False) () -- cant do this with $
+-- Val (True,False)
+--
 data (p :: k -> k1) $ (q :: k) deriving Show
 infixr 0 $
 
@@ -2285,7 +2316,7 @@ -- | similar to 'Control.Lens.&' for expressions taking exactly on argument
 --
 -- >>> pl @(Id & L1 & Singleton & Length) (13,"xyzw")
--- Present 1 (Length 1 | [13])
+-- Present 1 (Length 1)
 -- Val 1
 --
 -- >>> pl @(2 & (&&&) "abc") ()
@@ -2304,6 +2335,9 @@ -- Present 'a' (Thd 'a' | ("X",9,'a'))
 -- Val 'a'
 --
+-- >>> pz @('True %& 'False %& '(,)) ()
+-- Val (False,True)
+--
 data (q :: k) & (p :: k -> k1) deriving Show
 infixl 1 &
 
@@ -2311,126 +2345,6 @@   type PP (q & p) a = PP (p q) a
   eval _ = eval (Proxy @(p q))
 
--- | similar to 'pure'
---
--- >>> pz @(Pure Maybe Id) 4
--- Val (Just 4)
---
--- >>> pz @(Pure [] Id) 4
--- Val [4]
---
--- >>> pz @(Pure (Either String) Fst) (13,True)
--- Val (Right 13)
---
--- >>> pl @(Pure Maybe Id) 'x'
--- Present Just 'x' (Pure Just 'x' | 'x')
--- Val (Just 'x')
---
--- >>> pl @(Pure (Either _) Id) 'x'
--- Present Right 'x' (Pure Right 'x' | 'x')
--- Val (Right 'x')
---
--- >>> pl @(Pure (Either _) Id >> Swap) 'x'
--- Present Left 'x' ((>>) Left 'x' | {Swap Left 'x' | Right 'x'})
--- Val (Left 'x')
---
--- >>> pl @(Pure (Either ()) Id >> Swap) 'x'
--- Present Left 'x' ((>>) Left 'x' | {Swap Left 'x' | Right 'x'})
--- Val (Left 'x')
---
--- >>> pl @(Pure (Either String) Id >> Swap) 123
--- Present Left 123 ((>>) Left 123 | {Swap Left 123 | Right 123})
--- Val (Left 123)
---
-data Pure (t :: Type -> Type) p deriving Show
-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 NoInline opts msg0 pp [] of
-      Left e -> e
-      Right a ->
-        let b = pure a
-        in mkNode opts (Val b) (show3 opts msg0 b a) [hh pp]
-
--- | similar to 'Data.Coerce.coerce'
---
--- >>> pz @(Coerce (SG.Sum Integer)) (Identity (-13))
--- Val (Sum {getSum = -13})
---
--- >>> pl @(Coerce SG.Any) True
--- Present Any {getAny = True} (Coerce Any {getAny = True} | True)
--- Val (Any {getAny = True})
---
--- >>> pl @(Coerce Bool) (SG.Any True)
--- Present True (Coerce True | Any {getAny = True})
--- Val True
---
--- >>> pz @(Proxy 'True >> Coerce (Proxy 'False)) () ^!? acts . _Val . to typeRep
--- Just 'False
---
--- >>> pz @(Proxy Int >> Coerce (Proxy (String,Char))) () ^!? acts . _Val . to typeRep
--- Just ([Char],Char)
---
--- >>> import qualified GHC.Exts as GE
--- >>> pz @(Proxy GE.Any >> Coerce (Proxy Int)) () ^!? acts . _Val . to typeRep
--- Just Int
---
--- >>> pz @(Proxy '(_,_) >> Coerce (Proxy '(Float,Int))) () ^!? acts . _Val . to typeRep
--- Just ('(,) * * Float Int)
---
-data Coerce (t :: k) deriving Show -- has to be the same kind: Type to Type or Bool to Bool ...
-
-instance ( Coercible t a
-         , Show a
-         , Show t
-         ) => P (Coerce t) a where
-  type PP (Coerce t) a = t
-  eval _ opts a =
-    let msg0 = "Coerce"
-        d = a ^. coerced
-    in pure $ mkNode opts (Val d) (show3 opts msg0 d a) []
-
-{-
- -- | extracts the value level representation of the promoted 'DayOfWeek'
- --
- -- >>> pz @'Monday ()
- -- Val Monday
- --
- -- >>> pz @'Sunday ()
- -- Val Sunday
- --
-instance GetWeekDay dy => P (dy :: DayOfWeek) a where
-  type PP dy a = DayOfWeek
-  eval _ opts _ =
-    let dy = getWeekDay @dy
-        msg = "'" <> showL opts dy
-    in pure $ mkNode opts (Val dy) msg []
-
--- | get weekday from the typelevel
-class GetWeekDay (dy :: DayOfWeek) where
-  getWeekDay :: DayOfWeek
-instance GetWeekDay 'Sunday where
-  getWeekDay = Sunday
-instance GetWeekDay 'Monday where
-  getWeekDay = Monday
-instance GetWeekDay 'Tuesday where
-  getWeekDay = Tuesday
-instance GetWeekDay 'Wednesday where
-  getWeekDay = Wednesday
-instance GetWeekDay 'Thursday where
-  getWeekDay = Thursday
-instance GetWeekDay 'Friday where
-  getWeekDay = Friday
-instance GetWeekDay 'Saturday where
-  getWeekDay = Saturday
--}
-
 -- | first element in a tuple followed by the first element
 --
 -- >>> pz @L11 ((10,"ss"),2)
@@ -2564,3 +2478,167 @@   in case pp ^. ttVal of
        Val r -> Right r
        Fail {} -> Left $ prtTree opts pp
+
+-- | creates a 'Data.Semigroup.Arg' value using @p@ and @q@
+--
+-- >>> pz @('SG.Arg (C "S") 10) ()
+-- Val (Arg 'S' 10)
+--
+instance ( P p x
+         , P q x
+         , Show (PP p x)
+         , Show (PP q x)
+         ) => P ('SG.Arg p q) x where
+  type PP ('SG.Arg p q) x = SG.Arg (PP p x) (PP q x)
+  eval _ opts x = do
+    let msg0 = "'Arg"
+    lr <- runPQ NoInline msg0 (Proxy @p) (Proxy @q) opts x []
+    pure $ case lr of
+      Left e -> e
+      Right (p,q,pp,qq) ->
+        let hhs = [hh pp, hh qq]
+            ret = SG.Arg p q
+        in mkNode opts (Val ret) (msg0 <> " " <> showL opts p <> " " <> showL opts q) hhs
+
+-- | extracts a tuple from 'Data.Semigroup.Arg'
+--
+-- >>> pz @('SG.Arg (C "S") 10 >> Arg') ()
+-- Val ('S',10)
+--
+-- >>> pz @Arg' (SG.Arg 'S' 10)
+-- Val ('S',10)
+--
+data Arg' deriving Show
+
+instance x ~ SG.Arg a b => P Arg' x where
+  type PP Arg' x = ArgT x
+  eval _ opts (SG.Arg a b) =
+    let msg0 = "Arg'"
+        ret = (a,b)
+    in pure $ mkNode opts (Val ret) msg0 []
+
+type family ArgT (x :: Type) where
+  ArgT (SG.Arg a b) = (a,b)
+  ArgT o = GL.TypeError (
+      'GL.Text "ArgT: expected 'SG.Arg a b' "
+      ':$$: 'GL.Text "o = "
+      ':<>: 'GL.ShowType o)
+
+-- | extracts the () from type level @ENone@ if the value exists
+--
+-- >>> pl @'ENone ENone
+-- Present () ('ENone)
+-- Val ()
+--
+-- >>> pz @'ENone (ERight "aaa")
+-- Fail "'ENone found ERight"
+--
+instance x ~ Elr a b => P 'ENone x where
+  type PP 'ENone x = ()
+  eval _ opts x =
+    let msg0 = "'ENone"
+    in pure $ case x of
+      ELeft {} -> mkNode opts (Fail (msg0 <> " found ELeft")) "" []
+      ENone -> mkNode opts (Val ()) msg0 []
+      ERight {} -> mkNode opts (Fail (msg0 <> " found ERight")) "" []
+      EBoth {} -> mkNode opts (Fail (msg0 <> " found EBoth")) "" []
+
+-- | extracts the @a@ from type level @ELeft a@ if the value exists
+--
+-- >>> pl @('ELeft Id) (ELeft 12)
+-- Present 12 ('ELeft)
+-- Val 12
+--
+-- >>> pz @('ELeft Id) (ERight "aaa")
+-- Fail "'ELeft found ERight"
+--
+-- >>> pz @('ELeft Id) (EBoth 999 "aaa")
+-- Fail "'ELeft found EBoth"
+--
+-- >>> pl @('ELeft Id) (ERight 12)
+-- Error 'ELeft found ERight
+-- Fail "'ELeft found ERight"
+--
+instance ( PP p x ~ Elr a b
+         , P p x
+         )
+    => P ('ELeft p) x where
+  type PP ('ELeft p) x = ELeftT (PP p x)
+  eval _ opts x = do
+    let msg0 = "'ELeft"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR NoInline opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        case p of
+          ENone -> mkNode opts (Fail (msg0 <> " found ENone")) "" [hh pp]
+          ELeft a -> mkNode opts (Val a) msg0 [hh pp]
+          ERight {} -> mkNode opts (Fail (msg0 <> " found ERight")) "" [hh pp]
+          EBoth {} -> mkNode opts (Fail (msg0 <> " found EBoth")) "" [hh pp]
+
+-- | extracts the @b@ from type level @ERight b@ if the value exists
+--
+-- >>> pz @('ERight Id) (ERight 123)
+-- Val 123
+--
+-- >>> pz @('ERight Id) (ELeft "aaa")
+-- Fail "'ERight found ELeft"
+--
+-- >>> pz @('ERight Id) (EBoth 44 "aaa")
+-- Fail "'ERight found EBoth"
+--
+instance ( PP p x ~ Elr a b
+         , P p x
+         )
+    => P ('ERight p) x where
+  type PP ('ERight p) x = ERightT (PP p x)
+  eval _ opts x = do
+    let msg0 = "'ERight"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR NoInline opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        case p of
+          ENone -> mkNode opts (Fail (msg0 <> " found ENone")) "" [hh pp]
+          ELeft {} -> mkNode opts (Fail (msg0 <> " found ELeft")) "" [hh pp]
+          ERight b -> mkNode opts (Val b) msg0 [hh pp]
+          EBoth {} -> mkNode opts (Fail (msg0 <> " found EBoth")) "" [hh pp]
+
+-- | extracts the (a,b) from type level @EBoth a b@ if the value exists
+--
+-- >>> pz @('EBoth Id Id) (EBoth 123 "abc")
+-- Val (123,"abc")
+--
+-- >>> pz @('EBoth Id 5) (EBoth 123 "abcde")
+-- Val (123,5)
+--
+-- >>> pz @('EBoth Id Id) (ELeft "aaa")
+-- Fail "'EBoth found ELeft"
+--
+-- >>> pz @('EBoth Id Id) (ERight "aaa")
+-- Fail "'EBoth found ERight"
+--
+instance ( Show a
+         , Show b
+         , P p a
+         , P q b
+         , Show (PP p a)
+         , Show (PP q b)
+         ) => P ('EBoth p q) (Elr a b) where
+  type PP ('EBoth p q) (Elr a b) = (PP p a, PP q b)
+  eval _ opts th = do
+    let msg0 = "'EBoth"
+    case th of
+      EBoth a b -> do
+        pp <- eval (Proxy @p) opts a
+        case getValueLR NoInline opts msg0 pp [] of
+           Left e -> pure e
+           Right p -> do
+             qq <- eval (Proxy @q) opts b
+             pure $ case getValueLR NoInline opts (msg0 <> " q failed p=" <> showL opts p) qq [hh pp] of
+                Left e -> e
+                Right q ->
+                  let ret = (p,q)
+                  in  mkNode opts (Val ret) (show3 opts msg0 ret (EBoth a b)) [hh pp, hh qq]
+      _ -> pure $ mkNode opts (Fail (msg0 <> " found " <> showElr th)) "" []
+

@@ -19,6 +19,7 @@ {-# LANGUAGE DerivingStrategies #-}
 -- | promoted bit manipulation functions
 module Predicate.Data.Bits (
+  -- ** functions
     type (.&.)
   , type (.|.)
   , type (.^.)
@@ -36,7 +37,6 @@   , TestBit
   , Bit
   , ZeroBits
-
  ) where
 import Predicate.Core
 import Predicate.Util
@@ -199,7 +199,6 @@   type PP (BitShift p q) x = PP (BitShiftT p q) x
   eval _ = eval (Proxy @(BitShiftT p q))
 
-
 -- | shift left by @p@ using @q@: similar to flipped version of 'Data.Bits.shiftL'
 --
 -- >>> pz @(BitShiftL 1 Id) 123
@@ -322,8 +321,7 @@       Right (fromIntegral -> p,q,pp,qq) ->
         let hhs = [hh pp, hh qq]
             d = Bits.testBit q p
-        in mkNode opts (Val d) (msg0 <> " " <> showL opts p <> " " <> showL opts q <> " = " <> showL opts d) hhs
-
+        in mkNodeB opts d (msg0 <> " " <> showL opts p <> " " <> showL opts q <> " = " <> showL opts d) hhs
 
 -- | count number of bits at @p@: similar to 'Data.Bits.popCount'
 --

@@ -44,6 +44,7 @@   , IsOctDigitAll
   , IsSeparatorAll
   , IsLatin1All
+
  -- ** change case
   , ToTitle
   , ToUpper

@@ -16,6 +16,7 @@ {-# LANGUAGE EmptyDataDeriving #-}
 -- | promoted conditional functions
 module Predicate.Data.Condition (
+  -- ** functions
     If
   , Case
   , Case'
@@ -31,6 +32,11 @@   , Bools
   , BoolsQuick
   , BoolsN
+
+  -- ** type families
+  , ToGuardsT
+  , ToGuardsDetailT
+  , GuardsT
  ) where
 import Predicate.Core
 import Predicate.Misc
@@ -43,7 +49,6 @@ import Data.Kind (Type)
 import Data.Void (Void)
 import qualified Data.Type.Equality as DE
-import Data.Bool (bool)
 -- $setup
 -- >>> import Predicate.Prelude
 -- >>> :set -XDataKinds
@@ -83,19 +88,19 @@ -- Val [True,True,False,False,False]
 --
 -- >>> pl @(If (Gt 4) (Fail (Hole _) (PrintF "failing with %d" Id)) ()) 45
--- Error failing with 45 (If True)
+-- Error failing with 45 (If 'True)
 -- Fail "failing with 45"
 --
 -- >>> pl @(If (Gt 4) (Fail (Hole _) (PrintF "failing with %d" Id)) (Id * 7)) 3
 -- Present 21 (If 'False 21)
 -- Val 21
 --
--- >>> pl @(If (Gt 4) (Fail (Hole _) (PrintF "failing with %d" Id)) (Id * 7 >> ShowP Id >> Ones)) 3
+-- >>> pl @(If (Gt 4) (FailT _ (PrintF "failing with %d" Id)) (Id * 7 >> ShowP Id >> Ones)) 3
 -- Present ["2","1"] (If 'False ["2","1"])
 -- Val ["2","1"]
 --
--- >>> pl @(If (Gt 4) (Fail (Hole _) (PrintF "failing with %d" Id)) (ShowP (Id * 7) >> Ones)) 19
--- Error failing with 19 (If True)
+-- >>> pl @(If (Gt 4) (FailT _ (PrintF "failing with %d" Id)) (ShowP (Id * 7) >> Ones)) 19
+-- Error failing with 19 (If 'True)
 -- Fail "failing with 19"
 --
 data If p q r deriving Show
@@ -117,9 +122,9 @@         qqrr <- if b
                 then eval (Proxy @q) opts a
                 else eval (Proxy @r) opts a
-        pure $ case getValueLR Inline opts (msg0 <> " " <> show b) qqrr [hh pp, hh qqrr] of
+        pure $ case getValueLR Inline opts (msg0 <> " '" <> show b) qqrr [hh pp, hh qqrr] of
           Left e -> e
-          Right ret -> mkNodeCopy opts qqrr (msg0 <> " " <> bool "'False" "'True" b <> " " <> showL opts ret) [hh pp, hh qqrr]
+          Right ret -> mkNodeCopy opts qqrr (msg0 <> " '" <> show b <> " " <> showL opts ret) [hh pp]
 
 type family GuardsT (ps :: [k]) where
   GuardsT '[] = '[]
@@ -134,39 +139,11 @@   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
--- Val "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
--- Val "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
--- Val "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
--- Fail "asdf"
---
--- >>> pz @(Case (FailS "asdf" >> Snd >> UnproxyT) '[Lt 4,Lt 10,Same 50] '[PrintF "%d is lt4" Id, PrintF "%d is lt10" Id, PrintF "%d is same50" Id] Id) 99
--- Fail "asdf"
---
--- >>> pz @(Case (FailT _ "x") '[Same "a",Same "b"] '["hey","there"] Id) "b"
--- Val "there"
---
--- >>> pz @(Case (FailT _ "x") '[Id == "a",Id == "b"] '["hey","there"] Id) "a"
--- Val "hey"
---
--- >>> pz @(Case (FailT _ "x") '[Same "a",Same "b"] '["hey","there"] Id) "c"
--- Fail "x"
---
-data CaseImpl (n :: Nat) (e :: k0) (ps :: [k]) (qs :: [k1]) (r :: k2) deriving Show
--- 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@
+--   ps = conditions
+--   qs = what to do [one to one with ps]
+--   r = the value
+--   e = otherwise  -- leave til later
 --
 -- >>> pl @(Case (Snd >> FailP "xx") '[Gt 3, Lt 2, Same 3] '["gt3","lt2","eq3"] Id) 15
 -- Present "gt3" (Case(0 of 2) "gt3" | 15)
@@ -196,6 +173,30 @@ -- Present "151515" (Case(0) "151515" | 15)
 -- Val "151515"
 --
+-- >>> 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
+-- Val "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
+-- Val "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
+-- Val "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
+-- Fail "asdf"
+--
+-- >>> pz @(Case (FailS "asdf" >> Snd >> UnproxyT) '[Lt 4,Lt 10,Same 50] '[PrintF "%d is lt4" Id, PrintF "%d is lt10" Id, PrintF "%d is same50" Id] Id) 99
+-- Fail "asdf"
+--
+-- >>> pz @(Case (FailT _ "x") '[Same "a",Same "b"] '["hey","there"] Id) "b"
+-- Val "there"
+--
+-- >>> pz @(Case (FailT _ "x") '[Id == "a",Id == "b"] '["hey","there"] Id) "a"
+-- Val "hey"
+--
+-- >>> pz @(Case (FailT _ "x") '[Same "a",Same "b"] '["hey","there"] Id) "c"
+-- Fail "x"
+--
 data Case (e :: k0) (ps :: [k]) (qs :: [k1]) (r :: k2) deriving Show
 
 -- | like 'Case' but uses a generic error message (skips the @e@ parameter)
@@ -248,6 +249,8 @@   type PP (Case e ps qs r) x = PP (CaseImplT e ps qs r) x
   eval _ = eval (Proxy @(CaseImplT e ps qs r))
 
+data CaseImpl (n :: Nat) (e :: k0) (ps :: [k]) (qs :: [k1]) (r :: k2) deriving Show
+
 -- 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
@@ -289,12 +292,12 @@             qq <- eval (Proxy @q) opts a
             pure $ case getValueLR NoInline opts msgbase0 qq [hh rr, hh pp] of
               Left e -> e
-              Right b -> mkNode opts (Val b) (show3 opts msgbase0 b a) (hh rr : hh pp : verboseList opts qq)
+              Right q -> mkNodeCopy opts qq (show3 opts msgbase0 q a) [hh rr, hh pp]
           Right False -> do
-            ee <- eval (Proxy @e) opts (a, Proxy @(PP q (PP r x)))
-            pure $ case getValueLR NoInline opts ("Case:otherwise failed" <> nullIf ":" (ee ^. ttString)) ee [hh rr, hh pp] of
+            ww <- eval (Proxy @e) opts (a, Proxy @(PP q (PP r x)))
+            pure $ case getValueLR NoInline opts ("Case:otherwise failed" <> nullIf ":" (ww ^. ttString)) ww [hh rr, hh pp] of
               Left e -> e
-              Right b -> mkNode opts (Val b) (show3 opts msgbase0 b a) [hh rr, hh pp, hh ee]
+              Right w -> mkNodeCopy opts ww (show3 opts msgbase0 w a) [hh rr, hh pp]
 
 instance ( KnownNat n
          , GetLen ps
@@ -326,12 +329,12 @@             qq <- eval (Proxy @q) opts a
             pure $ case getValueLR NoInline opts msgbase0 qq [hh pp, hh rr] of
               Left e -> e
-              Right b -> mkNode opts (Val b) (show3 opts msgbase0 b a) (hh rr : hh pp : verboseList opts qq)
+              Right q -> mkNodeCopy opts qq (show3 opts msgbase0 q a) [hh rr, hh pp]
           Right False -> do
             ww <- eval (Proxy @(CaseImpl n e (p1 ': ps) (q1 ': qs) r)) opts z
             pure $ case getValueLR Inline opts "" ww [hh rr, hh pp] of
               Left e -> e
-              Right b -> mkNode opts (Val b) (show3 opts msgbase1 b a) [hh rr, hh pp, hh ww]
+              Right w -> mkNodeCopy opts ww (show3 opts msgbase1 w a) [hh rr, hh pp]
 
 
 data GuardsImpl (n :: Nat) (os :: [(k,k1)]) deriving Show
@@ -378,13 +381,16 @@          , 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
+  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 (Fail msg1) "" []
-    else eval (Proxy @(GuardsImpl (LenT ps) ps)) opts as
+    case chkSize opts msg0 as' [] of
+      Left e -> pure e
+      Right (asLen,as) ->
+        if n /= asLen then
+           let msg1 = msg0 <> badLength asLen n
+           in pure $ mkNode opts (Fail msg1) "" []
+        else eval (Proxy @(GuardsImpl (LenT ps) ps)) opts as
 
 instance ( [a] ~ x
          , Show a
@@ -398,7 +404,6 @@     let n = nat @n @Int
     in pure $ mkNode opts (Val []) ("Guards(" ++ show n ++ ")") []
 
-
 instance ( PP prt (Int, a) ~ String
          , P prt (Int, a)
          , KnownNat n
@@ -529,9 +534,9 @@         n = getLen @ps
     case chkSize opts msg1 as [] of
       Left e -> pure e
-      Right ws ->
-        if n /= length ws then
-           let msg2 = msg0 <> badLength ws n
+      Right (wsLen,ws) ->
+        if n /= wsLen then
+           let msg2 = msg0 <> badLength wsLen n
            in pure $ mkNode opts (Fail msg2) "" []
         else evalBool (Proxy @(BoolsImpl (LenT ps) ps)) opts ws
 
@@ -577,7 +582,9 @@          qq <- eval (Proxy @prt) opts (cpos,a) -- only run prt when predicate is False
          pure $ case getValueLR NoInline opts (msgbase2 <> " False predicate and prt failed") qq [hh pp] of
             Left e -> e
-            Right msgx -> mkNode opts (Fail (msgbase1 <> " [" <> msgx <> "]" <> nullSpace (topMessage pp))) "" (hh pp : verboseList opts qq)
+            Right msgx ->
+              let top = topMessage pp
+              in mkNode opts (Fail (msgbase1 <> " [" <> msgx <> "]" <> nullSpace top)) "" (hh pp : verboseList opts qq)
        Right True ->
          if pos == 0 then -- we are at the bottom of the tree
             pure $ mkNodeB opts True msgbase2 [hh pp]
@@ -637,13 +644,16 @@          , P (GuardsImpl (LenT ps) ps) x
          ) => P (GuardsDetailImpl ps) x where
   type PP (GuardsDetailImpl ps) x = PP (GuardsImpl (LenT ps) ps) x
-  eval _ opts as = do
+  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 (Fail msg1) "" []
-    else eval (Proxy @(GuardsImpl (LenT ps) ps)) opts as
+    case chkSize opts msg0 as' [] of
+      Left e -> pure e
+      Right (asLen,as) ->
+        if n /= asLen then
+           let msg1 = msg0 <> badLength asLen n
+           in pure $ mkNode opts (Fail msg1) "" []
+        else eval (Proxy @(GuardsImpl (LenT ps) ps)) opts as
 
 -- | if a predicate fails then then the corresponding symbol and value will be passed to the print function
 --
@@ -663,7 +673,6 @@   type PP (GuardsDetail prt ps) x = PP (GuardsDetailT prt ps) x
   eval _ = eval (Proxy @(GuardsDetailT prt ps))
 
---type family ToGuardsDetailT prt os where
 type family ToGuardsDetailT (prt :: k1) (os :: [(k2,k3)]) :: [(Type,k3)] where
   ToGuardsDetailT prt '[ '(s,p) ] = '(PrintT prt '(s,Snd), p) : '[]
   ToGuardsDetailT prt ( '(s,p) ': ps) = '(PrintT prt '(s,Snd), p) ': ToGuardsDetailT prt ps
@@ -764,8 +773,8 @@         qq <- eval (Proxy @prt) opts a
         pure $ case getValueLR NoInline opts (msg0 <> " Msg") qq [hh pp] of
           Left e -> e
-          Right ee -> mkNode opts (Fail ee) (msg0 <> " | " <> showL opts a) (hh pp : verboseList opts qq)
-      Right True -> pure $ mkNode opts (Val a) (msg0 <> "(ok) | " <> showL opts a) [hh pp]  -- dont show the guard message if successful
+          Right ee -> mkNode opts (Fail ee) (joinStrings msg0 (showL opts a)) (hh pp : verboseList opts qq)
+      Right True -> pure $ mkNode opts (Val a) (joinStrings (msg0 <> "(ok)") (showL opts a)) [hh pp]  -- dont show the guard message if successful
 
 -- | boolean guard
 --
@@ -790,7 +799,9 @@         qq <- eval (Proxy @prt) opts a
         pure $ case getValueLR NoInline opts (msg0 <> " Msg") qq [hh pp] of
           Left e -> e
-          Right ee -> mkNode opts (Fail ee) (msg0 <> nullSpace (topMessage pp)) [hh pp, hh qq]
+          Right ee ->
+            let top = topMessage pp
+            in mkNode opts (Fail ee) (msg0 <> nullSpace top) [hh pp, hh qq]
       Right True -> pure $ mkNodeB opts True "" [hh pp]  -- dont show the guard message if successful
 
 -- | uses 'Guard' but negates @p@
@@ -878,11 +889,11 @@   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
+    pp <- evalBool (Proxy @p) (zeroToLite opts) a -- temporarily lift DZero to DLite so as not to lose the failure message
     pure $ case getValueLR NoInline opts msg0 pp [] of
       Left e -> e
       Right False ->
-        let msgx = topMessage pp
-        in mkNode opts (Fail msgx) (msg0 <> " | " <> showL opts a) [hh pp]
+        let top = topMessage pp -- need DLite at least to get a reasonable message for the Fail case
+        in mkNode opts (Fail top) (joinStrings msg0 (showL opts a)) [hh pp]
       Right True ->
-        mkNode opts (Val a) (msg0 <> "(ok) | " <> showL opts a) [hh pp]
+        mkNode opts (Val a) (joinStrings (msg0 <> "(ok)") (showL opts a)) [hh pp]

@@ -47,7 +47,6 @@   , UnMkTime
   , UTCTimeToPosix
   , LocalTimeToUTC
-
  ) where
 import Predicate.Core
 import Predicate.Misc
@@ -91,8 +90,8 @@       Left e -> e
       Right (p,q,pp,qq) ->
         let msg1 = msg0 <> " (" <> p <> ")"
-            b = formatTime defaultTimeLocale p q
-        in mkNode opts (Val b) (msg1 <> " " <> litL opts b <> showVerbose opts " | " q) [hh pp, hh qq]
+            d = formatTime defaultTimeLocale p q
+        in mkNode opts (Val d) (msg1 <> " " <> litL opts d <> showVerbose opts " | " q) [hh pp, hh qq]
 
 -- | type level expression representing a formatted time
 --
@@ -135,7 +134,7 @@         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 (Val b) (lit3 opts msg1 b "fmt=" p <> showVerbose opts " | " q) hhs
+             Just d -> mkNode opts (Val d) (lit3 opts msg1 d "fmt=" p <> showVerbose opts " | " q) hhs
              Nothing -> mkNode opts (Fail (msg1 <> " failed to parse")) "" hhs
 -- | similar to 'Date.Time.parseTimeM'
 --
@@ -385,7 +384,7 @@         let (_, week, _dow) = toWeekDate p
         in mkNode opts (Val week) (show3 opts msg0 week p) [hh pp]
 
-class ToDayC a where
+class ToDayC (a :: Type) where
   getDay :: a -> Day
 instance ToDayC UTCTime where
   getDay = utctDay
@@ -400,7 +399,7 @@ instance ToDayC CP.SystemTime where
   getDay = getDay . CP.systemToUTCTime
 
-class ToTimeC a where
+class ToTimeC (a :: Type) where
   getTime :: a -> TimeOfDay
 instance ToTimeC UTCTime where
   getTime = getTime . utctDayTime

@@ -40,8 +40,13 @@  -- ** miscellaneous
   , type (|||)
   , type (+++)
-  , EitherX
+  , EitherIn
+  , EitherId
+  , LeftDef'
+  , RightDef'
 
+ -- type families
+  , EitherInT
  ) where
 import Predicate.Core
 import Predicate.Misc
@@ -146,14 +151,14 @@         pure $ case getValueLR NoInline opts msg0 pp [] of
           Left e -> e
           Right a1 -> let msg1 = msg0 ++ " Left"
-                      in mkNodeCopy opts pp (show3 opts msg1 a1 a) [hh pp]
+                      in mkNodeCopy opts pp (show3 opts msg1 a1 a) []
       Right a -> do
         qq <- eval (Proxy @q) opts a
         pure $ case getValueLR NoInline opts msg0 qq [] of
           Left e -> e
           Right a1 ->
             let msg1 = msg0 ++ " Right"
-            in mkNodeCopy opts qq (show3 opts msg1 a1 a) [hh qq]
+            in mkNodeCopy opts qq (show3 opts msg1 a1 a) []
 
 -- | similar to 'isLeft'
 --
@@ -240,16 +245,16 @@         pp <- eval (Proxy @p) opts a
         pure $ case getValueLR NoInline opts msg0 pp [] of
           Left e -> e
-          Right a1 ->
+          Right p ->
             let msg1 = msg0 ++ " Left"
-            in mkNode opts (Val (Left a1)) (msg1 <> " " <> showL opts a1 <> showVerbose opts " | " a) [hh pp]
+            in mkNode opts (Val (Left p)) (msg1 <> " " <> showL opts p <> showVerbose opts " | " a) [hh pp]
       Right a -> do
         qq <- eval (Proxy @q) opts a
         pure $ case getValueLR NoInline opts msg0 qq [] of
           Left e -> e
-          Right a1 ->
+          Right q ->
             let msg1 = msg0 ++ " Right"
-            in mkNode opts (Val (Right a1)) (msg1 <> " " <> showL opts a1 <> showVerbose opts " | " a) [hh qq]
+            in mkNode opts (Val (Right q)) (msg1 <> " " <> showL opts q <> showVerbose opts " | " a) [hh qq]
 
 -- | similar to 'partitionEithers'
 --
@@ -335,51 +340,6 @@           Left e -> e
           Right q -> mkNode opts (Val (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 (L11 + Snd)) (ShowP Id) Snd) (9,Left 123)
--- Val "132"
---
--- >>> pz @(EitherX (ShowP (L11 + Snd)) (ShowP Id) Snd) (9,Right 'x')
--- Val "((9,Right 'x'),'x')"
---
--- >>> pz @(EitherX (ShowP Id) (ShowP (Second Succ)) Snd) (9,Right 'x')
--- Val "((9,Right 'x'),'y')"
---
-data EitherX p q r deriving Show
-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 NoInline 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 NoInline opts msg1 pp [hh rr] of
-          Left e -> e
-          Right _ -> mkNodeCopy opts pp msg1 [hh rr, hh pp]
-      Right (Right b) -> do
-        let msg1 = msg0 <> "(Right)"
-        qq <- eval (Proxy @q) opts (x,b)
-        pure $ case getValueLR NoInline opts msg1 qq [hh rr] of
-          Left e -> e
-          Right _ -> mkNodeCopy opts 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 deriving Show
 
@@ -475,7 +435,7 @@             pp <- eval (Proxy @p) opts (b,x)
             pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
               Left e -> e
-              Right p -> mkNode opts (Val p) (msg0 <> " Right") [hh qq, hh pp]
+              Right _ -> mkNodeCopy opts pp (msg0 <> " Right") [hh qq]
 
 -- | extract the Right value from an 'Either': similar to 'Data.Either.fromRight'
 --
@@ -516,8 +476,7 @@             pp <- eval (Proxy @p) opts (a,x)
             pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
               Left e -> e
-              Right p -> mkNode opts (Val p) (msg0 <> " Left") [hh qq, hh pp]
-
+              Right _ -> mkNodeCopy opts pp (msg0 <> " Left") [hh qq]
 
 -- | extract the Left value from an 'Either' otherwise fail with a message
 --
@@ -617,3 +576,116 @@             pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
               Left e -> e
               Right p -> mkNode opts (Fail p) (msg0 <> " Left") [hh qq, hh pp]
+
+
+-- | destructor for Either (similar to 'Control.Arrow.|||' but with an extra environment @s@)
+--   @p@ @Left a@ receives @(PP t x,a)@
+--   @q@ @Right b@ receives @(PP t x,b)@
+--   @s@ points to the environment you want to pass in
+--   @t@ points to the Either value
+--
+-- >>> pz @(EitherIn (ShowP (Fst + Snd)) (ShowP Id) Fst Snd) (9,Left 123)
+-- Val "132"
+--
+-- >>> pz @(EitherIn (ShowP (Fst + Snd)) (ShowP Id) Fst Snd) (9,Right 'x')
+-- Val "(9,'x')"
+--
+-- >>> pz @(EitherIn (ShowP Id) (ShowP (Second Succ)) Fst Snd) (9,Right 'x')
+-- Val "(9,'y')"
+--
+-- >>> pz @(EitherIn (FailT _ (PrintF ("found left=%d") Snd)) (Second Succ) Fst Snd) (9,Right 'x')
+-- Val (9,'y')
+--
+-- >>> pz @(EitherIn (FailT _ (PrintF ("found left=%d") Snd)) (Second Succ) Fst Snd) (9,Left 13)
+-- Fail "found left=13"
+--
+data EitherIn p q s t deriving Show
+
+instance ( Show a
+         , Show b
+         , Show (PP q (y,b))
+         , P p (y,a)
+         , P q (y,b)
+         , PP p (y,a) ~ PP q (y,b)
+         , P s x
+         , P t x
+         , PP s x ~ y
+         , PP t x ~ Either a b
+         )  => P (EitherIn p q s t) x where
+  type PP (EitherIn p q s t) x = EitherInT p (PP s x) (PP t x)
+  eval _ opts x = do
+    let msg0 = "EitherIn"
+    lr <- runPQ NoInline msg0 (Proxy @s) (Proxy @t) opts x []
+    case lr of
+      Left e -> pure e
+      Right (s,t,ss,tt) -> do
+         let hhs = [hh ss, hh tt]
+         case t of
+            Left a -> do
+              let msg1 = msg0 <> "(Left)"
+              pp <- eval (Proxy @p) opts (s,a)
+              pure $ case getValueLR NoInline opts (msg1 <> " p failed") pp hhs of
+                   Left e -> e
+                   Right c -> mkNodeCopy opts pp (show3 opts msg1 c a) hhs
+            Right b -> do
+              let msg1 = msg0 <> "(Right)"
+              qq <- eval (Proxy @q) opts (s,b)
+              pure $ case getValueLR NoInline opts (msg1 <> " q failed") qq hhs of
+                   Left e -> e
+                   Right c -> mkNodeCopy opts qq (show3 opts msg1 c b) hhs
+
+type family EitherInT (p :: k) (y :: Type) (lr :: Type) where
+  EitherInT p y (Either a _) = PP p (y,a)
+  EitherInT _ _ o = GL.TypeError (
+      'GL.Text "EitherInT: expected 'Either a b' "
+      ':$$: 'GL.Text "o = "
+      ':<>: 'GL.ShowType o)
+
+-- | simple version of 'EitherIn' with Id as the Either value and the environment set to ()
+--
+-- >>> pz @(EitherId '(Id,"fromleft") '(888,Id)) (Right "ok")
+-- Val (888,"ok")
+--
+-- >>> pz @(EitherId '(Id,"fromleft") '(888,Id)) (Left 123)
+-- Val (123,"fromleft")
+--
+data EitherId p q deriving Show
+type EitherIdT p q = EitherIn (Snd >> p) (Snd >> q) () Id
+
+instance P (EitherIdT p q) x => P (EitherId p q) x where
+  type PP (EitherId p q) x = PP (EitherIdT p q) x
+  eval _ = eval (Proxy @(EitherIdT p q))
+
+
+-- | get Left or use the default value @p@: @q@ is the environment and @r@ is the Elr value
+--
+-- >>> pz @(LeftDef' 999 () Id) (Right "sdf")
+-- Val 999
+--
+-- >>> pz @(LeftDef' 999 () Id) (Left 1)
+-- Val 1
+--
+data LeftDef' p q r deriving Show
+
+type LeftDefT' p q r = EitherIn Snd (Fst >> p) q r
+
+instance P (LeftDefT' p q r) x => P (LeftDef' p q r) x where
+  type PP (LeftDef' p q r) x = PP (LeftDefT' p q r) x
+  eval _ = eval (Proxy @(LeftDefT' p q r))
+
+-- | get Right or use the default value @p@: @q@ is the environment and @r@ is the Elr value
+--
+-- >>> pz @(RightDef' 999 () Id) (Left "sdf")
+-- Val 999
+--
+-- >>> pz @(RightDef' 999 Fst Snd) (999,Right 1)
+-- Val 1
+--
+data RightDef' p q r deriving Show
+
+type RightDefT' p q r = EitherIn (Fst >> p) Snd q r
+
+instance P (RightDefT' p q r) x => P (RightDef' p q r) x where
+  type PP (RightDef' p q r) x = PP (RightDefT' p q r) x
+  eval _ = eval (Proxy @(RightDefT' p q r))
+

@@ -0,0 +1,716 @@+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE NoStarIsType #-}
+{-# LANGUAGE EmptyDataDeriving #-}
+-- | Elr related methods
+module Predicate.Data.Elr (
+
+ -- ** destructors
+    ENone'
+  , ELeft'
+  , ERight'
+  , EBoth'
+
+  , ElrIn
+  , ElrId
+  , ElrPair
+  , ElrInSimple
+  , PartitionElr
+
+  , ENoneDef
+  , ELeftDef
+  , ERightDef
+  , EBothDef
+
+ -- ** constructors
+  , MkENone
+  , MkELeft
+  , MkERight
+  , MkEBoth
+
+  , MkENone'
+  , MkELeft'
+  , MkERight'
+
+ -- ** boolean predicates
+  , IsENone
+  , IsELeft
+  , IsERight
+  , IsEBoth
+
+  -- ** converters
+  , These2Elr
+  , Elr2These
+  , Elr2Maybe
+ ) where
+import Predicate.Core
+import Predicate.Util
+import Predicate.Elr
+import Data.Kind (Type)
+import Control.Lens
+import Data.Proxy (Proxy(..))
+import Data.These (These)
+-- $setup
+-- >>> import Predicate.Prelude
+-- >>> import qualified Data.Semigroup as SG
+-- >>> :m + Data.These
+
+-- | 'ENone' constructor
+--
+-- >>> pz @(Proxy Int >> MkENone' UnproxyT 10) []
+-- Val ENone
+--
+data MkENone' t t1 deriving Show
+
+instance P (MkENone' t t1) x where
+  type PP (MkENone' t t1) x = Elr (PP t x) (PP t1 x)
+  eval _ opts _ =
+    let msg0 = "MkENone"
+        d = ENone
+    in pure $ mkNode opts (Val d) msg0 []
+
+-- | 'ENone' constructor
+--
+-- >>> pl @(MkENone () Id) 'x'
+-- Present ENone (MkENone)
+-- Val ENone
+--
+data MkENone (t :: Type) (t1 :: Type) deriving Show
+type MkENoneT (t :: Type) (t1 :: Type) = MkENone' (Hole t) (Hole t1)
+
+instance P (MkENone t t1) x where
+  type PP (MkENone t t1) x = PP (MkENoneT t t1) x
+  eval _ = eval (Proxy @(MkENoneT t t1))
+
+-- | 'ELeft' constructor
+--
+-- >>> pz @(Proxy Int >> MkELeft' UnproxyT 10) []
+-- Val (ELeft 10)
+--
+data MkELeft' t p deriving Show
+
+instance P p x
+      => P (MkELeft' t p) x where
+  type PP (MkELeft' t p) x = Elr (PP p x) (PP t x)
+  eval _ opts x = do
+    let msg0 = "MkELeft"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR NoInline opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let d = ELeft p
+        in mkNode opts (Val d) msg0 [hh pp]
+
+-- | 'ELeft' constructor
+--
+-- >>> pl @(MkELeft () Id) 'x'
+-- Present ELeft 'x' (MkELeft)
+-- Val (ELeft 'x')
+--
+-- >>> pl @(MkELeft () Fst) ('x',True)
+-- Present ELeft 'x' (MkELeft)
+-- Val (ELeft 'x')
+--
+-- >>> pz @(MkELeft _ Id) 44
+-- Val (ELeft 44)
+--
+data MkELeft (t :: Type) p deriving Show
+type MkELeftT (t :: Type) p = MkELeft' (Hole t) p
+
+instance P (MkELeftT t p) x => P (MkELeft t p) x where
+  type PP (MkELeft t p) x = PP (MkELeftT t p) x
+  eval _ = eval (Proxy @(MkELeftT t p))
+
+-- | similar to 'MkERight' where @t@ references the type
+data MkERight' t p deriving Show
+
+instance P p x
+      => P (MkERight' t p) x where
+  type PP (MkERight' t p) x = Elr (PP t x) (PP p x)
+  eval _ opts x = do
+    let msg0 = "MkERight"
+    pp <- eval (Proxy @p) opts x
+    pure $ case getValueLR NoInline opts msg0 pp [] of
+      Left e -> e
+      Right p ->
+        let d = ERight p
+        in mkNode opts (Val d) msg0 [hh pp]
+
+-- | 'ERight' constructor
+--
+-- >>> pz @(MkERight _ Id) 44
+-- Val (ERight 44)
+--
+-- >>> pz @(MkERight _ "Abc" <> MkELeft _ '[1,2] <> MkEBoth [3,4] "def") ()
+-- Val (EBoth [1,2,3,4] "Abcdef")
+--
+-- >>> pl @(MkERight () Id) 'x'
+-- Present ERight 'x' (MkERight)
+-- Val (ERight 'x')
+--
+data MkERight (t :: Type) p deriving Show
+type MkERightT (t :: Type) p = MkERight' (Hole t) p
+
+instance P (MkERightT t p) x => P (MkERight t p) x where
+  type PP (MkERight t p) x = PP (MkERightT t p) x
+  eval _ = eval (Proxy @(MkERightT t p))
+
+-- | 'EBoth' constructor
+--
+-- >>> pz @(MkEBoth Fst Snd) (44,'x')
+-- Val (EBoth 44 'x')
+--
+-- >>> pl @(MkEBoth Id 'True) 'x'
+-- Present EBoth 'x' True (MkEBoth)
+-- Val (EBoth 'x' True)
+--
+-- >>> pz @(MkENone _ _ <> MkELeft _ '[1] <> MkERight _ "abc" <> MkELeft _ '[2] <> MkEBoth '[3,4,5] "def") ()
+-- Val (EBoth [1,2,3,4,5] "abcdef")
+--
+data MkEBoth p q deriving Show
+instance ( P p a
+         , P q a
+         ) => P (MkEBoth p q) a where
+  type PP (MkEBoth p q) a = Elr (PP p a) (PP q a)
+  eval _ opts a = do
+    let msg0 = "MkEBoth"
+    lr <- runPQ NoInline msg0 (Proxy @p) (Proxy @q) opts a []
+    pure $ case lr of
+      Left e -> e
+      Right (p,q,pp,qq) ->
+        let d = EBoth p q
+        in mkNode opts (Val d) msg0 [hh pp, hh qq]
+
+data IsElr (th :: Elr x y) deriving Show
+-- x y can be anything
+
+-- trying to avoid Show instance because more likely to have ambiguity errors
+instance ( x ~ Elr a b
+         , Show a
+         , Show b
+         , GetElr th
+         ) => P (IsElr (th :: Elr x1 x2)) x where
+  type PP (IsElr th) x = Bool
+  eval _ opts x =
+    let msg0 = "Is"
+        (t,f) = getElr @_ @_ @th
+        b = f x
+    in pure $ mkNodeB opts b (msg0 <> t <> showVerbose opts " | " x) []
+
+-- | predicate on 'ENone'
+--
+-- >>> pz @IsENone ENone
+-- Val True
+--
+-- >>> pz @IsENone (EBoth 1 'a')
+-- Val False
+--
+data IsENone deriving Show
+type IsENoneT = IsElr 'ENone
+
+instance P IsENoneT x => P IsENone x where
+  type PP IsENone x = PP IsENoneT x
+  eval _ = evalBool (Proxy @IsENoneT)
+
+-- | predicate on 'ELeft'
+--
+-- >>> pz @IsELeft (ELeft "aBc")
+-- Val True
+--
+-- >>> pz @IsELeft (EBoth 1 'a')
+-- Val False
+--
+-- >>> pl @IsELeft (ELeft 12)
+-- True (IsELeft | ELeft 12)
+-- Val True
+--
+data IsELeft deriving Show
+type IsELeftT = IsElr ('ELeft '())
+
+instance P IsELeftT x => P IsELeft x where
+  type PP IsELeft x = PP IsELeftT x
+  eval _ = evalBool (Proxy @IsELeftT)
+
+-- | predicate on 'ERight'
+--
+-- >>> pl @IsERight (ELeft 12)
+-- False (IsERight | ELeft 12)
+-- Val False
+--
+data IsERight deriving Show
+type IsERightT = IsElr ('ERight '())
+
+instance P IsERightT x => P IsERight x where
+  type PP IsERight x = PP IsERightT x
+  eval _ = evalBool (Proxy @IsERightT)
+
+-- | predicate on 'EBoth'
+--
+-- >>> pl @IsEBoth (ELeft 12)
+-- False (IsEBoth | ELeft 12)
+-- Val False
+--
+-- >>> pz @IsEBoth (EBoth 1 'a')
+-- Val True
+--
+-- >>> pl @IsEBoth (EBoth 'x' 12)
+-- True (IsEBoth | EBoth 'x' 12)
+-- Val True
+--
+-- >>> pl @IsEBoth (ERight (SG.Sum 12))
+-- False (IsEBoth | ERight (Sum {getSum = 12}))
+-- Val False
+--
+-- >>> pl @IsEBoth (EBoth 1 (SG.Sum 12))
+-- True (IsEBoth | EBoth 1 (Sum {getSum = 12}))
+-- Val True
+--
+data IsEBoth deriving Show
+type IsEBothT = IsElr ('EBoth '() '())
+
+instance P IsEBothT x => P IsEBoth x where
+  type PP IsEBoth x = PP IsEBothT x
+  eval _ = evalBool (Proxy @IsEBothT)
+
+-- | tries to extract a () from the 'ENone' constructor
+--
+-- >>> pz @ENone' ENone
+-- Val ()
+--
+-- >>> pz @ENone' (ERight 'a')
+-- Fail "ENone' found ERight"
+--
+data ENone' deriving Show
+
+instance P ENone' (Elr x y) where
+  type PP ENone' (Elr x y) = ()
+  eval _ opts lr =
+    let msg0 = "ENone'"
+    in pure $ case lr of
+         ENone -> mkNode opts (Val ()) msg0 []
+         _ -> mkNode opts (Fail (msg0 <> " found " <> showElr lr)) "" []
+
+-- | tries to extract a value from the 'ELeft' constructor
+--
+-- >>> pz @(ELeft' >> Succ) (ELeft 20)
+-- Val 21
+--
+-- >>> pz @(ELeft' >> Succ) (ERight 'a')
+-- Fail "ELeft' found ERight"
+--
+data ELeft' deriving Show
+
+instance Show a => P ELeft' (Elr a x) where
+  type PP ELeft' (Elr a x) = a
+  eval _ opts lr =
+    let msg0 = "ELeft'"
+    in pure $ case lr of
+         ELeft a -> mkNode opts (Val a) (msg0 <> " " <> showL opts a) []
+         _ -> mkNode opts (Fail (msg0 <> " found " <> showElr lr)) "" []
+
+-- | tries to extract a value from the 'ERight' constructor
+--
+-- >>> pz @(ERight' >> Succ) (ERight 20)
+-- Val 21
+--
+-- >>> pz @(ERight' >> Succ) (ELeft 'a')
+-- Fail "ERight' found ELeft"
+--
+data ERight' deriving Show
+
+instance Show a => P ERight' (Elr x a) where
+  type PP ERight' (Elr x a) = a
+  eval _ opts lr =
+    let msg0 = "ERight'"
+    in pure $ case lr of
+         ERight a -> mkNode opts (Val a) (msg0 <> " " <> showL opts a) []
+         _ -> mkNode opts (Fail (msg0 <> " found " <> showElr lr)) "" []
+
+-- | tries to extract the values from the 'EBoth' constructor
+--
+-- >>> pz @(EBoth' >> Second Succ) (EBoth 1 'a')
+-- Val (1,'b')
+--
+-- >>> pz @(ERight' >> Succ) (ELeft 'a')
+-- Fail "ERight' found ELeft"
+--
+-- >>> pz @(EBoth' >> Second Succ) (ERight 8)
+-- Fail "EBoth' found ERight"
+--
+data EBoth' deriving Show
+
+instance ( Show a
+         , Show b
+        ) => P EBoth' (Elr a b) where
+  type PP EBoth' (Elr a b) = (a,b)
+  eval _ opts lr =
+    let msg0 = "EBoth'"
+    in pure $ case lr of
+         EBoth a b -> mkNode opts (Val (a,b)) (msg0 <> " " <> showL opts (a,b)) []
+         _ -> mkNode opts (Fail (msg0 <> " found " <> showElr lr)) "" []
+
+-- | similar to 'Predicate.Data.These.PartitionThese' for 'Elr'. returns a 4-tuple with the results so use 'Fst' 'Snd' 'Thd' 'L4' to extract
+--
+-- >>> pz @PartitionElr [ELeft 'a', ENone, ERight 2, ELeft 'c', EBoth 'z' 1, ERight 4, EBoth 'a' 2, ERight 99, ENone]
+-- Val ([(),()],"ac",[2,4,99],[('z',1),('a',2)])
+--
+-- >>> pz @PartitionElr [ELeft 4, ERight 'x', ERight 'y',EBoth 3 'b', ELeft 99, EBoth 5 'x']
+-- Val ([],[4,99],"xy",[(3,'b'),(5,'x')])
+--
+-- >>> pz @PartitionElr [ENone,ELeft 1,ERight 'x',ELeft 4,ERight 'y',EBoth 9 'z',ELeft 10,EBoth 8 'y']
+-- Val ([()],[1,4,10],"xy",[(9,'z'),(8,'y')])
+--
+data PartitionElr deriving Show
+
+instance ( Show a
+         , Show b
+         ) => P PartitionElr [Elr a b] where
+  type PP PartitionElr [Elr a b] = ([()], [a], [b], [(a, b)])
+  eval _ opts as =
+    let msg0 = "PartitionElr"
+        b = partitionElr as
+    in pure $ mkNode opts (Val b) (show3 opts msg0 b as) []
+
+-- | destructs an Elr value
+--   @n@ @ENone@ receives @(PP s x)@
+--   @p@ @ELeft a@ receives @(PP s x,a)@
+--   @q@ @ERight b@ receives @(PP s x,b)@
+--   @r@ @EBoth a b@ receives @(PP s x,(a,b))@
+--   @s@ points to the environment you want to pass in
+--   @t@ points to the Elr value
+--
+-- >>> pz @(ElrIn Id '(Snd,L12) '(L11,Snd) Snd Fst Snd) ((999,'a'), EBoth 12 'x')
+-- Val (12,'x')
+--
+-- >>> pz @(ElrIn Id '(Snd,L12) '(L11,Snd) Snd Fst Snd) ((999,'a'), ENone)
+-- Val (999,'a')
+--
+-- >>> pz @(ElrIn Id '(Snd,L12) '(L11,Snd) Snd Fst Snd) ((999,'a'), ERight 'z')
+-- Val (999,'z')
+--
+-- >>> pz @(ElrIn 999 Snd (Snd >> Len) (Snd >> Fst + Length Snd) () Id) (ELeft 13)
+-- Val 13
+--
+-- >>> pz @(ElrIn 999 Snd (Snd >> Len) (Snd >> Fst + Length Snd) () Id) (ERight "abcdef")
+-- Val 6
+--
+-- >>> pl @(ElrIn "none" "left" "right" "both" () Id) (ELeft (SG.Sum 12))
+-- Present "left" (ElrIn(ELeft) "left" | Sum {getSum = 12})
+-- Val "left"
+--
+-- >>> pl @(ElrIn '("",2) '(Snd,999) '("no value",Snd) Snd () Id) (EBoth "Ab" 13)
+-- Present ("Ab",13) (ElrIn(EBoth) ("Ab",13) | ("Ab",13))
+-- Val ("Ab",13)
+--
+-- >>> pl @(ElrIn '("",2) '(Snd,999) '("no value",Snd) Snd () Id) (ELeft "Ab")
+-- Present ("Ab",999) (ElrIn(ELeft) ("Ab",999) | "Ab")
+-- Val ("Ab",999)
+--
+-- >>> pl @(ElrIn '("",2) '(Snd,999) '("no value",Snd) Snd () Id) ENone
+-- Present ("",2) (ElrIn(ENone) ("",2) | ())
+-- Val ("",2)
+--
+-- >>> pl @(ElrIn (FailT _ "none found") '(Snd,"fromleft") '(888,Snd) Snd () Id)  ENone
+-- Error none found (ElrIn(ENone) n failed)
+-- Fail "none found"
+--
+data ElrIn n p q r s t deriving Show
+
+instance ( Show a
+         , Show b
+         , Show (PP r (y,(a,b)))
+         , P n y
+         , P p (y,a)
+         , P q (y,b)
+         , P r (y,(a,b))
+         , PP n y ~ PP p (y,a)
+         , PP p (y,a) ~ PP q (y,b)
+         , PP q (y,b) ~ PP r (y,(a,b))
+         , P s x
+         , P t x
+         , PP t x ~ Elr a b
+         , PP s x ~ y
+         )  => P (ElrIn n p q r s t) x where
+  type PP (ElrIn n p q r s t) x = PP n (PP s x)
+  eval _ opts x = do
+    let msg0 = "ElrIn"
+    lr <- runPQ NoInline msg0 (Proxy @s) (Proxy @t) opts x []
+    case lr of
+      Left e -> pure e
+      Right (s,t,ss,tt) -> do
+         let hhs = [hh ss, hh tt]
+         case t of
+            ENone -> do
+              let msg1 = msg0 <> "(ENone)"
+              nn <- eval (Proxy @n) opts s
+              pure $ case getValueLR NoInline opts (msg1 <> " n failed") nn hhs of
+                   Left e -> e
+                   Right c -> mkNodeCopy opts nn (show3 opts msg1 c ()) hhs
+            ELeft a -> do
+              let msg1 = msg0 <> "(ELeft)"
+              pp <- eval (Proxy @p) opts (s,a)
+              pure $ case getValueLR NoInline opts (msg1 <> " p failed") pp hhs of
+                   Left e -> e
+                   Right c -> mkNodeCopy opts pp (show3 opts msg1 c a) hhs
+            ERight b -> do
+              let msg1 = msg0 <> "(ERight)"
+              qq <- eval (Proxy @q) opts (s,b)
+              pure $ case getValueLR NoInline opts (msg1 <> " q failed") qq hhs of
+                   Left e -> e
+                   Right c -> mkNodeCopy opts qq (show3 opts msg1 c b) hhs
+            EBoth a b -> do
+              let msg1 = msg0 <> "(EBoth)"
+              rr <- eval (Proxy @r) opts (s,(a,b))
+              pure $ case getValueLR NoInline opts (msg1 <> " r failed") rr hhs of
+                   Left e -> e
+                   Right c -> mkNodeCopy opts rr (show3 opts msg1 c (a,b)) hhs
+
+-- | simple version of 'ElrIn' with Id as the Elr value and the environment set to ()
+--
+-- >>> pz @(ElrId '(999,"oops") '(Id,"fromleft") '(888,Id) Id) (EBoth 222 "ok")
+-- Val (222,"ok")
+--
+-- >>> pz @(ElrId '(999,"oops") '(Id,"fromleft") '(888,Id) Id) (ERight "ok")
+-- Val (888,"ok")
+--
+-- >>> pz @(ElrId '(999,"oops") '(Id,"fromleft") '(888,Id) Id) ENone
+-- Val (999,"oops")
+--
+-- >>> pz @(ElrId '(999,"oops") '(Id,"fromleft") '(888,Id) Id) (ELeft 123)
+-- Val (123,"fromleft")
+--
+-- >>> pl @(ElrId (FailT _ "none found" ) '(Id,"fromleft") '(888,Id) Id) ENone
+-- Error none found (ElrIn(ENone) n failed)
+-- Fail "none found"
+--
+data ElrId n p q r deriving Show
+
+type ElrIdT n p q r = ElrIn n (Snd >> p) (Snd >> q) (Snd >> r) () Id
+
+instance P (ElrIdT n p q r) x => P (ElrId n p q r) x where
+  type PP (ElrId n p q r) x = PP (ElrIdT n p q r) x
+  eval _ = eval (Proxy @(ElrIdT n p q r))
+
+-- | creates a pair where the values are filled in by @s@ and @t@ holds the Elr value
+--
+-- >>> pz @(ElrPair Fst Snd) ((999,"oops"),EBoth 2 "xx")
+-- Val (2,"xx")
+--
+-- >>> pz @(ElrPair Fst Snd) ((999,"oops"),ENone)
+-- Val (999,"oops")
+--
+-- >>> pz @(ElrPair Fst Snd) ((999,"oops"),ERight "ok")
+-- Val (999,"ok")
+--
+data ElrPair s t deriving Show
+
+type ElrPairT s t = ElrIn Id '(Snd,L12) '(L11,Snd) Snd s t
+
+instance P (ElrPairT s t) x => P (ElrPair s t) x where
+  type PP (ElrPair s t) x = PP (ElrPairT s t) x
+  eval _ = eval (Proxy @(ElrPairT s t))
+
+-- | similar to 'ElrIn' but without an environment @s@ and uses Id for @t@
+--
+-- >>> pz @(ElrInSimple 999 Id Len (Fst + Length Snd)) (ELeft 13)
+-- Val 13
+--
+-- >>> pz @(ElrInSimple 999 Id Len (Fst + Length Snd)) ENone
+-- Val 999
+--
+-- >>> pz @(ElrInSimple 999 Id Len (Fst + Length Snd)) (ERight "this is a long string")
+-- Val 21
+--
+-- >>> pz @(ElrInSimple 999 Id Len (Fst + Length Snd)) (EBoth 20 "somedata")
+-- Val 28
+--
+-- >>> pz @(ElrInSimple (FailT _ "err") (MkLeft _ Id) (MkRight _ Id) (If (Fst > Length Snd) (MkLeft _ Fst) (MkRight _ Snd))) (ERight "this is a long string")
+-- Val (Right "this is a long string")
+--
+-- >>> pz @(ElrInSimple (FailT _ "err") (MkLeft _ Id) (MkRight _ Id) (If (Fst > Length Snd) (MkLeft _ Fst) (MkRight _ Snd))) ENone
+-- Fail "err"
+--
+-- >>> pz @(ElrInSimple (FailT _ "err") (MkLeft _ Id) (MkRight _ Id) (If (Fst > Length Snd) (MkLeft _ Fst) (MkRight _ Snd))) (EBoth 1 "this is a long string")
+-- Val (Right "this is a long string")
+--
+-- >>> pz @(ElrInSimple (FailT _ "err") (MkLeft _ Id) (MkRight _ Id) (If (Fst > Length Snd) (MkLeft _ Fst) (MkRight _ Snd))) (EBoth 100 "this is a long string")
+-- Val (Left 100)
+--
+-- >>> pl @(ElrInSimple "none" "left" "right" "both") (ELeft (SG.Sum 12))
+-- Present "left" (ElrIn(ELeft) "left" | Sum {getSum = 12})
+-- Val "left"
+--
+-- >>> pl @(ElrInSimple (FailT _ "err") (Id &&& 999) ("no value" &&& Id) Id) (EBoth "Ab" 13)
+-- Present ("Ab",13) (ElrIn(EBoth) ("Ab",13) | ("Ab",13))
+-- Val ("Ab",13)
+--
+-- >>> pl @(ElrInSimple (FailT _ "err") (Id &&& 999) ("no value" &&& Id) Id) (ELeft "Ab")
+-- Present ("Ab",999) (ElrIn(ELeft) ("Ab",999) | "Ab")
+-- Val ("Ab",999)
+--
+-- >>> pl @(ElrInSimple (FailT _ "err") (Id &&& 999) ("no value" &&& Id) Id) (ERight 13)
+-- Present ("no value",13) (ElrIn(ERight) ("no value",13) | 13)
+-- Val ("no value",13)
+--
+data ElrInSimple n p q r deriving Show
+
+type ElrInSimpleT n p q r = ElrIn n (Snd >> p) (Snd >> q) (Snd >> r) () Id
+
+instance P (ElrInSimpleT n p q r) x => P (ElrInSimple n p q r) x where
+  type PP (ElrInSimple n p q r) x = PP (ElrInSimpleT n p q r) x
+  eval _ = eval (Proxy @(ElrInSimpleT n p q r))
+
+-- | get ENone or run @p@: really only useful when p is set to Fail: where @q@ is the environment and @r@ is the Elr value
+--
+-- >>> pz @(ENoneDef (FailT _ "not ENone") () Id) ENone
+-- Val ()
+--
+-- >>> pz @(ENoneDef (FailT _ "not ENone") () Id) (ELeft 1)
+-- Fail "not ENone"
+--
+-- >>> pz @(ENoneDef (FailT _ Id) Fst Snd) ("not right",EBoth 1 2)
+-- Fail "not right"
+--
+data ENoneDef p q r deriving Show
+
+type ENoneDefT p q r = ElrIn Id (Fst >> p) (Fst >> p) (Fst >> p) q r
+
+instance P (ENoneDefT p q r) x => P (ENoneDef p q r) x where
+  type PP (ENoneDef p q r) x = PP (ENoneDefT p q r) x
+  eval _ = eval (Proxy @(ENoneDefT p q r))
+
+-- | get ELeft or use the default value @p@: @q@ is the environment and @r@ is the Elr value
+--
+-- >>> pz @(ELeftDef Id Fst Snd) (999,ENone)
+-- Val 999
+--
+-- >>> pz @(ELeftDef 999 () Id) (ERight "sdf")
+-- Val 999
+--
+-- >>> pz @(ELeftDef 999 () Id) (ELeft 1)
+-- Val 1
+--
+data ELeftDef p q r deriving Show
+
+type ELeftDefT p q r = ElrIn p Snd (Fst >> p) (Fst >> p) q r
+
+instance P (ELeftDefT p q r) x => P (ELeftDef p q r) x where
+  type PP (ELeftDef p q r) x = PP (ELeftDefT p q r) x
+  eval _ = eval (Proxy @(ELeftDefT p q r))
+
+-- | get ERight or use the default value @p@: @q@ is the environment and @r@ is the Elr value
+--
+-- >>> pz @(ERightDef 999 () Id) ENone
+-- Val 999
+--
+-- >>> pz @(ERightDef 999 () Id) (ELeft "sdf")
+-- Val 999
+--
+-- >>> pz @(ERightDef 999 Fst Snd) (999,ERight 1)
+-- Val 1
+--
+data ERightDef p q r deriving Show
+
+type ERightDefT p q r = ElrIn p (Fst >> p) Snd (Fst >> p) q r
+
+instance P (ERightDefT p q r) x => P (ERightDef p q r) x where
+  type PP (ERightDef p q r) x = PP (ERightDefT p q r) x
+  eval _ = eval (Proxy @(ERightDefT p q r))
+
+-- | get EBoth or use the default value @p@: @q@ is the environment and @r@ is the Elr value
+--
+-- >>> pz @(EBothDef '(999,"xx") () Id) ENone
+-- Val (999,"xx")
+--
+-- >>> pz @(EBothDef '(999,"xx") () Id) (ERight "abc")
+-- Val (999,"xx")
+--
+-- >>> pz @(EBothDef '(999,"xx") () Id) (ELeft 1)
+-- Val (999,"xx")
+--
+-- >>> pz @(EBothDef '(999,"xx") () Id) (EBoth 1 "abc")
+-- Val (1,"abc")
+--
+-- >>> pz @(EBothDef Id Fst Snd) ((999,"xx"),ENone)
+-- Val (999,"xx")
+--
+data EBothDef p q r deriving Show
+
+type EBothDefT p q r = ElrIn p (Fst >> p) (Fst >> p) Snd q r
+
+instance P (EBothDefT p q r) x => P (EBothDef p q r) x where
+  type PP (EBothDef p q r) x = PP (EBothDefT p q r) x
+  eval _ = eval (Proxy @(EBothDefT p q r))
+
+-- | converts 'Elr' to 'These'
+--
+-- >>> pz @Elr2These ENone
+-- Val Nothing
+--
+-- >>> pz @Elr2These (ELeft 123)
+-- Val (Just (This 123))
+--
+data Elr2These deriving Show
+
+instance P Elr2These (Elr a b) where
+  type PP Elr2These (Elr a b) = Maybe (These a b)
+  eval _ opts x =
+    let msg0 = "Elr2These"
+        b = x ^. _elr2These
+    in pure $ mkNode opts (Val b) msg0 []
+
+-- | converts 'These' to 'Elr'
+--
+-- >>> pz @These2Elr (These 12 'x')
+-- Val (EBoth 12 'x')
+--
+-- >>> pz @These2Elr (This 123)
+-- Val (ELeft 123)
+--
+data These2Elr deriving Show
+
+instance P These2Elr (These a b) where
+  type PP These2Elr (These a b) = Elr a b
+  eval _ opts x =
+    let msg0 = "These2Elr"
+        b = _elr2These # Just x
+    in pure $ mkNode opts (Val b) msg0 []
+
+-- | converts 'Elr' to a pair of Maybes
+--
+-- >>> pz @Elr2Maybe ENone
+-- Val (Nothing,Nothing)
+--
+-- >>> pz @Elr2Maybe (ELeft 123)
+-- Val (Just 123,Nothing)
+--
+-- >>> pz @Elr2Maybe (EBoth 'x' 123)
+-- Val (Just 'x',Just 123)
+--
+-- >>> pz @Elr2Maybe (ERight 123)
+-- Val (Nothing,Just 123)
+--
+data Elr2Maybe deriving Show
+
+instance P Elr2Maybe (Elr a b) where
+  type PP Elr2Maybe (Elr a b) = (Maybe a, Maybe b)
+  eval _ opts x =
+    let msg0 = "Elr2Maybe"
+        b = x ^. _elr2Maybe
+    in pure $ mkNode opts (Val b) msg0 []
+
+
+

@@ -43,7 +43,6 @@   , Pred
   , ToEnum
   , ToEnum'
-
  ) where
 import Predicate.Core
 import Predicate.Util
@@ -51,6 +50,7 @@ import Data.Proxy (Proxy(..))
 import Data.Kind (Type)
 import Data.Tree (Tree)
+import Control.Lens (under,enum)
 -- $setup
 -- >>> :set -XDataKinds
 -- >>> :set -XTypeApplications
@@ -112,7 +112,7 @@    pp <- eval (Proxy @p) opts (Proxy @a)
    pure $ case getValueLR NoInline opts msg1 pp [hhqq] of
      Left e -> e
-     Right _ -> mkNodeCopy opts pp msg1 [hhqq, hh pp]
+     Right _ -> mkNodeCopy opts pp msg1 [hhqq]
 
 -- | bounded 'succ' function
 --
@@ -197,7 +197,7 @@ --
 data Succ deriving Show
 {-
->print $! (succ Proxy)
+>print $! (succ Proxy) -- need to force this to get an exception
 *** Exception: Proxy.succ
 -}
 instance ( Show x
@@ -226,6 +226,9 @@ -- >>> pz @(SuccN 2 'LT) ()
 -- Val GT
 --
+-- >>> pz @(SuccN (Negate 3) (C "x")) ()
+-- Val 'u'
+--
 data SuccN n p deriving Show
 
 instance ( Show a
@@ -242,7 +245,7 @@     case lr of
       Left e -> pure e
       Right (fromIntegral -> n :: Int,p,nn,pp) -> do
-        lr1 <- catchit (toEnum (fromEnum p + n))
+        lr1 <- catchit (under enum (+n) p)
         pure $ case lr1 of
           Left e -> mkNode opts (Fail (msg0 <> " " <> e)) (litL opts (msg0 <> " " <> show n <> " " <> show p)) [hh nn, hh pp]
           Right r -> mkNode opts (Val r) (litL opts (msg0 <> " " <> show n <> " " <> show p)) [hh nn, hh pp]
@@ -343,7 +346,6 @@ 
 instance ( PP p x ~ a
          , P p x
-         , Show a
          , Enum (PP t x)
          , Show (PP t x)
          , Integral a
@@ -354,8 +356,8 @@     pp <- eval (Proxy @p) opts x
     case getValueLR NoInline opts msg0 pp [] of
       Left e -> pure e
-      Right p -> do
-        lr <- catchit (toEnum $! fromIntegral p)
+      Right (fromIntegral -> p) -> do
+        lr <- catchit (toEnum p)
         pure $ case lr of
           Left e -> mkNode opts (Fail (msg0 <> " " <> e)) (showL opts p) [hh pp]
           Right n -> mkNode opts (Val n) (show3 opts msg0 n p) [hh pp]
@@ -414,7 +416,7 @@              dd <- eval (Proxy @def) opts (Proxy @(PP t a))
              pure $ case getValueLR NoInline opts msg1 dd [hh pp] of
                Left e -> e
-               Right _ -> mkNodeCopy opts dd msg1 [hh pp, hh dd]
+               Right _ -> mkNodeCopy opts dd msg1 [hh pp]
           Just n -> pure $ mkNode opts (Val n) (show3 opts msg0 n a) [hh pp]
 
 -- | bounded 'toEnum' function

@@ -40,7 +40,6 @@ 
  -- ** luhn check
   , IsLuhn
-
  ) where
 import Predicate.Core
 import Predicate.Misc
@@ -475,11 +474,11 @@     let msg0 = "IsLuhn"
     in pure $ case chkSize opts msg0 x [] of
          Left e -> e
-         Right ws ->
+         Right (_,ws) ->
           let xs = zipWith (*) (ws ^. reversed) (cycle' [1,2])
               ys = map (\w -> if w>=10 then w-9 else w) xs
               z = sum' ys
               ret = z `mod` 10
-          in if ret == 0 then mkNodeB opts True (msg0 <> " | " <> showL opts ws) []
+          in if ret == 0 then mkNodeB opts True (joinStrings msg0 (showL opts ws)) []
              else mkNodeB opts False (msg0 <> " map=" <> showL opts ys <> " sum=" <> showL opts z <> " ret=" <> showL opts ret <> showVerbose opts " | " ws) []
 

@@ -17,9 +17,11 @@ {-# LANGUAGE ViewPatterns #-}
 -- | promoted foldable functions
 module Predicate.Data.Foldable (
+  -- ** functions
     Concat
   , ConcatMap
   , Cycle
+  , FoldAla
   , FoldMap
 
   , ToListExt
@@ -39,7 +41,6 @@ 
   , Ands
   , Ors
-
  ) where
 import Predicate.Core
 import Predicate.Misc
@@ -48,7 +49,7 @@ import Control.Lens
 import Data.Typeable (Typeable, Proxy(Proxy))
 import Data.Kind (Type)
-import Data.Foldable (Foldable(toList))
+import Data.Foldable (Foldable(toList,fold))
 import qualified Data.List.NonEmpty as N
 import Data.List.NonEmpty (NonEmpty(..))
 import qualified GHC.Exts as GE
@@ -267,6 +268,12 @@ 
 -- | similar to 'concat'
 --
+-- >>> pz @Concat (Just "abc")
+-- Val "abc"
+--
+-- >>> pz @Concat (Left 123)
+-- Val []
+--
 -- >>> pz @Concat ["abc","D","eF","","G"]
 -- Val "abcDeFG"
 --
@@ -275,9 +282,9 @@ --
 data Concat deriving Show
 
-instance ( Show a
-         , Show x
+instance ( Show x
          , x ~ t [a]
+         , Show a
          , Foldable t
          ) => P Concat x where
   type PP Concat x = ExtractAFromTA x
@@ -305,8 +312,8 @@ --
 data Cycle n p deriving Show
 
-instance ( Show a
-         , PP p x ~ t a
+instance ( PP p x ~ t a
+         , Show x
          , P p x
          , Integral (PP n x)
          , P n x
@@ -322,11 +329,10 @@         let hhs = [hh nn, hh pp]
         in case chkSize opts msg0 p hhs of
             Left e ->  e
-            Right ps ->
+            Right (_,ps) ->
               let msg1 = msg0 <> "(" <> show n <> ")"
                   d = take n (cycle' ps)
-              in mkNode opts (Val d) (show3 opts msg1 d ps) hhs
-
+              in mkNode opts (Val d) (showVerbose opts msg1 x) hhs
 
 -- | similar to 'toList'
 --
@@ -398,97 +404,149 @@ --
 data Null deriving Show
 type NullT = Null' Id
+
 instance P NullT a => P Null a where
   type PP Null a = Bool
   eval _ = evalBool (Proxy @NullT)
 
+-- | similar to 'Data.Foldable.foldMap'
+--
+-- >>> pl @(FoldMap (Wrap (SG.Sum _) Id)) (Left "x")
+-- Present Sum {getSum = 0} (FoldMap <skipped>)
+-- Val (Sum {getSum = 0})
+--
+-- >>> pz @(FoldMap (Wrap (SG.Sum _) Id)) [1..5]
+-- Val (Sum {getSum = 15})
+--
+-- >>> pl @(FoldMap (Wrap (SG.Sum _) Id)) (Right 123)
+-- Present Sum {getSum = 123} (FoldMap Wrap Sum {getSum = 123} | 123)
+-- Val (Sum {getSum = 123})
+--
+-- >>> pl @(FoldMap (Map Len)) (Just ["abc","defg","h"])
+-- Present [3,4,1] (FoldMap Map [3,4,1] | ["abc","defg","h"])
+-- Val [3,4,1]
+--
+-- >>> pz @(FoldMap (Map Len)) (Just ["abc","defg","h"])
+-- Val [3,4,1]
+--
+-- >>> pz @(FoldMap (Wrap (SG.Sum _) Len)) ["abc","defg","h"]
+-- Val (Sum {getSum = 8})
+--
+-- >>> pz @(FoldMap (FoldMap (Wrap (SG.Sum _) Id))) (Just [1..10])
+-- Val (Sum {getSum = 55})
+--
+data FoldMap p deriving Show
+
+instance ( Traversable n
+         , Monoid t
+         , PP p a ~ t
+         , P p a
+         ) => P (FoldMap p) (n a) where
+  type PP (FoldMap p) (n a) = PP p a
+  eval _ opts na = do
+    let msg0 = "FoldMap"
+    nttb <- traverse
+              (fmap (\tt -> tt & ttString %~ litL opts
+                               & ttForest .~ [hh tt]) . eval (Proxy @p) opts)
+              na
+    let ttnb = sequenceA nttb
+    pure $ case getValueLR Inline opts "" ttnb [] of
+      Left e -> e
+      Right ret ->
+        let ind = case foldMap pure ret of
+                    [] -> " <skipped>"
+                    _:_ -> ""
+            d = fold ret
+        in ttnb & ttVal .~ Val d
+                & ttString %~ (msg0 <>) . (ind <>) . nullIf " "
+
 -- | wraps each item in the foldable container and then unwraps the mconcatenated result: uses 'Control.Lens.Wrapped.Wrapped'
 --
--- >>> pz @(FoldMap (SG.Sum _) Id) [44, 12, 3]
+-- >>> pz @(FoldAla (SG.Sum _)) [44, 12, 3]
 -- Val 59
 --
--- >>> pz @(FoldMap (SG.Product _) Id) [44, 12, 3]
+-- >>> pz @(FoldAla (SG.Product _)) [44, 12, 3]
 -- Val 1584
 --
--- >>> type Ands' p = FoldMap SG.All p
--- >>> pz @(Ands' Id) [True,False,True,True]
+-- >>> type Ands' = FoldAla SG.All
+-- >>> pz @Ands' [True,False,True,True]
 -- Val False
 --
--- >>> pz @(Ands' Id) [True,True,True]
+-- >>> pz @Ands' [True,True,True]
 -- Val True
 --
--- >>> pz @(Ands' Id) []
+-- >>> pz @Ands' []
 -- Val True
 --
--- >>> type Ors' p = FoldMap SG.Any p
--- >>> pz @(Ors' Id) [False,False,False]
+-- >>> type Ors' = FoldAla SG.Any
+-- >>> pz @Ors' [False,False,False]
 -- Val False
 --
--- >>> pz @(Ors' Id) []
+-- >>> pz @Ors' []
 -- Val False
 --
--- >>> pz @(Ors' Id) [False,False,False,True]
+-- >>> pz @Ors' [False,False,False,True]
 -- Val True
 --
--- >>> type AllPositive' = FoldMap SG.All (Map Positive)
+-- >>> type AllPositive' = Map Positive >> FoldAla SG.All
 -- >>> pz @AllPositive' [3,1,-5,10,2,3]
 -- Val False
 --
--- >>> type AllNegative' = FoldMap SG.All (Map Negative)
+-- >>> type AllNegative' = Map Negative >> FoldAla SG.All
 -- >>> pz @AllNegative' [-1,-5,-10,-2,-3]
 -- Val True
 --
 -- >>> :set -XKindSignatures
--- >>> type Max' (t :: Type) = FoldMap (SG.Max t) Id -- requires t be Bounded for monoid instance
+-- >>> type Max' (t :: Type) = FoldAla (SG.Max t) -- requires t be Bounded for monoid instance
 -- >>> pz @(Max' Int) [10,4,5,12,3,4]
 -- Val 12
 --
--- >>> pl @(FoldMap (SG.Sum _) Id) [14,8,17,13]
+-- >>> pl @(FoldAla (SG.Sum _)) [14,8,17,13]
 -- Present 52 ((>>) 52 | {getSum = 52})
 -- Val 52
 --
--- >>> pl @(FoldMap (SG.Max _) Id) [14 :: Int,8,17,13] -- allowed as the values are Bounded!
+-- >>> pl @(FoldAla (SG.Max _)) [14 :: Int,8,17,13] -- allowed as the values are Bounded!
 -- Present 17 ((>>) 17 | {getMax = 17})
 -- Val 17
 --
--- >>> pl @((Len >> (Elem Id '[4,7,1] || (Mod Id 3 >> Same 0))) || (FoldMap (SG.Sum _) Id >> Gt 200)) [1..20]
+-- >>> pl @((Len >> (Elem Id '[4,7,1] || (Mod Id 3 >> Same 0))) || (FoldAla (SG.Sum _) >> Gt 200)) [1..20]
 -- True (False || True)
 -- Val True
 --
--- >>> pl @((Len >> (Elem Id '[4,7,1] || (Mod Id 3 >> Same 0))) || (FoldMap (SG.Sum _) Id >> Gt 200)) [1..19]
+-- >>> pl @((Len >> (Elem Id '[4,7,1] || (Mod Id 3 >> Same 0))) || (FoldAla (SG.Sum _) >> Gt 200)) [1..19]
 -- False (False || False | ((>>) False | {1 == 0}) || ((>>) False | {190 > 200}))
 -- Val False
 --
--- >>> pl @((Len >> (Elem Id '[4,7,1] || (Mod Id 3 >> Same 0))) || (FoldMap (SG.Sum _) Id >> Gt 200)) []
+-- >>> pl @((Len >> (Elem Id '[4,7,1] || (Mod Id 3 >> Same 0))) || (FoldAla (SG.Sum _) >> Gt 200)) []
 -- True (True || False)
 -- Val True
 --
--- >>> pl @((Len >> (Elem Id '[4,7,1] || (Mod Id 3 >> Same 0))) &&& FoldMap (SG.Sum _) Id) [1..20]
+-- >>> pl @((Len >> (Elem Id '[4,7,1] || (Mod Id 3 >> Same 0))) &&& FoldAla (SG.Sum _)) [1..20]
 -- Present (False,210) ('(False,210))
 -- Val (False,210)
 --
--- >>> pl @(FoldMap SG.Any Id) [False,False,True,False]
+-- >>> pl @(FoldAla SG.Any) [False,False,True,False]
 -- Present True ((>>) True | {getAny = True})
 -- Val True
 --
--- >>> pl @(FoldMap SG.All Id) [False,False,True,False]
+-- >>> pl @(FoldAla SG.All) [False,False,True,False]
 -- Present False ((>>) False | {getAll = False})
 -- Val False
 --
--- >>> pl @(FoldMap (SG.Sum _) Id) (Just 13)
+-- >>> pl @(FoldAla (SG.Sum _)) (Just 13)
 -- Present 13 ((>>) 13 | {getSum = 13})
 -- Val 13
 --
--- >>> pl @(FoldMap (SG.Sum _) Id) [1..10]
+-- >>> pl @(FoldAla (SG.Sum _)) [1..10]
 -- Present 55 ((>>) 55 | {getSum = 55})
 -- Val 55
 --
-data FoldMap (t :: Type) p deriving Show
-type FoldMapT (t :: Type) p = Map' (Wrap t Id) p >> MConcat Id >> Unwrap
+data FoldAla (t :: Type) deriving Show
+type FoldAlaT (t :: Type) = Map' (Wrap t Id) Id >> MConcat >> Unwrap
 
-instance P (FoldMapT t p) x => P (FoldMap t p) x where
-  type PP (FoldMap t p) x = PP (FoldMapT t p) x
-  eval _ = eval (Proxy @(FoldMapT t p))
+instance P (FoldAlaT t) x => P (FoldAla t) x where
+  type PP (FoldAla t) x = PP (FoldAlaT t) x
+  eval _ = eval (Proxy @(FoldAlaT t))
 
 -- | similar to 'Data.Foldable.and'
 --
@@ -505,18 +563,20 @@ data Ands deriving Show
 
 instance ( x ~ t a
-         , Show (t a)
          , Foldable t
          , a ~ Bool
          ) => P Ands x where
   type PP Ands x = Bool
-  eval _ opts x =
+  eval _ opts x' =
     let msg0 = "Ands"
-        msg1 = msg0 ++ "(" ++ show (length x) ++ ")"
-        w = case findIndex not (toList x) of
-              Nothing -> ""
-              Just i -> " i="++show i
-    in pure $ mkNodeB opts (and x) (msg1 <> w <> showVerbose opts " | " x) []
+    in pure $ case chkSize opts msg0 x' [] of
+         Left e -> e
+         Right (xLen,x) ->
+           let msg1 = msg0 ++ "(" ++ show xLen ++ ")"
+               w = case findIndex not x of
+                     Nothing -> ""
+                     Just i -> " i="++show i
+           in mkNodeB opts (and x) (msg1 <> w <> showVerbose opts " | " x) []
 
 -- | similar to 'Data.Foldable.or'
 --
@@ -534,16 +594,18 @@ data Ors deriving Show
 
 instance ( x ~ t a
-         , Show x
          , Foldable t
          , a ~ Bool
          ) => P Ors x where
   type PP Ors x = Bool
-  eval _ opts x =
+  eval _ opts x' =
     let msg0 = "Ors"
-        msg1 = msg0 ++ "(" ++ show (length x) ++ ")"
-        w = case findIndex id (toList x) of
-              Nothing -> ""
-              Just i -> " i=" ++ show i
-    in pure $ mkNodeB opts (or x) (msg1 <> w <> showVerbose opts " | " x) []
+    in pure $ case chkSize opts msg0 x' [] of
+         Left e -> e
+         Right (xLen,x) ->
+           let msg1 = msg0 ++ "(" ++ show xLen ++ ")"
+               w = case findIndex id x of
+                     Nothing -> ""
+                     Just i -> " i="++show i
+           in mkNodeB opts (or x) (msg1 <> w <> showVerbose opts " | " x) []
 

@@ -42,7 +42,6 @@   -- ** date time
   , TimeUtc
   , TimeZt
-
  ) where
 import Predicate.Core
 import Predicate.Misc

@@ -16,6 +16,7 @@ {-# LANGUAGE EmptyDataDeriving #-}
 -- | promoted indexing functions
 module Predicate.Data.Index (
+  -- ** functions
     Ix
   , Ix'
   , IxL
@@ -223,7 +224,7 @@            pp <- eval (Proxy @def) opts (Proxy @a)
            pure $ case getValueLR Inline opts msg1 pp [] of
              Left e -> e
-             Right _ -> mkNodeCopy opts pp msg1 [hh pp]
+             Right _ -> mkNodeCopy opts pp msg1 []
          Just a -> pure $ mkNode opts (Val a) (msg0 <> " " <> showL opts a) []
 
 -- | similar to 'Data.List.!!' for lists with a default error message on failure
@@ -375,11 +376,11 @@ -- Present 3 (IxL('d') 3 | p=fromList [('a',0),('b',1),('c',2),('d',3)] | q='d')
 -- Val 3
 --
--- >>> pl @(Id !! FromString _ "d" &&& (Map' (Snd >> Gt 3 >> Coerce SG.Any) (IToList _) >> MConcat Id)) (M.fromList $ zip (map T.singleton "abcdefgh") [0 ..])
+-- >>> pl @(Id !! FromString _ "d" &&& (Map' (Snd >> Gt 3 >> Coerce SG.Any) (IToList _) >> MConcat)) (M.fromList $ zip (map T.singleton "abcdefgh") [0 ..])
 -- Present (3,Any {getAny = True}) ('(3,Any {getAny = True}))
 -- Val (3,Any {getAny = True})
 --
--- >>> pl @(Id !! FromString _ "d" &&& (Map' (Snd >> Gt 3 >> Wrap SG.Any Id) (IToList _) >> MConcat Id >> Unwrap)) (M.fromList $ zip (map T.singleton "abcdefgh") [0 ..])
+-- >>> pl @(Id !! FromString _ "d" &&& (Map' (Snd >> Gt 3 >> Wrap SG.Any Id) (IToList _) >> MConcat >> Unwrap)) (M.fromList $ zip (map T.singleton "abcdefgh") [0 ..])
 -- Present (3,True) ('(3,True))
 -- Val (3,True)
 --

@@ -16,6 +16,7 @@ {-# LANGUAGE EmptyDataDeriving #-}
 -- | promoted iterator functions
 module Predicate.Data.Iterator (
+  -- ** functions
     Scanl
   , ScanN
   , ScanNA
@@ -34,6 +35,8 @@   , DoN
   , Repeat
 
+  -- ** type families
+  , UnfoldrT
  ) where
 import Predicate.Core
 import Predicate.Misc
@@ -43,8 +46,9 @@ import Predicate.Data.Enum (type (...), Pred)
 import Predicate.Data.List (Last)
 import Predicate.Data.Maybe (MaybeBool)
-import GHC.TypeLits (Nat, KnownNat)
+import GHC.TypeLits (Nat, KnownNat, ErrorMessage((:$$:),(:<>:)))
 import qualified GHC.TypeLits as GL
+import Data.Kind (Type)
 import Control.Lens
 import Data.Proxy (Proxy(Proxy))
 import Data.Maybe (catMaybes)
@@ -97,7 +101,7 @@           Left e -> pure e
           Right _ -> do
             let ff i b as' rs
-                 | i >= oRecursion opts = pure (rs, Left $ mkNode opts (Fail (msg0 <> ":recursion limit i=" <> show i)) ("(b,as')=" <> showL opts (b,as')) [])
+                 | i >= getMaxRecursionValue opts = pure (rs, Left $ mkNode opts (Fail (msg0 <> ":recursion limit i=" <> show i)) ("(b,as')=" <> showL opts (b,as')) [])
                  | otherwise =
                        case as' of
                          [] -> pure (rs, Right ()) -- ++ [((i,q), mkNode opts (Val q) (msg0 <> "(done)") [])], Right ())
@@ -113,7 +117,7 @@                    let vals = map (view _1) abcs
                        itts = map (view _2 &&& view _3) abcs
                    in case lrx of
-                        Left e -> mkNodeCopy opts e msg0 (hh qq : hh rr : map (hh . prefixNumberToTT) itts ++ [hh e])
+                        Left e -> mkNodeCopy opts e msg0 (hh qq : hh rr : map (hh . prefixNumberToTT) itts)
                         Right () -> mkNode opts (Val vals) (show3' opts msg0 vals "b=" q <> showVerbose opts " | as=" r) (hh qq : hh rr : map (hh . prefixNumberToTT) itts)
 
 -- | iterates n times keeping all the results
@@ -331,7 +335,7 @@       Left e -> pure e
       Right q -> do
         let msg1 = msg0 <> " " <> showL opts q
-            ff i s rs | i >= oRecursion opts = pure (rs, Left $ mkNode opts (Fail (msg1 <> ":recursion limit i=" <> show i)) ("s=" <> showL opts s) [])
+            ff i s rs | i >= getMaxRecursionValue opts = pure (rs, Left $ mkNode opts (Fail (msg1 <> ":recursion limit i=" <> show i)) ("s=" <> showL opts s) [])
                       | otherwise = do
                               pp :: TT (PP p s) <- evalHide @p opts s
                               case getValueLR NoInline opts (msg1 <> " i=" <> show i <> " s=" <> show s) pp [] of
@@ -345,13 +349,17 @@                let vals = map (view _1) abcs
                    itts = map (view _2 &&& view _3) abcs
                in case lr of
-                   Left e -> mkNodeCopy opts e msg1 (hh qq : map (hh . prefixNumberToTT) itts ++ [hh e])
+                   Left e -> mkNodeCopy opts e msg1 (hh qq : map (hh . prefixNumberToTT) itts)
                    Right () ->
                      let ret = fst <$> catMaybes vals
                      in mkNode opts (Val ret) (show3' opts msg1 ret "s=" q ) (hh qq : map (hh . prefixNumberToTT) itts)
 
-type family UnfoldrT mbs where
-  UnfoldrT (Maybe (b, _s)) = b
+type family UnfoldrT (mbs :: Type) where
+  UnfoldrT (Maybe (b, _)) = b
+  UnfoldrT o = GL.TypeError (
+      'GL.Text "UnfoldrT: expected 'Maybe (b, _)' "
+      ':$$: 'GL.Text "o = "
+      ':<>: 'GL.ShowType o)
 
 -- | run @p@ @n@ times with state @s@
 data UnfoldN n p s deriving Show
@@ -458,13 +466,16 @@          , P (ParaImpl (LenT ps) ps) x
          ) => P (Para ps) x where
   type PP (Para ps) x = PP (ParaImpl (LenT ps) ps) x
-  eval _ opts as = do
+  eval _ opts as' = do
     let msg0 = "Para"
         n = getLen @ps
-    if n /= length as then
-       let msg1 = msg0 <> badLength as n
-       in pure $ mkNode opts (Fail msg1) "" []
-    else eval (Proxy @(ParaImpl (LenT ps) ps)) opts as
+    case chkSize opts msg0 as' [] of
+      Left e -> pure e
+      Right (asLen,as) ->
+        if n /= asLen then
+           let msg1 = msg0 <> badLength asLen n
+           in pure $ mkNode opts (Fail msg1) "" []
+        else eval (Proxy @(ParaImpl (LenT ps) ps)) opts as
 
 -- only allow non empty lists -- might need [a] ~ x but it seems fine
 instance GL.TypeError ('GL.Text "ParaImpl '[] invalid: requires at least one value in the list")
@@ -606,6 +617,7 @@ --
 data DoN (n :: Nat) p deriving Show
 type DoNT (n :: Nat) p = Do (RepeatT n p)
+
 instance P (DoNT n p) a => P (DoN n p) a where
   type PP (DoN n p) a = PP (DoNT n p) a
   eval _ = eval (Proxy @(DoNT n p))

@@ -16,6 +16,7 @@ {-# LANGUAGE EmptyDataDeriving #-}
 -- | promoted json encoding and decoding functions
 module Predicate.Data.Json (
+  -- ** functions
     ParseJson'
   , ParseJson
   , EncodeJson

@@ -1,6 +1,4 @@ {-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TupleSections #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -16,7 +14,6 @@ {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE NoStarIsType #-}
 {-# LANGUAGE EmptyDataDeriving #-}
-{-# LANGUAGE DeriveTraversable #-}
 -- | lifted promoted functions
 module Predicate.Data.Lifted (
  -- ** functor
@@ -25,6 +22,7 @@   , type (<&>)
 
  -- ** applicative
+  , Pure
   , type (<*>)
   , LiftA2
   , FPair
@@ -42,9 +40,16 @@ 
  -- ** alternative
   , type (<|>)
+  , EmptyT
+  , EmptyT'
+  , EmptyList
+  , EmptyList'
+  , EmptyBool
+  , EmptyBool'
 
  -- ** bifunctor
-  , type BiMap
+  , BiMap
+  , BiFoldMap
 
  -- ** comonad
   , Extract
@@ -63,16 +68,21 @@   , K
   , Lift
 
+ -- ** coerce
+  , Coerce
+
  -- ** error handling
   , Catch
   , Catch'
 
- -- ** miscellaneous
-  , ELR(..)
+ -- ** type families
+  , DotExpandT
+  , RDotExpandT
  ) where
 import Predicate.Core
 import Predicate.Misc
 import Predicate.Util
+import Predicate.Elr (getBifoldInfo)
 import qualified GHC.TypeLits as GL
 import Control.Applicative
 import Control.Monad (join)
@@ -83,6 +93,7 @@ import Data.Proxy (Proxy(..))
 import Data.Bitraversable
 import Data.Bifoldable
+import Data.Coerce (Coercible)
 -- $setup
 -- >>> :set -XDataKinds
 -- >>> :set -XTypeApplications
@@ -253,7 +264,157 @@         let d = p <|> q
         in mkNode opts (Val d) (show3' opts msg0 d "p=" p <> showVerbose opts " | q=" q) [hh pp, hh qq]
 
+-- | similar to 'Data.List.empty'
+--
+-- >>> pz @(EmptyT Maybe _) ()
+-- Val Nothing
+--
+-- >>> pz @(EmptyT [] _) ()
+-- Val []
+--
+-- >>> pz @(C "x" >> EmptyT [] String) (13,True)
+-- Val []
+--
+-- >>> pz @(Fst >> EmptyT (Either String) _) (13,True)
+-- Val (Left "")
+--
+-- >>> pz @(If 'True (MkJust 11) (EmptyT _ _)) ()
+-- Val (Just 11)
+--
+-- >>> pz @(EmptyT [] _ <> "123") ()
+-- Val "123"
+--
+data EmptyT (t :: Type -> Type) (t1 :: Type) deriving Show
+type EmptyTT (t :: Type -> Type) (t1 :: Type) = EmptyT' t (Hole t1)
 
+instance Alternative t => P (EmptyT t t1) x where
+  type PP (EmptyT t t1) x = PP (EmptyTT t t1) x
+  eval _ = eval (Proxy @(EmptyTT t t1))
+
+-- | similar to 'Data.List.empty' where @t@ is the type of the container and @t1@ is a reference to the type of the items in the container
+--
+-- >>> pz @(EmptyT' [] "x") ()
+-- Val []
+--
+-- >>> pz @(EmptyT' (Either String) (1 % 1)) ()
+-- Val (Left "")
+--
+-- >>> pl @(If 'True (MkJust 11) (EmptyT' _ 0)) ()
+-- Present Just 11 (If 'True Just 11)
+-- Val (Just 11)
+--
+-- >>> pz @(If 'True (MkJust 11) (EmptyT' _ (Hole Int))) ()
+-- Val (Just 11)
+--
+-- >>> pz @(If 'False (MkJust 11) (EmptyT' _ (Hole Int))) ()
+-- Val Nothing
+
+data EmptyT' (t :: Type -> Type) p deriving Show
+
+instance Alternative t => P (EmptyT' t p) x where
+  type PP (EmptyT' t p) x = t (PP p x)
+  eval _ opts _ =
+    let msg0 = "EmptyT'"
+        b = empty @t
+    in pure $ mkNode opts (Val b) msg0 []
+
+-- | creates an empty list for the given pointer to a type @t@
+--
+-- >>> pz @(EmptyList' 123 <> '[Id]) 99
+-- Val [99]
+--
+data EmptyList' (t :: k) deriving Show
+type EmptyListT' (t :: k) = EmptyT' [] t
+
+instance P (EmptyList' t) x where
+  type PP (EmptyList' t) x = PP (EmptyListT' t) x
+  eval _ = eval (Proxy @(EmptyListT' t))
+
+-- | creates an empty list for the given type
+--
+-- >>> pz @(Id :+ EmptyList _) 99
+-- Val [99]
+--
+data EmptyList (t :: Type) deriving Show
+type EmptyListT (t :: Type) = EmptyT [] t
+
+instance P (EmptyList t) x where
+  type PP (EmptyList t) x = PP (EmptyListT t) x
+  eval _ = eval (Proxy @(EmptyListT t))
+
+-- | Convenient method to convert a value @p@ to an Alternative based on a predicate @b@
+--
+--   if @b@ is True then pure @p@ else empty
+--
+-- >>> pz @(EmptyBool [] (Id > 4) 'True) 24
+-- Val [True]
+--
+-- >>> pz @(EmptyBool [] (Id > 4) 'True) 1
+-- Val []
+--
+data EmptyBool t b p deriving Show
+
+instance ( Show (PP p a)
+         , P b a
+         , P p a
+         , PP b a ~ Bool
+         , Alternative t
+         ) => P (EmptyBool t b p) a where
+  type PP (EmptyBool t b p) a = t (PP p a)
+  eval _ opts z = do
+    let msg0 = "EmptyBool"
+    bb <- evalBool (Proxy @b) opts z
+    case getValueLR NoInline opts (msg0 <> " b failed") bb [] of
+      Left e -> pure e
+      Right True -> do
+        pp <- eval (Proxy @p) opts z
+        pure $ case getValueLR NoInline opts (msg0 <> " p failed") pp [hh bb] of
+          Left e -> e
+          Right p -> mkNode opts (Val (pure p)) (msg0 <> "(False) Just " <> showL opts p) [hh bb, hh pp]
+      Right False -> pure $ mkNode opts (Val empty) (msg0 <> "(True)") [hh bb]
+
+
+-- | Convenient method to convert a value @p@ to an Alternative based on a predicate @b@
+--   the value of p drives the choice of Alternative to use for the empty
+--   similar to 'EmptyBool' but no need to provide @t@ as it is inferred from the resulting type of @p@
+--
+--   if @b@ is True then run @p@ else empty
+--
+-- >>> pz @(EmptyBool' (Id > 4) (MkJust (Id * 3))) 24
+-- Val (Just 72)
+--
+-- >>> pz @(EmptyBool' (Id > 4) (MkJust (Id * 3))) 2
+-- Val Nothing
+--
+-- >>> pz @(EmptyBool' (Len > 0) Head) ["Abcd","def","g"::String]
+-- Val "Abcd"
+--
+-- >>> pz @(EmptyBool' (Len > 0) Head) ([] :: [String])
+-- Val ""
+--
+data EmptyBool' b p deriving Show
+
+instance ( Show (PP p a)
+         , P b a
+         , P p a
+         , PP p a ~ t x
+         , PP b a ~ Bool
+         , Alternative t
+         ) => P (EmptyBool' b p) a where
+  type PP (EmptyBool' b p) a = PP p a
+  eval _ opts z = do
+    let msg0 = "EmptyBool'"
+    bb <- evalBool (Proxy @b) opts z
+    case getValueLR NoInline opts (msg0 <> " b failed") bb [] of
+      Left e -> pure e
+      Right True -> do
+        pp <- eval (Proxy @p) opts z
+        pure $ case getValueLR NoInline opts (msg0 <> " p failed") pp [hh bb] of
+          Left e -> e
+          Right p -> mkNodeCopy opts pp (msg0 <> "(False) Just " <> showL opts p) [hh bb]
+      Right False -> pure $ mkNode opts (Val empty) (msg0 <> "(True)") [hh bb]
+
+
 -- | similar to 'Control.Comonad.extract'
 --
 -- >>> pz @Extract (Nothing,Just 20)
@@ -433,7 +594,7 @@ 
 -- | like 'traverse'
 --
--- >>> pl @(Traverse (If (Gt 3) (Pure Maybe Id) (EmptyT Maybe))) [1..5]
+-- >>> pl @(Traverse (If (Gt 3) (Pure Maybe Id) (EmptyT Maybe _))) [1..5]
 -- Present Nothing ((>>) Nothing | {Sequence Nothing | [Nothing,Nothing,Nothing,Just 4,Just 5]})
 -- Val Nothing
 --
@@ -441,7 +602,7 @@ -- Present Nothing ((>>) Nothing | {Sequence Nothing | [Just 1,Just 2,Just 3,Nothing,Nothing]})
 -- Val Nothing
 --
--- >>> pl @(Traverse (If (Gt 0) (Pure Maybe Id) (EmptyT Maybe))) [1..5]
+-- >>> pl @(Traverse (If (Gt 0) (Pure Maybe Id) (EmptyT Maybe _))) [1..5]
 -- Present Just [1,2,3,4,5] ((>>) Just [1,2,3,4,5] | {Sequence Just [1,2,3,4,5] | [Just 1,Just 2,Just 3,Just 4,Just 5]})
 -- Val (Just [1,2,3,4,5])
 --
@@ -588,8 +749,8 @@          qq <- eval (Proxy @q) opts ((emsg, x), Proxy @(PP p x))
          pure $ case getValueLR NoInline opts (msg0 <> " default condition failed") qq [hh pp] of
             Left e1 -> e1
-            Right _ -> mkNodeCopy opts qq (msg0 <> " caught exception[" <> emsg <> "]") [hh pp, hh qq]
-      Right _ -> pure $ mkNodeCopy opts pp (msg0 <> " did not fire") [hh pp]
+            Right _ -> mkNodeCopy opts qq (msg0 <> " caught exception[" <> emsg <> "]") [hh pp]
+      Right _ -> pure $ mkNodeCopy opts pp (msg0 <> " did not fire") []
 
 -- | compose simple functions
 --
@@ -897,6 +1058,54 @@   type PP (p <&> q) x = PP (FMapFlipT p q) x
   eval _ = eval (Proxy @(FMapFlipT p q))
 
+
+-- | similar to 'pure'
+--
+-- >>> pz @(Pure Maybe Id) 4
+-- Val (Just 4)
+--
+-- >>> pz @(Pure [] Id) 4
+-- Val [4]
+--
+-- >>> pz @(Pure (Either String) Fst) (13,True)
+-- Val (Right 13)
+--
+-- >>> pl @(Pure Maybe Id) 'x'
+-- Present Just 'x' (Pure Just 'x' | 'x')
+-- Val (Just 'x')
+--
+-- >>> pl @(Pure (Either _) Id) 'x'
+-- Present Right 'x' (Pure Right 'x' | 'x')
+-- Val (Right 'x')
+--
+-- >>> pl @(Pure (Either _) Id >> Swap) 'x'
+-- Present Left 'x' ((>>) Left 'x' | {Swap Left 'x' | Right 'x'})
+-- Val (Left 'x')
+--
+-- >>> pl @(Pure (Either ()) Id >> Swap) 'x'
+-- Present Left 'x' ((>>) Left 'x' | {Swap Left 'x' | Right 'x'})
+-- Val (Left 'x')
+--
+-- >>> pl @(Pure (Either String) Id >> Swap) 123
+-- Present Left 123 ((>>) Left 123 | {Swap Left 123 | Right 123})
+-- Val (Left 123)
+--
+data Pure (t :: Type -> Type) p deriving Show
+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 NoInline opts msg0 pp [] of
+      Left e -> e
+      Right a ->
+        let b = pure a
+        in mkNode opts (Val b) (show3 opts msg0 b a) [hh pp]
+
 -- | runs 'Control.Applicative.liftA2' (,) against two values: LiftA2 is traversable and provides better debugging
 --
 -- >>> pz @(FPair Fst Snd) (Just 10, Just True)
@@ -992,7 +1201,7 @@ -- >>> pz @((1 ... 10) >>= EmptyBool [] Even '[Id,Id]) ()
 -- Val [[2,2],[4,4],[6,6],[8,8],[10,10]]
 --
--- >>> pz @((1 ... 10) >>= If Even '[Id,Id] (EmptyT [])) ()
+-- >>> pz @((1 ... 10) >>= If Even '[Id,Id] (EmptyT [] _)) ()
 -- Val [2,2,4,4,6,6,8,8,10,10]
 --
 -- >>> pz @(Lookup 0 Id >>= Lookup 1 Id) [[1,2,3]]
@@ -1212,9 +1421,9 @@ --       `- False Id False
 -- Val [This 2,This 3,That False,These 5 True]
 --
--- >>> pl @(BiMap Succ Head) (EEmpty @Int @String)
--- Present EEmpty (BiMap <skipped>)
--- Val EEmpty
+-- >>> pl @(BiMap Succ Head) (ENone @Int @String)
+-- Present ENone (BiMap <skipped>)
+-- Val ENone
 --
 -- >>> pl @(BiMap Succ Head) (ELeft @Int @String 10)
 -- Present ELeft 11 (BiMap(L) Succ 11 | 10)
@@ -1228,7 +1437,7 @@ -- Present EBoth 11 'x' (BiMap(B) Succ 11 | 10 | Head 'x' | "xyz")
 -- Val (EBoth 11 'x')
 --
--- >>> pan @(FMap $ BiMap Succ Head) [EEmpty,ELeft 10,ERight "abc",EBoth 10 "xyz"]
+-- >>> pan @(FMap $ BiMap Succ Head) [ENone,ELeft 10,ERight "abc",EBoth 10 "xyz"]
 -- P FMap BiMap <skipped> | BiMap(L) Succ 11 | BiMap(R) Head 'a' | BiMap(B) Succ 11 | Head 'x'
 -- |
 -- +- P BiMap <skipped>
@@ -1246,7 +1455,7 @@ --    +- P Succ 11
 --    |
 --    `- P Head 'x'
--- Val [EEmpty,ELeft 11,ERight 'a',EBoth 11 'x']
+-- Val [ENone,ELeft 11,ERight 'a',EBoth 11 'x']
 --
 data BiMap p q deriving Show
 
@@ -1272,57 +1481,114 @@       -> n a b
       -> m (TT (n (PP p a) (PP q b)))
 _bimapImpl opts proxyp proxyq msg0 hhs nab = do
-        nttb <- bitraverse
-                  (fmap (\tt -> tt & ttString %~ litL opts
-                                   & ttForest .~ [hh tt]) . eval proxyp opts)
-                  (fmap (\tt -> tt & ttString %~ litL opts
-                                   & ttForest .~ [hh tt]) . eval proxyq opts)
-                  nab
-        let ttnb = bisequence nttb
-        pure $ case getValueLR Inline opts "" ttnb hhs of
-          Left e -> e
-          Right ret ->
---            let ind = case bifoldMap (\x -> ([x],[])) (\x -> ([],[x])) ret of
-            let ind = case bifoldMap ((,mempty) . pure) ((mempty,) . pure) ret of
-                        ([], []) -> " <skipped>"
-                        (_:_, []) -> "(L)"
-                        ([], _:_) -> "(R)"
-                        (_:_, _:_) -> "(B)"
-            in ttnb & ttVal .~ Val ret
-                    & ttForest %~ (hhs <>)
-                    & ttString %~ (msg0 <>) . (ind <>) . nullIf " "
+  nttb <- bitraverse
+            (fmap (\tt -> tt & ttString %~ litL opts
+                             & ttForest .~ [hh tt]) . eval proxyp opts)
+            (fmap (\tt -> tt & ttString %~ litL opts
+                             & ttForest .~ [hh tt]) . eval proxyq opts)
+            nab
+  let ttnb = bisequence nttb
+  pure $ case getValueLR Inline opts "" ttnb hhs of
+    Left e -> e
+    Right ret ->
+      let ind = getBifoldInfo ret
+      in ttnb & ttVal .~ Val ret
+              & ttForest %~ (hhs <>)
+              & ttString %~ (msg0 <>) . (ind <>) . nullIf " "
 
--- | adt for testing out possible outcomes of Bifoldable used in BiMap
-data ELR a b = EEmpty | ELeft !a | ERight !b | EBoth !a !b deriving (Show,Eq,Ord,Foldable,Functor,Traversable)
+-- | a version of 'Data.Bifoldable.bifoldMap'
+--
+-- >>> pl @(BiFoldMap Id Id) (Right [10..13])
+-- Present [10,11,12,13] (BiFoldMap(R) Id [10,11,12,13])
+-- Val [10,11,12,13]
+--
+-- >>> pl @(BiFoldMap Id Id) (Left [10..13])
+-- Present [10,11,12,13] (BiFoldMap(L) Id [10,11,12,13])
+-- Val [10,11,12,13]
+--
+-- >>> pl @(BiFoldMap Id Id) (SG.Arg [1..5] [10..13])
+-- Present [1,2,3,4,5,10,11,12,13] (BiFoldMap(B) Id [1,2,3,4,5] | Id [10,11,12,13])
+-- Val [1,2,3,4,5,10,11,12,13]
+--
+-- >>> pz @(BiFoldMap (Wrap (SG.Sum _) Id) (Wrap (SG.Sum _) Id)) (SG.Arg 1 4)
+-- Val (Sum {getSum = 5})
+--
+-- >>> pl @(BiFoldMap '( '[Id], '[]) '( '[], '[Id])) (SG.Arg "hap" "bcd")
+-- Present (["hap"],["bcd"]) (BiFoldMap(B) '(["hap"],[]) | '([],["bcd"]))
+-- Val (["hap"],["bcd"])
+--
+-- >>> pz @(BiFoldMap '( Wrap (SG.Sum _) Id, MEmptyT _) '( MEmptyT _, Id)) (SG.Arg 123 "xyz")
+-- Val (Sum {getSum = 123},"xyz")
+--
+-- >>> pl @(BiFoldMap '( Wrap (SG.Sum _) Id, MEmptyT _) '( MEmptyT _, Id)) (Left 123)
+-- Present (Sum {getSum = 123},()) (BiFoldMap(L) '(Sum {getSum = 123},()))
+-- Val (Sum {getSum = 123},())
+--
+-- >>> pz @(BiFoldMap (MEmptyT _) $ FoldMap (FoldMap (Wrap (SG.Sum _) Id))) (Right (Just [1..10]))
+-- Val (Sum {getSum = 55})
+--
+data BiFoldMap p q deriving Show
 
-instance Bifunctor ELR where
-  bimap f g x =
-    case x of
-      EEmpty -> EEmpty
-      ELeft a -> ELeft (f a)
-      ERight b -> ERight (g b)
-      EBoth a b -> EBoth (f a) (g b)
+instance ( Bitraversable n
+         , Monoid t
+         , PP p a ~ t
+         , PP q b ~ t
+         , P p a
+         , P q b
+         ) => P (BiFoldMap p q) (n a b) where
+  type PP (BiFoldMap p q) (n a b) = PP p a
+  eval _ opts nab = do
+    let msg0 = "BiFoldMap"
+    nttb <- bitraverse
+              (fmap (\tt -> tt & ttString %~ litL opts
+                               & ttForest .~ [hh tt]) . eval (Proxy @p) opts)
+              (fmap (\tt -> tt & ttString %~ litL opts
+                               & ttForest .~ [hh tt]) . eval (Proxy @q) opts)
+              nab
+    let ttnb = bisequence nttb
+    pure $ case getValueLR Inline opts "" ttnb [] of
+      Left e -> e
+      Right ret ->
+        let d = bifoldMap id id ret
+            ind = getBifoldInfo ret
+        in ttnb & ttVal .~ Val d
+                & ttString %~ (msg0 <>) . (ind <>) . nullIf " "
 
-instance Bifoldable ELR where
-  bifoldMap f g x =
-    case x of
-      EEmpty -> mempty
-      ELeft a -> f a
-      ERight b -> g b
-      EBoth a b -> f a <> g b
+-- | similar to 'Data.Coerce.coerce'
+--
+-- >>> pz @(Coerce (SG.Sum Integer)) (Identity (-13))
+-- Val (Sum {getSum = -13})
+--
+-- >>> pl @(Coerce SG.Any) True
+-- Present Any {getAny = True} (Coerce Any {getAny = True} | True)
+-- Val (Any {getAny = True})
+--
+-- >>> pl @(Coerce Bool) (SG.Any True)
+-- Present True (Coerce True | Any {getAny = True})
+-- Val True
+--
+-- >>> pz @(Proxy 'True >> Coerce (Proxy 'False)) () ^!? acts . _Val . to typeRep
+-- Just 'False
+--
+-- >>> pz @(Proxy Int >> Coerce (Proxy (String,Char))) () ^!? acts . _Val . to typeRep
+-- Just ([Char],Char)
+--
+-- >>> import qualified GHC.Exts as GE
+-- >>> pz @(Proxy GE.Any >> Coerce (Proxy Int)) () ^!? acts . _Val . to typeRep
+-- Just Int
+--
+-- >>> pz @(Proxy '(_,_) >> Coerce (Proxy '(Float,Int))) () ^!? acts . _Val . to typeRep
+-- Just ('(,) * * Float Int)
+--
+data Coerce (t :: Type) deriving Show
 
-instance Bitraversable ELR where
-  bitraverse f g x =
-    case x of
-      EEmpty -> pure EEmpty
-      ELeft a -> ELeft <$> f a
-      ERight b -> ERight <$> g b
-      EBoth a b -> EBoth <$> f a <*> g b
+instance ( Coercible t a
+         , Show a
+         , Show t
+         ) => P (Coerce t) a where
+  type PP (Coerce t) a = t
+  eval _ opts a =
+    let msg0 = "Coerce"
+        d = a ^. coerced
+    in pure $ mkNode opts (Val d) (show3 opts msg0 d a) []
 
-instance SwapC ELR where
-  swapC =
-    \case
-      EEmpty -> EEmpty
-      ELeft a -> ERight a
-      ERight b -> ELeft b
-      EBoth a b -> EBoth b a

@@ -25,9 +25,6 @@   , type (+:)
   , type (++)
   , Singleton
-  , EmptyT
-  , EmptyList
-  , EmptyList'
 
  -- ** destructors
   , Uncons
@@ -98,7 +95,6 @@   , IsPrefix
   , IsInfix
   , IsSuffix
-
  ) where
 import Predicate.Core
 import Predicate.Misc
@@ -111,13 +107,12 @@ import Data.List (foldl', partition, intercalate, inits, tails, unfoldr, sortOn)
 import Data.Proxy (Proxy(Proxy))
 import Control.Monad (zipWithM)
-import Data.Kind (Type)
 import Data.Foldable (toList)
 import Control.Arrow (Arrow((***), (&&&)))
 import qualified Data.Sequence as Seq
 import Data.Bool (bool)
 import qualified Data.Map.Strict as M
-import Control.Applicative (Alternative(empty), liftA2)
+import Control.Applicative (liftA2)
 import Data.Containers.ListUtils (nubOrd)
 import qualified Data.List.NonEmpty as NE
 -- $setup
@@ -127,6 +122,7 @@ -- >>> :set -XOverloadedStrings
 -- >>> :set -XNoOverloadedLists
 -- >>> import qualified Data.Map.Strict as M
+-- >>> import qualified Data.Semigroup as SG
 -- >>> import qualified Data.Text as T
 -- >>> import Data.These
 -- >>> import Predicate.Prelude
@@ -226,7 +222,7 @@ -- >>> pz @(Fst +: Snd) ([],5)
 -- Val [5]
 --
--- >>> pz @(EmptyT [] +: 5) 5
+-- >>> pz @(EmptyT [] _ +: 5) 5
 -- Val [5]
 --
 -- >>> pl @('[1,2,3] +: 4) ()
@@ -411,10 +407,10 @@     qq <- eval (Proxy @q) opts a'
     case getValueLR NoInline opts msg0 qq [] of
       Left e -> pure e
-      Right q ->
-        case chkSize opts msg0 q [hh qq] of
+      Right q' ->
+        case chkSize opts msg0 q' [hh qq] of
           Left e -> pure e
-          Right _ -> do
+          Right (_,q) -> do
              ts <- zipWithM (\i a -> ((i, a),) <$> evalBoolHide @p opts a) [0::Int ..] q
              pure $ case splitAndAlign opts msg0 ts of
                Left e -> e
@@ -509,10 +505,10 @@     qq <- eval (Proxy @q) opts a'
     case getValueLR NoInline opts msg0 qq [] of
       Left e -> pure e
-      Right q ->
-        case chkSize opts msg0 q [hh qq] of
+      Right q' ->
+        case chkSize opts msg0 q' [hh qq] of
           Left e -> pure e
-          Right _ -> do
+          Right (_,q) -> do
              ts <- zipWithM (\i a -> ((i, a),) <$> evalHide @p opts a) [0::Int ..] q
              pure $ case splitAndAlign opts msg0 ts of
                    Left e -> e
@@ -584,6 +580,9 @@ -- `- False i=14: 'y' == 'e'
 -- Val ["h","e","ll","o","    ","g","oo","d","b","y","e"]
 --
+-- >>> pz @(GroupBy (Fst == Snd)  Id) (map (uncurry SG.Arg) [(10,0),(9,4),(9,3),(1,1),(9,6)])
+-- Val [[Arg 10 0],[Arg 9 4,Arg 9 3],[Arg 1 1],[Arg 9 6]]
+--
 data GroupBy p q deriving Show
 
 instance ( Show x
@@ -598,10 +597,10 @@     qq <- eval (Proxy @q) opts a'
     case getValueLR NoInline opts msg0 qq [] of
       Left e -> pure e
-      Right q ->
-        case chkSize opts msg0 q [hh qq] of
+      Right q' ->
+        case chkSize opts msg0 q' [hh qq] of
           Left e -> pure e
-          Right _ ->
+          Right (_,q) ->
              case q of
                [] -> pure $ mkNode opts (Val []) (show3' opts msg0 q "s=" q) [hh qq]
                [_] -> let ret = [q]
@@ -721,7 +720,7 @@ -- Val ([1,2],[3,4,5,6,7,8])
 --
 -- >>> pl @(Break (If (Gt 2) (FailT _ "ASfd") 'False) Id) [1..8]
--- Error ASfd (If True | Break predicate failed)
+-- Error ASfd (If 'True | Break predicate failed)
 -- Fail "ASfd"
 --
 -- >>> pl @(Break Snd Id) (zip [1..] [False,False,False,True,True,False])
@@ -750,10 +749,10 @@     qq <- eval (Proxy @q) opts a'
     case getValueLR NoInline opts msg0 qq [] of
       Left e -> pure e
-      Right q ->
-        case chkSize opts msg0 q [hh qq] of
+      Right q' ->
+        case chkSize opts msg0 q' [hh qq] of
           Left e -> pure e
-          Right _ -> do
+          Right (_,q) -> do
             let ff [] zs = pure (zs, [], Nothing) -- [(ia,qq)] extras | the rest of the data | optional last pivot or failure
                 ff ((i,a):ias) zs = do
                    pp <- evalBoolHide @p opts a
@@ -824,11 +823,11 @@     lr <- runPQ NoInline msg0 (Proxy @p) (Proxy @q) opts x []
     pure $ case lr of
       Left e -> e
-      Right (p,q,pp,qq) ->
+      Right (p',q',pp,qq) ->
         let hhs = [hh pp, hh qq]
-        in case chkSize2 opts msg0 p q hhs of
+        in case chkSize2 opts msg0 p' q' hhs of
           Left e -> e
-          Right _ ->
+          Right ((_,p),(_,q)) ->
             let d = intercalate p (map pure q)
             in mkNode opts (Val d) (show3 opts msg0 d p <> showVerbose opts " | " q) hhs
 
@@ -932,11 +931,11 @@ 
 instance x ~ [a] => P Ones x where
   type PP Ones x = [x]
-  eval _ opts x =
+  eval _ opts x' =
     let msg0 = "Ones"
-    in pure $ case chkSize opts msg0 x [] of
+    in pure $ case chkSize opts msg0 x' [] of
           Left e -> e
-          Right _ ->
+          Right (_,x) ->
             let d = map pure x
             in mkNode opts (Val d) msg0 []
 
@@ -963,13 +962,15 @@         qq <- eval (Proxy @q) opts a
         pure $ case getValueLR NoInline opts (msg1 <> " q failed") qq hhs of
           Left e -> e
-          Right q ->
-            let l = length q
-                diff = if n<=l then 0 else n-l
-                bs = if lft
-                     then replicate diff p <> q
-                     else q <> replicate diff p
-            in mkNode opts (Val bs) (show3 opts msg1 bs q) (hhs <> [hh qq])
+          Right q' ->
+            case chkSize opts msg0 q' [] of
+              Left e -> e
+              Right (qLen,q) ->
+                let diff = if n<=qLen then 0 else n-qLen
+                    bs = if lft
+                         then replicate diff p <> q
+                         else q <> replicate diff p
+                in mkNode opts (Val bs) (show3 opts msg1 bs q) (hhs <> [hh qq])
 
 -- | left pad @q@ with @n@ values from @p@
 --
@@ -1053,11 +1054,15 @@     lr <- runPQ NoInline msg0 (Proxy @ns) (Proxy @p) opts x []
     pure $ case lr of
       Left e -> e
-      Right (ns,p,nn,pp) ->
-        let zs = foldr (\n k s -> let (a,b) = splitAtNeg (fromIntegral n) s
-                                  in a:k b
-                       ) (\as -> [as | not (null as)]) ns p
-        in mkNode opts (Val zs) (show3' opts msg0 zs "ns=" ns <> showVerbose opts " | " p) [hh nn, hh pp]
+      Right (ns,p',nn,pp) ->
+        let hhs = [hh nn, hh pp]
+        in case chkSize opts msg0 p' hhs of
+             Left e -> e
+             Right (pLen,p) ->
+               let zs = foldr (\n k s -> let (a,b) = splitAtNeg pLen (fromIntegral n) s
+                                         in a:k b
+                              ) (\as -> [as | not (null as)]) ns p
+               in mkNode opts (Val zs) (show3' opts msg0 zs "ns=" ns <> showVerbose opts " | " p) hhs
 
 -- | similar to 'Data.List.splitAt'
 --
@@ -1094,13 +1099,18 @@     lr <- runPQ NoInline msg0 (Proxy @n) (Proxy @p) opts a []
     pure $ case lr of
       Left e -> e -- (Left e, tt')
-      Right (fromIntegral -> n,p,pp,qq) ->
-        let msg1 = msg0 <> " " <> showL opts n <> " " <> showL opts p
-            ret = splitAtNeg n p
-       in mkNode opts (Val ret) (show3' opts msg1 ret "n=" n <> showVerbose opts " | " p) [hh pp, hh qq]
+      Right (fromIntegral -> n,p',nn,pp) ->
+        let hhs = [hh nn, hh pp]
+        in case chkSize opts msg0 p' hhs of
+             Left e -> e
+             Right (pLen,p) ->
+               let msg1 = msg0 <> " " <> showL opts n <> " " <> showL opts p
+                   ret = splitAtNeg pLen n p
+               in mkNode opts (Val ret) (show3' opts msg1 ret "n=" n <> showVerbose opts " | " p) hhs
 
-splitAtNeg :: Int -> [a] -> ([a], [a])
-splitAtNeg n as = splitAt (if n<0 then length as + n else n) as
+splitAtNeg :: Int -> Int -> [a] -> ([a], [a])
+--splitAtNeg len n = splitAt (if n<0 then len + n else n)
+splitAtNeg len = splitAt . ifM (<0) (len+) id
 
 -- | take @n@ values from a list @p@: similar to 'Prelude.take'
 --
@@ -1196,7 +1206,7 @@             in if n <= 0 then mkNode opts (Fail (msg0 <> " n<=0")) "" hhs1
                else if i < 1 then mkNode opts (Fail (msg0 <> " i<1")) "" hhs1
                else let ret = unfoldr (\s -> if null s then Nothing else Just (take n s,drop i s)) p
-                in mkNode opts (Val ret) (show3' opts msg1 ret "n,i=" (n,i) <> showVerbose opts " | " p) hhs1
+                    in mkNode opts (Val ret) (show3' opts msg1 ret "n,i=" (n,i) <> showVerbose opts " | " p) hhs1
 
 -- empty lists at the type level wont work here
 
@@ -1471,11 +1481,11 @@                             Right rr ->
                               pure $  mkNode opts (Val (ll ++ w : rr))
                                      (msg0 <> " lhs=" <> showL opts ll <> " pivot " <> showL opts w <> " rhs=" <> showL opts rr)
-                                     (hh pp : [hh lhs | length ll > 1] ++ [hh rhs | length rr > 1])
+                                     (hh pp : [hh lhs | lengthGreaterThanOne ll] ++ [hh rhs | lengthGreaterThanOne rr])
         ret <- ff as
         pure $ case getValueLR NoInline opts msg0 ret [hh qq] of
           Left _e -> ret -- dont rewrap else will double up messages: already handled
-          Right xs -> mkNodeCopy opts ret (msg0 <> " " <> showL opts xs) [hh qq, hh ret]
+          Right xs -> mkNodeCopy opts ret (msg0 <> " " <> showL opts xs) [hh qq]
 
 -- | similar to 'Data.List.sortOn'
 --
@@ -1610,27 +1620,6 @@       Left e -> e
       Right p -> mkNode opts (Val [p]) msg0 [hh pp]
 
--- | creates an empty list for the given pointer to a type @t@
-data EmptyList' t deriving Show
-
-instance P (EmptyList' t) x where
-  type PP (EmptyList' t) x = [PP t x]
-  eval _ opts _ =
-    pure $ mkNode opts (Val []) "EmptyList" []
-
--- | creates an empty list for the given type
---
--- >>> pz @(Id :+ EmptyList _) 99
--- Val [99]
---
-data EmptyList (t :: Type) deriving Show
-type EmptyListT (t :: Type) = EmptyList' (Hole t)
-
-instance P (EmptyList t) x where
-  type PP (EmptyList t) x = PP (EmptyListT t) x
-  eval _ = eval (Proxy @(EmptyListT t))
-
-
 -- | like 'zipWith'
 --
 -- >>> pz @(ZipWith Id (1...5) (C "a" ... C "e")) ()
@@ -1665,13 +1654,12 @@     lr <- runPQ NoInline msg0 (Proxy @q) (Proxy @r) opts a []
     case lr of
       Left e -> pure e
-      Right (q,r,qq,rr) ->
+      Right (q',r',qq,rr) ->
         let hhs = [hh qq, hh rr]
-        in case chkSize2 opts msg0 q r hhs of
+        in case chkSize2 opts msg0 q' r' hhs of
           Left e -> pure e
-          Right _ -> do
-            let lls = (length q, length r)
-            if uncurry (==) lls then do
+          Right ((qLen,q),(rLen,r)) -> do
+            if qLen == rLen then do
                ts <- zipWithM (\i (x,y) -> ((i, (x,y)),) <$> evalHide @p opts (x,y)) [0::Int ..] (zip q r)
                pure $ case splitAndAlign opts msg0 ts of
                  Left e -> e
@@ -1682,7 +1670,7 @@                    in mkNode opts (Val ret) (show3' opts msg0 ret "s=" q ) (hh qq : map (hh . prefixNumberToTT) itts)
 
              else do
-                   let msg1 = msg0 ++ show lls
+                   let msg1 = msg0 ++ show (qLen,rLen)
                    pure $ mkNode opts (Fail (msg1 <> " length mismatch")) (showVerbose opts "q=" q <> showVerbose opts " | r=" r) hhs
 
 -- | Zip two lists to their maximum length using optional padding
@@ -1721,12 +1709,12 @@     lr <- runPQ NoInline msg0 (Proxy @p) (Proxy @q) opts a []
     case lr of
       Left e -> pure e
-      Right (p,q,pp,qq) -> do
+      Right (p',q',pp,qq) -> do
         let hhs = [hh pp, hh qq]
-        case chkSize2 opts msg0 p q hhs of
+        case chkSize2 opts msg0 p' q' hhs of
           Left e -> pure e
-          Right _ ->
-            case compare (length p) (length q) of
+          Right ((pLen,p),(qLen,q)) -> do
+            case compare pLen qLen of
               LT -> do
                 ll <- eval (Proxy @l) opts a
                 pure $ case getValueLR NoInline opts (msg0 <> " l failed") ll hhs of
@@ -1772,7 +1760,7 @@ -- Present [(1 % 1,'a'),(2 % 1,'b'),(3 % 1,'c'),(99 % 4,'d'),(99 % 4,'e')] (ZipL [(1 % 1,'a'),(2 % 1,'b'),(3 % 1,'c'),(99 % 4,'d'),(99 % 4,'e')] | p=[1 % 1,2 % 1,3 % 1] | q="abcde")
 -- Val [(1 % 1,'a'),(2 % 1,'b'),(3 % 1,'c'),(99 % 4,'d'),(99 % 4,'e')]
 --
--- >>> pl @(ZipL "X" (EmptyT _) Id) "abcd"
+-- >>> pl @(ZipL "X" (EmptyT _ _) Id) "abcd"
 -- Present [("X",'a'),("X",'b'),("X",'c'),("X",'d')] (ZipL [("X",'a'),("X",'b'),("X",'c'),("X",'d')] | p=[] | q="abcd")
 -- Val [("X",'a'),("X",'b'),("X",'c'),("X",'d')]
 --
@@ -1793,14 +1781,13 @@     lr <- runPQ NoInline msg0 (Proxy @p) (Proxy @q) opts a []
     case lr of
       Left e -> pure e
-      Right (p,q,pp,qq) -> do
+      Right (p',q',pp,qq) -> do
         let hhs = [hh pp, hh qq]
-        case chkSize2 opts msg0 p q hhs of
+        case chkSize2 opts msg0 p' q' hhs of
           Left e -> pure e
-          Right _ -> do
-            let lls = (length p,length q)
-            case uncurry compare lls of
-              GT -> let msg1 = msg0 ++ show lls
+          Right ((pLen,p),(qLen,q)) -> do
+            case compare pLen qLen of
+              GT -> let msg1 = msg0 ++ show (pLen,qLen)
                     in pure $ mkNode opts (Fail (msg1 ++ " rhs would be truncated")) (showVerbose opts "p=" p <> showVerbose opts " | q=" q) hhs
               _ -> do
                      ll <- eval (Proxy @l) opts a
@@ -1828,7 +1815,7 @@ -- Error ZipR(2,3) rhs would be truncated (p=[1,2] | q="abc")
 -- Fail "ZipR(2,3) rhs would be truncated"
 --
--- >>> pl @(ZipR (C "Y") (EmptyT _) Id) "abcd"
+-- >>> pl @(ZipR (C "Y") (EmptyT _ _) Id) "abcd"
 -- Error ZipR(0,4) rhs would be truncated (p=[] | q="abcd")
 -- Fail "ZipR(0,4) rhs would be truncated"
 --
@@ -1848,14 +1835,13 @@     lr <- runPQ NoInline msg0 (Proxy @p) (Proxy @q) opts a []
     case lr of
       Left e -> pure e
-      Right (p,q,pp,qq) -> do
+      Right (p',q',pp,qq) -> do
         let hhs = [hh pp, hh qq]
-        case chkSize2 opts msg0 p q hhs of
+        case chkSize2 opts msg0 p' q' hhs of
           Left e -> pure e
-          Right _ -> do
-            let lls = (length p,length q)
-            case uncurry compare lls of
-              LT -> let msg1 = msg0 ++ show lls
+          Right ((pLen,p),(qLen,q)) -> do
+            case compare pLen qLen of
+              LT -> let msg1 = msg0 ++ show (pLen,qLen)
                     in pure $ mkNode opts (Fail (msg1 ++ " rhs would be truncated")) (showVerbose opts "p=" p <> showVerbose opts " | q=" q) hhs
               _ -> do
                      rr <- eval (Proxy @r) opts a
@@ -1897,42 +1883,17 @@     lr <- runPQ NoInline msg0 (Proxy @p) (Proxy @q) opts a []
     pure $ case lr of
       Left e -> e
-      Right (p,q,pp,qq) ->
+      Right (p',q',pp,qq) ->
         let hhs = [hh pp, hh qq]
-        in case chkSize2 opts msg0 p q hhs of
+        in case chkSize2 opts msg0 p' q' hhs of
           Left e -> e
-          Right _ ->
-            let lls = (length p, length q)
-            in case uncurry compare lls of
+          Right ((pLen,p),(qLen,q)) -> do
+            case compare pLen qLen of
                  EQ -> let d = zip p q
                        in mkNode opts (Val d) (show3' opts msg0 d "p=" p <> showVerbose opts " | q=" q) hhs
-                 _ -> let msg1 = msg0 ++ show lls
+                 _ -> let msg1 = msg0 ++ show (pLen,qLen)
                       in mkNode opts (Fail (msg1 <> " length mismatch")) (showVerbose opts "p=" p <> showVerbose opts " | q=" q) hhs
 
--- | similar to 'Data.List.empty'
---
--- >>> pz @(EmptyT Maybe) ()
--- Val Nothing
---
--- >>> pz @(EmptyT []) ()
--- Val []
---
--- >>> pz @(C "x" >> EmptyT []) (13,True)
--- Val ""
---
--- >>> pz @(Fst >> EmptyT (Either String)) (13,True)
--- Val (Left "")
---
-data EmptyT (t :: Type -> Type) deriving Show
-
-instance Alternative t => P (EmptyT t) x where
-  type PP (EmptyT t) x = t x
-  eval _ opts _ =
-    let msg0 = "EmptyT"
-        b = empty @t
-    in pure $ mkNode opts (Val b) msg0 []
-
-
 -- | similar to 'Data.List.sum'
 --
 -- >>> pz @Sum [10,4,5,12,3,4]
@@ -2039,9 +2000,13 @@     lr <- runPQ NoInline msg0 (Proxy @p) (Proxy @q) opts x []
     pure $ case lr of
       Left e -> e
-      Right (p,q,pp,qq) ->
-        let msg1 = msg0 <> " | " <> showL opts p
-        in mkNodeB opts (ff p q) (msg1 <> " " <> showL opts q) [hh pp, hh qq]
+      Right (p',q',pp,qq) ->
+        let hhs = [hh pp, hh qq]
+        in case chkSize2 opts msg0 p' q' hhs of
+          Left e -> e
+          Right ((_,p),(_,q)) ->
+            let msg1 = joinStrings msg0 (showL opts p)
+            in mkNodeB opts (ff p q) (msg1 <> " " <> showL opts q) hhs
 
 -- | similar to 'Data.List.isPrefixOf'
 --
@@ -2140,11 +2105,11 @@     lr <- runPQ NoInline msg0 (Proxy @p) (Proxy @q) opts x []
     pure $ case lr of
       Left e -> e
-      Right (p,q,pp,qq) ->
+      Right (p',q',pp,qq) ->
         let hhs = [hh pp, hh qq]
-        in case chkSize2 opts msg0 p q hhs of
+        in case chkSize2 opts msg0 p' q' hhs of
           Left e -> e
-          Right _ ->
+          Right ((_,p),(_,q)) ->
             let d = liftA2 (,) p q
             in mkNode opts (Val d) (show3' opts msg0 d "p=" p <> showVerbose opts " | q=" q) hhs
 
@@ -2171,6 +2136,9 @@ --
 -- >>> pz @(PartitionsBy (L11 ==! L21) (L11 < L21) Id) [10,9,9,1,9,4]
 -- Val [[9],[1,4,9],[9,10]]
+--
+-- >>> pz @(PartitionsBy (Fst ==! Snd) (L11 == L21) Id) (map (uncurry SG.Arg) [(10,0),(9,4),(9,3),(1,1),(9,6)])
+-- Val [[Arg 10 0],[Arg 9 4,Arg 9 3,Arg 9 6],[Arg 1 1]]
 --
 data PartitionsBy p q r deriving Show
 type PartitionsByT p q r = SortBy p (Zip r (0 ... (Length r - 1))) >> GroupBy q Id >> SortOn (Head >> Snd) Id >> Map (Map Fst)

@@ -32,20 +32,24 @@   , JustFail
   , MapMaybe
   , CatMaybes
-  , MaybeIn
   , MaybeBool
-  , EmptyBool
+  , MaybeIn
+  , MaybeId
 
+ -- ** type families
+  , MaybeInT
  ) where
 import Predicate.Core
 import Predicate.Misc
 import Predicate.Util
 import Predicate.Data.Foldable (ConcatMap)
 import Predicate.Data.Monoid (MEmptyP)
+import Predicate.Data.Lifted (EmptyBool)
 import Data.Proxy (Proxy(..))
 import Data.Kind (Type)
 import Data.Maybe (isJust, isNothing)
-import Control.Applicative (Alternative(empty))
+import GHC.TypeLits (ErrorMessage((:$$:),(:<>:)))
+import qualified GHC.TypeLits as GL
 
 -- $setup
 -- >>> :set -XDataKinds
@@ -112,158 +116,6 @@         let d = Just p
         in mkNode opts (Val d) (msg0 <> " Just " <> showL opts p) [hh pp]
 
--- | similar to 'Data.Maybe.maybe'
---
--- provides a Proxy to the result of @q@ but does not provide the surrounding context
---
--- >>> pz @(MaybeIn "foundnothing" (ShowP Pred)) (Just 20)
--- Val "19"
---
--- >>> pz @(MaybeIn "found nothing" (ShowP Pred)) Nothing
--- Val "found nothing"
---
--- >>> pl @(MaybeIn 'True Id) (Nothing @Bool) -- need @() else breaks
--- True (MaybeIn(Nothing) True | Proxy)
--- Val True
---
--- >>> pl @(MaybeIn (FailT _ "failed4") Id) (Just 10)
--- Present 10 (MaybeIn(Just) 10 | 10)
--- Val 10
---
--- >>> pl @(MaybeIn 'False Id) (Nothing @Bool) -- breaks otherwise
--- False (MaybeIn(Nothing) False | Proxy)
--- Val False
---
--- >>> pl @(MaybeIn MEmptyP Id) (Just [1,2,3])
--- Present [1,2,3] (MaybeIn(Just) [1,2,3] | [1,2,3])
--- Val [1,2,3]
---
--- >>> pl @(MaybeIn MEmptyP Id) (Nothing @[Int])
--- Present [] (MaybeIn(Nothing) [] | Proxy)
--- Val []
---
--- >>> pl @(MaybeIn (FailP "err") Succ) (Just 116)
--- Present 117 (MaybeIn(Just) 117 | 116)
--- Val 117
---
--- >>> pl @(MaybeIn 99 Succ) (Nothing @Int)
--- Present 99 (MaybeIn(Nothing) 99 | Proxy)
--- Val 99
---
--- >>> pl @(MaybeIn (FailP "someval") Succ) (Nothing @())
--- Error someval (MaybeIn(Nothing))
--- Fail "someval"
---
--- >>> pl @(MaybeIn 'True 'False) (Nothing @())
--- True (MaybeIn(Nothing) True | Proxy)
--- Val True
---
--- >>> pl @(MaybeIn 'True 'False) (Just "aa")
--- False (MaybeIn(Just) False | "aa")
--- Val False
---
--- >>> pl @(MaybeIn MEmptyP (Fst ==! Snd)) (Just ('x','z'))
--- Present LT (MaybeIn(Just) LT | ('x','z'))
--- Val LT
---
--- >>> pl @(MaybeIn MEmptyP (Fst ==! Snd)) (Nothing @(Char,Char))
--- Present EQ (MaybeIn(Nothing) EQ | Proxy)
--- Val EQ
---
--- >>> pl @(MaybeIn (FailP "failed20") 'False) (Nothing @Int)
--- Error failed20 (MaybeIn(Nothing))
--- Fail "failed20"
---
--- >>> pl @(MaybeIn ('False >> FailS "failed21") 'False) (Nothing @Double)
--- Error failed21 (False | MaybeIn(Nothing))
--- Fail "failed21"
---
--- >>> pl @(MaybeIn (FailP "err") Id) (Nothing @Int)
--- Error err (MaybeIn(Nothing))
--- Fail "err"
---
--- >>> pl @(MaybeIn (FailP "err") Id) (Nothing @())
--- Error err (MaybeIn(Nothing))
--- Fail "err"
---
--- >>> pl @(MaybeIn MEmptyP Id) (Just (M.fromList [(1,'a')]))
--- Present fromList [(1,'a')] (MaybeIn(Just) fromList [(1,'a')] | fromList [(1,'a')])
--- Val (fromList [(1,'a')])
---
--- >>> pl @(MaybeIn MEmptyP Id) (Nothing @(M.Map () ()))
--- Present fromList [] (MaybeIn(Nothing) fromList [] | Proxy)
--- Val (fromList [])
---
--- >>> pl @(MaybeIn MEmptyP Ones) (Just @String "abc")
--- Present ["a","b","c"] (MaybeIn(Just) ["a","b","c"] | "abc")
--- Val ["a","b","c"]
---
--- >>> pl @(MaybeIn 99 Id) (Just 12)
--- Present 12 (MaybeIn(Just) 12 | 12)
--- Val 12
---
--- >>> pl @(MaybeIn 99 Id) Nothing
--- Present 99 (MaybeIn(Nothing) 99 | Proxy)
--- Val 99
---
--- >>> pl @(MaybeIn (99 -% 1) Id) Nothing
--- Present (-99) % 1 (MaybeIn(Nothing) (-99) % 1 | Proxy)
--- Val ((-99) % 1)
---
--- >>> pl @(MaybeIn 123 Id) (Nothing @Int)
--- Present 123 (MaybeIn(Nothing) 123 | Proxy)
--- Val 123
---
--- >>> pl @(MaybeIn 123 Id) (Just 9)
--- Present 9 (MaybeIn(Just) 9 | 9)
--- Val 9
---
--- >>> pl @(Uncons >> MaybeIn '(1,MEmptyT _) Id) []
--- Present (1,[]) ((>>) (1,[]) | {MaybeIn(Nothing) (1,[]) | Proxy})
--- Val (1,[])
---
--- >>> pl @(MaybeIn MEmptyP (ShowP Id >> Ones)) (Just 123)
--- Present ["1","2","3"] (MaybeIn(Just) ["1","2","3"] | 123)
--- Val ["1","2","3"]
---
--- >>> pl @(MaybeIn MEmptyP (ShowP Id >> Ones)) (Nothing @String)
--- Present [] (MaybeIn(Nothing) [] | Proxy)
--- Val []
---
--- >>> pl @(MaybeIn MEmptyP Ones) (Just @String "ab")
--- Present ["a","b"] (MaybeIn(Just) ["a","b"] | "ab")
--- Val ["a","b"]
---
--- >>> pl @(MaybeIn MEmptyP Ones) (Nothing @String)
--- Present [] (MaybeIn(Nothing) [] | Proxy)
--- Val []
---
-data MaybeIn p q deriving Show
-
--- tricky: the nothing case is the proxy of PP q a: ie proxy of the final result
-instance ( P q a
-         , Show a
-         , Show (PP q a)
-         , PP p (Proxy (PP q a)) ~ PP q a
-         , P p (Proxy (PP q a))
-         ) => P (MaybeIn p q) (Maybe a) where
-  type PP (MaybeIn p q) (Maybe a) = PP q a
-  eval _ opts ma = do
-    let msg0 = "MaybeIn"
-    case ma of
-      Nothing -> do
-        let msg1 = msg0 <> "(Nothing)"
-        pp <- eval (Proxy @p) opts (Proxy @(PP q a))
-        pure $ case getValueLR NoInline opts msg1 pp [] of
-          Left e -> e
-          Right b -> mkNodeCopy opts pp (msg1 <> " " <> showL opts b <> " | Proxy") [hh pp]
-      Just a -> do
-        let msg1 = msg0 <> "(Just)"
-        qq <- eval (Proxy @q) opts a
-        pure $ case getValueLR NoInline opts msg1 qq [] of
-          Left e -> e
-          Right b -> mkNodeCopy opts qq (show3 opts msg1 b a) [hh qq]
-
 -- | similar to 'Data.Maybe.isJust'
 --
 -- >>> pz @IsJust Nothing
@@ -313,7 +165,7 @@ -- Val [4,5]
 --
 data MapMaybe p q deriving Show
-type MapMaybeT p q = ConcatMap (p >> MaybeIn MEmptyP '[Id]) q
+type MapMaybeT p q = ConcatMap (p >> MaybeId MEmptyP '[Id]) q
 
 instance P (MapMaybeT p q) x => P (MapMaybe p q) x where
   type PP (MapMaybe p q) x = PP (MapMaybeT p q) x
@@ -344,11 +196,6 @@ -- >>> pz @(MaybeBool 'True 10) ()
 -- Val (Just 10)
 --
-
---    pu @(If 'True (MkJust 10) (EmptyT Maybe)) ()  -- doesnt work
---    <interactive>:211:1: error:
---       * Couldn't match type 'Int' with '()' arising from a use of 'pu'
-
 data MaybeBool b p deriving Show
 
 type MaybeBoolT b p = EmptyBool Maybe b p
@@ -357,38 +204,19 @@   type PP (MaybeBool b p) x = PP (MaybeBoolT b p) x
   eval _ = eval (Proxy @(MaybeBoolT b p))
 
--- | Convenient method to convert a value @p@ to an Alternative based on a predicate @b@
---
---   if @b@ is True then pure @p@ else empty
+-- | extract the value from a 'Maybe' otherwise use the default value: similar to 'Data.Maybe.fromMaybe'
 --
--- >>> pz @(EmptyBool [] (Id > 4) 'True) 24
--- Val [True]
+-- >>> pl @(JustDef 'True Id) Nothing -- preserves TrueP/FalseP in the default case
+-- True (JustDef Nothing)
+-- Val True
 --
--- >>> pz @(EmptyBool [] (Id > 4) 'True) 1
--- Val []
+-- >>> pl @(JustDef (Fst > 12) Snd) (3,Just False) -- ValP for normal case
+-- Present False (JustDef Just)
+-- Val False
 --
-data EmptyBool t b p deriving Show
-
-instance ( Show (PP p a)
-         , P b a
-         , P p a
-         , PP b a ~ Bool
-         , Alternative t
-         ) => P (EmptyBool t b p) a where
-  type PP (EmptyBool t b p) a = t (PP p a)
-  eval _ opts z = do
-    let msg0 = "EmptyBool"
-    bb <- evalBool (Proxy @b) opts z
-    case getValueLR NoInline opts (msg0 <> " b failed") bb [] of
-      Left e -> pure e
-      Right True -> do
-        pp <- eval (Proxy @p) opts z
-        pure $ case getValueLR NoInline opts (msg0 <> " p failed") pp [hh bb] of
-          Left e -> e
-          Right p -> mkNode opts (Val (pure p)) (msg0 <> "(False) Just " <> showL opts p) [hh bb, hh pp]
-      Right False -> pure $ mkNode opts (Val empty) (msg0 <> "(True)") [hh bb]
-
--- | extract the value from a 'Maybe' otherwise use the default value: similar to 'Data.Maybe.fromMaybe'
+-- >>> pl @(JustDef Fst Snd) (True,Nothing)
+-- Present True (JustDef Nothing)
+-- Val True
 --
 -- >>> pz @(JustDef (1 % 4) Id) (Just 20.4)
 -- Val (102 % 5)
@@ -454,7 +282,7 @@             pp <- eval (Proxy @p) opts x
             pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
               Left e -> e
-              Right b -> mkNode opts (Val b) (msg0 <> " Nothing") [hh qq, hh pp]
+              Right _ -> mkNodeCopy opts pp (msg0 <> " Nothing") [hh qq]
 
 
 -- | extract the value from a 'Maybe' or fail with the given message
@@ -493,3 +321,134 @@             pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
               Left e -> e
               Right p -> mkNode opts (Fail p) (msg0 <> " Nothing") [hh qq, hh pp]
+
+-- | destructs an Maybe value
+--   @n@ @Nothing@ receives @(PP s x,Proxy result)@ (you can use the proxy with MEmptyP)
+--   @p@ @Just a@ receives @(PP s x,a)@
+--   @s@ points to the environment you want to pass in
+--   @t@ points to the Maybe value
+--
+-- >>> pz @(MaybeIn Fst Snd Fst Snd) ('a', Just 'x')
+-- Val 'x'
+--
+-- >>> pz @(MaybeIn Fst Snd Fst Snd) ('a', Nothing)
+-- Val 'a'
+--
+-- >>> pl @(MaybeIn "none" "just"() Id) (Just (SG.Sum 12))
+-- Present "just" (MaybeIn(Just) "just" | Sum {getSum = 12})
+-- Val "just"
+--
+-- >>> pl @(MaybeIn (Snd >> FailP "oops") Snd Fst Snd) ("abc", Nothing)
+-- Error oops (Proxy | MaybeIn(Nothing) n failed)
+-- Fail "oops"
+--
+-- >>> pl @(MaybeIn (Snd >> MEmptyP) Snd Fst Snd) ("abc", Nothing)
+-- Present () (MaybeIn(Nothing) () | ())
+-- Val ()
+--
+data MaybeIn n p s t deriving Show
+
+instance ( Show a
+         , Show (PP p (y,a))
+         , P n (y,Proxy z)
+         , P p (y,a)
+         , PP n (y,Proxy z) ~ PP p (y,a)
+         , z ~ PP p (y,a)
+         , P s x
+         , P t x
+         , PP t x ~ Maybe a
+         , PP s x ~ y
+         )  => P (MaybeIn n p s t) x where
+  type PP (MaybeIn n p s t) x = MaybeInT p (PP s x) (PP t x)
+  eval _ opts x = do
+    let msg0 = "MaybeIn"
+    lr <- runPQ NoInline msg0 (Proxy @s) (Proxy @t) opts x []
+    case lr of
+      Left e -> pure e
+      Right (s,t,ss,tt) -> do
+         let hhs = [hh ss, hh tt]
+         case t of
+            Nothing -> do
+              let msg1 = msg0 <> "(Nothing)"
+              nn <- eval (Proxy @n) opts (s,Proxy @z)
+              pure $ case getValueLR NoInline opts (msg1 <> " n failed") nn hhs of
+                   Left e -> e
+                   Right c -> mkNodeCopy opts nn (show3 opts msg1 c ()) hhs
+            Just a -> do
+              let msg1 = msg0 <> "(Just)"
+              pp <- eval (Proxy @p) opts (s,a)
+              pure $ case getValueLR NoInline opts (msg1 <> " p failed") pp hhs of
+                   Left e -> e
+                   Right c -> mkNodeCopy opts pp (show3 opts msg1 c a) hhs
+
+type family MaybeInT (p :: k) (y :: Type) (ma :: Type) where
+  MaybeInT p y (Maybe a) = PP p (y,a)
+  MaybeInT _ _ o = GL.TypeError (
+      'GL.Text "MaybeInT: expected 'Maybe a' "
+      ':$$: 'GL.Text "o = "
+      ':<>: 'GL.ShowType o)
+
+-- | simple version of 'MaybeIn' with Id as the Maybe value and the environment set to ()
+--
+-- >>> pz @(MaybeId '("x","oops") '(Id,"fromjust")) (Just "ok")
+-- Val ("ok","fromjust")
+--
+-- >>> pz @(MaybeId '("x","oops") '(Id,"fromjust")) Nothing
+-- Val ("x","oops")
+--
+-- >>> pz @(MaybeId "found nothing" (ShowP Pred)) (Just 20)
+-- Val "19"
+--
+-- >>> pz @(MaybeId "found nothing" (ShowP Pred)) Nothing
+-- Val "found nothing"
+--
+-- >>> pl @(MaybeId 'True Id) Nothing
+-- True (MaybeIn(Nothing) True | ())
+-- Val True
+--
+-- >>> pl @(MaybeId 'True IdBool) (Just False)
+-- False (MaybeIn(Just) False | False)
+-- Val False
+--
+-- >>> pl @(MaybeId (FailT _ "failed4") Id) (Just 10)
+-- Present 10 (MaybeIn(Just) 10 | 10)
+-- Val 10
+--
+-- >>> pl @(MaybeId 'False Id) Nothing
+-- False (MaybeIn(Nothing) False | ())
+-- Val False
+--
+-- >>> pl @(MaybeId (FailT _ "err") Id) Nothing
+-- Error err (Proxy | MaybeIn(Nothing) n failed)
+-- Fail "err"
+--
+-- >>> pz @(MaybeId 99 Id) (Just 12)
+-- Val 12
+--
+-- >>> pz @(MaybeId 99 Id) Nothing
+-- Val 99
+--
+-- >>> pl @(MaybeId MEmptyP Ones) (Just "ab")
+-- Present ["a","b"] (MaybeIn(Just) ["a","b"] | "ab")
+-- Val ["a","b"]
+--
+-- >>> pl @(MaybeId MEmptyP Ones) Nothing
+-- Present [] (MaybeIn(Nothing) [] | ())
+-- Val []
+--
+-- >>> pl @(MaybeId MEmptyP (Fst ==! Snd)) (Just ('x','z'))
+-- Present LT (MaybeIn(Just) LT | ('x','z'))
+-- Val LT
+--
+-- >>> pl @(MaybeId MEmptyP (Fst ==! Snd)) (Nothing @(Char,Char))
+-- Present EQ (MaybeIn(Nothing) EQ | ())
+-- Val EQ
+--
+data MaybeId n p deriving Show
+
+type MaybeIdT n p = MaybeIn (Snd >> n) (Snd >> p) () Id
+
+instance P (MaybeIdT n p) x => P (MaybeId n p) x where
+  type PP (MaybeId n p) x = PP (MaybeIdT n p) x
+  eval _ = eval (Proxy @(MaybeIdT n p))
+

@@ -17,6 +17,7 @@ {-# LANGUAGE EmptyDataDeriving #-}
 -- | promoted 'Semigroup' and 'Monoid' functions
 module Predicate.Data.Monoid (
+  -- ** functions
     type (<>)
   , MConcat
   , SConcat
@@ -122,28 +123,23 @@ 
 -- | similar to 'mconcat'
 --
--- >>> pz @(MConcat Id) [SG.Sum 44, SG.Sum 12, SG.Sum 3]
+-- >>> pz @MConcat [SG.Sum 44, SG.Sum 12, SG.Sum 3]
 -- Val (Sum {getSum = 59})
 --
--- >>> pz @(Map '(Pure SG.Sum Id, Pure SG.Max Id) >> MConcat Id) [7 :: Int,6,1,3,5] -- monoid so need eg Int
+-- >>> pz @(Map '(Pure SG.Sum Id, Pure SG.Max Id) >> MConcat) [7 :: Int,6,1,3,5] -- monoid so need eg Int
 -- Val (Sum {getSum = 22},Max {getMax = 7})
 --
-data MConcat p deriving Show
+data MConcat deriving Show
 
-instance ( PP p x ~ [a]
-         , P p x
+instance ( x ~ [a]
          , Show a
          , Monoid a
-         ) => P (MConcat p) x where
-  type PP (MConcat p) x = ExtractAFromList (PP p x)
-  eval _ opts x = do
+         ) => P MConcat x where
+  type PP MConcat x = ExtractAFromList x
+  eval _ opts x =
     let msg0 = "MConcat"
-    pp <- eval (Proxy @p) opts x
-    pure $ case getValueLR NoInline opts msg0 pp [] of
-      Left e -> e
-      Right p ->
-        let b = mconcat p
-        in mkNode opts (Val b) (show3 opts msg0 b p) [hh pp]
+        b = mconcat x
+    in pure $ mkNode opts (Val b) (show3 opts msg0 b x) []
 
 -- | similar to 'SG.sconcat'
 --

@@ -1037,14 +1037,6 @@   type PP (ReadBase t n) x = PP (ReadBaseT t n) x
   eval _ = eval (Proxy @(ReadBaseT t n))
 
-getValidBase :: Int -> String
-getValidBase n =
-  let xs = ['0'..'9'] <> ['a'..'z']
-      len = length xs
-  in if n > len || n < 2
-     then errorInProgram $ "getValidBase: oops invalid base valid is 2 thru " ++ show len ++ " found " ++ show n
-     else take n xs
-
 -- | Display a number at base 2 to 36, similar to 'Numeric.showIntAtBase' but passes the sign through
 --
 -- >>> pz @(ShowBase 16) 4077
@@ -1117,8 +1109,8 @@ 
 -- | convert to bits
 --
--- >>> pl @(ToBits 123 >> UnShowBaseN 2) ()
--- Present 123 ((>>) 123 | {UnShowBaseN | 2 | [1,1,1,1,0,1,1]})
+-- >>> pl @(UnShowBaseN 2 (ToBits 123)) ()
+-- Present 123 (UnShowBaseN | 2 | [1,1,1,1,0,1,1])
 -- Val 123
 --
 data ToBits p deriving Show
@@ -1128,44 +1120,44 @@   type PP (ToBits p) x = PP (ToBitsT p) x
   eval _ = eval (Proxy @(ToBitsT p))
 
--- | reverse 'ShowBaseN'
+-- | reverse 'ShowBaseN': doesn't enforce that the values are in range of the given base
 --
--- >>> pz @(UnShowBaseN 2) [1,0,0,1,0]
+-- >>> pz @(UnShowBaseN 2 Id) [1,0,0,1,0]
 -- Val 18
 --
--- >>> pz @(UnShowBaseN 2) [1,1,1]
+-- >>> pz @(UnShowBaseN Fst Snd) (2,[1,1,1])
 -- Val 7
 --
--- >>> pz @(UnShowBaseN 16) [7,0,3,1]
+-- >>> pz @(UnShowBaseN 16 Id) [7,0,3,1]
 -- Val 28721
 --
--- >>> pz @(UnShowBaseN 16) [0]
+-- >>> pz @(UnShowBaseN 16 Id) [0]
 -- Val 0
 --
--- >>> pz @(UnShowBaseN 16) []
+-- >>> pz @(UnShowBaseN 16 Id) []
 -- Val 0
 --
-data UnShowBaseN n deriving Show
+data UnShowBaseN n p deriving Show
 
-instance ( x ~ [a]
+instance ( PP p x ~ [a]
          , PP n x ~ b
          , P n x
+         , P p x
          , Integral a
          , Integral b
-         ) => P (UnShowBaseN n) x where
-  type PP (UnShowBaseN n) x = Integer
+         ) => P (UnShowBaseN n p) x where
+  type PP (UnShowBaseN n p) x = Integer
   eval _ opts x = do
     let msg0 = "UnShowBaseN"
-    nn <- eval (Proxy @n) opts x
-    pure $ case getValueLR NoInline opts msg0 nn [] of
+    lr <- runPQ NoInline msg0 (Proxy @n) (Proxy @p) opts x []
+    pure $ case lr of
       Left e -> e
-      Right (fromIntegral -> n) ->
-         let xs = map fromIntegral x
-             hhs = [hh nn]
+      Right (fromIntegral -> n,p,nn,pp) ->
+         let xs = map fromIntegral p
+             hhs = [hh nn, hh pp]
          in if n < 2 then mkNode opts (Fail (msg0 <> " base must be greater than 1")) "" hhs
             else let b = snd $ foldr (\a (m,tot) -> (m*n, a*m+tot)) (1,0) xs
                  in mkNode opts (Val b) (msg0 <> showVerbose opts " | " n <> showVerbose opts " | " xs) hhs
-
 
 -- | calculate the amount to roundup to the next @n@
 --

@@ -1,7 +1,7 @@ {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
-  {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE DataKinds #-}
@@ -16,6 +16,7 @@ {-# LANGUAGE EmptyDataDeriving #-}
 -- | promoted 'Ordering' functions
 module Predicate.Data.Ordering (
+  -- ** functions
     type (>)
   , type (>=)
   , type (==)
@@ -564,4 +565,3 @@ instance P NegativeT x => P Negative x where
   type PP Negative x = PP NegativeT x
   eval _ = evalBool (Proxy @NegativeT)
-

@@ -31,6 +31,17 @@   , PApp
   , PApp2
 
+ -- ** type families
+  , Proxy2TT
+  , Pop0T
+  , Pop1T
+  , Pop1'T
+  , Pop2T
+  , Pop2'T
+  , PAppT
+  , PApp2T
+  , ProxifyT
+
  ) where
 import Predicate.Core
 import Predicate.Misc
@@ -74,13 +85,13 @@ 
 -- | makes a proxy from a one parameter container
 --
--- >>> pz @(Pop1' (Proxy EmptyT) Proxy1T 123) Nothing
+-- >>> pz @(Pop2' (Proxy EmptyT) Proxy1T (Proxy Int) 123) Nothing
 -- Val Nothing
 --
--- >>> pz @(Pop1' (Proxy EmptyT) Proxy1T 123) (Just 10)
+-- >>> pz @(Pop2' (Proxy EmptyT) Proxy1T (Proxy Int) 123) (Just 10)
 -- Val Nothing
 --
--- >>> pz @((Id $$ ()) >> Pop1' (Proxy EmptyT) Proxy1T 123) Just
+-- >>> pz @((Id $$ ()) >> Pop2' (Proxy EmptyT) Proxy1T (Proxy Int) 123) Just
 -- Val Nothing
 --
 data Proxy1T deriving Show
@@ -92,22 +103,22 @@ 
 -- | makes a proxy from a two parameter container
 --
--- >>> pz @(Pop1' (Proxy EmptyT) Proxy2T 123) (Left "ASf")
+-- >>> pz @(Pop2' (Proxy EmptyT) Proxy2T (Proxy Int) 123) (Left "ASf")
 -- Val (Left "")
 --
--- >>> pz @(Pop1' (Proxy EmptyT) Proxy2T 123) (Right 1)
+-- >>> pz @(Pop2' (Proxy EmptyT) Proxy2T (Proxy Int) 123) (Right 1)
 -- Val (Left "")
 --
--- >>> pz @((Id $$ "asdf") >> Pop1' (Proxy EmptyT) Proxy2T 123) Left
+-- >>> pz @((Id $$ "asdf") >> Pop2' (Proxy EmptyT) Proxy2T (Proxy Int) 123) Left
 -- Val (Left "")
 --
--- >>> pz @((Id $$ "asdf") >> Pop1' (Proxy EmptyT) Proxy2T 123) Right
+-- >>> pz @((Id $$ "asdf") >> Pop2' (Proxy EmptyT) Proxy2T (Proxy Int) 123) Right
 -- Val (Left "")
 --
--- >>> pz @(Pop1' (Proxy EmptyT) ((Id $$ "ss") >> Proxy2T) 123) Right
+-- >>> pz @(Pop2' (Proxy EmptyT) ((Id $$ "ss") >> Proxy2T) (Proxy Int) 123) Right
 -- Val (Left "")
 --
--- >>> pz @(Pop1' (Proxy EmptyT) ((Id $$ "ss") >> Proxy2T) 123) Left
+-- >>> pz @(Pop2' (Proxy EmptyT) ((Id $$ "ss") >> Proxy2T) (Proxy Int) 123) Left
 -- Val (Left "")
 --
 data Proxy2T deriving Show
@@ -196,7 +207,7 @@         zz <- eval (Proxy @z) opts q
         pure $ case getValueLR NoInline opts msg0 zz [hh qq] of
           Left e -> e
-          Right _z -> mkNodeCopy opts zz (msg0 <> nullIf " | " (zz ^. ttString)) [hh qq,hh zz]
+          Right _z -> mkNodeCopy opts zz (joinStrings msg0 (zz ^. ttString)) [hh qq]
 
 -- the key is to pass all the vars into the type family so ghc can figure stuff out
 type family Pop0T (p :: Type) (q :: Type) :: Type where
@@ -257,7 +268,7 @@         zz <- eval (Proxy @(z q)) opts r
         pure $ case getValueLR NoInline opts msg0 zz [hh rr] of
           Left e -> e
-          Right _z -> mkNodeCopy opts zz (msg0 <> nullIf " | " (zz ^. ttString)) [hh rr,hh zz]
+          Right _z -> mkNodeCopy opts zz (joinStrings msg0 (zz ^. ttString)) [hh rr]
 
 type family Pop1T (p :: Type) (q :: k) (r :: Type) :: Type where
   Pop1T (Proxy z) q r = PP (z q) r
@@ -319,7 +330,7 @@         zz <- eval (Proxy @(z w)) opts r
         pure $ case getValueLR NoInline opts msg0 zz [hh rr] of
           Left e -> e
-          Right _z -> mkNodeCopy opts zz (msg0 <> nullIf " | " (zz ^. ttString)) [hh rr,hh zz]
+          Right _z -> mkNodeCopy opts zz (joinStrings msg0 (zz ^. ttString)) [hh rr]
 
 type family Pop1'T (p :: Type) (q :: Type) (r :: Type) :: Type where
   Pop1'T (Proxy z) (Proxy w) r = PP (z w) r
@@ -356,7 +367,7 @@         zz <- eval (Proxy @(z q r)) opts s
         pure $ case getValueLR NoInline opts msg0 zz [hh ss] of
           Left e -> e
-          Right _z -> mkNodeCopy opts zz (msg0 <> nullIf " | " (zz ^. ttString)) [hh ss,hh zz]
+          Right _z -> mkNodeCopy opts zz (joinStrings msg0 (zz ^. ttString)) [hh ss]
 
 -- pass all the arguments in!!! else ghc gets confused
 type family Pop2T (p :: Type) (q :: k) (r :: k1) (s :: Type) :: Type where
@@ -400,7 +411,7 @@         zz <- eval (Proxy @(z w v)) opts s
         pure $ case getValueLR NoInline opts msg0 zz [hh ss] of
           Left e -> e
-          Right _z -> mkNodeCopy opts zz (msg0 <> nullIf " | " (zz ^. ttString)) [hh ss,hh zz]
+          Right _z -> mkNodeCopy opts zz (joinStrings msg0 (zz ^. ttString)) [hh ss]
 
 -- pass in all the arguments otherwise ghc gets confused
 type family Pop2'T (p :: Type) (q :: Type) (r :: Type) (s :: Type) :: Type where

@@ -28,6 +28,7 @@   , PrintL
   , PrintT
   , PrintI
+  , PrintC (..)
  ) where
 import Predicate.Core
 import Predicate.Misc
@@ -232,7 +233,7 @@ 
 -- | uses inductive tuples to replace variable arguments
 --
-class PrintC x where
+class PrintC (x :: Type) where
   prtC :: (PrintfArg a, PrintfType r) => String -> (a,x) -> r
 instance PrintC () where
   prtC s (a,()) = printf s a

@@ -16,6 +16,7 @@ {-# LANGUAGE EmptyDataDeriving #-}
 -- | promoted regular expression functions
 module Predicate.Data.Regex (
+  -- ** functions
     Re
   , Re'
   , Rescan
@@ -159,13 +160,6 @@   type PP (Re p) x = PP (ReT p) x
   eval _ = evalBool (Proxy @(ReT p))
 
--- only way with rescan is to be explicit: no repeats! and useanchors but not (?m)
--- or just use Re' but then we only get a bool ie doesnt capture groups
--- rescan returns Right [] as an failure!
--- [] is failure!
---  anchored means it has to start at the beginning: can have junk on the end which we cant detect but at least we know it starts at beginning
-
-
 -- | runs a regex matcher returning the original values and optionally any groups: see 'RH.scan'
 --
 -- >>> pl @(Rescan' '[ 'Anchored ] "([[:xdigit:]]{2})" Id) "wfeb12az"
@@ -202,11 +196,12 @@         in case compileRegex @rs msg1 p of
              Left (e,e1) -> mkNode opts (Fail e) e1 hhs
              Right regex ->
-               case splitAt (oRecursion opts) $ RH.scan regex q of
-                 (b, _:_) -> mkNode opts (Fail ("Regex looping(" ++ show (oRecursion opts) ++ ")")) (msg1 <> " " <> show (take 10 b) <> "..." <> showVerbose opts " | " q) hhs
-                 ([], _) -> -- this is a failure because an empty string is returned: so reuse p?
-                             mkNode opts (Fail "Regex no results") (msg1 <> showVerbose opts " | " q) [hh pp, hh qq]
-                 (b, _) -> mkNode opts (Val b) (lit3 opts msg1 b "" q) [hh pp, hh qq]
+               let r = getMaxRecursionValue opts
+               in case splitAt r $ RH.scan regex q of
+                    (b, _:_) -> mkNode opts (Fail ("Regex looping(" ++ show r ++ ")")) (msg1 <> " " <> show (take 10 b) <> "..." <> showVerbose opts " | " q) hhs
+                    ([], _) -> -- this is a failure because an empty string is returned: so reuse p?
+                                mkNode opts (Fail "Regex no results") (msg1 <> showVerbose opts " | " q) [hh pp, hh qq]
+                    (b, _) -> mkNode opts (Val b) (lit3 opts msg1 b "" q) [hh pp, hh qq]
 
 -- | see 'RH.scan'
 --
@@ -296,11 +291,12 @@         in case compileRegex @rs msg1 p of
           Left (e,e1) -> mkNode opts (Fail e) e1 hhs
           Right regex ->
-            case splitAt (oRecursion opts) $ RH.scanRanges regex q of
-              (b, _:_) -> mkNode opts (Fail ("Regex looping(" ++ show (oRecursion opts) ++ ")")) (msg1 <> " " <> show (take 10 b) <> "..." <> showVerbose opts " | " q) hhs
-              ([], _) -> -- this is a failure because an empty string is returned: so reuse p?
-                         mkNode opts (Fail "Regex no results") (msg1 <> showVerbose opts " | " q) hhs
-              (b, _) -> mkNode opts (Val b) (lit3 opts msg1 b "" q) hhs
+            let r = getMaxRecursionValue opts
+            in case splitAt r $ RH.scanRanges regex q of
+                 (b, _:_) -> mkNode opts (Fail ("Regex looping(" ++ show r ++ ")")) (msg1 <> " " <> show (take 10 b) <> "..." <> showVerbose opts " | " q) hhs
+                 ([], _) -> -- this is a failure because an empty string is returned: so reuse p?
+                            mkNode opts (Fail "Regex no results") (msg1 <> showVerbose opts " | " q) hhs
+                 (b, _) -> mkNode opts (Val b) (lit3 opts msg1 b "" q) hhs
 
 -- | see 'RH.scanRanges'
 --
@@ -344,11 +340,12 @@         in case compileRegex @rs msg1 p of
           Left (e,e1) -> mkNode opts (Fail e) e1 hhs
           Right regex ->
-            case splitAt (oRecursion opts) $ RH.split regex q of
-              (b, _:_) -> mkNode opts (Fail ("Regex looping(" ++ show (oRecursion opts) ++ ")")) (msg1 <> " " <> show (take 10 b) <> "..." <> showVerbose opts " | " q) hhs
-              ([], _) -> -- this is a failure because an empty string is returned: so reuse p?
-                         mkNode opts (Fail "Regex no results") (msg1 <> showVerbose opts " | " q) hhs
-              (b, _) -> mkNode opts (Val b) (lit3 opts msg1 b "" q) hhs
+            let r = getMaxRecursionValue opts
+            in case splitAt r $ RH.split regex q of
+                 (b, _:_) -> mkNode opts (Fail ("Regex looping(" ++ show r ++ ")")) (msg1 <> " " <> show (take 10 b) <> "..." <> showVerbose opts " | " q) hhs
+                 ([], _) -> -- this is a failure because an empty string is returned: so reuse p?
+                            mkNode opts (Fail "Regex no results") (msg1 <> showVerbose opts " | " q) hhs
+                 (b, _) -> mkNode opts (Val b) (lit3 opts msg1 b "" q) hhs
 
 -- | splits a string on a regex delimiter: see 'RH.split'
 --

@@ -17,6 +17,7 @@ {-# LANGUAGE EmptyDataDeriving #-}
 -- | promoted String functions
 module Predicate.Data.String (
+  -- ** functions
     TrimBoth
   , TrimL
   , TrimR
@@ -31,6 +32,7 @@   , IsSuffixCI
 
   , ToString
+  , ToStringC (..)
   , FromString
   , FromString'
  ) where
@@ -211,9 +213,13 @@     lr <- runPQ NoInline msg0 (Proxy @p) (Proxy @q) opts x []
     pure $ case lr of
       Left e -> e
-      Right (p,q,pp,qq) ->
-        let msg1 = msg0 <> (if ignore then "I" else "") <> " | " <> p
-        in mkNodeB opts (on ff lwr p q) (msg1 <> " " <> litL opts q) [hh pp, hh qq]
+      Right (p',q',pp,qq) ->
+        let hhs = [hh pp, hh qq]
+        in case chkSize2 opts msg0 p' q' hhs of
+          Left e -> e
+          Right ((_,p),(_,q)) ->
+            let msg1 = joinStrings (msg0 <> if ignore then "I" else "") p
+            in mkNodeB opts (on ff lwr p q) (msg1 <> " " <> litL opts q) hhs
 
 -- | similar to 'Data.List.isPrefixOf' for strings
 --
@@ -323,7 +329,7 @@   type PP ToString x = String
   eval _ opts x = pure $ mkNode opts (Val (toStringC x)) "ToString" []
 
-class ToStringC a where
+class ToStringC (a :: Type) where
   toStringC :: a -> String
 instance ToStringC String where
   toStringC = id
@@ -363,9 +369,9 @@ -- Val (fromList "abc")
 --
 data FromString (t :: Type) p deriving Show
-type FromStringPT (t :: Type) p = FromString' (Hole t) p
+type FromStringT (t :: Type) p = FromString' (Hole t) p
 
-instance P (FromStringPT t p) x => P (FromString t p) x where
-  type PP (FromString t p) x = PP (FromStringPT t p) x
-  eval _ = eval (Proxy @(FromStringPT t p))
+instance P (FromStringT t p) x => P (FromString t p) x where
+  type PP (FromString t p) x = PP (FromStringT t p) x
+  eval _ = eval (Proxy @(FromStringT t p))
 

@@ -28,7 +28,7 @@   , MkThat'
   , MkThese
 
- -- ** get rid of These
+ -- ** destructors
   , This'
   , That'
   , These'
@@ -45,14 +45,18 @@   , Heres
   , TheseIn
   , TheseId
+  , ThesePair
+  , ThisDef'
+  , ThatDef'
+  , TheseDef'
+  , TheseInSimple
   , PartitionThese
-  , TheseX
 
  -- ** miscellaneous
   , ZipThese
-  , Assoc
-  , Unassoc
 
+ -- ** type families
+  , TheseInT
  ) where
 import Predicate.Core
 import Predicate.Misc
@@ -61,6 +65,8 @@ import Data.Kind (Type)
 import Data.These (partitionThese, These(..))
 import qualified Data.These.Combinators as TheseC
+import qualified GHC.TypeLits as GL
+import GHC.TypeLits (ErrorMessage((:$$:),(:<>:)))
 
 -- $setup
 -- >>> :set -XDataKinds
@@ -170,71 +176,6 @@         b = TheseC.catThere as
     in pure $ mkNode opts (Val b) (show3 opts msg0 b as) []
 
--- | similar to 'Data.These.mergeTheseWith' but additionally provides @p@, @q@ and @r@ the original input as the first element in the tuple
---
--- >>> pz @(TheseX ((L11 + Snd) >> ShowP Id) (ShowP Id) L22 Snd) (9,This 123)
--- Val "132"
---
--- >>> pz @(TheseX '(Snd,"fromthis") '(Negate 99,Snd) Snd Id) (This 123)
--- Val (123,"fromthis")
---
--- >>> pz @(TheseX '(Snd,"fromthis") '(Negate 99,Snd) Snd Id) (That "fromthat")
--- Val (-99,"fromthat")
---
--- >>> pz @(TheseX '(Snd,"fromthis") '(Negate 99,Snd) Snd Id) (These 123 "fromthese")
--- Val (123,"fromthese")
---
--- >>> pl @(TheseX (PrintF "a=%d" (Snd >> Succ)) ("b=" <> Snd) (PrintT "a=%d b=%s" Snd) Id) (These @Int 9 "rhs")
--- Present "a=9 b=rhs" (TheseX(These))
--- Val "a=9 b=rhs"
---
--- >>> pl @(TheseX (PrintF "a=%d" (Snd >> Succ)) ("b=" <> Snd) (PrintT "a=%d b=%s" Snd) Id) (This @Int 9)
--- Present "a=10" (TheseX(This))
--- Val "a=10"
---
--- >>> pl @(TheseX (PrintF "a=%d" (Snd >> Succ)) ("b=" <> Snd) (PrintT "a=%d b=%s" Snd) Id) (That @Int "rhs")
--- Present "b=rhs" (TheseX(That))
--- Val "b=rhs"
---
-data TheseX p q r s deriving Show
-
-instance ( P s x
-         , P p (x,a)
-         , P q (x,b)
-         , P r (x,(a,b))
-         , PP s x ~ These a b
-         , PP p (x,a) ~ c
-         , PP q (x,b) ~ c
-         , PP r (x,(a,b)) ~ c
-         ) => P (TheseX p q r s) x where
-  type PP (TheseX p q r s) x = TheseXT (PP s x) x p
-  eval _ opts x = do
-    let msg0 = "TheseX"
-    ss <- eval (Proxy @s) opts x
-    case getValueLR NoInline opts msg0 ss [] of
-      Left e -> pure e
-      Right (This a) -> do
-        let msg1 = msg0 <> "(This)"
-        pp <- eval (Proxy @p) opts (x,a)
-        pure $ case getValueLR NoInline opts msg1 pp [hh ss] of
-          Left e -> e
-          Right _ -> mkNodeCopy opts pp msg1 [hh ss, hh pp]
-      Right (That b) -> do
-        let msg1 = msg0 <> "(That)"
-        qq <- eval (Proxy @q) opts (x,b)
-        pure $ case getValueLR NoInline opts msg1 qq [hh ss] of
-          Left e -> e
-          Right _ -> mkNodeCopy opts qq msg1 [hh ss, hh qq]
-      Right (These a b) -> do
-        let msg1 = msg0 <> "(These)"
-        rr <- eval (Proxy @r) opts (x,(a,b))
-        pure $ case getValueLR NoInline opts msg1 rr [hh ss] of
-          Left e -> e
-          Right _ -> mkNodeCopy opts rr msg1 [hh ss, hh rr]
-
-type family TheseXT lr x p where
-  TheseXT (These a _b) x p = PP p (x,a)
-
 -- | 'Data.These.This' constructor
 --
 -- >>> pz @(Proxy Int >> MkThis' UnproxyT 10) []
@@ -350,7 +291,7 @@   type PP (IsTh th) x = Bool
   eval _ opts x =
     let msg0 = "Is"
-        (t,f) = getThese @th
+        (t,f) = getThese @_ @_ @th
         b = f x
     in pure $ mkNodeB opts b (msg0 <> t <> showVerbose opts " | " x) []
 
@@ -414,101 +355,6 @@   type PP IsThese x = PP IsTheseT x
   eval _ = evalBool (Proxy @IsTheseT)
 
--- | similar to 'Data.These.these'
---
--- >>> pz @(TheseIn Id Len (Fst + Length Snd)) (This 13)
--- Val 13
---
--- >>> pz @(TheseIn Id Len (Fst + Length Snd)) (That "this is a long string")
--- Val 21
---
--- >>> pz @(TheseIn Id Len (Fst + Length Snd)) (These 20 "somedata")
--- Val 28
---
--- >>> pz @(TheseIn (MkLeft _ Id) (MkRight _ Id) (If (Fst > Length Snd) (MkLeft _ Fst) (MkRight _ Snd))) (That "this is a long string")
--- Val (Right "this is a long string")
---
--- >>> pz @(TheseIn (MkLeft _ Id) (MkRight _ Id) (If (Fst > Length Snd) (MkLeft _ Fst) (MkRight _ Snd))) (These 1 "this is a long string")
--- Val (Right "this is a long string")
---
--- >>> pz @(TheseIn (MkLeft _ Id) (MkRight _ Id) (If (Fst > Length Snd) (MkLeft _ Fst) (MkRight _ Snd))) (These 100 "this is a long string")
--- Val (Left 100)
---
--- >>> pl @(TheseIn "this" "that" "these") (This (SG.Sum 12))
--- Present "this" (TheseIn "this" | This Sum {getSum = 12})
--- Val "this"
---
--- >>> pl @(TheseIn (Id &&& 999) ("no value" &&& Id) Id) (These "Ab" 13)
--- Present ("Ab",13) (TheseIn ("Ab",13) | These "Ab" 13)
--- Val ("Ab",13)
---
--- >>> pl @(TheseIn (Id &&& 999) ("no value" &&& Id) Id) (This "Ab")
--- Present ("Ab",999) (TheseIn ("Ab",999) | This "Ab")
--- Val ("Ab",999)
---
--- >>> pl @(TheseIn (Id &&& 999) ("no value" &&& Id) Id) (That 13)
--- Present ("no value",13) (TheseIn ("no value",13) | That 13)
--- Val ("no value",13)
---
-data TheseIn p q r deriving Show
-
-instance ( Show a
-         , Show b
-         , Show (PP p a)
-         , P p a
-         , P q b
-         , P r (a,b)
-         , PP p a ~ PP q b
-         , PP p a ~ PP r (a,b)
-         , PP q b ~ PP r (a,b)
-         )  => P (TheseIn p q r) (These a b) where
-  type PP (TheseIn p q r) (These a b) = PP p a
-  eval _ opts th = do
-     let msg0 = "TheseIn"
-     case th of
-        This a -> do
-          let msg1 = "This "
-              msg2 = msg0 <> msg1
-          pp <- eval (Proxy @p) opts a
-          pure $ case getValueLR NoInline opts (msg2 <> "p failed") pp [] of
-               Left e -> e
-               Right c -> mkNode opts (Val c) (show3' opts msg0 c msg1 a) [hh pp]
-        That b -> do
-          let msg1 = "That "
-              msg2 = msg0 <> msg1
-          qq <- eval (Proxy @q) opts b
-          pure $ case getValueLR NoInline opts (msg2 <> "q failed") qq [] of
-               Left e -> e
-               Right c -> mkNode opts (Val c) (show3' opts msg0 c msg1 b) [hh qq]
-        These a b -> do
-          let msg1 = "These "
-              msg2 = msg0 <> msg1
-          rr <- eval (Proxy @r) opts (a,b)
-          pure $ case getValueLR NoInline opts (msg2 <> "r failed") rr [] of
-               Left e -> e
-               Right c -> mkNode opts (Val c) (show3 opts msg0 c (These a b)) [hh rr]
-
--- | TheseId: given a 'These' returns a tuple but you need to provide default values for both sides
---
--- >>> pl @(TheseId "xyz" 'True ) (This "abc")
--- Present ("abc",True) (TheseIn ("abc",True) | This "abc")
--- Val ("abc",True)
---
--- >>> pl @(TheseId "xyz" 'True) (That False)
--- Present ("xyz",False) (TheseIn ("xyz",False) | That False)
--- Val ("xyz",False)
---
--- >>> pl @(TheseId "xyz" 'True) (These "abc" False)
--- Present ("abc",False) (TheseIn ("abc",False) | These "abc" False)
--- Val ("abc",False)
---
-data TheseId p q deriving Show
-type TheseIdT p q = TheseIn '(Id, q) '(p, Id) Id
-
-instance P (TheseIdT p q) x => P (TheseId p q) x where
-  type PP (TheseId p q) x = PP (TheseIdT p q) x
-  eval _ = eval (Proxy @(TheseIdT p q))
-
 -- | similar to 'Data.Align.align' thats pads with 'Data.These.This' or 'Data.These.That' if one list is shorter than the other
 --
 -- the key is that all information about both lists are preserved
@@ -531,11 +377,11 @@ -- >>> pz @(ZipThese '[] '[]) "aBcDeF"
 -- Val []
 --
--- >>> pl @(ZipThese Fst Snd >> Map (TheseIn Id Id Fst)) (['w'..'y'],['a'..'f'])
+-- >>> pl @(ZipThese Fst Snd >> Map (TheseInSimple Id Id Fst)) (['w'..'y'],['a'..'f'])
 -- Present "wxydef" ((>>) "wxydef" | {Map "wxydef" | [These 'w' 'a',These 'x' 'b',These 'y' 'c',That 'd',That 'e',That 'f']})
 -- Val "wxydef"
 --
--- >>> pl @(("sdf" &&& Id) >> ZipThese Fst Snd >> Map (TheseIn (Id &&& 0) (C "x" &&& Id) Id)) [1..5]
+-- >>> pl @(("sdf" &&& Id) >> ZipThese Fst Snd >> Map (TheseInSimple (Id &&& 0) (C "x" &&& Id) Id)) [1..5]
 -- Present [('s',1),('d',2),('f',3),('x',4),('x',5)] ((>>) [('s',1),('d',2),('f',3),('x',4),('x',5)] | {Map [('s',1),('d',2),('f',3),('x',4),('x',5)] | [These 's' 1,These 'd' 2,These 'f' 3,That 4,That 5]})
 -- Val [('s',1),('d',2),('f',3),('x',4),('x',5)]
 --
@@ -562,12 +408,6 @@             let d = simpleAlign p q
             in mkNode opts (Val d) (show3' opts msg0 d "p=" p <> showVerbose opts " | q=" q) hhs
 
-simpleAlign :: [a] -> [b] -> [These a b]
-simpleAlign as [] = map This as
-simpleAlign [] bs = map That bs
-simpleAlign (a:as) (b:bs) = These a b : simpleAlign as bs
-
-
 -- | extract the This value from an 'These' otherwise use the default value
 --   if there is no This value then @p@ is passed the whole context only
 --
@@ -617,7 +457,7 @@             pp <- eval (Proxy @p) opts x
             pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
               Left e -> e
-              Right p -> mkNode opts (Val p) (msg0 <> " " <> showThese q) [hh qq, hh pp]
+              Right _ -> mkNodeCopy opts pp (msg0 <> " " <> showThese q) [hh qq]
 
 
 -- | extract the That value from an 'These' otherwise use the default value
@@ -662,7 +502,7 @@             pp <- eval (Proxy @p) opts x
             pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
               Left e -> e
-              Right p -> mkNode opts (Val p) (msg0 <> " " <> showThese q) [hh qq, hh pp]
+              Right _ -> mkNodeCopy opts pp (msg0 <> " " <> showThese q) [hh qq]
 
 -- | extract the These value from an 'These' otherwise use the default value
 --
@@ -718,7 +558,7 @@             pp <- eval (Proxy @p) opts x
             pure $ case getValueLR NoInline opts msg0 pp [hh qq] of
               Left e -> e
-              Right p -> mkNode opts (Val p) (msg0 <> " " <> showThese q) [hh qq, hh pp]
+              Right _ -> mkNodeCopy opts pp (msg0 <> " " <> showThese q) [hh qq]
 
 
 -- | extract the This value from a 'These' otherwise fail with a message
@@ -855,107 +695,6 @@               Right p -> mkNode opts (Fail p) (msg0 <> " " <> showThese q) [hh qq, hh pp]
 
 
--- | assoc using 'AssocC'
---
--- >>> pz @Assoc (This (These 123 'x'))
--- Val (These 123 (This 'x'))
---
--- >>> pz @Assoc ((99,'a'),True)
--- Val (99,('a',True))
---
--- >>> pz @Assoc ((99,'a'),True)
--- Val (99,('a',True))
---
--- >>> pz @Assoc (Right "Abc" :: Either (Either () ()) String)
--- Val (Right (Right "Abc"))
---
--- >>> pz @Assoc (Left (Left 'x'))
--- Val (Left 'x')
---
--- >>> pl @Assoc ((10,'c'),True)
--- Present (10,('c',True)) (Assoc (10,('c',True)) | ((10,'c'),True))
--- Val (10,('c',True))
---
--- >>> pl @(Assoc >> Unassoc) ((10,'c'),True)
--- Present ((10,'c'),True) ((>>) ((10,'c'),True) | {Unassoc ((10,'c'),True) | (10,('c',True))})
--- Val ((10,'c'),True)
---
-data Assoc deriving Show
-
-class AssocC p where
-  assoc :: p (p a b) c -> p a (p b c)
-  unassoc :: p a (p b c) -> p (p a b) c
-instance AssocC Either where
-  assoc (Left (Left a)) = Left a
-  assoc (Left (Right b)) = Right (Left b)
-  assoc (Right b) = Right (Right b)
-  unassoc (Left a) = Left (Left a)
-  unassoc (Right (Left b)) = Left (Right b)
-  unassoc (Right (Right b)) = Right b
-instance AssocC These where
-  assoc (This (This a)) = This a
-  assoc (This (That b)) = That (This b)
-  assoc (That b) = That (That b)
-  assoc (These (This a) c) = These a (That c)
-  assoc (These (That b) c) = That (These b c)
-  assoc (These (These a b) c) = These a (These b c)
-  assoc (This (These a b)) = These a (This b)
-  unassoc (This a) = This (This a)
-  unassoc (That (This b)) = This (That b)
-  unassoc (That (That b)) = That b
-  unassoc (These a (That c)) = These (This a) c
-  unassoc (That (These b c)) = These (That b) c
-  unassoc (These a (These b c)) = These (These a b) c
-  unassoc (These a (This b)) = This (These a b)
-
-instance AssocC (,) where
-  assoc ((a,b),c) = (a,(b,c))
-  unassoc (a,(b,c)) = ((a,b),c)
-
-instance ( AssocC p
-         , Show (p (p a b) c)
-         , Show (p a (p b c))
-         ) => P Assoc (p (p a b) c) where
-  type PP Assoc (p (p a b) c) = p a (p b c)
-  eval _ opts pabc =
-    let msg0 = "Assoc"
-        d = assoc pabc
-    in pure $ mkNode opts (Val d) (show3 opts msg0 d pabc) []
-
--- | unassoc using 'AssocC'
---
--- >>> pz @Unassoc (These 123 (This 'x'))
--- Val (This (These 123 'x'))
---
--- >>> pz @Unassoc (99,('a',True))
--- Val ((99,'a'),True)
---
--- >>> pz @Unassoc (This 10 :: These Int (These Bool ()))
--- Val (This (This 10))
---
--- >>> pz @Unassoc (Right (Right 123))
--- Val (Right 123)
---
--- >>> pz @Unassoc (Left 'x' :: Either Char (Either Bool Double))
--- Val (Left (Left 'x'))
---
--- >>> pl @Unassoc (10,('c',True))
--- Present ((10,'c'),True) (Unassoc ((10,'c'),True) | (10,('c',True)))
--- Val ((10,'c'),True)
---
-data Unassoc deriving Show
-
-instance ( AssocC p
-         , Show (p (p a b) c)
-         , Show (p a (p b c))
-         ) => P Unassoc (p a (p b c)) where
-  type PP Unassoc (p a (p b c)) = p (p a b) c
-  eval _ opts pabc =
-    let msg0 = "Unassoc"
-        d = unassoc pabc
-    in pure $ mkNode opts (Val d) (show3 opts msg0 d pabc) []
-
-
 -- | tries to extract a value from the 'Data.These.This' constructor
 --
 -- >>> pz @(This' >> Succ) (This 20)
@@ -1015,4 +754,264 @@          That _ -> mkNode opts (Fail (msg0 <> " found That")) "" []
          These a b -> mkNode opts (Val (a,b)) (msg0 <> " " <> showL opts (a,b)) []
 
+-- | destructor for These (similar to 'Data.These.these' but with an extra environment @s@)
+--   @p@ @This a@ receives @(PP t x,a)@
+--   @q@ @That b@ receives @(PP t x,b)@
+--   @r@ @These a b@ receives @(PP t x,(a,b))@
+--   @s@ points to the environment you want to pass in
+--   @t@ points to the These value
+--
+-- >>> pz @(TheseIn Snd Fst L21 Fst Snd) (999,This 123)
+-- Val 123
+--
+-- >>> pz @(TheseIn Snd Fst L21 Fst Snd) (999,That 123)
+-- Val 999
+--
+-- >>> pz @(TheseIn Snd Fst L21 Fst Snd) (999,These 9 11)
+-- Val 9
+--
+-- >>> pz @(TheseIn '(Snd,L12) '(L11,Snd) Snd Fst Snd) ((999,'a'), These 12 'x')
+-- Val (12,'x')
+--
+-- >>> pz @(TheseIn '(Snd,L12) '(L11,Snd) Snd Fst Snd) ((999,'a'), That 'z')
+-- Val (999,'z')
+--
+-- >>> pz @(TheseIn Snd (Snd >> Len) (Snd >> Fst + Length Snd) () Id) (This 13)
+-- Val 13
+--
+-- >>> pz @(TheseIn Snd (Snd >> Len) (Snd >> Fst + Length Snd) () Id) (That "abcdef")
+-- Val 6
+--
+-- >>> pl @(TheseIn "left" "right" "both" () Id) (This (SG.Sum 12))
+-- Present "left" (TheseIn "left" | This Sum {getSum = 12})
+-- Val "left"
+--
+-- >>> pl @(TheseIn '(Snd,999) '("no value",Snd) Snd () Id) (These "Ab" 13)
+-- Present ("Ab",13) (TheseIn ("Ab",13) | These "Ab" 13)
+-- Val ("Ab",13)
+--
+-- >>> pl @(TheseIn '(Snd,999) '("no value",Snd) Snd () Id) (This "Ab")
+-- Present ("Ab",999) (TheseIn ("Ab",999) | This "Ab")
+-- Val ("Ab",999)
+--
+-- >>> pz @(TheseIn ((Fst + Snd) >> ShowP Id) Snd "Xx" Fst Snd) (9,This 123)
+-- Val "132"
+--
+-- >>> pz @(TheseIn '(Snd,"fromthis") '(Negate 99,Snd) Snd () Id) (This 123)
+-- Val (123,"fromthis")
+--
+-- >>> pz @(TheseIn '(Snd,"fromthis") '(Negate 99,Snd) Snd () Id) (That "fromthat")
+-- Val (-99,"fromthat")
+--
+-- >>> pz @(TheseIn '(Snd,"fromthis") '(Negate 99,Snd) Snd () Id) (These 123 "fromthese")
+-- Val (123,"fromthese")
+--
+-- >>> pl @(TheseIn (PrintF "a=%d" (Snd >> Succ)) ("b=" <> Snd) (PrintT "a=%d b=%s" Snd) () Id) (These @Int 9 "rhs")
+-- Present "a=9 b=rhs" (TheseIn "a=9 b=rhs" | These 9 "rhs")
+-- Val "a=9 b=rhs"
+--
+-- >>> pl @(TheseIn (PrintF "a=%d" (Snd >> Succ)) ("b=" <> Snd) (PrintT "a=%d b=%s" Snd) () Id) (This @Int 9)
+-- Present "a=10" (TheseIn "a=10" | This 9)
+-- Val "a=10"
+--
+-- >>> pl @(TheseIn (PrintF "a=%d" (Snd >> Succ)) ("b=" <> Snd) (PrintT "a=%d b=%s" Snd) () Id) (That @Int "rhs")
+-- Present "b=rhs" (TheseIn "b=rhs" | That "rhs")
+-- Val "b=rhs"
+--
+-- >>> pz @(TheseIn ((Fst + Snd) >> ShowP Id) (ShowP Id) L22 Fst Snd) (9,This 123)
+-- Val "132"
+--
+data TheseIn p q r s t deriving Show
+
+instance ( Show a
+         , Show b
+         , Show (PP r (y,(a,b)))
+         , P p (y,a)
+         , P q (y,b)
+         , P r (y,(a,b))
+         , PP p (y,a) ~ PP q (y,b)
+         , PP q (y,b) ~ PP r (y,(a,b))
+         , P s x
+         , P t x
+         , PP s x ~ y
+         , PP t x ~ These a b
+         )  => P (TheseIn p q r s t) x where
+  type PP (TheseIn p q r s t) x = TheseInT r (PP s x) (PP t x)
+  eval _ opts x = do
+    let msg0 = "TheseIn"
+    lr <- runPQ NoInline msg0 (Proxy @s) (Proxy @t) opts x []
+    case lr of
+      Left e -> pure e
+      Right (s,t,ss,tt) -> do
+         let hhs = [hh ss, hh tt]
+         case t of
+            This a -> do
+              let msg1 = "This "
+                  msg2 = msg0 <> msg1
+              pp <- eval (Proxy @p) opts (s,a)
+              pure $ case getValueLR NoInline opts (msg2 <> "p failed") pp hhs of
+                   Left e -> e
+                   Right c -> mkNodeCopy opts pp (show3' opts msg0 c msg1 a) hhs
+            That b -> do
+              let msg1 = "That "
+                  msg2 = msg0 <> msg1
+              qq <- eval (Proxy @q) opts (s,b)
+              pure $ case getValueLR NoInline opts (msg2 <> "q failed") qq hhs of
+                   Left e -> e
+                   Right c -> mkNodeCopy opts qq (show3' opts msg0 c msg1 b) hhs
+            These a b -> do
+              let msg1 = "These "
+                  msg2 = msg0 <> msg1
+              rr <- eval (Proxy @r) opts (s,(a,b))
+              pure $ case getValueLR NoInline opts (msg2 <> "r failed") rr hhs of
+                   Left e -> e
+                   Right c -> mkNodeCopy opts rr (show3' opts msg0 c "" (These a b)) hhs
+
+type family TheseInT r y elr where
+  TheseInT r y (These a b) = PP r (y,(a,b))
+  TheseInT _ _ o = GL.TypeError (
+      'GL.Text "TheseInT: expected 'These a b' "
+      ':$$: 'GL.Text "o = "
+      ':<>: 'GL.ShowType o)
+
+-- | simple version of 'TheseIn' with Id as the These value and the environment set to ()
+--
+-- >>> pz @(TheseId '(Id,"fromleft") '(888,Id) Id) (These 222 "ok")
+-- Val (222,"ok")
+--
+-- >>> pz @(TheseId '(Id,"fromleft") '(888,Id) Id) (That "ok")
+-- Val (888,"ok")
+--
+-- >>> pz @(TheseId '(Id,"fromleft") '(888,Id) Id) (This 123)
+-- Val (123,"fromleft")
+--
+data TheseId p q r deriving Show
+type TheseIdT p q r = TheseIn (Snd >> p) (Snd >> q) (Snd >> r) () Id
+
+instance P (TheseIdT p q r) x => P (TheseId p q r) x where
+  type PP (TheseId p q r) x = PP (TheseIdT p q r) x
+  eval _ = eval (Proxy @(TheseIdT p q r))
+
+-- | provide the default pair in @s@ and @t@ refers to These
+--
+-- >>> pz @(ThesePair Fst Snd) ((999,"oops"),These 2 "xx")
+-- Val (2,"xx")
+--
+-- >>> pz @(ThesePair Fst Snd) ((999,"oops"),That "ok")
+-- Val (999,"ok")
+--
+data ThesePair s t deriving Show
+type ThesePairT s t = TheseIn '(Snd,L12) '(L11,Snd) Snd s t
+
+instance P (ThesePairT s t) x => P (ThesePair s t) x where
+  type PP (ThesePair s t) x = PP (ThesePairT s t) x
+  eval _ = eval (Proxy @(ThesePairT s t))
+
+
+-- | similar to 'Data.These.these' but without any environment
+--
+-- >>> pz @(TheseInSimple Id Len (Fst + Length Snd)) (This 13)
+-- Val 13
+--
+-- >>> pz @(TheseInSimple Id Len (Fst + Length Snd)) (That "this is a long string")
+-- Val 21
+--
+-- >>> pz @(TheseInSimple Id Len (Fst + Length Snd)) (These 20 "somedata")
+-- Val 28
+--
+-- >>> pz @(TheseInSimple (MkLeft _ Id) (MkRight _ Id) (If (Fst > Length Snd) (MkLeft _ Fst) (MkRight _ Snd))) (That "this is a long string")
+-- Val (Right "this is a long string")
+--
+-- >>> pz @(TheseInSimple (MkLeft _ Id) (MkRight _ Id) (If (Fst > Length Snd) (MkLeft _ Fst) (MkRight _ Snd))) (These 1 "this is a long string")
+-- Val (Right "this is a long string")
+--
+-- >>> pz @(TheseInSimple (MkLeft _ Id) (MkRight _ Id) (If (Fst > Length Snd) (MkLeft _ Fst) (MkRight _ Snd))) (These 100 "this is a long string")
+-- Val (Left 100)
+--
+-- >>> pl @(TheseInSimple "this" "that" "these") (This (SG.Sum 12))
+-- Present "this" (TheseIn "this" | This Sum {getSum = 12})
+-- Val "this"
+--
+-- >>> pl @(TheseInSimple (Id &&& 999) ("no value" &&& Id) Id) (These "Ab" 13)
+-- Present ("Ab",13) (TheseIn ("Ab",13) | These "Ab" 13)
+-- Val ("Ab",13)
+--
+-- >>> pl @(TheseInSimple (Id &&& 999) ("no value" &&& Id) Id) (This "Ab")
+-- Present ("Ab",999) (TheseIn ("Ab",999) | This "Ab")
+-- Val ("Ab",999)
+--
+-- >>> pl @(TheseInSimple (Id &&& 999) ("no value" &&& Id) Id) (That 13)
+-- Present ("no value",13) (TheseIn ("no value",13) | That 13)
+-- Val ("no value",13)
+--
+data TheseInSimple p q r deriving Show
+type TheseInSimpleT p q r = TheseIn (Snd >> p) (Snd >> q) (Snd >> r) () Id
+
+instance P (TheseInSimpleT p q r) x => P (TheseInSimple p q r) x where
+  type PP (TheseInSimple p q r) x = PP (TheseInSimpleT p q r) x
+  eval _ = eval (Proxy @(TheseInSimpleT p q r))
+
+
+-- | get This or use the default value @p@: @q@ is the environment and @r@ is the These value
+--
+-- >>> pz @(ThisDef' Id Fst Snd) (999,These 1 "xx")
+-- Val 999
+--
+-- >>> pz @(ThisDef' 999 () Id) (That "sdf")
+-- Val 999
+--
+-- >>> pz @(ThisDef' 999 () Id) (This 1)
+-- Val 1
+--
+data ThisDef' p q r deriving Show
+
+type ThisDefT' p q r = TheseIn Snd (Fst >> p) (Fst >> p) q r
+
+instance P (ThisDefT' p q r) x => P (ThisDef' p q r) x where
+  type PP (ThisDef' p q r) x = PP (ThisDefT' p q r) x
+  eval _ = eval (Proxy @(ThisDefT' p q r))
+
+-- | get That or use the default value @p@: @q@ is the environment and @r@ is the These value
+--
+-- >>> pz @(ThatDef' 999 () Id) (These "x" 1)
+-- Val 999
+--
+-- >>> pz @(ThatDef' 999 () Id) (This "sdf")
+-- Val 999
+--
+-- >>> pz @(ThatDef' 999 Fst Snd) (999,That 1)
+-- Val 1
+--
+data ThatDef' p q r deriving Show
+
+type ThatDefT' p q r = TheseIn (Fst >> p) Snd (Fst >> p) q r
+
+instance P (ThatDefT' p q r) x => P (ThatDef' p q r) x where
+  type PP (ThatDef' p q r) x = PP (ThatDefT' p q r) x
+  eval _ = eval (Proxy @(ThatDefT' p q r))
+
+-- | get These or use the default value @p@: @q@ is the environment and @r@ is the These value
+--
+-- >>> pz @(TheseDef' '(999,"xx") () Id) (These 12 "yy")
+-- Val (12,"yy")
+--
+-- >>> pz @(TheseDef' '(999,"xx") () Id) (That "abc")
+-- Val (999,"xx")
+--
+-- >>> pz @(TheseDef' '(999,"xx") () Id) (This 1)
+-- Val (999,"xx")
+--
+-- >>> pz @(TheseDef' '(999,"xx") () Id) (These 1 "abc")
+-- Val (1,"abc")
+--
+-- >>> pz @(TheseDef' Id Fst Snd) ((999,"xx"),That "yy")
+-- Val (999,"xx")
+--
+data TheseDef' p q r deriving Show
+
+type TheseDefT' p q r = TheseIn (Fst >> p) (Fst >> p) Snd q r
+
+instance P (TheseDefT' p q r) x => P (TheseDef' p q r) x where
+  type PP (TheseDef' p q r) x = PP (TheseDefT' p q r) x
+  eval _ = eval (Proxy @(TheseDefT' p q r))
 

@@ -25,6 +25,8 @@   , type (***)
   , Both
   , On
+  , On'
+  , Uncurry
 
  -- ** flat tuples
   , Tuple
@@ -44,6 +46,9 @@   , ReverseITuple
   , ToITupleList
 
+ -- ** assoc
+  , Assoc
+  , Unassoc
  ) where
 import Predicate.Core
 import Predicate.Misc
@@ -62,6 +67,7 @@ -- >>> :set -XNoOverloadedLists
 -- >>> import Predicate.Prelude
 -- >>> import qualified Data.Semigroup as SG
+-- >>> :m + Data.These
 -- >>> :m + Data.Ratio
 
 -- | duplicate a value into a tuple
@@ -266,7 +272,7 @@                           (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 <> nullIf " | " zz) [hh rr, hh pp, hh qq]
+                in mkNodeB opts (p&&q) (showL opts p <> " " <> msg0 <> " " <> joinStrings (showL opts q) zz) [hh rr, hh pp, hh qq]
 
 -- | applies @p@ to lhs of the tuple and @q@ to the rhs and then @Ands@ them together
 --
@@ -314,7 +320,7 @@                 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 <> nullIf " | " zz) [hh rr, hh pp, hh qq]
+                in mkNodeB opts (p||q) (showL opts p <> " " <> msg0 <> " " <> joinStrings (showL opts q) zz) [hh rr, hh pp, hh qq]
 
 -- | applies @p@ to lhs of the tuple and @q@ to the rhs and then @Ors@ them together
 --
@@ -377,45 +383,111 @@           Right b' ->
             mkNode opts (Val (b,b')) msg0 [hh pp, hh pp']
 
--- | similar to 'Data.Function.on': may require kind signatures: Both is a better choice
+-- | similar to 'Data.Function.on'
 --
+-- >>> pz @(On' (==!) Len Fst (Reverse << Snd)) ("1ss","x2")
+-- Val GT
+--
+data On' (p :: Type -> Type -> k) q r s deriving Show
+
+instance ( P q (PP r x)
+         , P q (PP s x)
+         , P r x
+         , P s x
+         , P (p Fst Snd) (PP q (PP r x), PP q (PP s x))
+   ) => P (On' p q r s) x where
+  type PP (On' p q r s) x = PP (p Fst Snd) (PP q (PP r x), PP q (PP s x))
+  eval _ opts x = do
+    let msg0 = "On'"
+    lr <- runPQ NoInline msg0 (Proxy @r) (Proxy @s) opts x []
+    case lr of
+      Left e -> pure e
+      Right (r,s,rr,ss) -> do
+        let hhs = [hh rr, hh ss]
+        qq <- eval (Proxy @q) opts r
+        case getValueLR NoInline opts msg0 qq hhs of
+          Left e -> pure e
+          Right b -> do
+            qq' <- eval (Proxy @q) opts s
+            case getValueLR NoInline opts msg0 qq' (hhs ++ [hh qq]) of
+              Left e -> pure e
+              Right b' -> do
+                pp <- eval (Proxy @(p Fst Snd)) opts (b,b')
+                let hhs1 = hhs ++ [hh qq, hh qq']
+                pure $ case getValueLR NoInline opts msg0 pp hhs1 of
+                  Left e -> e
+                  Right _ -> mkNodeCopy opts pp msg0 hhs1 -- so we can preserve ValP
+
+-- | similar to 'Data.Function.on' for tuples
+--
 -- >>> pz @(On (==!) Len) ("1ss","x2") -- or use Comparing or Both+Compare
 -- Val GT
 --
 -- >>> pz @('(4,2) >> On (**) (FromIntegral _)) ()
 -- Val 16.0
 --
--- >>> pz @('(4,2) >> Both (FromIntegral _) >> Fst ** Snd) () -- equivalent to the above but easier on ghc
+-- >>> pz @('(4,2) >> Both (FromIntegral _) >> Fst ** Snd) () -- equivalent to the above
 -- Val 16.0
 --
 -- >>> pz @(On (+) (Id * Id) >> Id ** (1 % 2 >> FromRational _)) (3,4)
 -- Val 5.0
 --
--- >>> pz @(Both (Id * Id) >> ((Fst + Snd) ** (1 % 2 >> FromRational _))) (3,4) -- equivalent to the above but easier on ghc
+-- >>> pz @(Both (Id * Id) >> ((Fst + Snd) ** (1 % 2 >> FromRational _))) (3,4) -- equivalent to the above
 -- Val 5.0
 --
-data On (p :: Type -> Type -> k2) q deriving Show
+-- >>> pz @(On (<>) (Pure [] Id)) ('x','y')
+-- Val "xy"
+--
+-- >>> pz @(On (Flip (<>)) (Pure [] Id)) ('x','y')
+-- Val "yx"
+--
+-- >>> pz @(On (Flip (<>)) (Pure _ Id) >> '(Len,Head,Last)) ('x','y')
+-- Val (2,'y','x')
+--
+data On (p :: Type -> Type -> k) q deriving Show
+type OnT p q = On' p q Fst Snd
 
-instance ( P q a
-         , P q a'
-         , P (p Fst Snd) (PP q a, PP q a')
-   ) => P (On p q) (a,a') where
-  type PP (On p q) (a,a') = PP (p Fst Snd) (PP q a, PP q a')
-  eval _ opts (a,a') = do
-    let msg0 = "On"
-    qq <- eval (Proxy @q) opts a
-    case getValueLR NoInline opts msg0 qq [] of
-      Left e -> pure e
-      Right b -> do
-        qq' <- eval (Proxy @q) opts a'
-        case getValueLR NoInline opts msg0 qq' [hh qq] of
-          Left e -> pure e
-          Right b' -> do
-            pp <- eval (Proxy @(p Fst Snd)) opts (b,b')
-            pure $ case getValueLR NoInline opts msg0 pp [hh qq, hh qq'] of
-              Left e -> e
-              Right p -> mkNode opts (Val p) msg0 [hh qq, hh qq', hh pp]
+instance P (OnT p q) x => P (On p q) x where
+  type PP (On p q) x = PP (OnT p q) x
+  eval _ = eval (Proxy @(OnT p q))
 
+-- | similar to 'uncurry'
+--
+-- >>> pl @(Uncurry (==)) ('x','x')
+-- True (On')
+-- Val True
+--
+-- >>> pz @(Uncurry (.&.)) (7,15)
+-- Val 7
+--
+-- >>> pz @(Uncurry (+)) (7,15)
+-- Val 22
+--
+-- >>> pz @(Uncurry (*)) (7,15)
+-- Val 105
+--
+-- >>> pz @(Uncurry '(,)) (7,15)
+-- Val (7,15)
+--
+-- >>> pz @(Uncurry ('(,,) 4)) ('x',True)
+-- Val (4,'x',True)
+--
+-- >>> pz @(Uncurry (Flip '(,))) (1,'x')
+-- Val ('x',1)
+--
+-- >>> pz @(Uncurry (<>)) ("ab","def")
+-- Val "abdef"
+--
+-- >>> pz @(Uncurry (<>)) (SG.Sum 12,SG.Sum 99)
+-- Val (Sum {getSum = 111})
+--
+data Uncurry (p :: Type -> Type -> k) deriving Show
+type UncurryT p = On p Id
+
+instance P (UncurryT p) x => P (Uncurry p) x where
+  type PP (Uncurry p) x = PP (UncurryT p) x
+  eval _ = eval (Proxy @(UncurryT p))
+
 -- | create a @n@ tuple from a list or fail
 --
 -- >>> pz @(Tuple 4) "abcdefg"
@@ -441,21 +513,21 @@          , Show a
          ) => P (Tuple n) x where
   type PP (Tuple n) x = TupleT n (ExtractAFromList x)
-  eval _ opts as =
+  eval _ opts xs' =
     let msg0 = "Tuple(" ++ show n ++ ")"
         n = nat @n @Int
-    in pure $ case getTupleC @n as of
-         Left es -> mkNode opts (Fail (msg0 <> " not enough elements(" <> show (length as) <> ")")) (showVerbose opts " | " es) []
-         Right r -> mkNode opts (Val r) msg0 []
+    in pure $ case chkSize opts msg0 xs' [] of
+        Left e -> e
+        Right (xsLen,xs) ->
+          case getTupleC @n xs of
+            Nothing -> mkNode opts (Fail (msg0 <> " not enough elements(" <> show xsLen <> ")")) (showVerbose opts " | " xs) []
+            Just r -> mkNode opts (Val r) msg0 []
 
 -- | create a @n@ tuple from a list and return as an Either
 --
 -- >>> pz @(Tuple' 4) "abcdefg"
 -- Val (Right ('a','b','c','d'))
 --
--- >>> pz @(Tuple' 4) "abc"
--- Val (Left "abc")
---
 -- >>> pz @(Tuple' 4) []
 -- Val (Left [])
 --
@@ -478,13 +550,16 @@          , x ~ [a]
          ) => P (Tuple' n) x where
   type PP (Tuple' n) x = Either x (TupleT n (ExtractAFromList x))
-  eval _ opts as =
+  eval _ opts xs' =
     let msg0 = "Tuple'(" ++ show n ++ ")"
         n = nat @n @Int
-        lr = getTupleC @n as
-    in pure $ case lr of
-         Left e -> mkNode opts (Val (Left e)) (msg0 <> " not enough elements(" <> show (length as) <> ")") []
-         Right ret -> mkNode opts (Val (Right ret)) msg0 []
+    in pure $ case chkSize opts msg0 xs' [] of
+      Left e -> e
+      Right (xsLen,xs) ->
+        let lr = getTupleC @n xs
+        in case lr of
+             Nothing -> mkNode opts (Val (Left xs)) (msg0 <> " not enough elements(" <> show xsLen <> ")") []
+             Just ret -> mkNode opts (Val (Right ret)) msg0 []
 
 -- | run @p@ with inductive tuples
 --
@@ -599,9 +674,83 @@          , xs ~ [a]
          ) => P (ToITupleList n) xs where
   type PP (ToITupleList n) xs = ToITupleListP n (ExtractAFromTA xs)
-  eval _ opts xs =
+  eval _ opts xs' =
     let msg0 = "ToITupleList(" <> show n <> ")"
         n = nat @n @Int
-    in pure $ case toITupleListC @n @a xs of
-         Left e -> mkNode opts (Fail e) (msg0 <> " instead found " <> show (length xs)) []
-         Right d -> mkNode opts (Val d) msg0 []
+    in pure $ case chkSize opts msg0 xs' [] of
+         Left e -> e
+         Right (xsLen,xs) ->
+           case toITupleListC @n @a xs of
+             Left e -> mkNode opts (Fail e) (msg0 <> " instead found " <> show xsLen) []
+             Right d -> mkNode opts (Val d) msg0 []
+
+-- | assoc using 'AssocC'
+--
+-- >>> pz @Assoc (This (These 123 'x'))
+-- Val (These 123 (This 'x'))
+--
+-- >>> pz @Assoc ((99,'a'),True)
+-- Val (99,('a',True))
+--
+-- >>> pz @Assoc ((99,'a'),True)
+-- Val (99,('a',True))
+--
+-- >>> pz @Assoc (Right "Abc" :: Either (Either () ()) String)
+-- Val (Right (Right "Abc"))
+--
+-- >>> pz @Assoc (Left (Left 'x'))
+-- Val (Left 'x')
+--
+-- >>> pl @Assoc ((10,'c'),True)
+-- Present (10,('c',True)) (Assoc (10,('c',True)) | ((10,'c'),True))
+-- Val (10,('c',True))
+--
+-- >>> pl @(Assoc >> Unassoc) ((10,'c'),True)
+-- Present ((10,'c'),True) ((>>) ((10,'c'),True) | {Unassoc ((10,'c'),True) | (10,('c',True))})
+-- Val ((10,'c'),True)
+--
+data Assoc deriving Show
+
+instance ( AssocC p
+         , Show (p (p a b) c)
+         , Show (p a (p b c))
+         ) => P Assoc (p (p a b) c) where
+  type PP Assoc (p (p a b) c) = p a (p b c)
+  eval _ opts pabc =
+    let msg0 = "Assoc"
+        d = assoc pabc
+    in pure $ mkNode opts (Val d) (show3 opts msg0 d pabc) []
+
+-- | unassoc using 'AssocC'
+--
+-- >>> pz @Unassoc (These 123 (This 'x'))
+-- Val (This (These 123 'x'))
+--
+-- >>> pz @Unassoc (99,('a',True))
+-- Val ((99,'a'),True)
+--
+-- >>> pz @Unassoc (This 10 :: These Int (These Bool ()))
+-- Val (This (This 10))
+--
+-- >>> pz @Unassoc (Right (Right 123))
+-- Val (Right 123)
+--
+-- >>> pz @Unassoc (Left 'x' :: Either Char (Either Bool Double))
+-- Val (Left (Left 'x'))
+--
+-- >>> pl @Unassoc (10,('c',True))
+-- Present ((10,'c'),True) (Unassoc ((10,'c'),True) | (10,('c',True)))
+-- Val ((10,'c'),True)
+--
+data Unassoc deriving Show
+
+instance ( AssocC p
+         , Show (p (p a b) c)
+         , Show (p a (p b c))
+         ) => P Unassoc (p a (p b c)) where
+  type PP Unassoc (p a (p b c)) = p (p a b) c
+  eval _ opts pabc =
+    let msg0 = "Unassoc"
+        d = unassoc pabc
+    in pure $ mkNode opts (Val d) (show3 opts msg0 d pabc) []
+

@@ -0,0 +1,343 @@+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE NoStarIsType #-}
+{-# LANGUAGE EmptyDataDeriving #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveLift #-}
+-- | Elr definition
+module Predicate.Elr (
+ -- definition
+    Elr(..)
+
+ -- ** prisms
+  , _ENone
+  , _ELeft
+  , _ERight
+  , _EBoth
+
+ -- ** isos
+  , _elr2Maybe
+  , _elr2These
+
+ -- ** boolean predicates
+  , isENone
+  , isELeft
+  , isERight
+  , isEBoth
+
+ -- ** type families
+  , ENoneT
+  , ELeftT
+  , ERightT
+  , EBothT
+
+ -- ** miscellaneous
+  , getBifoldInfo
+  , showElr
+  , GetElr(..)
+  , partitionElr
+  , fromElr
+  , mergeElrWith
+  , elr
+ ) where
+import Predicate.Misc
+import qualified GHC.TypeLits as GL
+import GHC.TypeLits (ErrorMessage((:$$:),(:<>:)))
+import Control.Lens
+import Data.Bitraversable (Bitraversable(..))
+import Data.Bifoldable (Bifoldable(bifoldMap))
+import GHC.Generics (Generic)
+import Control.DeepSeq (NFData)
+import Control.Monad (ap)
+import qualified Language.Haskell.TH.Lift as TH
+import Data.These (These(..))
+-- $setup
+-- >>> import Predicate.Prelude
+-- >>> import qualified Data.Semigroup as SG
+
+-- | similar to 'Data.These' with an additional empty constructor to support a Monoid instance
+data Elr a b =
+     ENone -- ^ empty constructor
+   | ELeft !a  -- ^ similar to 'Data.These.This'
+   | ERight !b -- ^ similar to 'Data.These.That'
+   | EBoth !a !b -- ^ similar to 'Data.These.These'
+   deriving stock (Show,Eq,Ord,Foldable,Functor,Traversable,Generic,TH.Lift)
+   deriving anyclass NFData
+
+makePrisms ''Elr
+
+instance (Semigroup a, Semigroup b) => Semigroup (Elr a b) where
+  ENone <> x' = x'
+  x <> ENone = x
+  ELeft a <> ELeft a' = ELeft (a <> a')
+  ELeft a <> ERight b' = EBoth a b'
+  ELeft a <> EBoth a' b' = EBoth (a <> a') b'
+  ERight b <> ELeft a' = EBoth a' b
+  ERight b <> ERight b' = ERight (b <> b')
+  ERight b <> EBoth a' b' = EBoth a' (b <> b')
+  EBoth a b <> ELeft a' = EBoth (a <> a') b
+  EBoth a b <> ERight b' = EBoth a (b <> b')
+  EBoth a b <> EBoth a' b' = EBoth (a <> a') (b <> b')
+
+instance (Monoid a, Monoid b) => Monoid (Elr a b) where
+  mempty = ENone
+
+instance Semigroup x => Applicative (Elr x) where
+  pure = ERight
+  (<*>) = ap
+
+instance Semigroup x => Monad (Elr x) where
+  return = pure
+  ENone >>= _ = ENone
+  ELeft x >>= _ = ELeft x
+  ERight a >>= amb = amb a
+  EBoth x a >>= amb =
+    case amb a of
+      ENone -> ELeft x
+      ELeft y -> ELeft (x <> y)
+      ERight b -> EBoth x b
+      EBoth y b -> EBoth (x <> y) b
+
+instance Bifunctor Elr where
+  bimap f g =
+    \case
+      ENone -> ENone
+      ELeft a -> ELeft (f a)
+      ERight b -> ERight (g b)
+      EBoth a b -> EBoth (f a) (g b)
+
+instance Bifoldable Elr where
+  bifoldMap f g =
+    \case
+      ENone -> mempty
+      ELeft a -> f a
+      ERight b -> g b
+      EBoth a b -> f a <> g b
+
+instance Bitraversable Elr where
+  bitraverse f g =
+    \case
+      ENone -> pure ENone
+      ELeft a -> ELeft <$> f a
+      ERight b -> ERight <$> g b
+      EBoth a b -> EBoth <$> f a <*> g b
+
+-- | display constructor name for 'Elr'
+showElr :: Elr a b -> String
+showElr = \case
+  ENone -> "ENone"
+  ELeft {} -> "ELeft"
+  ERight {} -> "ERight"
+  EBoth {} -> "EBoth"
+
+-- | get 'Elr' from typelevel [type application order is a b then th if explicit kind for th else is first parameter!
+class GetElr (th :: Elr k k1) where
+  getElr :: (String, Elr w v -> Bool)
+instance GetElr 'ENone where
+  getElr = ("ENone", isENone)
+instance GetElr ('ELeft x) where
+  getElr = ("ELeft", isELeft)
+instance GetElr ('ERight y) where
+  getElr = ("ERight", isERight)
+instance GetElr ('EBoth x y) where
+  getElr = ("EBoth", isEBoth)
+
+isENone, isELeft, isERight, isEBoth :: Elr a b -> Bool
+-- | predicate on ENone
+isENone ENone = True
+isENone _ = False
+
+-- | predicate on ELeft
+isELeft ELeft {} = True
+isELeft _ = False
+
+-- | predicate on ERight
+isERight ERight {} = True
+isERight _ = False
+
+-- | predicate on EBoth
+isEBoth EBoth {} = True
+isEBoth _ = False
+
+-- | extract the relevant type for 'ENone'
+type family ENoneT lr where
+  ENoneT (Elr _ _) = ()
+  ENoneT o = GL.TypeError (
+      'GL.Text "ENoneT: expected 'Elr a b' "
+      ':$$: 'GL.Text "o = "
+      ':<>: 'GL.ShowType o)
+
+-- | extract the relevant type for 'ELeft'
+type family ELeftT lr where
+  ELeftT (Elr a _) = a
+  ELeftT o = GL.TypeError (
+      'GL.Text "ELeftT: expected 'Elr a b' "
+      ':$$: 'GL.Text "o = "
+      ':<>: 'GL.ShowType o)
+
+-- | extract the relevant type for 'ERight'
+type family ERightT lr where
+  ERightT (Elr _ b) = b
+  ERightT o = GL.TypeError (
+      'GL.Text "ERightT: expected 'Elr a b' "
+      ':$$: 'GL.Text "o = "
+      ':<>: 'GL.ShowType o)
+
+-- | extract the relevant types for 'EBoth'
+type family EBothT lr where
+  EBothT (Elr a b) = (a,b)
+  EBothT o = GL.TypeError (
+      'GL.Text "EBothT: expected 'Elr a b' "
+      ':$$: 'GL.Text "o = "
+      ':<>: 'GL.ShowType o)
+
+-- | partition Elr into 4 lists for each constructor: foldMap (yep ...)
+partitionElr :: [Elr a b] -> ([()], [a], [b], [(a,b)])
+partitionElr = foldMapStrict $
+  \case
+    ENone -> ([()],[],[],[])
+    ELeft a -> ([],[a],[],[])
+    ERight b -> ([],[],[b],[])
+    EBoth a b -> ([],[],[],[(a,b)])
+
+-- | convert Elr to a tuple with default values
+fromElr :: a -> b -> Elr a b -> (a,b)
+fromElr a b =
+  \case
+    ENone -> (a,b)
+    ELeft v -> (v,b)
+    ERight w -> (a,w)
+    EBoth v w -> (v,w)
+
+-- | iso from 'Elr' to 'These'
+--
+-- >>> ENone & _elr2These .~ Just (This 12)
+-- ELeft 12
+--
+-- >>> ELeft 123 & _elr2These %~ fmap swapC
+-- ERight 123
+--
+_elr2These :: Iso (Elr a b) (Elr a' b') (Maybe (These a b)) (Maybe (These a' b'))
+_elr2These = iso fw bw
+  where
+  fw = \case
+         ENone -> Nothing
+         ELeft a -> Just (This a)
+         ERight b -> Just (That b)
+         EBoth a b -> Just (These a b)
+  bw = \case
+         Nothing -> ENone
+         Just (This a) -> ELeft a
+         Just (That b) -> ERight b
+         Just (These a b) -> EBoth a b
+
+-- | iso from 'Elr' to a pair of 'Maybe's
+--
+-- >>> ENone ^. _elr2Maybe
+-- (Nothing,Nothing)
+--
+-- >>> ELeft 123 ^. _elr2Maybe
+-- (Just 123,Nothing)
+--
+-- >>> EBoth 1 'a' ^. _elr2Maybe
+-- (Just 1,Just 'a')
+--
+_elr2Maybe :: Iso (Elr a b) (Elr a' b') (Maybe a, Maybe b) (Maybe a', Maybe b')
+_elr2Maybe = iso fw bw
+  where
+  fw = \case
+          ENone -> (Nothing, Nothing)
+          ELeft a -> (Just a, Nothing)
+          ERight b -> (Nothing, Just b)
+          EBoth a b -> (Just a, Just b)
+  bw = \case
+          (Nothing, Nothing) -> ENone
+          (Just a, Nothing) -> ELeft a
+          (Nothing, Just b) -> ERight b
+          (Just a, Just b) -> EBoth a b
+
+-- | 'GetLen' instances for 'Elr'
+instance GetLen 'ENone where
+  getLen = 0
+instance GetLen ('ELeft a) where
+  getLen = 0
+instance GetLen ('ERight b) where
+  getLen = 1
+instance GetLen ('EBoth a b) where
+  getLen = 1
+
+-- | 'AssocC' instances for 'Elr'
+instance AssocC Elr where
+  assoc ENone = ENone
+  assoc (ELeft ENone) = ENone
+  assoc (ELeft (ELeft a)) = ELeft a
+  assoc (ELeft (ERight b)) = ERight (ELeft b)
+  assoc (ELeft (EBoth a b)) = EBoth a (ELeft b)
+  assoc (ERight c) = ERight (ERight c)
+  assoc (EBoth ENone c) = ERight (ERight c)
+  assoc (EBoth (ELeft a) c) = EBoth a (ERight c)
+  assoc (EBoth (ERight b) c) = ERight (EBoth b c)
+  assoc (EBoth (EBoth a b) c) = EBoth a (EBoth b c)
+
+  unassoc ENone = ENone
+  unassoc (ELeft a) = ELeft (ELeft a)
+  unassoc (ERight ENone) = ELeft ENone
+  unassoc (ERight (ELeft b)) = ELeft (ERight b)
+  unassoc (ERight (ERight c)) = ERight c
+  unassoc (ERight (EBoth b c)) = EBoth (ERight b) c
+  unassoc (EBoth a ENone) = ELeft (ELeft a)
+  unassoc (EBoth a (ELeft b)) = ELeft (EBoth a b)
+  unassoc (EBoth a (ERight c)) = EBoth (ELeft a) c
+  unassoc (EBoth a (EBoth b c)) = EBoth (EBoth a b) c
+
+instance SwapC Elr where
+  swapC =
+    \case
+      ENone -> ENone
+      ELeft a -> ERight a
+      ERight b -> ELeft b
+      EBoth a b -> EBoth b a
+
+-- | returns the filled status of a Bifoldable container
+getBifoldInfo :: Bifoldable bi => bi a b -> String
+getBifoldInfo bi =
+  case bifoldMap (const (ELeft ())) (const (ERight ())) bi of
+    ENone -> " <skipped>"
+    ELeft () -> "(L)"
+    ERight () -> "(R)"
+    EBoth () () -> "(B)"
+
+-- | similar to 'elr' without a separate EBoth combinator
+mergeElrWith :: c -> (a -> c) -> (b -> c) -> (c -> c -> c) -> Elr a b -> c
+mergeElrWith c fa fb fcc =
+  \case
+    ENone -> c
+    ELeft a -> fa a
+    ERight b -> fb b
+    EBoth a b -> fcc (fa a) (fb b)
+
+-- | destruct 'Elr'
+elr :: c -> (a -> c) -> (b -> c) -> (a -> b -> c) -> Elr a b -> c
+elr c fa fb fab =
+  \case
+    ENone -> c
+    ELeft a -> fa a
+    ERight b -> fb b
+    EBoth a b -> fab a b

@@ -45,7 +45,6 @@   , TheseT
   , FnT
   , ApplyConstT
-  , CheckT
   , JoinT
   , FailWhenT
   , FailUnlessT
@@ -126,8 +125,13 @@   , _Id
   , sum'
   , product'
+  , foldMapStrict
   , cycle'
   , cmpOf
+  , ifM
+  , AssocC(..)
+  , simpleAlign
+  , getValidBase
   ) where
 import qualified GHC.TypeNats as GN
 import GHC.TypeLits (Symbol,Nat,KnownSymbol,KnownNat,ErrorMessage((:$$:),(:<>:)))
@@ -156,9 +160,8 @@ import Data.Char (isSpace)
 import qualified Control.Exception as E
 import Data.Tree (Tree(Node))
-import Control.Lens (Identity(..), Lens)
+import Control.Lens
 import qualified Data.Semigroup as SG
-import Data.Bifunctor (Bifunctor)
 -- $setup
 -- >>> :set -XDataKinds
 -- >>> :set -XTypeApplications
@@ -219,7 +222,7 @@ -- >>> getLen @('This 1)
 -- 0
 --
-class GetLen xs where -- (xs :: [k]) will break it! ghc 8.6.5
+class GetLen xs where
   getLen :: Int
 instance GetLen '[] where
   getLen = 0
@@ -250,7 +253,7 @@   These {} -> "These"
 
 -- | get 'These' from typelevel
-class GetThese th where
+class GetThese (th :: These a b) where
   getThese :: (String, These w v -> Bool)
 instance GetThese ('This x) where
   getThese = ("This", isThis)
@@ -421,7 +424,7 @@ -- >>> toITupleListC @2 [10,12,13,1]
 -- Left "toITupleListC: expected exactly 2 values"
 --
-class ToITupleListC (n :: Nat) a where
+class ToITupleListC (n :: Nat) (a :: Type) where
   type ToITupleListP n a
   toITupleListC :: [a] -> Either String (ToITupleListP n a)
 instance (GL.TypeError ('GL.Text "ToITupleListC: inductive tuple cannot be empty")) => ToITupleListC 0 a where
@@ -476,7 +479,7 @@   toITupleListC [a,b,c,d,e,f,g,h,i,j,k,l] = Right (a,(b,(c,(d,(e,(f,(g,(h,(i,(j,(k,(l,()))))))))))))
   toITupleListC _ = Left "toITupleListC: expected exactly 12 values"
 
-class ReverseITupleC x xs ys where
+class ReverseITupleC (x :: Type) (xs :: Type) (ys :: Type) where
   type ReverseITupleT x xs ys
   reverseITupleC :: x -> xs -> ys -> ReverseITupleT x xs ys
 instance ReverseITupleC x () ys  where
@@ -486,13 +489,13 @@   type ReverseITupleT x (w,ws) ys = (ReverseITupleT w ws (x,ys))
   reverseITupleC x (w,ws) ys = reverseITupleC w ws (x,ys)
 
--- partially apply the 2nd arg to an ADT -- $ and & work with functions only
--- doesnt apply more than once because we need to eval it
+-- | type level application: see 'Predicate.Core.$' which works for type level functions
 type family (p :: k -> k1) %% (q :: k) :: k1 where
   p %% q = p q
 
 infixl 9 %%
 
+-- | reverse type level application: see 'Predicate.Core.&' which works for type level functions
 type family (p :: k) %& (q :: k -> k1) :: k1 where
   p %& q = q p
 
@@ -575,8 +578,6 @@       ':$$: 'GL.Text "t a = "
       ':<>: 'GL.ShowType z)
 
-
--- todo: get ExtractAFromList failure to fire if wrong Type
 -- | type family to extract @a@ from a list of @a@
 type family ExtractAFromList (as :: Type) :: Type where
   ExtractAFromList [a] = a
@@ -585,6 +586,7 @@       ':$$: 'GL.Text "as = "
       ':<>: 'GL.ShowType z)
 
+-- | extract @a@ from a Maybe container
 type family MaybeT mb where
   MaybeT (Maybe a) = a
   MaybeT o = GL.TypeError (
@@ -592,7 +594,7 @@       ':$$: 'GL.Text "o = "
       ':<>: 'GL.ShowType o)
 
-
+-- | extract @a@ from a Either container
 type family LeftT lr where
   LeftT (Either a _) = a
   LeftT o = GL.TypeError (
@@ -600,6 +602,7 @@       ':$$: 'GL.Text "o = "
       ':<>: 'GL.ShowType o)
 
+-- | extract @b@ from a Either container
 type family RightT lr where
   RightT (Either _a b) = b
   RightT o = GL.TypeError (
@@ -607,6 +610,7 @@       ':$$: 'GL.Text "o = "
       ':<>: 'GL.ShowType o)
 
+-- | extract @a@ from a These container
 type family ThisT lr where
   ThisT (These a _b) = a
   ThisT o = GL.TypeError (
@@ -614,6 +618,7 @@       ':$$: 'GL.Text "o = "
       ':<>: 'GL.ShowType o)
 
+-- | extract @b@ from a These container
 type family ThatT lr where
   ThatT (These _a b) = b
   ThatT o = GL.TypeError (
@@ -621,6 +626,7 @@       ':$$: 'GL.Text "o = "
       ':<>: 'GL.ShowType o)
 
+-- | extract @a@ and @b@ from a These container
 type family TheseT lr where
   TheseT (These a b) = (a,b)
   TheseT o = GL.TypeError (
@@ -628,6 +634,7 @@       ':$$: 'GL.Text "o = "
       ':<>: 'GL.ShowType o)
 
+-- | extract @b@ from an arrow type
 type family FnT ab :: Type where
   FnT (_a -> b) = b
   FnT ab = GL.TypeError (
@@ -645,8 +652,7 @@        ':<>: 'GL.ShowType tb)
 
 type family ApplyConstT (ta :: Type) (b :: Type) :: Type where
---type family ApplyConstT ta b where -- less restrictive so allows ('Just Int) Bool through!
-  ApplyConstT (t _a) b = t b
+  ApplyConstT (t _) b = t b
   ApplyConstT ta b = GL.TypeError (
        'GL.Text "ApplyConstT: (t a) b but found something else"
        ':$$: 'GL.Text "t a = "
@@ -654,10 +660,6 @@        ':$$: 'GL.Text "b = "
        ':<>: 'GL.ShowType b)
 
-type family CheckT (tp :: Type) :: Bool where
-  CheckT () = GL.TypeError ('GL.Text "Printfn: inductive tuple cannot be empty")
-  CheckT _o = 'True
-
 errorInProgram :: HasCallStack => String -> x
 errorInProgram s = error $ "programmer error:" <> s
 
@@ -680,7 +682,7 @@ infixr 1 ~>
 
 -- | extract element 1 from a n-tuple
-class ExtractL1C tp where
+class ExtractL1C (tp :: Type) where
   type ExtractL1T tp
   extractL1C :: tp -> ExtractL1T tp
 instance ExtractL1C (a,b) where
@@ -706,7 +708,7 @@   extractL1C (a,_,_,_,_,_,_,_) = a
 
 -- | extract element 2 from a n-tuple
-class ExtractL2C tp where
+class ExtractL2C (tp :: Type) where
   type ExtractL2T tp
   extractL2C :: tp -> ExtractL2T tp
 instance ExtractL2C (a,b) where
@@ -732,7 +734,7 @@   extractL2C (_,b,_,_,_,_,_,_) = b
 
 -- | extract element 3 from a n-tuple
-class ExtractL3C tp where
+class ExtractL3C (tp :: Type) where
   type ExtractL3T tp
   extractL3C :: tp -> ExtractL3T tp
 instance ExtractL3C (a,b) where
@@ -758,7 +760,7 @@   extractL3C (_,_,c,_,_,_,_,_) = c
 
 -- | extract element 4 from a n-tuple
-class ExtractL4C tp where
+class ExtractL4C (tp :: Type) where
   type ExtractL4T tp
   extractL4C :: tp -> ExtractL4T tp
 instance ExtractL4C (a,b) where
@@ -784,7 +786,7 @@   extractL4C (_,_,_,d,_,_,_,_) = d
 
 -- | extract element 5 from a n-tuple
-class ExtractL5C tp where
+class ExtractL5C (tp :: Type) where
   type ExtractL5T tp
   extractL5C :: tp -> ExtractL5T tp
 instance ExtractL5C (a,b) where
@@ -810,7 +812,7 @@   extractL5C (_,_,_,_,e,_,_,_) = e
 
 -- | extract element 6 from a n-tuple
-class ExtractL6C tp where
+class ExtractL6C (tp :: Type) where
   type ExtractL6T tp
   extractL6C :: tp -> ExtractL6T tp
 instance ExtractL6C (a,b) where
@@ -836,7 +838,7 @@   extractL6C (_,_,_,_,_,f,_,_) = f
 
 -- | extract element 7 from a n-tuple
-class ExtractL7C tp where
+class ExtractL7C (tp :: Type) where
   type ExtractL7T tp
   extractL7C :: tp -> ExtractL7T tp
 instance ExtractL7C (a,b) where
@@ -862,7 +864,7 @@   extractL7C (_,_,_,_,_,_,g,_) = g
 
 -- | extract element 8 from a n-tuple
-class ExtractL8C tp where
+class ExtractL8C (tp :: Type) where
   type ExtractL8T tp
   extractL8C :: tp -> ExtractL8T tp
 instance ExtractL8C (a,b) where
@@ -888,86 +890,86 @@   extractL8C (_,_,_,_,_,_,_,h) = h
 
 -- | try to convert a list to a n-tuple
-class TupleC (n :: Nat) a where
+class TupleC (n :: Nat) (a :: Type) where
   type TupleT n a
-  getTupleC :: [a] -> Either [a] (TupleT n a)
+  getTupleC :: [a] -> Maybe (TupleT n a)
 
 -- | convert a list of at least 2 elements to a 2-tuple
 instance TupleC 2 a where
   type TupleT 2 a = (a,a)
   getTupleC = \case
-                a:b:_ -> Right (a,b)
-                o -> Left o
+                a:b:_ -> Just (a,b)
+                _ -> Nothing
 
 -- | convert a list of at least 3 elements to a 3-tuple
 instance TupleC 3 a where
   type TupleT 3 a = (a,a,a)
   getTupleC = \case
-                a:b:c:_ -> Right (a,b,c)
-                o -> Left o
+                a:b:c:_ -> Just (a,b,c)
+                _ -> Nothing
 
 -- | convert a list of at least 4 elements to a 4-tuple
 instance TupleC 4 a where
   type TupleT 4 a = (a,a,a,a)
   getTupleC = \case
-                a:b:c:d:_ -> Right (a,b,c,d)
-                o -> Left o
+                a:b:c:d:_ -> Just (a,b,c,d)
+                _ -> Nothing
 
 -- | convert a list of at least 5 elements to a 5-tuple
 instance TupleC 5 a where
   type TupleT 5 a = (a,a,a,a,a)
   getTupleC = \case
-                a:b:c:d:e:_ -> Right (a,b,c,d,e)
-                o -> Left o
+                a:b:c:d:e:_ -> Just (a,b,c,d,e)
+                _ -> Nothing
 
 -- | convert a list of at least 6 elements to a 6-tuple
 instance TupleC 6 a where
   type TupleT 6 a = (a,a,a,a,a,a)
   getTupleC = \case
-                a:b:c:d:e:f:_ -> Right (a,b,c,d,e,f)
-                o -> Left o
+                a:b:c:d:e:f:_ -> Just (a,b,c,d,e,f)
+                _ -> Nothing
 
 -- | convert a list of at least 7 elements to a 7-tuple
 instance TupleC 7 a where
   type TupleT 7 a = (a,a,a,a,a,a,a)
   getTupleC = \case
-                a:b:c:d:e:f:g:_ -> Right (a,b,c,d,e,f,g)
-                o -> Left o
+                a:b:c:d:e:f:g:_ -> Just (a,b,c,d,e,f,g)
+                _ -> Nothing
 
 -- | convert a list of at least 8 elements to a 8-tuple
 instance TupleC 8 a where
   type TupleT 8 a = (a,a,a,a,a,a,a,a)
   getTupleC = \case
-                a:b:c:d:e:f:g:h:_ -> Right (a,b,c,d,e,f,g,h)
-                o -> Left o
+                a:b:c:d:e:f:g:h:_ -> Just (a,b,c,d,e,f,g,h)
+                _ -> Nothing
 
 -- | convert a list of at least 9 elements to a 9-tuple
 instance TupleC 9 a where
   type TupleT 9 a = (a,a,a,a,a,a,a,a,a)
   getTupleC = \case
-                a:b:c:d:e:f:g:h:i:_ -> Right (a,b,c,d,e,f,g,h,i)
-                o -> Left o
+                a:b:c:d:e:f:g:h:i:_ -> Just (a,b,c,d,e,f,g,h,i)
+                _ -> Nothing
 
 -- | convert a list of at least 10 elements to a 10-tuple
 instance TupleC 10 a where
   type TupleT 10 a = (a,a,a,a,a,a,a,a,a,a)
   getTupleC = \case
-                a:b:c:d:e:f:g:h:i:j:_ -> Right (a,b,c,d,e,f,g,h,i,j)
-                o -> Left o
+                a:b:c:d:e:f:g:h:i:j:_ -> Just (a,b,c,d,e,f,g,h,i,j)
+                _ -> Nothing
 
 -- | convert a list of at least 11 elements to a 11-tuple
 instance TupleC 11 a where
   type TupleT 11 a = (a,a,a,a,a,a,a,a,a,a,a)
   getTupleC = \case
-                a:b:c:d:e:f:g:h:i:j:k:_ -> Right (a,b,c,d,e,f,g,h,i,j,k)
-                o -> Left o
+                a:b:c:d:e:f:g:h:i:j:k:_ -> Just (a,b,c,d,e,f,g,h,i,j,k)
+                _ -> Nothing
 
 -- | convert a list of at least 12 elements to a 12-tuple
 instance TupleC 12 a where
   type TupleT 12 a = (a,a,a,a,a,a,a,a,a,a,a,a)
   getTupleC = \case
-                a:b:c:d:e:f:g:h:i:j:k:l:_ -> Right (a,b,c,d,e,f,g,h,i,j,k,l)
-                o -> Left o
+                a:b:c:d:e:f:g:h:i:j:k:l:_ -> Just (a,b,c,d,e,f,g,h,i,j,k,l)
+                _ -> Nothing
 
 -- | prime predicate
 --
@@ -1046,7 +1048,7 @@ --
 -- >>> getNats @'[10,12,1]
 -- [10,12,1]
-class GetNats as where
+class GetNats (as :: [Nat]) where
   getNats :: [Int]
 instance GetNats '[] where
   getNats = []
@@ -1060,7 +1062,7 @@ -- >>> getSymbs @'["abc","def","g"]
 -- ["abc","def","g"]
 --
-class GetSymbs ns where
+class GetSymbs (ns :: [Symbol]) where
   getSymbs :: [String]
 instance GetSymbs '[] where
   getSymbs = []
@@ -1094,8 +1096,10 @@ data ROpt =
     Anchored -- ^ Force pattern anchoring
   | AutoCallout -- ^ Compile automatic callouts
---  | BsrAnycrlf --  \R matches only CR, LF, or CrlF
---  | BsrUnicode -- ^ \R matches all Unicode line endings
+{-
+  | BsrAnycrlf -- ^ \R matches only CR, LF, or CrlF
+  | BsrUnicode -- ^ \R matches all Unicode line endings
+-}
   | Caseless -- ^ Do caseless matching
   | DollarEndonly -- ^ dollar not to match newline at end
   | Dotall -- ^ matches anything including NL
@@ -1104,8 +1108,10 @@   | Extra -- ^ PCRE extra features (not much use currently)
   | Firstline -- ^ Force matching to be before newline
   | Multiline -- ^ caret and dollar match newlines within data
---  | NewlineAny -- ^ Recognize any Unicode newline sequence
---  | NewlineAnycrlf -- ^ Recognize CR, LF, and CrlF as newline sequences
+{-
+  | NewlineAny -- ^ Recognize any Unicode newline sequence
+  | NewlineAnycrlf -- ^ Recognize CR, LF, and CrlF as newline sequences
+-}
   | NewlineCr -- ^ Set CR as the newline sequence
   | NewlineCrlf -- ^ Set CrlF as the newline sequence
   | NewlineLf -- ^ Set LF as the newline sequence
@@ -1327,8 +1333,91 @@ product' :: (Foldable t, Num a) => t a -> a
 product' = foldl' (*) 1
 
+-- | strict version of 'Data.Foldable.foldMap': replace with Data.Foldable.foldMap' when more generally available
+foldMapStrict :: (Foldable t, Monoid m) => (a -> m) -> t a -> m
+foldMapStrict f = foldl' (\z a -> z <> f a) mempty
+
 cmpOf :: Eq a => Ordering -> ([a] -> [a] -> Bool, String)
 cmpOf = \case
            LT -> (isPrefixOf, "IsPrefix")
            EQ -> (isInfixOf, "IsInfix")
            GT -> (isSuffixOf, "IsSuffix")
+
+-- | lifted if statement
+ifM :: Monad m => m Bool -> m a -> m a -> m a
+ifM mb mt mf = do
+  b <- mb
+  if b then mt else mf
+
+
+class AssocC p where
+  assoc :: p (p a b) c -> p a (p b c)
+  unassoc :: p a (p b c) -> p (p a b) c
+instance AssocC Either where
+  assoc (Left (Left a)) = Left a
+  assoc (Left (Right b)) = Right (Left b)
+  assoc (Right b) = Right (Right b)
+
+  unassoc (Left a) = Left (Left a)
+  unassoc (Right (Left b)) = Left (Right b)
+  unassoc (Right (Right b)) = Right b
+instance AssocC These where
+  assoc (This (This a)) = This a
+  assoc (This (That b)) = That (This b)
+  assoc (This (These a b)) = These a (This b)
+  assoc (That c) = That (That c)
+  assoc (These (This a) c) = These a (That c)
+  assoc (These (That b) c) = That (These b c)
+  assoc (These (These a b) c) = These a (These b c)
+
+  unassoc (This a) = This (This a)
+  unassoc (That (This b)) = This (That b)
+  unassoc (That (That c)) = That c
+  unassoc (That (These b c)) = These (That b) c
+  unassoc (These a (This b)) = This (These a b)
+  unassoc (These a (That c)) = These (This a) c
+  unassoc (These a (These b c)) = These (These a b) c
+
+instance AssocC (,) where
+  assoc ((a,b),c) = (a,(b,c))
+  unassoc (a,(b,c)) = ((a,b),c)
+
+-- | zip two lists using These
+--
+-- >>> simpleAlign "ab" ""
+-- [This 'a',This 'b']
+--
+-- >>> simpleAlign "" "ab"
+-- [That 'a',That 'b']
+--
+-- >>> simpleAlign [1] "ab"
+-- [These 1 'a',That 'b']
+--
+-- >>> simpleAlign [] []
+-- []
+--
+-- >>> simpleAlign [1,2] "ab"
+-- [These 1 'a',These 2 'b']
+--
+simpleAlign :: [a] -> [b] -> [These a b]
+simpleAlign as [] = map This as
+simpleAlign [] bs = map That bs
+simpleAlign (a:as) (b:bs) = These a b : simpleAlign as bs
+
+-- | get base values for n between 2 and 36
+--
+-- >>> getValidBase 36
+-- "0123456789abcdefghijklmnopqrstuvwxyz"
+--
+-- >>> getValidBase 2
+-- "01"
+--
+-- >>> getValidBase 8
+-- "01234567"
+--
+getValidBase :: Int -> String
+getValidBase n
+  | n < 2 = errorInProgram $ "getValidBase: oops invalid base: found n<2 ie " ++ show n
+  | n > 36 = errorInProgram $ "getValidBase: oops invalid base: found n>36 ie " ++ show n
+  | otherwise = take n (['0'..'9'] <> ['a'..'z'])
+

@@ -1,13 +1,15 @@ -- | Dsl for evaluating and displaying type level expressions
 module Predicate.Prelude (
     module Predicate.Core
-  , module Predicate.Util
+  , module Predicate.Elr
   , module Predicate.Misc
+  , module Predicate.Util
   , module Predicate.Data.Bits
   , module Predicate.Data.Char
   , module Predicate.Data.Condition
   , module Predicate.Data.DateTime
   , module Predicate.Data.Either
+  , module Predicate.Data.Elr
   , module Predicate.Data.Enum
   , module Predicate.Data.Extra
   , module Predicate.Data.Foldable
@@ -29,6 +31,7 @@   , module Predicate.Data.Tuple
  ) where
 import Predicate.Core
+import Predicate.Elr
 import Predicate.Misc
 import Predicate.Util
 import Predicate.Data.Bits
@@ -36,6 +39,7 @@ import Predicate.Data.Condition
 import Predicate.Data.DateTime
 import Predicate.Data.Either
+import Predicate.Data.Elr
 import Predicate.Data.Enum
 import Predicate.Data.Extra
 import Predicate.Data.Foldable

@@ -233,8 +233,9 @@         case ma of
           Nothing ->
              let o = getOpt @opts
-             in if cnt >= oRecursion o
-                then error $ setOtherEffects o ("genRefined recursion exceeded(" ++ show (oRecursion o) ++ ")")
+                 r = getMaxRecursionValue o
+             in if cnt >= r
+                then error $ setOtherEffects o ("genRefined recursion exceeded(" ++ show r ++ ")")
                 else f (cnt+1)
           Just a -> pure $ unsafeRefined a
   in f 0

@@ -309,9 +309,10 @@         mi <- suchThatMaybe g (isJust . snd . runIdentity . eval2M @opts @ip @op)
         case mi of
           Nothing ->
-             if cnt >= oRecursion o
-             then error $ setOtherEffects o ("genRefined2P recursion exceeded(" ++ show (oRecursion o) ++ ")")
-             else f (cnt+1)
+             let r = getMaxRecursionValue o
+             in if cnt >= r
+                then error $ setOtherEffects o ("genRefined2P recursion exceeded(" ++ show r ++ ")")
+                else f (cnt+1)
           Just i ->
              case newRefined2 i of
                Left e -> errorInProgram $ "conversion failed:" ++ show e
@@ -497,7 +498,7 @@                  } deriving Eq
 
 instance Show Msg2 where
-  show (Msg2 a b c _d) = a <> nullIf " | " b <> nullIf "\n" c
+  show (Msg2 a b c _d) = joinStrings a b <> nullIf "\n" c
 
 -- | format the output from creating a 'Refined2' value into 'Msg2'
 prt2Impl :: forall a . Show a

@@ -326,8 +326,9 @@         case mppi of
           Nothing ->
              let o = getOpt @opts
-             in if cnt >= oRecursion o
-                then error $ setOtherEffects o ("genRefined3P recursion exceeded(" ++ show (oRecursion o) ++ ")")
+                 r = getMaxRecursionValue o
+             in if cnt >= r
+                then error $ setOtherEffects o ("genRefined3P recursion exceeded(" ++ show r ++ ")")
                 else f (cnt+1)
           Just ppi ->
              case evalQuick @opts @fmt ppi of
@@ -587,7 +588,7 @@                  } deriving Eq
 
 instance Show Msg3 where
-  show (Msg3 a b c _d) = a <> nullIf " | " b <> nullIf "\n" c
+  show (Msg3 a b c _d) = joinStrings a b <> nullIf "\n" c
 
 prt3Impl :: forall a . Show a
   => POpts

@@ -55,7 +55,6 @@ import Predicate.Refined2 (Msg2(..), RResults2(..), prt2Impl, Refined2C)
 import Predicate.Refined (RefinedC)
 import Predicate.Core
-import Predicate.Misc
 import Predicate.Util
 import Data.Proxy (Proxy(..))
 import Data.Aeson (ToJSON(..), FromJSON(..))
@@ -279,8 +278,9 @@         case mi of
           Nothing ->
              let o = getOpt @opts
-             in if cnt >= oRecursion o
-                then error $ setOtherEffects o ("genRefined5P recursion exceeded(" ++ show (oRecursion o) ++ ")")
+                 r = getMaxRecursionValue o
+             in if cnt >= r
+                then error $ setOtherEffects o ("genRefined5P recursion exceeded(" ++ show r ++ ")")
              else f (cnt+1)
           Just i -> pure $ unsafeRefined5 i
   in f 0
@@ -445,7 +445,7 @@           in if all isSpace zz then "FalseP" else "{" <> zz <> "}"
       w = case lr of
             Right True -> Right i
-            Right False -> Left $ "false boolean check" ++ nullIf " | " z
-            Left e -> Left $ "failed boolean check " ++ nullIf " | " e
+            Right False -> Left $ joinStrings "false boolean check" z
+            Left e -> Left $ joinStrings "failed boolean check " e
   in left (++ ("\n" ++ prtTreePure opts p2)) w
 

@@ -10,6 +10,7 @@ import Data.Fixed (Fixed(..))
 import qualified Language.Haskell.TH.Lift as TL
 import Data.Proxy (Proxy)
+import Data.These (These(..))
 
 deriving instance Lift Day
 deriving instance Lift LocalTime
@@ -17,6 +18,8 @@ deriving instance Lift TimeZone
 deriving instance Lift TimeOfDay
 deriving instance Lift (Fixed a)
+deriving instance Lift Ordering
+deriving instance (Lift a, Lift b) => Lift (These a b)
 
 $(TL.deriveLift ''DiffTime)
 

@@ -1,3 +1,4 @@+{-# LANGUAGE NumericUnderscores #-}
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE DeriveLift #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
@@ -103,9 +104,7 @@   , OptC
   , type OptT
   , getOpt
-  , subopts
-  , _DVerbose
-  , _Debug
+  , zeroToLite
   , defOpts
 
 -- ** formatting functions
@@ -118,6 +117,7 @@   , litL
   , litBL
   , litBS
+  , joinStrings
 
  -- ** printing methods
   , prtTreePure
@@ -132,6 +132,8 @@   , chkSize
   , chkSize2
   , badLength
+  , getMaxRecursionValue
+  , lengthGreaterThanOne
   ) where
 import Predicate.Misc
 import GHC.TypeLits (Symbol, Nat, KnownSymbol, KnownNat)
@@ -160,6 +162,7 @@ import GHC.Generics (Generic, Generic1)
 import qualified Language.Haskell.TH.Lift as TH
 import Instances.TH.Lift ()
+import Data.Kind (Type)
 -- $setup
 -- >>> :set -XDataKinds
 -- >>> :set -XTypeApplications
@@ -190,23 +193,23 @@ 
 -- | concatenate two strings with delimiter
 --
--- >>> jamSS "xyz" "abc"
+-- >>> joinStrings "xyz" "abc"
 -- "xyz | abc"
 --
--- >>> jamSS "" "abc"
+-- >>> joinStrings "" "abc"
 -- "abc"
 --
--- >>> jamSS "xyz" ""
+-- >>> joinStrings "xyz" ""
 -- "xyz"
 --
--- >>> jamSS "" ""
+-- >>> joinStrings "" ""
 -- ""
 --
-jamSS :: String -> String -> String
-jamSS s s1 = s <> (if null s || null s1 then "" else " | ") <> s1
+joinStrings :: String -> String -> String
+joinStrings s s1 = s <> (if null s || null s1 then "" else " | ") <> s1
 
 instance Semigroup PE where
-  PE b s <> PE b1 s1 = PE (b <> b1) (jamSS s s1)
+  PE b s <> PE b1 s1 = PE (b <> b1) (joinStrings s s1)
 
 -- | semigroup for ValP
 --
@@ -235,7 +238,7 @@ -- FailP "abc | xyz | def"
 --
 instance Semigroup ValP where
-   FailP s <> FailP s1 = FailP (jamSS s s1)
+   FailP s <> FailP s1 = FailP (joinStrings s s1)
    FailP s <> _ = FailP s
    _ <> FailP s = FailP s
    FalseP <> _ = FalseP
@@ -290,7 +293,7 @@ -- True
 --
 instance Semigroup (Val a) where
-   Fail s <> Fail s1 = Fail (jamSS s s1)
+   Fail s <> Fail s1 = Fail (joinStrings s s1)
    Fail s <> _ = Fail s
    _ <> Fail s = Fail s
    Val _ <> Val b = Val b
@@ -335,7 +338,7 @@ 
 instance Semigroup (TT a) where
    TT bp bt ss ts <> TT bp1 bt1 ss1 ts1 =
-     TT (bp <> bp1) (bt <> bt1) (jamSS ss ss1) (ts <> ts1)
+     TT (bp <> bp1) (bt <> bt1) (joinStrings ss ss1) (ts <> ts1)
 
 instance Monoid a => Monoid (TT a) where
    mempty = TT mempty mempty mempty mempty
@@ -352,7 +355,7 @@   z@(TT bp bt ss ts) >>= amb =
      case bt of
        Val a -> fixTTValP bp $ amb a
-                  & ttString %~ jamSS ss
+                  & ttString %~ joinStrings ss
                   & ttForest %~ (ts <>)
        Fail e -> z { _ttVal = Fail e }
 
@@ -362,7 +365,8 @@        -> String
        -> [Tree PE]
        -> TT a
-mkNodeCopy opts = mkNodeImpl opts . (_ttValP &&& _ttVal)
+mkNodeCopy opts tt msg pes =
+  mkNodeImpl opts (_ttValP tt, _ttVal tt) msg (pes <> [hh tt])
 
 -- | creates a Node for the evaluation tree
 mkNode :: POpts
@@ -432,6 +436,7 @@ hh :: TT a -> Tree PE
 hh (TT bp bt ss tt) = Node (PE (validateValP bp bt) ss) tt
 
+-- | flag for deciding whether to inline a tree or extend it
 data Inline = Inline | NoInline deriving (Show, Eq)
 
 -- | decorate the tree with more detail when there are errors but inline the error node
@@ -444,7 +449,7 @@ getValueLR inline opts msg0 tt hs =
 -- hack: if infix ...
   let ts = if _ttString tt `isInfixOf` msg0 then "" else _ttString tt
-      xs = ts <> (if null ts || null msg0 then "" else " | ") <> msg0
+      xs = joinStrings ts msg0
       tts = case inline of
               Inline -> hs <> _ttForest tt
               NoInline -> hs <> [hh tt]
@@ -452,7 +457,7 @@ 
 
 -- | elide the 'Identity' wrapper so it acts like a normal ADT
-type family HKD f a where
+type family HKD (f :: Type -> Type) (a :: Type) where
   HKD Identity a = a
   HKD f a = f a
 
@@ -466,7 +471,9 @@         , oDisp :: !(HKD f Disp) -- ^ display the tree using the normal tree or unicode
         , oColor :: !(HKD f (String, PColor)) -- ^ color palette used
         , oMsg :: ![String] -- ^ messages associated with type
-        , oRecursion :: !(HKD f Int) -- ^ max recursion
+        , oRecursion :: !(HKD f Int) -- ^ max recursion for small values
+        , oRecursionLarge :: !(HKD f Int) -- ^ max recursion for large values eg for Text
+        , oLarge :: !(HKD f Bool) -- ^ use large value recursion
         , oOther :: !(HKD f (Bool, SColor, SColor)) -- ^ other message effects
         , oNoColor :: !(HKD f Bool) -- ^ no colors
         }
@@ -485,7 +492,7 @@   , Show (HKD f (Bool, SColor, SColor))
   ) => Show (HOpts f)
 
--- | combine options ala monoid
+-- | convert to a usable option using defaults to fill in any gaps
 reifyOpts :: HOpts Last -> HOpts Identity
 reifyOpts h =
   HOpts (fromMaybe (oWidth defOpts) (coerce (oWidth h)))
@@ -497,6 +504,8 @@         )
         (oMsg defOpts <> oMsg h)
         (fromMaybe (oRecursion defOpts) (coerce (oRecursion h)))
+        (fromMaybe (oRecursionLarge defOpts) (coerce (oRecursionLarge h)))
+        (fromMaybe (oLarge defOpts) (coerce (oLarge h)))
         (if fromMaybe (oNoColor defOpts) (coerce (oNoColor h))
            then otherDef
            else fromMaybe (oOther defOpts) (coerce (oOther h))
@@ -511,10 +520,18 @@ setMessage :: String -> HOpts Last
 setMessage s = mempty { oMsg = pure s }
 
--- | set maximum recursion eg when running regex
+-- | set maximum recursion for small values eg when running regex
 setRecursion :: Int -> HOpts Last
 setRecursion i = mempty { oRecursion = pure i }
 
+-- | set maximum recursion for large values
+setRecursionLarge :: Int -> HOpts Last
+setRecursionLarge i = mempty { oRecursionLarge = pure i }
+
+-- | set maximum recursion eg when running regex
+setLarge :: Bool -> HOpts Last
+setLarge b = mempty { oLarge = pure b }
+
 -- | set color of title message
 setOther :: Bool
          -> Color
@@ -554,12 +571,11 @@ setDebug d =
   mempty { oDebug = pure d }
 
--- | monoid opts
 instance Monoid (HOpts Last) where
-  mempty = HOpts mempty mempty mempty mempty mempty mempty mempty mempty
+  mempty = HOpts mempty mempty mempty mempty mempty mempty mempty mempty mempty mempty
 
 instance Semigroup (HOpts Last) where
-  HOpts a b c d e f g h <> HOpts a' b' c' d' e' f' g' h'
+  HOpts a b c d e f g h i j <> HOpts a' b' c' d' e' f' g' h' i' j'
      = HOpts (a <> a')
              (b <> b')
              (c <> c')
@@ -568,6 +584,8 @@              (f <> f')
              (g <> g')
              (h <> h')
+             (i <> i')
+             (j <> j')
 
 --seqPOptsM :: HOpts Last -> Maybe (HOpts Identity)
 --seqPOptsM h = coerce (HOpts <$> oWidth h <*> oDebug h <*> oDisp h <*> oColor h)
@@ -586,6 +604,8 @@     , oColor = colorDef
     , oMsg = mempty
     , oRecursion = 100
+    , oRecursionLarge = 10_000
+    , oLarge = False
     , oOther = otherDef
     , oNoColor = False
     }
@@ -595,7 +615,9 @@ otherDef = coerce (True, Default, Default)
 
 nocolor, colorDef :: (String, PColor)
+-- | skip colors
 nocolor = ("nocolor", PColor $ flip const)
+-- | use default coloring from 'Color5'
 colorDef = Safe.fromJustNote "colorDef" $ coerce $ oColor $ getOptC @Color5
 
 -- | how much detail to show in the expression tree
@@ -610,16 +632,23 @@ isVerbose :: POpts -> Bool
 isVerbose = (DVerbose==) . oDebug
 
--- | color palettes
+-- | color palette for general display
 type Color1 = 'OColor "color1" 'Default 'Blue 'Default 'Red 'Black 'Cyan 'Black 'Yellow
+-- | color palette for general display
 type Color2 = 'OColor "color2" 'Default 'Magenta 'Default 'Red 'Black 'White 'Black 'Yellow
+-- | color palette for general display
 type Color3 = 'OColor "color3" 'Default 'Blue 'Red 'Default 'White 'Default 'Black 'Yellow
+-- | color palette for general display
 type Color4 = 'OColor "color4" 'Default 'Red 'Red 'Default 'Green 'Default 'Black 'Yellow
+-- | color palette for general display
 type Color5 = 'OColor "color5" 'Blue 'Default 'Red 'Default 'Cyan 'Default 'Yellow 'Default
 
+-- | color palette for effects used in 'Predicate.Core.Msg' and the refined modules
 type Other1 = 'OOther 'True 'Yellow 'Default
+-- | color palette for effects used in 'Predicate.Core.Msg' and the refined modules
 type Other2 = 'OOther 'True 'Default 'Default
 
+-- | display a message and three values where the last one is displayed in verbose mode
 show3 :: (Show a1, Show a2)
   => POpts
   -> String
@@ -628,6 +657,7 @@   -> String
 show3 opts msg0 ret = lit3 opts msg0 ret "" . show
 
+-- | display a message and four values where the last two are displayed in verbose mode
 show3' :: (Show a1, Show a2)
   => POpts
   -> String
@@ -637,6 +667,7 @@   -> String
 show3' opts msg0 ret fmt = lit3 opts msg0 ret fmt . show
 
+-- | display a message and four values where the last two are displayed in verbose mode
 lit3 :: Show a1
   => POpts
   -> String
@@ -650,7 +681,7 @@          msg0
       <> (if null msg0 then "" else " ")
       <> showL opts ret
-      <> litVerbose opts (" | " <> take 100 fmt) as
+      <> litVerbose opts (" | " <> litL opts fmt) as
 
 -- | more restrictive: only display data in verbose debug mode
 litVerbose :: POpts
@@ -665,9 +696,10 @@             -> String
             -> String
 showLitImpl o i s a =
-  if oDebug o >= i || oDebug o == DLite then take 100 s <> litL o a
+  if oDebug o >= i || oDebug o == DLite then litL o s <> litL o a
   else ""
 
+-- | show the value in verbose mode
 showVerbose :: Show a
   => POpts
   -> String
@@ -681,14 +713,16 @@   -> String
   -> a
   -> String
-showAImpl o i s a = showLitImpl o i (take 100 s) (show a)
+showAImpl o i s a = showLitImpl o i s (show a)
 
+-- | display a showable value limited to the width found in the options
 showL :: Show a
   => POpts
   -> a
   -> String
 showL o = litL o . show
 
+-- | display a value limited to the width found in the options
 litL :: POpts -> String -> String
 litL = litL' . oWidth
 
@@ -697,15 +731,17 @@   let (z,e) = splitAt i s
   in z ++ if null e then "" else "..."
 
+-- | display lazy bytestring output up to the maximum width in the options
 litBL :: POpts -> BL8.ByteString -> String
 litBL o s =
   let i = oWidth o
-  in litL' i (BL8.unpack (BL8.take (fromIntegral i) s))
+  in litL' i (BL8.unpack (BL8.take (1+fromIntegral i) s))
 
+-- | display bytestring output up to the maximum width in the options
 litBS :: POpts -> BS8.ByteString -> String
 litBS o s =
   let i = oWidth o
-  in litL' i (BS8.unpack (BS8.take i s))
+  in litL' i (BS8.unpack (BS8.take (i+1) s))
 
 -- | extract values from the trees or if there are errors return a tree with context
 splitAndAlign :: Show x =>
@@ -725,9 +761,16 @@ groupErrors :: [String] -> String
 groupErrors =
      intercalate " | "
-   . map (\xs@(x :| _) -> x <> (if length xs > 1 then "(" <> show (length xs) <> ")" else ""))
+   . map (\xs@(x :| _) -> x <> let ll = length xs in (if ll > 1 then "(" <> show ll <> ")" else ""))
    . N.group
 
+-- | returns True if the list has more than one element
+lengthGreaterThanOne :: [a] -> Bool
+lengthGreaterThanOne =
+  \case
+    _:_:_ -> True
+    _ -> False
+
 partitionTTExtended :: (w, TT a) -> Either ((w, TT x), String) (a, w, TT a)
 partitionTTExtended (s, t) =
   case _ttVal t of
@@ -749,6 +792,7 @@   then errorInProgram $ "shouldnt be calling this if we are dropping details: toNodeString " <> show (oDebug opts) <> " " <> show bpe
   else colorValP Long opts (_peValP bpe) <> " " <> _peString bpe
 
+-- | returns True if there the debug option supports a display in tree format
 hasNoTree :: POpts -> Bool
 hasNoTree opts =
   case oDebug opts of
@@ -773,6 +817,7 @@     ValP -> f "P"
   where f = colorMe o bp
 
+-- | flag for showing long or short output
 data Long = Long | Short deriving (Show, Eq)
 
 -- | render 'Val' value with colors
@@ -791,6 +836,7 @@                   ValP -> f "Present" <> " " <> show a
                   FailP {} -> errorInProgram $ "colorValLite: unexpected FailP " ++ show (bt,bp)
 
+-- | render coloured output for boolean values
 colorValBool ::
       POpts
    -> Val Bool
@@ -894,6 +940,8 @@   | OWidth !Nat           -- ^ set display width
   | OMsg !Symbol          -- ^ set text to add context to a failure message for refined types
   | ORecursion !Nat       -- ^ set recursion limit eg for regex
+  | ORecursionLarge !Nat  -- ^ set recursion limit for large fields
+  | OLarge !Bool          -- ^ use large recursion
   | OOther                -- ^ set effects for messages
      !Bool    -- ^ set underline
      !Color   -- ^ set foreground color
@@ -940,6 +988,10 @@    getOptC = setMessage (symb @s)
 instance KnownNat n => OptC ('ORecursion n) where
    getOptC = setRecursion (nat @n)
+instance KnownNat n => OptC ('ORecursionLarge n) where
+   getOptC = setRecursionLarge (nat @n)
+instance GetBool b => OptC ('OLarge b) where
+   getOptC = setLarge (getBool @b)
 instance ( GetBool b
          , GetColor c1
          , GetColor c2
@@ -1012,41 +1064,32 @@ instance OptC 'OUNV where
    getOptC = getOptC @('OANV ':# 'OUnicode)
 
--- | option synonyms to save a keystroke
+-- option synonyms to save a keystroke
+-- | debugging: no output
 type OZ = 'OZ     -- 'OAnsi ':# 'OColorOff ':# 'OZero
+-- | debugging: one line of summarised output without colors or effects
 type OL = 'OL     -- 'OAnsi ':# 'OColorOff ':# 'OLite ':# 'OWidth 200
+-- | ascii output with colours
 type OA = 'OA     -- 'OAnsi ':# Color5 ':# 'ONormal ':# Other2 ':# 'OWidth 100
+-- | ascii output with colours and bold background
 type OAB = 'OAB   -- 'OAnsi ':# Color1 ':# 'ONormal ':# Other1 ':# 'OWidth 100
+-- | ascii output without colours
 type OAN = 'OAN   -- 'OAnsi ':# 'OColorOff ':# 'ONormal ':# 'OWidth 100
+-- | ascii output without colours
 type OAV = 'OAV   -- 'OAnsi ':# Color5 ':# 'OVerbose ':# Other2 ':# 'OWidth 200
+-- | ascii output without colours
 type OANV = 'OANV -- 'OAnsi ':# 'OColorOff ':# 'OVerbose ':# 'OWidth 200
+-- | unicode output without colours
 type OU = 'OU     -- 'OUnicode ':# Color5 ':# 'ONormal ':# Other2 ':# 'OWidth 100
+-- | unicode output with colors and a bold background
 type OUB = 'OUB   -- 'OUnicode ':# Color1 ':# 'ONormal ':# Other1 ':# 'OWidth 100
+-- | unicode output without colours
 type OUN = 'OUN   -- 'OUnicode ':# 'OColorOff ':# 'OWidth 200
+-- | unicode output verbose with colours
 type OUV = 'OUV   -- 'OUnicode ':# Color5 ':# 'OVerbose ':# Other2 ':# 'OWidth 200
+-- | unicode output without colours and verbose
 type OUNV = 'OUNV -- 'OUnicode ':# 'OColorOff ':# 'OVerbose ':# 'OWidth 200
 
-_Debug :: Lens' POpts Debug
-_Debug afb opts = (\d -> opts { oDebug = d }) <$> afb (oDebug opts)
-
-_DVerboseI :: Prism' Debug ()
-_DVerboseI =
-  prism' (const DVerbose)
-  $ \case
-       DVerbose -> Just ()
-       _ -> Nothing
-
--- | traversal for DVerbose
---
--- >>> has _DVerbose (getOpt @OU)
--- False
---
--- >>> has _DVerbose (getOpt @OUV)
--- True
---
-_DVerbose :: Traversal' POpts ()
-_DVerbose = _Debug . _DVerboseI
-
 -- | convert typelevel options to 'POpts'
 --
 -- >>> (oDisp &&& fst . oColor &&& oWidth) (getOpt @(OA ':# OU ':# OA ':# 'OWidth 321 ':# Color4 ':# 'OMsg "test message"))
@@ -1073,11 +1116,11 @@    -> String
    -> t a
    -> [Tree PE]
-   -> Either (TT x) [a]
+   -> Either (TT x) (Int,[a])
 chkSize opts msg0 xs hhs =
-  let mx = oRecursion opts
+  let mx = getMaxRecursionValue opts
   in case splitAt mx (toList xs) of
-    (zs,[]) -> Right zs
+    (zs,[]) -> Right (length zs,zs)
     (_,_:_) -> Left $ mkNode opts (Fail (msg0 <> " list size exceeded")) ("max is " ++ show mx) hhs
 
 -- | deal with possible recursion on two lists
@@ -1087,10 +1130,14 @@    -> t a
    -> u b
    -> [Tree PE]
-   -> Either (TT x) ([a],[b])
+   -> Either (TT x) ((Int,[a]),(Int,[b]))
 chkSize2 opts msg0 xs ys hhs =
   (,) <$> chkSize opts msg0 xs hhs <*> chkSize opts msg0 ys hhs
 
+-- | get the current recursion value depending on the oLarge flag
+getMaxRecursionValue :: POpts -> Int
+getMaxRecursionValue = ifM oLarge oRecursionLarge oRecursion
+
 -- | pretty print a message
 formatOMsg :: POpts -> String -> String
 formatOMsg o suffix =
@@ -1098,9 +1145,9 @@     [] -> mempty
     s@(_:_) -> intercalate " | " (map (setOtherEffects o) s) <> suffix
 
--- | override options for 'DZero' so we dont lose error information
-subopts :: POpts -> POpts
-subopts opts =
+-- | override options for 'DZero' so we dont lose error information: especially if we want to extract the topMessage and use it for Fail case
+zeroToLite :: POpts -> POpts
+zeroToLite opts =
   case oDebug opts of
     DZero -> opts { oDebug = DLite }
     _ -> opts
@@ -1126,12 +1173,12 @@   OptT (x ': xs) = x ':# OptT xs
 
 -- | message to display when the length of a foldable is exceeded
-badLength :: Foldable t
-          => t a
+badLength :: Int
           -> Int
           -> String
-badLength as n = ":invalid length(" <> show (length as) <> ") expected " ++ show n
+badLength asLen n = ":invalid length(" <> show asLen <> ") expected " ++ show n
 
+-- | render the output from TT depending on the debug options
 prtTree :: Show x => POpts -> TT x -> String
 prtTree opts tt =
   case oDebug opts of
@@ -1146,6 +1193,7 @@      _ -> formatOMsg opts ""
           <> prtTreePure opts (hh tt)
 
+-- | return a singleton list of Tree if in verbose mode
 verboseList :: POpts -> TT a -> [Tree PE]
 verboseList o tt
   | isVerbose o = [hh tt]

@@ -46,10 +46,10 @@   , expectBT (Val ()) $ pl @(L22 >> L22) (1,('a',(3,(True,()))))
   , expectBT (Val True) $ pl @L31 (1,2,(True,4))
   , expectBT (Fail "failed3") $ pl @((Fst >> FailT _ "failed3" >> Le (6 -% 1)) || 'False) ([-5],True)
-  , expectBT (Val [(-999) % 1,10 % 1,20 % 1,(-999) % 1,30 % 1]) $ pl @(Map (Wrap (MM.First _) Id &&& (Pure Maybe (999 -% 1 ) >> Wrap (MM.First _) Id)) >> Map (Fst <> Snd) >> Map ('Just Unwrap)) [Nothing,Just 10,Just 20,Nothing,Just 30]
+  , expectBT (Val [(-999) % 1,10 % 1,20 % 1,(-999) % 1,30 % 1]) $ pl @(Map (Wrap (MM.First _) Id &&& (Pure Maybe (999 -% 1 ) >> Wrap (MM.First _) Id)) >> Map (Uncurry (<>)) >> Map ('Just Unwrap)) [Nothing,Just 10,Just 20,Nothing,Just 30]
   , expectBT (Val (True,3.4)) $ pl @(Thd >> Snd >> Fst) (1,'a',('x',((True,3.4),999)))
   , expectBT (Val [13,16,17]) $ pl @(Guard "err" (Len > 2) >> Map Succ) [12,15,16]
-  , expectBT (Val 55) $ pl @(Map (Wrap (SG.Sum _) Id) >> MConcat Id >> Unwrap) [1..10]
+  , expectBT (Val 55) $ pl @(Map (Wrap (SG.Sum _) Id) >> MConcat >> Unwrap) [1..10]
   , expectBT (Val 9) $ pl @((Wrap _ Id *** Wrap (SG.Sum _) Id) >> (Fst <> Snd) >> Unwrap) (4,5)
   , expectBT (Val (SG.Sum 9)) $ pl @((Wrap _ Id *** Wrap _ Id) >> (Fst <> Snd)) (4,5)
   , expectBT (Fail "len is bad") $ pl @Ip6Test "FE80::203:Baff:FE77:326FF"
@@ -60,7 +60,7 @@   , expectBT (Fail "Guards:invalid length(5) expected 4") $ pl @(Rescan "(\\d+)\\.?" >> ConcatMap Snd Id >> Map (ReadBase Int 10) >| Ip4op) "1.22.244.66.77"
   , expectBT (Val 256) $ pl @(Rescan "(?i)^\\\\x([0-9a-f]{2})$" >> OneP >> Snd >> OneP >> ReadBase Int 16 >> Succ) "\\xfF"
   , expectBT (Val 256) $ pl @(Rescan "(?i)^\\\\x(.{2})$" >> OneP >> Snd >> OneP >> ReadBase Int 16 >> Succ) "\\xfF"
-  , expectBT (Val (("fF",(255,"ff")),False)) $ pl @(Rescan "(?i)^\\\\x([0-9a-f]{2})$" >> OneP >> Snd >> OneP >> (Id &&& (ReadBase Int 16 >> (Id &&& ShowBase 16))) >> (Id &&& ((Id *** Snd) >> Fst == Snd))) "\\xfF"
+  , expectBT (Val (("fF",(255,"ff")),False)) $ pl @(Rescan "(?i)^\\\\x([0-9a-f]{2})$" >> OneP >> Snd >> OneP >> (Id &&& (ReadBase Int 16 >> (Id &&& ShowBase 16))) >> (Id &&& ((Id *** Snd) >> Uncurry (==)))) "\\xfF"
   , expectBT (Val [31,11,1999]) $ pl @(Rescan DdmmyyyyRE >> OneP >> Map' (ReadBase Int 10) Snd >| Ddmmyyyyop) "31-11-1999"
   , expectBT (Val (TimeOfDay 23 13 59)) $ pl @(Guard "hh:mm:ss regex failed" (Re HmsRE) >> ReadP TimeOfDay Id) "23:13:59"
   , expectBT (Fail "hh:mm:ss regex failed") $ pl @(Guard "hh:mm:ss regex failed" (Re HmsRE) >> ReadP TimeOfDay Id) "23:13:60"
@@ -153,8 +153,6 @@   , expectBT (Val (2,True)) $ pz @( FlipT '(,) 'True 2) ()
   , expectBT (Val (1,"ab",2)) $ pz @( FlipT ('(,,) 1) 2 Id) "ab"
   , expectBT (Val 13) $ pz @(12 & Lift Succ) ()
-  , expectBT (Val 10) $ pz @('[1,2,3,4] & FoldMap (SG.Sum _)) ()
-
 
   -- test semigroup interaction
   , expectEQR (These (Val 6) (Fail "xyz | hello")) $ fmap This (pz @Predicate.Sum [1,2,3]) <> fmap That (pz @(FailS "xyz") 5) <> fmap That (pz @(FailS "hello") 1)

@@ -112,3 +112,18 @@         (Pop2' (Proxy ('(,) :: Type -> Bool -> (Type,Bool))) (Proxy (W "bbb")) Fst Snd >> Snd)
         (Proxy 'True, Int))
 testKindSignature0C = newRefined (Proxy @'True,1234)
+
+testKindSignature0D :: Either Msg0
+      (Refined
+        OU
+        (On (**) (FromIntegral Double) >> Id < (FromIntegral Double << 144))
+        (Int, Int))
+testKindSignature0D = newRefined (14,4)
+
+testKindSignature0E :: Either Msg0
+      (Refined
+        OU
+        (On (Flip (<>)) (Pure [] Id) >> '(Len,Head,Last) >> Fst > 5)
+        (Char, Char))
+testKindSignature0E = newRefined ('x','y')
+

@@ -342,11 +342,10 @@      (Int,Int,String))
 testKindSignature2E = newRefined2 (1,2,"defghi")
 
--- awkward as  FoldMap t p has p for location of stuff and then we need to run in a context (usually Id relative to p)
 testKindSignature2F :: Either Msg2
    (Refined2 OU
      (Second (Map (ReadP Int '[Id])))
-     (Pop2 (Proxy (FoldMap :: Type -> Type -> Type)) (SG.Product Int) Snd Id >> Id > 4)
+     (Pop1 (Proxy (FoldAla :: Type -> Type)) (SG.Product Int) Snd >> Id > 4)
      (Char,String))
 testKindSignature2F = newRefined2 ('x',"23498")