Add valid refinement substitution suggestions for typed holes

This adds valid refinement substitution suggestions for typed holes and
documentation thereof.

Inspired by Agda's refinement facilities, this extends the typed holes
feature to be able to search for valid refinement substitutions, which
are substitutions that have one or more holes in them.

When the flag `-frefinement-level-substitutions=n` where `n > 0` is
passed, we also look for valid refinement substitutions, i.e.
substitutions that are valid, but adds more holes. Consider the
following:

  f :: [Integer] -> Integer
  f = _

Here the valid substitutions suggested will be (with the new
`-funclutter-valid-substitutions` flag for less verbosity set):

```
  Valid substitutions include
    f :: [Integer] -> Integer
    product :: forall (t :: * -> *).
              Foldable t => forall a. Num a => t a -> a
    sum :: forall (t :: * -> *).
          Foldable t => forall a. Num a => t a -> a
    maximum :: forall (t :: * -> *).
              Foldable t => forall a. Ord a => t a -> a
    minimum :: forall (t :: * -> *).
              Foldable t => forall a. Ord a => t a -> a
    head :: forall a. [a] -> a
    (Some substitutions suppressed; use -fmax-valid-substitutions=N or
-fno-max-valid-substitutions)
```

When the `-frefinement-level-substitutions=1` flag is given, we
additionally compute and report valid refinement substitutions:

```
  Valid refinement substitutions include
    foldl1 _ :: forall (t :: * -> *).
                Foldable t => forall a. (a -> a -> a) -> t a -> a
    foldr1 _ :: forall (t :: * -> *).
                Foldable t => forall a. (a -> a -> a) -> t a -> a
    head _ :: forall a. [a] -> a
    last _ :: forall a. [a] -> a
    error _ :: forall (a :: TYPE r).
                GHC.Stack.Types.HasCallStack => [Char] -> a
    errorWithoutStackTrace _ :: forall (a :: TYPE r). [Char] -> a
    (Some refinement substitutions suppressed; use
-fmax-refinement-substitutions=N or -fno-max-refinement-substitutions)
```

Which are substitutions with holes in them. This allows e.g. beginners
to discover the fold functions and similar.

We find these refinement suggestions by considering substitutions that
don't fit the type of the hole, but ones that would fit if given an
additional argument. We do this by creating a new type variable with
newOpenFlexiTyVarTy (e.g. `t_a1/m[tau:1]`), and then considering
substitutions of the type `t_a1/m[tau:1] -> v` where `v` is the type of
the hole. Since the simplifier is free to unify this new type variable
with any type (and it is cloned before each check to avoid
side-effects), we can now discover any identifiers that would fit if
given another identifier of a suitable type. This is then generalized
so that we can consider any number of additional arguments by setting
the `-frefinement-level-substitutions` flag to any number, and then
considering substitutions like e.g. `foldl _ _` with two additional
arguments.

This can e.g. help beginners discover the `fold` functions.
This could also help more advanced users figure out which morphisms
they can use when arrow chasing.
Then you could write `m = _ . m2 . m3` where `m2` and `m3` are some
morphisms, and not only get exact fits, but also help in finding
morphisms that might get you a little bit closer to where you want to
go in the diagram.

Reviewers: bgamari

Reviewed By: bgamari

Subscribers: rwbarton, thomie, carter

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

9 files changed, 857 insertions, 79 deletions

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 6cea932bf5..dc4967d136 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -555,7 +555,9 @@ data GeneralFlag
    | Opt_PprShowTicks
    | Opt_ShowHoleConstraints
    | Opt_NoShowValidSubstitutions
+   | Opt_UnclutterValidSubstitutions
    | Opt_NoSortValidSubstitutions
+   | Opt_AbstractRefSubstitutions
    | Opt_ShowLoadedModules
 
    -- Suppress all coercions, them replacing with '...'
