{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE CPP                   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE Trustworthy           #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
#if __GLASGOW_HASKELL__ >= 806
{-# LANGUAGE QuantifiedConstraints #-}
#endif
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

-- | 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.
module Data.Vinyl.Core where
import Data.Coerce (Coercible)
#if __GLASGOW_HASKELL__ < 808
import Data.Monoid (Monoid)
#endif
#if __GLASGOW_HASKELL__ < 804
import Data.Semigroup (Semigroup(..))
#endif
import Foreign.Ptr (castPtr, plusPtr)
import Foreign.Storable (Storable(..))
import Data.Functor.Product (Product(Pair))
import Data.List (intercalate)
import Data.Vinyl.Functor
import Data.Vinyl.TypeLevel
import Data.Type.Equality (TestEquality (..), (:~:) (..))
import Data.Type.Coercion (TestCoercion (..), Coercion (..))
import GHC.Generics
import GHC.Types (Constraint, Type)
import Unsafe.Coerce (unsafeCoerce)
import Control.DeepSeq (NFData, rnf)
#if __GLASGOW_HASKELL__ < 806
import Data.Constraint.Forall (Forall)
#endif

-- | 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 :: *@.
data Rec :: (u -> *) -> [u] -> * where
  RNil :: Rec f '[]
  (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs)

infixr 7 :&
infixr 5  <+>
infixl 8 <<$>>
infixl 8 <<*>>

instance TestEquality f => TestEquality (Rec f) where
  testEquality :: Rec f a -> Rec f b -> Maybe (a :~: b)
testEquality Rec f a
RNil Rec f b
RNil = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
  testEquality (f r
x :& Rec f rs
xs) (f r
y :& Rec f rs
ys) = do
    r :~: r
Refl <- f r -> f r -> Maybe (r :~: r)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f r
x f r
y
    rs :~: rs
Refl <- Rec f rs -> Rec f rs -> Maybe (rs :~: rs)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Rec f rs
xs Rec f rs
ys
    (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
  testEquality Rec f a
_ Rec f b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance TestCoercion f => TestCoercion (Rec f) where
  testCoercion :: Rec f a -> Rec f b -> Maybe (Coercion a b)
testCoercion Rec f a
RNil Rec f b
RNil = Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just Coercion a b
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
  testCoercion (f r
x :& Rec f rs
xs) (f r
y :& Rec f rs
ys) = do
    Coercion r r
Coercion <- f r -> f r -> Maybe (Coercion r r)
forall k (f :: k -> *) (a :: k) (b :: k).
TestCoercion f =>
f a -> f b -> Maybe (Coercion a b)
testCoercion f r
x f r
y
    Coercion rs rs
Coercion <- Rec f rs -> Rec f rs -> Maybe (Coercion rs rs)
forall k (f :: k -> *) (a :: k) (b :: k).
TestCoercion f =>
f a -> f b -> Maybe (Coercion a b)
testCoercion Rec f rs
xs Rec f rs
ys
    Coercion a b -> Maybe (Coercion a b)
forall a. a -> Maybe a
Just Coercion a b
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
  testCoercion Rec f a
_ Rec f b
_ = Maybe (Coercion a b)
forall a. Maybe a
Nothing

-- | Two records may be pasted together.
rappend
  :: Rec f as
  -> Rec f bs
  -> Rec f (as ++ bs)
rappend :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
rappend Rec f as
RNil Rec f bs
ys = Rec f bs
Rec f (as ++ bs)
ys
rappend (f r
x :& Rec f rs
xs) Rec f bs
ys = f r
x f r -> Rec f (rs ++ bs) -> Rec f (r : (rs ++ bs))
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& (Rec f rs
xs Rec f rs -> Rec f bs -> Rec f (rs ++ bs)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
`rappend` Rec f bs
ys)

-- | A shorthand for 'rappend'.
(<+>)
  :: Rec f as
  -> Rec f bs
  -> Rec f (as ++ bs)
<+> :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
(<+>) = Rec f as -> Rec f bs -> Rec f (as ++ bs)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
rappend

-- | 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.
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
rcombine :: (forall (a :: u). m a -> m a -> m a)
-> (forall (a :: u). f a -> m a)
-> (forall (a :: u). m a -> g a)
-> Rec f rs
-> Rec f rs
-> Rec g rs
rcombine forall (a :: u). m a -> m a -> m a
smash forall (a :: u). f a -> m a
toM forall (a :: u). m a -> g a
fromM Rec f rs
x Rec f rs
y =
  (forall (a :: u). m a -> g a) -> Rec m rs -> Rec g rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (a :: u). m a -> g a
fromM (Rec (Lift (->) m m) rs -> Rec m rs -> Rec m rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RApply rs =>
Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
rapply ((forall (x :: u). m x -> Lift (->) m m x)
-> Rec m rs -> Rec (Lift (->) m m) rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap ((m x -> m x) -> Lift (->) m m x
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 ((m x -> m x) -> Lift (->) m m x)
-> (m x -> m x -> m x) -> m x -> Lift (->) m m x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m x -> m x -> m x
forall (a :: u). m a -> m a -> m a
smash) Rec m rs
x') Rec m rs
y')
  where x' :: Rec m rs
x' = (forall (a :: u). f a -> m a) -> Rec f rs -> Rec m rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (a :: u). f a -> m a
toM Rec f rs
x
        y' :: Rec m rs
y' = (forall (a :: u). f a -> m a) -> Rec f rs -> Rec m rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (a :: u). f a -> m a
toM Rec f rs
y

-- | '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@.
class RMap rs where
  rmap :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs

instance RMap '[] where
  rmap :: (forall (x :: u). f x -> g x) -> Rec f '[] -> Rec g '[]
rmap forall (x :: u). f x -> g x
_ Rec f '[]
RNil = Rec g '[]
forall u (f :: u -> *). Rec f '[]
RNil
  {-# INLINE rmap #-}

instance RMap xs => RMap (x ': xs) where
  rmap :: (forall (x :: u). f x -> g x) -> Rec f (x : xs) -> Rec g (x : xs)
rmap forall (x :: u). f x -> g x
f (f r
x :& Rec f rs
xs) = f r -> g r
forall (x :: u). f x -> g x
f f r
x g r -> Rec g rs -> Rec g (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (x :: u). f x -> g x
f Rec f rs
xs
  {-# INLINE rmap #-}

-- | A shorthand for 'rmap'.
(<<$>>)
  :: RMap rs
  => (forall x. f x -> g x)
  -> Rec f rs
  -> Rec g rs
<<$>> :: (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
(<<$>>) = (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap
{-# INLINE (<<$>>) #-}

-- | An inverted shorthand for 'rmap'.
(<<&>>)
  :: RMap rs
  => Rec f rs
  -> (forall x. f x -> g x)
  -> Rec g rs
Rec f rs
xs <<&>> :: Rec f rs -> (forall (x :: u). f x -> g x) -> Rec g rs
<<&>> forall (x :: u). f x -> g x
f = (forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap forall (x :: u). f x -> g x
f Rec f rs
xs
{-# INLINE (<<&>>) #-}

-- | A record of components @f r -> g r@ may be applied to a record of @f@ to
-- get a record of @g@.
class RApply rs where
  rapply :: Rec (Lift (->) f g) rs
         -> Rec f rs
         -> Rec g rs

instance RApply '[] where
  rapply :: Rec (Lift (->) f g) '[] -> Rec f '[] -> Rec g '[]
rapply Rec (Lift (->) f g) '[]
_ Rec f '[]
RNil = Rec g '[]
forall u (f :: u -> *). Rec f '[]
RNil
  {-# INLINE rapply #-}

instance RApply xs => RApply (x ': xs) where
  rapply :: Rec (Lift (->) f g) (x : xs) -> Rec f (x : xs) -> Rec g (x : xs)
rapply (Lift (->) f g r
f :& Rec (Lift (->) f g) rs
fs) (f r
x :& Rec f rs
xs) = Lift (->) f g r -> f r -> g x
forall l l' (op :: l -> l' -> *) k (f :: k -> l) (g :: k -> l')
       (x :: k).
Lift op f g x -> op (f x) (g x)
getLift Lift (->) f g r
f f r
x g x -> Rec g rs -> Rec g (x : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& (Rec (Lift (->) f g) rs
fs Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RApply rs =>
Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
`rapply` Rec f rs
Rec f rs
xs)
  {-# INLINE rapply #-}

-- | A shorthand for 'rapply'.
(<<*>>)
  :: RApply rs
  => Rec (Lift (->) f g) rs
  -> Rec f rs
  -> Rec g rs
<<*>> :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
(<<*>>) = Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RApply rs =>
Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
rapply
{-# INLINE (<<*>>) #-}

-- | Given a section of some functor, records in that functor of any size are
-- inhabited.
class RecApplicative rs where
  rpure
    :: (forall x. f x)
    -> Rec f rs
instance RecApplicative '[] where
  rpure :: (forall (x :: u). f x) -> Rec f '[]
rpure forall (x :: u). f x
_ = Rec f '[]
forall u (f :: u -> *). Rec f '[]
RNil
  {-# INLINE rpure #-}
instance RecApplicative rs => RecApplicative (r ': rs) where
  rpure :: (forall (x :: u). f x) -> Rec f (r : rs)
rpure forall (x :: u). f x
s = f r
forall (x :: u). f x
s f r -> Rec f rs -> Rec f (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& (forall (x :: u). f x) -> Rec f rs
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure forall (x :: u). f x
s
  {-# INLINE rpure #-}

-- | 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.
rtraverse
  :: Applicative h
  => (forall x. f x -> h (g x))
  -> Rec f rs
  -> h (Rec g rs)
rtraverse :: (forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
rtraverse forall (x :: u). f x -> h (g x)
_ Rec f rs
RNil      = Rec g '[] -> h (Rec g '[])
forall (f :: * -> *) a. Applicative f => a -> f a
pure Rec g '[]
forall u (f :: u -> *). Rec f '[]
RNil
rtraverse forall (x :: u). f x -> h (g x)
f (f r
x :& Rec f rs
xs) = g r -> Rec g rs -> Rec g (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
(:&) (g r -> Rec g rs -> Rec g (r : rs))
-> h (g r) -> h (Rec g rs -> Rec g (r : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f r -> h (g r)
forall (x :: u). f x -> h (g x)
f f r
x h (Rec g rs -> Rec g (r : rs))
-> h (Rec g rs) -> h (Rec g (r : rs))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
forall u (h :: * -> *) (f :: u -> *) (g :: u -> *) (rs :: [u]).
Applicative h =>
(forall (x :: u). f x -> h (g x)) -> Rec f rs -> h (Rec g rs)
rtraverse forall (x :: u). f x -> h (g x)
f Rec f rs
xs
{-# INLINABLE rtraverse #-}

-- | 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]@.
rtraverseIn :: forall h f g rs.
               (forall a. f a -> g (ApplyToField h a))
            -> Rec f rs
            -> Rec g (MapTyCon h rs)
rtraverseIn :: (forall (a :: u). f a -> g (ApplyToField h a))
-> Rec f rs -> Rec g (MapTyCon h rs)
rtraverseIn forall (a :: u). f a -> g (ApplyToField h a)
_ Rec f rs
RNil = Rec g (MapTyCon h rs)
forall u (f :: u -> *). Rec f '[]
RNil
rtraverseIn forall (a :: u). f a -> g (ApplyToField h a)
f (f r
x :& Rec f rs
xs) = f r -> g (ApplyToField h r)
forall (a :: u). f a -> g (ApplyToField h a)
f f r
x g (ApplyToField h r)
-> Rec g (MapTyCon h rs)
-> Rec g (ApplyToField h r : MapTyCon h rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& (forall (a :: u). f a -> g (ApplyToField h a))
-> Rec f rs -> Rec g (MapTyCon h rs)
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 forall (a :: u). f a -> g (ApplyToField h a)
f Rec f rs
xs
{-# INLINABLE rtraverseIn #-}

-- | Push an outer layer of interpretation functor into each field.
rsequenceIn :: forall f g (rs :: [Type]). (Traversable f, Applicative g)
            => Rec (f :. g) rs -> Rec g (MapTyCon f rs)
rsequenceIn :: Rec (f :. g) rs -> Rec g (MapTyCon f rs)
rsequenceIn = (forall a. (:.) f g a -> g (ApplyToField f a))
-> Rec (f :. g) rs -> Rec g (MapTyCon f rs)
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 @f (f (g a) -> g (f a)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA (f (g a) -> g (f a))
-> (Compose f g a -> f (g a)) -> Compose f g a -> g (f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Compose f g a -> f (g a)
forall l (f :: l -> *) k (g :: k -> l) (x :: k).
Compose f g x -> f (g x)
getCompose)
{-# INLINABLE rsequenceIn #-}

-- | 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.
rzipWith :: (RMap xs, RApply xs)
         => (forall x. f x -> g x -> h x) -> Rec f xs -> Rec g xs -> Rec h xs
rzipWith :: (forall (x :: u). f x -> g x -> h x)
-> Rec f xs -> Rec g xs -> Rec h xs
rzipWith forall (x :: u). f x -> g x -> h x
f = Rec (Lift (->) g h) xs -> Rec g xs -> Rec h xs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RApply rs =>
Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
rapply (Rec (Lift (->) g h) xs -> Rec g xs -> Rec h xs)
-> (Rec f xs -> Rec (Lift (->) g h) xs)
-> Rec f xs
-> Rec g xs
-> Rec h xs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: u). f x -> Lift (->) g h x)
-> Rec f xs -> Rec (Lift (->) g h) xs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap ((g x -> h x) -> Lift (->) g h x
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 ((g x -> h x) -> Lift (->) g h x)
-> (f x -> g x -> h x) -> f x -> Lift (->) g h x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> g x -> h x
forall (x :: u). f x -> g x -> h x
f)

-- | Map each element of a record to a monoid and combine the results.
class RFoldMap rs where
  rfoldMapAux :: Monoid m
              => (forall x. f x -> m)
              -> m
              -> Rec f rs
              -> m

instance RFoldMap '[] where
  rfoldMapAux :: (forall (x :: u). f x -> m) -> m -> Rec f '[] -> m
rfoldMapAux forall (x :: u). f x -> m
_ m
m Rec f '[]
RNil = m
m
  {-# INLINE rfoldMapAux #-}

instance RFoldMap xs => RFoldMap (x ': xs) where
  rfoldMapAux :: (forall (x :: u). f x -> m) -> m -> Rec f (x : xs) -> m
rfoldMapAux forall (x :: u). f x -> m
f m
m (f r
r :& Rec f rs
rs) = (forall (x :: u). f x -> m) -> m -> Rec f rs -> m
forall u (rs :: [u]) m (f :: u -> *).
(RFoldMap rs, Monoid m) =>
(forall (x :: u). f x -> m) -> m -> Rec f rs -> m
rfoldMapAux forall (x :: u). f x -> m
f (m -> m -> m
forall a. Monoid a => a -> a -> a
mappend m
m (f r -> m
forall (x :: u). f x -> m
f f r
r)) Rec f rs
rs
  {-# INLINE rfoldMapAux #-}

rfoldMap :: forall rs m f. (Monoid m, RFoldMap rs)
         => (forall x. f x -> m) -> Rec f rs -> m
rfoldMap :: (forall (x :: u). f x -> m) -> Rec f rs -> m
rfoldMap forall (x :: u). f x -> m
f = (forall (x :: u). f x -> m) -> m -> Rec f rs -> m
forall u (rs :: [u]) m (f :: u -> *).
(RFoldMap rs, Monoid m) =>
(forall (x :: u). f x -> m) -> m -> Rec f rs -> m
rfoldMapAux forall (x :: u). f x -> m
f m
forall a. Monoid a => a
mempty
{-# INLINE rfoldMap #-}

-- | A record with uniform fields may be turned into a list.
class RecordToList rs where
  recordToList :: Rec (Const a) rs -> [a]

instance RecordToList '[] where
  recordToList :: Rec (Const a) '[] -> [a]
recordToList Rec (Const a) '[]
RNil = []
  {-# INLINE recordToList #-}

instance RecordToList xs => RecordToList (x ': xs) where
  recordToList :: Rec (Const a) (x : xs) -> [a]
recordToList (Const a r
x :& Rec (Const a) rs
xs) = Const a r -> a
forall a k (b :: k). Const a b -> a
getConst Const a r
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: Rec (Const a) rs -> [a]
forall u (rs :: [u]) a. RecordToList rs => Rec (Const a) rs -> [a]
recordToList Rec (Const a) rs
xs
  {-# INLINE recordToList #-}

-- | Wrap up a value with a capability given by its type
data Dict c a where
  Dict
    :: c a
    => a
    -> Dict c a

-- | 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.
class ReifyConstraint c f rs where
  reifyConstraint
    :: Rec f rs
    -> Rec (Dict c :. f) rs

instance ReifyConstraint c f '[] where
  reifyConstraint :: Rec f '[] -> Rec (Dict c :. f) '[]
reifyConstraint Rec f '[]
RNil = Rec (Dict c :. f) '[]
forall u (f :: u -> *). Rec f '[]
RNil
  {-# INLINE reifyConstraint #-}

instance (c (f x), ReifyConstraint c f xs)
  => ReifyConstraint c f (x ': xs) where
  reifyConstraint :: Rec f (x : xs) -> Rec (Dict c :. f) (x : xs)
reifyConstraint (f r
x :& Rec f rs
xs) = Dict c (f r) -> Compose (Dict c) f r
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (f r -> Dict c (f r)
forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict f r
x) Compose (Dict c) f r
-> Rec (Dict c :. f) rs -> Rec (Dict c :. f) (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& Rec f rs -> Rec (Dict c :. f) rs
forall u (c :: * -> Constraint) (f :: u -> *) (rs :: [u]).
ReifyConstraint c f rs =>
Rec f rs -> Rec (Dict c :. f) rs
reifyConstraint Rec f rs
xs
  {-# INLINE reifyConstraint #-}

-- | Build a record whose elements are derived solely from a
-- constraint satisfied by each.
class RPureConstrained c ts where
  rpureConstrained :: (forall a. c a => f a) -> Rec f ts

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

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

-- | Capture a type class instance dictionary. See
-- 'Data.Vinyl.Lens.getDict' for a way to obtain a 'DictOnly' value
-- from an 'RPureConstrained' constraint.
data DictOnly (c :: k -> Constraint) a where
  DictOnly :: forall c a. c a => DictOnly c a

-- | A useful technique is to use 'rmap (Pair (DictOnly @MyClass))' on
-- a 'Rec' to pair each field with a type class dictionary for
-- @MyClass@. This helper can then be used to eliminate the original.
withPairedDict :: (c a => f a -> r) -> Product (DictOnly c) f a -> r
withPairedDict :: (c a => f a -> r) -> Product (DictOnly c) f a -> r
withPairedDict c a => f a -> r
f (Pair DictOnly c a
DictOnly f a
x) = c a => f a -> r
f a -> r
f f a
x

-- | Build a record whose elements are derived solely from a
-- list of constraint constructors satisfied by each.
class RPureConstraints cs ts where
  rpureConstraints :: (forall a. AllSatisfied cs a => f a) -> Rec f ts

instance RPureConstraints cs '[] where
  rpureConstraints :: (forall (a :: u). AllSatisfied cs a => f a) -> Rec f '[]
rpureConstraints forall (a :: u). AllSatisfied cs a => f a
_ = Rec f '[]
forall u (f :: u -> *). Rec f '[]
RNil
  {-# INLINE rpureConstraints #-}

instance (AllSatisfied cs t, RPureConstraints cs ts)
  => RPureConstraints cs (t ': ts) where
  rpureConstraints :: (forall (a :: u). AllSatisfied cs a => f a) -> Rec f (t : ts)
rpureConstraints forall (a :: u). AllSatisfied cs a => f a
f = f t
forall (a :: u). AllSatisfied cs a => f a
f f t -> Rec f ts -> Rec f (t : ts)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& (forall (a :: u). AllSatisfied cs a => f a) -> Rec f ts
forall k u (cs :: k) (ts :: [u]) (f :: u -> *).
RPureConstraints cs ts =>
(forall (a :: u). AllSatisfied cs a => f a) -> Rec f ts
rpureConstraints @cs @ts forall (a :: u). AllSatisfied cs a => f a
f
  {-# INLINE rpureConstraints #-}

-- | Records may be shown insofar as their points may be shown.
-- 'reifyConstraint' is used to great effect here.
instance (RMap rs, ReifyConstraint Show f rs, RecordToList rs)
  => Show (Rec f rs) where
  show :: Rec f rs -> String
show Rec f rs
xs =
    (\String
str -> String
"{" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
str String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"}")
      ShowS
-> (Rec (Dict Show :. f) rs -> String)
-> Rec (Dict Show :. f) rs
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", "
      ([String] -> String)
-> (Rec (Dict Show :. f) rs -> [String])
-> Rec (Dict Show :. f) rs
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec (Const String) rs -> [String]
forall u (rs :: [u]) a. RecordToList rs => Rec (Const a) rs -> [a]
recordToList
      (Rec (Const String) rs -> [String])
-> (Rec (Dict Show :. f) rs -> Rec (Const String) rs)
-> Rec (Dict Show :. f) rs
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: u). (:.) (Dict Show) f x -> Const String x)
-> Rec (Dict Show :. f) rs -> Rec (Const String) rs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap (\(Compose (Dict x)) -> String -> Const String x
forall k a (b :: k). a -> Const a b
Const (String -> Const String x) -> String -> Const String x
forall a b. (a -> b) -> a -> b
$ f x -> String
forall a. Show a => a -> String
show f x
x)
      (Rec (Dict Show :. f) rs -> String)
-> Rec (Dict Show :. f) rs -> String
forall a b. (a -> b) -> a -> b
$ Rec f rs -> Rec (Dict Show :. f) rs
forall u (c :: * -> Constraint) (f :: u -> *) (rs :: [u]).
ReifyConstraint c f rs =>
Rec f rs -> Rec (Dict c :. f) rs
reifyConstraint @Show Rec f rs
xs

instance Semigroup (Rec f '[]) where
  Rec f '[]
RNil <> :: Rec f '[] -> Rec f '[] -> Rec f '[]
<> Rec f '[]
RNil = Rec f '[]
forall u (f :: u -> *). Rec f '[]
RNil

instance (Semigroup (f r), Semigroup (Rec f rs))
  => Semigroup (Rec f (r ': rs)) where
  (f r
x :& Rec f rs
xs) <> :: Rec f (r : rs) -> Rec f (r : rs) -> Rec f (r : rs)
<> (f r
y :& Rec f rs
ys) = (f r
x f r -> f r -> f r
forall a. Semigroup a => a -> a -> a
<> f r
f r
y) f r -> Rec f rs -> Rec f (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& (Rec f rs
xs Rec f rs -> Rec f rs -> Rec f rs
forall a. Semigroup a => a -> a -> a
<> Rec f rs
Rec f rs
ys)

instance Monoid (Rec f '[]) where
  mempty :: Rec f '[]
mempty = Rec f '[]
forall u (f :: u -> *). Rec f '[]
RNil
  Rec f '[]
RNil mappend :: Rec f '[] -> Rec f '[] -> Rec f '[]
`mappend` Rec f '[]
RNil = Rec f '[]
forall u (f :: u -> *). Rec f '[]
RNil

instance (Monoid (f r), Monoid (Rec f rs)) => Monoid (Rec f (r ': rs)) where
  mempty :: Rec f (r : rs)
mempty = f r
forall a. Monoid a => a
mempty f r -> Rec f rs -> Rec f (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& Rec f rs
forall a. Monoid a => a
mempty
  (f r
x :& Rec f rs
xs) mappend :: Rec f (r : rs) -> Rec f (r : rs) -> Rec f (r : rs)
`mappend` (f r
y :& Rec f rs
ys) = (f r -> f r -> f r
forall a. Monoid a => a -> a -> a
mappend f r
x f r
f r
y) f r -> Rec f rs -> Rec f (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& (Rec f rs -> Rec f rs -> Rec f rs
forall a. Monoid a => a -> a -> a
mappend Rec f rs
xs Rec f rs
Rec f rs
ys)

instance Eq (Rec f '[]) where
  Rec f '[]
_ == :: Rec f '[] -> Rec f '[] -> Bool
== Rec f '[]
_ = Bool
True
instance (Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs)) where
  (f r
x :& Rec f rs
xs) == :: Rec f (r : rs) -> Rec f (r : rs) -> Bool
== (f r
y :& Rec f rs
ys) = (f r
x f r -> f r -> Bool
forall a. Eq a => a -> a -> Bool
== f r
f r
y) Bool -> Bool -> Bool
&& (Rec f rs
xs Rec f rs -> Rec f rs -> Bool
forall a. Eq a => a -> a -> Bool
== Rec f rs
Rec f rs
ys)

instance Ord (Rec f '[]) where
  compare :: Rec f '[] -> Rec f '[] -> Ordering
compare Rec f '[]
_ Rec f '[]
_ = Ordering
EQ
instance (Ord (f r), Ord (Rec f rs)) => Ord (Rec f (r ': rs)) where
  compare :: Rec f (r : rs) -> Rec f (r : rs) -> Ordering
compare (f r
x :& Rec f rs
xs) (f r
y :& Rec f rs
ys) = Ordering -> Ordering -> Ordering
forall a. Monoid a => a -> a -> a
mappend (f r -> f r -> Ordering
forall a. Ord a => a -> a -> Ordering
compare f r
x f r
f r
y) (Rec f rs -> Rec f rs -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Rec f rs
xs Rec f rs
Rec f rs
ys)

instance Storable (Rec f '[]) where
  sizeOf :: Rec f '[] -> Int
sizeOf Rec f '[]
_    = Int
0
  alignment :: Rec f '[] -> Int
alignment Rec f '[]
_ = Int
0
  peek :: Ptr (Rec f '[]) -> IO (Rec f '[])
peek Ptr (Rec f '[])
_      = Rec f '[] -> IO (Rec f '[])
forall (m :: * -> *) a. Monad m => a -> m a
return Rec f '[]
forall u (f :: u -> *). Rec f '[]
RNil
  poke :: Ptr (Rec f '[]) -> Rec f '[] -> IO ()
poke Ptr (Rec f '[])
_ Rec f '[]
RNil = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance (Storable (f r), Storable (Rec f rs))
  => Storable (Rec f (r ': rs)) where
  sizeOf :: Rec f (r : rs) -> Int
sizeOf Rec f (r : rs)
_ = f r -> Int
forall a. Storable a => a -> Int
sizeOf (f r
forall a. HasCallStack => a
undefined :: f r) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Rec f rs -> Int
forall a. Storable a => a -> Int
sizeOf (Rec f rs
forall a. HasCallStack => a
undefined :: Rec f rs)
  {-# INLINE sizeOf #-}
  alignment :: Rec f (r : rs) -> Int
alignment Rec f (r : rs)
_ =  f r -> Int
forall a. Storable a => a -> Int
alignment (f r
forall a. HasCallStack => a
undefined :: f r)
  {-# INLINE alignment #-}
  peek :: Ptr (Rec f (r : rs)) -> IO (Rec f (r : rs))
peek Ptr (Rec f (r : rs))
ptr = do !f r
x <- Ptr (f r) -> IO (f r)
forall a. Storable a => Ptr a -> IO a
peek (Ptr (Rec f (r : rs)) -> Ptr (f r)
forall a b. Ptr a -> Ptr b
castPtr Ptr (Rec f (r : rs))
ptr)
                !Rec f rs
xs <- Ptr (Rec f rs) -> IO (Rec f rs)
forall a. Storable a => Ptr a -> IO a
peek (Ptr (Rec f (r : rs))
ptr Ptr (Rec f (r : rs)) -> Int -> Ptr (Rec f rs)
forall a b. Ptr a -> Int -> Ptr b
`plusPtr` f r -> Int
forall a. Storable a => a -> Int
sizeOf (f r
forall a. HasCallStack => a
undefined :: f r))
                Rec f (r : rs) -> IO (Rec f (r : rs))
forall (m :: * -> *) a. Monad m => a -> m a
return (Rec f (r : rs) -> IO (Rec f (r : rs)))
-> Rec f (r : rs) -> IO (Rec f (r : rs))
forall a b. (a -> b) -> a -> b
$ f r
x f r -> Rec f rs -> Rec f (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& Rec f rs
xs
  {-# INLINE peek #-}
  poke :: Ptr (Rec f (r : rs)) -> Rec f (r : rs) -> IO ()
poke Ptr (Rec f (r : rs))
ptr (!f r
x :& Rec f rs
xs) = Ptr (f r) -> f r -> IO ()
forall a. Storable a => Ptr a -> a -> IO ()
poke (Ptr (Rec f (r : rs)) -> Ptr (f r)
forall a b. Ptr a -> Ptr b
castPtr Ptr (Rec f (r : rs))
ptr) f r
x IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Ptr (Rec f rs) -> Rec f rs -> IO ()
forall a. Storable a => Ptr a -> a -> IO ()
poke (Ptr (Rec f (r : rs))
ptr Ptr (Rec f (r : rs)) -> Int -> Ptr (Rec f rs)
forall a b. Ptr a -> Int -> Ptr b
`plusPtr` f r -> Int
forall a. Storable a => a -> Int
sizeOf (f r
forall a. HasCallStack => a
undefined :: f r)) Rec f rs
xs
  {-# INLINE poke #-}

instance Generic (Rec f '[]) where
  type Rep (Rec f '[]) =
    C1 ('MetaCons "RNil" 'PrefixI 'False)
       (S1 ('MetaSel 'Nothing
          'NoSourceUnpackedness
          'NoSourceStrictness
          'DecidedLazy) U1)
  from :: Rec f '[] -> Rep (Rec f '[]) x
from Rec f '[]
RNil = M1
  S
  ('MetaSel
     'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
  U1
  x
-> M1
     C
     ('MetaCons "RNil" 'PrefixI 'False)
     (M1
        S
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
        U1)
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (U1 x
-> M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     U1
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 U1 x
forall k (p :: k). U1 p
U1)
  to :: Rep (Rec f '[]) x -> Rec f '[]
to (M1 (M1 U1)) = Rec f '[]
forall u (f :: u -> *). Rec f '[]
RNil

instance (Generic (Rec f rs)) => Generic (Rec f (r ': rs)) where
  type Rep (Rec f (r ': rs)) =
    C1 ('MetaCons ":&" ('InfixI 'RightAssociative 7) 'False)
    (S1 ('MetaSel 'Nothing
         'NoSourceUnpackedness
         'SourceStrict
         'DecidedStrict)
       (Rec0 (f r))
      :*:
      S1 ('MetaSel 'Nothing
           'NoSourceUnpackedness
           'NoSourceStrictness
           'DecidedLazy)
         (Rep (Rec f rs)))
  from :: Rec f (r : rs) -> Rep (Rec f (r : rs)) x
from (f r
x :& Rec f rs
xs) = (:*:)
  (M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict)
     (K1 R (f r)))
  (M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (Rep (Rec f rs)))
  x
-> M1
     C
     ('MetaCons ":&" ('InfixI 'RightAssociative 7) 'False)
     (M1
        S
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict)
        (K1 R (f r))
      :*: M1
            S
            ('MetaSel
               'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
            (Rep (Rec f rs)))
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (K1 R (f r) x
-> M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict)
     (K1 R (f r))
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f r -> K1 R (f r) x
forall k i c (p :: k). c -> K1 i c p
K1 f r
x) M1
  S
  ('MetaSel
     'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict)
  (K1 R (f r))
  x
-> M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (Rep (Rec f rs))
     x
-> (:*:)
     (M1
        S
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict)
        (K1 R (f r)))
     (M1
        S
        ('MetaSel
           'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
        (Rep (Rec f rs)))
     x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Rep (Rec f rs) x
-> M1
     S
     ('MetaSel
        'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy)
     (Rep (Rec f rs))
     x
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (Rec f rs -> Rep (Rec f rs) x
forall a x. Generic a => a -> Rep a x
from Rec f rs
xs))
  to :: Rep (Rec f (r : rs)) x -> Rec f (r : rs)
to (M1 (M1 (K1 x) :*: M1 xs)) = f r
x f r -> Rec f rs -> Rec f (r : rs)
forall a (f :: a -> *) (r :: a) (rs :: [a]).
f r -> Rec f rs -> Rec f (r : rs)
:& Rep (Rec f rs) x -> Rec f rs
forall a x. Generic a => Rep a x -> a
to Rep (Rec f rs) x
xs

instance ReifyConstraint NFData f xs => NFData (Rec f xs) where
  rnf :: Rec f xs -> ()
rnf = Rec (Dict NFData :. f) xs -> ()
forall (elems :: [u]). Rec (Dict NFData :. f) elems -> ()
go (Rec (Dict NFData :. f) xs -> ())
-> (Rec f xs -> Rec (Dict NFData :. f) xs) -> Rec f xs -> ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall u (c :: * -> Constraint) (f :: u -> *) (rs :: [u]).
ReifyConstraint c f rs =>
Rec f rs -> Rec (Dict c :. f) rs
forall (f :: u -> *) (rs :: [u]).
ReifyConstraint NFData f rs =>
Rec f rs -> Rec (Dict NFData :. f) rs
reifyConstraint @NFData
    where
      go :: forall elems. Rec (Dict NFData :. f) elems -> ()
      go :: Rec (Dict NFData :. f) elems -> ()
go Rec (Dict NFData :. f) elems
RNil = ()
      go (Compose (Dict f r
x) :& Rec (Dict NFData :. f) rs
xs) = f r -> ()
forall a. NFData a => a -> ()
rnf f r
x () -> () -> ()
`seq` Rec (Dict NFData :. f) rs -> ()
forall (elems :: [u]). Rec (Dict NFData :. f) elems -> ()
go Rec (Dict NFData :. f) rs
xs

type family Head xs where
  Head (x ': _) = x
type family Tail xs where
  Tail (_ ': xs) = xs

type family AllRepsMatch_ (f :: j -> *) (xs :: [j]) (g :: k -> *) (ys :: [k]) :: Constraint where
  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 ~ '[]

-- | @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]@
type AllRepsMatch f xs g ys = (AllRepsMatch_ f xs g ys, AllRepsMatch_ g ys f xs)

-- This two-sided approach means that the *length* of each list
-- can be inferred from the length of the other. I don't know how
-- useful that is in practice, but we get it almost for free.

-- | Given that for each element @x@ in the list @xs@,
repsMatchCoercion :: AllRepsMatch f xs g ys => Coercion (Rec f xs) (Rec g ys)
repsMatchCoercion :: Coercion (Rec f xs) (Rec g ys)
repsMatchCoercion = Coercion () () -> Coercion (Rec f xs) (Rec g ys)
forall a b. a -> b
unsafeCoerce (Coercion () ()
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion :: Coercion () ())

{-
-- "Proof" that repsMatchCoercion is sensible.
repsMatchConvert :: AllRepsMatch f xs g ys => Rec f xs -> Rec g ys
repsMatchConvert RNil = RNil
repsMatchConvert (x :& xs) = coerce x :& repsMatchConvert xs
-}

#if __GLASGOW_HASKELL__ >= 806
consMatchCoercion ::
  (forall (x :: k). Coercible (f x) (g x)) => Coercion (Rec f xs) (Rec g xs)
#else
consMatchCoercion :: forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
  Forall (Similar f g) => Coercion (Rec f xs) (Rec g xs)
#endif
consMatchCoercion :: Coercion (Rec f xs) (Rec g xs)
consMatchCoercion = Coercion () () -> Coercion (Rec f xs) (Rec g xs)
forall a b. a -> b
unsafeCoerce (Coercion () ()
forall k (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion :: Coercion () ())
{-
-- "Proof" that consMatchCoercion is sensible.
consMatchConvert ::
  (forall (x :: k). Coercible (f x) (g x)) => Rec f xs -> Rec g xs
consMatchConvert RNil = RNil
consMatchConvert (x :& xs) = coerce x :& consMatchConvert xs

-- And for old GHC.
consMatchConvert' :: forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
  Forall (Similar f g) => Rec f xs -> Rec g xs
consMatchConvert' RNil = RNil
consMatchConvert' ((x :: f x) :& xs) =
  case inst :: Forall (Similar f g) DC.:- Similar f g x of
    DC.Sub DC.Dict -> coerce x :& consMatchConvert' xs
-}

{-
-- This is sensible, but I suspect the ergonomics will be awful
-- thanks to the interaction between Coercible constraint resolution
-- and constraint resolution with quantified constraints. Is there
-- a good way to accomplish it?

-- | Given
--
-- @
-- forall x. Coercible (f x) (g x)
-- @
--
-- provide the constraint
--
-- @
-- forall xs. Coercible (Rec f xs) (Rec g xs)
-- @
consMatchCoercible :: forall k f g rep (r :: TYPE rep).
     (forall (x :: k). Coercible (f x) (g x))
  => ((forall (xs :: [k]). Coercible (Rec f xs) (Rec g xs)) => r) -> r
consMatchCoercible f = case unsafeCoerce @(Zouch f f) @(Zouch f g) (Zouch $ \r -> r) of
  Zouch q -> q f

newtype Zouch (f :: k -> *) (g :: k -> *) =
  Zouch (forall rep (r :: TYPE rep). ((forall (xs :: [k]). Coercible (Rec f xs) (Rec g xs)) => r) -> r)
-}