{-# 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, 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)