Feature request: Generalize :&:

[liarokapisv]

It would be very useful to have an indexed version of :&:.
Basically the alternative definition referenced in the docs:

This data type adds a constant product to a signature. Alternatively, this could have also been defined as
data (f :&': a) (g :: * -> *) e = f g e :&': a e
This is too general, however, for example for productHHom.

(I can't find any reference to productHHom.)

It also seems that the original :&: can be retrieved by just using a type synonym along with K:

type f :&: a = f :&': K a

In contrast the indexed version cannot be defined as a partially applied type synonym:

-- We can't do this, i is not visible:
-- type f :&': a = f :&: (a i) 
-- Instead we have to do this:
type (f :&': a) r i = (f :&: a i) r i

Unfortunately this means we can't use :&': with Term since we can't partially apply it. Therefore I think that working with the indexed version and retrieving the original with a type synonym would be more flexible. Here is an example where the indexed version is very useful. Note that for LNodeF we could use the original type while for ANodeF we need the indexed version.

Kinds regards.