Witnessing that previous type family clauses didn't match

Question

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.

Answer 1

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