Sort valid substitutions for typed holes by "relevance"

This is an initial attempt at tackling the issue of how to order the
suggestions provided by the valid substitutions checker, by sorting
them by creating a graph of how they subsume each other. We'd like to
order them in such a manner that the most "relevant" suggestions are
displayed first, so that the suggestion that the user might be looking
for is displayed before more far-fetched suggestions (and thus also
displayed when they'd otherwise be cut-off by the
`-fmax-valid-substitutions` limit). The previous ordering was based on
the order in which the elements appear in the list of imports, which I
believe is less correlated with relevance than this ordering.

A drawback of this approach is that, since we now want to sort the
elements, we can no longer "bail out early" when we've hit the
`-fmax-valid-substitutions` limit.

Reviewers: bgamari, dfeuer

Reviewed By: dfeuer

Subscribers: dfeuer, rwbarton, thomie, carter

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

4 files changed, 130 insertions, 55 deletions

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 05d1ec10bc..e93a133cf6 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -553,6 +553,8 @@ data GeneralFlag
    | Opt_PprCaseAsLet
    | Opt_PprShowTicks
    | Opt_ShowHoleConstraints
+   | Opt_NoShowValidSubstitutions
+   | Opt_NoSortValidSubstitutions
    | Opt_ShowLoadedModules
 
    -- Suppress all coercions, them replacing with '...'
@@ -800,8 +802,8 @@ data DynFlags = DynFlags {
 
   maxRelevantBinds      :: Maybe Int,   -- ^ Maximum number of bindings from the type envt
                                         --   to show in type error messages
-  maxValidSubstitutions :: Maybe Int,   -- ^ Maximum number of substitutions
-                                        --   to show in type error messages
+  maxValidSubstitutions :: Maybe Int,   -- ^ Maximum number of substitutions to
+                                        --   show in typed hole error messages
   maxUncoveredPatterns  :: Int,         -- ^ Maximum number of unmatched patterns to show
                                         --   in non-exhaustiveness warnings
   simplTickFactor       :: Int,         -- ^ Multiplier for simplifier ticks
@@ -3897,6 +3899,8 @@ fFlagsDeps = [
   flagSpec "show-warning-groups"              Opt_ShowWarnGroups,
   flagSpec "hide-source-paths"                Opt_HideSourcePaths,
   flagSpec "show-hole-constraints"            Opt_ShowHoleConstraints,
+  flagSpec "no-show-valid-substitutions"      Opt_NoShowValidSubstitutions,
+  flagSpec "no-sort-valid-substitutions"      Opt_NoSortValidSubstitutions,
   flagSpec "show-loaded-modules"              Opt_ShowLoadedModules,
   flagSpec "whole-archive-hs-libs"            Opt_WholeArchiveHsLibs
   ]
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index d895921411..fb27b4ed7c 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -50,7 +50,7 @@ import BasicTypes
 import ConLike          ( ConLike(..))
 import Util
 import TcEnv (tcLookup)
-import {-# SOURCE #-} TcSimplify ( tcCheckHoleFit )
+import {-# SOURCE #-} TcSimplify ( tcCheckHoleFit, tcSubsumes )
 import FastString
 import Outputable
 import SrcLoc
@@ -61,10 +61,13 @@ import Pair
 import qualified GHC.LanguageExtensions as LangExt
 import FV ( fvVarList, fvVarSet, unionFV )
 
-import Control.Monad    ( when )
+import Control.Monad    ( when, filterM )
 import Data.Foldable    ( toList )
-import Data.List        ( partition, mapAccumL, nub, sortBy, unfoldr, foldl')
+import Data.List        ( partition, mapAccumL, nub
+                        , sortBy, sort, unfoldr, foldl' )
 import qualified Data.Set as Set
+import Data.Graph       ( graphFromEdges, topSort )
+import Data.Function    ( on )
 
 import Data.Semigroup   ( Semigroup )
 import qualified Data.Semigroup as Semigroup
@@ -1085,7 +1088,9 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole })
                   = givenConstraintsMsg ctxt
                | otherwise = empty
 
-       ; sub_msg <- validSubstitutions tidy_simples ctxt ct
+       ; no_show_valid_substitutions <- goptM Opt_NoShowValidSubstitutions
+       ; sub_msg <- if no_show_valid_substitutions then return empty
+                    else validSubstitutions tidy_simples ctxt ct
        ; mkErrorMsgFromCt ctxt ct $
             important hole_msg `mappend`
             relevant_bindings (binds_msg $$ constraints_msg) `mappend`
@@ -1146,22 +1151,52 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole })
 
 mkHoleError _ _ ct = pprPanic "mkHoleError" (ppr ct)
 
+-- HoleFit is the type we use for a fit in valid substitutions. It contains the
+-- element that was checked and the elements Id.
+data HoleFit = HoleFit { hfEl :: GlobalRdrElt , hfId :: Id }
+
+-- We define an Eq and Ord instance to be able to build a graph.
+instance Eq HoleFit where
+   (==) = (==) `on` hfId
+
+-- We compare HoleFits by their gre_name instead of their Id, since we don't
+-- want our tests to be affected by the non-determinism of `nonDetCmpVar`,
+-- which is used to compare Ids.
+instance Ord HoleFit where
+  compare = compare `on` (gre_name . hfEl)
 
 -- See Note [Valid substitutions include ...]
 validSubstitutions :: [Ct] -> ReportErrCtxt -> Ct -> TcM SDoc
 validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
   do { rdr_env <- getGlobalRdrEnv
-     ; dflags <- getDynFlags
-     ; traceTc "findingValidSubstitutionsFor {" $ ppr wrapped_hole_ty
-     ; (discards, substitutions) <-
-        setTcLevel hole_lvl $
-         go (maxValidSubstitutions dflags) $
-          localsFirst $ globalRdrEnvElts rdr_env
-     ; traceTc "}" empty
-     ; return $ ppUnless (null substitutions) $
-                 hang (text "Valid substitutions include")
-                  2 (vcat (map ppr_sub substitutions)
-                    $$ ppWhen discards subsDiscardMsg) }
+     ; maxSubs <- maxValidSubstitutions <$> getDynFlags
+     ; sortSubs <- not <$> goptM Opt_NoSortValidSubstitutions
+     -- If we're not supposed to output any substitutions, we don't want to do
+     -- any work.
+     ; if maxSubs == Just 0
+       then return empty
+       else do { traceTc "findingValidSubstitutionsFor {" $ ppr wrapped_hole_ty
+               ; let limit = if sortSubs then Nothing else maxSubs
+               ; (discards, subs) <-
+                   setTcLevel hole_lvl $ go limit $ globalRdrEnvElts rdr_env
+                -- We split the fits into localFits and globalFits and show
+                -- local fit before global fits, since they are probably more
+                -- relevant to the user.
+               ; let (lclFits, gblFits) = partition (gre_lcl . hfEl) subs
+               ; (discards, sortedSubs) <-
+                   -- We sort the fits first, to prevent the order of
+                   -- suggestions being effected when identifiers are moved
+                   -- around in modules. We use (<*>) to expose the
+                   -- parallelism, in case it becomes useful later.
+                   if sortSubs then possiblyDiscard maxSubs <$>
+                     ((++) <$> sortByGraph (sort lclFits)
+                           <*> sortByGraph (sort gblFits))
+                   else return (discards, lclFits ++ gblFits)
+               ; traceTc "}" empty
+               ; return $ ppUnless (null sortedSubs) $
+                   hang (text "Valid substitutions include")
+                     2 (vcat (map ppr_sub sortedSubs)
+                        $$ ppWhen discards subsDiscardMsg) } }
   where
     -- We extract the type of the hole from the constraint.
     hole_ty :: TcPredType
