    {-# LANGUAGE AllowAmbiguousTypes #-}
    {-# LANGUAGE FlexibleContexts #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeApplications #-}
    {-# LANGUAGE UndecidableInstances #-}
    {-# LANGUAGE ConstraintKinds #-}
    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE DataKinds #-}

    module Data.Generics.Product.Internal.Param
      ( Context
      , derived
      ) where

    import Data.Generics.Product.Internal.Types
    import Data.Generics.Internal.VL.Traversal

    import GHC.Generics
    import Data.Kind
    import Data.Generics.Internal.Families
    import Data.Generics.Internal.GenericN
    import Data.Generics.Internal.Errors
    import GHC.TypeLits

    type Context n s t a b
      =  ( GenericN s
         , GenericN t
         -- TODO: merge the old 'Changing' code with 'GenericN'
         , Defined (Rep s)
           (NoGeneric s
             '[ 'Text "arising from a generic traversal of the type parameter at position " ':<>: QuoteType n
              , 'Text "of type " ':<>: QuoteType a ':<>: 'Text " in " ':<>: QuoteType s
              ])
           (() :: Constraint)
         , s ~ Infer t (P n b 'PTag) a
         , t ~ Infer s (P n a 'PTag) b
         , Error ((ArgCount s) <=? n) n (ArgCount s) s
         , a ~ ArgAt s n
         , b ~ ArgAt t n
         , GHasTypes ChGeneric (RepN s) (RepN t) (Param n a) (Param n b)
         )

    derived :: forall n s t a b. Context n s t a b => Traversal s t a b
    derived :: forall (n :: Nat) s t a b. Context n s t a b => Traversal s t a b
    derived = (Rep (Indexed s 0) (ZonkAny 0)
     -> f (Rep (Indexed t 0) (ZonkAny 0)))
    -> s -> f t
    (RepN s (ZonkAny 0) -> f (RepN t (ZonkAny 0))) -> s -> f t
    forall a b x.
    (GenericN a, GenericN b) =>
    Traversal a b (RepN a x) (RepN b x)
    Traversal s t (RepN s (ZonkAny 0)) (RepN t (ZonkAny 0))
    repIsoN ((Rep (Indexed s 0) (ZonkAny 0)
      -> f (Rep (Indexed t 0) (ZonkAny 0)))
     -> s -> f t)
    -> ((a -> f b)
        -> Rep (Indexed s 0) (ZonkAny 0)
        -> f (Rep (Indexed t 0) (ZonkAny 0)))
    -> (a -> f b)
    -> s
    -> f t
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . forall {k} {k1} (ch :: k) (s :: k1 -> *) (t :: k1 -> *) a b
           (x :: k1).
    GHasTypes ch s t a b =>
    Traversal (s x) (t x) a b
    forall ch (s :: * -> *) (t :: * -> *) a b x.
    GHasTypes ch s t a b =>
    Traversal (s x) (t x) a b
    gtypes_ @ChGeneric ((Param n a -> f (Param n b))
     -> Rep (Indexed s 0) (ZonkAny 0)
     -> f (Rep (Indexed t 0) (ZonkAny 0)))
    -> ((a -> f b) -> Param n a -> f (Param n b))
    -> (a -> f b)
    -> Rep (Indexed s 0) (ZonkAny 0)
    -> f (Rep (Indexed t 0) (ZonkAny 0))
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . forall (n :: Nat) a b (f :: * -> *).
    Applicative f =>
    (a -> f b) -> Param n a -> f (Param n b)
    paramIso @n

    -- this could be an iso but since we're operating on a VL traversal it's easier this way.
    repIsoN :: (GenericN a, GenericN b) => Traversal a b (RepN a x) (RepN b x)
    repIsoN :: forall a b x.
    (GenericN a, GenericN b) =>
    Traversal a b (RepN a x) (RepN b x)
    repIsoN RepN a x -> f (RepN b x)
    f a
    a = Rep (Indexed b 0) x -> b
    RepN b x -> b
    forall a x. GenericN a => RepN a x -> a
    forall x. RepN b x -> b
    toN (Rep (Indexed b 0) x -> b) -> f (Rep (Indexed b 0) x) -> f b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> RepN a x -> f (RepN b x)
    f (a -> RepN a x
    forall x. a -> RepN a x
    forall a x. GenericN a => a -> RepN a x
    fromN a
    a)

    -- this could be an iso but since we're operating on a VL traversal it's easier this way.
    paramIso :: Traversal (Param n a) (Param n b) a b
    paramIso :: forall (n :: Nat) a b (f :: * -> *).
    Applicative f =>
    (a -> f b) -> Param n a -> f (Param n b)
    paramIso a -> f b
    f Param n a
    a = b -> Param n b
    forall (n :: Nat) a. a -> Param n a
    StarParam (b -> Param n b) -> f b -> f (Param n b)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> a -> f b
    f (Param n a -> a
    forall (n :: Nat) a. Param n a -> a
    getStarParam Param n a
    a)

    type family Error (b :: Bool) (expected :: Nat) (actual :: Nat) (s :: Type) :: Constraint where
      Error 'False _ _ _
        = ()

      Error 'True expected actual typ
        = TypeError
            (     'Text "Expected a type with at least "
            ':<>: 'ShowType (expected + 1)
            ':<>: 'Text " parameters, but "
            ':$$: 'ShowType typ
            ':<>: 'Text " only has "
            ':<>: 'ShowType actual
            )