Witnessing that previous type family clauses didn't match

I have the following closed type family:

type family IsSpecialSize (n :: Nat) :: Bool where
    IsSpecialSize 8 = True
    IsSpecialSize 16 = True
    IsSpecialSize _ = False

I'd like to write a singleton witness and a decider for this type family:

data SSpecial (n :: Nat) where
    SSpecial8 :: SSpecial 8
    SSpecial16 :: SSpecial 16
    SNotSpecial :: (IsSpecialSize n ~ False) => SSpecial n

class DecideSSpecial (n :: Nat) where
    specialSize :: SSpecial n

The special cases are trivial to cover:

instance {-# OVERLAPPING #-} DecideSSpecial 8 where
    specialSize = SSpecial8

instance {-# OVERLAPPING #-} DecideSSpecial 16 where
    specialSize = SSpecial16

However, we get into trouble with the generic instance. We can't just write

instance {-# OVERLAPPABLE #-} (KnownNat n) => DecideSSpecial n where
    specialSize = SNotSpecial

since there is nothing in scope to prove that IsSpecialSize n ~ False. We can try adding it to the context of the last instance:

instance {-# OVERLAPPABLE #-} (KnownNat n, IsSpecialSize n ~ False) => DecideSSpecial n where
    specialSize = SNotSpecial

but then we can't use it abstracting over n; for example, the following definition fails to typecheck:

data Unsigned (n :: Nat) where
    U8 :: Word8 -> Unsigned 8
    U16 :: Word16 -> Unsigned 16
    U :: (IsSpecialSize n ~ False) => Integer -> Unsigned n

instance forall n. (KnownNat n) => Num (Unsigned n) where
    fromInteger = case specialSize @n of
        SSpecial8 -> U8 . fromInteger
        SSpecial16 -> U16 . fromInteger
        SNotSpecial -> U . fromInteger

with

    • Couldn't match type ‘IsSpecialSize n’ with ‘'False’
        arising from a use of ‘specialSize’
    • In the expression: specialSize @n

One thing I could do is to add DecideSSpecial n to the context of the Num instance:

instance forall n. (KnownNat n, DecideSSpecial n) => Num (Unsigned n) where

but I very much want to avoid that; after all, morally, I should be able to tell if any given KnownNat is equal to 8, 16 or neither.

There is currently no way to do this safely.

It would be possible if there were a way to obtain evidence of disequality at run time from a KnownNat constraint.

You can still create such a way unsafely (you can use GHC.TypeNats.sameNat, and unsafeCoerce a Refl in the Nothing case):

-- (==) and (:~:) from Data.Type.Equality
eqNat :: forall n m. (KnownNat n, KnownNat m) => Either ((n == m) :~: 'False) (n :~: m)
eqNat =
  case GHC.TypeNats.sameNat @n @m Proxy Proxy of
    Just r -> Right r
    Nothing -> Left (unsafeCoerce (Refl :: 'False :~: 'False))
-- The only piece of unsafe code in this answer.

Note that it is not quite as powerful as you might expect. In particular, disequality is not symmetric: ((n == m) ~ 'False) does not imply ((m == n) ~ 'False). So you have to be careful about the order of arguments of eqNat.

Since that uses a generic equality test, the IsSpecialSize test also needs to use it:

type IsSpecialSize n = (n == 8) || (n == 16)

Finally you can define a single instance, actually, a plain function.

specialSize :: forall n. KnownNat n => SSpecial n
specialSize =
  case eqNat @n @8 of
    Right Refl -> SSpecial8
    Left Refl ->
      case eqNat @n @16 of
        Right Refl -> SSpecial16
        Left Refl -> SNotSpecial