@@ -805,6 +807,12 @@ data DynFlags = DynFlags {
                                         --   to show in type error messages
   maxValidSubstitutions :: Maybe Int,   -- ^ Maximum number of substitutions to
                                         --   show in typed hole error messages
+  maxRefSubstitutions   :: Maybe Int,   -- ^ Maximum number of refinement
+                                        --   substitutions to show in typed hole
+                                        --   error messages
+  refLevelSubstitutions :: Maybe Int,   -- ^ Maximum level of refinement for
+                                        --   refinement substitutions in typed
+                                        --   typed hole error messages
   maxUncoveredPatterns  :: Int,         -- ^ Maximum number of unmatched patterns to show
                                         --   in non-exhaustiveness warnings
   simplTickFactor       :: Int,         -- ^ Multiplier for simplifier ticks
@@ -1665,6 +1673,8 @@ defaultDynFlags mySettings myLlvmTargets =
         ruleCheck               = Nothing,
         maxRelevantBinds        = Just 6,
         maxValidSubstitutions   = Just 6,
+        maxRefSubstitutions     = Just 6,
+        refLevelSubstitutions   = Nothing,
         maxUncoveredPatterns    = 4,
         simplTickFactor         = 100,
         specConstrThreshold     = Just 2000,
@@ -3290,6 +3300,14 @@ dynamic_flags_deps = [
       (intSuffix (\n d -> d { maxValidSubstitutions = Just n }))
   , make_ord_flag defFlag "fno-max-valid-substitutions"
       (noArg (\d -> d { maxValidSubstitutions = Nothing }))
+  , make_ord_flag defFlag "fmax-refinement-substitutions"
+      (intSuffix (\n d -> d { maxRefSubstitutions = Just n }))
+  , make_ord_flag defFlag "fno-max-refinement-substitutions"
+      (noArg (\d -> d { maxRefSubstitutions = Nothing }))
+  , make_ord_flag defFlag "frefinement-level-substitutions"
+      (intSuffix (\n d -> d { refLevelSubstitutions = Just n }))
+  , make_ord_flag defFlag "fno-refinement-level-substitutions"
+      (noArg (\d -> d { refLevelSubstitutions = Nothing }))
   , make_ord_flag defFlag "fmax-uncovered-patterns"
       (intSuffix (\n d -> d { maxUncoveredPatterns = n }))
   , make_ord_flag defFlag "fsimplifier-phases"
@@ -3904,6 +3922,8 @@ fFlagsDeps = [
   flagSpec "show-hole-constraints"            Opt_ShowHoleConstraints,
   flagSpec "no-show-valid-substitutions"      Opt_NoShowValidSubstitutions,
   flagSpec "no-sort-valid-substitutions"      Opt_NoSortValidSubstitutions,
+  flagSpec "abstract-refinement-substitutions" Opt_AbstractRefSubstitutions,
+  flagSpec "unclutter-valid-substitutions"    Opt_UnclutterValidSubstitutions,
   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 8d2238a985..1dba42d7b7 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -61,7 +61,7 @@ import Pair
 import qualified GHC.LanguageExtensions as LangExt
 import FV ( fvVarList, fvVarSet, unionFV )
 
-import Control.Monad    ( when, filterM )
+import Control.Monad    ( when, filterM, replicateM )
 import Data.Foldable    ( toList )
 import Data.List        ( partition, mapAccumL, nub
                         , sortBy, sort, unfoldr, foldl' )
@@ -1152,8 +1152,12 @@ 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 }
+-- element that was checked, the Id of that element as found by `tcLookup`,
+-- and the refinement level of the fit, which is the number of extra argument
+-- holes that this fit uses (e.g. if hfRefLvl is 2, the fit is for `Id _ _`).
+data HoleFit = HoleFit { hfEl :: GlobalRdrElt -- The element that was checked.
+                       , hfId :: Id           -- the elements id in the TcM.
+                       , hfRefLvl :: Int }    -- The number of holes in this fit
 
 -- We define an Eq and Ord instance to be able to build a graph.
 instance Eq HoleFit where
@@ -1161,54 +1165,139 @@ instance Eq HoleFit where
 
 -- 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.
+-- which is used to compare Ids. When comparing, we want HoleFits with a lower
+-- refinement level to come first.
 instance Ord HoleFit where
-  compare = compare `on` (gre_name . hfEl)
+  compare a b = cmp a b
+    where cmp  = if (hfRefLvl a) == (hfRefLvl b)
+                 then compare `on` (gre_name . hfEl)
+                 else compare `on` hfRefLvl
+
+instance Outputable HoleFit where
+    ppr = pprHoleFit False
+
+-- For pretty printing hole fits, we display the name and type of the fit,
+-- with added '_' to represent any extra arguments in case of a non-zero
+-- refinement level.
+pprHoleFit :: Bool -> HoleFit -> SDoc
+pprHoleFit showProv hf =
+    if showProv then sep [idAndTy, nest 2 provenance] else idAndTy
+    where name = gre_name (hfEl hf)
+          ty = varType (hfId hf)
+          holeVs = hsep $ replicate (hfRefLvl hf) $ text "_"
+          idAndTy = (pprPrefixOcc name <+> holeVs <+> dcolon <+> pprType ty)
+          provenance = parens $ pprNameProvenance (hfEl hf)
+
 
 -- See Note [Valid substitutions include ...]
 validSubstitutions :: [Ct] -> ReportErrCtxt -> Ct -> TcM SDoc
 validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
   do { rdr_env <- getGlobalRdrEnv
-     ; 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) } }
+     ; maxVSubs <- maxValidSubstitutions <$> getDynFlags
+     ; showProvenance <- not <$> goptM Opt_UnclutterValidSubstitutions
+     ; graphSortSubs <- not <$> goptM Opt_NoSortValidSubstitutions
+     ; refLevel <- refLevelSubstitutions <$> getDynFlags
+     ; traceTc "findingValidSubstitutionsFor { " $ ppr ct
+     ; traceTc "hole_lvl is:" $ ppr hole_lvl
+     ; traceTc "implics are: " $ ppr implics
+     ; traceTc "simples are: " $ ppr simples
+     ; (searchDiscards, subs) <-
+        findSubs graphSortSubs maxVSubs rdr_env 0 (wrapped_hole_ty, [])
+     ; (vDiscards, sortedSubs) <-
+        sortSubs graphSortSubs maxVSubs searchDiscards subs
+     ; let vMsg = ppUnless (null subs) $
+                    hang (text "Valid substitutions include") 2 $
+                    (vcat (map (pprHoleFit showProvenance) sortedSubs)
+                     $$ ppWhen vDiscards subsDiscardMsg)
+     ; refMsg <- if refLevel >= (Just 0) then
+         do { maxRSubs <- maxRefSubstitutions <$> getDynFlags
+            -- We can use from just, since we know that Nothing >= _ is False.
+            ; let refLvls = [1..(fromJust refLevel)]
+            -- We make a new refinement type for each level of refinement, where
+            -- the level of refinement indicates number of additional arguments
+            -- to allow.
+            ; ref_tys <- mapM (\l -> mkRefTy l >>= return . (,) l) refLvls
+            ; traceTc "ref_tys are" $ ppr ref_tys
+            ; refDs <-
+                mapM (uncurry $ findSubs graphSortSubs maxRSubs rdr_env) ref_tys
+            ; (rDiscards, sortedRSubs) <-
+                sortSubs graphSortSubs maxRSubs (any fst refDs) $
+                    concatMap snd refDs
+            ; return $
+                ppUnless (null sortedRSubs) $
+                  hang (text "Valid refinement substitutions include") 2 $
+                  (vcat (map (pprHoleFit showProvenance) sortedRSubs)
+                    $$ ppWhen rDiscards refSubsDiscardMsg) }
+       else return empty
+     ; traceTc "}" empty
+     ; return (vMsg $$ refMsg)}
   where
