{-# 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 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
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
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
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