GitLab

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

db1ce858

by sheaf at 2025-12-22T17:11:17-05:00

Do deep subsumption when computing valid hole fits

This commit makes a couple of improvements to the code that
computes "valid hole fits":

  1. It uses deep subsumption for data constructors.
     This matches up the multiplicities, as per
     Note [Typechecking data constructors].
     This fixes #26338 (test: LinearHoleFits).

  2. It now suggests (non-unidirectional) pattern synonyms as valid
     hole fits. This fixes #26339 (test: PatSynHoleFit).

  3. It uses 'stableNameCmp', to make the hole fit output deterministic.

-------------------------
Metric Increase:
    hard_hole_fits
-------------------------

72ee9100

by sheaf at 2025-12-22T17:11:17-05:00

Speed up hole fits with a quick pre-test

This speeds up the machinery for valid hole fits by doing a small
check to rule out obviously wrong hole fits, such as:

  1. A hole fit identifier whose type has a different TyCon at the head,
     after looking through foralls and (=>) arrows, e.g.:
        hole_ty = Int
        cand_ty = Maybe a
     or
        hole_ty = forall a b. a -> b
        cand_ty = forall x y. Either x y
  2. A hole fit identifier that is not polymorphic when the hole type
     is polymorphic, e.g.
       hole_ty = forall a. a -> a
       cand_ty = Int -> Int

-------------------------
Metric Decrease:
    hard_hole_fits
-------------------------

29 changed files:

compiler/GHC/Core/DataCon.hs
compiler/GHC/Tc/Errors/Hole.hs
compiler/GHC/Tc/Errors/Hole/FitTypes.hs
compiler/GHC/Tc/Errors/Ppr.hs
compiler/GHC/Tc/Gen/App.hs
compiler/GHC/Tc/Utils/Unify.hs
docs/users_guide/9.16.1-notes.rst
testsuite/tests/ghci/scripts/T8353.stderr
testsuite/tests/overloadedrecflds/should_fail/DRFHoleFits.stderr
testsuite/tests/perf/compiler/hard_hole_fits.stderr
testsuite/tests/plugins/test-hole-plugin.stderr
testsuite/tests/th/T15321.stderr
testsuite/tests/typecheck/should_compile/T13050.stderr
testsuite/tests/typecheck/should_compile/T14273.stderr
testsuite/tests/typecheck/should_compile/T14590.stderr
testsuite/tests/typecheck/should_compile/T25180.stderr
testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr
testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr
testsuite/tests/typecheck/should_compile/free_monad_hole_fits.stderr
testsuite/tests/typecheck/should_compile/hole_constraints.stderr
testsuite/tests/typecheck/should_compile/holes.stderr
testsuite/tests/typecheck/should_compile/holes2.stderr
testsuite/tests/typecheck/should_compile/holes3.stderr
testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr
testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr
testsuite/tests/typecheck/should_compile/type_in_type_hole_fits.stderr
testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr
testsuite/tests/typecheck/should_compile/valid_hole_fits_interactions.stderr
testsuite/tests/typecheck/should_fail/T14884.stderr

Changes:

compiler/GHC/Core/DataCon.hs