+    hole_loc = ctEvLoc $ ctEvidence ct
+    hole_lvl = ctLocLevel $ hole_loc
+
+    -- We make a refinement type by adding a new type variable in front
+    -- of the type of t h hole, going from e.g. [Integer] -> Integer
+    -- to t_a1/m[tau:1] -> [Integer] -> Integer. This allows the simplifier
+    -- to unify the new type variable with any type, allowing us
+    -- to suggest a "refinement substitution", like `(foldl1 _)` instead
+    -- of only concrete substitutions like `sum`.
+    mkRefTy :: Int -> TcM (TcType, [TcType])
+    mkRefTy refLvl = (\v -> (wrapHoleWithArgs v, v)) <$> newTyVarTys
+     where newTyVarTys = replicateM refLvl newOpenFlexiTyVarTy
+           wrapHoleWithArgs args = (wrap_ty . mkFunTys args) hole_ty
+
+
+    sortSubs :: Bool          -- Whether we should sort the subs or not
+                              -- by subsumption or not
+             -> Maybe Int     -- How many we should output, if limited.
+             -> Bool          -- Whether there were any discards in the
+                              -- initial search
+             -> [HoleFit]     -- The subs to sort
+             -> TcM (Bool, [HoleFit])
+    -- If we don't want to sort by the subsumption graph, we just sort it
+    -- such that local fits come before global fits, since local fits are
+    -- probably more relevant to the user.
+    sortSubs False _ discards subs = return (discards, sortedFits)
+        where (lclFits, gblFits) = partition (gre_lcl . hfEl) subs
+              sortedFits = lclFits ++ gblFits
+    -- 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.
+    sortSubs _ limit _ subs = possiblyDiscard limit <$>
+                                ((++) <$> sortByGraph (sort lclFits)
+                                      <*> sortByGraph (sort gblFits))
+        where (lclFits, gblFits) = partition (gre_lcl . hfEl) subs
+
+
+    findSubs :: Bool               -- Whether we should sort the subs or not
+             -> Maybe Int          -- How many we should output, if limited
+             -> GlobalRdrEnv       -- The elements to check whether fit
+             -> Int                -- The refinement level of the hole
+             -> (TcType, [TcType]) -- The type to check for fits and ref vars
+             -> TcM (Bool, [HoleFit])
+    -- We don't check if no output is desired.
+    findSubs _ (Just 0) _ _ _ = return (False, [])
+    findSubs sortSubs maxSubs rdr_env refLvl ht@(hole_ty, _) =
+      do { traceTc "checkingSubstitutionsFor {" $ ppr $ hole_ty
+         ; let limit = if sortSubs then Nothing else maxSubs
+         ; (discards, subs) <- setTcLevel hole_lvl $
+                                 go limit ht refLvl $
+                                    globalRdrEnvElts rdr_env
+         ; traceTc "}" empty
+         ; return (discards, subs) }
     -- We extract the type of the hole from the constraint.
     hole_ty :: TcPredType
     hole_ty = ctPred ct
-    hole_loc = ctEvLoc $ ctEvidence ct
-    hole_lvl = ctLocLevel $ hole_loc
     hole_fvs = tyCoFVsOfType hole_ty
 
     -- For checking, we wrap the type of the hole with all the givens
     -- from all the implications in the context.
+    wrap_ty :: TcType -> TcSigmaType
+    wrap_ty ty = foldl' wrapTypeWithImplication ty implics
+
     wrapped_hole_ty :: TcSigmaType
-    wrapped_hole_ty = foldl' wrapTypeWithImplication hole_ty implics
+    wrapped_hole_ty = wrap_ty hole_ty
 
     -- 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.
@@ -1217,15 +1306,6 @@ validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
       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 :: 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)
-
     -- These are the constraints whose every free unification variable is
     -- mentioned in the type of the hole.
     relevantCts :: [Ct]
@@ -1251,12 +1331,12 @@ validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
     -- constraints. Note that since we only pick constraints such that all their
     -- free variables are mentioned by the hole, the free variables of the hole
     -- are all the free variables of the constraints as well.
-    getHoleCloningSubst :: TcM TCvSubst
-    getHoleCloningSubst = mkTvSubstPrs <$> getClonedVars
+    getHoleCloningSubst :: TcType -> TcM TCvSubst
+    getHoleCloningSubst hole_ty = mkTvSubstPrs <$> getClonedVars
       where cloneFV :: TyVar -> TcM (TyVar, Type)
             cloneFV fv = ((,) fv) <$> newFlexiTyVarTy (varType fv)
             getClonedVars :: TcM [(TyVar, Type)]
-            getClonedVars = mapM cloneFV (fvVarList hole_fvs)
+            getClonedVars = mapM cloneFV (fvVarList $ tyCoFVsOfType hole_ty)
 
     -- This applies the given substitution to the given constraint.
     applySubToCt :: TCvSubst -> Ct -> Ct
@@ -1269,16 +1349,24 @@ validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
     -- To check: Clone all relevant cts and the hole
     -- then solve the subsumption check AND check that all other
     -- the other constraints were solved.
-    fitsHole :: Type -> TcM Bool
-    fitsHole typ =
+    fitsHole :: (TcType, [TcType]) -> Type -> TcM Bool
+    fitsHole (hole_ty, vars) typ =
       do { traceTc "checkingFitOf {" $ ppr typ
-         ; cloneSub <- getHoleCloningSubst
-         ; let cHoleTy = substTy cloneSub wrapped_hole_ty
+         ; cloneSub <- getHoleCloningSubst hole_ty
+         ; let cHoleTy = substTy cloneSub hole_ty
                cCts = map (applySubToCt cloneSub) relevantCts
-         ; fits <- tcCheckHoleFit (listToBag cCts) cHoleTy typ
-         ; traceTc "}" empty
-         ; return fits}
+               cVars = map (substTy cloneSub) vars
 
