diff --git a/haskus-utils-variant.cabal b/haskus-utils-variant.cabal
--- a/haskus-utils-variant.cabal
+++ b/haskus-utils-variant.cabal
@@ -1,18 +1,18 @@
-name: haskus-utils-variant
-version: 1.0
 cabal-version: >=1.20
-build-type: Simple
+name: haskus-utils-variant
+version: 2.0
 license: BSD3
 license-file: LICENSE
 copyright: Sylvain Henry 2018
 maintainer: sylvain@haskus.fr
+author: Sylvain Henry
 homepage: http://www.haskus.org
 synopsis: Haskus utility modules
 description:
     Variant (extensible sum type) and EADT (extensible recursive sum type)
     datatypes.
 category: System
-author: Sylvain Henry
+build-type: Simple
 
 source-repository head
     type: git
@@ -25,11 +25,26 @@
         Haskus.Utils.Variant.Flow
         Haskus.Utils.Variant.Cont
         Haskus.Utils.EADT
-    build-depends:
-        base >=4.9 && <4.12,
-        haskus-utils-types ==1.0.*,
-        haskus-utils-data ==1.0.*
-    default-language: Haskell2010
+        Haskus.Utils.EADT.TH
     hs-source-dirs: src/lib
+    default-language: Haskell2010
     ghc-options: -Wall
+    build-depends:
+        base >=4.9 && <4.12,
+        template-haskell >=2.13.0.0 && <2.14,
+        haskus-utils-types ==1.1.*,
+        haskus-utils-data ==1.1.*
 
+test-suite tests
+    type: exitcode-stdio-1.0
+    main-is: Main.hs
+    hs-source-dirs: src/tests
+    other-modules:
+        Variant
+    default-language: Haskell2010
+    ghc-options: -Wall -threaded
+    build-depends:
+        base >=4.11.1.0 && <4.12,
+        haskus-utils-variant -any,
+        tasty >=0.11 && <1.2,
+        tasty-quickcheck >=0.8 && <0.11
diff --git a/src/lib/Haskus/Utils/EADT.hs b/src/lib/Haskus/Utils/EADT.hs
--- a/src/lib/Haskus/Utils/EADT.hs
+++ b/src/lib/Haskus/Utils/EADT.hs
@@ -11,6 +11,8 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 
 -- | Extensible ADT
 module Haskus.Utils.EADT
@@ -26,6 +28,15 @@
    , variantFToValue
    , LiftableF
    , liftVariantF
+   , AlterVariantF
+   , alterVariantF
+   , AlgVariantF
+   , algVariantF
+   , splitVariantF
+   , variantFToCont
+   , variantFToContM
+   , contToVariantF
+   , contToVariantFM
    -- * Extensible ADT
    , EADT
    , (:<:)
@@ -33,7 +44,16 @@
    , appendEADT
    , liftEADT
    , popEADT
+   , AlterEADT
+   , alterEADT
+   , AlgEADT
+   , algEADT
+   , eadtToCont
+   , eadtToContM
+   , contToEADT
+   , contToEADTM
    -- * Reexport
+   , NoConstraint
    , module Haskus.Utils.Functor
    )
 where
@@ -42,7 +62,12 @@
 import Haskus.Utils.Functor
 import Haskus.Utils.Types.List
 import Haskus.Utils.Types
+import Haskus.Utils.ContFlow
 
+import Unsafe.Coerce
+import Data.Bifunctor
+import GHC.Exts (Any,Constraint)
+
 -- | Recursive Functor-like Variant
 newtype VariantF (xs :: [* -> *]) e
    = VariantF (V (ApplyAll e xs))
@@ -66,7 +91,7 @@
       Left xs -> toVariantFTail (fmap f (VariantF xs))
 
 -- | Pattern-match in a VariantF
-pattern FV :: forall c cs e. Popable c (ApplyAll e cs) => c -> VariantF cs e
+pattern FV :: forall c cs e. c :< (ApplyAll e cs) => c -> VariantF cs e
 pattern FV x = VariantF (V x)
 
 -- | Retrieve a single value
@@ -97,7 +122,7 @@
 
 -- | Pop VariantF
 popVariantF :: forall x xs ys e.
