[GHC] #12540: RFC: Allow not quantifying every top-level quantifiee

[GHC]

#12540: RFC: Allow not quantifying every top-level quantifiee
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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

 {{{#!hs
 reflected :: forall s m a. (Applicative m, Reifies s a) => TaggedT s m a
 }}}

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

 {{{#!hs
 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'')

 {{{#!hs
 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:

 {{{#!hs
 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?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12540>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler