Deriving instances for GADT containing Nat fields

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

The 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.

1 Like

I’m not sure I understand the question. Why isn’t it enough to do this?

deriving instance Ord a => Ord (Multi ns a)

If you are writing it explicitly, the type indices mean that you only need to compare MVal with MVal or :* with :*, because the other cases are ruled out by the types. Moreover all the statically-determined Nats must be equal for the comparison to be well-typed. So ultimately all you end up comparing is the value under the MVal.

1 Like

Ah, I hadn’t thought it would work with StandaloneDeriving . Thank you!

Generally speaking when deriving instances for GADTs you often need StandaloneDeriving, in order to specify the instance contexts explicitly. It works by generating the derived instances and then type-checking them, so if it doesn’t work it isn’t always obvious why, but for simple cases it is rather useful.

1 Like