[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
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by Iceland_jack:

@@ -11,1 +11,1 @@
- reflected :: forall s m a. (Applicative m, Reifies s a) => TaggedT s m a
+ reflected :: (Applicative m, Reifies s a) => TaggedT s m a

New description:

 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 :: (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#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler