simplistic-generics-2.0.0: Generic programming without too many type classes

Safe HaskellSafe
LanguageHaskell2010

Generics.Simplistic.Util

Contents

Synopsis

Utility Functions and Types

(&&&) :: Arrow a => a b c -> a b c' -> a b (c, c') infixr 3 #

Fanout: send the input to both argument arrows and combine their output.

The default definition may be overridden with a more efficient version if desired.

(***) :: Arrow a => a b c -> a b' c' -> a (b, b') (c, c') infixr 3 #

Split the input between the two argument arrows and combine their output. Note that this is in general not a functor.

The default definition may be overridden with a more efficient version if desired.

type (:->) f g = forall n. f n -> g n Source #

Natural transformations

(<.>) :: Monad m => (b -> m c) -> (a -> m b) -> a -> m c infixr 8 Source #

Kleisli Composition

Poly-kind indexed product functionality

data ((f :: k -> Type) :*: (g :: k -> Type)) (p :: k) :: forall k. (k -> Type) -> (k -> Type) -> k -> Type infixr 6 #

Products: encode multiple arguments to constructors

Constructors

(f p) :*: (g p) infixr 6 
Instances
(GDeep kappa fam f, GDeep kappa fam g) => GDeep kappa fam (f :*: g :: k -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Deep

Methods

gdfrom :: (f :*: g) x -> SRep (SFix kappa fam) (f :*: g) Source #

gdto :: SRep (SFix kappa fam) (f :*: g) -> (f :*: g) x Source #

Generic1 (f :*: g :: k -> Type) 
Instance details

Defined in GHC.Generics

Associated Types

type Rep1 (f :*: g) :: k -> Type #

Methods

from1 :: (f :*: g) a -> Rep1 (f :*: g) a #

to1 :: Rep1 (f :*: g) a -> (f :*: g) a #

(GNFData arity a, GNFData arity b) => GNFData arity (a :*: b) 
Instance details

Defined in Control.DeepSeq

Methods

grnf :: RnfArgs arity a0 -> (a :*: b) a0 -> ()

(ShowHO f, ShowHO g) => ShowHO (f :*: g :: ki -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

showHO :: (f :*: g) k -> String Source #

showsPrecHO :: Int -> (f :*: g) k -> ShowS Source #

(EqHO f, EqHO g) => EqHO (f :*: g :: ki -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

eqHO :: (f :*: g) k -> (f :*: g) k -> Bool Source #

(GShallow f, GShallow g) => GShallow (f :*: g :: k -> Type) Source # 
Instance details

Defined in Generics.Simplistic

Methods

sfrom :: (f :*: g) x -> SRep I (f :*: g) Source #

sto :: SRep I (f :*: g) -> (f :*: g) x Source #

(Monad f, Monad g) => Monad (f :*: g)

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Methods

(>>=) :: (f :*: g) a -> (a -> (f :*: g) b) -> (f :*: g) b #

(>>) :: (f :*: g) a -> (f :*: g) b -> (f :*: g) b #

return :: a -> (f :*: g) a #

fail :: String -> (f :*: g) a #

(Functor f, Functor g) => Functor (f :*: g)

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Methods

fmap :: (a -> b) -> (f :*: g) a -> (f :*: g) b #

(<$) :: a -> (f :*: g) b -> (f :*: g) a #

(MonadFix f, MonadFix g) => MonadFix (f :*: g)

Since: base-4.9.0.0

Instance details

Defined in Control.Monad.Fix

Methods

mfix :: (a -> (f :*: g) a) -> (f :*: g) a #

(Applicative f, Applicative g) => Applicative (f :*: g)

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Methods

pure :: a -> (f :*: g) a #

(<*>) :: (f :*: g) (a -> b) -> (f :*: g) a -> (f :*: g) b #

liftA2 :: (a -> b -> c) -> (f :*: g) a -> (f :*: g) b -> (f :*: g) c #

(*>) :: (f :*: g) a -> (f :*: g) b -> (f :*: g) b #

(<*) :: (f :*: g) a -> (f :*: g) b -> (f :*: g) a #

(Foldable f, Foldable g) => Foldable (f :*: g)

Since: base-4.9.0.0

Instance details

Defined in Data.Foldable

Methods

fold :: Monoid m => (f :*: g) m -> m #

foldMap :: Monoid m => (a -> m) -> (f :*: g) a -> m #

foldr :: (a -> b -> b) -> b -> (f :*: g) a -> b #

foldr' :: (a -> b -> b) -> b -> (f :*: g) a -> b #

foldl :: (b -> a -> b) -> b -> (f :*: g) a -> b #

foldl' :: (b -> a -> b) -> b -> (f :*: g) a -> b #

foldr1 :: (a -> a -> a) -> (f :*: g) a -> a #

foldl1 :: (a -> a -> a) -> (f :*: g) a -> a #

toList :: (f :*: g) a -> [a] #

null :: (f :*: g) a -> Bool #

length :: (f :*: g) a -> Int #

elem :: Eq a => a -> (f :*: g) a -> Bool #

maximum :: Ord a => (f :*: g) a -> a #

minimum :: Ord a => (f :*: g) a -> a #

sum :: Num a => (f :*: g) a -> a #

product :: Num a => (f :*: g) a -> a #

(Traversable f, Traversable g) => Traversable (f :*: g)

Since: base-4.9.0.0

Instance details

Defined in Data.Traversable

Methods

traverse :: Applicative f0 => (a -> f0 b) -> (f :*: g) a -> f0 ((f :*: g) b) #

sequenceA :: Applicative f0 => (f :*: g) (f0 a) -> f0 ((f :*: g) a) #

mapM :: Monad m => (a -> m b) -> (f :*: g) a -> m ((f :*: g) b) #

sequence :: Monad m => (f :*: g) (m a) -> m ((f :*: g) a) #

(Alternative f, Alternative g) => Alternative (f :*: g)

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Methods

empty :: (f :*: g) a #

(<|>) :: (f :*: g) a -> (f :*: g) a -> (f :*: g) a #

some :: (f :*: g) a -> (f :*: g) [a] #

many :: (f :*: g) a -> (f :*: g) [a] #

(MonadPlus f, MonadPlus g) => MonadPlus (f :*: g)

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Methods

mzero :: (f :*: g) a #

mplus :: (f :*: g) a -> (f :*: g) a -> (f :*: g) a #

(GShallow1 f, GShallow1 g) => GShallow1 (f :*: g) Source # 
Instance details

Defined in Generics.Simplistic

Methods

sfrom1 :: (f :*: g) a -> SRep1 (f :*: g) a Source #

sto1 :: SRep1 (f :*: g) a -> (f :*: g) a Source #

(Eq (f p), Eq (g p)) => Eq ((f :*: g) p)

Since: base-4.7.0.0

Instance details

Defined in GHC.Generics

Methods

(==) :: (f :*: g) p -> (f :*: g) p -> Bool #

(/=) :: (f :*: g) p -> (f :*: g) p -> Bool #

(Ord (f p), Ord (g p)) => Ord ((f :*: g) p)

Since: base-4.7.0.0

Instance details

Defined in GHC.Generics

Methods

compare :: (f :*: g) p -> (f :*: g) p -> Ordering #

(<) :: (f :*: g) p -> (f :*: g) p -> Bool #

(<=) :: (f :*: g) p -> (f :*: g) p -> Bool #

(>) :: (f :*: g) p -> (f :*: g) p -> Bool #

(>=) :: (f :*: g) p -> (f :*: g) p -> Bool #

max :: (f :*: g) p -> (f :*: g) p -> (f :*: g) p #

min :: (f :*: g) p -> (f :*: g) p -> (f :*: g) p #

(Read (f p), Read (g p)) => Read ((f :*: g) p)

Since: base-4.7.0.0

Instance details

Defined in GHC.Generics

Methods

readsPrec :: Int -> ReadS ((f :*: g) p) #

readList :: ReadS [(f :*: g) p] #

readPrec :: ReadPrec ((f :*: g) p) #

readListPrec :: ReadPrec [(f :*: g) p] #

(Show (f p), Show (g p)) => Show ((f :*: g) p)

Since: base-4.7.0.0

Instance details

Defined in GHC.Generics

Methods

showsPrec :: Int -> (f :*: g) p -> ShowS #

show :: (f :*: g) p -> String #

showList :: [(f :*: g) p] -> ShowS #

Generic ((f :*: g) p) 
Instance details

Defined in GHC.Generics

Associated Types

type Rep ((f :*: g) p) :: Type -> Type #

Methods

from :: (f :*: g) p -> Rep ((f :*: g) p) x #

to :: Rep ((f :*: g) p) x -> (f :*: g) p #

(Semigroup (f p), Semigroup (g p)) => Semigroup ((f :*: g) p)

Since: base-4.12.0.0

Instance details

Defined in GHC.Generics

Methods

(<>) :: (f :*: g) p -> (f :*: g) p -> (f :*: g) p #

sconcat :: NonEmpty ((f :*: g) p) -> (f :*: g) p #

stimes :: Integral b => b -> (f :*: g) p -> (f :*: g) p #

(Monoid (f p), Monoid (g p)) => Monoid ((f :*: g) p)

Since: base-4.12.0.0

Instance details

Defined in GHC.Generics

Methods

mempty :: (f :*: g) p #

mappend :: (f :*: g) p -> (f :*: g) p -> (f :*: g) p #

mconcat :: [(f :*: g) p] -> (f :*: g) p #

type Rep1 (f :*: g :: k -> Type)

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

type Rep ((f :*: g) p)

Since: base-4.7.0.0

Instance details

Defined in GHC.Generics

type Delta f = f :*: f Source #

Diagonal indexed functor

curry' :: ((f :*: g) x -> a) -> f x -> g x -> a Source #

Lifted curry

uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a Source #

Lifted uncurry

delta :: f :-> Delta f Source #

Duplicates its argument

deltaMap :: (f :-> g) -> Delta f :-> Delta g Source #

Applies the same function to both components of the pair

Poly-kind indexed sums

data Sum (f :: k -> Type) (g :: k -> Type) (a :: k) :: forall k. (k -> Type) -> (k -> Type) -> k -> Type #

Lifted sum of functors.

Constructors

InL (f a) 
InR (g a) 
Instances
Generic1 (Sum f g :: k -> Type) 
Instance details

Defined in Data.Functor.Sum

Associated Types

type Rep1 (Sum f g) :: k -> Type #

Methods

from1 :: Sum f g a -> Rep1 (Sum f g) a #

to1 :: Rep1 (Sum f g) a -> Sum f g a #

(ShowHO f, ShowHO g) => ShowHO (Sum f g :: ki -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

showHO :: Sum f g k -> String Source #

showsPrecHO :: Int -> Sum f g k -> ShowS Source #

(EqHO f, EqHO g) => EqHO (Sum f g :: ki -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

eqHO :: Sum f g k -> Sum f g k -> Bool Source #

(Functor f, Functor g) => Functor (Sum f g)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

Methods

fmap :: (a -> b) -> Sum f g a -> Sum f g b #

(<$) :: a -> Sum f g b -> Sum f g a #

(Foldable f, Foldable g) => Foldable (Sum f g)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

Methods

fold :: Monoid m => Sum f g m -> m #

foldMap :: Monoid m => (a -> m) -> Sum f g a -> m #

foldr :: (a -> b -> b) -> b -> Sum f g a -> b #

foldr' :: (a -> b -> b) -> b -> Sum f g a -> b #

foldl :: (b -> a -> b) -> b -> Sum f g a -> b #

foldl' :: (b -> a -> b) -> b -> Sum f g a -> b #

foldr1 :: (a -> a -> a) -> Sum f g a -> a #

foldl1 :: (a -> a -> a) -> Sum f g a -> a #

toList :: Sum f g a -> [a] #

null :: Sum f g a -> Bool #

length :: Sum f g a -> Int #

elem :: Eq a => a -> Sum f g a -> Bool #

maximum :: Ord a => Sum f g a -> a #

minimum :: Ord a => Sum f g a -> a #

sum :: Num a => Sum f g a -> a #

product :: Num a => Sum f g a -> a #

(Traversable f, Traversable g) => Traversable (Sum f g)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

Methods

traverse :: Applicative f0 => (a -> f0 b) -> Sum f g a -> f0 (Sum f g b) #

sequenceA :: Applicative f0 => Sum f g (f0 a) -> f0 (Sum f g a) #

mapM :: Monad m => (a -> m b) -> Sum f g a -> m (Sum f g b) #

sequence :: Monad m => Sum f g (m a) -> m (Sum f g a) #

(Eq1 f, Eq1 g) => Eq1 (Sum f g)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

Methods

liftEq :: (a -> b -> Bool) -> Sum f g a -> Sum f g b -> Bool #

(Ord1 f, Ord1 g) => Ord1 (Sum f g)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

Methods

liftCompare :: (a -> b -> Ordering) -> Sum f g a -> Sum f g b -> Ordering #

(Read1 f, Read1 g) => Read1 (Sum f g)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Sum f g a) #

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Sum f g a] #

liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Sum f g a) #

liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Sum f g a] #

(Show1 f, Show1 g) => Show1 (Sum f g)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Sum f g a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Sum f g a] -> ShowS #

