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

Data.Constraint.Deferrable

Description

The idea for this trick comes from Dimitrios Vytiniotis.

Synopsis

newtype UnsatisfiedConstraint = UnsatisfiedConstraint String
class Deferrable p where
- deferEither :: proxy p -> (p => r) -> Either String r
defer :: forall p r proxy. Deferrable p => proxy p -> (p => r) -> r
deferred :: forall p. Deferrable p :- p
defer_ :: forall p r. Deferrable p => (p => r) -> r
deferEither_ :: forall p r. Deferrable p => (p => r) -> Either String r
data (a :: k1) :~~: (b :: k2) where
- HRefl :: forall k1 (a :: k1). a :~~: a
data (a :: k) :~: (b :: k) where
- Refl :: forall k (a :: k). a :~: a

Documentation

newtype UnsatisfiedConstraint Source #

Constructors

UnsatisfiedConstraint String

Instances

Instances details

Show UnsatisfiedConstraint Source #
Instance details Defined in Data.Constraint.Deferrable Methods showsPrec :: Int -> UnsatisfiedConstraint -> ShowS show :: UnsatisfiedConstraint -> String showList :: [UnsatisfiedConstraint] -> ShowS
Exception UnsatisfiedConstraint Source #
Instance details Defined in Data.Constraint.Deferrable Methods toException :: UnsatisfiedConstraint -> SomeException fromException :: SomeException -> Maybe UnsatisfiedConstraint displayException :: UnsatisfiedConstraint -> String

class Deferrable p where Source #

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

Methods

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

Resolve a Deferrable constraint with observable failure.

Instances

Instances details

Deferrable () Source #
Instance details Defined in Data.Constraint.Deferrable Methods deferEither :: proxy () -> (() => r) -> Either String r Source #
(Deferrable a, Deferrable b) => Deferrable (a, b) Source #
Instance details Defined in Data.Constraint.Deferrable Methods deferEither :: proxy (a, b) -> ((a, b) => r) -> Either String r Source #
(Typeable k, Typeable a, Typeable b) => Deferrable (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.
Instance details Defined in Data.Constraint.Deferrable Methods deferEither :: proxy (a ~ b) -> (a ~ b => r) -> Either String r Source #
(Deferrable a, Deferrable b, Deferrable c) => Deferrable (a, b, c) Source #
Instance details Defined in Data.Constraint.Deferrable Methods deferEither :: proxy (a, b, c) -> ((a, b, c) => r) -> Either String r Source #
(Typeable i, Typeable j, Typeable a, Typeable b) => Deferrable (a ~~ b) Source #	Deferrable heterogenous equality constraints. Only available on GHC 8.0 or later.
Instance details Defined in Data.Constraint.Deferrable Methods deferEither :: proxy (a ~~ b) -> (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 (a :: k1) :~~: (b :: k2) where #

Constructors

HRefl :: forall k1 (a :: k1). a :~~: a

Instances

Instances details

Category ((:~~:) :: k -> k -> Type)
Instance details Defined in Control.Category Methods id :: forall (a :: k0). a :~~: a (.) :: forall (b :: k0) (c :: k0) (a :: k0). (b :~~: c) -> (a :~~: b) -> a :~~: c
TestCoercion ((:~~:) a :: k -> Type)
Instance details Defined in Data.Type.Coercion Methods testCoercion :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (Coercion a0 b)
TestEquality ((:~~:) a :: k -> Type)
Instance details Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b)
NFData2 ((:~~:) :: Type -> Type -> Type)
Instance details Defined in Control.DeepSeq Methods liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~~: b) -> ()
NFData1 ((:~~:) a :: Type -> Type)
Instance details Defined in Control.DeepSeq Methods liftRnf :: (a0 -> ()) -> (a :~~: a0) -> ()
a ~~ b => Bounded (a :~~: b)
Instance details Defined in Data.Type.Equality Methods minBound :: a :~~: b maxBound :: a :~~: b
a ~~ b => Enum (a :~~: b)
Instance details Defined in Data.Type.Equality Methods succ :: (a :~~: b) -> a :~~: b pred :: (a :~~: b) -> a :~~: b toEnum :: Int -> a :~~: b fromEnum :: (a :~~: b) -> Int enumFrom :: (a :~~: b) -> [a :~~: b] enumFromThen :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] enumFromTo :: (a :~~: b) -> (a :~~: b) -> [a :~~: b] enumFromThenTo :: (a :~~: b) -> (a :~~: b) -> (a :~~: b) -> [a :~~: b]
Eq (a :~~: b)
Instance details Defined in Data.Type.Equality Methods (==) :: (a :~~: b) -> (a :~~: b) -> Bool (/=) :: (a :~~: b) -> (a :~~: b) -> Bool
(Typeable i, Typeable j, Typeable a, Typeable b, a ~~ b) => Data (a :~~: b)
Instance details Defined in Data.Data Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~~: b) -> c (a :~~: b) gunfold :: (forall b0 r. Data b0 => c (b0 -> 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 b0. Data b0 => b0 -> b0) -> (a :~~: b) -> a :~~: b gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~~: b) -> r gmapQr :: forall r r'. (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 (a :~~: b)
Instance details Defined in Data.Type.Equality Methods compare :: (a :~~: b) -> (a :~~: b) -> Ordering (<) :: (a :~~: b) -> (a :~~: b) -> Bool (<=) :: (a :~~: b) -> (a :~~: b) -> Bool (>) :: (a :~~: b) -> (a :~~: b) -> Bool (>=) :: (a :~~: b) -> (a :~~: b) -> Bool max :: (a :~~: b) -> (a :~~: b) -> a :~~: b min :: (a :~~: b) -> (a :~~: b) -> a :~~: b
a ~~ b => Read (a :~~: b)
Instance details Defined in Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~~: b) readList :: ReadS [a :~~: b] readPrec :: ReadPrec (a :~~: b) readListPrec :: ReadPrec [a :~~: b]
Show (a :~~: b)
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~~: b) -> ShowS show :: (a :~~: b) -> String showList :: [a :~~: b] -> ShowS
NFData (a :~~: b)
Instance details Defined in Control.DeepSeq Methods rnf :: (a :~~: b) -> ()
HasDict (a ~~ b) (a :~~: b) Source #
Instance details Defined in Data.Constraint Methods evidence :: (a :~~: b) -> Dict (a ~~ b) Source #

