{-# LANGUAGE GADTs                   #-}
{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE TypeFamilies            #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Barbies.Internal.Dicts
  ( Dict(..)
  , requiringDict

  , ClassF
  , ClassFG
  )

where

import Data.Functor.Classes (Show1(..))


-- | @'Dict' c a@ is evidence that there exists an instance of @c a@.
--
--   It is essentially equivalent to @Dict (c a)@ from the
--   <http://hackage.haskell.org/package/constraints constraints> package,
--   but because of its kind, it allows us to define things like @'Dict' 'Show'@.
data Dict c a where
  Dict :: c a => Dict c a

instance Eq (Dict c a) where
  Dict c a
_ == :: Dict c a -> Dict c a -> Bool
== Dict c a
_ = Bool
True

instance Show (Dict c a) where
  showsPrec :: Int -> Dict c a -> ShowS
showsPrec Int
_ Dict c a
Dict = String -> ShowS
showString String
"Dict"

instance Show1 (Dict c)  where
  liftShowsPrec :: forall a.
(Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Dict c a -> ShowS
liftShowsPrec Int -> a -> ShowS
_ [a] -> ShowS
_ = forall a. Show a => Int -> a -> ShowS
showsPrec

-- | Turn a constrained-function into an unconstrained one
--   that uses the packed instance dictionary instead.
requiringDict :: (c  a => r) -> (Dict c a -> r)
requiringDict :: forall {k} (c :: k -> Constraint) (a :: k) r.
(c a => r) -> Dict c a -> r
requiringDict c a => r
r = \Dict c a
Dict -> c a => r
r

-- | 'ClassF' has one universal instance that makes @'ClassF' c f a@
--   equivalent to @c (f a)@. However, we have
--
-- @
-- 'ClassF c f :: k -> 'Data.Kind.Constraint'
-- @
--
-- This is useful since it allows to define constraint-constructors like
-- @'ClassF' 'Monoid' 'Maybe'@
class c (f a) => ClassF c f a where
instance c (f a) => ClassF c f a


-- | Like 'ClassF' but for binary relations.
class c (f a) (g a) => ClassFG c f g a where
instance c (f a) (g a) => ClassFG c f g a