module Control.Monad.Ology.General.Trans.Constraint where

import Control.Monad.Ology.General.Function
import Import

-- | Transitivity of some constraint @c@ from @m@ to @t m@.
type TransConstraint :: ((Type -> Type) -> Constraint) -> TransKind -> Constraint
class TransConstraint c t where
    hasTransConstraint ::
           forall (m :: Type -> Type). c m
        => Dict (c (t m))

transConstraintDict ::
       forall c t m. TransConstraint c t
    => Dict (c m)
    -> Dict (c (t m))
transConstraintDict :: forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type).
TransConstraint c t =>
Dict (c m) -> Dict (c (t m))
transConstraintDict Dict (c m)
Dict = forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type).
(TransConstraint c t, c m) =>
Dict (c (t m))
hasTransConstraint @c @t @m

withTransConstraintTM ::
       forall c t m a. (TransConstraint c t, c m)
    => (c (t m) => t m a)
    -> t m a
withTransConstraintTM :: forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type) a.
(TransConstraint c t, c m) =>
(c (t m) => t m a) -> t m a
withTransConstraintTM c (t m) => t m a
tma =
    case forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type).
(TransConstraint c t, c m) =>
Dict (c (t m))
hasTransConstraint @c @t @m of
        Dict (c (t m))
Dict -> c (t m) => t m a
tma

withTransConstraintTM' ::
       forall c t' t m a. (TransConstraint c t, c m)
    => (c (t m) => t' (t m) a)
    -> t' (t m) a
withTransConstraintTM' :: forall {k} (c :: (Type -> Type) -> Constraint)
       (t' :: (Type -> Type) -> k -> Type) (t :: TransKind)
       (m :: Type -> Type) (a :: k).
(TransConstraint c t, c m) =>
(c (t m) => t' (t m) a) -> t' (t m) a
withTransConstraintTM' c (t m) => t' (t m) a
tma =
    case forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type).
(TransConstraint c t, c m) =>
Dict (c (t m))
hasTransConstraint @c @t @m of
        Dict (c (t m))
Dict -> c (t m) => t' (t m) a
tma

withTransConstraintDict ::
       forall c t m c'. (TransConstraint c t, c m)
    => (c (t m) => Dict (c' (t m)))
    -> Dict (c' (t m))
withTransConstraintDict :: forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type) (c' :: (Type -> Type) -> Constraint).
(TransConstraint c t, c m) =>
(c (t m) => Dict (c' (t m))) -> Dict (c' (t m))
withTransConstraintDict c (t m) => Dict (c' (t m))
dict =
    case forall (c :: (Type -> Type) -> Constraint) (t :: TransKind)
       (m :: Type -> Type).
(TransConstraint c t, c m) =>
Dict (c (t m))
hasTransConstraint @c @t @m of
        Dict (c (t m))
Dict -> c (t m) => Dict (c' (t m))
dict