RFC: Allow not quantifying every top-level quantifiee

Minor nuisance, does this happen to anyone else?

Currently Haskell has an all-nothing policy on quantified type variables, either you quantify none or all (fine, let's ignore non-prenex quantification foo :: a -> forall b. b -> a). Can we have a top-level quantification of only a subset of the free variables?

Say I'm working on a function

reflected :: (Applicative m, Reifies s a) => TaggedT s m a

and I need to make s a scoped type variable, I always accidentally write

reflected :: forall s. (Applicative m, Reifies s a) => TaggedT s m a
reflected = TagT . pure . reflect $ (Proxy :: Proxy s)

This causes GHC to complain that the other types — m, a — are not in scope so and I have to add the remaining quantifiees I don't really care about (may have long names as well). It could be worse (dramatization)

ipartsOf :: forall i p f s t a. (Indexable [i] p, Functor f) => Traversing (Indexed i) f s t a a -> Over p f s t [a] [a]
ipartsOf l = conjoined
  (\f s -> let b = inline l sell s                            in outs b <$> f (wins b))
  (\f s -> let b = inline l sell s; (is, as) = unzip (pins b) in outs b <$> indexed f (is :: [i]) as)

appendAssocAxiom :: forall p q r as bs cs. p as -> q bs -> r cs -> Dict ((as ++ (bs ++ cs)) ~ ((as ++ bs) ++ cs))
appendAssocAxiom _ _ _ = unsafeCoerce (Dict :: Dict (as ~ as))

It would be nice to be nice to only have to specify the type one is interested in:

ipartsOf :: forall i. (Indexable [i] p, Functor f) => Traversing (Indexed i) f s t a a -> Over p f s t [a] [a]

appendAssocAxiom :: forall as. p as -> q bs -> r cs -> Dict ((as ++ (bs ++ cs)) ~ ((as ++ bs) ++ cs))

and have the others chosen in some way. This is not just useful for writing, but it makes it easier to read: If I see a type forall i p f s t a. ... any of them may appear in the function body, if I see a type forall i. ... I know only one is. Thoughts?