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, 27 insertions, 1 deletions

diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 17d9504f37..4be3e5efd1 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -83,7 +83,7 @@ module TcRnTypes(
         tyCoVarsOfCtList, tyCoVarsOfCtsList,
 
         WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
-        andWC, unionsWC, mkSimpleWC, mkImplicWC,
+        isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC,
         addInsols, insolublesOnly, addSimples, addImplics,
         tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples,
         tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt,
@@ -113,6 +113,7 @@ module TcRnTypes(
         ctEvRole,
 
         wrapType, wrapTypeWithImplication,
+        removeBindingShadowing,
 
         -- Constraint solver plugins
         TcPlugin(..), TcPluginResult(..), TcPluginSolver,
@@ -935,6 +936,23 @@ instance HasOccName TcBinder where
     occName (TcIdBndr_ExpType name _ _) = occName name
     occName (TcTvBndr name _)           = occName name
 
+-- fixes #12177
+-- Builds up a list of bindings whose OccName has not been seen before
+-- i.e., If    ys  = removeBindingShadowing xs
+-- then
+--  - ys is obtained from xs by deleting some elements
+--  - ys has no duplicate OccNames
+--  - The first duplicated OccName in xs is retained in ys
+-- Overloaded so that it can be used for both GlobalRdrElt in typed-hole
+-- substitutions and TcBinder when looking for relevant bindings.
+removeBindingShadowing :: HasOccName a => [a] -> [a]
+removeBindingShadowing bindings = reverse $ fst $ foldl
+    (\(bindingAcc, seenNames) binding ->
+    if occName binding `elemOccSet` seenNames -- if we've seen it
+        then (bindingAcc, seenNames)              -- skip it
+        else (binding:bindingAcc, extendOccSet seenNames (occName binding)))
+    ([], emptyOccSet) bindings
+
 ---------------------------
 -- Template Haskell stages and levels
 ---------------------------
@@ -2303,6 +2321,14 @@ isEmptyWC :: WantedConstraints -> Bool
 isEmptyWC (WC { wc_simple = f, wc_impl = i })
   = isEmptyBag f && isEmptyBag i
 
+
+-- | Checks whether a the given wanted constraints are solved, i.e.
+-- that there are no simple constraints left and all the implications
+-- are solved.
+isSolvedWC :: WantedConstraints -> Bool
+isSolvedWC WC {wc_simple = wc_simple, wc_impl = wc_impl} =
+  isEmptyBag wc_simple && allBag (isSolvedStatus . ic_status) wc_impl
+
 andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints
 andWC (WC { wc_simple = f1, wc_impl = i1 })
       (WC { wc_simple = f2, wc_impl = i2 })