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

import           Data.Kind
import           Data.PolyKinded.Functor
import           Data.Proxy

import           Generics.Kind

kfmapDefault :: forall k (f :: k) v as bs. (GenericK f, GenericK f, GFunctor (RepK f) v as bs)
             => Mappings v as bs -> f :@@: as -> f :@@: bs
kfmapDefault :: forall k (f :: k) (v :: Variances) (as :: LoT k) (bs :: LoT k).
(GenericK @k f, GenericK @k f, GFunctor @k (RepK @k f) v as bs) =>
Mappings @k v as bs -> (:@@:) @k f as -> (:@@:) @k f bs
kfmapDefault Mappings @k v as bs
v = forall k (f :: k) (x :: LoT k).
GenericK @k f =>
RepK @k f x -> (:@@:) @k f x
toK @k @f @bs (RepK @k f bs -> (:@@:) @k f bs)
-> ((:@@:) @k f as -> RepK @k f bs)
-> (:@@:) @k f as
-> (:@@:) @k f bs
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mappings @k v as bs -> RepK @k f as -> RepK @k f bs
forall k (f :: LoT k -> *) (v :: Variances) (as :: LoT k)
       (bs :: LoT k).
GFunctor @k f v as bs =>
Mappings @k v as bs -> f as -> f bs
gfmap Mappings @k v as bs
v (RepK @k f as -> RepK @k f bs)
-> ((:@@:) @k f as -> RepK @k f as)
-> (:@@:) @k f as
-> RepK @k f bs
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 @k @f @as

