#14990 closed bug (fixed)

"Valid refinement suggestions" have the wrong types

Reported by: goldfire Owned by: Tritlo
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.5
Keywords: Cc: Tritlo, Iceland_jack
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D4444
Wiki Page:

Description

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

Change History (12)

comment:1 Changed 21 months ago by RyanGlScott

Cc: Tritlo added

comment:2 Changed 21 months ago by Iceland_jack

Cc: Iceland_jack added

comment:3 Changed 21 months ago by Tritlo

Owner: set 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?

Last edited 21 months ago by Tritlo (previous) (diff)

comment:4 Changed 21 months ago by Tritlo

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?

comment:5 Changed 21 months ago by Tritlo

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’))

comment:6 Changed 21 months ago by goldfire

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!

comment:7 Changed 20 months ago by Tritlo

Status: newpatch

comment:8 Changed 20 months ago by RyanGlScott

Differential Rev(s): Phab:D4444

comment:9 Changed 19 months ago by Ben Gamari <ben@…>

In e0b44e2/ghc:

Improved Valid Hole Fits

I've changed the name from `Valid substitutions` to `Valid hole fits`,
since "substitution" already has a well defined meaning within the
theory. As part of this change, the flags and output is reanamed, with
substitution turning into hole-fit in most cases. "hole fit" was already
used internally in the code, it's clear and shouldn't cause any
confusion.

In this update, I've also reworked how we manage side-effects in the
hole we are considering.

This allows us to consider local bindings such as where clauses and
arguments to functions, suggesting e.g. `a` for `head (x:xs) where head
:: [a] -> a`.

It also allows us to find suggestions such as `maximum` for holes of
type `Ord a => a -> [a]`, and `max` when looking for a match for the
hole in `g = foldl1 _`, where `g :: Ord a => [a] -> a`.

We also show much improved output for refinement hole fits, and
fixes #14990. We now show the correct type of the function, but we also
now show what the arguments to the function should be e.g. `foldl1 (_ ::
Integer -> Integer -> Integer)` when looking for `[Integer] -> Integer`.

I've moved the bulk of the code from `TcErrors.hs` to a new file,
`TcHoleErrors.hs`, since it was getting too big to not live on it's own.

This addresses the considerations raised in #14969, and takes proper
care to set the `tcLevel` of the variables to the right level before
passing it to the simplifier.

We now also zonk the suggestions properly, which improves the output of
the refinement hole fits considerably.

This also filters out suggestions from the `GHC.Err` module, since even
though `error` and `undefined` are indeed valid hole fits, they are
"trivial", and almost never useful to the user.

We now find the hole fits using the proper manner, namely by solving
nested implications. This entails that the givens are passed along using
the implications the hole was nested in, which in turn should mean that
there will be fewer weird bugs in the typed holes.

I've also added a new sorting method (as suggested by SPJ) and sort by
the size of the types needed to turn the hole fits into the type of the
hole. This gives a reasonable approximation to relevance, and is much
faster than the subsumption check. I've also added a flag to toggle
whether to use this new sorting algorithm (as is done by default) or the
subsumption algorithm. This fixes #14969

I've also added documentation for these new flags and update the
documentation according to the new output.

Reviewers: bgamari, goldfire

Reviewed By: bgamari

Subscribers: simonpj, rwbarton, thomie, carter

GHC Trac Issues: #14969, #14990, #10946

Differential Revision: https://phabricator.haskell.org/D4444

comment:10 Changed 19 months ago by bgamari

Milestone: 8.6.1

I believe this should now be fixed.

comment:11 Changed 19 months ago by Tritlo

Yes, this has been fixed with e0b44e2/ghc.

comment:12 Changed 19 months ago by bgamari

Resolution: fixed
Status: patchclosed

Thanks!

Note: See TracTickets for help on using tickets.