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

1 files changed, 4 insertions, 5 deletions

diff --git a/testsuite/tests/typecheck/should_compile/T9497a.stderr b/testsuite/tests/typecheck/should_compile/T9497a.stderr
index b095e5a3f1..d24849df79 100644
--- a/testsuite/tests/typecheck/should_compile/T9497a.stderr
+++ b/testsuite/tests/typecheck/should_compile/T9497a.stderr
@@ -5,14 +5,13 @@ T9497a.hs:2:8: warning: [-Wtyped-holes (in -Wdefault)]
     • In the expression: _main
       In an equation for ‘main’: main = _main
     • Relevant bindings include main :: IO () (bound at T9497a.hs:2:1)
-      Valid substitutions include
-        main :: IO () (defined at T9497a.hs:2:1)
+      Valid hole fits include
+        main :: IO () (bound at T9497a.hs:2:1)
         readLn :: forall a. Read a => IO a
+          with readLn @()
           (imported from ‘Prelude’ at T9497a.hs:1:1
            (and originally defined in ‘System.IO’))
         mempty :: forall a. Monoid a => a
+          with mempty @(IO ())
           (imported from ‘Prelude’ at T9497a.hs:1:1
            (and originally defined in ‘GHC.Base’))
-        undefined :: forall a. GHC.Stack.Types.HasCallStack => a
-          (imported from ‘Prelude’ at T9497a.hs:1:1
-           (and originally defined in ‘GHC.Err’))