| 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
- data (a :: k) :~: (b :: k) where
Documentation
newtype UnsatisfiedConstraint Source #
Constructors
| UnsatisfiedConstraint String |
Instances
| Show UnsatisfiedConstraint Source # | |
|
Defined in Data.Constraint.Deferrable |
|
| Exception UnsatisfiedConstraint Source # | |
|
Defined in Data.Constraint.Deferrable Methods toException :: UnsatisfiedConstraint -> SomeException Source # fromException :: SomeException -> Maybe UnsatisfiedConstraint Source # displayException :: UnsatisfiedConstraint -> String Source # |
|
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
| Deferrable () Source # | |
|
Defined in Data.Constraint.Deferrable Methods deferEither :: proxy () -> (() => r) -> Either String r Source # |
|
| ( Deferrable a, Deferrable b) => Deferrable (a, b) Source # | |
|
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.org
trac
ghc
ticket/10343),
using this instance on GHC 7.10 will only work with
|
|
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 # | |
|
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. |
|
Defined in Data.Constraint.Deferrable |
|
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 #
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 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
Instances
| Category ( (:~~:) :: k -> k -> Type ) |
Since: base-4.10.0.0 |
| TestCoercion ( (:~~:) a :: k -> Type ) |
Since: base-4.10.0.0 |
|
Defined in Data.Type.Coercion |
|
| TestEquality ( (:~~:) a :: k -> Type ) |
Since: base-4.10.0.0 |
|
Defined in Data.Type.Equality |
|
| NFData2 ( (:~~:) :: Type -> Type -> Type ) |
Since: deepseq-1.4.3.0 |
|
Defined in Control.DeepSeq |
|
| NFData1 ( (:~~:) a :: Type -> Type ) |
Since: deepseq-1.4.3.0 |
|
Defined in Control.DeepSeq |
|
| a ~~ b => Bounded (a :~~: b) |
Since: base-4.10.0.0 |
| a ~~ b => Enum (a :~~: b) |
Since: base-4.10.0.0 |
|
Defined in 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 # |
|
| Eq (a :~~: b) |
Since: base-4.10.0.0 |
| ( Typeable i, Typeable j, Typeable a, Typeable b, a ~~ b) => Data (a :~~: b) |
Since: base-4.10.0.0 |
|
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) 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 # |
|
| Ord (a :~~: b) |
Since: base-4.10.0.0 |
|
Defined in 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 # |
|
| a ~~ b => Read (a :~~: b) |
Since: base-4.10.0.0 |
| Show (a :~~: b) |
Since: base-4.10.0.0 |
| NFData (a :~~: b) |
Since: deepseq-1.4.3.0 |
|
Defined in Control.DeepSeq |
|
| HasDict (a ~~ b) (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
Instances
| Category ( (:~:) :: k -> k -> Type ) |
Since: base-4.7.0.0 |
| TestCoercion ( (:~:) a :: k -> Type ) |
Since: base-4.7.0.0 |
|
Defined in Data.Type.Coercion |
|
| TestEquality ( (:~:) a :: k -> Type ) |
Since: base-4.7.0.0 |
|
Defined in Data.Type.Equality |
|
| NFData2 ( (:~:) :: Type -> Type -> Type ) |
Since: deepseq-1.4.3.0 |
|
Defined in Control.DeepSeq |
|
| NFData1 ( (:~:) a) |
Since: deepseq-1.4.3.0 |
|
Defined in Control.DeepSeq |
|
| a ~ b => Bounded (a :~: b) |
Since: base-4.7.0.0 |
| a ~ b => Enum (a :~: b) |
Since: base-4.7.0.0 |
|
Defined in 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 # |
|
| Eq (a :~: b) |
Since: base-4.7.0.0 |
| (a ~ b, Data a) => Data (a :~: b) |
Since: base-4.7.0.0 |
|
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) 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 # |
|
| Ord (a :~: b) |
Since: base-4.7.0.0 |
|
Defined in 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 # |
|
| a ~ b => Read (a :~: b) |
Since: base-4.7.0.0 |
| Show (a :~: b) |
Since: base-4.7.0.0 |
| NFData (a :~: b) |
Since: deepseq-1.4.3.0 |
|
Defined in Control.DeepSeq |
|
| HasDict (a ~ b) (a :~: b) Source # | |