{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Generics.Sum.Internal.Typed
-- Copyright   :  (C) 2020 Csongor Kiss
-- License     :  BSD3
-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Derive constructor-field-type-based prisms generically.
--
-----------------------------------------------------------------------------

module Data.Generics.Sum.Internal.Typed
  ( Context
  , derived
  , GAsType (..)
  ) where

import Data.Kind
import GHC.Generics

import GHC.TypeLits (TypeError, ErrorMessage (..), Symbol)
import Data.Generics.Internal.Errors
import Data.Generics.Internal.Families
import Data.Generics.Product.Internal.HList
import Data.Generics.Internal.Profunctor.Iso
import Data.Generics.Internal.Profunctor.Prism

type Context a s
  = ( Generic s
    , ErrorUnlessOne a s (CollectPartialType (TupleToList a) (Rep s))
    , GAsType (Rep s) a
    , Defined (Rep s)
      (NoGeneric s '[ 'Text "arising from a generic prism focusing on a constructor of type " ':<>: QuoteType a])
      (() :: Constraint)
    )

derived :: Context a s => Prism' s a
derived = repIso . _GTyped
{-# INLINE derived #-}

type family ErrorUnlessOne (a :: Type) (s :: Type) (ctors :: [Symbol]) :: Constraint where
  ErrorUnlessOne _ _ '[_]
    = ()

  ErrorUnlessOne a s '[]
    = TypeError
        (     'Text "The type "
        ':<>: 'ShowType s
        ':<>: 'Text " does not contain a constructor whose field is of type "
        ':<>: 'ShowType a
        )

  ErrorUnlessOne a s cs
    = TypeError
        (     'Text "The type "
        ':<>: 'ShowType s
        ':<>: 'Text " contains multiple constructors whose fields are of type "
        ':<>: 'ShowType a ':<>: 'Text "."
        ':$$: 'Text "The choice of constructor is thus ambiguous, could be any of:"
        ':$$: ShowSymbols cs
        )

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

-- |As 'AsType' but over generic representations as defined by "GHC.Generics".
class GAsType (f :: Type -> Type) (as :: Type) where
  _GTyped :: Prism (f x) (f x) as as

instance
  ( GIsList f f as as
  , ListTuple a a as as
  ) => GAsType (M1 C meta f) a where
  _GTyped = mIso . glist . tupled
  {-# INLINE _GTyped #-}

instance GSumAsType (HasPartialTypeP (TupleToList a) l) l r a => GAsType (l :+: r) a where
  _GTyped = _GSumTyped @(HasPartialTypeP (TupleToList a) l)
  {-# INLINE _GTyped #-}

instance GAsType f a => GAsType (M1 D meta f) a where
  _GTyped = mIso . _GTyped
  {-# INLINE _GTyped #-}

class GSumAsType (contains :: Bool) l r (a :: Type) where
  _GSumTyped :: Prism ((l :+: r) x) ((l :+: r) x) a a

instance GAsType l a => GSumAsType 'True l r a where
  _GSumTyped = left . _GTyped
  {-# INLINE _GSumTyped #-}

instance GAsType r a => GSumAsType 'False l r a where
  _GSumTyped = right . _GTyped
  {-# INLINE _GSumTyped #-}