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 `forall`

s from a type family, or somehow make a surround `forall`

have more variables?

Thanks