constraints-0.10: Constraint manipulation

Copyright(C) 2015-2016 Edward Kmett
LicenseBSD-style (see the file LICENSE)
MaintainerEdward Kmett <ekmett@gmail.com>
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Constraint.Deferrable

Description

The idea for this trick comes from Dimitrios Vytiniotis.

Synopsis

Documentation

class Deferrable p where Source #

Allow an attempt at resolution of a constraint at a later time

Minimal complete definition

deferEither

Methods

deferEither :: proxy p -> (p => r) -> Either String r Source #

Resolve a Deferrable constraint with observable failure.

Instances

Deferrable () Source # 

Methods

deferEither :: proxy () -> (() -> r) -> Either String r Source #

(Deferrable a, Deferrable b) => Deferrable (a, b) Source # 

Methods

deferEither :: proxy (a, b) -> ((a, b) -> r) -> Either String r Source #

(Typeable * k3, Typeable k3 a, Typeable k3 b) => Deferrable ((~) k3 a b) Source #

Deferrable homogeneous equality constraints.

Note that due to a GHC bug (https:/ghc.haskell.orgtracghcticket/10343), using this instance on GHC 7.10 will only work with *-kinded types.

Methods

deferEither :: proxy ((k3 ~ a) b) -> ((k3 ~ a) b -> r) -> Either String r Source #

(Deferrable a, Deferrable b, Deferrable c) => Deferrable (a, b, c) Source # 

Methods

deferEither :: proxy (a, b, c) -> ((a, b, c) -> r) -> Either String r Source #

(Typeable * i2, Typeable * j2, Typeable i2 a, Typeable j2 b) => Deferrable ((~~) i2 j2 a b) Source #

Deferrable heterogenous equality constraints.

Only available on GHC 8.0 or later.

Methods

deferEither :: proxy ((i2 ~~ j2) a b) -> ((i2 ~~ j2) a b -> r) -> Either String r Source #

defer :: forall p r proxy. Deferrable p => proxy p -> (p => r) -> r Source #

Defer a constraint for later resolution in a context where we want to upgrade failure into an error

deferred :: forall p. Deferrable p :- p Source #

defer_ :: forall p r. Deferrable p => (p => r) -> r Source #

A version of defer that uses visible type application in place of a Proxy.

Only available on GHC 8.0 or later.

deferEither_ :: forall p r. Deferrable p => (p => r) -> Either String r Source #

A version of deferEither that uses visible type application in place of a Proxy.

Only available on GHC 8.0 or later.

data (k1 :~~: k2) (a :: k1) (b :: k2) :: forall k1 k2. k1 -> k2 -> * where infix 4 #

Kind heterogeneous propositional equality. Like '(:~:)', a :~~: b is inhabited by a terminating value if and only if a is the same type as b.

Since: 4.10.0.0

Constructors

HRefl :: (:~~:) k1 k1 a a 

Instances

Category k ((:~~:) k k)

Since: 4.10.0.0

Methods

id :: cat a a #

(.) :: cat b c -> cat a b -> cat a c #

TestEquality k ((:~~:) k1 k a)

Since: 4.10.0.0

Methods

testEquality :: f a -> f b -> Maybe (((k1 :~~: k) a :~: a) b) #

NFData2 ((:~~:) * *)

Since: 1.4.3.0

Methods

liftRnf2 :: (a -> ()) -> (b -> ()) -> (* :~~: *) a b -> () #

NFData1 ((:~~:) k1 * a)

Since: 1.4.3.0

Methods

liftRnf :: (a -> ()) -> (k1 :~~: *) a a -> () #

(~~) k1 k2 a b => Bounded ((:~~:) k1 k2 a b)

Since: 4.10.0.0

Methods

minBound :: (k1 :~~: k2) a b #

maxBound :: (k1 :~~: k2) a b #

(~~) k1 k2 a b => Enum ((:~~:) k1 k2 a b)

Since: 4.10.0.0

Methods

succ :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b #

pred :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b #

toEnum :: Int -> (k1 :~~: k2) a b #

fromEnum :: (k1 :~~: k2) a b -> Int #

enumFrom :: (k1 :~~: k2) a b -> [(k1 :~~: k2) a b] #

enumFromThen :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> [(k1 :~~: k2) a b] #

enumFromTo :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> [(k1 :~~: k2) a b] #

enumFromThenTo :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> [(k1 :~~: k2) a b] #

Eq ((:~~:) k1 k2 a b)

Since: 4.10.0.0

Methods

(==) :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Bool #

(/=) :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Bool #

(Typeable * i2, Typeable * j2, Typeable i2 a, Typeable j2 b, (~~) i2 j2 a b) => Data ((:~~:) i2 j2 a b)

Since: 4.10.0.0

Methods

gfoldl :: (forall d c. Data d => c (d -> c) -> d -> c c) -> (forall g. g -> c g) -> (i2 :~~: j2) a b -> c ((i2 :~~: j2) a b) #

