Copyright	2009-2015 Edward Kmett
License	BSD3
Maintainer	Edward Kmett <ekmett@gmail.com>
Stability	experimental
Portability	portable
Safe Haskell	Safe
Language	Haskell98

Data.Tagged

Contents

Tagged values
Conversion
Proxy methods GHC dropped

Description

Synopsis

newtype Tagged (s :: k) b = Tagged {
- unTagged :: b
}
retag :: forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
untag :: forall {k} (s :: k) b. Tagged s b -> b
tagSelf :: a -> Tagged a a
untagSelf :: Tagged a a -> a
asTaggedTypeOf :: forall {k} s tagged (b :: k). s -> tagged s b -> s
witness :: Tagged a b -> a -> b
proxy :: forall {k} (s :: k) a proxy. Tagged s a -> proxy s -> a
unproxy :: forall {k} (s :: k) a. (Proxy s -> a) -> Tagged s a
tagWith :: forall {k} proxy (s :: k) a. proxy s -> a -> Tagged s a
reproxy :: forall {k1} {k2} proxy (a :: k1) (b :: k2). proxy a -> Proxy b

Tagged values

newtype Tagged (s :: k) b Source #

A Tagged s b value is a value b with an attached phantom type s. This can be used in place of the more traditional but less safe idiom of passing in an undefined value with the type, because unlike an (s -> b), a Tagged s b can't try to use the argument s as a real value.

Moreover, you don't have to rely on the compiler to inline away the extra argument, because the newtype is "free"

Tagged has kind k -> * -> * if the compiler supports PolyKinds, therefore there is an extra k showing in the instance haddocks that may cause confusion.

Constructors

Tagged
Fields unTagged :: b

Instances

Instances details

Generic1 (Tagged s :: Type -> Type) Source #

Instance details

Defined in Data.Tagged

Associated Types

type Rep1 (Tagged s :: Type -> Type)
Instance details Defined in Data.Tagged type Rep1 (Tagged s :: Type -> Type) = D1 ('MetaData "Tagged" "Data.Tagged" "tagged-0.8.10-IUw8S1MEcty60WZUz6twze" 'True) (C1 ('MetaCons "Tagged" 'PrefixI 'True) (S1 ('MetaSel ('Just "unTagged") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1))

Methods

from1 :: Tagged s a -> Rep1 (Tagged s) a

to1 :: Rep1 (Tagged s) a -> Tagged s a

Bifoldable (Tagged :: Type -> Type -> Type) Source #

Instance details

Defined in Data.Tagged

Methods

bifold :: Monoid m => Tagged m m -> m

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Tagged a b -> m

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Tagged a b -> c

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Tagged a b -> c

Bifoldable1 (Tagged :: Type -> Type -> Type) Source #

Instance details

Defined in Data.Tagged

Methods

bifold1 :: Semigroup m => Tagged m m -> m

bifoldMap1 :: Semigroup m => (a -> m) -> (b -> m) -> Tagged a b -> m

Bifunctor (Tagged :: Type -> Type -> Type) Source #

Instance details

Defined in Data.Tagged

Methods

bimap :: (a -> b) -> (c -> d) -> Tagged a c -> Tagged b d

first :: (a -> b) -> Tagged a c -> Tagged b c

second :: (b -> c) -> Tagged a b -> Tagged a c

Bitraversable (Tagged :: Type -> Type -> Type) Source #

Instance details

Defined in Data.Tagged

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Tagged a b -> f (Tagged c d)

Eq2 (Tagged :: Type -> Type -> Type) Source #

Instance details

Defined in Data.Tagged

Methods

liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> Tagged a c -> Tagged b d -> Bool

Ord2 (Tagged :: Type -> Type -> Type) Source #

Instance details

Defined in Data.Tagged

Methods

liftCompare2 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> Tagged a c -> Tagged b d -> Ordering

Read2 (Tagged :: Type -> Type -> Type) Source #

Instance details

Defined in Data.Tagged

Methods

liftReadsPrec2 :: (Int -> ReadS a) -> ReadS [a] -> (Int -> ReadS b) -> ReadS [b] -> Int -> ReadS (Tagged a b)

liftReadList2 :: (Int -> ReadS a) -> ReadS [a] -> (Int -> ReadS b) -> ReadS [b] -> ReadS [Tagged a b]

liftReadPrec2 :: ReadPrec a -> ReadPrec [a] -> ReadPrec b -> ReadPrec [b] -> ReadPrec (Tagged a b)

liftReadListPrec2 :: ReadPrec a -> ReadPrec [a] -> ReadPrec b -> ReadPrec [b] -> ReadPrec [Tagged a b]

Show2 (Tagged :: Type -> Type -> Type) Source #

Instance details

Defined in Data.Tagged

Methods

liftShowsPrec2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> Int -> Tagged a b -> ShowS

liftShowList2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> [Tagged a b] -> ShowS

Foldable1 (Tagged a) Source #

Instance details

Defined in Data.Tagged

Methods

fold1 :: Semigroup m => Tagged a m -> m

foldMap1 :: Semigroup m => (a0 -> m) -> Tagged a a0 -> m

foldMap1' :: Semigroup m => (a0 -> m) -> Tagged a a0 -> m

toNonEmpty :: Tagged a a0 -> NonEmpty a0

maximum :: Ord a0 => Tagged a a0 -> a0

minimum :: Ord a0 => Tagged a a0 -> a0

head :: Tagged a a0 -> a0

last :: Tagged a a0 -> a0

foldrMap1 :: (a0 -> b) -> (a0 -> b -> b) -> Tagged a a0 -> b

foldlMap1' :: (a0 -> b) -> (b -> a0 -> b) -> Tagged a a0 -> b

foldlMap1 :: (a0 -> b) -> (b -> a0 -> b) -> Tagged a a0 -> b

foldrMap1' :: (a0 -> b) -> (a0 -> b -> b) -> Tagged a a0 -> b

Eq1 (Tagged s) Source #

Instance details

Defined in Data.Tagged

Methods

liftEq :: (a -> b -> Bool) -> Tagged s a -> Tagged s b -> Bool

Ord1 (Tagged s) Source #

Instance details

Defined in Data.Tagged

Methods

liftCompare :: (a -> b -> Ordering) -> Tagged s a -> Tagged s b -> Ordering

Read1 (Tagged s) Source #

Instance details

Defined in Data.Tagged

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Tagged s a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Tagged s a]

liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Tagged s a)

liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Tagged s a]

