Avoid higher-order nested types?

[treeowl]

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?

[konsumlamm]

Related: #27.

I think it's not worth it if it's significantly more painful. My impression is that the demand for better type roles is rather low.

As a band-aid, we could provide a coerce{Min, Max}PQueue :: (Coercible a b) => {Min, Max}PQueue k a -> {Min, Max}PQueue k b function.

[treeowl]

Or more generally

Foo :: Coercible a b => Coercion (MinPQueue k a) (MinPQueue k b)

I've also played around with things like

bar :: ((forall k a b. Coercible a b => Coercible (MinPQueue k a) (MinPQueue k b)) => r) -> r

but at least in the past those tended to be tricky to use; I don't know if matters have improved.

[konsumlamm]

Or more generally

Foo :: Coercible a b => Coercion (MinPQueue k a) (MinPQueue k b)

Huh, TIL about Coercion. So this would allow people to get a Coercible (MinPQueue k a) (MinPQueue k b) constraint? That sounds even better than my suggestion.

[treeowl]

Yeah, it's in Data.Type.Coercion and it's definitely the most general extant approach with good ergonomics.