{-# OPTIONS_GHC -Wno-missing-methods #-}
{-# 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 Control.Monad.Free.Foil.Generic where

import           Data.Kind              (Constraint, Type)
import           Generics.Kind
import           Generics.Kind.Examples ()
import           GHC.TypeError

type ZipLoT :: LoT k -> LoT k -> LoT k
type family ZipLoT as bs where
  ZipLoT LoT0 LoT0 = LoT0
  ZipLoT (a :&&: as) (b :&&: bs) = ((a, b) :&&: ZipLoT as bs)

type Mappings :: LoT k -> LoT k -> LoT k -> Type
data Mappings (as :: LoT k) (bs :: LoT k) (cs :: LoT k) where
  M0 :: Mappings LoT0 LoT0 LoT0
  (:^:) :: (a -> b -> Maybe c) -> Mappings as bs cs -> Mappings (a :&&: as) (b :&&: bs) (c :&&: cs)

class PairMappings (as :: LoT k) (bs :: LoT k) where
  pairMappings :: Mappings as bs (ZipLoT as bs)

instance PairMappings LoT0 LoT0 where
  pairMappings :: Mappings 'LoT0 'LoT0 (ZipLoT 'LoT0 'LoT0)
pairMappings = Mappings 'LoT0 'LoT0 'LoT0
Mappings 'LoT0 'LoT0 (ZipLoT 'LoT0 'LoT0)
M0

instance PairMappings as bs => PairMappings ((a :: Type) :&&: as) ((b :: Type) :&&: bs) where
  pairMappings :: Mappings
  (a ':&&: as) (b ':&&: bs) (ZipLoT (a ':&&: as) (b ':&&: bs))
pairMappings = (\a
x b
y -> (a, b) -> Maybe (a, b)
forall a. a -> Maybe a
Just (a
x, b
y)) (a -> b -> Maybe (a, b))
-> Mappings as bs (ZipLoT as bs)
-> Mappings (a ':&&: as) (b ':&&: bs) ((a, b) ':&&: ZipLoT as bs)
forall {k} a b c (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
(a -> b -> Maybe c)
-> Mappings as bs cs
-> Mappings (a ':&&: as) (b ':&&: bs) (c ':&&: cs)
:^: Mappings as bs (ZipLoT as bs)
forall k (as :: LoT k) (bs :: LoT k).
PairMappings as bs =>
Mappings as bs (ZipLoT as bs)
pairMappings

class ApplyMappings (v :: TyVar d Type) where
  applyMappings :: forall (as :: LoT d) (bs :: LoT d) (cs :: LoT d).
    Mappings as bs cs -> Interpret (Var v) as -> Interpret (Var v) bs -> Maybe (Interpret (Var v) cs)

instance ApplyMappings (VZ :: TyVar (Type -> tys) Type) where
  applyMappings :: forall (as :: LoT (* -> tys)) (bs :: LoT (* -> tys))
       (cs :: LoT (* -> tys)).
Mappings as bs cs
-> Interpret ('Var 'VZ) as
-> Interpret ('Var 'VZ) bs
-> Maybe (Interpret ('Var 'VZ) cs)
applyMappings (a -> b -> Maybe c
f :^: Mappings as bs cs
_) Interpret ('Var 'VZ) as
x Interpret ('Var 'VZ) bs
y = a -> b -> Maybe c
f a
Interpret ('Var 'VZ) as
x b
Interpret ('Var 'VZ) bs
y

instance ApplyMappings v => ApplyMappings (VS v :: TyVar (ty -> tys) Type) where
  applyMappings :: forall (as :: LoT (ty -> tys)) (bs :: LoT (ty -> tys))
       (cs :: LoT (ty -> tys)).
Mappings as bs cs
-> Interpret ('Var ('VS v)) as
-> Interpret ('Var ('VS v)) bs
-> Maybe (Interpret ('Var ('VS v)) cs)
applyMappings (a -> b -> Maybe c
_ :^: Mappings as bs cs
fs) Interpret ('Var ('VS v)) as
x Interpret ('Var ('VS v)) bs
y = 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
Mappings as bs cs
fs Interpret ('Var v) as
Interpret ('Var ('VS v)) as
x Interpret ('Var v) bs
Interpret ('Var ('VS v)) bs
y

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

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)