Show1 (Tagged s) Source #

Instance details

Defined in Data.Tagged

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Tagged s a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Tagged s a] -> ShowS

Applicative (Tagged s) Source #

Instance details

Defined in Data.Tagged

Methods

pure :: a -> Tagged s a

(<*>) :: Tagged s (a -> b) -> Tagged s a -> Tagged s b

liftA2 :: (a -> b -> c) -> Tagged s a -> Tagged s b -> Tagged s c

(*>) :: Tagged s a -> Tagged s b -> Tagged s b

(<*) :: Tagged s a -> Tagged s b -> Tagged s a

Functor (Tagged s) Source #

Instance details

Defined in Data.Tagged

Methods

fmap :: (a -> b) -> Tagged s a -> Tagged s b

(<$) :: a -> Tagged s b -> Tagged s a

Monad (Tagged s) Source #

Instance details

Defined in Data.Tagged

Methods

(>>=) :: Tagged s a -> (a -> Tagged s b) -> Tagged s b

(>>) :: Tagged s a -> Tagged s b -> Tagged s b

return :: a -> Tagged s a

Foldable (Tagged s) Source #

Instance details

Defined in Data.Tagged

Methods

fold :: Monoid m => Tagged s m -> m

foldMap :: Monoid m => (a -> m) -> Tagged s a -> m

foldMap' :: Monoid m => (a -> m) -> Tagged s a -> m

foldr :: (a -> b -> b) -> b -> Tagged s a -> b

foldr' :: (a -> b -> b) -> b -> Tagged s a -> b

foldl :: (b -> a -> b) -> b -> Tagged s a -> b

foldl' :: (b -> a -> b) -> b -> Tagged s a -> b

foldr1 :: (a -> a -> a) -> Tagged s a -> a

foldl1 :: (a -> a -> a) -> Tagged s a -> a

toList :: Tagged s a -> [a]

null :: Tagged s a -> Bool

length :: Tagged s a -> Int

elem :: Eq a => a -> Tagged s a -> Bool

maximum :: Ord a => Tagged s a -> a

minimum :: Ord a => Tagged s a -> a

sum :: Num a => Tagged s a -> a

product :: Num a => Tagged s a -> a

Traversable (Tagged s) Source #

Instance details

Defined in Data.Tagged

Methods

