Standalone deriving fails for GADTs when unifying type variables within a context

I have a GADT that looks like:

data SumType (types :: [Type]) where
  Here  :: forall x xs. x          -> SumType (x ': xs)
  There :: forall x xs. SumType xs -> SumType (x ': xs)

which I can derive Eq for by doing

deriving instance (Eq x, Eq (SumType xs)) => Eq (SumType (x ': xs))

instance Eq (SumType '[]) where
  _ == _ = True

The Eq (SumType '[]) instance is needed to resolve the Eq (SumType xs) constraint in the Eq (SumType (x ': xs)) instance. It would be nice to just do

deriving instance (Eq x, Eq (SumType xs)) => Eq (SumType (x ': xs))
deriving instance Eq (SumType '[])

And have the derivation be the same as Void (since SumType '[] has no constructors). Instead, it's generating (cleaned up from -ddump-deriv)

instance Eq (SumType '[]) where
  (==) (Here a) (Here b) = a == b
  (==) (There a) (There b) = a == b
  (==) _ _ = False

and I get an error

    • Could not deduce: xs1 ~ xs
      from the context: '[] ~ (x : xs)
        bound by a pattern with constructor:
                   There :: forall x (xs :: [*]). SumType xs -> SumType (x : xs),
                 in an equation for ‘==’
      or from: '[] ~ (x1 : xs1)
        bound by a pattern with constructor:
                   There :: forall x (xs :: [*]). SumType xs -> SumType (x : xs),
                 in an equation for ‘==’
      ‘xs1’ is a rigid type variable bound by
        a pattern with constructor:
          There :: forall x (xs :: [*]). SumType xs -> SumType (x : xs),
        in an equation for ‘==’
      ‘xs’ is a rigid type variable bound by
        a pattern with constructor:
          There :: forall x (xs :: [*]). SumType xs -> SumType (x : xs),
        in an equation for ‘==’
      Expected type: SumType xs
        Actual type: SumType xs1
    • In the second argument of ‘(==)’, namely ‘b1’
      In the expression: ((a1 == b1))
      In an equation for ‘==’: (==) (There a1) (There b1) = ((a1 == b1))
      When typechecking the code for ‘==’
        in a derived instance for ‘Eq (SumType '[])’:
        To see the code I am typechecking, use -ddump-deriv
    • Relevant bindings include
        b1 :: SumType xs1
        a1 :: SumType xs
   |
70 | deriving instance Eq (SumType '[])
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This issue is similar to Standalone deriving fails for GADTs due to inaccessible code, but different because I believe it would typecheck if not for pattern matching on the constrained type variable.