Copyright	(C) 2011-2015 Edward Kmett (C) 2015 Ørjan Johansen (C) 2016 David Feuer
License	BSD-style (see the file LICENSE)
Maintainer	Edward Kmett <ekmett@gmail.com>
Stability	experimental
Portability	non-portable
Safe Haskell	Trustworthy
Language	Haskell2010

Data.Constraint.Forall

Description

This module uses a trick to provide quantification over constraints.

Synopsis

type family Forall (p :: k -> Constraint ) :: Constraint
inst :: forall p a. Forall p :- p a
class Forall (ComposeC p f) => ForallF (p :: k2 -> Constraint ) (f :: k1 -> k2)
instF :: forall p f a. ForallF p f :- p (f a)
type Forall1 p = Forall p
inst1 :: forall (p :: (* -> *) -> Constraint ) (f :: * -> *). Forall p :- p f
class Forall (Q p t) => ForallT (p :: k4 -> Constraint ) (t :: (k1 -> k2) -> k3 -> k4)
instT :: forall k1 k2 k3 k4 (p :: k4 -> Constraint ) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a)
type family ForallV :: k -> Constraint
class InstV (p :: k) c | k c -> p where
- instV :: ForallV p :- c
forall :: forall p. ( forall a. Dict (p a)) -> Dict ( Forall p)

Documentation

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

Instances details

type Forall (p :: k -> Constraint ) Source #
Instance details Defined in Data.Constraint.Forall type Forall (p :: k -> Constraint )

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

Instantiate a quantified Forall p constraint at type a .

class Forall (ComposeC p f) => ForallF (p :: k2 -> Constraint ) (f :: k1 -> k2) Source #

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

Instances details

Forall (ComposeC p f) => ForallF (p :: k2 -> Constraint ) (f :: k1 -> k2) Source #
Instance details Defined in Data.Constraint.Forall

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

Instantiate a quantified ForallF p f constraint at type a .

inst1 :: forall (p :: (* -> *) -> Constraint ) (f :: * -> *). Forall p :- p f Source #

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

class Forall (Q p t) => ForallT (p :: k4 -> Constraint ) (t :: (k1 -> k2) -> k3 -> k4) Source #

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

Instances details

Forall (Q p t) => ForallT (p :: k4 -> Constraint ) (t :: (k1 -> k2) -> k3 -> k4) Source #
Instance details Defined in Data.Constraint.Forall

instT :: forall k1 k2 k3 k4 (p :: k4 -> Constraint ) (t :: (k1 -> k2) -> k3 -> k4) (f :: k1 -> k2) (a :: k3). ForallT p t :- p (t f a) Source #

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

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

Instances details

type ForallV Source #
Instance details Defined in Data.Constraint.Forall type ForallV

class InstV (p :: k) c | k c -> p where Source #

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

Methods

Instances details

p ~ c => InstV (p :: Constraint ) c Source #
Instance details Defined in Data.Constraint.Forall Associated Types type ForallV' p Methods instV :: ForallV p :- c Source #
InstV (p a) c => InstV (p :: k1 -> k2 -> k3) c Source #
Instance details Defined in Data.Constraint.Forall Associated Types type ForallV' p Methods instV :: ForallV p :- c Source #
p a ~ c => InstV (p :: k -> Constraint ) c Source #
Instance details Defined in Data.Constraint.Forall Associated Types type ForallV' p Methods instV :: ForallV p :- c Source #

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