@@ -1175,16 +1210,18 @@ validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
     wrapped_hole_ty :: TcSigmaType
     wrapped_hole_ty = foldl' wrapTypeWithImplication hole_ty implics
 
-    -- We rearrange the elements to make locals appear at the top of the list,
-    -- since they're most likely to be relevant to the user
-    localsFirst :: [GlobalRdrElt] -> [GlobalRdrElt]
+    -- We rearrange the elements to make locals appear at the top of the list
+    -- since they're most likely to be relevant to the user.
+    localsFirst :: [HoleFit] -> [HoleFit]
     localsFirst elts = lcl ++ gbl
-      where (lcl, gbl) = partition gre_lcl elts
+      where (lcl, gbl) = partition (gre_lcl . hfEl) elts
+
 
     -- For pretty printing, we look up the name and type of the substitution
     -- we found.
-    ppr_sub :: (GlobalRdrElt, Id) -> SDoc
-    ppr_sub (elt, id) = sep [ idAndTy , nest 2 (parens $ pprNameProvenance elt)]
+    ppr_sub :: HoleFit -> SDoc
+    ppr_sub (HoleFit elt id) = sep [ idAndTy
+                                   , nest 2 (parens $ pprNameProvenance elt)]
       where name = gre_name elt
             ty = varType id
             idAndTy = (pprPrefixOcc name <+> dcolon <+> pprType ty)
@@ -1242,19 +1279,43 @@ validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
          ; traceTc "}" empty
          ; return fits}
 
