content: {-# LANGUAGE PolyKinds, UndecidableInstances #-}
  {-# LANGUAGE UndecidableSuperClasses #-}
  {-# OPTIONS_GHC -fno-warn-orphans -fno-warn-deprecations #-}
  -- | Constraints for indexed datatypes.
  --
  -- This module contains code that helps to specify that all
  -- elements of an indexed structure must satisfy a particular
  -- constraint.
  --
  module Data.SOP.Constraint
    ( module Data.SOP.Constraint
    , Constraint
    ) where
  
  import Data.Coerce
  import Data.Kind (Type, Constraint)
  
  -- import Data.SOP.Sing
  
  -- | Require a constraint for every element of a list.
  --
  -- If you have a datatype that is indexed over a type-level
  -- list, then you can use 'All' to indicate that all elements
  -- of that type-level list must satisfy a given constraint.
  --
  -- /Example:/ The constraint
  --
  -- > All Eq '[ Int, Bool, Char ]
  --
  -- is equivalent to the constraint
  --
  -- > (Eq Int, Eq Bool, Eq Char)
  --
  -- /Example:/ A type signature such as
  --
  -- > f :: All Eq xs => NP I xs -> ...
  --
  -- means that 'f' can assume that all elements of the n-ary
  -- product satisfy 'Eq'.
  --
  -- Note on superclasses: ghc cannot deduce superclasses from 'All'
  -- constraints.
  -- You might expect the following to compile
  --
  -- > class (Eq a) => MyClass a
  -- >
  -- > foo :: (All Eq xs) => NP f xs -> z
  -- > foo = [..]
  -- >
  -- > bar :: (All MyClass xs) => NP f xs -> x
  -- > bar = foo
  -- but it will fail with an error saying that it was unable to
  -- deduce the class constraint @'AllF' 'Eq' xs@ (or similar) in the
  -- definition of 'bar'.
  -- In cases like this you can use 'Data.SOP.Dict.Dict' from "Data.SOP.Dict"
  -- to prove conversions between constraints.
  -- See [this answer on SO for more details](https://stackoverflow.com/questions/50777865/super-classes-with-all-from-generics-sop).
  
  --
  class (AllF c xs, SListI xs) => All (c :: k -> Constraint) (xs :: [k]) where
  
    -- | Constrained paramorphism for a type-level list.
    --
    -- The advantage of writing functions in terms of 'cpara_SList' is that
    -- they are then typically not recursive, and can be unfolded statically if
    -- the type-level list is statically known.
    --
    -- @since 0.4.0.0
    --
    cpara_SList ::
         proxy c
      -> r '[]
      -> (forall y ys . (c y, All c ys) => r ys -> r (y ': ys))
      -> r xs
  
  instance All c '[] where
    cpara_SList _p nil _cons = nil
    {-# INLINE cpara_SList #-}
  
  instance (c x, All c xs) => All c (x ': xs) where
    cpara_SList p nil cons =
      cons (cpara_SList p nil cons)
    {-# INLINE cpara_SList #-}
  
  -- | Constrained case distinction on a type-level list.
  --
  -- @since 0.4.0.0
  --
  ccase_SList ::
       All c xs
    => proxy c
    -> r '[]
    -> (forall y ys . (c y, All c ys) => r (y ': ys))
    -> r xs
  ccase_SList p nil cons =
    cpara_SList p nil (const cons)
  {-# INLINE ccase_SList #-}
  
  -- | Type family used to implement 'All'.
  --
  type family
    AllF (c :: k -> Constraint) (xs :: [k]) :: Constraint where
    AllF _c '[]       = ()
    AllF  c (x ': xs) = (c x, All c xs)
  
  -- | Require a singleton for every inner list in a list of lists.
  type SListI2 = All SListI
  
  -- | Implicit singleton list.
  --
  -- A singleton list can be used to reveal the structure of
  -- a type-level list argument that the function is quantified
  -- over.
  --
  -- Since 0.4.0.0, this is now defined in terms of 'All'.
  -- A singleton list provides a witness for a type-level list
  -- where the elements need not satisfy any additional
  -- constraints.
  --
  -- @since 0.4.0.0
  --
  type SListI = All Top
  
  -- | Require a constraint for every element of a list of lists.
  --
  -- If you have a datatype that is indexed over a type-level
  -- list of lists, then you can use 'All2' to indicate that all
  -- elements of the inner lists must satisfy a given constraint.
  --
  -- /Example:/ The constraint
  --
  -- > All2 Eq '[ '[ Int ], '[ Bool, Char ] ]
  --
  -- is equivalent to the constraint
  --
  -- > (Eq Int, Eq Bool, Eq Char)
  --
  -- /Example:/ A type signature such as
  --
  -- > f :: All2 Eq xss => SOP I xs -> ...
  --
  -- means that 'f' can assume that all elements of the sum
  -- of product satisfy 'Eq'.
  --
  -- Since 0.4.0.0, this is merely a synonym for
  -- 'All (All c)'.
  --
  -- @since 0.4.0.0
  --
  type All2 c = All (All c)
  
  -- | Require a constraint pointwise for every pair of
  -- elements from two lists.
  --
  -- /Example:/ The constraint
  --
  -- > AllZip (~) '[ Int, Bool, Char ] '[ a, b, c ]
  --
  -- is equivalent to the constraint
  --
  -- > (Int ~ a, Bool ~ b, Char ~ c)
  --
  -- @since 0.3.1.0
  --
  class
    ( SListI xs, SListI ys
    , SameShapeAs xs ys, SameShapeAs ys xs
    , AllZipF c xs ys
    ) => AllZip (c :: a -> b -> Constraint) (xs :: [a]) (ys :: [b])
  instance
    ( SListI xs, SListI ys
    , SameShapeAs xs ys, SameShapeAs ys xs
    , AllZipF c xs ys
    ) => AllZip c xs ys
  
  -- | Type family used to implement 'AllZip'.
  --
  -- @since 0.3.1.0
  --
  type family
    AllZipF (c :: a -> b -> Constraint) (xs :: [a]) (ys :: [b])
      :: Constraint where
    AllZipF _c '[]      '[]        = ()
    AllZipF  c (x ': xs) (y ': ys) = (c x y, AllZip c xs ys)
  
  -- | Type family that forces a type-level list to be of the same
  -- shape as the given type-level list.
  --
  -- Since 0.5.0.0, this only tests the top-level structure of
  -- the list, and is intended to be used in conjunction with
  -- a separate construct (such as the 'AllZip', 'AllZipF'
  -- combination to tie the recursive knot). The reason is that
  -- making 'SameShapeAs' directly recursive leads to quadratic
  -- compile times.
  --
  -- The main use of this constraint is to help type inference to
  -- learn something about otherwise unknown type-level lists.
  --
  -- @since 0.5.0.0
  --
  type family
    SameShapeAs (xs :: [a]) (ys :: [b]) :: Constraint where
    SameShapeAs '[]       ys = (ys ~ '[])
    SameShapeAs (x ': xs) ys = (ys ~ (Head ys ': Tail ys))
  
  -- | Utility function to compute the head of a type-level list.
  --
  -- @since 0.3.1.0
  --
  type family Head (xs :: [a]) :: a where
    Head (x ': xs) = x
  
  -- | Utility function to compute the tail of a type-level list.
  --
  -- @since 0.3.1.0
  --
  type family Tail (xs :: [a]) :: [a] where
    Tail (x ': xs) = xs
  
  -- | The constraint @'LiftedCoercible' f g x y@ is equivalent
  -- to @'Data.Coerce.Coercible' (f x) (g y)@.
  --
  -- @since 0.3.1.0
  --
  class Coercible (f x) (g y) => LiftedCoercible f g x y
  instance Coercible (f x) (g y) => LiftedCoercible f g x y
  
  -- | Require a constraint pointwise for every pair of
  -- elements from two lists of lists.
  --
  --
  class (AllZipF (AllZip f) xss yss, SListI xss, SListI yss, SameShapeAs xss yss, SameShapeAs yss xss) => AllZip2 f xss yss
  instance (AllZipF (AllZip f) xss yss, SListI xss, SListI yss, SameShapeAs xss yss, SameShapeAs yss xss) => AllZip2 f xss yss
  
  -- | Composition of constraints.
  --
  -- Note that the result of the composition must be a constraint,
  -- and therefore, in @'Compose' f g@, the kind of @f@ is @k -> 'Constraint'@.
  -- The kind of @g@, however, is @l -> k@ and can thus be a normal
  -- type constructor.
  --
  -- A typical use case is in connection with 'All' on an 'Data.SOP.NP' or an
  -- 'Data.SOP.NS'. For example, in order to denote that all elements on an
  -- @'Data.SOP.NP' f xs@ satisfy 'Show', we can say @'All' ('Compose' 'Show' f) xs@.
  --
  -- @since 0.2
  --
  class (f (g x)) => (f `Compose` g) x
  instance (f (g x)) => (f `Compose` g) x
  infixr 9 `Compose`
  
  -- | Pairing of constraints.
  --
  -- @since 0.2
  --
  class (f x, g x) => (f `And` g) x
  instance (f x, g x) => (f `And` g) x
  infixl 7 `And`
  
  -- | A constraint that can always be satisfied.
  --
  -- @since 0.2
  --
  class Top x
  instance Top x
  
  -- | A generalization of 'All' and 'All2'.
  --
  -- The family 'AllN' expands to 'All' or 'All2' depending on whether
  -- the argument is indexed by a list or a list of lists.
  --
  type family AllN (h :: (k -> Type) -> (l -> Type)) (c :: k -> Constraint) :: l -> Constraint
  
  -- | A generalization of 'AllZip' and 'AllZip2'.
  --
  -- The family 'AllZipN' expands to 'AllZip' or 'AllZip2' depending on
  -- whther the argument is indexed by a list or a list of lists.
  --
  type family AllZipN (h :: (k -> Type) -> (l -> Type)) (c :: k1 -> k2 -> Constraint) :: l1 -> l2 -> Constraint
  
  -- | A generalization of 'SListI'.
  --
  -- The family 'SListIN' expands to 'SListI' or 'SListI2' depending
  -- on whether the argument is indexed by a list or a list of lists.
  --
  type family SListIN (h :: (k -> Type) -> (l -> Type)) :: l -> Constraint
  