{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Data.Diverse.CaseFunc where

import Data.Diverse.Case
import Data.Diverse.Reiterate
import Data.Diverse.TypeLevel
import Data.Kind

-- | This handler stores a polymorphic function that returns a different type.
--
-- @
-- let y = 'Data.Diverse.Which.pick' (5 :: Int) :: 'Data.Diverse.Which.Which' '[Int, Bool]
-- 'Data.Diverse.Which.switch' y ('CaseFunc' \@'Data.Typeable.Typeable' (show . typeRep . (pure \@Proxy))) \`shouldBe` "Int"
-- @
--
-- @
-- let x = (5 :: Int) 'Data.Diverse.Many../' False 'Data.Diverse.Many../' \'X' 'Data.Diverse.Many../' Just \'O' 'Data.Diverse.Many../' (6 :: Int) 'Data.Diverse.Many../' Just \'A' 'Data.Diverse.Many../' 'Data.Diverse.Many.nul'
-- 'Data.Diverse.AFoldable.afoldr' (:) [] ('Data.Diverse.Many.forMany' ('CaseFunc' \@'Data.Typeable.Typeable' (show . typeRep . (pure @Proxy))) x) \`shouldBe`
--     [\"Int", \"Bool", \"Char", \"Maybe Char", \"Int", \"Maybe Char"]
-- @
newtype CaseFunc (k :: Type -> Constraint) r (xs :: [Type]) = CaseFunc (forall x. k x => x -> r)
-- This was made possible by Syrak
-- https://www.reddit.com/r/haskell/comments/75zrci/help_how_to_pass_constraints_as_a_type_variable/

type instance CaseResult (CaseFunc k r) x = r

instance Reiterate (CaseFunc k r) xs where
    reiterate :: CaseFunc k r xs -> CaseFunc k r (Tail xs)
reiterate (CaseFunc forall x. k x => x -> r
f) = forall (k :: * -> Constraint) r (xs :: [*]).
(forall x. k x => x -> r) -> CaseFunc k r xs
CaseFunc forall x. k x => x -> r
f

instance k x => Case (CaseFunc k r) (x ': xs) where
    case' :: CaseFunc k r (x : xs)
-> Head (x : xs) -> CaseResult (CaseFunc k r) (Head (x : xs))
case' (CaseFunc forall x. k x => x -> r
f) = forall x. k x => x -> r
f

-- | This handler stores a polymorphic function that doesn't change the type.
--
-- @
-- let x = (5 :: Int) 'Data.Diverse.Many../' (6 :: Int8) 'Data.Diverse.Many../' (7 :: Int16) 'Data.Diverse.Many../' (8 :: Int32) 'Data.Diverse.Many../' 'Data.Diverse.Many.nil'
--     y = (15 :: Int) 'Data.Diverse.Many../' (16 :: Int8) 'Data.Diverse.Many../' (17 :: Int16) 'Data.Diverse.Many../' (18 :: Int32) 'Data.Diverse.Many../' 'Data.Diverse.Many.nil'
-- 'Data.Diverse.AFunctor.afmap' ('CaseFunc'' \@'Num' (+10)) x \`shouldBe` y
-- @
newtype CaseFunc' (k :: Type -> Constraint) (xs :: [Type]) = CaseFunc' (forall x. k x => x -> x)

type instance CaseResult (CaseFunc' k) x = x

instance Reiterate (CaseFunc' k) xs where
    reiterate :: CaseFunc' k xs -> CaseFunc' k (Tail xs)
reiterate (CaseFunc' forall x. k x => x -> x
f) = forall (k :: * -> Constraint) (xs :: [*]).
(forall x. k x => x -> x) -> CaseFunc' k xs
CaseFunc' forall x. k x => x -> x
f

instance k x => Case (CaseFunc' k) (x ': xs) where
    case' :: CaseFunc' k (x : xs)
-> Head (x : xs) -> CaseResult (CaseFunc' k) (Head (x : xs))
case' (CaseFunc' forall x. k x => x -> x
f) = forall x. k x => x -> x
f

-- | This handler stores a polymorphic function that work on higher kinds, eg 'Functor'
-- You may want to use @C0 for @k@
newtype CaseFunc1 (k :: Type -> Constraint) (k1 :: (Type -> Type) -> Constraint) (k0 :: Type -> Constraint) r (xs :: [Type]) = CaseFunc1 (forall f x. (k (f x), k1 f, k0 x) => f x -> f r)

type instance CaseResult (CaseFunc1 k k1 k0 r) (f x) = f r

instance Reiterate (CaseFunc1 k k1 k0 r) xs where
    reiterate :: CaseFunc1 k k1 k0 r xs -> CaseFunc1 k k1 k0 r (Tail xs)
reiterate (CaseFunc1 forall (f :: * -> *) x. (k (f x), k1 f, k0 x) => f x -> f r
f) = forall (k :: * -> Constraint) (k1 :: (* -> *) -> Constraint)
       (k0 :: * -> Constraint) r (xs :: [*]).
(forall (f :: * -> *) x. (k (f x), k1 f, k0 x) => f x -> f r)
-> CaseFunc1 k k1 k0 r xs
CaseFunc1 forall (f :: * -> *) x. (k (f x), k1 f, k0 x) => f x -> f r
f

instance (k (f x), k1 f, k0 x) => Case (CaseFunc1 k k1 k0 r) (f x ': xs) where
    case' :: CaseFunc1 k k1 k0 r (f x : xs)
-> Head (f x : xs)
-> CaseResult (CaseFunc1 k k1 k0 r) (Head (f x : xs))
case' (CaseFunc1 forall (f :: * -> *) x. (k (f x), k1 f, k0 x) => f x -> f r
f) = forall (f :: * -> *) x. (k (f x), k1 f, k0 x) => f x -> f r
f

newtype CaseFunc1_ (k :: Type -> Constraint) (k1 :: (Type -> Type) -> Constraint) (k0 :: Type -> Constraint) r x (xs :: [Type]) = CaseFunc1_ (forall f. (k (f x), k1 f, k0 x) => f x -> f r)

type instance CaseResult (CaseFunc1_ k k1 k0 r x) (f x) = f r

instance Reiterate (CaseFunc1_ k k1 k0 r x) xs where
    reiterate :: CaseFunc1_ k k1 k0 r x xs -> CaseFunc1_ k k1 k0 r x (Tail xs)
reiterate (CaseFunc1_ forall (f :: * -> *). (k (f x), k1 f, k0 x) => f x -> f r
f) = forall (k :: * -> Constraint) (k1 :: (* -> *) -> Constraint)
       (k0 :: * -> Constraint) r x (xs :: [*]).
(forall (f :: * -> *). (k (f x), k1 f, k0 x) => f x -> f r)
-> CaseFunc1_ k k1 k0 r x xs
CaseFunc1_ forall (f :: * -> *). (k (f x), k1 f, k0 x) => f x -> f r
f

instance (k (f x), k1 f, k0 x) => Case (CaseFunc1_ k k1 k0 r x) (f x ': xs) where
    case' :: CaseFunc1_ k k1 k0 r x (f x : xs)
-> Head (f x : xs)
-> CaseResult (CaseFunc1_ k k1 k0 r x) (Head (f x : xs))
case' (CaseFunc1_ forall (f :: * -> *). (k (f x), k1 f, k0 x) => f x -> f r
f) = forall (f :: * -> *). (k (f x), k1 f, k0 x) => f x -> f r
f


-- | A varation of 'CaseFunc1' that doesn't change the return type
newtype CaseFunc1' (k :: Type -> Constraint) (k1 :: (Type -> Type) -> Constraint) (k0 :: Type -> Constraint) (xs :: [Type]) = CaseFunc1' (forall f x. (k (f x), k1 f, k0 x) => f x -> f x)

type instance CaseResult (CaseFunc1' k k1 k0) (f x) = f x

instance Reiterate (CaseFunc1' k k1 k0) xs where
    reiterate :: CaseFunc1' k k1 k0 xs -> CaseFunc1' k k1 k0 (Tail xs)
reiterate (CaseFunc1' forall (f :: * -> *) x. (k (f x), k1 f, k0 x) => f x -> f x
f) = forall (k :: * -> Constraint) (k1 :: (* -> *) -> Constraint)
       (k0 :: * -> Constraint) (xs :: [*]).
(forall (f :: * -> *) x. (k (f x), k1 f, k0 x) => f x -> f x)
-> CaseFunc1' k k1 k0 xs
CaseFunc1' forall (f :: * -> *) x. (k (f x), k1 f, k0 x) => f x -> f x
f

instance (k (f x), k1 f, k0 x) => Case (CaseFunc1' k k1 k0) (f x ': xs) where
    case' :: CaseFunc1' k k1 k0 (f x : xs)
-> Head (f x : xs)
-> CaseResult (CaseFunc1' k k1 k0) (Head (f x : xs))
case' (CaseFunc1' forall (f :: * -> *) x. (k (f x), k1 f, k0 x) => f x -> f x
f) = forall (f :: * -> *) x. (k (f x), k1 f, k0 x) => f x -> f x
f