-    -- Kickoff the checking of the elements. The first argument
-    -- is a counter, so that we stop after finding functions up to
-    -- the limit the user gives us.
-    go :: Maybe Int -> [GlobalRdrElt] -> TcM (Bool, [(GlobalRdrElt, Id)])
+
+    -- Based on the flags, we might possibly discard some or all the
+    -- fits we've found.
+    possiblyDiscard :: Maybe Int -> [HoleFit] -> (Bool, [HoleFit])
+    possiblyDiscard (Just max) fits = (fits `lengthExceeds` max, take max fits)
+    possiblyDiscard Nothing fits = (False, fits)
+
+    -- Based on a suggestion by phadej on #ghc, we can sort the found fits
+    -- by constructing a subsumption graph, and then do a topological sort of
+    -- the graph. This makes the most specific types appear first, which are
+    -- probably those most relevant. This takes a lot of work (but results in
+    -- much more useful output), and can be disabled by
+    -- '-fno-sort-valid-substitutions'.
+    sortByGraph :: [HoleFit] -> TcM [HoleFit]
+    sortByGraph fits = go [] fits
+      where hfType :: HoleFit -> TcSigmaType
+            hfType = varType . hfId
+
+            go :: [(HoleFit, [HoleFit])] -> [HoleFit] -> TcM [HoleFit]
+            go sofar [] = return $ localsFirst topSorted
+              where toV (hf, adjs) = (hf, hfId hf, map hfId adjs)
+                    (graph, fromV, _) = graphFromEdges $ map toV sofar
+                    topSorted = map ((\(h,_,_) -> h) . fromV) $ topSort graph
+            go sofar (id:ids) =
+              do { adjs <- filterM (tcSubsumes (hfType id) . hfType) fits
+                 ; go ((id, adjs):sofar) ids }
+
+    -- Kickoff the checking of the elements.
+    go :: Maybe Int -> [GlobalRdrElt] -> TcM (Bool, [HoleFit])
     go = go_ []
 
-    -- We iterate over the elements, checking each one in turn. If
-    -- we've already found -fmax-valid-substitutions=n elements, we
-    -- look no further.
-    go_ :: [(GlobalRdrElt,Id)] -- What we've found so far.
-        -> Maybe Int           -- How many we're allowed to find, if limited.
-        -> [GlobalRdrElt]      -- The elements we've yet to check.
-        -> TcM (Bool, [(GlobalRdrElt, Id)])
+    -- We iterate over the elements, checking each one in turn for whether it
+    -- fits, and adding it to the results if it does.
+    go_ :: [HoleFit]               -- What we've found so far.
+        -> Maybe Int               -- How many we're allowed to find, if limited
+        -> [GlobalRdrElt]          -- The elements we've yet to check.
+        -> TcM (Bool, [HoleFit])
     go_ subs _ [] = return (False, reverse subs)
     go_ subs (Just 0) _ = return (True, reverse subs)
     go_ subs maxleft (el:elts) =
@@ -1266,7 +1327,7 @@ validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
              _ -> discard_it
          }
       where discard_it = go_ subs maxleft elts
-            keep_it id = go_ ((el,id):subs) ((\n -> n - 1) <$> maxleft) elts
+            keep_it id = go_ ((HoleFit el id):subs) ((\n->n-1) <$> maxleft) elts
             lookup name =
               do { thing <- tcLookup name
                  ; case thing of
@@ -1338,30 +1399,33 @@ The hole in `f` would generate the message:
     In an equation for ‘f’: f = _ "hello, world"
   • Relevant bindings include f :: [String] (bound at test.hs:6:1)
     Valid substitutions include
+      lines :: String -> [String]
+        (imported from ‘Prelude’ at test.hs:1:8-11
+         (and originally defined in ‘base-4.11.0.0:Data.OldList’))
+      words :: String -> [String]
+        (imported from ‘Prelude’ at test.hs:1:8-11
+         (and originally defined in ‘base-4.11.0.0:Data.OldList’))
+      read :: forall a. Read a => String -> a
+        (imported from ‘Prelude’ at test.hs:1:8-11
+         (and originally defined in ‘Text.Read’))
       inits :: forall a. [a] -> [[a]]
         (imported from ‘Data.List’ at test.hs:3:19-23
          (and originally defined in ‘base-4.11.0.0:Data.OldList’))
-      return :: forall (m :: * -> *). Monad m => forall a. a -> m a
+      repeat :: forall a. a -> [a]
         (imported from ‘Prelude’ at test.hs:1:8-11
-         (and originally defined in ‘GHC.Base’))
-      fail :: forall (m :: * -> *). Monad m => forall a. String -> m a
+         (and originally defined in ‘GHC.List’))
+      mempty :: forall a. Monoid a => a
         (imported from ‘Prelude’ at test.hs:1:8-11
          (and originally defined in ‘GHC.Base’))
