{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE CPP                   #-}
#if __GLASGOW_HASKELL__ < 806
{-# LANGUAGE TypeInType #-}
#endif

-- | Lenses into record fields.
module Data.Vinyl.Lens
  ( RecElem(..)
  , rget, rput, rput', rlens, rlens'
  , RElem
  , RecSubset(..)
  , rsubset, rcast, rreplace
  , rdowncast
  , RSubset
  , REquivalent
  , type (∈)
  , type (⊆)
  , type (≅)
  , type (<:)
  , type (:~:)
  ) where

import Data.Kind (Constraint)
import Data.Vinyl.Core
import Data.Vinyl.Functor
import Data.Vinyl.TypeLevel
#if __GLASGOW_HASKELL__ < 806
import Data.Kind
#endif

-- | The presence of a field in a record is witnessed by a lens into
-- its value.  The fifth parameter to 'RecElem', @i@, is there to help
-- the constraint solver realize that this is a decidable predicate
-- with respect to the judgemental equality in @k@.
class (i ~ RIndex r rs, NatToInt i)
  => RecElem (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k) (rs :: [k]) (rs' :: [k]) (i :: Nat) | r r' rs i -> rs' where
  -- | An opportunity for instances to generate constraints based on
  -- the functor parameter of records passed to class methods.
  type RecElemFCtx record (f :: k -> *) :: Constraint
  type RecElemFCtx record f = ()

  -- | We can get a lens for getting and setting the value of a field which is
  -- in a record. As a convenience, we take a proxy argument to fix the
  -- particular field being viewed. These lenses are compatible with the @lens@
  -- library. Morally:
  --
  -- > rlensC :: Lens' (Rec f rs) (Rec f rs') (f r) (f r')
  rlensC
    :: (Functor g, RecElemFCtx record f)
    => (f r -> g (f r'))
    -> record f rs
    -> g (record f rs')

  -- | For Vinyl users who are not using the @lens@ package, we provide a getter.
  rgetC
    :: (RecElemFCtx record f, r ~ r')
    => record f rs
    -> f r

  -- | For Vinyl users who are not using the @lens@ package, we also provide a
  -- setter. In general, it will be unambiguous what field is being written to,
  -- and so we do not take a proxy argument here.
  rputC
    :: RecElemFCtx record f
    => f r'
    -> record f rs
    -> record f rs'

-- | 'RecElem' for classic vinyl 'Rec' types.
type RElem x rs = RecElem Rec x x rs rs

-- This is an internal convenience stolen from the @lens@ library.
lens
  :: Functor f
  => (s -> a)
  -> (s -> b -> t)
  -> (a -> f b)
  -> s
  -> f t
lens :: (s -> a) -> (s -> b -> t) -> (a -> f b) -> s -> f t
lens s -> a
sa s -> b -> t
sbt a -> f b
afb s
s = (b -> t) -> f b -> f t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (s -> b -> t
sbt s
s) (f b -> f t) -> f b -> f t
forall a b. (a -> b) -> a -> b
$ a -> f b
afb (s -> a
sa s
s)
{-# INLINE lens #-}

instance RecElem Rec r r' (r ': rs) (r' ': rs) 'Z where
  rlensC :: (f r -> g (f r')) -> Rec f (r : rs) -> g (Rec f (r' : rs))
rlensC f r -> g (f r')
f (f r
x :& Rec f rs
xs) = (f r' -> Rec f (r' : rs)) -> g (f r') -> g (Rec f (r' : rs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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) (f r -> g (f r')
f f r
f r
x)
  {-# INLINE rlensC #-}
  rgetC :: Rec f (r : rs) -> f r
rgetC = Const (f r) (Rec f (Any : rs)) -> f r
forall a k (b :: k). Const a b -> a
getConst (Const (f r) (Rec f (Any : rs)) -> f r)
-> (Rec f (r : rs) -> Const (f r) (Rec f (Any : rs)))
-> Rec f (r : rs)
-> f r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f r -> Const (f r) (f Any))
-> Rec f (r : rs) -> Const (f r) (Rec f (Any : rs))
forall k (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k)
       (rs :: [k]) (rs' :: [k]) (i :: Nat) (g :: * -> *) (f :: k -> *).
(RecElem record r r' rs rs' i, Functor g, RecElemFCtx record f) =>
(f r -> g (f r')) -> record f rs -> g (record f rs')
rlensC f r -> Const (f r) (f Any)
forall k a (b :: k). a -> Const a b
Const
  {-# INLINE rgetC #-}
  rputC :: f r' -> Rec f (r : rs) -> Rec f (r' : rs)
rputC f r'
y = Identity (Rec f (r' : rs)) -> Rec f (r' : rs)
forall a. Identity a -> a
getIdentity (Identity (Rec f (r' : rs)) -> Rec f (r' : rs))
-> (Rec f (r : rs) -> Identity (Rec f (r' : rs)))
-> Rec f (r : rs)
-> Rec f (r' : rs)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f r -> Identity (f r'))
-> Rec f (r : rs) -> Identity (Rec f (r' : rs))
forall k (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k)
       (rs :: [k]) (rs' :: [k]) (i :: Nat) (g :: * -> *) (f :: k -> *).
(RecElem record r r' rs rs' i, Functor g, RecElemFCtx record f) =>
(f r -> g (f r')) -> record f rs -> g (record f rs')
rlensC @_ @_ @r (\f r
_ -> f r' -> Identity (f r')
forall a. a -> Identity a
Identity f r'
y)
  {-# INLINE rputC #-}

instance (RIndex r (s ': rs) ~ 'S i, RecElem Rec r r' rs rs' i)
  => RecElem Rec r r' (s ': rs) (s ': rs') ('S i) where
  rlensC :: (f r -> g (f r')) -> Rec f (s : rs) -> g (Rec f (s : rs'))
rlensC f r -> g (f r')
f (f r
x :& Rec f rs
xs) = (Rec f rs' -> Rec f (r : rs'))
-> g (Rec f rs') -> g (Rec f (r : rs'))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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)
:&) ((f r -> g (f r')) -> Rec f rs -> g (Rec f rs')
forall k (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k)
       (rs :: [k]) (rs' :: [k]) (i :: Nat) (g :: * -> *) (f :: k -> *).
(RecElem record r r' rs rs' i, Functor g, RecElemFCtx record f) =>
(f r -> g (f r')) -> record f rs -> g (record f rs')
rlensC f r -> g (f r')
f Rec f rs
xs)
  {-# INLINE rlensC #-}
  rgetC :: Rec f (s : rs) -> f r
rgetC = Const (f r) (Rec f (s : rs')) -> f r
forall a k (b :: k). Const a b -> a
getConst (Const (f r) (Rec f (s : rs')) -> f r)
-> (Rec f (s : rs) -> Const (f r) (Rec f (s : rs')))
-> Rec f (s : rs)
-> f r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f r -> Const (f r) (f r'))
-> Rec f (s : rs) -> Const (f r) (Rec f (s : rs'))
forall k (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k)
       (rs :: [k]) (rs' :: [k]) (i :: Nat) (g :: * -> *) (f :: k -> *).
(RecElem record r r' rs rs' i, Functor g, RecElemFCtx record f) =>
(f r -> g (f r')) -> record f rs -> g (record f rs')
rlensC @_ @_ @r @r' f r -> Const (f r) (f r')
forall k a (b :: k). a -> Const a b
Const
  {-# INLINE rgetC #-}
  rputC :: f r' -> Rec f (s : rs) -> Rec f (s : rs')
rputC f r'
y = Identity (Rec f (s : rs')) -> Rec f (s : rs')
forall a. Identity a -> a
getIdentity (Identity (Rec f (s : rs')) -> Rec f (s : rs'))
-> (Rec f (s : rs) -> Identity (Rec f (s : rs')))
-> Rec f (s : rs)
-> Rec f (s : rs')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f r -> Identity (f r'))
-> Rec f (s : rs) -> Identity (Rec f (s : rs'))
forall k (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k)
       (rs :: [k]) (rs' :: [k]) (i :: Nat) (g :: * -> *) (f :: k -> *).
(RecElem record r r' rs rs' i, Functor g, RecElemFCtx record f) =>
(f r -> g (f r')) -> record f rs -> g (record f rs')
rlensC @_ @_ @r (\f r
_ -> f r' -> Identity (f r')
forall a. a -> Identity a
Identity f r'
y)
  {-# INLINE rputC #-}

--  | The 'rgetC' field getter with the type arguments re-ordered for
--  more convenient usage with @TypeApplications@.
rget :: forall r rs f record.
        (RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f)
     => record f rs -> f r
rget :: record f rs -> f r
rget = record f rs -> f r
forall k (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k)
       (rs :: [k]) (rs' :: [k]) (i :: Nat) (f :: k -> *).
(RecElem record r r' rs rs' i, RecElemFCtx record f, r ~ r') =>
record f rs -> f r
rgetC

-- | The type-changing field setter 'rputC' with the type arguments
-- re-ordered for more convenient usage with @TypeApplications@.
rput' :: forall k (r :: k) (r' :: k) (rs :: [k]) (rs' :: [k]) record f
       . (RecElem record r r' rs rs' (RIndex r rs), RecElemFCtx record f)
      => f r' -> record f rs -> record f rs'
rput' :: f r' -> record f rs -> record f rs'
rput' = forall k (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k)
       (rs :: [k]) (rs' :: [k]) (i :: Nat) (f :: k -> *).
(RecElem record r r' rs rs' i, RecElemFCtx record f) =>
f r' -> record f rs -> record f rs'
forall (i :: Nat) (f :: k -> *).
(RecElem record r r' rs rs' i, RecElemFCtx record f) =>
f r' -> record f rs -> record f rs'
rputC @k @record @r @r' @rs @rs'

-- | Type-preserving field setter. This type is simpler to work with
-- than that of 'rput''.
rput :: forall k (r :: k) rs record f. (RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f)
      => f r -> record f rs -> record f rs
rput :: f r -> record f rs -> record f rs
rput = forall k (r :: k) (r' :: k) (rs :: [k]) (rs' :: [k])
       (record :: (k -> *) -> [k] -> *) (f :: k -> *).
(RecElem record r r' rs rs' (RIndex r rs), RecElemFCtx record f) =>
f r' -> record f rs -> record f rs'
forall (f :: k -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
f r -> record f rs -> record f rs
rput' @_ @r @r @rs @rs @record

-- | Type-changing field lens 'rlensC' with the type arguments
-- re-ordered for more convenient usage with @TypeApplications@.
rlens' :: forall r r' record rs rs' f g.
          (RecElem record r r' rs rs' (RIndex r rs), RecElemFCtx record f, Functor g)
       => (f r -> g (f r')) -> record f rs -> g (record f rs')
rlens' :: (f r -> g (f r')) -> record f rs -> g (record f rs')
rlens' = (f r -> g (f r')) -> record f rs -> g (record f rs')
forall k (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k)
       (rs :: [k]) (rs' :: [k]) (i :: Nat) (g :: * -> *) (f :: k -> *).
(RecElem record r r' rs rs' i, Functor g, RecElemFCtx record f) =>
(f r -> g (f r')) -> record f rs -> g (record f rs')
rlensC

-- | Type-preserving field lens. This type is simpler to work with
-- than that of 'rlens''.
rlens :: forall r record rs f g.
         (RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f, Functor g)
       => (f r -> g (f r)) -> record f rs -> g (record f rs)
rlens :: (f r -> g (f r)) -> record f rs -> g (record f rs)
rlens = (f r -> g (f r)) -> record f rs -> g (record f rs)
forall k (record :: (k -> *) -> [k] -> *) (r :: k) (r' :: k)
       (rs :: [k]) (rs' :: [k]) (i :: Nat) (g :: * -> *) (f :: k -> *).
(RecElem record r r' rs rs' i, Functor g, RecElemFCtx record f) =>
(f r -> g (f r')) -> record f rs -> g (record f rs')
rlensC

-- | If one field set is a subset another, then a lens of from the latter's
-- record to the former's is evident. That is, we can either cast a larger
-- record to a smaller one, or we may replace the values in a slice of a
-- record.
class is ~ RImage rs ss => RecSubset record rs ss is where
  -- | An opportunity for instances to generate constraints based on
  -- the functor parameter of records passed to class methods.
  type RecSubsetFCtx record (f :: k -> *) :: Constraint
  type RecSubsetFCtx record f = ()

  -- | This is a lens into a slice of the larger record. Morally, we have:
  --
  -- > rsubset :: Lens' (Rec f ss) (Rec f rs)
  rsubsetC
    :: (Functor g, RecSubsetFCtx record f)
    => (record f rs -> g (record f rs))
    -> record f ss
    -> g (record f ss)

  -- | The getter of the 'rsubset' lens is 'rcast', which takes a larger record
  -- to a smaller one by forgetting fields.
  rcastC
    :: RecSubsetFCtx record f
    => record f ss
    -> record f rs
  rcastC = Const (record f rs) (record f ss) -> record f rs
forall a k (b :: k). Const a b -> a
getConst (Const (record f rs) (record f ss) -> record f rs)
-> (record f ss -> Const (record f rs) (record f ss))
-> record f ss
-> record f rs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (record f rs -> Const (record f rs) (record f rs))
-> record f ss -> Const (record f rs) (record f ss)
forall k k (record :: (k -> *) -> [k] -> *) (rs :: [k]) (ss :: [k])
       (is :: [Nat]) (g :: * -> *) (f :: k -> *).
(RecSubset record rs ss is, Functor g, RecSubsetFCtx record f) =>
(record f rs -> g (record f rs)) -> record f ss -> g (record f ss)
rsubsetC record f rs -> Const (record f rs) (record f rs)
forall k a (b :: k). a -> Const a b
Const
  {-# INLINE rcastC #-}

  -- | The setter of the 'rsubset' lens is 'rreplace', which allows a slice of
  -- a record to be replaced with different values.
  rreplaceC
    :: RecSubsetFCtx record f
    => record f rs
    -> record f ss
    -> record f ss
  rreplaceC record f rs
rs = Identity (record f ss) -> record f ss
forall a. Identity a -> a
getIdentity (Identity (record f ss) -> record f ss)
-> (record f ss -> Identity (record f ss))
-> record f ss
-> record f ss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (record f rs -> Identity (record f rs))
-> record f ss -> Identity (record f ss)
forall k k (record :: (k -> *) -> [k] -> *) (rs :: [k]) (ss :: [k])
       (is :: [Nat]) (g :: * -> *) (f :: k -> *).
(RecSubset record rs ss is, Functor g, RecSubsetFCtx record f) =>
(record f rs -> g (record f rs)) -> record f ss -> g (record f ss)
rsubsetC (\record f rs
_ -> record f rs -> Identity (record f rs)
forall a. a -> Identity a
Identity record f rs
rs)
  {-# INLINE rreplaceC #-}

-- | A lens into a slice of the larger record. This is 'rsubsetC' with
-- the type arguments reordered for more convenient usage with
-- @TypeApplications@.
rsubset :: forall k rs ss f g record is.
           (RecSubset record (rs :: [k]) (ss :: [k]) is,
           Functor g, RecSubsetFCtx record f)
        => (record f rs -> g (record f rs)) -> record f ss -> g (record f ss)
rsubset :: (record f rs -> g (record f rs)) -> record f ss -> g (record f ss)
rsubset = (record f rs -> g (record f rs)) -> record f ss -> g (record f ss)
forall k k (record :: (k -> *) -> [k] -> *) (rs :: [k]) (ss :: [k])
       (is :: [Nat]) (g :: * -> *) (f :: k -> *).
(RecSubset record rs ss is, Functor g, RecSubsetFCtx record f) =>
(record f rs -> g (record f rs)) -> record f ss -> g (record f ss)
rsubsetC

-- | Takes a larger record to a smaller one by forgetting fields. This
-- is 'rcastC' with the type arguments reordered for more convenient
-- usage with @TypeApplications@.
rcast :: forall rs ss f record is.
        (RecSubset record rs ss is, RecSubsetFCtx record f)
      => record f ss -> record f rs
rcast :: record f ss -> record f rs
rcast = record f ss -> record f rs
forall k k (record :: (k -> *) -> [k] -> *) (rs :: [k]) (ss :: [k])
       (is :: [Nat]) (f :: k -> *).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcastC

-- | Allows a slice of a record to be replaced with different
-- values. This is 'rreplaceC' with the type arguments reordered for
-- more convenient usage with @TypeApplications@.
rreplace :: forall rs ss f record is.
            (RecSubset record rs ss is, RecSubsetFCtx record f)
         => record f rs -> record f ss -> record f ss
rreplace :: record f rs -> record f ss -> record f ss
rreplace = record f rs -> record f ss -> record f ss
forall k k (record :: (k -> *) -> [k] -> *) (rs :: [k]) (ss :: [k])
       (is :: [Nat]) (f :: k -> *).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f rs -> record f ss -> record f ss
rreplaceC

-- | Takes a smaller record to a larger one, a /downcast/, by layering a
-- 'Maybe' interpretation that lets us use 'Nothing' for the fields
-- not present in the smaller record.
rdowncast :: (RecApplicative ss, RMap rs, rs ⊆ ss)
              => Rec f rs -> Rec (Maybe :. f) ss
rdowncast :: Rec f rs -> Rec (Maybe :. f) ss
rdowncast = (Rec (Maybe :. f) rs -> Rec (Maybe :. f) ss -> Rec (Maybe :. f) ss)
-> Rec (Maybe :. f) ss
-> Rec (Maybe :. f) rs
-> Rec (Maybe :. f) ss
forall a b c. (a -> b -> c) -> b -> a -> c
flip Rec (Maybe :. f) rs -> Rec (Maybe :. f) ss -> Rec (Maybe :. f) ss
forall k k (rs :: [k]) (ss :: [k]) (f :: k -> *)
       (record :: (k -> *) -> [k] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f rs -> record f ss -> record f ss
rreplace ((forall (x :: u). (:.) Maybe f x) -> Rec (Maybe :. f) ss
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure (Maybe (f x) -> Compose Maybe f x
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose Maybe (f x)
forall a. Maybe a
Nothing)) (Rec (Maybe :. f) rs -> Rec (Maybe :. f) ss)
-> (Rec f rs -> Rec (Maybe :. f) rs)
-> Rec f rs
-> Rec (Maybe :. f) ss
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: u). f x -> (:.) Maybe f x)
-> Rec f rs -> Rec (Maybe :. f) 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 (Maybe (f x) -> Compose Maybe f x
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (Maybe (f x) -> Compose Maybe f x)
-> (f x -> Maybe (f x)) -> f x -> Compose Maybe f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> Maybe (f x)
forall a. a -> Maybe a
Just)

type RSubset = RecSubset Rec

instance RecSubset Rec '[] ss '[] where
  rsubsetC :: (Rec f '[] -> g (Rec f '[])) -> Rec f ss -> g (Rec f ss)
rsubsetC = (Rec f ss -> Rec f '[])
-> (Rec f ss -> Rec f '[] -> Rec f ss)
-> (Rec f '[] -> g (Rec f '[]))
-> Rec f ss
-> g (Rec f ss)
forall (f :: * -> *) s a b t.
Functor f =>
(s -> a) -> (s -> b -> t) -> (a -> f b) -> s -> f t
lens (Rec f '[] -> Rec f ss -> Rec f '[]
forall a b. a -> b -> a
const Rec f '[]
forall u (f :: u -> *). Rec f '[]
RNil) Rec f ss -> Rec f '[] -> Rec f ss
forall a b. a -> b -> a
const

instance (RElem r ss i , RSubset rs ss is) => RecSubset Rec (r ': rs) ss (i ': is) where
  rsubsetC :: (Rec f (r : rs) -> g (Rec f (r : rs))) -> Rec f ss -> g (Rec f ss)
rsubsetC = (Rec f ss -> Rec f (r : rs))
-> (Rec f ss -> Rec f (r : rs) -> Rec f ss)
-> (Rec f (r : rs) -> g (Rec f (r : rs)))
-> Rec f ss
-> g (Rec f ss)
forall (f :: * -> *) s a b t.
Functor f =>
(s -> a) -> (s -> b -> t) -> (a -> f b) -> s -> f t
lens (\Rec f ss
ss -> Rec f ss -> f r
forall k (r :: k) (rs :: [k]) (f :: k -> *)
       (record :: (k -> *) -> [k] -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
record f rs -> f r
rget Rec f ss
ss 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 ss -> Rec f rs
forall k k (record :: (k -> *) -> [k] -> *) (rs :: [k]) (ss :: [k])
       (is :: [Nat]) (f :: k -> *).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcastC Rec f ss
ss) Rec f ss -> Rec f (r : rs) -> Rec f ss
forall (f :: k -> *). Rec f ss -> Rec f (r : rs) -> Rec f ss
set
    where
      set :: Rec f ss -> Rec f (r ': rs) -> Rec f ss
      set :: Rec f ss -> Rec f (r : rs) -> Rec f ss
set Rec f ss
ss (f r
r :& Rec f rs
rs) = f r -> Rec f ss -> Rec f ss
forall k (r :: k) (rs :: [k]) (record :: (k -> *) -> [k] -> *)
       (f :: k -> *).
(RecElem record r r rs rs (RIndex r rs), RecElemFCtx record f) =>
f r -> record f rs -> record f rs
rput f r
r (Rec f ss -> Rec f ss) -> Rec f ss -> Rec f ss
forall a b. (a -> b) -> a -> b
$ Rec f rs -> Rec f ss -> Rec f ss
forall k k (record :: (k -> *) -> [k] -> *) (rs :: [k]) (ss :: [k])
       (is :: [Nat]) (f :: k -> *).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f rs -> record f ss -> record f ss
rreplaceC Rec f rs
rs Rec f ss
ss

-- | Two record types are equivalent when they are subtypes of each other.
type REquivalent rs ss is js = (RSubset rs ss is, RSubset ss rs js)

-- | A shorthand for 'RElem' which supplies its index.
type r ∈ rs = RElem r rs (RIndex r rs)

-- | A shorthand for 'RSubset' which supplies its image.
type rs ⊆ ss = RSubset rs ss (RImage rs ss)

-- | A shorthand for 'REquivalent' which supplies its images.
type rs ≅ ss = REquivalent rs ss (RImage rs ss) (RImage ss rs)

-- | A non-unicode equivalent of @(⊆)@.
type rs <: ss = rs ⊆ ss

-- | A non-unicode equivalent of @(≅)@.
type rs :~: ss = rs ≅ ss