[Haskell-cafe] Hiding type variables from the signature?

[Ignat Insarov]

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