{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE UndecidableInstances #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Row.Variants
--
-- This module implements extensible variants using closed type families.
--
-----------------------------------------------------------------------------


module Data.Row.Variants
  (
  -- * Types and constraints
    Label(..)
  , KnownSymbol, AllUniqueLabels, WellBehaved
  , Var, Row, Empty, type (≈)
  -- * Construction
  , HasType, pattern IsJust, singleton, unSingleton
  , fromLabels, fromLabelsMap
  -- ** Extension
  , type (.\), Lacks, type (.\/), diversify, extend, type (.+)
  -- ** Modification
  , update, focus, Modify, rename, Rename
  -- * Destruction
  , impossible, trial, trial', multiTrial, view
  , Subset
  , restrict, split
  -- ** Types for destruction
  , type (.!), type (.-), type (.\\), type (.==)
  -- * Native Conversion
  -- $native
  , toNative, fromNative, fromNativeGeneral
  , ToNative, FromNative, FromNativeGeneral
  , NativeRow
  -- * Row operations
  -- ** Map
  , Map, map, map', transform, transform'
  -- ** Fold
  , Forall, erase, eraseWithLabels, eraseZipGeneral, eraseZip
  -- ** Applicative-like functions
  , traverse, traverseMap
  , sequence
  -- ** Compose
  -- $compose
  , compose, uncompose
  -- ** labels
  , labels
  -- ** ApSingle functions
  , eraseSingle, mapSingle, mapSingleA, eraseZipSingle
  -- ** Coerce
  , coerceVar
  )
where

import Prelude hiding (map, sequence, traverse, zip)

import Control.Applicative
import Control.DeepSeq     (NFData(..), deepseq)

import Data.Bifunctor                 (Bifunctor(..))
import Data.Coerce
import Data.Functor.Compose
import Data.Functor.Identity
import Data.Functor.Product
import Data.Generics.Sum.Constructors (AsConstructor(..), AsConstructor'(..))
import Data.Maybe                     (fromMaybe)
import Data.Profunctor                (Choice(..), Profunctor(..))
import Data.Proxy
import Data.String                    (IsString)
import Data.Text                      (Text)

import qualified GHC.Generics as G
import           GHC.TypeLits

import Unsafe.Coerce

import Data.Row.Dictionaries
import Data.Row.Internal

{--------------------------------------------------------------------
  Polymorphic Variants
--------------------------------------------------------------------}

-- | The variant type.
data Var (r :: Row *) where
  OneOf :: Text -> HideType -> Var r

instance Forall r Show => Show (Var r) where
  show :: Var r -> String
show Var r
v = (\ (String
x, String
y) -> String
"{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}") ((String, String) -> String) -> (String, String) -> String
forall a b. (a -> b) -> a -> b
$ (forall a. Show a => a -> String) -> Var r -> (String, String)
forall (c :: * -> Constraint) (ρ :: Row *) s b.
(Forall ρ c, IsString s) =>
(forall a. c a => a -> b) -> Var ρ -> (s, b)
eraseWithLabels @Show forall a. Show a => a -> String
show Var r
v

instance Forall r Eq => Eq (Var r) where
  Var r
r == :: Var r -> Var r -> Bool
== Var r
r' = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (forall a. Eq a => a -> a -> Bool) -> Var r -> Var r -> Maybe Bool
forall (c :: * -> Constraint) (ρ :: Row *) b.
Forall ρ c =>
(forall a. c a => a -> a -> b) -> Var ρ -> Var ρ -> Maybe b
eraseZip @Eq forall a. Eq a => a -> a -> Bool
(==) Var r
r Var r
r'

instance (Forall r Eq, Forall r Ord) => Ord (Var r) where
  compare :: Var r -> Var r -> Ordering
  compare :: Var r -> Var r -> Ordering
compare = (Forall r Ord, IsString Text) =>
(forall x y.
 (Ord x, Ord y) =>
 Either (Text, x, x) ((Text, x), (Text, y)) -> Ordering)
-> Var r -> Var r -> Ordering
forall (c :: * -> Constraint) (ρ :: Row *) b s.
(Forall ρ c, IsString s) =>
(forall x y. (c x, c y) => Either (s, x, x) ((s, x), (s, y)) -> b)
-> Var ρ -> Var ρ -> b
eraseZipGeneral @Ord @r @Ordering @Text ((forall x y.
  (Ord x, Ord y) =>
  Either (Text, x, x) ((Text, x), (Text, y)) -> Ordering)
 -> Var r -> Var r -> Ordering)
-> (forall x y.
    (Ord x, Ord y) =>
    Either (Text, x, x) ((Text, x), (Text, y)) -> Ordering)
-> Var r
-> Var r
-> Ordering
forall a b. (a -> b) -> a -> b
$ \case
    (Left (Text
_, x
x, x
y))           -> x -> x -> Ordering
forall a. Ord a => a -> a -> Ordering
compare x
x x
y
    (Right ((Text
s1, x
_), (Text
s2, y
_))) -> Text -> Text -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Text
s1 Text
s2

instance Forall r NFData => NFData (Var r) where
  rnf :: Var r -> ()
rnf Var r
r = Const () r -> ()
forall a k (b :: k). Const a b -> a
getConst (Const () r -> ()) -> Const () r -> ()
forall a b. (a -> b) -> a -> b
$ Proxy (Proxy Identity, Proxy Either)
-> (Var Empty -> Const () Empty)
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, NFData τ, HasType ℓ τ ρ) =>
    Label ℓ -> Var ρ -> Either (Var (ρ .- ℓ)) (Identity τ))
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, NFData τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> Either (Const () ρ) (Identity τ) -> Const () (Extend ℓ τ ρ))
-> Var r
-> Const () r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @NFData @Either @Var @(Const ()) @Identity Proxy (Proxy Identity, Proxy Either)
forall k (t :: k). Proxy t
Proxy Var Empty -> Const () Empty
forall k b (b :: k). b -> Const () b
empty forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, NFData τ, HasType ℓ τ ρ) =>
Label ℓ -> Var ρ -> Either (Var (ρ .- ℓ)) (Identity τ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Var r -> Either (Var (r .- l)) (Identity (r .! l))
doUncons forall k a p (b :: k). NFData a => p -> a -> Const () b
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, NFData τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Either (Const () ρ) (Identity τ) -> Const () (Extend ℓ τ ρ)
doCons Var r
r
    where empty :: b -> Const () b
empty = Const () b -> b -> Const () b
forall a b. a -> b -> a
const (Const () b -> b -> Const () b) -> Const () b -> b -> Const () b
forall a b. (a -> b) -> a -> b
$ () -> Const () b
forall k a (b :: k). a -> Const a b
Const ()
          doUncons :: Label l -> Var r -> Either (Var (r .- l)) (Identity (r .! l))
doUncons Label l
l = ((r .! l) -> Identity (r .! l))
-> Either (Var (r .- l)) (r .! l)
-> Either (Var (r .- l)) (Identity (r .! l))
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (r .! l) -> Identity (r .! l)
forall a. a -> Identity a
Identity (Either (Var (r .- l)) (r .! l)
 -> Either (Var (r .- l)) (Identity (r .! l)))
-> (Var r -> Either (Var (r .- l)) (r .! l))
-> Var r
-> Either (Var (r .- l)) (Identity (r .! l))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var r -> Label l -> Either (Var (r .- l)) (r .! l))
-> Label l -> Var r -> Either (Var (r .- l)) (r .! l)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Var r -> Label l -> Either (Var (r .- l)) (r .! l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Label l
l
          doCons :: p -> a -> Const () b
doCons p
_ a
x = a -> Const () b -> Const () b
forall a b. NFData a => a -> b -> b
deepseq a
x (Const () b -> Const () b) -> Const () b -> Const () b
forall a b. (a -> b) -> a -> b
$ () -> Const () b
forall k a (b :: k). a -> Const a b
Const ()


{--------------------------------------------------------------------
  Basic Operations
--------------------------------------------------------------------}

-- | A Variant with no options is uninhabited.
impossible :: Var Empty -> a
impossible :: Var Empty -> a
impossible Var Empty
_ = String -> a
forall a. HasCallStack => String -> a
error String
"Impossible! Somehow, a variant of nothing was produced."

-- | A quick constructor to create a singleton variant.
singleton :: KnownSymbol l => Label l -> a -> Var (l .== a)
singleton :: Label l -> a -> Var (l .== a)
singleton = Label l -> a -> Var (l .== a)
forall (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Label l -> (r .! l) -> Var r
IsJust

-- | A quick destructor for singleton variants.
unSingleton :: forall l a. KnownSymbol l => Var (l .== a) -> (Label l, a)
unSingleton :: Var (l .== a) -> (Label l, a)
unSingleton (OneOf Text
_ (HideType a
x)) = (Label l
l, a -> a
forall a b. a -> b
unsafeCoerce a
x) where l :: Label l
l = Label l
forall (s :: Symbol). Label s
Label @l

-- | A pattern for variants; can be used to both destruct a variant
-- when in a pattern position or construct one in an expression position.
pattern IsJust :: forall l r. (AllUniqueLabels r, KnownSymbol l) => Label l -> r .! l -> Var r
pattern $bIsJust :: Label l -> (r .! l) -> Var r
$mIsJust :: forall r (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Var r -> (Label l -> (r .! l) -> r) -> (Void# -> r) -> r
IsJust l a <- (isJustHelper @l -> (l, Just a)) where
        IsJust (Label l -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
l) = Text -> HideType -> Var r
forall (r :: Row *). Text -> HideType -> Var r
OneOf Text
l (HideType -> Var r) -> ((r .! l) -> HideType) -> (r .! l) -> Var r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (r .! l) -> HideType
forall a. a -> HideType
HideType

isJustHelper :: forall l r. KnownSymbol l => Var r -> (Label l, Maybe (r .! l))
isJustHelper :: Var r -> (Label l, Maybe (r .! l))
isJustHelper Var r
v = (Label l
l, Label l -> Var r -> Maybe (r .! l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Var r -> Maybe (r .! l)
view Label l
l Var r
v) where l :: Label l
l = Label l
forall (s :: Symbol). Label s
Label @l

-- | Make the variant arbitrarily more diverse.
diversify :: forall r' r. Var r -> Var (r .\/ r')
diversify :: Var r -> Var (r .\/ r')
diversify = Var r -> Var (r .\/ r')
forall a b. a -> b
unsafeCoerce -- (OneOf l x) = OneOf l x

-- | A weaker version of 'diversify', but it's helpful for 'metamorph' as it explicitly
-- uses 'Extend'.
extend :: forall a l r. KnownSymbol l => Label l -> Var r -> Var (Extend l a r)
extend :: Label l -> Var r -> Var (Extend l a r)
extend Label l
_ = Var r -> Var (Extend l a r)
forall a b. a -> b
unsafeCoerce

-- | If the variant exists at the given label, update it to the given value.
-- Otherwise, do nothing.
update :: (KnownSymbol l, r .! l ≈ a) => Label l -> a -> Var r -> Var r
update :: Label l -> a -> Var r -> Var r
update (Label l -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
l') a
a (OneOf Text
l HideType
x) = Text -> HideType -> Var r
forall (r :: Row *). Text -> HideType -> Var r
OneOf Text
l (HideType -> Var r) -> HideType -> Var r
forall a b. (a -> b) -> a -> b
$ if Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
l' then a -> HideType
forall a. a -> HideType
HideType a
a else HideType
x

-- | If the variant exists at the given label, focus on the value associated with it.
-- Otherwise, do nothing.
focus :: forall l r r' a b p f.
  ( AllUniqueLabels r
  , AllUniqueLabels r'
  , KnownSymbol l
  , r  .! l ≈ a
  , r' .! l ≈ b
  , r' ≈ (r .- l) .\/ (l .== b)
  , Applicative f
  , Choice p
  ) => Label l -> p a (f b) -> p (Var r) (f (Var r'))
focus :: Label l -> p a (f b) -> p (Var r) (f (Var r'))
focus (Label l -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
l) =
  (Var r -> Either a (Var r'))
-> (Either (f b) (Var r') -> f (Var r'))
-> p (Either a (Var r')) (Either (f b) (Var r'))
-> p (Var r) (f (Var r'))
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap Var r -> Either a (Var r')
unwrap Either (f b) (Var r') -> f (Var r')
rewrap (p (Either a (Var r')) (Either (f b) (Var r'))
 -> p (Var r) (f (Var r')))
-> (p a (f b) -> p (Either a (Var r')) (Either (f b) (Var r')))
-> p a (f b)
-> p (Var r) (f (Var r'))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p a (f b) -> p (Either a (Var r')) (Either (f b) (Var r'))
forall (p :: * -> * -> *) a b c.
Choice p =>
p a b -> p (Either a c) (Either b c)
left'
  where
    unwrap :: Var r -> Either a (Var r')
    unwrap :: Var r -> Either a (Var r')
unwrap (OneOf Text
l' (HideType a
x))
      | Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
l'   = a -> Either a (Var r')
forall a b. a -> Either a b
Left (a -> a
forall a b. a -> b
unsafeCoerce a
x)
      | Bool
otherwise = Var r' -> Either a (Var r')
forall a b. b -> Either a b
Right (Text -> HideType -> Var r'
forall (r :: Row *). Text -> HideType -> Var r
OneOf Text
l' (a -> HideType
forall a. a -> HideType
HideType a
x))
    rewrap :: Either (f b) (Var r') -> f (Var r')
    rewrap :: Either (f b) (Var r') -> f (Var r')
rewrap = (f b -> f (Var r'))
-> (Var r' -> f (Var r')) -> Either (f b) (Var r') -> f (Var r')
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((b -> Var r') -> f b -> f (Var r')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> Var r') -> f b -> f (Var r'))
-> (b -> Var r') -> f b -> f (Var r')
forall a b. (a -> b) -> a -> b
$ Text -> HideType -> Var r'
forall (r :: Row *). Text -> HideType -> Var r
OneOf Text
l (HideType -> Var r') -> (b -> HideType) -> b -> Var r'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> HideType
forall a. a -> HideType
HideType) Var r' -> f (Var r')
forall (f :: * -> *) a. Applicative f => a -> f a
pure

-- | Rename the given label.
rename :: (KnownSymbol l, KnownSymbol l') => Label l -> Label l' -> Var r -> Var (Rename l l' r)
rename :: Label l -> Label l' -> Var r -> Var (Rename l l' r)
rename (Label l -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
l1) (Label l' -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
l2) (OneOf Text
l HideType
x) = Text -> HideType -> Var (Extend l' (r .! l) (r .- l))
forall (r :: Row *). Text -> HideType -> Var r
OneOf (if Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
l1 then Text
l2 else Text
l) HideType
x

-- | Convert a variant into either the value at the given label or a variant without
-- that label.  This is the basic variant destructor.
trial :: KnownSymbol l => Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial :: Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial (OneOf Text
l (HideType a
x)) (Label l -> Text
forall (s :: Symbol). KnownSymbol s => Label s -> Text
toKey -> Text
l') = if Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== Text
l' then (r .! l) -> Either (Var (r .- l)) (r .! l)
forall a b. b -> Either a b
Right (a -> r .! l
forall a b. a -> b
unsafeCoerce a
x) else Var (r .- l) -> Either (Var (r .- l)) (r .! l)
forall a b. a -> Either a b
Left (Text -> HideType -> Var (r .- l)
forall (r :: Row *). Text -> HideType -> Var r
OneOf Text
l (a -> HideType
forall a. a -> HideType
HideType a
x))

-- | A version of 'trial' that ignores the leftover variant.
trial' :: KnownSymbol l => Var r -> Label l -> Maybe (r .! l)
trial' :: Var r -> Label l -> Maybe (r .! l)
trial' = ((Var (r .- l) -> Maybe (r .! l))
-> ((r .! l) -> Maybe (r .! l))
-> Either (Var (r .- l)) (r .! l)
-> Maybe (r .! l)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (r .! l) -> Var (r .- l) -> Maybe (r .! l)
forall a b. a -> b -> a
const Maybe (r .! l)
forall a. Maybe a
Nothing) (r .! l) -> Maybe (r .! l)
forall a. a -> Maybe a
Just (Either (Var (r .- l)) (r .! l) -> Maybe (r .! l))
-> (Label l -> Either (Var (r .- l)) (r .! l))
-> Label l
-> Maybe (r .! l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Label l -> Either (Var (r .- l)) (r .! l))
 -> Label l -> Maybe (r .! l))
-> (Var r -> Label l -> Either (Var (r .- l)) (r .! l))
-> Var r
-> Label l
-> Maybe (r .! l)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var r -> Label l -> Either (Var (r .- l)) (r .! l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial

-- | A trial over multiple types
multiTrial :: forall x y. (AllUniqueLabels x, FreeForall x) => Var y -> Either (Var (y .\\ x)) (Var x)
multiTrial :: Var y -> Either (Var (y .\\ x)) (Var x)
multiTrial (OneOf Text
l HideType
x) = if Text
l Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall s. (IsString s, Forall x Unconstrained1) => [s]
forall k (ρ :: Row k) (c :: k -> Constraint) s.
(IsString s, Forall ρ c) =>
[s]
labels @x @Unconstrained1 then Var x -> Either (Var (y .\\ x)) (Var x)
forall a b. b -> Either a b
Right (Text -> HideType -> Var x
forall (r :: Row *). Text -> HideType -> Var r
OneOf Text
l HideType
x) else Var (y .\\ x) -> Either (Var (y .\\ x)) (Var x)
forall a b. a -> Either a b
Left (Text -> HideType -> Var (y .\\ x)
forall (r :: Row *). Text -> HideType -> Var r
OneOf Text
l HideType
x)

-- | A convenient function for using view patterns when dispatching variants.
--   For example:
--
-- @
-- myShow :: Var ("y" '::= String :| "x" '::= Int :| Empty) -> String
-- myShow (view x -> Just n) = "Int of "++show n
-- myShow (view y -> Just s) = "String of "++s @
view :: KnownSymbol l => Label l -> Var r -> Maybe (r .! l)
view :: Label l -> Var r -> Maybe (r .! l)
view = (Var r -> Label l -> Maybe (r .! l))
-> Label l -> Var r -> Maybe (r .! l)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Var r -> Label l -> Maybe (r .! l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Maybe (r .! l)
trial'

-- | Split a variant into two sub-variants.
split :: forall s r. (WellBehaved s, Subset s r) => Var r -> Either (Var (r .\\ s)) (Var s)
split :: Var r -> Either (Var (r .\\ s)) (Var s)
split (OneOf Text
l HideType
a) | Text
l Text -> [Text] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall s. (IsString s, Forall s Unconstrained1) => [s]
forall k (ρ :: Row k) (c :: k -> Constraint) s.
(IsString s, Forall ρ c) =>
[s]
labels @s @Unconstrained1 = Var s -> Either (Var (r .\\ s)) (Var s)
forall a b. b -> Either a b
Right (Var s -> Either (Var (r .\\ s)) (Var s))
-> Var s -> Either (Var (r .\\ s)) (Var s)
forall a b. (a -> b) -> a -> b
$ Text -> HideType -> Var s
forall (r :: Row *). Text -> HideType -> Var r
OneOf Text
l HideType
a
                  | Bool
otherwise                          = Var (r .\\ s) -> Either (Var (r .\\ s)) (Var s)
forall a b. a -> Either a b
Left  (Var (r .\\ s) -> Either (Var (r .\\ s)) (Var s))
-> Var (r .\\ s) -> Either (Var (r .\\ s)) (Var s)
forall a b. (a -> b) -> a -> b
$ Text -> HideType -> Var (r .\\ s)
forall (r :: Row *). Text -> HideType -> Var r
OneOf Text
l HideType
a

-- | Arbitrary variant restriction.  Turn a variant into a subset of itself.
restrict :: forall r r'. (WellBehaved r, Subset r r') => Var r' -> Maybe (Var r)
restrict :: Var r' -> Maybe (Var r)
restrict = (Var (r' .\\ r) -> Maybe (Var r))
-> (Var r -> Maybe (Var r))
-> Either (Var (r' .\\ r)) (Var r)
-> Maybe (Var r)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (Var r) -> Var (r' .\\ r) -> Maybe (Var r)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Var r)
forall a. Maybe a
Nothing) Var r -> Maybe (Var r)
forall a. a -> Maybe a
Just (Either (Var (r' .\\ r)) (Var r) -> Maybe (Var r))
-> (Var r' -> Either (Var (r' .\\ r)) (Var r))
-> Var r'
-> Maybe (Var r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var r' -> Either (Var (r' .\\ r)) (Var r)
forall (s :: Row *) (r :: Row *).
(WellBehaved s, Subset s r) =>
Var r -> Either (Var (r .\\ s)) (Var s)
split


{--------------------------------------------------------------------
  Folds and maps
--------------------------------------------------------------------}

-- | A standard fold
erase :: forall c ρ b. Forall ρ c => (forall a. c a => a -> b) -> Var ρ -> b
erase :: (forall a. c a => a -> b) -> Var ρ -> b
erase forall a. c a => a -> b
f = forall b. (String, b) -> b
forall a b. (a, b) -> b
snd @String ((String, b) -> b) -> (Var ρ -> (String, b)) -> Var ρ -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. c a => a -> b) -> Var ρ -> (String, b)
forall (c :: * -> Constraint) (ρ :: Row *) s b.
(Forall ρ c, IsString s) =>
(forall a. c a => a -> b) -> Var ρ -> (s, b)
eraseWithLabels @c forall a. c a => a -> b
f

-- | A fold with labels
eraseWithLabels :: forall c ρ s b. (Forall ρ c, IsString s) => (forall a. c a => a -> b) -> Var ρ -> (s,b)
eraseWithLabels :: (forall a. c a => a -> b) -> Var ρ -> (s, b)
eraseWithLabels forall a. c a => a -> b
f = Const (s, b) ρ -> (s, b)
forall a k (b :: k). Const a b -> a
getConst (Const (s, b) ρ -> (s, b))
-> (Var ρ -> Const (s, b) ρ) -> Var ρ -> (s, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy Identity, Proxy Either)
-> (Var Empty -> Const (s, b) Empty)
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> Var ρ -> Either (Var (ρ .- ℓ)) (Identity τ))
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> Either (Const (s, b) ρ) (Identity τ)
    -> Const (s, b) (Extend ℓ τ ρ))
-> Var ρ
-> Const (s, b) ρ
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @ρ @c @Either @Var @(Const (s,b)) @Identity Proxy (Proxy Identity, Proxy Either)
forall k (t :: k). Proxy t
Proxy Var Empty -> Const (s, b) Empty
forall a. Var Empty -> a
impossible forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> Var ρ -> Either (Var (ρ .- ℓ)) (Identity τ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Var r -> Either (Var (r .- l)) (Identity (r .! l))
doUncons forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Either (Const (s, b) ρ) (Identity τ)
-> Const (s, b) (Extend ℓ τ ρ)
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ) =>
Label ℓ
-> Either (Const (s, b) ρ) (Identity τ)
-> Const (s, b) (Extend ℓ τ ρ)
doCons
  where doUncons :: Label l -> Var r -> Either (Var (r .- l)) (Identity (r .! l))
doUncons Label l
l = ((r .! l) -> Identity (r .! l))
-> Either (Var (r .- l)) (r .! l)
-> Either (Var (r .- l)) (Identity (r .! l))
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (r .! l) -> Identity (r .! l)
forall a. a -> Identity a
Identity (Either (Var (r .- l)) (r .! l)
 -> Either (Var (r .- l)) (Identity (r .! l)))
-> (Var r -> Either (Var (r .- l)) (r .! l))
-> Var r
-> Either (Var (r .- l)) (Identity (r .! l))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var r -> Label l -> Either (Var (r .- l)) (r .! l))
-> Label l -> Var r -> Either (Var (r .- l)) (r .! l)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Var r -> Label l -> Either (Var (r .- l)) (r .! l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Label l
l
        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ)
               => Label ℓ -> Either (Const (s,b) ρ) (Identity τ) -> Const (s,b) (Extend ℓ τ ρ)
        doCons :: Label ℓ
-> Either (Const (s, b) ρ) (Identity τ)
-> Const (s, b) (Extend ℓ τ ρ)
doCons Label ℓ
_ (Left  (Const (s, b)
c)) = (s, b) -> Const (s, b) (Extend ℓ τ ρ)
forall k a (b :: k). a -> Const a b
Const (s, b)
c
        doCons Label ℓ
l (Right (Identity τ
x)) = (s, b) -> Const (s, b) (Extend ℓ τ ρ)
forall k a (b :: k). a -> Const a b
Const (Label ℓ -> s
forall s a. (IsString s, Show a) => a -> s
show' Label ℓ
l, τ -> b
forall a. c a => a -> b
f τ
x)


data ErasedVal c s = forall y. c y => ErasedVal (s, y)
data ErasePair c s ρ = ErasePair (Either (ErasedVal c s) (Var ρ)) (Either (ErasedVal c s) (Var ρ))

-- | A fold over two variants at once.  A call @eraseZipGeneral f x y@ will return
-- @f (Left (show l, a, b))@ when 'x' and 'y' both have values at the same label 'l'
-- and will return @f (Right ((show l1, a), (show l2, b)))@ when they have values
-- at different labels 'l1' and 'l2' respectively.
eraseZipGeneral
  :: forall c ρ b s. (Forall ρ c, IsString s)
  => (forall x y. (c x, c y) => Either (s, x, x) ((s, x), (s, y)) -> b)
  -> Var ρ -> Var ρ -> b
eraseZipGeneral :: (forall x y. (c x, c y) => Either (s, x, x) ((s, x), (s, y)) -> b)
-> Var ρ -> Var ρ -> b
eraseZipGeneral forall x y. (c x, c y) => Either (s, x, x) ((s, x), (s, y)) -> b
f Var ρ
x Var ρ
y = Const b ρ -> b
forall a k (b :: k). Const a b -> a
getConst (Const b ρ -> b) -> Const b ρ -> b
forall a b. (a -> b) -> a -> b
$ Proxy (Proxy (Const b), Proxy Either)
-> (ErasePair c s Empty -> Const b Empty)
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ
    -> ErasePair c s ρ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ))
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> Either (Const b ρ) (Const b τ) -> Const b (Extend ℓ τ ρ))
-> ErasePair c s ρ
-> Const b ρ
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @ρ @c @Either @(ErasePair c s) @(Const b) @(Const b) Proxy (Proxy (Const b), Proxy Either)
forall k (t :: k). Proxy t
Proxy ErasePair c s Empty -> Const b Empty
doNil forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ
-> ErasePair c s ρ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
doUncons forall k k k p a (b :: k) (b :: k) (b :: k).
p -> Either (Const a b) (Const a b) -> Const a b
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ -> Either (Const b ρ) (Const b τ) -> Const b (Extend ℓ τ ρ)
doCons (Either (ErasedVal c s) (Var ρ)
-> Either (ErasedVal c s) (Var ρ) -> ErasePair c s ρ
forall (c :: * -> Constraint) s (ρ :: Row *).
Either (ErasedVal c s) (Var ρ)
-> Either (ErasedVal c s) (Var ρ) -> ErasePair c s ρ
ErasePair (Var ρ -> Either (ErasedVal c s) (Var ρ)
forall a b. b -> Either a b
Right Var ρ
x) (Var ρ -> Either (ErasedVal c s) (Var ρ)
forall a b. b -> Either a b
Right Var ρ
y))
  where
    doNil :: ErasePair c s Empty -> Const b Empty
doNil (ErasePair (Left (ErasedVal (s, y)
a)) (Left (ErasedVal (s, y)
b))) =
      b -> Const b Empty
forall k a (b :: k). a -> Const a b
Const (b -> Const b Empty) -> b -> Const b Empty
forall a b. (a -> b) -> a -> b
$ Either (s, y, y) ((s, y), (s, y)) -> b
forall x y. (c x, c y) => Either (s, x, x) ((s, x), (s, y)) -> b
f (Either (s, y, y) ((s, y), (s, y)) -> b)
-> Either (s, y, y) ((s, y), (s, y)) -> b
forall a b. (a -> b) -> a -> b
$ ((s, y), (s, y)) -> Either (s, y, y) ((s, y), (s, y))
forall a b. b -> Either a b
Right ((s, y)
a, (s, y)
b)
    doNil (ErasePair (Right Var Empty
x) Either (ErasedVal c s) (Var Empty)
_) = Var Empty -> Const b Empty
forall a. Var Empty -> a
impossible Var Empty
x
    doNil (ErasePair Either (ErasedVal c s) (Var Empty)
_ (Right Var Empty
y)) = Var Empty -> Const b Empty
forall a. Var Empty -> a
impossible Var Empty
y
    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
             => Label ℓ -> ErasePair c s ρ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
    doUncons :: Label ℓ
-> ErasePair c s ρ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
doUncons Label ℓ
_ (ErasePair (Left (ErasedVal (s, y)
a)) (Left (ErasedVal (s, y)
b))) =
      Const b τ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. b -> Either a b
Right (Const b τ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ))
-> Const b τ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. (a -> b) -> a -> b
$ b -> Const b τ
forall k a (b :: k). a -> Const a b
Const (b -> Const b τ) -> b -> Const b τ
forall a b. (a -> b) -> a -> b
$ Either (s, y, y) ((s, y), (s, y)) -> b
forall x y. (c x, c y) => Either (s, x, x) ((s, x), (s, y)) -> b
f (Either (s, y, y) ((s, y), (s, y)) -> b)
-> Either (s, y, y) ((s, y), (s, y)) -> b
forall a b. (a -> b) -> a -> b
$ ((s, y), (s, y)) -> Either (s, y, y) ((s, y), (s, y))
forall a b. b -> Either a b
Right ((s, y)
a, (s, y)
b)
    doUncons Label ℓ
l (ErasePair (Right Var ρ
x) (Left ErasedVal c s
eb)) = case (Var ρ -> Label ℓ -> Either (Var (ρ .- ℓ)) (ρ .! ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Var ρ
x Label ℓ
l, ErasedVal c s
eb) of
      (Right τ
a, ErasedVal (s, y)
b) -> Const b τ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. b -> Either a b
Right (Const b τ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ))
-> Const b τ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. (a -> b) -> a -> b
$ b -> Const b τ
forall k a (b :: k). a -> Const a b
Const (b -> Const b τ) -> b -> Const b τ
forall a b. (a -> b) -> a -> b
$ Either (s, τ, τ) ((s, τ), (s, y)) -> b
forall x y. (c x, c y) => Either (s, x, x) ((s, x), (s, y)) -> b
f (Either (s, τ, τ) ((s, τ), (s, y)) -> b)
-> Either (s, τ, τ) ((s, τ), (s, y)) -> b
forall a b. (a -> b) -> a -> b
$ ((s, τ), (s, y)) -> Either (s, τ, τ) ((s, τ), (s, y))
forall a b. b -> Either a b
Right ((Label ℓ -> s
forall s a. (IsString s, Show a) => a -> s
show' Label ℓ
l, τ
a), (s, y)
b)
      (Left Var (ρ .- ℓ)
x', ErasedVal c s
_)           -> ErasePair c s (ρ .- ℓ)
-> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. a -> Either a b
Left (ErasePair c s (ρ .- ℓ)
 -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ))
-> ErasePair c s (ρ .- ℓ)
-> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. (a -> b) -> a -> b
$ Either (ErasedVal c s) (Var (ρ .- ℓ))
-> Either (ErasedVal c s) (Var (ρ .- ℓ)) -> ErasePair c s (ρ .- ℓ)
forall (c :: * -> Constraint) s (ρ :: Row *).
Either (ErasedVal c s) (Var ρ)
-> Either (ErasedVal c s) (Var ρ) -> ErasePair c s ρ
ErasePair (Var (ρ .- ℓ) -> Either (ErasedVal c s) (Var (ρ .- ℓ))
forall a b. b -> Either a b
Right Var (ρ .- ℓ)
x') (ErasedVal c s -> Either (ErasedVal c s) (Var (ρ .- ℓ))
forall a b. a -> Either a b
Left ErasedVal c s
eb)
    doUncons Label ℓ
l (ErasePair (Left ErasedVal c s
ea) (Right Var ρ
y)) = case (ErasedVal c s
ea, Var ρ -> Label ℓ -> Either (Var (ρ .- ℓ)) (ρ .! ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Var ρ
y Label ℓ
l) of
      (ErasedVal (s, y)
a, Right b) -> Const b τ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. b -> Either a b
Right (Const b τ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ))
-> Const b τ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. (a -> b) -> a -> b
$ b -> Const b τ
forall k a (b :: k). a -> Const a b
Const (b -> Const b τ) -> b -> Const b τ
forall a b. (a -> b) -> a -> b
$ Either (s, y, y) ((s, y), (s, τ)) -> b
forall x y. (c x, c y) => Either (s, x, x) ((s, x), (s, y)) -> b
f (Either (s, y, y) ((s, y), (s, τ)) -> b)
-> Either (s, y, y) ((s, y), (s, τ)) -> b
forall a b. (a -> b) -> a -> b
$ ((s, y), (s, τ)) -> Either (s, y, y) ((s, y), (s, τ))
forall a b. b -> Either a b
Right ((s, y)
a, (Label ℓ -> s
forall s a. (IsString s, Show a) => a -> s
show' Label ℓ
l, τ
b))
      (ErasedVal c s
_, Left Var (ρ .- ℓ)
x')           -> ErasePair c s (ρ .- ℓ)
-> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. a -> Either a b
Left (ErasePair c s (ρ .- ℓ)
 -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ))
-> ErasePair c s (ρ .- ℓ)
-> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. (a -> b) -> a -> b
$ Either (ErasedVal c s) (Var (ρ .- ℓ))
-> Either (ErasedVal c s) (Var (ρ .- ℓ)) -> ErasePair c s (ρ .- ℓ)
forall (c :: * -> Constraint) s (ρ :: Row *).
Either (ErasedVal c s) (Var ρ)
-> Either (ErasedVal c s) (Var ρ) -> ErasePair c s ρ
ErasePair (ErasedVal c s -> Either (ErasedVal c s) (Var (ρ .- ℓ))
forall a b. a -> Either a b
Left ErasedVal c s
ea) (Var (ρ .- ℓ) -> Either (ErasedVal c s) (Var (ρ .- ℓ))
forall a b. b -> Either a b
Right Var (ρ .- ℓ)
x')
    doUncons Label ℓ
l (ErasePair (Right Var ρ
x) (Right Var ρ
y)) = case (Var ρ -> Label ℓ -> Either (Var (ρ .- ℓ)) (ρ .! ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Var ρ
x Label ℓ
l, Var ρ -> Label ℓ -> Either (Var (ρ .- ℓ)) (ρ .! ℓ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Var ρ
y Label ℓ
l) of
      (Right (τ
a :: x), Right τ
b) -> Const b τ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. b -> Either a b
Right (Const b τ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ))
-> Const b τ -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. (a -> b) -> a -> b
$ b -> Const b τ
forall k a (b :: k). a -> Const a b
Const (b -> Const b τ) -> b -> Const b τ
forall a b. (a -> b) -> a -> b
$ (c τ, c τ) => Either (s, τ, τ) ((s, τ), (s, τ)) -> b
forall x y. (c x, c y) => Either (s, x, x) ((s, x), (s, y)) -> b
f @x @x (Either (s, τ, τ) ((s, τ), (s, τ)) -> b)
-> Either (s, τ, τ) ((s, τ), (s, τ)) -> b
forall a b. (a -> b) -> a -> b
$ (s, τ, τ) -> Either (s, τ, τ) ((s, τ), (s, τ))
forall a b. a -> Either a b
Left (Label ℓ -> s
forall s a. (IsString s, Show a) => a -> s
show' Label ℓ
l, τ
a, τ
b)
      (Right τ
a,        Left Var (ρ .- ℓ)
y') -> ErasePair c s (ρ .- ℓ)
-> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. a -> Either a b
Left (ErasePair c s (ρ .- ℓ)
 -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ))
-> ErasePair c s (ρ .- ℓ)
-> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. (a -> b) -> a -> b
$ Either (ErasedVal c s) (Var (ρ .- ℓ))
-> Either (ErasedVal c s) (Var (ρ .- ℓ)) -> ErasePair c s (ρ .- ℓ)
forall (c :: * -> Constraint) s (ρ :: Row *).
Either (ErasedVal c s) (Var ρ)
-> Either (ErasedVal c s) (Var ρ) -> ErasePair c s ρ
ErasePair (ErasedVal c s -> Either (ErasedVal c s) (Var (ρ .- ℓ))
forall a b. a -> Either a b
Left (ErasedVal c s -> Either (ErasedVal c s) (Var (ρ .- ℓ)))
-> ErasedVal c s -> Either (ErasedVal c s) (Var (ρ .- ℓ))
forall a b. (a -> b) -> a -> b
$ (s, τ) -> ErasedVal c s
forall (c :: * -> Constraint) s y. c y => (s, y) -> ErasedVal c s
ErasedVal (Label ℓ -> s
forall s a. (IsString s, Show a) => a -> s
show' Label ℓ
l, τ
a)) (Var (ρ .- ℓ) -> Either (ErasedVal c s) (Var (ρ .- ℓ))
forall a b. b -> Either a b
Right Var (ρ .- ℓ)
y')
      (Left Var (ρ .- ℓ)
x', Right τ
b)        -> ErasePair c s (ρ .- ℓ)
-> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. a -> Either a b
Left (ErasePair c s (ρ .- ℓ)
 -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ))
-> ErasePair c s (ρ .- ℓ)
-> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. (a -> b) -> a -> b
$ Either (ErasedVal c s) (Var (ρ .- ℓ))
-> Either (ErasedVal c s) (Var (ρ .- ℓ)) -> ErasePair c s (ρ .- ℓ)
forall (c :: * -> Constraint) s (ρ :: Row *).
Either (ErasedVal c s) (Var ρ)
-> Either (ErasedVal c s) (Var ρ) -> ErasePair c s ρ
ErasePair (Var (ρ .- ℓ) -> Either (ErasedVal c s) (Var (ρ .- ℓ))
forall a b. b -> Either a b
Right Var (ρ .- ℓ)
x') (ErasedVal c s -> Either (ErasedVal c s) (Var (ρ .- ℓ))
forall a b. a -> Either a b
Left (ErasedVal c s -> Either (ErasedVal c s) (Var (ρ .- ℓ)))
-> ErasedVal c s -> Either (ErasedVal c s) (Var (ρ .- ℓ))
forall a b. (a -> b) -> a -> b
$ (s, τ) -> ErasedVal c s
forall (c :: * -> Constraint) s y. c y => (s, y) -> ErasedVal c s
ErasedVal (Label ℓ -> s
forall s a. (IsString s, Show a) => a -> s
show' Label ℓ
l, τ
b))
      (Left Var (ρ .- ℓ)
x', Left Var (ρ .- ℓ)
y')        -> ErasePair c s (ρ .- ℓ)
-> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. a -> Either a b
Left (ErasePair c s (ρ .- ℓ)
 -> Either (ErasePair c s (ρ .- ℓ)) (Const b τ))
-> ErasePair c s (ρ .- ℓ)
-> Either (ErasePair c s (ρ .- ℓ)) (Const b τ)
forall a b. (a -> b) -> a -> b
$ Either (ErasedVal c s) (Var (ρ .- ℓ))
-> Either (ErasedVal c s) (Var (ρ .- ℓ)) -> ErasePair c s (ρ .- ℓ)
forall (c :: * -> Constraint) s (ρ :: Row *).
Either (ErasedVal c s) (Var ρ)
-> Either (ErasedVal c s) (Var ρ) -> ErasePair c s ρ
ErasePair (Var (ρ .- ℓ) -> Either (ErasedVal c s) (Var (ρ .- ℓ))
forall a b. b -> Either a b
Right Var (ρ .- ℓ)
x') (Var (ρ .- ℓ) -> Either (ErasedVal c s) (Var (ρ .- ℓ))
forall a b. b -> Either a b
Right Var (ρ .- ℓ)
y')
    doCons :: p -> Either (Const a b) (Const a b) -> Const a b
doCons p
_ (Left  (Const a
b)) = a -> Const a b
forall k a (b :: k). a -> Const a b
Const a
b
    doCons p
_ (Right (Const a
b)) = a -> Const a b
forall k a (b :: k). a -> Const a b
Const a
b


-- | A simpler fold over two variants at once
eraseZip :: forall c ρ b. Forall ρ c => (forall a. c a => a -> a -> b) -> Var ρ -> Var ρ -> Maybe b
eraseZip :: (forall a. c a => a -> a -> b) -> Var ρ -> Var ρ -> Maybe b
eraseZip forall a. c a => a -> a -> b
f = (Forall ρ c, IsString Text) =>
(forall x y.
 (c x, c y) =>
 Either (Text, x, x) ((Text, x), (Text, y)) -> Maybe b)
-> Var ρ -> Var ρ -> Maybe b
forall (c :: * -> Constraint) (ρ :: Row *) b s.
(Forall ρ c, IsString s) =>
(forall x y. (c x, c y) => Either (s, x, x) ((s, x), (s, y)) -> b)
-> Var ρ -> Var ρ -> b
eraseZipGeneral @c @ρ @(Maybe b) @Text ((forall x y.
  (c x, c y) =>
  Either (Text, x, x) ((Text, x), (Text, y)) -> Maybe b)
 -> Var ρ -> Var ρ -> Maybe b)
-> (forall x y.
    (c x, c y) =>
    Either (Text, x, x) ((Text, x), (Text, y)) -> Maybe b)
-> Var ρ
-> Var ρ
-> Maybe b
forall a b. (a -> b) -> a -> b
$ \case
    Left (Text
_,x
x,x
y) -> b -> Maybe b
forall a. a -> Maybe a
Just (x -> x -> b
forall a. c a => a -> a -> b
f x
x x
y)
    Either (Text, x, x) ((Text, x), (Text, y))
_            -> Maybe b
forall a. Maybe a
Nothing


-- | VMap is used internally as a type level lambda for defining variant maps.
newtype VMap f ρ = VMap { VMap f ρ -> Var (Map f ρ)
unVMap :: Var (Map f ρ) }
newtype VMap2 f g ρ = VMap2 { VMap2 f g ρ -> Var (Map f (Map g ρ))
unVMap2 :: Var (Map f (Map g ρ)) }

-- | A function to map over a variant given a constraint.
map :: forall c f r. Forall r c => (forall a. c a => a -> f a) -> Var r -> Var (Map f r)
map :: (forall a. c a => a -> f a) -> Var r -> Var (Map f r)
map forall a. c a => a -> f a
f = VMap f r -> Var (Map f r)
forall a (f :: a -> *) (ρ :: Row a). VMap f ρ -> Var (Map f ρ)
unVMap (VMap f r -> Var (Map f r))
-> (Var r -> VMap f r) -> Var r -> Var (Map f r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy Identity, Proxy Either)
-> (Var Empty -> VMap f Empty)
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> Var ρ -> Either (Var (ρ .- ℓ)) (Identity τ))
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> Either (VMap f ρ) (Identity τ) -> VMap f (Extend ℓ τ ρ))
-> Var r
-> VMap f r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @c @Either @Var @(VMap f) @Identity Proxy (Proxy Identity, Proxy Either)
forall k (t :: k). Proxy t
Proxy Var Empty -> VMap f Empty
forall a. Var Empty -> a
impossible forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> Var ρ -> Either (Var (ρ .- ℓ)) (Identity τ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Var r -> Either (Var (r .- l)) (Identity (r .! l))
doUncons forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ -> Either (VMap f ρ) (Identity τ) -> VMap f (Extend ℓ τ ρ)
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ -> Either (VMap f ρ) (Identity τ) -> VMap f (Extend ℓ τ ρ)
doCons
  where
    doUncons :: Label l -> Var r -> Either (Var (r .- l)) (Identity (r .! l))
doUncons Label l
l = ((r .! l) -> Identity (r .! l))
-> Either (Var (r .- l)) (r .! l)
-> Either (Var (r .- l)) (Identity (r .! l))
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (r .! l) -> Identity (r .! l)
forall a. a -> Identity a
Identity (Either (Var (r .- l)) (r .! l)
 -> Either (Var (r .- l)) (Identity (r .! l)))
-> (Var r -> Either (Var (r .- l)) (r .! l))
-> Var r
-> Either (Var (r .- l)) (Identity (r .! l))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var r -> Label l -> Either (Var (r .- l)) (r .! l))
-> Label l -> Var r -> Either (Var (r .- l)) (r .! l)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Var r -> Label l -> Either (Var (r .- l)) (r .! l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Label l
l
    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, AllUniqueLabels (Extend ℓ τ ρ))
           => Label ℓ -> Either (VMap f ρ) (Identity τ) -> VMap f (Extend ℓ τ ρ)
    doCons :: Label ℓ -> Either (VMap f ρ) (Identity τ) -> VMap f (Extend ℓ τ ρ)
doCons Label ℓ
l (Left (VMap Var (Map f ρ)
v)) = Var (Map f (Extend ℓ τ ρ)) -> VMap f (Extend ℓ τ ρ)
forall a (f :: a -> *) (ρ :: Row a). Var (Map f ρ) -> VMap f ρ
VMap (Var (Map f (Extend ℓ τ ρ)) -> VMap f (Extend ℓ τ ρ))
-> Var (Map f (Extend ℓ τ ρ)) -> VMap f (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ -> Var (Map f ρ) -> Var (Extend ℓ (f τ) (Map f ρ))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Var r -> Var (Extend l a r)
extend @(f τ) Label ℓ
l Var (Map f ρ)
v
      ((Extend ℓ (f τ) (Map f ρ) ~ Map f (Extend ℓ τ ρ)) =>
 Var (Map f (Extend ℓ τ ρ)))
-> Dict (Extend ℓ (f τ) (Map f ρ) ~ Map f (Extend ℓ τ ρ))
-> Var (Map f (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (f τ) (Map f ρ) ~ Map f (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @f @ℓ @τ @ρ
    doCons Label ℓ
l (Right (Identity τ
x)) = Var (Map f (Extend ℓ τ ρ)) -> VMap f (Extend ℓ τ ρ)
forall a (f :: a -> *) (ρ :: Row a). Var (Map f ρ) -> VMap f ρ
VMap (Var (Map f (Extend ℓ τ ρ)) -> VMap f (Extend ℓ τ ρ))
-> Var (Map f (Extend ℓ τ ρ)) -> VMap f (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ
-> (Map f (Extend ℓ τ ρ) .! ℓ) -> Var (Map f (Extend ℓ τ ρ))
forall (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Label l -> (r .! l) -> Var r
IsJust Label ℓ
l (τ -> f τ
forall a. c a => a -> f a
f τ
x)
      ((Extend ℓ (f τ) (Map f ρ) ~ Map f (Extend ℓ τ ρ)) =>
 Var (Map f (Extend ℓ τ ρ)))
-> Dict (Extend ℓ (f τ) (Map f ρ) ~ Map f (Extend ℓ τ ρ))
-> Var (Map f (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (f τ) (Map f ρ) ~ Map f (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @f @ℓ @τ @ρ
      (((Extend ℓ (f τ) (Map f ρ) .! ℓ) ~ f τ) =>
 Var (Map f (Extend ℓ τ ρ)))
-> Dict ((Extend ℓ (f τ) (Map f ρ) .! ℓ) ~ f τ)
-> Var (Map f (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict ((Extend ℓ (f τ) (Map f ρ) .! ℓ) ~ f τ)
forall k (l :: Symbol) (t :: k) (r :: Row k).
Dict ((Extend l t r .! l) ≈ t)
extendHas @ℓ @(f τ) @(Map f ρ)
      ((AllUniqueLabels (Map f (Extend ℓ τ ρ))
  ~ AllUniqueLabels (Extend ℓ τ ρ)) =>
 Var (Map f (Extend ℓ τ ρ)))
-> Dict
     (AllUniqueLabels (Map f (Extend ℓ τ ρ))
      ~ AllUniqueLabels (Extend ℓ τ ρ))
-> Var (Map f (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (AllUniqueLabels (Map f (Extend ℓ τ ρ))
   ~ AllUniqueLabels (Extend ℓ τ ρ))
forall k1 k2 (f :: k1 -> k2) (r :: Row k1).
Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
uniqueMap @f @(Extend ℓ τ ρ)

-- | A function to map over a variant given no constraint.
map' :: forall f r. FreeForall r => (forall a. a -> f a) -> Var r -> Var (Map f r)
map' :: (forall a. a -> f a) -> Var r -> Var (Map f r)
map' forall a. a -> f a
f = (forall a. Unconstrained1 a => a -> f a) -> Var r -> Var (Map f r)
forall (c :: * -> Constraint) (f :: * -> *) (r :: Row *).
Forall r c =>
(forall a. c a => a -> f a) -> Var r -> Var (Map f r)
map @Unconstrained1 forall a. a -> f a
forall a. Unconstrained1 a => a -> f a
f

-- | Lifts a natrual transformation over a variant.  In other words, it acts as a
-- variant transformer to convert a variant of @f a@ values to a variant of @g a@
-- values.  If no constraint is needed, instantiate the first type argument with
-- 'Unconstrained1'.
transform :: forall c r f g. Forall r c => (forall a. c a => f a -> g a) -> Var (Map f r) -> Var (Map g r)
transform :: (forall (a :: a). c a => f a -> g a)
-> Var (Map f r) -> Var (Map g r)
transform forall (a :: a). c a => f a -> g a
f = VMap g r -> Var (Map g r)
forall a (f :: a -> *) (ρ :: Row a). VMap f ρ -> Var (Map f ρ)
unVMap (VMap g r -> Var (Map g r))
-> (Var (Map f r) -> VMap g r) -> Var (Map f r) -> Var (Map g r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy f, Proxy Either)
-> (VMap f Empty -> VMap g Empty)
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> VMap f ρ -> Either (VMap f (ρ .- ℓ)) (f τ))
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> Either (VMap g ρ) (f τ) -> VMap g (Extend ℓ τ ρ))
-> VMap f r
-> VMap g r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @c @Either @(VMap f) @(VMap g) @f Proxy (Proxy f, Proxy Either)
forall k (t :: k). Proxy t
Proxy VMap f Empty -> VMap g Empty
forall c. VMap f Empty -> c
doNil forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> VMap f ρ -> Either (VMap f (ρ .- ℓ)) (f τ)
doUncons forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ, AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ -> Either (VMap g ρ) (f τ) -> VMap g (Extend ℓ τ ρ)
forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ -> Either (VMap g ρ) (f τ) -> VMap g (Extend ℓ τ ρ)
doCons (VMap f r -> VMap g r)
-> (Var (Map f r) -> VMap f r) -> Var (Map f r) -> VMap g r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var (Map f r) -> VMap f r
forall a (f :: a -> *) (ρ :: Row a). Var (Map f ρ) -> VMap f ρ
VMap
  where
    doNil :: VMap f Empty -> c
doNil = Var Empty -> c
forall a. Var Empty -> a
impossible (Var Empty -> c)
-> (VMap f Empty -> Var Empty) -> VMap f Empty -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VMap f Empty -> Var Empty
forall a (f :: a -> *) (ρ :: Row a). VMap f ρ -> Var (Map f ρ)
unVMap
    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, HasType ℓ τ ρ)
             => Label ℓ -> VMap f ρ -> Either (VMap f (ρ .- ℓ)) (f τ)
    doUncons :: Label ℓ -> VMap f ρ -> Either (VMap f (ρ .- ℓ)) (f τ)
doUncons Label ℓ
l = (Var (Map f (ρ .- ℓ)) -> VMap f (ρ .- ℓ))
-> Either (Var (Map f (ρ .- ℓ))) (f τ)
-> Either (VMap f (ρ .- ℓ)) (f τ)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Var (Map f (ρ .- ℓ)) -> VMap f (ρ .- ℓ)
forall a (f :: a -> *) (ρ :: Row a). Var (Map f ρ) -> VMap f ρ
VMap (Either (Var (Map f (ρ .- ℓ))) (f τ)
 -> Either (VMap f (ρ .- ℓ)) (f τ))
-> (VMap f ρ -> Either (Var (Map f (ρ .- ℓ))) (f τ))
-> VMap f ρ
-> Either (VMap f (ρ .- ℓ)) (f τ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var (Map f ρ) -> Label ℓ -> Either (Var (Map f (ρ .- ℓ))) (f τ))
-> Label ℓ -> Var (Map f ρ) -> Either (Var (Map f (ρ .- ℓ))) (f τ)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Var (Map f ρ) -> Label ℓ -> Either (Var (Map f (ρ .- ℓ))) (f τ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Label ℓ
l (Var (Map f ρ) -> Either (Var (Map f (ρ .- ℓ))) (f τ))
-> (VMap f ρ -> Var (Map f ρ))
-> VMap f ρ
-> Either (Var (Map f (ρ .- ℓ))) (f τ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VMap f ρ -> Var (Map f ρ)
forall a (f :: a -> *) (ρ :: Row a). VMap f ρ -> Var (Map f ρ)
unVMap
      (((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ)) =>
 VMap f ρ -> Either (VMap f (ρ .- ℓ)) (f τ))
-> ((τ ≈ τ)
    :- ((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ)))
-> VMap f ρ
-> Either (VMap f (ρ .- ℓ)) (f τ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((ρ .! ℓ) ≈ τ)
:- ((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ))
forall k b (f :: k -> b) (l :: Symbol) (t :: k) (r :: Row k).
((r .! l) ≈ t)
:- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
mapHas @f @ℓ @τ @ρ
    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, AllUniqueLabels (Extend ℓ τ ρ))
           => Label ℓ -> Either (VMap g ρ) (f τ) -> VMap g (Extend ℓ τ ρ)
    doCons :: Label ℓ -> Either (VMap g ρ) (f τ) -> VMap g (Extend ℓ τ ρ)
doCons Label ℓ
l (Left (VMap Var (Map g ρ)
v)) = Var (Map g (Extend ℓ τ ρ)) -> VMap g (Extend ℓ τ ρ)
forall a (f :: a -> *) (ρ :: Row a). Var (Map f ρ) -> VMap f ρ
VMap (Var (Map g (Extend ℓ τ ρ)) -> VMap g (Extend ℓ τ ρ))
-> Var (Map g (Extend ℓ τ ρ)) -> VMap g (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ -> Var (Map g ρ) -> Var (Extend ℓ (g τ) (Map g ρ))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Var r -> Var (Extend l a r)
extend @(g τ) Label ℓ
l Var (Map g ρ)
v
      ((Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ)) =>
 Var (Map g (Extend ℓ τ ρ)))
-> Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
-> Var (Map g (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @g @ℓ @τ @ρ
    doCons Label ℓ
l (Right f τ
x) = Var (Map g (Extend ℓ τ ρ)) -> VMap g (Extend ℓ τ ρ)
forall a (f :: a -> *) (ρ :: Row a). Var (Map f ρ) -> VMap f ρ
VMap (Var (Map g (Extend ℓ τ ρ)) -> VMap g (Extend ℓ τ ρ))
-> Var (Map g (Extend ℓ τ ρ)) -> VMap g (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ
-> (Map g (Extend ℓ τ ρ) .! ℓ) -> Var (Map g (Extend ℓ τ ρ))
forall (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Label l -> (r .! l) -> Var r
IsJust Label ℓ
l (f τ -> g τ
forall (a :: a). c a => f a -> g a
f f τ
x)
      ((Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ)) =>
 Var (Map g (Extend ℓ τ ρ)))
-> Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
-> Var (Map g (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @g @ℓ @τ @ρ
      (((Extend ℓ (g τ) (Map g ρ) .! ℓ) ~ g τ) =>
 Var (Map g (Extend ℓ τ ρ)))
-> Dict ((Extend ℓ (g τ) (Map g ρ) .! ℓ) ~ g τ)
-> Var (Map g (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict ((Extend ℓ (g τ) (Map g ρ) .! ℓ) ~ g τ)
forall k (l :: Symbol) (t :: k) (r :: Row k).
Dict ((Extend l t r .! l) ≈ t)
extendHas @ℓ @(g τ) @(Map g ρ)
      ((AllUniqueLabels (Map g (Extend ℓ τ ρ))
  ~ AllUniqueLabels (Extend ℓ τ ρ)) =>
 Var (Map g (Extend ℓ τ ρ)))
-> Dict
     (AllUniqueLabels (Map g (Extend ℓ τ ρ))
      ~ AllUniqueLabels (Extend ℓ τ ρ))
-> Var (Map g (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (AllUniqueLabels (Map g (Extend ℓ τ ρ))
   ~ AllUniqueLabels (Extend ℓ τ ρ))
forall k1 k2 (f :: k1 -> k2) (r :: Row k1).
Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
uniqueMap @g @(Extend ℓ τ ρ)

-- | A form of @transformC@ that doesn't have a constraint on @a@
transform' :: forall r f g . FreeForall r => (forall a. f a -> g a) -> Var (Map f r) -> Var (Map g r)
transform' :: (forall (a :: a). f a -> g a) -> Var (Map f r) -> Var (Map g r)
transform' forall (a :: a). f a -> g a
f = (forall (a :: a). Unconstrained1 a => f a -> g a)
-> Var (Map f r) -> Var (Map g r)
forall a (c :: a -> Constraint) (r :: Row a) (f :: a -> *)
       (g :: a -> *).
Forall r c =>
(forall (a :: a). c a => f a -> g a)
-> Var (Map f r) -> Var (Map g r)
transform @Unconstrained1 @r forall (a :: a). f a -> g a
forall (a :: a). Unconstrained1 a => f a -> g a
f

-- | Traverse a function over a variant.
traverse :: forall c f r. (Forall r c, Functor f) => (forall a. c a => a -> f a) -> Var r -> f (Var r)
traverse :: (forall a. c a => a -> f a) -> Var r -> f (Var r)
traverse forall a. c a => a -> f a
f = (Forall r c, Functor f) => Var (Map f r) -> f (Var r)
forall (f :: * -> *) (r :: Row *) (c :: * -> Constraint).
(Forall r c, Functor f) =>
Var (Map f r) -> f (Var r)
sequence' @f @r @c (Var (Map f r) -> f (Var r))
-> (Var r -> Var (Map f r)) -> Var r -> f (Var r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. c a => a -> f a) -> Var r -> Var (Map f r)
forall (c :: * -> Constraint) (f :: * -> *) (r :: Row *).
Forall r c =>
(forall a. c a => a -> f a) -> Var r -> Var (Map f r)
map @c @f @r forall a. c a => a -> f a
f

-- | Traverse a function over a Mapped variant.
traverseMap :: forall c f g h r.
  (Forall r c, Functor f) => (forall a. c a => g a -> f (h a)) -> Var (Map g r) -> f (Var (Map h r))
traverseMap :: (forall (a :: a). c a => g a -> f (h a))
-> Var (Map g r) -> f (Var (Map h r))
traverseMap forall (a :: a). c a => g a -> f (h a)
f =
  (Forall (Map h r) (IsA c h), Functor f) =>
Var (Map f (Map h r)) -> f (Var (Map h r))
forall (f :: * -> *) (r :: Row *) (c :: * -> Constraint).
(Forall r c, Functor f) =>
Var (Map f r) -> f (Var r)
sequence' @f @(Map h r) @(IsA c h) (Var (Map f (Map h r)) -> f (Var (Map h r)))
-> (Var (Map g r) -> Var (Map f (Map h r)))
-> Var (Map g r)
-> f (Var (Map h r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  Forall r c => Var (Map (Compose f h) r) -> Var (Map f (Map h r))
forall a b (c :: a -> Constraint) (f :: b -> *) (g :: a -> b)
       (r :: Row a).
Forall r c =>
Var (Map (Compose f g) r) -> Var (Map f (Map g r))
uncompose' @c @f @h @r (Var (Map (Compose f h) r) -> Var (Map f (Map h r)))
-> (Var (Map g r) -> Var (Map (Compose f h) r))
-> Var (Map g r)
-> Var (Map f (Map h r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (forall (a :: a). c a => g a -> Compose f h a)
-> Var (Map g r) -> Var (Map (Compose f h) r)
forall a (c :: a -> Constraint) (r :: Row a) (f :: a -> *)
       (g :: a -> *).
Forall r c =>
(forall (a :: a). c a => f a -> g a)
-> Var (Map f r) -> Var (Map g r)
transform @c @r @g @(Compose f h) (f (h a) -> Compose f h a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (h a) -> Compose f h a)
-> (g a -> f (h a)) -> g a -> Compose f h a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. g a -> f (h a)
forall (a :: a). c a => g a -> f (h a)
f)
  (Forall (Map h r) (IsA c h) => Var (Map g r) -> f (Var (Map h r)))
-> (Forall r c :- Forall (Map h r) (IsA c h))
-> Var (Map g r)
-> f (Var (Map h r))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Forall r c :- Forall (Map h r) (IsA c h)
forall k1 k2 (f :: k1 -> k2) (ρ :: Row k1) (c :: k1 -> Constraint).
Forall ρ c :- Forall (Map f ρ) (IsA c f)
mapForall @h @r @c

-- | Applicative sequencing over a variant with arbitrary constraint.
sequence' :: forall f r c. (Forall r c, Functor f) => Var (Map f r) -> f (Var r)
sequence' :: Var (Map f r) -> f (Var r)
sequence' = Compose f Var r -> f (Var r)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose f Var r -> f (Var r))
-> (Var (Map f r) -> Compose f Var r) -> Var (Map f r) -> f (Var r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy f, Proxy Either)
-> (VMap f Empty -> Compose f Var Empty)
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> VMap f ρ -> Either (VMap f (ρ .- ℓ)) (f τ))
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> Either (Compose f Var ρ) (f τ) -> Compose f Var (Extend ℓ τ ρ))
-> VMap f r
-> Compose f Var r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @c @Either @(VMap f) @(Compose f Var) @f Proxy (Proxy f, Proxy Either)
forall k (t :: k). Proxy t
Proxy VMap f Empty -> Compose f Var Empty
forall c. VMap f Empty -> c
doNil forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> VMap f ρ -> Either (VMap f (ρ .- ℓ)) (f τ)
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, HasType ℓ τ ρ) =>
Label ℓ -> VMap f ρ -> Either (VMap f (ρ .- ℓ)) (f τ)
doUncons forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Either (Compose f Var ρ) (f τ) -> Compose f Var (Extend ℓ τ ρ)
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Either (Compose f Var ρ) (f τ) -> Compose f Var (Extend ℓ τ ρ)
doCons (VMap f r -> Compose f Var r)
-> (Var (Map f r) -> VMap f r) -> Var (Map f r) -> Compose f Var r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var (Map f r) -> VMap f r
forall a (f :: a -> *) (ρ :: Row a). Var (Map f ρ) -> VMap f ρ
VMap
  where
    doNil :: VMap f Empty -> c
doNil = Var Empty -> c
forall a. Var Empty -> a
impossible (Var Empty -> c)
-> (VMap f Empty -> Var Empty) -> VMap f Empty -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VMap f Empty -> Var Empty
forall a (f :: a -> *) (ρ :: Row a). VMap f ρ -> Var (Map f ρ)
unVMap
    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, HasType ℓ τ ρ)
             => Label ℓ -> VMap f ρ -> Either (VMap f (ρ .- ℓ)) (f τ)
    doUncons :: Label ℓ -> VMap f ρ -> Either (VMap f (ρ .- ℓ)) (f τ)
doUncons Label ℓ
l = (Var (Map f (ρ .- ℓ)) -> VMap f (ρ .- ℓ))
-> Either (Var (Map f (ρ .- ℓ))) (f τ)
-> Either (VMap f (ρ .- ℓ)) (f τ)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Var (Map f (ρ .- ℓ)) -> VMap f (ρ .- ℓ)
forall a (f :: a -> *) (ρ :: Row a). Var (Map f ρ) -> VMap f ρ
VMap (Either (Var (Map f (ρ .- ℓ))) (f τ)
 -> Either (VMap f (ρ .- ℓ)) (f τ))
-> (VMap f ρ -> Either (Var (Map f (ρ .- ℓ))) (f τ))
-> VMap f ρ
-> Either (VMap f (ρ .- ℓ)) (f τ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var (Map f ρ) -> Label ℓ -> Either (Var (Map f (ρ .- ℓ))) (f τ))
-> Label ℓ -> Var (Map f ρ) -> Either (Var (Map f (ρ .- ℓ))) (f τ)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Var (Map f ρ) -> Label ℓ -> Either (Var (Map f (ρ .- ℓ))) (f τ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Label ℓ
l (Var (Map f ρ) -> Either (Var (Map f (ρ .- ℓ))) (f τ))
-> (VMap f ρ -> Var (Map f ρ))
-> VMap f ρ
-> Either (Var (Map f (ρ .- ℓ))) (f τ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VMap f ρ -> Var (Map f ρ)
forall a (f :: a -> *) (ρ :: Row a). VMap f ρ -> Var (Map f ρ)
unVMap
      (((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ)) =>
 VMap f ρ -> Either (VMap f (ρ .- ℓ)) (f τ))
-> ((τ ≈ τ)
    :- ((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ)))
-> VMap f ρ
-> Either (VMap f (ρ .- ℓ)) (f τ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((ρ .! ℓ) ≈ τ)
:- ((Map f ρ .! ℓ) ≈ f τ, (Map f ρ .- ℓ) ≈ Map f (ρ .- ℓ))
forall k b (f :: k -> b) (l :: Symbol) (t :: k) (r :: Row k).
((r .! l) ≈ t)
:- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
mapHas @f @ℓ @τ @ρ
    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, AllUniqueLabels (Extend ℓ τ ρ))
           => Label ℓ -> Either (Compose f Var ρ) (f τ) -> Compose f Var (Extend ℓ τ ρ)
    doCons :: Label ℓ
-> Either (Compose f Var ρ) (f τ) -> Compose f Var (Extend ℓ τ ρ)
doCons Label ℓ
l (Left (Compose f (Var ρ)
v)) = f (Var (Extend ℓ τ ρ)) -> Compose f Var (Extend ℓ τ ρ)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (Var (Extend ℓ τ ρ)) -> Compose f Var (Extend ℓ τ ρ))
-> f (Var (Extend ℓ τ ρ)) -> Compose f Var (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ -> Var ρ -> Var (Extend ℓ τ ρ)
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Var r -> Var (Extend l a r)
extend @τ Label ℓ
l (Var ρ -> Var (Extend ℓ τ ρ))
-> f (Var ρ) -> f (Var (Extend ℓ τ ρ))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Var ρ)
v
    doCons Label ℓ
l (Right f τ
fx) = f (Var (Extend ℓ τ ρ)) -> Compose f Var (Extend ℓ τ ρ)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (Var (Extend ℓ τ ρ)) -> Compose f Var (Extend ℓ τ ρ))
-> f (Var (Extend ℓ τ ρ)) -> Compose f Var (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ -> (Extend ℓ τ ρ .! ℓ) -> Var (Extend ℓ τ ρ)
forall (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Label l -> (r .! l) -> Var r
IsJust Label ℓ
l (τ -> Var (Extend ℓ τ ρ)) -> f τ -> f (Var (Extend ℓ τ ρ))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f τ
fx
      (((Extend ℓ τ ρ .! ℓ) ~ τ) => f (Var (Extend ℓ τ ρ)))
-> Dict ((Extend ℓ τ ρ .! ℓ) ~ τ) -> f (Var (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict ((Extend ℓ τ ρ .! ℓ) ~ τ)
forall k (l :: Symbol) (t :: k) (r :: Row k).
Dict ((Extend l t r .! l) ≈ t)
extendHas @ℓ @τ @ρ


-- | Applicative sequencing over a variant
sequence :: forall f r. (FreeForall r, Functor f) => Var (Map f r) -> f (Var r)
sequence :: Var (Map f r) -> f (Var r)
sequence = (Forall r Unconstrained1, Functor f) => Var (Map f r) -> f (Var r)
forall (f :: * -> *) (r :: Row *) (c :: * -> Constraint).
(Forall r c, Functor f) =>
Var (Map f r) -> f (Var r)
sequence' @f @r @Unconstrained1

-- $compose
-- We can easily convert between mapping two functors over the types of a row
-- and mapping the composition of the two functors.  The following two functions
-- perform this composition with the gaurantee that:
--
-- >>> compose . uncompose = id
--
-- >>> uncompose . compose = id

-- | Convert from a variant where two functors have been mapped over the types to
-- one where the composition of the two functors is mapped over the types.
compose :: forall f g r . FreeForall r => Var (Map f (Map g r)) -> Var (Map (Compose f g) r)
compose :: Var (Map f (Map g r)) -> Var (Map (Compose f g) r)
compose = VMap (Compose f g) r -> Var (Map (Compose f g) r)
forall a (f :: a -> *) (ρ :: Row a). VMap f ρ -> Var (Map f ρ)
unVMap (VMap (Compose f g) r -> Var (Map (Compose f g) r))
-> (Var (Map f (Map g r)) -> VMap (Compose f g) r)
-> Var (Map f (Map g r))
-> Var (Map (Compose f g) r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy (Compose f g), Proxy Either)
-> (VMap2 f g Empty -> VMap (Compose f g) Empty)
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, Unconstrained1 τ, HasType ℓ τ ρ) =>
    Label ℓ
    -> VMap2 f g ρ -> Either (VMap2 f g (ρ .- ℓ)) (Compose f g τ))
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, Unconstrained1 τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> Either (VMap (Compose f g) ρ) (Compose f g τ)
    -> VMap (Compose f g) (Extend ℓ τ ρ))
-> VMap2 f g r
-> VMap (Compose f g) r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @Unconstrained1 @Either @(VMap2 f g) @(VMap (Compose f g)) @(Compose f g) Proxy (Proxy (Compose f g), Proxy Either)
forall k (t :: k). Proxy t
Proxy VMap2 f g Empty -> VMap (Compose f g) Empty
forall c. VMap2 f g Empty -> c
doNil forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, Unconstrained1 τ, HasType ℓ τ ρ) =>
Label ℓ
-> VMap2 f g ρ -> Either (VMap2 f g (ρ .- ℓ)) (Compose f g τ)
forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, HasType ℓ τ ρ) =>
Label ℓ
-> VMap2 f g ρ -> Either (VMap2 f g (ρ .- ℓ)) (Compose f g τ)
doUncons forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Either (VMap (Compose f g) ρ) (Compose f g τ)
-> VMap (Compose f g) (Extend ℓ τ ρ)
forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, Unconstrained1 τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Either (VMap (Compose f g) ρ) (Compose f g τ)
-> VMap (Compose f g) (Extend ℓ τ ρ)
doCons (VMap2 f g r -> VMap (Compose f g) r)
-> (Var (Map f (Map g r)) -> VMap2 f g r)
-> Var (Map f (Map g r))
-> VMap (Compose f g) r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var (Map f (Map g r)) -> VMap2 f g r
forall a a (f :: a -> *) (g :: a -> a) (ρ :: Row a).
Var (Map f (Map g ρ)) -> VMap2 f g ρ
VMap2
  where
    doNil :: VMap2 f g Empty -> c
doNil = Var Empty -> c
forall a. Var Empty -> a
impossible (Var Empty -> c)
-> (VMap2 f g Empty -> Var Empty) -> VMap2 f g Empty -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VMap2 f g Empty -> Var Empty
forall a (f :: a -> *) a (g :: a -> a) (ρ :: Row a).
VMap2 f g ρ -> Var (Map f (Map g ρ))
unVMap2
    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, HasType ℓ τ ρ)
             => Label ℓ -> VMap2 f g ρ -> Either (VMap2 f g (ρ .- ℓ)) (Compose f g τ)
    doUncons :: Label ℓ
-> VMap2 f g ρ -> Either (VMap2 f g (ρ .- ℓ)) (Compose f g τ)
doUncons Label ℓ
l = (Var (Map f (Map g (ρ .- ℓ))) -> VMap2 f g (ρ .- ℓ))
-> (f (g τ) -> Compose f g τ)
-> Either (Var (Map f (Map g (ρ .- ℓ)))) (f (g τ))
-> Either (VMap2 f g (ρ .- ℓ)) (Compose f g τ)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Var (Map f (Map g (ρ .- ℓ))) -> VMap2 f g (ρ .- ℓ)
forall a a (f :: a -> *) (g :: a -> a) (ρ :: Row a).
Var (Map f (Map g ρ)) -> VMap2 f g ρ
VMap2 f (g τ) -> Compose f g τ
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Either (Var (Map f (Map g (ρ .- ℓ)))) (f (g τ))
 -> Either (VMap2 f g (ρ .- ℓ)) (Compose f g τ))
-> (VMap2 f g ρ -> Either (Var (Map f (Map g (ρ .- ℓ)))) (f (g τ)))
-> VMap2 f g ρ
-> Either (VMap2 f g (ρ .- ℓ)) (Compose f g τ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var (Map f (Map g ρ))
 -> Label ℓ -> Either (Var (Map f (Map g (ρ .- ℓ)))) (f (g τ)))
-> Label ℓ
-> Var (Map f (Map g ρ))
-> Either (Var (Map f (Map g (ρ .- ℓ)))) (f (g τ))
forall a b c. (a -> b -> c) -> b -> a -> c
flip Var (Map f (Map g ρ))
-> Label ℓ -> Either (Var (Map f (Map g (ρ .- ℓ)))) (f (g τ))
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Label ℓ
l (Var (Map f (Map g ρ))
 -> Either (Var (Map f (Map g (ρ .- ℓ)))) (f (g τ)))
-> (VMap2 f g ρ -> Var (Map f (Map g ρ)))
-> VMap2 f g ρ
-> Either (Var (Map f (Map g (ρ .- ℓ)))) (f (g τ))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VMap2 f g ρ -> Var (Map f (Map g ρ))
forall a (f :: a -> *) a (g :: a -> a) (ρ :: Row a).
VMap2 f g ρ -> Var (Map f (Map g ρ))
unVMap2
      (((Map f (Map g ρ) .! ℓ) ≈ f (g τ),
  (Map f (Map g ρ) .- ℓ) ≈ Map f (Map g (ρ .- ℓ))) =>
 VMap2 f g ρ -> Either (VMap2 f g (ρ .- ℓ)) (Compose f g τ))
-> ((g τ ≈ g τ)
    :- ((Map f (Map g ρ) .! ℓ) ≈ f (g τ),
        (Map f (Map g ρ) .- ℓ) ≈ Map f (Map g (ρ .- ℓ))))
-> VMap2 f g ρ
-> Either (VMap2 f g (ρ .- ℓ)) (Compose f g τ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((Map g ρ .! ℓ) ≈ g τ)
:- ((Map f (Map g ρ) .! ℓ) ≈ f (g τ),
    (Map f (Map g ρ) .- ℓ) ≈ Map f (Map g ρ .- ℓ))
forall k b (f :: k -> b) (l :: Symbol) (t :: k) (r :: Row k).
((r .! l) ≈ t)
:- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
mapHas @f @ℓ @(g τ) @(Map g ρ)
      (((Map g ρ .! ℓ) ≈ g τ, (Map g ρ .- ℓ) ≈ Map g (ρ .- ℓ)) =>
 VMap2 f g ρ -> Either (VMap2 f g (ρ .- ℓ)) (Compose f g τ))
-> ((τ ≈ τ)
    :- ((Map g ρ .! ℓ) ≈ g τ, (Map g ρ .- ℓ) ≈ Map g (ρ .- ℓ)))
-> VMap2 f g ρ
-> Either (VMap2 f g (ρ .- ℓ)) (Compose f g τ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((ρ .! ℓ) ≈ τ)
:- ((Map g ρ .! ℓ) ≈ g τ, (Map g ρ .- ℓ) ≈ Map g (ρ .- ℓ))
forall k b (f :: k -> b) (l :: Symbol) (t :: k) (r :: Row k).
((r .! l) ≈ t)
:- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
mapHas @g @ℓ @τ @ρ
    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, AllUniqueLabels (Extend ℓ τ ρ))
           => Label ℓ -> Either (VMap (Compose f g) ρ) (Compose f g τ) -> VMap (Compose f g) (Extend ℓ τ ρ)
    doCons :: Label ℓ
-> Either (VMap (Compose f g) ρ) (Compose f g τ)
-> VMap (Compose f g) (Extend ℓ τ ρ)
doCons Label ℓ
l (Left (VMap Var (Map (Compose f g) ρ)
v)) = Var (Map (Compose f g) (Extend ℓ τ ρ))
-> VMap (Compose f g) (Extend ℓ τ ρ)
forall a (f :: a -> *) (ρ :: Row a). Var (Map f ρ) -> VMap f ρ
VMap (Var (Map (Compose f g) (Extend ℓ τ ρ))
 -> VMap (Compose f g) (Extend ℓ τ ρ))
-> Var (Map (Compose f g) (Extend ℓ τ ρ))
-> VMap (Compose f g) (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ
-> Var (Map (Compose f g) ρ)
-> Var (Extend ℓ (Compose f g τ) (Map (Compose f g) ρ))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Var r -> Var (Extend l a r)
extend @(Compose f g τ) Label ℓ
l Var (Map (Compose f g) ρ)
v
      ((Extend ℓ (Compose f g τ) (Map (Compose f g) ρ)
  ~ Map (Compose f g) (Extend ℓ τ ρ)) =>
 Var (Map (Compose f g) (Extend ℓ τ ρ)))
-> Dict
     (Extend ℓ (Compose f g τ) (Map (Compose f g) ρ)
      ~ Map (Compose f g) (Extend ℓ τ ρ))
-> Var (Map (Compose f g) (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (Extend ℓ (Compose f g τ) (Map (Compose f g) ρ)
   ~ Map (Compose f g) (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @(Compose f g) @ℓ @τ @ρ
    doCons Label ℓ
l (Right Compose f g τ
x) = Var (Map (Compose f g) (Extend ℓ τ ρ))
-> VMap (Compose f g) (Extend ℓ τ ρ)
forall a (f :: a -> *) (ρ :: Row a). Var (Map f ρ) -> VMap f ρ
VMap (Var (Map (Compose f g) (Extend ℓ τ ρ))
 -> VMap (Compose f g) (Extend ℓ τ ρ))
-> Var (Map (Compose f g) (Extend ℓ τ ρ))
-> VMap (Compose f g) (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ
-> (Map (Compose f g) (Extend ℓ τ ρ) .! ℓ)
-> Var (Map (Compose f g) (Extend ℓ τ ρ))
forall (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Label l -> (r .! l) -> Var r
IsJust Label ℓ
l Compose f g τ
Map (Compose f g) (Extend ℓ τ ρ) .! ℓ
x
      ((Extend ℓ (Compose f g τ) (Map (Compose f g) ρ)
  ~ Map (Compose f g) (Extend ℓ τ ρ)) =>
 Var (Map (Compose f g) (Extend ℓ τ ρ)))
-> Dict
     (Extend ℓ (Compose f g τ) (Map (Compose f g) ρ)
      ~ Map (Compose f g) (Extend ℓ τ ρ))
-> Var (Map (Compose f g) (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (Extend ℓ (Compose f g τ) (Map (Compose f g) ρ)
   ~ Map (Compose f g) (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @(Compose f g) @ℓ @τ @ρ
      (((Extend ℓ (Compose f g τ) (Map (Compose f g) ρ) .! ℓ)
  ~ Compose f g τ) =>
 Var (Map (Compose f g) (Extend ℓ τ ρ)))
-> Dict
     ((Extend ℓ (Compose f g τ) (Map (Compose f g) ρ) .! ℓ)
      ~ Compose f g τ)
-> Var (Map (Compose f g) (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  ((Extend ℓ (Compose f g τ) (Map (Compose f g) ρ) .! ℓ)
   ~ Compose f g τ)
forall k (l :: Symbol) (t :: k) (r :: Row k).
Dict ((Extend l t r .! l) ≈ t)
extendHas @ℓ @((Compose f g) τ) @(Map (Compose f g) ρ)
      ((AllUniqueLabels (Map (Compose f g) (Extend ℓ τ ρ))
  ~ AllUniqueLabels (Extend ℓ τ ρ)) =>
 Var (Map (Compose f g) (Extend ℓ τ ρ)))
-> Dict
     (AllUniqueLabels (Map (Compose f g) (Extend ℓ τ ρ))
      ~ AllUniqueLabels (Extend ℓ τ ρ))
-> Var (Map (Compose f g) (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (AllUniqueLabels (Map (Compose f g) (Extend ℓ τ ρ))
   ~ AllUniqueLabels (Extend ℓ τ ρ))
forall k1 k2 (f :: k1 -> k2) (r :: Row k1).
Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
uniqueMap @(Compose f g) @(Extend ℓ τ ρ)

-- | A version of 'uncompose' that allows an arbitrary constraint.
uncompose' :: forall c f g r . Forall r c => Var (Map (Compose f g) r) -> Var (Map f (Map g r))
uncompose' :: Var (Map (Compose f g) r) -> Var (Map f (Map g r))
uncompose' = VMap2 f g r -> Var (Map f (Map g r))
forall a (f :: a -> *) a (g :: a -> a) (ρ :: Row a).
VMap2 f g ρ -> Var (Map f (Map g ρ))
unVMap2 (VMap2 f g r -> Var (Map f (Map g r)))
-> (Var (Map (Compose f g) r) -> VMap2 f g r)
-> Var (Map (Compose f g) r)
-> Var (Map f (Map g r))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy (Compose f g), Proxy Either)
-> (VMap (Compose f g) Empty -> VMap2 f g Empty)
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ
    -> VMap (Compose f g) ρ
    -> Either (VMap (Compose f g) (ρ .- ℓ)) (Compose f g τ))
-> (forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> Either (VMap2 f g ρ) (Compose f g τ)
    -> VMap2 f g (Extend ℓ τ ρ))
-> VMap (Compose f g) r
-> VMap2 f g r
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @r @c @Either @(VMap (Compose f g)) @(VMap2 f g) @(Compose f g) Proxy (Proxy (Compose f g), Proxy Either)
forall k (t :: k). Proxy t
Proxy VMap (Compose f g) Empty -> VMap2 f g Empty
forall c. VMap (Compose f g) Empty -> c
doNil forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ
-> VMap (Compose f g) ρ
-> Either (VMap (Compose f g) (ρ .- ℓ)) (Compose f g τ)
forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, HasType ℓ τ ρ) =>
Label ℓ
-> VMap (Compose f g) ρ
-> Either (VMap (Compose f g) (ρ .- ℓ)) (Compose f g τ)
doUncons forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Either (VMap2 f g ρ) (Compose f g τ) -> VMap2 f g (Extend ℓ τ ρ)
forall (ℓ :: Symbol) (τ :: a) (ρ :: Row a).
(KnownSymbol ℓ, AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Either (VMap2 f g ρ) (Compose f g τ) -> VMap2 f g (Extend ℓ τ ρ)
doCons (VMap (Compose f g) r -> VMap2 f g r)
-> (Var (Map (Compose f g) r) -> VMap (Compose f g) r)
-> Var (Map (Compose f g) r)
-> VMap2 f g r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var (Map (Compose f g) r) -> VMap (Compose f g) r
forall a (f :: a -> *) (ρ :: Row a). Var (Map f ρ) -> VMap f ρ
VMap
  where
    doNil :: VMap (Compose f g) Empty -> c
doNil = Var Empty -> c
forall a. Var Empty -> a
impossible (Var Empty -> c)
-> (VMap (Compose f g) Empty -> Var Empty)
-> VMap (Compose f g) Empty
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VMap (Compose f g) Empty -> Var Empty
forall a (f :: a -> *) (ρ :: Row a). VMap f ρ -> Var (Map f ρ)
unVMap
    doUncons :: forall ℓ τ ρ. (KnownSymbol ℓ, HasType ℓ τ ρ)
             => Label ℓ -> VMap (Compose f g) ρ -> Either (VMap (Compose f g) (ρ .- ℓ)) (Compose f g τ)
    doUncons :: Label ℓ
-> VMap (Compose f g) ρ
-> Either (VMap (Compose f g) (ρ .- ℓ)) (Compose f g τ)
doUncons Label ℓ
l = (Var (Map (Compose f g) (ρ .- ℓ)) -> VMap (Compose f g) (ρ .- ℓ))
-> Either (Var (Map (Compose f g) (ρ .- ℓ))) (Compose f g τ)
-> Either (VMap (Compose f g) (ρ .- ℓ)) (Compose f g τ)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Var (Map (Compose f g) (ρ .- ℓ)) -> VMap (Compose f g) (ρ .- ℓ)
forall a (f :: a -> *) (ρ :: Row a). Var (Map f ρ) -> VMap f ρ
VMap (Either (Var (Map (Compose f g) (ρ .- ℓ))) (Compose f g τ)
 -> Either (VMap (Compose f g) (ρ .- ℓ)) (Compose f g τ))
-> (VMap (Compose f g) ρ
    -> Either (Var (Map (Compose f g) (ρ .- ℓ))) (Compose f g τ))
-> VMap (Compose f g) ρ
-> Either (VMap (Compose f g) (ρ .- ℓ)) (Compose f g τ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var (Map (Compose f g) ρ)
 -> Label ℓ
 -> Either (Var (Map (Compose f g) (ρ .- ℓ))) (Compose f g τ))
-> Label ℓ
-> Var (Map (Compose f g) ρ)
-> Either (Var (Map (Compose f g) (ρ .- ℓ))) (Compose f g τ)
forall a b c. (a -> b -> c) -> b -> a -> c
flip Var (Map (Compose f g) ρ)
-> Label ℓ
-> Either (Var (Map (Compose f g) (ρ .- ℓ))) (Compose f g τ)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Label ℓ
l (Var (Map (Compose f g) ρ)
 -> Either (Var (Map (Compose f g) (ρ .- ℓ))) (Compose f g τ))
-> (VMap (Compose f g) ρ -> Var (Map (Compose f g) ρ))
-> VMap (Compose f g) ρ
-> Either (Var (Map (Compose f g) (ρ .- ℓ))) (Compose f g τ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VMap (Compose f g) ρ -> Var (Map (Compose f g) ρ)
forall a (f :: a -> *) (ρ :: Row a). VMap f ρ -> Var (Map f ρ)
unVMap
      (((Map (Compose f g) ρ .! ℓ) ≈ Compose f g τ,
  (Map (Compose f g) ρ .- ℓ) ≈ Map (Compose f g) (ρ .- ℓ)) =>
 VMap (Compose f g) ρ
 -> Either (VMap (Compose f g) (ρ .- ℓ)) (Compose f g τ))
-> ((τ ≈ τ)
    :- ((Map (Compose f g) ρ .! ℓ) ≈ Compose f g τ,
        (Map (Compose f g) ρ .- ℓ) ≈ Map (Compose f g) (ρ .- ℓ)))
-> VMap (Compose f g) ρ
-> Either (VMap (Compose f g) (ρ .- ℓ)) (Compose f g τ)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((ρ .! ℓ) ≈ τ)
:- ((Map (Compose f g) ρ .! ℓ) ≈ Compose f g τ,
    (Map (Compose f g) ρ .- ℓ) ≈ Map (Compose f g) (ρ .- ℓ))
forall k b (f :: k -> b) (l :: Symbol) (t :: k) (r :: Row k).
((r .! l) ≈ t)
:- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
mapHas @(Compose f g) @ℓ @τ @ρ
    doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, AllUniqueLabels (Extend ℓ τ ρ))
           => Label ℓ -> Either (VMap2 f g ρ) (Compose f g τ) -> VMap2 f g (Extend ℓ τ ρ)
    doCons :: Label ℓ
-> Either (VMap2 f g ρ) (Compose f g τ) -> VMap2 f g (Extend ℓ τ ρ)
doCons Label ℓ
l (Left (VMap2 Var (Map f (Map g ρ))
v)) = Var (Map f (Map g (Extend ℓ τ ρ))) -> VMap2 f g (Extend ℓ τ ρ)
forall a a (f :: a -> *) (g :: a -> a) (ρ :: Row a).
Var (Map f (Map g ρ)) -> VMap2 f g ρ
VMap2 (Var (Map f (Map g (Extend ℓ τ ρ))) -> VMap2 f g (Extend ℓ τ ρ))
-> Var (Map f (Map g (Extend ℓ τ ρ))) -> VMap2 f g (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ
-> Var (Map f (Map g ρ))
-> Var (Extend ℓ (f (g τ)) (Map f (Map g ρ)))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Var r -> Var (Extend l a r)
extend @(f (g τ)) Label ℓ
l Var (Map f (Map g ρ))
v
      ((Extend ℓ (f (g τ)) (Map f (Map g ρ))
  ~ Map f (Map g (Extend ℓ τ ρ))) =>
 Var (Map f (Map g (Extend ℓ τ ρ))))
-> Dict
     (Extend ℓ (f (g τ)) (Map f (Map g ρ))
      ~ Map f (Map g (Extend ℓ τ ρ)))
-> Var (Map f (Map g (Extend ℓ τ ρ)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (Extend ℓ (f (g τ)) (Map f (Map g ρ))
   ≈ Map f (Extend ℓ (g τ) (Map g ρ)))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @f @ℓ @(g τ) @(Map g ρ)
      ((Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ)) =>
 Var (Map f (Map g (Extend ℓ τ ρ))))
-> Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
-> Var (Map f (Map g (Extend ℓ τ ρ)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @g @ℓ @τ @ρ
    doCons Label ℓ
l (Right (Compose f (g τ)
x)) = Var (Map f (Map g (Extend ℓ τ ρ))) -> VMap2 f g (Extend ℓ τ ρ)
forall a a (f :: a -> *) (g :: a -> a) (ρ :: Row a).
Var (Map f (Map g ρ)) -> VMap2 f g ρ
VMap2 (Var (Map f (Map g (Extend ℓ τ ρ))) -> VMap2 f g (Extend ℓ τ ρ))
-> Var (Map f (Map g (Extend ℓ τ ρ))) -> VMap2 f g (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ
-> (Map f (Extend ℓ (g τ) (Map g ρ)) .! ℓ)
-> Var (Map f (Extend ℓ (g τ) (Map g ρ)))
forall (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Label l -> (r .! l) -> Var r
IsJust Label ℓ
l f (g τ)
Map f (Extend ℓ (g τ) (Map g ρ)) .! ℓ
x
      ((Extend ℓ (f (g τ)) (Map f (Map g ρ))
  ≈ Map f (Extend ℓ (g τ) (Map g ρ))) =>
 Var (Map f (Map g (Extend ℓ τ ρ))))
-> Dict
     (Extend ℓ (f (g τ)) (Map f (Map g ρ))
      ≈ Map f (Extend ℓ (g τ) (Map g ρ)))
-> Var (Map f (Map g (Extend ℓ τ ρ)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (Extend ℓ (f (g τ)) (Map f (Map g ρ))
   ≈ Map f (Extend ℓ (g τ) (Map g ρ)))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @f @ℓ @(g τ) @(Map g ρ)
      ((Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ)) =>
 Var (Map f (Map g (Extend ℓ τ ρ))))
-> Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
-> Var (Map f (Map g (Extend ℓ τ ρ)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (g τ) (Map g ρ) ~ Map g (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @g @ℓ @τ @ρ
      (((Extend ℓ (f (g τ)) (Map f (Map g ρ)) .! ℓ) ~ f (g τ)) =>
 Var (Map f (Map g (Extend ℓ τ ρ))))
-> Dict ((Extend ℓ (f (g τ)) (Map f (Map g ρ)) .! ℓ) ~ f (g τ))
-> Var (Map f (Map g (Extend ℓ τ ρ)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict ((Extend ℓ (f (g τ)) (Map f (Map g ρ)) .! ℓ) ~ f (g τ))
forall k (l :: Symbol) (t :: k) (r :: Row k).
Dict ((Extend l t r .! l) ≈ t)
extendHas @ℓ @(f (g τ)) @(Map f (Map g ρ))
      ((AllUniqueLabels (Map f (Extend ℓ (g τ) (Map g ρ)))
  ~ AllUniqueLabels (Extend ℓ (g τ) (Map g ρ))) =>
 Var (Map f (Map g (Extend ℓ τ ρ))))
-> Dict
     (AllUniqueLabels (Map f (Extend ℓ (g τ) (Map g ρ)))
      ~ AllUniqueLabels (Extend ℓ (g τ) (Map g ρ)))
-> Var (Map f (Map g (Extend ℓ τ ρ)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (AllUniqueLabels (Map f (Extend ℓ (g τ) (Map g ρ)))
   ~ AllUniqueLabels (Extend ℓ (g τ) (Map g ρ)))
forall k1 k2 (f :: k1 -> k2) (r :: Row k1).
Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
uniqueMap @f @(Extend ℓ (g τ) (Map g ρ))
      ((AllUniqueLabels (Map g (Extend ℓ τ ρ))
  ~ AllUniqueLabels (Extend ℓ τ ρ)) =>
 Var (Map f (Map g (Extend ℓ τ ρ))))
-> Dict
     (AllUniqueLabels (Map g (Extend ℓ τ ρ))
      ~ AllUniqueLabels (Extend ℓ τ ρ))
-> Var (Map f (Map g (Extend ℓ τ ρ)))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (AllUniqueLabels (Map g (Extend ℓ τ ρ))
   ~ AllUniqueLabels (Extend ℓ τ ρ))
forall k1 k2 (f :: k1 -> k2) (r :: Row k1).
Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
uniqueMap @g @(Extend ℓ τ ρ)

-- | Convert from a variant where the composition of two functors have been mapped
-- over the types to one where the two functors are mapped individually one at a
-- time over the types.
uncompose :: forall f g r . FreeForall r => Var (Map (Compose f g) r) -> Var (Map f (Map g r))
uncompose :: Var (Map (Compose f g) r) -> Var (Map f (Map g r))
uncompose = Forall r Unconstrained1 =>
Var (Map (Compose f g) r) -> Var (Map f (Map g r))
forall a b (c :: a -> Constraint) (f :: b -> *) (g :: a -> b)
       (r :: Row a).
Forall r c =>
Var (Map (Compose f g) r) -> Var (Map f (Map g r))
uncompose' @Unconstrained1 @f @g @r

-- | Coerce a variant to a coercible representation.  The 'BiForall' in the context
-- indicates that the type of any option in @r1@ can be coerced to the type of
-- the corresponding option in @r2@.
--
-- Internally, this is implemented just with `unsafeCoerce`, but we provide the
-- following implementation as a proof:
--
-- > newtype ConstV a b = ConstV { unConstV :: Var a }
-- > newtype ConstV a b = FlipConstV { unFlipConstV :: Var b }
-- > coerceVar :: forall r1 r2. BiForall r1 r2 Coercible => Var r1 -> Var r2
-- > coerceVar = unFlipConstV . biMetamorph @_ @_ @r1 @r2 @Coercible @Either @ConstV @FlipConstV @Const Proxy doNil doUncons doCons . ConstV
-- >   where
-- >     doNil = impossible . unConstV
-- >     doUncons l = bimap ConstV Const . flip trial l . unConstV
-- >     doCons :: forall ℓ τ1 τ2 ρ1 ρ2. (KnownSymbol ℓ, Coercible τ1 τ2, AllUniqueLabels (Extend ℓ τ2 ρ2))
-- >            => Label ℓ -> Either (FlipConstV ρ1 ρ2) (Const τ1 τ2)
-- >            -> FlipConstV (Extend ℓ τ1 ρ1) (Extend ℓ τ2 ρ2)
-- >     doCons l (Left (FlipConstV v)) = FlipConstV $ extend @τ2 l v
-- >     doCons l (Right (Const x)) = FlipConstV $ IsJust l (coerce @τ1 @τ2 x)
-- >       \\ extendHas @ρ2 @ℓ @τ2
coerceVar :: forall r1 r2. BiForall r1 r2 Coercible => Var r1 -> Var r2
coerceVar :: Var r1 -> Var r2
coerceVar = Var r1 -> Var r2
forall a b. a -> b
unsafeCoerce

{--------------------------------------------------------------------
  Variant initialization
--------------------------------------------------------------------}

-- | Initialize a variant from a producer function that accepts labels.  If this
-- function returns more than one possibility, then one is chosen arbitrarily to
-- be the value in the variant.
fromLabels :: forall c ρ f. (Alternative f, Forall ρ c, AllUniqueLabels ρ)
           => (forall l a. (KnownSymbol l, c a) => Label l -> f a) -> f (Var ρ)
fromLabels :: (forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a)
-> f (Var ρ)
fromLabels forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a
mk = Compose f Var ρ -> f (Var ρ)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose f Var ρ -> f (Var ρ)) -> Compose f Var ρ -> f (Var ρ)
forall a b. (a -> b) -> a -> b
$ Proxy (Proxy Proxy, Proxy Const)
-> (Const () Empty -> Compose f Var Empty)
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> Const () ρ -> Const (Const () (ρ .- ℓ)) (Proxy τ))
-> (forall (ℓ :: Symbol) τ (ρ :: Row *).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> Const (Compose f Var ρ) (Proxy τ)
    -> Compose f Var (Extend ℓ τ ρ))
-> Const () ρ
-> Compose f Var ρ
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @ρ @c @Const @(Const ()) @(Compose f Var) @Proxy
                                        Proxy (Proxy Proxy, Proxy Const)
forall k (t :: k). Proxy t
Proxy Const () Empty -> Compose f Var Empty
forall k1 (f :: * -> *) p (g :: k1 -> *) (a :: k1).
Alternative f =>
p -> Compose f g a
doNil forall k k p p (b :: k) (b :: k). p -> p -> Const (Const () b) b
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> Const () ρ -> Const (Const () (ρ .- ℓ)) (Proxy τ)
doUncons forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Const (Compose f Var ρ) (Proxy τ)
-> Compose f Var (Extend ℓ τ ρ)
forall (ℓ :: Symbol) τ (ρ :: Row *).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Const (Compose f Var ρ) (Proxy τ)
-> Compose f Var (Extend ℓ τ ρ)
doCons (() -> Const () ρ
forall k a (b :: k). a -> Const a b
Const ())
  where doNil :: p -> Compose f g a
doNil p
_ = f (g a) -> Compose f g a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g a) -> Compose f g a) -> f (g a) -> Compose f g a
forall a b. (a -> b) -> a -> b
$ f (g a)
forall (f :: * -> *) a. Alternative f => f a
empty
        doUncons :: p -> p -> Const (Const () b) b
doUncons p
_ p
_ = Const () b -> Const (Const () b) b
forall k a (b :: k). a -> Const a b
Const (Const () b -> Const (Const () b) b)
-> Const () b -> Const (Const () b) b
forall a b. (a -> b) -> a -> b
$ () -> Const () b
forall k a (b :: k). a -> Const a b
Const ()
        doCons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, AllUniqueLabels (Extend ℓ τ ρ))
               => Label ℓ -> Const (Compose f Var ρ) (Proxy τ) -> Compose f Var (Extend ℓ τ ρ)
        doCons :: Label ℓ
-> Const (Compose f Var ρ) (Proxy τ)
-> Compose f Var (Extend ℓ τ ρ)
doCons Label ℓ
l (Const (Compose f (Var ρ)
v)) = f (Var (Extend ℓ τ ρ)) -> Compose f Var (Extend ℓ τ ρ)
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (Var (Extend ℓ τ ρ)) -> Compose f Var (Extend ℓ τ ρ))
-> f (Var (Extend ℓ τ ρ)) -> Compose f Var (Extend ℓ τ ρ)
forall a b. (a -> b) -> a -> b
$ Label ℓ -> (Extend ℓ τ ρ .! ℓ) -> Var (Extend ℓ τ ρ)
forall (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Label l -> (r .! l) -> Var r
IsJust Label ℓ
l (τ -> Var (Extend ℓ τ ρ)) -> f τ -> f (Var (Extend ℓ τ ρ))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Label ℓ -> f τ
forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a
mk Label ℓ
l f (Var (Extend ℓ τ ρ))
-> f (Var (Extend ℓ τ ρ)) -> f (Var (Extend ℓ τ ρ))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Label ℓ -> Var ρ -> Var (Extend ℓ τ ρ)
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Var r -> Var (Extend l a r)
extend @τ Label ℓ
l (Var ρ -> Var (Extend ℓ τ ρ))
-> f (Var ρ) -> f (Var (Extend ℓ τ ρ))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Var ρ)
v
          (((Extend ℓ τ ρ .! ℓ) ~ τ) => f (Var (Extend ℓ τ ρ)))
-> Dict ((Extend ℓ τ ρ .! ℓ) ~ τ) -> f (Var (Extend ℓ τ ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict ((Extend ℓ τ ρ .! ℓ) ~ τ)
forall k (l :: Symbol) (t :: k) (r :: Row k).
Dict ((Extend l t r .! l) ≈ t)
extendHas @ℓ @τ @ρ

-- | Initialize a variant over a `Map`.
fromLabelsMap :: forall c f g ρ. (Alternative f, Forall ρ c, AllUniqueLabels ρ)
              => (forall l a. (KnownSymbol l, c a) => Label l -> f (g a)) -> f (Var (Map g ρ))
fromLabelsMap :: (forall (l :: Symbol) (a :: a).
 (KnownSymbol l, c a) =>
 Label l -> f (g a))
-> f (Var (Map g ρ))
fromLabelsMap forall (l :: Symbol) (a :: a).
(KnownSymbol l, c a) =>
Label l -> f (g a)
f = (forall (l :: Symbol) a.
 (KnownSymbol l, IsA c g a) =>
 Label l -> f a)
-> f (Var (Map g ρ))
forall (c :: * -> Constraint) (ρ :: Row *) (f :: * -> *).
(Alternative f, Forall ρ c, AllUniqueLabels ρ) =>
(forall (l :: Symbol) a. (KnownSymbol l, c a) => Label l -> f a)
-> f (Var ρ)
fromLabels @(IsA c g) @(Map g ρ) @f forall (l :: Symbol) a.
(KnownSymbol l, IsA c g a) =>
Label l -> f a
inner
               (Forall (Map g ρ) (IsA c g) => f (Var (Map g ρ)))
-> (Forall ρ c :- Forall (Map g ρ) (IsA c g)) -> f (Var (Map g ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Forall ρ c :- Forall (Map g ρ) (IsA c g)
forall k1 k2 (f :: k1 -> k2) (ρ :: Row k1) (c :: k1 -> Constraint).
Forall ρ c :- Forall (Map f ρ) (IsA c f)
mapForall @g @ρ @c
               ((AllUniqueLabels (Map g ρ) ~ AllUniqueLabels ρ) =>
 f (Var (Map g ρ)))
-> Dict (AllUniqueLabels (Map g ρ) ~ AllUniqueLabels ρ)
-> f (Var (Map g ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (AllUniqueLabels (Map g ρ) ~ AllUniqueLabels ρ)
forall k1 k2 (f :: k1 -> k2) (r :: Row k1).
Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
uniqueMap @g @ρ
   where inner :: forall l a. (KnownSymbol l, IsA c g a) => Label l -> f a
         inner :: Label l -> f a
inner Label l
l = case IsA c g a => As c g a
forall k k (c :: k -> Constraint) (f :: k -> k) (a :: k).
IsA c f a =>
As c f a
as @c @g @a of As c g a
As -> Label l -> f (g t)
forall (l :: Symbol) (a :: a).
(KnownSymbol l, c a) =>
Label l -> f (g a)
f Label l
l

{--------------------------------------------------------------------
  Functions for variants of ApSingle
--------------------------------------------------------------------}

newtype VApS x fs = VApS { VApS x fs -> Var (ApSingle fs x)
unVApS :: Var (ApSingle fs x) }
newtype VApSF x g fs = VApSF { VApSF x g fs -> g (Var (ApSingle fs x))
unVApSF :: g (Var (ApSingle fs x)) }
newtype FlipApp (x :: k) (f :: k -> *) = FlipApp (f x)

-- | A version of 'erase' that works even when the row-type of the variant argument
-- is of the form @ApSingle fs x@.
eraseSingle
  :: forall c fs x y
   . Forall fs c
  => (forall f . (c f) => f x -> y)
  -> Var (ApSingle fs x)
  -> y
eraseSingle :: (forall (f :: a -> *). c f => f x -> y) -> Var (ApSingle fs x) -> y
eraseSingle forall (f :: a -> *). c f => f x -> y
f = (forall a. ActsOn c x a => a -> y) -> Var (ApSingle fs x) -> y
forall (c :: * -> Constraint) (ρ :: Row *) b.
Forall ρ c =>
(forall a. c a => a -> b) -> Var ρ -> b
erase @(ActsOn c x) @(ApSingle fs x) @y forall a. ActsOn c x a => a -> y
g
  (Forall (ApSingle fs x) (ActsOn c x) => Var (ApSingle fs x) -> y)
-> (Forall fs c :- Forall (ApSingle fs x) (ActsOn c x))
-> Var (ApSingle fs x)
-> y
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Forall fs c :- Forall (ApSingle fs x) (ActsOn c x)
forall k1 k2 (a :: k1) (fs :: Row (k1 -> k2))
       (c :: (k1 -> k2) -> Constraint).
Forall fs c :- Forall (ApSingle fs a) (ActsOn c a)
apSingleForall @x @fs @c
  where
    g :: forall a. ActsOn c x a => a -> y
    g :: a -> y
g a
a = case ActsOn c x a => As' c x a
forall k k (c :: (k -> k) -> Constraint) (t :: k) (a :: k).
ActsOn c t a =>
As' c t a
actsOn @c @x @a of As' c x a
As' -> f x -> y
forall (f :: a -> *). c f => f x -> y
f a
f x
a

-- | Performs a functorial-like map over an 'ApSingle' variant.
-- In other words, it acts as a variant transformer to convert a variant of
-- @f x@ values to a variant of @f y@ values.  If no constraint is needed,
-- instantiate the first type argument with 'Unconstrained1'.
mapSingle
  :: forall c fs x y
   . (Forall fs c)
  => (forall f . (c f) => f x -> f y)
  -> Var (ApSingle fs x)
  -> Var (ApSingle fs y)
mapSingle :: (forall (f :: a -> *). c f => f x -> f y)
-> Var (ApSingle fs x) -> Var (ApSingle fs y)
mapSingle forall (f :: a -> *). c f => f x -> f y
f = Identity (Var (ApSingle fs y)) -> Var (ApSingle fs y)
forall a. Identity a -> a
runIdentity (Identity (Var (ApSingle fs y)) -> Var (ApSingle fs y))
-> (Var (ApSingle fs x) -> Identity (Var (ApSingle fs y)))
-> Var (ApSingle fs x)
-> Var (ApSingle fs y)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (f :: a -> *). c f => f x -> Identity (f y))
-> Var (ApSingle fs x) -> Identity (Var (ApSingle fs y))
forall a (c :: (a -> *) -> Constraint) (fs :: Row (a -> *))
       (g :: * -> *) (x :: a) (y :: a).
(Forall fs c, Functor g) =>
(forall (f :: a -> *). c f => f x -> g (f y))
-> Var (ApSingle fs x) -> g (Var (ApSingle fs y))
mapSingleA @c @fs @Identity @x @y (f y -> Identity (f y)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (f y -> Identity (f y)) -> (f x -> f y) -> f x -> Identity (f y)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> f y
forall (f :: a -> *). c f => f x -> f y
f)


-- | Like `mapSingle`, but works over a functor.
mapSingleA :: forall c fs g x y.
  (Forall fs c, Functor g) => (forall f. c f => f x -> g (f y)) -> Var (ApSingle fs x) -> g (Var (ApSingle fs y))
mapSingleA :: (forall (f :: a -> *). c f => f x -> g (f y))
-> Var (ApSingle fs x) -> g (Var (ApSingle fs y))
mapSingleA forall (f :: a -> *). c f => f x -> g (f y)
f = VApSF y g fs -> g (Var (ApSingle fs y))
forall a (x :: a) (g :: * -> *) (fs :: Row (a -> *)).
VApSF x g fs -> g (Var (ApSingle fs x))
unVApSF (VApSF y g fs -> g (Var (ApSingle fs y)))
-> (Var (ApSingle fs x) -> VApSF y g fs)
-> Var (ApSingle fs x)
-> g (Var (ApSingle fs y))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (Proxy (FlipApp x), Proxy Either)
-> (VApS x Empty -> VApSF y g Empty)
-> (forall (ℓ :: Symbol) (τ :: a -> *) (ρ :: Row (a -> *)).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> VApS x ρ -> Either (VApS x (ρ .- ℓ)) (FlipApp x τ))
-> (forall (ℓ :: Symbol) (τ :: a -> *) (ρ :: Row (a -> *)).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> Either (VApSF y g ρ) (FlipApp x τ) -> VApSF y g (Extend ℓ τ ρ))
-> VApS x fs
-> VApSF y g fs
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @fs @c @Either @(VApS x) @(VApSF y g) @(FlipApp x)
             Proxy (Proxy (FlipApp x), Proxy Either)
forall k (t :: k). Proxy t
Proxy VApS x Empty -> VApSF y g Empty
forall c. VApS x Empty -> c
doNil forall (l :: Symbol) (f :: a -> *) (fs :: Row (a -> *)).
(c f, (fs .! l) ≈ f, KnownSymbol l) =>
Label l -> VApS x fs -> Either (VApS x (fs .- l)) (FlipApp x f)
forall (ℓ :: Symbol) (τ :: a -> *) (ρ :: Row (a -> *)).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> VApS x ρ -> Either (VApS x (ρ .- ℓ)) (FlipApp x τ)
doUncons forall (l :: Symbol) (f :: a -> *) (fs :: Row (a -> *)).
(KnownSymbol l, c f, AllUniqueLabels (Extend l f fs)) =>
Label l
-> Either (VApSF y g fs) (FlipApp x f) -> VApSF y g (Extend l f fs)
forall (ℓ :: Symbol) (τ :: a -> *) (ρ :: Row (a -> *)).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Either (VApSF y g ρ) (FlipApp x τ) -> VApSF y g (Extend ℓ τ ρ)
doCons (VApS x fs -> VApSF y g fs)
-> (Var (ApSingle fs x) -> VApS x fs)
-> Var (ApSingle fs x)
-> VApSF y g fs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var (ApSingle fs x) -> VApS x fs
forall a (x :: a) (fs :: Row (a -> *)).
Var (ApSingle fs x) -> VApS x fs
VApS
 where
  doNil :: VApS x Empty -> c
doNil = Var Empty -> c
forall a. Var Empty -> a
impossible (Var Empty -> c)
-> (VApS x Empty -> Var Empty) -> VApS x Empty -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VApS x Empty -> Var Empty
forall a (x :: a) (fs :: Row (a -> *)).
VApS x fs -> Var (ApSingle fs x)
unVApS

  doUncons :: forall l f fs
           .  ( c f, fs .! l ≈ f, KnownSymbol l)
           => Label l -> VApS x fs -> Either (VApS x (fs .- l)) (FlipApp x f)
  doUncons :: Label l -> VApS x fs -> Either (VApS x (fs .- l)) (FlipApp x f)
doUncons Label l
l = (Var (ApSingle (fs .- l) x) -> VApS x (fs .- l))
-> (f x -> FlipApp x f)
-> Either (Var (ApSingle (fs .- l) x)) (f x)
-> Either (VApS x (fs .- l)) (FlipApp x f)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Var (ApSingle (fs .- l) x) -> VApS x (fs .- l)
forall a (x :: a) (fs :: Row (a -> *)).
Var (ApSingle fs x) -> VApS x fs
VApS f x -> FlipApp x f
forall k (x :: k) (f :: k -> *). f x -> FlipApp x f
FlipApp
             (Either (Var (ApSingle (fs .- l) x)) (f x)
 -> Either (VApS x (fs .- l)) (FlipApp x f))
-> (VApS x fs -> Either (Var (ApSingle (fs .- l) x)) (f x))
-> VApS x fs
-> Either (VApS x (fs .- l)) (FlipApp x f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var (ApSingle fs x)
 -> Label l -> Either (Var (ApSingle (fs .- l) x)) (f x))
-> Label l
-> Var (ApSingle fs x)
-> Either (Var (ApSingle (fs .- l) x)) (f x)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((ApSingle fs x .! l) ≈ f x,
 (ApSingle fs x .- l) ≈ ApSingle (fs .- l) x) =>
Var (ApSingle fs x)
-> Label l -> Either (Var (ApSingle (fs .- l) x)) (f x)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial (((ApSingle fs x .! l) ≈ f x,
  (ApSingle fs x .- l) ≈ ApSingle (fs .- l) x) =>
 Var (ApSingle fs x)
 -> Label l -> Either (Var (ApSingle (fs .- l) x)) (f x))
-> ((f ≈ f)
    :- ((ApSingle fs x .! l) ≈ f x,
        (ApSingle fs x .- l) ≈ ApSingle (fs .- l) x))
-> Var (ApSingle fs x)
-> Label l
-> Either (Var (ApSingle (fs .- l) x)) (f x)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((fs .! l) ≈ f)
:- ((ApSingle fs x .! l) ≈ f x,
    (ApSingle fs x .- l) ≈ ApSingle (fs .- l) x)
forall a b (x :: a) (l :: Symbol) (f :: a -> b)
       (r :: Row (a -> b)).
((r .! l) ≈ f)
:- ((ApSingle r x .! l) ≈ f x,
    (ApSingle r x .- l) ≈ ApSingle (r .- l) x)
apSingleHas @x @l @f @fs) Label l
l
             (Var (ApSingle fs x) -> Either (Var (ApSingle (fs .- l) x)) (f x))
-> (VApS x fs -> Var (ApSingle fs x))
-> VApS x fs
-> Either (Var (ApSingle (fs .- l) x)) (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VApS x fs -> Var (ApSingle fs x)
forall a (x :: a) (fs :: Row (a -> *)).
VApS x fs -> Var (ApSingle fs x)
unVApS

  doCons :: forall l f fs. (KnownSymbol l, c f, AllUniqueLabels (Extend l f fs))
         => Label l
         -> Either (VApSF y g fs) (FlipApp x f)
         -> VApSF y g (Extend l f fs)
  doCons :: Label l
-> Either (VApSF y g fs) (FlipApp x f) -> VApSF y g (Extend l f fs)
doCons Label l
l (Right (FlipApp f x
x)) = g (Var (ApSingle (Extend l f fs) y)) -> VApSF y g (Extend l f fs)
forall a (x :: a) (g :: * -> *) (fs :: Row (a -> *)).
g (Var (ApSingle fs x)) -> VApSF x g fs
VApSF (g (Var (ApSingle (Extend l f fs) y)) -> VApSF y g (Extend l f fs))
-> g (Var (ApSingle (Extend l f fs) y))
-> VApSF y g (Extend l f fs)
forall a b. (a -> b) -> a -> b
$ Label l
-> (ApSingle (Extend l f fs) y .! l)
-> Var (ApSingle (Extend l f fs) y)
forall (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Label l -> (r .! l) -> Var r
IsJust Label l
l (f y -> Var (ApSingle (Extend l f fs) y))
-> g (f y) -> g (Var (ApSingle (Extend l f fs) y))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (f x -> g (f y)
forall (f :: a -> *). c f => f x -> g (f y)
f f x
x)
    ((Extend l (f y) (ApSingle fs y) ~ ApSingle (Extend l f fs) y) =>
 g (Var (ApSingle (Extend l f fs) y)))
-> Dict
     (Extend l (f y) (ApSingle fs y) ~ ApSingle (Extend l f fs) y)
-> g (Var (ApSingle (Extend l f fs) y))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend l (f y) (ApSingle fs y) ~ ApSingle (Extend l f fs) y)
forall a b (τ :: a) (ℓ :: Symbol) (f :: a -> b)
       (r :: Row (a -> b)).
Dict (Extend ℓ (f τ) (ApSingle r τ) ≈ ApSingle (Extend ℓ f r) τ)
apSingleExtendSwap @y @l @f @fs
    (((Extend l (f y) (ApSingle fs y) .! l) ~ f y) =>
 g (Var (ApSingle (Extend l f fs) y)))
-> Dict ((Extend l (f y) (ApSingle fs y) .! l) ~ f y)
-> g (Var (ApSingle (Extend l f fs) y))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict ((Extend l (f y) (ApSingle fs y) .! l) ~ f y)
forall k (l :: Symbol) (t :: k) (r :: Row k).
Dict ((Extend l t r .! l) ≈ t)
extendHas @l @(f y) @(ApSingle fs y)
    ((AllUniqueLabels (ApSingle (Extend l f fs) y)
  ~ AllUniqueLabels (Extend l f fs)) =>
 g (Var (ApSingle (Extend l f fs) y)))
-> Dict
     (AllUniqueLabels (ApSingle (Extend l f fs) y)
      ~ AllUniqueLabels (Extend l f fs))
-> g (Var (ApSingle (Extend l f fs) y))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (AllUniqueLabels (ApSingle (Extend l f fs) y)
   ~ AllUniqueLabels (Extend l f fs))
forall a k (x :: a) (r :: Row (a -> k)).
Dict (AllUniqueLabels (ApSingle r x) ≈ AllUniqueLabels r)
uniqueApSingle @y @(Extend l f fs)
  doCons Label l
l (Left (VApSF g (Var (ApSingle fs y))
v)) = g (Var (ApSingle (Extend l f fs) y)) -> VApSF y g (Extend l f fs)
forall a (x :: a) (g :: * -> *) (fs :: Row (a -> *)).
g (Var (ApSingle fs x)) -> VApSF x g fs
VApSF (g (Var (ApSingle (Extend l f fs) y)) -> VApSF y g (Extend l f fs))
-> g (Var (ApSingle (Extend l f fs) y))
-> VApSF y g (Extend l f fs)
forall a b. (a -> b) -> a -> b
$ Label l
-> Var (ApSingle fs y) -> Var (Extend l (f y) (ApSingle fs y))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Var r -> Var (Extend l a r)
extend @(f y) Label l
l (Var (ApSingle fs y) -> Var (Extend l (f y) (ApSingle fs y)))
-> g (Var (ApSingle fs y))
-> g (Var (Extend l (f y) (ApSingle fs y)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> g (Var (ApSingle fs y))
v
    ((Extend l (f y) (ApSingle fs y) ~ ApSingle (Extend l f fs) y) =>
 g (Var (ApSingle (Extend l f fs) y)))
-> Dict
     (Extend l (f y) (ApSingle fs y) ~ ApSingle (Extend l f fs) y)
-> g (Var (ApSingle (Extend l f fs) y))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend l (f y) (ApSingle fs y) ~ ApSingle (Extend l f fs) y)
forall a b (τ :: a) (ℓ :: Symbol) (f :: a -> b)
       (r :: Row (a -> b)).
Dict (Extend ℓ (f τ) (ApSingle r τ) ≈ ApSingle (Extend ℓ f r) τ)
apSingleExtendSwap @y @l @f @fs


-- | A version of 'eraseZip' that works even when the row-types of the variant
-- arguments are of the form @ApSingle fs x@.
eraseZipSingle :: forall c fs x y z
                . (Forall fs c)
               => (forall f. c f => f x -> f y -> z)
               -> Var (ApSingle fs x) -> Var (ApSingle fs y) -> Maybe z
eraseZipSingle :: (forall (f :: a -> *). c f => f x -> f y -> z)
-> Var (ApSingle fs x) -> Var (ApSingle fs y) -> Maybe z
eraseZipSingle forall (f :: a -> *). c f => f x -> f y -> z
f Var (ApSingle fs x)
x Var (ApSingle fs y)
y = Const (Maybe z) fs -> Maybe z
forall a k (b :: k). Const a b -> a
getConst (Const (Maybe z) fs -> Maybe z) -> Const (Maybe z) fs -> Maybe z
forall a b. (a -> b) -> a -> b
$ Proxy (Proxy (Const (Maybe z)), Proxy Either)
-> (Product (VApS x) (VApS y) Empty -> Const (Maybe z) Empty)
-> (forall (ℓ :: Symbol) (τ :: a -> *) (ρ :: Row (a -> *)).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ
    -> Product (VApS x) (VApS y) ρ
    -> Either (Product (VApS x) (VApS y) (ρ .- ℓ)) (Const (Maybe z) τ))
-> (forall (ℓ :: Symbol) (τ :: a -> *) (ρ :: Row (a -> *)).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> Either (Const (Maybe z) ρ) (Const (Maybe z) τ)
    -> Const (Maybe z) (Extend ℓ τ ρ))
-> Product (VApS x) (VApS y) fs
-> Const (Maybe z) fs
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @fs @c @Either
    @(Product (VApS x) (VApS y)) @(Const (Maybe z)) @(Const (Maybe z))
    Proxy (Proxy (Const (Maybe z)), Proxy Either)
forall k (t :: k). Proxy t
Proxy Product (VApS x) (VApS y) Empty -> Const (Maybe z) Empty
forall a. Product (VApS x) (VApS y) Empty -> Const (Maybe z) Empty
doNil forall (l :: Symbol) (f :: a -> *) (ρ :: Row (a -> *)).
(KnownSymbol l, c f, (ρ .! l) ≈ f) =>
Label l
-> Product (VApS x) (VApS y) ρ
-> Either (Product (VApS x) (VApS y) (ρ .- l)) (Const (Maybe z) f)
forall (ℓ :: Symbol) (τ :: a -> *) (ρ :: Row (a -> *)).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ
-> Product (VApS x) (VApS y) ρ
-> Either (Product (VApS x) (VApS y) (ρ .- ℓ)) (Const (Maybe z) τ)
doUncons forall k (l :: Symbol) (τ :: k) (ρ :: Row k).
Label l
-> Either (Const (Maybe z) ρ) (Const (Maybe z) τ)
-> Const (Maybe z) (Extend l τ ρ)
forall (ℓ :: Symbol) (τ :: a -> *) (ρ :: Row (a -> *)).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Either (Const (Maybe z) ρ) (Const (Maybe z) τ)
-> Const (Maybe z) (Extend ℓ τ ρ)
doCons (VApS x fs -> VApS y fs -> Product (VApS x) (VApS y) fs
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (Var (ApSingle fs x) -> VApS x fs
forall a (x :: a) (fs :: Row (a -> *)).
Var (ApSingle fs x) -> VApS x fs
VApS Var (ApSingle fs x)
x) (Var (ApSingle fs y) -> VApS y fs
forall a (x :: a) (fs :: Row (a -> *)).
Var (ApSingle fs x) -> VApS x fs
VApS Var (ApSingle fs y)
y))

  where doNil :: Product (VApS x) (VApS y) Empty
              -> Const (Maybe z) Empty
        doNil :: Product (VApS x) (VApS y) Empty -> Const (Maybe z) Empty
doNil (Pair (VApS Var (ApSingle Empty x)
z) VApS y Empty
_) = Maybe z -> Const (Maybe z) Empty
forall k a (b :: k). a -> Const a b
Const (Var Empty -> Maybe z
forall a. Var Empty -> a
impossible Var (ApSingle Empty x)
Var Empty
z)

        doUncons :: forall l f ρ
                  . (KnownSymbol l, c f, ρ .! l ≈ f)
                 => Label l
                 -> Product (VApS x) (VApS y) ρ
                 -> Either (Product (VApS x) (VApS y) (ρ .- l))
                           (Const (Maybe z) f)
        doUncons :: Label l
-> Product (VApS x) (VApS y) ρ
-> Either (Product (VApS x) (VApS y) (ρ .- l)) (Const (Maybe z) f)
doUncons Label l
l (Pair (VApS Var (ApSingle ρ x)
r1) (VApS Var (ApSingle ρ y)
r2)) =
          case (
            Var (ApSingle ρ x)
-> Label l -> Either (Var (ApSingle ρ x .- l)) (ApSingle ρ x .! l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Var (ApSingle ρ x)
r1 Label l
l (((ApSingle ρ x .! l) ≈ f x,
  (ApSingle ρ x .- l) ≈ ApSingle (ρ .- l) x) =>
 Either (Var (ApSingle (ρ .- l) x)) (f x))
-> ((f ≈ f)
    :- ((ApSingle ρ x .! l) ≈ f x,
        (ApSingle ρ x .- l) ≈ ApSingle (ρ .- l) x))
-> Either (Var (ApSingle (ρ .- l) x)) (f x)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((ρ .! l) ≈ f)
:- ((ApSingle ρ x .! l) ≈ f x,
    (ApSingle ρ x .- l) ≈ ApSingle (ρ .- l) x)
forall a b (x :: a) (l :: Symbol) (f :: a -> b)
       (r :: Row (a -> b)).
((r .! l) ≈ f)
:- ((ApSingle r x .! l) ≈ f x,
    (ApSingle r x .- l) ≈ ApSingle (r .- l) x)
apSingleHas @x @l @f @ρ,
            Var (ApSingle ρ y)
-> Label l -> Either (Var (ApSingle ρ y .- l)) (ApSingle ρ y .! l)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial Var (ApSingle ρ y)
r2 Label l
l (((ApSingle ρ y .! l) ≈ f y,
  (ApSingle ρ y .- l) ≈ ApSingle (ρ .- l) y) =>
 Either (Var (ApSingle (ρ .- l) y)) (f y))
-> ((f ≈ f)
    :- ((ApSingle ρ y .! l) ≈ f y,
        (ApSingle ρ y .- l) ≈ ApSingle (ρ .- l) y))
-> Either (Var (ApSingle (ρ .- l) y)) (f y)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ ((ρ .! l) ≈ f)
:- ((ApSingle ρ y .! l) ≈ f y,
    (ApSingle ρ y .- l) ≈ ApSingle (ρ .- l) y)
forall a b (x :: a) (l :: Symbol) (f :: a -> b)
       (r :: Row (a -> b)).
((r .! l) ≈ f)
:- ((ApSingle r x .! l) ≈ f x,
    (ApSingle r x .- l) ≈ ApSingle (r .- l) x)
apSingleHas @y @l @f @ρ
          ) of
            (Right f x
u, Right f y
v) -> Const (Maybe z) f
-> Either (Product (VApS x) (VApS y) (ρ .- l)) (Const (Maybe z) f)
forall a b. b -> Either a b
Right (Const (Maybe z) f
 -> Either (Product (VApS x) (VApS y) (ρ .- l)) (Const (Maybe z) f))
-> Const (Maybe z) f
-> Either (Product (VApS x) (VApS y) (ρ .- l)) (Const (Maybe z) f)
forall a b. (a -> b) -> a -> b
$ Maybe z -> Const (Maybe z) f
forall k a (b :: k). a -> Const a b
Const (Maybe z -> Const (Maybe z) f) -> Maybe z -> Const (Maybe z) f
forall a b. (a -> b) -> a -> b
$ z -> Maybe z
forall a. a -> Maybe a
Just (z -> Maybe z) -> z -> Maybe z
forall a b. (a -> b) -> a -> b
$ f x -> f y -> z
forall (f :: a -> *). c f => f x -> f y -> z
f @f f x
u f y
v
            (Left Var (ApSingle (ρ .- l) x)
us, Left Var (ApSingle (ρ .- l) y)
vs) -> Product (VApS x) (VApS y) (ρ .- l)
-> Either (Product (VApS x) (VApS y) (ρ .- l)) (Const (Maybe z) f)
forall a b. a -> Either a b
Left (VApS x (ρ .- l)
-> VApS y (ρ .- l) -> Product (VApS x) (VApS y) (ρ .- l)
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (Var (ApSingle (ρ .- l) x) -> VApS x (ρ .- l)
forall a (x :: a) (fs :: Row (a -> *)).
Var (ApSingle fs x) -> VApS x fs
VApS Var (ApSingle (ρ .- l) x)
us) (Var (ApSingle (ρ .- l) y) -> VApS y (ρ .- l)
forall a (x :: a) (fs :: Row (a -> *)).
Var (ApSingle fs x) -> VApS x fs
VApS Var (ApSingle (ρ .- l) y)
vs))
            (Either (Var (ApSingle (ρ .- l) x)) (f x),
 Either (Var (ApSingle (ρ .- l) y)) (f y))
_                  -> Const (Maybe z) f
-> Either (Product (VApS x) (VApS y) (ρ .- l)) (Const (Maybe z) f)
forall a b. b -> Either a b
Right (Const (Maybe z) f
 -> Either (Product (VApS x) (VApS y) (ρ .- l)) (Const (Maybe z) f))
-> Const (Maybe z) f
-> Either (Product (VApS x) (VApS y) (ρ .- l)) (Const (Maybe z) f)
forall a b. (a -> b) -> a -> b
$ Maybe z -> Const (Maybe z) f
forall k a (b :: k). a -> Const a b
Const Maybe z
forall a. Maybe a
Nothing

        doCons :: forall k l τ (ρ :: Row k)
                . Label l
               -> Either (Const (Maybe z) ρ) (Const (Maybe z) τ)
               -> Const (Maybe z) (Extend l τ ρ)
        doCons :: Label l
-> Either (Const (Maybe z) ρ) (Const (Maybe z) τ)
-> Const (Maybe z) (Extend l τ ρ)
doCons Label l
_ (Left (Const Maybe z
w))  = Maybe z -> Const (Maybe z) (Extend l τ ρ)
forall k a (b :: k). a -> Const a b
Const Maybe z
w
        doCons Label l
_ (Right (Const Maybe z
w)) = Maybe z -> Const (Maybe z) (Extend l τ ρ)
forall k a (b :: k). a -> Const a b
Const Maybe z
w

{--------------------------------------------------------------------
  Generic instance
--------------------------------------------------------------------}

-- The generic structure we want Vars to have is not the hidden internal one,
-- but rather one that appears as a Haskell sum type.  Thus, we can't derive
-- Generic automatically.
--
-- The following Generic instance creates a representation of a Var that is
-- very similar to a native Haskell sum type except that the tree of possibilities (':+:')
-- that it produces will be extremely unbalanced.  I don't think this is a problem.
-- Furthermore, because we don't want Vars to always have a trailing void option on
-- the end, we must have a special case for singleton Vars, which means that
-- we can't use metamorph.

instance GenericVar r => G.Generic (Var r) where
  type Rep (Var r) =
    G.D1 ('G.MetaData "Var" "Data.Row.Variants" "row-types" 'False) (RepVar r)
  from :: Var r -> Rep (Var r) x
from = RepVar r x
-> M1
     D
     ('MetaData "Var" "Data.Row.Variants" "row-types" 'False)
     (RepVar r)
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (RepVar r x
 -> M1
      D
      ('MetaData "Var" "Data.Row.Variants" "row-types" 'False)
      (RepVar r)
      x)
-> (Var r -> RepVar r x)
-> Var r
-> M1
     D
     ('MetaData "Var" "Data.Row.Variants" "row-types" 'False)
     (RepVar r)
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var r -> RepVar r x
forall (r :: Row *) x. GenericVar r => Var r -> RepVar r x
fromVar
  to :: Rep (Var r) x -> Var r
to = RepVar r x -> Var r
forall (r :: Row *) x. GenericVar r => RepVar r x -> Var r
toVar (RepVar r x -> Var r)
-> (M1
      D
      ('MetaData "Var" "Data.Row.Variants" "row-types" 'False)
      (RepVar r)
      x
    -> RepVar r x)
-> M1
     D
     ('MetaData "Var" "Data.Row.Variants" "row-types" 'False)
     (RepVar r)
     x
-> Var r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1
  D
  ('MetaData "Var" "Data.Row.Variants" "row-types" 'False)
  (RepVar r)
  x
-> RepVar r x
forall i (c :: Meta) k (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1

class GenericVar r where
  type RepVar (r :: Row *) :: * -> *
  fromVar :: Var r -> RepVar r x
  toVar   :: RepVar r x -> Var r

instance GenericVar Empty where
  type RepVar Empty = G.V1
  fromVar :: Var Empty -> RepVar Empty x
fromVar = Var Empty -> RepVar Empty x
forall a. Var Empty -> a
impossible
  toVar :: RepVar Empty x -> Var Empty
toVar = RepVar Empty x -> Var Empty
\case

instance KnownSymbol name => GenericVar (R '[name :-> t]) where
  type RepVar (R (name :-> t ': '[])) = G.C1
    ('G.MetaCons name 'G.PrefixI 'False)
    (G.S1 ('G.MetaSel 'Nothing 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)
          (G.Rec0 t))
  fromVar :: Var ('R '[ name ':-> t]) -> RepVar ('R '[ name ':-> t]) x
fromVar (Var ('R '[ name ':-> t]) -> (Label name, t)
forall (l :: Symbol) a.
KnownSymbol l =>
Var (l .== a) -> (Label l, a)
unSingleton -> (Label name
_, t
a)) = M1
  S
  ('MetaSel
     'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
  (K1 R t)
  x
-> M1
     C
     ('MetaCons name 'PrefixI 'False)
     (M1
        S
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
        (K1 R t))
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (K1 R t x
-> M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (K1 R t)
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (t -> K1 R t x
forall k i c (p :: k). c -> K1 i c p
G.K1 t
a))
  toVar :: RepVar ('R '[ name ':-> t]) x -> Var ('R '[ name ':-> t])
toVar (G.M1 (G.M1 (G.K1 a))) = Label name
-> ('R '[ name ':-> t] .! name) -> Var ('R '[ name ':-> t])
forall (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Label l -> (r .! l) -> Var r
IsJust (Label name
forall (s :: Symbol). Label s
Label @name) t
'R '[ name ':-> t] .! name
a

instance
    ( GenericVar (R (name' :-> t' ': r'))
    , KnownSymbol name, Extend name t ('R (name' :-> t' ': r')) ≈ 'R (name :-> t ': (name' :-> t' ': r'))
    , AllUniqueLabels (R (name :-> t ': (name' :-> t' ': r')))
    ) => GenericVar (R (name :-> t ': (name' :-> t' ': r'))) where
  type RepVar (R (name :-> t ': (name' :-> t' ': r'))) = (G.C1
    ('G.MetaCons name 'G.PrefixI 'False)
    (G.S1 ('G.MetaSel 'Nothing 'G.NoSourceUnpackedness 'G.NoSourceStrictness 'G.DecidedLazy)
          (G.Rec0 t)))  G.:+: RepVar (R (name' :-> t' ': r'))
  fromVar :: Var ('R ((name ':-> t) : (name' ':-> t') : r'))
-> RepVar ('R ((name ':-> t) : (name' ':-> t') : r')) x
fromVar Var ('R ((name ':-> t) : (name' ':-> t') : r'))
v = case Var ('R ((name ':-> t) : (name' ':-> t') : r'))
-> Label name
-> Either
     (Var ('R ((name ':-> t) : (name' ':-> t') : r') .- name))
     ('R ((name ':-> t) : (name' ':-> t') : r') .! name)
forall (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Var r -> Label l -> Either (Var (r .- l)) (r .! l)
trial @name Var ('R ((name ':-> t) : (name' ':-> t') : r'))
v Label name
forall (s :: Symbol). Label s
Label of
    Left Var ('R ((name ':-> t) : (name' ':-> t') : r') .- name)
v' -> RepVar ('R ((name' ':-> t') : r')) x
-> (:+:)
     (C1
        ('MetaCons name 'PrefixI 'False)
        (S1
           ('MetaSel
              'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
           (Rec0 t)))
     (RepVar ('R ((name' ':-> t') : r')))
     x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
G.R1 (Var ('R ((name' ':-> t') : r'))
-> RepVar ('R ((name' ':-> t') : r')) x
forall (r :: Row *) x. GenericVar r => Var r -> RepVar r x
fromVar Var ('R ((name ':-> t) : (name' ':-> t') : r') .- name)
Var ('R ((name' ':-> t') : r'))
v')
    Right 'R ((name ':-> t) : (name' ':-> t') : r') .! name
a -> M1
  C
  ('MetaCons name 'PrefixI 'False)
  (S1
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (Rec0 t))
  x
-> (:+:)
     (C1
        ('MetaCons name 'PrefixI 'False)
        (S1
           ('MetaSel
              'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
           (Rec0 t)))
     (RepVar ('R ((name' ':-> t') : r')))
     x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
G.L1 (M1
  S
  ('MetaSel
     'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
  (Rec0 t)
  x
-> M1
     C
     ('MetaCons name 'PrefixI 'False)
     (S1
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
        (Rec0 t))
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (K1 R t x
-> M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (Rec0 t)
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (t -> K1 R t x
forall k i c (p :: k). c -> K1 i c p
G.K1 t
'R ((name ':-> t) : (name' ':-> t') : r') .! name
a)))
  toVar :: RepVar ('R ((name ':-> t) : (name' ':-> t') : r')) x
-> Var ('R ((name ':-> t) : (name' ':-> t') : r'))
toVar (G.L1 (G.M1 (G.M1 (G.K1 a)))) = Label name
-> ('R ((name ':-> t) : (name' ':-> t') : r') .! name)
-> Var ('R ((name ':-> t) : (name' ':-> t') : r'))
forall (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Label l -> (r .! l) -> Var r
IsJust (Label name
forall (s :: Symbol). Label s
Label @name) t
'R ((name ':-> t) : (name' ':-> t') : r') .! name
a
  toVar (G.R1 g) = Label name
-> Var ('R ((name' ':-> t') : r'))
-> Var (Extend name t ('R ((name' ':-> t') : r')))
forall a (l :: Symbol) (r :: Row *).
KnownSymbol l =>
Label l -> Var r -> Var (Extend l a r)
extend @t @name @('R (name' :-> t' ': r')) Label name
forall (s :: Symbol). Label s
Label (Var ('R ((name' ':-> t') : r'))
 -> Var (Extend name t ('R ((name' ':-> t') : r'))))
-> Var ('R ((name' ':-> t') : r'))
-> Var (Extend name t ('R ((name' ':-> t') : r')))
forall a b. (a -> b) -> a -> b
$ RepVar ('R ((name' ':-> t') : r')) x
-> Var ('R ((name' ':-> t') : r'))
forall (r :: Row *) x. GenericVar r => RepVar r x -> Var r
toVar RepVar ('R ((name' ':-> t') : r')) x
g

{--------------------------------------------------------------------
  Native data type compatibility
--------------------------------------------------------------------}

-- $native
-- The 'toNative' and 'fromNative' functions allow one to convert between
-- 'Var's and regular Haskell data types ("native" types) that have the same
-- number of constructors such that each constructor has one field and the same
-- name as one of the options of the 'Var', which has the same type as that field.
-- As expected, they compose to form the identity.  Alternatively, one may use
-- 'fromNativeGeneral', which allows a variant with excess options to  still be
-- transformed to a native type.  Because of this, 'fromNativeGeneral' requires a type
-- application (although 'fromNative' does not).  The only requirement is that
-- the native Haskell data type be an instance of 'Generic'.
--
-- For example, consider the following simple data type:
--
-- >>> data Pet = Dog {age :: Int} | Cat {age :: Int} deriving (Generic, Show)
--
-- Then, we have the following:
--
-- >>> toNative $ IsJust (Label @"Dog") 3 :: Pet
-- Dog {age = 3}
-- >>> V.fromNative $ Dog 3 :: Var ("Dog" .== Int .+ "Cat" .== Int)
-- {Dog=3}

type family NativeRow t where
  NativeRow t = NativeRowG (G.Rep t)

type family NativeRowG t where
  NativeRowG (G.M1 G.D m cs) = NativeRowG cs
  NativeRowG G.V1 = Empty
  NativeRowG (l G.:+: r) = NativeRowG l .+ NativeRowG r
  NativeRowG (G.C1 ('G.MetaCons name fixity sels) (G.S1 m (G.Rec0 t))) = name .== t


-- | Conversion helper to bring a variant back into a Haskell type. Note that the
-- native Haskell type must be an instance of 'Generic'.
class ToNativeG a where
  toNative' :: Var (NativeRowG a) -> a x

instance ToNativeG cs => ToNativeG (G.D1 m cs) where
  toNative' :: Var (NativeRowG (D1 m cs)) -> D1 m cs x
toNative' = cs x -> D1 m cs x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (cs x -> D1 m cs x)
-> (Var (NativeRowG cs) -> cs x)
-> Var (NativeRowG cs)
-> D1 m cs x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var (NativeRowG cs) -> cs x
forall k (a :: k -> *) (x :: k).
ToNativeG a =>
Var (NativeRowG a) -> a x
toNative'

instance ToNativeG G.V1 where
  toNative' :: Var (NativeRowG V1) -> V1 x
toNative' = Var (NativeRowG V1) -> V1 x
forall a. Var Empty -> a
impossible

instance (KnownSymbol name)
    => ToNativeG (G.C1 ('G.MetaCons name fixity sels)
                (G.S1 m (G.Rec0 t))) where
  toNative' :: Var (NativeRowG (C1 ('MetaCons name fixity sels) (S1 m (Rec0 t))))
-> C1 ('MetaCons name fixity sels) (S1 m (Rec0 t)) x
toNative' = M1 S m (Rec0 t) x
-> C1 ('MetaCons name fixity sels) (S1 m (Rec0 t)) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (M1 S m (Rec0 t) x
 -> C1 ('MetaCons name fixity sels) (S1 m (Rec0 t)) x)
-> (Var ('R '[ name ':-> t]) -> M1 S m (Rec0 t) x)
-> Var ('R '[ name ':-> t])
-> C1 ('MetaCons name fixity sels) (S1 m (Rec0 t)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 R t x -> M1 S m (Rec0 t) x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
G.M1 (K1 R t x -> M1 S m (Rec0 t) x)
-> (Var ('R '[ name ':-> t]) -> K1 R t x)
-> Var ('R '[ name ':-> t])
-> M1 S m (Rec0 t) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> K1 R t x
forall k i c (p :: k). c -> K1 i c p
G.K1 (t -> K1 R t x)
-> (Var ('R '[ name ':-> t]) -> t)
-> Var ('R '[ name ':-> t])
-> K1 R t x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Label name, t) -> t
forall a b. (a, b) -> b
snd ((Label name, t) -> t)
-> (Var ('R '[ name ':-> t]) -> (Label name, t))
-> Var ('R '[ name ':-> t])
-> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var ('R '[ name ':-> t]) -> (Label name, t)
forall (l :: Symbol) a.
KnownSymbol l =>
Var (l .== a) -> (Label l, a)
unSingleton

instance ( ToNativeG l, ToNativeG r, (NativeRowG l .+ NativeRowG r) .\\ NativeRowG r ≈ NativeRowG l
         , AllUniqueLabels (NativeRowG r), FreeForall (NativeRowG r))
    => ToNativeG (l G.:+: r) where
  toNative' :: Var (NativeRowG (l :+: r)) -> (:+:) l r x
toNative' Var (NativeRowG (l :+: r))
v = case Var (NativeRowG (l :+: r))
-> Either
     (Var (NativeRowG (l :+: r) .\\ NativeRowG r)) (Var (NativeRowG r))
forall (x :: Row *) (y :: Row *).
(AllUniqueLabels x, FreeForall x) =>
Var y -> Either (Var (y .\\ x)) (Var x)
multiTrial @(NativeRowG r) @(NativeRowG (l G.:+: r)) Var (NativeRowG (l :+: r))
v of
    Left  Var (NativeRowG (l :+: r) .\\ NativeRowG r)
v' -> l x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
G.L1 (l x -> (:+:) l r x) -> l x -> (:+:) l r x
forall a b. (a -> b) -> a -> b
$ Var (NativeRowG l) -> l x
forall k (a :: k -> *) (x :: k).
ToNativeG a =>
Var (NativeRowG a) -> a x
toNative' Var (NativeRowG (l :+: r) .\\ NativeRowG r)
Var (NativeRowG l)
v'
    Right Var (NativeRowG r)
v' -> r x -> (:+:) l r x
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
G.R1 (r x -> (:+:) l r x) -> r x -> (:+:) l r x
forall a b. (a -> b) -> a -> b
$ Var (NativeRowG r) -> r x
forall k (a :: k -> *) (x :: k).
ToNativeG a =>
Var (NativeRowG a) -> a x
toNative' Var (NativeRowG r)
v'

type ToNative t = (G.Generic t, ToNativeG (G.Rep t))

-- | Convert a variant to a native Haskell type.
toNative :: ToNative t => Var (NativeRow t) -> t
toNative :: Var (NativeRow t) -> t
toNative = Rep t Any -> t
forall a x. Generic a => Rep a x -> a
G.to (Rep t Any -> t)
-> (Var (NativeRowG (Rep t)) -> Rep t Any)
-> Var (NativeRowG (Rep t))
-> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var (NativeRowG (Rep t)) -> Rep t Any
forall k (a :: k -> *) (x :: k).
ToNativeG a =>
Var (NativeRowG a) -> a x
toNative'


-- | Conversion helper to turn a Haskell variant into a row-types extensible
-- variant. Note that the native Haskell type must be an instance of 'Generic'.
class FromNativeG a where
  fromNative' :: a x -> Var (NativeRowG a)

instance FromNativeG cs => FromNativeG (G.D1 m cs) where
  fromNative' :: D1 m cs x -> Var (NativeRowG (D1 m cs))
fromNative' (G.M1 cs x
v) = cs x -> Var (NativeRowG cs)
forall k (a :: k -> *) (x :: k).
FromNativeG a =>
a x -> Var (NativeRowG a)
fromNative' cs x
v

instance FromNativeG G.V1 where
  fromNative' :: V1 x -> Var (NativeRowG V1)
fromNative' = V1 x -> Var (NativeRowG V1)
\ case

instance KnownSymbol name
    => FromNativeG (G.C1 ('G.MetaCons name fixity sels)
                       (G.S1 m (G.Rec0 t))) where
  fromNative' :: C1 ('MetaCons name fixity sels) (S1 m (Rec0 t)) x
-> Var
     (NativeRowG (C1 ('MetaCons name fixity sels) (S1 m (Rec0 t))))
fromNative' (G.M1 (G.M1 (G.K1 t
x))) = Label name
-> ('R '[ name ':-> t] .! name) -> Var ('R '[ name ':-> t])
forall (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Label l -> (r .! l) -> Var r
IsJust (Label name
forall (s :: Symbol). Label s
Label @name) t
'R '[ name ':-> t] .! name
x

instance (FromNativeG l, FromNativeG r) => FromNativeG (l G.:+: r) where
  -- Ideally, we would use 'diversify' here instead of 'unsafeCoerce', but it
  -- makes the constraints really hairy.
  fromNative' :: (:+:) l r x -> Var (NativeRowG (l :+: r))
fromNative' (G.L1 l x
x) = Var (NativeRowG l) -> Var (NativeRowG l .+ NativeRowG r)
forall a b. a -> b
unsafeCoerce (Var (NativeRowG l) -> Var (NativeRowG l .+ NativeRowG r))
-> Var (NativeRowG l) -> Var (NativeRowG l .+ NativeRowG r)
forall a b. (a -> b) -> a -> b
$ l x -> Var (NativeRowG l)
forall k (a :: k -> *) (x :: k).
FromNativeG a =>
a x -> Var (NativeRowG a)
fromNative' @l l x
x
  fromNative' (G.R1 r x
y) = Var (NativeRowG r) -> Var (NativeRowG l .+ NativeRowG r)
forall a b. a -> b
unsafeCoerce (Var (NativeRowG r) -> Var (NativeRowG l .+ NativeRowG r))
-> Var (NativeRowG r) -> Var (NativeRowG l .+ NativeRowG r)
forall a b. (a -> b) -> a -> b
$ r x -> Var (NativeRowG r)
forall k (a :: k -> *) (x :: k).
FromNativeG a =>
a x -> Var (NativeRowG a)
fromNative' @r r x
y

type FromNative t = (G.Generic t, FromNativeG (G.Rep t))

-- | Convert a Haskell variant to a row-types Var.
fromNative :: FromNative t => t -> Var (NativeRow t)
fromNative :: t -> Var (NativeRow t)
fromNative = Rep t Any -> Var (NativeRowG (Rep t))
forall k (a :: k -> *) (x :: k).
FromNativeG a =>
a x -> Var (NativeRowG a)
fromNative' (Rep t Any -> Var (NativeRowG (Rep t)))
-> (t -> Rep t Any) -> t -> Var (NativeRowG (Rep t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Rep t Any
forall a x. Generic a => a -> Rep a x
G.from


-- | Conversion helper to turn a Haskell variant into a row-types extensible
-- variant. Note that the native Haskell type must be an instance of 'Generic'.
class FromNativeGeneralG a ρ where
  fromNativeGeneral' :: a x -> Var ρ

instance FromNativeGeneralG cs ρ => FromNativeGeneralG (G.D1 m cs) ρ where
  fromNativeGeneral' :: D1 m cs x -> Var ρ
fromNativeGeneral' (G.M1 cs x
v) = cs x -> Var ρ
forall k (a :: k -> *) (ρ :: Row *) (x :: k).
FromNativeGeneralG a ρ =>
a x -> Var ρ
fromNativeGeneral' cs x
v

instance FromNativeGeneralG G.V1 ρ where
  fromNativeGeneral' :: V1 x -> Var ρ
fromNativeGeneral' = V1 x -> Var ρ
\ case

instance (KnownSymbol name, ρ .! name ≈ t, AllUniqueLabels ρ)
    => FromNativeGeneralG (G.C1 ('G.MetaCons name fixity sels)
                  (G.S1 m (G.Rec0 t))) ρ where
  fromNativeGeneral' :: C1 ('MetaCons name fixity sels) (S1 m (Rec0 t)) x -> Var ρ
fromNativeGeneral' (G.M1 (G.M1 (G.K1 t
x))) = Label name -> (ρ .! name) -> Var ρ
forall (l :: Symbol) (r :: Row *).
(AllUniqueLabels r, KnownSymbol l) =>
Label l -> (r .! l) -> Var r
IsJust (Label name
forall (s :: Symbol). Label s
Label @name) t
ρ .! name
x

instance (FromNativeGeneralG l ρ, FromNativeGeneralG r ρ)
    => FromNativeGeneralG (l G.:+: r) ρ where
  -- Ideally, we would use 'diversify' here instead of 'unsafeCoerce', but it
  -- makes the constraints really hairy.
  fromNativeGeneral' :: (:+:) l r x -> Var ρ
fromNativeGeneral' (G.L1 l x
x) = Var ρ -> Var ρ
forall a b. a -> b
unsafeCoerce (Var ρ -> Var ρ) -> Var ρ -> Var ρ
forall a b. (a -> b) -> a -> b
$ l x -> Var ρ
forall k (a :: k -> *) (ρ :: Row *) (x :: k).
FromNativeGeneralG a ρ =>
a x -> Var ρ
fromNativeGeneral' @l @ρ l x
x
  fromNativeGeneral' (G.R1 r x
y) = Var ρ -> Var ρ
forall a b. a -> b
unsafeCoerce (Var ρ -> Var ρ) -> Var ρ -> Var ρ
forall a b. (a -> b) -> a -> b
$ r x -> Var ρ
forall k (a :: k -> *) (ρ :: Row *) (x :: k).
FromNativeGeneralG a ρ =>
a x -> Var ρ
fromNativeGeneral' @r @ρ r x
y

type FromNativeGeneral t ρ = (G.Generic t, FromNativeGeneralG (G.Rep t) ρ)

-- | Convert a Haskell variant to a row-types Var.
fromNativeGeneral :: FromNativeGeneral t ρ => t -> Var ρ
fromNativeGeneral :: t -> Var ρ
fromNativeGeneral = Rep t Any -> Var ρ
forall k (a :: k -> *) (ρ :: Row *) (x :: k).
FromNativeGeneralG a ρ =>
a x -> Var ρ
fromNativeGeneral' (Rep t Any -> Var ρ) -> (t -> Rep t Any) -> t -> Var ρ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t -> Rep t Any
forall a x. Generic a => a -> Rep a x
G.from


{--------------------------------------------------------------------
  Generic-lens compatibility
--------------------------------------------------------------------}

-- | Every possibility of a row-types based variant has an 'AsConstructor' instance.
instance {-# OVERLAPPING #-}
  ( AllUniqueLabels r
  , AllUniqueLabels r'
  , KnownSymbol name
  , r  .! name ≈ a
  , r' .! name ≈ b
  , r' ≈ (r .- name) .\/ (name .== b))
  => AsConstructor name (Var r) (Var r') a b where
  _Ctor :: p a (f b) -> p (Var r) (f (Var r'))
_Ctor = Label name -> p a (f b) -> p (Var r) (f (Var r'))
forall (l :: Symbol) (r :: Row *) (r' :: Row *) a b
       (p :: * -> * -> *) (f :: * -> *).
(AllUniqueLabels r, AllUniqueLabels r', KnownSymbol l,
 (r .! l) ≈ a, (r' .! l) ≈ b, r' ≈ ((r .- l) .\/ (l .== b)),
 Applicative f, Choice p) =>
Label l -> p a (f b) -> p (Var r) (f (Var r'))
focus (Label name
forall (s :: Symbol). Label s
Label @name)
  {-# INLINE _Ctor #-}

instance {-# OVERLAPPING #-}
  ( AllUniqueLabels r
  , KnownSymbol name
  , r  .! name ≈ a
  , r ≈ (r .- name) .\/ (name .== a))
  => AsConstructor' name (Var r) a where
  _Ctor' :: p a (f a) -> p (Var r) (f (Var r))
_Ctor' = Label name -> p a (f a) -> p (Var r) (f (Var r))
forall (l :: Symbol) (r :: Row *) (r' :: Row *) a b
       (p :: * -> * -> *) (f :: * -> *).
(AllUniqueLabels r, AllUniqueLabels r', KnownSymbol l,
 (r .! l) ≈ a, (r' .! l) ≈ b, r' ≈ ((r .- l) .\/ (l .== b)),
 Applicative f, Choice p) =>
Label l -> p a (f b) -> p (Var r) (f (Var r'))
focus (Label name
forall (s :: Symbol). Label s
Label @name)
  {-# INLINE _Ctor' #-}