{-# OPTIONS_GHC -Wno-missing-methods -Wno-orphans #-}
{-# LANGUAGE AllowAmbiguousTypes      #-}
{-# LANGUAGE ConstraintKinds          #-}
{-# LANGUAGE DataKinds                #-}
{-# LANGUAGE DefaultSignatures        #-}
{-# LANGUAGE FlexibleContexts         #-}
{-# LANGUAGE FlexibleInstances        #-}
{-# LANGUAGE GADTs                    #-}
{-# LANGUAGE InstanceSigs             #-}
{-# LANGUAGE MultiParamTypeClasses    #-}
{-# LANGUAGE PolyKinds                #-}
{-# LANGUAGE RankNTypes               #-}
{-# LANGUAGE ScopedTypeVariables      #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications         #-}
{-# LANGUAGE TypeFamilies             #-}
{-# LANGUAGE TypeOperators            #-}
{-# LANGUAGE UndecidableInstances     #-}
module Data.ZipMatchK.Generic where

import           Data.Kind              (Constraint, Type)
import           Data.List.NonEmpty
import           Generics.Kind
import           Generics.Kind.Examples ()
import           GHC.TypeError
import           Data.ZipMatchK.Mappings

-- | Kind-polymorphic syntactic (first-order) unification of two values.
--
-- Note: @f@ is expected to be a traversable n-functor,
-- but at the moment we lack a @TraversableK@ constraint.
class ZipMatchK (f :: k) where
  -- | Perform one level of equality testing:
  --
  -- * when @k = 'Type'@, values are compared directly (e.g. via 'Eq');
  -- * when @k = 'Type' -> 'Type'@, we compare term constructors;
  --   if term constructors are unequal, we return 'Nothing';
  --   otherwise, we pair up all components with a given function.
  zipMatchWithK :: forall as bs cs. Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)
  default zipMatchWithK :: forall as bs cs.
    (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs)
    => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)
  zipMatchWithK = forall (f :: k) (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
(GenericK f, GZipMatch (RepK f),
 ReqsZipMatchWith (RepK f) as bs cs) =>
Mappings as bs cs
-> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs)
forall {k} (f :: k) (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
(GenericK f, GZipMatch (RepK f),
 ReqsZipMatchWith (RepK f) as bs cs) =>
Mappings as bs cs
-> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs)
genericZipMatchWithK @f @as @bs @cs

-- | Generic implementation of 'Data.ZipMatch.zipMatchK'.
genericZipMatchK :: forall f as bs.
    (GenericK f, GZipMatch (RepK f), ReqsZipMatch (RepK f) as bs, PairMappings as bs)
    => f :@@: as -> f :@@: bs -> Maybe (f :@@: (ZipLoT as bs))
genericZipMatchK :: forall {k} (f :: k) (as :: LoT k) (bs :: LoT k).
(GenericK f, GZipMatch (RepK f), ReqsZipMatch (RepK f) as bs,
 PairMappings as bs) =>
(f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: ZipLoT as bs)
genericZipMatchK = forall (f :: k) (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
(GenericK f, GZipMatch (RepK f),
 ReqsZipMatchWith (RepK f) as bs cs) =>
Mappings as bs cs
-> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs)
forall {k} (f :: k) (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
(GenericK f, GZipMatch (RepK f),
 ReqsZipMatchWith (RepK f) as bs cs) =>
Mappings as bs cs
-> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs)
genericZipMatchWithK @f @as @bs Mappings as bs (ZipLoT as bs)
forall k (as :: LoT k) (bs :: LoT k).
PairMappings as bs =>
Mappings as bs (ZipLoT as bs)
pairMappings

-- | Generic implementation of 'zipMatchWithK'.
genericZipMatchWithK :: forall f as bs cs.
    (GenericK f, GZipMatch (RepK f), ReqsZipMatchWith (RepK f) as bs cs)
    => Mappings as bs cs -> f :@@: as -> f :@@: bs -> Maybe (f :@@: cs)
genericZipMatchWithK :: forall {k} (f :: k) (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
(GenericK f, GZipMatch (RepK f),
 ReqsZipMatchWith (RepK f) as bs cs) =>
Mappings as bs cs
-> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs)
genericZipMatchWithK Mappings as bs cs
mappings f :@@: as
x f :@@: bs
y = forall k (f :: k) (x :: LoT k). GenericK f => RepK f x -> f :@@: x
toK @_ @f @cs (RepK f cs -> f :@@: cs) -> Maybe (RepK f cs) -> Maybe (f :@@: cs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mappings as bs cs -> RepK f as -> RepK f bs -> Maybe (RepK f cs)
forall k (f :: LoT k -> *) (as :: LoT k) (bs :: LoT k)
       (cs :: LoT k).
(GZipMatch f, ReqsZipMatchWith f as bs cs) =>
Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith (RepK f) as bs cs =>
Mappings as bs cs -> RepK f as -> RepK f bs -> Maybe (RepK f cs)
gzipMatchWith Mappings as bs cs
mappings
  (forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @f @as f :@@: as
x)
  (forall k (f :: k) (x :: LoT k).
GenericK f =>
(f :@@: x) -> RepK f x
fromK @_ @f @bs f :@@: bs
y)

instance GenericK (,) where
  type RepK (,) = Field Var0 :*: Field Var1
instance GenericK ((,) a) where
  type RepK ((,) a) = Field (Kon a) :*: Field Var0
instance GenericK NonEmpty where
  type RepK NonEmpty = Field Var0 :*: Field ([] :$: Var0)

instance ZipMatchK (,)
instance ZipMatchK a => ZipMatchK ((,) a)
instance ZipMatchK []
instance ZipMatchK Maybe
instance ZipMatchK Either
instance ZipMatchK a => ZipMatchK (Either a)
instance ZipMatchK NonEmpty

type ReqsZipMatch f as bs = ReqsZipMatchWith f as bs (ZipLoT as bs)
class GZipMatch (f :: LoT k -> Type) where
  type ReqsZipMatchWith f (as :: LoT k) (bs :: LoT k) (cs :: LoT k) :: Constraint
  gzipMatchWith :: ReqsZipMatchWith f as bs cs => Mappings as bs cs -> f as -> f bs -> Maybe (f cs)

instance GZipMatch V1 where
  type ReqsZipMatchWith V1 as bs cs = ()
  gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith V1 as bs cs =>
Mappings as bs cs -> V1 as -> V1 bs -> Maybe (V1 cs)
gzipMatchWith Mappings as bs cs
_ V1 as
_ V1 bs
_ = [Char] -> Maybe (V1 cs)
forall a. HasCallStack => [Char] -> a
error [Char]
"impossible: Generics.Kind.V1 value!" -- FIXME: should be absurd

instance GZipMatch U1 where
  type ReqsZipMatchWith U1 as bs cs = ()
  gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith U1 as bs cs =>
Mappings as bs cs -> U1 as -> U1 bs -> Maybe (U1 cs)
gzipMatchWith Mappings as bs cs
_ U1 as
U1 U1 bs
U1 = U1 cs -> Maybe (U1 cs)
forall a. a -> Maybe a
Just U1 cs
forall k (p :: k). U1 p
U1

instance GZipMatch f => GZipMatch (M1 i c f) where
  type ReqsZipMatchWith (M1 i c f) as bs cs = ReqsZipMatchWith f as bs cs
  gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith (M1 i c f) as bs cs =>
Mappings as bs cs
-> M1 i c f as -> M1 i c f bs -> Maybe (M1 i c f cs)
gzipMatchWith Mappings as bs cs
g (M1 f as
x) (M1 f bs
y) = f cs -> M1 i c f cs
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f cs -> M1 i c f cs) -> Maybe (f cs) -> Maybe (M1 i c f cs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
forall k (f :: LoT k -> *) (as :: LoT k) (bs :: LoT k)
       (cs :: LoT k).
(GZipMatch f, ReqsZipMatchWith f as bs cs) =>
Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith f as bs cs =>
Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
gzipMatchWith Mappings as bs cs
g f as
x f bs
y

instance (GZipMatch f, GZipMatch g) => GZipMatch (f :+: g) where
  type ReqsZipMatchWith (f :+: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)
  gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith (f :+: g) as bs cs =>
Mappings as bs cs
-> (:+:) f g as -> (:+:) f g bs -> Maybe ((:+:) f g cs)
gzipMatchWith Mappings as bs cs
g (L1 f as
x) (L1 f bs
y) = f cs -> (:+:) f g cs
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f cs -> (:+:) f g cs) -> Maybe (f cs) -> Maybe ((:+:) f g cs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
forall k (f :: LoT k -> *) (as :: LoT k) (bs :: LoT k)
       (cs :: LoT k).
(GZipMatch f, ReqsZipMatchWith f as bs cs) =>
Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith f as bs cs =>
Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
gzipMatchWith Mappings as bs cs
g f as
x f bs
y
  gzipMatchWith Mappings as bs cs
g (R1 g as
x) (R1 g bs
y) = g cs -> (:+:) f g cs
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g cs -> (:+:) f g cs) -> Maybe (g cs) -> Maybe ((:+:) f g cs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mappings as bs cs -> g as -> g bs -> Maybe (g cs)
forall k (f :: LoT k -> *) (as :: LoT k) (bs :: LoT k)
       (cs :: LoT k).
(GZipMatch f, ReqsZipMatchWith f as bs cs) =>
Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith g as bs cs =>
Mappings as bs cs -> g as -> g bs -> Maybe (g cs)
gzipMatchWith Mappings as bs cs
g g as
x g bs
y
  gzipMatchWith Mappings as bs cs
_ (:+:) f g as
_ (:+:) f g bs
_           = Maybe ((:+:) f g cs)
forall a. Maybe a
Nothing

instance (GZipMatch f, GZipMatch g) => GZipMatch (f :*: g) where
  type ReqsZipMatchWith (f :*: g) as bs cs = (ReqsZipMatchWith f as bs cs, ReqsZipMatchWith g as bs cs)
  gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith (f :*: g) as bs cs =>
Mappings as bs cs
-> (:*:) f g as -> (:*:) f g bs -> Maybe ((:*:) f g cs)
gzipMatchWith Mappings as bs cs
g (f as
x :*: g as
y) (f bs
x' :*: g bs
y') =
    (f cs -> g cs -> (:*:) f g cs)
-> Maybe (f cs) -> Maybe (g cs) -> Maybe ((:*:) f g cs)
forall a b c. (a -> b -> c) -> Maybe a -> Maybe b -> Maybe c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 f cs -> g cs -> (:*:) f g cs
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
(:*:) (Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
forall k (f :: LoT k -> *) (as :: LoT k) (bs :: LoT k)
       (cs :: LoT k).
(GZipMatch f, ReqsZipMatchWith f as bs cs) =>
Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith f as bs cs =>
Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
gzipMatchWith Mappings as bs cs
g f as
x f bs
x') (Mappings as bs cs -> g as -> g bs -> Maybe (g cs)
forall k (f :: LoT k -> *) (as :: LoT k) (bs :: LoT k)
       (cs :: LoT k).
(GZipMatch f, ReqsZipMatchWith f as bs cs) =>
Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith g as bs cs =>
Mappings as bs cs -> g as -> g bs -> Maybe (g cs)
gzipMatchWith Mappings as bs cs
g g as
y g bs
y')

instance ZipMatchFields t => GZipMatch (Field t) where
  type ReqsZipMatchWith (Field t) as bs cs = ReqsZipMatchFieldsWith t as bs cs
  gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith (Field t) as bs cs =>
Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)
gzipMatchWith Mappings as bs cs
f Field t as
x Field t bs
y = Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)
forall d (t :: Atom d (*)) (as :: LoT d) (bs :: LoT d)
       (cs :: LoT d).
(ZipMatchFields t, ReqsZipMatchFieldsWith t as bs cs) =>
Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)
forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchFieldsWith t as bs cs =>
Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)
zipMatchFieldsWith Mappings as bs cs
f Field t as
x Field t bs
y

instance GZipMatch f => GZipMatch (c :=>: f) where
  type ReqsZipMatchWith (c :=>: f) as bs cs = (ReqsZipMatchWith f as bs cs, Interpret c cs)
  -- really we want          = (Interpret c as, Interpret c bs) => (ReqsZipMatch f as bs, Interpret c (ZipLoT as bs))
  gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith (c :=>: f) as bs cs =>
Mappings as bs cs
-> (:=>:) c f as -> (:=>:) c f bs -> Maybe ((:=>:) c f cs)
gzipMatchWith Mappings as bs cs
g (SuchThat f as
x) (SuchThat f bs
y) = f cs -> (:=>:) c f cs
forall {d} (c :: Atom d Constraint) (x :: LoT d) (f :: LoT d -> *).
Interpret c x =>
f x -> (:=>:) c f x
SuchThat (f cs -> (:=>:) c f cs) -> Maybe (f cs) -> Maybe ((:=>:) c f cs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
forall k (f :: LoT k -> *) (as :: LoT k) (bs :: LoT k)
       (cs :: LoT k).
(GZipMatch f, ReqsZipMatchWith f as bs cs) =>
Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith f as bs cs =>
Mappings as bs cs -> f as -> f bs -> Maybe (f cs)
gzipMatchWith Mappings as bs cs
g f as
x f bs
y

instance TypeError ('Text "Existentials are not supported")
         => GZipMatch (Exists k f) where
  type ReqsZipMatchWith (Exists k f) as bs cs = TypeError ('Text "Existentials are not supported")
  gzipMatchWith :: forall (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ReqsZipMatchWith (Exists k f) as bs cs =>
Mappings as bs cs
-> Exists k f as -> Exists k f bs -> Maybe (Exists k f cs)
gzipMatchWith = Mappings as bs cs
-> Exists k f as -> Exists k f bs -> Maybe (Exists k f cs)
forall a. HasCallStack => a
undefined

class ZipMatchFields (t :: Atom d Type) where
  type ReqsZipMatchFieldsWith t (as :: LoT d) (bs :: LoT d) (cs :: LoT d) :: Constraint
  zipMatchFieldsWith :: ReqsZipMatchFieldsWith t as bs cs => Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)

instance ApplyMappings v => ZipMatchFields (Var v) where
  -- this is always true, but GHC is not smart enough to know that, I think
  type ReqsZipMatchFieldsWith (Var v) as bs cs = () -- InterpretVar v cs ~ (InterpretVar v as, InterpretVar v bs))
  zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
ReqsZipMatchFieldsWith ('Var v) as bs cs =>
Mappings as bs cs
-> Field ('Var v) as
-> Field ('Var v) bs
-> Maybe (Field ('Var v) cs)
zipMatchFieldsWith Mappings as bs cs
g (Field Interpret ('Var v) as
x) (Field Interpret ('Var v) bs
y) = Interpret ('Var v) cs -> Field ('Var v) cs
InterpretVar v cs -> Field ('Var v) cs
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field (InterpretVar v cs -> Field ('Var v) cs)
-> Maybe (InterpretVar v cs) -> Maybe (Field ('Var v) cs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall d (v :: TyVar d (*)) (as :: LoT d) (bs :: LoT d)
       (cs :: LoT d).
ApplyMappings v =>
Mappings as bs cs
-> Interpret ('Var v) as
-> Interpret ('Var v) bs
-> Maybe (Interpret ('Var v) cs)
applyMappings @_ @v Mappings as bs cs
g Interpret ('Var v) as
x Interpret ('Var v) bs
y

instance ZipMatchK k => ZipMatchFields (Kon k) where
  type ReqsZipMatchFieldsWith (Kon k) as bs cs = ()
  zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
ReqsZipMatchFieldsWith ('Kon k) as bs cs =>
Mappings as bs cs
-> Field ('Kon k) as
-> Field ('Kon k) bs
-> Maybe (Field ('Kon k) cs)
zipMatchFieldsWith Mappings as bs cs
_ (Field Interpret ('Kon k) as
l) (Field Interpret ('Kon k) bs
r) = k -> Field ('Kon k) cs
Interpret ('Kon k) cs -> Field ('Kon k) cs
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field (k -> Field ('Kon k) cs) -> Maybe k -> Maybe (Field ('Kon k) cs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k (f :: k) (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ZipMatchK f =>
Mappings as bs cs
-> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs)
zipMatchWithK @_ @k Mappings 'LoT0 'LoT0 'LoT0
M0 k :@@: 'LoT0
Interpret ('Kon k) as
l k :@@: 'LoT0
Interpret ('Kon k) bs
r

instance {-# OVERLAPPING #-} (ZipMatchFields t, ZipMatchK k) => ZipMatchFields (Kon k :@: t) where
  type ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs = ReqsZipMatchFieldsWith t as bs cs

  zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith (Kon k :@: t) as bs cs =>
    Mappings as bs cs -> Field (Kon k :@: t) as -> Field (Kon k :@: t) bs -> Maybe (Field (Kon (k :: Type -> Type) :@: t) cs)
  zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
ReqsZipMatchFieldsWith ('Kon k ':@: t) as bs cs =>
Mappings as bs cs
-> Field ('Kon k ':@: t) as
-> Field ('Kon k ':@: t) bs
-> Maybe (Field ('Kon k ':@: t) cs)
zipMatchFieldsWith Mappings as bs cs
g (Field Interpret ('Kon k ':@: t) as
l) (Field Interpret ('Kon k ':@: t) bs
r) =
    k (Interpret t cs) -> Field ('Kon k ':@: t) cs
Interpret ('Kon k ':@: t) cs -> Field ('Kon k ':@: t) cs
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field (k (Interpret t cs) -> Field ('Kon k ':@: t) cs)
-> Maybe (k (Interpret t cs)) -> Maybe (Field ('Kon k ':@: t) cs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k (f :: k) (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ZipMatchK f =>
Mappings as bs cs
-> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs)
zipMatchWithK @_ @k @(Interpret t as :&&: LoT0) @(Interpret t bs :&&: LoT0) @(Interpret t cs :&&: LoT0)
      ((\Interpret t as
ll Interpret t bs
rr -> forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
forall (t :: Atom d (*)) (x :: LoT d). Field t x -> Interpret t x
unField @t (Field t cs -> Interpret t cs)
-> Maybe (Field t cs) -> Maybe (Interpret t cs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)
forall d (t :: Atom d (*)) (as :: LoT d) (bs :: LoT d)
       (cs :: LoT d).
(ZipMatchFields t, ReqsZipMatchFieldsWith t as bs cs) =>
Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)
forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
ReqsZipMatchFieldsWith t as bs cs =>
Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)
zipMatchFieldsWith Mappings as bs cs
g (Interpret t as -> Field t as
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Interpret t as
ll) (Interpret t bs -> Field t bs
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Interpret t bs
rr)) (Interpret t as -> Interpret t bs -> Maybe (Interpret t cs))
-> Mappings 'LoT0 'LoT0 'LoT0
-> Mappings
     (Interpret t as ':&&: 'LoT0)
     (Interpret t bs ':&&: 'LoT0)
     (Interpret t cs ':&&: 'LoT0)
forall {k1} a b c (as1 :: LoT k1) (bs1 :: LoT k1) (cs1 :: LoT k1).
(a -> b -> Maybe c)
-> Mappings as1 bs1 cs1
-> Mappings (a ':&&: as1) (b ':&&: bs1) (c ':&&: cs1)
:^: Mappings 'LoT0 'LoT0 'LoT0
M0) k :@@: (Interpret t as ':&&: 'LoT0)
Interpret ('Kon k ':@: t) as
l k :@@: (Interpret t bs ':&&: 'LoT0)
Interpret ('Kon k ':@: t) bs
r

instance {-# OVERLAPPING #-} (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) => ZipMatchFields ((Kon (k :: Type -> Type -> Type) :@: t1) :@: t2) where
  type ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs = (ReqsZipMatchFieldsWith t1 as bs cs, ReqsZipMatchFieldsWith t2 as bs cs)

  zipMatchFieldsWith :: forall as bs cs. ReqsZipMatchFieldsWith ((Kon k :@: t1) :@: t2) as bs cs =>
    Mappings as bs cs -> Field ((Kon k :@: t1) :@: t2) as -> Field ((Kon k :@: t1) :@: t2) bs -> Maybe (Field ((Kon k :@: t1) :@: t2) cs)
  zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
ReqsZipMatchFieldsWith (('Kon k ':@: t1) ':@: t2) as bs cs =>
Mappings as bs cs
-> Field (('Kon k ':@: t1) ':@: t2) as
-> Field (('Kon k ':@: t1) ':@: t2) bs
-> Maybe (Field (('Kon k ':@: t1) ':@: t2) cs)
zipMatchFieldsWith Mappings as bs cs
g (Field Interpret (('Kon k ':@: t1) ':@: t2) as
l) (Field Interpret (('Kon k ':@: t1) ':@: t2) bs
r) =
    k (Interpret t1 cs) (Interpret t2 cs)
-> Field (('Kon k ':@: t1) ':@: t2) cs
Interpret (('Kon k ':@: t1) ':@: t2) cs
-> Field (('Kon k ':@: t1) ':@: t2) cs
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field (k (Interpret t1 cs) (Interpret t2 cs)
 -> Field (('Kon k ':@: t1) ':@: t2) cs)
-> Maybe (k (Interpret t1 cs) (Interpret t2 cs))
-> Maybe (Field (('Kon k ':@: t1) ':@: t2) cs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k (f :: k) (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
ZipMatchK f =>
Mappings as bs cs
-> (f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: cs)
zipMatchWithK @_ @k @(Interpret t1 as :&&: Interpret t2 as :&&: LoT0) @(Interpret t1 bs :&&: Interpret t2 bs :&&: LoT0) @(Interpret t1 cs :&&: Interpret t2 cs :&&: LoT0)
      ((\Interpret t1 as
ll Interpret t1 bs
rr -> forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
forall (t :: Atom d (*)) (x :: LoT d). Field t x -> Interpret t x
unField @t1 (Field t1 cs -> Interpret t1 cs)
-> Maybe (Field t1 cs) -> Maybe (Interpret t1 cs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mappings as bs cs
-> Field t1 as -> Field t1 bs -> Maybe (Field t1 cs)
forall d (t :: Atom d (*)) (as :: LoT d) (bs :: LoT d)
       (cs :: LoT d).
(ZipMatchFields t, ReqsZipMatchFieldsWith t as bs cs) =>
Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)
forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
ReqsZipMatchFieldsWith t1 as bs cs =>
Mappings as bs cs
-> Field t1 as -> Field t1 bs -> Maybe (Field t1 cs)
zipMatchFieldsWith Mappings as bs cs
g (Interpret t1 as -> Field t1 as
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Interpret t1 as
ll) (Interpret t1 bs -> Field t1 bs
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Interpret t1 bs
rr))
        (Interpret t1 as -> Interpret t1 bs -> Maybe (Interpret t1 cs))
-> Mappings
     (Interpret t2 as ':&&: 'LoT0)
     (Interpret t2 bs ':&&: 'LoT0)
     (Interpret t2 cs ':&&: 'LoT0)
-> Mappings
     (Interpret t1 as ':&&: (Interpret t2 as ':&&: 'LoT0))
     (Interpret t1 bs ':&&: (Interpret t2 bs ':&&: 'LoT0))
     (Interpret t1 cs ':&&: (Interpret t2 cs ':&&: 'LoT0))
forall {k1} a b c (as1 :: LoT k1) (bs1 :: LoT k1) (cs1 :: LoT k1).
(a -> b -> Maybe c)
-> Mappings as1 bs1 cs1
-> Mappings (a ':&&: as1) (b ':&&: bs1) (c ':&&: cs1)
:^: ((\Interpret t2 as
ll Interpret t2 bs
rr -> forall {d} (t :: Atom d (*)) (x :: LoT d).
Field t x -> Interpret t x
forall (t :: Atom d (*)) (x :: LoT d). Field t x -> Interpret t x
unField @t2 (Field t2 cs -> Interpret t2 cs)
-> Maybe (Field t2 cs) -> Maybe (Interpret t2 cs)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Mappings as bs cs
-> Field t2 as -> Field t2 bs -> Maybe (Field t2 cs)
forall d (t :: Atom d (*)) (as :: LoT d) (bs :: LoT d)
       (cs :: LoT d).
(ZipMatchFields t, ReqsZipMatchFieldsWith t as bs cs) =>
Mappings as bs cs -> Field t as -> Field t bs -> Maybe (Field t cs)
forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
ReqsZipMatchFieldsWith t2 as bs cs =>
Mappings as bs cs
-> Field t2 as -> Field t2 bs -> Maybe (Field t2 cs)
zipMatchFieldsWith Mappings as bs cs
g (Interpret t2 as -> Field t2 as
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Interpret t2 as
ll) (Interpret t2 bs -> Field t2 bs
forall {d} (t :: Atom d (*)) (x :: LoT d).
Interpret t x -> Field t x
Field Interpret t2 bs
rr))
        (Interpret t2 as -> Interpret t2 bs -> Maybe (Interpret t2 cs))
-> Mappings 'LoT0 'LoT0 'LoT0
-> Mappings
     (Interpret t2 as ':&&: 'LoT0)
     (Interpret t2 bs ':&&: 'LoT0)
     (Interpret t2 cs ':&&: 'LoT0)
forall {k1} a b c (as1 :: LoT k1) (bs1 :: LoT k1) (cs1 :: LoT k1).
(a -> b -> Maybe c)
-> Mappings as1 bs1 cs1
-> Mappings (a ':&&: as1) (b ':&&: bs1) (c ':&&: cs1)
:^: Mappings 'LoT0 'LoT0 'LoT0
M0)) k :@@: (Interpret t1 as ':&&: (Interpret t2 as ':&&: 'LoT0))
Interpret (('Kon k ':@: t1) ':@: t2) as
l k :@@: (Interpret t1 bs ':&&: (Interpret t2 bs ':&&: 'LoT0))
Interpret (('Kon k ':@: t1) ':@: t2) bs
r

instance {-# OVERLAPPABLE #-} TypeError
  ('Text "The type constructor is kind-polymorphic:"
  :$$: 'Text "  " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (kk -> Type)
  :$$: 'Text "Possible fix:"
  :$$: 'Text "  add an explicit kind signature"
  :$$: 'Text "    " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (Type -> Type))
  => ZipMatchFields (Kon (k :: kk -> Type) :@: t) where
  zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
ReqsZipMatchFieldsWith ('Kon k ':@: t) as bs cs =>
Mappings as bs cs
-> Field ('Kon k ':@: t) as
-> Field ('Kon k ':@: t) bs
-> Maybe (Field ('Kon k ':@: t) cs)
zipMatchFieldsWith = Mappings as bs cs
-> Field ('Kon k ':@: t) as
-> Field ('Kon k ':@: t) bs
-> Maybe (Field ('Kon k ':@: t) cs)
forall a. HasCallStack => a
undefined

instance {-# OVERLAPPABLE #-} TypeError
  ('Text "The type constructor is kind-polymorphic:"
  :$$: 'Text "  " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (kk1 -> kk2 -> Type)
  :$$: 'Text "Possible fix:"
  :$$: 'Text "  add an explicit kind signature"
  :$$: 'Text "    " :<>: 'ShowType k :<>: 'Text " : " :<>: 'ShowType (Type -> Type -> Type))
  => ZipMatchFields ((Kon (k :: kk1 -> kk2 -> Type) :@: t1) :@: t2) where
  zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
ReqsZipMatchFieldsWith (('Kon k ':@: t1) ':@: t2) as bs cs =>
Mappings as bs cs
-> Field (('Kon k ':@: t1) ':@: t2) as
-> Field (('Kon k ':@: t1) ':@: t2) bs
-> Maybe (Field (('Kon k ':@: t1) ':@: t2) cs)
zipMatchFieldsWith = Mappings as bs cs
-> Field (('Kon k ':@: t1) ':@: t2) as
-> Field (('Kon k ':@: t1) ':@: t2) bs
-> Maybe (Field (('Kon k ':@: t1) ':@: t2) cs)
forall a. HasCallStack => a
undefined

instance {-# OVERLAPPABLE #-} TypeError
  ('Text "Atom :@: is not supported by ZipMatchFields is a general form:"
  :$$: 'Text "  when attempting to use a generic instance for"
  :$$: 'ShowType (f :@: t)
  :$$: 'ShowType f :<>: 'Text " : " :<>: 'ShowType (Atom d (k1 -> Type)))
  => ZipMatchFields ((f :: Atom d (k1 -> Type)) :@: t) where
  -- type ReqsZipMatchFieldsWith (f :@: t) as bs cs = TypeError ('Text "Atom :@: is not supported by ZipMatchFields is a general form")
  zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
ReqsZipMatchFieldsWith (f ':@: t) as bs cs =>
Mappings as bs cs
-> Field (f ':@: t) as
-> Field (f ':@: t) bs
-> Maybe (Field (f ':@: t) cs)
zipMatchFieldsWith = Mappings as bs cs
-> Field (f ':@: t) as
-> Field (f ':@: t) bs
-> Maybe (Field (f ':@: t) cs)
forall a. HasCallStack => a
undefined

instance TypeError
  ('Text "Atom ForAll is not supported by ZipMatchFields"
  :$$: 'Text "  when attempting to use a generic instance for"
  :$$: 'ShowType (ForAll a)) => ZipMatchFields (ForAll a) where
  type ReqsZipMatchFieldsWith (ForAll a) as bs cs = TypeError ('Text "Atom ForAll is not supported by ZipMatchFields")
  zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
ReqsZipMatchFieldsWith ('ForAll a) as bs cs =>
Mappings as bs cs
-> Field ('ForAll a) as
-> Field ('ForAll a) bs
-> Maybe (Field ('ForAll a) cs)
zipMatchFieldsWith = Mappings as bs cs
-> Field ('ForAll a) as
-> Field ('ForAll a) bs
-> Maybe (Field ('ForAll a) cs)
forall a. HasCallStack => a
undefined
instance TypeError
  ('Text "Atom :=>>: is not supported by ZipMatchFields"
  :$$: 'Text "  when attempting to use a generic instance for"
  :$$: 'ShowType (c :=>>: a)) => ZipMatchFields (c :=>>: a) where
  type ReqsZipMatchFieldsWith (c :=>>: a) as bs cs = TypeError ('Text "Atom :=>>: is not supported by ZipMatchFields")
  zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
ReqsZipMatchFieldsWith (c ':=>>: a) as bs cs =>
Mappings as bs cs
-> Field (c ':=>>: a) as
-> Field (c ':=>>: a) bs
-> Maybe (Field (c ':=>>: a) cs)
zipMatchFieldsWith = Mappings as bs cs
-> Field (c ':=>>: a) as
-> Field (c ':=>>: a) bs
-> Maybe (Field (c ':=>>: a) cs)
forall a. HasCallStack => a
undefined
instance TypeError
  ('Text "Atom Eval is not supported by ZipMatchFields"
  :$$: 'Text "  when attempting to use a generic instance for"
  :$$: 'ShowType (Eval a)) => ZipMatchFields (Eval a) where
  type ReqsZipMatchFieldsWith (Eval a) as bs cs = TypeError ('Text "Atom Eval is not supported by ZipMatchFields")
  zipMatchFieldsWith :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
ReqsZipMatchFieldsWith ('Eval a) as bs cs =>
Mappings as bs cs
-> Field ('Eval a) as
-> Field ('Eval a) bs
-> Maybe (Field ('Eval a) cs)
zipMatchFieldsWith = Mappings as bs cs
-> Field ('Eval a) as
-> Field ('Eval a) bs
-> Maybe (Field ('Eval a) cs)
forall a. HasCallStack => a
undefined