Polymorphic value support?

[Wizek]

Here I've asked a question initially about polymorphism with dependent-maps.

And we've found that the following definitions can work.

data Foo1 a where
  AnInt :: Foo1 Int
  AString :: Foo1 String
  ANum :: (Num n, Typeable n, Show n) => Foo1 n

data Foo2 n a where
  AnInt :: Foo2 n Int
  AString :: Foo2 n String
  ANum :: (Num n, Typeable n, Show n) => Foo2 n

If one defines instances by hand, e.g.:

instance GEq (Foo2 n) where
  geq AnInt AnInt = return Refl
  geq AString AString = return Refl
  geq ANum ANum = return Refl
  geq _ _ = Nothing

instance GCompare (Foo2 n) where
  gcompare AnInt AnInt = GEQ
  gcompare AnInt _ = GLT
  gcompare _ AnInt = GGT
  gcompare AString AString = GEQ
  gcompare AString _ = GLT
  gcompare _ AString = GGT
  gcompare (ANum :: Foo2 n a) (ANum :: Foo2 n b) = (eqT @a @b) & \case
    Just (Refl :: a :~: b) -> GEQ
    Nothing   -> error "This shouldn't happen"
  gcompare ANum _ = GLT
  gcompare _ ANum = GGT

But I wonder, doesn't/couldn't deriveGEq, deriveGCompare support deriving these kinds of instances somehow? Because hand-defining these doesn't scale much. E.g.

deriveGEq      ''Foo2
deriveGCompare ''Foo2

deriveGEq      ''(Foo2 n)
deriveGCompare ''(Foo2 n)

These give me the following kinds of errors, respectively:

exp-dep-map.hs:39:1: error:
    • Expecting one more argument to ‘Foo2’
      Expected kind ‘* -> *’, but ‘Foo2’ has kind ‘* -> * -> *’
    • In the first argument of ‘GEq’, namely ‘Foo2’
      In the instance declaration for ‘GEq Foo2’
   |
39 | deriveGEq      ''Foo
   | ^^^^^^^^^^^^^^^^^^^^

exp-dep-map.hs:40:19: error: parse error on input ‘Foo2’
   |
40 | deriveGEq      ''(Foo2 n)
   |                   ^^^

Also, is #6 relevant? PolyKinds makes me think that it may be, as one of the type errors is a kind-error.

cc obsidiansystems/dependent-map#16, because it would be nice to see a small self-contained example in the readme/docs if/when pol'ism is supported.

p.s. If it turns out that this is hard to solve with TH, maybe instances can be derived via generics too?