The fact that x1 is \y -> (y, y) is superficial, though. Something like x1 = Just also increases exponentially, and makes clear that using a deduplicated DAG for representing type terms doesn't solve this.
Ah, you're right. If one goes to x_{i+1}, then there will be 2^i Maybes in the type. The number of Maybe-occurrences in the type doubles in each step and sharing won't help there.
