I think you may need to review your type theory, as several of your assertions are incorrect.
Let's address your main question (and backhanded point) - as others have pointed out type recursion of the type you requested is not allowed. This does not mean that c++ does not support type recursion. It supports it perfectly well. The type recursion you requested is type name recursion, which is a syntactic flair that actually has no consequence on the actual type system.
C++ allows tuple membership recursion by proxy. For instance, c++ allows
class A
{
A * oneOfMe_;
};
That is type recursion that has real consequences. (And obviously no language can do this without internal proxy representation because size is infinitely recursive otherwise).
Also C++ allows translationtime polymorphism, which allow for the creation of objects that act like any type you may create using name recursion. The name recursion is only used to unload types to members or provide translationtime behavior assignments in the type system. Type tags, type traits, etc. are well known c++ idioms for this.
To prove that type name recursion does not add functionality to a type system, it only needs to be pointed out that c++'s type system allows a fully Turing Complete type calculation, using metaprogramming on compiletime constants (and typelists of them), through simple mapping of names to constants. This means there is a function MakeItC++:YourIdeaOfPrettyName->TypeParametrisedByTypelistOfInts that makes any Turing computible typesystem you want.
As you know, being a student of type theory, variants are dual to tuple products. In the type category, any property of variants has a dual property of tuple products with arrows reversed. If you work consistently with the duality, you do not get properties with "new capabilities" (in terms of type calculations). So on the level of type calculations, you obviously don't need variants. (This should also be obvious from the Turing Completeness.)
However, in terms of runtime behavior in an imperative language, you do get different behavior. And it is bad behavior. Whereas products restrict semantics, variants relax semantics. You should never want this, as it provably destroys code correctness. The history of statically typed programming languages has been moving towards greater and greater expression of the semantics in the type system, with the goal that the compiler should be able to understand when the program does not mean what you want it to. The goal has been to turn the compiler into the program verification system.
For instance, with type units, you can express that a particular value isn't just an int but is actually an acceleration measured in meters per square seconds. Assigning a value that is a velocity expressed in feet per hour divided by a timespan of minutes shouldn't just divide the two values - it should note that a conversion is necessary (and either perform it or fail compilation or... do the right thing). Assinging a force should fail compilation. Doing these kinds of checks on program meaning could have given us potentially more martian exploration, for instance.
Variants are the opposite direction. Sure, "if you code correctly, they work correctly", but that's not the point with code verification. They provably add code loci where a different engineer, unfamiliar with current type usage, can introduce the incorrect semantic assumption without translation failure. And, there is always a code transformation that changes an imperative code section from one that uses Variants unsafely to one that use semantically validated non-variant types, so their use is also "always suboptimal".
The majority of runtime uses for variants are typically those that are better encapsulated in runtime polymorphism. Runtime polymorphism has a statically verified semantics that may have associated runtime invariant checking and unlike variants (where the sum type is universally declared in one code locus) actually supports the Open-Closed principle. By needing to declare a variant in one location, you must change that location everytime you add a new functional type to the sum. This means that code never closes to change, and therefore may have bugs introduced. Runtime polymorphism, though, allows new behaviors to be added in separate code loci from the other behaviors.
(And besides, most real language type systems are not distributive anyway. (a, b | c) =/= (a, b) | (a, c) so what is the point here?)
I would be careful making blanket statements about what makes a type system good without getting some experience in the field, particularly if your point is to be provocative and political and enact change. I do not see anything in your post that actually points to healthy changes for any computer language. I do not see features, safety, or any of the other actual real-world concerns being addressed. I totally get the love of type theory. I think every computer scientist should know Cateogry Theory and the denotational semantics of programming languages (domain theory, cartesian categories, all the good stuff). I think if more people understood the Curry-Howard isomorphism as an ontological manifesto, constructivist logics would get more respect.
But none of that provides reasons to attack the c++ type system. There are legitimate attacks for nearly every language - type name recursion and variant availability are not them.
EDIT: Since my point about Turing completeness does not seem to be understood, nor my comment about the c++ way of using type tags and traits to offload type calculations, maybe an example is in order.
Now the OP claims to want this in a usage case for lists, which my earlier point on the layout easily handles. Better, just use std::list. But from other comments and elsewhere, I think they really want this to work on the Felix->C++ translation.
So, what I think the OP thinks they want is something like
template <typename Type>
class SomeClass
{
// ...
};
and then be able to build a type
SomeClass< /*insert the SomeClass<...> type created here*/ >
I've mentioned this is just a naming convention wanted. Nobody wants typenames - they are transients of the translation process. What is actually wanted is what you will do with Type later on in the structural composition of the type. It will be used in typename calculations to produce member data and method signatures.
So, what can be done in c++ is
struct SelfTag {};
Then, when you want to refer to self, just put this type tag there.
When it's meaningful to do the type calculation, you have a template specialisation on SelfTag that will substitute SomeClass<SelfTag> instead of substituting SelfTag in the appropriate place of the type calculation.
My point here is that the c++ type system is Turing Complete - and that means a lot more than what I think the OP is reading everytime I've written that. Any type calculation may be done (given constraints of compiler recursion) and that really does mean that if you have a problem in one type system in a completely different language, you can find a translation here. I hope this makes things even clearer about my point. Coming back and saying "well you still can't do XYZ in the type system" would be clearly missing the point.