[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
      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 bgamari:

Old description:

> 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.  Notice that if any foralls are suppressed, then they are all at the
> "top" of the type (albeit possibly under class constraints).
>
> Reasons behind the conditions:
>
> 1. No comment.  The ''only'' effect of `-fprint-explicit-foralls` should
> be to turn off the suppression of foralls, and print all foralls
> unconditionally.
>
> 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.  E.g. `forall (a ::
> Nat). blah`
>
> 3. `Required` type variables must be supplied; omitting these would be
> very confusing.  E.b. in `T :: forall k -> k -> Type` it would be jolly
> confusing to omit the `forall k ->` part, leaving `T :: k -> Type`.
>
> 4. If a type has nested `forall`s, it's best to print all the foralls,
> including any at the top. Example
> {{{
> f :: forall a. (forall b. b -> b) -> a -> a
> }}}
>   Currently we suppress the outer forall, but with the nested forall we
> are well out of Haskell98-land and it seems better to display them all.
>
>   Reason for exception: the type of `return` is properly
> {{{
> return :: 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, to display
> {{{
> return :: Monad m => a -> m a
> }}}
>
> 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`.

New description:

 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.  Notice that if any foralls are suppressed, then they are all at the
 "top" of the type (albeit possibly under class constraints).

 Reasons behind the conditions:

 1. No comment.  The ''only'' effect of `-fprint-explicit-foralls` should
 be to turn off the suppression of foralls, and print all foralls
 unconditionally.

 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.  E.g. `forall (a :: Nat).
 blah`

 3. `Required` type variables must be supplied; omitting these would be
 very confusing.  E.b. in `T :: forall k -> k -> Type` it would be jolly
 confusing to omit the `forall k ->` part, leaving `T :: k -> Type`.

 4. If a type has nested `forall`s, it's best to print all the foralls,
 including any at the top. Example
 {{{
 f :: forall a. (forall b. b -> b) -> a -> a
 }}}
  Currently we suppress the outer forall, but with the nested forall we are
 well out of Haskell98-land and it seems better to display them all.

  Reason for exception: the type of `return` is properly
 {{{
 return :: 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, to display
 {{{
 return :: Monad m => a -> m a
 }}}

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