I think one practical disadvantage of the Haskell approach is that you need to wrap and unwrap your types if you want a different ordering on an existing type.

I think one practical disadvantage of the Haskell approach is that you need to wrap and unwrap your types if you want a different ordering on an existing type. But the main reason why I didn't like the Haskell approach isn't ergonomic but conceptual. To me, the type of the heap should depend on the Ord instance, because the invariant satisfied by the values of type `Heap a` depends on the Ord instance of `a`, not just on the type `a` itself. This invariant is not encoded in the type system in Haskell, but in a dependently typed language you could do that. But in order to even write down the invariant, you need access to the Ord instance. So the type signature of union could be: union : {a:Type} → {o:Ord a} → Heap o → Heap o → Heap o In this case the problem of mixing up heaps with different orderings is ruled out by ordinary type checking, rather than via an extra meta-theoretical invariant satisfied by the language. Although ML modules don't let you encode the invariant either, they at least set it up in the same way, because the type Heap(o).t depends on the o and not just on o.t, and the type checker also views it that way and will say Heap(o).t ≠ Heap(o').t even when o.t = o'.t. In Haskell on the other hand, if we desugar type classes to passing around records, then we can suddenly break the invariant in type safe code. Maybe I'm imposing values on Haskell that have no practical significance in that context, but to me the way Haskell does it feels like a hack.