fmapDefault' :: forall (f :: Type -> Type) a b.
                (GenericK f, GenericK f,
                 GFunctor (RepK f) '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0))
              => (a -> b) -> f a -> f b
fmapDefault' :: forall (f :: * -> *) a b.
(GenericK @(* -> *) f, GenericK @(* -> *) f,
 GFunctor
   @(* -> *)
   (RepK @(* -> *) f)
   ((':) @Variance 'Co ('[] @Variance))
   ((':&&:) @(*) @(*) a 'LoT0)
   ((':&&:) @(*) @(*) b 'LoT0)) =>
(a -> b) -> f a -> f b
fmapDefault' a -> b
f = Mappings
  @(* -> *)
  ((':) @Variance 'Co ('[] @Variance))
  ((':&&:) @(*) @(*) a 'LoT0)
  ((':&&:) @(*) @(*) b 'LoT0)
-> (:@@:) @(* -> *) f ((':&&:) @(*) @(*) a 'LoT0)
-> (:@@:) @(* -> *) f ((':&&:) @(*) @(*) b 'LoT0)
forall k (f :: k) (v :: Variances) (as :: LoT k) (bs :: LoT k).
(GenericK @k f, GenericK @k f, GFunctor @k (RepK @k f) v as bs) =>
Mappings @k v as bs -> (:@@:) @k f as -> (:@@:) @k f bs
kfmapDefault (Mapping 'Co a b
a -> b
f Mapping 'Co a b
-> Mappings @(*) ('[] @Variance) 'LoT0 'LoT0
-> Mappings
     @(* -> *)
     ((':) @Variance 'Co ('[] @Variance))
     ((':&&:) @(*) @(*) a 'LoT0)
     ((':&&:) @(*) @(*) b 'LoT0)
forall {k1} (v1 :: Variance) a b (vs :: Variances) (as :: LoT k1)
       (bs :: LoT k1).
Mapping v1 a b
-> Mappings @k1 vs as bs
-> Mappings
     @(* -> k1)
     ((':) @Variance v1 vs)
     ((':&&:) @(*) @k1 a as)
     ((':&&:) @(*) @k1 b bs)
:^: Mappings @(*) ('[] @Variance) 'LoT0 'LoT0
M0 :: Mappings '[ 'Co ] (a ':&&: 'LoT0) (b ':&&: 'LoT0))

class GFunctor (f :: LoT k -> Type) (v :: Variances) (as :: LoT k) (bs :: LoT k) where
  gfmap :: Mappings v as bs -> f as -> f bs

instance GFunctor U1 v as bs where
  gfmap :: Mappings @k v as bs -> U1 @(LoT k) as -> U1 @(LoT k) bs
gfmap Mappings @k v as bs
_ U1 @(LoT k) as
U1 = U1 @(LoT k) bs
forall k (p :: k). U1 @k p
U1

instance GFunctor f v as bs => GFunctor (M1 i c f) v as bs where
  gfmap :: Mappings @k v as bs -> M1 @(LoT k) i c f as -> M1 @(LoT k) i c f bs
gfmap Mappings @k v as bs
v (M1 f as
x) = f bs -> M1 @(LoT k) i c f bs
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 @k i c f p
M1 (Mappings @k v as bs -> f as -> f bs
forall k (f :: LoT k -> *) (v :: Variances) (as :: LoT k)
       (bs :: LoT k).
GFunctor @k f v as bs =>
Mappings @k v as bs -> f as -> f bs
gfmap Mappings @k v as bs
v f as
x)

instance (GFunctor f v as bs, GFunctor g v as bs)
         => GFunctor (f :+: g) v as bs where
  gfmap :: Mappings @k v as bs
-> (:+:) @(LoT k) f g as -> (:+:) @(LoT k) f g bs
gfmap Mappings @k v as bs
v (L1 f as
x) = f bs -> (:+:) @(LoT k) f g bs
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> (:+:) @k f g p
L1 (Mappings @k v as bs -> f as -> f bs
forall k (f :: LoT k -> *) (v :: Variances) (as :: LoT k)
       (bs :: LoT k).
GFunctor @k f v as bs =>
Mappings @k v as bs -> f as -> f bs
gfmap Mappings @k v as bs
v f as
x)
  gfmap Mappings @k v as bs
v (R1 g as
x) = g bs -> (:+:) @(LoT k) f g bs
forall k (f :: k -> *) (g :: k -> *) (p :: k).
g p -> (:+:) @k f g p
R1 (Mappings @k v as bs -> g as -> g bs
forall k (f :: LoT k -> *) (v :: Variances) (as :: LoT k)
       (bs :: LoT k).
GFunctor @k f v as bs =>
Mappings @k v as bs -> f as -> f bs
gfmap Mappings @k v as bs
v g as
x)

instance (GFunctor f v as bs, GFunctor g v as bs)
         => GFunctor (f :*: g) v as bs where
  gfmap :: Mappings @k v as bs
-> (:*:) @(LoT k) f g as -> (:*:) @(LoT k) f g bs
gfmap Mappings @k v as bs
v (f as
x :*: g as
y) = Mappings @k v as bs -> f as -> f bs
forall k (f :: LoT k -> *) (v :: Variances) (as :: LoT k)
       (bs :: LoT k).
GFunctor @k f v as bs =>
Mappings @k v as bs -> f as -> f bs
gfmap Mappings @k v as bs
v f as
x f bs -> g bs -> (:*:) @(LoT k) f g bs
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) @k f g p
:*: Mappings @k v as bs -> g as -> g bs
forall k (f :: LoT k -> *) (v :: Variances) (as :: LoT k)
       (bs :: LoT k).
GFunctor @k f v as bs =>
Mappings @k v as bs -> f as -> f bs
gfmap Mappings @k v as bs
v g as
y

instance (Interpret c as => GFunctor f v as bs, {- Ty c as => -} Interpret c bs)
         => GFunctor (c :=>: f) v as bs where
  gfmap :: Mappings @k v as bs -> (:=>:) @k c f as -> (:=>:) @k c f bs
gfmap Mappings @k v as bs
v (SuchThat f as
x) = f bs -> (:=>:) @k c f bs
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 (Mappings @k v as bs -> f as -> f bs
forall k (f :: LoT k -> *) (v :: Variances) (as :: LoT k)
       (bs :: LoT k).
GFunctor @k f v as bs =>
Mappings @k v as bs -> f as -> f bs
gfmap Mappings @k v as bs
v f as
x)

instance forall f v as bs.
         (forall (t :: Type). GFunctor f ('Co ': v) (t ':&&: as) (t ':&&: bs))
         => GFunctor (Exists Type f) v as bs where
  gfmap :: Mappings @k v as bs -> Exists @k (*) f as -> Exists @k (*) f bs
gfmap Mappings @k v as bs
v (Exists (f ((':&&:) @(*) @k t as)
x :: f (t ':&&: x)))
    = f ((':&&:) @(*) @k t bs) -> Exists @k (*) f bs
forall k (t :: k) d (f :: LoT (k -> d) -> *) (x :: LoT d).
f ((':&&:) @k @d t x) -> Exists @d k f x
Exists (Mappings
  @(* -> k)
  ((':) @Variance 'Co v)
  ((':&&:) @(*) @k t as)
  ((':&&:) @(*) @k t bs)
-> f ((':&&:) @(*) @k t as) -> f ((':&&:) @(*) @k t bs)
forall k (f :: LoT k -> *) (v :: Variances) (as :: LoT k)
       (bs :: LoT k).
GFunctor @k f v as bs =>
Mappings @k v as bs -> f as -> f bs
gfmap ((Mapping 'Co t t
t -> t
forall a. a -> a
id Mapping 'Co t t
-> Mappings @k v as bs
-> Mappings
     @(* -> k)
     ((':) @Variance 'Co v)
     ((':&&:) @(*) @k t as)
     ((':&&:) @(*) @k t bs)
forall {k1} (v1 :: Variance) a b (vs :: Variances) (as :: LoT k1)
       (bs :: LoT k1).
Mapping v1 a b
-> Mappings @k1 vs as bs
-> Mappings
     @(* -> k1)
     ((':) @Variance v1 vs)
     ((':&&:) @(*) @k1 a as)
     ((':&&:) @(*) @k1 b bs)
:^: Mappings @k v as bs
v) :: Mappings ('Co ': v) (t ':&&: as) (t ':&&: bs)) f ((':&&:) @(*) @k t as)
x)

class GFunctorArg (t :: Atom d Type)
                  (v :: Variances) (intended :: Variance)
                  (as :: LoT d) (bs :: LoT d) where
  gfmapf :: Proxy t -> Proxy intended
         -> Mappings v as bs
         -> Mapping intended (Interpret t as) (Interpret t bs)

instance forall t v as bs. GFunctorArg t v 'Co as bs
         => GFunctor (Field t) v as bs where
  gfmap :: Mappings @k v as bs -> Field @k t as -> Field @k t bs
gfmap Mappings @k v as bs
v (Field Interpret @k @(*) t as
x) = Interpret @k @(*) t bs -> Field @k t bs
forall {d} (t :: Atom @LiftedRep d (*)) (x :: LoT d).
Interpret @d @(*) t x -> Field @d t x
Field (Proxy @(Atom @LiftedRep k (*)) t
-> Proxy @Variance 'Co
-> Mappings @k v as bs
-> Mapping 'Co (Interpret @k @(*) t as) (Interpret @k @(*) t bs)
forall d (t :: Atom @LiftedRep d (*)) (v :: Variances)
       (intended :: Variance) (as :: LoT d) (bs :: LoT d).
GFunctorArg @d t v intended as bs =>
Proxy @(Atom @LiftedRep d (*)) t
-> Proxy @Variance intended
-> Mappings @d v as bs
-> Mapping
     intended (Interpret @d @(*) t as) (Interpret @d @(*) t bs)
gfmapf (forall {k} (t :: k). Proxy @k t
forall (t :: Atom @LiftedRep k (*)).
Proxy @(Atom @LiftedRep k (*)) t
Proxy @t) (forall {k} (t :: k). Proxy @k t
forall (t :: Variance). Proxy @Variance t
Proxy @'Co) Mappings @k v as bs
v Interpret @k @(*) t as
x)

instance GFunctorArg ('Kon t) v 'Co as bs where
  gfmapf :: Proxy @(Atom @LiftedRep d (*)) ('Kon @(*) @d t)
-> Proxy @Variance 'Co
-> Mappings @d v as bs
-> Mapping
     'Co
     (Interpret @d @(*) ('Kon @(*) @d t) as)
     (Interpret @d @(*) ('Kon @(*) @d t) bs)
gfmapf Proxy @(Atom @LiftedRep d (*)) ('Kon @(*) @d t)
_ Proxy @Variance 'Co
_ Mappings @d v as bs
_ = Mapping
  'Co
  (Interpret @d @(*) ('Kon @(*) @d t) as)
  (Interpret @d @(*) ('Kon @(*) @d t) bs)
t -> t
forall a. a -> a
id
instance GFunctorArg ('Kon t) v 'Contra as bs where
  gfmapf :: Proxy @(Atom @LiftedRep d (*)) ('Kon @(*) @d t)
-> Proxy @Variance 'Contra
-> Mappings @d v as bs
-> Mapping
     'Contra
     (Interpret @d @(*) ('Kon @(*) @d t) as)
     (Interpret @d @(*) ('Kon @(*) @d t) bs)
gfmapf Proxy @(Atom @LiftedRep d (*)) ('Kon @(*) @d t)
_ Proxy @Variance 'Contra
_ Mappings @d v as bs
_ = Mapping
  'Contra
  (Interpret @d @(*) ('Kon @(*) @d t) as)
  (Interpret @d @(*) ('Kon @(*) @d t) bs)
t -> t
forall a. a -> a
id

instance forall d (f :: Atom (Type -> d) Type) v (as :: LoT d) (bs :: LoT d).
         (forall (t :: Type). GFunctorArg f ('Co ': v) 'Co (t ':&&: as) (t ':&&: bs))
         => GFunctorArg ('ForAll f) v 'Co as bs where
  gfmapf :: Proxy @(Atom @LiftedRep d (*)) ('ForAll @(*) @d f)
-> Proxy @Variance 'Co
-> Mappings @d v as bs
-> Mapping
     'Co
     (Interpret @d @(*) ('ForAll @(*) @d f) as)
     (Interpret @d @(*) ('ForAll @(*) @d f) bs)
gfmapf Proxy @(Atom @LiftedRep d (*)) ('ForAll @(*) @d f)
_ Proxy @Variance 'Co
_ Mappings @d v as bs
v ForAllI @(*) @d f as
x = (forall t. WrappedI @(* -> d) f ((':&&:) @(*) @d t bs))
-> ForAllI @(*) @d f bs
forall {d1} {d} (f :: Atom @LiftedRep (d1 -> d) (*))
       (tys :: LoT d).
(forall (t :: d1). WrappedI @(d1 -> d) f ((':&&:) @d1 @d t tys))
-> ForAllI @d1 @d f tys
fromWrappedI ((forall t. WrappedI @(* -> d) f ((':&&:) @(*) @d t bs))
 -> ForAllI @(*) @d f bs)
-> (forall t. WrappedI @(* -> d) f ((':&&:) @(*) @d t bs))
-> ForAllI @(*) @d f bs
forall a b. (a -> b) -> a -> b
$ WrappedI @(* -> d) f ((':&&:) @(*) @d t as)
-> WrappedI @(* -> d) f ((':&&:) @(*) @d t bs)
forall t.
WrappedI @(* -> d) f ((':&&:) @(*) @d t as)
-> WrappedI @(* -> d) f ((':&&:) @(*) @d t bs)
go (WrappedI @(* -> d) f ((':&&:) @(*) @d t as)
 -> WrappedI @(* -> d) f ((':&&:) @(*) @d t bs))
-> WrappedI @(* -> d) f ((':&&:) @(*) @d t as)
-> WrappedI @(* -> d) f ((':&&:) @(*) @d t bs)
forall a b. (a -> b) -> a -> b
$ ForAllI @(*) @d f as -> WrappedI @(* -> d) f ((':&&:) @(*) @d t as)
forall {d1} {ks} (f :: Atom @LiftedRep (d1 -> ks) (*))
       (tys :: LoT ks) (t :: d1).
ForAllI @d1 @ks f tys
-> WrappedI @(d1 -> ks) f ((':&&:) @d1 @ks t tys)
toWrappedI ForAllI @(*) @d f as
x
    where
      go :: forall (t :: Type). WrappedI f (t ':&&: as) -> WrappedI f (t ':&&: bs)
      go :: forall t.
WrappedI @(* -> d) f ((':&&:) @(*) @d t as)
-> WrappedI @(* -> d) f ((':&&:) @(*) @d t bs)
go (WrapI Interpret @(* -> d) @(*) f ((':&&:) @(*) @d t as)
p) = Interpret @(* -> d) @(*) f ((':&&:) @(*) @d t bs)
-> WrappedI @(* -> d) f ((':&&:) @(*) @d t bs)
forall d (f :: Atom @LiftedRep d (*)) (tys :: LoT d).
Interpret @d @(*) f tys -> WrappedI @d f tys
WrapI (forall d (t :: Atom @LiftedRep d (*)) (v :: Variances)
       (intended :: Variance) (as :: LoT d) (bs :: LoT d).
GFunctorArg @d t v intended as bs =>
Proxy @(Atom @LiftedRep d (*)) t
-> Proxy @Variance intended
-> Mappings @d v as bs
-> Mapping
     intended (Interpret @d @(*) t as) (Interpret @d @(*) t bs)
gfmapf @(Type -> d) @f @('Co ': v) @'Co @(t ':&&: as) @(t ':&&: bs)
                           Proxy @(Atom @LiftedRep (* -> d) (*)) f
forall {k} (t :: k). Proxy @k t
Proxy Proxy @Variance 'Co
forall {k} (t :: k). Proxy @k t
Proxy (Mapping 'Co t t
t -> t
forall a. a -> a
id Mapping 'Co t t
-> Mappings @d v as bs
-> Mappings
     @(* -> d)
     ((':) @Variance 'Co v)
     ((':&&:) @(*) @d t as)
     ((':&&:) @(*) @d t bs)
forall {k1} (v1 :: Variance) a b (vs :: Variances) (as :: LoT k1)
       (bs :: LoT k1).
Mapping v1 a b
-> Mappings @k1 vs as bs
-> Mappings
     @(* -> k1)
     ((':) @Variance v1 vs)
     ((':&&:) @(*) @k1 a as)
     ((':&&:) @(*) @k1 b bs)
:^: Mappings @d v as bs
v) Interpret @(* -> d) @(*) f ((':&&:) @(*) @d t as)
p)

instance GFunctorArg ('Var 'VZ) (r ': v) r (a ':&&: as) (b ':&&: bs) where
  gfmapf :: Proxy
  @(Atom @LiftedRep (* -> xs) (*))
  ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
-> Proxy @Variance r
-> Mappings
     @(* -> xs)
     ((':) @Variance r v)
     ((':&&:) @(*) @xs a as)
     ((':&&:) @(*) @xs b bs)
-> Mapping
     r
     (Interpret
        @(* -> xs)
        @(*)
        ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
        ((':&&:) @(*) @xs a as))
     (Interpret
        @(* -> xs)
        @(*)
        ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
        ((':&&:) @(*) @xs b bs))
gfmapf Proxy
  @(Atom @LiftedRep (* -> xs) (*))
  ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
_ Proxy @Variance r
_ (Mapping v1 a b
f :^: Mappings @k1 vs as bs
_) = Mapping
  r
  (Interpret
     @(* -> xs)
     @(*)
     ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
     ((':&&:) @(*) @xs a as))
  (Interpret
     @(* -> xs)
     @(*)
     ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
     ((':&&:) @(*) @xs b bs))
Mapping v1 a b
f

instance forall vr pre v intended a as b bs.
         GFunctorArg ('Var vr) v intended as bs
         => GFunctorArg ('Var ('VS vr)) (pre ': v) intended (a ':&&: as) (b ':&&: bs) where
  gfmapf :: Proxy
  @(Atom @LiftedRep (x -> ks) (*))
  ('Var @(x -> ks) @(*) ('VS @ks @(*) @x vr))
-> Proxy @Variance intended
-> Mappings
     @(x -> ks)
     ((':) @Variance pre v)
     ((':&&:) @x @ks a as)
     ((':&&:) @x @ks b bs)
-> Mapping
     intended
     (Interpret
        @(x -> ks)
        @(*)
        ('Var @(x -> ks) @(*) ('VS @ks @(*) @x vr))
        ((':&&:) @x @ks a as))
     (Interpret
        @(x -> ks)
        @(*)
        ('Var @(x -> ks) @(*) ('VS @ks @(*) @x vr))
        ((':&&:) @x @ks b bs))
gfmapf Proxy
  @(Atom @LiftedRep (x -> ks) (*))
  ('Var @(x -> ks) @(*) ('VS @ks @(*) @x vr))
_ Proxy @Variance intended
_ (Mapping v1 a b
_ :^: Mappings @k1 vs as bs
rest) = Proxy @(Atom @LiftedRep ks (*)) ('Var @ks @(*) vr)
-> Proxy @Variance intended
-> Mappings @ks vs as bs
-> Mapping
     intended
     (Interpret @ks @(*) ('Var @ks @(*) vr) as)
     (Interpret @ks @(*) ('Var @ks @(*) vr) bs)
forall d (t :: Atom @LiftedRep d (*)) (v :: Variances)
       (intended :: Variance) (as :: LoT d) (bs :: LoT d).
GFunctorArg @d t v intended as bs =>
Proxy @(Atom @LiftedRep d (*)) t
-> Proxy @Variance intended
-> Mappings @d v as bs
-> Mapping
     intended (Interpret @d @(*) t as) (Interpret @d @(*) t bs)
gfmapf (forall {k} (t :: k). Proxy @k t
forall (t :: Atom @LiftedRep ks (*)).
Proxy @(Atom @LiftedRep ks (*)) t
Proxy @('Var vr)) (forall {k} (t :: k). Proxy @k t
forall (t :: Variance). Proxy @Variance t
Proxy @intended) Mappings @ks vs as bs
Mappings @k1 vs as bs
rest

instance forall f x v v1 as bs.
         (KFunctor f '[v1] (Interpret x as ':&&: 'LoT0) (Interpret x bs ':&&: 'LoT0),
          GFunctorArg x v v1 as bs)
         => GFunctorArg (f :$: x) v 'Co as bs where
  gfmapf :: Proxy @(Atom @LiftedRep d (*)) ((:$:) @d @(*) @(*) f x)
-> Proxy @Variance 'Co
-> Mappings @d v as bs
-> Mapping
     'Co
     (Interpret @d @(*) ((:$:) @d @(*) @(*) f x) as)
     (Interpret @d @(*) ((:$:) @d @(*) @(*) f x) bs)
gfmapf Proxy @(Atom @LiftedRep d (*)) ((:$:) @d @(*) @(*) f x)
_ Proxy @Variance 'Co
_ Mappings @d v as bs
v = Mappings
  @(* -> *)
  ((':) @Variance v1 ('[] @Variance))
  ((':&&:) @(*) @(*) (Interpret @d @(*) x as) 'LoT0)
  ((':&&:) @(*) @(*) (Interpret @d @(*) x bs) 'LoT0)
-> (:@@:)
     @(* -> *) f ((':&&:) @(*) @(*) (Interpret @d @(*) x as) 'LoT0)
-> (:@@:)
     @(* -> *) f ((':&&:) @(*) @(*) (Interpret @d @(*) x bs) 'LoT0)
forall k (f :: k) (v :: Variances) (as :: LoT k) (bs :: LoT k).
KFunctor @k f v as bs =>
Mappings @k v as bs -> (:@@:) @k f as -> (:@@:) @k f bs
kfmap (Proxy @(Atom @LiftedRep d (*)) x
-> Proxy @Variance v1
-> Mappings @d v as bs
-> Mapping v1 (Interpret @d @(*) x as) (Interpret @d @(*) x bs)
forall d (t :: Atom @LiftedRep d (*)) (v :: Variances)
       (intended :: Variance) (as :: LoT d) (bs :: LoT d).
GFunctorArg @d t v intended as bs =>
Proxy @(Atom @LiftedRep d (*)) t
-> Proxy @Variance intended
-> Mappings @d v as bs
-> Mapping
     intended (Interpret @d @(*) t as) (Interpret @d @(*) t bs)
gfmapf (forall {k} (t :: k). Proxy @k t
forall (t :: Atom @LiftedRep d (*)).
Proxy @(Atom @LiftedRep d (*)) t
Proxy @x) (forall {k} (t :: k). Proxy @k t
forall (t :: Variance). Proxy @Variance t
Proxy @v1) Mappings @d v as bs
v Mapping v1 (Interpret @d @(*) x as) (Interpret @d @(*) x bs)
-> Mappings @(*) ('[] @Variance) 'LoT0 'LoT0
-> Mappings
     @(* -> *)
     ((':) @Variance v1 ('[] @Variance))
     ((':&&:) @(*) @(*) (Interpret @d @(*) x as) 'LoT0)
     ((':&&:) @(*) @(*) (Interpret @d @(*) x bs) 'LoT0)
forall {k1} (v1 :: Variance) a b (vs :: Variances) (as :: LoT k1)
       (bs :: LoT k1).
Mapping v1 a b
-> Mappings @k1 vs as bs
-> Mappings
     @(* -> k1)
     ((':) @Variance v1 vs)
     ((':&&:) @(*) @k1 a as)
     ((':&&:) @(*) @k1 b bs)
:^: Mappings @(*) ('[] @Variance) 'LoT0 'LoT0
M0)

instance forall f x y v v1 v2 as bs.
         (KFunctor f '[v1, v2] (Interpret x as ':&&: Interpret y as ':&&: 'LoT0)
                               (Interpret x bs ':&&: Interpret y bs ':&&: 'LoT0),
          GFunctorArg x v v1 as bs, GFunctorArg y v v2 as bs)
         => GFunctorArg (f :$: x ':@: y) v 'Co as bs where
  gfmapf :: Proxy
  @(Atom @LiftedRep d (*))
  ((':@:) @d @(*) @(*) ((:$:) @d @(* -> *) @(*) f x) y)
-> Proxy @Variance 'Co
-> Mappings @d v as bs
-> Mapping
     'Co
     (Interpret
        @d @(*) ((':@:) @d @(*) @(*) ((:$:) @d @(* -> *) @(*) f x) y) as)
     (Interpret
        @d @(*) ((':@:) @d @(*) @(*) ((:$:) @d @(* -> *) @(*) f x) y) bs)
gfmapf Proxy
  @(Atom @LiftedRep d (*))
  ((':@:) @d @(*) @(*) ((:$:) @d @(* -> *) @(*) f x) y)
_ Proxy @Variance 'Co
_ Mappings @d v as bs
v = Mappings
  @(* -> * -> *)
  ((':) @Variance v1 ((':) @Variance v2 ('[] @Variance)))
  ((':&&:)
     @(*)
     @(* -> *)
     (Interpret @d @(*) x as)
     ((':&&:) @(*) @(*) (Interpret @d @(*) y as) 'LoT0))
  ((':&&:)
     @(*)
     @(* -> *)
     (Interpret @d @(*) x bs)
     ((':&&:) @(*) @(*) (Interpret @d @(*) y bs) 'LoT0))
-> (:@@:)
     @(* -> * -> *)
     f
     ((':&&:)
        @(*)
        @(* -> *)
        (Interpret @d @(*) x as)
        ((':&&:) @(*) @(*) (Interpret @d @(*) y as) 'LoT0))
-> (:@@:)
     @(* -> * -> *)
     f
     ((':&&:)
        @(*)
        @(* -> *)
        (Interpret @d @(*) x bs)
        ((':&&:) @(*) @(*) (Interpret @d @(*) y bs) 'LoT0))
forall k (f :: k) (v :: Variances) (as :: LoT k) (bs :: LoT k).
KFunctor @k f v as bs =>
Mappings @k v as bs -> (:@@:) @k f as -> (:@@:) @k f bs
kfmap (Proxy @(Atom @LiftedRep d (*)) x
-> Proxy @Variance v1
-> Mappings @d v as bs
-> Mapping v1 (Interpret @d @(*) x as) (Interpret @d @(*) x bs)
forall d (t :: Atom @LiftedRep d (*)) (v :: Variances)
       (intended :: Variance) (as :: LoT d) (bs :: LoT d).
GFunctorArg @d t v intended as bs =>
Proxy @(Atom @LiftedRep d (*)) t
-> Proxy @Variance intended
-> Mappings @d v as bs
-> Mapping
     intended (Interpret @d @(*) t as) (Interpret @d @(*) t bs)
gfmapf (forall {k} (t :: k). Proxy @k t
forall (t :: Atom @LiftedRep d (*)).
Proxy @(Atom @LiftedRep d (*)) t
Proxy @x) (forall {k} (t :: k). Proxy @k t
forall (t :: Variance). Proxy @Variance t
Proxy @v1) Mappings @d v as bs
v Mapping v1 (Interpret @d @(*) x as) (Interpret @d @(*) x bs)
-> Mappings
     @(* -> *)
     ((':) @Variance v2 ('[] @Variance))
     ((':&&:) @(*) @(*) (Interpret @d @(*) y as) 'LoT0)
     ((':&&:) @(*) @(*) (Interpret @d @(*) y bs) 'LoT0)
-> Mappings
     @(* -> * -> *)
     ((':) @Variance v1 ((':) @Variance v2 ('[] @Variance)))
     ((':&&:)
        @(*)
        @(* -> *)
        (Interpret @d @(*) x as)
        ((':&&:) @(*) @(*) (Interpret @d @(*) y as) 'LoT0))
     ((':&&:)
        @(*)
        @(* -> *)
        (Interpret @d @(*) x bs)
        ((':&&:) @(*) @(*) (Interpret @d @(*) y bs) 'LoT0))
forall {k1} (v1 :: Variance) a b (vs :: Variances) (as :: LoT k1)
       (bs :: LoT k1).
Mapping v1 a b
-> Mappings @k1 vs as bs
-> Mappings
     @(* -> k1)
     ((':) @Variance v1 vs)
     ((':&&:) @(*) @k1 a as)
     ((':&&:) @(*) @k1 b bs)
:^:
                        Proxy @(Atom @LiftedRep d (*)) y
-> Proxy @Variance v2
-> Mappings @d v as bs
-> Mapping v2 (Interpret @d @(*) y as) (Interpret @d @(*) y bs)
forall d (t :: Atom @LiftedRep d (*)) (v :: Variances)
       (intended :: Variance) (as :: LoT d) (bs :: LoT d).
GFunctorArg @d t v intended as bs =>
Proxy @(Atom @LiftedRep d (*)) t
-> Proxy @Variance intended
-> Mappings @d v as bs
-> Mapping
     intended (Interpret @d @(*) t as) (Interpret @d @(*) t bs)
gfmapf (forall {k} (t :: k). Proxy @k t
forall (t :: Atom @LiftedRep d (*)).
Proxy @(Atom @LiftedRep d (*)) t
Proxy @y) (forall {k} (t :: k). Proxy @k t
forall (t :: Variance). Proxy @Variance t
Proxy @v2) Mappings @d v as bs
v Mapping v2 (Interpret @d @(*) y as) (Interpret @d @(*) y bs)
-> Mappings @(*) ('[] @Variance) 'LoT0 'LoT0
-> Mappings
     @(* -> *)
     ((':) @Variance v2 ('[] @Variance))
     ((':&&:) @(*) @(*) (Interpret @d @(*) y as) 'LoT0)
     ((':&&:) @(*) @(*) (Interpret @d @(*) y bs) 'LoT0)
forall {k1} (v1 :: Variance) a b (vs :: Variances) (as :: LoT k1)
       (bs :: LoT k1).
Mapping v1 a b
-> Mappings @k1 vs as bs
-> Mappings
     @(* -> k1)
     ((':) @Variance v1 vs)
     ((':&&:) @(*) @k1 a as)
     ((':&&:) @(*) @k1 b bs)
:^: Mappings @(*) ('[] @Variance) 'LoT0 'LoT0
M0)

instance forall f x y z v v1 v2 v3 as bs.
         (KFunctor f '[v1, v2, v3] (Interpret x as ':&&: Interpret y as ':&&: Interpret z as ':&&: 'LoT0)
                                   (Interpret x bs ':&&: Interpret y bs ':&&: Interpret z bs ':&&: 'LoT0),
          GFunctorArg x v v1 as bs, GFunctorArg y v v2 as bs, GFunctorArg z v v3 as bs)
         => GFunctorArg (f :$: x ':@: y ':@: z) v 'Co as bs where
  gfmapf :: Proxy
  @(Atom @LiftedRep d (*))
  ((':@:)
     @d
     @(*)
     @(*)
     ((':@:) @d @(*) @(* -> *) ((:$:) @d @(* -> * -> *) @(*) f x) y)
     z)
-> Proxy @Variance 'Co
-> Mappings @d v as bs
-> Mapping
     'Co
     (Interpret
        @d
        @(*)
        ((':@:)
           @d
           @(*)
           @(*)
           ((':@:) @d @(*) @(* -> *) ((:$:) @d @(* -> * -> *) @(*) f x) y)
           z)
        as)
     (Interpret
        @d
        @(*)
        ((':@:)
           @d
           @(*)
           @(*)
           ((':@:) @d @(*) @(* -> *) ((:$:) @d @(* -> * -> *) @(*) f x) y)
           z)
        bs)
gfmapf Proxy
  @(Atom @LiftedRep d (*))
  ((':@:)
     @d
     @(*)
     @(*)
     ((':@:) @d @(*) @(* -> *) ((:$:) @d @(* -> * -> *) @(*) f x) y)
     z)
_ Proxy @Variance 'Co
_ Mappings @d v as bs
v = Mappings
  @(* -> * -> * -> *)
  ((':)
     @Variance
     v1
     ((':) @Variance v2 ((':) @Variance v3 ('[] @Variance))))
  ((':&&:)
     @(*)
     @(* -> * -> *)
     (Interpret @d @(*) x as)
     ((':&&:)
        @(*)
        @(* -> *)
        (Interpret @d @(*) y as)
        ((':&&:) @(*) @(*) (Interpret @d @(*) z as) 'LoT0)))
  ((':&&:)
     @(*)
     @(* -> * -> *)
     (Interpret @d @(*) x bs)
     ((':&&:)
        @(*)
        @(* -> *)
        (Interpret @d @(*) y bs)
        ((':&&:) @(*) @(*) (Interpret @d @(*) z bs) 'LoT0)))
-> (:@@:)
     @(* -> * -> * -> *)
     f
     ((':&&:)
        @(*)
        @(* -> * -> *)
        (Interpret @d @(*) x as)
        ((':&&:)
           @(*)
           @(* -> *)
           (Interpret @d @(*) y as)
           ((':&&:) @(*) @(*) (Interpret @d @(*) z as) 'LoT0)))
-> (:@@:)
     @(* -> * -> * -> *)
     f
     ((':&&:)
        @(*)
        @(* -> * -> *)
        (Interpret @d @(*) x bs)
        ((':&&:)
           @(*)
           @(* -> *)
           (Interpret @d @(*) y bs)
           ((':&&:) @(*) @(*) (Interpret @d @(*) z bs) 'LoT0)))
forall k (f :: k) (v :: Variances) (as :: LoT k) (bs :: LoT k).
KFunctor @k f v as bs =>
Mappings @k v as bs -> (:@@:) @k f as -> (:@@:) @k f bs
kfmap (Proxy @(Atom @LiftedRep d (*)) x
-> Proxy @Variance v1
-> Mappings @d v as bs
-> Mapping v1 (Interpret @d @(*) x as) (Interpret @d @(*) x bs)
forall d (t :: Atom @LiftedRep d (*)) (v :: Variances)
       (intended :: Variance) (as :: LoT d) (bs :: LoT d).
GFunctorArg @d t v intended as bs =>
Proxy @(Atom @LiftedRep d (*)) t
-> Proxy @Variance intended
-> Mappings @d v as bs
-> Mapping
     intended (Interpret @d @(*) t as) (Interpret @d @(*) t bs)
gfmapf (forall {k} (t :: k). Proxy @k t
forall (t :: Atom @LiftedRep d (*)).
Proxy @(Atom @LiftedRep d (*)) t
Proxy @x) (forall {k} (t :: k). Proxy @k t
forall (t :: Variance). Proxy @Variance t
Proxy @v1) Mappings @d v as bs
v Mapping v1 (Interpret @d @(*) x as) (Interpret @d @(*) x bs)
-> Mappings
     @(* -> * -> *)
     ((':) @Variance v2 ((':) @Variance v3 ('[] @Variance)))
     ((':&&:)
        @(*)
        @(* -> *)
        (Interpret @d @(*) y as)
        ((':&&:) @(*) @(*) (Interpret @d @(*) z as) 'LoT0))
     ((':&&:)
        @(*)
        @(* -> *)
        (Interpret @d @(*) y bs)
        ((':&&:) @(*) @(*) (Interpret @d @(*) z bs) 'LoT0))
-> Mappings
     @(* -> * -> * -> *)
     ((':)
        @Variance
        v1
        ((':) @Variance v2 ((':) @Variance v3 ('[] @Variance))))
     ((':&&:)
        @(*)
        @(* -> * -> *)
        (Interpret @d @(*) x as)
        ((':&&:)
           @(*)
           @(* -> *)
           (Interpret @d @(*) y as)
           ((':&&:) @(*) @(*) (Interpret @d @(*) z as) 'LoT0)))
     ((':&&:)
        @(*)
        @(* -> * -> *)
        (Interpret @d @(*) x bs)
        ((':&&:)
           @(*)
           @(* -> *)
           (Interpret @d @(*) y bs)
           ((':&&:) @(*) @(*) (Interpret @d @(*) z bs) 'LoT0)))
forall {k1} (v1 :: Variance) a b (vs :: Variances) (as :: LoT k1)
       (bs :: LoT k1).
Mapping v1 a b
-> Mappings @k1 vs as bs
-> Mappings
     @(* -> k1)
     ((':) @Variance v1 vs)
     ((':&&:) @(*) @k1 a as)
     ((':&&:) @(*) @k1 b bs)
:^:
                        Proxy @(Atom @LiftedRep d (*)) y
-> Proxy @Variance v2
-> Mappings @d v as bs
-> Mapping v2 (Interpret @d @(*) y as) (Interpret @d @(*) y bs)
forall d (t :: Atom @LiftedRep d (*)) (v :: Variances)
       (intended :: Variance) (as :: LoT d) (bs :: LoT d).
GFunctorArg @d t v intended as bs =>
Proxy @(Atom @LiftedRep d (*)) t
-> Proxy @Variance intended
-> Mappings @d v as bs
-> Mapping
     intended (Interpret @d @(*) t as) (Interpret @d @(*) t bs)
gfmapf (forall {k} (t :: k). Proxy @k t
forall (t :: Atom @LiftedRep d (*)).
Proxy @(Atom @LiftedRep d (*)) t
Proxy @y) (forall {k} (t :: k). Proxy @k t
forall (t :: Variance). Proxy @Variance t
Proxy @v2) Mappings @d v as bs
v Mapping v2 (Interpret @d @(*) y as) (Interpret @d @(*) y bs)
-> Mappings
     @(* -> *)
     ((':) @Variance v3 ('[] @Variance))
     ((':&&:) @(*) @(*) (Interpret @d @(*) z as) 'LoT0)
     ((':&&:) @(*) @(*) (Interpret @d @(*) z bs) 'LoT0)
-> Mappings
     @(* -> * -> *)
     ((':) @Variance v2 ((':) @Variance v3 ('[] @Variance)))
     ((':&&:)
        @(*)
        @(* -> *)
        (Interpret @d @(*) y as)
        ((':&&:) @(*) @(*) (Interpret @d @(*) z as) 'LoT0))
     ((':&&:)
        @(*)
        @(* -> *)
        (Interpret @d @(*) y bs)
        ((':&&:) @(*) @(*) (Interpret @d @(*) z bs) 'LoT0))
forall {k1} (v1 :: Variance) a b (vs :: Variances) (as :: LoT k1)
       (bs :: LoT k1).
Mapping v1 a b
-> Mappings @k1 vs as bs
-> Mappings
     @(* -> k1)
     ((':) @Variance v1 vs)
     ((':&&:) @(*) @k1 a as)
     ((':&&:) @(*) @k1 b bs)
:^:
                        Proxy @(Atom @LiftedRep d (*)) z
-> Proxy @Variance v3
-> Mappings @d v as bs
-> Mapping v3 (Interpret @d @(*) z as) (Interpret @d @(*) z bs)
forall d (t :: Atom @LiftedRep d (*)) (v :: Variances)
       (intended :: Variance) (as :: LoT d) (bs :: LoT d).
GFunctorArg @d t v intended as bs =>
Proxy @(Atom @LiftedRep d (*)) t
-> Proxy @Variance intended
-> Mappings @d v as bs
-> Mapping
     intended (Interpret @d @(*) t as) (Interpret @d @(*) t bs)
gfmapf (forall {k} (t :: k). Proxy @k t
forall (t :: Atom @LiftedRep d (*)).
Proxy @(Atom @LiftedRep d (*)) t
Proxy @z) (forall {k} (t :: k). Proxy @k t
forall (t :: Variance). Proxy @Variance t
Proxy @v3) Mappings @d v as bs
v Mapping v3 (Interpret @d @(*) z as) (Interpret @d @(*) z bs)
-> Mappings @(*) ('[] @Variance) 'LoT0 'LoT0
-> Mappings
     @(* -> *)
     ((':) @Variance v3 ('[] @Variance))
     ((':&&:) @(*) @(*) (Interpret @d @(*) z as) 'LoT0)
     ((':&&:) @(*) @(*) (Interpret @d @(*) z bs) 'LoT0)
forall {k1} (v1 :: Variance) a b (vs :: Variances) (as :: LoT k1)
       (bs :: LoT k1).
Mapping v1 a b
-> Mappings @k1 vs as bs
-> Mappings
     @(* -> k1)
     ((':) @Variance v1 vs)
     ((':&&:) @(*) @k1 a as)
     ((':&&:) @(*) @k1 b bs)
:^: Mappings @(*) ('[] @Variance) 'LoT0 'LoT0
M0)