CombineRefs can be more thoroughly exclusive.

[treeowl]

At present, you have

data RefType = Relative | Absolute

type family Combine a b where
   Combine Relative Absolute = Absolute
   Combine Absolute Relative = Absolute
   Combine Relative Relative = Relative

-- | Combine @Ref@s which can be meaningfully combined. Note the absence of the absolute-absolute case; there's no
--   good meaning for combining two absolute references, so it is statically prohibited.
class CombineRefs a b where
   combine :: Ref a -> Ref b -> Ref (Combine a b)
instance CombineRefs Absolute Relative where
   combine (Abs a) (Rel b) = Abs (a + b)
instance CombineRefs Relative Absolute where
   combine (Rel a) (Abs b) = Abs (a + b)
instance CombineRefs Relative Relative where
   combine (Rel a) (Rel b) = Rel (a + b)

It's possible to write a bogus instance

instance CombineRefs Absolute Absolute where
  combine (Abs _) (Abs _) = undefined

because Combine Absolute Absolute is not considered an invalid type, per se, but rather "stuck". It is inhabited only by bottom.

You can make this instance impossible by writing something like

class Sane (a :: RefType)
instance Sane Relative
instance Sane Absolute
class Sane (Combine a b) => CombineRefs a b where ...

While Combine Absolute Absolute has kind RefType, it is now impossible (without OverlappingInstances) to make it an instance of Sane (because the only instance that would include it would be instance Sane a), and therefore impossible to make the bogus instance.

[treeowl]

You can exclude even in the presence of OverlappingInstances by using Typeable instead of Sane, Sane has much less potential for runtime overhead.