Show valid substitutions for typed holes
AcceptedPublic

Authored by Tritlo on Sat, Mar 18, 8:49 AM.

Details

Summary

The idea is to implement a mechanism similar to PureScript, where they
suggest which identifiers in scope would fit the given hole. In
PureScript, they use subsumption (which is what we would like here as
well). For subsumption, we would have to check each type in scope whether
the hole is a subtype of the given type, but that would require
tcSubType and constraint satisfiability checking. Currently, TcSimplify uses
a lot of functions from TcErrors, so that would require more of
a rewrite, I will hold on with that for now, and submit the more simpler
type equality version.

As an example, consider

ps :: String -> IO ()
ps = putStrLn

ps2 :: a -> IO ()
ps2 _ = putStrLn "hello, world"

main :: IO ()
main = _ "hello, world"

The results would be something like

• Found hole: _ :: [Char] -> IO ()
• In the expression: _
  In a stmt of a 'do' block: _ "hello, world"
  In the expression:
    do _ "hello, world"
• Relevant bindings include
    main :: IO () (bound at test.hs:13:1)
    ps :: String -> IO () (bound at test.hs:7:1)
    ps2 :: forall a. a  -> IO () (bound at test.hs:10:1)
  Valid substitutions include
    putStrLn :: String
                -> IO () (imported from ‘Prelude’ at test.hs:1:1-14
                          (and originally defined in ‘System.IO’))
    putStr :: String
              -> IO () (imported from ‘Prelude’ at test.hs:1:1-14
                        (and originally defined in ‘System.IO’))

We'd like here for ps2 to be suggested as well, but for that we require
subsumption.

There are a very large number of changes, so older changes are hidden. Show Older Changes
Tritlo updated this revision to Diff 11802.Sat, Mar 18, 1:15 PM

Fix the output of the failing test to match the expected output.

Tritlo updated this revision to Diff 11803.Sat, Mar 18, 1:39 PM

Use pprPrefixOcc to handle operators correctly

Tritlo updated this revision to Diff 11804.Sat, Mar 18, 2:10 PM

Now the tests should (finally!) match. Sorry, whoever is getting notified of
all this!

Tritlo edited the summary of this revision. (Show Details)Sat, Mar 18, 4:41 PM
dfeuer requested changes to this revision.Sat, Mar 18, 6:40 PM
dfeuer added a subscriber: dfeuer.

Could you add a source note explaining what this new code does (mostly copy/paste from your commit message)? Also, it might be helpful to explain in a little more detail (in that source note) what obstacles you foresee implementing the more general subsumption check, so the thought you've put into it doesn't get lost in the mists of time.

compiler/typecheck/TcErrors.hs
1092–1184

Several places in validSubstitutions use some version of catMaybes . map f. These should all probably be written mapMaybe f instead.

This revision now requires changes to proceed.Sat, Mar 18, 6:40 PM
Tritlo updated this revision to Diff 11806.EditedSat, Mar 18, 7:11 PM

Add source note on validSubstitutions, and rewrite catMaybes . map to mapMaybe

dfeuer accepted this revision.Sat, Mar 18, 7:20 PM
This revision is now accepted and ready to land.Sat, Mar 18, 7:20 PM
Wizek added a subscriber: Wizek.Sat, Mar 18, 10:47 PM
mpickering requested changes to this revision.Sun, Mar 19, 4:59 PM
mpickering added a subscriber: mpickering.

It seems the error messages now contain redundant information when a binding is both "relevant" and "very relevant" (type correct).

There are also other changes to the error messages which are not accounted for.

Please could you add some tests which stress more complicated cases and the distinction between the two implementations you described?