@@ -30,7 +30,7 @@ module GHC.Core.DataCon (
          dataConRepType, dataConInstSig, dataConFullSig,
          dataConName, dataConIdentity, dataConTag, dataConTagZ,
          dataConTyCon, dataConOrigTyCon,
 -        dataConWrapperType, dataConNonlinearType,
 +        dataConWrapperType,
          dataConUnivTyVars, dataConExTyCoVars, dataConUnivAndExTyCoVars,
          dataConConcreteTyVars,
          dataConUserTyVars, dataConUserTyVarBinders,
@@ -1568,23 +1568,6 @@ dataConWrapperType (MkData { dcUserTyVarBinders = user_tvbs,
      mkScaledFunTys arg_tys $
      res_ty
 -dataConNonlinearType :: DataCon -> Type
 --- ^ Just like 'dataConWrapperType', but with the
 --- linearity on the arguments all zapped to Many.
 ---
 --- Only used temporarily as a stop-gap for hole fit suggestions
 --- until #26338 is fixed.
 -dataConNonlinearType (MkData { dcUserTyVarBinders = user_tvbs,
 -                               dcOtherTheta = theta, dcOrigArgTys = arg_tys,
 -                               dcOrigResTy = res_ty,
 -                               dcStupidTheta = stupid_theta })
 -  = mkForAllTys user_tvbs $
 -    mkInvisFunTys (stupid_theta ++ theta) $
 -    mkScaledFunTys arg_tys' $
 -    res_ty
 -  where
 -    arg_tys' = map (\(Scaled w t) -> Scaled (case w of OneTy -> ManyTy; _ -> w) t) arg_tys
+-
  -- | Finds the instantiated types of the arguments required to construct a
  -- 'DataCon' representation
  -- NB: these INCLUDE any dictionary args

compiler/GHC/Tc/Errors/Hole.hs

@@ -36,13 +36,16 @@ import GHC.Tc.Utils.Monad
  import GHC.Tc.Types.Constraint
  import GHC.Tc.Types.Origin
  import GHC.Tc.Utils.TcMType
 +import GHC.Tc.TyCl.PatSyn (patSynBuilderOcc)
  import GHC.Tc.Types.Evidence
  import GHC.Tc.Types.CtLoc
  import GHC.Tc.Utils.TcType
  import GHC.Tc.Zonk.TcType
  import GHC.Core.TyCon( TyCon, isGenerativeTyCon )
  import GHC.Core.TyCo.Rep( Type(..) )
 +import GHC.Core.Type (funTyFlagTyCon)
  import GHC.Core.DataCon
 +import GHC.Core.PatSyn (patSynName)
  import GHC.Core.Predicate( Pred(..), classifyPredType, eqRelRole )
  import GHC.Types.Basic
  import GHC.Types.Name
@@ -50,6 +53,8 @@ import GHC.Types.Name.Reader
  import GHC.Builtin.Names ( gHC_INTERNAL_ERR, gHC_INTERNAL_UNSAFE_COERCE )
  import GHC.Builtin.Types ( tupleDataConName, unboxedSumDataConName )
  import GHC.Types.Id
 +import GHC.Types.Name.Set (extendNameSet, NameSet, emptyNameSet)
 +import GHC.Types.Var (isVisibleFunArg)
  import GHC.Types.Var.Set
  import GHC.Types.Var.Env
  import GHC.Types.TyThing
@@ -71,7 +76,10 @@ import Data.Graph       ( graphFromEdges, topSort )
  import GHC.Tc.Solver    ( simplifyTopWanteds )
  import GHC.Tc.Solver.Monad ( runTcSEarlyAbort )
 -import GHC.Tc.Utils.Unify ( tcSubTypeSigma )
 +import GHC.Tc.Utils.Unify
 +  ( DeepSubsumptionFlag(..), DeepSubsumptionDepth(..)
 +  , tcSubTypeHoleFit
 +  )
  import GHC.HsToCore.Docs ( extractDocs )
  import GHC.Hs.Doc
@@ -91,7 +99,6 @@ import GHC.Data.EnumSet (EnumSet)
  import qualified GHC.Data.EnumSet as EnumSet
  import qualified GHC.LanguageExtensions as LangExt
+-
  {-
  Note [Valid hole fits include ...]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -245,6 +252,23 @@ In addition, we call withoutUnification to reset any unified metavariables; this
  call is actually done outside tcCheckHoleFit so that the results can be formatted
  for the user before resetting variables.
 +Note [Deep subsumption in tcCheckHoleFit]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +To check that a candidate fits in a hole, we perform a subsumption check, as
 +detailed in Note [Checking hole fits]. However, should we also perform deep
 +subsumption? Well, certainly if the user has enabled deep subsumption, and also
 +in cases where deep subsumption is required such as to perform eta-expansion
 +of data constructors, e.g.
++
 +  data T = MkT Int Bool -- so that MkT :: Int %1 -> Bool %1 -> T
++
 +  foo :: Int %1 -> Bool -> T
 +  foo = _
++
 +We should suggest MkT as a valid hole fit, because deep subsumption will
 +eta expand to make the multiplicities line up, as per
 +Note [Typechecking data constructors] in GHC.Tc.Gen.Head.
++
  Note [Valid refinement hole fits include ...]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  When the `-frefinement-level-hole-fits=N` flag is given, we additionally look
@@ -405,24 +429,61 @@ is discarded.
  Note [Speeding up valid hole-fits]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -To fix #16875 we noted that a lot of time was being spent on unnecessary work.
+-
 -When we'd call `tcCheckHoleFit hole hole_ty ty`, we would end up by generating
 -a constraint to show that `hole_ty ~ ty`, including any constraints in `ty`. For
 -example, if `hole_ty = Int` and `ty = Foldable t => (a -> Bool) -> t a -> Bool`,
 -we'd have `(a_a1pa[sk:1] -> Bool) -> t_t2jk[sk:1] a_a1pa[sk:1] -> Bool ~# Int`
 -from the coercion, as well as `Foldable t_t2jk[sk:1]`. By adding a flag to
 -`TcSEnv` and adding a `runTcSEarlyAbort`, we can fail as soon as we hit
 -an insoluble constraint. Since we don't need the result in the case that it
 -fails, a boolean `False` (i.e. "it didn't work" from `runTcSEarlyAbort`)
 -is sufficient.
+-
 -We also check whether the type of the hole is an immutable type variable (i.e.
 -a skolem). In that case, the only possible fits are fits of exactly that type,
 -which can only come from the locals. This speeds things up quite a bit when we
 -don't know anything about the type of the hole. This also helps with degenerate
 -fits like (`id (_ :: a)` and `head (_ :: [a])`) when looking for fits of type
 -`a`, where `a` is a skolem.
 +When computing valid hole fits, we want to quickly rule out identifiers that
 +clearly don't fit the type of the hole, without doing too much work.
 +This is important for the performance of the "valid hole fits" feature,
 +which is known to be slow in some cases (#16875).
++
 +The valid hole fits machinery is given the type of the hole and a possible
 +candidate identifier, and it computes whether the identifier can be used by
 +performing a subtype check
++
 +  tcSubTypeHoleFit .. cand_ty hole_ty
++
 +which checks that the type of the candidate identifier is more general than
 +the type of the hole.
++
 +We currently use the following shortcuts.
++
 +  1. When computing a set of candidate identifiers for a hole:
++
 +    (FastHoles1)
 +      If 'hole_ty' is an immutable type variable (i.e. a skolem type variable),
 +      then the only possible (useful) fits are fits of exactly that type, which
 +      can only come from locally bound variables for which that skolem is in scope.
 +      In that case, only include local identifiers in the list of candidate Ids.
++
 +      This speeds things up quite a bit when we don't know anything about the type
 +      of the hole, and helps with degenerate fits like (`id (_ :: a)` and `head (_ :: [a])`)
 +      when looking for fits of type `a`, where `a` is a skolem.
++
 +  2. When checking whether a particular candidate 'cand_ty :: cand_ty' fits 'hole_ty':
++
 +    (FastHoles2)
 +      Abort early if 'cand_ty' is obviously not a subtype of 'hole_ty',
 +      according to a cheap test. The current cheap test is in 'definitelyNotSubType',
 +      which detects the following cases:
++
 +        1. 'cand_ty' and 'hole_ty' have a different TyCon at the head, after
 +           looking through foralls and (=>) arrows, e.g.:
 +              hole_ty = Int     -- headed by Int
 +              cand_ty = Maybe a -- headed by Maybe
 +           or
 +              hole_ty = forall a b. a -> b               -- headed by (->)
 +              cand_ty = forall x y. Num x => Either x y  -- headed by Either
 +        2. 'hole_ty' is polymorphic but 'cand_ty' has no polymorphism, e.g.
 +              hole_ty = forall a. a -> a
 +              cand_ty = Int -> Int
++
 +    (FastHoles3)
 +      After calling 'tcSubTypeHoleFit' but before running the solver on the
 +      constraints that it generated, do a quick check to see if any constraint
 +      is obviously insoluble. See Note [tcCheckHoleFit: fast insolubility check].
++
 +    (FastHoles4)
 +      When running the solver on the constraints generated by 'tcSubTypeHoleFit',
 +      do it in a special mode that stops immediately as soon as it spots an
 +      insoluble constraint, using 'runTcSEarlyAbort'.
  -}
  -- We read the various -no-show-*-of-hole-fits flags
@@ -517,8 +578,6 @@ getLocalBindings tidy_orig ct_loc
          discard_it = go env sofar tc_bndrs
          keep_it id = go env (id:sofar) tc_bndrs
+-
+-
  -- See Note [Valid hole fits include ...]
  findValidHoleFits :: TidyEnv        -- ^ The tidy_env for zonking
                    -> [Implication]  -- ^ Enclosing implications for givens
@@ -558,8 +617,10 @@ findValidHoleFits tidy_env implics simples h@(Hole { hole_sort = ExprHole _
                        map IdHFCand lclBinds ++ map GreHFCand lcl
             globals = map GreHFCand gbl
             syntax = map NameHFCand (builtIns exts)
 -           -- If the hole is a rigid type-variable, then we only check the
++
 +           -- If the hole is a rigid type variable, then we only check the
             -- locals, since only they can match the type (in a meaningful way).
 +           -- See (FastHoles1) in Note [Speeding up valid hole-fits].
             only_locals = any isImmutableTyVar $ getTyVar_maybe hole_ty
             to_check = if only_locals then locals
                        else locals ++ syntax ++ globals
@@ -679,7 +740,6 @@ findValidHoleFits tidy_env implics simples h@(Hole { hole_sort = ExprHole _
      possiblyDiscard (Just max) fits = (fits `lengthExceeds` max, take max fits)
      possiblyDiscard Nothing fits = (False, fits)
+-
  -- We don't (as of yet) handle holes in types, only in expressions.
  findValidHoleFits env _ _ _ = return (env, noValidHoleFits)
@@ -732,13 +792,14 @@ sortHoleFitsBySize = return . sortOn sizeOfFit
  -- '-fno-sort-valid-hole-fits'.
  sortHoleFitsByGraph :: [TcHoleFit] -> TcM [TcHoleFit]
  sortHoleFitsByGraph fits = go [] fits
 -  where tcSubsumesWCloning :: TcType -> TcType -> TcM Bool
 -        tcSubsumesWCloning ht ty = withoutUnification fvs (tcSubsumes ht ty)
 -          where fvs = tyCoFVsOfTypes [ht,ty]
 +  where tcSubsumesWCloning :: TcSigmaType -> TcSigmaType -> TcM Bool
 +        tcSubsumesWCloning fit_ty cand_ty =
 +          withoutUnification (tyCoFVsOfTypes [fit_ty, cand_ty]) $
 +            tcSubsumes fit_ty cand_ty
          go :: [(TcHoleFit, [TcHoleFit])] -> [TcHoleFit] -> TcM [TcHoleFit]
          go sofar [] = do { traceTc "subsumptionGraph was" $ ppr sofar
                           ; return $ uncurry (++) $ partition hfIsLcl topSorted }
 -          where toV (hf, adjs) = (hf, hfId hf, map hfId adjs)
 +          where toV (hf, adjs) = (hf, hfName hf, map hfName adjs)
                  (graph, fromV, _) = graphFromEdges $ map toV sofar
                  topSorted = map ((\(h,_,_) -> h) . fromV) $ topSort graph
          go sofar (hf:hfs) =
@@ -763,7 +824,7 @@ tcFilterHoleFits :: Maybe Int
  tcFilterHoleFits (Just 0) _ _ _ = return (False, []) -- Stop right away on 0
  tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
    do { traceTc "checkingFitsFor {" $ ppr hole_ty
 -     ; (discards, subs) <- go [] emptyVarSet limit ht candidates
 +     ; (discards, subs) <- go [] emptyNameSet limit ht candidates
       ; traceTc "checkingFitsFor }" empty
       ; return (discards, subs) }
    where
@@ -772,8 +833,8 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
      -- Kickoff the checking of the elements.
      -- We iterate over the elements, checking each one in turn for whether
      -- it fits, and adding it to the results if it does.
 -    go :: [TcHoleFit]           -- What we've found so far.
 -       -> VarSet              -- Ids we've already checked
 +    go :: [TcHoleFit]         -- What we've found so far.
 +       -> NameSet             -- Names of identifiers we have already checked
         -> Maybe Int           -- How many we're allowed to find, if limited
         -> (TcType, [TcTyVar]) -- The type, and its refinement variables.
         -> [HoleFitCandidate]  -- The elements we've yet to check.
@@ -786,40 +847,59 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
          do { traceTc "lookingUp" $ ppr el
             ; maybeThing <- lookup el
             ; case maybeThing of
 -               Just (id, id_ty) | not_trivial id ->
 -                       do { fits <- fitsHole ty id_ty
 +               Just cand@(_, is_dc, cand_ty) ->
 +                       do { fits <- fitsHole ty cand_ty is_dc
                            ; case fits of
 -                              Just (wrp, matches) -> keep_it id id_ty wrp matches
 +                              Just (wrp, matches) -> keep_it cand wrp matches
                                _ -> discard_it }
                 _ -> discard_it }
          where
 -          -- We want to filter out undefined and the likes from GHC.Err (#17940)
 -          not_trivial id = nameModule_maybe (idName id) `notElem` [Just gHC_INTERNAL_ERR, Just gHC_INTERNAL_UNSAFE_COERCE]
+-
 -          lookup :: HoleFitCandidate -> TcM (Maybe (Id, Type))
 -          lookup (IdHFCand id) = return (Just (id, idType id))
 -          lookup hfc = do { thing <- tcLookup name
 -                          ; return $ case thing of
 -                                       ATcId {tct_id = id} -> Just (id, idType id)
 -                                       AGlobal (AnId id)   -> Just (id, idType id)
 -                                       AGlobal (AConLike (RealDataCon con)) ->
 -                                           Just (dataConWrapId con, dataConNonlinearType con)
 -                                       _ -> Nothing }
 -            where name = case hfc of
 -                           GreHFCand gre   -> greName gre
 -                           NameHFCand name -> name
 +          mk_id i
 +            -- Filter out undefined and the likes from GHC.Err (#17940).
 +            --
 +            -- TODO: we might want to filter out more, e.g. if the user defines
 +            --
 +            --   todo :: forall a. a
 +            --   todo = undefined
 +            --
 +            -- we probably don't want to suggest 'todo' as a hole fit either.
 +            | let nm = idName i
 +            , nameModule_maybe nm `notElem` [Just gHC_INTERNAL_ERR, Just gHC_INTERNAL_UNSAFE_COERCE]
 +            = Just (nm, False, idType i)
 +            | otherwise
 +            = Nothing
++
 +          lookup :: HoleFitCandidate -> TcM (Maybe (Name, Bool, Type))
 +          lookup (IdHFCand id) = return $ mk_id id
 +          lookup hfc =
 +            do { thing <- tcLookup name
 +               ; return $
 +                   case thing of
 +                     ATcId {tct_id = id} -> mk_id id
 +                     AGlobal (AnId id)   -> mk_id id
 +                     AGlobal (AConLike (RealDataCon con)) ->
 +                         Just (dataConName con, True, dataConWrapperType con)
 +                     AGlobal (AConLike (PatSynCon ps))
 +                       | Just (_,t) <- patSynBuilderOcc ps
 +                       -> -- If we ever get a 'Todo' pattern synonym,
 +                          -- we should filter it out here.
 +                         Just (patSynName ps, False, t)
 +                     _ -> Nothing }
++
 +            where
 +              name = case hfc of
 +                        GreHFCand gre   -> greName gre
 +                        NameHFCand name -> name
++
            discard_it = go subs seen maxleft ty elts
 -          keep_it eid eid_ty wrp ms = go (fit:subs) (extendVarSet seen eid)
 +          keep_it (enm, _, ety) wrp ms = go (fit:subs) (extendNameSet seen enm)
                                   ((\n -> n - 1) <$> maxleft) ty elts
              where
 -              fit = HoleFit { hfId = eid, hfCand = el, hfType = eid_ty
 +              fit = HoleFit { hfName = enm, hfCand = el, hfType = ety
                              , hfRefLvl = length (snd ty)
                              , hfWrap = wrp, hfMatches = ms
                              , hfDoc = Nothing }
+-
+-
+-
      unfoldWrapper :: HsWrapper -> [Type]
      unfoldWrapper = reverse . unfWrp'
        where
@@ -828,7 +908,6 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
          unfWrp' (WpCompose w1 w2) = unfWrp' w1 ++ unfWrp' w2
          unfWrp' _                  = []
+-
      -- The real work happens here, where we invoke the type checker using
      -- tcCheckHoleFit to see whether the given type fits the hole.
      fitsHole :: (TcType, [TcTyVar]) -- The type of the hole wrapped with the
@@ -845,27 +924,36 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
                                      -- In the base case with no additional
                                      -- holes, h_ty will just be t and ref_vars
                                      -- will be [].
 -             -> TcType -- The type we're checking to whether it can be
 -                       -- instantiated to the type h_ty.
 +             -> TcType -- The type of the hole fit candidate
 +             -> Bool   -- Is the hole fit candidate a data constructor?
               -> TcM (Maybe ([TcType], [TcType])) -- If it is not a match, we
                                                   -- return Nothing. Otherwise,
                                                   -- we Just return the list of
                                                   -- types that quantified type
 -                                                 -- variables in ty would take
 +                                                 -- variables in cand_ty would take
                                                   -- if used in place of h_ty,
                                                   -- and the list types of any
                                                   -- additional holes simulated
                                                   -- with the refinement
                                                   -- variables in ref_vars.
 -    fitsHole (h_ty, ref_vars) ty =
 +    fitsHole (h_ty, ref_vars) cand_ty cand_is_datacon =
      -- We wrap this with the withoutUnification to avoid having side-effects
      -- beyond the check, but we rely on the side-effects when looking for
      -- refinement hole fits, so we can't wrap the side-effects deeper than this.
        withoutUnification fvs $
 -      do { traceTc "checkingFitOf {" $ ppr ty
 -         ; (fits, wrp) <- tcCheckHoleFit hole h_ty ty
 -         ; traceTc "Did it fit?" $ ppr fits
 -         ; traceTc "wrap is: " $ ppr wrp
 +      do { traceTc "checkingFitOf {" $ ppr cand_ty
++
 +           -- Compute 'ds_flag' with the same logic as 'getDeepSubsumptionFlag_DataConHead'.
 +         ; user_ds <- xoptM LangExt.DeepSubsumption
 +         ; let ds_flag
 +                 | user_ds
 +                 = Deep DeepSub
 +                 | cand_is_datacon
 +                 = Deep TopSub
 +                 | otherwise
 +                 = Shallow
 +         ; mbWrap <- tcCheckHoleFit ds_flag hole h_ty cand_ty
 +         ; traceTc "Did it fit?" $ ppr mbWrap
           ; traceTc "checkingFitOf }" empty
           -- We'd like to avoid refinement suggestions like `id _ _` or
           -- `head _ _`, and only suggest refinements where our all phantom
@@ -875,7 +963,8 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
           -- variables, i.e. zonk them to read their final value to check for
           -- abstract refinements, and to report what the type of the simulated
           -- holes must be for this to be a match.
 -         ; if fits then do {
 +         ; case mbWrap of
 +            { Just wrp -> do {
                -- Zonking is expensive, so we only do it if required.
                z_wrp_tys <- liftZonkM $ zonkTcTypes (unfoldWrapper wrp)
              ; if null ref_vars
@@ -895,12 +984,10 @@ tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
                        ; if allowAbstract || (allFilled && allConcrete )
                          then return $ Just (z_wrp_tys, z_vars)
                          else return Nothing }}
 -           else return Nothing }
 -     where fvs = mkFVs ref_vars `unionFV` hole_fvs `unionFV` tyCoFVsOfType ty
 +           ; Nothing -> return Nothing } }
 +     where fvs = mkFVs ref_vars `unionFV` hole_fvs `unionFV` tyCoFVsOfType cand_ty
             hole = typed_hole { th_hole = Nothing }
+-
+-
  -- | Checks whether a MetaTyVar is flexible or not.
  isFlexiTyVar :: TcTyVar -> TcM Bool
  isFlexiTyVar tv | isMetaTyVar tv = isFlexi <$> readMetaTyVar tv
@@ -923,7 +1010,7 @@ withoutUnification free_vars action =
  -- discarding any errors. Subsumption here means that the ty_b can fit into the
  -- ty_a, i.e. `tcSubsumes a b == True` if b is a subtype of a.
  tcSubsumes :: TcSigmaType -> TcSigmaType -> TcM Bool
 -tcSubsumes ty_a ty_b = fst <$> tcCheckHoleFit dummyHole ty_a ty_b
 +tcSubsumes ty_a ty_b = isJust <$> tcCheckHoleFit Shallow dummyHole ty_a ty_b
    where dummyHole = TypedHole { th_relevant_cts = emptyBag
                                , th_implics      = []
                                , th_hole         = Nothing }
@@ -932,16 +1019,22 @@ tcSubsumes ty_a ty_b = fst <$> tcCheckHoleFit dummyHole ty_a ty_b
  -- #14273. This makes sure that when checking whether a type fits the hole,
  -- the type has to be subsumed by type of the hole as well as fulfill all
  -- constraints on the type of the hole.
 -tcCheckHoleFit :: TypedHole   -- ^ The hole to check against
 +tcCheckHoleFit :: DeepSubsumptionFlag
 +               -> TypedHole   -- ^ The hole to check against
                 -> TcSigmaType
                 -- ^ The type of the hole to check against (possibly modified,
                 -- e.g. refined with additional holes for refinement hole-fits.)
 -               -> TcSigmaType -- ^ The type to check whether fits.
 -               -> TcM (Bool, HsWrapper)
 -               -- ^ Whether it was a match, and the wrapper from hole_ty to ty.
 -tcCheckHoleFit _ hole_ty ty | hole_ty `eqType` ty
 -    = return (True, idHsWrapper)
 -tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
 +               -> TcSigmaType
 +                 -- ^ The candidate fit type
 +               -> TcM (Maybe HsWrapper)
 +               -- ^ Whether it was a match, and the wrapper from hole_ty to cand_ty
 +tcCheckHoleFit _ _ hole_ty cand_ty
 +  -- (FastHoles2) from Note [Speeding up valid hole-fits]
 +  | definitelyNotSubType cand_ty hole_ty
 +  = return Nothing
 +  | hole_ty `eqType` cand_ty
 +  = return $ Just idHsWrapper
 +tcCheckHoleFit ds_flag (TypedHole {..}) hole_ty cand_ty = discardErrs $
    do { -- We wrap the subtype constraint in the implications to pass along the
         -- givens, and so we must ensure that any nested implications and skolems
         -- end up with the correct level. The implications are ordered so that
@@ -952,16 +1045,21 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
                            [] -> getTcLevel
                            -- imp is the innermost implication
                            (imp:_) -> return (ic_tclvl imp)
 -     ; (wrap, wanted) <- setTcLevel innermost_lvl $ captureConstraints $
 -                         tcSubTypeSigma orig (ExprSigCtxt NoRRC) ty hole_ty
++
 +     ; (wrap, wanted) <-
 +         setTcLevel innermost_lvl $ captureConstraints $
 +         tcSubTypeHoleFit ds_flag orig cand_ty hole_ty
 +           -- See Note [Deep subsumption in tcCheckHoleFit]
++
       ; traceTc "Checking hole fit {" empty
       ; traceTc "wanteds are: " $ ppr wanted
       ; if | isEmptyWC wanted, isEmptyBag th_relevant_cts
            -> do { traceTc "}" empty
 -                ; return (True, wrap) }
 +                ; return $ Just wrap }
 -          | checkInsoluble wanted -- See Note [Fast path for tcCheckHoleFit]
 -          -> return (False, wrap)
 +          -- (FastHoles3) from Note [Speeding up valid hole-fits]
 +          | checkInsoluble wanted
 +          -> return Nothing
            | otherwise
            -> do { fresh_binds <- newTcEvBinds
@@ -979,10 +1077,16 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
                    -- the wanteds, because they are freshly generated by the
                    -- call to`tcSubtype_NC`.
                  ; traceTc "final_wc is: " $ ppr final_wc
 -                  -- See Note [Speeding up valid hole-fits]
 -                ; (rem, _) <- tryTc $ runTcSEarlyAbort $ simplifyTopWanteds final_wc
++
 +                  -- runTcSEarlyAbort: (FastHoles4) from Note [Speeding up valid hole-fits]
 +                ; (rem, _) <- tryTc $ runTcSEarlyAbort
 +                                    $ simplifyTopWanteds final_wc
                  ; traceTc "}" empty
 -                ; return (any isSolvedWC rem, wrap) } }
 +                ; return $
 +                    if any isSolvedWC rem
 +                    then Just wrap
 +                    else Nothing
 +                } }
    where
      orig = ExprHoleOrigin (hole_occ <$> th_hole)
@@ -993,15 +1097,15 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $
      setWCAndBinds binds imp wc
        = mkImplicWC $ unitBag $ imp { ic_wanted = wc , ic_binds = binds }
 -{- Note [Fast path for tcCheckHoleFit]
 +{- Note [tcCheckHoleFit: fast insolubility check]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -In `tcCheckHoleFit` we compare (with `tcSubTypeSigma`) the type of the hole
 +In `tcCheckHoleFit` we compare (with `tcSubTypeHoleFit`) the type of the hole
  with the type of zillions of in-scope functions, to see which would "fit".
  Most of these checks fail!  They generate obviously-insoluble constraints.
  For these very-common cases we don't want to crank up the full constraint
  solver.  It's much more efficient to do a quick-and-dirty check for insolubility.
 -Now, `tcSubTypeSigma` uses the on-the-fly unifier in GHC.Tc.Utils.Unify,
 +Now, `tcSubTypeHoleFit` uses the on-the-fly unifier in GHC.Tc.Utils.Unify,
  it has already done the dirt-simple unification. So our quick-and-dirty
  check can simply look for constraints like (Int ~ Bool).  We don't need
  to worry about (Maybe Int ~ Maybe Bool).
@@ -1010,9 +1114,8 @@ The quick-and-dirty check is in `checkInsoluble`. It can make a big
  difference: For test hard_hole_fits, compile-time allocation goes down by 37%!
  -}
+-
  checkInsoluble :: WantedConstraints -> Bool
 --- See Note [Fast path for tcCheckHoleFit]
 +-- See Note [tcCheckHoleFit: fast insolubility check]
  checkInsoluble (WC { wc_simple = simples })
    = any is_insol simples
    where
@@ -1021,7 +1124,7 @@ checkInsoluble (WC { wc_simple = simples })
                      _              -> False
  definitelyNotEqual :: Role -> TcType -> TcType -> Bool
 --- See Note [Fast path for tcCheckHoleFit]
 +-- See Note [tcCheckHoleFit: fast insolubility check]
  -- Specifically, does not need to recurse under type constructors
  definitelyNotEqual r t1 t2
    = go t1 t2
@@ -1041,3 +1144,46 @@ definitelyNotEqual r t1 t2
      go_tc _ (FunTy {})    = True
      go_tc _ (ForAllTy {}) = True
      go_tc _ _ = False
++
 +-- | @definitelyNotSubType cand_ty hole_ty@ computes whether @cand_ty@ is
 +-- **definitely not** a subtype of @hole_ty@, in order to quickly rule out
 +-- a possible hole fit candidate without having to do any solving.
 +--
 +-- See (FastHoles2) in Note [Speeding up valid hole-fits].
 +definitelyNotSubType :: TcType -> TcType -> Bool
 +definitelyNotSubType = go
 +  where
 +    go cand_ty hole_ty
 +      -- Expand type synonyms
 +      | Just cand_ty' <- coreView cand_ty
 +      = go cand_ty' hole_ty
 +      | Just hole_ty' <- coreView hole_ty
 +      = go cand_ty hole_ty'
++
 +      -- Different TyCons at the head (looking through foralls and =>).
 +      | Just tc1 <- tc_head cand_ty
 +      , Just tc2 <- tc_head hole_ty
 +      , tc1 /= tc2
 +      = True
++
 +      -- Non-forall type does not fit a forall-typed hole.
 +      | isSigmaTy hole_ty
 +      , isTauTy cand_ty
 +      = True
++
 +      | otherwise
 +      = False
++
 +    -- Is this Type a TyConApp, after looking under foralls and =>?
 +    -- If so, return the TyCon at the head.
 +    tc_head :: Type -> Maybe TyCon
 +    tc_head (FunTy { ft_af = af, ft_res = res })
 +      | not $ isVisibleFunArg af
 +      = tc_head res
 +      | otherwise
 +      = Just $ funTyFlagTyCon af
 +    tc_head (TyConApp tc _)
 +      = Just tc
 +    tc_head (ForAllTy _ body)
 +      = tc_head body
 +    tc_head _ = Nothing

compiler/GHC/Tc/Errors/Hole/FitTypes.hs

@@ -19,6 +19,7 @@ import GHC.Types.Name
  import GHC.Data.Bag
  import Data.Function ( on )
 +import qualified Data.Semigroup as S
  data TypedHole = TypedHole { th_relevant_cts :: Bag CtEvidence
                             -- ^ Any relevant Cts to the hole
@@ -77,15 +78,15 @@ instance Ord HoleFitCandidate where
  -- 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 TcHoleFit =
 -  HoleFit { hfId   :: Id       -- ^ The elements id in the TcM
 -          , hfCand :: HoleFitCandidate  -- ^ The candidate that was checked.
 -          , hfType :: TcType -- ^ The type of the id, possibly zonked.
 -          , hfRefLvl :: Int  -- ^ The number of holes in this fit.
 -          , hfWrap :: [TcType] -- ^ The wrapper for the match.
 +  HoleFit { hfName :: Name              -- ^ The name of the hole fit identifier
 +          , hfCand :: HoleFitCandidate  -- ^ The candidate that was checked
 +          , hfType :: TcType -- ^ The type of the hole fit (possibly zonked)
 +          , hfRefLvl :: Int  -- ^ The number of holes in this fit
 +          , hfWrap :: [TcType] -- ^ The wrapper for the match
            , hfMatches :: [TcType]
            -- ^ What the refinement variables got matched with, if anything
            , hfDoc :: Maybe [HsDocString]
 -          -- ^ Documentation of this HoleFit, if available.
 +          -- ^ Documentation of this HoleFit, if available
+           }
  data HoleFit
@@ -96,30 +97,25 @@ data HoleFit
  -- We define an Eq and Ord instance to be able to build a graph.
  instance Eq TcHoleFit where
 -   (==) = (==) `on` hfId
 +   (==) = (==) `on` hfName
  instance Outputable HoleFit where
    ppr (TcHoleFit hf)  = ppr hf
    ppr (RawHoleFit sd) = sd
  instance Outputable TcHoleFit where
 -  ppr (HoleFit _ cand ty _ _ mtchs _) =
 -    hang (name <+> holes) 2 (text "where" <+> name <+> dcolon <+> (ppr ty))
 -    where name = ppr $ getName cand
 -          holes = sep $ map (parens . (text "_" <+> dcolon <+>) . ppr) mtchs
+-
 --- We compare HoleFits by their 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. When comparing, we want HoleFits with a lower
 --- refinement level to come first.
 +  ppr (HoleFit { hfName = cand, hfType = ty, hfMatches = mtchs }) =
 +    hang (ppr cand <+> holes) 2 (text "where" <+> ppr cand <+> dcolon <+> (ppr ty))
 +    where holes = sep $ map (parens . (text "_" <+> dcolon <+>) . ppr) mtchs
++
 +-- | Compare HoleFits by their 'Name'. Use 'stableNameCmp' to avoid non-determinism.
 +--
 +-- When comparing, we want HoleFits with a lower refinement level to come first.
  instance Ord TcHoleFit where
 ---  compare (RawHoleFit _) (RawHoleFit _) = EQ
 ---  compare (RawHoleFit _) _ = LT
 ---  compare _ (RawHoleFit _) = GT
 -  compare a@(HoleFit {}) b@(HoleFit {}) = cmp a b
 -    where cmp  = if hfRefLvl a == hfRefLvl b
 -                 then compare `on` (getName . hfCand)
 -                 else compare `on` hfRefLvl
 +  compare a@(HoleFit {}) b@(HoleFit {}) =
 +    compare (hfRefLvl a) (hfRefLvl b)
 +      S.<>
 +    stableNameCmp (hfName a) (hfName b)
  hfIsLcl :: TcHoleFit -> Bool
  hfIsLcl hf@(HoleFit {}) = case hfCand hf of

compiler/GHC/Tc/Errors/Ppr.hs

@@ -3595,7 +3595,7 @@ pprHoleFit :: HoleFitDispConfig -> HoleFit -> SDoc
  pprHoleFit _ (RawHoleFit sd) = sd
  pprHoleFit (HFDC sWrp sWrpVars sTy sProv sMs) (TcHoleFit (HoleFit {..})) =
   hang display 2 provenance
 - where tyApp = sep $ zipWithEqual pprArg vars hfWrap
 + where tyApp = sep $ zipWith pprArg vars hfWrap
           where pprArg b arg = case binderFlag b of
                                  Specified -> text "@" <> pprParendType arg
                                    -- Do not print type application for inferred
@@ -3604,20 +3604,9 @@ pprHoleFit (HFDC sWrp sWrpVars sTy sProv sMs) (TcHoleFit (HoleFit {..})) =
                                  Required  -> pprPanic "pprHoleFit: bad Required"
                                                           (ppr b <+> ppr arg)
         tyAppVars = sep $ punctuate comma $
 -           zipWithEqual (\v t -> ppr (binderVar v) <+> text "~" <+> pprParendType t)
 +           zipWith (\v t -> ppr (binderVar v) <+> text "~" <+> pprParendType t)
             vars hfWrap
+-
 -       vars = unwrapTypeVars hfType
 -         where
 -           -- Attempts to get all the quantified type variables in a type,
 -           -- e.g.
 -           -- return :: forall (m :: * -> *) Monad m => (forall a . a -> m a)
 -           -- into [m, a]
 -           unwrapTypeVars :: Type -> [ForAllTyBinder]
 -           unwrapTypeVars t = vars ++ case splitFunTy_maybe unforalled of
 -                               Just (_, _, _, unfunned) -> unwrapTypeVars unfunned
 -                               _ -> []
 -             where (vars, unforalled) = splitForAllForAllTyBinders t
 +       vars = deepInvisTvBinders hfType
         holeVs = sep $ map (parens . (text "_" <+> dcolon <+>) . ppr) hfMatches
         holeDisp = if sMs then holeVs
                    else sep $ replicate (length hfMatches) $ text "_"
@@ -3644,6 +3633,18 @@ pprHoleFit (HFDC sWrp sWrpVars sTy sProv sMs) (TcHoleFit (HoleFit {..})) =
                   NameHFCand name -> text "bound at" <+> ppr (getSrcLoc name)
                   IdHFCand id_ -> text "bound at" <+> ppr (getSrcLoc id_)
 +-- | Similar to 'tcDeepSplitSigmaTy_maybe', but just cares about the binders.
 +deepInvisTvBinders :: TcSigmaType -> [ForAllTyBinder]
 +deepInvisTvBinders = go
 +  where
 +    go ty | Just (_arg_ty, res_ty) <- tcSplitFunTy_maybe ty
 +          = go res_ty
 +          | (tvs, body) <- splitForAllForAllTyBinders ty
 +          , not (null tvs)
 +          = tvs ++ go body
 +          | otherwise
 +          = []
++
  -- | Add a "Constraints include..." message.
  --
  -- See Note [Constraints include ...]

compiler/GHC/Tc/Gen/App.hs

@@ -420,20 +420,6 @@ quickLookResultType :: TcRhoType -> ExpRhoType -> TcM ()
  quickLookResultType app_res_rho (Check exp_rho) = qlUnify app_res_rho exp_rho
  quickLookResultType _           _               = return ()
 --- | Variant of 'getDeepSubsumptionFlag' which enables a top-level subsumption
 --- in order to implement the plan of Note [Typechecking data constructors].
 -getDeepSubsumptionFlag_DataConHead :: HsExpr GhcTc -> TcM DeepSubsumptionFlag
 -getDeepSubsumptionFlag_DataConHead app_head =
 -  do { user_ds <- xoptM LangExt.DeepSubsumption
 -     ; return $
 -         if | user_ds
 -            -> Deep DeepSub
 -            | XExpr (ConLikeTc (RealDataCon {})) <- app_head
 -            -> Deep TopSub
 -            | otherwise
 -            -> Shallow
 -    }
+-
  finishApp :: (HsExpr GhcTc, AppCtxt) -> [HsExprArg 'TcpTc]
            -> TcRhoType -> HsWrapper
            -> TcM (HsExpr GhcTc)

compiler/GHC/Tc/Utils/Unify.hs

@@ -11,7 +11,7 @@
  module GHC.Tc.Utils.Unify (
    -- Full-blown subsumption
    tcWrapResult, tcWrapResultO, tcWrapResultMono,
 -  tcSubType, tcSubTypeSigma, tcSubTypePat, tcSubTypeDS,
 +  tcSubType, tcSubTypeSigma, tcSubTypePat, tcSubTypeDS, tcSubTypeHoleFit,
    addSubTypeCtxt,
    tcSubTypeAmbiguity, tcSubMult,
    checkConstraints, checkTvConstraints,
@@ -19,7 +19,7 @@ module GHC.Tc.Utils.Unify (
    -- Skolemisation
    DeepSubsumptionFlag(..), DeepSubsumptionDepth(..),
 -  getDeepSubsumptionFlag,
 +  getDeepSubsumptionFlag, getDeepSubsumptionFlag_DataConHead,
    isRhoTyDS,
    tcSkolemise, tcSkolemiseCompleteSig, tcSkolemiseExpectedType,
@@ -77,6 +77,7 @@ import GHC.Tc.Utils.TcMType qualified as TcM
  import GHC.Tc.Solver.InertSet
 +import GHC.Core.ConLike (ConLike(..))
  import GHC.Core.Type
  import GHC.Core.TyCo.Rep hiding (Refl)
  import GHC.Core.TyCo.FVs( isInjectiveInType )
@@ -1485,6 +1486,16 @@ tcSubTypeSigma :: CtOrigin       -- where did the actual type arise / why are we
  tcSubTypeSigma orig ctxt ty_actual ty_expected
    = tc_sub_type (unifyType Nothing) orig ctxt ty_actual ty_expected
 +tcSubTypeHoleFit :: DeepSubsumptionFlag
 +                 -> CtOrigin
 +                 -> TcSigmaType  -- ^ Candidate expression type
 +                 -> TcSigmaType  -- ^ Expected type (= hole type)
 +                 -> TcM HsWrapper
 +tcSubTypeHoleFit ds_flag orig cand_ty hole_ty =
 +   -- See Note [Deep subsumption in tcCheckHoleFit]
 +  tc_sub_type_ds (Nothing, Top) ds_flag (unifyType Nothing)
 +    orig (ExprSigCtxt NoRRC) cand_ty hole_ty
++
  ---------------
  tcSubTypeAmbiguity :: UserTypeCtxt   -- Where did this type arise
                     -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
@@ -2015,6 +2026,20 @@ getDeepSubsumptionFlag =
         else return Shallow
+      }
 +-- | Variant of 'getDeepSubsumptionFlag' which enables a top-level subsumption
 +-- in order to implement the plan of Note [Typechecking data constructors].
 +getDeepSubsumptionFlag_DataConHead :: HsExpr GhcTc -> TcM DeepSubsumptionFlag
 +getDeepSubsumptionFlag_DataConHead app_head =
 +  do { user_ds <- xoptM LangExt.DeepSubsumption
 +     ; return $
 +         if | user_ds
 +            -> Deep DeepSub
 +            | XExpr (ConLikeTc (RealDataCon {})) <- app_head
 +            -> Deep TopSub
 +            | otherwise
 +            -> Shallow
 +    }
++
  -- | 'tc_sub_type_deep' is where the actual work happens for deep subsumption.
  --
  -- Given @ty_actual@ (a sigma-type) and @ty_expected@ (deeply skolemised, i.e.

docs/users_guide/9.16.1-notes.rst

@@ -42,6 +42,9 @@ Compiler
    bound to variables. The very similar pattern ``Foo{bar = Bar{baz = 42}}``
    will will not yet mark ``bar`` or ``baz`` as covered.
 +- Pattern synonyms can now be suggested as valid hole fits (except, of course,
 +  if they are unidirectional).
++
  - When multiple ``-msse*`` flags are given, the maximum version takes effect.
    For example, ``-msse4.2 -msse2`` is now equivalent to ``-msse4.2``.
    Previously, only the last flag took effect.
@@ -52,6 +55,7 @@ Compiler
    in addition to :ghc-flag:`-mavx2`.
    Refer to the users' guide for more details about each individual flag.
++
  GHCi
  ~~~~

testsuite/tests/ghci/scripts/T8353.stderr

+-
  Defer03.hs:4:5: warning: [GHC-83865] [-Wdeferred-type-errors (in -Wdefault)]
      • Couldn't match expected type ‘Int’ with actual type ‘Char’
      • In the expression: 'p'
@@ -9,8 +8,8 @@ Defer03.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • In an equation for ‘f’: f = _
      • Relevant bindings include f :: Int (bound at Defer03.hs:7:1)
        Valid hole fits include
 -        f :: Int (bound at Defer03.hs:7:1)
          a :: Int (defined at Defer03.hs:4:1)
 +        f :: Int (bound at Defer03.hs:7:1)
          maxBound :: forall a. Bounded a => a
            with maxBound @Int
            (imported from ‘Prelude’
@@ -30,8 +29,8 @@ Defer03.hs:7:5: error: [GHC-88464]
      • In an equation for ‘f’: f = _
      • Relevant bindings include f :: Int (bound at Defer03.hs:7:1)
        Valid hole fits include
 -        f :: Int (bound at Defer03.hs:7:1)
          a :: Int (defined at Defer03.hs:4:1)
 +        f :: Int (bound at Defer03.hs:7:1)
          maxBound :: forall a. Bounded a => a
            with maxBound @Int
            (imported from ‘Prelude’
@@ -51,8 +50,8 @@ Defer03.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • In an equation for ‘f’: f = _
      • Relevant bindings include f :: Int (bound at Defer03.hs:7:1)
        Valid hole fits include
 -        f :: Int (bound at Defer03.hs:7:1)
          a :: Int (defined at Defer03.hs:4:1)
 +        f :: Int (bound at Defer03.hs:7:1)
          maxBound :: forall a. Bounded a => a
            with maxBound @Int
            (imported from ‘Prelude’
@@ -72,8 +71,8 @@ Defer03.hs:7:5: error: [GHC-88464]
      • In an equation for ‘f’: f = _
      • Relevant bindings include f :: Int (bound at Defer03.hs:7:1)
        Valid hole fits include
 -        f :: Int (bound at Defer03.hs:7:1)
          a :: Int (defined at Defer03.hs:4:1)
 +        f :: Int (bound at Defer03.hs:7:1)
          maxBound :: forall a. Bounded a => a
            with maxBound @Int
            (imported from ‘Prelude’
@@ -93,8 +92,8 @@ Defer03.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • In an equation for ‘f’: f = _
      • Relevant bindings include f :: Int (bound at Defer03.hs:7:1)
        Valid hole fits include
 -        f :: Int (bound at Defer03.hs:7:1)
          a :: Int (defined at Defer03.hs:4:1)
 +        f :: Int (bound at Defer03.hs:7:1)
          maxBound :: forall a. Bounded a => a
            with maxBound @Int
            (imported from ‘Prelude’

testsuite/tests/overloadedrecflds/should_fail/DRFHoleFits.stderr

+-
  DRFHoleFits.hs:7:7: error: [GHC-88464]
      • Found hole: _ :: T -> Int
      • In the expression: _ :: T -> Int
@@ -6,8 +5,8 @@ DRFHoleFits.hs:7:7: error: [GHC-88464]
      • Relevant bindings include
          bar :: T -> Int (bound at DRFHoleFits.hs:7:1)
        Valid hole fits include
 -        foo :: T -> Int (defined at DRFHoleFits.hs:5:16)
          bar :: T -> Int (defined at DRFHoleFits.hs:7:1)
 +        foo :: T -> Int (defined at DRFHoleFits.hs:5:16)
  DRFHoleFits.hs:8:7: error: [GHC-88464]
      • Found hole: _ :: A.S -> Int
@@ -20,3 +19,4 @@ DRFHoleFits.hs:8:7: error: [GHC-88464]
          A.foo :: A.S -> Int
            (imported qualified from ‘DRFHoleFits_A’ at DRFHoleFits.hs:3:1-35
             (and originally defined at DRFHoleFits_A.hs:5:16-18))
++

testsuite/tests/perf/compiler/hard_hole_fits.stderr

@@ -299,10 +299,10 @@ hard_hole_fits.hs:29:35: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            (bound at hard_hole_fits.hs:29:21)
          testMe :: HsExpr GhcPs -> Int (bound at hard_hole_fits.hs:14:1)
        Valid hole fits include
 -        n :: Language.Haskell.Syntax.Basic.ConTag
 -          (bound at hard_hole_fits.hs:29:25)
          i :: Language.Haskell.Syntax.Basic.SumWidth
            (bound at hard_hole_fits.hs:29:27)
 +        n :: Language.Haskell.Syntax.Basic.ConTag
 +          (bound at hard_hole_fits.hs:29:25)
          maxBound :: forall a. Bounded a => a
            with maxBound @Int
            (imported from ‘Prelude’

testsuite/tests/plugins/test-hole-plugin.stderr

+-
  test-hole-plugin.hs:12:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • Found hole: _too_long :: [Int] -> Int
        Or perhaps ‘_too_long’ is mis-spelled, or not in scope
@@ -14,11 +13,11 @@ test-hole-plugin.hs:13:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • Relevant bindings include
          j :: [Int] -> Int (bound at test-hole-plugin.hs:13:1)
        Valid hole fits include
 -        j :: [Int] -> Int
          f :: [Int] -> Int
 -        i :: [Int] -> Int
          g :: [Int] -> Int
          h :: [Int] -> Int
 +        i :: [Int] -> Int
 +        j :: [Int] -> Int
          head :: forall a. GHC.Internal.Stack.Types.HasCallStack => [a] -> a
          (Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)
@@ -59,3 +58,4 @@ test-hole-plugin.hs:16:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          minimum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
          product :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
          sum :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
++

testsuite/tests/th/T15321.stderr

@@ -6,7 +6,7 @@ T15321.hs:9:9: error: [GHC-88464]
          fail :: forall (m :: * -> *) a.
                  (MonadFail m, GHC.Internal.Stack.Types.HasCallStack) =>
                  String -> m a
 -          with fail @GHC.Internal.TH.Monad.Q @GHC.Internal.TH.Syntax.Exp
 +          with fail @GHC.Internal.TH.Monad.Q
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Control.Monad.Fail’))

testsuite/tests/typecheck/should_compile/T13050.stderr

@@ -7,13 +7,9 @@ T13050.hs:4:9: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          x :: Int (bound at T13050.hs:4:3)
          f :: Int -> Int -> Int (bound at T13050.hs:4:1)
        Valid hole fits include
 -        f :: Int -> Int -> Int (bound at T13050.hs:4:1)
          g :: Int -> Int -> Int (bound at T13050.hs:5:1)
          q :: Int -> Int -> Int (bound at T13050.hs:6:1)
 -        (-) :: forall a. Num a => a -> a -> a
 -          with (-) @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 +        f :: Int -> Int -> Int (bound at T13050.hs:4:1)
          asTypeOf :: forall a. a -> a -> a
            with asTypeOf @Int
            (imported from ‘Prelude’
@@ -22,22 +18,6 @@ T13050.hs:4:9: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with const @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        subtract :: forall a. Num a => a -> a -> a
 -          with subtract @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 -        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 -          with (^) @Int @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        gcd :: forall a. Integral a => a -> a -> a
 -          with gcd @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        lcm :: forall a. Integral a => a -> a -> a
 -          with lcm @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
          max :: forall a. Ord a => a -> a -> a
            with max @Int
            (imported from ‘Prelude’
@@ -54,10 +34,30 @@ T13050.hs:4:9: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with (+) @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Num’))
 +        (-) :: forall a. Num a => a -> a -> a
 +          with (-) @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        subtract :: forall a. Num a => a -> a -> a
 +          with subtract @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 +          with (^) @Int @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          div :: forall a. Integral a => a -> a -> a
            with div @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Real’))
 +        gcd :: forall a. Integral a => a -> a -> a
 +          with gcd @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
 +        lcm :: forall a. Integral a => a -> a -> a
 +          with lcm @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          mod :: forall a. Integral a => a -> a -> a
            with mod @Int
            (imported from ‘Prelude’
@@ -74,12 +74,12 @@ T13050.hs:4:9: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with seq @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Prim’))
 -        return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @((->) Int) @Int
 +        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +          with pure @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @((->) Int) @Int
 +        return :: forall (m :: * -> *) a. Monad m => a -> m a
 +          with return @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
@@ -92,13 +92,9 @@ T13050.hs:5:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          x :: Int (bound at T13050.hs:5:3)
          g :: Int -> Int -> Int (bound at T13050.hs:5:1)
        Valid hole fits include
 -        g :: Int -> Int -> Int (bound at T13050.hs:5:1)
          f :: Int -> Int -> Int (defined at T13050.hs:4:1)
          q :: Int -> Int -> Int (bound at T13050.hs:6:1)
 -        (-) :: forall a. Num a => a -> a -> a
 -          with (-) @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 +        g :: Int -> Int -> Int (bound at T13050.hs:5:1)
          asTypeOf :: forall a. a -> a -> a
            with asTypeOf @Int
            (imported from ‘Prelude’
@@ -107,22 +103,6 @@ T13050.hs:5:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with const @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        subtract :: forall a. Num a => a -> a -> a
 -          with subtract @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 -        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 -          with (^) @Int @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        gcd :: forall a. Integral a => a -> a -> a
 -          with gcd @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        lcm :: forall a. Integral a => a -> a -> a
 -          with lcm @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
          max :: forall a. Ord a => a -> a -> a
            with max @Int
            (imported from ‘Prelude’
@@ -139,10 +119,30 @@ T13050.hs:5:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with (+) @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Num’))
 +        (-) :: forall a. Num a => a -> a -> a
 +          with (-) @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        subtract :: forall a. Num a => a -> a -> a
 +          with subtract @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 +          with (^) @Int @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          div :: forall a. Integral a => a -> a -> a
            with div @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Real’))
 +        gcd :: forall a. Integral a => a -> a -> a
 +          with gcd @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
 +        lcm :: forall a. Integral a => a -> a -> a
 +          with lcm @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          mod :: forall a. Integral a => a -> a -> a
            with mod @Int
            (imported from ‘Prelude’
@@ -159,12 +159,12 @@ T13050.hs:5:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with seq @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Prim’))
 -        return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @((->) Int) @Int
 +        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +          with pure @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @((->) Int) @Int
 +        return :: forall (m :: * -> *) a. Monad m => a -> m a
 +          with return @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
@@ -178,13 +178,9 @@ T13050.hs:6:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          x :: Int (bound at T13050.hs:6:3)
          q :: Int -> Int -> Int (bound at T13050.hs:6:1)
        Valid hole fits include
 -        q :: Int -> Int -> Int (bound at T13050.hs:6:1)
          f :: Int -> Int -> Int (defined at T13050.hs:4:1)
          g :: Int -> Int -> Int (defined at T13050.hs:5:1)
 -        (-) :: forall a. Num a => a -> a -> a
 -          with (-) @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 +        q :: Int -> Int -> Int (bound at T13050.hs:6:1)
          asTypeOf :: forall a. a -> a -> a
            with asTypeOf @Int
            (imported from ‘Prelude’
@@ -193,22 +189,6 @@ T13050.hs:6:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with const @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        subtract :: forall a. Num a => a -> a -> a
 -          with subtract @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 -        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 -          with (^) @Int @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        gcd :: forall a. Integral a => a -> a -> a
 -          with gcd @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        lcm :: forall a. Integral a => a -> a -> a
 -          with lcm @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
          max :: forall a. Ord a => a -> a -> a
            with max @Int
            (imported from ‘Prelude’
@@ -225,10 +205,30 @@ T13050.hs:6:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with (+) @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Num’))
 +        (-) :: forall a. Num a => a -> a -> a
 +          with (-) @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        subtract :: forall a. Num a => a -> a -> a
 +          with subtract @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 +          with (^) @Int @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          div :: forall a. Integral a => a -> a -> a
            with div @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Real’))
 +        gcd :: forall a. Integral a => a -> a -> a
 +          with gcd @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
 +        lcm :: forall a. Integral a => a -> a -> a
 +          with lcm @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          mod :: forall a. Integral a => a -> a -> a
            with mod @Int
            (imported from ‘Prelude’
@@ -245,12 +245,12 @@ T13050.hs:6:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with seq @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Prim’))
 -        return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @((->) Int) @Int
 +        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +          with pure @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @((->) Int) @Int
 +        return :: forall (m :: * -> *) a. Monad m => a -> m a
 +          with return @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))

testsuite/tests/typecheck/should_compile/T14273.stderr

@@ -28,27 +28,27 @@ T14273.hs:7:32: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          pleaseShow :: Bool -> a -> Maybe String (bound at T14273.hs:6:1)
        Constraints include Show a (from T14273.hs:5:1-49)
        Valid hole fits include
 -        a :: a (bound at T14273.hs:7:17)
          k :: String (bound at T14273.hs:10:1)
 +        a :: a (bound at T14273.hs:7:17)
          otherwise :: Bool
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        False :: Bool
 +        EQ :: Ordering
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Types’))
 -        True :: Bool
 +        GT :: Ordering
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Types’))
          LT :: Ordering
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Types’))
 -        EQ :: Ordering
 +        () :: () (bound at <wired into compiler>)
 +        False :: Bool
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Types’))
 -        GT :: Ordering
 +        True :: Bool
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Types’))
 -        () :: () (bound at <wired into compiler>)
          pi :: forall a. Floating a => a
            with pi @Double
            (imported from ‘Prelude’

testsuite/tests/typecheck/should_compile/T14590.stderr

@@ -8,14 +8,10 @@ T14590.hs:4:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          x :: Int (bound at T14590.hs:4:4)
          f1 :: Int -> Int -> Int (bound at T14590.hs:4:1)
        Valid hole fits include
 -        f1 :: Int -> Int -> Int (bound at T14590.hs:4:1)
          f2 :: Int -> Int -> Int (bound at T14590.hs:5:1)
          f3 :: Int -> Int -> Int (bound at T14590.hs:6:1)
          f4 :: Int -> Int -> Int (bound at T14590.hs:7:1)
 -        (-) :: forall a. Num a => a -> a -> a
 -          with (-) @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 +        f1 :: Int -> Int -> Int (bound at T14590.hs:4:1)
          asTypeOf :: forall a. a -> a -> a
            with asTypeOf @Int
            (imported from ‘Prelude’
@@ -24,22 +20,6 @@ T14590.hs:4:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with const @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        subtract :: forall a. Num a => a -> a -> a
 -          with subtract @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 -        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 -          with (^) @Int @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        gcd :: forall a. Integral a => a -> a -> a
 -          with gcd @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        lcm :: forall a. Integral a => a -> a -> a
 -          with lcm @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
          max :: forall a. Ord a => a -> a -> a
            with max @Int
            (imported from ‘Prelude’
@@ -56,10 +36,30 @@ T14590.hs:4:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with (+) @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Num’))
 +        (-) :: forall a. Num a => a -> a -> a
 +          with (-) @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        subtract :: forall a. Num a => a -> a -> a
 +          with subtract @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 +          with (^) @Int @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          div :: forall a. Integral a => a -> a -> a
            with div @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Real’))
 +        gcd :: forall a. Integral a => a -> a -> a
 +          with gcd @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
 +        lcm :: forall a. Integral a => a -> a -> a
 +          with lcm @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          mod :: forall a. Integral a => a -> a -> a
            with mod @Int
            (imported from ‘Prelude’
@@ -76,12 +76,12 @@ T14590.hs:4:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with seq @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Prim’))
 -        return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @((->) Int) @Int
 +        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +          with pure @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @((->) Int) @Int
 +        return :: forall (m :: * -> *) a. Monad m => a -> m a
 +          with return @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
