{-# 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 :: Traversal s t a b
derived = (Rep (Indexed s 0) Any -> f (Rep (Indexed t 0) Any)) -> s -> f t
forall a b x.
(GenericN a, GenericN b) =>
Traversal a b (RepN a x) (RepN b x)
repIsoN ((Rep (Indexed s 0) Any -> f (Rep (Indexed t 0) Any)) -> s -> f t)
-> ((a -> f b)
    -> Rep (Indexed s 0) Any -> f (Rep (Indexed t 0) Any))
-> (a -> f b)
-> s
-> f t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k k (ch :: k) (s :: k -> *) (t :: k -> *) a b (x :: k).
GHasTypes ch s t a b =>
Traversal (s x) (t x) a b
forall (s :: * -> *) (t :: * -> *) a b x.
GHasTypes ChGeneric s t a b =>
Traversal (s x) (t x) a b
gtypes_ @ChGeneric ((Param n a -> f (Param n b))
 -> Rep (Indexed s 0) Any -> f (Rep (Indexed t 0) Any))
-> ((a -> f b) -> Param n a -> f (Param n b))
-> (a -> f b)
-> Rep (Indexed s 0) Any
-> f (Rep (Indexed t 0) Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. Traversal (Param n a) (Param n b) a b
forall (n :: Nat) a b. Traversal (Param n a) (Param n b) a 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 :: 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
forall a x. GenericN a => RepN a x -> a
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 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 :: (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
        )