-   ( Popable (x e) (ApplyAll e xs)
+   ( x e :< ApplyAll e xs
    , Filter (x e) (ApplyAll e xs) ~ ApplyAll e ys
    ) => VariantF xs e -> Either (VariantF ys e) (x e)
 {-# INLINE popVariantF #-}
@@ -107,7 +132,7 @@
 
 -- | Map the matching types of a variant
 mapVariantF :: forall a b cs e ds as.
-   ( MappableVariant (a e) (b e) as
+   ( MapVariant (a e) (b e) as
    , ds ~ ReplaceNS (IndexesOf a cs) b cs
    , as ~ ApplyAll e cs
    , ApplyAll e ds ~ ReplaceNS (IndexesOf (a e) as) (b e) as
@@ -126,6 +151,111 @@
    ) => VariantF as e -> VariantF bs e
 liftVariantF (VariantF v) = VariantF (liftVariant' v)
 
+class AlterVariantF (c :: (* -> *) -> Constraint) e (xs :: [* -> *]) where
+   alterVariantF' :: (forall (f :: * -> *). c f => f e -> f e) -> Word -> Any -> Any
+
+instance AlterVariantF c e '[] where
+   {-# INLINE alterVariantF' #-}
+   alterVariantF' _ = undefined
+
+instance
+   ( AlterVariantF c e xs
+   , c x
+   ) => AlterVariantF c e (x ': xs)
+   where
+      {-# INLINE alterVariantF' #-}
+      alterVariantF' f t v =
+         case t of
+            0 -> unsafeCoerce (f (unsafeCoerce v :: x e))
+            n -> alterVariantF' @c @e @xs f (n-1) v
+
+-- | Alter a variant. You need to specify the constraints required by the
+-- modifying function.
+--
+-- Usage:
+--    alterVariantF @NoConstraint id         v
+--    alterVariantF @Resizable    (resize 4) v
+--
+--
+--    -- Multiple constraints:
+--    class (Ord a, Num a) => OrdNum a
+--    instance (Ord a, Num a) => OrdNum a
+--    alterVariantF @OrdNum foo v
+--
+alterVariantF :: forall c e (xs :: [* -> *]).
+   ( AlterVariantF c e xs
+   ) => (forall (f :: * -> *). c f => f e -> f e) -> VariantF xs e -> VariantF xs e
+{-# INLINABLE alterVariantF #-}
+alterVariantF f (VariantF (Variant t a)) =
+   VariantF (Variant t (alterVariantF' @c @e @xs f t a))
+
+
+class AlgVariantF (c :: (* -> *) -> Constraint) e (xs :: [* -> *]) where
+   algVariantF' :: (forall (f :: * -> *). c f => f e -> e) -> Word -> Any -> e
+
+instance AlgVariantF c e '[] where
+   {-# INLINE algVariantF' #-}
+   algVariantF' _ = undefined
+
+instance
+   ( AlgVariantF c e xs
+   , c x
+   ) => AlgVariantF c e (x ': xs)
+   where
+      {-# INLINE algVariantF' #-}
+      algVariantF' f t v =
+         case t of
+            0 -> f (unsafeCoerce v :: x e)
+            n -> algVariantF' @c @e @xs f (n-1) v
+
+-- | Apply an algebra to a VariantF. You need to specify the constraints
+-- required by the modifying function.
+--
+-- Usage:
+--    algVariantF @NoConstraint id         v
+--    algVariantF @Resizable    (resize 4) v
+algVariantF :: forall c e (xs :: [* -> *]).
+   ( AlgVariantF c e xs
+   ) => (forall (f :: * -> *). c f => f e -> e) -> VariantF xs e -> e
+{-# INLINABLE algVariantF #-}
+algVariantF f (VariantF (Variant t a)) = algVariantF' @c @e @xs f t a
+
+
+-- | Split a VariantF in two
+splitVariantF :: forall as xs e.
+   ( Complement (ApplyAll e xs) (ApplyAll e as) ~ ApplyAll e (Complement xs as)
+   , SplitVariant (ApplyAll e as) (ApplyAll e xs) (ApplyAll e xs)
+   ) => VariantF xs e
+     -> Either (VariantF as e) (VariantF (Complement xs as) e)
+splitVariantF (VariantF v) = bimap VariantF VariantF (splitVariant v)
+
+-- | Convert a VariantF into a multi-continuation
+variantFToCont :: ContVariant (ApplyAll e xs)
+   => VariantF xs e -> ContFlow (ApplyAll e xs) r
+variantFToCont (VariantF v) = variantToCont v
+
+-- | Convert a VariantF into a multi-continuation
+variantFToContM ::
+   ( ContVariant (ApplyAll e xs)
+   , Monad m
+   ) => m (VariantF xs e) -> ContFlow (ApplyAll e xs) (m r)
+variantFToContM f = variantToContM (unvariantF <$> f)
+   where
+      unvariantF (VariantF v) = v
+
+-- | Convert a multi-continuation into a VariantF
+contToVariantF :: forall xs e.
+   ( ContVariant (ApplyAll e xs)
+   ) => ContFlow (ApplyAll e xs) (V (ApplyAll e xs)) -> VariantF xs e
+contToVariantF c = VariantF (contToVariant c)
+
+-- | Convert a multi-continuation into a VariantF
+contToVariantFM :: forall xs e m.
+   ( ContVariant (ApplyAll e xs)
+   , Monad m
+   ) => ContFlow (ApplyAll e xs) (m (V (ApplyAll e xs))) -> m (VariantF xs e)
+contToVariantFM f = VariantF <$> contToVariantM f
+
 --------------------------------------------
 -- Extensible ADT
 --------------------------------------------
@@ -148,9 +278,9 @@
    ( e ~ EADT cs  -- allow easy use of TypeApplication to set the EADT type
    , f :<: cs     -- constraint synonym ensuring `f` is in `cs`
    ) => f (EADT cs) -> EADT cs
-pattern VF x = Fix (VariantF (V' x))   -- `V'` match a variant value (without
-                                       -- checking the membership: we already
-                                       -- do it with :<:)
+pattern VF x = Fix (VariantF (VSilent x))
+   -- `VSilent` matches a variant value without checking the membership: we
+   -- already do it with :<:
 
 -- | Append new "constructors" to the EADT
 appendEADT :: forall ys xs zs.
@@ -172,7 +302,54 @@
 popEADT :: forall xs f e.
    ( f :<: xs
    , e ~ EADT xs
-   , Popable (f e) (ApplyAll e xs)
+   , f e :< ApplyAll e xs
    , Filter (f e) (ApplyAll e xs) ~ ApplyAll e (Filter f xs)
    ) => EADT xs -> Either (VariantF (Filter f xs) (EADT xs)) (f (EADT xs))
 popEADT (Fix v) = popVariantF v
+
+type AlterEADT c xs = AlterVariantF c (EADT xs) xs
+
+-- | Alter an EADT value
+alterEADT :: forall c xs.
+   ( AlterEADT c xs
+   ) => (forall f. c f => f (EADT xs) -> f (EADT xs)) -> EADT xs -> EADT xs
+alterEADT f (Fix v) = Fix (alterVariantF @c @(EADT xs) f v)
+
+type AlgEADT c xs = AlgVariantF c (EADT xs) xs
+
+-- | Apply an algebra to an EADT value
+algEADT :: forall c xs.
+   ( AlgEADT c xs
+   ) => (forall f. c f => f (EADT xs) -> EADT xs) -> EADT xs -> EADT xs
+algEADT f (Fix v) = algVariantF @c @(EADT xs) f v
+
+-- | Convert an EADT into a multi-continuation
+eadtToCont ::
+   ( ContVariant (ApplyAll (Fix (VariantF xs)) xs)
+   ) => Fix (VariantF xs) -> ContFlow (ApplyAll (Fix (VariantF xs)) xs) r
+eadtToCont (Fix v) = variantFToCont v
+
+-- | Convert an EADT into a multi-continuation
+eadtToContM ::
+   ( ContVariant (ApplyAll (Fix (VariantF xs)) xs)
+   , Monad m
+   ) => m (Fix (VariantF xs))
+     -> ContFlow (ApplyAll (Fix (VariantF xs)) xs) (m r)
+eadtToContM f = variantFToContM (unfix <$> f)
+
+-- | Convert a multi-continuation into an EADT
+contToEADT ::
+   ( ContVariant (ApplyAll (Fix (VariantF xs)) xs)
+   ) => ContFlow (ApplyAll (Fix (VariantF xs)) xs)
+                 (V (ApplyAll (Fix (VariantF xs)) xs))
+     -> Fix (VariantF xs)
+contToEADT c = Fix (contToVariantF c)
+
+-- | Convert a multi-continuation into an EADT
+contToEADTM ::
+   ( ContVariant (ApplyAll (Fix (VariantF xs)) xs)
+   , Monad f
+   ) => ContFlow (ApplyAll (Fix (VariantF xs)) xs)
+                 (f (V (ApplyAll (Fix (VariantF xs)) xs)))
+     -> f (Fix (VariantF xs))
+contToEADTM f = Fix <$> contToVariantFM f
diff --git a/src/lib/Haskus/Utils/EADT/TH.hs b/src/lib/Haskus/Utils/EADT/TH.hs
new file mode 100644
--- /dev/null
+++ b/src/lib/Haskus/Utils/EADT/TH.hs
@@ -0,0 +1,150 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- | Template-Haskell helpers for EADTs
+module Haskus.Utils.EADT.TH
+   ( eadtPattern
+   , eadtPatternT
+   )
+where
+
+import Language.Haskell.TH
+import Control.Monad
+import Haskus.Utils.EADT
+
+-- | Create a pattern synonym for an EADT constructor
+--
+-- E.g.
+--
+-- > data ConsF a e = ConsF a e deriving (Functor)
+-- > $(eadtPattern 'ConsF "Cons")
+-- >
+-- > ====>
+-- >
+-- > pattern Cons :: ConsF a :<: xs => a -> EADT xs -> EADT xs
+-- > pattern Cons a l = VF (ConsF a l)
+--
+eadtPattern
+   :: Name       -- ^ Actual constructor (e.g., ConsF)
+   -> String     -- ^ Name of the pattern (e.g., Cons)
+   -> Q [Dec]
+eadtPattern consName patStr = eadtPattern' consName patStr Nothing
+
+-- | Create a pattern synonym for an EADT constructor that is part of a
+-- specified EADT.
+--
+-- This can be useful to help the type inference because instead of using a
+-- generic "EADT xs" type, the pattern uses the provided type.
+--
+-- E.g.
+--
+-- > data ConsF a e = ConsF a e deriving (Functor)
+-- > data NilF    e = NilF      deriving (Functor)
+-- >
+-- > type List a = EADT '[ConsF a, NilF]
+-- >
+-- > $(eadtPatternT 'ConsF "ConsList" [t|forall a. List a|])
+-- >
+-- > ====>
+-- >
+-- > pattern ConsList ::
+--    ( List a ~ EADT xs
+--    , ConsF a :<: xs
+--    ) => a -> List a -> List a
+-- > pattern ConsList a l = VF (ConsF a l)
+--
+-- Note that you have to quantify free variables explicitly with 'forall'
+--
+eadtPatternT
+   :: Name       -- ^ Actual constructor (e.g., ConsF)
+   -> String     -- ^ Name of the pattern (e.g., Cons)
+   -> Q Type     -- ^ Type of the EADT (e.g., [t|forall a. List a|])
+   -> Q [Dec]
+eadtPatternT consName patStr qtype =
+   eadtPattern' consName patStr (Just qtype)
+
+
+-- | Create a pattern synonym for an EADT constructor
+eadtPattern'
+   :: Name       -- ^ Actual constructor (e.g., ConsF)
+   -> String     -- ^ Name of the pattern (e.g., Cons)
+   -> Maybe (Q Type) -- ^ EADT type
+   -> Q [Dec]
+eadtPattern' consName patStr mEadtTy= do
+   let patName = mkName patStr
+
+   typ <- reify consName >>= \case
+            DataConI _ t _ -> return t
+            _              -> fail $ show consName ++ " isn't a data constructor"
+
+   case typ of
+      ForallT tvs _ tys -> do
+         -- make pattern
+         let getConArity = \case
+               _ :->: b -> 1 + getConArity b
+               _        -> 0
+
+             conArity = getConArity tys
+         conArgs <- replicateM conArity (newName "c")
+
+         let vf     = mkName "Haskus.Utils.EADT.VF"
+
+         let pat    = PatSynD patName (PrefixPatSyn conArgs) ImplBidir
+                         (ConP vf [ConP consName (fmap VarP conArgs)])
+
+         let
+            -- retrieve constructor type without the functor var
+            -- e.g. ConsF a for ConsF a e
+            getConTyp (_ :->: b) = getConTyp b
+            getConTyp (AppT a _) = a -- remove last AppT (functor var)
+            getConTyp _          = error "Invalid constructor type"
+
+            conTyp = getConTyp tys
+
+            -- [* -> *]
+            tyToTyList = AppT ListT (AppT (AppT ArrowT StarT) StarT)
+
+         -- make pattern type
+         (newTvs,eadtTy,ctx) <- do
+            xsName <- newName "xs"
+            let
+               xs = VarT xsName
+               xsTy = KindedTV xsName tyToTyList
+            eadtXs <- [t| EADT $(return xs) |]
+
+            prd <-  [t| $(return conTyp) :<: $(return xs) |]
+            case mEadtTy of
+               Nothing -> return ([xsTy],eadtXs,[prd])
+               Just ty -> do
+                  ty' <- ty
+                  let (tvs',ty'',ctx') = case ty' of
+                        ForallT tvs'' ctx'' t -> (tvs'',t,ctx'')
+                        _                     -> ([],ty',[])
+                  prd2 <- [t| $(return ty'') ~ EADT $(return xs) |]
+                  return (xsTy:tvs',ty'',prd:prd2:ctx')
+
+         let
+            -- remove functor var; add new type var
+            tvs'       = init tvs ++ newTvs
+            -- retreive functor var in "e"
+            KindedTV e StarT = last tvs
+
+            -- replace functor variable with EADT type
+            go (VarT x :->: b)
+               | x == e      = eadtTy :->: go b
+            go (a :->: b)    = a :->: go b
+            go _             = eadtTy
+            t'               = go tys
+
+
+         let sig = PatSynSigD patName (ForallT tvs' ctx t')
+
+         return [sig,pat]
+
+      _ -> fail $ show consName ++ "'s type doesn't have a free variable, it can't be a functor"
+
+
+pattern (:->:) :: Type -> Type -> Type
+pattern a :->: b = AppT (AppT ArrowT a) b
diff --git a/src/lib/Haskus/Utils/Variant.hs b/src/lib/Haskus/Utils/Variant.hs
--- a/src/lib/Haskus/Utils/Variant.hs
+++ b/src/lib/Haskus/Utils/Variant.hs
@@ -18,8 +18,7 @@
 
 -- | Open sum type
 module Haskus.Utils.Variant
-   ( Variant
-   , V
+   ( V (..)
    , variantIndex
    -- * Patterns
    , pattern V
@@ -33,34 +32,37 @@
    , fromVariantAt
    , popVariantAt
    , popVariantHead
-   , updateVariantAt
+   , mapVariantAt
+   , mapVariantAtM
    , foldMapVariantAt
    , foldMapVariantAtM
    -- * Operations by type
    , toVariant
    , Member
    , Filter
-   , Popable
-   , MaybePopable
    , popVariant
    , popVariantMaybe
    , fromVariant
    , fromVariantMaybe
    , fromVariantFirst
-   , updateVariantFirst
-   , updateVariantFirstM
-   , MappableVariant
+   , mapVariantFirst
+   , mapVariantFirstM
+   , ReplaceAll
+   , MapVariant
    , mapVariant
+   , mapNubVariant
    , foldMapVariantFirst
    , foldMapVariantFirstM
    , foldMapVariant
    -- * Generic operations with type classes
-   , AlterVariant
-   , TraverseVariant
    , NoConstraint
+   , AlterVariant
    , alterVariant
+   , TraverseVariant
    , traverseVariant
    , traverseVariant_
+   , ReduceVariant
+   , reduceVariant
    -- * Conversions between variants
    , appendVariant
    , prependVariant
@@ -71,8 +73,12 @@
    , Flattenable
    , FlattenVariant
    , flattenVariant
-   , ExtractMonad
+   , ExtractM
    , joinVariant
+   , joinVariantUnsafe
+   , JoinVariant
+   , splitVariant
+   , SplitVariant
    -- * Conversions to/from other data types
    , variantToValue
    , variantFromValue
@@ -83,7 +89,7 @@
    -- ** Continuations
    , ContVariant (..)
    -- ** Internals
-   , pattern V'
+   , pattern VSilent
    , liftVariant'
    , fromVariant'
    , popVariant'
@@ -94,7 +100,8 @@
 where
 
 import Unsafe.Coerce
-import GHC.Exts (Any,Constraint)
+import GHC.Exts (Any)
+import Data.Typeable
 
 import Haskus.Utils.Monad
 import Haskus.Utils.Types
@@ -105,20 +112,18 @@
 
 -- | A variant contains a value whose type is at the given position in the type
 -- list
-data Variant (l :: [*]) = Variant {-# UNPACK #-} !Word Any
-
-type V = Variant
+data V (l :: [*]) = Variant {-# UNPACK #-} !Word Any
 
 -- Make GHC consider `l` as a representational parameter to make coercions
 -- between Variant values unsafe
-type role Variant representational
+type role V representational
 
 -- | Pattern synonym for Variant
 --
 -- Usage: case v of
 --          V (x :: Int)    -> ...
 --          V (x :: String) -> ...
-pattern V :: forall c cs. Popable c cs => c -> Variant cs
+pattern V :: forall c cs. (c :< cs) => c -> V cs
 pattern V x <- (fromVariant -> Just x)
    where
       V x = toVariant x
@@ -126,27 +131,27 @@
 -- | Silent pattern synonym for Variant
 --
 -- Usage: case v of
---          V (x :: Int)    -> ...
---          V (x :: String) -> ...
-pattern V' :: forall c cs.
+--          VSilent (x :: Int)    -> ...
+--          VSilent (x :: String) -> ...
+pattern VSilent :: forall c cs.
    ( Member' c cs
    , PopVariant c cs
-   ) => c -> Variant cs
-pattern V' x <- (fromVariant' -> Just x)
+   ) => c -> V cs
+pattern VSilent x <- (fromVariant' -> Just x)
    where
-      V' x = toVariant' x
+      VSilent x = toVariant' x
 
 -- | Statically unchecked matching on a Variant
-pattern VMaybe :: forall c cs. (MaybePopable c cs) => c -> Variant cs
+pattern VMaybe :: forall c cs. (c :<? cs) => c -> V cs
 pattern VMaybe x <- (fromVariantMaybe -> Just x)
 
-instance Eq (Variant '[]) where
-   (==) = error "Empty variant"
+instance Eq (V '[]) where
+   (==) _ _ = True
 
 instance
-   ( Eq (Variant xs)
+   ( Eq (V xs)
    , Eq x
-   ) => Eq (Variant (x ': xs))
+   ) => Eq (V (x ': xs))
    where
       {-# INLINE (==) #-}
       (==) v1@(Variant t1 _) v2@(Variant t2 _)
@@ -156,13 +161,13 @@
             (Left as, Left bs) -> as == bs
             _                  -> False
 
-instance Ord (Variant '[]) where
+instance Ord (V '[]) where
    compare = error "Empty variant"
 
 instance
-   ( Ord (Variant xs)
+   ( Ord (V xs)
    , Ord x
-   ) => Ord (Variant (x ': xs))
+   ) => Ord (V (x ': xs))
    where
       compare v1 v2 = case (popVariantHead v1, popVariantHead v2) of
          (Right a, Right b) -> compare a b
@@ -170,16 +175,21 @@
          (Right _, Left _)  -> LT
          (Left _, Right _)  -> GT
 
-instance Show (Variant '[]) where
-   show = error "Empty variant"
+instance Show (V '[]) where
+   show _ = "V '[]"
 
 instance
-   ( Show (Variant xs)
+   ( Show (V xs)
    , Show x
-   ) => Show (Variant (x ': xs))
+   , Typeable x
+   ) => Show (V (x ': xs))
    where
       show v = case popVariantHead v of
-         Right x -> show x
+         Right x -> let parens s
+                           | ' ' `elem` s = "(" ++ s ++ ")"
+                           | otherwise    = s
+                        -- naive parenthesing but it works
+                     in "V @" ++ parens (show (typeOf x)) ++ " " ++ parens (show x)
          Left xs -> show xs
 
 -----------------------------------------------------------
@@ -187,31 +197,31 @@
 -----------------------------------------------------------
 
 -- | Get Variant index
-variantIndex :: Variant a -> Word
+variantIndex :: V a -> Word
 variantIndex (Variant n _) = n
 
 -- | Set the value with the given indexed type
 toVariantAt :: forall (n :: Nat) (l :: [*]).
    ( KnownNat n
-   ) => Index n l -> Variant l
-{-# INLINE toVariantAt #-}
+   ) => Index n l -> V l
+{-# INLINABLE toVariantAt #-}
 toVariantAt a = Variant (natValue' @n) (unsafeCoerce a)
 
 -- | Set the first value
-toVariantHead :: forall x xs. x -> Variant (x ': xs)
-{-# INLINE toVariantHead #-}
+toVariantHead :: forall x xs. x -> V (x ': xs)
+{-# INLINABLE toVariantHead #-}
 toVariantHead a = Variant 0 (unsafeCoerce a)
 
 -- | Set the tail
-toVariantTail :: forall x xs. Variant xs -> Variant (x ': xs)
-{-# INLINE toVariantTail #-}
+toVariantTail :: forall x xs. V xs -> V (x ': xs)
+{-# INLINABLE toVariantTail #-}
 toVariantTail (Variant t a) = Variant (t+1) a
 
 -- | Get the value if it has the indexed type
 fromVariantAt :: forall (n :: Nat) (l :: [*]).
    ( KnownNat n
-   ) => Variant l -> Maybe (Index n l)
-{-# INLINE fromVariantAt #-}
+   ) => V l -> Maybe (Index n l)
+{-# INLINABLE fromVariantAt #-}
 fromVariantAt (Variant t a) = do
    guard (t == natValue' @n)
    return (unsafeCoerce a) -- we know it is the effective type
@@ -220,8 +230,8 @@
 -- variant
 popVariantAt :: forall (n :: Nat) l. 
    ( KnownNat n
-   ) => Variant l -> Either (Variant (RemoveAt n l)) (Index n l)
-{-# INLINE popVariantAt #-}
+   ) => V l -> Either (V (RemoveAt n l)) (Index n l)
+{-# INLINABLE popVariantAt #-}
 popVariantAt v@(Variant t a) = case fromVariantAt @n v of
    Just x  -> Right x
    Nothing -> Left $ if t > natValue' @n
@@ -229,23 +239,36 @@
       else Variant t a
 
 -- | Pop the head of a variant value
-popVariantHead :: forall x xs. Variant (x ': xs) -> Either (Variant xs) x
-{-# INLINE popVariantHead #-}
+popVariantHead :: forall x xs. V (x ': xs) -> Either (V xs) x
+{-# INLINABLE popVariantHead #-}
 popVariantHead v@(Variant t a) = case fromVariantAt @0 v of
    Just x  -> Right x
    Nothing -> Left $ Variant (t-1) a
 
--- | Update a variant value
-updateVariantAt :: forall (n :: Nat) a b l.
+-- | Update a single variant value by index
+mapVariantAt :: forall (n :: Nat) a b l.
    ( KnownNat n
    , a ~ Index n l
-   ) => (a -> b) -> Variant l -> Variant (ReplaceN n b l)
-{-# INLINE updateVariantAt #-}
-updateVariantAt f v@(Variant t a) =
+   ) => (a -> b) -> V l -> V (ReplaceN n b l)
+{-# INLINABLE mapVariantAt #-}
+mapVariantAt f v@(Variant t a) =
    case fromVariantAt @n v of
       Nothing -> Variant t a
       Just x  -> Variant t (unsafeCoerce (f x))
 
+-- | Applicative update of a single variant value by index
+mapVariantAtM :: forall (n :: Nat) a b l m .
+   ( KnownNat n
+   , Applicative m
+   , a ~ Index n l
+   )
+   => (a -> m b) -> V l -> m (V (ReplaceN n b l))
+{-# INLINABLE mapVariantAtM #-}
+mapVariantAtM f v@(Variant t a) =
+   case fromVariantAt @n v of
+      Nothing -> pure (Variant t a)
+      Just x  -> Variant t <$> unsafeCoerce (f x)
+
 -----------------------------------------------------------
 -- Operations by type
 -----------------------------------------------------------
@@ -255,8 +278,8 @@
 -- Use the first matching type index.
 toVariant :: forall a l.
    ( Member a l
-   ) => a -> Variant l
-{-# INLINE toVariant #-}
+   ) => a -> V l
+{-# INLINABLE toVariant #-}
 toVariant = toVariantAt @(IndexOf a l)
 
 -- | Put a value into a Variant (silent)
@@ -264,15 +287,16 @@
 -- Use the first matching type index.
 toVariant' :: forall a l.
    ( Member' a l
-   ) => a -> Variant l
-{-# INLINE toVariant' #-}
+   ) => a -> V l
+{-# INLINABLE toVariant' #-}
 toVariant' = toVariantAt @(IndexOf a l)
 
 class PopVariant a xs where
    -- | Remove a type from a variant
-   popVariant' :: Variant xs -> Either (Variant (Filter a xs)) a
+   popVariant' :: V xs -> Either (V (Filter a xs)) a
 
 instance PopVariant a '[] where
+   {-# INLINE popVariant' #-}
    popVariant' _ = undefined
 
 instance forall a xs n xs' y ys.
@@ -292,49 +316,77 @@
               | n-1 < t   -> popVariant' @a @xs' (Variant (t-1) a)
               | otherwise -> Left (Variant t a)
 
--- | a is popable in xs
-type Popable a xs =
-   ( Member a xs
-   , PopVariant a xs
-   )
+class SplitVariant as rs xs where
+   splitVariant' :: V xs -> Either (V as) (V (Complement rs as))
 
--- | a may be popable in xs
-type MaybePopable a xs =
-   ( PopVariant a xs
-   )
+instance SplitVariant as rs '[] where
+   {-# INLINE splitVariant' #-}
+   splitVariant' _ = undefined
 
-type (:<) a xs  = Popable a xs
-type (:<?) a xs = MaybePopable a xs
+instance forall as rs xs x n m.
+   ( n ~ MaybeIndexOf x as
+   , m ~ IndexOf x rs
+   , SplitVariant as rs xs
+   , KnownNat m
+   , KnownNat n
+   ) => SplitVariant as rs (x ': xs)
+   where
+      {-# INLINE splitVariant' #-}
+      splitVariant' (Variant 0 v)
+         = case natValue' @n of
+            0 -> Right (Variant (natValue' @m) v)
+            t -> Left (Variant (t-1) v)
+      splitVariant' (Variant t v)
+         = splitVariant' @as @rs (Variant (t-1) v :: V xs)
 
+-- | Split a variant in two
+splitVariant :: forall as xs.
+   ( SplitVariant as xs xs
+   ) => V xs -> Either (V as) (V (Complement xs as))
+splitVariant = splitVariant' @as @xs
 
+-- | A value of type "x" can be extracted from (V xs)
+type (:<) x xs =
+   ( Member x xs
+   , x :<? xs
+   )
+
+-- | A value of type "x" **might** be extracted from (V xs).
+-- We don't check that "x" is in "xs".
+type (:<?) x xs =
+   ( PopVariant x xs
+   )
+
 -- | Extract a type from a variant. Return either the value of this type or the
 -- remaining variant
 popVariant :: forall a xs.
-   ( Popable a xs
-   ) => Variant xs -> Either (Variant (Filter a xs)) a
+   ( a :< xs
+   ) => V xs -> Either (V (Filter a xs)) a
+{-# INLINABLE popVariant #-}
 popVariant v = popVariant' @a v
 
 -- | Extract a type from a variant. Return either the value of this type or the
 -- remaining variant
 popVariantMaybe :: forall a xs.
-   ( MaybePopable a xs
-   ) => Variant xs -> Either (Variant (Filter a xs)) a
+   ( a :<? xs
+   ) => V xs -> Either (V (Filter a xs)) a
+{-# INLINABLE popVariantMaybe #-}
 popVariantMaybe v = popVariant' @a v
 
 -- | Pick the first matching type of a Variant
 --
--- fromVariantFirst @A (Variant 2 undefined :: Variant '[A,B,A]) == Nothing
+-- fromVariantFirst @A (Variant 2 undefined :: V '[A,B,A]) == Nothing
 fromVariantFirst :: forall a l.
    ( Member a l
-   ) => Variant l -> Maybe a
-{-# INLINE fromVariantFirst #-}
+   ) => V l -> Maybe a
+{-# INLINABLE fromVariantFirst #-}
 fromVariantFirst = fromVariantAt @(IndexOf a l)
 
 -- | Try to a get a value of a given type from a Variant
 fromVariant :: forall a xs.
-   ( Popable a xs
-   ) => Variant xs -> Maybe a
-{-# INLINE fromVariant #-}
+   ( a :< xs
+   ) => V xs -> Maybe a
+{-# INLINABLE fromVariant #-}
 fromVariant v = case popVariant v of
    Right a -> Just a
    Left _  -> Nothing
@@ -342,8 +394,8 @@
 -- | Try to a get a value of a given type from a Variant (silent)
 fromVariant' :: forall a xs.
    ( PopVariant a xs
-   ) => Variant xs -> Maybe a
-{-# INLINE fromVariant' #-}
+   ) => V xs -> Maybe a
+{-# INLINABLE fromVariant' #-}
 fromVariant' v = case popVariant' v of
    Right a -> Just a
    Left _  -> Nothing
@@ -351,66 +403,79 @@
 -- | Try to a get a value of a given type from a Variant that may not even
 -- support the given type.
 fromVariantMaybe :: forall a xs.
-   ( MaybePopable a xs
-   ) => Variant xs -> Maybe a
-{-# INLINE fromVariantMaybe #-}
+   ( a :<? xs
+   ) => V xs -> Maybe a
+{-# INLINABLE fromVariantMaybe #-}
 fromVariantMaybe v = case popVariantMaybe v of
    Right a -> Just a
    Left _  -> Nothing
 
--- | Update a variant value
-updateVariantFirst :: forall a b n l.
+-- | Update of the first matching variant value
+mapVariantFirst :: forall a b n l.
    ( Member a l
    , n ~ IndexOf a l
-   ) => (a -> b) -> Variant l -> Variant (ReplaceN n b l)
-{-# INLINE updateVariantFirst #-}
-updateVariantFirst f v = updateVariantAt @n f v
+   ) => (a -> b) -> V l -> V (ReplaceN n b l)
+{-# INLINABLE mapVariantFirst #-}
+mapVariantFirst f v = mapVariantAt @n f v
 
--- | Monadic update of the first matching variant value
-updateVariantFirstM :: forall (n :: Nat) l l2 m .
-   (KnownNat n, Monad m)
-   => (Index n l -> m (Index n l2)) -> Variant l -> m (Variant l2)
-{-# INLINE updateVariantFirstM #-}
-updateVariantFirstM f v@(Variant t a) =
-   case fromVariantAt @n v of
-      Nothing -> return (Variant t a)
-      Just x  -> Variant t <$> unsafeCoerce (f x)
+-- | Applicative update of the first matching variant value
+mapVariantFirstM :: forall a b n l m.
+   ( Member a l
+   , n ~ IndexOf a l
+   , Applicative m
+   ) => (a -> m b) -> V l -> m (V (ReplaceN n b l))
+{-# INLINABLE mapVariantFirstM #-}
+mapVariantFirstM f v = mapVariantAtM @n f v
 
-class MapVariant a b cs (is :: [Nat]) where
-   mapVariant' :: (a -> b) -> Variant cs -> Variant (ReplaceNS is b cs)
+class MapVariantIndexes a b cs (is :: [Nat]) where
+   mapVariant' :: (a -> b) -> V cs -> V (ReplaceNS is b cs)
 
-instance MapVariant a b '[] is where
+instance MapVariantIndexes a b '[] is where
    {-# INLINE mapVariant' #-}
    mapVariant' = undefined
 
-instance MapVariant a b cs '[] where
+instance MapVariantIndexes a b cs '[] where
    {-# INLINE mapVariant' #-}
    mapVariant' _ v = v
 
 instance forall a b cs is i.
-   ( MapVariant a b (ReplaceN i b cs) is
+   ( MapVariantIndexes a b (ReplaceN i b cs) is
    , a ~ Index i cs
    , KnownNat i
-   ) => MapVariant a b cs (i ': is) where
+   ) => MapVariantIndexes a b cs (i ': is) where
    {-# INLINE mapVariant' #-}
-   mapVariant' f v = mapVariant' @a @b @(ReplaceN i b cs) @is f (updateVariantAt @i f v)
+   mapVariant' f v = mapVariant' @a @b @(ReplaceN i b cs) @is f (mapVariantAt @i f v)
 
-type MappableVariant a b cs =
-   ( MapVariant a b cs (IndexesOf a cs)
+type MapVariant a b cs =
+   ( MapVariantIndexes a b cs (IndexesOf a cs)
    )
 
+type ReplaceAll a b cs = ReplaceNS (IndexesOf a cs) b cs
+
+
 -- | Map the matching types of a variant
 mapVariant :: forall a b cs.
-   ( MappableVariant a b cs
-   ) => (a -> b) -> Variant cs -> Variant (ReplaceNS (IndexesOf a cs) b cs)
+   ( MapVariant a b cs
+   ) => (a -> b) -> V cs -> V (ReplaceAll a b cs)
+{-# INLINABLE mapVariant #-}
 mapVariant = mapVariant' @a @b @cs @(IndexesOf a cs)
 
+-- | Map the matching types of a variant and nub the result
+mapNubVariant :: forall a b cs ds rs.
+   ( MapVariant a b cs
+   , ds ~ ReplaceNS (IndexesOf a cs) b cs
+   , rs ~ Nub ds
+   , Liftable ds rs
+   ) => (a -> b) -> V cs -> V rs
+{-# INLINABLE mapNubVariant #-}
+mapNubVariant f = nubVariant . mapVariant f
 
+
 -- | Update a variant value with a variant and fold the result
 foldMapVariantAt :: forall (n :: Nat) l l2 .
    ( KnownNat n
    , KnownNat (Length l2)
-   ) => (Index n l -> Variant l2) -> Variant l -> Variant (ReplaceAt n l l2)
+   ) => (Index n l -> V l2) -> V l -> V (ReplaceAt n l l2)
 foldMapVariantAt f v@(Variant t a) =
    case fromVariantAt @n v of
       Nothing ->
@@ -430,7 +495,7 @@
    ( KnownNat n
    , KnownNat (Length l2)
    , Monad m
-   ) => (Index n l -> m (Variant l2)) -> Variant l -> m (Variant (ReplaceAt n l l2))
+   ) => (Index n l -> m (V l2)) -> V l -> m (V (ReplaceAt n l l2))
 foldMapVariantAtM f v@(Variant t a) =
    case fromVariantAt @n v of
       Nothing ->
@@ -453,7 +518,7 @@
    , KnownNat (Length l2)
    , n ~ IndexOf a l
    , a ~ Index n l
-   ) => (a -> Variant l2) -> Variant l -> Variant (ReplaceAt n l l2)
+   ) => (a -> V l2) -> V l -> V (ReplaceAt n l l2)
 foldMapVariantFirst f v = foldMapVariantAt @n f v
 
 -- | Update a variant value with a variant and fold the result
@@ -471,7 +536,7 @@
 -- | Update a variant value with a variant and fold the result
 foldMapVariant :: forall a cs ds i.
    ( i ~ IndexOf a cs
-   , Popable a cs
+   , a :< cs
    ) => (a -> V ds) -> V cs -> V (InsertAt i (Filter a cs) ds)
 foldMapVariant f v = case popVariant v of
    Right a -> case f a of
@@ -489,12 +554,16 @@
 -- Generic operations with type classes
 -----------------------------------------------------------
 
+-- | Useful to specify a "* -> Constraint" function returning an empty constraint
+class NoConstraint a
+instance NoConstraint a
+
 class AlterVariant c (b :: [*]) where
-   alterVariant' :: Alter c -> Word -> Any -> Any
+   alterVariant' :: (forall a. c a => a -> a) -> Word -> Any -> Any
 
 instance AlterVariant c '[] where
    {-# INLINE alterVariant' #-}
-   alterVariant' = undefined
+   alterVariant' _ = undefined
 
 instance
    ( AlterVariant c xs
@@ -502,27 +571,40 @@
    ) => AlterVariant c (x ': xs)
    where
       {-# INLINE alterVariant' #-}
-      alterVariant' m@(Alter f) t v =
+      alterVariant' f t v =
          case t of
             0 -> unsafeCoerce (f (unsafeCoerce v :: x))
-            n -> alterVariant' @c @xs m (n-1) v
+            n -> alterVariant' @c @xs f (n-1) v
 
--- | Wrap a function and its constraints
-data Alter (c :: * -> Constraint) = Alter (forall a. c a => a -> a)
+-- | Alter a variant. You need to specify the constraints required by the
+-- modifying function.
+--
+-- Usage:
+--    alterVariant @NoConstraint id         v
+--    alterVariant @Resizable    (resize 4) v
+--
+--
+--    -- Multiple constraints:
+--    class (Ord a, Num a) => OrdNum a
+--    instance (Ord a, Num a) => OrdNum a
+--    alterVariant @OrdNum foo v
+--
+alterVariant :: forall c (a :: [*]).
+   ( AlterVariant c a
+   ) => (forall x. c x => x -> x) -> V a  -> V a
+{-# INLINABLE alterVariant #-}
+alterVariant f (Variant t a) = 
+   Variant t (alterVariant' @c @a f t a)
 
--- | Wrap a function and its constraints
-data AlterM (c :: * -> Constraint) m = AlterM (forall a. (Monad m, c a) => a -> m a)
 
--- | Useful to specify a "* -> Constraint" function returning no constraint
-class NoConstraint a
-instance NoConstraint a
 
+
 class TraverseVariant c (b :: [*]) m where
-   traverseVariant' :: AlterM c m -> Word -> Any -> m Any
+   traverseVariant' :: (forall a . (Monad m, c a) => a -> m a) -> Word -> Any -> m Any
 
 instance TraverseVariant c '[] m where
    {-# INLINE traverseVariant' #-}
-   traverseVariant' = undefined
+   traverseVariant' _ = undefined
 
 instance
    ( TraverseVariant c xs m
@@ -531,64 +613,81 @@
    ) => TraverseVariant c (x ': xs) m
    where
       {-# INLINE traverseVariant' #-}
-      traverseVariant' m@(AlterM f) t v =
+      traverseVariant' f t v =
          case t of
             0 -> unsafeCoerce <$> f (unsafeCoerce v :: x)
-            n -> traverseVariant' @c @xs m (n-1) v
+            n -> traverseVariant' @c @xs f (n-1) v
 
 
--- | Alter a variant. You need to specify the constraints required by the
--- modifying function.
---
--- Usage:
---    alterVariant @NoConstraint id         v
---    alterVariant @Resizable    (resize 4) v
---
---    class (Ord a, Num a) => OrdNum a
---    instance (Ord a, Num a) => OrdNum a
---
-{-# INLINE alterVariant #-}
-alterVariant :: forall c (a :: [*]).
-   ( AlterVariant c a
-   ) => (forall x. c x => x -> x) -> Variant a  -> Variant a
-alterVariant f (Variant t a) = 
-   Variant t (alterVariant' @c @a (Alter @c f) t a)
-
 -- | Traverse a variant. You need to specify the constraints required by the
 -- modifying function.
-{-# INLINE traverseVariant #-}
 traverseVariant :: forall c (a :: [*]) m.
    ( TraverseVariant c a m
    , Monad m
-   ) => (forall x. c x => x -> m x) -> Variant a  -> m (Variant a)
+   ) => (forall x. c x => x -> m x) -> V a  -> m (V a)
+{-# INLINABLE traverseVariant #-}
 traverseVariant f (Variant t a) = 
-   Variant t <$> traverseVariant' @c @a (AlterM @c @m f) t a
+   Variant t <$> traverseVariant' @c @a f t a
 
 -- | Traverse a variant. You need to specify the constraints required by the
 -- modifying function.
 traverseVariant_ :: forall c (a :: [*]) m.
    ( TraverseVariant c a m
    , Monad m
-   ) => (forall x. c x => x -> m ()) -> Variant a  -> m ()
+   ) => (forall x. c x => x -> m ()) -> V a -> m ()
+{-# INLINABLE traverseVariant_ #-}
 traverseVariant_ f v = void (traverseVariant @c @a f' v)
    where
       f' :: forall x. c x => x -> m x
       f' x = f x >> return x
 
+
+
+class ReduceVariant c r (b :: [*]) where
+   reduceVariant' :: (forall a. c a => a -> r) -> Word -> Any -> r
+
+instance ReduceVariant c r '[] where
+   {-# INLINE reduceVariant' #-}
+   reduceVariant' _ = undefined
+
+instance
+   ( ReduceVariant c r xs
+   , c x
+   ) => ReduceVariant c r (x ': xs)
+   where
+      {-# INLINE reduceVariant' #-}
+      reduceVariant' f t v =
+         case t of
+            0 -> f (unsafeCoerce v :: x)
+            n -> reduceVariant' @c @r @xs f (n-1) v
+
+-- | Reduce a variant to a single value by using a class function. You need to
+-- specify the constraints required by the modifying function.
+--
+-- Usage:
+--    reduceVariant @Show show v
+--
+reduceVariant :: forall c r (a :: [*]).
+   ( ReduceVariant c r a
+   ) => (forall x. c x => x -> r) -> V a  -> r
+{-# INLINABLE reduceVariant #-}
+reduceVariant f (Variant t a) = reduceVariant' @c @r @a f t a
+
+
 -----------------------------------------------------------
 -- Conversions between variants
 -----------------------------------------------------------
 
 -- | Extend a variant by appending other possible values
-appendVariant :: forall (ys :: [*]) (xs :: [*]). Variant xs -> Variant (Concat xs ys)
-{-# INLINE appendVariant #-}
+appendVariant :: forall (ys :: [*]) (xs :: [*]). V xs -> V (Concat xs ys)
+{-# INLINABLE appendVariant #-}
 appendVariant (Variant t a) = Variant t a
 
 -- | Extend a variant by prepending other possible values
 prependVariant :: forall (ys :: [*]) (xs :: [*]).
    ( KnownNat (Length ys)
-   ) => Variant xs -> Variant (Concat ys xs)
-{-# INLINE prependVariant #-}
+   ) => V xs -> V (Concat ys xs)
+{-# INLINABLE prependVariant #-}
 prependVariant (Variant t a) = Variant (n+t) a
    where
       n = natValue' @(Length ys)
@@ -600,10 +699,11 @@
    )
 
 class LiftVariant xs ys where
-   liftVariant' :: Variant xs -> Variant ys
+   liftVariant' :: V xs -> V ys
 
 instance LiftVariant '[] ys where
-   liftVariant' = error "Lifting empty variant"
+   {-# INLINE liftVariant' #-}
+   liftVariant' _ = undefined
 
 instance forall xs ys x.
       ( LiftVariant xs ys
@@ -619,39 +719,41 @@
 -- | Lift a variant into another
 --
 -- Set values to the first matching type
-liftVariant :: forall xs ys.
+liftVariant :: forall ys xs.
    ( Liftable xs ys
-   ) => Variant xs -> Variant ys
-{-# INLINE liftVariant #-}
+   ) => V xs -> V ys
+{-# INLINABLE liftVariant #-}
 liftVariant = liftVariant'
 
 -- | Nub the type list
 nubVariant :: (Liftable xs (Nub xs)) => V xs -> V (Nub xs)
+{-# INLINABLE nubVariant #-}
 nubVariant = liftVariant
 
 -- | Product of two variants
 productVariant :: forall xs ys.
    ( KnownNat (Length ys)
-   ) => Variant xs -> Variant ys -> Variant (Product xs ys)
+   ) => V xs -> V ys -> V (Product xs ys)
+{-# INLINABLE productVariant #-}
 productVariant (Variant n1 a1) (Variant n2 a2)
    = Variant (n1 * natValue @(Length ys) + n2) (unsafeCoerce (a1,a2))
 
 type family FlattenVariant (xs :: [*]) :: [*] where
-   FlattenVariant '[]             = '[]
-   FlattenVariant (Variant xs:ys) = Concat xs (FlattenVariant ys)
-   FlattenVariant (y:ys)          = y ': FlattenVariant ys
+   FlattenVariant '[]       = '[]
+   FlattenVariant (V xs:ys) = Concat xs (FlattenVariant ys)
+   FlattenVariant (y:ys)    = y ': FlattenVariant ys
 
 class Flattenable a rs where
    toFlattenVariant :: Word -> a -> rs
 
-instance Flattenable (Variant '[]) rs where
+instance Flattenable (V '[]) rs where
    {-# INLINE toFlattenVariant #-}
    toFlattenVariant _ _ = undefined
 
 instance forall xs ys rs.
-   ( Flattenable (Variant ys) (Variant rs)
+   ( Flattenable (V ys) (V rs)
    , KnownNat (Length xs)
-   ) => Flattenable (Variant (Variant xs ': ys)) (Variant rs)
+   ) => Flattenable (V (V xs ': ys)) (V rs)
    where
    {-# INLINE toFlattenVariant #-}
    toFlattenVariant i v = case popVariantHead v of
@@ -660,48 +762,81 @@
 
 -- | Flatten variants in a variant
 flattenVariant :: forall xs.
-   ( Flattenable (Variant xs) (Variant (FlattenVariant xs))
-   ) => Variant xs -> Variant (FlattenVariant xs)
+   ( Flattenable (V xs) (V (FlattenVariant xs))
+   ) => V xs -> V (FlattenVariant xs)
+{-# INLINABLE flattenVariant #-}
 flattenVariant v = toFlattenVariant 0 v
 
-type family ExtractMonad m f where
-   ExtractMonad m '[m x]      = '[x]
-   ExtractMonad m (m x ': xs) = x ': ExtractMonad m xs
+type family ExtractM m f where
+   ExtractM m '[]         = '[]
+   ExtractM m (m x ': xs) = x ': ExtractM m xs
 
--- | Join on a variant
+class JoinVariant m xs where
+   -- | Join on a variant
+   --
+   -- Transform a variant of applicatives as follow:
+   --    f :: V '[m a, m b, m c] -> m (V '[a,b,c])
+   --    f = joinVariant @m
+   --
+   joinVariant :: V xs -> m (V (ExtractM m xs))
+
+instance JoinVariant m '[] where
+   {-# INLINE joinVariant #-}
+   joinVariant _ = undefined
+
+instance forall m xs a.
+   ( Functor m
+   , ExtractM m (m a ': xs) ~ (a ': ExtractM m xs)
+   , JoinVariant m xs
+   ) => JoinVariant m (m a ': xs) where
+   {-# INLINE joinVariant #-}
+   joinVariant (Variant 0 a) = (Variant 0 . unsafeCoerce) <$> (unsafeCoerce a :: m a)
+   joinVariant (Variant n a) = prependVariant @'[a] <$> joinVariant (Variant (n-1) a :: V xs)
+
+-- | Join on a variant in an unsafe way.
 --
--- Transform a variant of applicatives as follow:
---    V'[m a, m b, m c] ===> m (V'[a,b,c])
+-- Works with IO for example but not with Maybe.
 --
-joinVariant :: forall m xs ys.
-   ( Applicative m
-   , ys ~ ExtractMonad m xs
-   ) => Variant xs -> m (Variant ys)
-joinVariant (Variant t act) = Variant t <$> (unsafeCoerce act :: m Any)
+joinVariantUnsafe :: forall m xs ys.
+   ( Functor m
+   , ys ~ ExtractM m xs
+   ) => V xs -> m (V ys)
+{-# INLINABLE joinVariantUnsafe #-}
+joinVariantUnsafe (Variant t act) = Variant t <$> (unsafeCoerce act :: m Any)
 
+
+
 -----------------------------------------------------------
 -- Conversions to other data types
 -----------------------------------------------------------
 
 -- | Retrieve a single value
-variantToValue :: Variant '[a] -> a
-{-# INLINE variantToValue #-}
+variantToValue :: V '[a] -> a
+{-# INLINABLE variantToValue #-}
 variantToValue (Variant _ a) = unsafeCoerce a
 
 -- | Create a variant from a single value
-variantFromValue :: a -> Variant '[a]
-{-# INLINE variantFromValue #-}
+variantFromValue :: a -> V '[a]
+{-# INLINABLE variantFromValue #-}
 variantFromValue a = Variant 0 (unsafeCoerce a)
 
 
 -- | Convert a variant of two values in a Either
-variantToEither :: forall a b. Variant '[a,b] -> Either b a
+variantToEither :: forall a b. V '[a,b] -> Either b a
+{-# INLINABLE variantToEither #-}
 variantToEither (Variant 0 a) = Right (unsafeCoerce a)
 variantToEither (Variant _ a) = Left (unsafeCoerce a)
 
+-- | Lift an Either into a Variant (reversed order by convention)
+variantFromEither :: Either a b -> V '[b,a]
+{-# INLINABLE variantFromEither #-}
+variantFromEither (Left a)  = toVariantAt @1 a
+variantFromEither (Right b) = toVariantAt @0 b
+
+
 class VariantToHList xs where
    -- | Convert a variant into a HList of Maybes
-   variantToHList :: Variant xs -> HList (Map Maybe xs)
+   variantToHList :: V xs -> HList (Map Maybe xs)
 
 instance VariantToHList '[] where
    variantToHList _ = HNil
@@ -713,36 +848,30 @@
       variantToHList v@(Variant t a) =
             fromVariantAt @0 v `HCons` variantToHList v'
          where
-            v' :: Variant xs
+            v' :: V xs
             v' = Variant (t-1) a
 
 -- | Get variant possible values in a tuple of Maybe types
 variantToTuple :: forall l t.
    ( VariantToHList l
    , HTuple' (Map Maybe l) t
-   ) => Variant l -> t
+   ) => V l -> t
 variantToTuple = hToTuple' . variantToHList
 
 
--- | Lift an Either into a Variant (reversed order by convention)
-variantFromEither :: Either a b -> Variant '[b,a]
-{-# INLINE variantFromEither #-}
-variantFromEither (Left a)  = toVariantAt @1 a
-variantFromEither (Right b) = toVariantAt @0 b
 
-
 class ContVariant xs where
    -- | Convert a variant into a multi-continuation
-   variantToCont :: Variant xs -> ContFlow xs r
+   variantToCont :: V xs -> ContFlow xs r
 
    -- | Convert a variant into a multi-continuation
-   variantToContM :: Monad m => m (Variant xs) -> ContFlow xs (m r)
+   variantToContM :: Monad m => m (V xs) -> ContFlow xs (m r)
 
    -- | Convert a multi-continuation into a Variant
-   contToVariant :: ContFlow xs (Variant xs) -> Variant xs
+   contToVariant :: ContFlow xs (V xs) -> V xs
 
    -- | Convert a multi-continuation into a Variant
-   contToVariantM :: Monad m => ContFlow xs (m (Variant xs)) -> m (Variant xs)
+   contToVariantM :: Monad m => ContFlow xs (m (V xs)) -> m (V xs)
 
 instance ContVariant '[a] where
    {-# INLINE variantToCont #-}
diff --git a/src/lib/Haskus/Utils/Variant/Flow.hs b/src/lib/Haskus/Utils/Variant/Flow.hs
--- a/src/lib/Haskus/Utils/Variant/Flow.hs
+++ b/src/lib/Haskus/Utils/Variant/Flow.hs
@@ -26,8 +26,8 @@
    , flowTraverseFilter
    , flowForFilter
    , Liftable
-   , Popable
-   , MaybePopable
+   , (:<)
+   , (:<?)
    -- * Functor, applicative equivalents
    , (<$<)
    , (<*<)
@@ -198,7 +198,7 @@
 import Haskus.Utils.Tuple
 
 -- | Control-flow
-type Flow m (l :: [*]) = m (Variant l)
+type Flow m (l :: [*]) = m (V l)
 
 type IOV l = Flow IO l
 
@@ -211,22 +211,22 @@
    ( Monad m
    , KnownNat n
    ) => Index n xs -> Flow m xs
-{-# INLINE flowSetN #-}
+{-# INLINABLE flowSetN #-}
 flowSetN = return . toVariantAt @n
 
 -- | Return in the first well-typed element
 flowSet :: (Member x xs, Monad m) => x -> Flow m xs
-{-# INLINE flowSet #-}
+{-# INLINABLE flowSet #-}
 flowSet = return . toVariant
 
 -- | Return a single element
 flowSingle :: Monad m => x -> Flow m '[x]
-{-# INLINE flowSingle #-}
+{-# INLINABLE flowSingle #-}
 flowSingle = flowSetN @0
 
 -- | Lift a flow into another
 flowLift :: (Liftable xs ys , Monad m) => Flow m xs -> Flow m ys
-{-# INLINE flowLift #-}
+{-# INLINABLE flowLift #-}
 flowLift = fmap liftVariant
 
 -- | Lift a flow into a ContFlow
@@ -274,13 +274,13 @@
 
 -- | Extract single flow result
 flowRes :: Functor m => Flow m '[x] -> m x
-{-# INLINE flowRes #-}
+{-# INLINABLE flowRes #-}
 flowRes = fmap variantToValue
 
 
 -- | Lift an operation on a Variant into an operation on a flow
-liftm :: Monad m => (Variant x -> a -> m b) -> Flow m x -> a -> m b
-{-# INLINE liftm #-}
+liftm :: Monad m => (V x -> a -> m b) -> Flow m x -> a -> m b
+{-# INLINABLE liftm #-}
 liftm op x a = do
    x' <- x
    op x' a
@@ -291,7 +291,7 @@
 
 -- | Map a pure function onto the correct value in the flow
 flowMap :: Monad m => Flow m (x ': xs) -> (x -> y) -> Flow m (y ': xs)
-{-# INLINE flowMap #-}
+{-# INLINABLE flowMap #-}
 flowMap = (>.-.>)
 
 -- | Bind two flows in a monadish way (error types union)
@@ -301,29 +301,29 @@
    , zs ~ Union xs ys
    , Monad m
    ) => Flow m (x ': ys) -> (x -> Flow m xs) -> Flow m zs
-{-# INLINE flowBind #-}
+{-# INLINABLE flowBind #-}
 flowBind = (>.~|>)
 
 -- | Bind two flows in a monadic way (constant error types)
 flowBind' :: Monad m => Flow m (x ': xs) -> (x -> Flow m (y ': xs)) -> Flow m (y ': xs)
-{-# INLINE flowBind' #-}
+{-# INLINABLE flowBind' #-}
 flowBind' = (>.~$>)
 
 -- | Match a value in a flow
 flowMatch :: forall x xs zs m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    , Liftable (Filter x xs) zs
    ) => Flow m xs -> (x -> Flow m zs) -> Flow m zs
-{-# INLINE flowMatch #-}
+{-# INLINABLE flowMatch #-}
 flowMatch = (>%~^>)
 
 -- | Match a value in a flow and use a non-returning failure in this case
 flowMatchFail :: forall x xs m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    ) => Flow m xs -> (x -> m ()) -> Flow m (Filter x xs)
-{-# INLINE flowMatchFail #-}
+{-# INLINABLE flowMatchFail #-}
 flowMatchFail = (>%~!!>)
 
 ----------------------------------------------------------
@@ -333,8 +333,8 @@
 -- | Extract the first value, set the first value
 (.~.>) :: forall m l x a.
    ( Monad m )
-   => Variant (a ': l) -> (a -> m x) -> Flow m (x ': l)
-{-# INLINE (.~.>) #-}
+   => V (a ': l) -> (a -> m x) -> Flow m (x ': l)
+{-# INLINABLE (.~.>) #-}
 (.~.>) v f = makeFlowOp selectFirst (applyM f) combineFirst v
 
 infixl 0 .~.>
@@ -343,7 +343,7 @@
 (>.~.>) :: forall m l x a.
    ( Monad m )
    => Flow m (a ': l) -> (a -> m x) -> Flow m (x ': l)
-{-# INLINE (>.~.>) #-}
+{-# INLINABLE (>.~.>) #-}
 (>.~.>) = liftm (.~.>)
 
 infixl 0 >.~.>
@@ -353,8 +353,8 @@
    ( KnownNat k
    , k ~ Length l2
    , Monad m )
-   => Variant (a ': l) -> (a -> Flow m l2) -> Flow m (Concat l2 l)
-{-# INLINE (.~+>) #-}
+   => V (a ': l) -> (a -> Flow m l2) -> Flow m (Concat l2 l)
+{-# INLINABLE (.~+>) #-}
 (.~+>) v f = makeFlowOp selectFirst (applyF f) combineConcat v
 
 infixl 0 .~+>
@@ -365,7 +365,7 @@
    , k ~ Length l2
    , Monad m )
    => Flow m (a ': l) -> (a -> Flow m l2) -> Flow m (Concat l2 l)
-{-# INLINE (>.~+>) #-}
+{-# INLINABLE (>.~+>) #-}
 (>.~+>) = liftm (.~+>)
 
 infixl 0 >.~+>
@@ -375,8 +375,8 @@
    ( Monad m
    , Liftable xs zs
    , Liftable ys zs
-   ) => Variant (a ': ys) -> (a -> Flow m xs) -> Flow m zs
-{-# INLINE (.~^^>) #-}
+   ) => V (a ': ys) -> (a -> Flow m xs) -> Flow m zs
+{-# INLINABLE (.~^^>) #-}
 (.~^^>) v f = makeFlowOp selectFirst (applyF f) combineLiftBoth v
 
 infixl 0 .~^^>
@@ -388,7 +388,7 @@
    , Liftable xs zs
    , Liftable ys zs
    ) => Flow m (a ': ys) -> (a -> Flow m xs) -> Flow m zs
-{-# INLINE (>.~^^>) #-}
+{-# INLINABLE (>.~^^>) #-}
 (>.~^^>) = liftm (.~^^>)
 
 infixl 0 >.~^^>
@@ -397,8 +397,8 @@
 (.~^>) :: forall m a ys zs.
    ( Monad m
    , Liftable ys zs
-   ) => Variant (a ': ys) -> (a -> Flow m zs) -> Flow m zs
-{-# INLINE (.~^>) #-}
+   ) => V (a ': ys) -> (a -> Flow m zs) -> Flow m zs
+{-# INLINABLE (.~^>) #-}
 (.~^>) v f = makeFlowOp selectFirst (applyF f) combineLiftUnselected v
 
 infixl 0 .~^>
@@ -408,7 +408,7 @@
    ( Monad m
    , Liftable ys zs
    ) => Flow m (a ': ys) -> (a -> Flow m zs) -> Flow m zs
-{-# INLINE (>.~^>) #-}
+{-# INLINABLE (>.~^>) #-}
 (>.~^>) = liftm (.~^>)
 
 infixl 0 >.~^>
@@ -416,8 +416,8 @@
 -- | Extract the first value, use the same tail
 (.~$>) :: forall m x xs a.
    ( Monad m
-   ) => Variant (a ': xs) -> (a -> Flow m (x ': xs)) -> Flow m (x ': xs)
-{-# INLINE (.~$>) #-}
+   ) => V (a ': xs) -> (a -> Flow m (x ': xs)) -> Flow m (x ': xs)
+{-# INLINABLE (.~$>) #-}
 (.~$>) v f = makeFlowOp selectFirst (applyF f) combineSameTail v
 
 infixl 0 .~$>
@@ -426,7 +426,7 @@
 (>.~$>) :: forall m x xs a.
    ( Monad m
    ) => Flow m (a ': xs) -> (a -> Flow m (x ': xs)) -> Flow m (x ': xs)
-{-# INLINE (>.~$>) #-}
+{-# INLINABLE (>.~$>) #-}
 (>.~$>) = liftm (.~$>)
 
 infixl 0 >.~$>
@@ -437,8 +437,8 @@
    , Liftable ys zs
    , zs ~ Union xs ys
    , Monad m
-   ) => Variant (a ': ys) -> (a -> Flow m xs) -> Flow m zs
-{-# INLINE (.~|>) #-}
+   ) => V (a ': ys) -> (a -> Flow m xs) -> Flow m zs
+{-# INLINABLE (.~|>) #-}
 (.~|>) v f = makeFlowOp selectFirst (applyF f) combineUnion v
 
 infixl 0 .~|>
@@ -450,7 +450,7 @@
    , zs ~ Union xs ys
    , Monad m
    ) => Flow m (a ': ys) -> (a -> Flow m xs) -> Flow m zs
-{-# INLINE (>.~|>) #-}
+{-# INLINABLE (>.~|>) #-}
 (>.~|>) = liftm (.~|>)
 
 infixl 0 >.~|>
@@ -458,8 +458,8 @@
 -- | Extract the first value and perform effect. Passthrough the input value
 (.~=>) ::
    ( Monad m
-   ) => Variant (a ': l) -> (a -> m ()) -> Flow m (a ': l)
-{-# INLINE (.~=>) #-}
+   ) => V (a ': l) -> (a -> m ()) -> Flow m (a ': l)
+{-# INLINABLE (.~=>) #-}
 (.~=>) v f = case popVariantHead v of
    Right u -> f u >> return v
    Left  _ -> return v
@@ -470,7 +470,7 @@
 (>.~=>) ::
    ( Monad m
    ) => Flow m (a ': l) -> (a -> m ()) -> Flow m (a ': l)
-{-# INLINE (>.~=>) #-}
+{-# INLINABLE (>.~=>) #-}
 (>.~=>) = liftm (.~=>)
 
 infixl 0 >.~=>
@@ -478,8 +478,8 @@
 -- | Extract the first value and perform effect.
 (.~!>) ::
    ( Monad m
-   ) => Variant (a ': l) -> (a -> m ()) -> m ()
-{-# INLINE (.~!>) #-}
+   ) => V (a ': l) -> (a -> m ()) -> m ()
+{-# INLINABLE (.~!>) #-}
 (.~!>) v f = case popVariantHead v of
    Right u -> f u
    Left  _ -> return ()
@@ -490,7 +490,7 @@
 (>.~!>) ::
    ( Monad m
    ) => Flow m (a ': l) -> (a -> m ()) -> m ()
-{-# INLINE (>.~!>) #-}
+{-# INLINABLE (>.~!>) #-}
 (>.~!>) = liftm (.~!>)
 
 infixl 0 >.~!>
@@ -498,8 +498,8 @@
 -- | Extract the first value and perform effect.
 (.~!!>) ::
    ( Monad m
-   ) => Variant (a ': l) -> (a -> m ()) -> m (Variant l)
-{-# INLINE (.~!!>) #-}
+   ) => V (a ': l) -> (a -> m ()) -> m (V l)
+{-# INLINABLE (.~!!>) #-}
 (.~!!>) v f = case popVariantHead v of
    Right u -> f u >> error ".~!!> error"
    Left  l -> return l
@@ -509,8 +509,8 @@
 -- | Extract the first value and perform effect.
 (>.~!!>) ::
    ( Monad m
-   ) => Flow m (a ': l) -> (a -> m ()) -> m (Variant l)
-{-# INLINE (>.~!!>) #-}
+   ) => Flow m (a ': l) -> (a -> m ()) -> m (V l)
+{-# INLINABLE (>.~!!>) #-}
 (>.~!!>) = liftm (.~!!>)
 
 infixl 0 >.~!!>
@@ -522,8 +522,8 @@
 -- | Extract the first value, set the first value
 (.-.>) :: forall m l x a.
    ( Monad m )
-   => Variant (a ': l) -> (a -> x) -> Flow m (x ': l)
-{-# INLINE (.-.>) #-}
+   => V (a ': l) -> (a -> x) -> Flow m (x ': l)
+{-# INLINABLE (.-.>) #-}
 (.-.>) v f = makeFlowOp selectFirst (applyPure (liftV f)) combineFirst v
 
 infixl 0 .-.>
@@ -532,7 +532,7 @@
 (>.-.>) :: forall m l x a.
    ( Monad m )
    => Flow m (a ': l) -> (a -> x) -> Flow m (x ': l)
-{-# INLINE (>.-.>) #-}
+{-# INLINABLE (>.-.>) #-}
 (>.-.>) = liftm (.-.>)
 
 infixl 0 >.-.>
@@ -540,8 +540,8 @@
 -- | Extract the first value, set the first value
 (<.-.) :: forall m l x a.
    ( Monad m )
-   => (a -> x) -> Variant (a ': l) -> Flow m (x ': l)
-{-# INLINE (<.-.) #-}
+   => (a -> x) -> V (a ': l) -> Flow m (x ': l)
+{-# INLINABLE (<.-.) #-}
 (<.-.) = flip (.-.>)
 
 infixr 0 <.-.
@@ -550,7 +550,7 @@
 (<.-.<) :: forall m l x a.
    ( Monad m )
    => (a -> x) -> Flow m (a ': l) -> Flow m (x ': l)
-{-# INLINE (<.-.<) #-}
+{-# INLINABLE (<.-.<) #-}
 (<.-.<) = flip (>.-.>)
 
 infixr 0 <.-.<
@@ -563,7 +563,7 @@
 (<$<) :: forall m l a b.
    ( Monad m )
    => (a -> b) -> Flow m (a ': l) -> Flow m (b ': l)
-{-# INLINE (<$<) #-}
+{-# INLINABLE (<$<) #-}
 (<$<) = (<.-.<)
 
 infixl 4 <$<
@@ -572,7 +572,7 @@
 (<*<) :: forall m l a b.
    ( Monad m )
    => Flow m ((a -> b) ': l) -> Flow m (a ': l) -> Flow m (b ': l)
-{-# INLINE (<*<) #-}
+{-# INLINABLE (<*<) #-}
 (<*<) mf mg = mf >.~$> (mg >.-.>)
 
 infixl 4 <*<
@@ -584,7 +584,7 @@
    , Liftable ys zs
    , zs ~ Union xs ys
    ) => Flow m ((y -> z) ': xs) -> Flow m (y ': ys) -> Flow m (z ': zs)
-{-# INLINE (<|<) #-}
+{-# INLINABLE (<|<) #-}
 (<|<) mf mg = 
    mf >..-..> liftVariant
       >.~$> (\f -> mg >..-..> liftVariant
@@ -600,8 +600,8 @@
 -- | Extract the first value, set the first value
 (.~~.>) :: forall m l x a.
    ( Monad m )
-   => Variant (a ': l) -> m x -> Flow m (x ': l)
-{-# INLINE (.~~.>) #-}
+   => V (a ': l) -> m x -> Flow m (x ': l)
+{-# INLINABLE (.~~.>) #-}
 (.~~.>) v f = v .~.> const f
 
 infixl 0 .~~.>
@@ -610,7 +610,7 @@
 (>.~~.>) :: forall m l x a.
    ( Monad m )
    => Flow m (a ': l) -> m x -> Flow m (x ': l)
-{-# INLINE (>.~~.>) #-}
+{-# INLINABLE (>.~~.>) #-}
 (>.~~.>) = liftm (.~~.>)
 
 infixl 0 >.~~.>
@@ -620,8 +620,8 @@
    ( KnownNat k
    , k ~ Length l2
    , Monad m )
-   => Variant (a ': l) -> Flow m l2 -> Flow m (Concat l2 l)
-{-# INLINE (.~~+>) #-}
+   => V (a ': l) -> Flow m l2 -> Flow m (Concat l2 l)
+{-# INLINABLE (.~~+>) #-}
 (.~~+>) v f = v .~+> const f
 
 infixl 0 .~~+>
@@ -632,7 +632,7 @@
    , k ~ Length l2
    , Monad m )
    => Flow m (a ': l) -> Flow m l2 -> Flow m (Concat l2 l)
-{-# INLINE (>.~~+>) #-}
+{-# INLINABLE (>.~~+>) #-}
 (>.~~+>) = liftm (.~~+>)
 
 infixl 0 >.~~+>
@@ -642,8 +642,8 @@
    ( Monad m
    , Liftable xs zs
    , Liftable ys zs
-   ) => Variant (a ': ys) -> Flow m xs -> Flow m zs
-{-# INLINE (.~~^^>) #-}
+   ) => V (a ': ys) -> Flow m xs -> Flow m zs
+{-# INLINABLE (.~~^^>) #-}
 (.~~^^>) v f = v .~^^> const f
 
 infixl 0 .~~^^>
@@ -655,7 +655,7 @@
    , Liftable xs zs
    , Liftable ys zs
    ) => Flow m (a ': ys) -> Flow m xs -> Flow m zs
-{-# INLINE (>.~~^^>) #-}
+{-# INLINABLE (>.~~^^>) #-}
 (>.~~^^>) = liftm (.~~^^>)
 
 infixl 0 >.~~^^>
@@ -664,8 +664,8 @@
 (.~~^>) :: forall m a ys zs.
    ( Monad m
    , Liftable ys zs
-   ) => Variant (a ': ys) -> Flow m zs -> Flow m zs
-{-# INLINE (.~~^>) #-}
+   ) => V (a ': ys) -> Flow m zs -> Flow m zs
+{-# INLINABLE (.~~^>) #-}
 (.~~^>) v f = v .~^> const f
 
 infixl 0 .~~^>
@@ -675,7 +675,7 @@
    ( Monad m
    , Liftable ys zs
    ) => Flow m (a ': ys) -> Flow m zs -> Flow m zs
-{-# INLINE (>.~~^>) #-}
+{-# INLINABLE (>.~~^>) #-}
 (>.~~^>) = liftm (.~~^>)
 
 infixl 0 >.~~^>
@@ -683,8 +683,8 @@
 -- | Extract the first value, use the same output type
 (.~~$>) :: forall m x xs a.
    ( Monad m
-   ) => Variant (a ': xs) -> Flow m (x ': xs) -> Flow m (x ': xs)
-{-# INLINE (.~~$>) #-}
+   ) => V (a ': xs) -> Flow m (x ': xs) -> Flow m (x ': xs)
+{-# INLINABLE (.~~$>) #-}
 (.~~$>) v f = v .~$> const f
 
 infixl 0 .~~$>
@@ -693,7 +693,7 @@
 (>.~~$>) :: forall m x xs a.
    ( Monad m
    ) => Flow m (a ': xs) -> Flow m (x ': xs) -> Flow m (x ': xs)
-{-# INLINE (>.~~$>) #-}
+{-# INLINABLE (>.~~$>) #-}
 (>.~~$>) = liftm (.~~$>)
 
 infixl 0 >.~~$>
@@ -704,8 +704,8 @@
    , Liftable ys zs
    , zs ~ Union xs ys
    , Monad m
-   ) => Variant (a ': ys) -> Flow m xs -> Flow m zs
-{-# INLINE (.~~|>) #-}
+   ) => V (a ': ys) -> Flow m xs -> Flow m zs
+{-# INLINABLE (.~~|>) #-}
 (.~~|>) v f = v .~|> const f
 
 infixl 0 .~~|>
@@ -717,7 +717,7 @@
    , zs ~ Union xs ys
    , Monad m
    ) => Flow m (a ': ys) -> Flow m xs -> Flow m zs
-{-# INLINE (>.~~|>) #-}
+{-# INLINABLE (>.~~|>) #-}
 (>.~~|>) = liftm (.~~|>)
 
 infixl 0 >.~~|>
@@ -725,8 +725,8 @@
 -- | Extract the first value and perform effect. Passthrough the input value
 (.~~=>) ::
    ( Monad m
-   ) => Variant (a ': l) -> m () -> Flow m (a ': l)
-{-# INLINE (.~~=>) #-}
+   ) => V (a ': l) -> m () -> Flow m (a ': l)
+{-# INLINABLE (.~~=>) #-}
 (.~~=>) v f = v .~=> const f
 
 infixl 0 .~~=>
@@ -735,7 +735,7 @@
 (>.~~=>) ::
    ( Monad m
    ) => Flow m (a ': l) -> m () -> Flow m (a ': l)
-{-# INLINE (>.~~=>) #-}
+{-# INLINABLE (>.~~=>) #-}
 (>.~~=>) = liftm (.~~=>)
 
 infixl 0 >.~~=>
@@ -743,8 +743,8 @@
 -- | Extract the first value and perform effect.
 (.~~!>) ::
    ( Monad m
-   ) => Variant (a ': l) -> m () -> m ()
-{-# INLINE (.~~!>) #-}
+   ) => V (a ': l) -> m () -> m ()
+{-# INLINABLE (.~~!>) #-}
 (.~~!>) v f = v .~!> const f
 
 infixl 0 .~~!>
@@ -753,7 +753,7 @@
 (>.~~!>) ::
    ( Monad m
    ) => Flow m (a ': l) -> m () -> m ()
-{-# INLINE (>.~~!>) #-}
+{-# INLINABLE (>.~~!>) #-}
 (>.~~!>) = liftm (.~~!>)
 
 infixl 0 >.~~!>
@@ -766,8 +766,8 @@
 -- | Extract the tail, set the first value
 (..~.>) ::
    ( Monad m
-   ) => Variant (a ': l) -> (Variant l -> m a) -> m a
-{-# INLINE (..~.>) #-}
+   ) => V (a ': l) -> (V l -> m a) -> m a
+{-# INLINABLE (..~.>) #-}
 (..~.>) v f = makeFlowOp selectTail (applyVM f) combineSingle v
 
 infixl 0 ..~.>
@@ -775,8 +775,8 @@
 -- | Extract the tail, set the first value
 (>..~.>) ::
    ( Monad m
-   ) => Flow m (a ': l) -> (Variant l -> m a) -> m a
-{-# INLINE (>..~.>) #-}
+   ) => Flow m (a ': l) -> (V l -> m a) -> m a
+{-# INLINABLE (>..~.>) #-}
 (>..~.>) = liftm (..~.>)
 
 infixl 0 >..~.>
@@ -784,8 +784,8 @@
 -- | Extract the tail, set the first value (pure function)
 (..-.>) ::
    ( Monad m
-   ) => Variant (a ': l) -> (Variant l -> a) -> m a
-{-# INLINE (..-.>) #-}
+   ) => V (a ': l) -> (V l -> a) -> m a
+{-# INLINABLE (..-.>) #-}
 (..-.>) v f = case popVariantHead v of
    Right u -> return u
    Left  l -> return (f l)
@@ -795,8 +795,8 @@
 -- | Extract the tail, set the first value (pure function)
 (>..-.>) ::
    ( Monad m
-   ) => Flow m (a ': l) -> (Variant l -> a) -> m a
-{-# INLINE (>..-.>) #-}
+   ) => Flow m (a ': l) -> (V l -> a) -> m a
+{-# INLINABLE (>..-.>) #-}
 (>..-.>) = liftm (..-.>)
 
 infixl 0 >..-.>
@@ -804,8 +804,8 @@
 -- | Extract the tail, set the tail
 (..-..>) :: forall a l xs m.
    ( Monad m
-   ) => Variant (a ': l) -> (Variant l -> Variant xs) -> Flow m (a ': xs)
-{-# INLINE (..-..>) #-}
+   ) => V (a ': l) -> (V l -> V xs) -> Flow m (a ': xs)
+{-# INLINABLE (..-..>) #-}
 (..-..>) v f = case popVariantHead v of
    Right u -> flowSetN @0 u
    Left  l -> return (prependVariant @'[a] (f l))
@@ -815,8 +815,8 @@
 -- | Extract the tail, set the tail
 (>..-..>) ::
    ( Monad m
-   ) => Flow m (a ': l) -> (Variant l -> Variant xs) -> Flow m (a ': xs)
-{-# INLINE (>..-..>) #-}
+   ) => Flow m (a ': l) -> (V l -> V xs) -> Flow m (a ': xs)
+{-# INLINABLE (>..-..>) #-}
 (>..-..>) = liftm (..-..>)
 
 infixl 0 >..-..>
@@ -824,8 +824,8 @@
 -- | Extract the tail, set the tail
 (..~..>) :: forall a l xs m.
    ( Monad m
-   ) => Variant (a ': l) -> (Variant l -> Flow m xs) -> Flow m (a ': xs)
-{-# INLINE (..~..>) #-}
+   ) => V (a ': l) -> (V l -> Flow m xs) -> Flow m (a ': xs)
+{-# INLINABLE (..~..>) #-}
 (..~..>) v f = case popVariantHead v of
    Right u -> flowSetN @0 u
    Left  l -> prependVariant @'[a] <$> f l
@@ -835,8 +835,8 @@
 -- | Extract the tail, set the tail
 (>..~..>) ::
    ( Monad m
-   ) => Flow m (a ': l) -> (Variant l -> Flow m xs) -> Flow m (a ': xs)
-{-# INLINE (>..~..>) #-}
+   ) => Flow m (a ': l) -> (V l -> Flow m xs) -> Flow m (a ': xs)
+{-# INLINABLE (>..~..>) #-}
 (>..~..>) = liftm (..~..>)
 
 infixl 0 >..~..>
@@ -845,8 +845,8 @@
 (..~^^>) ::
    ( Monad m
    , Liftable xs (a ': zs)
-   ) => Variant (a ': l) -> (Variant l -> Flow m xs) -> Flow m (a ': zs)
-{-# INLINE (..~^^>) #-}
+   ) => V (a ': l) -> (V l -> Flow m xs) -> Flow m (a ': zs)
+{-# INLINABLE (..~^^>) #-}
 (..~^^>) v f = case popVariantHead v of
    Right u -> flowSetN @0 u
    Left  l -> liftVariant <$> f l
@@ -857,8 +857,8 @@
 (>..~^^>) ::
    ( Monad m
    , Liftable xs (a ': zs)
-   ) => Flow m  (a ': l) -> (Variant l -> Flow m xs) -> Flow m (a ': zs)
-{-# INLINE (>..~^^>) #-}
+   ) => Flow m  (a ': l) -> (V l -> Flow m xs) -> Flow m (a ': zs)
+{-# INLINABLE (>..~^^>) #-}
 (>..~^^>) = liftm (..~^^>)
 
 infixl 0 >..~^^>
@@ -867,8 +867,8 @@
 (..~^>) ::
    ( Monad m
    , Member a zs
-   ) => Variant (a ': l) -> (Variant l -> Flow m zs) -> Flow m zs
-{-# INLINE (..~^>) #-}
+   ) => V (a ': l) -> (V l -> Flow m zs) -> Flow m zs
+{-# INLINABLE (..~^>) #-}
 (..~^>) v f = case popVariantHead v of
    Right u -> flowSet u
    Left  l -> f l
@@ -879,8 +879,8 @@
 (>..~^>) ::
    ( Monad m
    , Member a zs
-   ) => Flow m (a ': l) -> (Variant l -> Flow m zs) -> Flow m zs
-{-# INLINE (>..~^>) #-}
+   ) => Flow m (a ': l) -> (V l -> Flow m zs) -> Flow m zs
+{-# INLINABLE (>..~^>) #-}
 (>..~^>) = liftm (..~^>)
 
 infixl 0 >..~^>
@@ -888,10 +888,10 @@
 -- | Match in the tail, connect to the expected result
 (..?~^>) ::
    ( Monad m
-   , MaybePopable a xs
+   , a :<? xs
    , Liftable (Filter a xs) ys
-   ) => Variant (x ': xs) -> (a -> Flow m ys) -> Flow m (x ': ys)
-{-# INLINE (..?~^>) #-}
+   ) => V (x ': xs) -> (a -> Flow m ys) -> Flow m (x ': ys)
+{-# INLINABLE (..?~^>) #-}
 (..?~^>) v f = v ..~..> (\v' -> v' ?~^> f)
 
 infixl 0 ..?~^>
@@ -899,10 +899,10 @@
 -- | Match in the tail, connect to the expected result
 (>..?~^>) ::
    ( Monad m
-   , MaybePopable a xs
+   , a :<? xs
    , Liftable (Filter a xs) ys
    ) => Flow m (x ': xs) -> (a -> Flow m ys) -> Flow m (x ': ys)
-{-# INLINE (>..?~^>) #-}
+{-# INLINABLE (>..?~^>) #-}
 (>..?~^>) = liftm (..?~^>)
 
 infixl 0 >..?~^>
@@ -910,10 +910,10 @@
 -- | Match in the tail, connect to the expected result
 (..%~^>) ::
    ( Monad m
-   , Popable a xs
+   , a :< xs
    , Liftable (Filter a xs) ys
-   ) => Variant (x ': xs) -> (a -> Flow m ys) -> Flow m (x ': ys)
-{-# INLINE (..%~^>) #-}
+   ) => V (x ': xs) -> (a -> Flow m ys) -> Flow m (x ': ys)
+{-# INLINABLE (..%~^>) #-}
 (..%~^>) v f = v ..~..> (\v' -> v' %~^> f)
 
 infixl 0 ..%~^>
@@ -921,10 +921,10 @@
 -- | Match in the tail, connect to the expected result
 (>..%~^>) ::
    ( Monad m
-   , Popable a xs
+   , a :< xs
    , Liftable (Filter a xs) ys
    ) => Flow m (x ': xs) -> (a -> Flow m ys) -> Flow m (x ': ys)
-{-# INLINE (>..%~^>) #-}
+{-# INLINABLE (>..%~^>) #-}
 (>..%~^>) = liftm (..%~^>)
 
 infixl 0 >..%~^>
@@ -932,11 +932,11 @@
 -- | Match in the tail, lift to the expected result
 (..?~^^>) ::
    ( Monad m
-   , MaybePopable a xs
+   , a :<? xs
    , Liftable (Filter a xs) zs
    , Liftable ys zs
-   ) => Variant (x ': xs) -> (a -> Flow m ys) -> Flow m (x ': zs)
-{-# INLINE (..?~^^>) #-}
+   ) => V (x ': xs) -> (a -> Flow m ys) -> Flow m (x ': zs)
+{-# INLINABLE (..?~^^>) #-}
 (..?~^^>) v f = v ..~..> (\v' -> v' ?~^^> f)
 
 infixl 0 ..?~^^>
@@ -944,11 +944,11 @@
 -- | Match in the tail, lift to the expected result
 (>..?~^^>) ::
    ( Monad m
-   , MaybePopable a xs
+   , a :<? xs
    , Liftable (Filter a xs) zs
    , Liftable ys zs
    ) => Flow m (x ': xs) -> (a -> Flow m ys) -> Flow m (x ': zs)
-{-# INLINE (>..?~^^>) #-}
+{-# INLINABLE (>..?~^^>) #-}
 (>..?~^^>) = liftm (..?~^^>)
 
 infixl 0 >..?~^^>
@@ -956,11 +956,11 @@
 -- | Match in the tail, lift to the expected result
 (..%~^^>) ::
    ( Monad m
-   , Popable a xs
+   , a :< xs
    , Liftable (Filter a xs) zs
    , Liftable ys zs
-   ) => Variant (x ': xs) -> (a -> Flow m ys) -> Flow m (x ': zs)
-{-# INLINE (..%~^^>) #-}
+   ) => V (x ': xs) -> (a -> Flow m ys) -> Flow m (x ': zs)
+{-# INLINABLE (..%~^^>) #-}
 (..%~^^>) v f = v ..~..> (\v' -> v' %~^^> f)
 
 infixl 0 ..%~^^>
@@ -968,11 +968,11 @@
 -- | Match in the tail, lift to the expected result
 (>..%~^^>) ::
    ( Monad m
-   , Popable a xs
+   , a :< xs
    , Liftable (Filter a xs) zs
    , Liftable ys zs
    ) => Flow m (x ': xs) -> (a -> Flow m ys) -> Flow m (x ': zs)
-{-# INLINE (>..%~^^>) #-}
+{-# INLINABLE (>..%~^^>) #-}
 (>..%~^^>) = liftm (..%~^^>)
 
 infixl 0 >..%~^^>
@@ -980,10 +980,10 @@
 -- | Match in the tail, keep the same types
 (..?~$>) ::
    ( Monad m
-   , MaybePopable a xs
+   , a :<? xs
    , Liftable (Filter a xs) (x ': xs)
-   ) => Variant (x ': xs) -> (a -> Flow m (x ': xs)) -> Flow m (x ': xs)
-{-# INLINE (..?~$>) #-}
+   ) => V (x ': xs) -> (a -> Flow m (x ': xs)) -> Flow m (x ': xs)
+{-# INLINABLE (..?~$>) #-}
 (..?~$>) v f = case popVariantHead v of
    Right _ -> return v
    Left xs -> xs ?~^> f
@@ -993,10 +993,10 @@
 -- | Match in the tail, keep the same types
 (>..?~$>) ::
    ( Monad m
-   , MaybePopable a xs
+   , a :<? xs
    , Liftable (Filter a xs) (x ': xs)
    ) => Flow m (x ': xs) -> (a -> Flow m (x ': xs)) -> Flow m (x ': xs)
-{-# INLINE (>..?~$>) #-}
+{-# INLINABLE (>..?~$>) #-}
 (>..?~$>) = liftm (..?~$>)
 
 infixl 0 >..?~$>
@@ -1004,10 +1004,10 @@
 -- | Match in the tail, keep the same types
 (..%~$>) ::
    ( Monad m
-   , Popable a xs
+   , a :< xs
    , Liftable (Filter a xs) (x ': xs)
-   ) => Variant (x ': xs) -> (a -> Flow m (x ': xs)) -> Flow m (x ': xs)
-{-# INLINE (..%~$>) #-}
+   ) => V (x ': xs) -> (a -> Flow m (x ': xs)) -> Flow m (x ': xs)
+{-# INLINABLE (..%~$>) #-}
 (..%~$>) v f = case popVariantHead v of
    Right _ -> return v
    Left xs -> xs %~^> f
@@ -1017,10 +1017,10 @@
 -- | Match in the tail, keep the same types
 (>..%~$>) ::
    ( Monad m
-   , Popable a xs
+   , a :< xs
    , Liftable (Filter a xs) (x ': xs)
    ) => Flow m (x ': xs) -> (a -> Flow m (x ': xs)) -> Flow m (x ': xs)
-{-# INLINE (>..%~$>) #-}
+{-# INLINABLE (>..%~$>) #-}
 (>..%~$>) = liftm (..%~$>)
 
 infixl 0 >..%~$>
@@ -1029,8 +1029,8 @@
 -- | Extract the tail and perform an effect. Passthrough the input value
 (..~=>) ::
    ( Monad m
-   ) => Variant (x ': xs) -> (Variant xs -> m ()) -> Flow m (x ': xs)
-{-# INLINE (..~=>) #-}
+   ) => V (x ': xs) -> (V xs -> m ()) -> Flow m (x ': xs)
+{-# INLINABLE (..~=>) #-}
 (..~=>) v f = case popVariantHead v of
    Right _ -> return v
    Left  l -> f l >> return v
@@ -1040,8 +1040,8 @@
 -- | Extract the tail and perform an effect. Passthrough the input value
 (>..~=>) ::
    ( Monad m
-   ) => Flow m (x ': xs) -> (Variant xs -> m ()) -> Flow m (x ': xs)
-{-# INLINE (>..~=>) #-}
+   ) => Flow m (x ': xs) -> (V xs -> m ()) -> Flow m (x ': xs)
+{-# INLINABLE (>..~=>) #-}
 (>..~=>) = liftm (..~=>)
 
 infixl 0 >..~=>
@@ -1049,8 +1049,8 @@
 -- | Extract the tail and perform an effect
 (..~!>) ::
    ( Monad m
-   ) => Variant (x ': xs) -> (Variant xs -> m ()) -> m ()
-{-# INLINE (..~!>) #-}
+   ) => V (x ': xs) -> (V xs -> m ()) -> m ()
+{-# INLINABLE (..~!>) #-}
 (..~!>) v f = case popVariantHead v of
    Right _ -> return ()
    Left  l -> f l
@@ -1060,8 +1060,8 @@
 -- | Extract the tail and perform an effect
 (>..~!>) ::
    ( Monad m
-   ) => Flow m (x ': xs) -> (Variant xs -> m ()) -> m ()
-{-# INLINE (>..~!>) #-}
+   ) => Flow m (x ': xs) -> (V xs -> m ()) -> m ()
+{-# INLINABLE (>..~!>) #-}
 (>..~!>) = liftm (..~!>)
 
 infixl 0 >..~!>
@@ -1069,8 +1069,8 @@
 -- | Extract the tail and perform an effect
 (..~!!>) ::
    ( Monad m
-   ) => Variant (x ': xs) -> (Variant xs -> m ()) -> m x
-{-# INLINE (..~!!>) #-}
+   ) => V (x ': xs) -> (V xs -> m ()) -> m x
+{-# INLINABLE (..~!!>) #-}
 (..~!!>) v f = case popVariantHead v of
    Right x -> return x
    Left xs -> f xs >> error "..~!!> error"
@@ -1080,8 +1080,8 @@
 -- | Extract the tail and perform an effect
 (>..~!!>) ::
    ( Monad m
-   ) => Flow m (x ': xs) -> (Variant xs -> m ()) -> m x
-{-# INLINE (>..~!!>) #-}
+   ) => Flow m (x ': xs) -> (V xs -> m ()) -> m x
+{-# INLINABLE (>..~!!>) #-}
 (>..~!!>) = liftm (..~!!>)
 
 infixl 0 >..~!!>
@@ -1089,9 +1089,9 @@
 -- | Match in the tail and perform an effect
 (..?~!!>) ::
    ( Monad m
-   , MaybePopable y xs
-   ) => Variant (x ': xs) -> (y -> m ()) -> Flow m (x ': Filter y xs)
-{-# INLINE (..?~!!>) #-}
+   , y :<? xs
+   ) => V (x ': xs) -> (y -> m ()) -> Flow m (x ': Filter y xs)
+{-# INLINABLE (..?~!!>) #-}
 (..?~!!>) v f = v ..~..> (\xs -> xs ?~!!> f)
 
 infixl 0 ..?~!!>
@@ -1099,9 +1099,9 @@
 -- | Match in the tail and perform an effect
 (>..?~!!>) ::
    ( Monad m
-   , MaybePopable y xs
+   , y :<? xs
    ) => Flow m (x ': xs) -> (y -> m ()) -> Flow m (x ': Filter y xs)
-{-# INLINE (>..?~!!>) #-}
+{-# INLINABLE (>..?~!!>) #-}
 (>..?~!!>) = liftm (..?~!!>)
 
 infixl 0 >..?~!!>
@@ -1109,9 +1109,9 @@
 -- | Match in the tail and perform an effect
 (..%~!!>) ::
    ( Monad m
-   , Popable y xs
-   ) => Variant (x ': xs) -> (y -> m ()) -> Flow m (x ': Filter y xs)
-{-# INLINE (..%~!!>) #-}
+   , y :< xs
+   ) => V (x ': xs) -> (y -> m ()) -> Flow m (x ': Filter y xs)
+{-# INLINABLE (..%~!!>) #-}
 (..%~!!>) v f = v ..~..> (\xs -> xs %~!!> f)
 
 infixl 0 ..%~!!>
@@ -1119,9 +1119,9 @@
 -- | Match in the tail and perform an effect
 (>..%~!!>) ::
    ( Monad m
-   , Popable y xs
+   , y :< xs
    ) => Flow m (x ': xs) -> (y -> m ()) -> Flow m (x ': Filter y xs)
-{-# INLINE (>..%~!!>) #-}
+{-# INLINABLE (>..%~!!>) #-}
 (>..%~!!>) = liftm (..%~!!>)
 
 infixl 0 >..%~!!>
@@ -1129,9 +1129,9 @@
 -- | Match in the tail and perform an effect
 (..?~!>) ::
    ( Monad m
-   , MaybePopable y xs
-   ) => Variant (x ': xs) -> (y -> m ()) -> m ()
-{-# INLINE (..?~!>) #-}
+   , y :<? xs
+   ) => V (x ': xs) -> (y -> m ()) -> m ()
+{-# INLINABLE (..?~!>) #-}
 (..?~!>) v f = case popVariantHead v of
    Right _ -> return ()
    Left xs -> xs ?~!> f
@@ -1141,9 +1141,9 @@
 -- | Match in the tail and perform an effect
 (>..?~!>) ::
    ( Monad m
-   , MaybePopable y xs
+   , y :<? xs
    ) => Flow m (x ': xs) -> (y -> m ()) -> m ()
-{-# INLINE (>..?~!>) #-}
+{-# INLINABLE (>..?~!>) #-}
 (>..?~!>) = liftm (..?~!>)
 
 infixl 0 >..?~!>
@@ -1151,9 +1151,9 @@
 -- | Match in the tail and perform an effect
 (..%~!>) ::
    ( Monad m
-   , Popable y xs
-   ) => Variant (x ': xs) -> (y -> m ()) -> m ()
-{-# INLINE (..%~!>) #-}
+   , y :< xs
+   ) => V (x ': xs) -> (y -> m ()) -> m ()
+{-# INLINABLE (..%~!>) #-}
 (..%~!>) v f = case popVariantHead v of
    Right _ -> return ()
    Left xs -> xs %~!> f
@@ -1163,9 +1163,9 @@
 -- | Match in the tail and perform an effect
 (>..%~!>) ::
    ( Monad m
-   , Popable y xs
+   , y :< xs
    ) => Flow m (x ': xs) -> (y -> m ()) -> m ()
-{-# INLINE (>..%~!>) #-}
+{-# INLINABLE (>..%~!>) #-}
 (>..%~!>) = liftm (..%~!>)
 
 infixl 0 >..%~!>
@@ -1178,9 +1178,9 @@
 (?~.>) :: forall x xs y ys m.
    ( ys ~ Filter x xs
    , Monad m
-   , MaybePopable x xs
-   ) => Variant xs -> (x -> m y) -> Flow m (y ': ys)
-{-# INLINE (?~.>) #-}
+   , x :<? xs
+   ) => V xs -> (x -> m y) -> Flow m (y ': ys)
+{-# INLINABLE (?~.>) #-}
 (?~.>) v f = case popVariantMaybe v of
    Right x -> flowSetN @0 =<< f x
    Left ys -> prependVariant @'[y] <$> return ys
@@ -1191,9 +1191,9 @@
 (>?~.>) ::
    ( ys ~ Filter x xs
    , Monad m
-   , MaybePopable x xs
+   , x :<? xs
    ) => Flow m xs -> (x -> m y) -> Flow m (y ': ys)
-{-# INLINE (>?~.>) #-}
+{-# INLINABLE (>?~.>) #-}
 (>?~.>) = liftm (?~.>)
 
 infixl 0 >?~.>
@@ -1202,9 +1202,9 @@
 (%~.>) :: forall x xs y ys m.
    ( ys ~ Filter x xs
    , Monad m
-   , Popable x xs
-   ) => Variant xs -> (x -> m y) -> Flow m (y ': ys)
-{-# INLINE (%~.>) #-}
+   , x :< xs
+   ) => V xs -> (x -> m y) -> Flow m (y ': ys)
+{-# INLINABLE (%~.>) #-}
 (%~.>) = (?~.>)
 
 infixl 0 %~.>
@@ -1213,9 +1213,9 @@
 (>%~.>) ::
    ( ys ~ Filter x xs
    , Monad m
-   , Popable x xs
+   , x :< xs
    ) => Flow m xs -> (x -> m y) -> Flow m (y ': ys)
-{-# INLINE (>%~.>) #-}
+{-# INLINABLE (>%~.>) #-}
 (>%~.>) = liftm (%~.>)
 
 infixl 0 >%~.>
@@ -1223,10 +1223,10 @@
 -- | Pop element, concat the result
 (?~+>) :: forall x xs ys m.
    ( Monad m
-   , MaybePopable x xs
+   , x :<? xs
    , KnownNat (Length ys)
-   ) => Variant xs -> (x -> Flow m ys) -> Flow m (Concat ys (Filter x xs))
-{-# INLINE (?~+>) #-}
+   ) => V xs -> (x -> Flow m ys) -> Flow m (Concat ys (Filter x xs))
+{-# INLINABLE (?~+>) #-}
 (?~+>) v f = case popVariantMaybe v of
    Right x -> appendVariant  @(Filter x xs) <$> f x
    Left ys -> prependVariant @ys            <$> return ys
@@ -1236,10 +1236,10 @@
 -- | Pop element, concat the result
 (>?~+>) :: forall x xs ys m.
    ( Monad m
-   , MaybePopable x xs
+   , x :< xs
    , KnownNat (Length ys)
    ) => Flow m xs -> (x -> Flow m ys) -> Flow m (Concat ys (Filter x xs))
-{-# INLINE (>?~+>) #-}
+{-# INLINABLE (>?~+>) #-}
 (>?~+>) = liftm (?~+>)
 
 infixl 0 >?~+>
@@ -1247,10 +1247,10 @@
 -- | Pop element, concat the result
 (%~+>) :: forall x xs ys m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    , KnownNat (Length ys)
-   ) => Variant xs -> (x -> Flow m ys) -> Flow m (Concat ys (Filter x xs))
-{-# INLINE (%~+>) #-}
+   ) => V xs -> (x -> Flow m ys) -> Flow m (Concat ys (Filter x xs))
+{-# INLINABLE (%~+>) #-}
 (%~+>) = (?~+>)
 
 infixl 0 %~+>
@@ -1258,10 +1258,10 @@
 -- | Pop element, concat the result
 (>%~+>) :: forall x xs ys m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    , KnownNat (Length ys)
    ) => Flow m xs -> (x -> Flow m ys) -> Flow m (Concat ys (Filter x xs))
-{-# INLINE (>%~+>) #-}
+{-# INLINABLE (>%~+>) #-}
 (>%~+>) = liftm (%~+>)
 
 infixl 0 >%~+>
@@ -1269,11 +1269,11 @@
 -- | Pop element, lift the result
 (?~^^>) :: forall x xs ys zs m.
    ( Monad m
-   , MaybePopable x xs
+   , x :<? xs
    , Liftable (Filter x xs) zs
    , Liftable ys zs
-   ) => Variant xs -> (x -> Flow m ys) -> Flow m zs
-{-# INLINE (?~^^>) #-}
+   ) => V xs -> (x -> Flow m ys) -> Flow m zs
+{-# INLINABLE (?~^^>) #-}
 (?~^^>) v f = case popVariantMaybe v of
    Right x -> liftVariant <$> f x
    Left ys -> liftVariant <$> return ys
@@ -1283,11 +1283,11 @@
 -- | Pop element, lift the result
 (>?~^^>) :: forall x xs ys zs m.
    ( Monad m
-   , MaybePopable x xs
+   , x :<? xs
    , Liftable (Filter x xs) zs
    , Liftable ys zs
    ) => Flow m xs -> (x -> Flow m ys) -> Flow m zs
-{-# INLINE (>?~^^>) #-}
+{-# INLINABLE (>?~^^>) #-}
 (>?~^^>) = liftm (?~^^>)
 
 infixl 0 >?~^^>
@@ -1295,11 +1295,11 @@
 -- | Pop element, lift the result
 (%~^^>) :: forall x xs ys zs m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    , Liftable (Filter x xs) zs
    , Liftable ys zs
-   ) => Variant xs -> (x -> Flow m ys) -> Flow m zs
-{-# INLINE (%~^^>) #-}
+   ) => V xs -> (x -> Flow m ys) -> Flow m zs
+{-# INLINABLE (%~^^>) #-}
 (%~^^>) = (?~^^>)
 
 infixl 0 %~^^>
@@ -1307,11 +1307,11 @@
 -- | Pop element, lift the result
 (>%~^^>) :: forall x xs ys zs m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    , Liftable (Filter x xs) zs
    , Liftable ys zs
    ) => Flow m xs -> (x -> Flow m ys) -> Flow m zs
-{-# INLINE (>%~^^>) #-}
+{-# INLINABLE (>%~^^>) #-}
 (>%~^^>) = liftm (%~^^>)
 
 infixl 0 >%~^^>
@@ -1319,10 +1319,10 @@
 -- | Pop element, connect to the expected output
 (?~^>) :: forall x xs zs m.
    ( Monad m
-   , MaybePopable x xs
+   , x :<? xs
    , Liftable (Filter x xs) zs
-   ) => Variant xs -> (x -> Flow m zs) -> Flow m zs
-{-# INLINE (?~^>) #-}
+   ) => V xs -> (x -> Flow m zs) -> Flow m zs
+{-# INLINABLE (?~^>) #-}
 (?~^>) v f = case popVariantMaybe v of
    Right x -> f x
    Left ys -> return (liftVariant ys)
@@ -1332,10 +1332,10 @@
 -- | Pop element, connect to the expected output
 (>?~^>) :: forall x xs zs m.
    ( Monad m
-   , MaybePopable x xs
+   , x :<? xs
    , Liftable (Filter x xs) zs
    ) => Flow m xs -> (x -> Flow m zs) -> Flow m zs
-{-# INLINE (>?~^>) #-}
+{-# INLINABLE (>?~^>) #-}
 (>?~^>) = liftm (?~^>)
 
 infixl 0 >?~^>
@@ -1343,10 +1343,10 @@
 -- | Pop element, connect to the expected output
 (%~^>) :: forall x xs zs m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    , Liftable (Filter x xs) zs
-   ) => Variant xs -> (x -> Flow m zs) -> Flow m zs
-{-# INLINE (%~^>) #-}
+   ) => V xs -> (x -> Flow m zs) -> Flow m zs
+{-# INLINABLE (%~^>) #-}
 (%~^>) = (?~^>)
 
 infixl 0 %~^>
@@ -1354,10 +1354,10 @@
 -- | Pop element, connect to the expected output
 (>%~^>) :: forall x xs zs m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    , Liftable (Filter x xs) zs
    ) => Flow m xs -> (x -> Flow m zs) -> Flow m zs
-{-# INLINE (>%~^>) #-}
+{-# INLINABLE (>%~^>) #-}
 (>%~^>) = liftm (%~^>)
 
 infixl 0 >%~^>
@@ -1365,9 +1365,9 @@
 -- | Pop element, use the same output type
 (?~$>) :: forall x xs m.
    ( Monad m
-   , MaybePopable x xs
-   ) => Variant xs -> (x -> Flow m xs) -> Flow m xs
-{-# INLINE (?~$>) #-}
+   , x :<? xs
+   ) => V xs -> (x -> Flow m xs) -> Flow m xs
+{-# INLINABLE (?~$>) #-}
 (?~$>) v f = case popVariantMaybe v of
    Right x -> f x
    Left _  -> return v
@@ -1377,9 +1377,9 @@
 -- | Pop element, use the same output type
 (>?~$>) :: forall x xs m.
    ( Monad m
-   , MaybePopable x xs
+   , x :<? xs
    ) => Flow m xs -> (x -> Flow m xs) -> Flow m xs
-{-# INLINE (>?~$>) #-}
+{-# INLINABLE (>?~$>) #-}
 (>?~$>) = liftm (?~$>)
 
 infixl 0 >?~$>
@@ -1387,9 +1387,9 @@
 -- | Pop element, use the same output type
 (%~$>) :: forall x xs m.
    ( Monad m
-   , Popable x xs
-   ) => Variant xs -> (x -> Flow m xs) -> Flow m xs
-{-# INLINE (%~$>) #-}
+   , x :< xs
+   ) => V xs -> (x -> Flow m xs) -> Flow m xs
+{-# INLINABLE (%~$>) #-}
 (%~$>) = (?~$>)
 
 infixl 0 %~$>
@@ -1397,9 +1397,9 @@
 -- | Pop element, use the same output type
 (>%~$>) :: forall x xs m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    ) => Flow m xs -> (x -> Flow m xs) -> Flow m xs
-{-# INLINE (>%~$>) #-}
+{-# INLINABLE (>%~$>) #-}
 (>%~$>) = liftm (%~$>)
 
 infixl 0 >%~$>
@@ -1407,12 +1407,12 @@
 -- | Pop element, fusion the result
 (?~|>) :: forall x xs ys zs m.
    ( Monad m
-   , MaybePopable x xs
+   , x :<? xs
    , Liftable (Filter x xs) zs
    , Liftable ys zs
    , zs ~ Union (Filter x xs) ys
-   ) => Variant xs -> (x -> Flow m ys) -> Flow m zs
-{-# INLINE (?~|>) #-}
+   ) => V xs -> (x -> Flow m ys) -> Flow m zs
+{-# INLINABLE (?~|>) #-}
 (?~|>) v f = case popVariantMaybe v of
    Right x -> liftVariant <$> f x
    Left ys -> return (liftVariant ys)
@@ -1422,12 +1422,12 @@
 -- | Pop element, fusion the result
 (>?~|>) :: forall x xs ys zs m.
    ( Monad m
-   , MaybePopable x xs
+   , x :<? xs
    , Liftable (Filter x xs) zs
    , Liftable ys zs
    , zs ~ Union (Filter x xs) ys
    ) => Flow m xs -> (x -> Flow m ys) -> Flow m zs
-{-# INLINE (>?~|>) #-}
+{-# INLINABLE (>?~|>) #-}
 (>?~|>) = liftm (?~|>)
 
 infixl 0 >?~|>
@@ -1435,12 +1435,12 @@
 -- | Pop element, fusion the result
 (%~|>) :: forall x xs ys zs m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    , Liftable (Filter x xs) zs
    , Liftable ys zs
    , zs ~ Union (Filter x xs) ys
-   ) => Variant xs -> (x -> Flow m ys) -> Flow m zs
-{-# INLINE (%~|>) #-}
+   ) => V xs -> (x -> Flow m ys) -> Flow m zs
+{-# INLINABLE (%~|>) #-}
 (%~|>) = (?~|>)
 
 infixl 0 %~|>
@@ -1448,12 +1448,12 @@
 -- | Pop element, fusion the result
 (>%~|>) :: forall x xs ys zs m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    , Liftable (Filter x xs) zs
    , Liftable ys zs
    , zs ~ Union (Filter x xs) ys
    ) => Flow m xs -> (x -> Flow m ys) -> Flow m zs
-{-# INLINE (>%~|>) #-}
+{-# INLINABLE (>%~|>) #-}
 (>%~|>) = liftm (%~|>)
 
 infixl 0 >%~|>
@@ -1461,9 +1461,9 @@
 -- | Pop element and perform effect. Passthrough the input value.
 (?~=>) :: forall x xs m.
    ( Monad m
-   , MaybePopable x xs
-   ) => Variant xs -> (x -> m ()) -> Flow m xs
-{-# INLINE (?~=>) #-}
+   , x :<? xs
+   ) => V xs -> (x -> m ()) -> Flow m xs
+{-# INLINABLE (?~=>) #-}
 (?~=>) v f = case popVariantMaybe v of
    Right x -> f x >> return v
    Left _  -> return v
@@ -1473,9 +1473,9 @@
 -- | Pop element and perform effect. Passthrough the input value.
 (>?~=>) :: forall x xs m.
    ( Monad m
-   , MaybePopable x xs
+   , x :<? xs
    ) => Flow m xs -> (x -> m ()) -> Flow m xs
-{-# INLINE (>?~=>) #-}
+{-# INLINABLE (>?~=>) #-}
 (>?~=>) = liftm (?~=>)
 
 infixl 0 >?~=>
@@ -1483,9 +1483,9 @@
 -- | Pop element and perform effect. Passthrough the input value.
 (%~=>) :: forall x xs m.
    ( Monad m
-   , Popable x xs
-   ) => Variant xs -> (x -> m ()) -> Flow m xs
-{-# INLINE (%~=>) #-}
+   , x :< xs
+   ) => V xs -> (x -> m ()) -> Flow m xs
+{-# INLINABLE (%~=>) #-}
 (%~=>) = (?~=>)
 
 infixl 0 %~=>
@@ -1493,9 +1493,9 @@
 -- | Pop element and perform effect. Passthrough the input value.
 (>%~=>) :: forall x xs m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    ) => Flow m xs -> (x -> m ()) -> Flow m xs
-{-# INLINE (>%~=>) #-}
+{-# INLINABLE (>%~=>) #-}
 (>%~=>) = liftm (%~=>)
 
 infixl 0 >%~=>
@@ -1503,9 +1503,9 @@
 -- | Pop element and perform effect.
 (?~!>) :: forall x xs m.
    ( Monad m
-   , MaybePopable x xs
-   ) => Variant xs -> (x -> m ()) -> m ()
-{-# INLINE (?~!>) #-}
+   , x :<? xs
+   ) => V xs -> (x -> m ()) -> m ()
+{-# INLINABLE (?~!>) #-}
 (?~!>) v f = case popVariantMaybe v of
    Right x -> f x
    Left _  -> return ()
@@ -1515,9 +1515,9 @@
 -- | Pop element and perform effect.
 (>?~!>) :: forall x xs m.
    ( Monad m
-   , MaybePopable x xs
+   , x :<? xs
    ) => Flow m xs -> (x -> m ()) -> m ()
-{-# INLINE (>?~!>) #-}
+{-# INLINABLE (>?~!>) #-}
 (>?~!>) = liftm (?~!>)
 
 infixl 0 >?~!>
@@ -1525,9 +1525,9 @@
 -- | Pop element and perform effect.
 (%~!>) :: forall x xs m.
    ( Monad m
-   , Popable x xs
-   ) => Variant xs -> (x -> m ()) -> m ()
-{-# INLINE (%~!>) #-}
+   , x :< xs
+   ) => V xs -> (x -> m ()) -> m ()
+{-# INLINABLE (%~!>) #-}
 (%~!>) = (?~!>)
 
 infixl 0 %~!>
@@ -1535,9 +1535,9 @@
 -- | Pop element and perform effect.
 (>%~!>) :: forall x xs m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    ) => Flow m xs -> (x -> m ()) -> m ()
-{-# INLINE (>%~!>) #-}
+{-# INLINABLE (>%~!>) #-}
 (>%~!>) = liftm (%~!>)
 
 infixl 0 >%~!>
@@ -1545,9 +1545,9 @@
 -- | Pop element and perform effect.
 (?~!!>) :: forall x xs m.
    ( Monad m
-   , MaybePopable x xs
-   ) => Variant xs -> (x -> m ()) -> Flow m (Filter x xs)
-{-# INLINE (?~!!>) #-}
+   , x :<? xs
+   ) => V xs -> (x -> m ()) -> Flow m (Filter x xs)
+{-# INLINABLE (?~!!>) #-}
 (?~!!>) v f = case popVariantMaybe v of
    Right x -> f x >> error "?~!!> error"
    Left u  -> return u
@@ -1557,9 +1557,9 @@
 -- | Pop element and perform effect.
 (>?~!!>) :: forall x xs m.
    ( Monad m
-   , MaybePopable x xs
+   , x :<? xs
    ) => Flow m xs -> (x -> m ()) -> Flow m (Filter x xs)
-{-# INLINE (>?~!!>) #-}
+{-# INLINABLE (>?~!!>) #-}
 (>?~!!>) = liftm (?~!!>)
 
 infixl 0 >?~!!>
@@ -1567,9 +1567,9 @@
 -- | Pop element and perform effect.
 (%~!!>) :: forall x xs m.
    ( Monad m
-   , Popable x xs
-   ) => Variant xs -> (x -> m ()) -> Flow m (Filter x xs)
-{-# INLINE (%~!!>) #-}
+   , x :< xs
+   ) => V xs -> (x -> m ()) -> Flow m (Filter x xs)
+{-# INLINABLE (%~!!>) #-}
 (%~!!>) = (?~!!>)
 
 infixl 0 %~!!>
@@ -1577,9 +1577,9 @@
 -- | Pop element and perform effect.
 (>%~!!>) :: forall x xs m.
    ( Monad m
-   , Popable x xs
+   , x :< xs
    ) => Flow m xs -> (x -> m ()) -> Flow m (Filter x xs)
-{-# INLINE (>%~!!>) #-}
+{-# INLINABLE (>%~!!>) #-}
 (>%~!!>) = liftm (%~!!>)
 
 infixl 0 >%~!!>
@@ -1591,31 +1591,31 @@
 
 -- | Make a flow operator
 makeFlowOp :: Monad m =>
-      (Variant as -> Either (Variant bs) (Variant cs))
-      -> (Variant cs -> Flow m ds)
-      -> (Either (Variant bs) (Variant ds) -> es)
-      -> Variant as -> m es
-{-# INLINE makeFlowOp #-}
+      (V as -> Either (V bs) (V cs))
+      -> (V cs -> Flow m ds)
+      -> (Either (V bs) (V ds) -> es)
+      -> V as -> m es
+{-# INLINABLE makeFlowOp #-}
 makeFlowOp select apply combine v = combine <$> traverse apply (select v)
 
 -- | Make a flow operator
 makeFlowOpM :: Monad m =>
-      (Variant as -> Either (Variant bs) (Variant cs))
-      -> (Variant cs -> Flow m ds)
-      -> (Either (Variant bs) (Variant ds) -> es)
+      (V as -> Either (V bs) (V cs))
+      -> (V cs -> Flow m ds)
+      -> (Either (V bs) (V ds) -> es)
       -> Flow m as -> m es
-{-# INLINE makeFlowOpM #-}
+{-# INLINABLE makeFlowOpM #-}
 makeFlowOpM select apply combine v = v >>= makeFlowOp select apply combine
 
 
 -- | Select the first value
-selectFirst :: Variant (x ': xs) -> Either (Variant xs) (Variant '[x])
-{-# INLINE selectFirst #-}
+selectFirst :: V (x ': xs) -> Either (V xs) (V '[x])
+{-# INLINABLE selectFirst #-}
 selectFirst = fmap (toVariantAt @0) . popVariantHead
 
 -- | Select the tail
-selectTail :: Variant (x ': xs) -> Either (Variant '[x]) (Variant xs)
-{-# INLINE selectTail #-}
+selectTail :: V (x ': xs) -> Either (V '[x]) (V xs)
+{-# INLINABLE selectTail #-}
 selectTail = flipEither . selectFirst
    where
       flipEither (Left x)  = Right x
@@ -1623,54 +1623,54 @@
 
 -- | Select by type
 selectType ::
-   ( Popable x xs
-   ) => Variant xs -> Either (Variant (Filter x xs)) (Variant '[x])
-{-# INLINE selectType #-}
+   ( x :< xs
+   ) => V xs -> Either (V (Filter x xs)) (V '[x])
+{-# INLINABLE selectType #-}
 selectType = fmap (toVariantAt @0) . popVariant
 
 -- | Const application
-applyConst :: Flow m ys -> (Variant xs -> Flow m ys)
-{-# INLINE applyConst #-}
+applyConst :: Flow m ys -> (V xs -> Flow m ys)
+{-# INLINABLE applyConst #-}
 applyConst = const
 
 -- | Pure application
-applyPure :: Monad m => (Variant xs -> Variant ys) -> Variant xs -> Flow m ys
-{-# INLINE applyPure #-}
+applyPure :: Monad m => (V xs -> V ys) -> V xs -> Flow m ys
+{-# INLINABLE applyPure #-}
 applyPure f = return . f
 
 -- | Lift a monadic function
-applyM :: Monad m => (a -> m b) -> Variant '[a] -> Flow m '[b]
-{-# INLINE applyM #-}
+applyM :: Monad m => (a -> m b) -> V '[a] -> Flow m '[b]
+{-# INLINABLE applyM #-}
 applyM = liftF
 
 -- | Lift a monadic function
-applyVM :: Monad m => (Variant a -> m b) -> Variant a -> Flow m '[b]
-{-# INLINE applyVM #-}
+applyVM :: Monad m => (V a -> m b) -> V a -> Flow m '[b]
+{-# INLINABLE applyVM #-}
 applyVM f = fmap (toVariantAt @0) . f
 
 -- | Lift a monadic function
-applyF :: (a -> Flow m b) -> Variant '[a] -> Flow m b
-{-# INLINE applyF #-}
+applyF :: (a -> Flow m b) -> V '[a] -> Flow m b
+{-# INLINABLE applyF #-}
 applyF f = f . variantToValue
 
 -- | Set the first value (the "correct" one)
-combineFirst :: forall x xs. Either (Variant xs) (Variant '[x]) -> Variant (x ': xs)
-{-# INLINE combineFirst #-}
+combineFirst :: forall x xs. Either (V xs) (V '[x]) -> V (x ': xs)
+{-# INLINABLE combineFirst #-}
 combineFirst = \case
    Right x -> appendVariant  @xs x
    Left xs -> prependVariant @'[x] xs
 
 -- | Set the first value, keep the same tail type 
 combineSameTail :: forall x xs.
-   Either (Variant xs) (Variant (x ': xs)) -> Variant (x ': xs)
-{-# INLINE combineSameTail #-}
+   Either (V xs) (V (x ': xs)) -> V (x ': xs)
+{-# INLINABLE combineSameTail #-}
 combineSameTail = \case
    Right x -> x
    Left xs -> prependVariant @'[x] xs
 
 -- | Return the valid variant unmodified
-combineEither :: Either (Variant xs) (Variant xs) -> Variant xs
-{-# INLINE combineEither #-}
+combineEither :: Either (V xs) (V xs) -> V xs
+{-# INLINABLE combineEither #-}
 combineEither = \case
    Right x -> x
    Left x  -> x
@@ -1678,8 +1678,8 @@
 -- | Concatenate unselected values
 combineConcat :: forall xs ys.
    ( KnownNat (Length xs)
-   ) => Either (Variant ys) (Variant xs) -> Variant (Concat xs ys)
-{-# INLINE combineConcat #-}
+   ) => Either (V ys) (V xs) -> V (Concat xs ys)
+{-# INLINABLE combineConcat #-}
 combineConcat = \case
    Right xs -> appendVariant  @ys xs
    Left ys  -> prependVariant @xs ys
@@ -1688,8 +1688,8 @@
 combineUnion ::
    ( Liftable xs (Union xs ys)
    , Liftable ys (Union xs ys)
-   ) => Either (Variant ys) (Variant xs) -> Variant (Union xs ys)
-{-# INLINE combineUnion #-}
+   ) => Either (V ys) (V xs) -> V (Union xs ys)
+{-# INLINABLE combineUnion #-}
 combineUnion = \case
    Right xs -> liftVariant xs
    Left  ys -> liftVariant ys
@@ -1697,8 +1697,8 @@
 -- | Lift unselected
 combineLiftUnselected ::
    ( Liftable ys xs
-   ) => Either (Variant ys) (Variant xs) -> Variant xs
-{-# INLINE combineLiftUnselected #-}
+   ) => Either (V ys) (V xs) -> V xs
+{-# INLINABLE combineLiftUnselected #-}
 combineLiftUnselected = \case
    Right xs -> xs
    Left ys  -> liftVariant ys
@@ -1707,27 +1707,27 @@
 combineLiftBoth ::
    ( Liftable ys zs
    , Liftable xs zs
-   ) => Either (Variant ys) (Variant xs) -> Variant zs
-{-# INLINE combineLiftBoth #-}
+   ) => Either (V ys) (V xs) -> V zs
+{-# INLINABLE combineLiftBoth #-}
 combineLiftBoth = \case
    Right xs -> liftVariant xs
    Left ys  -> liftVariant ys
 
 -- | Single value
-combineSingle :: Either (Variant '[x]) (Variant '[x]) -> x
-{-# INLINE combineSingle #-}
+combineSingle :: Either (V '[x]) (V '[x]) -> x
+{-# INLINABLE combineSingle #-}
 combineSingle = \case
    Right x -> variantToValue x
    Left  x -> variantToValue x
 
 
 -- | Lift a pure function into a Variant to Variant function
-liftV :: (a -> b) -> Variant '[a] -> Variant '[b]
-liftV = updateVariantAt @0
+liftV :: (a -> b) -> V '[a] -> V '[b]
+liftV = mapVariantAt @0
 
 -- | Lift a function into a Flow
-liftF :: Monad m => (a -> m b) -> Variant '[a] -> Flow m '[b]
-liftF = updateVariantFirstM @0
+liftF :: Monad m => (a -> m b) -> V '[a] -> Flow m '[b]
+liftF = mapVariantAtM @0
 
 
 -----------------------------------
@@ -1744,7 +1744,7 @@
    ExtractRHS '[]              = '[]
    ExtractRHS ((_ -> x) ': xs) = x ': ExtractRHS xs
 
-type LiftContTuple x = ListToTuple (ReplaceRHS (TupleToList x) (Variant (ExtractRHS (TupleToList x))))
+type LiftContTuple x = ListToTuple (ReplaceRHS (TupleToList x) (V (ExtractRHS (TupleToList x))))
 
 class LiftCont x where
    -- | Lift a tuple of functions (a -> r1, b -> r2, ...) into a tuple of
@@ -1848,30 +1848,32 @@
 (-||) :: forall fs xs zs.
    ( LiftCont fs
    , zs ~ ExtractRHS (TupleToList fs)
-   , LiftContTuple fs ~ ContListToTuple xs (Variant zs)
+   , LiftContTuple fs ~ ContListToTuple xs (V zs)
    , ContVariant xs
-   ) => Variant xs -> fs -> Variant zs
+   ) => V xs -> fs -> V zs
 (-||) v fs = variantToCont v >::> liftCont fs
 
 -- | Applicative pure multi-map
 (-||>) :: forall m fs xs zs ks.
    ( LiftCont fs
    , zs ~ ExtractRHS (TupleToList fs)
-   , LiftContTuple fs ~ ContListToTuple xs (Variant zs)
+   , LiftContTuple fs ~ ContListToTuple xs (V zs)
    , ContVariant xs
-   , ks ~ ExtractMonad m zs
+   , ks ~ ExtractM m zs
    , Applicative m
-   ) => Variant xs -> fs -> Flow m ks
+   , JoinVariant m zs
+   ) => V xs -> fs -> Flow m ks
 (-||>) v fs = joinVariant (v -|| fs)
 
 -- | Monadic pure multi-map
 (>-||>) :: forall m fs xs zs ks.
    ( LiftCont fs
    , zs ~ ExtractRHS (TupleToList fs)
-   , LiftContTuple fs ~ ContListToTuple xs (Variant zs)
+   , LiftContTuple fs ~ ContListToTuple xs (V zs)
    , ContVariant xs
-   , ks ~ ExtractMonad m zs
+   , ks ~ ExtractM m zs
    , Monad m
+   , JoinVariant m zs
    ) => Flow m xs -> fs -> Flow m ks
 (>-||>) act fs = do
    r <- act
@@ -1901,13 +1903,13 @@
 (~||) :: forall fs xs zs ys rs.
    ( LiftCont fs
    , zs ~ ExtractRHS (TupleToList fs)
-   , LiftContTuple fs ~ ContListToTuple xs (Variant zs)
+   , LiftContTuple fs ~ ContListToTuple xs (V zs)
    , ContVariant xs
    , ys ~ FlattenVariant zs
-   , Flattenable (Variant zs) (Variant ys)
+   , Flattenable (V zs) (V ys)
    , Liftable ys (Nub ys)
    , rs ~ Nub ys
-   ) => Variant xs -> fs -> Variant rs
+   ) => V xs -> fs -> V rs
 (~||) v fs = nubVariant (flattenVariant (v -|| fs))
 
 -- | Applicative variant multi-map
@@ -1953,14 +1955,15 @@
    ( ContVariant xs
    , LiftCont fs
    , zs ~ ExtractRHS (TupleToList fs)
-   , LiftContTuple fs ~ ContListToTuple xs (Variant zs)
-   , ks ~ ExtractMonad m zs
+   , LiftContTuple fs ~ ContListToTuple xs (V zs)
+   , ks ~ ExtractM m zs
    , ys ~ FlattenVariant ks
-   , Flattenable (Variant ks) (Variant ys)
+   , Flattenable (V ks) (V ys)
    , rs ~ Nub ys
    , Liftable ys rs
    , Applicative m
-   ) => Variant xs -> fs -> Flow m rs
+   , JoinVariant m zs
+   ) => V xs -> fs -> Flow m rs
 (~||>) v fs = nubVariant <$> (flattenVariant <$> joinVariant (v -|| fs))
 
 -- | Monadic variant multi-map
@@ -1968,13 +1971,14 @@
    ( ContVariant xs
    , LiftCont fs
    , zs ~ ExtractRHS (TupleToList fs)
-   , LiftContTuple fs ~ ContListToTuple xs (Variant zs)
-   , ks ~ ExtractMonad m zs
+   , LiftContTuple fs ~ ContListToTuple xs (V zs)
+   , ks ~ ExtractM m zs
    , ys ~ FlattenVariant ks
-   , Flattenable (Variant ks) (Variant ys)
+   , Flattenable (V ks) (V ys)
    , rs ~ Nub ys
    , Liftable ys rs
    , Monad m
+   , JoinVariant m zs
    ) => Flow m xs -> fs -> Flow m rs
 (>~||>) act fs = do
    r <- act
diff --git a/src/tests/Main.hs b/src/tests/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/tests/Main.hs
@@ -0,0 +1,8 @@
+import Test.Tasty
+
+import Variant
+
+main :: IO ()
+main = defaultMain $ testGroup "utils-variant"
+   [ testsVariant
+   ]
diff --git a/src/tests/Variant.hs b/src/tests/Variant.hs
new file mode 100644
--- /dev/null
+++ b/src/tests/Variant.hs
@@ -0,0 +1,129 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Variant
+   ( testsVariant
+   )
+where
+
+import Test.Tasty
+import Test.Tasty.QuickCheck as QC
+import Data.Either
+
+import Haskus.Utils.Variant
+
+data A = A deriving (Show,Eq)
+data B = B deriving (Show,Eq)
+data C = C deriving (Show,Eq)
+data D = D deriving (Show,Eq)
+data E = E deriving (Show,Eq)
+data F = F deriving (Show,Eq)
+
+type ABC = V '[A,B,C]
+type DEF = V '[D,E,F]
+
+b :: ABC
+b = toVariantAt @1 B
+
+b2d :: B -> D
+b2d = const D
+
+c2d :: C -> D
+c2d = const D
+
+b2def :: B -> DEF
+b2def = const (toVariant E)
+
+c2def :: C -> DEF
+c2def = const (toVariant E)
+
+
+testsVariant :: TestTree
+testsVariant = testGroup "Variant" $
+   [ testProperty "set/get by index (match)"
+         (fromVariantAt @1 b == Just B)
+   , testProperty "set/get by index (dont' match)"
+         (fromVariantAt @0 b == Nothing)
+   , testProperty "set/get by type (match)"
+         (fromVariant    (toVariant B :: ABC) == Just B)
+   , testProperty "set/get by type (don't match)"
+         (fromVariant @C (toVariant B :: ABC) == Nothing)
+
+   , testProperty "variant equality (match)"
+         (b == b)
+   , testProperty "variant equality (don't match)"
+         (b /= toVariant C)
+
+   , testProperty "update by index (match)"
+         (mapVariantAt @1 (const D) b == toVariantAt @1 D)
+   , testProperty "update by index (don't match)"
+         (mapVariantAt @0 (const F) b == toVariantAt @1 B)
+   , testProperty "update by type (match)"
+         (mapVariantFirst b2d b == toVariantAt @1 D)
+   , testProperty "update by type (don't match)"
+         (mapVariantFirst c2d b == toVariant B)
+   , testProperty "update/fold by index (match)"
+         (foldMapVariantAt @1 b2def b == toVariant E)
+   , testProperty "update/fold by index (don't match)"
+         (foldMapVariantAt @2 c2def b == toVariant B)
+
+   , testProperty "Convert into tuple"
+         (variantToTuple b == (Nothing, Just B, Nothing))
+   , testProperty "Convert single variant"
+         (variantToValue (toVariant A :: V '[A]) == A)
+
+   , testProperty "Lift Either: Left"
+         (variantFromEither (Left A :: Either A B) == toVariant A)
+   , testProperty "Lift Either: Right"
+         (variantFromEither (Right B :: Either A B) == toVariant B)
+
+   , testProperty "To Either: Left"
+         (variantToEither (toVariant B :: V '[A,B]) == Left B)
+   , testProperty "To Either: Right"
+         (variantToEither (toVariant A :: V '[A,B]) == Right A)
+
+   , testProperty "popVariantHead (match)"
+         (popVariantHead (toVariant A :: ABC) == Right A)
+   , testProperty "popVariantHead (don't match)"
+         (isLeft (popVariantHead b))
+
+   , testProperty "popVariantAt (match)"
+         (popVariantAt @1 b == Right B)
+   , testProperty "popVariantAt (don't match)"
+         (isLeft (popVariantAt @2 b))
+
+   , testProperty "popVariant (match)"
+         (popVariant @D (toVariantAt @4 D :: V '[A,B,C,B,D,E,D]) == Right D)
+   , testProperty "popVariant (match)"
+         (popVariant @D (toVariantAt @6 D :: V '[A,B,C,B,D,E,D]) == Right D)
+   , testProperty "popVariant (don't match)"
+         (popVariant @B (toVariantAt @4 D :: V '[A,B,C,B,D,E,D]) == Left (toVariantAt @2 D))
+
+   , testProperty "prependVariant"
+         (fromVariantAt @4 (prependVariant @'[D,E,F] b) == Just B)
+   , testProperty "appendVariant"
+         (fromVariantAt @1 (appendVariant @'[D,E,F] b)  == Just B)
+
+   , testProperty "alterVariant"
+         (alterVariant @Num (+1) (toVariant (1.0 :: Float) :: V '[Int,Float]) == toVariant (2.0 :: Float))
+   , testProperty "alterVariant"
+         (alterVariant @Num (+1) (toVariant (1.0 :: Float) :: V '[Float,Int]) == toVariant (2.0 :: Float))
+
+   , testProperty "traverseVariant"
+         (traverseVariant @OrdNum (\x -> if x > 1 then Just x else Nothing)
+            (toVariant (2.0 :: Float) :: V '[Float,Int]) == Just (toVariant (2.0 :: Float)))
+   , testProperty "traverseVariant"
+         (traverseVariant @OrdNum (\x -> if x > 1 then Just x else Nothing)
+            (toVariant (0.5 :: Float) :: V '[Float,Int]) == Nothing)
+
+   , testProperty "liftVariant"
+         (fromVariant (liftVariant b :: V '[D,A,E,B,F,C])  == Just B)
+   ]
+
+class (Ord a, Num a) => OrdNum a
+instance (Ord a, Num a) => OrdNum a