@@ -96,14 +96,10 @@ T14590.hs:5:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          x :: Int (bound at T14590.hs:5:4)
          f2 :: Int -> Int -> Int (bound at T14590.hs:5:1)
        Valid hole fits include
 -        f2 :: Int -> Int -> Int (bound at T14590.hs:5:1)
          f1 :: Int -> Int -> Int (defined at T14590.hs:4:1)
          f3 :: Int -> Int -> Int (bound at T14590.hs:6:1)
          f4 :: Int -> Int -> Int (bound at T14590.hs:7:1)
 -        (-) :: forall a. Num a => a -> a -> a
 -          with (-) @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 +        f2 :: Int -> Int -> Int (bound at T14590.hs:5:1)
          asTypeOf :: forall a. a -> a -> a
            with asTypeOf @Int
            (imported from ‘Prelude’
@@ -112,22 +108,6 @@ T14590.hs:5:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with const @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        subtract :: forall a. Num a => a -> a -> a
 -          with subtract @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 -        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 -          with (^) @Int @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        gcd :: forall a. Integral a => a -> a -> a
 -          with gcd @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        lcm :: forall a. Integral a => a -> a -> a
 -          with lcm @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
          max :: forall a. Ord a => a -> a -> a
            with max @Int
            (imported from ‘Prelude’
@@ -144,10 +124,30 @@ T14590.hs:5:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with (+) @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Num’))
 +        (-) :: forall a. Num a => a -> a -> a
 +          with (-) @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        subtract :: forall a. Num a => a -> a -> a
 +          with subtract @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 +          with (^) @Int @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          div :: forall a. Integral a => a -> a -> a
            with div @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Real’))
 +        gcd :: forall a. Integral a => a -> a -> a
 +          with gcd @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
 +        lcm :: forall a. Integral a => a -> a -> a
 +          with lcm @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          mod :: forall a. Integral a => a -> a -> a
            with mod @Int
            (imported from ‘Prelude’
@@ -164,12 +164,12 @@ T14590.hs:5:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with seq @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Prim’))
 -        return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @((->) Int) @Int
 +        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +          with pure @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @((->) Int) @Int
 +        return :: forall (m :: * -> *) a. Monad m => a -> m a
 +          with return @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
