I have a multi-index type (i.e. a value together with a tuple of natural numbers), and I would like to give it e.g. an Ord instance to use its values within a data structure. I understand having Nat in there is a complication but I can’t understand why.
data Multi :: [Nat] -> * -> * where MVal :: a -> Multi ' a (:*) :: KnownNat n => Proxy n -> Multi ns a -> Multi (n ': ns) a
-- >>> (Proxy :: Proxy 32) :* (Proxy :: Proxy 16) :* (MVal pi) -- :: Floating a => Multi '[32, 16] a
instance (Eq a, Ord a) => Ord (Multi ' a) case (corresponding to the
MVal constructor) is straightforward but I can’t wrap my head around the other one. I’d be happy to pull in a library for this, as long as its dependency footprint is reasonably small.
Thank you in advance for any help and/or pointers.