traverse :: Applicative f => (a -> f b) -> Tagged s a -> f (Tagged s b)

sequenceA :: Applicative f => Tagged s (f a) -> f (Tagged s a)

mapM :: Monad m => (a -> m b) -> Tagged s a -> m (Tagged s b)

sequence :: Monad m => Tagged s (m a) -> m (Tagged s a)

NFData b => NFData (Tagged s b) Source #

Instance details

Defined in Data.Tagged

Methods

rnf :: Tagged s b -> ()

(Semigroup a, Monoid a) => Monoid (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

mempty :: Tagged s a

mappend :: Tagged s a -> Tagged s a -> Tagged s a

mconcat :: [Tagged s a] -> Tagged s a

Semigroup a => Semigroup (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

(<>) :: Tagged s a -> Tagged s a -> Tagged s a

sconcat :: NonEmpty (Tagged s a) -> Tagged s a

stimes :: Integral b => b -> Tagged s a -> Tagged s a

Bits a => Bits (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

(.&.) :: Tagged s a -> Tagged s a -> Tagged s a

(.|.) :: Tagged s a -> Tagged s a -> Tagged s a

xor :: Tagged s a -> Tagged s a -> Tagged s a

complement :: Tagged s a -> Tagged s a

shift :: Tagged s a -> Int -> Tagged s a

rotate :: Tagged s a -> Int -> Tagged s a

zeroBits :: Tagged s a

bit :: Int -> Tagged s a

setBit :: Tagged s a -> Int -> Tagged s a

clearBit :: Tagged s a -> Int -> Tagged s a

complementBit :: Tagged s a -> Int -> Tagged s a

testBit :: Tagged s a -> Int -> Bool

bitSizeMaybe :: Tagged s a -> Maybe Int

bitSize :: Tagged s a -> Int

isSigned :: Tagged s a -> Bool

shiftL :: Tagged s a -> Int -> Tagged s a

unsafeShiftL :: Tagged s a -> Int -> Tagged s a

shiftR :: Tagged s a -> Int -> Tagged s a

unsafeShiftR :: Tagged s a -> Int -> Tagged s a

rotateL :: Tagged s a -> Int -> Tagged s a

rotateR :: Tagged s a -> Int -> Tagged s a

popCount :: Tagged s a -> Int

FiniteBits a => FiniteBits (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

finiteBitSize :: Tagged s a -> Int

countLeadingZeros :: Tagged s a -> Int

countTrailingZeros :: Tagged s a -> Int

(Data s, Data b) => Data (Tagged s b) Source #

Instance details

Defined in Data.Tagged

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Tagged s b -> c (Tagged s b)

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Tagged s b)

toConstr :: Tagged s b -> Constr

dataTypeOf :: Tagged s b -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Tagged s b))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Tagged s b))

gmapT :: (forall b0. Data b0 => b0 -> b0) -> Tagged s b -> Tagged s b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Tagged s b -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Tagged s b -> r