@@ -182,14 +182,10 @@ T14590.hs:6:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          x :: Int (bound at T14590.hs:6:4)
          f3 :: Int -> Int -> Int (bound at T14590.hs:6:1)
        Valid hole fits include
 -        f3 :: Int -> Int -> Int (bound at T14590.hs:6:1)
          f1 :: Int -> Int -> Int (defined at T14590.hs:4:1)
          f2 :: Int -> Int -> Int (defined at T14590.hs:5:1)
          f4 :: Int -> Int -> Int (bound at T14590.hs:7:1)
 -        (-) :: forall a. Num a => a -> a -> a
 -          with (-) @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 +        f3 :: Int -> Int -> Int (bound at T14590.hs:6:1)
          asTypeOf :: forall a. a -> a -> a
            with asTypeOf @Int
            (imported from ‘Prelude’
@@ -198,22 +194,6 @@ T14590.hs:6:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with const @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        subtract :: forall a. Num a => a -> a -> a
 -          with subtract @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 -        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 -          with (^) @Int @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        gcd :: forall a. Integral a => a -> a -> a
 -          with gcd @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        lcm :: forall a. Integral a => a -> a -> a
 -          with lcm @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
          max :: forall a. Ord a => a -> a -> a
            with max @Int
            (imported from ‘Prelude’
@@ -230,10 +210,30 @@ T14590.hs:6:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with (+) @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Num’))
 +        (-) :: forall a. Num a => a -> a -> a
 +          with (-) @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        subtract :: forall a. Num a => a -> a -> a
 +          with subtract @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 +          with (^) @Int @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          div :: forall a. Integral a => a -> a -> a
            with div @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Real’))
 +        gcd :: forall a. Integral a => a -> a -> a
 +          with gcd @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
 +        lcm :: forall a. Integral a => a -> a -> a
 +          with lcm @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          mod :: forall a. Integral a => a -> a -> a
            with mod @Int
            (imported from ‘Prelude’
@@ -250,12 +250,12 @@ T14590.hs:6:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with seq @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Prim’))
 -        return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @((->) Int) @Int
 +        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +          with pure @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @((->) Int) @Int
 +        return :: forall (m :: * -> *) a. Monad m => a -> m a
 +          with return @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
