Hello café, hope you all doing well! I have this code [1]. Its purpose is to provide an `fmap` that works at any depth. Here is the gist of the gist: ```Haskell fmapz ∷ forall seed fruit seed' fruit' peels recursive. Squeezish seed seed' fruit fruit' peels recursive ⇒ (seed → seed') → fruit → fruit' fmapz function = stretch . fmap @(Squeezed (Strip seed fruit)) function . squeeze ``` As the examples show, it works, and even has some type inference. However, the type signature is unwieldy. It seems like it should have only 4 variables, but I have to also do some type level book-keeping for which the other 2 variables are needed. These book-keeping type variables are determined by type families from the other 4, so surely I can hide them inside a type synonym or something like that? I tried giving a quantified constraint, like so: ```Haskell type Squeezish ∷ ★ → ★ → ★ → ★ → Constraint type Squeezish seed seed' fruit fruit' = forall peels recursive. Squeezish' seed seed' fruit fruit' peels recursive class Squeezish' seed seed' fruit fruit' (peels ∷ [★ → ★]) (recursive ∷ Bool) instance ( peels ~ Strip seed fruit , ForAll peels Functor , Squeezy seed' fruit' peels recursive , Squeezy seed fruit peels recursive ) ⇒ Squeezish' seed seed' fruit fruit' peels recursive ``` — But then the constraints from the context of `Squeezish'` fail to make it to the use site and numerous errors arise. What can I do to solve this problem? Or is it theoretically impossible? [1]: https://gist.github.com/kindaro/6056f753bcf356ced96b817fee72533c