[GHC] #8191: Do not trim type environment when reporting type holes

[GHC]

#8191: Do not trim type environment when reporting type holes
------------------------------------+-------------------------------------
       Reporter:  simonpj           |             Owner:
           Type:  bug               |            Status:  new
       Priority:  normal            |         Milestone:
      Component:  Compiler          |           Version:  7.6.3
       Keywords:                    |  Operating System:  Unknown/Multiple
   Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
     Difficulty:  Unknown           |         Test Case:
     Blocked By:                    |          Blocking:
Related Tickets:                    |
------------------------------------+-------------------------------------
 Andres writes: I've just started playing with `TypeHoles`. (I'm writing
 some Haskell course
 materials and would like to use them from the very beginning once they
 become
 available.)

 However, I must say that I don't understand the current notion of
 "relevance"
 that seems to determine whether local bindings are included or not.

 The current rule seems to be that bindings are included only if the
 intersection between the type variables their types involve and the type
 variables in the whole is non-empty. However, I think this is confusing.

 Let's look at a number of examples:
 {{{
 > f1 :: Int -> Int -> Int
 > f1 x y = _

     Found hole ‛_’ with type: Int
     In the expression: _
     In an equation for ‛f1’: f1 x y = _
 }}}
 No bindings are shown.
 {{{
 > f2 :: a -> a -> a
 > f2 x y = _

     Found hole ‛_’ with type: a
     Where: ‛a’ is a rigid type variable bound by
                the type signature for f2 :: a -> a -> a at List.hs:6:7
     Relevant bindings include
       f2 :: a -> a -> a (bound at List.hs:7:1)
       x :: a (bound at List.hs:7:4)
       y :: a (bound at List.hs:7:6)
     In the expression: _
     In an equation for ‛f2’: f2 x y = _
 }}}
 Both `x` and `y` (and `f2`) are shown. Why should this be treated
 differently
 from `f1`?
 {{{
 > f3 :: Int -> (Int -> a) -> a
 > f3 x y = _

     Found hole ‛_’ with type: a
     Where: ‛a’ is a rigid type variable bound by
                the type signature for f3 :: Int -> (Int -> a) -> a at
 List.hs:9:7
     Relevant bindings include
       f3 :: Int -> (Int -> a) -> a (bound at List.hs:10:1)
       y :: Int -> a (bound at List.hs:10:6)
     In the expression: _
     In an equation for ‛f3’: f3 x y = _
 }}}
 Here, `y` is shown, but `x` isn't, even though `y` has to be applied to an
 Int
 in order to produce an `a`. Of course, it's possible to obtain an `Int`
 from
 elsewhere ...
 {{{
 f4 :: a -> (a -> b) -> b
 f4 x y = _

     Found hole ‛_’ with type: b
     Where: ‛b’ is a rigid type variable bound by
                the type signature for f4 :: a -> (a -> b) -> b at
 List.hs:12:7
     Relevant bindings include
       f4 :: a -> (a -> b) -> b (bound at List.hs:13:1)
       y :: a -> b (bound at List.hs:13:6)
     In the expression: _
     In an equation for ‛f4’: f4 x y = _
 }}}
 Again, only `y` is shown, and `x` isn't. But here, the only sane way of
 filling
 the hole is by applying `y` to `x`. Why is one more relevant than the
 other?
 {{{
 f5 x y = _

     Found hole ‛_’ with type: t2
     Where: ‛t2’ is a rigid type variable bound by
                 the inferred type of f5 :: t -> t1 -> t2 at List.hs:15:1
     Relevant bindings include
       f5 :: t -> t1 -> t2 (bound at List.hs:15:1)
     In the expression: _
     In an equation for ‛f5’: f5 x y = _
 }}}
 Neither `x` and `y` are included without a type signature. Even though all
 of
 the above types are admissible, which would convince GHC that one or even
 all may be relevant.

 IMHO, this isn't worth it. It's a confusing rule. Just include all local
 bindings
 in the output, always. That's potentially verbose, but easy to understand.
 It's
 also potentially really helpful, because it trains beginning programmers
 to see
 what types local variables get, and it's a way to obtain complex types of
 locally
 bound variables for expert programmers. It's also much easier to explain.
 It
 should be easier to implement, too :)

 Could we please change it?

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