{-# language AllowAmbiguousTypes   #-}
{-# language DataKinds             #-}
{-# language FlexibleContexts      #-}
{-# language FlexibleInstances     #-}
{-# language MultiParamTypeClasses #-}
{-# language PolyKinds             #-}
{-# language QuantifiedConstraints #-}
{-# language ScopedTypeVariables   #-}
{-# language TypeApplications      #-}
{-# language TypeFamilies          #-}
{-# language TypeOperators         #-}
{-# language UndecidableInstances  #-}
module Generics.Kind.Derive.Traversable where

import           Data.Kind
import           GHC.TypeLits
import           Generics.Kind

traverseDefaultPos :: forall v f as bs g.
                      (GenericK f, GenericK f,
                       GTraversable (RepK f) v as bs,
                       Applicative g)
                   => (Interpret ('Var v) as -> g (Interpret ('Var v) bs))
                   -> f :@@: as -> g (f :@@: bs)
traverseDefaultPos :: forall {k} (v :: TyVar @LiftedRep k (*)) (f :: k) (as :: LoT k)
       (bs :: LoT k) (g :: * -> *).
(GenericK @k f, GenericK @k f, GTraversable @k (RepK @k f) v as bs,
 Applicative g) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> (:@@:) @k f as -> g ((:@@:) @k f bs)
traverseDefaultPos Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
f = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall k (f :: k) (x :: LoT k).
GenericK @k f =>
RepK @k f x -> (:@@:) @k f x
toK @_ @f @bs) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k) (g :: * -> *).
(GTraversable @k f v as bs, Applicative g) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> f as -> g (f bs)
gtraverse @_ @(RepK f) @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (f :: k) (x :: LoT k).
GenericK @k f =>
(:@@:) @k f x -> RepK @k f x
fromK @_ @f @as

traverseDefault :: forall f a b g. (GenericK f, GenericK f,
                   GTraversable (RepK f) 'VZ (LoT1 a) (LoT1 b), Applicative g)
                => (a -> g b) -> f a -> g (f b)
traverseDefault :: forall (f :: * -> *) a b (g :: * -> *).
(GenericK @(* -> *) f, GenericK @(* -> *) f,
 GTraversable
   @(* -> *)
   (RepK @(* -> *) f)
   ('VZ @(*) @(*))
   (LoT1 @(*) a)
   (LoT1 @(*) b),
 Applicative g) =>
(a -> g b) -> f a -> g (f b)
traverseDefault = forall {k} (v :: TyVar @LiftedRep k (*)) (f :: k) (as :: LoT k)
       (bs :: LoT k) (g :: * -> *).
(GenericK @k f, GenericK @k f, GTraversable @k (RepK @k f) v as bs,
 Applicative g) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> (:@@:) @k f as -> g ((:@@:) @k f bs)
traverseDefaultPos @'VZ @f @(LoT1 a) @(LoT1 b)

class GTraversable (f :: LoT k -> Type) (v :: TyVar k Type)
                   (as :: LoT k) (bs :: LoT k) where
  gtraverse :: Applicative g
            => (Interpret ('Var v) as -> g (Interpret ('Var v) bs))
            -> f as -> g (f bs)

instance GTraversable U1 v as bs where
  gtraverse :: forall (g :: * -> *).
Applicative g =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> U1 @(LoT k) as -> g (U1 @(LoT k) bs)
gtraverse Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
_ U1 @(LoT k) as
U1 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall k (p :: k). U1 @k p
U1

instance forall f v as bs i c. GTraversable f v as bs
         => GTraversable (M1 i c f) v as bs where
  gtraverse :: forall (g :: * -> *).
Applicative g =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> M1 @(LoT k) i c f as -> g (M1 @(LoT k) i c f bs)
gtraverse Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v (M1 f as
x) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 @k i c f p
M1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k) (g :: * -> *).
(GTraversable @k f v as bs, Applicative g) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> f as -> g (f bs)
gtraverse @_ @f @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v f as
x

instance forall f g v as bs. (GTraversable f v as bs, GTraversable g v as bs)
         => GTraversable (f :+: g) v as bs where
  gtraverse :: forall (g :: * -> *).
Applicative g =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> (:+:) @(LoT k) f g as -> g ((:+:) @(LoT k) f g bs)
gtraverse Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v (L1 f as
x) = forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> (:+:) @k f g p
L1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k) (g :: * -> *).
(GTraversable @k f v as bs, Applicative g) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> f as -> g (f bs)
gtraverse @_ @f @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v f as
x
  gtraverse Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v (R1 g as
x) = forall k (f :: k -> *) (g :: k -> *) (p :: k).
g p -> (:+:) @k f g p
R1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k) (g :: * -> *).
(GTraversable @k f v as bs, Applicative g) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> f as -> g (f bs)
gtraverse @_ @g @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v g as
x

instance forall f g v as bs. (GTraversable f v as bs, GTraversable g v as bs)
         => GTraversable (f :*: g) v as bs where
  gtraverse :: forall (g :: * -> *).
Applicative g =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> (:*:) @(LoT k) f g as -> g ((:*:) @(LoT k) f g bs)
gtraverse Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v (f as
x :*: g as
y) = forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) @k f g p
(:*:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k) (g :: * -> *).
(GTraversable @k f v as bs, Applicative g) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> f as -> g (f bs)
gtraverse @_ @f @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v f as
x
                                forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k) (g :: * -> *).
(GTraversable @k f v as bs, Applicative g) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> f as -> g (f bs)
gtraverse @_ @g @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v g as
y

instance forall c f v as bs z.
         (Interpret c as => GTraversable f v as bs, z ~ Interpret c bs, Interpret c as => z)
         => GTraversable (c :=>: f) v as bs where
  gtraverse :: forall (g :: * -> *).
Applicative g =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> (:=>:) @k c f as -> g ((:=>:) @k c f bs)
gtraverse Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v (SuchThat f as
x) = forall {d} (c :: Atom @LiftedRep d Constraint) (x :: LoT d)
       (f :: LoT d -> *).
Interpret @d @Constraint c x =>
f x -> (:=>:) @d c f x
SuchThat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k) (g :: * -> *).
(GTraversable @k f v as bs, Applicative g) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> f as -> g (f bs)
gtraverse @_ @f @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v f as
x

instance forall k f v as bs.
         (forall (t :: k). GTraversable f ('VS v) (t ':&&: as) (t ':&&: bs))
         => GTraversable (Exists k f) v as bs where
  gtraverse :: forall (g :: * -> *).
Applicative g =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> Exists @k k f as -> g (Exists @k k f bs)
gtraverse Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v (Exists (f ((':&&:) @k @k t as)
x :: f (t ':&&: x)))
    = forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f ((':&&:) @k @d t x) -> Exists @d k f x
Exists forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k) (g :: * -> *).
(GTraversable @k f v as bs, Applicative g) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> f as -> g (f bs)
gtraverse @_ @f @('VS v) @(t ':&&: x) @(t ':&&: _) Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v f ((':&&:) @k @k t as)
x

instance forall t v as bs. GTraversableArg t v as bs (ContainsTyVar v t)
         => GTraversable (Field t) v as bs where
  gtraverse :: forall (g :: * -> *).
Applicative g =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> g (Interpret @k @(*) ('Var @k @(*) v) bs))
-> Field @k t as -> g (Field @k t bs)
gtraverse Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v (Field Interpret @k @(*) t as
x) = forall {d} (t :: Atom @LiftedRep d (*)) (x :: LoT d).
Interpret @d @(*) t x -> Field @d t x
Field forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall d (t :: Atom @LiftedRep d (*)) (v :: TyVar @LiftedRep d (*))
       (as :: LoT d) (bs :: LoT d) (p :: Bool) (g :: * -> *).
(GTraversableArg @d t v as bs p, Applicative g) =>
(Interpret @d @(*) ('Var @d @(*) v) as
 -> g (Interpret @d @(*) ('Var @d @(*) v) bs))
-> Interpret @d @(*) t as -> g (Interpret @d @(*) t bs)
gtraversef @_ @t @v @as @bs @(ContainsTyVar v t) Interpret @k @(*) ('Var @k @(*) v) as
-> g (Interpret @k @(*) ('Var @k @(*) v) bs)
v Interpret @k @(*) t as
x

class GTraversableArg (t :: Atom d Type) (v :: TyVar d Type)
                      (as :: LoT d) (bs :: LoT d) (p :: Bool) where
  gtraversef :: Applicative g
             => (Interpret ('Var v) as -> g (Interpret ('Var v) bs))
             -> Interpret t as -> g (Interpret t bs)

instance (Interpret t as ~ Interpret t bs) => GTraversableArg t v as bs 'False where
  gtraversef :: forall (g :: * -> *).
Applicative g =>
(Interpret @d @(*) ('Var @d @(*) v) as
 -> g (Interpret @d @(*) ('Var @d @(*) v) bs))
-> Interpret @d @(*) t as -> g (Interpret @d @(*) t bs)
gtraversef Interpret @d @(*) ('Var @d @(*) v) as
-> g (Interpret @d @(*) ('Var @d @(*) v) bs)
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance TypeError ('Text "Should never get here")
         => GTraversableArg ('Kon t) v as bs whatever where
  gtraversef :: forall (g :: * -> *).
Applicative g =>
(Interpret @d @(*) ('Var @d @(*) v) as
 -> g (Interpret @d @(*) ('Var @d @(*) v) bs))
-> Interpret @d @(*) ('Kon @(*) @d t) as
-> g (Interpret @d @(*) ('Kon @(*) @d t) bs)
gtraversef Interpret @d @(*) ('Var @d @(*) v) as
-> g (Interpret @d @(*) ('Var @d @(*) v) bs)
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure

instance ( Traversable (Interpret f as), Interpret f as ~ Interpret f bs
         , GTraversableArg x v as bs (ContainsTyVar v x))
         => GTraversableArg (f ':@: x) v as bs 'True where
  gtraversef :: forall (g :: * -> *).
Applicative g =>
(Interpret @d @(*) ('Var @d @(*) v) as
 -> g (Interpret @d @(*) ('Var @d @(*) v) bs))
-> Interpret @d @(*) ((':@:) @d @(*) @(*) f x) as
-> g (Interpret @d @(*) ((':@:) @d @(*) @(*) f x) bs)
gtraversef Interpret @d @(*) ('Var @d @(*) v) as
-> g (Interpret @d @(*) ('Var @d @(*) v) bs)
f Interpret @d @(*) ((':@:) @d @(*) @(*) f x) as
x = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall d (t :: Atom @LiftedRep d (*)) (v :: TyVar @LiftedRep d (*))
       (as :: LoT d) (bs :: LoT d) (p :: Bool) (g :: * -> *).
(GTraversableArg @d t v as bs p, Applicative g) =>
(Interpret @d @(*) ('Var @d @(*) v) as
 -> g (Interpret @d @(*) ('Var @d @(*) v) bs))
-> Interpret @d @(*) t as -> g (Interpret @d @(*) t bs)
gtraversef @_ @x @v @as @bs @(ContainsTyVar v x) Interpret @d @(*) ('Var @d @(*) v) as
-> g (Interpret @d @(*) ('Var @d @(*) v) bs)
f) Interpret @d @(*) ((':@:) @d @(*) @(*) f x) as
x

-- We found the same variable
instance GTraversableArg ('Var 'VZ) 'VZ (a ':&&: as) (b ':&&: bs) 'True where
  gtraversef :: forall (g :: * -> *).
Applicative g =>
(Interpret
   @(* -> xs)
   @(*)
   ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
   ((':&&:) @(*) @xs a as)
 -> g (Interpret
         @(* -> xs)
         @(*)
         ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
         ((':&&:) @(*) @xs b bs)))
-> Interpret
     @(* -> xs)
     @(*)
     ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
     ((':&&:) @(*) @xs a as)
-> g (Interpret
        @(* -> xs)
        @(*)
        ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
        ((':&&:) @(*) @xs b bs))
gtraversef Interpret
  @(* -> xs)
  @(*)
  ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
  ((':&&:) @(*) @xs a as)
-> g (Interpret
        @(* -> xs)
        @(*)
        ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
        ((':&&:) @(*) @xs b bs))
f Interpret
  @(* -> xs)
  @(*)
  ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
  ((':&&:) @(*) @xs a as)
x = Interpret
  @(* -> xs)
  @(*)
  ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
  ((':&&:) @(*) @xs a as)
-> g (Interpret
        @(* -> xs)
        @(*)
        ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
        ((':&&:) @(*) @xs b bs))
f Interpret
  @(* -> xs)
  @(*)
  ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
  ((':&&:) @(*) @xs a as)
x
-- We need to keep looking
instance forall d (v :: TyVar d Type) n r as s bs isthere.
         GTraversableArg ('Var v) n as bs isthere
         => GTraversableArg ('Var ('VS v)) ('VS n) (r ':&&: as) (s ':&&: bs) isthere where
  gtraversef :: forall (g :: * -> *).
Applicative g =>
(Interpret
   @(x -> d)
   @(*)
   ('Var @(x -> d) @(*) ('VS @d @(*) @x n))
   ((':&&:) @x @d r as)
 -> g (Interpret
         @(x -> d)
         @(*)
         ('Var @(x -> d) @(*) ('VS @d @(*) @x n))
         ((':&&:) @x @d s bs)))
-> Interpret
     @(x -> d)
     @(*)
     ('Var @(x -> d) @(*) ('VS @d @(*) @x v))
     ((':&&:) @x @d r as)
-> g (Interpret
        @(x -> d)
        @(*)
        ('Var @(x -> d) @(*) ('VS @d @(*) @x v))
        ((':&&:) @x @d s bs))
gtraversef Interpret
  @(x -> d)
  @(*)
  ('Var @(x -> d) @(*) ('VS @d @(*) @x n))
  ((':&&:) @x @d r as)
-> g (Interpret
        @(x -> d)
        @(*)
        ('Var @(x -> d) @(*) ('VS @d @(*) @x n))
        ((':&&:) @x @d s bs))
f Interpret
  @(x -> d)
  @(*)
  ('Var @(x -> d) @(*) ('VS @d @(*) @x v))
  ((':&&:) @x @d r as)
x = forall d (t :: Atom @LiftedRep d (*)) (v :: TyVar @LiftedRep d (*))
       (as :: LoT d) (bs :: LoT d) (p :: Bool) (g :: * -> *).
(GTraversableArg @d t v as bs p, Applicative g) =>
(Interpret @d @(*) ('Var @d @(*) v) as
 -> g (Interpret @d @(*) ('Var @d @(*) v) bs))
-> Interpret @d @(*) t as -> g (Interpret @d @(*) t bs)
gtraversef @d @('Var v) @n @as @bs @isthere Interpret
  @(x -> d)
  @(*)
  ('Var @(x -> d) @(*) ('VS @d @(*) @x n))
  ((':&&:) @x @d r as)
-> g (Interpret
        @(x -> d)
        @(*)
        ('Var @(x -> d) @(*) ('VS @d @(*) @x n))
        ((':&&:) @x @d s bs))
f Interpret
  @(x -> d)
  @(*)
  ('Var @(x -> d) @(*) ('VS @d @(*) @x v))
  ((':&&:) @x @d r as)
x
-- If we arrive to another we do not want, keep it as it is
instance TypeError ('Text "Should never get here")
         => GTraversableArg ('Var 'VZ) ('VS n) (r ':&&: as) (r ':&&: bs) 'True where
  gtraversef :: forall (g :: * -> *).
Applicative g =>
(Interpret
   @(* -> xs)
   @(*)
   ('Var @(* -> xs) @(*) ('VS @xs @(*) @(*) n))
   ((':&&:) @(*) @xs r as)
 -> g (Interpret
         @(* -> xs)
         @(*)
         ('Var @(* -> xs) @(*) ('VS @xs @(*) @(*) n))
         ((':&&:) @(*) @xs r bs)))
-> Interpret
     @(* -> xs)
     @(*)
     ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
     ((':&&:) @(*) @xs r as)
-> g (Interpret
        @(* -> xs)
        @(*)
        ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
        ((':&&:) @(*) @xs r bs))
gtraversef Interpret
  @(* -> xs)
  @(*)
  ('Var @(* -> xs) @(*) ('VS @xs @(*) @(*) n))
  ((':&&:) @(*) @xs r as)
-> g (Interpret
        @(* -> xs)
        @(*)
        ('Var @(* -> xs) @(*) ('VS @xs @(*) @(*) n))
        ((':&&:) @(*) @xs r bs))
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure