monad-levels-0.1.0.0: Control/Monad/Levels/Constraints.hs
{-# LANGUAGE ConstraintKinds, DataKinds, DefaultSignatures, FlexibleContexts,
FlexibleInstances, MultiParamTypeClasses, ScopedTypeVariables,
TupleSections, TypeFamilies, TypeOperators, UndecidableInstances
#-}
-- unsafeCoerceConstraint is used to prevent the need for a complex
-- induction proof (which I'm not sure can actually be achieved).
{-# LANGUAGE Trustworthy #-}
{- |
Module : Control.Monad.Levels.Constraints
Description : A Level-based approach to constraints
Copyright : (c) Ivan Lazar Miljenovic
License : 3-Clause BSD-style
Maintainer : Ivan.Miljenovic@gmail.com
-}
module Control.Monad.Levels.Constraints
( -- * Constraints in the monad stack
liftSat
, lowerSat
, lowerSat'
, lowerFunction
, SatisfyConstraint
, SatisfyConstraintF
, SatMonad
, SatMonadValue
, CanLowerFunc
, SatFunction
, ValidConstraint(..)
, ConstraintPassThrough
-- ** Internal types and classes
, SatisfyConstraint_(SatMonad_, SatValue_, CanLowerFunc_)
, SatDepth
, proofInst
-- * Variadic functions
, VariadicFunction
, VarFunction
, VariadicLower
, LowerV
, SatV
, CanLower
, VarFunctionSat
, MkVarFn
, MkVarFnFrom
, Func
-- ** Variadic arguments
, VariadicArg(VariadicType)
, LowerableVArg
, LiftableVArg
, WrappableVArg
, ValueOnly
, Const
, MonadicValue
, MonadicOther
, MonadicTuple
-- * Re-exported for convenience
, Proxy(..)
) where
import Control.Monad.Levels.ConstraintPassing
import Control.Monad.Levels.Definitions
import Data.Constraint ((:-) (..), Constraint, Dict (..), (\\))
import Data.Constraint.Unsafe (unsafeCoerceConstraint)
import Data.Monoid (Monoid (mempty))
import Data.Proxy (Proxy (..), asProxyTypeOf)
-- -----------------------------------------------------------------------------
data Nat = Zero | Suc Nat
predP :: Proxy (Suc n) -> Proxy n
predP _ = Proxy
-- | Inductively find the \"floor\" in the 'MonadTower' where the
-- specified constraint is satisfied.
--
-- This class is only exported for documentation purposes: no other
-- instances are possible, and most of the internals are not safe to
-- use outside of this module.
--
-- You should use 'SatisfyConstraint' instead of this in your
-- constraints.
class (ValidConstraint c, MonadTower m) => SatisfyConstraint_ (n :: Nat) c m where
-- | The monad in the stack that satisfies the constraint.
type SatMonad_ n c m :: * -> *
-- | The value in the stack within the monad that satisfies the
-- constraint.
type SatValue_ n c m a
-- | The extra constraints needed to be able to lower the provided
-- 'VariadicFunction' @f@ to the satisfying monad.
type CanLowerFunc_ f n c m a :: Constraint
_liftSat :: Proxy n -> Proxy c -> Proxy m -> Proxy a -> SatMonad_ n c m a -> m a
_lower :: (VariadicFunction f, CanLowerFunc_ f n c m a)
=> Proxy n -> Proxy c -> Proxy f -> Proxy m -> Proxy a
-> VarFunctionSat f n c m a
-> VarFunction f m a
-- | The satisfying monad for the specified constraint.
instance (ValidConstraint c, MonadTower m, c m) => SatisfyConstraint_ Zero c m where
type SatMonad_ Zero c m = m
type SatValue_ Zero c m a = a
type CanLowerFunc_ f Zero c m a = ()
_liftSat _ _ _ _ m = m
_lower _n c vf m _a f = f \\ validSatFunc0 c m vf
-- | Inductive step for finding the satisfying monad. Note the usage
-- of 'ConstraintPassThrough' to ensure that only (constraint,monad
-- level) pairings that are valid are considered.
instance (ConstraintPassThrough c m True, SatisfyConstraint_ n c (LowerMonad m))
=> SatisfyConstraint_ (Suc n) c m where
type SatMonad_ (Suc n) c m = SatMonad_ n c (LowerMonad m)
type SatValue_ (Suc n) c m a = SatValue_ n c (LowerMonad m) (InnerValue m a)
type CanLowerFunc_ f (Suc n) c m a = ( (CanLower f m a)
, (CanLowerFunc_ (LowerV f m) n c (LowerMonad m) (InnerValue m a)))
_liftSat n c m a sm = wrap a (\ _unwrap addI -> addInternalM addI (_liftSat (predP n) c (lowerP m) a sm))
\\ proofInst m a
_lower n c vf m a f = applyVFn vf m a (\ _unwrap _addI -> _lower (predP n)
c
(plowerF m vf)
(lowerP m)
(innerP m a)
f
\\ validLowerFunc m vf
\\ validSatFunc n c m vf)
lowerP :: (MonadLevel m) => Proxy m -> Proxy (LowerMonad m)
lowerP _ = Proxy
{-# INLINE lowerP #-}
innerP :: (MonadLevel m) => Proxy m -> Proxy a -> Proxy (InnerValue m a)
innerP _ _ = Proxy
{-# INLINE innerP #-}
-- | For a specified constraint @c@ and 'MonadTower' @m@,
-- @SatisfyConstraint c m@ specifies that it is possible to reach a
-- monad in the tower that specifies the constraint.
type SatisfyConstraint c m = ( SatisfyConstraint_ (SatDepth c m) c m
, c (SatMonad c m)
-- Best current way of stating that the
-- satisfying monad is a lower level of
-- the specified one.
, BaseMonad (SatMonad c m) ~ BaseMonad m)
-- | An extension of 'SatisfyConstraint' that also ensures that any
-- additional constraints needed to satisfy a 'VariadicFunction' @f@
-- to achieve an end result based upon the type @m a@ are met.
type SatisfyConstraintF c m a f = ( SatisfyConstraint c m
, VariadicFunction f
, CanLowerFunc f c m a)
-- | Any additional constraints that may be needed for a specified
-- 'VariadicFunction' to be valid as it is lowered to the satisfying
-- monad.
--
-- This typically matters only if 'ValueOnly' or 'MonadicOther' are
-- used.
type CanLowerFunc f c m a = CanLowerFunc_ f (SatDepth c m) c m a
-- | Lift a value of the satisfying monad to the top of the tower.
liftSat :: forall c m a. (SatisfyConstraint c m) =>
Proxy c -> SatMonad c m a -> m a
liftSat p = _liftSat (Proxy :: Proxy (SatDepth c m)) p (Proxy :: Proxy m) (Proxy :: Proxy a)
-- | The type of the 'VariadicFunction' @f@ when the provided
-- constraint is satisfied.
type SatFunction c f m a = VarFunctionSat f (SatDepth c m) c m a
-- | Converts @m a@ into what the value in the monadic stack is where
-- the monad satisfies the provided constraint.
type SatMonadValue c m a = SatMonad_ (SatDepth c m) c m (SatValue_ (SatDepth c m) c m a)
-- | Lower a function from the top of the monad tower down to the
-- satisfying monad in which it can be applied.
lowerSat :: forall c m a f. (SatisfyConstraintF c m a f) =>
Proxy c -> Proxy f -> Proxy m -> Proxy a
-> SatFunction c f m a -> VarFunction f m a
lowerSat c vf m a f = _lower n c vf m a f
where
n :: Proxy (SatDepth c m)
n = Proxy
type MFunc = MkVarFn MonadicValue
-- | A variant of 'lowerSat' for when @CanLower f m a ~ ()@.
lowerSat' :: forall c m a f. (SatisfyConstraint c m, VariadicFunction f)
=> Proxy c -> Proxy f -> Proxy m -> Proxy a
-> (() :- CanLower f m a)
-> SatFunction c f m a -> VarFunction f m a
lowerSat' c vf m a prf f = _lower n c vf m a f \\ simpleFuncProof vf c m a prf
where
n :: Proxy (SatDepth c m)
n = Proxy
-- | A specialised instance of 'lowerSat' where a simple function of
-- type @m a -> m a@ is lowered to the satisfying monad.
lowerFunction :: forall c m a. (SatisfyConstraint c m) => Proxy c
-> (SatMonadValue c m a -> SatMonadValue c m a)
-> m a -> m a
lowerFunction c f = lowerSat' c vf m a (Sub Dict) f
where
vf :: Proxy MFunc
vf = Proxy
m :: Proxy m
m = Proxy
a :: Proxy a
a = Proxy
simpleFuncProof :: (SatisfyConstraint c m, VariadicFunction f)
=> Proxy f -> Proxy c -> Proxy m -> Proxy a
-> (() :- CanLower f m a) -> (() :- CanLowerFunc f c m a)
simpleFuncProof _ _ _ _ (Sub Dict) = unsafeCoerceConstraint
{-# INLINE simpleFuncProof #-}
-- Will always be @~ ()@ by construction, but an actual proof would
-- need to be by induction.
-- -----------------------------------------------------------------------------
-- Converts the monadic stack into a list of sub-stacks, and tests if
-- each sub-stack satisfies the constraint.
type TrySatisfy (c :: (* -> *) -> Constraint) (m :: (* -> *)) = TrySatisfy' c (BaseMonad m) m
type family TrySatisfy' (c :: (* -> *) -> Constraint) (b :: (* -> *)) (m :: (* -> *)) :: [Bool] where
TrySatisfy' c b b = ConstraintSatisfied c b ': '[]
TrySatisfy' c b m = ConstraintSatisfied c m ': TrySatisfy' c b (LowerMonad m)
type family FindTrue (bms :: [Bool]) :: Nat where
FindTrue (True ': t) = Zero
FindTrue (False ': t) = Suc (FindTrue t)
-- | Calculate how many levels down is the satisfying monad.
type SatDepth (c :: (* -> *) -> Constraint) (m :: * -> *) = FindTrue (TrySatisfy c m)
-- | The Monad in the tower that satisfies the provided constraint.
type SatMonad (c :: (* -> *) -> Constraint) (m :: * -> *) = SatMonad_ (SatDepth c m) c m
-- -----------------------------------------------------------------------------
-- | Base class for dealing with variadic functions\/arguments.
class VariadicLower v where
-- | The type when lowered to the 'LowerMonad'. In most cases this
-- will be the same value.
type LowerV v (m :: * -> *) :: *
type LowerV v m = v
-- | The type when applied to the satisfying monad.
type SatV v (n :: Nat) (c :: (* -> *) -> Constraint) (m :: * -> *) :: *
type SatV v n c m = v
-- | Any additional constraints needed when lowering @v@.
type CanLower v (m :: * -> *) a :: Constraint
type CanLower v m a = ()
-- | Class representing arguments\/parameters for lower-able variadic
-- functions.
--
-- When considering a function with an end result based upon @m a@,
-- the following argument types are available:
--
-- [@'ValueOnly'@] corresponds to @a@.
--
-- [@'Const' b@] corresponds to some other type @b@.
--
-- [@'MonadicValue'@] corresponds to @m a@.
--
-- [@'MonadicOther' b@] corresponds to @m b@.
--
-- [@'MonadicTuple' b@] corresponds to @m (a,b)@.
--
-- [@'Func' v1 v2@] corresponds to @v1 -> v2@.
class (VariadicLower v) => VariadicArg v where
-- | The type that the variadic guard corresponds to within the
-- monad @(m a)@.
type VariadicType v (m :: * -> *) a
validSatArg0 :: (SatisfyConstraint_ Zero c m)
=> Proxy c -> Proxy m -> Proxy v
-> SatisfyConstraint_ Zero c m :- SatV v Zero c m ~ v
default validSatArg0 :: (SatisfyConstraint_ Zero c m)
=> Proxy c -> Proxy m -> Proxy v
-> SatisfyConstraint_ Zero c m :- v ~ v
validSatArg0 _ _ _ = Sub Dict
validSatArg :: (SatisfyConstraint_ (Suc n) c m)
=> Proxy (Suc n) -> Proxy c -> Proxy m -> Proxy v
-> SatisfyConstraint_ (Suc n) c m
:- SatV v (Suc n) c m ~ SatV (LowerV v m) n c (LowerMonad m)
default validSatArg :: (SatisfyConstraint_ (Suc n) c m)
=> Proxy (Suc n) -> Proxy c -> Proxy m -> Proxy v
-> SatisfyConstraint_ (Suc n) c m
:- v ~ v
validSatArg _ _ _ _ = Sub Dict
-- | Variadic arguments that can be lowered. All 'VariadicArg' values
-- are instances of this class.
--
-- This actually defines how a variadic argument is lowered down to
-- the 'LowerMonad'.
class (VariadicArg v) => LowerableVArg v where
validLowerArg :: (MonadLevel m) => Proxy m -> Proxy v -> MonadLevel m :- LowerableVArg (LowerV v m)
default validLowerArg :: (MonadLevel m, LowerV v m ~ v)
=> Proxy m -> Proxy v -> MonadLevel m :- LowerableVArg v
validLowerArg _ _ = Sub Dict
lowerVArg :: (MonadLevel m, CanLower v m a)
=> Proxy v -> Proxy m -> Proxy a
-> VariadicType v m a
-> Unwrapper m a (LowerVArg v m a)
-- | In contrast to 'LowerableVArg', this class is for 'VariadicArg'
-- values that can be /lifted/ from the 'LowerMonad'.
--
-- This is important for @'Func' v1 v2@ arguments, as to lower a
-- function we need to /lift/ @v1@ before applying the function, and
-- then subsequently lower the result.
--
-- All instances of 'VariadicArg' are instances of this with the
-- exception of 'ValueOnly' (as it's not always possible to convert
-- an arbitrary @'InnerValue' m a@ back into an @a@).
class (VariadicArg v) => LiftableVArg v where
validLiftArg :: (MonadLevel m) => Proxy m -> Proxy v -> MonadLevel m :- LiftableVArg (LowerV v m)
default validLiftArg :: (MonadLevel m, LowerV v m ~ v)
=> Proxy m -> Proxy v -> MonadLevel m :- LiftableVArg v
validLiftArg _ _ = Sub Dict
liftVArg :: (MonadLevel m, CanLower v m a)
=> Proxy v -> Proxy m -> Proxy a
-> LowerVArg v m a
-> Unwrapper m a (VariadicType v m a)
-- | Variadic arguments that can be lifted via a call to 'wrap'. Only
-- those that have a 'VariadicType' that is a monadic value can thus
-- be instances of this class.
class (LiftableVArg v) => WrappableVArg v where
validWrapArg :: (MonadLevel m) => Proxy m -> Proxy v -> MonadLevel m :- WrappableVArg (LowerV v m)
default validWrapArg :: (MonadLevel m, LowerV v m ~ v)
=> Proxy m -> Proxy v -> MonadLevel m :- WrappableVArg v
validWrapArg _ _ = Sub Dict
wrapVArg :: (MonadLevel m, CanLower v m a)
=> Proxy v -> Proxy m -> Proxy a
-> Unwrapper m a (LowerVArg v m a) -> VariadicType v m a
type LowerVArg v m a = VariadicType (LowerV v m) (LowerMonad m) (InnerValue m a)
-- | A constant type that does not depend upon the current monadic
-- context. That is, @Const b@ corresponds to just @b@. It is kept
-- as-is when lowering through the different levels.
data Const (b :: *)
instance VariadicLower (Const b)
instance VariadicArg (Const b) where
type VariadicType (Const b) m a = b
instance LowerableVArg (Const b) where
lowerVArg _ _ _ b _ _ = b
instance LiftableVArg (Const b) where
liftVArg _ _ _ b _ _ = b
-- | Corresponds to @m a@.
data MonadicValue
instance VariadicLower MonadicValue
instance VariadicArg MonadicValue where
type VariadicType MonadicValue m a = m a
instance LowerableVArg MonadicValue where
lowerVArg _ pm pa m unwrap _ = unwrap m \\ (proofInst pm pa)
instance LiftableVArg MonadicValue where
liftVArg _ m a mv _ _ = wrap a (\ _ _ -> mv) \\ proofInst m a
instance WrappableVArg MonadicValue where
wrapVArg _ m a f = wrap a f \\ proofInst m a
-- | Whilst 'MonadLevel' requires @CanUnwrap m a a@ for all @a@, the
-- type system can't always determine this. This is a helper
-- function to do so.
proofInst :: (MonadLevel m) => Proxy m -> Proxy a -> (MonadLevel m :- CanUnwrap m a a)
proofInst _ _ = getUnwrapSelfProof
{-# INLINE proofInst #-}
-- | Corresponds to @m b@, where the final result is based upon @m a@.
-- This requires the extra constraint of @'CanUnwrap' m a b@.
data MonadicOther b
instance VariadicLower (MonadicOther b) where
type LowerV (MonadicOther b) m = MonadicOther (InnerValue m b)
type SatV (MonadicOther b) n c m = MonadicOther (SatValue_ n c m b)
type CanLower (MonadicOther b) m a = CanUnwrap m a b
instance VariadicArg (MonadicOther b) where
type VariadicType (MonadicOther b) m a = m b
validSatArg0 _ _ _ = Sub Dict
validSatArg _ _ _ _ = Sub Dict
instance LowerableVArg (MonadicOther b) where
validLowerArg _ _ = Sub Dict
lowerVArg _ _ _ m unwrap _ = unwrap m
instance LiftableVArg (MonadicOther b) where
validLiftArg _ _ = Sub Dict
liftVArg _ _ a m _ _ = wrap a (\ _ _ -> m)
instance WrappableVArg (MonadicOther b) where
validWrapArg _ _ = Sub Dict
wrapVArg _ _ a f = wrap a f
-- | Corresponds to @m (a,b)@. This requires the extra constraints of
-- @'CanAddInternal' m@ and @'AllowOtherValues' m ~ True@ (This is
-- used instead of 'CanUnwrap' as a simplification).
data MonadicTuple b
instance VariadicLower (MonadicTuple b) where
type CanLower (MonadicTuple b) m a = (CanGetInternal m, AllowOtherValues m ~ True)
instance VariadicArg (MonadicTuple b) where
type VariadicType (MonadicTuple b) m a = m (a,b)
instance (Monoid b) => LowerableVArg (MonadicTuple b) where
lowerVArg v _ a lm unwrap addI = fmap shiftI (unwrap lm)
where
b = tupleProxy v
ab = proxyPair a b
shiftI iv = let bv = getInternal addI mempty (snd . (`asProxyTypeOf` ab)) iv
in (mapInternal addI (fst . (`asProxyTypeOf` ab)) iv, bv)
tupleProxy :: Proxy (MonadicTuple b) -> Proxy b
tupleProxy _ = Proxy
{-# INLINE tupleProxy #-}
proxyPair :: Proxy a -> Proxy b -> Proxy (a,b)
proxyPair _ _ = Proxy
{-# INLINE proxyPair #-}
instance LiftableVArg (MonadicTuple b) where
liftVArg _ _ a mab _ addI = wrap a ( \ _ _ -> fmap shiftI mab)
where
shiftI (iva,b) = mapInternal addI ((,b) . (`asProxyTypeOf`a)) iva
instance WrappableVArg (MonadicTuple b) where
wrapVArg _ _ a f = wrap a ( \ unwrap addI -> fmap (shiftI addI) (f unwrap addI))
where
shiftI ai (iva, b) = mapInternal ai ((,b) . (`asProxyTypeOf`a)) iva
-- | This corresponds to @a@ when the final result is based upon @m
-- a@. This requires the extra constraint of @'CanAddInternal' m@.
data ValueOnly
instance VariadicLower ValueOnly where
type CanLower ValueOnly m a = CanAddInternal m
instance VariadicArg ValueOnly where
type VariadicType ValueOnly m a = a
instance LowerableVArg ValueOnly where
lowerVArg _ _ _ a _ addI = addInternal addI a \\ addIntProof addI
-- | Represents the function @v1 -> v2@.
data Func (v1 :: *) (v2 :: *)
pfa :: Proxy (Func a b) -> Proxy a
pfa _ = Proxy
pfb :: Proxy (Func a b) -> Proxy b
pfb _ = Proxy
instance (VariadicLower a, VariadicLower b) => VariadicLower (Func a b) where
type LowerV (Func va vb) m = Func (LowerV va m) (LowerV vb m)
type SatV (Func va vb) n c m = Func (SatV va n c m) (SatV vb n c m)
type CanLower (Func va vb) m a = ((CanLower va m a), (CanLower vb m a))
instance (VariadicArg va, VariadicArg vb) => VariadicArg (Func va vb) where
type VariadicType (Func va vb) m a = VariadicType va m a -> VariadicType vb m a
validSatArg0 c m f = Sub Dict \\ validSatArg0 c m (pfa f)
\\ validSatArg0 c m (pfb f)
validSatArg n c m f = Sub Dict \\ validSatArg n c m (pfa f)
\\ validSatArg n c m (pfb f)
instance (LiftableVArg va, LowerableVArg vb) => LowerableVArg (Func va vb) where
validLowerArg m f = Sub Dict \\ validLiftArg m (pfa f)
\\ validLowerArg m (pfb f)
-- lower . f . lift
lowerVArg pf m a f unwrap addI
= (\ v -> lowerVArg (pfb pf) m a v unwrap addI)
. f
. (\ v -> liftVArg (pfa pf) m a v unwrap addI)
instance (LowerableVArg va, LiftableVArg vb) => LiftableVArg (Func va vb) where
validLiftArg m f = Sub Dict \\ validLowerArg m (pfa f)
\\ validLiftArg m (pfb f)
-- lift . f . lower
liftVArg pf m a f unwrap addI
= (\ v -> liftVArg (pfb pf) m a v unwrap addI)
. f
. (\ v -> lowerVArg (pfa pf) m a v unwrap addI)
-- | A function composed of variadic arguments that produces a value
-- based upon the type @m a@.
class (VariadicLower f) => VariadicFunction f where
-- | The function (that produces a value based upon the type @m a@)
-- that this instance corresponds to.
type VarFunction f (m :: * -> *) a
validLowerFunc :: (MonadLevel m) => Proxy m -> Proxy f -> MonadLevel m :- VariadicFunction (LowerV f m)
validSatFunc0 :: (SatisfyConstraint_ Zero c m)
=> Proxy c -> Proxy m -> Proxy f
-> SatisfyConstraint_ Zero c m :- SatV f Zero c m ~ f
validSatFunc :: (SatisfyConstraint_ (Suc n) c m)
=> Proxy (Suc n) -> Proxy c -> Proxy m -> Proxy f
-> SatisfyConstraint_ (Suc n) c m
:- SatV f (Suc n) c m ~ SatV (LowerV f m) n c (LowerMonad m)
applyVFn :: (MonadLevel m, CanLower f m a)
=> Proxy f -> Proxy m -> Proxy a
-> Unwrapper m a (VarFunctionLower f m a)
-> VarFunction f m a
type VarFunctionLower f (m :: * -> *) a = VarFunction (LowerV f m) (LowerMonad m) (InnerValue m a)
-- | The function represented by the 'VariadicFunction' when lowered
-- to the satisfying monad.
type VarFunctionSat f n c m a = VarFunction (SatV f n c m) (SatMonad_ n c m) (SatValue_ n c m a)
plowerF :: (MonadLevel m, VariadicFunction f) => Proxy m -> Proxy f -> Proxy (LowerV f m)
plowerF _ _ = Proxy
-- | The fundamental way of creating a 'VariadicFunction'. @MkVarFn
-- v@ corresponds to a function of type @'VariadicType' v m a -> m
-- a@ for some specified @m a@.
--
-- If more than one argument is needed for a function, they can be
-- prepended on using 'Func'.
type MkVarFn v = Func v (MkVarFnFrom MonadicValue)
-- | The result of a 'VariadicFunction'. This can't be used on its
-- own, and needs to have at least one 'Func' attached to it.
data MkVarFnFrom va
pmvff :: Proxy (MkVarFnFrom va) -> Proxy va
pmvff _ = Proxy
instance (VariadicLower va) => VariadicLower (MkVarFnFrom va) where
type LowerV (MkVarFnFrom va) m = MkVarFnFrom (LowerV va m)
type SatV (MkVarFnFrom va) n c m = MkVarFnFrom (SatV va n c m)
type CanLower (MkVarFnFrom va) m a = CanLower va m a
instance (WrappableVArg va) => VariadicFunction (MkVarFnFrom va) where
type VarFunction (MkVarFnFrom va) m a = VariadicType va m a
validLowerFunc m pmf = Sub Dict \\ validWrapArg m (pmvff pmf)
validSatFunc0 c m pmf = Sub Dict \\ validSatArg0 c m (pmvff pmf)
validSatFunc n c m pmf = Sub Dict \\ validSatArg n c m (pmvff pmf)
applyVFn pmf m a f = wrapVArg (pmvff pmf) m a f
instance (LowerableVArg va, VariadicFunction vf) => VariadicFunction (Func va vf) where
type VarFunction (Func va vf) m a = (VariadicType va m a) -> VarFunction vf m a
validLowerFunc m f = Sub Dict \\ validLowerArg m (pfa f)
\\ validLowerFunc m (pfb f)
validSatFunc0 c m f = Sub Dict \\ validSatArg0 c m (pfa f)
\\ validSatFunc0 c m (pfb f)
validSatFunc n c m f = Sub Dict \\ validSatArg n c m (pfa f)
\\ validSatFunc n c m (pfb f)
applyVFn pf m a f va = applyVFn (pfb pf) m a
(\ unwrap addI ->
f unwrap addI (lowerVArg (pfa pf) m a va unwrap addI))
-- -----------------------------------------------------------------------------