Data.Constraint.Extras

Documentation

class ArgDict (c :: k -> Constraint) (f :: k -> *) where

Morally, this class is for GADTs whose indices can be finitely enumerated. It provides operations which will select the appropriate type class dictionary from among a list of contenders based on a value of the type. There are a few different variations of this which we'd like to be able to support, and they're all implemented in the same fashion at the term level, by pattern matching on the constructors of the GADT, and producing Dict as the result. It would be nice to have some way to stop the proliferation of these variants and unify the existing ones, but at the moment, it appears to require honest type level functions. (Closed type families which must be fully applied didn't quite cut it when I tried). Some symbolic type-level application could do the trick, but I didn't want to go quite that far at the time of writing.

Minimal complete definition

argDict

Associated Types

type ConstraintsFor f (c :: k -> Constraint) :: Constraint

Methods

argDict :: ConstraintsFor f c => f a -> Dict (c a)

type ConstraintsFor' f (c :: k -> Constraint) (g :: k' -> k) = ConstraintsFor f (ComposeC c g)

argDict' :: forall f c g a. Has' c f g => f a -> Dict (c (g a))

type ConstraintsForV (f :: (k -> k') -> *) (c :: k' -> Constraint) (g :: k) = ConstraintsFor f (FlipC (ComposeC c) g)

argDictV :: forall f c g v. HasV c f g => f v -> Dict (c (v g))

type ArgDictV f c = ArgDict f c

Deprecated: Just use ArgDict

type Has (c :: k -> Constraint) f = (ArgDict c f, ConstraintsFor f c)

type Has' (c :: k -> Constraint) f (g :: k' -> k) = (ArgDict (ComposeC c g) f, ConstraintsFor' f c g)

type HasV c f g = (ArgDict (FlipC (ComposeC c) g) f, ConstraintsForV f c g)

has :: forall c f a r. Has c f => f a -> (c a => r) -> r

has' :: forall c g f a r. Has' c f g => f a -> (c (g a) => r) -> r

hasV :: forall c g f v r. HasV c f g => f v -> (c (v g) => r) -> r

whichever :: forall c t a r. ForallF c t => (c (t a) => r) -> r

class Implies1 c d where

Allows explicit specification of constraint implication

Minimal complete definition

implies1

Methods

implies1 :: c a :- d a