constraints-extras- Utility package for constraints

Safe HaskellSafe




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

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


Associated Types

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


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

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

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

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

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

type ArgDictV f c = ArgDict f c Source #

Deprecated: Just use ArgDict

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

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

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

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

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

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

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

class Implies1 c d where Source #

Allows explicit specification of constraint implication

Minimal complete definition



implies1 :: c a :- d a Source #