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

import           Data.Kind
import           Data.Proxy
import           Generics.Kind
import qualified Fcf.Core as Fcf
import           Fcf.Combinators (Pure, Pure1, type (<=<))

fmapDefaultOne :: (GenericK f,
                   GenericK f,
                   GFunctorOne (RepK f),
                   Reqs (RepK f) a b)
                => (a -> b) -> f a -> f b
fmapDefaultOne :: forall (f :: * -> *) a b.
(GenericK @(* -> *) f, GenericK @(* -> *) f,
 GFunctorOne (RepK @(* -> *) f), Reqs (RepK @(* -> *) f) a b) =>
(a -> b) -> f a -> f b
fmapDefaultOne a -> b
f = RepK @(* -> *) f ((':&&:) @(*) @(*) b 'LoT0) -> f b
RepK @(* -> *) f ((':&&:) @(*) @(*) b 'LoT0)
-> (:@@:) @(* -> *) f ((':&&:) @(*) @(*) b 'LoT0)
forall k (f :: k) (x :: LoT k).
GenericK @k f =>
RepK @k f x -> (:@@:) @k f x
forall (x :: LoT (* -> *)).
RepK @(* -> *) f x -> (:@@:) @(* -> *) f x
toK (RepK @(* -> *) f ((':&&:) @(*) @(*) b 'LoT0) -> f b)
-> (f a -> RepK @(* -> *) f ((':&&:) @(*) @(*) b 'LoT0))
-> f a
-> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b)
-> RepK @(* -> *) f (LoT1 @(*) a)
-> RepK @(* -> *) f ((':&&:) @(*) @(*) b 'LoT0)
forall a b.
Reqs (RepK @(* -> *) f) a b =>
(a -> b)
-> RepK @(* -> *) f (LoT1 @(*) a) -> RepK @(* -> *) f (LoT1 @(*) b)
forall (f :: LoT (* -> *) -> *) a b.
(GFunctorOne f, Reqs f a b) =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
gfmapo a -> b
f (RepK @(* -> *) f (LoT1 @(*) a)
 -> RepK @(* -> *) f ((':&&:) @(*) @(*) b 'LoT0))
-> (f a -> RepK @(* -> *) f (LoT1 @(*) a))
-> f a
-> RepK @(* -> *) f ((':&&:) @(*) @(*) b 'LoT0)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> RepK @(* -> *) f (LoT1 @(*) a)
(:@@:) @(* -> *) f (LoT1 @(*) a) -> RepK @(* -> *) f (LoT1 @(*) a)
forall k (f :: k) (x :: LoT k).
GenericK @k f =>
(:@@:) @k f x -> RepK @k f x
forall (x :: LoT (* -> *)).
(:@@:) @(* -> *) f x -> RepK @(* -> *) f x
fromK

class GFunctorOne (f :: LoT (Type -> Type) -> Type) where
  type family Reqs f a b :: Constraint
  gfmapo :: Reqs f a b => (a -> b) -> f (LoT1 a) -> f (LoT1 b)

gfmapo' :: forall a b f. (GFunctorOne f, Reqs f a b)
        => (a -> b) -> f (LoT1 a) -> f (LoT1 b)
gfmapo' :: forall a b (f :: LoT (* -> *) -> *).
(GFunctorOne f, Reqs f a b) =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
gfmapo' = (a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
forall a b.
Reqs f a b =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
forall (f :: LoT (* -> *) -> *) a b.
(GFunctorOne f, Reqs f a b) =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
gfmapo


instance GFunctorOne U1 where
  type Reqs U1 a b = ()
  gfmapo :: forall a b.
Reqs (U1 @(LoT (* -> *))) a b =>
(a -> b)
-> U1 @(LoT (* -> *)) (LoT1 @(*) a)
-> U1 @(LoT (* -> *)) (LoT1 @(*) b)
gfmapo a -> b
_ U1 @(LoT (* -> *)) (LoT1 @(*) a)
U1 = U1 @(LoT (* -> *)) (LoT1 @(*) b)
forall k (p :: k). U1 @k p
U1

instance GFunctorOne f => GFunctorOne (M1 i c f) where
  type Reqs (M1 i c f) a b = Reqs f a b
  gfmapo :: forall a b.
Reqs (M1 @(LoT (* -> *)) i c f) a b =>
(a -> b)
-> M1 @(LoT (* -> *)) i c f (LoT1 @(*) a)
-> M1 @(LoT (* -> *)) i c f (LoT1 @(*) b)
gfmapo a -> b
v (M1 f (LoT1 @(*) a)
x) = f (LoT1 @(*) b) -> M1 @(LoT (* -> *)) i c f (LoT1 @(*) b)
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 @k i c f p
M1 ((a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
forall a b.
Reqs f a b =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
forall (f :: LoT (* -> *) -> *) a b.
(GFunctorOne f, Reqs f a b) =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
gfmapo a -> b
v f (LoT1 @(*) a)
x)

instance (GFunctorOne f, GFunctorOne g)
         => GFunctorOne (f :+: g) where
  type Reqs (f :+: g) a b = (Reqs f a b, Reqs g a b)
  gfmapo :: forall a b.
Reqs ((:+:) @(LoT (* -> *)) f g) a b =>
(a -> b)
-> (:+:) @(LoT (* -> *)) f g (LoT1 @(*) a)
-> (:+:) @(LoT (* -> *)) f g (LoT1 @(*) b)
gfmapo a -> b
v (L1 f (LoT1 @(*) a)
x) = f (LoT1 @(*) b) -> (:+:) @(LoT (* -> *)) f g (LoT1 @(*) b)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> (:+:) @k f g p
L1 ((a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
forall a b.
Reqs f a b =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
forall (f :: LoT (* -> *) -> *) a b.
(GFunctorOne f, Reqs f a b) =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
gfmapo a -> b
v f (LoT1 @(*) a)
x)
  gfmapo a -> b
v (R1 g (LoT1 @(*) a)
x) = g (LoT1 @(*) b) -> (:+:) @(LoT (* -> *)) f g (LoT1 @(*) b)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
g p -> (:+:) @k f g p
R1 ((a -> b) -> g (LoT1 @(*) a) -> g (LoT1 @(*) b)
forall a b.
Reqs g a b =>
(a -> b) -> g (LoT1 @(*) a) -> g (LoT1 @(*) b)
forall (f :: LoT (* -> *) -> *) a b.
(GFunctorOne f, Reqs f a b) =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
gfmapo a -> b
v g (LoT1 @(*) a)
x)

instance (GFunctorOne f, GFunctorOne g)
         => GFunctorOne (f :*: g) where
  type Reqs (f :*: g) a b = (Reqs f a b, Reqs g a b)
  gfmapo :: forall a b.
Reqs ((:*:) @(LoT (* -> *)) f g) a b =>
(a -> b)
-> (:*:) @(LoT (* -> *)) f g (LoT1 @(*) a)
-> (:*:) @(LoT (* -> *)) f g (LoT1 @(*) b)
gfmapo a -> b
v (f (LoT1 @(*) a)
x :*: g (LoT1 @(*) a)
y) = (a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
forall a b.
Reqs f a b =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
forall (f :: LoT (* -> *) -> *) a b.
(GFunctorOne f, Reqs f a b) =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
gfmapo a -> b
v f (LoT1 @(*) a)
x f (LoT1 @(*) b)
-> g (LoT1 @(*) b) -> (:*:) @(LoT (* -> *)) f g (LoT1 @(*) b)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) @k f g p
:*: (a -> b) -> g (LoT1 @(*) a) -> g (LoT1 @(*) b)
forall a b.
Reqs g a b =>
(a -> b) -> g (LoT1 @(*) a) -> g (LoT1 @(*) b)
forall (f :: LoT (* -> *) -> *) a b.
(GFunctorOne f, Reqs f a b) =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
gfmapo a -> b
v g (LoT1 @(*) a)
y

instance GFunctorOne f => GFunctorOne (c :=>: f) where
  type Reqs (c :=>: f) a b = (Interpret c (LoT1 b), Reqs f a b)
  -- actually you want     = Interpret c (LoT1 a) => (Interpret c (LoT1 b), Reqs f a b)
  gfmapo :: forall a b.
Reqs ((:=>:) @(* -> *) c f) a b =>
(a -> b)
-> (:=>:) @(* -> *) c f (LoT1 @(*) a)
-> (:=>:) @(* -> *) c f (LoT1 @(*) b)
gfmapo a -> b
v (SuchThat f (LoT1 @(*) a)
x) = f (LoT1 @(*) b) -> (:=>:) @(* -> *) c f (LoT1 @(*) b)
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 ((a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
forall a b.
Reqs f a b =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
forall (f :: LoT (* -> *) -> *) a b.
(GFunctorOne f, Reqs f a b) =>
(a -> b) -> f (LoT1 @(*) a) -> f (LoT1 @(*) b)
gfmapo a -> b
v f (LoT1 @(*) a)
x)

class GFunctorOneArg (t :: Atom (Type -> Type) Type) where
  gfmapof :: Proxy t -> (a -> b)
          -> Interpret t (LoT1 a) -> Interpret t (LoT1 b)

instance GFunctorOneArg t => GFunctorOne (Field t) where
  type Reqs (Field t) a b = (() :: Constraint)
  gfmapo :: forall a b.
Reqs (Field @(* -> *) t) a b =>
(a -> b)
-> Field @(* -> *) t (LoT1 @(*) a)
-> Field @(* -> *) t (LoT1 @(*) b)
gfmapo a -> b
v (Field Interpret @(* -> *) @(*) t (LoT1 @(*) a)
x) = Interpret @(* -> *) @(*) t (LoT1 @(*) b)
-> Field @(* -> *) t (LoT1 @(*) b)
forall {d} (t :: Atom @LiftedRep d (*)) (x :: LoT d).
Interpret @d @(*) t x -> Field @d t x
Field (Proxy @(Atom @LiftedRep (* -> *) (*)) t
-> (a -> b)
-> Interpret @(* -> *) @(*) t (LoT1 @(*) a)
-> Interpret @(* -> *) @(*) t (LoT1 @(*) b)
forall a b.
Proxy @(Atom @LiftedRep (* -> *) (*)) t
-> (a -> b)
-> Interpret @(* -> *) @(*) t (LoT1 @(*) a)
-> Interpret @(* -> *) @(*) t (LoT1 @(*) b)
forall (t :: Atom @LiftedRep (* -> *) (*)) a b.
GFunctorOneArg t =>
Proxy @(Atom @LiftedRep (* -> *) (*)) t
-> (a -> b)
-> Interpret @(* -> *) @(*) t (LoT1 @(*) a)
-> Interpret @(* -> *) @(*) t (LoT1 @(*) b)
gfmapof (forall {k} (t :: k). Proxy @k t
forall (t :: Atom @LiftedRep (* -> *) (*)).
Proxy @(Atom @LiftedRep (* -> *) (*)) t
Proxy @t) a -> b
v Interpret @(* -> *) @(*) t (LoT1 @(*) a)
x)

-- A constant
instance GFunctorOneArg ('Kon t) where
  gfmapof :: forall a b.
Proxy @(Atom @LiftedRep (* -> *) (*)) ('Kon @(*) @(* -> *) t)
-> (a -> b)
-> Interpret @(* -> *) @(*) ('Kon @(*) @(* -> *) t) (LoT1 @(*) a)
-> Interpret @(* -> *) @(*) ('Kon @(*) @(* -> *) t) (LoT1 @(*) b)
gfmapof Proxy @(Atom @LiftedRep (* -> *) (*)) ('Kon @(*) @(* -> *) t)
_ a -> b
_ Interpret @(* -> *) @(*) ('Kon @(*) @(* -> *) t) (LoT1 @(*) a)
x = Interpret @(* -> *) @(*) ('Kon @(*) @(* -> *) t) (LoT1 @(*) a)
Interpret
  @(* -> *) @(*) ('Kon @(*) @(* -> *) t) ((':&&:) @(*) @(*) b 'LoT0)
x
-- The type variable itself
instance GFunctorOneArg Var0 where
  gfmapof :: forall a b.
Proxy @(Atom @LiftedRep (* -> *) (*)) (Var0 @(*) @(*))
-> (a -> b)
-> Interpret @(* -> *) @(*) (Var0 @(*) @(*)) (LoT1 @(*) a)
-> Interpret @(* -> *) @(*) (Var0 @(*) @(*)) (LoT1 @(*) b)
gfmapof Proxy @(Atom @LiftedRep (* -> *) (*)) (Var0 @(*) @(*))
_ a -> b
f Interpret @(* -> *) @(*) (Var0 @(*) @(*)) (LoT1 @(*) a)
x = a -> b
f a
Interpret @(* -> *) @(*) (Var0 @(*) @(*)) (LoT1 @(*) a)
x
-- Going through functor
instance forall f x.
         (Functor f, GFunctorOneArg x)
         => GFunctorOneArg (f :$: x) where
  gfmapof :: forall a b.
Proxy
  @(Atom @LiftedRep (* -> *) (*)) ((:$:) @(* -> *) @(*) @(*) f x)
-> (a -> b)
-> Interpret
     @(* -> *) @(*) ((:$:) @(* -> *) @(*) @(*) f x) (LoT1 @(*) a)
-> Interpret
     @(* -> *) @(*) ((:$:) @(* -> *) @(*) @(*) f x) (LoT1 @(*) b)
gfmapof Proxy
  @(Atom @LiftedRep (* -> *) (*)) ((:$:) @(* -> *) @(*) @(*) f x)
_ a -> b
f Interpret
  @(* -> *) @(*) ((:$:) @(* -> *) @(*) @(*) f x) (LoT1 @(*) a)
x = (Interpret @(* -> *) @(*) x (LoT1 @(*) a)
 -> Interpret @(* -> *) @(*) x ((':&&:) @(*) @(*) b 'LoT0))
-> f (Interpret @(* -> *) @(*) x (LoT1 @(*) a))
-> f (Interpret @(* -> *) @(*) x ((':&&:) @(*) @(*) b 'LoT0))
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Proxy @(Atom @LiftedRep (* -> *) (*)) x
-> (a -> b)
-> Interpret @(* -> *) @(*) x (LoT1 @(*) a)
-> Interpret @(* -> *) @(*) x ((':&&:) @(*) @(*) b 'LoT0)
forall a b.
Proxy @(Atom @LiftedRep (* -> *) (*)) x
-> (a -> b)
-> Interpret @(* -> *) @(*) x (LoT1 @(*) a)
-> Interpret @(* -> *) @(*) x (LoT1 @(*) b)
forall (t :: Atom @LiftedRep (* -> *) (*)) a b.
GFunctorOneArg t =>
Proxy @(Atom @LiftedRep (* -> *) (*)) t
-> (a -> b)
-> Interpret @(* -> *) @(*) t (LoT1 @(*) a)
-> Interpret @(* -> *) @(*) t (LoT1 @(*) b)
gfmapof (forall {k} (t :: k). Proxy @k t
forall (t :: Atom @LiftedRep (* -> *) (*)).
Proxy @(Atom @LiftedRep (* -> *) (*)) t
Proxy @x) a -> b
f) f (Interpret @(* -> *) @(*) x (LoT1 @(*) a))
Interpret
  @(* -> *) @(*) ((:$:) @(* -> *) @(*) @(*) f x) (LoT1 @(*) a)
x

-- Support for Hkd, defunctionalized variant, simplfiied GenericK instance.
instance EFunctor f => GFunctorOneArg (Eval (Kon f :@: Var0)) where
  gfmapof :: forall a b.
Proxy
  @(Atom @LiftedRep (* -> *) (*))
  ('Eval
     @(* -> *)
     @(*)
     ((':@:)
        @(* -> *)
        @(*)
        @(* -> *)
        ('Kon @(* -> * -> *) @(* -> *) f)
        (Var0 @(*) @(*))))
-> (a -> b)
-> Interpret
     @(* -> *)
     @(*)
     ('Eval
        @(* -> *)
        @(*)
        ((':@:)
           @(* -> *)
           @(*)
           @(* -> *)
           ('Kon @(* -> * -> *) @(* -> *) f)
           (Var0 @(*) @(*))))
     (LoT1 @(*) a)
-> Interpret
     @(* -> *)
     @(*)
     ('Eval
        @(* -> *)
        @(*)
        ((':@:)
           @(* -> *)
           @(*)
           @(* -> *)
           ('Kon @(* -> * -> *) @(* -> *) f)
           (Var0 @(*) @(*))))
     (LoT1 @(*) b)
gfmapof Proxy
  @(Atom @LiftedRep (* -> *) (*))
  ('Eval
     @(* -> *)
     @(*)
     ((':@:)
        @(* -> *)
        @(*)
        @(* -> *)
        ('Kon @(* -> * -> *) @(* -> *) f)
        (Var0 @(*) @(*))))
_ a -> b
f Interpret
  @(* -> *)
  @(*)
  ('Eval
     @(* -> *)
     @(*)
     ((':@:)
        @(* -> *)
        @(*)
        @(* -> *)
        ('Kon @(* -> * -> *) @(* -> *) f)
        (Var0 @(*) @(*))))
  (LoT1 @(*) a)
x = forall (f :: * -> * -> *) a b.
EFunctor f =>
(a -> b) -> Eval @(*) (f a) -> Eval @(*) (f b)
emap @f a -> b
f Eval @(*) (f a)
Interpret
  @(* -> *)
  @(*)
  ('Eval
     @(* -> *)
     @(*)
     ((':@:)
        @(* -> *)
        @(*)
        @(* -> *)
        ('Kon @(* -> * -> *) @(* -> *) f)
        (Var0 @(*) @(*))))
  (LoT1 @(*) a)
x

-- Unary first-class family as a functor.
class EFunctor (f :: Type -> Fcf.Exp Type) where
  emap :: (a -> b) -> Fcf.Eval (f a) -> Fcf.Eval (f b)

-- The functor "x" (identity functor).
instance EFunctor Pure where
  emap :: forall a b.
(a -> b) -> Eval @(*) (Pure @(*) a) -> Eval @(*) (Pure @(*) b)
emap = (a -> b) -> a -> b
(a -> b) -> Eval @(*) (Pure @(*) a) -> Eval @(*) (Pure @(*) b)
forall a. a -> a
id

-- The functor "f x", for any Functor f
instance Functor f => EFunctor (Pure1 f) where
  emap :: forall a b.
(a -> b)
-> Eval @(*) (Pure1 @(*) @(*) f a)
-> Eval @(*) (Pure1 @(*) @(*) f b)
emap = (a -> b) -> f a -> f b
(a -> b)
-> Eval @(*) (Pure1 @(*) @(*) f a)
-> Eval @(*) (Pure1 @(*) @(*) f b)
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap

-- Composition of functors
instance (EFunctor t, EFunctor u) => EFunctor (t <=< u) where
  emap :: forall a b.
(a -> b)
-> Eval @(*) ((<=<) @(*) @(*) @(*) t u a)
-> Eval @(*) ((<=<) @(*) @(*) @(*) t u b)
emap = forall (f :: * -> * -> *) a b.
EFunctor f =>
(a -> b) -> Eval @(*) (f a) -> Eval @(*) (f b)
emap @t ((Eval @(*) (u a) -> Eval @(*) (u b))
 -> Eval @(*) (t (Eval @(*) (u a)))
 -> Eval @(*) (t (Eval @(*) (u b))))
-> ((a -> b) -> Eval @(*) (u a) -> Eval @(*) (u b))
-> (a -> b)
-> Eval @(*) (t (Eval @(*) (u a)))
-> Eval @(*) (t (Eval @(*) (u b)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> * -> *) a b.
EFunctor f =>
(a -> b) -> Eval @(*) (f a) -> Eval @(*) (f b)
emap @u