Returning `forall` from type family?

Learn
#1

Does anyone know of a way to return a forall from a type family?

I essentially have something like f :: forall x (vars :: Vars x). F x vars to work around this issue, then Vars x reduces to NP I ?something to allow me to have many variables in the forall.
The issue with this is that type inference completely breaks with this. The result of F x vars returns something like Idx vars 1 -> Idx vars 2 -> ..., and even if you tell GHC what the results of the type family applications are, GHC can’t figure out that given many such results, vars can be inferred. How can I make this work?

Example:

type family Fst (x :: NP I [Type, Type]) :: Type where
  Fst ('I a :* 'I b :* 'Nil) = a

type family Snd (x :: NP I [Type, Type]) :: Type where
  Snd ('I a :* 'I b :* 'Nil) = b

swap :: forall (ab :: NP I [Type, Type]). (Fst ab, Snd ab) -> (Snd ab, Fst ab)
swap = undefined

ab should be unambiguous here, but it’s not. Is there a way to make this infer ab, or is there perhaps another way to return foralls from a type family, or somehow make a surround forall have more variables?

Thanks

#2

As far as I understand, the issue here, is that if you call the type family, it can’t be sure that it reduces; i.e. that ab ~ 'I a :* 'I b :* 'Nil, if you add that constraint, it works.

#3

Then I need an a and b in scope, which doesn’t solve the problem, because I don’t have any other variables in scope, because the type family can’t introduce any.