@@ -269,14 +269,10 @@ T14590.hs:7:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          x :: Int (bound at T14590.hs:7:4)
          f4 :: Int -> Int -> Int (bound at T14590.hs:7:1)
        Valid hole fits include
 -        f4 :: Int -> Int -> Int (bound at T14590.hs:7:1)
          f1 :: Int -> Int -> Int (defined at T14590.hs:4:1)
          f2 :: Int -> Int -> Int (defined at T14590.hs:5:1)
          f3 :: Int -> Int -> Int (defined at T14590.hs:6:1)
 -        (-) :: forall a. Num a => a -> a -> a
 -          with (-) @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 +        f4 :: Int -> Int -> Int (bound at T14590.hs:7:1)
          asTypeOf :: forall a. a -> a -> a
            with asTypeOf @Int
            (imported from ‘Prelude’
@@ -285,22 +281,6 @@ T14590.hs:7:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with const @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        subtract :: forall a. Num a => a -> a -> a
 -          with subtract @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Num’))
 -        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 -          with (^) @Int @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        gcd :: forall a. Integral a => a -> a -> a
 -          with gcd @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
 -        lcm :: forall a. Integral a => a -> a -> a
 -          with lcm @Int
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Real’))
          max :: forall a. Ord a => a -> a -> a
            with max @Int
            (imported from ‘Prelude’
@@ -317,10 +297,30 @@ T14590.hs:7:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with (+) @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Num’))
 +        (-) :: forall a. Num a => a -> a -> a
 +          with (-) @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        subtract :: forall a. Num a => a -> a -> a
 +          with subtract @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Num’))
 +        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 +          with (^) @Int @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          div :: forall a. Integral a => a -> a -> a
            with div @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Real’))
 +        gcd :: forall a. Integral a => a -> a -> a
 +          with gcd @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
 +        lcm :: forall a. Integral a => a -> a -> a
 +          with lcm @Int
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Real’))
          mod :: forall a. Integral a => a -> a -> a
            with mod @Int
            (imported from ‘Prelude’
@@ -337,12 +337,12 @@ T14590.hs:7:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with seq @Int @Int
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Prim’))
 -        return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @((->) Int) @Int
 +        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +          with pure @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @((->) Int) @Int
 +        return :: forall (m :: * -> *) a. Monad m => a -> m a
 +          with return @((->) Int)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))

testsuite/tests/typecheck/should_compile/T25180.stderr

@@ -29,16 +29,20 @@ T25180.hs:19:8: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          tup1 :: a -> Solo a (bound at T25180.hs:19:1)
        Valid hole fits include
          tup1 :: a -> Solo a (bound at T25180.hs:19:1)
 +        Solo :: forall a. a -> Solo a
 +          with Solo @a
 +          (imported from ‘Data.Tuple’ at T25180.hs:6:1-17
 +           (and originally defined in ‘GHC.Internal.Tuple’))
          MkSolo :: forall a. a -> Solo a
            with MkSolo @a
            (imported from ‘Data.Tuple’ at T25180.hs:6:1-17
             (and originally defined in ‘GHC.Internal.Tuple’))
 -        return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @Solo @a
 +        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +          with pure @Solo
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @Solo @a
 +        return :: forall (m :: * -> *) a. Monad m => a -> m a
 +          with return @Solo
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))

testsuite/tests/typecheck/should_compile/abstract_refinement_hole_fits.stderr

+-
  abstract_refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • Found hole: _ :: [Integer] -> Integer
      • In an equation for ‘f’: f = _
@@ -6,8 +5,8 @@ abstract_refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -W
          f :: [Integer] -> Integer
            (bound at abstract_refinement_hole_fits.hs:4:1)
        Valid hole fits include
 -        f :: [Integer] -> Integer
          g :: [Integer] -> Integer
 +        f :: [Integer] -> Integer
          head :: forall a. GHC.Internal.Stack.Types.HasCallStack => [a] -> a
          last :: forall a. GHC.Internal.Stack.Types.HasCallStack => [a] -> a
          maximum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
@@ -61,46 +60,46 @@ abstract_refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -W
            where fst :: forall a b. (a, b) -> a
          snd (_ :: (a3, t0 -> [Integer] -> Integer)) (_ :: t0)
            where snd :: forall a b. (a, b) -> b
 -        return (_ :: Integer)
 -          where return :: forall (m :: * -> *) a. Monad m => a -> m a
          pure (_ :: Integer)
            where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -        (>>=) (_ :: [Integer] -> a6) (_ :: a6 -> [Integer] -> Integer)
 -          where (>>=) :: forall (m :: * -> *) a b.
 -                         Monad m =>
 -                         m a -> (a -> m b) -> m b
 -        (>>) (_ :: [Integer] -> a5) (_ :: [Integer] -> Integer)
 -          where (>>) :: forall (m :: * -> *) a b.
 -                        Monad m =>
 -                        m a -> m b -> m b
 -        fmap (_ :: a7 -> Integer) (_ :: [Integer] -> a7)
 -          where fmap :: forall (f :: * -> *) a b.
 +        return (_ :: Integer)
 +          where return :: forall (m :: * -> *) a. Monad m => a -> m a
 +        (*>) (_ :: [Integer] -> a8) (_ :: [Integer] -> Integer)
 +          where (*>) :: forall (f :: * -> *) a b.
 +                        Applicative f =>
 +                        f a -> f b -> f b
 +        (<$) (_ :: Integer) (_ :: [Integer] -> b5)
 +          where (<$) :: forall (f :: * -> *) a b.
                          Functor f =>
 -                        (a -> b) -> f a -> f b
 +                        a -> f b -> f a
 +        (<*) (_ :: [Integer] -> Integer) (_ :: [Integer] -> b4)
 +          where (<*) :: forall (f :: * -> *) a b.
 +                        Applicative f =>
 +                        f a -> f b -> f a
          (<*>) (_ :: [Integer] -> a9 -> Integer) (_ :: [Integer] -> a9)
            where (<*>) :: forall (f :: * -> *) a b.
                           Applicative f =>
                           f (a -> b) -> f a -> f b
 -        (*>) (_ :: [Integer] -> a8) (_ :: [Integer] -> Integer)
 -          where (*>) :: forall (f :: * -> *) a b.
 -                        Applicative f =>
 -                        f a -> f b -> f b
          (=<<) (_ :: a1 -> [Integer] -> Integer) (_ :: [Integer] -> a1)
            where (=<<) :: forall (m :: * -> *) a b.
                           Monad m =>
                           (a -> m b) -> m a -> m b
 +        (>>) (_ :: [Integer] -> a5) (_ :: [Integer] -> Integer)
 +          where (>>) :: forall (m :: * -> *) a b.
 +                        Monad m =>
 +                        m a -> m b -> m b
 +        (>>=) (_ :: [Integer] -> a6) (_ :: a6 -> [Integer] -> Integer)
 +          where (>>=) :: forall (m :: * -> *) a b.
 +                         Monad m =>
 +                         m a -> (a -> m b) -> m b
 +        fmap (_ :: a7 -> Integer) (_ :: [Integer] -> a7)
 +          where fmap :: forall (f :: * -> *) a b.
 +                        Functor f =>
 +                        (a -> b) -> f a -> f b
          (<$>) (_ :: a2 -> Integer) (_ :: [Integer] -> a2)
            where (<$>) :: forall (f :: * -> *) a b.
                           Functor f =>
                           (a -> b) -> f a -> f b
 -        (<*) (_ :: [Integer] -> Integer) (_ :: [Integer] -> b4)
 -          where (<*) :: forall (f :: * -> *) a b.
 -                        Applicative f =>
 -                        f a -> f b -> f a
 -        (<$) (_ :: Integer) (_ :: [Integer] -> b5)
 -          where (<$) :: forall (f :: * -> *) a b.
 -                        Functor f =>
 -                        a -> f b -> f a
          id (_ :: [Integer] -> Integer)
            where id :: forall a. a -> a
          head (_ :: [[Integer] -> Integer])
@@ -125,16 +124,16 @@ abstract_refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -W
            where const :: forall a b. a -> b -> a
          uncurry (_ :: a4 -> b3 -> [Integer] -> Integer) (_ :: (a4, b3))
            where uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
 -        seq (_ :: t2) (_ :: [Integer] -> Integer)
 -          where seq :: forall a b. a -> b -> b
          ($!) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
            where ($!) :: forall a b. (a -> b) -> a -> b
 +        seq (_ :: t2) (_ :: [Integer] -> Integer)
 +          where seq :: forall a b. a -> b -> b
          ($) (_ :: t0 -> [Integer] -> Integer) (_ :: t0)
            where ($) :: forall a b. (a -> b) -> a -> b
 -        return (_ :: [Integer] -> Integer) (_ :: t0)
 -          where return :: forall (m :: * -> *) a. Monad m => a -> m a
          pure (_ :: [Integer] -> Integer) (_ :: t0)
            where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +        return (_ :: [Integer] -> Integer) (_ :: t0)
 +          where return :: forall (m :: * -> *) a. Monad m => a -> m a
  abstract_refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • Found hole: _ :: Integer -> [Integer] -> Integer
@@ -145,8 +144,8 @@ abstract_refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -W
            (bound at abstract_refinement_hole_fits.hs:7:1)
        Valid hole fits include
          const :: forall a b. a -> b -> a
 -        return :: forall (m :: * -> *) a. Monad m => a -> m a
          pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +        return :: forall (m :: * -> *) a. Monad m => a -> m a
        Valid refinement hole fits include
          foldl (_ :: Integer -> Integer -> Integer)
            where foldl :: forall (t :: * -> *) b a.
@@ -190,49 +189,49 @@ abstract_refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -W
            where fst :: forall a b. (a, b) -> a
          snd (_ :: (a3, t0 -> Integer -> [Integer] -> Integer)) (_ :: t0)
            where snd :: forall a b. (a, b) -> b
 -        return (_ :: [Integer] -> Integer)
 -          where return :: forall (m :: * -> *) a. Monad m => a -> m a
          pure (_ :: [Integer] -> Integer)
            where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -        (>>=) (_ :: Integer -> a6)
 -              (_ :: a6 -> Integer -> [Integer] -> Integer)
 -          where (>>=) :: forall (m :: * -> *) a b.
 -                         Monad m =>
 -                         m a -> (a -> m b) -> m b
 -        (>>) (_ :: Integer -> a5) (_ :: Integer -> [Integer] -> Integer)
 -          where (>>) :: forall (m :: * -> *) a b.
 -                        Monad m =>
 -                        m a -> m b -> m b
 -        fmap (_ :: a7 -> [Integer] -> Integer) (_ :: Integer -> a7)
 -          where fmap :: forall (f :: * -> *) a b.
 +        return (_ :: [Integer] -> Integer)
 +          where return :: forall (m :: * -> *) a. Monad m => a -> m a
 +        (*>) (_ :: Integer -> a8) (_ :: Integer -> [Integer] -> Integer)
 +          where (*>) :: forall (f :: * -> *) a b.
 +                        Applicative f =>
 +                        f a -> f b -> f b
 +        (<$) (_ :: [Integer] -> Integer) (_ :: Integer -> b5)
 +          where (<$) :: forall (f :: * -> *) a b.
                          Functor f =>
 -                        (a -> b) -> f a -> f b
 +                        a -> f b -> f a
 +        (<*) (_ :: Integer -> [Integer] -> Integer) (_ :: Integer -> b4)
 +          where (<*) :: forall (f :: * -> *) a b.
 +                        Applicative f =>
 +                        f a -> f b -> f a
          (<*>) (_ :: Integer -> a9 -> [Integer] -> Integer)
                (_ :: Integer -> a9)
            where (<*>) :: forall (f :: * -> *) a b.
                           Applicative f =>
                           f (a -> b) -> f a -> f b
 -        (*>) (_ :: Integer -> a8) (_ :: Integer -> [Integer] -> Integer)
 -          where (*>) :: forall (f :: * -> *) a b.
 -                        Applicative f =>
 -                        f a -> f b -> f b
          (=<<) (_ :: a1 -> Integer -> [Integer] -> Integer)
                (_ :: Integer -> a1)
            where (=<<) :: forall (m :: * -> *) a b.
                           Monad m =>
                           (a -> m b) -> m a -> m b
 +        (>>) (_ :: Integer -> a5) (_ :: Integer -> [Integer] -> Integer)
 +          where (>>) :: forall (m :: * -> *) a b.
 +                        Monad m =>
 +                        m a -> m b -> m b
 +        (>>=) (_ :: Integer -> a6)
 +              (_ :: a6 -> Integer -> [Integer] -> Integer)
 +          where (>>=) :: forall (m :: * -> *) a b.
 +                         Monad m =>
 +                         m a -> (a -> m b) -> m b
 +        fmap (_ :: a7 -> [Integer] -> Integer) (_ :: Integer -> a7)
 +          where fmap :: forall (f :: * -> *) a b.
 +                        Functor f =>
 +                        (a -> b) -> f a -> f b
          (<$>) (_ :: a2 -> [Integer] -> Integer) (_ :: Integer -> a2)
            where (<$>) :: forall (f :: * -> *) a b.
                           Functor f =>
                           (a -> b) -> f a -> f b
 -        (<*) (_ :: Integer -> [Integer] -> Integer) (_ :: Integer -> b4)
 -          where (<*) :: forall (f :: * -> *) a b.
 -                        Applicative f =>
 -                        f a -> f b -> f a
 -        (<$) (_ :: [Integer] -> Integer) (_ :: Integer -> b5)
 -          where (<$) :: forall (f :: * -> *) a b.
 -                        Functor f =>
 -                        a -> f b -> f a
          id (_ :: Integer -> [Integer] -> Integer)
            where id :: forall a. a -> a
          head (_ :: [Integer -> [Integer] -> Integer])
