Sum of indexed functors

Question

In Slicing It, Conor McBride develops indexed functors, and then describes their sums and products on a slide "Sum and Product" (slides are unlabelled, about 90% into the presentation). This slide begins

-- sum - choose between compatible structures
data (:+:) :: (i ->- o) -> (i ->- o) -> (i ->- o) where
    L :: s x :-> (s :+: t) x
    R :: t x :-> (s :+: t) x
instance (IFunctor s, IFunctor t) => IFunctor (s :+: t) where
    imap f (L sx) = L (imap f sx)
    imap f (R tx) = R (imap f tx)

In particular, this definition of :+: requires that both indexed functors have the same source index i. I wonder why this is the case. Can this be relaxed e.g. to allowing

-- sum - choose between compatible structures
data (:+:) :: (i ->- o) -> (j ->- o) -> (Either i j ->- o) where
    L :: s x :-> (s :+: t) x
    R :: t x :-> (s :+: t) x

where i and j are now different types?

Answer 1

@chi Thanks for your pointer. It turns out I was wrong -- my suggestion doesn't work, it is not possible to combine different inputs. However, it is possible to use Either for the output kinds, leading to the constructor @chi suggested:

data (:+:) :: (i ->- o) -> (i ->- u) -> (i ->- Either o u) where
    L :: s x o -> (s :+: t) x ('Left o)
    R :: t x u -> (s :+: t) x ('Right u)

Both the :+: and the :*: types on the slides take two types as arguments, i.e. essentially a pair of arguments. I believe my suggestion might work if they took an alternative (i.e. an Either) of type arguments, as in

data (:|:) :: Either (i ->- o) (j ->- o) -> (Either i j ->- o)