Data.Constraint.Forall

This module uses a trick to provide quantification over constraints.

Documentation

type family Forall (p :: k -> Constraint) :: Constraint

A representation of the quantified constraint forall a. p a.

Instances

type Forall k p

type Forall k p

inst :: forall p a. Forall p :- p a

Instantiate a quantified Forall p constraint at type a.

class Forall (ComposeC p f) => ForallF p f

A representation of the quantified constraint forall a. p (f a).

Instances

Forall k1 (ComposeC k1 k2 p f) => ForallF k1 k2 p f

instF :: forall p f a. ForallF p f :- p (f a)

Instantiate a quantified ForallF p f constraint at type a.

type Forall1 p = Forall p

inst1 :: forall p f. Forall p :- p f

Instantiate a quantified constraint on kind * -> *. This is now redundant since inst became polykinded.

class Forall (Q p t) => ForallT p t

A representation of the quantified constraint forall f a. p (t f a).

Instances

Forall (k1 -> k2) (Q k3 (k1 -> k2) k4 p t) => ForallT k3 k2 k1 k4 p t

instT :: forall p t f a. ForallT p t :- p (t f a)

Instantiate a quantified ForallT p t constraint at types f and a.

type family ForallV :: k -> Constraint

A representation of the quantified constraint forall a1 a2 ... an . p a1 a2 ... an, supporting a variable number of parameters.

Instances

type ForallV k

type ForallV k

class InstV p c | k c -> p where

Instantiate a quantified ForallV p constraint as c, where c ~ p a1 a2 ... an.

Minimal complete definition

instV

Methods

instV :: ForallV p :- c

Instances

(~) Constraint p c => InstV Constraint p c

Associated Types

type ForallV' p (c :: p) :: Constraint

Methods

instV :: ForallV p c :- c

InstV (k2 -> k3) (p a) c => InstV (k1 -> k2 -> k3) p c

Associated Types

type ForallV' p (c :: p) :: Constraint

Methods

instV :: ForallV p c :- c

(~) Constraint (p a) c => InstV (k -> Constraint) p c

Associated Types

type ForallV' p (c :: p) :: Constraint

Methods

instV :: ForallV p c :- c

forall :: forall p. (forall a. Dict (p a)) -> Dict (Forall p)