+         ; absFits <- tcCheckHoleFit (listToBag cCts) cHoleTy typ
+         ; traceTc "}" empty
+         -- We'd like to avoid refinement suggestions like `id _ _` or
+         -- `head _ _`, and only suggest refinements where our all phantom
+         -- variables got unified during the checking. This can be disabled
+         -- with the `-fabstract-refinement-substitutions` flag.
+         ; if absFits && (not . null) vars then
+            goptM Opt_AbstractRefSubstitutions `orM`
+              allM isFilledMetaTyVar (fvVarList $ tyCoFVsOfTypes cVars)
+            else return absFits }
 
     -- Based on the flags, we might possibly discard some or all the
     -- fits we've found.
@@ -1298,7 +1386,8 @@ validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
             hfType = varType . hfId
 
             go :: [(HoleFit, [HoleFit])] -> [HoleFit] -> TcM [HoleFit]
-            go sofar [] = return $ localsFirst topSorted
+            go sofar [] = do { traceTc "subsumptionGraph was" $ ppr 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
@@ -1307,27 +1396,30 @@ validSubstitutions simples (CEC {cec_encl = implics}) ct | isExprHoleCt ct =
                  ; go ((id, adjs):sofar) ids }
 
     -- Kickoff the checking of the elements.
-    go :: Maybe Int -> [GlobalRdrElt] -> TcM (Bool, [HoleFit])
+    go :: Maybe Int -> (TcType, [TcType]) -> Int
+        -> [GlobalRdrElt] -> TcM (Bool, [HoleFit])
     go = go_ []
 
     -- 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.
