content: {-# LANGUAGE AllowAmbiguousTypes #-}
  {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DefaultSignatures #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE InstanceSigs #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  module T15703_aux where
  
  import Data.Kind
  import Data.Type.Equality
  import GHC.Generics
  
  data family Sing :: forall k. k -> Type
  data instance Sing :: forall a b. (a, b) -> Type where
    STuple2 :: Sing x -> Sing y -> Sing '(x, y)
  
  data TyFun :: Type -> Type -> Type
  type a ~> b = TyFun a b -> Type
  infixr 0 ~>
  type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
  type f @@ x = f `Apply` x
  infixl 9 @@
  
  newtype instance Sing (f :: k1 ~> k2) =
    SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }
  
  type SingFunction1 f = forall t. Sing t -> Sing (f @@ t)
  singFun1 :: forall f. SingFunction1 f -> Sing f
  singFun1 f = SLambda f
  
  type SingFunction2 (f :: a1 ~> a2 ~> b) =
    forall t1 t2. Sing t1 -> Sing t2 -> Sing (f @@ t1 @@ t2)
  singFun2 :: forall f. SingFunction2 f -> Sing f
  singFun2 f = SLambda (\x -> singFun1 (f x))
  
  type SingFunction3 (f :: a1 ~> a2 ~> a3 ~> b) =
       forall t1 t2 t3.
       Sing t1 -> Sing t2 -> Sing t3
    -> Sing (f @@ t1 @@ t2 @@ t3)
  singFun3 :: forall f. SingFunction3 f -> Sing f
  singFun3 f = SLambda (\x -> singFun2 (f x))
  
  (@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
  (@@) f = applySing f
  
  type family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where
    (f :. g) x = f @@ (g @@ x)
  
  data (.@#@$) :: forall b c a. (b ~> c) ~> (a ~> b) ~> (a ~> c)
  type instance Apply (.@#@$) f = (.@#@$$) f
  data (.@#@$$) :: forall b c a. (b ~> c) -> (a ~> b) ~> (a ~> c)
  type instance Apply ((.@#@$$) f) g = f .@#@$$$ g
  data (.@#@$$$) :: forall b c a. (b ~> c) -> (a ~> b) -> (a ~> c)
  type instance Apply (f .@#@$$$ g) x = (f :. g) x
  
  (%.) :: forall b c a (f :: b ~> c) (g :: a ~> b) (x :: a).
          Sing f -> Sing g -> Sing x -> Sing ((f :. g) x)
  (f %. g) x = f @@ (g @@ x)
  
  type family Id (x :: a) :: a where
    Id x = x
  
  data IdSym0 :: forall a. a ~> a
  type instance Apply IdSym0 x = Id x
  
  sId :: forall a (x :: a). Sing x -> Sing (Id x)
  sId x = x
  
  data instance Sing :: forall i k c (p :: k). K1 i c p -> Type where
    SK1 :: Sing x -> Sing ('K1 x)
  
  data instance Sing :: forall k i (c :: Meta) (f :: k -> Type) (p :: k).
                        M1 i c f p -> Type where
    SM1 :: Sing x -> Sing ('M1 x)
  data M1Sym0 :: forall k i (c :: Meta) (f :: k -> Type) (p :: k).
                 f p ~> M1 i c f p
  type instance Apply M1Sym0 x = 'M1 x
  
  data instance Sing :: forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
                        (f :*: g) p -> Type where
    (:%*:) :: Sing x -> Sing y -> Sing (x ':*: y)
  
  data instance Sing :: forall p. Par1 p -> Type where
    SPar1 :: Sing x -> Sing ('Par1 x)
  
  class PGeneric1 (f :: k -> Type) where
    type From1 (z :: f a)      :: Rep1 f a
    type To1   (z :: Rep1 f a) :: f a
  
  class SGeneric1 (f :: k -> Type) where
    sFrom1 :: forall (a :: k) (z :: f a).      Sing z -> Sing (From1 z)
    sTo1   :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)
  
  class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k -> Type) where
    sTof1 :: forall (a :: k) (z :: f a).      Sing z -> To1 (From1 z)        :~: z
    sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> From1 (To1 r :: f a) :~: r
  
  instance PGeneric1 ((,) a) where
    type From1 '(x, y) = 'M1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('Par1 y)))
    type To1   ('M1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('Par1 y)))) = '(x, y)
  
  instance SGeneric1 ((,) a) where
    sFrom1 (STuple2 x y) = SM1 (SM1 (SM1 (SK1 x) :%*: SM1 (SPar1 y)))
    sTo1   (SM1 (SM1 (SM1 (SK1 x) :%*: SM1 (SPar1 y)))) = STuple2 x y
  
  instance VGeneric1 ((,) a) where
    sTof1 STuple2{} = Refl
    sFot1 (SM1 (SM1 (SM1 SK1{} :%*: SM1 SPar1{}))) = Refl
  
  class PSemigroup a where
    type (x :: a) <> (y :: a) :: a
  
  class SSemigroup a where
    (%<>) :: forall (x :: a) (y :: a).
             Sing x -> Sing y -> Sing (x <> y)
  
  class (PSemigroup a, SSemigroup a) => VSemigroup a where
    semigroupAssociative :: forall (x :: a) (y :: a) (z :: a).
                            Sing x -> Sing y -> Sing z
                         -> (x <> (y <> z)) :~: ((x <> y) <> z)
  
  class PSemigroup a => PMonoid a where
    type Mempty :: a
  
  class SSemigroup a => SMonoid a where
    sMempty :: Sing (Mempty :: a)
  
  class (PMonoid a, SMonoid a, VSemigroup a) => VMonoid a where
    monoidLeftIdentity  :: forall (x :: a).
                           Sing x -> (Mempty <> x) :~: x
    monoidRightIdentity :: forall (x :: a).
                           Sing x -> (x <> Mempty) :~: x
  