[Git][ghc/ghc][wip/hole-refactor] Refactor hole constraints.
Richard Eisenberg
gitlab at gitlab.haskell.org
Sat May 2 20:40:17 UTC 2020
Richard Eisenberg pushed to branch wip/hole-refactor at Glasgow Haskell Compiler / GHC
Commits:
57d2bba3 by Richard Eisenberg at 2020-05-01T16:37:38+00:00
Refactor hole constraints.
Previously, holes (both expression holes / out of scope variables and
partial-type-signature wildcards) were emitted as *constraints* via
the CHoleCan constructor. While this worked fine for error reporting,
there was a fair amount of faff in keeping these constraints in line.
In particular, and unlike other constraints, we could never change
a CHoleCan to become CNonCanonical. In addition:
* the "predicate" of a CHoleCan constraint was really the type
of the hole, which is not a predicate at all
* type-level holes (partial type signature wildcards) carried
evidence, which was never used
* tcNormalise (used in the pattern-match checker) had to create
a hole constraint just to extract it again; it was quite messy
The new approach is to record holes directly in WantedConstraints.
It flows much more nicely now.
Along the way, I did some cleaning up of commentary in
GHC.Tc.Errors.Hole, which I had a hard time understanding.
This was instigated by a future patch that will refactor
the way predicates are handled. The fact that CHoleCan's
"predicate" wasn't really a predicate is incompatible with
that future patch.
No test case, because this is meant to be purely internal.
- - - - -
18 changed files:
- compiler/GHC/HsToCore/PmCheck/Oracle.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Errors/Hole.hs
- compiler/GHC/Tc/Errors/Hole.hs-boot
- compiler/GHC/Tc/Errors/Hole/FitTypes.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Gen/Rule.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Flatten.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Types/Origin.hs
- compiler/GHC/Tc/Utils/Monad.hs
- compiler/GHC/Tc/Utils/TcMType.hs
Changes:
=====================================
compiler/GHC/HsToCore/PmCheck/Oracle.hs
=====================================
@@ -438,7 +438,7 @@ then
newtypes.
(b) dcs is the list of newtype constructors "skipped", every time we normalise
a newtype to its core representation, we keep track of the source data
- constructor. For convenienve, we also track the type we unwrap and the
+ constructor. For convenience, we also track the type we unwrap and the
type of its field. Example: @Down 42@ => @[(Down @Int, Down, Int)]
(c) core_ty is the rewritten type. That is,
pmTopNormaliseType env ty_cs ty = Just (src_ty, dcs, core_ty)
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -285,8 +285,8 @@ important :: SDoc -> Report
important doc = mempty { report_important = [doc] }
-- | Put a doc into the relevant bindings block.
-relevant_bindings :: SDoc -> Report
-relevant_bindings doc = mempty { report_relevant_bindings = [doc] }
+mk_relevant_bindings :: SDoc -> Report
+mk_relevant_bindings doc = mempty { report_relevant_bindings = [doc] }
-- | Put a doc into the valid hole fits block.
valid_hole_fits :: SDoc -> Report
@@ -524,16 +524,29 @@ This only matters in instance declarations..
-}
reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
-reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
+reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics
+ , wc_holes = holes })
= do { traceTc "reportWanteds" (vcat [ text "Simples =" <+> ppr simples
- , text "Suppress =" <+> ppr (cec_suppress ctxt)])
- ; traceTc "rw2" (ppr tidy_cts)
-
- -- First deal with things that are utterly wrong
+ , text "Suppress =" <+> ppr (cec_suppress ctxt)
+ , text "tidy_cts =" <+> ppr tidy_cts
+ , text "tidy_holes = " <+> ppr tidy_holes ])
+
+ -- First, deal with any out-of-scope errors:
+ ; let (out_of_scope, other_holes) = partition isOutOfScopeHole tidy_holes
+ -- don't suppress out-of-scope errors
+ ctxt_for_scope_errs = ctxt { cec_suppress = False }
+ ; (_, no_out_of_scope) <- askNoErrs $
+ reportHoles tidy_cts ctxt_for_scope_errs out_of_scope
+
+ -- Next, deal with things that are utterly wrong
-- Like Int ~ Bool (incl nullary TyCons)
-- or Int ~ t a (AppTy on one side)
-- These /ones/ are not suppressed by the incoming context
- ; let ctxt_for_insols = ctxt { cec_suppress = False }
+ -- (but will be by out-of-scope errors)
+ ; let ctxt_for_insols = ctxt { cec_suppress = not no_out_of_scope }
+ ; reportHoles tidy_cts ctxt_for_insols other_holes
+ -- holes never suppress
+
; (ctxt1, cts1) <- tryReporters ctxt_for_insols report1 tidy_cts
-- Now all the other constraints. We suppress errors here if
@@ -554,7 +567,8 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
-- if there's a *given* insoluble here (= inaccessible code)
where
env = cec_tidy ctxt
- tidy_cts = bagToList (mapBag (tidyCt env) simples)
+ tidy_cts = bagToList (mapBag (tidyCt env) simples)
+ tidy_holes = bagToList (mapBag (tidyHole env) holes)
-- report1: ones that should *not* be suppressed by
-- an insoluble somewhere else in the tree
@@ -562,9 +576,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
-- (see GHC.Tc.Utils.insolubleCt) is caught here, otherwise
-- we might suppress its error message, and proceed on past
-- type checking to get a Lint error later
- report1 = [ ("Out of scope", unblocked is_out_of_scope, True, mkHoleReporter tidy_cts)
- , ("Holes", unblocked is_hole, False, mkHoleReporter tidy_cts)
- , ("custom_error", unblocked is_user_type_error, True, mkUserTypeErrorReporter)
+ report1 = [ ("custom_error", unblocked is_user_type_error, True, mkUserTypeErrorReporter)
, given_eq_spec
, ("insoluble2", unblocked utterly_wrong, True, mkGroupReporter mkEqErr)
@@ -593,8 +605,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
unblocked checker ct pred = checker ct pred
-- rigid_nom_eq, rigid_nom_tv_eq,
- is_hole, is_dict,
- is_equality, is_ip, is_irred :: Ct -> Pred -> Bool
+ is_dict, is_equality, is_ip, is_irred :: Ct -> Pred -> Bool
is_given_eq ct pred
| EqPred {} <- pred = arisesFromGivens ct
@@ -617,9 +628,6 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1)
non_tv_eq _ _ = False
- is_out_of_scope ct _ = isOutOfScopeCt ct
- is_hole ct _ = isHoleCt ct
-
is_user_type_error ct _ = isUserTypeErrorCt ct
is_homo_equality _ (EqPred _ ty1 ty2) = tcTypeKind ty1 `tcEqType` tcTypeKind ty2
@@ -705,12 +713,12 @@ mkSkolReporter ctxt cts
| eq_lhs_type ct1 ct2 = True
| otherwise = False
-mkHoleReporter :: [Ct] -> Reporter
--- Reports errors one at a time
-mkHoleReporter tidy_simples ctxt
- = mapM_ $ \ct -> do { err <- mkHoleError tidy_simples ctxt ct
- ; maybeReportHoleError ctxt ct err
- ; maybeAddDeferredHoleBinding ctxt err ct }
+reportHoles :: [Ct] -- other (tidied) constraints
+ -> ReportErrCtxt -> [Hole] -> TcM ()
+reportHoles tidy_cts ctxt
+ = mapM_ $ \hole -> do { err <- mkHoleError tidy_cts ctxt hole
+ ; maybeReportHoleError ctxt hole err
+ ; maybeAddDeferredHoleBinding ctxt err hole }
mkUserTypeErrorReporter :: Reporter
mkUserTypeErrorReporter ctxt
@@ -742,7 +750,7 @@ mkGivenErrorReporter ctxt cts
inaccessible_msg = hang (text "Inaccessible code in")
2 (ppr (ic_info implic))
report = important inaccessible_msg `mappend`
- relevant_bindings binds_msg
+ mk_relevant_bindings binds_msg
; err <- mkEqErr_help dflags ctxt report ct'
Nothing ty1 ty2
@@ -843,15 +851,27 @@ suppressGroup mk_err ctxt cts
; traceTc "Suppressing errors for" (ppr cts)
; mapM_ (addDeferredBinding ctxt err) cts }
-maybeReportHoleError :: ReportErrCtxt -> Ct -> ErrMsg -> TcM ()
+maybeReportHoleError :: ReportErrCtxt -> Hole -> ErrMsg -> TcM ()
+maybeReportHoleError ctxt hole err
+ | isOutOfScopeHole hole
+ -- Always report an error for out-of-scope variables
+ -- Unless -fdefer-out-of-scope-variables is on,
+ -- in which case the messages are discarded.
+ -- See #12170, #12406
+ = -- If deferring, report a warning only if -Wout-of-scope-variables is on
+ case cec_out_of_scope_holes ctxt of
+ HoleError -> reportError err
+ HoleWarn ->
+ reportWarning (Reason Opt_WarnDeferredOutOfScopeVariables) err
+ HoleDefer -> return ()
+
-- Unlike maybeReportError, these "hole" errors are
-- /not/ suppressed by cec_suppress. We want to see them!
-maybeReportHoleError ctxt ct err
+maybeReportHoleError ctxt (Hole { hole_sort = TypeHole }) err
-- When -XPartialTypeSignatures is on, warnings (instead of errors) are
-- generated for holes in partial type signatures.
-- Unless -fwarn-partial-type-signatures is not on,
-- in which case the messages are discarded.
- | isTypeHoleCt ct
= -- For partial type signatures, generate warnings only, and do that
-- only if -fwarn-partial-type-signatures is on
case cec_type_holes ctxt of
@@ -859,22 +879,12 @@ maybeReportHoleError ctxt ct err
HoleWarn -> reportWarning (Reason Opt_WarnPartialTypeSignatures) err
HoleDefer -> return ()
- -- Always report an error for out-of-scope variables
- -- Unless -fdefer-out-of-scope-variables is on,
- -- in which case the messages are discarded.
- -- See #12170, #12406
- | isOutOfScopeCt ct
- = -- If deferring, report a warning only if -Wout-of-scope-variables is on
- case cec_out_of_scope_holes ctxt of
- HoleError -> reportError err
- HoleWarn ->
- reportWarning (Reason Opt_WarnDeferredOutOfScopeVariables) err
- HoleDefer -> return ()
-
+maybeReportHoleError ctxt hole@(Hole { hole_sort = ExprHole _ }) err
-- Otherwise this is a typed hole in an expression,
- -- but not for an out-of-scope variable
- | otherwise
+ -- but not for an out-of-scope variable (because that goes through a
+ -- different function)
= -- If deferring, report a warning only if -Wtyped-holes is on
+ ASSERT( not (isOutOfScopeHole hole) )
case cec_expr_holes ctxt of
HoleError -> reportError err
HoleWarn -> reportWarning (Reason Opt_WarnTypedHoles) err
@@ -899,10 +909,7 @@ addDeferredBinding ctxt err ct
, CtWanted { ctev_pred = pred, ctev_dest = dest } <- ctEvidence ct
-- Only add deferred bindings for Wanted constraints
= do { dflags <- getDynFlags
- ; let err_msg = pprLocErrMsg err
- err_fs = mkFastString $ showSDoc dflags $
- err_msg $$ text "(deferred type error)"
- err_tm = evDelayedError pred err_fs
+ ; let err_tm = mkErrorTerm dflags pred err
ev_binds_var = cec_binds ctxt
; case dest of
@@ -917,11 +924,27 @@ addDeferredBinding ctxt err ct
| otherwise -- Do not set any evidence for Given/Derived
= return ()
-maybeAddDeferredHoleBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
-maybeAddDeferredHoleBinding ctxt err ct
- | isExprHoleCt ct
- = addDeferredBinding ctxt err ct -- Only add bindings for holes in expressions
- | otherwise -- not for holes in partial type signatures
+mkErrorTerm :: DynFlags -> Type -- of the error term
+ -> ErrMsg -> EvTerm
+mkErrorTerm dflags ty err = evDelayedError ty err_fs
+ where
+ err_msg = pprLocErrMsg err
+ err_fs = mkFastString $ showSDoc dflags $
+ err_msg $$ text "(deferred type error)"
+maybeAddDeferredHoleBinding :: ReportErrCtxt -> ErrMsg -> Hole -> TcM ()
+maybeAddDeferredHoleBinding ctxt err (Hole { hole_sort = ExprHole ev_id })
+-- Only add bindings for holes in expressions
+-- not for holes in partial type signatures
+-- cf. addDeferredBinding
+ | deferringAnyBindings ctxt
+ = do { dflags <- getDynFlags
+ ; let err_tm = mkErrorTerm dflags (idType ev_id) err
+ -- NB: idType ev_id, not hole_ty. hole_ty might be rewritten.
+ -- See Note [Holes] in GHC.Tc.Types.Constraint
+ ; addTcEvBind (cec_binds ctxt) $ mkWantedEvBind ev_id err_tm }
+ | otherwise
+ = return ()
+maybeAddDeferredHoleBinding _ _ (Hole { hole_sort = TypeHole })
= return ()
tryReporters :: ReportErrCtxt -> [ReporterSpec] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
@@ -961,7 +984,6 @@ tryReporter ctxt (str, keep_me, suppress_after, reporter) cts
where
(yeses, nos) = partition (\ct -> keep_me ct (classifyPredType (ctPred ct))) cts
-
pprArising :: CtOrigin -> SDoc
-- Used for the main, top-level error message
-- We've done special processing for TypeEq, KindEq, Given
@@ -1104,15 +1126,16 @@ mkIrredErr ctxt cts
; let orig = ctOrigin ct1
msg = couldNotDeduce (getUserGivens ctxt) (map ctPred cts, orig)
; mkErrorMsgFromCt ctxt ct1 $
- important msg `mappend` relevant_bindings binds_msg }
+ important msg `mappend` mk_relevant_bindings binds_msg }
where
(ct1:_) = cts
----------------
-mkHoleError :: [Ct] -> ReportErrCtxt -> Ct -> TcM ErrMsg
-mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_occ = occ, cc_hole = hole_sort })
- | isOutOfScopeCt ct -- Out of scope variables, like 'a', where 'a' isn't bound
- -- Suggest possible in-scope variables in the message
+mkHoleError :: [Ct] -> ReportErrCtxt -> Hole -> TcM ErrMsg
+mkHoleError _tidy_simples _ctxt hole@(Hole { hole_occ = occ
+ , hole_ty = hole_ty
+ , hole_loc = ct_loc })
+ | isOutOfScopeHole hole
= do { dflags <- getDynFlags
; rdr_env <- getGlobalRdrEnv
; imp_info <- getImports
@@ -1122,48 +1145,52 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_occ = occ, cc_hole = hole_sort }
errDoc [out_of_scope_msg] []
[unknownNameSuggestions dflags hpt curr_mod rdr_env
(tcl_rdr lcl_env) imp_info (mkRdrUnqual occ)] }
+ where
+ herald | isDataOcc occ = text "Data constructor not in scope:"
+ | otherwise = text "Variable not in scope:"
- | otherwise -- Explicit holes, like "_" or "_f"
- = do { (ctxt, binds_msg, ct) <- relevantBindings False ctxt ct
+ out_of_scope_msg -- Print v :: ty only if the type has structure
+ | boring_type = hang herald 2 (ppr occ)
+ | otherwise = hang herald 2 (pp_occ_with_type occ hole_ty)
+
+ lcl_env = ctLocEnv ct_loc
+ boring_type = isTyVarTy hole_ty
+
+ -- general case: not an out-of-scope error
+mkHoleError tidy_simples ctxt hole@(Hole { hole_occ = occ
+ , hole_ty = hole_ty
+ , hole_sort = sort
+ , hole_loc = ct_loc })
+ = do { (ctxt, binds_msg)
+ <- relevant_bindings False ctxt lcl_env (tyCoVarsOfType hole_ty)
-- The 'False' means "don't filter the bindings"; see Trac #8191
; show_hole_constraints <- goptM Opt_ShowHoleConstraints
; let constraints_msg
- | isExprHoleCt ct, show_hole_constraints
+ | ExprHole _ <- sort, show_hole_constraints
= givenConstraintsMsg ctxt
| otherwise
= empty
; show_valid_hole_fits <- goptM Opt_ShowValidHoleFits
; (ctxt, sub_msg) <- if show_valid_hole_fits
- then validHoleFits ctxt tidy_simples ct
+ then validHoleFits ctxt tidy_simples hole
else return (ctxt, empty)
- ; mkErrorMsgFromCt ctxt ct $
+ ; mkErrorReport ctxt lcl_env $
important hole_msg `mappend`
- relevant_bindings (binds_msg $$ constraints_msg) `mappend`
+ mk_relevant_bindings (binds_msg $$ constraints_msg) `mappend`
valid_hole_fits sub_msg }
where
- ct_loc = ctLoc ct
lcl_env = ctLocEnv ct_loc
- hole_ty = ctEvPred (ctEvidence ct)
hole_kind = tcTypeKind hole_ty
tyvars = tyCoVarsOfTypeList hole_ty
- boring_type = isTyVarTy hole_ty
-
- out_of_scope_msg -- Print v :: ty only if the type has structure
- | boring_type = hang herald 2 (ppr occ)
- | otherwise = hang herald 2 pp_with_type
- pp_with_type = hang (pprPrefixOcc occ) 2 (dcolon <+> pprType hole_ty)
- herald | isDataOcc occ = text "Data constructor not in scope:"
- | otherwise = text "Variable not in scope:"
-
- hole_msg = case hole_sort of
- ExprHole -> vcat [ hang (text "Found hole:")
- 2 pp_with_type
- , tyvars_msg, expr_hole_hint ]
+ hole_msg = case sort of
+ ExprHole _ -> vcat [ hang (text "Found hole:")
+ 2 (pp_occ_with_type occ hole_ty)
+ , tyvars_msg, expr_hole_hint ]
TypeHole -> vcat [ hang (text "Found type wildcard" <+> quotes (ppr occ))
2 (text "standing for" <+> quotes pp_hole_type_with_kind)
, tyvars_msg, type_hole_hint ]
@@ -1207,21 +1234,22 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_occ = occ, cc_hole = hole_sort }
= ppWhenOption sdocPrintExplicitCoercions $
quotes (ppr tv) <+> text "is a coercion variable"
-mkHoleError _ _ ct = pprPanic "mkHoleError" (ppr ct)
+pp_occ_with_type :: OccName -> Type -> SDoc
+pp_occ_with_type occ hole_ty = hang (pprPrefixOcc occ) 2 (dcolon <+> pprType hole_ty)
-- We unwrap the ReportErrCtxt here, to avoid introducing a loop in module
-- imports
validHoleFits :: ReportErrCtxt -- The context we're in, i.e. the
-- implications and the tidy environment
-> [Ct] -- Unsolved simple constraints
- -> Ct -- The hole constraint.
+ -> Hole -- The hole
-> TcM (ReportErrCtxt, SDoc) -- We return the new context
-- with a possibly updated
-- tidy environment, and
-- the message.
validHoleFits ctxt@(CEC {cec_encl = implics
- , cec_tidy = lcl_env}) simps ct
- = do { (tidy_env, msg) <- findValidHoleFits lcl_env implics simps ct
+ , cec_tidy = lcl_env}) simps hole
+ = do { (tidy_env, msg) <- findValidHoleFits lcl_env implics simps hole
; return (ctxt {cec_tidy = tidy_env}, msg) }
-- See Note [Constraints include ...]
@@ -1255,7 +1283,7 @@ mkIPErr ctxt cts
= couldNotDeduce givens (preds, orig)
; mkErrorMsgFromCt ctxt ct1 $
- important msg `mappend` relevant_bindings binds_msg }
+ important msg `mappend` mk_relevant_bindings binds_msg }
where
(ct1:_) = cts
@@ -1337,7 +1365,7 @@ mkEqErr1 ctxt ct -- Wanted or derived;
; dflags <- getDynFlags
; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct) $$ ppr keep_going)
; let report = mconcat [important wanted_msg, important coercible_msg,
- relevant_bindings binds_msg]
+ mk_relevant_bindings binds_msg]
; if keep_going
then mkEqErr_help dflags ctxt report ct is_oriented ty1 ty2
else mkErrorMsgFromCt ctxt ct report }
@@ -1513,7 +1541,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2
filter isTyVar $
fvVarList $
tyCoFVsOfType ty1 `unionFV` tyCoFVsOfType ty2
- extra3 = relevant_bindings $
+ extra3 = mk_relevant_bindings $
ppWhen (not (null interesting_tyvars)) $
hang (text "Type variable kinds:") 2 $
vcat (map (tyvar_binding . tidyTyCoVarOcc (cec_tidy ctxt))
@@ -2819,27 +2847,45 @@ relevantBindings :: Bool -- True <=> filter by tyvar; False <=> no filtering
-> TcM (ReportErrCtxt, SDoc, Ct)
-- Also returns the zonked and tidied CtOrigin of the constraint
relevantBindings want_filtering ctxt ct
- = do { dflags <- getDynFlags
+ = do { traceTc "relevantBindings" (ppr ct)
; (env1, tidy_orig) <- zonkTidyOrigin (cec_tidy ctxt) (ctLocOrigin loc)
- ; let ct_tvs = tyCoVarsOfCt ct `unionVarSet` extra_tvs
-- For *kind* errors, report the relevant bindings of the
-- enclosing *type* equality, because that's more useful for the programmer
- extra_tvs = case tidy_orig of
+ ; let extra_tvs = case tidy_orig of
KindEqOrigin t1 m_t2 _ _ -> tyCoVarsOfTypes $
t1 : maybeToList m_t2
_ -> emptyVarSet
- ; traceTc "relevantBindings" $
- vcat [ ppr ct
- , pprCtOrigin (ctLocOrigin loc)
- , ppr ct_tvs
+ ct_fvs = tyCoVarsOfCt ct `unionVarSet` extra_tvs
+
+ -- Put a zonked, tidied CtOrigin into the Ct
+ loc' = setCtLocOrigin loc tidy_orig
+ ct' = setCtLoc ct loc'
+ ctxt1 = ctxt { cec_tidy = env1 }
+
+ ; (ctxt2, doc) <- relevant_bindings want_filtering ctxt1 lcl_env ct_fvs
+ ; return (ctxt2, doc, ct') }
+ where
+ loc = ctLoc ct
+ lcl_env = ctLocEnv loc
+
+-- slightly more general version, to work also with holes
+relevant_bindings :: Bool
+ -> ReportErrCtxt
+ -> TcLclEnv
+ -> TyCoVarSet
+ -> TcM (ReportErrCtxt, SDoc)
+relevant_bindings want_filtering ctxt lcl_env ct_tvs
+ = do { dflags <- getDynFlags
+ ; traceTc "relevant_bindings" $
+ vcat [ ppr ct_tvs
, pprWithCommas id [ ppr id <+> dcolon <+> ppr (idType id)
| TcIdBndr id _ <- tcl_bndrs lcl_env ]
, pprWithCommas id
[ ppr id | TcIdBndr_ExpType id _ _ <- tcl_bndrs lcl_env ] ]
; (tidy_env', docs, discards)
- <- go dflags env1 ct_tvs (maxRelevantBinds dflags)
+ <- go dflags (cec_tidy ctxt) (maxRelevantBinds dflags)
emptyVarSet [] False
(removeBindingShadowing $ tcl_bndrs lcl_env)
-- tcl_bndrs has the innermost bindings first,
@@ -2849,17 +2895,10 @@ relevantBindings want_filtering ctxt ct
hang (text "Relevant bindings include")
2 (vcat docs $$ ppWhen discards discardMsg)
- -- Put a zonked, tidied CtOrigin into the Ct
- loc' = setCtLocOrigin loc tidy_orig
- ct' = setCtLoc ct loc'
ctxt' = ctxt { cec_tidy = tidy_env' }
- ; return (ctxt', doc, ct') }
+ ; return (ctxt', doc) }
where
- ev = ctEvidence ct
- loc = ctEvLoc ev
- lcl_env = ctLocEnv loc
-
run_out :: Maybe Int -> Bool
run_out Nothing = False
run_out (Just n) = n <= 0
@@ -2868,14 +2907,14 @@ relevantBindings want_filtering ctxt ct
dec_max = fmap (\n -> n - 1)
- go :: DynFlags -> TidyEnv -> TcTyVarSet -> Maybe Int -> TcTyVarSet -> [SDoc]
+ go :: DynFlags -> TidyEnv -> Maybe Int -> TcTyVarSet -> [SDoc]
-> Bool -- True <=> some filtered out due to lack of fuel
-> [TcBinder]
-> TcM (TidyEnv, [SDoc], Bool) -- The bool says if we filtered any out
-- because of lack of fuel
- go _ tidy_env _ _ _ docs discards []
+ go _ tidy_env _ _ docs discards []
= return (tidy_env, reverse docs, discards)
- go dflags tidy_env ct_tvs n_left tvs_seen docs discards (tc_bndr : tc_bndrs)
+ go dflags tidy_env n_left tvs_seen docs discards (tc_bndr : tc_bndrs)
= case tc_bndr of
TcTvBndr {} -> discard_it
TcIdBndr id top_lvl -> go2 (idName id) (idType id) top_lvl
@@ -2891,7 +2930,7 @@ relevantBindings want_filtering ctxt ct
Nothing -> discard_it -- No info; discard
}
where
- discard_it = go dflags tidy_env ct_tvs n_left tvs_seen docs
+ discard_it = go dflags tidy_env n_left tvs_seen docs
discards tc_bndrs
go2 id_name id_type top_lvl
= do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env id_type
@@ -2916,12 +2955,12 @@ relevantBindings want_filtering ctxt ct
else if run_out n_left && id_tvs `subVarSet` tvs_seen
-- We've run out of n_left fuel and this binding only
-- mentions already-seen type variables, so discard it
- then go dflags tidy_env ct_tvs n_left tvs_seen docs
+ then go dflags tidy_env n_left tvs_seen docs
True -- Record that we have now discarded something
tc_bndrs
-- Keep this binding, decrement fuel
- else go dflags tidy_env' ct_tvs (dec_max n_left) new_seen
+ else go dflags tidy_env' (dec_max n_left) new_seen
(doc:docs) discards tc_bndrs }
=====================================
compiler/GHC/Tc/Errors/Hole.hs
=====================================
@@ -2,17 +2,9 @@
{-# LANGUAGE ExistentialQuantification #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
module GHC.Tc.Errors.Hole
- ( findValidHoleFits, tcFilterHoleFits
- , tcCheckHoleFit, tcSubsumes
- , withoutUnification
- , fromPureHFPlugin
- -- Re-exports for convenience
- , hfIsLcl
- , pprHoleFit, debugHoleFitDispConfig
+ ( findValidHoleFits
-- Re-exported from GHC.Tc.Errors.Hole.FitTypes
- , TypedHole (..), HoleFit (..), HoleFitCandidate (..)
- , CandPlugin, FitPlugin
, HoleFitPlugin (..), HoleFitPluginR (..)
)
where
@@ -121,7 +113,7 @@ The hole in `f` would generate the message:
Valid hole fits are found by checking top level identifiers and local bindings
in scope for whether their type can be instantiated to the the type of the hole.
Additionally, we also need to check whether all relevant constraints are solved
-by choosing an identifier of that type as well, see Note [Relevant Constraints]
+by choosing an identifier of that type as well, see Note [Relevant constraints]
Since checking for subsumption results in the side-effect of type variables
being unified by the simplifier, we need to take care to restore them after
@@ -143,9 +135,13 @@ that the quantified type variables would take if that fit is used, like
If -XTypeApplications is enabled, this can even be copied verbatim as a
replacement for the hole.
-
-Note [Nested implications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Checking hole fits]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+If we have a hole of type hole_ty, we want to know whether a variable
+of type ty is a valid fit for the whole. This is a subsumption check:
+we wish to know whether ty <: hole_ty. But, of course, the check
+must take into account any givens and relevant constraints.
+(See also Note [Relevant constraints]).
For the simplifier to be able to use any givens present in the enclosing
implications to solve relevant constraints, we nest the wanted subsumption
@@ -156,10 +152,7 @@ As an example, let's look at the following code:
f :: Show a => a -> String
f x = show _
-The hole will result in the hole constraint:
-
- [WD] __a1ph {0}:: a0_a1pd[tau:2] (CHoleCan: ExprHole(_))
-
+Suppose the hole is assigned type a0_a1pd[tau:2].
Here the nested implications are just one level deep, namely:
[Implic {
@@ -170,36 +163,25 @@ Here the nested implications are just one level deep, namely:
Given = $dShow_a1pc :: Show a_a1pa[sk:2]
Wanted =
WC {wc_simple =
- [WD] __a1ph {0}:: a_a1pd[tau:2] (CHoleCan: ExprHole(_))
- [WD] $dShow_a1pe {0}:: Show a_a1pd[tau:2] (CDictCan(psc))}
+ [WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CDictCan(psc))}
Binds = EvBindsVar<a1pi>
Needed inner = []
Needed outer = []
the type signature for:
f :: forall a. Show a => a -> String }]
-As we can see, the givens say that the information about the skolem
-`a_a1pa[sk:2]` fulfills the Show constraint.
-
-The simples are:
+As we can see, the givens say that the skolem
+`a_a1pa[sk:2]` fulfills the Show constraint, and that we must prove
+the [W] Show a0_a1pd[tau:2] constraint -- that is, whatever fills the
+hole must have a Show instance.
- [[WD] __a1ph {0}:: a0_a1pd[tau:2] (CHoleCan: ExprHole(_)),
- [WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical)]
-
-I.e. the hole `a0_a1pd[tau:2]` and the constraint that the type of the hole must
-fulfill `Show a0_a1pd[tau:2])`.
-
-So when we run the check, we need to make sure that the
-
- [WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical)
-
-Constraint gets solved. When we now check for whether `x :: a0_a1pd[tau:2]` fits
-the hole in `tcCheckHoleFit`, the call to `tcSubType` will end up writing the
-meta type variable `a0_a1pd[tau:2] := a_a1pa[sk:2]`. By wrapping the wanted
-constraints needed by tcSubType_NC and the relevant constraints (see
-Note [Relevant Constraints] for more details) in the nested implications, we
-can pass the information in the givens along to the simplifier. For our example,
-we end up needing to check whether the following constraints are soluble.
+When we now check whether `x :: a_a1pa[sk:2]` fits the hole in
+`tcCheckHoleFit`, the call to `tcSubType` will end up unifying the meta type
+variable `a0_a1pd[tau:2] := a_a1pa[sk:2]`. By wrapping the wanted constraints
+needed by tcSubType_NC and the relevant constraints (see Note [Relevant
+Constraints] for more details) in the nested implications, we can pass the
+information in the givens along to the simplifier. For our example, we end up
+needing to check whether the following constraints are soluble.
WC {wc_impl =
Implic {
@@ -223,10 +205,12 @@ with a final WC of WC {}, confirming x :: a0_a1pd[tau:2] as a match.
To avoid side-effects on the nested implications, we create a new EvBindsVar so
that any changes to the ev binds during a check remains localised to that check.
-
+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 [Valid refinement hole fits include ...]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When the `-frefinement-level-hole-fits=N` flag is given, we additionally look
for "valid refinement hole fits"", i.e. valid hole fits with up to N
additional holes in them.
@@ -337,10 +321,8 @@ In the free monad example above, this is demonstrated with
be applied to an expression of type `a -> Free f b` in order to match.
If -XScopedTypeVariables is enabled, this hole fit can even be copied verbatim.
-
-Note [Relevant Constraints]
-~~~~~~~~~~~~~~~~~~~
-
+Note [Relevant constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
As highlighted by #14273, we need to check any relevant constraints as well
as checking for subsumption. Relevant constraints are the simple constraints
whose free unification variables are mentioned in the type of the hole.
@@ -351,10 +333,9 @@ as is the case in
f :: String
f = show _
-Where the simples will be :
+Here, the hole is given type a0_a1kv[tau:1]. Then, the emitted constraint is:
- [[WD] __a1kz {0}:: a0_a1kv[tau:1] (CHoleCan: ExprHole(_)),
- [WD] $dShow_a1kw {0}:: Show a0_a1kv[tau:1] (CNonCanonical)]
+ [WD] $dShow_a1kw {0}:: Show a0_a1kv[tau:1] (CNonCanonical)
However, when there are multiple holes, we need to be more careful. As an
example, Let's take a look at the following code:
@@ -362,29 +343,24 @@ example, Let's take a look at the following code:
f :: Show a => a -> String
f x = show (_b (show _a))
-Here there are two holes, `_a` and `_b`, and the simple constraints passed to
+Here there are two holes, `_a` and `_b`. Suppose _a :: a0_a1pd[tau:2] and
+_b :: a1_a1po[tau:2]. Then, the simple constraints passed to
findValidHoleFits are:
- [[WD] _a_a1pi {0}:: String
- -> a0_a1pd[tau:2] (CHoleCan: ExprHole(_b)),
- [WD] _b_a1ps {0}:: a1_a1po[tau:2] (CHoleCan: ExprHole(_a)),
- [WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical),
+ [[WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical),
[WD] $dShow_a1pp {0}:: Show a1_a1po[tau:2] (CNonCanonical)]
-
-Here we have the two hole constraints for `_a` and `_b`, but also additional
-constraints that these holes must fulfill. When we are looking for a match for
-the hole `_a`, we filter the simple constraints to the "Relevant constraints",
-by throwing out all hole constraints and any constraints which do not mention
-a variable mentioned in the type of the hole. For hole `_a`, we will then
-only require that the `$dShow_a1pp` constraint is solved, since that is
-the only non-hole constraint that mentions any free type variables mentioned in
-the hole constraint for `_a`, namely `a_a1pd[tau:2]` , and similarly for the
-hole `_b` we only require that the `$dShow_a1pe` constraint is solved.
+When we are looking for a match for the hole `_a`, we filter the simple
+constraints to the "Relevant constraints", by throwing out any constraints
+which do not mention a variable mentioned in the type of the hole. For hole
+`_a`, we will then only require that the `$dShow_a1pe` constraint is solved,
+since that is the only constraint that mentions any free type variables
+mentioned in the hole constraint for `_a`, namely `a_a1pd[tau:2]`, and
+similarly for the hole `_b` we only require that the `$dShow_a1pe` constraint
+is solved.
Note [Leaking errors]
-~~~~~~~~~~~~~~~~~~~
-
+~~~~~~~~~~~~~~~~~~~~~
When considering candidates, GHC believes that we're checking for validity in
actual source. However, As evidenced by #15321, #15007 and #15202, this can
cause bewildering error messages. The solution here is simple: if a candidate
@@ -393,17 +369,12 @@ is discarded.
-}
-
data HoleFitDispConfig = HFDC { showWrap :: Bool
, showWrapVars :: Bool
, showType :: Bool
, showProv :: Bool
, showMatches :: Bool }
-debugHoleFitDispConfig :: HoleFitDispConfig
-debugHoleFitDispConfig = HFDC True True True False False
-
-
-- We read the various -no-show-*-of-hole-fits flags
-- and set the display config accordingly.
getHoleFitDispConfig :: TcM HoleFitDispConfig
@@ -516,13 +487,12 @@ pprHoleFit (HFDC sWrp sWrpVars sTy sProv sMs) (HoleFit {..}) =
GreHFCand gre -> pprNameProvenance gre
_ -> text "bound at" <+> ppr (getSrcLoc name)
-getLocalBindings :: TidyEnv -> Ct -> TcM [Id]
-getLocalBindings tidy_orig ct
- = do { (env1, _) <- zonkTidyOrigin tidy_orig (ctLocOrigin loc)
+getLocalBindings :: TidyEnv -> CtLoc -> TcM [Id]
+getLocalBindings tidy_orig ct_loc
+ = do { (env1, _) <- zonkTidyOrigin tidy_orig (ctLocOrigin ct_loc)
; go env1 [] (removeBindingShadowing $ tcl_bndrs lcl_env) }
where
- loc = ctEvLoc (ctEvidence ct)
- lcl_env = ctLocEnv loc
+ lcl_env = ctLocEnv ct_loc
go :: TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
go _ sofar [] = return (reverse sofar)
@@ -542,11 +512,13 @@ findValidHoleFits :: TidyEnv -- ^ The tidy_env for zonking
-> [Ct]
-- ^ The unsolved simple constraints in the implication for
-- the hole.
- -> Ct -- ^ The hole constraint itself
+ -> Hole
-> TcM (TidyEnv, SDoc)
-findValidHoleFits tidy_env implics simples ct | isExprHoleCt ct =
+findValidHoleFits tidy_env implics simples h@(Hole { hole_sort = ExprHole _
+ , hole_loc = ct_loc
+ , hole_ty = hole_ty }) =
do { rdr_env <- getGlobalRdrEnv
- ; lclBinds <- getLocalBindings tidy_env ct
+ ; lclBinds <- getLocalBindings tidy_env ct_loc
; maxVSubs <- maxValidHoleFits <$> getDynFlags
; hfdc <- getHoleFitDispConfig
; sortingAlg <- getSortingAlg
@@ -554,7 +526,9 @@ findValidHoleFits tidy_env implics simples ct | isExprHoleCt ct =
; hfPlugs <- tcg_hf_plugins <$> getGblEnv
; let findVLimit = if sortingAlg > NoSorting then Nothing else maxVSubs
refLevel = refLevelHoleFits dflags
- hole = TyH (listToBag relevantCts) implics (Just ct)
+ hole = TypedHole { th_relevant_cts = listToBag relevantCts
+ , th_implics = implics
+ , th_hole = Just h }
(candidatePlugins, fitPlugins) =
unzip $ map (\p-> ((candPlugin p) hole, (fitPlugin p) hole)) hfPlugs
; traceTc "findingValidHoleFitsFor { " $ ppr hole
@@ -625,11 +599,9 @@ findValidHoleFits tidy_env implics simples ct | isExprHoleCt ct =
where
-- We extract the type, the tcLevel and the types free variables
-- from from the constraint.
- hole_ty :: TcPredType
- hole_ty = ctPred ct
hole_fvs :: FV
hole_fvs = tyCoFVsOfType hole_ty
- hole_lvl = ctLocLevel $ ctEvLoc $ ctEvidence ct
+ hole_lvl = ctLocLevel ct_loc
-- BuiltInSyntax names like (:) and []
builtIns :: [Name]
@@ -668,7 +640,7 @@ findValidHoleFits tidy_env implics simples ct | isExprHoleCt ct =
<*> sortByGraph (sort gblFits)
where (lclFits, gblFits) = span hfIsLcl subs
- -- See Note [Relevant Constraints]
+ -- See Note [Relevant constraints]
relevantCts :: [Ct]
relevantCts = if isEmptyVarSet (fvVarSet hole_fvs) then []
else filter isRelevant simples
@@ -684,7 +656,6 @@ findValidHoleFits tidy_env implics simples ct | isExprHoleCt ct =
-- trying to find hole fits for many holes at once.
isRelevant ct = not (isEmptyVarSet (ctFreeVarSet ct))
&& anyFVMentioned ct
- && not (isHoleCt ct)
-- We zonk the hole fits so that the output aligns with the rest
-- of the typed hole error message output.
@@ -761,7 +732,7 @@ tcFilterHoleFits :: Maybe Int
-- ^ We return whether or not we stopped due to hitting the limit
-- and the fits we found.
tcFilterHoleFits (Just 0) _ _ _ = return (False, []) -- Stop right away on 0
-tcFilterHoleFits limit (TyH {..}) ht@(hole_ty, _) candidates =
+tcFilterHoleFits limit typed_hole ht@(hole_ty, _) candidates =
do { traceTc "checkingFitsFor {" $ ppr hole_ty
; (discards, subs) <- go [] emptyVarSet limit ht candidates
; traceTc "checkingFitsFor }" empty
@@ -895,8 +866,7 @@ tcFilterHoleFits limit (TyH {..}) ht@(hole_ty, _) candidates =
else return Nothing }
else return Nothing }
where fvs = mkFVs ref_vars `unionFV` hole_fvs `unionFV` tyCoFVsOfType ty
- hole = TyH tyHRelevantCts tyHImplics Nothing
-
+ hole = typed_hole { th_hole = Nothing }
subsDiscardMsg :: SDoc
subsDiscardMsg =
@@ -925,7 +895,8 @@ withoutUnification free_vars action =
-- Reset any mutated free variables
; mapM_ restore flexis
; return result }
- where restore = flip writeTcRef Flexi . metaTyVarRef
+ where restore tv = do { traceTc "withoutUnification: restore flexi" (ppr tv)
+ ; writeTcRef (metaTyVarRef tv) Flexi }
fuvs = fvVarList free_vars
-- | Reports whether first type (ty_a) subsumes the second type (ty_b),
@@ -933,14 +904,14 @@ withoutUnification free_vars action =
-- 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
- where dummyHole = TyH emptyBag [] Nothing
+ where dummyHole = TypedHole { th_relevant_cts = emptyBag
+ , th_implics = []
+ , th_hole = Nothing }
-- | A tcSubsumes which takes into account relevant constraints, to fix trac
-- #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.
--- Note: The simplifier may perform unification, so make sure to restore any
--- free type variables to avoid side-effects.
tcCheckHoleFit :: TypedHole -- ^ The hole to check against
-> TcSigmaType
-- ^ The type to check against (possibly modified, e.g. refined)
@@ -949,56 +920,48 @@ tcCheckHoleFit :: TypedHole -- ^ The hole to check against
-- ^ 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 (TyH {..}) hole_ty ty = discardErrs $
+tcCheckHoleFit (TypedHole {..}) hole_ty 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
-- the innermost (the one with the highest level) is first, so it
-- suffices to get the level of the first one (or the current level, if
-- there are no implications involved).
- innermost_lvl <- case tyHImplics of
+ innermost_lvl <- case th_implics of
[] -> getTcLevel
-- imp is the innermost implication
(imp:_) -> return (ic_tclvl imp)
- ; (wrp, wanted) <- setTcLevel innermost_lvl $ captureConstraints $
- tcSubType_NC ExprSigCtxt ty hole_ty
+ ; (wrap, wanted) <- setTcLevel innermost_lvl $ captureConstraints $
+ tcSubType_NC ExprSigCtxt ty hole_ty
; traceTc "Checking hole fit {" empty
; traceTc "wanteds are: " $ ppr wanted
- ; if isEmptyWC wanted && isEmptyBag tyHRelevantCts
- then traceTc "}" empty >> return (True, wrp)
+ ; if isEmptyWC wanted && isEmptyBag th_relevant_cts
+ then do { traceTc "}" empty
+ ; return (True, wrap) }
else do { fresh_binds <- newTcEvBinds
-- The relevant constraints may contain HoleDests, so we must
-- take care to clone them as well (to avoid #15370).
- ; cloned_relevants <- mapBagM cloneWanted tyHRelevantCts
+ ; cloned_relevants <- mapBagM cloneWanted th_relevant_cts
-- We wrap the WC in the nested implications, see
- -- Note [Nested Implications]
- ; let outermost_first = reverse tyHImplics
- setWC = setWCAndBinds fresh_binds
+ -- Note [Checking hole fits]
+ ; let outermost_first = reverse th_implics
-- We add the cloned relevants to the wanteds generated by
- -- the call to tcSubType_NC, see Note [Relevant Constraints]
+ -- the call to tcSubType_NC, see Note [Relevant constraints]
-- There's no need to clone the wanteds, because they are
-- freshly generated by `tcSubtype_NC`.
w_rel_cts = addSimples wanted cloned_relevants
- w_givens = foldr setWC w_rel_cts outermost_first
- ; traceTc "w_givens are: " $ ppr w_givens
- ; rem <- runTcSDeriveds $ simpl_top w_givens
+ final_wc = foldr (setWCAndBinds fresh_binds) w_rel_cts outermost_first
+ ; traceTc "final_wc is: " $ ppr final_wc
+ ; rem <- runTcSDeriveds $ simpl_top final_wc
-- We don't want any insoluble or simple constraints left, but
-- solved implications are ok (and necessary for e.g. undefined)
; traceTc "rems was:" $ ppr rem
; traceTc "}" empty
- ; return (isSolvedWC rem, wrp) } }
+ ; return (isSolvedWC rem, wrap) } }
where
setWCAndBinds :: EvBindsVar -- Fresh ev binds var.
-> Implication -- The implication to put WC in.
-> WantedConstraints -- The WC constraints to put implic.
-> WantedConstraints -- The new constraints.
setWCAndBinds binds imp wc
- = WC { wc_simple = emptyBag
- , wc_impl = unitBag $ imp { ic_wanted = wc , ic_binds = binds } }
-
--- | Maps a plugin that needs no state to one with an empty one.
-fromPureHFPlugin :: HoleFitPlugin -> HoleFitPluginR
-fromPureHFPlugin plug =
- HoleFitPluginR { hfPluginInit = newTcRef ()
- , hfPluginRun = const plug
- , hfPluginStop = const $ return () }
+ = mkImplicWC $ unitBag $ imp { ic_wanted = wc , ic_binds = binds }
=====================================
compiler/GHC/Tc/Errors/Hole.hs-boot
=====================================
@@ -5,9 +5,9 @@
module GHC.Tc.Errors.Hole where
import GHC.Tc.Types ( TcM )
-import GHC.Tc.Types.Constraint ( Ct, Implication )
+import GHC.Tc.Types.Constraint ( Ct, Hole, Implication )
import GHC.Utils.Outputable ( SDoc )
import GHC.Types.Var.Env ( TidyEnv )
-findValidHoleFits :: TidyEnv -> [Implication] -> [Ct] -> Ct
+findValidHoleFits :: TidyEnv -> [Implication] -> [Ct] -> Hole
-> TcM (TidyEnv, SDoc)
=====================================
compiler/GHC/Tc/Errors/Hole/FitTypes.hs
=====================================
@@ -21,20 +21,21 @@ import GHC.Types.Name
import Data.Function ( on )
-data TypedHole = TyH { tyHRelevantCts :: Cts
- -- ^ Any relevant Cts to the hole
- , tyHImplics :: [Implication]
- -- ^ The nested implications of the hole with the
- -- innermost implication first.
- , tyHCt :: Maybe Ct
- -- ^ The hole constraint itself, if available.
- }
+data TypedHole = TypedHole { th_relevant_cts :: Cts
+ -- ^ Any relevant Cts to the hole
+ , th_implics :: [Implication]
+ -- ^ The nested implications of the hole with the
+ -- innermost implication first.
+ , th_hole :: Maybe Hole
+ -- ^ The hole itself, if available. Only for debugging.
+ }
instance Outputable TypedHole where
- ppr (TyH rels implics ct)
+ ppr (TypedHole { th_relevant_cts = rels
+ , th_implics = implics
+ , th_hole = hole })
= hang (text "TypedHole") 2
- (ppr rels $+$ ppr implics $+$ ppr ct)
-
+ (ppr rels $+$ ppr implics $+$ ppr hole)
-- | HoleFitCandidates are passed to hole fit plugins and then
-- checked whether they fit a given typed-hole.
@@ -51,9 +52,6 @@ pprHoleFitCand (IdHFCand cid) = text "Id HFC: " <> ppr cid
pprHoleFitCand (NameHFCand cname) = text "Name HFC: " <> ppr cname
pprHoleFitCand (GreHFCand cgre) = text "Gre HFC: " <> ppr cgre
-
-
-
instance NamedThing HoleFitCandidate where
getName hfc = case hfc of
IdHFCand cid -> idName cid
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -36,7 +36,6 @@ import {-# SOURCE #-} GHC.Tc.Gen.Splice( tcSpliceExpr, tcTypedBracket, tcUntyp
import GHC.Builtin.Names.TH( liftStringName, liftName )
import GHC.Hs
-import GHC.Tc.Types.Constraint ( HoleSort(..) )
import GHC.Tc.Utils.Zonk
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.Unify
@@ -1408,22 +1407,21 @@ Suppose 'wurble' is not in scope, and we have
Then the renamer will make (HsUnboundVar "wurble) for 'wurble',
and the typechecker will typecheck it with tcUnboundId, giving it
-a type 'alpha', and emitting a deferred CHoleCan constraint, to
-be reported later.
+a type 'alpha', and emitting a deferred Hole, to be reported later.
But then comes the visible type application. If we do nothing, we'll
generate an immediate failure (in tc_app_err), saying that a function
of type 'alpha' can't be applied to Bool. That's insane! And indeed
users complain bitterly (#13834, #17150.)
-The right error is the CHoleCan, which has /already/ been emitted by
+The right error is the Hole, which has /already/ been emitted by
tcUnboundId. It later reports 'wurble' as out of scope, and tries to
give its type.
Fortunately in tcArgs we still have access to the function, so we can
check if it is a HsUnboundVar. We use this info to simply skip over
any visible type arguments. We've already inferred the type of the
-function, so we'll /already/ have emitted a CHoleCan constraint;
+function, so we'll /already/ have emitted a Hole;
failing preserves that constraint.
We do /not/ want to fail altogether in this case (via failM) becuase
@@ -1900,14 +1898,13 @@ tcUnboundId :: HsExpr GhcRn -> OccName -> ExpRhoType -> TcM (HsExpr GhcTc)
-- Others might simply be variables that accidentally have no binding site
--
-- We turn all of them into HsVar, since HsUnboundVar can't contain an
--- Id; and indeed the evidence for the CHoleCan does bind it, so it's
+-- Id; and indeed the evidence for the ExprHole does bind it, so it's
-- not unbound any more!
tcUnboundId rn_expr occ res_ty
= do { ty <- newOpenFlexiTyVarTy -- Allow Int# etc (#12531)
; name <- newSysName occ
; let ev = mkLocalId name ty
- ; can <- newHoleCt ExprHole ev ty
- ; emitInsoluble can
+ ; emitNewExprHole occ ev ty
; tcWrapResultO (UnboundOccurrenceOf occ) rn_expr
(HsVar noExtField (noLoc ev)) ty res_ty }
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -419,7 +419,7 @@ tcHsTypeApp wc_ty kind
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A HsWildCardBndrs's hswc_ext now only includes /named/ wildcards, so
any unnamed wildcards stay unchanged in hswc_body. When called in
-tcHsTypeApp, tcCheckLHsType will call emitAnonWildCardHoleConstraint
+tcHsTypeApp, tcCheckLHsType will call emitAnonTypeHole
on these anonymous wildcards. However, this would trigger
error/warning when an anonymous wildcard is passed in as a visible type
argument, which we do not want because users should be able to write
@@ -891,7 +891,7 @@ tcAnonWildCardOcc wc exp_kind
; warning <- woptM Opt_WarnPartialTypeSignatures
; unless (part_tysig && not warning) $
- emitAnonWildCardHoleConstraint wc_tv
+ emitAnonTypeHole wc_tv
-- Why the 'unless' guard?
-- See Note [Wildcards in visible kind application]
@@ -911,11 +911,11 @@ x = MkT
So we should allow '@_' without emitting any hole constraints, and
regardless of whether PartialTypeSignatures is enabled or not. But how would
the typechecker know which '_' is being used in VKA and which is not when it
-calls emitNamedWildCardHoleConstraints in tcHsPartialSigType on all HsWildCardBndrs?
+calls emitNamedTypeHole in tcHsPartialSigType on all HsWildCardBndrs?
The solution then is to neither rename nor include unnamed wildcards in HsWildCardBndrs,
but instead give every anonymous wildcard a fresh wild tyvar in tcAnonWildCardOcc.
And whenever we see a '@', we automatically turn on PartialTypeSignatures and
-turn off hole constraint warnings, and do not call emitAnonWildCardHoleConstraint
+turn off hole constraint warnings, and do not call emitAnonTypeHole
under these conditions.
See related Note [Wildcards in visible type application] here and
Note [The wildcard story for types] in GHC.Hs.Types
@@ -3192,7 +3192,7 @@ tcHsPartialSigType ctxt sig_ty
-- Spit out the wildcards (including the extra-constraints one)
-- as "hole" constraints, so that they'll be reported if necessary
-- See Note [Extra-constraint holes in partial type signatures]
- ; emitNamedWildCardHoleConstraints wcs
+ ; mapM_ emitNamedTypeHole wcs
-- Zonk, so that any nested foralls can "see" their occurrences
-- See Note [Checking partial type signatures], in
@@ -3365,7 +3365,7 @@ tcHsPatSigType ctxt sig_ty
do { sig_ty <- tcHsOpenType hs_ty
; return (wcs, sig_ty) }
- ; emitNamedWildCardHoleConstraints wcs
+ ; mapM_ emitNamedTypeHole wcs
-- sig_ty might have tyvars that are at a higher TcLevel (if hs_ty
-- contains a forall). Promote these.
=====================================
compiler/GHC/Tc/Gen/Rule.hs
=====================================
@@ -460,9 +460,9 @@ getRuleQuantCts wc
= float_wc emptyVarSet wc
where
float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
- float_wc skol_tvs (WC { wc_simple = simples, wc_impl = implics })
+ float_wc skol_tvs (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes })
= ( simple_yes `andCts` implic_yes
- , WC { wc_simple = simple_no, wc_impl = implics_no })
+ , emptyWC { wc_simple = simple_no, wc_impl = implics_no, wc_holes = holes })
where
(simple_yes, simple_no) = partitionBag (rule_quant_ct skol_tvs) simples
(implic_yes, implics_no) = mapAccumBagL (float_implic skol_tvs)
@@ -480,8 +480,6 @@ getRuleQuantCts wc
| EqPred _ t1 t2 <- classifyPredType (ctPred ct)
, not (ok_eq t1 t2)
= False -- Note [RULE quantification over equalities]
- | isHoleCt ct
- = False -- Don't quantify over type holes, obviously
| otherwise
= tyCoVarsOfCt ct `disjointVarSet` skol_tvs
=====================================
compiler/GHC/Tc/Module.hs
=====================================
@@ -2589,7 +2589,7 @@ tcRnType hsc_env flexi normalise rdr_type
-- kindGeneralize, below
solveEqualities $
tcNamedWildCardBinders wcs $ \ wcs' ->
- do { emitNamedWildCardHoleConstraints wcs'
+ do { mapM_ emitNamedTypeHole wcs'
; tcLHsTypeUnsaturated rn_type }
-- Do kind generalisation; see Note [Kind-generalise in tcRnType]
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -31,7 +31,7 @@ import GHC.Prelude
import GHC.Data.Bag
import GHC.Core.Class ( Class, classKey, classTyCon )
import GHC.Driver.Session
-import GHC.Types.Id ( idType, mkLocalId )
+import GHC.Types.Id ( idType )
import GHC.Tc.Utils.Instantiate
import GHC.Data.List.SetOps
import GHC.Types.Name
@@ -42,6 +42,7 @@ import GHC.Tc.Errors
import GHC.Tc.Types.Evidence
import GHC.Tc.Solver.Interact
import GHC.Tc.Solver.Canonical ( makeSuperClasses, solveCallStack )
+import GHC.Tc.Solver.Flatten ( flattenType )
import GHC.Tc.Utils.TcMType as TcM
import GHC.Tc.Utils.Monad as TcM
import GHC.Tc.Solver.Monad as TcS
@@ -145,8 +146,7 @@ simplifyTop wanteds
; saved_msg <- TcM.readTcRef errs_var
; TcM.writeTcRef errs_var emptyMessages
- ; warnAllUnsolved $ WC { wc_simple = unsafe_ol
- , wc_impl = emptyBag }
+ ; warnAllUnsolved $ emptyWC { wc_simple = unsafe_ol }
; whyUnsafe <- fst <$> TcM.readTcRef errs_var
; TcM.writeTcRef errs_var saved_msg
@@ -638,27 +638,15 @@ tcNormalise :: Bag EvVar -> Type -> TcM Type
tcNormalise given_ids ty
= do { lcl_env <- TcM.getLclEnv
; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
- ; wanted_ct <- mk_wanted_ct
+ ; norm_loc <- getCtLocM PatCheckOrigin Nothing
; (res, _ev_binds) <- runTcS $
do { traceTcS "tcNormalise {" (ppr given_ids)
; let given_cts = mkGivens given_loc (bagToList given_ids)
; solveSimpleGivens given_cts
- ; wcs <- solveSimpleWanteds (unitBag wanted_ct)
- -- It's an invariant that this wc_simple will always be
- -- a singleton Ct, since that's what we fed in as input.
- ; let ty' = case bagToList (wc_simple wcs) of
- (ct:_) -> ctEvPred (ctEvidence ct)
- cts -> pprPanic "tcNormalise" (ppr cts)
+ ; ty' <- flattenType norm_loc ty
; traceTcS "tcNormalise }" (ppr ty')
; pure ty' }
; return res }
- where
- mk_wanted_ct :: TcM Ct
- mk_wanted_ct = do
- let occ = mkVarOcc "$tcNorm"
- name <- newSysName occ
- let ev = mkLocalId name ty
- newHoleCt ExprHole ev ty
{- Note [Superclasses and satisfiability]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -696,11 +684,8 @@ if some local equalities are solved for. See "Wrinkle: Local equalities"
in Note [Type normalisation] in Check.
To accomplish its stated goal, tcNormalise first feeds the local constraints
-into solveSimpleGivens, then stuffs the argument type in a CHoleCan, and feeds
-that singleton Ct into solveSimpleWanteds, which reduces the type in the
-CHoleCan as much as possible with respect to the local given constraints. When
-solveSimpleWanteds is finished, we dig out the type from the CHoleCan and
-return that.
+into solveSimpleGivens, then uses flattenType to simplify the desired type
+with respect to the givens.
***********************************************************************************
* *
@@ -889,8 +874,8 @@ mkResidualConstraints rhs_tclvl ev_binds_var
, ic_no_eqs = False
, ic_info = skol_info }
- ; return (WC { wc_simple = outer_simple
- , wc_impl = implics })}
+ ; return (emptyWC { wc_simple = outer_simple
+ , wc_impl = implics })}
where
full_theta = map idType full_theta_vars
skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
@@ -1516,7 +1501,7 @@ solveWantedsAndDrop wanted
solveWanteds :: WantedConstraints -> TcS WantedConstraints
-- so that the inert set doesn't mindlessly propagate.
-- NB: wc_simples may be wanted /or/ derived now
-solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics })
+solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics, wc_holes = holes })
= do { cur_lvl <- TcS.getTcLevel
; traceTcS "solveWanteds {" $
vcat [ text "Level =" <+> ppr cur_lvl
@@ -1530,9 +1515,12 @@ solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics })
implics `unionBags` wc_impl wc1
; dflags <- getDynFlags
- ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
+ ; solved_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
(wc1 { wc_impl = implics2 })
+ ; holes' <- simplifyHoles holes
+ ; let final_wc = solved_wc { wc_holes = holes' }
+
; ev_binds_var <- getTcEvBindsVar
; bb <- TcS.getTcEvBindsMap ev_binds_var
; traceTcS "solveWanteds }" $
@@ -1779,12 +1767,13 @@ setImplicationStatus implic@(Implic { ic_status = status
then Nothing
else Just final_implic }
where
- WC { wc_simple = simples, wc_impl = implics } = wc
+ WC { wc_simple = simples, wc_impl = implics, wc_holes = holes } = wc
pruned_simples = dropDerivedSimples simples
pruned_implics = filterBag keep_me implics
pruned_wc = WC { wc_simple = pruned_simples
- , wc_impl = pruned_implics }
+ , wc_impl = pruned_implics
+ , wc_holes = holes } -- do not prune holes; these should be reported
keep_me :: Implication -> Bool
keep_me ic
@@ -1898,6 +1887,14 @@ neededEvVars implic@(Implic { ic_given = givens
| is_given = needs -- Add the rhs vars of the Wanted bindings only
| otherwise = evVarsOfTerm rhs `unionVarSet` needs
+-------------------------------------------------
+simplifyHoles :: Bag Hole -> TcS (Bag Hole)
+simplifyHoles = mapBagM simpl_hole
+ where
+ simpl_hole :: Hole -> TcS Hole
+ simpl_hole h@(Hole { hole_ty = ty, hole_loc = loc })
+ = do { ty' <- flattenType loc ty
+ ; return (h { hole_ty = ty' }) }
{- Note [Delete dead Given evidence bindings]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2143,7 +2140,6 @@ approximateWC float_past_equalities wc
is_floatable skol_tvs ct
| isGivenCt ct = False
- | isHoleCt ct = False
| insolubleEqCt ct = False
| otherwise = tyCoVarsOfCt ct `disjointVarSet` skol_tvs
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -34,7 +34,6 @@ import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe )
import GHC.Types.Var
import GHC.Types.Var.Env( mkInScopeSet )
import GHC.Types.Var.Set( delVarSetList )
-import GHC.Types.Name.Occurrence ( OccName )
import GHC.Utils.Outputable
import GHC.Driver.Session( DynFlags )
import GHC.Types.Name.Set
@@ -67,8 +66,7 @@ Canonicalization converts a simple constraint to a canonical form. It is
unary (i.e. treats individual constraints one at a time).
Constraints originating from user-written code come into being as
-CNonCanonicals (except for CHoleCans, arising from holes). We know nothing
-about these constraints. So, first:
+CNonCanonicals. We know nothing about these constraints. So, first:
Classify CNonCanoncal constraints, depending on whether they
are equalities, class predicates, or other.
@@ -137,9 +135,6 @@ canonicalize (CFunEqCan { cc_ev = ev
= {-# SCC "canEqLeafFunEq" #-}
canCFunEqCan ev fn xis1 fsk
-canonicalize (CHoleCan { cc_ev = ev, cc_occ = occ, cc_hole = hole })
- = canHole ev occ hole
-
{-
************************************************************************
* *
@@ -718,17 +713,6 @@ canIrred status ev
_ -> continueWith $
mkIrredCt status new_ev } }
-canHole :: CtEvidence -> OccName -> HoleSort -> TcS (StopOrContinue Ct)
-canHole ev occ hole_sort
- = do { let pred = ctEvPred ev
- ; (xi,co) <- flatten FM_SubstOnly ev pred -- co :: xi ~ pred
- ; rewriteEvidence ev xi co `andWhenContinue` \ new_ev ->
- do { updInertIrreds (`snocCts` (CHoleCan { cc_ev = new_ev
- , cc_occ = occ
- , cc_hole = hole_sort }))
- ; stopWith new_ev "Emit insoluble hole" } }
-
-
{- *********************************************************************
* *
* Quantified predicates
@@ -1401,6 +1385,7 @@ can_eq_app ev s1 t1 s2 t2
| CtDerived {} <- ev
= do { unifyDeriveds loc [Nominal, Nominal] [s1, t1] [s2, t2]
; stopWith ev "Decomposed [D] AppTy" }
+
| CtWanted { ctev_dest = dest } <- ev
= do { co_s <- unifyWanted loc Nominal s1 s2
; let arg_loc
=====================================
compiler/GHC/Tc/Solver/Flatten.hs
=====================================
@@ -5,7 +5,7 @@
module GHC.Tc.Solver.Flatten(
FlattenMode(..),
flatten, flattenKind, flattenArgsNom,
- rewriteTyVar,
+ rewriteTyVar, flattenType,
unflattenWanteds
) where
@@ -825,6 +825,20 @@ flattenArgsNom ev tc tys
; traceTcS "flatten }" (vcat (map ppr tys'))
; return (tys', cos, kind_co) }
+-- | Flatten a type w.r.t. nominal equality. This is useful to rewrite
+-- a type w.r.t. any givens. It does not do type-family reduction. This
+-- will never emit new constraints. Call this when the inert set contains
+-- only givens.
+flattenType :: CtLoc -> TcType -> TcS TcType
+flattenType loc ty
+ -- More info about FM_SubstOnly in Note [Holes] in GHC.Tc.Types.Constraint
+ = do { (xi, _) <- runFlatten FM_SubstOnly loc Given NomEq $
+ flatten_one ty
+ -- use Given flavor so that it is rewritten
+ -- only w.r.t. Givens, never Wanteds/Deriveds
+ -- (Shouldn't matter, if only Givens are present
+ -- anyway)
+ ; return xi }
{- *********************************************************************
* *
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -195,7 +195,7 @@ solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
-- Try solving these constraints
-- Affects the unification state (of course) but not the inert set
-- The result is not necessarily zonked
-solve_simple_wanteds (WC { wc_simple = simples1, wc_impl = implics1 })
+solve_simple_wanteds (WC { wc_simple = simples1, wc_impl = implics1, wc_holes = holes })
= nestTcS $
do { solveSimples simples1
; (implics2, tv_eqs, fun_eqs, others) <- getUnsolvedInerts
@@ -204,7 +204,8 @@ solve_simple_wanteds (WC { wc_simple = simples1, wc_impl = implics1 })
-- See Note [Unflatten after solving the simple wanteds]
; return ( unif_count
, WC { wc_simple = others `andCts` unflattened_eqs
- , wc_impl = implics1 `unionBags` implics2 }) }
+ , wc_impl = implics1 `unionBags` implics2
+ , wc_holes = holes }) }
{- Note [The solveSimpleWanteds loop]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -264,7 +265,7 @@ runTcPluginsGiven
-- 'solveSimpleWanteds' should feed the updated wanteds back into the
-- main solver.
runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
-runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_impl = implics1 })
+runTcPluginsWanted wc@(WC { wc_simple = simples1 })
| isEmptyBag simples1
= return (False, wc)
| otherwise
@@ -285,11 +286,10 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_impl = implics1 })
; mapM_ setEv solved_wanted
; return ( notNull (pluginNewCts p)
- , WC { wc_simple = listToBag new_wanted `andCts`
+ , wc { wc_simple = listToBag new_wanted `andCts`
listToBag unsolved_wanted `andCts`
listToBag unsolved_derived `andCts`
- listToBag insols
- , wc_impl = implics1 } ) } }
+ listToBag insols } ) } }
where
setEv :: (EvTerm,Ct) -> TcS ()
setEv (ev,ct) = case ctEvidence ct of
@@ -494,7 +494,6 @@ interactWithInertsStage wi
CIrredCan {} -> interactIrred ics wi
CDictCan {} -> interactDict ics wi
_ -> pprPanic "interactWithInerts" (ppr wi) }
- -- CHoleCan are put straight into inert_frozen, so never get here
-- CNonCanonical have been canonicalised
data InteractResult
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -198,7 +198,7 @@ import GHC.Types.Unique.Set
Note [WorkList priorities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A WorkList contains canonical and non-canonical items (of all flavors).
+A WorkList contains canonical and non-canonical items (of all flavours).
Notice that each Ct now has a simplification depth. We may
consider using this depth for prioritization as well in the future.
@@ -1653,8 +1653,7 @@ add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys })
add_item _ item
= pprPanic "upd_inert set: can't happen! Inserting " $
- ppr item -- Can't be CNonCanonical, CHoleCan,
- -- because they only land in inert_irreds
+ ppr item -- Can't be CNonCanonical because they only land in inert_irreds
bumpUnsolvedCount :: CtEvidence -> Int -> Int
bumpUnsolvedCount ev n | isWanted ev = n+1
@@ -1896,10 +1895,6 @@ be decomposed. Otherwise we end up with a "Can't match [Int] ~
[[Int]]" which is true, but a bit confusing because the outer type
constructors match.
-Similarly, if we have a CHoleCan, we'd like to rewrite it with any
-Givens, to give as informative an error messasge as possible
-(#12468, #11325).
-
Hence:
* In the main simplifier loops in GHC.Tc.Solver (solveWanteds,
simpl_loop), we feed the insolubles in solveSimpleWanteds,
@@ -2352,8 +2347,6 @@ removeInertCt is ct =
CQuantCan {} -> panic "removeInertCt: CQuantCan"
CIrredCan {} -> panic "removeInertCt: CIrredEvCan"
CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
- CHoleCan {} -> panic "removeInertCt: CHoleCan"
-
lookupFlatCache :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType, CtFlavour))
lookupFlatCache fam_tc tys
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -14,8 +14,7 @@ module GHC.Tc.Types.Constraint (
isEmptyCts, isCTyEqCan, isCFunEqCan,
isPendingScDict, superClassesMightHelp, getPendingWantedScs,
isCDictCan_Maybe, isCFunEqCan_maybe,
- isCNonCanonical, isWantedCt, isDerivedCt,
- isGivenCt, isHoleCt, isOutOfScopeCt, isExprHoleCt, isTypeHoleCt,
+ isCNonCanonical, isWantedCt, isDerivedCt, isGivenCt,
isUserTypeErrorCt, getUserTypeErrorMsg,
ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
ctEvId, mkTcEqPredLikeEv,
@@ -26,9 +25,11 @@ module GHC.Tc.Types.Constraint (
tyCoVarsOfCt, tyCoVarsOfCts,
tyCoVarsOfCtList, tyCoVarsOfCtsList,
+ Hole(..), HoleSort(..), isOutOfScopeHole,
+
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC,
- addInsols, insolublesOnly, addSimples, addImplics,
+ addInsols, insolublesOnly, addSimples, addImplics, addHole,
tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples,
tyCoVarsOfWCList, insolubleCt, insolubleEqCt,
isDroppableCt, insolubleImplic,
@@ -62,9 +63,6 @@ module GHC.Tc.Types.Constraint (
pprEvVarTheta,
pprEvVars, pprEvVarWithType,
- -- holes
- HoleSort(..),
-
)
where
@@ -202,14 +200,6 @@ data Ct
cc_ev :: CtEvidence
}
- | CHoleCan { -- See Note [Hole constraints]
- -- Treated as an "insoluble" constraint
- -- See Note [Insoluble constraints]
- cc_ev :: CtEvidence,
- cc_occ :: OccName, -- The name of this hole
- cc_hole :: HoleSort -- The sort of this hole (expr, type, ...)
- }
-
| CQuantCan QCInst -- A quantified constraint
-- NB: I expect to make more of the cases in Ct
-- look like this, with the payload in an
@@ -230,13 +220,47 @@ instance Outputable QCInst where
ppr (QCI { qci_ev = ev }) = ppr ev
------------
+-- | A hole stores the information needed to report diagnostics
+-- about holes in terms (unbound identifiers or underscores) or
+-- in types (also called wildcards, as used in partial type
+-- signatures). See Note [Holes].
+data Hole
+ = Hole { hole_sort :: HoleSort -- ^ What flavour of hole is this?
+ , hole_occ :: OccName -- ^ The name of this hole
+ , hole_ty :: TcType -- ^ Type to be printed to the user
+ -- For expression holes: type of expr
+ -- For type holes: the missing type
+ , hole_loc :: CtLoc -- ^ Where hole was written
+ }
+ -- For the hole_loc, we usually only want the TcLclEnv stored within.
+ -- Except when we flatten, where we need a whole location. And this
+ -- might get reported to the user if reducing type families in a
+ -- hole type loops.
+
+
-- | Used to indicate which sort of hole we have.
-data HoleSort = ExprHole
+data HoleSort = ExprHole Id
-- ^ Either an out-of-scope variable or a "true" hole in an
- -- expression (TypedHoles)
+ -- expression (TypedHoles).
+ -- The 'Id' is where to store "evidence": this evidence
+ -- will be an erroring expression for -fdefer-type-errors.
| TypeHole
-- ^ A hole in a type (PartialTypeSignatures)
+instance Outputable Hole where
+ ppr (Hole { hole_sort = ExprHole id
+ , hole_occ = occ
+ , hole_ty = ty })
+ = parens $ (braces $ ppr occ <> colon <> ppr id) <+> dcolon <+> ppr ty
+ ppr (Hole { hole_sort = TypeHole
+ , hole_occ = occ
+ , hole_ty = ty })
+ = braces $ ppr occ <> colon <> ppr ty
+
+instance Outputable HoleSort where
+ ppr (ExprHole id) = text "ExprHole:" <> ppr id
+ ppr TypeHole = text "TypeHole"
+
------------
-- | Used to indicate extra information about why a CIrredCan is irreducible
data CtIrredStatus
@@ -252,20 +276,8 @@ instance Outputable CtIrredStatus where
ppr BlockedCIS = text "(blocked)"
ppr OtherCIS = text "(soluble)"
-{- Note [Hole constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-CHoleCan constraints are used for two kinds of holes,
-distinguished by cc_hole:
-
- * For holes in expressions
- e.g. f x = g _ x
-
- * For holes in type signatures
- e.g. f :: _ -> _
- f x = [x,True]
-
-Note [CIrredCan constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [CIrredCan constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
CIrredCan constraints are used for constraints that are "stuck"
- we can't solve them (yet)
- we can't use them to solve other constraints
@@ -350,6 +362,40 @@ unenforced).
The almost-function-free property is checked by isAlmostFunctionFree in GHC.Tc.Utils.TcType.
The flattener (in GHC.Tc.Solver.Flatten) produces types that are almost function-free.
+Note [Holes]
+~~~~~~~~~~~~
+This Note explains how GHC tracks *holes*.
+
+A hole represents one of two conditions:
+ - A missing bit of an expression. Example: foo x = x + _
+ - A missing bit of a type. Example: bar :: Int -> _
+
+What these have in common is that both cause GHC to emit a diagnostic to the
+user describing the bit that is left out.
+
+When a hole is encountered, a new entry of type Hole is added to the ambient
+WantedConstraints. The type (hole_ty) of the hole is then simplified during
+solving (with respect to any Givens in surrounding implications). It is
+reported with all the other errors in GHC.Tc.Errors. No type family reduction
+is done on hole types; this is purely because we think it will produce
+better error messages not to reduce type families. This is why the
+GHC.Tc.Solver.Flatten.flattenType function uses FM_SubstOnly.
+
+For expression holes, the user has the option of deferring errors until runtime
+with -fdefer-type-errors. In this case, the hole actually has evidence: this
+evidence is an erroring expression that prints an error and crashes at runtime.
+The ExprHole variant of holes stores the Id that will be bound to this evidence;
+during constraint generation, this Id was inserted into the expression output
+by the type checker.
+
+You might think that the type of the stored Id is the same as the type of the
+hole. However, because the hole type (hole_ty) is rewritten with respect to
+givens, this might not be the case. That is, the hole_ty is always (~) to the
+type of the Id, but they might not be `eqType`. We need the type of the generated
+evidence to match what is expected in the context of the hole, and so we must
+store these types separately.
+
+Type-level holes have no evidence at all.
-}
mkNonCanonical :: CtEvidence -> Ct
@@ -419,7 +465,6 @@ instance Outputable Ct where
| pend_sc -> text "CDictCan(psc)"
| otherwise -> text "CDictCan"
CIrredCan { cc_status = status } -> text "CIrredCan" <> ppr status
- CHoleCan { cc_occ = occ } -> text "CHoleCan:" <+> ppr occ
CQuantCan (QCI { qci_pend_sc = pend_sc })
| pend_sc -> text "CQuantCan(psc)"
| otherwise -> text "CQuantCan"
@@ -482,9 +527,10 @@ tyCoVarsOfWCList = fvVarList . tyCoFVsOfWC
-- computation. See Note [Deterministic FV] in GHC.Utils.FV.
tyCoFVsOfWC :: WantedConstraints -> FV
-- Only called on *zonked* things, hence no need to worry about flatten-skolems
-tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic })
+tyCoFVsOfWC (WC { wc_simple = simple, wc_impl = implic, wc_holes = holes })
= tyCoFVsOfCts simple `unionFV`
- tyCoFVsOfBag tyCoFVsOfImplic implic
+ tyCoFVsOfBag tyCoFVsOfImplic implic `unionFV`
+ tyCoFVsOfBag tyCoFVsOfHole holes
-- | Returns free variables of Implication as a composable FV computation.
-- See Note [Deterministic FV] in GHC.Utils.FV.
@@ -500,6 +546,9 @@ tyCoFVsOfImplic (Implic { ic_skols = skols
tyCoFVsVarBndrs givens $
tyCoFVsOfWC wanted
+tyCoFVsOfHole :: Hole -> FV
+tyCoFVsOfHole (Hole { hole_ty = ty }) = tyCoFVsOfType ty
+
tyCoFVsOfBag :: (a -> FV) -> Bag a -> FV
tyCoFVsOfBag tvs_of = foldr (unionFV . tvs_of) emptyFV
@@ -552,7 +601,6 @@ isDroppableCt ct
keep_deriv
= case ct of
- CHoleCan {} -> True
CIrredCan { cc_status = InsolubleCIS } -> keep_eq True
_ -> keep_eq False
@@ -676,26 +724,6 @@ isCNonCanonical :: Ct -> Bool
isCNonCanonical (CNonCanonical {}) = True
isCNonCanonical _ = False
-isHoleCt:: Ct -> Bool
-isHoleCt (CHoleCan {}) = True
-isHoleCt _ = False
-
-isOutOfScopeCt :: Ct -> Bool
--- A Hole that does not have a leading underscore is
--- simply an out-of-scope variable, and we treat that
--- a bit differently when it comes to error reporting
-isOutOfScopeCt (CHoleCan { cc_occ = occ }) = not (startsWithUnderscore occ)
-isOutOfScopeCt _ = False
-
-isExprHoleCt :: Ct -> Bool
-isExprHoleCt (CHoleCan { cc_hole = ExprHole }) = True
-isExprHoleCt _ = False
-
-isTypeHoleCt :: Ct -> Bool
-isTypeHoleCt (CHoleCan { cc_hole = TypeHole }) = True
-isTypeHoleCt _ = False
-
-
{- Note [Custom type errors in constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -884,37 +912,39 @@ v%************************************************************************
data WantedConstraints
= WC { wc_simple :: Cts -- Unsolved constraints, all wanted
, wc_impl :: Bag Implication
+ , wc_holes :: Bag Hole
}
emptyWC :: WantedConstraints
-emptyWC = WC { wc_simple = emptyBag, wc_impl = emptyBag }
+emptyWC = WC { wc_simple = emptyBag
+ , wc_impl = emptyBag
+ , wc_holes = emptyBag }
mkSimpleWC :: [CtEvidence] -> WantedConstraints
mkSimpleWC cts
- = WC { wc_simple = listToBag (map mkNonCanonical cts)
- , wc_impl = emptyBag }
+ = emptyWC { wc_simple = listToBag (map mkNonCanonical cts) }
mkImplicWC :: Bag Implication -> WantedConstraints
mkImplicWC implic
- = WC { wc_simple = emptyBag, wc_impl = implic }
+ = emptyWC { wc_impl = implic }
isEmptyWC :: WantedConstraints -> Bool
-isEmptyWC (WC { wc_simple = f, wc_impl = i })
- = isEmptyBag f && isEmptyBag i
-
+isEmptyWC (WC { wc_simple = f, wc_impl = i, wc_holes = holes })
+ = isEmptyBag f && isEmptyBag i && isEmptyBag holes
-- | Checks whether a the given wanted constraints are solved, i.e.
-- that there are no simple constraints left and all the implications
-- are solved.
isSolvedWC :: WantedConstraints -> Bool
-isSolvedWC WC {wc_simple = wc_simple, wc_impl = wc_impl} =
- isEmptyBag wc_simple && allBag (isSolvedStatus . ic_status) wc_impl
+isSolvedWC WC {wc_simple = wc_simple, wc_impl = wc_impl, wc_holes = holes} =
+ isEmptyBag wc_simple && allBag (isSolvedStatus . ic_status) wc_impl && isEmptyBag holes
andWC :: WantedConstraints -> WantedConstraints -> WantedConstraints
-andWC (WC { wc_simple = f1, wc_impl = i1 })
- (WC { wc_simple = f2, wc_impl = i2 })
+andWC (WC { wc_simple = f1, wc_impl = i1, wc_holes = h1 })
+ (WC { wc_simple = f2, wc_impl = i2, wc_holes = h2 })
= WC { wc_simple = f1 `unionBags` f2
- , wc_impl = i1 `unionBags` i2 }
+ , wc_impl = i1 `unionBags` i2
+ , wc_holes = h1 `unionBags` h2 }
unionsWC :: [WantedConstraints] -> WantedConstraints
unionsWC = foldr andWC emptyWC
@@ -931,11 +961,16 @@ addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints
addInsols wc cts
= wc { wc_simple = wc_simple wc `unionBags` cts }
+addHole :: WantedConstraints -> Hole -> WantedConstraints
+addHole wc hole
+ = wc { wc_holes = hole `consBag` wc_holes wc }
+
insolublesOnly :: WantedConstraints -> WantedConstraints
-- Keep only the definitely-insoluble constraints
-insolublesOnly (WC { wc_simple = simples, wc_impl = implics })
+insolublesOnly (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes })
= WC { wc_simple = filterBag insolubleCt simples
- , wc_impl = mapBag implic_insols_only implics }
+ , wc_impl = mapBag implic_insols_only implics
+ , wc_holes = filterBag isOutOfScopeHole holes }
where
implic_insols_only implic
= implic { ic_wanted = insolublesOnly (ic_wanted implic) }
@@ -953,9 +988,10 @@ insolubleImplic :: Implication -> Bool
insolubleImplic ic = isInsolubleStatus (ic_status ic)
insolubleWC :: WantedConstraints -> Bool
-insolubleWC (WC { wc_impl = implics, wc_simple = simples })
+insolubleWC (WC { wc_impl = implics, wc_simple = simples, wc_holes = holes })
= anyBag insolubleCt simples
|| anyBag insolubleImplic implics
+ || anyBag isOutOfScopeHole holes -- See Note [Insoluble holes]
insolubleCt :: Ct -> Bool
-- Definitely insoluble, in particular /excluding/ type-hole constraints
@@ -963,7 +999,6 @@ insolubleCt :: Ct -> Bool
-- b) that is insoluble
-- c) and does not arise from a Given
insolubleCt ct
- | isHoleCt ct = isOutOfScopeCt ct -- See Note [Insoluble holes]
| not (insolubleEqCt ct) = False
| arisesFromGivens ct = False -- See Note [Given insolubles]
| otherwise = True
@@ -986,11 +1021,17 @@ insolubleEqCt :: Ct -> Bool
insolubleEqCt (CIrredCan { cc_status = InsolubleCIS }) = True
insolubleEqCt _ = False
+-- | Does this hole represent an "out of scope" error?
+-- See Note [Insoluble holes]
+isOutOfScopeHole :: Hole -> Bool
+isOutOfScopeHole (Hole { hole_occ = occ }) = not (startsWithUnderscore occ)
+
instance Outputable WantedConstraints where
- ppr (WC {wc_simple = s, wc_impl = i})
+ ppr (WC {wc_simple = s, wc_impl = i, wc_holes = h})
= text "WC" <+> braces (vcat
[ ppr_bag (text "wc_simple") s
- , ppr_bag (text "wc_impl") i ])
+ , ppr_bag (text "wc_impl") i
+ , ppr_bag (text "wc_holes") h ])
ppr_bag :: Outputable a => SDoc -> Bag a -> SDoc
ppr_bag doc bag
@@ -1035,7 +1076,7 @@ Hole constraints that ARE NOT treated as truly insoluble:
a) type holes, arising from PartialTypeSignatures,
b) "true" expression holes arising from TypedHoles
-An "expression hole" or "type hole" constraint isn't really an error
+An "expression hole" or "type hole" isn't really an error
at all; it's a report saying "_ :: Int" here. But an out-of-scope
variable masquerading as expression holes IS treated as truly
insoluble, so that it trumps other errors during error reporting.
@@ -1512,10 +1553,6 @@ ctFlavourRole (CTyEqCan { cc_ev = ev, cc_eq_rel = eq_rel })
= (ctEvFlavour ev, eq_rel)
ctFlavourRole (CFunEqCan { cc_ev = ev })
= (ctEvFlavour ev, NomEq)
-ctFlavourRole (CHoleCan { cc_ev = ev })
- = (ctEvFlavour ev, NomEq) -- NomEq: CHoleCans can be rewritten by
- -- by nominal equalities but empahatically
- -- not by representational equalities
ctFlavourRole ct
= ctEvFlavourRole (ctEvidence ct)
=====================================
compiler/GHC/Tc/Types/Origin.hs
=====================================
@@ -427,7 +427,9 @@ data CtOrigin
-- We only need a CtOrigin on the first, because the location
-- is pinned on the entire error message
- | HoleOrigin
+ | ExprHoleOrigin OccName -- from an expression hole
+ | TypeHoleOrigin OccName -- from a type hole (partial type signature)
+ | PatCheckOrigin -- normalisation of a type during pattern-match checking
| UnboundOccurrenceOf OccName
| ListOrigin -- An overloaded list
| BracketOrigin -- An overloaded quotation bracket
@@ -640,7 +642,9 @@ pprCtO MCompOrigin = text "a statement in a monad comprehension"
pprCtO ProcOrigin = text "a proc expression"
pprCtO (TypeEqOrigin t1 t2 _ _)= text "a type equality" <+> sep [ppr t1, char '~', ppr t2]
pprCtO AnnOrigin = text "an annotation"
-pprCtO HoleOrigin = text "a use of" <+> quotes (text "_")
+pprCtO (ExprHoleOrigin occ) = text "a use of" <+> quotes (ppr occ)
+pprCtO (TypeHoleOrigin occ) = text "a use of wildcard" <+> quotes (ppr occ)
+pprCtO PatCheckOrigin = text "a pattern-match completeness check"
pprCtO ListOrigin = text "an overloaded list"
pprCtO StaticOrigin = text "a static form"
pprCtO BracketOrigin = text "a quotation bracket"
=====================================
compiler/GHC/Tc/Utils/Monad.hs
=====================================
@@ -98,14 +98,14 @@ module GHC.Tc.Utils.Monad(
chooseUniqueOccTc,
getConstraintVar, setConstraintVar,
emitConstraints, emitStaticConstraints, emitSimple, emitSimples,
- emitImplication, emitImplications, emitInsoluble,
+ emitImplication, emitImplications, emitInsoluble, emitHole,
discardConstraints, captureConstraints, tryCaptureConstraints,
pushLevelAndCaptureConstraints,
pushTcLevelM_, pushTcLevelM, pushTcLevelsM,
getTcLevel, setTcLevel, isTouchableTcM,
getLclTypeEnv, setLclTypeEnv,
traceTcConstraints,
- emitNamedWildCardHoleConstraints, emitAnonWildCardHoleConstraint,
+ emitNamedTypeHole, emitAnonTypeHole,
-- * Template Haskell context
recordThUse, recordThSpliceUse,
@@ -1569,12 +1569,11 @@ emitInsoluble ct
; lie_var <- getConstraintVar
; updTcRef lie_var (`addInsols` unitBag ct) }
-emitInsolubles :: Cts -> TcM ()
-emitInsolubles cts
- | isEmptyBag cts = return ()
- | otherwise = do { traceTc "emitInsolubles" (ppr cts)
- ; lie_var <- getConstraintVar
- ; updTcRef lie_var (`addInsols` cts) }
+emitHole :: Hole -> TcM ()
+emitHole hole
+ = do { traceTc "emitHole" (ppr hole)
+ ; lie_var <- getConstraintVar
+ ; updTcRef lie_var (`addHole` hole) }
-- | Throw out any constraints emitted by the thing_inside
discardConstraints :: TcM a -> TcM a
@@ -1644,34 +1643,28 @@ traceTcConstraints msg
hang (text (msg ++ ": LIE:")) 2 (ppr lie)
}
-emitAnonWildCardHoleConstraint :: TcTyVar -> TcM ()
-emitAnonWildCardHoleConstraint tv
- = do { ct_loc <- getCtLocM HoleOrigin Nothing
- ; emitInsolubles $ unitBag $
- CHoleCan { cc_ev = CtDerived { ctev_pred = mkTyVarTy tv
- , ctev_loc = ct_loc }
- , cc_occ = mkTyVarOcc "_"
- , cc_hole = TypeHole } }
-
-emitNamedWildCardHoleConstraints :: [(Name, TcTyVar)] -> TcM ()
-emitNamedWildCardHoleConstraints wcs
- = do { ct_loc <- getCtLocM HoleOrigin Nothing
- ; emitInsolubles $ listToBag $
- map (do_one ct_loc) wcs }
+emitAnonTypeHole :: TcTyVar -> TcM ()
+emitAnonTypeHole tv
+ = do { ct_loc <- getCtLocM (TypeHoleOrigin occ) Nothing
+ ; let hole = Hole { hole_sort = TypeHole
+ , hole_occ = occ
+ , hole_ty = mkTyVarTy tv
+ , hole_loc = ct_loc }
+ ; emitHole hole }
+ where
+ occ = mkTyVarOcc "_"
+
+emitNamedTypeHole :: (Name, TcTyVar) -> TcM ()
+emitNamedTypeHole (name, tv)
+ = do { ct_loc <- setSrcSpan (nameSrcSpan name) $
+ getCtLocM (TypeHoleOrigin occ) Nothing
+ ; let hole = Hole { hole_sort = TypeHole
+ , hole_occ = occ
+ , hole_ty = mkTyVarTy tv
+ , hole_loc = ct_loc }
+ ; emitHole hole }
where
- do_one :: CtLoc -> (Name, TcTyVar) -> Ct
- do_one ct_loc (name, tv)
- = CHoleCan { cc_ev = CtDerived { ctev_pred = mkTyVarTy tv
- , ctev_loc = ct_loc' }
- , cc_occ = occName name
- , cc_hole = TypeHole }
- where
- real_span = case nameSrcSpan name of
- RealSrcSpan span _ -> span
- UnhelpfulSpan str -> pprPanic "emitNamedWildCardHoleConstraints"
- (ppr name <+> quotes (ftext str))
- -- Wildcards are defined locally, and so have RealSrcSpans
- ct_loc' = setCtLocSpan ct_loc real_span
+ occ = nameOccName name
{- Note [Constraints and errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -41,10 +41,11 @@ module GHC.Tc.Utils.TcMType (
--------------------------------
-- Creating new evidence variables
newEvVar, newEvVars, newDict,
- newWanted, newWanteds, newHoleCt, cloneWanted, cloneWC,
+ newWanted, newWanteds, cloneWanted, cloneWC,
emitWanted, emitWantedEq, emitWantedEvVar, emitWantedEvVars,
emitDerivedEqs,
newTcEvBinds, newNoTcEvBinds, addTcEvBind,
+ emitNewExprHole,
newCoercionHole, fillCoercionHole, isFilledCoercionHole,
unpackCoercionHole, unpackCoercionHole_maybe,
@@ -67,7 +68,7 @@ module GHC.Tc.Utils.TcMType (
--------------------------------
-- Zonking and tidying
zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin,
- tidyEvVar, tidyCt, tidySkolemInfo,
+ tidyEvVar, tidyCt, tidyHole, tidySkolemInfo,
zonkTcTyVar, zonkTcTyVars,
zonkTcTyVarToTyVar, zonkTyVarTyVarPairs,
zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkDTyCoVarSetAndFV,
@@ -193,17 +194,6 @@ newWanted orig t_or_k pty
newWanteds :: CtOrigin -> ThetaType -> TcM [CtEvidence]
newWanteds orig = mapM (newWanted orig Nothing)
--- | Create a new 'CHoleCan' 'Ct'.
-newHoleCt :: HoleSort -> Id -> Type -> TcM Ct
-newHoleCt hole ev ty = do
- loc <- getCtLocM HoleOrigin Nothing
- pure $ CHoleCan { cc_ev = CtWanted { ctev_pred = ty
- , ctev_dest = EvVarDest ev
- , ctev_nosh = WDeriv
- , ctev_loc = loc }
- , cc_occ = getOccName ev
- , cc_hole = hole }
-
----------------------------------------------
-- Cloning constraints
----------------------------------------------
@@ -286,6 +276,18 @@ emitWantedEvVar origin ty
emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
emitWantedEvVars orig = mapM (emitWantedEvVar orig)
+-- | Emit a new wanted expression hole
+emitNewExprHole :: OccName -- of the hole
+ -> Id -- of the evidence
+ -> Type -> TcM ()
+emitNewExprHole occ ev_id ty
+ = do { loc <- getCtLocM (ExprHoleOrigin occ) (Just TypeLevel)
+ ; let hole = Hole { hole_sort = ExprHole ev_id
+ , hole_occ = getOccName ev_id
+ , hole_ty = ty
+ , hole_loc = loc }
+ ; emitHole hole }
+
newDict :: Class -> [TcType] -> TcM DictId
newDict cls tys
= do { name <- newSysName (mkDictOcc (getOccName cls))
@@ -2002,21 +2004,28 @@ zonkWC :: WantedConstraints -> TcM WantedConstraints
zonkWC wc = zonkWCRec wc
zonkWCRec :: WantedConstraints -> TcM WantedConstraints
-zonkWCRec (WC { wc_simple = simple, wc_impl = implic })
+zonkWCRec (WC { wc_simple = simple, wc_impl = implic, wc_holes = holes })
= do { simple' <- zonkSimples simple
; implic' <- mapBagM zonkImplication implic
- ; return (WC { wc_simple = simple', wc_impl = implic' }) }
+ ; holes' <- mapBagM zonkHole holes
+ ; return (WC { wc_simple = simple', wc_impl = implic', wc_holes = holes' }) }
zonkSimples :: Cts -> TcM Cts
zonkSimples cts = do { cts' <- mapBagM zonkCt cts
; traceTc "zonkSimples done:" (ppr cts')
; return cts' }
+zonkHole :: Hole -> TcM Hole
+zonkHole hole@(Hole { hole_ty = ty })
+ = do { ty' <- zonkTcType ty
+ ; return (hole { hole_ty = ty' }) }
+ -- No need to zonk the Id in any ExprHole because we never look at it
+ -- until after the final zonk and desugaring
+
{- Note [zonkCt behaviour]
~~~~~~~~~~~~~~~~~~~~~~~~~~
zonkCt tries to maintain the canonical form of a Ct. For example,
- a CDictCan should stay a CDictCan;
- - a CHoleCan should stay a CHoleCan
- a CIrredCan should stay a CIrredCan with its cc_status flag intact
Why?, for example:
@@ -2026,8 +2035,6 @@ Why?, for example:
don't preserve a canonical form, @expandSuperClasses@ fails to expand
superclasses. This is what happened in #11525.
-- For CHoleCan, once we forget that it's a hole, we can never recover that info.
-
- For CIrredCan we want to see if a constraint is insoluble with insolubleWC
On the other hand, we change CTyEqCan to CNonCanonical, because of all of
@@ -2046,10 +2053,6 @@ creates e.g. a CDictCan where the cc_tyars are /not/ function free.
zonkCt :: Ct -> TcM Ct
-- See Note [zonkCt behaviour]
-zonkCt ct@(CHoleCan { cc_ev = ev })
- = do { ev' <- zonkCtEvidence ev
- ; return $ ct { cc_ev = ev' } }
-
zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
= do { ev' <- zonkCtEvidence ev
; args' <- mapM zonkTcType args
@@ -2262,17 +2265,15 @@ zonkTidyOrigin env orig = return (env, orig)
tidyCt :: TidyEnv -> Ct -> Ct
-- Used only in error reporting
tidyCt env ct
- = ct { cc_ev = tidy_ev env (ctEvidence ct) }
+ = ct { cc_ev = tidy_ev (ctEvidence ct) }
where
- tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence
+ tidy_ev :: CtEvidence -> CtEvidence
-- NB: we do not tidy the ctev_evar field because we don't
-- show it in error messages
- tidy_ev env ctev@(CtGiven { ctev_pred = pred })
- = ctev { ctev_pred = tidyType env pred }
- tidy_ev env ctev@(CtWanted { ctev_pred = pred })
- = ctev { ctev_pred = tidyType env pred }
- tidy_ev env ctev@(CtDerived { ctev_pred = pred })
- = ctev { ctev_pred = tidyType env pred }
+ tidy_ev ctev = ctev { ctev_pred = tidyType env (ctev_pred ctev) }
+
+tidyHole :: TidyEnv -> Hole -> Hole
+tidyHole env h@(Hole { hole_ty = ty }) = h { hole_ty = tidyType env ty }
----------------
tidyEvVar :: TidyEnv -> EvVar -> EvVar
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/57d2bba3908770d5ff94bb1a39585acfd7b7f82c
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/57d2bba3908770d5ff94bb1a39585acfd7b7f82c
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200502/e4d912fd/attachment-0001.html>
More information about the ghc-commits
mailing list