testsuite/tests/typecheck/should_compile/holes2.stderr
12 ↗(On Diff #11806)

Why did this change?

This revision now requires changes to proceed.Sun, Mar 19, 4:59 PM
Tritlo marked an inline comment as done.Sun, Mar 19, 7:43 PM

It seems the error messages now contain redundant information when a binding is both "relevant" and "very relevant" (type correct).

There are also other changes to the error messages which are not accounted for.

Please could you add some tests which stress more complicated cases and the distinction between the two implementations you described?

I will look into the unaccounted for changes, though I'm not really sure where the changes originate.
What do you mean "test the distinction"? Do you mean that I should make a test to show that a -> IO () in the example is not found?
Would you prefer for it to not show things that are already displayed in "relevant bindings"? I would like to see them in both places, even though the output is a bit longer, since a relevant binding isn't necessarily a valid substitution.

In D3361#96696, @Tritlo wrote:

It seems the error messages now contain redundant information when a binding is both "relevant" and "very relevant" (type correct).

There are also other changes to the error messages which are not accounted for.

Please could you add some tests which stress more complicated cases and the distinction between the two implementations you described?

I will look into the unaccounted for changes, though I'm not really sure where the changes originate.

Perhaps it is because you are forcing instances to be loaded which are not imported by them module you are testing.
Try changing the error message to print out all possible instances and then seeing which ones are different before and after your patch.

What do you mean "test the distinction"? Do you mean that I should make a test to show that a -> IO () in the example is not found?

Yes ideally. If that is hard to do don't worry about it but some tests would be good.

Would you prefer for it to not show things that are already displayed in "relevant bindings"? I would like to see them in both places, even though the output is a bit longer, since a relevant binding isn't necessarily a valid substitution.

I don't think showing them in both places is good. There are four distinct classifications of bindings in my mind:

  1. In local scope but not type correct
  2. In local scope but a candidate for the hole
  3. In global scope and a candidate for the hole
  4. In global scope and no type correct

Currently we display 1 & 2 in the error messages, you are proposing that we display 1,2 and 3. In your patch you display (1 & 2) and (2 & 3) which is where the redundancy comes in.

This also seems like it could be quite expensive when there are many identifiers in scope (say 100 000) or using lots of holes will cause a lot of work to be repeated. Have you tried this in these situations?
A better solution might be to first build a map from types to identifiers and then reuse that for each hole.

Tritlo updated this revision to Diff 11818.Mon, Mar 20, 6:22 AM

Fix extra instances being brought into scope accidentally due to tcLookupImported_maybe, switched to lookupTypeHscEnv instead.

Tritlo added a comment.EditedMon, Mar 20, 6:28 AM
In D3361#96696, @Tritlo wrote:

It seems the error messages now contain redundant information when a binding is both "relevant" and "very relevant" (type correct).

There are also other changes to the error messages which are not accounted for.

Please could you add some tests which stress more complicated cases and the distinction between the two implementations you described?

I will look into the unaccounted for changes, though I'm not really sure where the changes originate.

Perhaps it is because you are forcing instances to be loaded which are not imported by them module you are testing.
Try changing the error message to print out all possible instances and then seeing which ones are different before and after your patch.

What do you mean "test the distinction"? Do you mean that I should make a test to show that a -> IO () in the example is not found?

Yes ideally. If that is hard to do don't worry about it but some tests would be good.

Would you prefer for it to not show things that are already displayed in "relevant bindings"? I would like to see them in both places, even though the output is a bit longer, since a relevant binding isn't necessarily a valid substitution.

I don't think showing them in both places is good. There are four distinct classifications of bindings in my mind:

  1. In local scope but not type correct
  2. In local scope but a candidate for the hole
  3. In global scope and a candidate for the hole
  4. In global scope and no type correct

    Currently we display 1 & 2 in the error messages, you are proposing that we display 1,2 and 3. In your patch you display (1 & 2) and (2 & 3) which is where the redundancy comes in.

    This also seems like it could be quite expensive when there are many identifiers in scope (say 100 000) or using lots of holes will cause a lot of work to be repeated. Have you tried this in these situations? A better solution might be to first build a map from types to identifiers and then reuse that for each hole.

I've fixed the additional instances being brought into scope, I didn't realize that tcLookupImported_maybe tried to be smart when it encountered something it didn't know about, which caused it to import interface files (I think). Still new to GHC internals!

I suppose you're right about (1 & 2) and (2 & 3). I'll change it to display only valid substitutions in the global scope. This will also reduce some of the work being duplicated between relevantBindings and validSubstitutions.

Performance will definitely be an issue if there are a lot of identifiers in scope, but as it currently is, it stops after having found -fmax-valid-substitutions that fit the hole. Having a map from types to identifiers would definitely help for many holes, but I think that for a high number of identifiers, it might slow things down a bit. I believe though that since this only fires when there are holes, this is not a big issue. Any thoughts on that?

In D3361#96714, @Tritlo wrote:
In D3361#96696, @Tritlo wrote:

It seems the error messages now contain redundant information when a binding is both "relevant" and "very relevant" (type correct).

There are also other changes to the error messages which are not accounted for.

Please could you add some tests which stress more complicated cases and the distinction between the two implementations you described?

I will look into the unaccounted for changes, though I'm not really sure where the changes originate.

Perhaps it is because you are forcing instances to be loaded which are not imported by them module you are testing.
Try changing the error message to print out all possible instances and then seeing which ones are different before and after your patch.

What do you mean "test the distinction"? Do you mean that I should make a test to show that a -> IO () in the example is not found?

Yes ideally. If that is hard to do don't worry about it but some tests would be good.

Would you prefer for it to not show things that are already displayed in "relevant bindings"? I would like to see them in both places, even though the output is a bit longer, since a relevant binding isn't necessarily a valid substitution.

I don't think showing them in both places is good. There are four distinct classifications of bindings in my mind:

  1. In local scope but not type correct
  2. In local scope but a candidate for the hole
  3. In global scope and a candidate for the hole
  4. In global scope and no type correct

    Currently we display 1 & 2 in the error messages, you are proposing that we display 1,2 and 3. In your patch you display (1 & 2) and (2 & 3) which is where the redundancy comes in.

    This also seems like it could be quite expensive when there are many identifiers in scope (say 100 000) or using lots of holes will cause a lot of work to be repeated. Have you tried this in these situations? A better solution might be to first build a map from types to identifiers and then reuse that for each hole.

I've fixed the additional instances being brought into scope, I didn't realize that tcLookupImported_maybe tried to be smart when it encountered something it didn't know about, which caused it to import interface files (I think). Still new to GHC internals!

I suppose you're right about (1 & 2) and (2 & 3). I'll change it to display only valid substitutions in the global scope. This will also reduce some of the work being duplicated between relevantBindings and validSubstitutions.

I'll also add some more tests, though I'm not sure how. Is there any resource I can look at into how you add tests?

Performance will definitely be an issue if there are a lot of identifiers in scope, but as it currently is, it stops after having found -fmax-valid-substitutions that fit the hole. Having a map from types to identifiers would definitely help for many holes, but I think that for a high number of identifiers, it might slow things down a bit. I believe though that since this only fires when there are holes, this is not a big issue. Any thoughts on that?

Good job fixing that problem. It looked like something which might have been tricky to track down.

There is a wiki page which describes how to add tests - https://ghc.haskell.org/trac/ghc/wiki/Building/RunningTests/Adding

You can mostly get away with looking at existing tests and cargo culting.

The main thing I am worried about is that if it takes a very long time with the 100 000 identifiers case then it will not be obvious what the problem is for someone to debug.
Could you perhaps try creating a few modules with a lot of identifiers in scope and then creating a hole with a type which matches none of them and seeing how long it takes.
Looking at the implementation you are relying on laziness to ensure that things stop after the first n holes but this could be quite fragile. There are still lookups for every identifier in global scope.

Another thing I thought about, it could be the case that a data constructor would have the right type to fill a hole. I don't think your implementation works here.

compiler/typecheck/TcErrors.hs
1136

This bit means we won't find data constructors.

mpickering requested changes to this revision.Mon, Mar 20, 6:53 AM
This revision now requires changes to proceed.Mon, Mar 20, 6:53 AM
Tritlo updated this revision to Diff 11819.Mon, Mar 20, 9:38 AM

Fix data constructors not being suggested, and add test specifically for valid substitutions, which includes checking that subsumable types are not suggested.

Tritlo updated this revision to Diff 11820.Mon, Mar 20, 10:14 AM

Fix tests that changed after removing local imports and the note.

Tritlo updated this revision to Diff 11821.Mon, Mar 20, 10:15 AM

Missed one. Sorry!

Tritlo updated this revision to Diff 11822.Mon, Mar 20, 11:15 AM

Change to explicity tail recursive checking of substituteable, so as to not not rely on laziness.

Tritlo updated this revision to Diff 11823.Mon, Mar 20, 11:40 AM

Cleaned up a bit

So I've tested the performance a bit, and it does not seem to slow it down appreciably. I generated a file with a lot of Ids, with the following

main :: IO ()
main = writeFile f $ unlines $ "module ManyIds where":(map out [0..10000])
 where f = "ManyIds.hs"
       out i = "a" ++ show i ++ " :: Int -> Int\n"
            ++ "a" ++ show i ++ " _ = " ++ show i

in another file, manyIdsTest.hs, was the following:

import ManyIds

test :: Int -> Int
test = _

main :: IO ()
main = return ()

Compiling ManyIds took some time with both my HEAD and GHC 8.0.2, which is why I reduced the number of identifiers down to 10_000 from 100_000.

Timing it with unix time, I got the following:
ghc -o test manyIdsTest.hs 20,28s user 0,83s system 91% cpu 23,041 total
./inplace/bin/ghc-stage2 -o test manyIdsTest.hs -fno-max-valid-substitutions 21,59s user 1,38s system 88% cpu 25,874 total
So even with -fno-max-valid-substitutions, it's not appreciably slower (I suspect the extra second is mostly from writing stdout to a file)

In D3361#96734, @Tritlo wrote:

So I've tested the performance a bit, and it does not seem to slow it down appreciably. I generated a file with a lot of Ids, with the following

main :: IO ()
main = writeFile f $ unlines $ "module ManyIds where":(map out [0..10000])
 where f = "ManyIds.hs"
       out i = "a" ++ show i ++ " :: Int -> Int\n"
            ++ "a" ++ show i ++ " _ = " ++ show i

in another file, manyIdsTest.hs, was the following:

import ManyIds

test :: Int -> Int
test = _

main :: IO ()
main = return ()

Compiling ManyIds took some time with both my HEAD and GHC 8.0.2, which is why I reduced the number of identifiers down to 10_000 from 100_000.

Timing it with unix time, I got the following:
ghc -o test manyIdsTest.hs 20,28s user 0,83s system 91% cpu 23,041 total
./inplace/bin/ghc-stage2 -o test manyIdsTest.hs -fno-max-valid-substitutions 21,59s user 1,38s system 88% cpu 25,874 total
So even with -fno-max-valid-substitutions, it's not appreciably slower (I suspect the extra second is mostly from writing stdout to a file)

Great!

Is the only issue to deal with now the duplication of information in relevant and type correct bindings?

Tritlo updated this revision to Diff 11824.Mon, Mar 20, 1:03 PM

Fix the last test, should be good to go.

In D3361#96734, @Tritlo wrote:

So I've tested the performance a bit, and it does not seem to slow it down appreciably. I generated a file with a lot of Ids, with the following

main :: IO ()
main = writeFile f $ unlines $ "module ManyIds where":(map out [0..10000])
 where f = "ManyIds.hs"
       out i = "a" ++ show i ++ " :: Int -> Int\n"
            ++ "a" ++ show i ++ " _ = " ++ show i

in another file, manyIdsTest.hs, was the following:

import ManyIds

test :: Int -> Int
test = _

main :: IO ()
main = return ()

Compiling ManyIds took some time with both my HEAD and GHC 8.0.2, which is why I reduced the number of identifiers down to 10_000 from 100_000.

Timing it with unix time, I got the following:
ghc -o test manyIdsTest.hs 20,28s user 0,83s system 91% cpu 23,041 total
./inplace/bin/ghc-stage2 -o test manyIdsTest.hs -fno-max-valid-substitutions 21,59s user 1,38s system 88% cpu 25,874 total
So even with -fno-max-valid-substitutions, it's not appreciably slower (I suspect the extra second is mostly from writing stdout to a file)

Great!

Is the only issue to deal with now the duplication of information in relevant and type correct bindings?

No, it now only checks ids that are in scope from being imported. I think it makes more sense to keep the information as it is in relevant bindings, so that we do not disturb the output too much. I'm going to add one last thing, which is to reverse the displayed substitutions, as the order got reversed when I made the tail recursive version :)

Tritlo updated this revision to Diff 11825.Mon, Mar 20, 1:18 PM

Reverse the list of outputted substitutions, to match alphabetic order (and the implementation in relevant bindings).

Tritlo updated this revision to Diff 11828.Mon, Mar 20, 1:36 PM

Fix error in comment. This should be good to go now!

mpickering requested changes to this revision.Tue, Mar 21, 5:06 AM

Ok the code looks good now but still some error message wibbles I think.

I don't think the output is still completely perfect. Only suggesting imported identifiers is too strong. Identifiers defined in the module but not local are not relevant nor suggested if they have the right type.
In your example, ps is now not suggested when it is more likely to be the identifier the user is looking for as they defined it locally in the module.

compiler/typecheck/TcErrors.hs
1111

maybe Nothing tyToId is the same as fmap tyToId.

How about fmap tyToId <$> lookupTypeHscEnv env name

This revision now requires changes to proceed.Tue, Mar 21, 5:06 AM
Tritlo marked 2 inline comments as done.Tue, Mar 21, 6:23 AM
Tritlo added inline comments.
compiler/typecheck/TcErrors.hs
1111

No, that results in IO (Maybe (Maybe Id)), instead of IO (Maybe Id). I can swap it out with (>>= tyToId) <$> lookupTypeHscEnv env name instead.

mpickering added inline comments.Tue, Mar 21, 6:25 AM
compiler/typecheck/TcErrors.hs
1111

Ah you are right that is a bit awkward. I think I prefer maybe Nothing tyToId <$> lookupTypeHscEnv env name in that case but it's up to you.

Tritlo updated this revision to Diff 11838.EditedTue, Mar 21, 1:31 PM
Tritlo marked 2 inline comments as done.

It now finds substitutables from the local module as well, but takes care to not report anything that relevantBindings reports. I measured the performance again, and it still holds up even in the ManyIds case.

Tritlo marked an inline comment as done.Tue, Mar 21, 1:33 PM
Tritlo updated this revision to Diff 11839.Tue, Mar 21, 1:37 PM

Update note to match implementation better.

mpickering accepted this revision.Tue, Mar 21, 3:51 PM

Good job!

This revision is now accepted and ready to land.Tue, Mar 21, 3:51 PM
Tritlo edited the summary of this revision. (Show Details)Wed, Mar 22, 6:41 AM
Tritlo updated this revision to Diff 11857.EditedThu, Mar 23, 9:01 PM

Added a function to make sure that locals that fit the hole are preferred over imported ids. Makes the output much more useful, and performance still holds up, even in the degenerate ManyIds test. Is this still ok, @mpickering? I could revert it if you prefer the old version.

Yes, this is a good idea but the implementation of the function could be improved.

compiler/typecheck/TcErrors.hs
1116

Use partition or sortBy.

Tritlo updated this revision to Diff 11865.Fri, Mar 24, 10:27 AM

Use partition instead of two filters.

Tritlo marked an inline comment as done.Fri, Mar 24, 10:39 AM