-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Rage against the quantification
--   
--   Data types and typeclasses to deal with universally and existentially
--   quantified types
@package quantification
@version 0.4


-- | Data types and type classes for working with existentially quantified
--   values. In the event that Quantified Class Constraints ever land in
--   GHC, this package will be considered obsolete. The benefit that most
--   of the typeclasses in this module provide is that they help populate
--   the instances of <a>Exists</a>.
module Data.Exists

-- | Hide a type parameter.
data Exists (f :: k -> Type)
Exists :: !(f a) -> Exists

-- | Hide two type parameters.
data Exists2 (f :: k -> j -> Type)
Exists2 :: !(f a b) -> Exists2

-- | Hide three type parameters.
data Exists3 (f :: k -> j -> l -> Type)
Exists3 :: !(f a b c) -> Exists3
data Some (f :: k -> Type)
Some :: !(Sing a) -> !(f a) -> Some
data DependentPair (f :: k -> Type) (g :: k -> Type)
DependentPair :: (f a) -> (g a) -> DependentPair
data WitnessedEquality (a :: k) (b :: k)
[WitnessedEqualityEqual] :: WitnessedEquality a a
[WitnessedEqualityUnequal] :: WitnessedEquality a b
data WitnessedOrdering (a :: k) (b :: k)
[WitnessedOrderingLT] :: WitnessedOrdering a b
[WitnessedOrderingEQ] :: WitnessedOrdering a a
[WitnessedOrderingGT] :: WitnessedOrdering a b
class EqForall f
eqForall :: EqForall f => f a -> f a -> Bool
class EqForall f => EqForallPoly f
eqForallPoly :: EqForallPoly f => f a -> f b -> WitnessedEquality a b
eqForallPoly :: (EqForallPoly f, TestEquality f) => f a -> f b -> WitnessedEquality a b

-- | Variant of <a>EqForall</a> that requires a pi-quantified type.
class EqForeach f
eqForeach :: EqForeach f => Sing a -> f a -> f a -> Bool
class EqForall f => OrdForall f
compareForall :: OrdForall f => f a -> f a -> Ordering
class (OrdForall f, EqForallPoly f) => OrdForallPoly f
compareForallPoly :: OrdForallPoly f => f a -> f b -> WitnessedOrdering a b

