"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