{-# 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.FunctorPosition where

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

fmapDefaultPos :: forall v f as bs.
                  (GenericK f, GenericK f,
                   GFunctorPos (RepK f) v as bs)
               => (Interpret ('Var v) as -> Interpret ('Var v) bs)
               -> f :@@: as -> f :@@: bs
fmapDefaultPos :: forall {k} (v :: TyVar @LiftedRep k (*)) (f :: k) (as :: LoT k)
       (bs :: LoT k).
(GenericK @k f, GenericK @k f,
 GFunctorPos @k (RepK @k f) v as bs) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> (:@@:) @k f as -> (:@@:) @k f bs
fmapDefaultPos Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) bs
f = forall k (f :: k) (x :: LoT k).
GenericK @k f =>
RepK @k f x -> (:@@:) @k f x
toK @_ @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
. forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k).
GFunctorPos @k f v as bs =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> f as -> f bs
gfmapp @_ @(RepK f) @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) bs
f (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 @_ @f @as

fmapDefault :: forall f a b. (GenericK f, GenericK f,
               GFunctorPos (RepK f) 'VZ (LoT1 a) (LoT1 b))
            => (a -> b) -> f a -> f b
fmapDefault :: forall (f :: * -> *) a b.
(GenericK @(* -> *) f, GenericK @(* -> *) f,
 GFunctorPos
   @(* -> *)
   (RepK @(* -> *) f)
   ('VZ @(*) @(*))
   (LoT1 @(*) a)
   (LoT1 @(*) b)) =>
(a -> b) -> f a -> f b
fmapDefault = forall {k} (v :: TyVar @LiftedRep k (*)) (f :: k) (as :: LoT k)
       (bs :: LoT k).
(GenericK @k f, GenericK @k f,
 GFunctorPos @k (RepK @k f) v as bs) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> (:@@:) @k f as -> (:@@:) @k f bs
forall (v :: TyVar @LiftedRep (* -> *) (*)) (f :: * -> *)
       (as :: LoT (* -> *)) (bs :: LoT (* -> *)).
(GenericK @(* -> *) f, GenericK @(* -> *) f,
 GFunctorPos @(* -> *) (RepK @(* -> *) f) v as bs) =>
(Interpret @(* -> *) @(*) ('Var @(* -> *) @(*) v) as
 -> Interpret @(* -> *) @(*) ('Var @(* -> *) @(*) v) bs)
-> (:@@:) @(* -> *) f as -> (:@@:) @(* -> *) f bs
fmapDefaultPos @'VZ @f @(LoT1 a) @(LoT1 b)

bimapDefault :: forall f a c b d.
                (GenericK f, GenericK f, GenericK f,
                 GFunctorPos (RepK f) 'VZ       (LoT2 a d) (LoT2 c d),
                 GFunctorPos (RepK f) ('VS 'VZ) (LoT2 a b) (LoT2 a d))
             => (a -> c) -> (b -> d) -> f a b -> f c d
bimapDefault :: forall (f :: * -> * -> *) a c b d.
(GenericK @(* -> * -> *) f, GenericK @(* -> * -> *) f,
 GenericK @(* -> * -> *) f,
 GFunctorPos
   @(* -> * -> *)
   (RepK @(* -> * -> *) f)
   ('VZ @(*) @(* -> *))
   (LoT2 @(*) @(*) a d)
   (LoT2 @(*) @(*) c d),
 GFunctorPos
   @(* -> * -> *)
   (RepK @(* -> * -> *) f)
   ('VS @(* -> *) @(*) @(*) ('VZ @(*) @(*)))
   (LoT2 @(*) @(*) a b)
   (LoT2 @(*) @(*) a d)) =>
(a -> c) -> (b -> d) -> f a b -> f c d
bimapDefault a -> c
f b -> d
g = forall {k} (v :: TyVar @LiftedRep k (*)) (f :: k) (as :: LoT k)
       (bs :: LoT k).
(GenericK @k f, GenericK @k f,
 GFunctorPos @k (RepK @k f) v as bs) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> (:@@:) @k f as -> (:@@:) @k f bs
forall (v :: TyVar @LiftedRep (* -> * -> *) (*)) (f :: * -> * -> *)
       (as :: LoT (* -> * -> *)) (bs :: LoT (* -> * -> *)).
(GenericK @(* -> * -> *) f, GenericK @(* -> * -> *) f,
 GFunctorPos @(* -> * -> *) (RepK @(* -> * -> *) f) v as bs) =>
(Interpret @(* -> * -> *) @(*) ('Var @(* -> * -> *) @(*) v) as
 -> Interpret @(* -> * -> *) @(*) ('Var @(* -> * -> *) @(*) v) bs)
-> (:@@:) @(* -> * -> *) f as -> (:@@:) @(* -> * -> *) f bs
fmapDefaultPos @'VZ       @f @(LoT2 a d) @(LoT2 c d) a -> c
Interpret
  @(* -> * -> *)
  @(*)
  ('Var @(* -> * -> *) @(*) ('VZ @(*) @(* -> *)))
  (LoT2 @(*) @(*) a d)
-> Interpret
     @(* -> * -> *)
     @(*)
     ('Var @(* -> * -> *) @(*) ('VZ @(*) @(* -> *)))
     (LoT2 @(*) @(*) c d)
f
                 (f a d -> f c d) -> (f a b -> f a d) -> f a b -> f c d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (v :: TyVar @LiftedRep k (*)) (f :: k) (as :: LoT k)
       (bs :: LoT k).
(GenericK @k f, GenericK @k f,
 GFunctorPos @k (RepK @k f) v as bs) =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> (:@@:) @k f as -> (:@@:) @k f bs
forall (v :: TyVar @LiftedRep (* -> * -> *) (*)) (f :: * -> * -> *)
       (as :: LoT (* -> * -> *)) (bs :: LoT (* -> * -> *)).
(GenericK @(* -> * -> *) f, GenericK @(* -> * -> *) f,
 GFunctorPos @(* -> * -> *) (RepK @(* -> * -> *) f) v as bs) =>
(Interpret @(* -> * -> *) @(*) ('Var @(* -> * -> *) @(*) v) as
 -> Interpret @(* -> * -> *) @(*) ('Var @(* -> * -> *) @(*) v) bs)
-> (:@@:) @(* -> * -> *) f as -> (:@@:) @(* -> * -> *) f bs
fmapDefaultPos @('VS 'VZ) @f @(LoT2 a b) @(LoT2 a d) b -> d
Interpret
  @(* -> * -> *)
  @(*)
  ('Var
     @(* -> * -> *) @(*) ('VS @(* -> *) @(*) @(*) ('VZ @(*) @(*))))
  (LoT2 @(*) @(*) a b)
-> Interpret
     @(* -> * -> *)
     @(*)
     ('Var
        @(* -> * -> *) @(*) ('VS @(* -> *) @(*) @(*) ('VZ @(*) @(*))))
     (LoT2 @(*) @(*) a d)
g

class GFunctorPos (f :: LoT k -> Type) (v :: TyVar k Type)
                  (as :: LoT k) (bs :: LoT k) where
  gfmapp :: (Interpret ('Var v) as -> Interpret ('Var v) bs)
         -> f as -> f bs

instance GFunctorPos U1 v as bs where
  gfmapp :: (Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> U1 @(LoT k) as -> U1 @(LoT k) bs
gfmapp Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) bs
_ U1 @(LoT k) as
U1 = U1 @(LoT k) bs
forall k (p :: k). U1 @k p
U1

instance forall f v as bs i c. GFunctorPos f v as bs
         => GFunctorPos (M1 i c f) v as bs where
  gfmapp :: (Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> M1 @(LoT k) i c f as -> M1 @(LoT k) i c f bs
gfmapp Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) 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 (forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k).
GFunctorPos @k f v as bs =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> f as -> f bs
gfmapp @_ @f @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) bs
v f as
x)

instance forall f g v as bs. (GFunctorPos f v as bs, GFunctorPos g v as bs)
         => GFunctorPos (f :+: g) v as bs where
  gfmapp :: (Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> (:+:) @(LoT k) f g as -> (:+:) @(LoT k) f g bs
gfmapp Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) 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 (forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k).
GFunctorPos @k f v as bs =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> f as -> f bs
gfmapp @_ @f @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) bs
v f as
x)
  gfmapp Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) 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 (forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k).
GFunctorPos @k f v as bs =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> f as -> f bs
gfmapp @_ @g @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) bs
v g as
x)

instance forall f g v as bs. (GFunctorPos f v as bs, GFunctorPos g v as bs)
         => GFunctorPos (f :*: g) v as bs where
  gfmapp :: (Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> (:*:) @(LoT k) f g as -> (:*:) @(LoT k) f g bs
gfmapp Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) bs
v (f as
x :*: g as
y) = forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k).
GFunctorPos @k f v as bs =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> f as -> f bs
gfmapp @_ @f @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) 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
:*: forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k).
GFunctorPos @k f v as bs =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> f as -> f bs
gfmapp @_ @g @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) bs
v g as
y

