{-# 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 :: forall (a :: [u]) (b :: [u]). Rec f a -> Rec f b -> Maybe (a :~: b)
testEquality Rec f a
RNil Rec f b
RNil = forall a. a -> Maybe a
Just 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 <- 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 <- 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
    forall a. a -> Maybe a
Just forall {k} (a :: k). a :~: a
Refl
  testEquality Rec f a
_ Rec f b
_ = forall a. Maybe a
Nothing

instance TestCoercion f => TestCoercion (Rec f) where
  testCoercion :: forall (a :: [u]) (b :: [u]).
Rec f a -> Rec f b -> Maybe (Coercion a b)
testCoercion Rec f a
RNil Rec f b
RNil = forall a. a -> Maybe a
Just 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 <- 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 <- 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
    forall a. a -> Maybe a
Just forall {k} (a :: k) (b :: k). Coercible a b => Coercion a b
Coercion
  testCoercion Rec f a
_ Rec f b
_ = forall a. Maybe a
Nothing

-- | Two records may be pasted together.
rappend
  :: Rec f as
  -> Rec f bs
  -> Rec f (as ++ bs)
rappend :: forall {k} (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
rappend Rec f as
RNil Rec f bs
ys = Rec f bs
ys
rappend (f r
x :& Rec f rs
xs) Rec f bs
ys = f r
x forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& (Rec f rs
xs 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)
<+> :: forall {k} (f :: k -> *) (as :: [k]) (bs :: [k]).
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 {u} (rs :: [u]) (m :: u -> *) (f :: u -> *) (g :: u -> *).
(RMap rs, RApply rs) =>
(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 {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 (forall {u} (rs :: [u]) (f :: u -> *) (g :: u -> *).
RApply rs =>
Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
rapply (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 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 {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 {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 (f :: u -> *) (g :: u -> *).
(forall (x :: u). f x -> g x) -> Rec f '[] -> Rec g '[]
rmap forall (x :: u). f x -> g x
_ Rec f '[]
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
  {-# INLINE rmap #-}

instance RMap xs => RMap (x ': xs) where
  rmap :: forall (f :: u -> *) (g :: u -> *).
(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) = forall (x :: u). f x -> g x
f f r
x forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : 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 {u} (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap 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 <<&>> :: forall {u} (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
Rec f rs -> (forall (x :: u). f x -> g x) -> Rec g rs
<<&>> forall (x :: u). f x -> g x
f = 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 :: forall (f :: u -> *) (g :: u -> *).
Rec (Lift (->) f g) '[] -> Rec f '[] -> Rec g '[]
rapply Rec (Lift (->) f g) '[]
_ Rec f '[]
RNil = forall {u} (f :: u -> *). Rec f '[]
RNil
  {-# INLINE rapply #-}

instance RApply xs => RApply (x ': xs) where
  rapply :: forall (f :: u -> *) (g :: u -> *).
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) = forall l l' k (op :: l -> l' -> *) (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 forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& (Rec (Lift (->) f g) rs
fs 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
xs)
  {-# INLINE rapply #-}

-- | A shorthand for 'rapply'.
(<<*>>)
  :: RApply 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
(<<*>>) = 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 (f :: u -> *). (forall (x :: u). f x) -> Rec f '[]
rpure forall (x :: u). f x
_ = forall {u} (f :: u -> *). Rec f '[]
RNil
  {-# INLINE rpure #-}
instance RecApplicative rs => RecApplicative (r ': rs) where
  rpure :: forall (f :: u -> *). (forall (x :: u). f x) -> Rec f (r : rs)
rpure forall (x :: u). f x
s = forall (x :: u). f x
s forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : 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 {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)
_ Rec f rs
RNil      = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall {u} (f :: u -> *). Rec f '[]
RNil
rtraverse forall (x :: u). f x -> h (g x)
f (f r
x :& Rec f rs
xs) = forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
(:&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (x :: u). f x -> h (g x)
f f r
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 {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)
_ Rec f rs
RNil = 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) = forall (a :: u). f a -> g (ApplyToField h a)
f f r
x forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : 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 :: forall (f :: * -> *) (g :: * -> *) (rs :: [*]).
(Traversable f, Applicative g) =>
Rec (f :. g) rs -> Rec g (MapTyCon f rs)
rsequenceIn = 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 (forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA 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)
{-# 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 {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 (x :: u). f x -> g x -> h x
f = forall {u} (rs :: [u]) (f :: u -> *) (g :: u -> *).
RApply rs =>
Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs
rapply forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 m (f :: u -> *).
Monoid m =>
(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 m (f :: u -> *).
Monoid m =>
(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 {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 (forall a. Monoid a => a -> a -> a
mappend m
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 {u} (rs :: [u]) m (f :: u -> *).
(Monoid m, RFoldMap rs) =>
(forall (x :: u). f x -> m) -> Rec f rs -> m
rfoldMap forall (x :: u). f x -> m
f = 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 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 :: forall a. Rec (Const a) '[] -> [a]
recordToList Rec (Const a) '[]
RNil = []
  {-# INLINE recordToList #-}

instance RecordToList xs => RecordToList (x ': xs) where
  recordToList :: forall a. Rec (Const a) (x : xs) -> [a]
recordToList (Const a r
x :& Rec (Const a) rs
xs) = forall k a (b :: k). Const a b -> a
getConst Const a r
x forall a. a -> [a] -> [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 = 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) = forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (forall (c :: * -> Constraint) a. c a => a -> Dict c a
Dict 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 -> *) (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 (f :: k -> *). (forall (a :: k). c a => f a) -> Rec f '[]
rpureConstrained forall (a :: k). c a => f a
_ = forall {u} (f :: u -> *). Rec f '[]
RNil
  {-# INLINE rpureConstrained #-}

instance (c x, RPureConstrained c xs) => RPureConstrained c (x ': xs) where
  rpureConstrained :: forall (f :: a -> *).
(forall (a :: a). c a => f a) -> Rec f (x : xs)
rpureConstrained forall (a :: a). c a => f a
f = forall (a :: a). c a => f a
f forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& forall {k} (c :: k -> Constraint) (ts :: [k]) (f :: k -> *).
RPureConstrained c ts =>
(forall (a :: k). 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 :: forall {k} (c :: k -> Constraint) (a :: k) (f :: k -> *) r.
(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 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 (f :: u -> *).
(forall (a :: u). AllSatisfied cs a => f a) -> Rec f '[]
rpureConstraints forall (a :: u). AllSatisfied cs a => f a
_ = forall {u} (f :: u -> *). Rec f '[]
RNil
  {-# INLINE rpureConstraints #-}

instance (AllSatisfied cs t, RPureConstraints cs ts)
  => RPureConstraints cs (t ': ts) where
  rpureConstraints :: forall (f :: u -> *).
(forall (a :: u). AllSatisfied cs a => f a) -> Rec f (t : ts)
rpureConstraints forall (a :: u). AllSatisfied cs a => f a
f = forall (a :: u). AllSatisfied cs a => f a
f forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& 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
"{" forall a. Semigroup a => a -> a -> a
<> String
str forall a. Semigroup a => a -> a -> a
<> String
"}")
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [[a]] -> [a]
intercalate String
", "
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {u} (rs :: [u]) a.
RecordToList rs =>
Rec (Const a) rs -> [a]
recordToList
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 f x
x)) -> forall k a (b :: k). a -> Const a b
Const forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show f x
x)
      forall a b. (a -> b) -> a -> b
$ 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 = 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 forall a. Semigroup a => a -> a -> a
<> f r
y) forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& (Rec f rs
xs forall a. Semigroup a => a -> a -> a
<> Rec f rs
ys)

instance Monoid (Rec f '[]) where
  mempty :: Rec f '[]
mempty = forall {u} (f :: u -> *). Rec f '[]
RNil
  Rec f '[]
RNil mappend :: Rec f '[] -> Rec f '[] -> Rec f '[]
`mappend` Rec f '[]
RNil = 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 = forall a. Monoid a => a
mempty forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : 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) = (forall a. Monoid a => a -> a -> a
mappend f r
x f r
y) forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : rs)
:& (forall a. Monoid a => a -> a -> a
mappend Rec f rs
xs 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 forall a. Eq a => a -> a -> Bool
== f r
y) Bool -> Bool -> Bool
&& (Rec f rs
xs forall a. Eq a => a -> a -> Bool
== 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) = forall a. Monoid a => a -> a -> a
mappend (forall a. Ord a => a -> a -> Ordering
compare f r
x f r
y) (forall a. Ord a => a -> a -> Ordering
compare Rec f rs
xs 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 '[])
_      = forall (m :: * -> *) a. Monad m => a -> m a
return forall {u} (f :: u -> *). Rec f '[]
RNil
  poke :: Ptr (Rec f '[]) -> Rec f '[] -> IO ()
poke Ptr (Rec f '[])
_ Rec f '[]
RNil = 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)
_ = forall a. Storable a => a -> Int
sizeOf (forall a. HasCallStack => a
undefined :: f r) forall a. Num a => a -> a -> a
+ forall a. Storable a => a -> Int
sizeOf (forall a. HasCallStack => a
undefined :: Rec f rs)
  {-# INLINE sizeOf #-}
  alignment :: Rec f (r : rs) -> Int
alignment Rec f (r : rs)
_ =  forall a. Storable a => a -> Int
alignment (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 <- forall a. Storable a => Ptr a -> IO a
peek (forall a b. Ptr a -> Ptr b
castPtr Ptr (Rec f (r : rs))
ptr)
                !Rec f rs
xs <- forall a. Storable a => Ptr a -> IO a
peek (Ptr (Rec f (r : rs))
ptr forall a b. Ptr a -> Int -> Ptr b
`plusPtr` forall a. Storable a => a -> Int
sizeOf (forall a. HasCallStack => a
undefined :: f r))
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ f r
x forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
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) = forall a. Storable a => Ptr a -> a -> IO ()
poke (forall a b. Ptr a -> Ptr b
castPtr Ptr (Rec f (r : rs))
ptr) f r
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a. Storable a => Ptr a -> a -> IO ()
poke (Ptr (Rec f (r : rs))
ptr forall a b. Ptr a -> Int -> Ptr b
`plusPtr` forall a. Storable a => a -> Int
sizeOf (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 :: forall x. Rec f '[] -> Rep (Rec f '[]) x
from Rec f '[]
RNil = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall k (p :: k). U1 p
U1)
  to :: forall x. Rep (Rec f '[]) x -> Rec f '[]
to (M1 (M1 U1 x
U1)) = 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 :: forall x. Rec f (r : rs) -> Rep (Rec f (r : rs)) x
from (f r
x :& Rec f rs
xs) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall k i c (p :: k). c -> K1 i c p
K1 f r
x) forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (forall a x. Generic a => a -> Rep a x
from Rec f rs
xs))
  to :: forall x. Rep (Rec f (r : rs)) x -> Rec f (r : rs)
to (M1 (M1 (K1 f r
x) :*: M1 Rep (Rec f rs) x
xs)) = f r
x forall {u} (f :: u -> *) (r :: u) (rs :: [u]).
f r -> Rec f rs -> Rec f (r : 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 = forall (elems :: [u]). Rec (Dict NFData :. f) elems -> ()
go 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
reifyConstraint @NFData
    where
      go :: forall elems. Rec (Dict NFData :. f) elems -> ()
      go :: forall (elems :: [u]). Rec (Dict NFData :. f) elems -> ()
go Rec (Dict NFData :. f) elems
RNil = ()
      go (Compose (Dict f r
x) :& Rec (Dict NFData :. f) rs
xs) = forall a. NFData a => a -> ()
rnf f r
x seq :: forall a b. a -> b -> b
`seq` 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 :: forall {u} {u} (f :: u -> *) (xs :: [u]) (g :: u -> *) (ys :: [u]).
AllRepsMatch f xs g ys =>
Coercion (Rec f xs) (Rec g ys)
repsMatchCoercion = forall a b. a -> b
unsafeCoerce (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 :: forall k (f :: k -> *) (g :: k -> *) (xs :: [k]).
(forall (x :: k). Coercible (f x) (g x)) =>
Coercion (Rec f xs) (Rec g xs)
consMatchCoercion = forall a b. a -> b
unsafeCoerce (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)
-}