diff --git a/benchmarks/Dynamic.hs b/benchmarks/Dynamic.hs
--- a/benchmarks/Dynamic.hs
+++ b/benchmarks/Dynamic.hs
@@ -1,7 +1,7 @@
 {-# OPTIONS_GHC -fcontext-stack=100 #-}
 
 import Criterion.Main
-import Criterion.Config
+import Criterion.Types
 import Data.Monoid
 
 import Data.TypeRep
@@ -25,10 +25,10 @@
 dynListBase n = concat [[Base.toDyn i, Base.toDyn (even i)] | i <- [0..n]]
 
 dynSum :: [Dynamic Types] -> Int
-dynSum ds = sum [i | d <- ds, Just i <- [fromDyn d]]
+dynSum ds = sum [i | d <- ds, Right i <- [fromDyn d]]
 
 dynSum2 :: [Dynamic Types2] -> Int
-dynSum2 ds = sum [i | d <- ds, Just i <- [fromDyn d]]
+dynSum2 ds = sum [i | d <- ds, Right i <- [fromDyn d]]
 
 dynSumBase :: [Base.Dynamic] -> Int
 dynSumBase ds = sum [i | d <- ds, Just i <- [Base.fromDynamic d]]
@@ -43,15 +43,16 @@
 testDynBase = dynSumBase . dynListBase
 
 main :: IO ()
-main = defaultMainWith (defaultConfig {cfgSummaryFile = Last $ Just "bench-results/dynamic.csv"}) (return ())
+main = defaultMainWith (defaultConfig {csvFile = Just "bench-results/dynamic.csv"})
     [ bgroup "size=1000"
-       [ bench "testDyn"     $ nf testDyn     1000
-       , bench "testDyn2"    $ nf testDyn2    1000
-       , bench "testDynBase" $ nf testDynBase 1000
-       ]
+        [ bench "testDyn"     $ nf testDyn     1000
+        , bench "testDyn2"    $ nf testDyn2    1000
+        , bench "testDynBase" $ nf testDynBase 1000
+        ]
     , bgroup "size=2000"
-       [ bench "testDyn"     $ nf testDyn     2000
-       , bench "testDyn2"    $ nf testDyn2    2000
-       , bench "testDynBase" $ nf testDynBase 2000
-       ]
+        [ bench "testDyn"     $ nf testDyn     2000
+        , bench "testDyn2"    $ nf testDyn2    2000
+        , bench "testDynBase" $ nf testDynBase 2000
+        ]
     ]
+
diff --git a/examples/Simple.hs b/examples/Simple.hs
--- a/examples/Simple.hs
+++ b/examples/Simple.hs
@@ -8,13 +8,15 @@
 hlist = [toDyn True, toDyn (1 :: Int)]
   -- Prints: [True,1]
 
-addDyn :: (TypeEq ts ts, PWitness Num ts ts) => Dynamic ts -> Dynamic ts -> Maybe (Dynamic ts)
+addDyn :: (TypeEq ts ts, PWitness Num ts ts) =>
+    Dynamic ts -> Dynamic ts -> Either String (Dynamic ts)
 addDyn (Dyn ta a) (Dyn tb b) = do
     Dict <- typeEq ta tb
     Dict <- pwit pNum ta
     return (Dyn ta (a+b))
 
 
+
 test1 = toDyn (1 :: Int) `addDyn` toDyn (2 :: Int)
   -- Prints: Just 3
 
@@ -24,5 +26,5 @@
     putStrLn "All tests passed"
   where
     t1 = show hlist == "[True,1]"
-    t2 = show (test1 :: Maybe (Dynamic MyUniverse)) == "Just 3"
+    t2 = show (test1 :: Either String (Dynamic MyUniverse)) == "Right 3"
 
diff --git a/open-typerep.cabal b/open-typerep.cabal
--- a/open-typerep.cabal
+++ b/open-typerep.cabal
@@ -1,5 +1,5 @@
 name:                open-typerep
-version:             0.2
+version:             0.3.1
 synopsis:            Open type representations and dynamic types
 description:         This package uses Data Types à la Carte to provide open type representations
                      and dynamic types/coercions for open type universes.
@@ -39,7 +39,6 @@
 stability:           experimental
 build-type:          Simple
 cabal-version:       >=1.10
-tested-with:         GHC==7.6.2, GHC==7.8.2
 
 extra-source-files:
   examples/*.hs
@@ -52,8 +51,9 @@
   hs-source-dirs: src
 
   exposed-modules:
-    Data.TypeRep
     Data.TypeRep.Internal
+    Data.TypeRep
+    Data.TypeRep.VarArg
 
   other-modules:
     Data.TypeRep.Sub
@@ -61,16 +61,19 @@
   build-depends:
     base        >=4 && <5,
     constraints >=0.3,
+    mtl         >=2.1,
     syntactic   >=2.0,
     tagged      >=0.4
 
   default-language: Haskell2010
 
   default-extensions:
+    ConstraintKinds
     FlexibleContexts
     FlexibleInstances
     GADTs
     MultiParamTypeClasses
+    Rank2Types
     ScopedTypeVariables
     TypeFamilies
     TypeOperators
@@ -108,7 +111,7 @@
 
   build-depends:
     base,
-    criterion,
+    criterion >= 1,
     open-typerep
 
   default-language: Haskell2010
diff --git a/src/Data/TypeRep/Internal.hs b/src/Data/TypeRep/Internal.hs
--- a/src/Data/TypeRep/Internal.hs
+++ b/src/Data/TypeRep/Internal.hs
@@ -6,7 +6,10 @@
 
 
 
-import Data.Constraint (Dict (..))
+import Control.Monad.Except
+import Data.Char (isAlphaNum)
+
+import Data.Constraint (Constraint, Dict (..))
 import Data.Proxy (Proxy (..))
 
 import Data.Syntactic
@@ -49,31 +52,38 @@
 typeRep = TypeRep typeRep'
 
 -- | Equality on type representations
-class TypeEq t u
+class Render t => TypeEq t u
   where
     typeEqSym
         :: (t sig1, Args (AST u) sig1)
         -> (t sig2, Args (AST u) sig2)
-        -> Maybe (Dict (DenResult sig1 ~ DenResult sig2))
+        -> Either String (Dict (DenResult sig1 ~ DenResult sig2))
+  -- The reason to have `Render` as a super class is not to leak unnecessary stuff in the type of
+  -- `typeEq`.
 
 instance (TypeEq t1 t, TypeEq t2 t) => TypeEq (t1 :+: t2) t
   where
     typeEqSym (InjL t1, as1) (InjL t2, as2) = typeEqSym (t1,as1) (t2,as2)
     typeEqSym (InjR t1, as1) (InjR t2, as2) = typeEqSym (t1,as1) (t2,as2)
-    typeEqSym _ _ = Nothing
-
-instance TypeEq t t => TypeEq (AST t) t
-  where
-    typeEqSym (Sym t1, as1)   (Sym t2, as2)   = typeEqSym (t1,as1) (t2,as2)
-    typeEqSym (s1 :$ a1, as1) (s2 :$ a2, as2) = typeEqSym (s1, a1 :* as1) (s2, a2 :* as2)
+    typeEqSym _ _ = throwError ""
 
 instance TypeEq Empty t
   where
     typeEqSym = error "typeEqSym: Empty"
 
 -- | Equality on type representations
-typeEq :: forall t a b . TypeEq t t => TypeRep t a -> TypeRep t b -> Maybe (Dict (a ~ b))
-typeEq (TypeRep s1) (TypeRep s2) = typeEqSym (s1, Nil :: Args (AST t) (Full a)) (s2, Nil)
+typeEq :: (TypeEq t t, MonadError String m) => TypeRep t a -> TypeRep t b -> m (Dict (a ~ b))
+typeEq t1@(TypeRep s1) t2@(TypeRep s2) = case go (s1, Nil) (s2, Nil) of
+    Left _     -> throwError $ "type mismatch: " ++ show t1 ++ " /= " ++ show t2
+    Right Dict -> return Dict
+  where
+    go :: TypeEq t t
+      => (AST t sig1, Args (AST t) sig1)
+      -> (AST t sig2, Args (AST t) sig2)
+      -> Either String (Dict ((DenResult sig1 ~ DenResult sig2)))
+    go (Sym t1, as1)   (Sym t2, as2)   = typeEqSym (t1,as1) (t2,as2)
+    go (s1 :$ a1, as1) (s2 :$ a2, as2) = go (s1, a1 :* as1) (s2, a2 :* as2)
+    go _ _ = throwError ""
 
 -- | Type constructor matching. This function makes it possible to match on type representations
 -- without dealing with the underlying 'AST' representation.
@@ -101,6 +111,12 @@
 matchConM :: Monad m => TypeRep t c -> m [E (TypeRep t)]
 matchConM = return . matchCon
 
+-- | Show the name of type classes
+class ShowClass (p :: * -> Constraint)
+  where
+    -- | Show the name of a type class
+    showClass :: Proxy p -> String
+
 -- | Witness a type constraint for a reified type
 class Witness p t u
   where
@@ -117,47 +133,57 @@
     witSym (s :$ a) as = witSym s (a :* as)
 
 -- | Partially witness a type constraint for a reified type
-class PWitness p t u
+class (ShowClass p, Render t) => PWitness p t u
   where
-    pwitSym :: t sig -> Args (AST u) sig -> Maybe (Dict (p (DenResult sig)))
-    pwitSym _ _ = Nothing
+    pwitSym :: t sig -> Args (AST u) sig -> Either String (Dict (p (DenResult sig)))
+    pwitSym _ _ = throwError ""
+  -- The reason to have `Render` as a super class is not to leak unnecessary stuff in the type of
+  -- `pwit`.
 
 instance (PWitness p t1 t, PWitness p t2 t) => PWitness p (t1 :+: t2) t
   where
     pwitSym (InjL s) as = pwitSym s as
     pwitSym (InjR s) as = pwitSym s as
 
-instance PWitness p t t => PWitness p (AST t) t
-  where
-    pwitSym (Sym s)  as = pwitSym s as
-    pwitSym (s :$ a) as = pwitSym s (a :* as)
-
 -- | Default implementation of 'pwitSym' for types that have a 'Witness' instance
-pwitSymDefault :: Witness p t u => t sig -> Args (AST u) sig -> Maybe (Dict (p (DenResult sig)))
-pwitSymDefault t = Just . witSym t
+pwitSymDefault :: Witness p t u =>
+    t sig -> Args (AST u) sig -> Either String (Dict (p (DenResult sig)))
+pwitSymDefault t = return . witSym t
 
 -- | Witness a type constraint for a reified type
 wit :: forall p t a . Witness p t t => Proxy p -> TypeRep t a -> Dict (p a)
 wit _ (TypeRep a) = witSym a (Nil :: Args (AST t) (Full a))
 
 -- | Partially witness a type constraint for a reified type
-pwit :: forall p t a . PWitness p t t => Proxy p -> TypeRep t a -> Maybe (Dict (p a))
-pwit _ (TypeRep a) = pwitSym a (Nil :: Args (AST t) (Full a))
+pwit :: forall p t m a . (PWitness p t t, MonadError String m) =>
+    Proxy p -> TypeRep t a -> m (Dict (p a))
+pwit p t@(TypeRep a) = case go a Nil of
+    Left _  -> throwError $ unwords ["cannot deduce", showClass p, classArg]
+    Right a -> return a
+  where
+    st       = show t
+    classArg = if all isAlphaNum st then st else "(" ++ st ++ ")"
 
+    go :: AST t sig -> Args (AST t) sig -> Either String (Dict (p (DenResult sig)))
+    go (Sym s)  as = pwitSym s as
+    go (s :$ a) as = go s (a :* as)
 
 
+
 ----------------------------------------------------------------------------------------------------
 -- * Dynamic types
 ----------------------------------------------------------------------------------------------------
 
 -- | Safe cast (does not use @unsafeCoerce@)
-cast :: forall t a b . (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> a -> Maybe b
+cast :: forall t a b . (Typeable t a, Typeable t b, TypeEq t t) =>
+    Proxy t -> a -> Either String b
 cast _ a = do
     Dict <- typeEq (typeRep :: TypeRep t a) (typeRep :: TypeRep t b)
     return a
 
 -- | Safe generalized cast (does not use @unsafeCoerce@)
-gcast :: forall t a b c . (Typeable t a, Typeable t b, TypeEq t t) => Proxy t -> c a -> Maybe (c b)
+gcast :: forall t a b c . (Typeable t a, Typeable t b, TypeEq t t) =>
+    Proxy t -> c a -> Either String (c b)
 gcast _ a = do
     Dict <- typeEq (typeRep :: TypeRep t a) (typeRep :: TypeRep t b)
     return a
@@ -170,7 +196,7 @@
 toDyn :: Typeable t a => a -> Dynamic t
 toDyn = Dyn typeRep
 
-fromDyn :: forall t a . (Typeable t a, TypeEq t t) => Dynamic t -> Maybe a
+fromDyn :: forall t a . (Typeable t a, TypeEq t t) => Dynamic t -> Either String a
 fromDyn (Dyn t a) = do
     Dict <- typeEq t (typeRep :: TypeRep t a)
     return a
@@ -178,8 +204,8 @@
 instance (TypeEq t t, Witness Eq t t) => Eq (Dynamic t)
   where
     Dyn ta a == Dyn tb b
-        | Just Dict <- typeEq ta tb
-        , Dict      <- wit pEq ta
+        | Right Dict <- typeEq ta tb
+        , Dict       <- wit pEq ta
         = a == b
     _ == _ = False
 
@@ -197,12 +223,20 @@
 class    Any a
 instance Any a
 
+instance ShowClass Any          where showClass _ = "Any"
+instance ShowClass Eq           where showClass _ = "Eq"
+instance ShowClass Ord          where showClass _ = "Ord"
+instance ShowClass Show         where showClass _ = "Show"
+instance ShowClass Num          where showClass _ = "Num"
+instance ShowClass Integral     where showClass _ = "Integral"
+instance ShowClass (Typeable t) where showClass _ = "Typeable ..."
+
 -- | Witness a 'Typeable' constraint for a reified type
 witTypeable :: Witness (Typeable t) t t => TypeRep t a -> Dict (Typeable t a)
 witTypeable = wit Proxy
 
 -- | Partially witness a 'Typeable' constraint for a reified type
-pwitTypeable :: PWitness (Typeable t) t t => TypeRep t a -> Maybe (Dict (Typeable t a))
+pwitTypeable :: PWitness (Typeable t) t t => TypeRep t a -> Either String (Dict (Typeable t a))
 pwitTypeable = pwit Proxy
 
 pAny :: Proxy Any
@@ -293,10 +327,10 @@
 instance (ListType  :<: t, Typeable t a)               => Typeable t [a]      where typeRep' = listType typeRep'
 instance (FunType   :<: t, Typeable t a, Typeable t b) => Typeable t (a -> b) where typeRep' = funType typeRep' typeRep'
 
-instance TypeEq BoolType  t where typeEqSym (BoolType, Nil)  (BoolType, Nil)  = Just Dict
-instance TypeEq CharType  t where typeEqSym (CharType, Nil)  (CharType, Nil)  = Just Dict
-instance TypeEq IntType   t where typeEqSym (IntType, Nil)   (IntType, Nil)   = Just Dict
-instance TypeEq FloatType t where typeEqSym (FloatType, Nil) (FloatType, Nil) = Just Dict
+instance TypeEq BoolType  t where typeEqSym (BoolType, Nil)  (BoolType, Nil)  = return Dict
+instance TypeEq CharType  t where typeEqSym (CharType, Nil)  (CharType, Nil)  = return Dict
+instance TypeEq IntType   t where typeEqSym (IntType, Nil)   (IntType, Nil)   = return Dict
+instance TypeEq FloatType t where typeEqSym (FloatType, Nil) (FloatType, Nil) = return Dict
 
 instance TypeEq t t => TypeEq ListType t
   where
@@ -342,12 +376,12 @@
 instance Witness Any ListType  t where witSym _ _ = Dict
 instance Witness Any FunType   t where witSym _ _ = Dict
 
-instance PWitness Any BoolType  t where pwitSym _ _ = Just Dict
-instance PWitness Any CharType  t where pwitSym _ _ = Just Dict
-instance PWitness Any IntType   t where pwitSym _ _ = Just Dict
-instance PWitness Any FloatType t where pwitSym _ _ = Just Dict
-instance PWitness Any ListType  t where pwitSym _ _ = Just Dict
-instance PWitness Any FunType   t where pwitSym _ _ = Just Dict
+instance PWitness Any BoolType  t where pwitSym _ _ = return Dict
+instance PWitness Any CharType  t where pwitSym _ _ = return Dict
+instance PWitness Any IntType   t where pwitSym _ _ = return Dict
+instance PWitness Any FloatType t where pwitSym _ _ = return Dict
+instance PWitness Any ListType  t where pwitSym _ _ = return Dict
+instance PWitness Any FunType   t where pwitSym _ _ = return Dict
 
 instance                   Witness Eq BoolType  t where witSym BoolType  Nil = Dict
 instance                   Witness Eq CharType  t where witSym CharType  Nil = Dict
@@ -407,8 +441,8 @@
 instance PWitness Integral ListType  t
 instance PWitness Integral FunType   t
 
-dynToInteger :: PWitness Integral t t => Dynamic t -> Maybe Integer
-dynToInteger (Dyn tr a)
-    | Just Dict <- pwit pIntegral tr = Just (toInteger a)
-dynToInteger _ = Nothing
+dynToInteger :: PWitness Integral t t => Dynamic t -> Either String Integer
+dynToInteger (Dyn tr a) = do
+    Dict <- pwit pIntegral tr
+    return (toInteger a)
 
diff --git a/src/Data/TypeRep/Sub.hs b/src/Data/TypeRep/Sub.hs
--- a/src/Data/TypeRep/Sub.hs
+++ b/src/Data/TypeRep/Sub.hs
@@ -1,12 +1,24 @@
-{-# LANGUAGE OverlappingInstances #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE UndecidableInstances #-}
 
+#ifndef MIN_VERSION_GLASGOW_HASKELL
+#define MIN_VERSION_GLASGOW_HASKELL(a,b,c,d) 0
+#endif
+  -- MIN_VERSION_GLASGOW_HASKELL was introduced in GHC 7.10
+
+#if MIN_VERSION_GLASGOW_HASKELL(7,10,0,0)
+#else
+{-# LANGUAGE OverlappingInstances #-}
+#endif
+
 -- | This module is only to limit the scope of the @OverlappingInstances@ flag
 
 module Data.TypeRep.Sub where
 
+-- TODO Merge this module with `Data.TypeRep.Internal` when support for < 7.10 is dropped
 
 
+
 import Data.Syntactic
 
 import Data.TypeRep.Internal
@@ -23,11 +35,12 @@
     -- | Cast a type representation to a larger universe
     weakenUniverse :: TypeRep sub a -> TypeRep sup a
 
-instance SubUniverse t t
+
+instance {-# OVERLAPPING #-} SubUniverse t t
   where
     weakenUniverse = id
 
-instance (SubUniverse sub sup', sup ~ (t :+: sup')) => SubUniverse sub sup
+instance {-# OVERLAPPING #-} (SubUniverse sub sup', sup ~ (t :+: sup')) => SubUniverse sub sup
   where
     weakenUniverse = sugar . mapAST InjR . desugar . weakenUniverse
 
diff --git a/src/Data/TypeRep/VarArg.hs b/src/Data/TypeRep/VarArg.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/TypeRep/VarArg.hs
@@ -0,0 +1,181 @@
+-- | Utilities for polyvariadic functions
+
+module Data.TypeRep.VarArg where
+
+
+
+import Control.Monad.Except
+
+import Data.Syntactic
+import Data.TypeRep
+import Data.TypeRep.Internal
+
+
+
+----------------------------------------------------------------------------------------------------
+-- * Working with polyvariadic functions
+----------------------------------------------------------------------------------------------------
+
+-- | Newtype marking the result of a N-ary function
+newtype Res a = Res a
+
+-- | Put a 'Res' marker at the result type of a function
+--
+-- > ToRes (a -> b -> ... -> x) = a -> b -> ... -> Res x
+type family ToRes a where
+  ToRes (a -> b) = a -> ToRes b
+  ToRes a        = Res a
+
+-- | Remove the 'Res' marker at the result type of a function
+--
+-- > FromRes (a -> b -> ... -> Res x) = a -> b -> ... -> x
+type family FromRes a where
+  FromRes (a -> b) = a -> FromRes b
+  FromRes (Res a)  = a
+
+-- | Witness of the arity of a function. 'Arity' will normally be indexed by @(`ToRes` a)@.
+data Arity a
+  where
+    FunRes :: Arity (Res a)
+    FunArg :: Arity b -> Arity (a -> b)
+
+class VarArg t
+  where
+    aritySym :: VarArg u => t sig -> Args (AST u) sig -> Arity (ToRes (DenResult sig))
+    fromResInvSym :: (VarArg u, a ~ DenResult sig) =>
+        t sig -> Args (AST u) sig -> Dict (FromRes (ToRes a) ~ a)
+
+instance (VarArg t1, VarArg t2) => VarArg (t1 :+: t2)
+  where
+    aritySym      (InjL t) = aritySym t
+    aritySym      (InjR t) = aritySym t
+    fromResInvSym (InjL t) = fromResInvSym t
+    fromResInvSym (InjR t) = fromResInvSym t
+
+instance VarArg BoolType
+  where
+    aritySym BoolType Nil      = FunRes
+    fromResInvSym BoolType Nil = Dict
+
+instance VarArg CharType
+  where
+    aritySym CharType Nil      = FunRes
+    fromResInvSym CharType Nil = Dict
+
+instance VarArg IntType
+  where
+    aritySym IntType Nil      = FunRes
+    fromResInvSym IntType Nil = Dict
+
+instance VarArg FloatType
+  where
+    aritySym FloatType Nil      = FunRes
+    fromResInvSym FloatType Nil = Dict
+
+instance VarArg ListType
+  where
+    aritySym ListType _      = FunRes
+    fromResInvSym ListType _ = Dict
+
+instance VarArg FunType
+  where
+    aritySym FunType (_ :* b :* Nil) = FunArg $ arity $ TypeRep b
+    fromResInvSym FunType (_ :* b :* Nil)
+        | Dict <- fromResInv $ TypeRep b = Dict
+
+-- | Get the 'Arity' of a type. The purpose is to be able to distinguish between functions and
+-- non-functions without having to handle all cases of a 'TypeRep'.
+arity :: VarArg t => TypeRep t a -> Arity (ToRes a)
+arity = simpleMatch aritySym . unTypeRep
+
+-- | Prove that 'FromRes' is the inverse of 'ToRes'
+fromResInv :: VarArg t => TypeRep t a -> Dict (FromRes (ToRes a) ~ a)
+fromResInv = simpleMatch fromResInvSym . unTypeRep
+
+-- TODO With injective type families `fromResInv` is probably not going to be needed:
+--
+--   https://ghc.haskell.org/trac/ghc/ticket/6018
+
+type NonFunction a = ToRes a ~ Res a
+
+-- | Attempt to prove that a type is not a function type
+nonFunction :: (VarArg t, MonadError String m) => TypeRep t a -> m (Dict (NonFunction a))
+nonFunction t | Dict <- fromResInv t = case arity t of
+    FunRes -> return Dict
+    _      -> throwError "nonFunction: function type"
+
+
+
+----------------------------------------------------------------------------------------------------
+-- * N-ary monadic functions
+----------------------------------------------------------------------------------------------------
+
+-- | Give a function a monadic result type. @(`FunM` m)@ will normally be indexed by @(`ToRes` a)@.
+--
+-- > FunM m (a -> b -> ... -> Res x) = a -> b -> ... -> m x
+type family FunM m a where
+  FunM m (a -> b) = a -> FunM m b
+  FunM m (Res a)  = m a
+
+-- | Lift a function to a similar function with monadic result type
+--
+-- > liftMonadic _ _ f = \a b ... x -> return (f a b ... x)
+liftMonadic :: forall t a m . (VarArg t, Monad m) => Proxy m -> TypeRep t a -> a -> FunM m (ToRes a)
+liftMonadic _ t f | Dict <- fromResInv t = go (arity t) f
+  where
+    go :: (FromRes (ToRes b) ~ b) => Arity (ToRes b) -> b -> FunM m (ToRes b)
+    go FunRes     a = return a
+    go (FunArg b) f = \a -> go b (f a)
+
+-- | Run the result of a monadic function
+--
+-- > runMonadic run _ f = \a b ... x -> run (f a b ... x)
+runMonadic :: forall t a m . VarArg t =>
+    (forall a . m a -> a) -> TypeRep t a -> FunM m (ToRes a) -> a
+runMonadic run t f | Dict <- fromResInv t = go (arity t) f
+  where
+    go :: (FromRes (ToRes b) ~ b) => Arity (ToRes b) -> FunM m (ToRes b) -> b
+    go FunRes a     = run a
+    go (FunArg b) f = \a -> go b (f a)
+
+-- | Compose a function with an N-ary monadic function
+--
+-- > compMonadic f _ g = \a b ... x -> f (g a b ... x)
+compMonadic :: forall t a m1 m2 . VarArg t =>
+    (forall a . m1 a -> m2 a) -> TypeRep t a -> FunM m1 (ToRes a) -> FunM m2 (ToRes a)
+compMonadic f t g | Dict <- fromResInv t = go (Proxy :: Proxy a) (arity t) g
+  where
+    go :: (FromRes (ToRes b) ~ b) =>
+        Proxy b -> Arity (ToRes b) -> FunM m1 (ToRes b) -> FunM m2 (ToRes b)
+    go _ FunRes a        = f a
+    go _ fa@(FunArg b) g = \a -> go (mkProxy fa) b (g a)
+      where
+        mkProxy = const Proxy :: Arity (x -> y) -> Proxy (FromRes y)
+
+-- | Give a function monadic arguments and result type. @(`FunM2` m)@ will normally be indexed by
+-- @(`ToRes` a)@.
+--
+-- > FunM m (a -> b -> ... -> Res x) = m a -> m b -> ... -> m x
+type family FunM2 m a where
+  FunM2 m (a -> b) = m a -> FunM2 m b
+  FunM2 m (Res a)  = m a
+
+-- | Lift a function to a similar function with monadic arguments and result
+--
+-- > liftMonadic f = \ma mb ... mx -> do
+-- >     a <- ma
+-- >     b <- mb
+-- >     ...
+-- >     x <- mx
+-- >     return (f a b ... x)
+liftMonadic2 :: forall t a m . (VarArg t, Monad m) =>
+    Proxy m -> TypeRep t a -> a -> FunM2 m (ToRes a)
+liftMonadic2 _ t f | Dict <- fromResInv t = go (arity t) (return f)
+  where
+    go :: (FromRes (ToRes b) ~ b) => Arity (ToRes b) -> m b -> FunM2 m (ToRes b)
+    go FunRes     ma = ma
+    go (FunArg b) mf = \ma -> go b $ do
+        f <- mf
+        a <- ma
+        return (f a)
+