{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Hefty.Union.Strengthen where
import Control.Effect (type (~>))
import Data.Hefty.Union (MemberRec, Union (inject0, (|+:)), injectRec, weaken)
import Data.Type.Equality (type (==))
import GHC.TypeNats (Natural, type (-))
class
(Union u, isMZero ~ (m == 0), isNZero ~ (n == 0)) =>
StrengthenUnder_ (isMZero :: Bool) (m :: Natural) (isNZero :: Bool) (n :: Natural) u es es'
| m n es -> es'
where
strengthenNUnderM_ :: u es f ~> u es' f
type StrengthenUnder n m = StrengthenUnder_ (m == 0) m (n == 0) n
type Strengthen n = StrengthenUnder_ 'True 0 (n == 0) n
strengthenNUnderM :: forall n m u es' f es. StrengthenUnder n m u es es' => u es f ~> u es' f
strengthenNUnderM :: forall (n :: Natural) (m :: Natural) (u :: [SigClass] -> SigClass)
(es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
StrengthenUnder n m u es es' =>
u es f ~> u es' f
strengthenNUnderM = forall (isMZero :: Bool) (m :: Natural) (isNZero :: Bool)
(n :: Natural) (u :: [SigClass] -> SigClass) (es :: [SigClass])
(es' :: [SigClass]) (f :: * -> *).
StrengthenUnder_ isMZero m isNZero n u es es' =>
u es f ~> u es' f
strengthenNUnderM_ @(m == 0) @m @(n == 0) @n
{-# INLINE strengthenNUnderM #-}
strengthenN :: forall n u es' f es. Strengthen n u es es' => u es f ~> u es' f
strengthenN :: forall (n :: Natural) (u :: [SigClass] -> SigClass)
(es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
Strengthen n u es es' =>
u es f ~> u es' f
strengthenN = forall (isMZero :: Bool) (m :: Natural) (isNZero :: Bool)
(n :: Natural) (u :: [SigClass] -> SigClass) (es :: [SigClass])
(es' :: [SigClass]) (f :: * -> *).
StrengthenUnder_ isMZero m isNZero n u es es' =>
u es f ~> u es' f
strengthenNUnderM_ @( 'True) @0 @(n == 0) @n
{-# INLINE strengthenN #-}
instance
(Union u, StrengthenUnder n (m - 1) u es es', (m == 0) ~ 'False, isNZero ~ (n == 0)) =>
StrengthenUnder_ 'False m isNZero n u (e ': es) (e ': es')
where
strengthenNUnderM_ :: forall (f :: * -> *). u (e : es) f ~> u (e : es') f
strengthenNUnderM_ = forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
(es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
(f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Natural) (m :: Natural) (u :: [SigClass] -> SigClass)
(es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
StrengthenUnder n m u es es' =>
u es f ~> u es' f
strengthenNUnderM @n @(m - 1)
{-# INLINE strengthenNUnderM_ #-}
instance
(Union u, Strengthen (n - 1) u es es', MemberRec u e es, (n == 0) ~ 'False) =>
StrengthenUnder_ 'True 0 'False n u (e ': es) es'
where
strengthenNUnderM_ :: forall (f :: * -> *). u (e : es) f ~> u es' f
strengthenNUnderM_ = forall (n :: Natural) (u :: [SigClass] -> SigClass)
(es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
Strengthen n u es es' =>
u es f ~> u es' f
strengthenN @(n - 1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (u :: [SigClass] -> SigClass) (e :: SigClass)
(es :: [SigClass]) (f :: * -> *).
MemberRec u e es =>
e f ~> u es f
injectRec forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall a. a -> a
id)
{-# INLINE strengthenNUnderM_ #-}
instance Union u => StrengthenUnder_ 'True 0 'True 0 u es es where
strengthenNUnderM_ :: forall (f :: * -> *). u es f ~> u es f
strengthenNUnderM_ = forall a. a -> a
id
{-# INLINE strengthenNUnderM_ #-}