gmapQ :: (forall d. Data d => d -> u) -> Tagged s b -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Tagged s b -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Tagged s b -> m (Tagged s b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Tagged s b -> m (Tagged s b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Tagged s b -> m (Tagged s b)

IsString a => IsString (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

fromString :: String -> Tagged s a

Bounded b => Bounded (Tagged s b) Source #

Instance details

Defined in Data.Tagged

Methods

minBound :: Tagged s b

maxBound :: Tagged s b

Enum a => Enum (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

succ :: Tagged s a -> Tagged s a

pred :: Tagged s a -> Tagged s a

toEnum :: Int -> Tagged s a

fromEnum :: Tagged s a -> Int

enumFrom :: Tagged s a -> [Tagged s a]

enumFromThen :: Tagged s a -> Tagged s a -> [Tagged s a]

enumFromTo :: Tagged s a -> Tagged s a -> [Tagged s a]

enumFromThenTo :: Tagged s a -> Tagged s a -> Tagged s a -> [Tagged s a]

Floating a => Floating (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

pi :: Tagged s a

exp :: Tagged s a -> Tagged s a

log :: Tagged s a -> Tagged s a

sqrt :: Tagged s a -> Tagged s a

(**) :: Tagged s a -> Tagged s a -> Tagged s a

logBase :: Tagged s a -> Tagged s a -> Tagged s a

sin :: Tagged s a -> Tagged s a

cos :: Tagged s a -> Tagged s a

tan :: Tagged s a -> Tagged s a

asin :: Tagged s a -> Tagged s a

acos :: Tagged s a -> Tagged s a

atan :: Tagged s a -> Tagged s a

sinh :: Tagged s a -> Tagged s a

cosh :: Tagged s a -> Tagged s a

tanh :: Tagged s a -> Tagged s a

asinh :: Tagged s a -> Tagged s a

acosh :: Tagged s a -> Tagged s a

atanh :: Tagged s a -> Tagged s a

log1p :: Tagged s a -> Tagged s a

expm1 :: Tagged s a -> Tagged s a

log1pexp :: Tagged s a -> Tagged s a

log1mexp :: Tagged s a -> Tagged s a

RealFloat a => RealFloat (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

floatRadix :: Tagged s a -> Integer

floatDigits :: Tagged s a -> Int

floatRange :: Tagged s a -> (Int, Int)

decodeFloat :: Tagged s a -> (Integer, Int)

encodeFloat :: Integer -> Int -> Tagged s a

exponent :: Tagged s a -> Int

significand :: Tagged s a -> Tagged s a

scaleFloat :: Int -> Tagged s a -> Tagged s a

isNaN :: Tagged s a -> Bool

isInfinite :: Tagged s a -> Bool

isDenormalized :: Tagged s a -> Bool

isNegativeZero :: Tagged s a -> Bool

isIEEE :: Tagged s a -> Bool

atan2 :: Tagged s a -> Tagged s a -> Tagged s a

Storable a => Storable (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

sizeOf :: Tagged s a -> Int

alignment :: Tagged s a -> Int

peekElemOff :: Ptr (Tagged s a) -> Int -> IO (Tagged s a)

pokeElemOff :: Ptr (Tagged s a) -> Int -> Tagged s a -> IO ()

peekByteOff :: Ptr b -> Int -> IO (Tagged s a)

pokeByteOff :: Ptr b -> Int -> Tagged s a -> IO ()

peek :: Ptr (Tagged s a) -> IO (Tagged s a)

poke :: Ptr (Tagged s a) -> Tagged s a -> IO ()

Generic (Tagged s b) Source #

Instance details

Defined in Data.Tagged

Associated Types

type Rep (Tagged s b)
Instance details Defined in Data.Tagged type Rep (Tagged s b) = D1 ('MetaData "Tagged" "Data.Tagged" "tagged-0.8.10-IUw8S1MEcty60WZUz6twze" 'True) (C1 ('MetaCons "Tagged" 'PrefixI 'True) (S1 ('MetaSel ('Just "unTagged") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)))

Methods

from :: Tagged s b -> Rep (Tagged s b) x

to :: Rep (Tagged s b) x -> Tagged s b

Ix b => Ix (Tagged s b) Source #

Instance details

Defined in Data.Tagged

Methods

range :: (Tagged s b, Tagged s b) -> [Tagged s b]

index :: (Tagged s b, Tagged s b) -> Tagged s b -> Int

unsafeIndex :: (Tagged s b, Tagged s b) -> Tagged s b -> Int

inRange :: (Tagged s b, Tagged s b) -> Tagged s b -> Bool

rangeSize :: (Tagged s b, Tagged s b) -> Int

unsafeRangeSize :: (Tagged s b, Tagged s b) -> Int

Num a => Num (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

(+) :: Tagged s a -> Tagged s a -> Tagged s a

(-) :: Tagged s a -> Tagged s a -> Tagged s a

(*) :: Tagged s a -> Tagged s a -> Tagged s a

negate :: Tagged s a -> Tagged s a

abs :: Tagged s a -> Tagged s a

signum :: Tagged s a -> Tagged s a

fromInteger :: Integer -> Tagged s a

Read b => Read (Tagged s b) Source #

Instance details

Defined in Data.Tagged

Methods

readsPrec :: Int -> ReadS (Tagged s b)

readList :: ReadS [Tagged s b]

readPrec :: ReadPrec (Tagged s b)

readListPrec :: ReadPrec [Tagged s b]

Fractional a => Fractional (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

(/) :: Tagged s a -> Tagged s a -> Tagged s a

recip :: Tagged s a -> Tagged s a

fromRational :: Rational -> Tagged s a

Integral a => Integral (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

quot :: Tagged s a -> Tagged s a -> Tagged s a

rem :: Tagged s a -> Tagged s a -> Tagged s a

div :: Tagged s a -> Tagged s a -> Tagged s a

mod :: Tagged s a -> Tagged s a -> Tagged s a

quotRem :: Tagged s a -> Tagged s a -> (Tagged s a, Tagged s a)

divMod :: Tagged s a -> Tagged s a -> (Tagged s a, Tagged s a)

toInteger :: Tagged s a -> Integer

Real a => Real (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

toRational :: Tagged s a -> Rational

RealFrac a => RealFrac (Tagged s a) Source #

Instance details

Defined in Data.Tagged

Methods

properFraction :: Integral b => Tagged s a -> (b, Tagged s a)

truncate :: Integral b => Tagged s a -> b

round :: Integral b => Tagged s a -> b

ceiling :: Integral b => Tagged s a -> b

floor :: Integral b => Tagged s a -> b

Show b => Show (Tagged s b) Source #

Instance details

Defined in Data.Tagged

Methods

showsPrec :: Int -> Tagged s b -> ShowS

show :: Tagged s b -> String

showList :: [Tagged s b] -> ShowS

Eq b => Eq (Tagged s b) Source #

Instance details

Defined in Data.Tagged

Methods

(==) :: Tagged s b -> Tagged s b -> Bool

(/=) :: Tagged s b -> Tagged s b -> Bool

Ord b => Ord (Tagged s b) Source #

Instance details

Defined in Data.Tagged

Methods

compare :: Tagged s b -> Tagged s b -> Ordering

(<) :: Tagged s b -> Tagged s b -> Bool

(<=) :: Tagged s b -> Tagged s b -> Bool

(>) :: Tagged s b -> Tagged s b -> Bool

(>=) :: Tagged s b -> Tagged s b -> Bool

max :: Tagged s b -> Tagged s b -> Tagged s b

min :: Tagged s b -> Tagged s b -> Tagged s b

type Rep1 (Tagged s :: Type -> Type) Source #

Instance details

Defined in Data.Tagged

type Rep1 (Tagged s :: Type -> Type) = D1 ('MetaData "Tagged" "Data.Tagged" "tagged-0.8.10-IUw8S1MEcty60WZUz6twze" 'True) (C1 ('MetaCons "Tagged" 'PrefixI 'True) (S1 ('MetaSel ('Just "unTagged") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1))

type Rep (Tagged s b) Source #

Instance details

Defined in Data.Tagged

type Rep (Tagged s b) = D1 ('MetaData "Tagged" "Data.Tagged" "tagged-0.8.10-IUw8S1MEcty60WZUz6twze" 'True) (C1 ('MetaCons "Tagged" 'PrefixI 'True) (S1 ('MetaSel ('Just "unTagged") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)))

retag :: forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b Source #

Some times you need to change the tag you have lying around. Idiomatic usage is to make a new combinator for the relationship between the tags that you want to enforce, and define that combinator using retag.

data Succ n
retagSucc :: Tagged n a -> Tagged (Succ n) a
retagSucc = retag

untag :: forall {k} (s :: k) b. Tagged s b -> b Source #

Alias for unTagged

tagSelf :: a -> Tagged a a Source #

Tag a value with its own type.

untagSelf :: Tagged a a -> a Source #

untagSelf is a type-restricted version of untag.

asTaggedTypeOf :: forall {k} s tagged (b :: k). s -> tagged s b -> s Source #

asTaggedTypeOf is a type-restricted version of const. It is usually used as an infix operator, and its typing forces its first argument (which is usually overloaded) to have the same type as the tag of the second.

witness :: Tagged a b -> a -> b Source #

Conversion

proxy :: forall {k} (s :: k) a proxy. Tagged s a -> proxy s -> a Source #

Convert from a Tagged representation to a representation based on a Proxy.

unproxy :: forall {k} (s :: k) a. (Proxy s -> a) -> Tagged s a Source #

Convert from a representation based on a Proxy to a Tagged representation.

tagWith :: forall {k} proxy (s :: k) a. proxy s -> a -> Tagged s a Source #

Another way to convert a proxy to a tag.

Proxy methods GHC dropped

reproxy :: forall {k1} {k2} proxy (a :: k1) (b :: k2). proxy a -> Proxy b Source #

Some times you need to change the proxy you have lying around. Idiomatic usage is to make a new combinator for the relationship between the proxies that you want to enforce, and define that combinator using reproxy.

data Succ n
reproxySucc :: proxy n -> Proxy (Succ n)
reproxySucc = reproxy