"Valid refinement suggestions" have the wrong types

I've recently discovered that the "valid suggestions" feature for typed holes is quite powerful. For example, if I say

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

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture

changed weight to 5

added Tbug Trac import labels

assigned to @Tritlo

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? Or would it have to be ((+) :: Num a0 => a0 -> a0 -> a0) (_ :: a0) :: a0 -> a0 for the constraint to be picked up?

One issue that pops up: Is it more or less useful to have the type of the expression rather than the type of the function being suggested? In this case, it would be (-) (_ :: Integer) :: Integer -> Integer, as specified by the type of the hole. In fact, if we show the specialized type, it would be the type of the hole in all situations, since that's what we're looking for in the first place! Right?

How does the following look (ignore the double mention of f in the valid substitution list)?

tref.hs:4:5: error:
    • Found hole: _ :: [Integer] -> Integer
    • In the expression: _
      In an equation for ‘f’: f = _
    • Relevant bindings include
        f :: [Integer] -> Integer (bound at tref.hs:4:1)
      Valid substitutions include
        f :: [Integer] -> Integer (bound at tref.hs:4:1)
        main :: forall a. a (bound at tref.hs:7:1)
        f :: [Integer] -> Integer (defined at tref.hs:4:1)
      Valid refinement substitutions include
        foldl1 (_ :: Integer -> Integer -> Integer)
          where foldl1 :: forall (t :: * -> *).
                          Data.Foldable.Foldable t =>
                          forall a. (a -> a -> a) -> t a -> a
          (imported from ‘Prelude’ at tref.hs:1:17-22
           (and originally defined in ‘Data.Foldable’))
        foldr1 (_ :: Integer -> Integer -> Integer)
          where foldr1 :: forall (t :: * -> *).
                          Data.Foldable.Foldable t =>
                          forall a. (a -> a -> a) -> t a -> a
          (imported from ‘Prelude’ at tref.hs:1:47-52
           (and originally defined in ‘Data.Foldable’))
        foldl (_ :: Integer -> Integer -> Integer) (_ :: Integer)
          where foldl :: forall (t :: * -> *).
                         Data.Foldable.Foldable t =>
                         forall b a. (b -> a -> b) -> b -> t a -> b
          (imported from ‘Prelude’ at tref.hs:1:33-37
           (and originally defined in ‘Data.Foldable’))
        foldr (_ :: Integer -> Integer -> Integer) (_ :: Integer)
          where foldr :: forall (t :: * -> *).
                         Data.Foldable.Foldable t =>
                         forall a b. (a -> b -> b) -> b -> t a -> b
          (imported from ‘Prelude’ at tref.hs:1:40-44
           (and originally defined in ‘Data.Foldable’))

You ask a good question about IDE usage. I don't have a good answer there... the Num a0 constraint is something more for the programmer to know about than to have literally in the code anywhere.

As for the new output, I like it! Thanks!

Trac metadata

Trac field	Value
Differential revisions	- → D4444

mentioned in commit e0b44e2e

changed milestone to %8.6.1

I believe this should now be fixed.

Yes, this has been fixed with e0b44e2e/ghc.

closed

Thanks!

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

added Pnormal label