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)
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.
At present, you have
It's possible to write a bogus instance
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
While
Combine Absolute Absolute
has kindRefType
, it is now impossible (withoutOverlappingInstances
) to make it an instance ofSane
(because the only instance that would include it would beinstance Sane a
), and therefore impossible to make the bogus instance.