    {-# 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
    _ = Int -> Dict c 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 -> r
    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