{-# LANGUAGE TypeOperators, EmptyDataDecls, RankNTypes #-}
{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, KindSignatures #-}
{-# LANGUAGE GADTs, TypeInType, PatternGuards #-}

-- |
-- Module      : Data.Type.RList
-- Copyright   : (c) 2016 Edwin Westbrook
--
-- License     : BSD3
--
-- Maintainer  : westbrook@galois.com
-- Stability   : experimental
-- Portability : GHC
--
-- A /right list/, or 'RList', is a list where cons adds to the end, or the
-- right-hand side, of a list. This is useful conceptually for contexts of
-- name-bindings, where the most recent name-binding is intuitively at the end
-- of the context.

module Data.Type.RList where

import Prelude hiding (map, foldr)
import Data.Kind
import Data.Type.Equality
import Data.Proxy (Proxy(..))
import Data.Functor.Constant
import Data.Typeable

-------------------------------------------------------------------------------
-- * Right-lists as a datatype
-------------------------------------------------------------------------------

-- | A form of lists where elements are added to the right instead of the left
data RList a
  = RNil
  | (RList a) :> a

-- | Append two 'RList's at the type level
type family ((r1 :: RList k) :++: (r2 :: RList k)) :: RList k
infixr 5 :++:
type instance (r :++: 'RNil) = r
type instance (r1 :++: (r2 ':> a)) = (r1 :++: r2) ':> a

-------------------------------------------------------------------------------
-- * Proofs of membership in a type-level list
-------------------------------------------------------------------------------

{-|
  A @Member ctx a@ is a \"proof\" that the type @a@ is in the type
  list @ctx@, meaning that @ctx@ equals

>  t0 ':>' a ':>' t1 ':>' ... ':>' tn

  for some types @t0,t1,...,tn@.
-}
data Member (ctx :: RList k1) (a :: k2) where
  Member_Base :: Member (ctx :> a) a
  Member_Step :: Member ctx a -> Member (ctx :> b) a
  deriving Typeable

instance Show (Member r a) where
  showsPrec :: Int -> Member r a -> ShowS
showsPrec Int
p = Bool -> Member r a -> ShowS
forall k1 k2 (ctx :: RList k1) (a :: k2).
Bool -> Member ctx a -> ShowS
showsPrecMember (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) where
    showsPrecMember :: Bool -> Member ctx a -> ShowS
    showsPrecMember :: Bool -> Member ctx a -> ShowS
showsPrecMember Bool
_ Member ctx a
Member_Base = String -> ShowS
showString String
"Member_Base"
    showsPrecMember Bool
p (Member_Step Member ctx a
prf) = Bool -> ShowS -> ShowS
showParen Bool
p (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString String
"Member_Step" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Member ctx a -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 Member ctx a
prf

instance TestEquality (Member ctx) where
  testEquality :: Member ctx a -> Member ctx b -> Maybe (a :~: b)
testEquality Member ctx a
Member_Base Member ctx b
Member_Base = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
  testEquality (Member_Step Member ctx a
memb1) (Member_Step Member ctx b
memb2)
    | Just a :~: b
Refl <- Member ctx a -> Member ctx b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality Member ctx a
memb1 Member ctx b
Member ctx b
memb2
    = (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl
  testEquality Member ctx a
_ Member ctx b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance Eq (Member ctx a) where
  Member ctx a
Member_Base == :: Member ctx a -> Member ctx a -> Bool
== Member ctx a
Member_Base = Bool
True
  (Member_Step Member ctx a
memb1) == (Member_Step Member ctx a
memb2) = Member ctx a
memb1 Member ctx a -> Member ctx a -> Bool
forall a. Eq a => a -> a -> Bool
== Member ctx a
Member ctx a
memb2
  Member ctx a
_ == Member ctx a
_ = Bool
False

--toEq :: Member (Nil :> a) b -> b :~: a
--toEq Member_Base = Refl
--toEq _ = error "Should not happen! (toEq)"

-- | Weaken a 'Member' proof by prepending another context to the context it
-- proves membership in
weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
weakenMemberL Proxy r1
_ Member r2 a
Member_Base = Member (r1 :++: r2) a
forall k2 (ctx :: RList k2) (ctx :: k2). Member (ctx ':> ctx) ctx
Member_Base
weakenMemberL Proxy r1
tag (Member_Step Member ctx a
mem) = Member (r1 :++: ctx) a -> Member ((r1 :++: ctx) ':> b) a
forall k1 k2 (ctx :: RList k1) (a :: k2) (b :: k1).
Member ctx a -> Member (ctx ':> b) a
Member_Step (Proxy r1 -> Member ctx a -> Member (r1 :++: ctx) a
forall k1 k2 (r1 :: RList k1) (r2 :: RList k1) (a :: k2).
Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
weakenMemberL Proxy r1
tag Member ctx a
mem)


------------------------------------------------------------
-- * Proofs that one list equals the append of two others
------------------------------------------------------------

{-|
  An @Append ctx1 ctx2 ctx@ is a \"proof\" that @ctx = ctx1 ':++:' ctx2@.
-}
data Append ctx1 ctx2 ctx where
  Append_Base :: Append ctx RNil ctx
  Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)

-- | Make an 'Append' proof from any 'RAssign' vector for the second
-- argument of the append.
mkAppend :: RAssign f c2 -> Append c1 c2 (c1 :++: c2)
mkAppend :: RAssign f c2 -> Append c1 c2 (c1 :++: c2)
mkAppend RAssign f c2
MNil = Append c1 c2 (c1 :++: c2)
forall a (ctx :: RList a). Append ctx 'RNil ctx
Append_Base
mkAppend (RAssign f c
c :>: f a
_) = Append c1 c (c1 :++: c) -> Append c1 (c ':> a) ((c1 :++: c) ':> a)
forall a (ctx1 :: RList a) (ctx2 :: RList a) (ctx :: RList a)
       (a :: a).
Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 ':> a) (ctx ':> a)
Append_Step (RAssign f c -> Append c1 c (c1 :++: c)
forall k (f :: k -> *) (c2 :: RList k) (c1 :: RList k).
RAssign f c2 -> Append c1 c2 (c1 :++: c2)
mkAppend RAssign f c
c)

-- | A version of 'mkAppend' that takes in a 'Proxy' argument.
mkMonoAppend :: Proxy c1 -> RAssign f c2 -> Append c1 c2 (c1 :++: c2)
mkMonoAppend :: Proxy c1 -> RAssign f c2 -> Append c1 c2 (c1 :++: c2)
mkMonoAppend Proxy c1
_ = RAssign f c2 -> Append c1 c2 (c1 :++: c2)
forall k (f :: k -> *) (c2 :: RList k) (c1 :: RList k).
RAssign f c2 -> Append c1 c2 (c1 :++: c2)
mkAppend

-- | The inverse of 'mkAppend', that builds an 'RAssign' from an 'Append'
proxiesFromAppend :: Append c1 c2 c -> RAssign Proxy c2
proxiesFromAppend :: Append c1 c2 c -> RAssign Proxy c2
proxiesFromAppend Append c1 c2 c
Append_Base = RAssign Proxy c2
forall k (f :: k -> *). RAssign f 'RNil
MNil
proxiesFromAppend (Append_Step Append c1 ctx2 ctx
a) = Append c1 ctx2 ctx -> RAssign Proxy ctx2
forall k (c1 :: RList k) (c2 :: RList k) (c :: RList k).
Append c1 c2 c -> RAssign Proxy c2
proxiesFromAppend Append c1 ctx2 ctx
a RAssign Proxy ctx2 -> Proxy a -> RAssign Proxy (ctx2 ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Proxy a
forall k (t :: k). Proxy t
Proxy


-------------------------------------------------------------------------------
-- * Contexts
-------------------------------------------------------------------------------

{-|
  An @RAssign f r@ an assignment of an @f a@ for each @a@ in the 'RList' @r@
-}
data RAssign (f :: k -> *) (c :: RList k) where
  MNil :: RAssign f RNil
  (:>:) :: RAssign f c -> f a -> RAssign f (c :> a)

-- | Create an empty 'RAssign' vector.
empty :: RAssign f RNil
empty :: RAssign f 'RNil
empty = RAssign f 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil

-- | Create a singleton 'RAssign' vector.
singleton :: f a -> RAssign f (RNil :> a)
singleton :: f a -> RAssign f ('RNil ':> a)
singleton f a
x = RAssign f 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil RAssign f 'RNil -> f a -> RAssign f ('RNil ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: f a
x

-- | Look up an element of an 'RAssign' vector using a 'Member' proof
get :: Member c a -> RAssign f c -> f a
get :: Member c a -> RAssign f c -> f a
get Member c a
Member_Base (RAssign f c
_ :>: f a
x) = f a
f a
x
get (Member_Step Member ctx a
mem') (RAssign f c
mc :>: f a
_) = Member ctx a -> RAssign f ctx -> f a
forall k (c :: RList k) (a :: k) (f :: k -> *).
Member c a -> RAssign f c -> f a
get Member ctx a
mem' RAssign f ctx
RAssign f c
mc

-- | Heterogeneous type application, including a proof that the input kind of
-- the function equals the kind of the type argument
data HApply (f :: k1 -> Type) (a :: k2) where
  HApply :: forall k (f :: k -> Type) (a :: k). f a -> HApply f a

-- | Look up an element of an 'RAssign' vector using a 'Member' proof at what
-- GHC thinks might be a different kind, i.e., heterogeneously
hget :: forall k1 k2 (f :: k1 -> Type) (c :: RList k1) (a :: k2).
        Member c a -> RAssign f c -> HApply f a
hget :: Member c a -> RAssign f c -> HApply f a
hget Member c a
Member_Base (RAssign f c
_ :>: f a
x) = f a -> HApply f a
forall k (f :: k -> *) (a :: k). f a -> HApply f a
HApply f a
x
hget (Member_Step Member ctx a
mem') (RAssign f c
mc :>: f a
_) = Member ctx a -> RAssign f ctx -> HApply f a
forall k1 k2 (f :: k1 -> *) (c :: RList k1) (a :: k2).
Member c a -> RAssign f c -> HApply f a
hget Member ctx a
mem' RAssign f ctx
RAssign f c
mc

-- | Modify an element of an 'RAssign' vector using a 'Member' proof.
modify :: Member c a -> (f a -> f a) -> RAssign f c -> RAssign f c
modify :: Member c a -> (f a -> f a) -> RAssign f c -> RAssign f c
modify Member c a
Member_Base f a -> f a
f (RAssign f c
xs :>: f a
x) = RAssign f c
xs RAssign f c -> f a -> RAssign f (c ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: f a -> f a
f f a
f a
x
modify (Member_Step Member ctx a
mem') f a -> f a
f (RAssign f c
xs :>: f a
x) = Member ctx a -> (f a -> f a) -> RAssign f ctx -> RAssign f ctx
forall k (c :: RList k) (a :: k) (f :: k -> *).
Member c a -> (f a -> f a) -> RAssign f c -> RAssign f c
modify Member ctx a
mem' f a -> f a
f RAssign f ctx
RAssign f c
xs RAssign f ctx -> f a -> RAssign f (ctx ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: f a
x

-- | Set an element of an 'RAssign' vector using a 'Member' proof.
set :: Member c a -> f a -> RAssign f c -> RAssign f c
set :: Member c a -> f a -> RAssign f c -> RAssign f c
set Member c a
memb f a
x = Member c a -> (f a -> f a) -> RAssign f c -> RAssign f c
forall k (c :: RList k) (a :: k) (f :: k -> *).
Member c a -> (f a -> f a) -> RAssign f c -> RAssign f c
modify Member c a
memb (f a -> f a -> f a
forall a b. a -> b -> a
const f a
x)

-- | Test if an object is in an 'RAssign', returning a 'Member' proof if it is
memberElem :: TestEquality f => f a -> RAssign f ctx -> Maybe (Member ctx a)
memberElem :: f a -> RAssign f ctx -> Maybe (Member ctx a)
memberElem f a
_ RAssign f ctx
MNil = Maybe (Member ctx a)
forall a. Maybe a
Nothing
memberElem f a
x (RAssign f c
_ :>: f a
y) | Just a :~: a
Refl <- f a -> f a -> Maybe (a :~: a)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f a
x f a
y = Member (c ':> a) a -> Maybe (Member (c ':> a) a)
forall a. a -> Maybe a
Just Member (c ':> a) a
forall k2 (ctx :: RList k2) (ctx :: k2). Member (ctx ':> ctx) ctx
Member_Base
memberElem f a
x (RAssign f c
xs :>: f a
_) = (Member c a -> Member (c ':> a) a)
-> Maybe (Member c a) -> Maybe (Member (c ':> a) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Member c a -> Member (c ':> a) a
forall k1 k2 (ctx :: RList k1) (a :: k2) (b :: k1).
Member ctx a -> Member (ctx ':> b) a
Member_Step (Maybe (Member c a) -> Maybe (Member (c ':> a) a))
-> Maybe (Member c a) -> Maybe (Member (c ':> a) a)
forall a b. (a -> b) -> a -> b
$ f a -> RAssign f c -> Maybe (Member c a)
forall k2 (f :: k2 -> *) (a :: k2) (ctx :: RList k2).
TestEquality f =>
f a -> RAssign f ctx -> Maybe (Member ctx a)
memberElem f a
x RAssign f c
xs

-- | Map a function on all elements of an 'RAssign' vector.
map :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c
map :: (forall (x :: k). f x -> g x) -> RAssign f c -> RAssign g c
map forall (x :: k). f x -> g x
_ RAssign f c
MNil = RAssign g c
forall k (f :: k -> *). RAssign f 'RNil
MNil
map forall (x :: k). f x -> g x
f (RAssign f c
mc :>: f a
x) = (forall (x :: k). f x -> g x) -> RAssign f c -> RAssign g c
forall k (f :: k -> *) (g :: k -> *) (c :: RList k).
(forall (x :: k). f x -> g x) -> RAssign f c -> RAssign g c
map forall (x :: k). f x -> g x
f RAssign f c
mc RAssign g c -> g a -> RAssign g (c ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: f a -> g a
forall (x :: k). f x -> g x
f f a
x

-- | An alternate name for 'map' that does not clash with the prelude
mapRAssign :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c
mapRAssign :: (forall (x :: k). f x -> g x) -> RAssign f c -> RAssign g c
mapRAssign = (forall (x :: k). f x -> g x) -> RAssign f c -> RAssign g c
forall k (f :: k -> *) (g :: k -> *) (c :: RList k).
(forall (x :: k). f x -> g x) -> RAssign f c -> RAssign g c
map

-- | Map a binary function on all pairs of elements of two 'RAssign' vectors.
map2 :: (forall x. f x -> g x -> h x) ->
                RAssign f c -> RAssign g c -> RAssign h c
map2 :: (forall (x :: k). f x -> g x -> h x)
-> RAssign f c -> RAssign g c -> RAssign h c
map2 forall (x :: k). f x -> g x -> h x
_ RAssign f c
MNil RAssign g c
MNil = RAssign h c
forall k (f :: k -> *). RAssign f 'RNil
MNil
map2 forall (x :: k). f x -> g x -> h x
f (RAssign f c
xs :>: f a
x) (RAssign g c
ys :>: g a
y) = (forall (x :: k). f x -> g x -> h x)
-> RAssign f c -> RAssign g c -> RAssign h c
forall k (f :: k -> *) (g :: k -> *) (h :: k -> *) (c :: RList k).
(forall (x :: k). f x -> g x -> h x)
-> RAssign f c -> RAssign g c -> RAssign h c
map2 forall (x :: k). f x -> g x -> h x
f RAssign f c
xs RAssign g c
RAssign g c
ys RAssign h c -> h a -> RAssign h (c ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: f a -> g a -> h a
forall (x :: k). f x -> g x -> h x
f f a
x g a
g a
y

-- | Take the tail of an 'RAssign'
tail :: RAssign f (ctx :> a) -> RAssign f ctx
tail :: RAssign f (ctx ':> a) -> RAssign f ctx
tail (RAssign f c
xs :>: f a
_) = RAssign f ctx
RAssign f c
xs

-- | Convert a monomorphic 'RAssign' to a list
toList :: RAssign (Constant a) c -> [a]
toList :: RAssign (Constant a) c -> [a]
toList = (forall (a :: k). Constant a a -> a)
-> RAssign (Constant a) c -> [a]
forall k (f :: k -> *) b (ctx :: RList k).
(forall (a :: k). f a -> b) -> RAssign f ctx -> [b]
mapToList forall (a :: k). Constant a a -> a
forall a k (b :: k). Constant a b -> a
getConstant

-- | Map a function with monomorphic output type across an 'RAssign' to create a
-- standard list:
--
-- > mapToList f = toList . map (Constant . f)
mapToList :: (forall a. f a -> b) -> RAssign f ctx -> [b]
mapToList :: (forall (a :: k). f a -> b) -> RAssign f ctx -> [b]
mapToList forall (a :: k). f a -> b
_ RAssign f ctx
MNil = []
mapToList forall (a :: k). f a -> b
f (RAssign f c
xs :>: f a
x) = (forall (a :: k). f a -> b) -> RAssign f c -> [b]
forall k (f :: k -> *) b (ctx :: RList k).
(forall (a :: k). f a -> b) -> RAssign f ctx -> [b]
mapToList forall (a :: k). f a -> b
f RAssign f c
xs [b] -> [b] -> [b]
forall a. [a] -> [a] -> [a]
++ [f a -> b
forall (a :: k). f a -> b
f f a
x]

-- | Append two 'RAssign' vectors.
append :: RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2)
append :: RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2)
append RAssign f c1
mc RAssign f c2
MNil = RAssign f c1
RAssign f (c1 :++: c2)
mc
append RAssign f c1
mc1 (RAssign f c
mc2 :>: f a
x) = RAssign f c1 -> RAssign f c -> RAssign f (c1 :++: c)
forall k (f :: k -> *) (c1 :: RList k) (c2 :: RList k).
RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2)
append RAssign f c1
mc1 RAssign f c
mc2 RAssign f (c1 :++: c) -> f a -> RAssign f ((c1 :++: c) ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: f a
x

-- | Perform a right fold across an 'RAssign'
foldr :: (forall a. f a -> r -> r) -> r -> RAssign f ctx -> r
foldr :: (forall (a :: k). f a -> r -> r) -> r -> RAssign f ctx -> r
foldr forall (a :: k). f a -> r -> r
_ r
r RAssign f ctx
MNil = r
r
foldr forall (a :: k). f a -> r -> r
f r
r (RAssign f c
xs :>: f a
x) = f a -> r -> r
forall (a :: k). f a -> r -> r
f f a
x (r -> r) -> r -> r
forall a b. (a -> b) -> a -> b
$ (forall (a :: k). f a -> r -> r) -> r -> RAssign f c -> r
forall k (f :: k -> *) r (ctx :: RList k).
(forall (a :: k). f a -> r -> r) -> r -> RAssign f ctx -> r
foldr forall (a :: k). f a -> r -> r
f r
r RAssign f c
xs

-- | Split an 'RAssign' vector into two pieces. The first argument is a
-- phantom argument that gives the form of the first list piece.
split :: (c ~ (c1 :++: c2)) => prx c1 ->
                 RAssign any c2 -> RAssign f c -> (RAssign f c1, RAssign f c2)
split :: prx c1
-> RAssign any c2 -> RAssign f c -> (RAssign f c1, RAssign f c2)
split prx c1
_ RAssign any c2
MNil RAssign f c
mc = (RAssign f c
RAssign f c1
mc, RAssign f c2
forall k (f :: k -> *). RAssign f 'RNil
MNil)
split prx c1
_ (RAssign any c
any :>: any a
_) (RAssign f c
mc :>: f a
x) = (RAssign f c1
mc1, RAssign f c
mc2 RAssign f c -> f a -> RAssign f (c ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: f a
x)
  where (RAssign f c1
mc1, RAssign f c
mc2) = Proxy c1
-> RAssign any c -> RAssign f c -> (RAssign f c1, RAssign f c)
forall k (c :: RList k) (c1 :: RList k) (c2 :: RList k)
       (prx :: RList k -> *) (any :: k -> *) (f :: k -> *).
(c ~ (c1 :++: c2)) =>
prx c1
-> RAssign any c2 -> RAssign f c -> (RAssign f c1, RAssign f c2)
split Proxy c1
forall k (t :: k). Proxy t
Proxy RAssign any c
any RAssign f c
mc

-- | Create a vector of proofs that each type in @c@ is a 'Member' of @c@.
members :: RAssign f c -> RAssign (Member c) c
members :: RAssign f c -> RAssign (Member c) c
members RAssign f c
MNil = RAssign (Member c) c
forall k (f :: k -> *). RAssign f 'RNil
MNil
members (RAssign f c
c :>: f a
_) = (forall (x :: k). Member c x -> Member (c ':> a) x)
-> RAssign (Member c) c -> RAssign (Member (c ':> a)) c
forall k (f :: k -> *) (g :: k -> *) (c :: RList k).
(forall (x :: k). f x -> g x) -> RAssign f c -> RAssign g c
map forall (x :: k). Member c x -> Member (c ':> a) x
forall k1 k2 (ctx :: RList k1) (a :: k2) (b :: k1).
Member ctx a -> Member (ctx ':> b) a
Member_Step (RAssign f c -> RAssign (Member c) c
forall k (f :: k -> *) (c :: RList k).
RAssign f c -> RAssign (Member c) c
members RAssign f c
c) RAssign (Member (c ':> a)) c
-> Member (c ':> a) a -> RAssign (Member (c ':> a)) (c ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Member (c ':> a) a
forall k2 (ctx :: RList k2) (ctx :: k2). Member (ctx ':> ctx) ctx
Member_Base

-- | A type-class which ensures that ctx is a valid context, i.e., has
-- | the form (RNil :> t1 :> ... :> tn) for some types t1 through tn
class TypeCtx ctx where
  typeCtxProxies :: RAssign Proxy ctx

instance TypeCtx RNil where
  typeCtxProxies :: RAssign Proxy 'RNil
typeCtxProxies = RAssign Proxy 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil

instance TypeCtx ctx => TypeCtx (ctx :> a) where
  typeCtxProxies :: RAssign Proxy (ctx ':> a)
typeCtxProxies = RAssign Proxy ctx
forall k (ctx :: RList k). TypeCtx ctx => RAssign Proxy ctx
typeCtxProxies RAssign Proxy ctx -> Proxy a -> RAssign Proxy (ctx ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Proxy a
forall k (t :: k). Proxy t
Proxy