-- | Variant of <a>OrdForall</a> that requires a pi-quantified type.
class EqForeach f => OrdForeach f
compareForeach :: OrdForeach f => Sing a -> f a -> f a -> Ordering
class ShowForall f
showsPrecForall :: ShowForall f => Int -> f a -> ShowS
class ShowForeach f
showsPrecForeach :: ShowForeach f => Sing a -> Int -> f a -> ShowS
class ReadForall f
readPrecForall :: ReadForall f => ReadPrec (Exists f)
class EnumForall f
toEnumForall :: EnumForall f => Int -> Exists f
fromEnumForall :: EnumForall f => f a -> Int
class BoundedForall f
minBoundForall :: BoundedForall f => Exists f
maxBoundForall :: BoundedForall f => Exists f
class SemigroupForall f
sappendForall :: SemigroupForall f => f a -> f a -> f a
class SemigroupForall f => MonoidForall f
memptyForall :: MonoidForall f => Sing a -> f a
class HashableForall f
hashWithSaltForall :: HashableForall f => Int -> f a -> Int
class PathPieceForall f
fromPathPieceForall :: PathPieceForall f => Text -> Maybe (Exists f)
toPathPieceForall :: PathPieceForall f => f a -> Text
class FromJSONForall f
parseJSONForall :: FromJSONForall f => Sing a -> Value -> Parser (f a)
class FromJSONExists f
parseJSONExists :: FromJSONExists f => Value -> Parser (Exists f)
class ToJSONForall f
toJSONForall :: ToJSONForall f => f a -> Value
data ToJSONKeyFunctionForall f
ToJSONKeyTextForall :: !(forall a. f a -> Text) -> !(forall a. f a -> Encoding' Text) -> ToJSONKeyFunctionForall f
ToJSONKeyValueForall :: !(forall a. f a -> Value) -> !(forall a. f a -> Encoding) -> ToJSONKeyFunctionForall f
data FromJSONKeyFunctionForall f
FromJSONKeyTextParserForall :: !(forall a. Sing a -> Text -> Parser (f a)) -> FromJSONKeyFunctionForall f
FromJSONKeyValueForall :: !(forall a. Sing a -> Value -> Parser (f a)) -> FromJSONKeyFunctionForall f
class ToJSONKeyForall f
toJSONKeyForall :: ToJSONKeyForall f => ToJSONKeyFunctionForall f
class FromJSONKeyExists f
fromJSONKeyExists :: FromJSONKeyExists f => FromJSONKeyFunction (Exists f)
class FromJSONKeyForall f
fromJSONKeyForall :: FromJSONKeyForall f => FromJSONKeyFunctionForall f
class StorableForall (f :: k -> Type)
peekForall :: StorableForall f => Sing a -> Ptr (f a) -> IO (f a)
pokeForall :: StorableForall f => Ptr (f a) -> f a -> IO ()
sizeOfFunctorForall :: StorableForall f => f a -> Int
sizeOfForall :: forall (a :: k). StorableForall f => Proxy f -> Sing a -> Int
class EqForall2 f
eqForall2 :: EqForall2 f => f a b -> f a b -> Bool
class EqForallPoly2 f
eqForallPoly2 :: EqForallPoly2 f => f a b -> f c d -> Bool
class ShowForall2 f
showsPrecForall2 :: ShowForall2 f => Int -> f a b -> ShowS
data SingList :: [k] -> Type
[SingListNil] :: SingList '[]
[SingListCons] :: Sing r -> SingList rs -> SingList (r : rs)
data SingMaybe :: Maybe k -> Type
[SingMaybeJust] :: Sing a -> SingMaybe ( 'Just a)
[SingMaybeNothing] :: SingMaybe  'Nothing
class Reify a
reify :: Reify a => Sing a
class Unreify k
unreify :: forall (a :: k) b. Unreify k => Sing a -> (Reify a => b) -> b
class EqSing k
eqSing :: forall (a :: k) (b :: k). EqSing k => Sing a -> Sing b -> Maybe (a :~: b)
class ToJSONSing k
toJSONSing :: forall (a :: k). ToJSONSing k => Sing a -> Value
class FromJSONSing k
parseJSONSing :: FromJSONSing k => Value -> Parser (Exists (Sing :: k -> Type))
class ToSing (f :: k -> Type)
toSing :: ToSing f => f a -> Sing a
showsForall :: ShowForall f => f a -> ShowS
showForall :: ShowForall f => f a -> String
showsForall2 :: ShowForall2 f => f a b -> ShowS
showForall2 :: ShowForall2 f => f a b -> String
defaultEqForallPoly :: (TestEquality f, EqForall f) => f a -> f b -> WitnessedEquality a b
defaultCompareForallPoly :: (TestEquality f, OrdForall f) => f a -> f b -> Ordering

-- | Parse a <a>Map</a> whose key type is higher-kinded. This only creates
--   a valid <a>Map</a> if the <a>OrdForall</a> instance agrees with the
--   <a>Ord</a> instance.
parseJSONMapForallKey :: forall f a v. (FromJSONKeyForall f, OrdForall f) => (Value -> Parser v) -> Sing a -> Value -> Parser (Map (f a) v)
weakenEquality :: WitnessedEquality a b -> Bool
weakenOrdering :: WitnessedOrdering a b -> Ordering
unreifyList :: forall (as :: [k]) b. Unreify k => SingList as -> (Reify as => b) -> b
instance forall k (f :: k -> *) (a :: k). Data.Exists.EqForall f => GHC.Classes.Eq (Data.Exists.Apply f a)
instance forall k (f :: k -> *) (a :: k). Data.Exists.OrdForall f => GHC.Classes.Ord (Data.Exists.Apply f a)
instance forall k (f :: k -> *). (Data.Exists.FromJSONForall f, Data.Exists.FromJSONSing k) => Data.Aeson.Types.FromJSON.FromJSON (Data.Exists.Some f)
instance forall k (f :: k -> *). (Data.Exists.ToJSONForall f, Data.Exists.ToJSONSing k) => Data.Aeson.Types.ToJSON.ToJSON (Data.Exists.Some f)
instance forall k (f :: k -> *) (g :: k -> *). (Data.Exists.EqForallPoly f, Data.Exists.ToSing f, Data.Exists.EqForeach g) => GHC.Classes.Eq (Data.Exists.DependentPair f g)
instance forall k (f :: k -> *) (g :: k -> *). (Data.Exists.OrdForallPoly f, Data.Exists.ToSing f, Data.Exists.OrdForeach g) => GHC.Classes.Ord (Data.Exists.DependentPair f g)
instance forall k (f :: k -> *) (g :: k -> *). (Data.Exists.ShowForall f, Data.Exists.ToSing f, Data.Exists.ShowForeach g) => GHC.Show.Show (Data.Exists.DependentPair f g)
instance forall k (f :: k -> *). (Data.Exists.EqForall f, Data.Exists.EqSing k) => GHC.Classes.Eq (Data.Exists.Some f)
instance Data.Exists.Reify 'GHC.Base.Nothing
instance forall a1 (a2 :: a1). Data.Exists.Reify a2 => Data.Exists.Reify ('GHC.Base.Just a2)
instance Data.Exists.Reify '[]
instance forall a1 (a2 :: a1) (as :: [a1]). (Data.Exists.Reify a2, Data.Exists.Reify as) => Data.Exists.Reify (a2 : as)
instance Data.Exists.EqSing a => Data.Exists.EqSing [a]
instance Data.Exists.Unreify k => Data.Exists.Unreify [k]
instance forall k (f :: * -> *) (g :: k -> *). (Data.Aeson.Types.FromJSON.FromJSON1 f, Data.Exists.FromJSONForall g) => Data.Exists.FromJSONForall (Data.Functor.Compose.Compose f g)
instance Data.Exists.SemigroupForall Data.Proxy.Proxy
instance forall k (f :: k -> *). Data.Exists.PathPieceForall f => Web.PathPieces.PathPiece (Data.Exists.Exists f)
instance forall k (f :: k -> *). Data.Exists.BoundedForall f => GHC.Enum.Bounded (Data.Exists.Exists f)
instance forall k (f :: k -> *). Data.Exists.EnumForall f => GHC.Enum.Enum (Data.Exists.Exists f)
instance forall k (f :: k -> *). (Data.Exists.FromJSONKeyExists f, Data.Exists.FromJSONExists f) => Data.Aeson.Types.FromJSON.FromJSONKey (Data.Exists.Exists f)
instance forall k (f :: k -> *). Data.Exists.FromJSONExists f => Data.Aeson.Types.FromJSON.FromJSON (Data.Exists.Exists f)
instance forall k (f :: k -> *). (Data.Exists.ToJSONKeyForall f, Data.Exists.ToJSONForall f) => Data.Aeson.Types.ToJSON.ToJSONKey (Data.Exists.Exists f)
instance forall k (f :: k -> *). Data.Exists.ToJSONForall f => Data.Aeson.Types.ToJSON.ToJSON (Data.Exists.Exists f)
instance forall k (f :: * -> *) (g :: k -> *). (Data.Aeson.Types.ToJSON.ToJSON1 f, Data.Exists.ToJSONForall g) => Data.Exists.ToJSONForall (Data.Functor.Compose.Compose f g)
instance Data.Hashable.Class.Hashable a => Data.Exists.HashableForall (Data.Functor.Const.Const a)
instance forall k (f :: k -> *). Data.Exists.HashableForall f => Data.Hashable.Class.Hashable (Data.Exists.Exists f)
instance forall k j (f :: k -> j -> *). Data.Exists.EqForallPoly2 f => GHC.Classes.Eq (Data.Exists.Exists2 f)
instance Data.Exists.EqForall2 (Data.Type.Equality.:~:)
instance Data.Exists.ReadForall Data.Proxy.Proxy
instance forall k (f :: k -> *). Data.Exists.ReadForall f => GHC.Read.Read (Data.Exists.Exists f)
instance forall k j (f :: k -> j -> *). Data.Exists.ShowForall2 f => GHC.Show.Show (Data.Exists.Exists2 f)
instance Data.Exists.ShowForall Data.Proxy.Proxy
instance forall k (f :: k -> *). Data.Exists.ShowForall f => GHC.Show.Show (Data.Exists.Exists f)
instance forall k (f :: k -> *) (g :: k -> *). (Data.Exists.ShowForall f, Data.Exists.ShowForall g) => Data.Exists.ShowForall (Data.Functor.Product.Product f g)
instance forall k (f :: * -> *) (g :: k -> *). (Data.Functor.Classes.Show1 f, Data.Exists.ShowForall g) => Data.Exists.ShowForall (Data.Functor.Compose.Compose f g)
instance forall k (f :: k -> *). Data.Exists.OrdForallPoly f => GHC.Classes.Ord (Data.Exists.Exists f)
instance forall k (f :: k -> *) (g :: k -> *). (Data.Exists.OrdForallPoly f, Data.Exists.OrdForallPoly g) => Data.Exists.OrdForallPoly (Data.Functor.Product.Product f g)
instance forall k (f :: k -> *). Data.Exists.EqForallPoly f => GHC.Classes.Eq (Data.Exists.Exists f)
instance forall k (f :: k -> *) (g :: k -> *). (Data.Exists.EqForallPoly f, Data.Exists.EqForallPoly g) => Data.Exists.EqForallPoly (Data.Functor.Product.Product f g)
instance Data.Exists.OrdForall Data.Proxy.Proxy
instance GHC.Classes.Ord a => Data.Exists.OrdForall (Data.Functor.Const.Const a)
instance forall k (f :: k -> *) (g :: k -> *). (Data.Exists.OrdForall f, Data.Exists.OrdForall g) => Data.Exists.OrdForall (Data.Functor.Product.Product f g)
instance forall k (f :: k -> *) (g :: k -> *). (Data.Exists.OrdForall f, Data.Exists.OrdForall g) => Data.Exists.OrdForall (Data.Functor.Sum.Sum f g)
instance Data.Exists.EqForall Data.Proxy.Proxy
instance forall k (a :: k). Data.Exists.EqForall ((Data.Type.Equality.:~:) a)
instance GHC.Classes.Eq a => Data.Exists.EqForall (Data.Functor.Const.Const a)
instance forall k (f :: k -> *) (g :: k -> *). (Data.Exists.EqForall f, Data.Exists.EqForall g) => Data.Exists.EqForall (Data.Functor.Product.Product f g)
instance forall k (f :: * -> *) (g :: k -> *). (Data.Functor.Classes.Eq1 f, Data.Exists.EqForall g) => Data.Exists.EqForall (Data.Functor.Compose.Compose f g)
instance forall k (f :: k -> *) (g :: k -> *). (Data.Exists.EqForall f, Data.Exists.EqForall g) => Data.Exists.EqForall (Data.Functor.Sum.Sum f g)

module Data.Monoid.Lifted

-- | Laws for this typeclass:
--   
--   <ul>
--   <li><pre>liftAppend f a (liftAppend f b c) = liftAppend f (liftAppend
--   f a b) c</pre></li>
--   </ul>
class Semigroup1 f
liftAppend :: Semigroup1 f => (a -> a -> a) -> f a -> f a -> f a

-- | Laws for this typeclass:
--   
--   <ul>
--   <li><pre>liftAppend f a (liftEmpty mempty) = a</pre></li>
--   </ul>
class Semigroup1 f => Monoid1 f
liftEmpty :: Monoid1 f => a -> f a
append1 :: (Semigroup1 f, Semigroup a) => f a -> f a -> f a
empty1 :: (Monoid1 f, Monoid a) => f a
instance (Data.Monoid.Lifted.Monoid1 f, Data.Monoid.Lifted.Monoid1 g) => Data.Monoid.Lifted.Monoid1 (Data.Functor.Compose.Compose f g)
instance Data.Monoid.Lifted.Monoid1 GHC.Types.IO
instance (Data.Hashable.Class.Hashable k, GHC.Classes.Eq k) => Data.Monoid.Lifted.Monoid1 (Data.HashMap.Base.HashMap k)
instance Data.Monoid.Lifted.Monoid1 []
instance Data.Monoid.Lifted.Monoid1 Data.Functor.Identity.Identity
instance (Data.Monoid.Lifted.Monoid1 f, Data.Monoid.Lifted.Monoid1 g) => Data.Monoid.Lifted.Monoid1 (Data.Functor.Product.Product f g)
instance Data.Monoid.Lifted.Monoid1 Data.Semigroup.Internal.Dual
instance (GHC.Base.Semigroup a, GHC.Base.Monoid a) => Data.Monoid.Lifted.Monoid1 ((,) a)
instance Data.Monoid.Lifted.Monoid1 Data.Proxy.Proxy
instance Data.Monoid.Lifted.Monoid1 ((->) a)
instance Data.Monoid.Lifted.Semigroup1 GHC.Base.Maybe
instance (Data.Monoid.Lifted.Semigroup1 f, Data.Monoid.Lifted.Semigroup1 g) => Data.Monoid.Lifted.Semigroup1 (Data.Functor.Compose.Compose f g)
instance Data.Monoid.Lifted.Semigroup1 GHC.Types.IO
instance GHC.Classes.Ord k => Data.Monoid.Lifted.Semigroup1 (Data.Map.Internal.Map k)
instance (Data.Hashable.Class.Hashable k, GHC.Classes.Eq k) => Data.Monoid.Lifted.Semigroup1 (Data.HashMap.Base.HashMap k)
instance Data.Monoid.Lifted.Semigroup1 []
instance Data.Monoid.Lifted.Semigroup1 Data.Functor.Identity.Identity
instance (Data.Monoid.Lifted.Semigroup1 f, Data.Monoid.Lifted.Semigroup1 g) => Data.Monoid.Lifted.Semigroup1 (Data.Functor.Product.Product f g)
instance Data.Monoid.Lifted.Semigroup1 Data.Semigroup.Internal.Dual
instance GHC.Base.Semigroup a => Data.Monoid.Lifted.Semigroup1 ((,) a)
instance Data.Monoid.Lifted.Semigroup1 Data.Proxy.Proxy
instance Data.Monoid.Lifted.Semigroup1 ((->) a)

module Topaz.Types
data Elem (rs :: [k]) (r :: k)
[ElemHere] :: Elem (r : rs) r
[ElemThere] :: Elem rs r -> Elem (s : rs) r
data Rec :: (k -> Type) -> [k] -> Type
[RecNil] :: Rec f '[]
[RecCons] :: f r -> Rec f rs -> Rec f (r : rs)
data NestRec :: (k -> Type) -> Nest k -> Type
[NestRec] :: Rec f rs -> Rec (NestRec f) ns -> NestRec f ( 'Nest ns rs)
newtype Fix f
Fix :: (f (Fix f)) -> Fix f
newtype HFix h a
HFix :: (h (HFix h) a) -> HFix h a
data Nest a
Nest :: [Nest a] -> [a] -> Nest a
class EqHetero h
eqHetero :: EqHetero h => (forall x. f x -> f x -> Bool) -> h f a -> h f a -> Bool
class TestEqualityHetero h
testEqualityHetero :: TestEqualityHetero h => (forall x y. f x -> f y -> Maybe (x :~: y)) -> h f a -> h f b -> Maybe (a :~: b)
data Nat
Succ :: Nat -> Nat
Zero :: Nat
data SingNat :: Nat -> Type
[SingZero] :: SingNat  'Zero
[SingSucc] :: SingNat n -> SingNat ( 'Succ n)
data Vector :: Nat -> Type -> Type
[VectorNil] :: Vector  'Zero a
[VectorCons] :: a -> Vector n a -> Vector ( 'Succ n) a
instance forall k (h :: (k -> *) -> k -> *). Topaz.Types.TestEqualityHetero h => Data.Type.Equality.TestEquality (Topaz.Types.HFix h)
instance forall k (h :: (k -> *) -> k -> *). Topaz.Types.EqHetero h => Data.Exists.EqForall (Topaz.Types.HFix h)
instance forall k (h :: (k -> *) -> k -> *) (a :: k). Topaz.Types.EqHetero h => GHC.Classes.Eq (Topaz.Types.HFix h a)
instance Data.Monoid.Lifted.Semigroup1 f => GHC.Base.Semigroup (Topaz.Types.Fix f)
instance Data.Monoid.Lifted.Monoid1 f => GHC.Base.Monoid (Topaz.Types.Fix f)
instance forall k (f :: k -> *). Data.Type.Equality.TestEquality f => Data.Type.Equality.TestEquality (Topaz.Types.Rec f)
instance forall k (f :: k -> *). Data.Type.Coercion.TestCoercion f => Data.Type.Coercion.TestCoercion (Topaz.Types.Rec f)
instance forall k (f :: k -> *) (as :: [k]). Data.Exists.EqForall f => GHC.Classes.Eq (Topaz.Types.Rec f as)
instance forall k (f :: k -> *). Data.Exists.HashableForall f => Data.Exists.HashableForall (Topaz.Types.Rec f)
instance forall k (f :: k -> *) (as :: [k]). Data.Exists.HashableForall f => Data.Hashable.Class.Hashable (Topaz.Types.Rec f as)
instance forall k (f :: k -> *). Data.Exists.ShowForall f => Data.Exists.ShowForall (Topaz.Types.Rec f)
instance forall k (f :: k -> *) (as :: [k]). Data.Exists.ShowForall f => GHC.Show.Show (Topaz.Types.Rec f as)
instance forall k (f :: k -> *). Data.Exists.EqForall f => Data.Exists.EqForall (Topaz.Types.Rec f)
instance forall k (f :: k -> *) (as :: [k]). Data.Exists.OrdForall f => GHC.Classes.Ord (Topaz.Types.Rec f as)
instance forall k (f :: k -> *). Data.Exists.OrdForall f => Data.Exists.OrdForall (Topaz.Types.Rec f)
instance forall k (f :: k -> *) (as :: [k]). Data.Exists.SemigroupForall f => GHC.Base.Semigroup (Topaz.Types.Rec f as)
instance forall k (f :: k -> *) (as :: [k]). (Data.Exists.MonoidForall f, Data.Exists.Reify as) => GHC.Base.Monoid (Topaz.Types.Rec f as)
instance forall k (f :: k -> *). Data.Exists.MonoidForall f => Data.Exists.MonoidForall (Topaz.Types.Rec f)
instance forall k (f :: k -> *). Data.Exists.SemigroupForall f => Data.Exists.SemigroupForall (Topaz.Types.Rec f)
instance forall k (f :: k -> *) (as :: [k]). Data.Exists.ToJSONForall f => Data.Aeson.Types.ToJSON.ToJSON (Topaz.Types.Rec f as)
instance forall k (f :: k -> *). Data.Exists.ToJSONForall f => Data.Exists.ToJSONForall (Topaz.Types.Rec f)
instance forall k (f :: k -> *) (as :: [k]). (Data.Exists.FromJSONForall f, Data.Exists.Reify as) => Data.Aeson.Types.FromJSON.FromJSON (Topaz.Types.Rec f as)
instance forall k (f :: k -> *). Data.Exists.FromJSONForall f => Data.Exists.FromJSONForall (Topaz.Types.Rec f)
instance forall k (f :: k -> *). Data.Exists.StorableForall f => Data.Exists.StorableForall (Topaz.Types.Rec f)
instance forall k (f :: k -> *) (as :: [k]). (Data.Exists.StorableForall f, Data.Exists.Reify as) => Foreign.Storable.Storable (Topaz.Types.Rec f as)
instance forall k (f :: k -> *). Data.Exists.FromJSONExists f => Data.Exists.FromJSONExists (Topaz.Types.Rec f)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Topaz.Types.Vector n a)

module Topaz.Rec
data Rec :: (k -> Type) -> [k] -> Type
[RecNil] :: Rec f '[]
[RecCons] :: f r -> Rec f rs -> Rec f (r : rs)
map :: (forall x. f x -> g x) -> Rec f as -> Rec g as
append :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
traverse :: Applicative h => (forall x. f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
traverse_ :: Applicative h => (forall x. f x -> h b) -> Rec f rs -> h ()
zipWith :: (forall x. f x -> g x -> h x) -> Rec f rs -> Rec g rs -> Rec h rs

-- | Map each element of a record to a monoid and combine the results.
foldMap :: forall f m rs. Monoid m => (forall x. f x -> m) -> Rec f rs -> m
foldMap1 :: forall f m r rs. Semigroup m => (forall x. f x -> m) -> Rec f (r : rs) -> m
get :: Elem rs r -> Rec f rs -> f r
put :: Elem rs r -> f r -> Rec f rs -> Rec f rs
gets :: Rec (Elem rs) ss -> Rec f rs -> Rec f ss
puts :: Rec (Elem rs) ss -> Rec f rs -> Rec f ss -> Rec f rs
fromSingList :: SingList as -> Rec Sing as