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

-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Generics.Sum.Internal.Subtype
-- Copyright   :  (C) 2020 Csongor Kiss
-- License     :  BSD3
-- Maintainer  :  Csongor Kiss <kiss.csongor.kiss@gmail.com>
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Structural subtype relationships between sum types.
--
-----------------------------------------------------------------------------

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

import Data.Generics.Product.Internal.HList
import Data.Generics.Sum.Internal.Typed (GAsType (..))

import Data.Kind
import GHC.Generics
import Data.Generics.Internal.Profunctor.Iso
import Data.Generics.Internal.Profunctor.Prism
import Data.Generics.Internal.Families.Has

type Context sub sup
  = ( Generic sub
    , Generic sup
    , GAsSubtype (Rep sub) (Rep sup)
    )

derived :: Context sub sup => Prism' sup sub
derived = repIso . _GSub . fromIso repIso
{-# INLINE derived #-}

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

-- |As 'AsSubtype' but over generic representations as defined by
--  "GHC.Generics".
class GAsSubtype (subf :: Type -> Type) (supf :: Type -> Type) where
  _GSub :: Prism' (supf x) (subf x)

instance
  ( GSplash sub sup
  , GDowncast sub sup
  ) => GAsSubtype sub sup where
  _GSub f = prism _GSplash _GDowncast f
  {-# INLINE _GSub #-}

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

class GSplash (sub :: Type -> Type) (sup :: Type -> Type) where
  _GSplash :: sub x -> sup x

instance (GSplash a sup, GSplash b sup) => GSplash (a :+: b) sup where
  _GSplash (L1 rep) = _GSplash rep
  _GSplash (R1 rep) = _GSplash rep
  {-# INLINE _GSplash #-}

instance
  ( GIsList subf subf as as
  , ListTuple as' as' as as
  , GAsType supf as'
  ) => GSplash (C1 meta subf) supf where
  _GSplash p = build (_GTyped . fromIso (mIso . glist . tupled)) p
  {-# INLINE _GSplash #-}

instance GSplash sub sup => GSplash (D1 c sub) sup where
  _GSplash (M1 m) = _GSplash m
  {-# INLINE _GSplash #-}

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

class GDowncast sub sup where
  _GDowncast :: sup x -> Either (sup x) (sub x)

instance
  ( GIsList sup sup as as
  , GDowncastC (HasPartialTypeP as sub) sub sup
  ) => GDowncast sub (C1 m sup) where
  _GDowncast (M1 m) = case _GDowncastC @(HasPartialTypeP as sub) m of
    Left _ -> Left (M1 m)
    Right r -> Right r
  {-# INLINE _GDowncast #-}

instance (GDowncast sub l, GDowncast sub r) => GDowncast sub (l :+: r) where
  _GDowncast (L1 x) = case _GDowncast x of
    Left _ -> Left (L1 x)
    Right r -> Right r
  _GDowncast (R1 x) = case _GDowncast x of
    Left _ -> Left (R1 x)
    Right r -> Right r
  {-# INLINE _GDowncast #-}

instance GDowncast sub sup => GDowncast sub (D1 m sup) where
  _GDowncast (M1 m) = case _GDowncast m of
    Left _ -> Left (M1 m)
    Right r -> Right r
  {-# INLINE _GDowncast #-}

class GDowncastC (contains :: Bool) sub sup where
  _GDowncastC :: sup x -> Either (sup x) (sub x)

instance GDowncastC 'False sub sup where
  _GDowncastC sup = Left sup
  {-# INLINE _GDowncastC #-}

instance
  ( GAsType sub subl'
  , GIsList sup sup subl subl
  , ListTuple subl' subl' subl subl
  ) => GDowncastC 'True sub sup where
  _GDowncastC sup = Right (build (_GTyped . fromIso (glist . tupled)) sup)
  {-# INLINE _GDowncastC #-}