[GHC] #16320: Clean up printing of foralls

[GHC]

#16320: Clean up printing of foralls
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           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:
-------------------------------------+-------------------------------------
 Simon and I agreed on several infelicities around the printing of types
 with foralls. Before cleaning up the code, though, we wanted a
 ''specification'' of what we should do. Here is what we have.

 When printing types for users (in GHCi and certain error messages), it is
 convenient to sometimes suppress `forall`s. Given a type `ty` to print,
 `forall`s will be suppressed when ''all'' of the following are true:

 1. `-fprint-explicit-foralls` is not in effect.
 2. The kinds of all bound type variables are Haskell98-style. That is, the
 kinds consist only of `Type` and `->`.
 3. No bound type variable is `Required`.
 4. The `forall`s are all at the top. Exception: `forall`s are allowed to
 be mixed with class constraints, but no `forall`s can appear under a
 proper `->`.
 5. No two quantified type variables are spelled the same.

 This decision is made once, while looking at the overall type. Once made,
 it is not challenged: either all `forall`s in a type are printed, or none
 are.

 Reasons behind the conditions:

 1. No comment.
 2. Currently, we print `forall k (a :: k). ...` when there is a bound type
 variable with a variable kind. But, really, the fact that it's a variable
 isn't the only way it could be interesting.
 3. `Required` type variables must be supplied; omitting these would be
 very confusing.
 4. If a type has nested `forall`s, it's best to print. Reason for
 exception: the type of `return` is properly `forall (m :: Type -> Type).
 Monad m => forall (a :: Type). a -> m a`. Note that a `forall` is under a
 class constraint. But we want to suppress the `forall`s there, too.
 5. Imagine this abuse of our language:

 {{{#!hs
 class C a b where
   meth :: forall a. a -> b
 }}}

 The type of `meth` is `forall a b. C a b => forall a. a -> b`. This is,
 actually, a well-formed type, where one type variable shadows another. But
 if we don't print the `forall`s, any reader will come to the wrong
 conclusion about the meaning of the type.

 This is a slight tweak to the current rules, meaning more `forall`s are
 printed than previously. Pointedly, this will not happen in
 Haskell98-style code, so they will not appear for beginners. The current
 state of affairs is messy, on the other hand, where some `forall`s may be
 suppressed in a type while others are printed, causing more trouble.

 While in town, any fix should also address comment:17:ticket:11786, which
 is about a seeming inefficiency of the implementation of
 `eliminateRuntimeReps`.

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