-      mempty :: forall a. Monoid a => a
+      return :: forall (m :: * -> *). Monad m => forall a. a -> m a
         (imported from ‘Prelude’ at test.hs:1:8-11
          (and originally defined in ‘GHC.Base’))
       pure :: forall (f :: * -> *). Applicative f => forall a. a -> f a
         (imported from ‘Prelude’ at test.hs:1:8-11
          (and originally defined in ‘GHC.Base’))
-      read :: forall a. Read a => String -> a
-        (imported from ‘Prelude’ at test.hs:1:8-11
-         (and originally defined in ‘Text.Read’))
-      lines :: String -> [String]
-        (imported from ‘Prelude’ at test.hs:1:8-11
-         (and originally defined in ‘base-4.11.0.0:Data.OldList’))
-      words :: String -> [String]
+      fail :: forall (m :: * -> *). Monad m => forall a. String -> m a
         (imported from ‘Prelude’ at test.hs:1:8-11
-         (and originally defined in ‘base-4.11.0.0:Data.OldList’))
+         (and originally defined in ‘GHC.Base’))
       error :: forall (a :: TYPE r). GHC.Stack.Types.HasCallStack => [Char] -> a
         (imported from ‘Prelude’ at test.hs:1:8-11
          (and originally defined in ‘GHC.Err’))
@@ -1371,9 +1435,7 @@ The hole in `f` would generate the message:
       undefined :: forall (a :: TYPE r). GHC.Stack.Types.HasCallStack => a
         (imported from ‘Prelude’ at test.hs:1:8-11
          (and originally defined in ‘GHC.Err’))
-      repeat :: forall a. a -> [a]
-        (imported from ‘Prelude’ at test.hs:1:8-11
-         (and originally defined in ‘GHC.List’))
+
 
 Valid substitutions are found by checking top level identifiers in scope for
 whether their type is subsumed by the type of the hole. Additionally, as
@@ -1386,7 +1448,13 @@ variables are all mentioned by the type of the hole. Since checking for
 subsumption results in the side effect of type variables being unified by the
 simplifier, we need to take care to clone the variables in the hole and relevant
 constraints before checking whether an identifier fits into the hole, to avoid
-affecting the hole and later checks.
+affecting the hole and later checks. When outputting, take the fits found for
+the hole and build a subsumption graph, where fit a and fit b are connected if
+a subsumes b. We then sort the graph topologically, and output the suggestions
+in that order. This is done in order to display "more relevant" suggestions
+first where the most specific suggestions (i.e. the ones that are subsumed by
+the other suggestions) appear first. This puts suggestions such as `error` and
+`undefined` last, as seen in the example above.
 
 
 Note [Constraints include ...]
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index e0588ea914..08c781d78c 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -494,13 +494,14 @@ tcSubsumes = tcCheckHoleFit emptyBag
 
 -- | A tcSubsumes which takes into account relevant constraints, to fix trac
 -- #14273. Make sure that the constraints are cloned, since the simplifier may
--- perform unification
+-- perform unification.
 tcCheckHoleFit :: Cts -> TcSigmaType -> TcSigmaType -> TcM Bool
 tcCheckHoleFit _ hole_ty ty | hole_ty `eqType` ty = return True
 tcCheckHoleFit relevantCts hole_ty ty = discardErrs $
- do {  (_, wanted, _) <- pushLevelAndCaptureConstraints $
+ do { (_, wanted, _) <- pushLevelAndCaptureConstraints $
                            tcSubType_NC ExprSigCtxt ty hole_ty
-    ; (rem, _) <- runTcS (simpl_top $ addSimples wanted relevantCts)
+    ; rem <- runTcSDeriveds $
+               simpl_top $ addSimples wanted relevantCts
     -- We don't want any insoluble or simple constraints left,
     -- but solved implications are ok (and neccessary for e.g. undefined)
     ; return (isEmptyBag (wc_simple rem)
diff --git a/compiler/typecheck/TcSimplify.hs-boot b/compiler/typecheck/TcSimplify.hs-boot
index 979894ce3a..6455a73b6a 100644
--- a/compiler/typecheck/TcSimplify.hs-boot
+++ b/compiler/typecheck/TcSimplify.hs-boot
@@ -4,6 +4,8 @@ import GhcPrelude
 import TcRnTypes  ( TcM, Cts )
 import TcType ( TcSigmaType )
 
--- This boot file exists solely to make tcCheckHoleFit avaialble in TcErrors
+-- This boot file exists solely to make tcCheckHoleFit and tcSubsumes avaialble
+-- in TcErrors
 
+tcSubsumes :: TcSigmaType -> TcSigmaType -> TcM Bool
 tcCheckHoleFit :: Cts -> TcSigmaType -> TcSigmaType -> TcM Bool