Asserting that typeclass holds for all results of type family application

I've got a type family defined as follows:

type family Vec a (n :: Nat) where
  Vec a Z = a
  Vec a (S n) = (a, Vec a n)

I'd like to assert that the result of applying this type family always fulfills the SymVal class constraint from the SBV package:

forall a . (SymVal a) => SymVal (Vec a n)

There is SymVal instances a,b, so whenever SymVal a holds, then SymVal (Vec a n) should hold, for any value of n. How can I ensure GHC sees that SymVal is always implemented for the result of the type family application?

However, I don't know how to express this. Do I write an instance? A deriving clause? I'm not creating a new type, simply mapping numbers to existing ones.

Or am I totally on the wrong track? Should I be using a data family, or functional dependencies?

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 ...