Asserting that typeclass holds for all results of type family application

Can't be done. You just gotta put the constraint everywhere. It's a real bummer.

I don't know the precise context in which you require these SymVal (Vec a n) instances, but generally speaking if you have a piece of code that requires the instance SymVal (Vec a n) then you should add it as a context:

foo :: forall (a :: Type) (n :: Nat). SymVal (Vec a n) => ...

When foo is called with a specific n, the constraint solver will reduce the type family application and use the instances

instance ( SymVal p, SymVal q ) => SymVal (p,q)

At the end of that process, the constraint solver will want an instance for SymVal a. So you'll be able to call foo:

• if you specify a given value for n, allowing the type family applications to fully reduce, and use a type a which has an instance for SymVal:

bar :: forall (a :: Type). SymVal a => ...
bar = ... foo @a @(S (S (S Z))) ...

baz :: ...
baz = ... foo @Float @(S Z) ... -- Float has a SymVal instance

• defer instance search by providing the same context:

quux :: forall (a :: Type) (n :: Nat). SymVal (Vec a n) => ...
quux = ... foo @a @n ...

GHC can't automatically deduce SymVal (Vec a n) from SymVal a, because without further context it cannot reduce the type family application, and thus doesn't know which instance to choose. If you want GHC to be able to perform this deduction, you would have to pass n explicitly as an argument. This can be emulated with singletons :

deduceSymVal :: forall (a :: Type) (n :: Nat). Sing n -> Dict (SymVal a) -> Dict (SymVal (Vec a n))
deduceSymVal sz@SZ Dict =
  case sz of
    ( _ :: Sing Z )
      -> Dict
deduceSymVal ( ss@(SS sm) ) Dict
  = case ss of
      ( _ :: Sing (S m) ) ->
        case deduceSymVal @a @m sm Dict of
          Dict -> Dict

(Note that these obnoxious case statements would be eliminated with type applications in patterns, mais c'est la vie.)

You can then use this function to allow GHC to deduce a SymVal (Vec a n) constraint from a SymVal a constraint, as long as you are able to provide a singleton for n (which amounts to passing n explicitly as opposed to being parametric over it):

flob :: forall (a :: Type) (n :: Nat). (SymVal a, SingI n) => ...
flob = case deduceSymVal @a (sing @n) Dict of
  Dict -- matching on 'Dict' provides a `SymVal (Vec a n)` instance
    -> ... foo @a @n ...