[GHC] #14990: "Valid refinement suggestions" have the wrong types

31 Mar 2018

      #14990: "Valid refinement suggestions" have the wrong types
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.5
           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:
-------------------------------------+-------------------------------------
 I've recently discovered that the "valid suggestions" feature for typed
 holes is quite powerful. For example, if I say

 {{{#!hs
 module Bug where

 import Prelude (Integer, Num(..))

 x :: Integer
 x = _ 5
 }}}

 and compile it with

 {{{
...
ghc Bug.hs -frefinement-level-substitutions=2
 }}}
I get

 {{{
 Bug.hs:6:5: error:
     • Found hole: _ :: Integer -> Integer
     • In the expression: _
       In the expression: _ 5
       In an equation for ‘x’: x = _ 5
     • Relevant bindings include x :: Integer (bound at Bug.hs:6:1)
       Valid substitutions include
         negate :: forall a. Num a => a -> a
           (imported from ‘Prelude’ at Bug.hs:3:26-32
            (and originally defined in ‘GHC.Num’))
         abs :: forall a. Num a => a -> a
           (imported from ‘Prelude’ at Bug.hs:3:26-32
            (and originally defined in ‘GHC.Num’))
         signum :: forall a. Num a => a -> a
           (imported from ‘Prelude’ at Bug.hs:3:26-32
            (and originally defined in ‘GHC.Num’))
         fromInteger :: forall a. Num a => Integer -> a
           (imported from ‘Prelude’ at Bug.hs:3:26-32
            (and originally defined in ‘GHC.Num’))
       Valid refinement substitutions include
         (-) _ :: forall a. Num a => a -> a -> a
           (imported from ‘Prelude’ at Bug.hs:3:26-32
            (and originally defined in ‘GHC.Num’))
         (*) _ :: forall a. Num a => a -> a -> a
           (imported from ‘Prelude’ at Bug.hs:3:26-32
            (and originally defined in ‘GHC.Num’))
         (+) _ :: forall a. Num a => a -> a -> a
           (imported from ‘Prelude’ at Bug.hs:3:26-32
            (and originally defined in ‘GHC.Num’))
   |
 6 | x = _ 5
   |     ^
 }}}

 Note the ''refinement suggestions'', that look not only for single
 identifiers that fill the hole but for function calls that could, as well.

 However, the formatting of the refinement suggestions is incorrect,
 stating, for example, that `(+) _ :: forall a. Num a => a -> a -> a`. This
 is plain wrong. We ''could'' say `(+) _ :: a0 -> a0` where `Num a0`, and
 that would be right, but even better would be something like

 {{{
   (+) x1 :: Integer -> Integer
     where x1 :: Integer
 }}}

 Now, I know that the first parameter to `(+)` must be an integer.

 In a more polymorphic situation, it could be

 {{{
   (+) x1 :: a0 -> a0
     where x1 :: a0
           (Num a0) holds
 }}}

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