data (a :: k) :~: (b :: k) where #

Constructors

Refl :: forall k (a :: k). a :~: a

Instances

Instances details

Category ((:~:) :: k -> k -> Type)
Instance details Defined in Control.Category Methods id :: forall (a :: k0). a :~: a (.) :: forall (b :: k0) (c :: k0) (a :: k0). (b :~: c) -> (a :~: b) -> a :~: c
TestCoercion ((:~:) a :: k -> Type)
Instance details Defined in Data.Type.Coercion Methods testCoercion :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b)
TestEquality ((:~:) a :: k -> Type)
Instance details Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)
NFData2 ((:~:) :: Type -> Type -> Type)
Instance details Defined in Control.DeepSeq Methods liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> ()
NFData1 ((:~:) a)
Instance details Defined in Control.DeepSeq Methods liftRnf :: (a0 -> ()) -> (a :~: a0) -> ()
a ~ b => Bounded (a :~: b)
Instance details Defined in Data.Type.Equality Methods minBound :: a :~: b maxBound :: a :~: b
a ~ b => Enum (a :~: b)
Instance details Defined in Data.Type.Equality Methods succ :: (a :~: b) -> a :~: b pred :: (a :~: b) -> a :~: b toEnum :: Int -> a :~: b fromEnum :: (a :~: b) -> Int enumFrom :: (a :~: b) -> [a :~: b] enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b]
Eq (a :~: b)
Instance details Defined in Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool (/=) :: (a :~: b) -> (a :~: b) -> Bool
(a ~ b, Data a) => Data (a :~: b)
Instance details Defined in Data.Data Methods gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b) gunfold :: (forall b0 r. Data b0 => c (b0 -> 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 b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r gmapQr :: forall r r'. (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 (a :~: b)
Instance details Defined in Data.Type.Equality Methods compare :: (a :~: b) -> (a :~: b) -> Ordering (<) :: (a :~: b) -> (a :~: b) -> Bool (<=) :: (a :~: b) -> (a :~: b) -> Bool (>) :: (a :~: b) -> (a :~: b) -> Bool (>=) :: (a :~: b) -> (a :~: b) -> Bool max :: (a :~: b) -> (a :~: b) -> a :~: b min :: (a :~: b) -> (a :~: b) -> a :~: b
a ~ b => Read (a :~: b)
Instance details Defined in Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~: b) readList :: ReadS [a :~: b] readPrec :: ReadPrec (a :~: b) readListPrec :: ReadPrec [a :~: b]
Show (a :~: b)
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS show :: (a :~: b) -> String showList :: [a :~: b] -> ShowS
NFData (a :~: b)
Instance details Defined in Control.DeepSeq Methods rnf :: (a :~: b) -> ()
HasDict (a ~ b) (a :~: b) Source #
Instance details Defined in Data.Constraint Methods evidence :: (a :~: b) -> Dict (a ~ b) Source #