{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module T15703 where

import Data.Kind
import Data.Type.Equality
import GHC.Generics
import T15703_aux

-----
-- The important bits
-----

-- DefaultSignatures-based instances
instance PMonoid a => PApplicative ((,) a)
instance SMonoid a => SApplicative ((,) a)
instance VMonoid a => VApplicative ((,) a)

instance SApplicative f => SApplicative (M1 i c f) where
  sPure x = singFun3 @(.@#@$) (%.) @@ singFun1 @M1Sym0 SM1 @@ (singFun1 @PureSym0 sPure) @@ x
  -- If I change the implementation of sPure above to be this:
  --
  --   sPure x = SM1 (sPure x)
  --
  -- Then T15703.hs compiles quickly again (< 1 second) with -O1.

  SM1 f %<*> SM1 x = SM1 (f %<*> x)

-------------------------------------------------------------------------------

type GenericPure :: a -> f a
type family GenericPure (x :: a) :: f a where
  GenericPure x = To1 (Pure x)

type GenericPureC (f :: Type -> Type) (x :: a) =
  (Pure x :: f a) ~ (GenericPure x :: f a)

type GenericAp :: f (a ~> b) -> f a -> f b
type family (g :: f (a ~> b)) `GenericAp` (x :: f a) :: f b where
  g `GenericAp` x = To1 (From1 g <*> From1 x)

type GenericApC (g :: f (a ~> b)) (x :: f a) =
  (g <*> x) ~ (g `GenericAp` x)

class PApplicative f where
  type Pure (x :: a) :: f a
  type Pure x = GenericPure x

  type (g :: f (a ~> b)) <*> (x :: f a) :: f b
  type g <*> x = g `GenericAp` x

data PureSym0 :: forall f a. a ~> f a
type instance Apply PureSym0 x = Pure x

data (<*>@#@$) :: forall f a b. f (a ~> b) ~> f a ~> f b
type instance Apply (<*>@#@$) g = (<*>@#@$$) g
data (<*>@#@$$) :: forall f a b. f (a ~> b) -> f a ~> f b
type instance Apply ((<*>@#@$$) g) x = g <*> x

class SApplicative f where
  sPure         :: forall a (x :: a).
                   Sing x -> Sing (Pure x :: f a)
  default sPure :: forall a (x :: a).
                   ( SGeneric1 f, SApplicative (Rep1 f)
                   , GenericPureC f x )
                => Sing x -> Sing (Pure x :: f a)
  sPure = sTo1 . sPure

  (%<*>)         :: forall a b (g :: f (a ~> b)) (x :: f a).
                    Sing g -> Sing x -> Sing (g <*> x)
  default (%<*>) :: forall a b (g :: f (a ~> b)) (x :: f a).
                    ( SGeneric1 f, SApplicative (Rep1 f)
                    , GenericApC g x )
                 => Sing g -> Sing x -> Sing (g <*> x)
  sg %<*> sx = sTo1 (sFrom1 sg %<*> sFrom1 sx)

class (PApplicative f, SApplicative f) => VApplicative f where
  applicativeHomomorphism         :: forall a b (g :: a ~> b) (x :: a).
                                     Sing g -> Sing x
                                  -> (Pure g <*> Pure x) :~: (Pure (g `Apply` x) :: f b)
  default applicativeHomomorphism :: forall a b (g :: a ~> b) (x :: a).
                                     ( VGeneric1 f, VApplicative (Rep1 f)
                                     , GenericPureC f g, GenericPureC f x, GenericPureC f (g `Apply` x)
                                     , GenericApC (Pure g :: f (a ~> b)) (Pure x :: f a)
                                     )
                                  => Sing g -> Sing x
                                  -> (Pure g <*> Pure x) :~: (Pure (g `Apply` x) :: f b)
  applicativeHomomorphism sg sx
    | Refl <- sFot1 @Type @f (sPure sg)
    , Refl <- sFot1 @Type @f (sPure sx)
    , Refl <- applicativeHomomorphism @(Rep1 f) sg sx
    , Refl <- sFot1 @Type @f pureGX
    , Refl <- sTof1 @Type @f (sTo1 pureGX)
    = Refl
    where
      pureGX :: Sing (Pure (Apply g x) :: Rep1 f b)
      pureGX = sPure (sg @@ sx)

instance PApplicative (K1 i c) where
  type Pure _ = 'K1 Mempty
  type 'K1 x <*> 'K1 y = 'K1 (x <> y)

instance SMonoid c => SApplicative (K1 i c) where
  sPure _ = SK1 sMempty
  SK1 x %<*> SK1 y = SK1 (x %<> y)

instance VMonoid c => VApplicative (K1 i c) where
  applicativeHomomorphism _ _ | Refl <- monoidLeftIdentity (sMempty @c) = Refl

instance PApplicative (M1 i c f) where
  type Pure x = 'M1 (Pure x)
  type 'M1 ff <*> 'M1 x = 'M1 (ff <*> x)

instance VApplicative f => VApplicative (M1 i c f) where
  applicativeHomomorphism sg sx
    | Refl <- applicativeHomomorphism @f sg sx
    = Refl

instance PApplicative (f :*: g) where
  type Pure a = Pure a ':*: Pure a
  type (ff ':*: gg) <*> (x ':*: y) = (ff <*> x) ':*: (gg <*> y)

instance (SApplicative f, SApplicative g) => SApplicative (f :*: g) where
  sPure a = sPure a :%*: sPure a
  (f :%*: g) %<*> (x :%*: y) = (f %<*> x) :%*: (g %<*> y)

instance (VApplicative f, VApplicative g) => VApplicative (f :*: g) where
  applicativeHomomorphism sg sx
    | Refl <- applicativeHomomorphism @f sg sx
    , Refl <- applicativeHomomorphism @g sg sx
    = Refl

instance PApplicative Par1 where
  type Pure x = 'Par1 x
  type 'Par1 f <*> 'Par1 x = 'Par1 (f @@ x)

instance SApplicative Par1 where
  sPure = SPar1
  SPar1 f %<*> SPar1 x = SPar1 (f @@ x)

instance VApplicative Par1 where
  applicativeHomomorphism _ _ = Refl