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

31 Mar 2018

      #14990: "Valid refinement suggestions" have the wrong types
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  Tritlo
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.5
      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:                    |
-------------------------------------+-------------------------------------
Changes (by Tritlo):

 * owner:  (none) => Tritlo

Comment:

 Yes, I agree! Of course the type displayed should be the type of the
 actual expression and not just the type of the function suggested. That
 only works in the single identifier case.

 In the current version, it now shows the type of the additional holes,
 like this:

 {{{
     • 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
         abs :: forall a. Num a => a -> a
         signum :: forall a. Num a => a -> a
         fromInteger :: forall a. Num a => Integer -> a
       Valid refinement substitutions include
         (-) (_ :: Integer) :: forall a. Num a => a -> a -> a
         (*) (_ :: Integer) :: forall a. Num a => a -> a -> a
         (+) (_ :: Integer) :: forall a. Num a => a -> a -> a
   }}}

 Having any constraints known constraints on these would be very helpful, I
 agree, and the types of the functions themselves should be the type of the
 entire expression.

 In the more polymorphic case, it would say:

 {{{
   (+) (_ :: a0) :: a0 -> a0
     where (Num a0)
 }}}

 However, I worry that this might then become less useful for IDEs in the
 future. I think it would be best to have something displayed that can
 directly replace the hole. How would you present the `(Num a0)` constraint
 so that it would be picked up by the hole itself? Is it possible to use
 `ScopedTypeVariables` maybe? And have it say `(+) (_ :: a0) :: Num a0 =>
 a0 -> a0`?

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