@@ -259,13 +258,14 @@ abstract_refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -W
          uncurry (_ :: a4 -> b3 -> Integer -> [Integer] -> Integer)
                  (_ :: (a4, b3))
            where uncurry :: forall a b c. (a -> b -> c) -> (a, b) -> c
 -        seq (_ :: t2) (_ :: Integer -> [Integer] -> Integer)
 -          where seq :: forall a b. a -> b -> b
          ($!) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
            where ($!) :: forall a b. (a -> b) -> a -> b
 +        seq (_ :: t2) (_ :: Integer -> [Integer] -> Integer)
 +          where seq :: forall a b. a -> b -> b
          ($) (_ :: t0 -> Integer -> [Integer] -> Integer) (_ :: t0)
            where ($) :: forall a b. (a -> b) -> a -> b
 -        return (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
 -          where return :: forall (m :: * -> *) a. Monad m => a -> m a
          pure (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
            where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +        return (_ :: Integer -> [Integer] -> Integer) (_ :: t0)
 +          where return :: forall (m :: * -> *) a. Monad m => a -> m a
++

testsuite/tests/typecheck/should_compile/constraint_hole_fits.stderr

+-
  constraint_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • Found hole: _ :: [a] -> a
        Where: ‘a’ is a rigid type variable bound by
@@ -42,10 +41,10 @@ constraint_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            where ($) :: forall a b. (a -> b) -> a -> b
          ($!) (_ :: [a] -> a)
            where ($!) :: forall a b. (a -> b) -> a -> b
 -        return (_ :: a)
 -          where return :: forall (m :: * -> *) a. Monad m => a -> m a
          pure (_ :: a)
            where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +        return (_ :: a)
 +          where return :: forall (m :: * -> *) a. Monad m => a -> m a
          id (_ :: [a] -> a)
            where id :: forall a. a -> a
          head (_ :: [[a] -> a])
@@ -62,3 +61,4 @@ constraint_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            where (!!) :: forall a.
                          GHC.Internal.Stack.Types.HasCallStack =>
                          [a] -> Int -> a
++

testsuite/tests/typecheck/should_compile/free_monad_hole_fits.stderr

+-
  free_monad_hole_fits.hs:14:28: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • Found hole:
          _a :: (Free f a -> Free f b) -> f (Free f a) -> f (Free f b)
@@ -55,10 +54,6 @@ free_monad_hole_fits.hs:25:31: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault
        Constraints include
          Applicative f (from free_monad_hole_fits.hs:22:10-40)
        Valid refinement hole fits include
 -        fmap (_ :: a -> b)
 -          where fmap :: forall (f :: * -> *) a b.
 -                        Functor f =>
 -                        (a -> b) -> f a -> f b
          (<*>) (_ :: Free f (a -> b))
            where (<*>) :: forall (f :: * -> *) a b.
                           Applicative f =>
@@ -67,6 +62,10 @@ free_monad_hole_fits.hs:25:31: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault
            where (=<<) :: forall (m :: * -> *) a b.
                           Monad m =>
                           (a -> m b) -> m a -> m b
 +        fmap (_ :: a -> b)
 +          where fmap :: forall (f :: * -> *) a b.
 +                        Functor f =>
 +                        (a -> b) -> f a -> f b
          (<$>) (_ :: a -> b)
            where (<$>) :: forall (f :: * -> *) a b.
                           Functor f =>
@@ -75,3 +74,4 @@ free_monad_hole_fits.hs:25:31: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault
            where ($) :: forall a b. (a -> b) -> a -> b
          pure (_ :: Free f b)
            where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
++

testsuite/tests/typecheck/should_compile/hole_constraints.stderr

+-
  hole_constraints.hs:8:6: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • Found hole: _ :: a
        Where: ‘a’ is a rigid type variable bound by
@@ -67,8 +66,9 @@ hole_constraints.hs:27:32: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          foo :: AnyShow -> String (bound at hole_constraints.hs:27:1)
        Constraints include Show a (from hole_constraints.hs:27:19-27)
        Valid hole fits include
 -        f3 :: forall a. C a => a
          f1 :: forall a. Eq a => a
          f2 :: forall a. (Show a, Eq a) => a
 +        f3 :: forall a. C a => a
          [] :: forall a. [a]
          mempty :: forall a. Monoid a => a
++

testsuite/tests/typecheck/should_compile/holes.stderr

@@ -40,18 +40,12 @@ holes.hs:11:15: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          y :: [a] (bound at holes.hs:11:3)
          z :: [a] -> [a] (bound at holes.hs:11:1)
        Valid hole fits include
 -        y :: [a]
 -        z :: [a] -> [a]
          g :: Int -> Char
          h :: [Char]
 +        y :: [a]
 +        z :: [a] -> [a]
          f :: forall {p}. p
          otherwise :: Bool
 -        False :: Bool
 -        True :: Bool
 -        LT :: Ordering
 -        EQ :: Ordering
 -        GT :: Ordering
 -        () :: ()
          (&&) :: Bool -> Bool -> Bool
          not :: Bool -> Bool
          (||) :: Bool -> Bool -> Bool
@@ -74,22 +68,48 @@ holes.hs:11:15: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          putStrLn :: String -> IO ()
          readFile :: FilePath -> IO String
          writeFile :: FilePath -> String -> IO ()
 +        EQ :: Ordering
 +        GT :: Ordering
 +        LT :: Ordering
 +        () :: ()
 +        False :: Bool
 +        True :: Bool
          (++) :: forall a. [a] -> [a] -> [a]
 -        filter :: forall a. (a -> Bool) -> [a] -> [a]
 -        fromInteger :: forall a. Num a => Integer -> a
 -        (-) :: forall a. Num a => a -> a -> a
 -        fromRational :: forall a. Fractional a => Rational -> a
 -        negate :: forall a. Num a => a -> a
 -        fromIntegral :: forall a b. (Integral a, Num b) => a -> b
 -        toInteger :: forall a. Integral a => a -> Integer
 -        toRational :: forall a. Real a => a -> Rational
 -        (:) :: forall a. a -> [a] -> [a]
 -        Nothing :: forall a. Maybe a
 -        Just :: forall a. a -> Maybe a
 -        [] :: forall a. [a]
          asTypeOf :: forall a. a -> a -> a
          id :: forall a. a -> a
          until :: forall a. (a -> Bool) -> (a -> a) -> a -> a
 +        (**) :: forall a. Floating a => a -> a -> a
 +        acos :: forall a. Floating a => a -> a
 +        acosh :: forall a. Floating a => a -> a
 +        asin :: forall a. Floating a => a -> a
 +        asinh :: forall a. Floating a => a -> a
 +        atan :: forall a. Floating a => a -> a
 +        atan2 :: forall a. RealFloat a => a -> a -> a
 +        atanh :: forall a. Floating a => a -> a
 +        cos :: forall a. Floating a => a -> a
 +        cosh :: forall a. Floating a => a -> a
 +        decodeFloat :: forall a. RealFloat a => a -> (Integer, Int)
 +        encodeFloat :: forall a. RealFloat a => Integer -> Int -> a
 +        exp :: forall a. Floating a => a -> a
 +        exponent :: forall a. RealFloat a => a -> Int
 +        floatDigits :: forall a. RealFloat a => a -> Int
 +        floatRadix :: forall a. RealFloat a => a -> Integer
 +        floatRange :: forall a. RealFloat a => a -> (Int, Int)
 +        isDenormalized :: forall a. RealFloat a => a -> Bool
 +        isIEEE :: forall a. RealFloat a => a -> Bool
 +        isInfinite :: forall a. RealFloat a => a -> Bool
 +        isNaN :: forall a. RealFloat a => a -> Bool
 +        isNegativeZero :: forall a. RealFloat a => a -> Bool
 +        log :: forall a. Floating a => a -> a
 +        logBase :: forall a. Floating a => a -> a -> a
 +        pi :: forall a. Floating a => a
 +        scaleFloat :: forall a. RealFloat a => Int -> a -> a
 +        significand :: forall a. RealFloat a => a -> a
 +        sin :: forall a. Floating a => a -> a
 +        sinh :: forall a. Floating a => a -> a
 +        sqrt :: forall a. Floating a => a -> a
 +        tan :: forall a. Floating a => a -> a
 +        tanh :: forall a. Floating a => a -> a
          ioError :: forall a.
                     GHC.Internal.Stack.Types.HasCallStack =>
                     IOError -> IO a
@@ -102,6 +122,7 @@ holes.hs:11:15: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
                   [a] -> [a]
          drop :: forall a. Int -> [a] -> [a]
          dropWhile :: forall a. (a -> Bool) -> [a] -> [a]
 +        filter :: forall a. (a -> Bool) -> [a] -> [a]
          head :: forall a. GHC.Internal.Stack.Types.HasCallStack => [a] -> a
          init :: forall a.
                  GHC.Internal.Stack.Types.HasCallStack =>
@@ -120,80 +141,57 @@ holes.hs:11:15: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
                  [a] -> [a]
          take :: forall a. Int -> [a] -> [a]
          takeWhile :: forall a. (a -> Bool) -> [a] -> [a]
 -        subtract :: forall a. Num a => a -> a -> a
 -        readParen :: forall a. Bool -> ReadS a -> ReadS a
 -        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 -        even :: forall a. Integral a => a -> Bool
 -        gcd :: forall a. Integral a => a -> a -> a
 -        lcm :: forall a. Integral a => a -> a -> a
 -        odd :: forall a. Integral a => a -> Bool
 -        (**) :: forall a. Floating a => a -> a -> a
 -        acos :: forall a. Floating a => a -> a
 -        acosh :: forall a. Floating a => a -> a
 -        asin :: forall a. Floating a => a -> a
 -        asinh :: forall a. Floating a => a -> a
 -        atan :: forall a. Floating a => a -> a
 -        atanh :: forall a. Floating a => a -> a
 -        cos :: forall a. Floating a => a -> a
 -        cosh :: forall a. Floating a => a -> a
 -        exp :: forall a. Floating a => a -> a
 -        log :: forall a. Floating a => a -> a
 -        logBase :: forall a. Floating a => a -> a -> a
 -        pi :: forall a. Floating a => a
 -        sin :: forall a. Floating a => a -> a
 -        sinh :: forall a. Floating a => a -> a
 -        sqrt :: forall a. Floating a => a -> a
 -        tan :: forall a. Floating a => a -> a
 -        tanh :: forall a. Floating a => a -> a
 -        atan2 :: forall a. RealFloat a => a -> a -> a
 -        decodeFloat :: forall a. RealFloat a => a -> (Integer, Int)
 -        encodeFloat :: forall a. RealFloat a => Integer -> Int -> a
 -        exponent :: forall a. RealFloat a => a -> Int
 -        floatDigits :: forall a. RealFloat a => a -> Int
 -        floatRadix :: forall a. RealFloat a => a -> Integer
 -        floatRange :: forall a. RealFloat a => a -> (Int, Int)
 -        isDenormalized :: forall a. RealFloat a => a -> Bool
 -        isIEEE :: forall a. RealFloat a => a -> Bool
 -        isInfinite :: forall a. RealFloat a => a -> Bool
 -        isNaN :: forall a. RealFloat a => a -> Bool
 -        isNegativeZero :: forall a. RealFloat a => a -> Bool
 -        scaleFloat :: forall a. RealFloat a => Int -> a -> a
 -        significand :: forall a. RealFloat a => a -> a
          (*) :: forall a. Num a => a -> a -> a
          (+) :: forall a. Num a => a -> a -> a
 +        (-) :: forall a. Num a => a -> a -> a
          abs :: forall a. Num a => a -> a
 +        fromInteger :: forall a. Num a => Integer -> a
 +        negate :: forall a. Num a => a -> a
          signum :: forall a. Num a => a -> a
 +        subtract :: forall a. Num a => a -> a -> a
 +        readParen :: forall a. Bool -> ReadS a -> ReadS a
          (/) :: forall a. Fractional a => a -> a -> a
 -        recip :: forall a. Fractional a => a -> a
 +        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
          div :: forall a. Integral a => a -> a -> a
          divMod :: forall a. Integral a => a -> a -> (a, a)
 +        even :: forall a. Integral a => a -> Bool
 +        fromIntegral :: forall a b. (Integral a, Num b) => a -> b
 +        fromRational :: forall a. Fractional a => Rational -> a
 +        gcd :: forall a. Integral a => a -> a -> a
 +        lcm :: forall a. Integral a => a -> a -> a
          mod :: forall a. Integral a => a -> a -> a
 +        odd :: forall a. Integral a => a -> Bool
          quot :: forall a. Integral a => a -> a -> a
          quotRem :: forall a. Integral a => a -> a -> (a, a)
 +        recip :: forall a. Fractional a => a -> a
          rem :: forall a. Integral a => a -> a -> a
 -        zip :: forall a b. [a] -> [b] -> [(a, b)]
 +        toInteger :: forall a. Integral a => a -> Integer
 +        toRational :: forall a. Real a => a -> Rational
 +        Just :: forall a. a -> Maybe a
 +        Nothing :: forall a. Maybe a
 +        (:) :: forall a. a -> [a] -> [a]
 +        [] :: forall a. [a]
 +        const :: forall a b. a -> b -> a
          map :: forall a b. (a -> b) -> [a] -> [b]
 -        realToFrac :: forall a b. (Real a, Fractional b) => a -> b
          Left :: forall a b. a -> Either a b
          Right :: forall a b. b -> Either a b
 -        (,) :: forall a b. a -> b -> (a, b)
 -        const :: forall a b. a -> b -> a
          maybe :: forall b a. b -> (a -> b) -> Maybe a -> b
          fst :: forall a b. (a, b) -> a
          snd :: forall a b. (a, b) -> b
          scanl :: forall b a. (b -> a -> b) -> b -> [a] -> [b]
          scanr :: forall a b. (a -> b -> b) -> b -> [a] -> [b]
          unzip :: forall a b. [(a, b)] -> ([a], [b])
 +        zip :: forall a b. [a] -> [b] -> [(a, b)]
          (^^) :: forall a b. (Fractional a, Integral b) => a -> b -> a
          ceiling :: forall a b. (RealFrac a, Integral b) => a -> b
          floor :: forall a b. (RealFrac a, Integral b) => a -> b
          properFraction :: forall a b.
                            (RealFrac a, Integral b) =>
                            a -> (b, a)
 +        realToFrac :: forall a b. (Real a, Fractional b) => a -> b
          round :: forall a b. (RealFrac a, Integral b) => a -> b
          truncate :: forall a b. (RealFrac a, Integral b) => a -> b
 -        seq :: forall a b. a -> b -> b
 -        (,,) :: forall a b c. a -> b -> c -> (a, b, c)
 +        (,) :: forall a b. a -> b -> (a, b)
          ($!) :: forall a b. (a -> b) -> a -> b
          (.) :: forall b c a. (b -> c) -> (a -> b) -> a -> c
          either :: forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
@@ -202,11 +200,13 @@ holes.hs:11:15: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          unzip3 :: forall a b c. [(a, b, c)] -> ([a], [b], [c])
          zip3 :: forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
          zipWith :: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
 +        seq :: forall a b. a -> b -> b
 +        (,,) :: forall a b c. a -> b -> c -> (a, b, c)
          ($) :: forall a b. (a -> b) -> a -> b
 -        (,,,) :: forall a b c d. a -> b -> c -> d -> (a, b, c, d)
          flip :: forall a b c. (a -> b -> c) -> b -> a -> c
          zipWith3 :: forall a b c d.
                      (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
 +        (,,,) :: forall a b c d. a -> b -> c -> d -> (a, b, c, d)
          (,,,,) :: forall a b c d e.
                    a -> b -> c -> d -> e -> (a, b, c, d, e)
          (,,,,,) :: forall a b c d e f.

testsuite/tests/typecheck/should_compile/holes2.stderr

+-
  holes2.hs:3:5: warning: [GHC-39999] [-Wdeferred-type-errors (in -Wdefault)]
      • Ambiguous type variable ‘a0’ arising from a use of ‘show’
        prevents the constraint ‘(Show a0)’ from being solved.
@@ -8,7 +7,7 @@ holes2.hs:3:5: warning: [GHC-39999] [-Wdeferred-type-errors (in -Wdefault)]
            -- Defined in ‘GHC.Internal.Data.Either’
          instance Show Ordering -- Defined in ‘GHC.Internal.Show’
          ...plus 26 others
 -        ...plus 48 instances involving out-of-scope types
 +        ...plus 49 instances involving out-of-scope types
          (use -fprint-potential-instances to see them all)
      • In the expression: show _
        In an equation for ‘f’: f = show _
@@ -23,10 +22,11 @@ holes2.hs:3:10: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
        Valid hole fits include
          f :: String
          otherwise :: Bool
 -        False :: Bool
 -        True :: Bool
 -        LT :: Ordering
          EQ :: Ordering
          GT :: Ordering
 +        LT :: Ordering
          () :: ()
 +        False :: Bool
 +        True :: Bool
          pi :: forall a. Floating a => a
++

testsuite/tests/typecheck/should_compile/holes3.stderr

@@ -43,18 +43,12 @@ holes3.hs:11:15: error: [GHC-88464]
          y :: [a] (bound at holes3.hs:11:3)
          z :: [a] -> [a] (bound at holes3.hs:11:1)
        Valid hole fits include
 -        y :: [a]
 -        z :: [a] -> [a]
          g :: Int -> Char
          h :: [Char]
 +        y :: [a]
 +        z :: [a] -> [a]
          f :: forall {p}. p
          otherwise :: Bool
 -        False :: Bool
 -        True :: Bool
 -        LT :: Ordering
 -        EQ :: Ordering
 -        GT :: Ordering
 -        () :: ()
          (&&) :: Bool -> Bool -> Bool
          not :: Bool -> Bool
          (||) :: Bool -> Bool -> Bool
@@ -77,22 +71,48 @@ holes3.hs:11:15: error: [GHC-88464]
          putStrLn :: String -> IO ()
          readFile :: FilePath -> IO String
          writeFile :: FilePath -> String -> IO ()
 +        EQ :: Ordering
 +        GT :: Ordering
 +        LT :: Ordering
 +        () :: ()
 +        False :: Bool
 +        True :: Bool
          (++) :: forall a. [a] -> [a] -> [a]
 -        filter :: forall a. (a -> Bool) -> [a] -> [a]
 -        fromInteger :: forall a. Num a => Integer -> a
 -        (-) :: forall a. Num a => a -> a -> a
 -        fromRational :: forall a. Fractional a => Rational -> a
 -        negate :: forall a. Num a => a -> a
 -        fromIntegral :: forall a b. (Integral a, Num b) => a -> b
 -        toInteger :: forall a. Integral a => a -> Integer
 -        toRational :: forall a. Real a => a -> Rational
 -        (:) :: forall a. a -> [a] -> [a]
 -        Nothing :: forall a. Maybe a
 -        Just :: forall a. a -> Maybe a
 -        [] :: forall a. [a]
          asTypeOf :: forall a. a -> a -> a
          id :: forall a. a -> a
          until :: forall a. (a -> Bool) -> (a -> a) -> a -> a
 +        (**) :: forall a. Floating a => a -> a -> a
 +        acos :: forall a. Floating a => a -> a
 +        acosh :: forall a. Floating a => a -> a
 +        asin :: forall a. Floating a => a -> a
 +        asinh :: forall a. Floating a => a -> a
 +        atan :: forall a. Floating a => a -> a
 +        atan2 :: forall a. RealFloat a => a -> a -> a
 +        atanh :: forall a. Floating a => a -> a
 +        cos :: forall a. Floating a => a -> a
 +        cosh :: forall a. Floating a => a -> a
 +        decodeFloat :: forall a. RealFloat a => a -> (Integer, Int)
 +        encodeFloat :: forall a. RealFloat a => Integer -> Int -> a
 +        exp :: forall a. Floating a => a -> a
 +        exponent :: forall a. RealFloat a => a -> Int
 +        floatDigits :: forall a. RealFloat a => a -> Int
 +        floatRadix :: forall a. RealFloat a => a -> Integer
 +        floatRange :: forall a. RealFloat a => a -> (Int, Int)
 +        isDenormalized :: forall a. RealFloat a => a -> Bool
 +        isIEEE :: forall a. RealFloat a => a -> Bool
 +        isInfinite :: forall a. RealFloat a => a -> Bool
 +        isNaN :: forall a. RealFloat a => a -> Bool
 +        isNegativeZero :: forall a. RealFloat a => a -> Bool
 +        log :: forall a. Floating a => a -> a
 +        logBase :: forall a. Floating a => a -> a -> a
 +        pi :: forall a. Floating a => a
 +        scaleFloat :: forall a. RealFloat a => Int -> a -> a
 +        significand :: forall a. RealFloat a => a -> a
 +        sin :: forall a. Floating a => a -> a
 +        sinh :: forall a. Floating a => a -> a
 +        sqrt :: forall a. Floating a => a -> a
 +        tan :: forall a. Floating a => a -> a
 +        tanh :: forall a. Floating a => a -> a
          ioError :: forall a.
                     GHC.Internal.Stack.Types.HasCallStack =>
                     IOError -> IO a
@@ -105,6 +125,7 @@ holes3.hs:11:15: error: [GHC-88464]
                   [a] -> [a]
          drop :: forall a. Int -> [a] -> [a]
          dropWhile :: forall a. (a -> Bool) -> [a] -> [a]
 +        filter :: forall a. (a -> Bool) -> [a] -> [a]
          head :: forall a. GHC.Internal.Stack.Types.HasCallStack => [a] -> a
          init :: forall a.
                  GHC.Internal.Stack.Types.HasCallStack =>
@@ -123,80 +144,57 @@ holes3.hs:11:15: error: [GHC-88464]
                  [a] -> [a]
          take :: forall a. Int -> [a] -> [a]
          takeWhile :: forall a. (a -> Bool) -> [a] -> [a]
 -        subtract :: forall a. Num a => a -> a -> a
 -        readParen :: forall a. Bool -> ReadS a -> ReadS a
 -        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
 -        even :: forall a. Integral a => a -> Bool
 -        gcd :: forall a. Integral a => a -> a -> a
 -        lcm :: forall a. Integral a => a -> a -> a
 -        odd :: forall a. Integral a => a -> Bool
 -        (**) :: forall a. Floating a => a -> a -> a
 -        acos :: forall a. Floating a => a -> a
 -        acosh :: forall a. Floating a => a -> a
 -        asin :: forall a. Floating a => a -> a
 -        asinh :: forall a. Floating a => a -> a
 -        atan :: forall a. Floating a => a -> a
 -        atanh :: forall a. Floating a => a -> a
 -        cos :: forall a. Floating a => a -> a
 -        cosh :: forall a. Floating a => a -> a
 -        exp :: forall a. Floating a => a -> a
 -        log :: forall a. Floating a => a -> a
 -        logBase :: forall a. Floating a => a -> a -> a
 -        pi :: forall a. Floating a => a
 -        sin :: forall a. Floating a => a -> a
 -        sinh :: forall a. Floating a => a -> a
 -        sqrt :: forall a. Floating a => a -> a
 -        tan :: forall a. Floating a => a -> a
 -        tanh :: forall a. Floating a => a -> a
 -        atan2 :: forall a. RealFloat a => a -> a -> a
 -        decodeFloat :: forall a. RealFloat a => a -> (Integer, Int)
 -        encodeFloat :: forall a. RealFloat a => Integer -> Int -> a
 -        exponent :: forall a. RealFloat a => a -> Int
 -        floatDigits :: forall a. RealFloat a => a -> Int
 -        floatRadix :: forall a. RealFloat a => a -> Integer
 -        floatRange :: forall a. RealFloat a => a -> (Int, Int)
 -        isDenormalized :: forall a. RealFloat a => a -> Bool
 -        isIEEE :: forall a. RealFloat a => a -> Bool
 -        isInfinite :: forall a. RealFloat a => a -> Bool
 -        isNaN :: forall a. RealFloat a => a -> Bool
 -        isNegativeZero :: forall a. RealFloat a => a -> Bool
 -        scaleFloat :: forall a. RealFloat a => Int -> a -> a
 -        significand :: forall a. RealFloat a => a -> a
          (*) :: forall a. Num a => a -> a -> a
          (+) :: forall a. Num a => a -> a -> a
 +        (-) :: forall a. Num a => a -> a -> a
          abs :: forall a. Num a => a -> a
 +        fromInteger :: forall a. Num a => Integer -> a
 +        negate :: forall a. Num a => a -> a
          signum :: forall a. Num a => a -> a
 +        subtract :: forall a. Num a => a -> a -> a
 +        readParen :: forall a. Bool -> ReadS a -> ReadS a
          (/) :: forall a. Fractional a => a -> a -> a
 -        recip :: forall a. Fractional a => a -> a
 +        (^) :: forall a b. (Num a, Integral b) => a -> b -> a
          div :: forall a. Integral a => a -> a -> a
          divMod :: forall a. Integral a => a -> a -> (a, a)
 +        even :: forall a. Integral a => a -> Bool
 +        fromIntegral :: forall a b. (Integral a, Num b) => a -> b
 +        fromRational :: forall a. Fractional a => Rational -> a
 +        gcd :: forall a. Integral a => a -> a -> a
 +        lcm :: forall a. Integral a => a -> a -> a
          mod :: forall a. Integral a => a -> a -> a
 +        odd :: forall a. Integral a => a -> Bool
          quot :: forall a. Integral a => a -> a -> a
          quotRem :: forall a. Integral a => a -> a -> (a, a)
 +        recip :: forall a. Fractional a => a -> a
          rem :: forall a. Integral a => a -> a -> a
 -        zip :: forall a b. [a] -> [b] -> [(a, b)]
 +        toInteger :: forall a. Integral a => a -> Integer
 +        toRational :: forall a. Real a => a -> Rational
 +        Just :: forall a. a -> Maybe a
 +        Nothing :: forall a. Maybe a
 +        (:) :: forall a. a -> [a] -> [a]
 +        [] :: forall a. [a]
 +        const :: forall a b. a -> b -> a
          map :: forall a b. (a -> b) -> [a] -> [b]
 -        realToFrac :: forall a b. (Real a, Fractional b) => a -> b
          Left :: forall a b. a -> Either a b
          Right :: forall a b. b -> Either a b
 -        (,) :: forall a b. a -> b -> (a, b)
 -        const :: forall a b. a -> b -> a
          maybe :: forall b a. b -> (a -> b) -> Maybe a -> b
          fst :: forall a b. (a, b) -> a
          snd :: forall a b. (a, b) -> b
          scanl :: forall b a. (b -> a -> b) -> b -> [a] -> [b]
          scanr :: forall a b. (a -> b -> b) -> b -> [a] -> [b]
          unzip :: forall a b. [(a, b)] -> ([a], [b])
 +        zip :: forall a b. [a] -> [b] -> [(a, b)]
          (^^) :: forall a b. (Fractional a, Integral b) => a -> b -> a
          ceiling :: forall a b. (RealFrac a, Integral b) => a -> b
          floor :: forall a b. (RealFrac a, Integral b) => a -> b
          properFraction :: forall a b.
                            (RealFrac a, Integral b) =>
                            a -> (b, a)
 +        realToFrac :: forall a b. (Real a, Fractional b) => a -> b
          round :: forall a b. (RealFrac a, Integral b) => a -> b
          truncate :: forall a b. (RealFrac a, Integral b) => a -> b
 -        seq :: forall a b. a -> b -> b
 -        (,,) :: forall a b c. a -> b -> c -> (a, b, c)
 +        (,) :: forall a b. a -> b -> (a, b)
          ($!) :: forall a b. (a -> b) -> a -> b
          (.) :: forall b c a. (b -> c) -> (a -> b) -> a -> c
          either :: forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
@@ -205,11 +203,13 @@ holes3.hs:11:15: error: [GHC-88464]
          unzip3 :: forall a b c. [(a, b, c)] -> ([a], [b], [c])
          zip3 :: forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
          zipWith :: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
 +        seq :: forall a b. a -> b -> b
 +        (,,) :: forall a b c. a -> b -> c -> (a, b, c)
          ($) :: forall a b. (a -> b) -> a -> b
 -        (,,,) :: forall a b c d. a -> b -> c -> d -> (a, b, c, d)
          flip :: forall a b c. (a -> b -> c) -> b -> a -> c
          zipWith3 :: forall a b c d.
                      (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
 +        (,,,) :: forall a b c d. a -> b -> c -> d -> (a, b, c, d)
          (,,,,) :: forall a b c d e.
                    a -> b -> c -> d -> e -> (a, b, c, d, e)
          (,,,,,) :: forall a b c d e f.

testsuite/tests/typecheck/should_compile/refinement_hole_fits.stderr

@@ -4,8 +4,8 @@ refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • Relevant bindings include
          f :: [Integer] -> Integer (bound at refinement_hole_fits.hs:4:1)
        Valid hole fits include
 -        f :: [Integer] -> Integer (bound at refinement_hole_fits.hs:4:1)
          g :: [Integer] -> Integer (bound at refinement_hole_fits.hs:7:1)
 +        f :: [Integer] -> Integer (bound at refinement_hole_fits.hs:4:1)
          head :: forall a. GHC.Internal.Stack.Types.HasCallStack => [a] -> a
            with head @Integer
            (imported from ‘Prelude’
@@ -15,19 +15,19 @@ refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.List’))
          maximum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
 -          with maximum @[] @Integer
 +          with maximum @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Data.Foldable’))
          minimum :: forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
 -          with minimum @[] @Integer
 +          with minimum @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Data.Foldable’))
          product :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
 -          with product @[] @Integer
 +          with product @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Data.Foldable’))
          sum :: forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
 -          with sum @[] @Integer
 +          with sum @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Data.Foldable’))
        Valid refinement hole fits include