instance forall c f v as bs z.
         (Interpret c as => GFunctorPos f v as bs, z ~ Interpret c bs, Interpret c as => z)
         => GFunctorPos (c :=>: f) v as bs where
  gfmapp :: (Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> (:=>:) @k c f as -> (:=>:) @k c f bs
gfmapp Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) 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 (forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k).
GFunctorPos @k f v as bs =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> f as -> f bs
gfmapp @_ @f @v @as @bs Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) bs
v f as
x)

instance forall k f v as bs.
         (forall (t :: k). GFunctorPos f ('VS v) (t ':&&: as) (t ':&&: bs))
         => GFunctorPos (Exists k f) v as bs where
  gfmapp :: (Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> Exists @k k f as -> Exists @k k f bs
gfmapp Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) bs
v (Exists (f ((':&&:) @k @k t as)
x :: f (t ':&&: x)))
    = f ((':&&:) @k @k t bs) -> Exists @k 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 (forall k (f :: LoT k -> *) (v :: TyVar @LiftedRep k (*))
       (as :: LoT k) (bs :: LoT k).
GFunctorPos @k f v as bs =>
(Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> f as -> f bs
gfmapp @_ @f @('VS v) @(t ':&&: x) @(t ':&&: _) Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) bs
Interpret
  @(k -> k)
  @(*)
  ('Var @(k -> k) @(*) ('VS @k @(*) @k v))
  ((':&&:) @k @k t as)
-> Interpret
     @(k -> k)
     @(*)
     ('Var @(k -> k) @(*) ('VS @k @(*) @k v))
     ((':&&:) @k @k t bs)
v f ((':&&:) @k @k t as)
x)

instance forall t v as bs. GFunctorArgPos t v as bs (ContainsTyVar v t)
         => GFunctorPos (Field t) v as bs where
  gfmapp :: (Interpret @k @(*) ('Var @k @(*) v) as
 -> Interpret @k @(*) ('Var @k @(*) v) bs)
-> Field @k t as -> Field @k t bs
gfmapp Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) 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 (forall d (t :: Atom @LiftedRep d (*)) (v :: TyVar @LiftedRep d (*))
       (as :: LoT d) (bs :: LoT d) (p :: Bool).
GFunctorArgPos @d t v as bs p =>
(Interpret @d @(*) ('Var @d @(*) v) as
 -> Interpret @d @(*) ('Var @d @(*) v) bs)
-> Interpret @d @(*) t as -> Interpret @d @(*) t bs
gfmappf @_ @t @v @as @bs @(ContainsTyVar v t) Interpret @k @(*) ('Var @k @(*) v) as
-> Interpret @k @(*) ('Var @k @(*) v) bs
v Interpret @k @(*) t as
x)

class GFunctorArgPos (t :: Atom d Type) (v :: TyVar d Type)
                     (as :: LoT d) (bs :: LoT d)
                     (p :: Bool) where
  gfmappf :: (Interpret ('Var v) as -> Interpret ('Var v) bs)
          -> Interpret t as -> Interpret t bs

instance (Interpret t as ~ Interpret t bs) => GFunctorArgPos t v as bs 'False where
  gfmappf :: (Interpret @d @(*) ('Var @d @(*) v) as
 -> Interpret @d @(*) ('Var @d @(*) v) bs)
-> Interpret @d @(*) t as -> Interpret @d @(*) t bs
gfmappf Interpret @d @(*) ('Var @d @(*) v) as
-> Interpret @d @(*) ('Var @d @(*) v) bs
_ = Interpret @d @(*) t as -> Interpret @d @(*) t bs
Interpret @d @(*) t bs -> Interpret @d @(*) t bs
forall a. a -> a
id

instance TypeError ('Text "Should never get here")
         => GFunctorArgPos ('Kon t) v as bs whatever where
  gfmappf :: (Interpret @d @(*) ('Var @d @(*) v) as
 -> Interpret @d @(*) ('Var @d @(*) v) bs)
-> Interpret @d @(*) ('Kon @(*) @d t) as
-> Interpret @d @(*) ('Kon @(*) @d t) bs
gfmappf Interpret @d @(*) ('Var @d @(*) v) as
-> Interpret @d @(*) ('Var @d @(*) v) bs
_ = t -> t
Interpret @d @(*) ('Kon @(*) @d t) as
-> Interpret @d @(*) ('Kon @(*) @d t) bs
forall a. a -> a
id

instance ( Functor (Interpret f as), Interpret f as ~ Interpret f bs
         , GFunctorArgPos x v as bs (ContainsTyVar v x) )
         => GFunctorArgPos (f ':@: x) v as bs 'True where
  gfmappf :: (Interpret @d @(*) ('Var @d @(*) v) as
 -> Interpret @d @(*) ('Var @d @(*) v) bs)
-> Interpret @d @(*) ((':@:) @d @(*) @(*) f x) as
-> Interpret @d @(*) ((':@:) @d @(*) @(*) f x) bs
gfmappf Interpret @d @(*) ('Var @d @(*) v) as
-> Interpret @d @(*) ('Var @d @(*) v) bs
f Interpret @d @(*) ((':@:) @d @(*) @(*) f x) as
x = (Interpret @d @(*) x as -> Interpret @d @(*) x bs)
-> Interpret @d @(* -> *) f bs (Interpret @d @(*) x as)
-> Interpret @d @(* -> *) f bs (Interpret @d @(*) x bs)
forall a b.
(a -> b)
-> Interpret @d @(* -> *) f bs a -> Interpret @d @(* -> *) f bs b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall d (t :: Atom @LiftedRep d (*)) (v :: TyVar @LiftedRep d (*))
       (as :: LoT d) (bs :: LoT d) (p :: Bool).
GFunctorArgPos @d t v as bs p =>
(Interpret @d @(*) ('Var @d @(*) v) as
 -> Interpret @d @(*) ('Var @d @(*) v) bs)
-> Interpret @d @(*) t as -> Interpret @d @(*) t bs
gfmappf @_ @x @v @as @bs @(ContainsTyVar v x) Interpret @d @(*) ('Var @d @(*) v) as
-> Interpret @d @(*) ('Var @d @(*) v) bs
f) Interpret @d @(*) ((':@:) @d @(*) @(*) f x) as
Interpret @d @(* -> *) f bs (Interpret @d @(*) x as)
x

-- We found the same variable
instance GFunctorArgPos ('Var 'VZ) 'VZ (a ':&&: as) (b ':&&: bs) 'True where
  gfmappf :: (Interpret
   @(* -> xs)
   @(*)
   ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
   ((':&&:) @(*) @xs a as)
 -> Interpret
      @(* -> xs)
      @(*)
      ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
      ((':&&:) @(*) @xs b bs))
-> Interpret
     @(* -> xs)
     @(*)
     ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
     ((':&&:) @(*) @xs a as)
-> Interpret
     @(* -> xs)
     @(*)
     ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
     ((':&&:) @(*) @xs b bs)
gfmappf Interpret
  @(* -> xs)
  @(*)
  ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
  ((':&&:) @(*) @xs a as)
-> 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)
-> 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.
         GFunctorArgPos ('Var v) n as bs isthere
         => GFunctorArgPos ('Var ('VS v)) ('VS n) (r ':&&: as) (s ':&&: bs) isthere where
  gfmappf :: (Interpret
   @(x -> d)
   @(*)
   ('Var @(x -> d) @(*) ('VS @d @(*) @x n))
   ((':&&:) @x @d r as)
 -> 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)
-> Interpret
     @(x -> d)
     @(*)
     ('Var @(x -> d) @(*) ('VS @d @(*) @x v))
     ((':&&:) @x @d s bs)
gfmappf Interpret
  @(x -> d)
  @(*)
  ('Var @(x -> d) @(*) ('VS @d @(*) @x n))
  ((':&&:) @x @d r as)
-> 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).
GFunctorArgPos @d t v as bs p =>
(Interpret @d @(*) ('Var @d @(*) v) as
 -> Interpret @d @(*) ('Var @d @(*) v) bs)
-> Interpret @d @(*) t as -> Interpret @d @(*) t bs
gfmappf @d @('Var v) @n @as @bs @isthere Interpret @d @(*) ('Var @d @(*) n) as
-> Interpret @d @(*) ('Var @d @(*) n) bs
Interpret
  @(x -> d)
  @(*)
  ('Var @(x -> d) @(*) ('VS @d @(*) @x n))
  ((':&&:) @x @d r as)
-> Interpret
     @(x -> d)
     @(*)
     ('Var @(x -> d) @(*) ('VS @d @(*) @x n))
     ((':&&:) @x @d s bs)
f Interpret @d @(*) ('Var @d @(*) v) as
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")
         => GFunctorArgPos ('Var 'VZ) ('VS n) (r ':&&: as) (r ':&&: bs) 'True where
  gfmappf :: (Interpret
   @(* -> xs)
   @(*)
   ('Var @(* -> xs) @(*) ('VS @xs @(*) @(*) n))
   ((':&&:) @(*) @xs r as)
 -> Interpret
      @(* -> xs)
      @(*)
      ('Var @(* -> xs) @(*) ('VS @xs @(*) @(*) n))
      ((':&&:) @(*) @xs r bs))
-> Interpret
     @(* -> xs)
     @(*)
     ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
     ((':&&:) @(*) @xs r as)
-> Interpret
     @(* -> xs)
     @(*)
     ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
     ((':&&:) @(*) @xs r bs)
gfmappf Interpret
  @(* -> xs)
  @(*)
  ('Var @(* -> xs) @(*) ('VS @xs @(*) @(*) n))
  ((':&&:) @(*) @xs r as)
-> Interpret
     @(* -> xs)
     @(*)
     ('Var @(* -> xs) @(*) ('VS @xs @(*) @(*) n))
     ((':&&:) @(*) @xs r bs)
_ = r -> r
Interpret
  @(* -> xs)
  @(*)
  ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
  ((':&&:) @(*) @xs r as)
-> Interpret
     @(* -> xs)
     @(*)
     ('Var @(* -> xs) @(*) ('VZ @(*) @xs))
     ((':&&:) @(*) @xs r bs)
forall a. a -> a
id
instance TypeError ('Text "Should never get here")
         => GFunctorArgPos ('Var ('VS n)) 'VZ (r ':&&: 'LoT0) (r ':&&: 'LoT0) 'True where
  gfmappf :: (Interpret
   @(* -> *)
   @(*)
   ('Var @(* -> *) @(*) ('VZ @(*) @(*)))
   ((':&&:) @(*) @(*) r 'LoT0)
 -> Interpret
      @(* -> *)
      @(*)
      ('Var @(* -> *) @(*) ('VZ @(*) @(*)))
      ((':&&:) @(*) @(*) r 'LoT0))
-> Interpret
     @(* -> *)
     @(*)
     ('Var @(* -> *) @(*) ('VS @(*) @(*) @(*) n))
     ((':&&:) @(*) @(*) r 'LoT0)
-> Interpret
     @(* -> *)
     @(*)
     ('Var @(* -> *) @(*) ('VS @(*) @(*) @(*) n))
     ((':&&:) @(*) @(*) r 'LoT0)
gfmappf Interpret
  @(* -> *)
  @(*)
  ('Var @(* -> *) @(*) ('VZ @(*) @(*)))
  ((':&&:) @(*) @(*) r 'LoT0)
-> Interpret
     @(* -> *)
     @(*)
     ('Var @(* -> *) @(*) ('VZ @(*) @(*)))
     ((':&&:) @(*) @(*) r 'LoT0)
_ = Interpret
  @(* -> *)
  @(*)
  ('Var @(* -> *) @(*) ('VS @(*) @(*) @(*) n))
  ((':&&:) @(*) @(*) r 'LoT0)
-> Interpret
     @(* -> *)
     @(*)
     ('Var @(* -> *) @(*) ('VS @(*) @(*) @(*) n))
     ((':&&:) @(*) @(*) r 'LoT0)
InterpretVar @(*) @(*) n 'LoT0 -> InterpretVar @(*) @(*) n 'LoT0
forall a. a -> a
id

-- Alternative implementation
{-
type family EqualTyVar (v :: TyVar d Type) (w :: TyVar d Type) :: Bool where
  EqualTyVar v v = True
  EqualTyVar v w = False

class GFunctorVarPos (v :: TyVar d Type) (w :: TyVar d Type)
                     (as :: LoT d) (bs :: LoT d)
                     (equal :: Bool) where
  gfmappv :: (Interpret (Var w) as -> Interpret (Var w) bs)
          -> Interpret (Var v) as -> Interpret (Var v) bs

instance v ~ w => GFunctorVarPos v w as bs True where
  gfmappv f = f
instance (Interpret (Var v) as ~ Interpret (Var v) bs)
        => GFunctorVarPos v w as bs False where
  gfmappv _ = id

instance forall v w as bs. GFunctorVarPos v w as bs (EqualTyVar v w)
         => GFunctorArgPos (Var v) w as bs True where
  gfmappf = gfmappv @_ @v @w @as @bs @(EqualTyVar v w)
-}