(See http://stackoverflow.com/a/31223058/2476735)

BothWithMoreTypeLevelFns.hs

-- The following lets you write:
--   ghci> both @All Proxy (Proxy :: Proxy (TyApp Maybe)) Just (1, 'a')
--   (Just 1,Just 'a')
--
-- The type involved in that example is:
--   ghci> :t both @All Proxy (Proxy :: Proxy (TyApp Maybe))
--   both @All Proxy (Proxy :: Proxy (TyApp Maybe))
--     :: (forall r x. (All x, TyApp Maybe x r) => x -> r)
--        -> (a, b) -> (Maybe a, Maybe b)

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TypeFamilies #-}
{-# LANGUAGE RankNTypes, ConstraintKinds #-}

import GHC.Exts (Constraint)
import Data.Proxy

both :: (c a, c b
        ,p a r1  -- p is a relation between a and r1
        ,p b r2  -- and also a relation between b and r2
        )
     => Proxy c
        -> Proxy p
        -> (forall r x. (c x, p x r) => x -> r) -- An input type x and a corresponding
                                                -- result type r are valid iff the p from
                                                -- before is a relation between x and r,
                                                -- where x is an instance of c
        -> (a, b)
        -> (r1, r2)
both Proxy Proxy f (x, y) = (f x, f y)

class fa ~ f a => TyApp f a fa
instance TyApp f a (f a)

class All a
instance All a