genericZipMatch2
   :: forall sig scope scope' term term'.
   (GenericK sig, GZipMatch (RepK sig), ReqsZipMatch (RepK sig) (scope :&&: term :&&: 'LoT0) (scope' :&&: term' :&&: 'LoT0))
   => sig scope term -> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
genericZipMatch2 :: forall (sig :: * -> * -> *) scope scope' term term'.
(GenericK sig, GZipMatch (RepK sig),
 ReqsZipMatch
   (RepK sig)
   (scope ':&&: (term ':&&: 'LoT0))
   (scope' ':&&: (term' ':&&: 'LoT0))) =>
sig scope term
-> sig scope' term' -> Maybe (sig (scope, scope') (term, term'))
genericZipMatch2 = 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)
forall (f :: * -> * -> *) (as :: LoT (* -> * -> *))
       (bs :: LoT (* -> * -> *)).
(GenericK f, GZipMatch (RepK f), ReqsZipMatch (RepK f) as bs,
 PairMappings as bs) =>
(f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: ZipLoT as bs)
genericZipMatchK @sig @(scope :&&: term :&&: 'LoT0) @(scope' :&&: term' :&&: 'LoT0)

zipMatchK :: forall f as bs. (ZipMatchK f, PairMappings as bs) => f :@@: as -> f :@@: bs -> Maybe (f :@@: ZipLoT as bs)
zipMatchK :: forall {k} (f :: k) (as :: LoT k) (bs :: LoT k).
(ZipMatchK f, PairMappings as bs) =>
(f :@@: as) -> (f :@@: bs) -> Maybe (f :@@: ZipLoT as bs)
zipMatchK = 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 @_ @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

class ZipMatchK (f :: k) where
  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

zipMatchViaEq :: Eq a => Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaEq :: forall {k} a (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
Eq a =>
Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaEq Mappings as bs cs
_ a
x a
y
  | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = a -> Maybe a
forall a. a -> Maybe a
Just a
x
  | Bool
otherwise = Maybe a
forall a. Maybe a
Nothing

zipMatchViaChooseLeft :: Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaChooseLeft :: forall {k} (as :: LoT k) (bs :: LoT k) (cs :: LoT k) a.
Mappings as bs cs -> a -> a -> Maybe a
zipMatchViaChooseLeft Mappings as bs cs
_ a
x a
_ = a -> Maybe a
forall a. a -> Maybe a
Just a
x

-- instance ZipMatchK (,)     -- missing GenericK instance upstream
instance ZipMatchK []
instance ZipMatchK Maybe
instance ZipMatchK Either
instance ZipMatchK a => ZipMatchK (Either a)

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 (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 :@: 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 {k} a b c (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
(a -> b -> Maybe c)
-> Mappings as bs cs
-> Mappings (a ':&&: as) (b ':&&: bs) (c ':&&: cs)
:^: 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 (ZipMatchFields t1, ZipMatchFields t2, ZipMatchK k) => ZipMatchFields ((Kon k :@: 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 {k} a b c (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
(a -> b -> Maybe c)
-> Mappings as bs cs
-> Mappings (a ':&&: as) (b ':&&: bs) (c ':&&: cs)
:^: ((\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 {k} a b c (as :: LoT k) (bs :: LoT k) (cs :: LoT k).
(a -> b -> Maybe c)
-> Mappings as bs cs
-> Mappings (a ':&&: as) (b ':&&: bs) (c ':&&: cs)
:^: 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 "Atom :@: is not supported by ZipMatchFields is a general form") => ZipMatchFields (f :@: 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") => 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") => 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") => 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

-- instance ZipMatchFields (ForAll f) where
--   type ReqsZipMatchFields (ForAll f) as bs = ???
--   zipMatchFields = ???

-- instance ZipMatchFields (c :=>>: f) where
--   type ReqsZipMatchFields (c :=>>: f) as bs = ???
--   zipMatchFields = ???

-- instance ZipMatchFields (Eval f) where
--   type ReqsZipMatchFields (Eval f) as bs = ???
--   zipMatchFields = ???