{-# 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 Dict = Proves Proxy

{-# COMPLETE Dict #-}

-- | destructing a 'Dict'
withDict :: Dict c -> (c => r) -> r
withDict d k = proves d (const k)

-- | destruct a 'Has'
proves :: Has c f a -> (c a => f a -> r) -> r
proves (Proves x) k = k 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)