[GHC] #12183: Display all relevant local bindings

10 Jun 2016

      #12183: Display all relevant local bindings
-------------------------------------+-------------------------------------
           Reporter:  ezyang         |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           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:
-------------------------------------+-------------------------------------
 Presently, "Relevant bindings" messages (e.g., from holes) will attempt to
 report all local bindings, and relevant global bindings (by some
 heuristic), up to the number of bindings specified by `-fmax-relevant-
 binds=N`. For example, here is an error I recently had with a small number
 of relevant bindings:

 {{{
 Productive.hs:162:16: error:
     • Found hole: _ :: Par (D k0 (Stream k0 b))
       Where: ‘k0’ is an ambiguous type variable
              ‘b’ is a rigid type variable bound by
                the type signature for:
                  maapM :: forall a b.
                           (a -> Par b)
                           -> (forall (k :: Clock). Stream k a) -> Par
 (Forall1 Stream b)
                at Productive.hs:155:10
     • In the second argument of ‘(<$>)’, namely ‘_’
       In a stmt of a 'do' block: Cons b <$> _
       In the expression:
         do { (a, s') <- deStreamCons s;
              b <- f a;
              b' <- f (scar (unForall1 s'));
              Cons b <$> _ }
     • Relevant bindings include
         b' :: b (bound at Productive.hs:159:5)
         b :: b (bound at Productive.hs:158:5)
         s' :: Forall1 Stream a (bound at Productive.hs:157:9)
         (Some bindings suppressed; use -fmax-relevant-binds=N or -fno-max-
 relevant-binds)
 }}}

 When I set `-fno-max-relevant-binds)`, this extends with:

 {{{
         a :: a (bound at Productive.hs:157:6)
         s :: forall (k :: Clock). Stream k a (bound at
 Productive.hs:156:9)
         f :: a -> Par b (bound at Productive.hs:156:7)
         maapM :: (a -> Par b)
                  -> (forall (k :: Clock). Stream k a) -> Par (Forall1
 Stream b)
           (bound at Productive.hs:156:1)
         take :: forall a.
                 Int -> (forall (k :: Clock). Stream k a) -> Par [a]
           (bound at Productive.hs:143:1)
 ...and a pile more global binds...
 }}}

 I think this is not really the behavior we want. If I'm doing an Agda/Coq
 development, what I want is for the compiler to tell me all LOCAL
 bindings. Heuristically picked global bindings might be nice, but it's not
 a priority (after all, I probably have explicit type signatures for all of
 these anyway.)

 Thus, I propose that `-fmax-relevant-binds=N` be changed to apply to
 GLOBAL bindings only, and that GHC should unconditionally print all local
 bindings. Furthermore, I suggest that by default `-fmax-relevant-binds=0`.

 As a minor addendum, I don't find the context information `In the second
 argument of ‘(<$>)’, namely ‘_’`, etc. very useful. Just makes the message
 longer and harder to view.

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