{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Functor.Compose.Singletons
-- Copyright   :  (C) 2021 Ryan Scott
-- License     :  BSD-style (see LICENSE)
-- Maintainer  :  Richard Eisenberg (rae@cs.brynmawr.edu)
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Exports the promoted and singled versions of the 'Compose' data type.
--
-----------------------------------------------------------------------------

module Data.Functor.Compose.Singletons (
  -- * The 'Compose' singleton
  Sing, SCompose(..), GetCompose, sGetCompose,

  -- * Defunctionalization symbols
  ComposeSym0, ComposeSym1,
  GetComposeSym0, GetComposeSym1
  ) where

import Control.Applicative
import Control.Applicative.Singletons
import Data.Eq.Singletons
import Data.Foldable.Singletons
import Data.Functor.Compose
import Data.Functor.Singletons
import Data.Ord.Singletons
import Data.Kind
import Data.Semigroup.Singletons
import Data.Singletons.Base.Instances (SList(..), (:@#@$), NilSym0)
import Data.Singletons.TH
import Data.Singletons.TH.Options
import Data.Traversable.Singletons

$(withOptions defaultOptions{genSingKindInsts = False}
    (genSingletons [''Compose]))

$(singletonsOnly [d|
  deriving instance Eq (f (g a)) => Eq (Compose f g a)
  deriving instance Ord (f (g a)) => Ord (Compose f g a)

  -- Note that in the instances below, we explicitly annotate `f` with its kind
  -- (Type -> Type), which is not something that is done in the original base
  -- library. This is because when singletons-th promotes instance declarations,
  -- it omits the instance contexts. As such, the instance declarations (as well
  -- as the associated defunctionalization symbols) would be given overly
  -- polymorphic kinds due to kind generalization, e.g.,
  --
  --   instance PFunctor (Compose (f :: k -> Type) (g :: Type -> k)) where ...
  --
  -- Annotating `f :: Type -> Type` is a clunky but reliable way of preventing
  -- this. See also Note [Using standalone kind signatures not present in the
  -- base library] in Control.Monad.Singletons.Internal for a similar situation
  -- where class definitions can become overly polymorphic unless given an
  -- explicit kind.

  instance (Functor f, Functor g) => Functor (Compose (f :: Type -> Type) g) where
      fmap f (Compose x) = Compose (fmap (fmap f) x)
      a <$ (Compose x) = Compose (fmap (a <$) x)

  instance (Foldable f, Foldable g) => Foldable (Compose (f :: Type -> Type) g) where
      foldMap f (Compose t) = foldMap (foldMap f) t

  instance (Traversable f, Traversable g) => Traversable (Compose (f :: Type -> Type) g) where
      traverse f (Compose t) = Compose <$> traverse (traverse f) t

  instance (Applicative f, Applicative g) => Applicative (Compose (f :: Type -> Type) g) where
      pure x = Compose (pure (pure x))
      Compose f <*> Compose x = Compose (liftA2 (<*>) f x)
      liftA2 f (Compose x) (Compose y) =
        Compose (liftA2 (liftA2 f) x y)

  instance (Alternative f, Applicative g) => Alternative (Compose (f :: Type -> Type) g) where
      empty = Compose empty
      Compose x <|> Compose y = Compose (x <|> y)
  |])