{-# Options_GHC -Wno-name-shadowing #-}

{-# Language AllowAmbiguousTypes        #-}
{-# Language CPP                        #-}
{-# Language ConstraintKinds            #-}
{-# Language DataKinds                  #-}
{-# Language DefaultSignatures          #-}
{-# Language DerivingStrategies         #-}
{-# Language EmptyCase                  #-}
{-# Language FlexibleContexts           #-}
{-# Language FlexibleInstances          #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language InstanceSigs               #-}
{-# Language LambdaCase                 #-}
{-# Language MultiParamTypeClasses      #-}
{-# Language PolyKinds                  #-}
{-# Language RankNTypes                 #-}
{-# Language ScopedTypeVariables        #-}
{-# Language StandaloneKindSignatures   #-}
{-# Language TypeApplications           #-}
{-# Language TypeFamilies               #-}
{-# Language TypeOperators              #-}
{-# Language UndecidableInstances       #-}

module Generic.Applicative.Internal where

import Control.Applicative
import Data.Coerce
import Data.Functor.Compose
import Data.Functor.Identity
import Data.Functor.Product
import Data.Functor.Sum
import Data.Kind
import Data.Proxy
import Data.Void
import GHC.Generics
import Unsafe.Coerce

#if MIN_VERSION_base(4,17,0)
#define HAS_GENERICALLY
#endif

type SumKind :: Type -> Type
type SumKind k = (k -> Type) -> (k -> Type) -> (k -> Type)

type (~>) :: (k -> Type) -> (k -> Type) -> Type
type f ~> g = forall x. f x -> g x

absurdZero :: Const Void a -> b
absurdZero :: Const Void a -> b
absurdZero (Const Void
void) = Void -> b
forall a. Void -> a
absurd Void
void

absurdV1 :: V1 a -> b
absurdV1 :: V1 a -> b
absurdV1 = V1 a -> b
\case

-- This is following a couple of requirements:
-- 
--  1. I want to use the more user-facing Data.Functor vocabulary
--     rather than GHC.Generics.
-- 
--  2. I want to get rid of nested functors
-- 
--       (Par1 :*: Par1) :*: (Par1 :*: Par1)
--     
--     intead I want
--
--       Product (Product Identity Identity) (Product Identity Identity)
-- 
--  3. I don't want to terminate the sums or products with @Const
--     Void@ or @Const ()@.
-- 
--  4. The sums should be replaced by a type-level list of sums, such
--     that the user can override its Applicative behaviour.
-- 
-- 'ConvSum' (1. and 2.) translates to Sum, Product and Compose and
-- flattens the representation, but this results in terminating
-- functors @Const Void@ and @Const ()@.
--
-- 'ConvBæSum' (3.) removes terminating @Const Void@ and @Const ()@.
-- 
-- @ReplaceSums [sum1, sum2, ..] rep1@ replaces the sums of a
-- representation @rep1@.
type  ConvSum :: (k -> Type) -> Constraint
class ConvSum (rep1 :: k -> Type) where
  type ToSum (rep1 :: k -> Type) (end :: k -> Type) :: k -> Type

  convToSum     :: Proxy end -> rep1 ~> ToSum rep1 end
  convToSumSkip :: end ~> ToSum rep1 end
  convFromSum :: ToSum rep1 end a -> (rep1 a -> res) -> (end a -> res) -> res

instance (ConvSum rep1, ConvSum rep1') => ConvSum (rep1 :+: rep1') where
  type ToSum (rep1 :+: rep1') end = ToSum rep1 (ToSum rep1' end)

  convToSum :: forall end. Proxy end -> (rep1 :+: rep1') ~> ToSum rep1 (ToSum rep1' end)
  convToSum :: Proxy end -> (rep1 :+: rep1') ~> ToSum rep1 (ToSum rep1' end)
convToSum Proxy end
end (L1 rep1 x
l1) = Proxy (ToSum rep1' end) -> rep1 x -> ToSum rep1 (ToSum rep1' end) x
forall k (rep1 :: k -> *) (end :: k -> *).
ConvSum rep1 =>
Proxy end -> rep1 ~> ToSum rep1 end
convToSum @_ @_ @(ToSum rep1' end) (Proxy end -> Proxy (ToSum rep1' end)
asToSum Proxy end
end) rep1 x
l1 where

    asToSum :: Proxy end -> Proxy (ToSum rep1' end)
    asToSum :: Proxy end -> Proxy (ToSum rep1' end)
asToSum = Proxy end -> Proxy (ToSum rep1' end)
forall a. Monoid a => a
mempty

  convToSum Proxy end
end (R1 rep1' x
r1) = ToSum rep1' end x -> ToSum rep1 (ToSum rep1' end) x
forall k (rep1 :: k -> *) (end :: k -> *).
ConvSum rep1 =>
end ~> ToSum rep1 end
convToSumSkip @_ @rep1 @(ToSum rep1' end) 
    (Proxy end -> rep1' x -> ToSum rep1' end x
forall k (rep1 :: k -> *) (end :: k -> *).
ConvSum rep1 =>
Proxy end -> rep1 ~> ToSum rep1 end
convToSum Proxy end
end rep1' x
r1)

  convToSumSkip :: end ~> ToSum rep1 (ToSum rep1' end)
  convToSumSkip :: end x -> ToSum rep1 (ToSum rep1' end) x
convToSumSkip end x
end = ToSum rep1' end x -> ToSum rep1 (ToSum rep1' end) x
forall k (rep1 :: k -> *) (end :: k -> *).
ConvSum rep1 =>
end ~> ToSum rep1 end
convToSumSkip @_ @rep1
    (end x -> ToSum rep1' end x
forall k (rep1 :: k -> *) (end :: k -> *).
ConvSum rep1 =>
end ~> ToSum rep1 end
convToSumSkip @_ @rep1' end x
end)

  convFromSum :: forall end res a. ToSum rep1 (ToSum rep1' end) a -> ((rep1 :+: rep1') a -> res) -> (end a -> res) -> res
  convFromSum :: ToSum rep1 (ToSum rep1' end) a
-> ((:+:) rep1 rep1' a -> res) -> (end a -> res) -> res
convFromSum ToSum rep1 (ToSum rep1' end) a
sum (:+:) rep1 rep1' a -> res
fromSum end a -> res
fromEnd = 
    ToSum rep1 (ToSum rep1' end) a
-> (rep1 a -> res) -> (ToSum rep1' end a -> res) -> res
forall k (rep1 :: k -> *) (end :: k -> *) (a :: k) res.
ConvSum rep1 =>
ToSum rep1 end a -> (rep1 a -> res) -> (end a -> res) -> res
convFromSum ToSum rep1 (ToSum rep1' end) a
sum ((:+:) rep1 rep1' a -> res
fromSum ((:+:) rep1 rep1' a -> res)
-> (rep1 a -> (:+:) rep1 rep1' a) -> rep1 a -> res
forall b c a. (b -> c) -> (a -> b) -> a -> c
. rep1 a -> (:+:) rep1 rep1' a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1) ((ToSum rep1' end a -> res) -> res)
-> (ToSum rep1' end a -> res) -> res
forall a b. (a -> b) -> a -> b
$ \ToSum rep1' end a
sum' -> 
      ToSum rep1' end a -> (rep1' a -> res) -> (end a -> res) -> res
forall k (rep1 :: k -> *) (end :: k -> *) (a :: k) res.
ConvSum rep1 =>
ToSum rep1 end a -> (rep1 a -> res) -> (end a -> res) -> res
convFromSum ToSum rep1' end a
sum' ((:+:) rep1 rep1' a -> res
fromSum ((:+:) rep1 rep1' a -> res)
-> (rep1' a -> (:+:) rep1 rep1' a) -> rep1' a -> res
forall b c a. (b -> c) -> (a -> b) -> a -> c
. rep1' a -> (:+:) rep1 rep1' a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1) end a -> res
fromEnd

instance ConvSum V1 where
  type ToSum V1 end = end

  convToSum :: Proxy end -> V1 ~> end
  convToSum :: Proxy end -> V1 ~> end
convToSum Proxy end
_ = V1 x -> end x
forall k (a :: k) b. V1 a -> b
absurdV1

  convToSumSkip :: end ~> end
  convToSumSkip :: end x -> end x
convToSumSkip = end x -> end x
forall a. a -> a
id

  convFromSum :: end a -> (rep1 a -> res) -> (end a -> res) -> res
  convFromSum :: end a -> (rep1 a -> res) -> (end a -> res) -> res
convFromSum end a
end rep1 a -> res
_ end a -> res
fromEnd = end a -> res
fromEnd end a
end

instance ConvSum rep1 => ConvSum (D1 meta rep1) where
  type ToSum (D1 meta rep1) end = ToSum rep1 end

  convToSum :: Proxy end -> D1 meta rep1 ~> ToSum rep1 end
  convToSum :: Proxy end -> D1 meta rep1 ~> ToSum rep1 end
convToSum Proxy end
end (M1 rep1 x
d1) = Proxy end -> rep1 x -> ToSum rep1 end x
forall k (rep1 :: k -> *) (end :: k -> *).
ConvSum rep1 =>
Proxy end -> rep1 ~> ToSum rep1 end
convToSum Proxy end
end rep1 x
d1

  convToSumSkip :: end ~> ToSum rep1 end
  convToSumSkip :: end x -> ToSum rep1 end x
convToSumSkip = forall (end :: k -> *). ConvSum rep1 => end ~> ToSum rep1 end
forall k (rep1 :: k -> *) (end :: k -> *).
ConvSum rep1 =>
end ~> ToSum rep1 end
convToSumSkip @_ @rep1 

  convFromSum :: ToSum rep1 end a -> (D1 meta rep1 a -> res) -> (end a -> res) -> res
  convFromSum :: ToSum rep1 end a
-> (D1 meta rep1 a -> res) -> (end a -> res) -> res
convFromSum ToSum rep1 end a
sum D1 meta rep1 a -> res
fromD1 = ToSum rep1 end a -> (rep1 a -> res) -> (end a -> res) -> res
forall k (rep1 :: k -> *) (end :: k -> *) (a :: k) res.
ConvSum rep1 =>
ToSum rep1 end a -> (rep1 a -> res) -> (end a -> res) -> res
convFromSum ToSum rep1 end a
sum (D1 meta rep1 a -> res
fromD1 (D1 meta rep1 a -> res)
-> (rep1 a -> D1 meta rep1 a) -> rep1 a -> res
forall b c a. (b -> c) -> (a -> b) -> a -> c
. rep1 a -> D1 meta rep1 a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1)

instance ConvProduct rep1 => ConvSum (C1 meta rep1) where
  type ToSum (C1 meta rep1) end = Sum (ToProduct rep1 (Const ())) end

  convToSum :: forall end. Proxy end -> C1 meta rep1 ~> Sum (ToProduct rep1 (Const ())) end
  convToSum :: Proxy end -> C1 meta rep1 ~> Sum (ToProduct rep1 (Const ())) end
convToSum Proxy end
Proxy (M1 rep1 x
c1) = ToProduct rep1 (Const ()) x
-> Sum (ToProduct rep1 (Const ())) end x
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL 
    (rep1 x -> Const () x -> ToProduct rep1 (Const ()) x
forall k (rep1 :: k -> *) (a :: k) (end :: k -> *).
ConvProduct rep1 =>
rep1 a -> end a -> ToProduct rep1 end a
convToProduct @_ @rep1 rep1 x
c1 (() -> Const () x
forall k a (b :: k). a -> Const a b
Const ()))

  convToSumSkip :: end ~> Sum (ToProduct rep1 (Const ())) end
  convToSumSkip :: end x -> Sum (ToProduct rep1 (Const ())) end x
convToSumSkip = end x -> Sum (ToProduct rep1 (Const ())) end x
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR

  convFromSum :: Sum (ToProduct rep1 (Const ())) end a -> (C1 meta rep1 a -> res) -> (end a -> res) -> res
  convFromSum :: Sum (ToProduct rep1 (Const ())) end a
-> (C1 meta rep1 a -> res) -> (end a -> res) -> res
convFromSum (InL ToProduct rep1 (Const ()) a
prod) C1 meta rep1 a -> res
fromC1 end a -> res
_       = ToProduct rep1 (Const ()) a -> (rep1 a -> Const () a -> res) -> res
forall k (rep1 :: k -> *) (end :: k -> *) (a :: k) res.
ConvProduct rep1 =>
ToProduct rep1 end a -> (rep1 a -> end a -> res) -> res
convFromProduct @_ @rep1 @(Const ()) ToProduct rep1 (Const ()) a
prod ((rep1 a -> Const () a -> res) -> res)
-> (rep1 a -> Const () a -> res) -> res
forall a b. (a -> b) -> a -> b
$ \rep1 a
r Const () a
_ -> C1 meta rep1 a -> res
fromC1 (rep1 a -> C1 meta rep1 a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 rep1 a
r)
  convFromSum (InR end a
end)  C1 meta rep1 a -> res
_      end a -> res
fromEnd = end a -> res
fromEnd end a
end

-- ×

type ConvProduct :: (k -> Type) -> Constraint

class ConvProduct (rep1 :: k -> Type) where
  type ToProduct (rep1 :: k -> Type) (end :: k -> Type) :: k -> Type 

  convToProduct :: rep1 a -> end a -> ToProduct rep1 end a

  convFromProduct :: ToProduct rep1 end a -> (rep1 a -> end a -> res) -> res

instance (ConvProduct rep1, ConvProduct rep1') => ConvProduct (rep1 :*: rep1') where
  type ToProduct (rep1 :*: rep1') end = ToProduct rep1 (ToProduct rep1' end)

  convToProduct :: (rep1 :*: rep1') a -> end a -> ToProduct rep1 (ToProduct rep1' end) a
  convToProduct :: (:*:) rep1 rep1' a
-> end a -> ToProduct rep1 (ToProduct rep1' end) a
convToProduct (rep1 a
r :*: rep1' a
r') end a
end = rep1 a
-> ToProduct rep1' end a -> ToProduct rep1 (ToProduct rep1' end) a
forall k (rep1 :: k -> *) (a :: k) (end :: k -> *).
ConvProduct rep1 =>
rep1 a -> end a -> ToProduct rep1 end a
convToProduct rep1 a
r (rep1' a -> end a -> ToProduct rep1' end a
forall k (rep1 :: k -> *) (a :: k) (end :: k -> *).
ConvProduct rep1 =>
rep1 a -> end a -> ToProduct rep1 end a
convToProduct rep1' a
r' end a
end)

  convFromProduct :: ToProduct rep1 (ToProduct rep1' end) a
                  -> ((rep1 :*: rep1') a -> end a -> res) -> res
  convFromProduct :: ToProduct rep1 (ToProduct rep1' end) a
-> ((:*:) rep1 rep1' a -> end a -> res) -> res
convFromProduct ToProduct rep1 (ToProduct rep1' end) a
prod (:*:) rep1 rep1' a -> end a -> res
next = 
    ToProduct rep1 (ToProduct rep1' end) a
-> (rep1 a -> ToProduct rep1' end a -> res) -> res
forall k (rep1 :: k -> *) (end :: k -> *) (a :: k) res.
ConvProduct rep1 =>
ToProduct rep1 end a -> (rep1 a -> end a -> res) -> res
convFromProduct ToProduct rep1 (ToProduct rep1' end) a
prod ((rep1 a -> ToProduct rep1' end a -> res) -> res)
-> (rep1 a -> ToProduct rep1' end a -> res) -> res
forall a b. (a -> b) -> a -> b
$ \rep1 a
r ToProduct rep1' end a
end -> 
      ToProduct rep1' end a -> (rep1' a -> end a -> res) -> res
forall k (rep1 :: k -> *) (end :: k -> *) (a :: k) res.
ConvProduct rep1 =>
ToProduct rep1 end a -> (rep1 a -> end a -> res) -> res
convFromProduct ToProduct rep1' end a
end ((rep1' a -> end a -> res) -> res)
-> (rep1' a -> end a -> res) -> res
forall a b. (a -> b) -> a -> b
$ \rep1' a
r' end a
end' -> 
        (:*:) rep1 rep1' a -> end a -> res
next (rep1 a
r rep1 a -> rep1' a -> (:*:) rep1 rep1' a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: rep1' a
r') end a
end'

instance ConvProduct U1 where
  type ToProduct U1 end = end

  convToProduct :: U1 a -> end a -> end a
  convToProduct :: U1 a -> end a -> end a
convToProduct U1 a
U1 = end a -> end a
forall a. a -> a
id

  convFromProduct :: end a -> (U1 a -> end a -> res) -> res
  convFromProduct :: end a -> (U1 a -> end a -> res) -> res
convFromProduct end a
end U1 a -> end a -> res
fromU1 = U1 a -> end a -> res
fromU1 U1 a
forall k (p :: k). U1 p
U1 end a
end

instance ConvField rep1 => ConvProduct (S1 meta rep1) where
  type ToProduct (S1 meta rep1) end = Product (ToField rep1) end

  convToProduct :: S1 meta rep1 a -> end a -> Product (ToField rep1) end a
  convToProduct :: S1 meta rep1 a -> end a -> Product (ToField rep1) end a
convToProduct (M1 rep1 a
s1) end a
end = ToField rep1 a -> end a -> Product (ToField rep1) end a
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (rep1 a -> ToField rep1 a
forall k (rep1 :: k -> *). ConvField rep1 => rep1 ~> ToField rep1
convToField rep1 a
s1) end a
end

  convFromProduct :: Product (ToField rep1) end a -> (S1 meta rep1 a -> end a -> res) -> res
  convFromProduct :: Product (ToField rep1) end a
-> (S1 meta rep1 a -> end a -> res) -> res
convFromProduct (Pair ToField rep1 a
field end a
end) S1 meta rep1 a -> end a -> res
next = 
    S1 meta rep1 a -> end a -> res
next (rep1 a -> S1 meta rep1 a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (ToField rep1 a -> rep1 a
forall k (rep1 :: k -> *). ConvField rep1 => ToField rep1 ~> rep1
convFromField ToField rep1 a
field)) end a
end

type  ConvField :: (k -> Type) -> Constraint
class ConvField (rep1 :: k -> Type) where
  type ToField (rep1 :: k -> Type) :: (k -> Type)
  convToField :: rep1 ~> ToField rep1
  default
    convToField :: Coercible (rep1 a) (ToField rep1 a) => rep1 a -> ToField rep1 a
  convToField = rep1 a -> ToField rep1 a
coerce

  convFromField :: ToField rep1 ~> rep1
  default
    convFromField :: Coercible (ToField rep1 a) (rep1 a) => ToField rep1 a -> rep1 a
  convFromField = ToField rep1 a -> rep1 a
coerce

instance ConvField (K1 tag a) where
  type ToField (K1 tag a) = Const a

instance ConvField (Rec1 f) where
  type ToField (Rec1 f) = f

instance ConvField Par1 where
  type ToField Par1 = Identity

instance (Functor rep1, ConvField rep1') => ConvField (rep1 :.: rep1') where
  type ToField (rep1 :.: rep1') = Compose rep1 (ToField rep1')

  convToField :: (rep1 :.: rep1') ~> Compose rep1 (ToField rep1')
  convToField :: (:.:) rep1 rep1' x -> Compose rep1 (ToField rep1') x
convToField (Comp1 rep1 (rep1' x)
rs) = rep1 (ToField rep1' x) -> Compose rep1 (ToField rep1') x
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (rep1' x -> ToField rep1' x
forall k (rep1 :: k -> *). ConvField rep1 => rep1 ~> ToField rep1
convToField (rep1' x -> ToField rep1' x)
-> rep1 (rep1' x) -> rep1 (ToField rep1' x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> rep1 (rep1' x)
rs)

  convFromField :: Compose rep1 (ToField rep1') ~> (rep1 :.: rep1')
  convFromField :: Compose rep1 (ToField rep1') x -> (:.:) rep1 rep1' x
convFromField (Compose rep1 (ToField rep1' x)
rs) = rep1 (rep1' x) -> (:.:) rep1 rep1' x
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (ToField rep1' x -> rep1' x
forall k (rep1 :: k -> *). ConvField rep1 => ToField rep1 ~> rep1
convFromField (ToField rep1' x -> rep1' x)
-> rep1 (ToField rep1' x) -> rep1 (rep1' x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> rep1 (ToField rep1' x)
rs)

-- Bæ +
type SumTag :: Type
data SumTag = RightZero | NormalSum | NotSum

type
  CheckSum :: (k -> Type) -> SumTag
type family
  CheckSum rep1 where
  CheckSum (Sum rep1 (Const Void)) = 'RightZero
  CheckSum (Sum rep1 rep')         = 'NormalSum
  CheckSum rep                     = 'NotSum

type BæSum :: (k -> Type) -> (k -> Type)
type BæSum rep1 = BæSum_ (CheckSum rep1) rep1

type ConvBæSum :: (k -> Type) -> Constraint
type ConvBæSum rep1 = ConvBæSum_ (CheckSum rep1) rep1

type
  ConvBæSum_ :: SumTag -> (k -> Type) -> Constraint
class CheckSum rep1 ~ tag
   => ConvBæSum_ tag (rep1 :: k -> Type) where
  type BæSum_ tag (rep1 :: k -> Type) :: k -> Type
  convBæSum :: rep1 ~> BæSum rep1
  convHæSum :: BæSum rep1 ~> rep1

instance (ConvBæProduct rep1, CheckSum (Sum rep1 (Const Void)) ~ 'RightZero, void ~ Void) => ConvBæSum_ 'RightZero (Sum rep1 (Const void)) where
  type BæSum_ 'RightZero (Sum rep1 (Const void)) = BæProduct rep1
  convBæSum :: Sum rep1 (Const Void) ~> BæProduct rep1
  convBæSum :: Sum rep1 (Const Void) x -> BæProduct rep1 x
convBæSum = \case
    InL rep1 x
r  -> rep1 x -> BæProduct rep1 x
forall k (tag :: ProductTag) (rep1 :: k -> *).
ConvBæProduct_ tag rep1 =>
rep1 ~> BæProduct rep1
convBæProduct rep1 x
r
    InR Const Void x
v1 -> Const Void x -> BæProduct rep1 x
forall k (a :: k) b. Const Void a -> b
absurdZero Const Void x
v1

  convHæSum :: BæProduct rep1 ~> Sum rep1 (Const Void)
  convHæSum :: BæProduct rep1 x -> Sum rep1 (Const Void) x
convHæSum BæProduct rep1 x
bæProd = rep1 x -> Sum rep1 (Const Void) x
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (BæProduct rep1 x -> rep1 x
forall k (tag :: ProductTag) (rep1 :: k -> *).
ConvBæProduct_ tag rep1 =>
BæProduct rep1 ~> rep1
convHæProduct BæProduct rep1 x
bæProd)

instance ( CheckSum (Sum rep1 rep1') ~ 'NormalSum
         , ConvBæProduct rep1 
         , ConvBæSum rep1' )
      => ConvBæSum_ 'NormalSum (Sum rep1 rep1') where
  type BæSum_ 'NormalSum (Sum rep1 rep1') = Sum (BæProduct rep1) (BæSum rep1')
  convBæSum :: Sum rep1 rep1' ~> Sum (BæProduct rep1) (BæSum rep1')
  convBæSum :: Sum rep1 rep1' x -> Sum (BæProduct rep1) (BæSum rep1') x
convBæSum = \case
   InL rep1 x
r  -> BæProduct_ (CheckProduct rep1) rep1 x
-> Sum (BæProduct rep1) (BæSum rep1') x
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (rep1 x -> BæProduct_ (CheckProduct rep1) rep1 x
forall k (tag :: ProductTag) (rep1 :: k -> *).
ConvBæProduct_ tag rep1 =>
rep1 ~> BæProduct rep1
convBæProduct rep1 x
r)
   InR rep1' x
r' -> BæSum_ (CheckSum rep1') rep1' x
-> Sum (BæProduct rep1) (BæSum rep1') x
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR (rep1' x -> BæSum_ (CheckSum rep1') rep1' x
forall k (tag :: SumTag) (rep1 :: k -> *).
ConvBæSum_ tag rep1 =>
rep1 ~> BæSum rep1
convBæSum rep1' x
r')

  convHæSum :: Sum (BæProduct rep1) (BæSum rep1') ~> Sum rep1 rep1'
  convHæSum :: Sum (BæProduct rep1) (BæSum rep1') x -> Sum rep1 rep1' x
convHæSum (InL BæProduct rep1 x
bæProd) = rep1 x -> Sum rep1 rep1' x
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (BæProduct rep1 x -> rep1 x
forall k (tag :: ProductTag) (rep1 :: k -> *).
ConvBæProduct_ tag rep1 =>
BæProduct rep1 ~> rep1
convHæProduct BæProduct rep1 x
bæProd)
  convHæSum (InR BæSum rep1' x
bæSum)  = rep1' x -> Sum rep1 rep1' x
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR (BæSum rep1' x -> rep1' x
forall k (tag :: SumTag) (rep1 :: k -> *).
ConvBæSum_ tag rep1 =>
BæSum rep1 ~> rep1
convHæSum BæSum rep1' x
bæSum)

instance CheckSum rep1 ~ 'NotSum
      => ConvBæSum_ 'NotSum rep1 where
  type BæSum_ 'NotSum rep1 = rep1
  convBæSum :: rep1 ~> rep1
  convHæSum :: rep1 ~> rep1
  convBæSum :: rep1 x -> rep1 x
convBæSum = rep1 x -> rep1 x
forall a. a -> a
id
  convHæSum :: rep1 x -> rep1 x
convHæSum = rep1 x -> rep1 x
forall a. a -> a
id

-- Bæ ×

type ProductTag :: Type
data ProductTag = RightOne | NormalProduct | NotProduct

type
  CheckProduct :: (k -> Type) -> ProductTag
type family
  CheckProduct rep1 where
  CheckProduct (Product rep1 (Const ())) = 'RightOne
  CheckProduct (Product rep1 rep')       = 'NormalProduct
  CheckProduct rep                       = 'NotProduct

type BæProduct :: (k -> Type) -> (k -> Type)
type BæProduct rep1 = BæProduct_ (CheckProduct rep1) rep1

type ConvBæProduct :: (k -> Type) -> Constraint
type ConvBæProduct rep1 = ConvBæProduct_ (CheckProduct rep1) rep1

type ConvBæProduct_ :: ProductTag -> (k -> Type) -> Constraint

class tag ~ CheckProduct rep1
   => ConvBæProduct_ tag (rep1 :: k -> Type) where
  type BæProduct_ tag (rep1 :: k -> Type) :: k -> Type
  convBæProduct :: rep1 ~> BæProduct rep1
  convHæProduct :: BæProduct rep1 ~> rep1

instance unit ~ () => ConvBæProduct_ 'RightOne (Product rep1 (Const unit)) where 
  type BæProduct_ 'RightOne (Product rep1 (Const unit)) = rep1

  convBæProduct :: Product rep1 (Const ()) ~> rep1
  convBæProduct :: Product rep1 (Const ()) x -> rep1 x
convBæProduct (Pair rep1 x
r (Const ())) = rep1 x
r

  convHæProduct :: rep1 ~> Product rep1 (Const ())
  convHæProduct :: rep1 x -> Product rep1 (Const ()) x
convHæProduct rep1 x
r = rep1 x -> Const () x -> Product rep1 (Const ()) x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair rep1 x
r (() -> Const () x
forall k a (b :: k). a -> Const a b
Const ())

instance ( CheckProduct (Product rep1 rep1') ~ 'NormalProduct
         , ConvBæProduct rep1'
         )
      => ConvBæProduct_ 'NormalProduct (Product rep1 rep1') where 
  type BæProduct_ 'NormalProduct (Product rep1 rep1') = Product rep1 (BæProduct rep1')
  convBæProduct :: Product rep1 rep1' ~> Product rep1 (BæProduct rep1')
  convBæProduct :: Product rep1 rep1' x -> Product rep1 (BæProduct rep1') x
convBæProduct (Pair rep1 x
r rep1' x
r') = rep1 x
-> BæProduct_ (CheckProduct rep1') rep1' x
-> Product rep1 (BæProduct rep1') x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair rep1 x
r (rep1' x -> BæProduct_ (CheckProduct rep1') rep1' x
forall k (tag :: ProductTag) (rep1 :: k -> *).
ConvBæProduct_ tag rep1 =>
rep1 ~> BæProduct rep1
convBæProduct rep1' x
r')

  convHæProduct :: Product rep1 (BæProduct rep1') ~> Product rep1 rep1'
  convHæProduct :: Product rep1 (BæProduct rep1') x -> Product rep1 rep1' x
convHæProduct (Pair rep1 x
r BæProduct rep1' x
bæProd) = rep1 x -> rep1' x -> Product rep1 rep1' x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair rep1 x
r (BæProduct rep1' x -> rep1' x
forall k (tag :: ProductTag) (rep1 :: k -> *).
ConvBæProduct_ tag rep1 =>
BæProduct rep1 ~> rep1
convHæProduct BæProduct rep1' x
bæProd)

instance CheckProduct rep1 ~ 'NotProduct
      => ConvBæProduct_ 'NotProduct rep1 where
  type BæProduct_ 'NotProduct rep1 = rep1

  convHæProduct :: rep1 ~> rep1
  convBæProduct :: rep1 ~> rep1
  convHæProduct :: rep1 x -> rep1 x
convHæProduct = rep1 x -> rep1 x
forall a. a -> a
id
  convBæProduct :: rep1 x -> rep1 x
convBæProduct = rep1 x -> rep1 x
forall a. a -> a
id

type Flatten :: (k -> Type) -> (k -> Type)
type Flatten rep1 = ToSum rep1 (Const Void)

flatten :: ConvSum rep1 => rep1 ~> Flatten rep1
flatten :: rep1 ~> Flatten rep1
flatten = Proxy (Const Void) -> rep1 ~> Flatten rep1
forall k (rep1 :: k -> *) (end :: k -> *).
ConvSum rep1 =>
Proxy end -> rep1 ~> ToSum rep1 end
convToSum (Proxy (Const Void)
forall k (t :: k). Proxy t
Proxy @(Const Void))

nest :: ConvSum rep1 => Flatten rep1 a -> rep1 a
nest :: Flatten rep1 a -> rep1 a
nest Flatten rep1 a
flat = Flatten rep1 a
-> (rep1 a -> rep1 a) -> (Const Void a -> rep1 a) -> rep1 a
forall k (rep1 :: k -> *) (end :: k -> *) (a :: k) res.
ConvSum rep1 =>
ToSum rep1 end a -> (rep1 a -> res) -> (end a -> res) -> res
convFromSum Flatten rep1 a
flat rep1 a -> rep1 a
forall a. a -> a
id Const Void a -> rep1 a
forall k (a :: k) b. Const Void a -> b
absurdZero

-- NewSums
type
  ReplaceSums :: [SumKind k] -> (k -> Type) -> (k -> Type)
type family
  ReplaceSums sums rep1 where
  ReplaceSums (sum:sums) (Sum rep1 rep1') = rep1 `sum` ReplaceSums sums rep1'
  ReplaceSums '[]        rep1             = rep1

replaceSums :: forall sums rep1. rep1 ~> ReplaceSums sums rep1
replaceSums :: rep1 x -> ReplaceSums sums rep1 x
replaceSums = rep1 x -> ReplaceSums sums rep1 x
forall a b. a -> b
unsafeCoerce

placeSums :: forall sums rep1. ReplaceSums sums rep1 ~> rep1 
placeSums :: ReplaceSums sums rep1 x -> rep1 x
placeSums = ReplaceSums sums rep1 x -> rep1 x
forall a b. a -> b
unsafeCoerce

type    NewSums :: [SumKind k] -> (k -> Type) -> (k -> Type)
newtype NewSums sums f a = NewSums { NewSums sums f a -> f a
reduce :: f a }

instance (Generic1 f, ConvBæSum_ (CheckSum (ToSum (Rep1 f) (Const Void))) (ToSum (Rep1 f) (Const Void)), ConvSum (Rep1 f)) => Generic1 @k (NewSums @k sums f) where
  type Rep1 (NewSums sums f) = ReplaceSums sums (BæSum_ (CheckSum (ToSum (Rep1 f) (Const Void))) (ToSum (Rep1 f) (Const Void)))

  from1 :: NewSums sums f ~> ReplaceSums sums (BæSum_ (CheckSum (ToSum (Rep1 f) (Const Void))) (ToSum (Rep1 f) (Const Void)))
  from1 :: NewSums sums f x
-> ReplaceSums
     sums
     (BæSum_
        (CheckSum (ToSum (Rep1 f) (Const Void)))
        (ToSum (Rep1 f) (Const Void)))
     x
from1 = forall k (sums :: [SumKind k]) (rep1 :: k -> *).
rep1 ~> ReplaceSums sums rep1
forall (rep1 :: k -> *). rep1 ~> ReplaceSums sums rep1
replaceSums @sums (BæSum_
   (CheckSum (ToSum (Rep1 f) (Const Void)))
   (ToSum (Rep1 f) (Const Void))
   x
 -> ReplaceSums
      sums
      (BæSum_
         (CheckSum (ToSum (Rep1 f) (Const Void)))
         (ToSum (Rep1 f) (Const Void)))
      x)
-> (NewSums sums f x
    -> BæSum_
         (CheckSum (ToSum (Rep1 f) (Const Void)))
         (ToSum (Rep1 f) (Const Void))
         x)
-> NewSums sums f x
-> ReplaceSums
     sums
     (BæSum_
        (CheckSum (ToSum (Rep1 f) (Const Void)))
        (ToSum (Rep1 f) (Const Void)))
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ToSum (Rep1 f) (Const Void) x
-> BæSum_
     (CheckSum (ToSum (Rep1 f) (Const Void)))
     (ToSum (Rep1 f) (Const Void))
     x
forall k (tag :: SumTag) (rep1 :: k -> *).
ConvBæSum_ tag rep1 =>
rep1 ~> BæSum rep1
convBæSum (ToSum (Rep1 f) (Const Void) x
 -> BæSum_
      (CheckSum (ToSum (Rep1 f) (Const Void)))
      (ToSum (Rep1 f) (Const Void))
      x)
-> (NewSums sums f x -> ToSum (Rep1 f) (Const Void) x)
-> NewSums sums f x
-> BæSum_
     (CheckSum (ToSum (Rep1 f) (Const Void)))
     (ToSum (Rep1 f) (Const Void))
     x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep1 f x -> ToSum (Rep1 f) (Const Void) x
forall k (rep1 :: k -> *). ConvSum rep1 => rep1 ~> Flatten rep1
flatten (Rep1 f x -> ToSum (Rep1 f) (Const Void) x)
-> (NewSums sums f x -> Rep1 f x)
-> NewSums sums f x
-> ToSum (Rep1 f) (Const Void) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> Rep1 f x
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 (f x -> Rep1 f x)
-> (NewSums sums f x -> f x) -> NewSums sums f x -> Rep1 f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewSums sums f x -> f x
forall k (sums :: [SumKind k]) (f :: k -> *) (a :: k).
NewSums sums f a -> f a
reduce

  to1 :: ReplaceSums sums (BæSum_ (CheckSum (ToSum (Rep1 f) (Const Void))) (ToSum (Rep1 f) (Const Void))) ~> NewSums sums f 
  to1 :: ReplaceSums
  sums
  (BæSum_
     (CheckSum (ToSum (Rep1 f) (Const Void)))
     (ToSum (Rep1 f) (Const Void)))
  x
-> NewSums sums f x
to1 = f x -> NewSums sums f x
forall k (sums :: [SumKind k]) (f :: k -> *) (a :: k).
f a -> NewSums sums f a
NewSums (f x -> NewSums sums f x)
-> (ReplaceSums
      sums
      (BæSum_
         (CheckSum (ToSum (Rep1 f) (Const Void)))
         (ToSum (Rep1 f) (Const Void)))
      x
    -> f x)
-> ReplaceSums
     sums
     (BæSum_
        (CheckSum (ToSum (Rep1 f) (Const Void)))
        (ToSum (Rep1 f) (Const Void)))
     x
-> NewSums sums f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep1 f x -> f x
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (Rep1 f x -> f x)
-> (ReplaceSums
      sums
      (BæSum_
         (CheckSum (ToSum (Rep1 f) (Const Void)))
         (ToSum (Rep1 f) (Const Void)))
      x
    -> Rep1 f x)
-> ReplaceSums
     sums
     (BæSum_
        (CheckSum (ToSum (Rep1 f) (Const Void)))
        (ToSum (Rep1 f) (Const Void)))
     x
-> f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ToSum (Rep1 f) (Const Void) x -> Rep1 f x
forall k (rep1 :: k -> *) (a :: k).
ConvSum rep1 =>
Flatten rep1 a -> rep1 a
nest (ToSum (Rep1 f) (Const Void) x -> Rep1 f x)
-> (ReplaceSums
      sums
      (BæSum_
         (CheckSum (ToSum (Rep1 f) (Const Void)))
         (ToSum (Rep1 f) (Const Void)))
      x
    -> ToSum (Rep1 f) (Const Void) x)
-> ReplaceSums
     sums
     (BæSum_
        (CheckSum (ToSum (Rep1 f) (Const Void)))
        (ToSum (Rep1 f) (Const Void)))
     x
-> Rep1 f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BæSum_
  (CheckSum (ToSum (Rep1 f) (Const Void)))
  (ToSum (Rep1 f) (Const Void))
  x
-> ToSum (Rep1 f) (Const Void) x
forall k (tag :: SumTag) (rep1 :: k -> *).
ConvBæSum_ tag rep1 =>
BæSum rep1 ~> rep1
convHæSum (BæSum_
   (CheckSum (ToSum (Rep1 f) (Const Void)))
   (ToSum (Rep1 f) (Const Void))
   x
 -> ToSum (Rep1 f) (Const Void) x)
-> (ReplaceSums
      sums
      (BæSum_
         (CheckSum (ToSum (Rep1 f) (Const Void)))
         (ToSum (Rep1 f) (Const Void)))
      x
    -> BæSum_
         (CheckSum (ToSum (Rep1 f) (Const Void)))
         (ToSum (Rep1 f) (Const Void))
         x)
-> ReplaceSums
     sums
     (BæSum_
        (CheckSum (ToSum (Rep1 f) (Const Void)))
        (ToSum (Rep1 f) (Const Void)))
     x
-> ToSum (Rep1 f) (Const Void) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k (sums :: [SumKind k]) (rep1 :: k -> *).
ReplaceSums sums rep1 ~> rep1
forall (rep1 :: k -> *). ReplaceSums sums rep1 ~> rep1
placeSums @sums

#ifndef HAS_GENERICALLY
type    Generically1 :: forall k. (k -> Type) -> (k -> Type)
newtype Generically1 f a = Generically1 (f a)
  deriving newtype Rep1 (Generically1 f) a -> Generically1 f a
Generically1 f a -> Rep1 (Generically1 f) a
(forall (a :: k). Generically1 f a -> Rep1 (Generically1 f) a)
-> (forall (a :: k). Rep1 (Generically1 f) a -> Generically1 f a)
-> Generic1 (Generically1 f)
forall (a :: k). Rep1 (Generically1 f) a -> Generically1 f a
forall (a :: k). Generically1 f a -> Rep1 (Generically1 f) a
forall k (f :: k -> *) (a :: k).
Generic1 f =>
Rep1 (Generically1 f) a -> Generically1 f a
forall k (f :: k -> *) (a :: k).
Generic1 f =>
Generically1 f a -> Rep1 (Generically1 f) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
to1 :: Rep1 (Generically1 f) a -> Generically1 f a
$cto1 :: forall k (f :: k -> *) (a :: k).
Generic1 f =>
Rep1 (Generically1 f) a -> Generically1 f a
from1 :: Generically1 f a -> Rep1 (Generically1 f) a
$cfrom1 :: forall k (f :: k -> *) (a :: k).
Generic1 f =>
Generically1 f a -> Rep1 (Generically1 f) a
Generic1

instance (Generic1 f, Functor (Rep1 f)) => Functor (Generically1 f) where
  fmap :: (a -> a') -> (Generically1 f a -> Generically1 f a')
  fmap :: (a -> a') -> Generically1 f a -> Generically1 f a'
fmap a -> a'
f (Generically1 f a
as) = f a' -> Generically1 f a'
forall k (f :: k -> *) (a :: k). f a -> Generically1 f a
Generically1
    (Rep1 f a' -> f a'
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 ((a -> a') -> Rep1 f a -> Rep1 f a'
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a'
f (f a -> Rep1 f a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 f a
as)))

  (<$) :: a -> Generically1 f b -> Generically1 f a
  a
a <$ :: a -> Generically1 f b -> Generically1 f a
<$ Generically1 f b
as = f a -> Generically1 f a
forall k (f :: k -> *) (a :: k). f a -> Generically1 f a
Generically1
    (Rep1 f a -> f a
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (a
a a -> Rep1 f b -> Rep1 f a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ f b -> Rep1 f b
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 f b
as))

instance (Generic1 f, Applicative (Rep1 f)) => Applicative (Generically1 f) where
  pure :: a -> Generically1 f a
  pure :: a -> Generically1 f a
pure a
a = f a -> Generically1 f a
forall k (f :: k -> *) (a :: k). f a -> Generically1 f a
Generically1
    (Rep1 f a -> f a
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (a -> Rep1 f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a))

  (<*>) :: Generically1 f (a1 -> a2) -> Generically1 f a1 -> Generically1 f a2
  Generically1 f (a1 -> a2)
fs <*> :: Generically1 f (a1 -> a2) -> Generically1 f a1 -> Generically1 f a2
<*> Generically1 f a1
as = f a2 -> Generically1 f a2
forall k (f :: k -> *) (a :: k). f a -> Generically1 f a
Generically1
    (Rep1 f a2 -> f a2
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (f (a1 -> a2) -> Rep1 f (a1 -> a2)
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 f (a1 -> a2)
fs Rep1 f (a1 -> a2) -> Rep1 f a1 -> Rep1 f a2
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f a1 -> Rep1 f a1
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 f a1
as))

  liftA2 :: (a1 -> a2 -> a3)
         -> (Generically1 f a1 -> Generically1 f a2 -> Generically1 f a3)
  liftA2 :: (a1 -> a2 -> a3)
-> Generically1 f a1 -> Generically1 f a2 -> Generically1 f a3
liftA2 a1 -> a2 -> a3
(·) (Generically1 f a1
as) (Generically1 f a2
bs) = f a3 -> Generically1 f a3
forall k (f :: k -> *) (a :: k). f a -> Generically1 f a
Generically1
    (Rep1 f a3 -> f a3
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 ((a1 -> a2 -> a3) -> Rep1 f a1 -> Rep1 f a2 -> Rep1 f a3
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a1 -> a2 -> a3
(·) (f a1 -> Rep1 f a1
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 f a1
as) (f a2 -> Rep1 f a2
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 f a2
bs)))
#endif