+    go_ :: [HoleFit]          -- What we've found so far.
+        -> Maybe Int          -- How many we're allowed to find, if limited
+        -> (TcType, [TcType]) -- The type to check, and refinement variables.
+        -> Int                -- The refinement level of the hole we're checking
+        -> [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) =
+    go_ subs _ _ _ [] = return (False, reverse subs)
+    go_ subs (Just 0) _ _ _ = return (True, reverse subs)
+    go_ subs maxleft t r (el:elts) =
       do { traceTc "lookingUp" $ ppr el
          ; maybeThing <- lookup (gre_name el)
          ; case maybeThing of
-             Just id -> do { fits <- fitsHole (varType id)
-                           ; if fits then (keep_it id) else discard_it }
-             _ -> discard_it
-         }
-      where discard_it = go_ subs maxleft elts
-            keep_it id = go_ ((HoleFit el id):subs) ((\n->n-1) <$> maxleft) elts
+             Just id -> do { fits <- fitsHole t (varType id)
+                           ; if fits then keep_it (HoleFit el id r)
+                                     else discard_it }
+             _ -> discard_it }
+      where discard_it = go_ subs maxleft t r elts
+            keep_it fit = go_ (fit:subs) ((\n -> n - 1) <$> maxleft) t r elts
             lookup name =
               do { thing <- tcLookup name
                  ; case thing of
@@ -1456,6 +1548,60 @@ 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.
 
+When the flag `-frefinement-level-substitutions=n` where `n > 0` is passed, we
+also look for valid refinement substitutions, i.e. substitutions that are valid,
+but adds more holes. Consider the following:
+
+  f :: [Integer] -> Integer
+  f = _
+
+Here the valid substitutions suggested will be (with the
+`-funclutter-valid-substitutions` flag set):
+
+  Valid substitutions include
+    f :: [Integer] -> Integer
+    product :: forall (t :: * -> *).
+              Foldable t => forall a. Num a => t a -> a
+    sum :: forall (t :: * -> *).
+          Foldable t => forall a. Num a => t a -> a
+    maximum :: forall (t :: * -> *).
+              Foldable t => forall a. Ord a => t a -> a
+    minimum :: forall (t :: * -> *).
+              Foldable t => forall a. Ord a => t a -> a
+    head :: forall a. [a] -> a
+    (Some substitutions suppressed;
+        use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)
+
+When the `-frefinement-level-substitutions=1` flag is given, we additionally
+compute and report valid refinement substitutions:
+
+  Valid refinement substitutions include
+    foldl1 _ :: forall (t :: * -> *).
+                Foldable t => forall a. (a -> a -> a) -> t a -> a
+    foldr1 _ :: forall (t :: * -> *).
+                Foldable t => forall a. (a -> a -> a) -> t a -> a
+    head _ :: forall a. [a] -> a
+    last _ :: forall a. [a] -> a
+    error _ :: forall (a :: TYPE r).
+                GHC.Stack.Types.HasCallStack => [Char] -> a
+    errorWithoutStackTrace _ :: forall (a :: TYPE r). [Char] -> a
+    (Some refinement substitutions suppressed;
+      use -fmax-refinement-substitutions=N or -fno-max-refinement-substitutions)
+
+Which are substitutions with holes in them. This allows e.g. beginners to
+discover the fold functions and similar.
+
+We find these refinement suggestions by considering substitutions that don't
+fit the type of the hole, but ones that would fit if given an additional
+argument. We do this by creating a new type variable with `newOpenFlexiTyVarTy`
+(e.g. `t_a1/m[tau:1]`), and then considering substitutions of the type
+`t_a1/m[tau:1] -> v` where `v` is the type of the hole. Since the simplifier is
+free to unify this new type variable with any type (and it is cloned before each
+check to avoid side-effects), we can now discover any identifiers that would fit
+if given another identifier of a suitable type. This is then generalized so that
+we can consider any number of additional arguments by setting the
+`-frefinement-level-substitutions` flag to any number, and then considering
+substitutions like e.g. `foldl _ _` with two additional arguments.
 
 Note [Constraints include ...]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -3166,6 +3312,12 @@ subsDiscardMsg =
     text "(Some substitutions suppressed;" <+>
     text "use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)"
 
+refSubsDiscardMsg :: SDoc
+refSubsDiscardMsg =
+    text "(Some refinement substitutions suppressed;" <+>
+    text "use -fmax-refinement-substitutions=N" <+>
+    text "or -fno-max-refinement-substitutions)"
+
 -----------------------
 warnDefaulting :: [Ct] -> Type -> TcM ()
 warnDefaulting wanteds default_ty
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index d2c8dd8a43..4b11fa6114 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -2592,17 +2592,17 @@ pprEvVarWithType v = ppr v <+> dcolon <+> pprType (evVarPred v)
 
 -- | Wraps the given type with the constraints (via ic_given) in the given
 -- implication, according to the variables mentioned (via ic_skols)
--- in the implication.
+-- in the implication, but taking care to only wrap those variables
+-- that are mentioned in the type or the implication.
 wrapTypeWithImplication :: Type -> Implication -> Type
-wrapTypeWithImplication ty impl =
-  wrapType ty (ic_skols impl) (map idType $ ic_given impl)
+wrapTypeWithImplication ty impl = wrapType ty mentioned_skols givens
+    where givens = map idType $ ic_given impl
+          skols = ic_skols impl
+          freeVars = fvVarSet $ tyCoFVsOfTypes (ty:givens)
+          mentioned_skols = filter (`elemVarSet` freeVars) skols
 
 wrapType :: Type -> [TyVar] -> [PredType] -> Type
-wrapType ty skols givens =
-    wrapWithAllSkols $ mkFunTys givens ty
-    where forAllTy :: Type -> TyVar -> Type
-          forAllTy ty tv = mkForAllTy tv Specified ty
-          wrapWithAllSkols ty = foldl forAllTy ty skols
+wrapType ty skols givens = mkSpecForAllTys skols $ mkFunTys givens ty
 
 
 {-
diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst
index d213a5cdba..439f4d2555 100644
--- a/docs/users_guide/glasgow_exts.rst
+++ b/docs/users_guide/glasgow_exts.rst
@@ -11051,6 +11051,12 @@ for typed holes:
                 (imported from ‘Prelude’ at show_constraints.hs:1:8-11
                 (and originally defined in ‘GHC.Err’))
 
+.. _typed-hole-valid-substitutions:
+
+Valid Substitutions
+-------------------
+GHC sometimes suggests valid substitutions for typed holes, which is
+configurable by a few flags.
 
 .. ghc-flag:: -fno-show-valid-substitutions
     :shortdesc: Disables showing a list of valid substitutions for typed holes
@@ -11146,9 +11152,115 @@ for typed holes:
 
     The list of valid substitutions is limited by displaying up to 6
     substitutions per hole. The number of substitutions shown can be set by this
-    flag. Turning the limit off with ``-fno-max-valid-substitutions`` displays
-    all the found substitutions. 
+    flag. Turning the limit off with :ghc-flag:`-fno-max-valid-substitutions`
+    displays all found substitutions.
+
+.. ghc-flag:: -funclutter-valid-substitutions
+    :shortdesc: Unclutter the list of valid substitutions by not showing
+        provenance of suggestion.
+    :type: dynamic
+    :category: verbosity
+
+    :default: off
+
+    This flag can be toggled to decrease the verbosity of the valid
+    substitution suggestions by not showing the provenance the suggestions.
+
+.. _typed-holes-refinement-substitutions:
+
+Refinement Substitutions
+~~~~~~~~~~~~~~~~~~~~~~~~
+
+When the flag :ghc-flag:`-frefinement-level-substitutions=⟨n⟩` is set to an
+``n`` larger than ``0``, GHC will offer up a list of valid refinement
+substitutions, which are valid substitutions that need up to ``n`` levels of
+additional refinement to be complete, where each level represents an additional
+hole in the substitution that requires filling in.  As an example, consider the
+hole in ::
+
+  f :: [Integer] -> Integer
+  f = _
+
+When the refinement level is not set, it will only offer valid substitutions
+suggestions: ::
+
+  Valid substitutions include
+    f :: [Integer] -> Integer
+    product :: forall (t :: * -> *).
+              Foldable t => forall a. Num a => t a -> a
+    sum :: forall (t :: * -> *).
+          Foldable t => forall a. Num a => t a -> a
+    maximum :: forall (t :: * -> *).
+              Foldable t => forall a. Ord a => t a -> a
+    minimum :: forall (t :: * -> *).
+              Foldable t => forall a. Ord a => t a -> a
+    head :: forall a. [a] -> a
+    (Some substitutions suppressed; use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)
+
+However, with :ghc-flag:`-frefinement-level-substitutions=⟨n⟩` set to e.g. `1`,
+it will additionally offer up a list of refinement substitutions, in this case: ::
+
+  Valid refinement substitutions include
+    foldl1 _ :: forall (t :: * -> *).
+                Foldable t => forall a. (a -> a -> a) -> t a -> a
+    foldr1 _ :: forall (t :: * -> *).
+                Foldable t => forall a. (a -> a -> a) -> t a -> a
+    head _ :: forall a. [a] -> a
+    last _ :: forall a. [a] -> a
+    error _ :: forall (a :: TYPE r).
+                GHC.Stack.Types.HasCallStack => [Char] -> a
+    errorWithoutStackTrace _ :: forall (a :: TYPE r). [Char] -> a
+    (Some refinement substitutions suppressed;
+      use -fmax-refinement-substitutions=N or -fno-max-refinement-substitutions)
+
+Which shows that the hole could be replaced with e.g. ``foldl1 _``. While not
+fixing the hole, this can help users understand what options they have.
+ 
+.. ghc-flag:: -frefinement-level-substitutions=⟨n⟩
+    :shortdesc: *default: off.* Sets the level of refinement of the
+         refinement substitutions, where level ``n`` means that substitutions
+         of up to ``n`` holes will be considered.
+    :type: dynamic
+    :reverse: -fno-refinement-level-substitutions
+    :category: verbosity
 
+    :default: off
+
+    The list of valid refinement substitutions is generated by considering
+    substitutions with a varying amount of additional holes. The amount of
+    holes in a refinement can be set by this flag. If the flag is set to 0
+    or not set at all, no valid refinement substitutions will be suggested.
+
+.. ghc-flag:: -fabstract-refinement-substitutions
+    :shortdesc: *default: off.* Toggles whether refinements where one or more
+         or more of the holes are abstract are reported.
+    :type: dynamic
+    :reverse: -fno-abstract-refinement-substitutions
+    :category: verbosity
+
+    :default: off
+
+    Valid list of valid refinement substitutions can often grow large when
+    the refinement level is ``>= 2``, with holes like ``head _ _`` or
+    ``fst _ _``, which are valid refinements, but which are unlikely to be
+    relevant since one or more of the holes are still completely open, in that
+    neither the type nor kind of those holes are constrained by the proposed
+    identifier at all. By default, such holes are not reported. By turning this
+    flag on, such holes are included in the list of valid refinement substitutions.
+
+.. ghc-flag:: -fmax-refinement-substitutions=⟨n⟩
+    :shortdesc: *default: 6.* Set the maximum number of refinement substitutions
+         for typed holes to display in type error messages.
+    :type: dynamic
+    :reverse: -fno-max-refinement-substitutions
+    :category: verbosity
+
+    :default: 6
+
+    The list of valid refinement substitutions is limited by displaying up to 6
+    substitutions per hole. The number of substitutions shown can be set by this
+    flag. Turning the limit off with :ghc-flag:`-fno-max-refinement-substitutions`
+    displays all found substitutions.
 
 .. _partial-type-signatures:
 
diff --git a/testsuite/tests/typecheck/should_compile/abstract_refinement_substitutions.hs b/testsuite/tests/typecheck/should_compile/abstract_refinement_substitutions.hs
new file mode 100644
index 0000000000..4949632308
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/abstract_refinement_substitutions.hs
@@ -0,0 +1,7 @@
+module AbstractRefinementSubstitutions where
+
+f :: [Integer] -> Integer
+f = _
+
+g :: [Integer] -> Integer
+g = _ 0
diff --git a/testsuite/tests/typecheck/should_compile/abstract_refinement_substitutions.stderr b/testsuite/tests/typecheck/should_compile/abstract_refinement_substitutions.stderr
new file mode 100644
index 0000000000..1b8bfdec8a
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/abstract_refinement_substitutions.stderr
@@ -0,0 +1,290 @@
+
+abstract_refinement_substitutions.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
+    • Found hole: _ :: [Integer] -> Integer
+    • In the expression: _
+      In an equation for ‘f’: f = _
+    • Relevant bindings include
+        f :: [Integer] -> Integer
+          (bound at abstract_refinement_substitutions.hs:4:1)
+      Valid substitutions include
+        f :: [Integer] -> Integer
+          (defined at abstract_refinement_substitutions.hs:4:1)
+        g :: [Integer] -> Integer
+          (defined at abstract_refinement_substitutions.hs:7:1)
+        product :: forall (t :: * -> *).
+                   Foldable t =>
+                   forall a. Num a => t a -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Foldable’))
+        sum :: forall (t :: * -> *).
+               Foldable t =>
+               forall a. Num a => t a -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Foldable’))
+        maximum :: forall (t :: * -> *).
+                   Foldable t =>
+                   forall a. Ord a => t a -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Foldable’))
+        minimum :: forall (t :: * -> *).
+                   Foldable t =>
+                   forall a. Ord a => t a -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Foldable’))
+        head :: forall a. [a] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.List’))
+        last :: forall a. [a] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.List’))
+        undefined :: forall (a :: TYPE r).
+                     GHC.Stack.Types.HasCallStack =>
+                     a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
+      Valid refinement substitutions include
+        foldr _ _ :: forall (t :: * -> *).
+                     Foldable t =>
+                     forall a b. (a -> b -> b) -> b -> t a -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Foldable’))
+        foldl1 _ :: forall (t :: * -> *).
+                    Foldable t =>
+                    forall a. (a -> a -> a) -> t a -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Foldable’))
+        foldr1 _ :: forall (t :: * -> *).
+                    Foldable t =>
+                    forall a. (a -> a -> a) -> t a -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Foldable’))
+        foldl _ _ :: forall (t :: * -> *).
+                     Foldable t =>
+                     forall b a. (b -> a -> b) -> b -> t a -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Foldable’))
+        last _ _ :: forall a. [a] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.List’))
+        head _ _ :: forall a. [a] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.List’))
+        head _ :: forall a. [a] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.List’))
+        last _ :: forall a. [a] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.List’))
+        (!!) _ _ :: forall a. [a] -> Int -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.List’))
+        undefined _ :: forall (a :: TYPE r).
+                       GHC.Stack.Types.HasCallStack =>
+                       a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
+        errorWithoutStackTrace _ :: forall (a :: TYPE r). [Char] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
+        error _ :: forall (a :: TYPE r).
+                   GHC.Stack.Types.HasCallStack =>
+                   [Char] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
+        error _ _ :: forall (a :: TYPE r).
+                     GHC.Stack.Types.HasCallStack =>
+                     [Char] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
+        errorWithoutStackTrace _ _ :: forall (a :: TYPE r). [Char] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
+        id _ :: forall a. a -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        flip _ _ :: forall a b c. (a -> b -> c) -> b -> a -> c
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        const _ :: forall a b. a -> b -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        asTypeOf _ _ :: forall a. a -> a -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        const _ _ :: forall a b. a -> b -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        (.) _ _ :: forall b c a. (b -> c) -> (a -> b) -> a -> c
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        ($!) _ :: forall a (b :: TYPE r). (a -> b) -> a -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        uncurry _ _ :: forall a b c. (a -> b -> c) -> (a, b) -> c
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Tuple’))
+        curry _ _ :: forall a b c. ((a, b) -> c) -> a -> b -> c
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Tuple’))
+        ($) _ :: forall a (b :: TYPE r). (a -> b) -> a -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        ($) _ _ :: forall a (b :: TYPE r). (a -> b) -> a -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        ($!) _ _ :: forall a (b :: TYPE r). (a -> b) -> a -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        id _ _ :: forall a. a -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        snd _ :: forall a b. (a, b) -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Tuple’))
+        snd _ _ :: forall a b. (a, b) -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Tuple’))
+        fst _ :: forall a b. (a, b) -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Tuple’))
+        fst _ _ :: forall a b. (a, b) -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Tuple’))
+        seq _ _ :: forall a b. a -> b -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Prim’))
+        undefined _ _ :: forall (a :: TYPE r).
+                         GHC.Stack.Types.HasCallStack =>
+                         a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
+
+abstract_refinement_substitutions.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
+    • Found hole: _ :: Integer -> [Integer] -> Integer
+    • In the expression: _
+      In the expression: _ 0
+      In an equation for ‘g’: g = _ 0
+    • Relevant bindings include
+        g :: [Integer] -> Integer
+          (bound at abstract_refinement_substitutions.hs:7:1)
+      Valid substitutions include
+        const :: forall a b. a -> b -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        undefined :: forall (a :: TYPE r).
+                     GHC.Stack.Types.HasCallStack =>
+                     a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
+      Valid refinement substitutions include
+        foldr _ :: forall (t :: * -> *).
+                   Foldable t =>
+                   forall a b. (a -> b -> b) -> b -> t a -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Foldable’))
+        foldl _ :: forall (t :: * -> *).
+                   Foldable t =>
+                   forall b a. (b -> a -> b) -> b -> t a -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Foldable’))
+        last _ _ :: forall a. [a] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.List’))
+        head _ _ :: forall a. [a] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.List’))
+        head _ :: forall a. [a] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.List’))
+        last _ :: forall a. [a] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.List’))
+        (!!) _ _ :: forall a. [a] -> Int -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.List’))
+        undefined _ :: forall (a :: TYPE r).
+                       GHC.Stack.Types.HasCallStack =>
+                       a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
+        errorWithoutStackTrace _ :: forall (a :: TYPE r). [Char] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
+        error _ :: forall (a :: TYPE r).
+                   GHC.Stack.Types.HasCallStack =>
+                   [Char] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
+        error _ _ :: forall (a :: TYPE r).
+                     GHC.Stack.Types.HasCallStack =>
+                     [Char] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
+        errorWithoutStackTrace _ _ :: forall (a :: TYPE r). [Char] -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
+        id _ :: forall a. a -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        flip _ :: forall a b c. (a -> b -> c) -> b -> a -> c
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        flip _ _ :: forall a b c. (a -> b -> c) -> b -> a -> c
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        const _ :: forall a b. a -> b -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        asTypeOf _ _ :: forall a. a -> a -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        const _ _ :: forall a b. a -> b -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        (.) _ _ :: forall b c a. (b -> c) -> (a -> b) -> a -> c
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        ($!) _ _ :: forall a (b :: TYPE r). (a -> b) -> a -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        uncurry _ _ :: forall a b c. (a -> b -> c) -> (a, b) -> c
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Tuple’))
+        curry _ :: forall a b c. ((a, b) -> c) -> a -> b -> c
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Tuple’))
+        curry _ _ :: forall a b c. ((a, b) -> c) -> a -> b -> c
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Tuple’))
+        ($) _ :: forall a (b :: TYPE r). (a -> b) -> a -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        ($) _ _ :: forall a (b :: TYPE r). (a -> b) -> a -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        ($!) _ :: forall a (b :: TYPE r). (a -> b) -> a -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        id _ _ :: forall a. a -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Base’))
+        snd _ :: forall a b. (a, b) -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Tuple’))
+        snd _ _ :: forall a b. (a, b) -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Tuple’))
+        fst _ :: forall a b. (a, b) -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Tuple’))
+        fst _ _ :: forall a b. (a, b) -> a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘Data.Tuple’))
+        seq _ _ :: forall a b. a -> b -> b
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Prim’))
+        undefined _ _ :: forall (a :: TYPE r).
+                         GHC.Stack.Types.HasCallStack =>
+                         a
+          (imported from ‘Prelude’ at abstract_refinement_substitutions.hs:1:8-38
+           (and originally defined in ‘GHC.Err’))
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 9db9393654..2d3c3cd118 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -391,6 +391,8 @@ test('hole_constraints_nested', normal, compile, ['-fdefer-type-errors -fno-max-
 test('valid_substitutions', [extra_files(['ValidSubs.hs'])],
     multimod_compile, ['valid_substitutions','-fdefer-type-errors -fno-max-valid-substitutions'])
 test('valid_substitutions_interactions', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
+test('refinement_substitutions', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions -fno-max-refinement-substitutions -frefinement-level-substitutions=2'])
+test('abstract_refinement_substitutions', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions -fno-max-refinement-substitutions -frefinement-level-substitutions=2 -fabstract-refinement-substitutions'])
 test('T7408', normal, compile, [''])
 test('UnboxStrictPrimitiveFields', normal, compile, [''])
 test('T7541', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/refinement_substitutions.hs b/testsuite/tests/typecheck/should_compile/refinement_substitutions.hs
new file mode 100644
index 0000000000..345a6c8f8e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/refinement_substitutions.hs
@@ -0,0 +1,7 @@
+module RefinementSubstitutions where
+
+f :: [Integer] -> Integer
+f = _
+
+g :: [Integer] -> Integer
+g = _ 0
diff --git a/testsuite/tests/typecheck/should_compile/refinement_substitutions.stderr b/testsuite/tests/typecheck/should_compile/refinement_substitutions.stderr
new file mode 100644
index 0000000000..95f5686603
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/refinement_substitutions.stderr
@@ -0,0 +1,188 @@
+
+refinement_substitutions.hs:4:5: warning: [-Wtyped-holes (in -Wdefault)]
+    • Found hole: _ :: [Integer] -> Integer
+    • In the expression: _
+      In an equation for ‘f’: f = _
+    • Relevant bindings include
+        f :: [Integer] -> Integer
+          (bound at refinement_substitutions.hs:4:1)
+      Valid substitutions include
+        f :: [Integer] -> Integer
+          (defined at refinement_substitutions.hs:4:1)
+        g :: [Integer] -> Integer
+          (defined at refinement_substitutions.hs:7:1)
+        product :: forall (t :: * -> *).
+                   Foldable t =>
+                   forall a. Num a => t a -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Foldable’))
+        sum :: forall (t :: * -> *).
+               Foldable t =>
+               forall a. Num a => t a -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Foldable’))
+        maximum :: forall (t :: * -> *).
+                   Foldable t =>
+                   forall a. Ord a => t a -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Foldable’))
+        minimum :: forall (t :: * -> *).
+                   Foldable t =>
+                   forall a. Ord a => t a -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Foldable’))
+        head :: forall a. [a] -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.List’))
+        last :: forall a. [a] -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.List’))
+        undefined :: forall (a :: TYPE r).
+                     GHC.Stack.Types.HasCallStack =>
+                     a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Err’))
+      Valid refinement substitutions include
+        foldr _ _ :: forall (t :: * -> *).
+                     Foldable t =>
+                     forall a b. (a -> b -> b) -> b -> t a -> b
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Foldable’))
+        foldl1 _ :: forall (t :: * -> *).
+                    Foldable t =>
+                    forall a. (a -> a -> a) -> t a -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Foldable’))
+        foldr1 _ :: forall (t :: * -> *).
+                    Foldable t =>
+                    forall a. (a -> a -> a) -> t a -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Foldable’))
+        foldl _ _ :: forall (t :: * -> *).
+                     Foldable t =>
+                     forall b a. (b -> a -> b) -> b -> t a -> b
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Foldable’))
+        head _ :: forall a. [a] -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.List’))
+        last _ :: forall a. [a] -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.List’))
+        (!!) _ _ :: forall a. [a] -> Int -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.List’))
+        error _ :: forall (a :: TYPE r).
+                   GHC.Stack.Types.HasCallStack =>
+                   [Char] -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Err’))
+        errorWithoutStackTrace _ :: forall (a :: TYPE r). [Char] -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Err’))
+        asTypeOf _ _ :: forall a. a -> a -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        const _ :: forall a b. a -> b -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        (.) _ _ :: forall b c a. (b -> c) -> (a -> b) -> a -> c
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        uncurry _ _ :: forall a b c. (a -> b -> c) -> (a, b) -> c
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Tuple’))
+        ($) _ :: forall a (b :: TYPE r). (a -> b) -> a -> b
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        ($!) _ :: forall a (b :: TYPE r). (a -> b) -> a -> b
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        id _ :: forall a. a -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        snd _ :: forall a b. (a, b) -> b
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Tuple’))
+        fst _ :: forall a b. (a, b) -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Tuple’))
+
+refinement_substitutions.hs:7:5: warning: [-Wtyped-holes (in -Wdefault)]
+    • Found hole: _ :: Integer -> [Integer] -> Integer
+    • In the expression: _
+      In the expression: _ 0
+      In an equation for ‘g’: g = _ 0
+    • Relevant bindings include
+        g :: [Integer] -> Integer
+          (bound at refinement_substitutions.hs:7:1)
+      Valid substitutions include
+        const :: forall a b. a -> b -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        undefined :: forall (a :: TYPE r).
+                     GHC.Stack.Types.HasCallStack =>
+                     a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Err’))
+      Valid refinement substitutions include
+        foldr _ :: forall (t :: * -> *).
+                   Foldable t =>
+                   forall a b. (a -> b -> b) -> b -> t a -> b
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Foldable’))
+        foldl _ :: forall (t :: * -> *).
+                   Foldable t =>
+                   forall b a. (b -> a -> b) -> b -> t a -> b
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Foldable’))
+        head _ :: forall a. [a] -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.List’))
+        last _ :: forall a. [a] -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.List’))
+        (!!) _ _ :: forall a. [a] -> Int -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.List’))
+        error _ :: forall (a :: TYPE r).
+                   GHC.Stack.Types.HasCallStack =>
+                   [Char] -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Err’))
+        errorWithoutStackTrace _ :: forall (a :: TYPE r). [Char] -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Err’))
+        flip _ :: forall a b c. (a -> b -> c) -> b -> a -> c
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        asTypeOf _ _ :: forall a. a -> a -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        const _ :: forall a b. a -> b -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        (.) _ _ :: forall b c a. (b -> c) -> (a -> b) -> a -> c
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        uncurry _ _ :: forall a b c. (a -> b -> c) -> (a, b) -> c
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Tuple’))
+        curry _ :: forall a b c. ((a, b) -> c) -> a -> b -> c
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Tuple’))
+        ($) _ :: forall a (b :: TYPE r). (a -> b) -> a -> b
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        ($!) _ :: forall a (b :: TYPE r). (a -> b) -> a -> b
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        id _ :: forall a. a -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘GHC.Base’))
+        snd _ :: forall a b. (a, b) -> b
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Tuple’))
+        fst _ :: forall a b. (a, b) -> a
+          (imported from ‘Prelude’ at refinement_substitutions.hs:1:8-30
+           (and originally defined in ‘Data.Tuple’))