Avoid higher-order nested types?

If we get rid of the higher-order nested types, then we get better type roles:

newtype Zero a = Zero a
data Succ k rk = Succ {-# UNPACK #-} !(Tree k rk) rk
data Tree k rk = Tree !k rk
data Forest k rk
  = Nil
  | Skip (Forest k (Succ k rk))
  | Cons {-# UNPACK #-} !(Tree k rk) (Forest k (Succ k rk))
newtype BinomHeap k a = BH (Forest k (Zero a))
type role BinomHeap nominal representational

The only problem is that the GADT-style stuff for unordered operations gets considerably less pretty. Implementing unsafe key maps and normal maps and unordered traversals seems to require something like

data Natty k1 k2 a1 a2 rk1 rk2 where
  Zeroy :: Natty k1 k2 a1 a2 (Zero a1) (Zero a2)
  Succy :: !(Natty k1 k2 a1 a2 rk1 rk2) -> Natty k1 k2 a1 a2 (Succ k1 rk1) (Succ k1 rk2)

that relates the list-of-trees type for the origin type to that of the destination type.

Is it worth the pain to get the better type role?

Start by examining the proposed Zero, Succ, Tree, Forest, BinomHeap, and Natty types in the issue, then trace how unordered maps and traversals would use them. The issue names no files or tests; progress would require deciding whether the improved type roles justify the added GADT complexity and identifying the affected operations.