{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE CPP                   #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

{-| This module uses 'RecAll' to extend common typeclass methods to records.
    Generally, it is preferable to use the original typeclass methods to these
    variants. For example, in most places where 'recCompare' could be used,
    you could use 'compare' instead. They are useful in scenarios
    that involve working on unknown subsets of a record's fields
    because 'RecAll' constraints can easily be weakened. An example of this
    is given at the bottom of this page.
-}

module Data.Vinyl.Class.Method
  ( -- * Mapping methods over records
    RecMapMethod(..)
  , rmapMethodF
  , mapFields
  , RecMapMethod1(..)
  , RecPointed(..)
  , rtraverseInMethod
  , rsequenceInFields
    -- * Support for 'RecMapMethod'
  , FieldTyper, ApplyFieldTyper, PayloadType
    -- * Eq Functions
  ,  recEq
     -- * Ord Functions
  , recCompare
    -- * Monoid Functions
  , recMempty
  , recMappend
  , recMconcat
    -- * Num Functions
  , recAdd
  , recSubtract
  , recMultiply
  , recAbs
  , recSignum
  , recNegate
    -- * Bounded Functions
  , recMinBound
  , recMaxBound
    -- * Example
    -- $example
  ) where
import Data.Functor.Product (Product(Pair))
import Data.Vinyl.Core
import Data.Vinyl.Derived (KnownField, AllFields, FieldRec, traverseField)
import Data.Vinyl.Functor ((:.), getCompose, ElField(..))
import Data.Vinyl.TypeLevel
#if __GLASGOW_HASKELL__ < 804
import Data.Monoid
#endif

recEq :: RecAll f rs Eq => Rec f rs -> Rec f rs -> Bool
recEq :: forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Eq =>
Rec f rs -> Rec f rs -> Bool
recEq Rec f rs
RNil Rec f rs
RNil = Bool
True
recEq (f r
a :& Rec f rs
as) (f r
b :& Rec f rs
bs) = f r
a forall a. Eq a => a -> a -> Bool
== f r
b Bool -> Bool -> Bool
&& forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Eq =>
Rec f rs -> Rec f rs -> Bool
recEq Rec f rs
as Rec f rs
bs

recCompare :: RecAll f rs Ord => Rec f rs -> Rec f rs -> Ordering
recCompare :: forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Ord =>
Rec f rs -> Rec f rs -> Ordering
recCompare Rec f rs
RNil Rec f rs
RNil = Ordering
EQ
recCompare (f r
a :& Rec f rs
as) (f r
b :& Rec f rs
bs) = forall a. Ord a => a -> a -> Ordering
compare f r
a f r
b forall a. Semigroup a => a -> a -> a
<> forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Ord =>
Rec f rs -> Rec f rs -> Ordering
recCompare Rec f rs
as Rec f rs
bs

-- | This function differs from the original 'mempty' in that
--   it takes an argument. In some cases, you will already
--   have a record of the type you are interested in, and
--   that can be passed an the argument. In other situations
--   where this is not the case, you may need the
--   interpretation function of the argument record to be
--   @Const ()@ or @Proxy@ so the you can generate the
--   argument with 'rpure'.
recMempty :: RecAll f rs Monoid => Rec proxy rs -> Rec f rs
recMempty :: forall {u} (f :: u -> *) (rs :: [u]) (proxy :: u -> *).
RecAll f rs Monoid =>
Rec proxy rs -> Rec f rs
recMempty Rec proxy rs
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
recMempty (proxy r
_ :& Rec proxy rs
rs) = forall a. Monoid a => a
mempty forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (f :: u -> *) (rs :: [u]) (proxy :: u -> *).
RecAll f rs Monoid =>
Rec proxy rs -> Rec f rs
recMempty Rec proxy rs
rs

recMappend :: RecAll f rs Monoid => Rec f rs -> Rec f rs -> Rec f rs
recMappend :: forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Monoid =>
Rec f rs -> Rec f rs -> Rec f rs
recMappend Rec f rs
RNil Rec f rs
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
recMappend (f r
a :& Rec f rs
as) (f r
b :& Rec f rs
bs) = forall a. Monoid a => a -> a -> a
mappend f r
a f r
b forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Monoid =>
Rec f rs -> Rec f rs -> Rec f rs
recMappend Rec f rs
as Rec f rs
bs

-- | This function differs from the original 'mconcat'.
--   See 'recMempty'.
recMconcat :: RecAll f rs Monoid => Rec proxy rs -> [Rec f rs] -> Rec f rs
recMconcat :: forall {u} (f :: u -> *) (rs :: [u]) (proxy :: u -> *).
RecAll f rs Monoid =>
Rec proxy rs -> [Rec f rs] -> Rec f rs
recMconcat Rec proxy rs
p [] = forall {u} (f :: u -> *) (rs :: [u]) (proxy :: u -> *).
RecAll f rs Monoid =>
Rec proxy rs -> Rec f rs
recMempty Rec proxy rs
p
recMconcat Rec proxy rs
p (Rec f rs
rec : [Rec f rs]
recs) = forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Monoid =>
Rec f rs -> Rec f rs -> Rec f rs
recMappend Rec f rs
rec (forall {u} (f :: u -> *) (rs :: [u]) (proxy :: u -> *).
RecAll f rs Monoid =>
Rec proxy rs -> [Rec f rs] -> Rec f rs
recMconcat Rec proxy rs
p [Rec f rs]
recs)

recAdd :: RecAll f rs Num => Rec f rs -> Rec f rs -> Rec f rs
recAdd :: forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Num =>
Rec f rs -> Rec f rs -> Rec f rs
recAdd Rec f rs
RNil Rec f rs
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
recAdd (f r
a :& Rec f rs
as) (f r
b :& Rec f rs
bs) = (f r
a forall a. Num a => a -> a -> a
+ f r
b) forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Num =>
Rec f rs -> Rec f rs -> Rec f rs
recAdd Rec f rs
as Rec f rs
bs

recSubtract :: RecAll f rs Num => Rec f rs -> Rec f rs -> Rec f rs
recSubtract :: forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Num =>
Rec f rs -> Rec f rs -> Rec f rs
recSubtract Rec f rs
RNil Rec f rs
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
recSubtract (f r
a :& Rec f rs
as) (f r
b :& Rec f rs
bs) = (f r
a forall a. Num a => a -> a -> a
- f r
b) forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Num =>
Rec f rs -> Rec f rs -> Rec f rs
recSubtract Rec f rs
as Rec f rs
bs

recMultiply :: RecAll f rs Num => Rec f rs -> Rec f rs -> Rec f rs
recMultiply :: forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Num =>
Rec f rs -> Rec f rs -> Rec f rs
recMultiply Rec f rs
RNil Rec f rs
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
recMultiply (f r
a :& Rec f rs
as) (f r
b :& Rec f rs
bs) = (f r
a forall a. Num a => a -> a -> a
* f r
b) forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Num =>
Rec f rs -> Rec f rs -> Rec f rs
recSubtract Rec f rs
as Rec f rs
bs

recAbs :: RecAll f rs Num => Rec f rs -> Rec f rs
recAbs :: forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Num =>
Rec f rs -> Rec f rs
recAbs Rec f rs
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
recAbs (f r
a :& Rec f rs
as) = forall a. Num a => a -> a
abs f r
a forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Num =>
Rec f rs -> Rec f rs
recAbs Rec f rs
as

recSignum :: RecAll f rs Num => Rec f rs -> Rec f rs
recSignum :: forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Num =>
Rec f rs -> Rec f rs
recSignum Rec f rs
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
recSignum (f r
a :& Rec f rs
as) = forall a. Num a => a -> a
signum f r
a forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Num =>
Rec f rs -> Rec f rs
recAbs Rec f rs
as

recNegate :: RecAll f rs Num => Rec f rs -> Rec f rs
recNegate :: forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Num =>
Rec f rs -> Rec f rs
recNegate Rec f rs
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
recNegate (f r
a :& Rec f rs
as) = forall a. Num a => a -> a
negate f r
a forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (f :: u -> *) (rs :: [u]).
RecAll f rs Num =>
Rec f rs -> Rec f rs
recAbs Rec f rs
as

-- | This function differs from the original 'minBound'.
--   See 'recMempty'.
recMinBound :: RecAll f rs Bounded => Rec proxy rs -> Rec f rs
recMinBound :: forall {u} (f :: u -> *) (rs :: [u]) (proxy :: u -> *).
RecAll f rs Bounded =>
Rec proxy rs -> Rec f rs
recMinBound Rec proxy rs
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
recMinBound (proxy r
_ :& Rec proxy rs
rs) = forall a. Bounded a => a
minBound forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (f :: u -> *) (rs :: [u]) (proxy :: u -> *).
RecAll f rs Bounded =>
Rec proxy rs -> Rec f rs
recMinBound Rec proxy rs
rs

-- | This function differs from the original 'maxBound'.
--   See 'recMempty'.
recMaxBound :: RecAll f rs Bounded => Rec proxy rs -> Rec f rs
recMaxBound :: forall {u} (f :: u -> *) (rs :: [u]) (proxy :: u -> *).
RecAll f rs Bounded =>
Rec proxy rs -> Rec f rs
recMaxBound Rec proxy rs
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
recMaxBound (proxy r
_ :& Rec proxy rs
rs) = forall a. Bounded a => a
maxBound forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (f :: u -> *) (rs :: [u]) (proxy :: u -> *).
RecAll f rs Bounded =>
Rec proxy rs -> Rec f rs
recMaxBound Rec proxy rs
rs

-- | When we wish to apply a typeclass method to each field of a
-- 'Rec', we typically care about typeclass instances of the record
-- field types irrespective of the record's functor context. To expose
-- the field types themselves, we utilize a constraint built from a
-- defunctionalized type family in the 'rmapMethod' method. The
-- symbols of the function space are defined by this data type.
data FieldTyper = FieldId | FieldSnd

-- | The interpretation function of the 'FieldTyper' symbols.
type family ApplyFieldTyper (f :: FieldTyper) (a :: k) :: * where
  ApplyFieldTyper 'FieldId a = a
  ApplyFieldTyper 'FieldSnd a = Snd a

-- | A mapping of record contexts into the 'FieldTyper' function
-- space. We explicitly match on 'ElField' to pick out the payload
-- type, and 'Compose' to pick out the inner-most context. All other
-- type constructor contexts are understood to not perform any
-- computation on their arguments.
type family FieldPayload (f :: u -> *) :: FieldTyper where
  FieldPayload ElField = 'FieldSnd
  FieldPayload (f :. g) = FieldPayload g
  FieldPayload f = 'FieldId

-- | Shorthand for combining 'ApplyFieldTyper' and 'FieldPayload'.
type family PayloadType f (a :: u) :: * where
  PayloadType f a = ApplyFieldTyper (FieldPayload f) a

-- | Generate a record from fields derived from type class
-- instances.
class RecPointed c f ts where
  rpointMethod :: (forall a. c (f a) => f a) -> Rec f ts

instance RecPointed c f '[] where
  rpointMethod :: (forall (a :: u). c (f a) => f a) -> Rec f '[]
rpointMethod forall (a :: u). c (f a) => f a
_ = forall {u} (f :: u -> *). Rec f '[]
RNil
  {-# INLINE rpointMethod #-}

instance (c (f t), RecPointed c f ts)
  => RecPointed c f (t ': ts) where
  rpointMethod :: (forall (a :: a). c (f a) => f a) -> Rec f (t : ts)
rpointMethod forall (a :: a). c (f a) => f a
f = forall (a :: a). c (f a) => f a
f forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (c :: * -> Constraint) (f :: u -> *) (ts :: [u]).
RecPointed c f ts =>
(forall (a :: u). c (f a) => f a) -> Rec f ts
rpointMethod @c forall (a :: a). c (f a) => f a
f
  {-# INLINE rpointMethod #-}

-- | Apply a typeclass method to each field of a 'Rec' where the class
-- constrains the index of the field, but not its interpretation
-- functor.
class RecMapMethod c f ts where
  rmapMethod :: (forall a. c (PayloadType f a) => f a -> g a)
             -> Rec f ts -> Rec g ts

-- | Apply a typeclass method to each field of a 'Rec' where the class
-- constrains the field when considered as a value interpreted by the
-- record's interpretation functor.
class RecMapMethod1 c f ts where
  rmapMethod1 :: (forall a. c (f a) => f a -> g a)
              -> Rec f ts -> Rec g ts

instance RecMapMethod c f '[] where
  rmapMethod :: forall (g :: u -> *).
(forall (a :: u). c (PayloadType f a) => f a -> g a)
-> Rec f '[] -> Rec g '[]
rmapMethod forall (a :: u). c (PayloadType f a) => f a -> g a
_ Rec f '[]
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
  {-# INLINE rmapMethod #-}

instance RecMapMethod1 c f '[] where
  rmapMethod1 :: forall (g :: u -> *).
(forall (a :: u). c (f a) => f a -> g a) -> Rec f '[] -> Rec g '[]
rmapMethod1 forall (a :: u). c (f a) => f a -> g a
_ Rec f '[]
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
  {-# INLINE rmapMethod1 #-}

instance (c (PayloadType f t), RecMapMethod c f ts)
  => RecMapMethod c f (t ': ts) where
  rmapMethod :: forall (g :: a -> *).
(forall (a :: a). c (PayloadType f a) => f a -> g a)
-> Rec f (t : ts) -> Rec g (t : ts)
rmapMethod forall (a :: a). c (PayloadType f a) => f a -> g a
f (f r
x :& Rec f rs
xs) = forall (a :: a). c (PayloadType f a) => f a -> g a
f f r
x forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (c :: * -> Constraint) (f :: u -> *) (ts :: [u])
       (g :: u -> *).
RecMapMethod c f ts =>
(forall (a :: u). c (PayloadType f a) => f a -> g a)
-> Rec f ts -> Rec g ts
rmapMethod @c forall (a :: a). c (PayloadType f a) => f a -> g a
f Rec f rs
xs
  {-# INLINE rmapMethod #-}

instance (c (f t), RecMapMethod1 c f ts) => RecMapMethod1 c f (t ': ts) where
  rmapMethod1 :: forall (g :: a -> *).
(forall (a :: a). c (f a) => f a -> g a)
-> Rec f (t : ts) -> Rec g (t : ts)
rmapMethod1 forall (a :: a). c (f a) => f a -> g a
f (f r
x :& Rec f rs
xs) = forall (a :: a). c (f a) => f a -> g a
f f r
x forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {u} (c :: * -> Constraint) (f :: u -> *) (ts :: [u])
       (g :: u -> *).
RecMapMethod1 c f ts =>
(forall (a :: u). c (f a) => f a -> g a) -> Rec f ts -> Rec g ts
rmapMethod1 @c forall (a :: a). c (f a) => f a -> g a
f Rec f rs
xs
  {-# INLINE rmapMethod1 #-}

-- | Apply a typeclass method to each field of a @Rec f ts@ using the
-- 'Functor' instance for @f@ to lift the function into the
-- functor. This is a commonly-used specialization of 'rmapMethod'
-- composed with 'fmap'.
rmapMethodF :: forall c f ts. (Functor f, FieldPayload f ~ 'FieldId, RecMapMethod c f ts)
            => (forall a. c a => a -> a) -> Rec f ts -> Rec f ts
rmapMethodF :: forall (c :: * -> Constraint) (f :: * -> *) (ts :: [*]).
(Functor f, FieldPayload f ~ 'FieldId, RecMapMethod c f ts) =>
(forall a. c a => a -> a) -> Rec f ts -> Rec f ts
rmapMethodF forall a. c a => a -> a
f = forall {u} (c :: * -> Constraint) (f :: u -> *) (ts :: [u])
       (g :: u -> *).
RecMapMethod c f ts =>
(forall (a :: u). c (PayloadType f a) => f a -> g a)
-> Rec f ts -> Rec g ts
rmapMethod @c (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. c a => a -> a
f)
{-# INLINE rmapMethodF #-}

-- | Apply a typeclass method to each field of a 'FieldRec'. This is a
-- specialization of 'rmapMethod'.
mapFields :: forall c ts. RecMapMethod c ElField ts
           => (forall a. c a => a -> a) -> FieldRec ts -> FieldRec ts
mapFields :: forall (c :: * -> Constraint) (ts :: [(Symbol, *)]).
RecMapMethod c ElField ts =>
(forall a. c a => a -> a) -> FieldRec ts -> FieldRec ts
mapFields forall a. c a => a -> a
f = forall {u} (c :: * -> Constraint) (f :: u -> *) (ts :: [u])
       (g :: u -> *).
RecMapMethod c f ts =>
(forall (a :: u). c (PayloadType f a) => f a -> g a)
-> Rec f ts -> Rec g ts
rmapMethod @c forall (t :: (Symbol, *)).
c (PayloadType ElField t) =>
ElField t -> ElField t
g
  where g :: c (PayloadType ElField t) => ElField t -> ElField t
        g :: forall (t :: (Symbol, *)).
c (PayloadType ElField t) =>
ElField t -> ElField t
g (Field Snd t
x) = forall (t :: (Symbol, *)). Snd t -> ElField t
Field (forall a. c a => a -> a
f Snd t
x)
{-# INLINE mapFields #-}

-- | Like 'rtraverseIn', but the function between functors may be
-- constrained.
rtraverseInMethod :: forall c h f g rs.
                     (RMap rs, RPureConstrained c rs, RApply rs)
                  => (forall a. c a => f a -> g (ApplyToField h a))
                  -> Rec f rs
                  -> Rec g (MapTyCon h rs)
rtraverseInMethod :: forall {u} (c :: u -> Constraint) (h :: * -> *) (f :: u -> *)
       (g :: u -> *) (rs :: [u]).
(RMap rs, RPureConstrained c rs, RApply rs) =>
(forall (a :: u). c a => f a -> g (ApplyToField h a))
-> Rec f rs -> Rec g (MapTyCon h rs)
rtraverseInMethod forall (a :: u). c a => f a -> g (ApplyToField h a)
f = forall {u} (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (a :: u). f a -> g (ApplyToField h a))
-> Rec f rs -> Rec g (MapTyCon h rs)
rtraverseIn @h (forall {k} (c :: k -> Constraint) (a :: k) (f :: k -> *) r.
(c a => f a -> r) -> Product (DictOnly c) f a -> r
withPairedDict @c forall (a :: u). c a => f a -> g (ApplyToField h a)
f)
                    forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {u} (xs :: [u]) (f :: u -> *) (g :: u -> *) (h :: u -> *).
(RMap xs, RApply xs) =>
(forall (x :: u). f x -> g x -> h x)
-> Rec f xs -> Rec g xs -> Rec h xs
rzipWith forall {k} (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (forall {k} (c :: k -> Constraint) (ts :: [k]) (f :: k -> *).
RPureConstrained c ts =>
(forall (a :: k). c a => f a) -> Rec f ts
rpureConstrained @c forall (b :: u). c b => DictOnly c b
aux)
  where aux :: c b => DictOnly c b
        aux :: forall (b :: u). c b => DictOnly c b
aux = forall {k} (c :: k -> Constraint) (a :: k). c a => DictOnly c a
DictOnly

-- Note: rtraverseInMethod is written with that `aux` helper in order
-- to work around compatibility with GHC < 8.4. Write it more
-- naturally as `DictOnly @c` does not work with older compilers.

-- | Push an outer layer of interpretation functor into each named field.
rsequenceInFields :: forall f rs. (Functor f, AllFields rs, RMap rs)
                  => Rec (f :. ElField) rs -> Rec ElField (MapTyCon f rs)
rsequenceInFields :: forall (f :: * -> *) (rs :: [(Symbol, *)]).
(Functor f, AllFields rs, RMap rs) =>
Rec (f :. ElField) rs -> Rec ElField (MapTyCon f rs)
rsequenceInFields = forall {u} (c :: u -> Constraint) (h :: * -> *) (f :: u -> *)
       (g :: u -> *) (rs :: [u]).
(RMap rs, RPureConstrained c rs, RApply rs) =>
(forall (a :: u). c a => f a -> g (ApplyToField h a))
-> Rec f rs -> Rec g (MapTyCon h rs)
rtraverseInMethod @KnownField (forall (s :: Symbol) (f :: * -> *) a b.
(KnownSymbol s, Functor f) =>
(a -> b) -> f (ElField '(s, a)) -> ElField '(s, f b)
traverseField forall a. a -> a
id forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall l k (f :: l -> *) (g :: k -> l) (x :: k).
Compose f g x -> f (g x)
getCompose)


{- $example
    This module provides variants of typeclass methods that have
    a 'RecAll' constraint instead of the normal typeclass
    constraint. For example, a type-specialized 'compare' would
    look like this:

> compare :: Ord (Rec f rs) => Rec f rs -> Rec f rs -> Ordering

    The 'recCompare' function looks like this:

> recCompare :: RecAll f rs Ord => Rec f rs -> Rec f rs -> Ordering

    The only difference is the constraint. Let's look at a potential
    use case for these functions.

    Let's write a function that projects out a subrecord from two records and
    then compares those for equality. We can write this with
    the '<:' operator from @Data.Vinyl.Lens@ and the normal 'compare'
    function. We don't need 'recCompare':

> -- This needs ScopedTypeVariables
> projectAndCompare :: forall super sub f. (super <: sub, Ord (Rec f sub))
>                   => Proxy sub -> Rec f super -> Rec f super -> Ordering
> projectAndCompare _ a b = compare (rcast a :: Rec f sub) (rcast b :: Rec f sub)

    That works fine for the majority of use cases, and it is probably how you should
    write the function if it does everything you need. However, let's consider
    a somewhat more complicated case.

    What if the exact subrecord we were projecting couldn't be
    known at compile time? Assume that the end user was allowd to
    choose the fields on which he or she wanted to compare records.
    The @projectAndCompare@ function cannot handle this because of the
    @Ord (Rec f sub)@ constraint. Even if we amend the constraint to
    read @Ord (Rec f super)@ instead, we cannot use this information
    to recover the @Ord (Rec f sub)@ constraint that we need. Let's
    try another approach.

    We can use the following GADT to prove subsethood:

> data Sublist (super :: [k]) (sub :: [k]) where
>   SublistNil   :: Sublist '[]
>   SublistSuper :: Proxy r -> Sublist super sub -> Sublist (r ': super) sub
>   SublistBoth  :: Proxy r -> Sublist super sub -> Sublist (r ': super) (r ': sub)
>
> projectRec :: Sublist super sub -> Rec f super -> Rec f sub
> projectRec s r = case s of
>   SublistNil -> RNil
>   SublistBoth n snext -> case r of
>     rhead :& rtail -> rhead :& projectRec snext rtail
>   SublistSuper n snext -> case r of
>     rhead :& rtail -> projectRec snext rtail

    It is also possible to write a typeclass to generate @Sublist@s
    implicitly, but that is beyond the scope of this example. Let's
    now write a function to use @Sublist@ to weaken a 'RecAll'
    constraint:

> import Data.Vinyl.Core hiding (Dict)
> import Data.Constraint
>
> weakenRecAll :: Proxy f -> Proxy c -> Sublist super sub -> RecAll f super c :- RecAll f sub c
> weakenRecAll f c s = case s of
>   SublistNil -> Sub Dict
>   SublistSuper _ snext -> Sub $ case weakenRecAll f c snext of
>     Sub Dict -> Dict
>   SublistBoth _ snext -> Sub $ case weakenRecAll f c snext of
>     Sub Dict -> Dict

    Now we can write a different version of our original function:

> -- This needs ScopedTypeVariables
> projectAndCompare2 :: forall super sub f. (RecAll f super Ord)
>                    => Sublist super sub -> Rec f super -> Rec f super -> Ordering
> projectAndCompare2 s a b = case weakenRecAll (Proxy :: Proxy f) (Proxy :: Proxy Ord) s of
>   Sub Dict -> recCompare (projectRec s a) (projectRec s b)

    Notice that in this case, the 'Ord' constraint applies to the full set of fields
    and is then weakened to target a subset of them instead.
-}