| 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.
- data UnsatisfiedConstraint = UnsatisfiedConstraint String
- class Deferrable p where
- 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 :~~: b where
- data (k :~: a) b :: forall k. k -> k -> * where
Documentation
class Deferrable p where #
Allow an attempt at resolution of a constraint at a later time
Minimal complete definition
Methods
deferEither :: proxy p -> (p => r) -> Either String r #
Resolve a Deferrable constraint with observable failure.
Instances
| Deferrable () # | |
| (Deferrable a, Deferrable b) => Deferrable (a, b) # | |
| (Typeable * k2, Typeable k2 a, Typeable k2 b) => Deferrable ((~) k2 a b) # | 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 |
| (Deferrable a, Deferrable b, Deferrable c) => Deferrable (a, b, c) # | |
| (Typeable * i1, Typeable * j1, Typeable i1 a, Typeable j1 b) => Deferrable ((~~) i1 j1 a b) # | Deferrable heterogenous equality constraints. Only available on GHC 8.0 or later. |
defer :: forall p r proxy. Deferrable p => proxy p -> (p => r) -> r #
Defer a constraint for later resolution in a context where we want to upgrade failure into an error
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 #
A version of deferEither that uses visible type application in place of a Proxy.
Only available on GHC 8.0 or later.
Kind heterogeneous propositional equality. Like '(:~:)', a :~~: b is
inhabited by a terminating value if and only if a is the same type as b.
Only available on GHC 8.0 or later.
data (k :~: a) b :: 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