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