| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Data.HTree.Constraint
Description
A couple of types to work with Constraints
Synopsis
- data Has (c :: k -> Constraint) (f :: k -> Type) (k1 :: k) where
- Proves :: forall {k} (c :: k -> Constraint) (k1 :: k) (f :: k -> Type). c k1 => f k1 -> Has c f k1
- type HasTypeable = Has (Typeable :: k -> Constraint)
- type HasIs (k1 :: k) = Has (k ~ k1)
- proves :: forall {k} c f (a :: k) r. Has c f a -> (c a => f a -> r) -> r
- class c => Charge c (a :: k)
- type Dict c = Has (Charge c :: Type -> Constraint) (Proxy :: Type -> Type) ()
- pattern Dict :: () => c => Dict c
- withDict :: Dict c -> (c => r) -> r
proving a constraint
data Has (c :: k -> Constraint) (f :: k -> Type) (k1 :: k) where Source #
a functor useful for proving a constraint for some type
>>>import Data.Functor.Identity>>>Proves @Eq (Identity (5 :: Int))Proves (Identity 5)
Constructors
| Proves :: forall {k} (c :: k -> Constraint) (k1 :: k) (f :: k -> Type). c k1 => f k1 -> Has c f k1 |
Instances
synonyms for proving a constraint
type HasTypeable = Has (Typeable :: k -> Constraint) Source #
type HasIs (k1 :: k) = Has (k ~ k1) Source #
Has but specialised to a constant type, Some (HasIs k f) is isomorphic to f k
helpers to work with constraints
class c => Charge c (a :: k) Source #
transform a Constraint in something of kind k -> to be
able to use it in ConstraintHas
Instances
| c => Charge c (a :: k) Source # | |
Defined in Data.HTree.Constraint | |
Dict
type Dict c = Has (Charge c :: Type -> Constraint) (Proxy :: Type -> Type) () Source #
a Dict witnesses some constraint