Exinst.Singletons

See the README file for documentation: https://hackage.haskell.org/package/exinst#readme

1 type index

data Some1 f1

Instances

(SingKind k1 (KProxy k1), SDecide k1 (KProxy k1), Dict1 k1 Eq f1) => Eq (Some1 k1 f1)

(SingKind k1 (KProxy k1), SDecide k1 (KProxy k1), Ord (DemoteRep k1 (KProxy k1)), Dict1 k1 Ord f1, Eq (Some1 k1 f1)) => Ord (Some1 k1 f1)

(SingKind k1 (KProxy k1), Show (DemoteRep k1 (KProxy k1)), Dict1 k1 Show f1) => Show (Some1 k1 f1)

some1

Arguments

:: forall (f1 :: k1 -> *). SingI a1

=> f1 a1

-> Some1 f1

withSome1Sing

Arguments

:: forall (f1 :: k1 -> *) (r :: *). Some1 f1

-> (forall a1. Sing a1 -> f1 a1 -> r)

-> r

Like withSome1, but takes an explicit Sing instead of a SingI instance.

withSome1

Arguments

:: forall (f1 :: k1 -> *) (r :: *). Some1 f1

-> (forall a1. SingI a1 => f1 a1 -> r)

-> r

fromSome1

Arguments

:: forall (f1 :: k1 -> *). (SingI a1, SDecide (KProxy :: KProxy k1))

=> Some1 f1

-> Maybe (f1 a1)

class Dict1 c f1 where

Methods

dict1 :: Sing a1 -> Dict (c (f1 a1))

2 type indexes

data Some2 f2

Instances

(SingKind k2 (KProxy k2), SingKind k1 (KProxy k1), SDecide k2 (KProxy k2), SDecide k1 (KProxy k1), Dict2 k2 k1 Eq f2) => Eq (Some2 k2 k1 f2)

(SingKind k2 (KProxy k2), SingKind k1 (KProxy k1), SDecide k2 (KProxy k2), SDecide k1 (KProxy k1), Ord (DemoteRep k2 (KProxy k2)), Ord (DemoteRep k1 (KProxy k1)), Dict2 k2 k1 Ord f2, Eq (Some2 k2 k1 f2)) => Ord (Some2 k2 k1 f2)

(SingKind k2 (KProxy k2), SingKind k1 (KProxy k1), Show (DemoteRep k2 (KProxy k2)), Show (DemoteRep k1 (KProxy k1)), Dict2 k2 k1 Show f2) => Show (Some2 k2 k1 f2)

some2

Arguments

:: forall (f2 :: k2 -> k1 -> *). (SingI a2, SingI a1)

=> f2 a2 a1

-> Some2 f2

withSome2Sing

Arguments

:: forall (f2 :: k2 -> k1 -> *) (r :: *). Some2 f2

-> (forall a2 a1. Sing a2 -> Sing a1 -> f2 a2 a1 -> r)

-> r

Like withSome2, but takes explicit Sings instead of SingI instances.

withSome2

Arguments

:: forall (f2 :: k2 -> k1 -> *) (r :: *). Some2 f2

-> (forall a2 a1. (SingI a2, SingI a1) => f2 a2 a1 -> r)

-> r

fromSome2

Arguments

:: forall (f2 :: k2 -> k1 -> *). (SingI a2, SDecide (KProxy :: KProxy k2), SingI a1, SDecide (KProxy :: KProxy k1))

=> Some2 f2

-> Maybe (f2 a2 a1)

class Dict2 c f2 where

Methods

dict2 :: Sing a2 -> Sing a1 -> Dict (c (f2 a2 a1))

3 type indexes

data Some3 f3

Instances

(SingKind k3 (KProxy k3), SingKind k2 (KProxy k2), SingKind k1 (KProxy k1), SDecide k3 (KProxy k3), SDecide k2 (KProxy k2), SDecide k1 (KProxy k1), Dict3 k3 k2 k1 Eq f3) => Eq (Some3 k3 k2 k1 f3)

(SingKind k3 (KProxy k3), SingKind k2 (KProxy k2), SingKind k1 (KProxy k1), SDecide k3 (KProxy k3), SDecide k2 (KProxy k2), SDecide k1 (KProxy k1), Ord (DemoteRep k3 (KProxy k3)), Ord (DemoteRep k2 (KProxy k2)), Ord (DemoteRep k1 (KProxy k1)), Dict3 k3 k2 k1 Ord f3, Eq (Some3 k3 k2 k1 f3)) => Ord (Some3 k3 k2 k1 f3)

