
-- | Okasaki's simple representation of a pairing heap, but with
-- a size index.
data Heap n a where
  E :: Heap 'Z a
  T :: a -> HVec n a -> Heap ('S n) a

-- Coercing a heap could destroy the heap property, so we declare both
-- type parameters nominal.
type role Heap nominal nominal

-- | A vector of heaps whose sizes sum to the index.
data HVec n a where
  HNil :: HVec 'Z a