(NFData1 f, NFData1 g) => NFData1 (Sum f g)

Since: deepseq-1.4.3.0

Instance details

Defined in Control.DeepSeq

Methods

liftRnf :: (a -> ()) -> Sum f g a -> () #

(Eq1 f, Eq1 g, Eq a) => Eq (Sum f g a)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

Methods

(==) :: Sum f g a -> Sum f g a -> Bool #

(/=) :: Sum f g a -> Sum f g a -> Bool #

(Typeable a, Typeable f, Typeable g, Typeable k, Data (f a), Data (g a)) => Data (Sum f g a)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g0. g0 -> c g0) -> Sum f g a -> c (Sum f g a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Sum f g a) #

toConstr :: Sum f g a -> Constr #

dataTypeOf :: Sum f g a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Sum f g a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Sum f g a)) #

gmapT :: (forall b. Data b => b -> b) -> Sum f g a -> Sum f g a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sum f g a -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sum f g a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Sum f g a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Sum f g a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sum f g a -> m (Sum f g a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sum f g a -> m (Sum f g a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sum f g a -> m (Sum f g a) #

(Ord1 f, Ord1 g, Ord a) => Ord (Sum f g a)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

Methods

compare :: Sum f g a -> Sum f g a -> Ordering #

(<) :: Sum f g a -> Sum f g a -> Bool #

(<=) :: Sum f g a -> Sum f g a -> Bool #

(>) :: Sum f g a -> Sum f g a -> Bool #

(>=) :: Sum f g a -> Sum f g a -> Bool #

max :: Sum f g a -> Sum f g a -> Sum f g a #

min :: Sum f g a -> Sum f g a -> Sum f g a #

(Read1 f, Read1 g, Read a) => Read (Sum f g a)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

Methods

readsPrec :: Int -> ReadS (Sum f g a) #

readList :: ReadS [Sum f g a] #

readPrec :: ReadPrec (Sum f g a) #

readListPrec :: ReadPrec [Sum f g a] #

(Show1 f, Show1 g, Show a) => Show (Sum f g a)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

Methods

showsPrec :: Int -> Sum f g a -> ShowS #

show :: Sum f g a -> String #

showList :: [Sum f g a] -> ShowS #

Generic (Sum f g a) 
Instance details

Defined in Data.Functor.Sum

Associated Types

type Rep (Sum f g a) :: Type -> Type #

Methods

from :: Sum f g a -> Rep (Sum f g a) x #

to :: Rep (Sum f g a) x -> Sum f g a #

(NFData1 f, NFData1 g, NFData a) => NFData (Sum f g a)

Since: deepseq-1.4.3.0

Instance details

Defined in Control.DeepSeq

Methods

rnf :: Sum f g a -> () #

type Rep1 (Sum f g :: k -> Type)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

type Rep (Sum f g a)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Sum

either' :: (f :-> r) -> (g :-> r) -> Sum f g :-> r Source #

Higher-order sum eliminator

either'' :: (forall x. f x -> a) -> (forall y. g y -> a) -> Sum f g r -> a Source #

Just like either', but the result type is of kind Star

Constraints

class c => d => Implies c d Source #

Constraint implication

Instances
c -> d => Implies c d Source # 
Instance details

Defined in Generics.Simplistic.Util

class Trivial c Source #

Trivial constraint

Instances
Trivial (c :: k) Source # 
Instance details

Defined in Generics.Simplistic.Util

Higher-order Eq and Show

class EqHO (f :: ki -> *) where Source #

Higher order , poly kinded, version of Eq

Methods

eqHO :: forall k. f k -> f k -> Bool Source #

Instances
EqHO (U1 :: ki -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

eqHO :: U1 k -> U1 k -> Bool Source #

EqHO (V1 :: ki -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

eqHO :: V1 k -> V1 k -> Bool Source #

Eq a => EqHO (Const a :: ki -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

eqHO :: Const a k -> Const a k -> Bool Source #

(EqHO f, EqHO g) => EqHO (Sum f g :: ki -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

eqHO :: Sum f g k -> Sum f g k -> Bool Source #

(EqHO f, EqHO g) => EqHO (f :*: g :: ki -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

eqHO :: (f :*: g) k -> (f :*: g) k -> Bool Source #

(All Eq kappa, EqHO h) => EqHO (Holes kappa fam h :: Type -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Deep

Methods

eqHO :: Holes kappa fam h k -> Holes kappa fam h k -> Bool Source #

class ShowHO (f :: ki -> *) where Source #

Higher order, poly kinded, version of Show; We provide the same showsPrec mechanism. The documentation of Text.Show has a good example of the correct usage of showsPrec:

infixr 5 :^:
data Tree a =  Leaf a  |  Tree a :^: Tree a

instance (Show a) => Show (Tree a) where
  showsPrec d (Leaf m) = showParen (d > app_prec) $
       showString "Leaf " . showsPrec (app_prec+1) m
    where app_prec = 10

  showsPrec d (u :^: v) = showParen (d > up_prec) $
       showsPrec (up_prec+1) u .
       showString " :^: "      .
       showsPrec (up_prec+1) v
    where up_prec = 5

Minimal complete definition

showHO | showsPrecHO

Methods

showHO :: forall k. f k -> String Source #

showsPrecHO :: forall k. Int -> f k -> ShowS Source #

Instances
Show a => ShowHO (Const a :: ki -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

showHO :: Const a k -> String Source #

showsPrecHO :: Int -> Const a k -> ShowS Source #

(ShowHO f, ShowHO g) => ShowHO (Sum f g :: ki -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

showHO :: Sum f g k -> String Source #

showsPrecHO :: Int -> Sum f g k -> ShowS Source #

(ShowHO f, ShowHO g) => ShowHO (f :*: g :: ki -> Type) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

showHO :: (f :*: g) k -> String Source #

showsPrecHO :: Int -> (f :*: g) k -> ShowS Source #

Existential Wrapper

data Exists (f :: k -> *) :: * where Source #

Existential type wrapper. This comesin particularly handy when we want to add mrsop terms to some container. See Generics.MRSOP.Holes.Unify for example.

Constructors

Exists :: f x -> Exists f 
Instances
ShowHO f => Show (Exists f) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

showsPrec :: Int -> Exists f -> ShowS #

show :: Exists f -> String #

showList :: [Exists f] -> ShowS #

exMap :: (forall x. f x -> g x) -> Exists f -> Exists g Source #

Maps over Exists

exMapM :: Monad m => (forall x. f x -> m (g x)) -> Exists f -> m (Exists g) Source #

Maps a monadic actino over Exists

exElim :: (forall x. f x -> a) -> Exists f -> a Source #

eliminates an Exists

Elem functionality

type Elem a as = (IsElem a as ~ True, HasElem a as) Source #

We will carry constructive information on the constraint. Forcing IsElem to true

type NotElem a as = IsElem a as ~ False Source #

Negation of Elem

class HasElem a as where Source #

Methods

hasElem :: ElemPrf a as Source #

Instances
HasElem a2 as => HasElem (a2 :: a1) (b ': as :: [a1]) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

hasElem :: ElemPrf a2 (b ': as) Source #

HasElem (a2 :: a1) (a2 ': as :: [a1]) Source # 
Instance details

Defined in Generics.Simplistic.Util

Methods

hasElem :: ElemPrf a2 (a2 ': as) Source #

data ElemPrf a as where Source #

Constructors

Here :: ElemPrf a (a ': as) 
There :: ElemPrf a as -> ElemPrf a (b ': as) 

type family IsElem (a :: k) (as :: [k]) :: Bool where ... Source #

Equations

IsElem a (a ': as) = True 
IsElem a (b ': as) = IsElem a as 
IsElem a '[] = False 

sameTy :: forall fam x y. (Elem x fam, Elem y fam) => Proxy fam -> Proxy x -> Proxy y -> Maybe (x :~: y) Source #

Returns whether two types are the same, given that both belong to the same list.

Witnessing and All constraints

type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where ... Source #

Equations

All c '[] = () 
All c (x ': xs) = (c x, All c xs) 

data Witness c x where Source #

Carries information about x being an instance of c

Constructors

Witness :: c x => Witness c x 

witness :: forall x xs c. (HasElem x xs, All c xs) => Proxy xs -> Witness c x Source #

Provides the witness that x is an instance of c

witnessPrf :: All c xs => ElemPrf x xs -> Witness c x Source #

Provides the witness that x is an instance of c

weq :: forall x xs. (All Eq xs, Elem x xs) => Proxy xs -> x -> x -> Bool Source #

Fetches the Eq instance for an element of a list

wshow :: forall x xs. (All Show xs, Elem x xs) => Proxy xs -> x -> String Source #

Fetches the Eq instance for an element of a list