{-# 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
newtype CaseFunc (k :: Type -> Constraint) r (xs :: [Type]) = CaseFunc (forall x. k x => x -> r)
type instance CaseResult (CaseFunc k r) x = r
instance Reiterate (CaseFunc k r) xs where
reiterate (CaseFunc f) = CaseFunc f
instance k x => Case (CaseFunc k r) (x ': xs) where
case' (CaseFunc f) = f
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' f) = CaseFunc' f
instance k x => Case (CaseFunc' k) (x ': xs) where
case' (CaseFunc' f) = f
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 f) = CaseFunc1 f
instance (k (f x), k1 f, k0 x) => Case (CaseFunc1 k k1 k0 r) (f x ': xs) where
case' (CaseFunc1 f) = f
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' f) = CaseFunc1' f
instance (k (f x), k1 f, k0 x) => Case (CaseFunc1' k k1 k0) (f x ': xs) where
case' (CaseFunc1' f) = f