(SingKind k3 (KProxy k3), SingKind k2 (KProxy k2), SingKind k1 (KProxy k1), Show (DemoteRep k3 (KProxy k3)), Show (DemoteRep k2 (KProxy k2)), Show (DemoteRep k1 (KProxy k1)), Dict3 k3 k2 k1 Show f3) => Show (Some3 k3 k2 k1 f3)

some3

Arguments

:: forall (f3 :: k3 -> k2 -> k1 -> *). (SingI a3, SingI a2, SingI a1)

=> f3 a3 a2 a1

-> Some3 f3

withSome3Sing

Arguments

:: forall (f3 :: k3 -> k2 -> k1 -> *) (r :: *). Some3 f3

-> (forall a3 a2 a1. Sing a3 -> Sing a2 -> Sing a1 -> f3 a3 a2 a1 -> r)

-> r

Like withSome3, but takes explicit Sings instead of SingI instances.

withSome3

Arguments

:: forall (f3 :: k3 -> k2 -> k1 -> *) (r :: *). Some3 f3

-> (forall a3 a2 a1. (SingI a3, SingI a2, SingI a1) => f3 a3 a2 a1 -> r)

-> r

fromSome3

Arguments

:: forall (f3 :: k3 -> k2 -> k1 -> *). (SingI a3, SDecide (KProxy :: KProxy k3), SingI a2, SDecide (KProxy :: KProxy k2), SingI a1, SDecide (KProxy :: KProxy k1))

=> Some3 f3

-> Maybe (f3 a3 a2 a1)

class Dict3 c f3 where

Methods

dict3 :: Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f3 a3 a2 a1))

4 type indexes

data Some4 f4

Instances

(SingKind k4 (KProxy k4), SingKind k3 (KProxy k3), SingKind k2 (KProxy k2), SingKind k1 (KProxy k1), SDecide k4 (KProxy k4), SDecide k3 (KProxy k3), SDecide k2 (KProxy k2), SDecide k1 (KProxy k1), Dict4 k4 k3 k2 k1 Eq f4) => Eq (Some4 k4 k3 k2 k1 f4)

(SingKind k4 (KProxy k4), SingKind k3 (KProxy k3), SingKind k2 (KProxy k2), SingKind k1 (KProxy k1), SDecide k4 (KProxy k4), SDecide k3 (KProxy k3), SDecide k2 (KProxy k2), SDecide k1 (KProxy k1), Ord (DemoteRep k4 (KProxy k4)), Ord (DemoteRep k3 (KProxy k3)), Ord (DemoteRep k2 (KProxy k2)), Ord (DemoteRep k1 (KProxy k1)), Dict4 k4 k3 k2 k1 Ord f4, Eq (Some4 k4 k3 k2 k1 f4)) => Ord (Some4 k4 k3 k2 k1 f4)

(SingKind k4 (KProxy k4), SingKind k3 (KProxy k3), SingKind k2 (KProxy k2), SingKind k1 (KProxy k1), Show (DemoteRep k4 (KProxy k4)), Show (DemoteRep k3 (KProxy k3)), Show (DemoteRep k2 (KProxy k2)), Show (DemoteRep k1 (KProxy k1)), Dict4 k4 k3 k2 k1 Show f4) => Show (Some4 k4 k3 k2 k1 f4)

some4

Arguments

:: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *). (SingI a4, SingI a3, SingI a2, SingI a1)

=> f4 a4 a3 a2 a1

-> Some4 f4

withSome4Sing

Arguments

:: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) (r :: *). Some4 f4

-> (forall a4 a3 a2 a1. Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> f4 a4 a3 a2 a1 -> r)

-> r

Like withSome4, but takes explicit Sings instead of SingI instances.

withSome4

Arguments

:: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *) (r :: *). Some4 f4

-> (forall a4 a3 a2 a1. (SingI a4, SingI a3, SingI a2, SingI a1) => f4 a4 a3 a2 a1 -> r)

-> r

fromSome4

Arguments

:: forall (f4 :: k4 -> k3 -> k2 -> k1 -> *). (SingI a4, SDecide (KProxy :: KProxy k4), SingI a3, SDecide (KProxy :: KProxy k3), SingI a2, SDecide (KProxy :: KProxy k2), SingI a1, SDecide (KProxy :: KProxy k1))

=> Some4 f4

-> Maybe (f4 a4 a3 a2 a1)

class Dict4 c f4 where

Methods

dict4 :: Sing a4 -> Sing a3 -> Sing a2 -> Sing a1 -> Dict (c (f4 a4 a3 a2 a1))