@@ -35,35 +35,35 @@ refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            where foldl1 :: forall (t :: * -> *) a.
                            Foldable t =>
                            (a -> a -> a) -> t a -> a
 -          with foldl1 @[] @Integer
 +          with foldl1 @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Data.Foldable’))
          foldr1 (_ :: Integer -> Integer -> Integer)
            where foldr1 :: forall (t :: * -> *) a.
                            Foldable t =>
                            (a -> a -> a) -> t a -> a
 -          with foldr1 @[] @Integer
 +          with foldr1 @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Data.Foldable’))
          foldl (_ :: Integer -> Integer -> Integer) (_ :: Integer)
            where foldl :: forall (t :: * -> *) b a.
                           Foldable t =>
                           (b -> a -> b) -> b -> t a -> b
 -          with foldl @[] @Integer @Integer
 +          with foldl @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Data.Foldable’))
          foldl' (_ :: Integer -> Integer -> Integer) (_ :: Integer)
            where foldl' :: forall (t :: * -> *) b a.
                            Foldable t =>
                            (b -> a -> b) -> b -> t a -> b
 -          with foldl' @[] @Integer @Integer
 +          with foldl' @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Data.Foldable’))
          foldr (_ :: Integer -> Integer -> Integer) (_ :: Integer)
            where foldr :: forall (t :: * -> *) a b.
                           Foldable t =>
                           (a -> b -> b) -> b -> t a -> b
 -          with foldr @[] @Integer @Integer
 +          with foldr @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Data.Foldable’))
          const (_ :: Integer)
