There is a surprising amount of special-casing in singletons just for the sake of the Eq class. Ultimately, the root of all the special-casing is this default implementation for the associated (==) type:

Where:

The problem with this default is that for a significant portion of singleton types, DefaultEq is a rather roundabout way of defining (==). In order to reduce the first equation to True, you have to know that they are the exact same type. For instance, if you tried implement a PEq instance for Maybe that uses DefaultEq, then you wouldn't be able to implement an implementation of SEq by simple pattern matching and recursion:

instance PEq (Maybe a)
instance SEq (Maybe a) where
  SNothing %== SNothing = STrue
  SNothing %== SJust{}  = SFalse
  SJust{}  %== SNothing = SFalse
  SJust sx %== SJust sy = sx %== sy

error:
    • Could not deduce: (n == n1)
                        ~ Data.Singletons.Prelude.Eq.DefaultEq ('Just n) ('Just n1)
      from the context: a1 ~ 'Just n
        bound by a pattern with constructor:
                   SJust :: forall a (n :: a). Sing n -> SMaybe ('Just n),
                 in an equation for ‘%==’
        at Bug.hs:22:3-10
      or from: b ~ 'Just n1
        bound by a pattern with constructor:
                   SJust :: forall a (n :: a). Sing n -> SMaybe ('Just n),
                 in an equation for ‘%==’
        at Bug.hs:22:16-23
      Expected type: Sing (a1 == b)
        Actual type: Sing (n == n1)
    • In the expression: sx %== sy
      In an equation for ‘%==’: SJust sx %== SJust sy = sx %== sy
      In the instance declaration for ‘SEq (Maybe a)’
    • Relevant bindings include
        sy :: Sing n1 (bound at Bug.hs:22:22)
        sx :: Sing n (bound at Bug.hs:22:9)
        (%==) :: Sing a1 -> Sing b -> Sing (a1 == b)
          (bound at Bug.hs:19:12)
   |
22 |   SJust sx %== SJust sy = sx %== sy
   |                           ^^^^^^^^^

In fact, I can only think of three examples where DefaultEq is actually used in practice: the PEq instances for Nat, Symbol, and TYPE rep. The SEq instances defined on top of them, however, are very atypical for the singletons library, as they rely on Typeable and unsafeCoerce tricks. Most other instances, however, do not (and cannot) make use of DefaultEq, which makes me believe that we should change it.

My proposal: make (==)'s default implementation be \x y -> not (x == y), just like it is in base. Doing so would let us simply promote and single Eq using the existing TH machinery, rather than forcing us to laboriously define PEq and SEq by hand.