{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds  #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE GADTs      #-}
{-# LANGUAGE PolyKinds  #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeApplications #-}
-- | Commonly used 'Rec' instantiations.
module Data.Vinyl.Derived where

import Data.Proxy
import Data.Vinyl.ARec
import Data.Vinyl.Core
import Data.Vinyl.Functor
import Data.Vinyl.Lens
import Data.Vinyl.TypeLevel (Fst, Snd, RIndex)
import GHC.OverloadedLabels
import GHC.TypeLits

-- | Alias for Field spec
type a ::: b = '(a, b)

-- | A record of named fields.
type FieldRec = Rec ElField

-- | An 'ARec' of named fields to provide constant-time field access.
type AFieldRec ts = ARec ElField ts

-- | Heterogeneous list whose elements are evaluated during list
-- construction.
type HList = Rec Identity

-- | Heterogeneous list whose elements are left as-is during list
-- construction (cf. 'HList').
type LazyHList = Rec Thunk

-- | Get the data payload of an 'ElField'.
getField :: ElField '(s,t) -> t
getField :: ElField '(s, t) -> t
getField (Field Snd '(s, t)
x) = t
Snd '(s, t)
x

-- | Get the label name of an 'ElField'.
getLabel :: forall s t. KnownSymbol s => ElField '(s,t) -> String
getLabel :: ElField '(s, t) -> String
getLabel (Field Snd '(s, t)
_) = Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy s
forall k (t :: k). Proxy t
Proxy::Proxy s)

-- | 'ElField' is isomorphic to a functor something like @Compose
-- ElField ('(,) s)@.
fieldMap :: (a -> b) -> ElField '(s,a) -> ElField '(s,b)
fieldMap :: (a -> b) -> ElField '(s, a) -> ElField '(s, b)
fieldMap a -> b
f (Field Snd '(s, a)
x) = Snd '(s, b) -> ElField '(s, b)
forall (t :: (Symbol, *)). Snd t -> ElField t
Field (a -> b
f a
Snd '(s, a)
x)
{-# INLINE fieldMap #-}

-- | Something in the spirit of 'traverse' for 'ElField' whose kind
-- fights the standard library.
traverseField :: (KnownSymbol s, Functor f)
              => (a -> b) -> f (ElField '(s,a)) -> ElField '(s, f b)
traverseField :: (a -> b) -> f (ElField '(s, a)) -> ElField '(s, f b)
traverseField a -> b
f f (ElField '(s, a))
t = Snd '(s, f b) -> ElField '(s, f b)
forall (t :: (Symbol, *)). Snd t -> ElField t
Field ((ElField '(s, a) -> b) -> f (ElField '(s, a)) -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (a -> b
f (a -> b) -> (ElField '(s, a) -> a) -> ElField '(s, a) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ElField '(s, a) -> a
forall (s :: Symbol) t. ElField '(s, t) -> t
getField)  f (ElField '(s, a))
t)

-- | Lens for an 'ElField''s data payload.
rfield :: Functor f => (a -> f b) -> ElField '(s,a) -> f (ElField '(s,b))
rfield :: (a -> f b) -> ElField '(s, a) -> f (ElField '(s, b))
rfield a -> f b
f (Field Snd '(s, a)
x) = (b -> ElField '(s, b)) -> f b -> f (ElField '(s, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> ElField '(s, b)
forall (t :: (Symbol, *)). Snd t -> ElField t
Field (a -> f b
f a
Snd '(s, a)
x)
{-# INLINE rfield #-}

infix 8 =:

-- | Operator for creating an 'ElField'. With the @-XOverloadedLabels@
-- extension, this permits usage such as, @#foo =: 23@ to produce a
-- value of type @ElField ("foo" ::: Int)@.
(=:) :: KnownSymbol l => Label (l :: Symbol) -> (v :: *) -> ElField (l ::: v)
Label l
_ =: :: Label l -> v -> ElField (l ::: v)
=: v
v = Snd (l ::: v) -> ElField (l ::: v)
forall (t :: (Symbol, *)). Snd t -> ElField t
Field v
Snd (l ::: v)
v

-- | Get a named field from a record.
rgetf
  :: forall l f v record us.
     (HasField record l us us v v, RecElemFCtx record f)
  => Label l -> record f us -> f (l ::: v)
rgetf :: Label l -> record f us -> f (l ::: v)
rgetf Label l
_ = forall (rs :: [(Symbol, k)]) (f :: (Symbol, k) -> *)
       (record :: ((Symbol, k) -> *) -> [(Symbol, k)] -> *).
(RecElem record (l ::: v) (l ::: v) rs rs (RIndex (l ::: v) rs),
 RecElemFCtx record f) =>
record f rs -> f (l ::: v)
forall k (r :: k) (rs :: [k]) (f :: k -> *)
       (record :: (k -> *) -> [k] -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
rget @(l ::: v)

-- | Get the value associated with a named field from a record.
rvalf
  :: (HasField record l us us v v, RecElemFCtx record ElField)
  => Label l -> record ElField us -> v
rvalf :: Label l -> record ElField us -> v
rvalf Label l
x = ElField '(l, v) -> v
forall (s :: Symbol) t. ElField '(s, t) -> t
getField (ElField '(l, v) -> v)
-> (record ElField us -> ElField '(l, v)) -> record ElField us -> v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label l -> record ElField us -> ElField '(l, v)
forall k (l :: Symbol) (f :: (Symbol, k) -> *) (v :: k)
       (record :: ((Symbol, k) -> *) -> [(Symbol, k)] -> *)
       (us :: [(Symbol, k)]).
(HasField record l us us v v, RecElemFCtx record f) =>
Label l -> record f us -> f (l ::: v)
rgetf Label l
x

-- | Set a named field. @rputf' #foo 23@ sets the field named @#foo@ to
-- @23@.
rputf' :: forall l v v' record us us'.
          (HasField record l us us' v v', KnownSymbol l, RecElemFCtx record ElField)
       => Label l -> v' -> record ElField us -> record ElField us'
rputf' :: Label l -> v' -> record ElField us -> record ElField us'
rputf' Label l
_ = forall k (r :: k) (r' :: k) (rs :: [k]) (rs' :: [k])
       (record :: (k -> *) -> [k] -> *) (f :: k -> *).
(RecElem record r r' rs rs' (RIndex r rs), RecElemFCtx record f) =>
f r' -> record f rs -> record f rs'
forall (r' :: (Symbol, *)) (rs :: [(Symbol, *)])
       (rs' :: [(Symbol, *)])
       (record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *)
       (f :: (Symbol, *) -> *).
(RecElem record (l ::: v) r' rs rs' (RIndex (l ::: v) rs),
 RecElemFCtx record f) =>
f r' -> record f rs -> record f rs'
rput' @_ @(l:::v) (ElField '(l, v') -> record ElField us -> record ElField us')
-> (v' -> ElField '(l, v'))
-> v'
-> record ElField us
-> record ElField us'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v' -> ElField '(l, v')
forall (t :: (Symbol, *)). Snd t -> ElField t
Field :: v' -> ElField '(l,v'))

-- | Set a named field without changing its type. @rputf #foo 23@ sets
-- the field named @#foo@ to @23@.
rputf :: forall l v record us.
          (HasField record l us us v v, KnownSymbol l, RecElemFCtx record ElField)
       => Label l -> v -> record ElField us -> record ElField us
rputf :: Label l -> v -> record ElField us -> record ElField us
rputf Label l
_ = forall (rs :: [(Symbol, *)])
       (record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *)
       (f :: (Symbol, *) -> *).
(RecElem record (l ::: v) (l ::: v) rs rs (RIndex (l ::: v) rs),
 RecElemFCtx record f) =>
f (l ::: v) -> record f rs -> record f rs
forall k (r :: k) (rs :: [k]) (record :: (k -> *) -> [k] -> *)
       (f :: k -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
f r -> record f rs -> record f rs
rput @_ @(l:::v) (ElField (l ::: v) -> record ElField us -> record ElField us)
-> (v -> ElField (l ::: v))
-> v
-> record ElField us
-> record ElField us
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> ElField (l ::: v)
forall (t :: (Symbol, *)). Snd t -> ElField t
Field

-- | A lens into a 'Rec' identified by a 'Label'.
rlensfL' :: forall l v v' record g f us us'.
             (Functor g, HasField record l us us' v v', RecElemFCtx record f)
          => Label l
          -> (f (l ::: v) -> g (f (l ::: v')))
          -> record f us
          -> g (record f us')
rlensfL' :: Label l
-> (f (l ::: v) -> g (f (l ::: v')))
-> record f us
-> g (record f us')
rlensfL' Label l
_ f (l ::: v) -> g (f (l ::: v'))
f = (f (l ::: v) -> g (f (l ::: v')))
-> record f us -> g (record f us')
forall k (r :: k) (r' :: k) (record :: (k -> *) -> [k] -> *)
       (rs :: [k]) (rs' :: [k]) (f :: k -> *) (g :: * -> *).
(RecElem record r r' rs rs' (RIndex r rs), RecElemFCtx record f,
 Functor g) =>
(f r -> g (f r')) -> record f rs -> g (record f rs')
rlens' @(l ::: v) f (l ::: v) -> g (f (l ::: v'))
f

-- | A type-preserving lens into a 'Rec' identified by a 'Label'.
rlensfL :: forall l v record g f us.
           (Functor g, HasField record l us us v v, RecElemFCtx record f)
        => Label l
        -> (f (l ::: v) -> g (f (l ::: v)))
        -> record f us
        -> g (record f us)
rlensfL :: Label l
-> (f (l ::: v) -> g (f (l ::: v)))
-> record f us
-> g (record f us)
rlensfL Label l
_ f (l ::: v) -> g (f (l ::: v))
f = (f (l ::: v) -> g (f (l ::: v))) -> record f us -> g (record f us)
forall k (r :: k) (r' :: k) (record :: (k -> *) -> [k] -> *)
       (rs :: [k]) (rs' :: [k]) (f :: k -> *) (g :: * -> *).
(RecElem record r r' rs rs' (RIndex r rs), RecElemFCtx record f,
 Functor g) =>
(f r -> g (f r')) -> record f rs -> g (record f rs')
rlens' @(l ::: v) f (l ::: v) -> g (f (l ::: v))
f

-- | A lens into the payload value of a 'Rec' field identified by a
-- 'Label'.
rlensf' :: forall l v v' record g us us'.
           (Functor g, HasField record l us us' v v', RecElemFCtx record ElField)
        => Label l -> (v -> g v') -> record ElField us -> g (record ElField us')
rlensf' :: Label l
-> (v -> g v') -> record ElField us -> g (record ElField us')
rlensf' Label l
_ v -> g v'
f = (ElField (l ::: v) -> g (ElField '(l, v')))
-> record ElField us -> g (record ElField us')
forall k (r :: k) (r' :: k) (record :: (k -> *) -> [k] -> *)
       (rs :: [k]) (rs' :: [k]) (f :: k -> *) (g :: * -> *).
(RecElem record r r' rs rs' (RIndex r rs), RecElemFCtx record f,
 Functor g) =>
(f r -> g (f r')) -> record f rs -> g (record f rs')
rlens' @(l ::: v) ((v -> g v') -> ElField (l ::: v) -> g (ElField '(l, v'))
forall (f :: * -> *) a b (s :: Symbol).
Functor f =>
(a -> f b) -> ElField '(s, a) -> f (ElField '(s, b))
rfield v -> g v'
f)

-- | A type-preserving lens into the payload value of a 'Rec' field
-- identified by a 'Label'.
rlensf :: forall l v record g us.
          (Functor g, HasField record l us us v v, RecElemFCtx record ElField)
        => Label l -> (v -> g v) -> record ElField us -> g (record ElField us)
rlensf :: Label l -> (v -> g v) -> record ElField us -> g (record ElField us)
rlensf Label l
_ v -> g v
f = (ElField (l ::: v) -> g (ElField (l ::: v)))
-> record ElField us -> g (record ElField us)
forall k (r :: k) (record :: (k -> *) -> [k] -> *) (rs :: [k])
       (f :: k -> *) (g :: * -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f,
 Functor g) =>
(f r -> g (f r)) -> record f rs -> g (record f rs)
rlens @(l ::: v) ((v -> g v) -> ElField (l ::: v) -> g (ElField (l ::: v))
forall (f :: * -> *) a b (s :: Symbol).
Functor f =>
(a -> f b) -> ElField '(s, a) -> f (ElField '(s, b))
rfield v -> g v
f)

-- | Shorthand for a 'FieldRec' with a single field.
(=:=) :: KnownSymbol s => Label (s :: Symbol) -> a -> FieldRec '[ '(s,a) ]
=:= :: Label s -> a -> FieldRec '[ '(s, a)]
(=:=) Label s
_ a
x = Snd '(s, a) -> ElField '(s, a)
forall (t :: (Symbol, *)). Snd t -> ElField t
Field a
Snd '(s, a)
x ElField '(s, a) -> Rec ElField '[] -> FieldRec '[ '(s, a)]
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& Rec ElField '[]
forall u (f :: u -> *). Rec f '[]
RNil

-- | A proxy for field types.
data SField (field :: k) = SField

instance Eq (SField a) where SField a
_ == :: SField a -> SField a -> Bool
== SField a
_ = Bool
True
instance Ord (SField a) where compare :: SField a -> SField a -> Ordering
compare SField a
_ SField a
_ = Ordering
EQ
instance KnownSymbol s => Show (SField '(s,t)) where
  show :: SField '(s, t) -> String
show SField '(s, t)
_ = String
"SField "String -> ShowS
forall a. [a] -> [a] -> [a]
++Proxy s -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy s
forall k (t :: k). Proxy t
Proxy::Proxy s)

type family FieldType l fs where
  FieldType l '[] = TypeError ('Text "Cannot find label "
                               ':<>: 'ShowType l
                               ':<>: 'Text " in fields")
  FieldType l ((l ::: v) ': fs) = v
  FieldType l ((l' ::: v') ': fs) = FieldType l fs

-- | Constraint that a label is associated with a particular type in a
-- record.
type HasField record l fs fs' v v' =
  (RecElem record (l ::: v) (l ::: v') fs fs' (RIndex (l ::: v) fs), FieldType l fs ~ v, FieldType l fs' ~ v')

-- | Proxy for label type
data Label (a :: Symbol) = Label
  deriving (Label a -> Label a -> Bool
(Label a -> Label a -> Bool)
-> (Label a -> Label a -> Bool) -> Eq (Label a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (a :: Symbol). Label a -> Label a -> Bool
/= :: Label a -> Label a -> Bool
$c/= :: forall (a :: Symbol). Label a -> Label a -> Bool
== :: Label a -> Label a -> Bool
$c== :: forall (a :: Symbol). Label a -> Label a -> Bool
Eq, Int -> Label a -> ShowS
[Label a] -> ShowS
Label a -> String
(Int -> Label a -> ShowS)
-> (Label a -> String) -> ([Label a] -> ShowS) -> Show (Label a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (a :: Symbol). Int -> Label a -> ShowS
forall (a :: Symbol). [Label a] -> ShowS
forall (a :: Symbol). Label a -> String
showList :: [Label a] -> ShowS
$cshowList :: forall (a :: Symbol). [Label a] -> ShowS
show :: Label a -> String
$cshow :: forall (a :: Symbol). Label a -> String
showsPrec :: Int -> Label a -> ShowS
$cshowsPrec :: forall (a :: Symbol). Int -> Label a -> ShowS
Show)

instance s ~ s' => IsLabel s (Label s') where
#if __GLASGOW_HASKELL__ < 802
  fromLabel _ = Label
#else
  fromLabel :: Label s'
fromLabel = Label s'
forall (a :: Symbol). Label a
Label
#endif

-- | Defines a constraint that lets us extract the label from an
-- 'ElField'. Used in 'rmapf' and 'rpuref'.
class (KnownSymbol (Fst a), a ~ '(Fst a, Snd a)) => KnownField a where
instance KnownSymbol l => KnownField (l ::: v) where

-- | Shorthand for working with records of fields as in 'rmapf' and
-- 'rpuref'.
type AllFields fs = (RPureConstrained KnownField fs, RecApplicative fs, RApply fs)

-- | Map a function between functors across a 'Rec' taking advantage
-- of knowledge that each element is an 'ElField'.
rmapf :: AllFields fs
      => (forall a. KnownField a => f a -> g a)
      -> Rec f fs -> Rec g fs
rmapf :: (forall (a :: (Symbol, k)). KnownField a => f a -> g a)
-> Rec f fs -> Rec g fs
rmapf forall (a :: (Symbol, k)). KnownField a => f a -> g a
f = ((forall (a :: (Symbol, k)). KnownField a => Lift (->) f g a)
-> Rec (Lift (->) f g) fs
forall u (c :: u -> Constraint) (ts :: [u]) (f :: u -> *).
RPureConstrained c ts =>
(forall (a :: u). c a => f a) -> Rec f ts
rpureConstrained @KnownField ((f a -> g a) -> Lift (->) f g a
forall l l' k (op :: l -> l' -> *) (f :: k -> l) (g :: k -> l')
       (x :: k).
op (f x) (g x) -> Lift op f g x
Lift f a -> g a
forall (a :: (Symbol, k)). KnownField a => f a -> g a
f) Rec (Lift (->) f g) fs -> Rec f fs -> Rec g fs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RApply rs =>
Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
<<*>>)

-- | Remove the first component (e.g. the label) from a type-level
-- list of pairs.
type family Unlabeled ts where
  Unlabeled '[] = '[]
  Unlabeled ('(s,x) ': xs) = x ': Unlabeled xs

-- | Facilities for removing and replacing the type-level label, or
-- column name, part of a record.
class StripFieldNames ts where
  stripNames :: Rec ElField ts -> Rec Identity (Unlabeled ts)
  stripNames' :: Functor f => Rec (f :. ElField) ts -> Rec f (Unlabeled ts)
  withNames :: Rec Identity (Unlabeled ts) -> Rec ElField ts
  withNames' :: Functor f => Rec f (Unlabeled ts) -> Rec (f :. ElField) ts

instance StripFieldNames '[] where
  stripNames :: Rec ElField '[] -> Rec Identity (Unlabeled '[])
stripNames Rec ElField '[]
RNil = Rec Identity (Unlabeled '[])
forall u (f :: u -> *). Rec f '[]
RNil
  stripNames' :: Rec (f :. ElField) '[] -> Rec f (Unlabeled '[])
stripNames' Rec (f :. ElField) '[]
RNil = Rec f (Unlabeled '[])
forall u (f :: u -> *). Rec f '[]
RNil
  withNames :: Rec Identity (Unlabeled '[]) -> Rec ElField '[]
withNames Rec Identity (Unlabeled '[])
RNil = Rec ElField '[]
forall u (f :: u -> *). Rec f '[]
RNil
  withNames' :: Rec f (Unlabeled '[]) -> Rec (f :. ElField) '[]
withNames' Rec f (Unlabeled '[])
RNil = Rec (f :. ElField) '[]
forall u (f :: u -> *). Rec f '[]
RNil

instance (KnownSymbol s, StripFieldNames ts) => StripFieldNames ('(s,t) ': ts) where
  stripNames :: Rec ElField ('(s, t) : ts)
-> Rec Identity (Unlabeled ('(s, t) : ts))
stripNames (Field Snd r
x :& Rec ElField rs
xs) = t -> Identity t
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
Snd r
x Identity t
-> Rec Identity (Unlabeled ts) -> Rec Identity (t : Unlabeled ts)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& Rec ElField rs -> Rec Identity (Unlabeled rs)
forall (ts :: [(Symbol, *)]).
StripFieldNames ts =>
Rec ElField ts -> Rec Identity (Unlabeled ts)
stripNames Rec ElField rs
xs
  stripNames' :: Rec (f :. ElField) ('(s, t) : ts)
-> Rec f (Unlabeled ('(s, t) : ts))
stripNames' (Compose f (ElField r)
x :& Rec (f :. ElField) rs
xs) = (ElField '(s, t) -> t) -> f (ElField '(s, t)) -> f t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ElField '(s, t) -> t
forall (s :: Symbol) t. ElField '(s, t) -> t
getField f (ElField r)
f (ElField '(s, t))
x f t -> Rec f (Unlabeled ts) -> Rec f (t : Unlabeled ts)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& Rec (f :. ElField) rs -> Rec f (Unlabeled rs)
forall (ts :: [(Symbol, *)]) (f :: * -> *).
(StripFieldNames ts, Functor f) =>
Rec (f :. ElField) ts -> Rec f (Unlabeled ts)
stripNames' Rec (f :. ElField) rs
xs
  withNames :: Rec Identity (Unlabeled ('(s, t) : ts))
-> Rec ElField ('(s, t) : ts)
withNames (Identity r
x :& Rec Identity rs
xs) = Snd '(s, t) -> ElField '(s, t)
forall (t :: (Symbol, *)). Snd t -> ElField t
Field r
Snd '(s, t)
x ElField '(s, t) -> Rec ElField ts -> Rec ElField ('(s, t) : ts)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& Rec Identity (Unlabeled ts) -> Rec ElField ts
forall (ts :: [(Symbol, *)]).
StripFieldNames ts =>
Rec Identity (Unlabeled ts) -> Rec ElField ts
withNames Rec Identity rs
Rec Identity (Unlabeled ts)
xs
  withNames' :: Rec f (Unlabeled ('(s, t) : ts))
-> Rec (f :. ElField) ('(s, t) : ts)
withNames' (f r
x :& Rec f rs
xs) = f (ElField '(s, t)) -> Compose f ElField '(s, t)
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose ((r -> ElField '(s, t)) -> f r -> f (ElField '(s, t))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap r -> ElField '(s, t)
forall (t :: (Symbol, *)). Snd t -> ElField t
Field f r
x) Compose f ElField '(s, t)
-> Rec (f :. ElField) ts -> Rec (f :. ElField) ('(s, t) : ts)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& Rec f (Unlabeled ts) -> Rec (f :. ElField) ts
forall (ts :: [(Symbol, *)]) (f :: * -> *).
(StripFieldNames ts, Functor f) =>
Rec f (Unlabeled ts) -> Rec (f :. ElField) ts
withNames' Rec f rs
Rec f (Unlabeled ts)
xs

-- | Construct a 'Rec' with 'ElField' elements.
rpuref :: AllFields fs => (forall a. KnownField a => f a) -> Rec f fs
rpuref :: (forall (a :: (Symbol, k)). KnownField a => f a) -> Rec f fs
rpuref forall (a :: (Symbol, k)). KnownField a => f a
f = (forall (a :: (Symbol, k)). KnownField a => f a) -> Rec f fs
forall u (c :: u -> Constraint) (ts :: [u]) (f :: u -> *).
RPureConstrained c ts =>
(forall (a :: u). c a => f a) -> Rec f ts
rpureConstrained @KnownField forall (a :: (Symbol, k)). KnownField a => f a
f

-- | Operator synonym for 'rmapf'.
(<<$$>>)
  :: AllFields fs
  => (forall a. KnownField a => f a -> g a) -> Rec f fs -> Rec g fs
<<$$>> :: (forall (a :: (Symbol, k)). KnownField a => f a -> g a)
-> Rec f fs -> Rec g fs
(<<$$>>) = (forall (a :: (Symbol, k)). KnownField a => f a -> g a)
-> Rec f fs -> Rec g fs
forall k (fs :: [(Symbol, k)]) (f :: (Symbol, k) -> *)
       (g :: (Symbol, k) -> *).
AllFields fs =>
(forall (a :: (Symbol, k)). KnownField a => f a -> g a)
-> Rec f fs -> Rec g fs
rmapf

-- | Produce a 'Rec' of the labels of a 'Rec' of 'ElField's.
rlabels :: AllFields fs => Rec (Const String) fs
rlabels :: Rec (Const String) fs
rlabels = (forall (a :: (Symbol, k)). KnownField a => Const String a)
-> Rec (Const String) fs
forall k (fs :: [(Symbol, k)]) (f :: (Symbol, k) -> *).
AllFields fs =>
(forall (a :: (Symbol, k)). KnownField a => f a) -> Rec f fs
rpuref forall k (l :: Symbol) (v :: k).
KnownSymbol l =>
Const String (l ::: v)
forall (a :: (Symbol, k)). KnownField a => Const String a
getLabel'
  where getLabel' :: forall l v. KnownSymbol l
                  => Const String (l ::: v)
        getLabel' :: Const String (l ::: v)
getLabel' = String -> Const String (l ::: v)
forall k a (b :: k). a -> Const a b
Const (Proxy l -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy l
forall k (t :: k). Proxy t
Proxy::Proxy l))

-- * Specializations for working with an 'ARec' of named fields.