@@ -84,14 +84,14 @@ refinement_hole_fits.hs:4:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with ($!) @GHC.Internal.Types.LiftedRep @[Integer] @Integer
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        return (_ :: Integer)
 -          where return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @((->) [Integer]) @Integer
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Base’))
          pure (_ :: Integer)
            where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @((->) [Integer]) @Integer
 +          with pure @((->) [Integer])
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Base’))
 +        return (_ :: Integer)
 +          where return :: forall (m :: * -> *) a. Monad m => a -> m a
 +          with return @((->) [Integer])
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
          j (_ :: [Integer] -> Integer)
@@ -141,12 +141,12 @@ refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with const @Integer @[Integer]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @((->) [Integer]) @Integer
 +        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +          with pure @((->) [Integer])
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @((->) [Integer]) @Integer
 +        return :: forall (m :: * -> *) a. Monad m => a -> m a
 +          with return @((->) [Integer])
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
        Valid refinement hole fits include
@@ -154,21 +154,21 @@ refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            where foldl :: forall (t :: * -> *) b a.
                           Foldable t =>
                           (b -> a -> b) -> b -> t a -> b
 -          with foldl @[] @Integer @Integer
 +          with foldl @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Data.Foldable’))
          foldl' (_ :: Integer -> Integer -> Integer)
            where foldl' :: forall (t :: * -> *) b a.
                            Foldable t =>
                            (b -> a -> b) -> b -> t a -> b
 -          with foldl' @[] @Integer @Integer
 +          with foldl' @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Data.Foldable’))
          foldr (_ :: Integer -> Integer -> Integer)
            where foldr :: forall (t :: * -> *) a b.
                           Foldable t =>
                           (a -> b -> b) -> b -> t a -> b
 -          with foldr @[] @Integer @Integer
 +          with foldr @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Data.Foldable’))
          curry (_ :: (Integer, [Integer]) -> Integer)
@@ -204,14 +204,14 @@ refinement_hole_fits.hs:7:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
                      @([Integer] -> Integer)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
 -        return (_ :: [Integer] -> Integer)
 -          where return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @((->) Integer) @([Integer] -> Integer)
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Base’))
          pure (_ :: [Integer] -> Integer)
            where pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @((->) Integer) @([Integer] -> Integer)
 +          with pure @((->) Integer)
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Base’))
 +        return (_ :: [Integer] -> Integer)
 +          where return :: forall (m :: * -> *) a. Monad m => a -> m a
 +          with return @((->) Integer)
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
          j (_ :: Integer -> [Integer] -> Integer)

testsuite/tests/typecheck/should_compile/subsumption_sort_hole_fits.stderr

@@ -26,15 +26,15 @@ subsumption_sort_hole_fits.hs:2:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdef
          fail :: forall (m :: * -> *) a.
                  (MonadFail m, GHC.Internal.Stack.Types.HasCallStack) =>
                  String -> m a
 -          with fail @[] @String
 +          with fail @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Control.Monad.Fail’))
          return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @[] @String
 +          with return @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))
          pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @[] @String
 +          with pure @[]
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Base’))

testsuite/tests/typecheck/should_compile/type_in_type_hole_fits.stderr

+-
  type_in_type_hole_fits.hs:79:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • Found hole:
          _a :: [Integer] -> Sorted (O (NLogN 2 0)) (O N) True Integer
@@ -14,18 +13,18 @@ type_in_type_hole_fits.hs:79:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefau
                    [a] -> Sorted cpu mem stable a
            with Sorted @(O (NLogN 2 0)) @(O N) @True @Integer
            (defined at type_in_type_hole_fits.hs:54:18)
 -        mergeSort :: forall a (n :: AsympPoly) (m :: AsympPoly)
 -                            (s :: Bool).
 -                     (Ord a, n >=. O (N *. LogN), m >=. O N, IsStable s) =>
 -                     [a] -> Sorted n m s a
 -          with mergeSort @Integer @(O (NLogN 2 0)) @(O N) @True
 -          (defined at type_in_type_hole_fits.hs:61:1)
          insertionSort :: forall a (n :: AsympPoly) (m :: AsympPoly)
                                  (s :: Bool).
                           (Ord a, n >=. O (N ^. 2), m >=. O One, IsStable s) =>
                           [a] -> Sorted n m s a
            with insertionSort @Integer @(O (NLogN 2 0)) @(O N) @True
            (defined at type_in_type_hole_fits.hs:65:1)
 +        mergeSort :: forall a (n :: AsympPoly) (m :: AsympPoly)
 +                            (s :: Bool).
 +                     (Ord a, n >=. O (N *. LogN), m >=. O N, IsStable s) =>
 +                     [a] -> Sorted n m s a
 +          with mergeSort @Integer @(O (NLogN 2 0)) @(O N) @True
 +          (defined at type_in_type_hole_fits.hs:61:1)
  type_in_type_hole_fits.hs:82:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • Found hole:
@@ -37,16 +36,16 @@ type_in_type_hole_fits.hs:82:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefau
          mySortB :: Sorted (O (N *. LogN)) (O N) False Integer
            (bound at type_in_type_hole_fits.hs:82:1)
        Valid hole fits include
 -        quickSort :: forall a (n :: AsympPoly) (m :: AsympPoly).
 -                     (Ord a, n >=. O (N *. LogN), m >=. O N) =>
 -                     [a] -> Sorted n m False a
 -          with quickSort @Integer @(O (NLogN 1 1)) @(O N)
 -          (defined at type_in_type_hole_fits.hs:71:1)
          heapSort :: forall a (n :: AsympPoly) (m :: AsympPoly).
                      (Ord a, n >=. O (N *. LogN), m >=. O One) =>
                      [a] -> Sorted n m False a
            with heapSort @Integer @(O (NLogN 1 1)) @(O N)
            (defined at type_in_type_hole_fits.hs:74:1)
 +        quickSort :: forall a (n :: AsympPoly) (m :: AsympPoly).
 +                     (Ord a, n >=. O (N *. LogN), m >=. O N) =>
 +                     [a] -> Sorted n m False a
 +          with quickSort @Integer @(O (NLogN 1 1)) @(O N)
 +          (defined at type_in_type_hole_fits.hs:71:1)
          Sorted :: forall (cpu :: AsympPoly) (mem :: AsympPoly)
                           (stable :: Bool) a.
                    [a] -> Sorted cpu mem stable a
@@ -79,3 +78,4 @@ type_in_type_hole_fits.hs:85:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefau
                    [a] -> Sorted cpu mem stable a
            with Sorted @(O (NLogN 1 1)) @(O One) @False @Integer
            (defined at type_in_type_hole_fits.hs:54:18)
++

testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr

@@ -25,15 +25,15 @@ valid_hole_fits.hs:17:17: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          x :: Int (bound at valid_hole_fits.hs:16:12)
          c :: Int -> IO Int (bound at valid_hole_fits.hs:16:1)
        Valid hole fits include
 -        c :: Int -> IO Int (bound at valid_hole_fits.hs:16:1)
          a :: Int -> IO Int (bound at valid_hole_fits.hs:12:1)
          b :: Int -> IO Int (bound at valid_hole_fits.hs:14:1)
 -        return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @IO @Int
 +        c :: Int -> IO Int (bound at valid_hole_fits.hs:16:1)
 +        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +          with pure @IO
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Base’))
 -        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @IO @Int
 +        return :: forall (m :: * -> *) a. Monad m => a -> m a
 +          with return @IO
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Base’))
@@ -82,12 +82,12 @@ valid_hole_fits.hs:27:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with Just @Integer
            (imported from ‘Data.Maybe’ at valid_hole_fits.hs:5:1-17
             (and originally defined in ‘GHC.Internal.Maybe’))
 -        return :: forall (m :: * -> *) a. Monad m => a -> m a
 -          with return @Maybe @Integer
 +        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 +          with pure @Maybe
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Base’))
 -        pure :: forall (f :: * -> *) a. Applicative f => a -> f a
 -          with pure @Maybe @Integer
 +        return :: forall (m :: * -> *) a. Monad m => a -> m a
 +          with return @Maybe
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Base’))
@@ -100,28 +100,28 @@ valid_hole_fits.hs:30:10: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • Relevant bindings include
          f :: String (bound at valid_hole_fits.hs:30:1)
        Valid hole fits include
 -        f :: String (bound at valid_hole_fits.hs:30:1)
 -        k :: Maybe Integer (defined at valid_hole_fits.hs:27:1)
          h :: String (bound at valid_hole_fits.hs:34:1)
 +        k :: Maybe Integer (defined at valid_hole_fits.hs:27:1)
 +        f :: String (bound at valid_hole_fits.hs:30:1)
          otherwise :: Bool
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Base’))
 -        False :: Bool
 +        EQ :: Ordering
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Types’))
 -        True :: Bool
 +        GT :: Ordering
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Types’))
          LT :: Ordering
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Types’))
 -        EQ :: Ordering
 +        () :: () (bound at <wired into compiler>)
 +        False :: Bool
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Types’))
 -        GT :: Ordering
 +        True :: Bool
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Types’))
 -        () :: () (bound at <wired into compiler>)
          pi :: forall a. Floating a => a
            with pi @Double
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
@@ -139,22 +139,14 @@ valid_hole_fits.hs:34:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
          not :: Bool -> Bool
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Classes’))
 -        enumFrom :: forall a. Enum a => a -> [a]
 -          with enumFrom @Bool
 -          (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
 -           (and originally defined in ‘GHC.Internal.Enum’))
 -        Just :: forall a. a -> Maybe a
 -          with Just @Bool
 -          (imported from ‘Data.Maybe’ at valid_hole_fits.hs:5:1-17
 -           (and originally defined in ‘GHC.Internal.Maybe’))
          id :: forall a. a -> a
            with id @Bool
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Base’))
 -        repeat :: forall a. a -> [a]
 -          with repeat @Bool
 +        enumFrom :: forall a. Enum a => a -> [a]
 +          with enumFrom @Bool
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
 -           (and originally defined in ‘GHC.Internal.List’))
 +           (and originally defined in ‘GHC.Internal.Enum’))
          fromEnum :: forall a. Enum a => a -> Int
            with fromEnum @Bool
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
@@ -167,10 +159,18 @@ valid_hole_fits.hs:34:11: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with succ @Bool
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Enum’))
 +        repeat :: forall a. a -> [a]
 +          with repeat @Bool
 +          (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
 +           (and originally defined in ‘GHC.Internal.List’))
          show :: forall a. Show a => a -> String
            with show @Bool
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Show’))
 +        Just :: forall a. a -> Maybe a
 +          with Just @Bool
 +          (imported from ‘Data.Maybe’ at valid_hole_fits.hs:5:1-17
 +           (and originally defined in ‘GHC.Internal.Maybe’))
  valid_hole_fits.hs:34:14: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • Found hole: _ :: Bool
@@ -213,7 +213,7 @@ valid_hole_fits.hs:38:10: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with (:) @a
            (bound at <wired into compiler>)
          (<$) :: forall (f :: * -> *) a b. Functor f => a -> f b -> f a
 -          with (<$) @[] @a @a
 +          with (<$) @[]
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Base’))
          seq :: forall a b. a -> b -> b
@@ -243,16 +243,16 @@ valid_hole_fits.hs:41:8: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
            with readIO @()
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.System.IO’))
 -        print :: forall a. Show a => a -> IO ()
 -          with print @String
 -          (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
 -           (and originally defined in ‘GHC.Internal.System.IO’))
          fail :: forall (m :: * -> *) a.
                  (MonadFail m, GHC.Internal.Stack.Types.HasCallStack) =>
                  String -> m a
 -          with fail @IO @()
 +          with fail @IO
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
             (and originally defined in ‘GHC.Internal.Control.Monad.Fail’))
 +        print :: forall a. Show a => a -> IO ()
 +          with print @String
 +          (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40
 +           (and originally defined in ‘GHC.Internal.System.IO’))
          mempty :: forall a. Monoid a => a
            with mempty @(String -> IO ())
            (imported from ‘Prelude’ at valid_hole_fits.hs:3:1-40

testsuite/tests/typecheck/should_compile/valid_hole_fits_interactions.stderr

+-
  valid_hole_fits_interactions.hs:15:5: warning: [GHC-88464] [-Wtyped-holes (in -Wdefault)]
      • Found hole: _ :: SBool True
      • In an equation for ‘f’: f = _
      • Relevant bindings include
          f :: SBool True (bound at valid_hole_fits_interactions.hs:15:1)
        Valid hole fits include
 -        f :: SBool True (bound at valid_hole_fits_interactions.hs:15:1)
          STrue :: SBool True
            (defined at valid_hole_fits_interactions.hs:12:3)
 +        f :: SBool True (bound at valid_hole_fits_interactions.hs:15:1)
++

testsuite/tests/typecheck/should_fail/T14884.stderr

@@ -5,18 +5,18 @@ T14884.hs:4:5: error: [GHC-88464]
        In an equation for ‘x’: x = _ print "abc"
      • Relevant bindings include x :: IO () (bound at T14884.hs:4:1)
        Valid hole fits include
 +        foldMap :: forall (t :: * -> *) m a.
 +                   (Foldable t, Monoid m) =>
 +                   (a -> m) -> t a -> m
 +          with foldMap @[]
 +          (imported from ‘Prelude’
 +           (and originally defined in ‘GHC.Internal.Data.Foldable’))
          mapM_ :: forall (t :: * -> *) (m :: * -> *) a b.
                   (Foldable t, Monad m) =>
                   (a -> m b) -> t a -> m ()
            with mapM_ @[] @IO @Char @()
            (imported from ‘Prelude’
             (and originally defined in ‘GHC.Internal.Data.Foldable’))
 -        foldMap :: forall (t :: * -> *) m a.
 -                   (Foldable t, Monoid m) =>
 -                   (a -> m) -> t a -> m
 -          with foldMap @[] @(IO ()) @Char
 -          (imported from ‘Prelude’
 -           (and originally defined in ‘GHC.Internal.Data.Foldable’))
          id :: forall a. a -> a
            with id @(String -> IO ())
            (imported from ‘Prelude’