constraints-0.14.2: Constraint manipulation

Copyright | (C) 2015-2021 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 :: (p => r) -> Either String r
- defer :: Deferrable p => (p => r) -> r
- deferred :: Deferrable p :- p
- 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

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

class Deferrable p where Source #

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

Methods

deferEither :: (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 :: (() => r) -> Either String r Source #
(Deferrable a, Deferrable b) => Deferrable (a, b) Source # |
Instance details Defined in Data.Constraint.Deferrable Methods deferEither :: ((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 :: ((a, b, c) => 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 :: (a ~ b => 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 :: (a ~~ b => r) -> Either String r Source #

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

deferred :: Deferrable p :- p Source #

data (a :: k1) :~~: (b :: k2) where infix 4 Source #

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: base-4.10.0.0

Constructors

HRefl :: forall {k1} (a :: k1). a :~~: a |

#### Instances

Instances details

Category ((:~~:) :: k -> k -> Type) | Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Control.Category Methods id :: forall (a :: k). a :~~: a Source # (.) :: forall (b :: k) (c :: k) (a :: k). (b :~~: c) -> (a :~~: b) -> a :~~: c Source #
TestCoercion ((:~~:) a :: k -> Type) | Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Coercion Methods testCoercion :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (Coercion a0 b) Source #
TestEquality ((:~~:) a :: k -> Type) | Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) Source #
NFData2 ((:~~:) :: Type -> Type -> Type) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~~: b) -> () Source #
NFData1 ((:~~:) a :: Type -> Type) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf :: (a0 -> ()) -> (a :~~: a0) -> () Source #
a ~~ b => Boring (a :~~: b) | Heterogeneous type equality is `Boring` too.
Instance details Defined in Data.Boring Methods boring :: a :~~: b Source #
NFData (a :~~: b) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods rnf :: (a :~~: b) -> () Source #
(Typeable i, Typeable j, Typeable a, Typeable b, a ~~ b) => Data (a :~~: b) | Since: base-4.10.0.0

Instance details

Defined in GHC.Internal.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) Source #

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

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

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

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

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

gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~~: b) -> a :~~: b Source #

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

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

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

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

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

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

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

a ~~ b => Bounded (a :~~: b) | Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods minBound :: a :~~: b Source # maxBound :: a :~~: b Source #
a ~~ b => Enum (a :~~: b) | Since: base-4.10.0.0

Instance details

Defined in GHC.Internal.Data.Type.Equality

Methods

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

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

toEnum :: Int -> a :~~: b Source #

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

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

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

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

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

a ~~ b => Read (a :~~: b) | Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~~: b) Source # readList :: ReadS [a :~~: b] Source # readPrec :: ReadPrec (a :~~: b) Source # readListPrec :: ReadPrec [a :~~: b] Source #
Show (a :~~: b) | Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods showsPrec :: Int -> (a :~~: b) -> ShowS Source # show :: (a :~~: b) -> String Source # showList :: [a :~~: b] -> ShowS Source #
Eq (a :~~: b) | Since: base-4.10.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods (==) :: (a :~~: b) -> (a :~~: b) -> Bool Source # (/=) :: (a :~~: b) -> (a :~~: b) -> Bool Source #
Ord (a :~~: b) | Since: base-4.10.0.0

Instance details

Defined in GHC.Internal.Data.Type.Equality

Methods

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

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

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

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

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

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

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

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 infix 4 Source #

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: base-4.7.0.0

Constructors

Refl :: forall {k} (a :: k). a :~: a |

#### Instances

Instances details

Category ((:~:) :: k -> k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Control.Category Methods id :: forall (a :: k). a :~: a Source # (.) :: forall (b :: k) (c :: k) (a :: k). (b :~: c) -> (a :~: b) -> a :~: c Source #
TestCoercion ((:~:) a :: k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Coercion Methods testCoercion :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) Source #
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods testEquality :: forall (a0 :: k) (b :: k). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source #
NFData2 ((:~:) :: Type -> Type -> Type) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf2 :: (a -> ()) -> (b -> ()) -> (a :~: b) -> () Source #
NFData1 ((:~:) a) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods liftRnf :: (a0 -> ()) -> (a :~: a0) -> () Source #
a ~ b => Boring (a :~: b) | Homogeneous type equality is `Boring` too.
Instance details Defined in Data.Boring Methods boring :: a :~: b Source #
NFData (a :~: b) | Since: deepseq-1.4.3.0
Instance details Defined in Control.DeepSeq Methods rnf :: (a :~: b) -> () Source #
(a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.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) Source #

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

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

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

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

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

gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b Source #

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

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

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

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

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

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

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

a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods minBound :: a :~: b Source # maxBound :: a :~: b Source #
a ~ b => Enum (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.Data.Type.Equality

Methods

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

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

toEnum :: Int -> a :~: b Source #

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

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

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

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

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

a ~ b => Read (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~: b) Source # readList :: ReadS [a :~: b] Source # readPrec :: ReadPrec (a :~: b) Source # readListPrec :: ReadPrec [a :~: b] Source #
Show (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS Source # show :: (a :~: b) -> String Source # showList :: [a :~: b] -> ShowS Source #
Eq (a :~: b) | Since: base-4.7.0.0
Instance details Defined in GHC.Internal.Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool Source # (/=) :: (a :~: b) -> (a :~: b) -> Bool Source #
Ord (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in GHC.Internal.Data.Type.Equality

Methods

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

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

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

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

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

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

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

HasDict (a ~ b) (a :~: b) Source # |
Instance details Defined in Data.Constraint Methods evidence :: (a :~: b) -> Dict (a ~ b) Source #