Safe Haskell	Trustworthy
Language	Haskell2010

Data.Vinyl.Core

Description

Core vinyl definitions. The Rec data type is defined here, but also of interest are definitions commonly used functions like rmap, rapply, and rtraverse.

The definitions in this module are written in terms of type classes so that the definitions may be specialized to each record type at which they are used. This usually helps with runtime performance, but can slow down compilation time. If you are experiencing poor compile times, you may wish to try the semantically equivalent definitions in the Data.Vinyl.Recursive module: they should produce the same results given the same inputs as functions defined in this module, but they will not be specialized to your record type. Instead, they treat the record as a list of fields, so will have performance linear in the size of the record.

Synopsis

data Rec :: (u -> *) -> [u] -> * where
- RNil :: Rec f '[]
- (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs)
rappend :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
(<+>) :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
rcombine :: (RMap rs, RApply rs) => (forall a. m a -> m a -> m a) -> (forall a. f a -> m a) -> (forall a. m a -> g a) -> Rec f rs -> Rec f rs -> Rec g rs
class RMap rs where
- rmap :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs
(<<$>>) :: RMap rs => (forall x. f x -> g x) -> Rec f rs -> Rec g rs
(<<&>>) :: RMap rs => Rec f rs -> (forall x. f x -> g x) -> Rec g rs
class RApply rs where
- rapply :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
(<<*>>) :: RApply rs => Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
class RecApplicative rs where
- rpure :: (forall x. f x) -> Rec f rs
rtraverse :: Applicative h => (forall x. f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
rtraverseIn :: forall h f g rs. (forall a. f a -> g (ApplyToField h a)) -> Rec f rs -> Rec g (MapTyCon h rs)
rsequenceIn :: forall f g (rs :: [Type]). (Traversable f, Applicative g) => Rec (f :. g) rs -> Rec g (MapTyCon f rs)
rzipWith :: (RMap xs, RApply xs) => (forall x. f x -> g x -> h x) -> Rec f xs -> Rec g xs -> Rec h xs
class RFoldMap rs where
- rfoldMapAux :: Monoid m => (forall x. f x -> m) -> m -> Rec f rs -> m
rfoldMap :: forall rs m f. (Monoid m, RFoldMap rs) => (forall x. f x -> m) -> Rec f rs -> m
class RecordToList rs where
- recordToList :: Rec (Const a) rs -> [a]
data Dict c a where
- Dict :: c a => a -> Dict c a
class ReifyConstraint c f rs where
- reifyConstraint :: Rec f rs -> Rec (Dict c :. f) rs
class RPureConstrained c ts where
- rpureConstrained :: (forall a. c a => f a) -> Rec f ts
data DictOnly (c :: k -> Constraint) a where
- DictOnly :: forall c a. c a => DictOnly c a
withPairedDict :: (c a => f a -> r) -> Product (DictOnly c) f a -> r
class RPureConstraints cs ts where
- rpureConstraints :: (forall a. AllSatisfied cs a => f a) -> Rec f ts
type family Head xs where ...
type family Tail xs where ...
type family AllRepsMatch_ (f :: j -> *) (xs :: [j]) (g :: k -> *) (ys :: [k]) :: Constraint where ...
type AllRepsMatch f xs g ys = (AllRepsMatch_ f xs g ys, AllRepsMatch_ g ys f xs)
repsMatchCoercion :: AllRepsMatch f xs g ys => Coercion (Rec f xs) (Rec g ys)
consMatchCoercion :: (forall (x :: k). Coercible (f x) (g x)) => Coercion (Rec f xs) (Rec g xs)

Documentation

data Rec :: (u -> *) -> [u] -> * where Source #

A record is parameterized by a universe u, an interpretation f and a list of rows rs. The labels or indices of the record are given by inhabitants of the kind u; the type of values at any label r :: u is given by its interpretation f r :: *.

Constructors

RNil :: Rec f '[]
(:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs) infixr 7

Instances

Instances details

RecSubset (Rec :: (k -> Type) -> [k] -> Type) ('[] :: [k]) (ss :: [k]) ('[] :: [Nat]) Source #
Instance details Defined in Data.Vinyl.Lens Associated Types type RecSubsetFCtx Rec f Source # Methods rsubsetC :: forall g (f :: k0 -> Type). (Functor g, RecSubsetFCtx Rec f) => (Rec f '[] -> g (Rec f '[])) -> Rec f ss -> g (Rec f ss) Source # rcastC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f ss -> Rec f '[] Source # rreplaceC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f '[] -> Rec f ss -> Rec f ss Source #
(RElem r ss i, RSubset rs ss is) => RecSubset (Rec :: (k -> Type) -> [k] -> Type) (r ': rs :: [k]) (ss :: [k]) (i ': is) Source #
Instance details Defined in Data.Vinyl.Lens Associated Types type RecSubsetFCtx Rec f Source # Methods rsubsetC :: forall g (f :: k0 -> Type). (Functor g, RecSubsetFCtx Rec f) => (Rec f (r ': rs) -> g (Rec f (r ': rs))) -> Rec f ss -> g (Rec f ss) Source # rcastC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f ss -> Rec f (r ': rs) Source # rreplaceC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f (r ': rs) -> Rec f ss -> Rec f ss Source #
RecElem (Rec :: (a -> Type) -> [a] -> Type) (r :: a) (r' :: a) (r ': rs :: [a]) (r' ': rs :: [a]) 'Z Source #
Instance details Defined in Data.Vinyl.Lens Associated Types type RecElemFCtx Rec f Source # Methods rlensC :: (Functor g, RecElemFCtx Rec f) => (f r -> g (f r')) -> Rec f (r ': rs) -> g (Rec f (r' ': rs)) Source # rgetC :: (RecElemFCtx Rec f, r ~ r') => Rec f (r ': rs) -> f r Source # rputC :: RecElemFCtx Rec f => f r' -> Rec f (r ': rs) -> Rec f (r' ': rs) Source #
(RIndex r (s ': rs) ~ 'S i, RecElem (Rec :: (a -> Type) -> [a] -> Type) r r' rs rs' i) => RecElem (Rec :: (a -> Type) -> [a] -> Type) (r :: a) (r' :: a) (s ': rs :: [a]) (s ': rs' :: [a]) ('S i) Source #
Instance details Defined in Data.Vinyl.Lens Associated Types type RecElemFCtx Rec f Source # Methods rlensC :: (Functor g, RecElemFCtx Rec f) => (f r -> g (f r')) -> Rec f (s ': rs) -> g (Rec f (s ': rs')) Source # rgetC :: (RecElemFCtx Rec f, r ~ r') => Rec f (s ': rs) -> f r Source # rputC :: RecElemFCtx Rec f => f r' -> Rec f (s ': rs) -> Rec f (s ': rs') Source #
TestCoercion f => TestCoercion (Rec f :: [u] -> Type) Source #
Instance details Defined in Data.Vinyl.Core Methods testCoercion :: forall (a :: k) (b :: k). Rec f a -> Rec f b -> Maybe (Coercion a b) #
TestEquality f => TestEquality (Rec f :: [u] -> Type) Source #
Instance details Defined in Data.Vinyl.Core Methods testEquality :: forall (a :: k) (b :: k). Rec f a -> Rec f b -> Maybe (a :~: b) #
(Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs)) Source #
Instance details Defined in Data.Vinyl.Core Methods (==) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool # (/=) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool #
Eq (Rec f ('[] :: [u])) Source #
Instance details Defined in Data.Vinyl.Core Methods (==) :: Rec f '[] -> Rec f '[] -> Bool # (/=) :: Rec f '[] -> Rec f '[] -> Bool #
(Ord (f r), Ord (Rec f rs)) => Ord (Rec f (r ': rs)) Source #
Instance details Defined in Data.Vinyl.Core Methods compare :: Rec f (r ': rs) -> Rec f (r ': rs) -> Ordering # (<) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool # (<=) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool # (>) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool # (>=) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool # max :: Rec f (r ': rs) -> Rec f (r ': rs) -> Rec f (r ': rs) # min :: Rec f (r ': rs) -> Rec f (r ': rs) -> Rec f (r ': rs) #
Ord (Rec f ('[] :: [u])) Source #
Instance details Defined in Data.Vinyl.Core Methods compare :: Rec f '[] -> Rec f '[] -> Ordering # (<) :: Rec f '[] -> Rec f '[] -> Bool # (<=) :: Rec f '[] -> Rec f '[] -> Bool # (>) :: Rec f '[] -> Rec f '[] -> Bool # (>=) :: Rec f '[] -> Rec f '[] -> Bool # max :: Rec f '[] -> Rec f '[] -> Rec f '[] # min :: Rec f '[] -> Rec f '[] -> Rec f '[] #
(RMap rs, ReifyConstraint Show f rs, RecordToList rs) => Show (Rec f rs) Source #	Records may be shown insofar as their points may be shown. `reifyConstraint` is used to great effect here.
Instance details Defined in Data.Vinyl.Core Methods showsPrec :: Int -> Rec f rs -> ShowS # show :: Rec f rs -> String # showList :: [Rec f rs] -> ShowS #
Generic (Rec f rs) => Generic (Rec f (r ': rs)) Source #
Instance details Defined in Data.Vinyl.Core Associated Types type Rep (Rec f (r ': rs)) :: Type -> Type # Methods from :: Rec f (r ': rs) -> Rep (Rec f (r ': rs)) x # to :: Rep (Rec f (r ': rs)) x -> Rec f (r ': rs) #
Generic (Rec f ('[] :: [u])) Source #
Instance details Defined in Data.Vinyl.Core Associated Types type Rep (Rec f '[]) :: Type -> Type # Methods from :: Rec f '[] -> Rep (Rec f '[]) x # to :: Rep (Rec f '[]) x -> Rec f '[] #
(Semigroup (f r), Semigroup (Rec f rs)) => Semigroup (Rec f (r ': rs)) Source #
Instance details Defined in Data.Vinyl.Core Methods (<>) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Rec f (r ': rs) # sconcat :: NonEmpty (Rec f (r ': rs)) -> Rec f (r ': rs) # stimes :: Integral b => b -> Rec f (r ': rs) -> Rec f (r ': rs) #
Semigroup (Rec f ('[] :: [u])) Source #
Instance details Defined in Data.Vinyl.Core Methods (<>) :: Rec f '[] -> Rec f '[] -> Rec f '[] # sconcat :: NonEmpty (Rec f '[]) -> Rec f '[] # stimes :: Integral b => b -> Rec f '[] -> Rec f '[] #
(Monoid (f r), Monoid (Rec f rs)) => Monoid (Rec f (r ': rs)) Source #
Instance details Defined in Data.Vinyl.Core Methods mempty :: Rec f (r ': rs) # mappend :: Rec f (r ': rs) -> Rec f (r ': rs) -> Rec f (r ': rs) # mconcat :: [Rec f (r ': rs)] -> Rec f (r ': rs) #
Monoid (Rec f ('[] :: [u])) Source #
Instance details Defined in Data.Vinyl.Core Methods mempty :: Rec f '[] # mappend :: Rec f '[] -> Rec f '[] -> Rec f '[] # mconcat :: [Rec f '[]] -> Rec f '[] #
(Storable (f r), Storable (Rec f rs)) => Storable (Rec f (r ': rs)) Source #
Instance details Defined in Data.Vinyl.Core Methods sizeOf :: Rec f (r ': rs) -> Int # alignment :: Rec f (r ': rs) -> Int # peekElemOff :: Ptr (Rec f (r ': rs)) -> Int -> IO (Rec f (r ': rs)) # pokeElemOff :: Ptr (Rec f (r ': rs)) -> Int -> Rec f (r ': rs) -> IO () # peekByteOff :: Ptr b -> Int -> IO (Rec f (r ': rs)) # pokeByteOff :: Ptr b -> Int -> Rec f (r ': rs) -> IO () # peek :: Ptr (Rec f (r ': rs)) -> IO (Rec f (r ': rs)) # poke :: Ptr (Rec f (r ': rs)) -> Rec f (r ': rs) -> IO () #
Storable (Rec f ('[] :: [u])) Source #
Instance details Defined in Data.Vinyl.Core Methods sizeOf :: Rec f '[] -> Int # alignment :: Rec f '[] -> Int # peekElemOff :: Ptr (Rec f '[]) -> Int -> IO (Rec f '[]) # pokeElemOff :: Ptr (Rec f '[]) -> Int -> Rec f '[] -> IO () # peekByteOff :: Ptr b -> Int -> IO (Rec f '[]) # pokeByteOff :: Ptr b -> Int -> Rec f '[] -> IO () # peek :: Ptr (Rec f '[]) -> IO (Rec f '[]) # poke :: Ptr (Rec f '[]) -> Rec f '[] -> IO () #
ReifyConstraint NFData f xs => NFData (Rec f xs) Source #
Instance details Defined in Data.Vinyl.Core Methods rnf :: Rec f xs -> () #
type RecSubsetFCtx (Rec :: (k -> Type) -> [k] -> Type) (f :: k -> Type) Source #
Instance details Defined in Data.Vinyl.Lens type RecSubsetFCtx (Rec :: (k -> Type) -> [k] -> Type) (f :: k -> Type) = ()
type RecSubsetFCtx (Rec :: (k -> Type) -> [k] -> Type) (f :: k -> Type) Source #
Instance details Defined in Data.Vinyl.Lens type RecSubsetFCtx (Rec :: (k -> Type) -> [k] -> Type) (f :: k -> Type) = ()
type RecElemFCtx (Rec :: (a -> Type) -> [a] -> Type) (f :: a -> Type) Source #
Instance details Defined in Data.Vinyl.Lens type RecElemFCtx (Rec :: (a -> Type) -> [a] -> Type) (f :: a -> Type) = ()
type RecElemFCtx (Rec :: (a -> Type) -> [a] -> Type) (f :: a -> Type) Source #
Instance details Defined in Data.Vinyl.Lens type RecElemFCtx (Rec :: (a -> Type) -> [a] -> Type) (f :: a -> Type) = ()
type Rep (Rec f (r ': rs)) Source #
Instance details Defined in Data.Vinyl.Core type Rep (Rec f (r ': rs)) = C1 ('MetaCons ":&" ('InfixI 'RightAssociative 7) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (f r)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rep (Rec f rs)))
type Rep (Rec f ('[] :: [u])) Source #
Instance details Defined in Data.Vinyl.Core type Rep (Rec f ('[] :: [u])) = C1 ('MetaCons "RNil" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (U1 :: Type -> Type))

rappend :: Rec f as -> Rec f bs -> Rec f (as ++ bs) Source #

Two records may be pasted together.

(<+>) :: Rec f as -> Rec f bs -> Rec f (as ++ bs) infixr 5 Source #

A shorthand for rappend.

rcombine :: (RMap rs, RApply rs) => (forall a. m a -> m a -> m a) -> (forall a. f a -> m a) -> (forall a. m a -> g a) -> Rec f rs -> Rec f rs -> Rec g rs Source #

Combine two records by combining their fields using the given function. The first argument is a binary operation for combining two values (e.g. (<>)), the second argument takes a record field into the type equipped with the desired operation, the third argument takes the combined value back to a result type.

class RMap rs where Source #

Rec _ rs with labels in kind u gives rise to a functor Hask^u -> Hask; that is, a natural transformation between two interpretation functors f,g may be used to transport a value from Rec f rs to Rec g rs.

Methods

rmap :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs Source #

Instances

Instances details

RMap ('[] :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods rmap :: (forall (x :: u0). f x -> g x) -> Rec f '[] -> Rec g '[] Source #
RMap xs => RMap (x ': xs :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods rmap :: (forall (x0 :: u0). f x0 -> g x0) -> Rec f (x ': xs) -> Rec g (x ': xs) Source #

(<<$>>) :: RMap rs => (forall x. f x -> g x) -> Rec f rs -> Rec g rs infixl 8 Source #

A shorthand for rmap.

(<<&>>) :: RMap rs => Rec f rs -> (forall x. f x -> g x) -> Rec g rs Source #

An inverted shorthand for rmap.

class RApply rs where Source #

A record of components f r -> g r may be applied to a record of f to get a record of g.

Methods

rapply :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs Source #

Instances

Instances details

RApply ('[] :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods rapply :: forall (f :: u0 -> Type) (g :: u0 -> Type). Rec (Lift (->) f g) '[] -> Rec f '[] -> Rec g '[] Source #
RApply xs => RApply (x ': xs :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods rapply :: forall (f :: u0 -> Type) (g :: u0 -> Type). Rec (Lift (->) f g) (x ': xs) -> Rec f (x ': xs) -> Rec g (x ': xs) Source #

(<<*>>) :: RApply rs => Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs infixl 8 Source #

A shorthand for rapply.

class RecApplicative rs where Source #

Given a section of some functor, records in that functor of any size are inhabited.

Methods

rpure :: (forall x. f x) -> Rec f rs Source #

Instances

Instances details

RecApplicative ('[] :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods rpure :: (forall (x :: u0). f x) -> Rec f '[] Source #
RecApplicative rs => RecApplicative (r ': rs :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods rpure :: (forall (x :: u0). f x) -> Rec f (r ': rs) Source #

rtraverse :: Applicative h => (forall x. f x -> h (g x)) -> Rec f rs -> h (Rec g rs) Source #

A record may be traversed with respect to its interpretation functor. This can be used to yank (some or all) effects from the fields of the record to the outside of the record.

rtraverseIn :: forall h f g rs. (forall a. f a -> g (ApplyToField h a)) -> Rec f rs -> Rec g (MapTyCon h rs) Source #

While rtraverse pulls the interpretation functor out of the record, rtraverseIn pushes the interpretation functor in to each field type. This is particularly useful when you wish to discharge that interpretation on a per-field basis. For instance, rather than a Rec IO '[a,b], you may wish to have a Rec Identity '[IO a, IO b] so that you can evaluate a single field to obtain a value of type Rec Identity '[a, IO b].

rsequenceIn :: forall f g (rs :: [Type]). (Traversable f, Applicative g) => Rec (f :. g) rs -> Rec g (MapTyCon f rs) Source #

Push an outer layer of interpretation functor into each field.

rzipWith :: (RMap xs, RApply xs) => (forall x. f x -> g x -> h x) -> Rec f xs -> Rec g xs -> Rec h xs Source #

Given a natural transformation from the product of f and g to h, we have a natural transformation from the product of Rec f and Rec g to Rec h. You can also think about this operation as zipping two records with the same element types but different interpretations.

class RFoldMap rs where Source #

Map each element of a record to a monoid and combine the results.

Methods

rfoldMapAux :: Monoid m => (forall x. f x -> m) -> m -> Rec f rs -> m Source #

Instances

Instances details

RFoldMap ('[] :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods rfoldMapAux :: Monoid m => (forall (x :: u0). f x -> m) -> m -> Rec f '[] -> m Source #
RFoldMap xs => RFoldMap (x ': xs :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods rfoldMapAux :: Monoid m => (forall (x0 :: u0). f x0 -> m) -> m -> Rec f (x ': xs) -> m Source #

rfoldMap :: forall rs m f. (Monoid m, RFoldMap rs) => (forall x. f x -> m) -> Rec f rs -> m Source #

class RecordToList rs where Source #

A record with uniform fields may be turned into a list.

Methods

recordToList :: Rec (Const a) rs -> [a] Source #

Instances

Instances details

RecordToList ('[] :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods recordToList :: Rec (Const a) '[] -> [a] Source #
RecordToList xs => RecordToList (x ': xs :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods recordToList :: Rec (Const a) (x ': xs) -> [a] Source #

data Dict c a where Source #

Wrap up a value with a capability given by its type

Constructors

Dict :: c a => a -> Dict c a

class ReifyConstraint c f rs where Source #

Sometimes we may know something for all fields of a record, but when you expect to be able to each of the fields, you are then out of luck. Surely given ∀x:u.φ(x) we should be able to recover x:u ⊢ φ(x)! Sadly, the constraint solver is not quite smart enough to realize this and we must make it patently obvious by reifying the constraint pointwise with proof.

Methods

reifyConstraint :: Rec f rs -> Rec (Dict c :. f) rs Source #

Instances

Instances details

ReifyConstraint c (f :: u -> Type) ('[] :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods reifyConstraint :: Rec f '[] -> Rec (Dict c :. f) '[] Source #
(c (f x), ReifyConstraint c f xs) => ReifyConstraint c (f :: a -> Type) (x ': xs :: [a]) Source #
Instance details Defined in Data.Vinyl.Core Methods reifyConstraint :: Rec f (x ': xs) -> Rec (Dict c :. f) (x ': xs) Source #

class RPureConstrained c ts where Source #

Build a record whose elements are derived solely from a constraint satisfied by each.

Methods

rpureConstrained :: (forall a. c a => f a) -> Rec f ts Source #

Instances

Instances details

RPureConstrained (c :: u -> Constraint) ('[] :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods rpureConstrained :: (forall (a :: u0). c a => f a) -> Rec f '[] Source #
(c x, RPureConstrained c xs) => RPureConstrained (c :: a -> Constraint) (x ': xs :: [a]) Source #
Instance details Defined in Data.Vinyl.Core Methods rpureConstrained :: (forall (a0 :: u). c a0 => f a0) -> Rec f (x ': xs) Source #

data DictOnly (c :: k -> Constraint) a where Source #

Capture a type class instance dictionary. See getDict for a way to obtain a DictOnly value from an RPureConstrained constraint.

Constructors

DictOnly :: forall c a. c a => DictOnly c a

withPairedDict :: (c a => f a -> r) -> Product (DictOnly c) f a -> r Source #

A useful technique is to use 'rmap (Pair (DictOnly MyClass))' on a Rec to pair each field with a type class dictionary forMyClass@. This helper can then be used to eliminate the original.

class RPureConstraints cs ts where Source #

Build a record whose elements are derived solely from a list of constraint constructors satisfied by each.

Methods

rpureConstraints :: (forall a. AllSatisfied cs a => f a) -> Rec f ts Source #

Instances

Instances details

RPureConstraints (cs :: k) ('[] :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods rpureConstraints :: (forall (a :: u0). AllSatisfied cs a => f a) -> Rec f '[] Source #
(AllSatisfied cs t, RPureConstraints cs ts) => RPureConstraints (cs :: k) (t ': ts :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods rpureConstraints :: (forall (a :: u0). AllSatisfied cs a => f a) -> Rec f (t ': ts) Source #

type family Head xs where ... Source #

Equations

Head (x ': _) = x

type family Tail xs where ... Source #

Equations

Tail (_ ': xs) = xs

type family AllRepsMatch_ (f :: j -> *) (xs :: [j]) (g :: k -> *) (ys :: [k]) :: Constraint where ... Source #

Equations

AllRepsMatch_ f (x ': xs) g ys = (ys ~ (Head ys ': Tail ys), Coercible (f x) (g (Head ys)), AllRepsMatch_ f xs g (Tail ys))
AllRepsMatch_ _ '[] _ ys = ys ~ '[]

type AllRepsMatch f xs g ys = (AllRepsMatch_ f xs g ys, AllRepsMatch_ g ys f xs) Source #

AllRepsMatch f xs g ys means that xs and ys have the same lengths, and that mapping f over xs and g over ys produces lists whose corresponding elements are Coercible with each other. For example, the following hold:

AllRepsMatch Proxy '[1,2,3] Proxy '[4,5,6] AllRepsMatch Sum '[Int,Word] Identity '[Min Int, Max Word]

repsMatchCoercion :: AllRepsMatch f xs g ys => Coercion (Rec f xs) (Rec g ys) Source #

Given that for each element x in the list xs,

consMatchCoercion :: (forall (x :: k). Coercible (f x) (g x)) => Coercion (Rec f xs) (Rec g xs) Source #