{-# LANGUAGE UndecidableSuperClasses #-}

-- | A couple of types to work with Constraints
module Data.HTree.Constraint
  ( -- * proving a constraint
    Has (..)

    -- ** synonyms for proving a constraint
  , HasTypeable
  , HasIs

    -- ** helpers to work with constraints
  , proves
  , Charge

    -- * Dict
  , type Dict
  , pattern Dict

    -- ** functions for working with 'Dict's
  , withDict
  )
where

import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (Proxy))
import Type.Reflection (Typeable)

-- | a functor useful for proving a constraint for some type
--
-- >>> import Data.Functor.Identity
-- >>> Proves @Eq (Identity (5 :: Int))
-- Proves (Identity 5)
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

-- | transform a 'Constraint' in something of kind @k -> 'Constraint'@ to be
--   able to use it in 'Has'
type Charge :: Constraint -> k -> Constraint
class c => Charge c a

instance c => Charge c a

-- | a Dict witnesses some constraint
type Dict :: Constraint -> Type
type Dict c = Has (Charge c) Proxy ()

-- | match on a Dict
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 #-}

-- | destructing a '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)

-- | destruct a 'Has'
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

-- | 'Has' but specialised to 'Typeable'
type HasTypeable :: (k -> Type) -> k -> Type
type HasTypeable = Has Typeable

-- | 'Has' but specialised to a constant type, @Some (HasIs k f)@ is isomorphic to @f k@
type HasIs :: k -> (k -> Type) -> k -> Type
type HasIs k = Has ((~) k)

deriving stock instance Show (f k) => Show (Has c f k)