[GHC] #9091: print and/or apply constraints when showing info for typed holes

8 May 2014

      #9091: print and/or apply constraints when showing info for typed holes
-------------------------------------------+-------------------------------
       Reporter:  kosmikus                 |             Owner:
           Type:  feature request          |            Status:  new
       Priority:  normal                   |         Milestone:
      Component:  Compiler (Type checker)  |           Version:  7.8.2
       Keywords:                           |  Operating System:
   Architecture:  Unknown/Multiple         |  Unknown/Multiple
     Difficulty:  Unknown                  |   Type of failure:
     Blocked By:                           |  None/Unknown
Related Tickets:                           |         Test Case:
                                           |          Blocking:
-------------------------------------------+-------------------------------
 Typed holes are fantastic already, but could be even better. Consider the
 following three examples:

 == Example 1 ==

 {{{
 f :: Eq a => a -> a -> Bool
 f x y = _
 }}}

 GHC-7.8.2 shows:
 {{{
     Found hole ‘_’ with type: Bool
     Relevant bindings include
       y :: a (bound at THC.hs:4:5)
       x :: a (bound at THC.hs:4:3)
       f :: a -> a -> Bool (bound at THC.hs:4:1)
     In the expression: _
     In an equation for ‘f’: f x y = _
 }}}

 GHC additionally knows that `Eq a` holds. It would be great if it would
 print that, too.

 == Example 2 ==

 {{{
 g :: (forall a. Eq a => a -> Bool) -> Bool
 g f = f _
 }}}

 GHC-7.8.2 shows:
 {{{
     Found hole ‘_’ with type: a0
     Where: ‘a0’ is an ambiguous type variable
     Relevant bindings include
       f :: forall a. Eq a => a -> Bool (bound at THC.hs:7:3)
       g :: (forall a. Eq a => a -> Bool) -> Bool (bound at THC.hs:7:1)
     In the first argument of ‘f’, namely ‘_’
     In the expression: f _
     In an equation for ‘g’: g f = f _
 }}}

 GHC additionally knows the `Eq a0` must hold. It would be nice if it could
 indicate that.

 == Example 3 ==

 {{{
 data X a where
   Y :: X Int

 h :: X a -> a -> a
 h Y x = _
 }}}

 GHC-7.8.2 shows:
 {{{
     Found hole ‘_’ with type: Int
     Relevant bindings include
       x :: a (bound at THC.hs:13:5)
       h :: X a -> a -> a (bound at THC.hs:13:1)
     In the expression: _
     In an equation for ‘h’: h Y x = _
 }}}

 Interestingly, GHC shows that we have to produce an `Int`. Unfortunately,
 it shows that `x` is of type `a`. GHC additionally knows that `a ~ Int`.
 It would be nice if GHC could either apply the constraint to show that `x
 :: Int` or at least show the constraint.

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