gunfold :: (forall c r. Data c => c (c -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ((i2 :~~: j2) a b) #

toConstr :: (i2 :~~: j2) a b -> Constr #

dataTypeOf :: (i2 :~~: j2) a b -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ((i2 :~~: j2) a b)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ((i2 :~~: j2) a b)) #

gmapT :: (forall c. Data c => c -> c) -> (i2 :~~: j2) a b -> (i2 :~~: j2) a b #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (i2 :~~: j2) a b -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (i2 :~~: j2) a b -> r #

gmapQ :: (forall d. Data d => d -> u) -> (i2 :~~: j2) a b -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> (i2 :~~: j2) a b -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (i2 :~~: j2) a b -> m ((i2 :~~: j2) a b) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (i2 :~~: j2) a b -> m ((i2 :~~: j2) a b) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (i2 :~~: j2) a b -> m ((i2 :~~: j2) a b) #

Ord ((:~~:) k1 k2 a b)

Since: 4.10.0.0

Methods

compare :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Ordering #

(<) :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Bool #

(<=) :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Bool #

(>) :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Bool #

(>=) :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> Bool #

max :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> (k1 :~~: k2) a b #

min :: (k1 :~~: k2) a b -> (k1 :~~: k2) a b -> (k1 :~~: k2) a b #

(~~) k1 k2 a b => Read ((:~~:) k1 k2 a b)

Since: 4.10.0.0

Methods

readsPrec :: Int -> ReadS ((k1 :~~: k2) a b) #

readList :: ReadS [(k1 :~~: k2) a b] #

readPrec :: ReadPrec ((k1 :~~: k2) a b) #

readListPrec :: ReadPrec [(k1 :~~: k2) a b] #

Show ((:~~:) k1 k2 a b)

Since: 4.10.0.0

Methods

showsPrec :: Int -> (k1 :~~: k2) a b -> ShowS #

show :: (k1 :~~: k2) a b -> String #

showList :: [(k1 :~~: k2) a b] -> ShowS #

NFData ((:~~:) k1 k2 a b)

Since: 1.4.3.0

Methods

rnf :: (k1 :~~: k2) a b -> () #

data (k :~: (a :: k)) (b :: k) :: forall k. k -> k -> * where infix 4 #

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: 4.7.0.0

Constructors

Refl :: (:~:) k a a 

Instances

Category k ((:~:) k)

Since: 4.7.0.0

Methods

id :: cat a a #

(.) :: cat b c -> cat a b -> cat a c #

TestEquality k ((:~:) k a)

Since: 4.7.0.0

Methods

testEquality :: f a -> f b -> Maybe (((k :~: a) :~: a) b) #

NFData2 ((:~:) *)

Since: 1.4.3.0

Methods

liftRnf2 :: (a -> ()) -> (b -> ()) -> (* :~: a) b -> () #

NFData1 ((:~:) * a)

Since: 1.4.3.0

Methods

liftRnf :: (a -> ()) -> (* :~: a) a -> () #

(~) k a b => Bounded ((:~:) k a b)

Since: 4.7.0.0

Methods

minBound :: (k :~: a) b #

maxBound :: (k :~: a) b #

(~) k a b => Enum ((:~:) k a b)

Since: 4.7.0.0

Methods

succ :: (k :~: a) b -> (k :~: a) b #

pred :: (k :~: a) b -> (k :~: a) b #

toEnum :: Int -> (k :~: a) b #

fromEnum :: (k :~: a) b -> Int #

enumFrom :: (k :~: a) b -> [(k :~: a) b] #

enumFromThen :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] #

enumFromTo :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] #

enumFromThenTo :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b -> [(k :~: a) b] #

Eq ((:~:) k a b) 

Methods

(==) :: (k :~: a) b -> (k :~: a) b -> Bool #

(/=) :: (k :~: a) b -> (k :~: a) b -> Bool #

((~) * a b, Data a) => Data ((:~:) * a b)

Since: 4.7.0.0

Methods

gfoldl :: (forall d c. Data d => c (d -> c) -> d -> c c) -> (forall g. g -> c g) -> (* :~: a) b -> c ((* :~: a) b) #

gunfold :: (forall c r. Data c => c (c -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ((* :~: a) b) #

toConstr :: (* :~: a) b -> Constr #

dataTypeOf :: (* :~: a) b -> DataType #

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ((* :~: a) b)) #

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ((* :~: a) b)) #

gmapT :: (forall c. Data c => c -> c) -> (* :~: a) b -> (* :~: a) b #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (* :~: a) b -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (* :~: a) b -> r #

gmapQ :: (forall d. Data d => d -> u) -> (* :~: a) b -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> (* :~: a) b -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (* :~: a) b -> m ((* :~: a) b) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (* :~: a) b -> m ((* :~: a) b) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (* :~: a) b -> m ((* :~: a) b) #

Ord ((:~:) k a b) 

Methods

compare :: (k :~: a) b -> (k :~: a) b -> Ordering #

(<) :: (k :~: a) b -> (k :~: a) b -> Bool #

(<=) :: (k :~: a) b -> (k :~: a) b -> Bool #

(>) :: (k :~: a) b -> (k :~: a) b -> Bool #

(>=) :: (k :~: a) b -> (k :~: a) b -> Bool #

max :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b #

min :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b #

(~) k a b => Read ((:~:) k a b)

Since: 4.7.0.0

Methods

readsPrec :: Int -> ReadS ((k :~: a) b) #

readList :: ReadS [(k :~: a) b] #

readPrec :: ReadPrec ((k :~: a) b) #

readListPrec :: ReadPrec [(k :~: a) b] #

Show ((:~:) k a b) 

Methods

showsPrec :: Int -> (k :~: a) b -> ShowS #

show :: (k :~: a) b -> String #

showList :: [(k :~: a) b] -> ShowS #

NFData ((:~:) k a b)

Since: 1.4.3.0

Methods

rnf :: (k :~: a) b -> () #