{-# LANGUAGE UndecidableSuperClasses #-}
module Data.HTree.Constraint
(
Has (..)
, HasTypeable
, HasIs
, proves
, Charge
, type Dict
, pattern Dict
, withDict
)
where
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (Proxy))
import Type.Reflection (Typeable)
type Has :: forall k. (k -> Constraint) -> (k -> Type) -> k -> Type
data Has c f k where
Proves :: c k => f k -> Has c f k
type Charge :: Constraint -> k -> Constraint
class c => Charge c a
instance c => Charge c a
type Dict :: Constraint -> Type
type Dict c = Has (Charge c) Proxy ()
pattern Dict :: forall (c :: Constraint). forall. c => Dict c
pattern $mDict :: forall {r} {c :: Constraint}.
Dict c -> (c => r) -> ((# #) -> r) -> r
$bDict :: forall (c :: Constraint). c => Dict c
Dict = Proves Proxy
{-# COMPLETE Dict #-}
withDict :: Dict c -> (c => r) -> r
withDict :: forall (c :: Constraint) r. Dict c -> (c => r) -> r
withDict Dict c
d c => r
k = Dict c -> (Charge @Type c () => Proxy @Type () -> r) -> r
forall {k} (c :: k -> Constraint) (f :: k -> Type) (a :: k) r.
Has @k c f a -> (c a => f a -> r) -> r
proves Dict c
d (r -> Proxy @Type () -> r
forall a b. a -> b -> a
const r
c => r
k)
proves :: Has c f a -> (c a => f a -> r) -> r
proves :: forall {k} (c :: k -> Constraint) (f :: k -> Type) (a :: k) r.
Has @k c f a -> (c a => f a -> r) -> r
proves (Proves f a
x) c a => f a -> r
k = c a => f a -> r
f a -> r
k f a
x
type HasTypeable :: (k -> Type) -> k -> Type
type HasTypeable = Has Typeable
type HasIs :: k -> (k -> Type) -> k -> Type
type HasIs k = Has ((~) k)
deriving stock instance Show (f k) => Show (Has c f k)