Generics: Documentation of `:.:` + formulate `Rec1` in terms of `:.:` and `Par1`?

I was a bit confused when I investigated the Rep1 representation of the following nested datatype:

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveFunctor #-}

module Lib where

import GHC.Generics

data Fork a = Fork a a
  deriving (Generic, Functor, Generic1)
data Perfect a = Zero a | Succ (Perfect (Fork a))
  deriving (Generic, Functor, Generic1)

In GHCi, I get (after stripping off metadata)

> :kind! Rep1 Perfect
Rep1 Perfect :: * -> *
= Par1 :+: (Perfect :.: Rec1 Fork)

Similarly to the definition of rose trees in https://hackage.haskell.org/package/base-4.16.0.0/docs/GHC-Generics.html#g:17, we get a :.: due to the nesting. But what I found confusing is the lack of Rec1 around the left arg of :.:, Perfect. I assumed that similar to :*:, both left and right args of :.: would be ... well, some type constructor used in the result of Rep1, for which we have no explicit kind (which IMO makes GHC.Generics a bit awkward to use, because you never know whether you have matched on all type constructors that can happen in a Rep1).

But in this case, clearly the RHS of :.: is such a type constructor of the Rep1 result kind (Rec1 Fork), whereas the LHS Perfect is not! It doesn't have the "pseudo-/sub-kind" of * -> * I would have expected; it is in fact an arbitrary type of kind * -> *.

So I read the original paper on the Generics impl and there we have

Note the arg function. When it sees a field type such as Perfect (Fork a), it matches the fourth GRHS, because isRep1 Perfect holds (because it has a Rep1 instance) and Fork a is neither ground (it mentions the parameter a), nor exactly the parameter a (in which case it would match the third GRHS, as it does for Fork a).

That suggests that indeed, the LHS of :.: is an arbitrary type constructor of kind * -> * which has a Generic1 instance. I wish that the documentation for :.: mentioned this asymmetry!

And now that I think of it, why do we need Rec1 in the first place? The way I see it, Rec1 f is literally just f :.: Par1. We'd get

> :kind! Rep1 Perfect
Rep1 Perfect :: * -> *
= Par1 :+: (Perfect :.: (Perfect :.: Par1))

I guess :.: is a bit more complex to think about and only relevant in the nested data type case at the moment. Nevertheless, a good design would force you to think about :.: in generic functions from the get go. The programmer then would match on f :.: Par1 only if they really can't come up with a polymorphically recursive function that properly handles :.:.

So I have two requests:

1. Update the documentation to reflect the asymmetry of :.:, namely that the LHS is always a type constructor that has a Generic1/Rep1 instance, whereas the RHS is a Rep1 generic view.
2. Deprecate Rec1 in favor of (:.: Par1), just as we deprecated Par0 in favor of Rec0.

I really want (1), I don't necessarily need (2). Although (2) means that we end up with Rec0 and Par1, which is a bit strange. Maybe we should simply name the former K and the latter P?