Simon Peyton Jones pushed to branch wip/26805 at Glasgow Haskell Compiler / GHC Commits: 22f6f55e by Simon Peyton Jones at 2026-01-22T17:42:22+00:00 Rejig the NeededEvId stuff again!! Fixes #26772 I hope - - - - - 16 changed files: - compiler/GHC/Core/TyCo/Rep.hs - compiler/GHC/Core/TyCo/Subst.hs - compiler/GHC/Core/TyCo/Tidy.hs - compiler/GHC/Tc/Gen/Expr.hs - compiler/GHC/Tc/Solver/Default.hs - compiler/GHC/Tc/Solver/Equality.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Types/Constraint.hs - compiler/GHC/Tc/Types/Evidence.hs - compiler/GHC/Tc/Utils/Monad.hs - compiler/GHC/Tc/Utils/TcMType.hs - compiler/GHC/Tc/Utils/Unify.hs - compiler/GHC/Tc/Zonk/TcType.hs - compiler/GHC/Tc/Zonk/Type.hs - compiler/GHC/Utils/Trace.hs Changes: ===================================== compiler/GHC/Core/TyCo/Rep.hs ===================================== @@ -1688,11 +1688,9 @@ holes `HoleCo`, which get filled in later. -- | A coercion to be filled in by the type-checker. See Note [Coercion holes] data CoercionHole - = CoercionHole { ch_co_var :: CoVar - -- See Note [Coercion holes] wrinkle (COH2) - - , ch_ref :: IORef (Maybe CoercionPlusHoles) - } + = CH { ch_co_var :: CoVar -- See Note [Coercion holes] wrinkle (COH2) + , ch_ref :: IORef (Maybe CoercionPlusHoles) + } data CoercionPlusHoles = CPH { cph_co :: Coercion @@ -1714,7 +1712,7 @@ instance Data.Data CoercionHole where dataTypeOf _ = mkNoRepType "CoercionHole" instance Outputable CoercionHole where - ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv) + ppr (CH { ch_co_var = cv }) = braces (ppr cv) instance Outputable CoercionPlusHoles where ppr (CPH { cph_co = co, cph_holes = holes }) @@ -1723,7 +1721,7 @@ instance Outputable CoercionPlusHoles where , text "cph_holes =" <+> ppr holes ]) instance Uniquable CoercionHole where - getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv + getUnique (CH { ch_co_var = cv }) = getUnique cv -- | A CoHoleSet stores a set of CoercionHoles that have been used to rewrite ===================================== compiler/GHC/Core/TyCo/Subst.hs ===================================== @@ -892,8 +892,7 @@ subst_co subst co in cos' `seqList` cos' -- See Note [Substituting in a coercion hole] - go_hole h@(CoercionHole { ch_co_var = cv }) - = h { ch_co_var = updateVarType go_ty cv } + go_hole h@(CH { ch_co_var = cv }) = h { ch_co_var = updateVarType go_ty cv } -- | Perform a substitution within a 'DVarSet' of free variables, -- returning the shallow free coercion variables. ===================================== compiler/GHC/Core/TyCo/Tidy.hs ===================================== @@ -357,7 +357,7 @@ tidyCo env co go_cv cv = tidyTyCoVarOcc env cv - go_hole (CoercionHole cv r) = (CoercionHole $! go_cv cv) r + go_hole (CH cv r) = (CH $! go_cv cv) r -- Tidy even the holes; tidied types should have tidied kinds tidyCos :: TidyEnv -> [Coercion] -> [Coercion] ===================================== compiler/GHC/Tc/Gen/Expr.hs ===================================== @@ -199,6 +199,9 @@ tcPolyExprCheck expr res_ty -> TcM (HsExpr GhcTc) outer_skolemise (Left ty) thing_inside = do { (wrap, expr') <- tcSkolemiseExpectedType ty thing_inside + ; traceTc "outer_skol" (vcat [ text "wrap" <+> ppr wrap + , text "expr'" <+> ppr expr' + , text "wrapped" <+> ppr (mkHsWrap wrap expr') ]) ; return (mkHsWrap wrap expr') } outer_skolemise (Right sig) thing_inside = do { (wrap, expr') <- tcSkolemiseCompleteSig sig thing_inside ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -272,10 +272,9 @@ unsatisfiableEv_maybe v = (v,) <$> isUnsatisfiableCt_maybe (idType v) -- solve all the other Wanted constraints, including those nested within -- deeper implications. solveImplicationUsingUnsatGiven :: (EvVar, Type) -> Implication -> TcS Implication -solveImplicationUsingUnsatGiven - unsat_given@(given_ev,_) +solveImplicationUsingUnsatGiven unsat_given impl@(Implic { ic_wanted = wtd, ic_tclvl = tclvl, ic_binds = ev_binds_var - , ic_need_implic = inner, ic_info = skol_info }) + , ic_info = skol_info }) | isCoEvBindsVar ev_binds_var -- We can't use Unsatisfiable evidence in kinds. -- See Note [Coercion evidence only] in GHC.Tc.Types.Evidence. @@ -283,9 +282,7 @@ solveImplicationUsingUnsatGiven | otherwise = do { wcs <- nestImplicTcS skol_info ev_binds_var tclvl $ go_wc wtd ; setImplicationStatus $ - impl { ic_wanted = wcs - , ic_need_implic = inner `extendEvNeedSet` given_ev } } - -- Record that the Given is needed; I'm not certain why + impl { ic_wanted = wcs } } where go_wc :: WantedConstraints -> TcS WantedConstraints go_wc wc@(WC { wc_simple = wtds, wc_impl = impls }) ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -601,7 +601,7 @@ can_eq_nc_forall ev eq_rel s1 s2 -- they are kept alive by `neededEvVars`. Admittedly they are free in `all_co`, -- but only if we zonk it, which `neededEvVars` does not do (see test T7196). ev_binds_var <- getTcEvBindsVar - ; updTcEvBinds ev_binds_var nested_ev_binds_var + ; combineTcEvBinds ev_binds_var nested_ev_binds_var ; setWantedEq orig_dest (CPH { cph_co = all_co, cph_holes = emptyCoHoleSet }) -- emptyCoHoleSet: fully solved, so all_co has no holes ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -15,7 +15,7 @@ module GHC.Tc.Solver.Monad ( failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS, runTcSEqualities, nestTcS, nestImplicTcS, tryShortCutTcS, nestFunDepsTcS, - setEvBindsTcS, setTcLevelTcS, updTcEvBinds, + setEvBindsTcS, setTcLevelTcS, selectNextWorkItem, getWorkList, @@ -58,7 +58,7 @@ module GHC.Tc.Solver.Monad ( getInstEnvs, getFamInstEnvs, -- Getting the environments getTopEnv, getGblEnv, getLclEnv, setSrcSpan, getTcEvBindsVar, getTcLevel, - getTcEvTyCoVars, getTcEvBindsMap, setTcEvBindsMap, + getTcEvBindsMap, setTcEvBindsMap, getTcEvBindsState, combineTcEvBinds, tcLookupClass, tcLookupId, tcLookupTyCon, -- Inerts @@ -1140,7 +1140,7 @@ csTraceTcM mk_doc {-# INLINE csTraceTcM #-} -- see Note [INLINE conditional tracing utilities] runTcS :: TcS a -- What to run - -> TcM (a, EvBindMap) + -> TcM (a, EvBindsMap) runTcS tcs = do { ev_binds_var <- TcM.newTcEvBinds ; res <- runTcSWithEvBinds ev_binds_var tcs @@ -1222,7 +1222,7 @@ runTcSWithEvBinds' mode ev_binds_var thing_inside ---------------------------- #if defined(DEBUG) -checkForCyclicBinds :: EvBindMap -> TcM () +checkForCyclicBinds :: EvBindsMap -> TcM () checkForCyclicBinds ev_binds_map | null cycles = return () @@ -1380,18 +1380,24 @@ tryShortCutTcS (TcS thing_inside) , tcs_inerts = new_inert_var , tcs_worklist = new_wl_var } - ; TcM.traceTc "tryTcS {" $ + ; TcM.traceTc "tryShortCutTcS {" $ vcat [ text "old_ev_binds:" <+> ppr old_ev_binds_var , text "new_ev_binds:" <+> ppr new_ev_binds_var , ppr old_inerts ] ; solved <- thing_inside nest_env - ; TcM.traceTc "tryTcS }" (ppr solved) + ; TcM.traceTc "tryShortCutTcS }" (ppr solved) ; if not solved then return False else do { -- Successfully solved -- Add the new bindings to the existing ones - ; TcM.updTcEvBinds old_ev_binds_var new_ev_binds_var + ; old_ebvs <- TcM.readTcRef (ebv_binds old_ev_binds_var) + + ; TcM.combineTcEvBinds old_ev_binds_var new_ev_binds_var + + ; final_ebvs <- TcM.readTcRef (ebv_binds old_ev_binds_var) + ; TcM.traceTc "update" (text "old" <+> ppr old_ebvs $$ + text "new" <+> ppr final_ebvs) -- Update the existing inert set ; new_inerts <- TcM.readTcRef new_inert_var @@ -1465,21 +1471,21 @@ getTcEvBindsVar = TcS (return . tcs_ev_binds) getTcLevel :: TcS TcLevel getTcLevel = wrapTcS TcM.getTcLevel -getTcEvTyCoVars :: EvBindsVar -> TcS [TcCoercion] -getTcEvTyCoVars ev_binds_var - = wrapTcS $ TcM.getTcEvTyCoVars ev_binds_var +getTcEvBindsState :: EvBindsVar -> TcS EvBindsState +getTcEvBindsState ev_binds_var + = wrapTcS $ TcM.getTcEvBindsState ev_binds_var -getTcEvBindsMap :: EvBindsVar -> TcS EvBindMap +getTcEvBindsMap :: EvBindsVar -> TcS EvBindsMap getTcEvBindsMap ev_binds_var = wrapTcS $ TcM.getTcEvBindsMap ev_binds_var -setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS () +setTcEvBindsMap :: EvBindsVar -> EvBindsMap -> TcS () setTcEvBindsMap ev_binds_var binds = wrapTcS $ TcM.setTcEvBindsMap ev_binds_var binds -updTcEvBinds :: EvBindsVar -> EvBindsVar -> TcS () -updTcEvBinds evb nested_evb - = wrapTcS $ TcM.updTcEvBinds evb nested_evb +combineTcEvBinds :: EvBindsVar -> EvBindsVar -> TcS () +combineTcEvBinds evb nested_evb + = wrapTcS $ TcM.combineTcEvBinds evb nested_evb getDefaultInfo :: TcS (DefaultEnv, Bool) getDefaultInfo = wrapTcS TcM.tcGetDefaultTys @@ -2029,12 +2035,9 @@ setWantedDict dest canonical tm HoleDest h -> pprPanic "setWantedEq: HoleDest" (ppr h) fillCoercionHole :: CoercionHole -> CoercionPlusHoles -> TcS () -fillCoercionHole hole co_plus_holes@(CPH { cph_co = co }) +fillCoercionHole hole co_plus_holes = do { ev_binds_var <- getTcEvBindsVar - ; wrapTcS $ do { -- Record usage of the free vars of this coercion - TcM.updTcRef (ebv_tcvs ev_binds_var) (co :) - ; -- Fill the hole - TcM.fillCoercionHole hole co_plus_holes } + ; wrapTcS $ TcM.addTcEvCoBind ev_binds_var hole co_plus_holes ; kickOutAfterFillingCoercionHole hole co_plus_holes } newTcEvBinds :: TcS EvBindsVar ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -33,7 +33,6 @@ import qualified GHC.Tc.Zonk.TcType as TcM import GHC.Core.Predicate import GHC.Core.Reduction import GHC.Core.Coercion -import GHC.Core.TyCo.FVs( coVarsOfCos ) import GHC.Core.Class( classHasSCs ) import GHC.Types.Id( idType ) @@ -432,12 +431,10 @@ solveImplication imp@(Implic { ic_tclvl = tclvl , ic_wanted = final_wanted }) ; evbinds <- TcS.getTcEvBindsMap ev_binds_var - ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var ; traceTcS "solveImplication end }" $ vcat [ text "has_given_eqs =" <+> ppr has_given_eqs , text "res_implic =" <+> ppr res_implic - , text "implication evbinds =" <+> ppr (evBindMapBinds evbinds) - , text "implication tvcs =" <+> ppr tcvs ] + , text "evbinds =" <+> ppr evbinds ] ; return res_implic } @@ -460,30 +457,27 @@ setImplicationStatus :: Implication -> TcS Implication -- * Prune unnecessary evidence bindings -- * Prune unnecessary child implications -- Precondition: the ic_status field is not already IC_Solved -setImplicationStatus implic@(Implic { ic_status = old_status - , ic_info = info - , ic_wanted = wc }) - = assertPpr (not (isSolvedStatus old_status)) (ppr info) $ - -- Precondition: we only set the status if it is not already solved - do { traceTcS "setImplicationStatus {" (ppr implic) - - ; let solved = isSolvedWC wc - ; new_implic <- neededEvVars implic - ; bad_telescope <- if solved then checkBadTelescope implic - else return False - - ; let new_status | insolubleWC wc = IC_Insoluble - | not solved = IC_Unsolved - | bad_telescope = IC_BadTelescope - | otherwise = IC_Solved { ics_dead = dead_givens } - dead_givens = findRedundantGivens new_implic - new_wc = pruneImplications wc - - final_implic = new_implic { ic_status = new_status - , ic_wanted = new_wc } - - ; traceTcS "setImplicationStatus }" (ppr final_implic) - ; return final_implic } +setImplicationStatus implic@(Implic { ic_wanted = wc }) + | insolubleWC wc + = do { traceTcS "setImplicationStatus:insoluble {" (ppr implic) + ; return (implic { ic_status = IC_Insoluble }) } + + | not (isSolvedWC wc) + = -- Precondition: we only set the status if it is not /already/ solved + do { traceTcS "setImplicationStatus:in progress {" (ppr implic) + ; return (implic { ic_status = IC_Unsolved }) } + + | otherwise -- The Wanteds are all solved + = do { traceTcS "setImplicationStatus:solved {" (ppr implic) + ; bad_telescope <- checkBadTelescope implic + ; if bad_telescope + then return (implic { ic_status = IC_BadTelescope }) + else + + do { solved_status <- computeSolvedStatus implic + ; let pruned_wc = pruneImplications wc + ; return (implic { ic_status = solved_status + , ic_wanted = pruned_wc }) } } pruneImplications :: WantedConstraints -> WantedConstraints -- We have now recorded the `ic_need` variables of the child @@ -502,8 +496,8 @@ pruneImplications wc@(WC { wc_impl = implics }) | otherwise = True -- Otherwise, keep it -findRedundantGivens :: Implication -> [EvVar] -findRedundantGivens (Implic { ic_info = info, ic_need = need, ic_given = givens }) +findRedundantGivens :: SkolemInfoAnon -> NeededEvIds -> [EvVar] -> [EvVar] +findRedundantGivens info need givens | not (warnRedundantGivens info) -- Don't report redundant constraints at all = [] -- See (TRC4) of Note [Tracking redundant constraints] @@ -520,9 +514,8 @@ findRedundantGivens (Implic { ic_info = info, ic_need = need, ic_given = givens unused_givens = filterOut is_used givens - needed_givens_ignoring_default_methods = ens_fvs need is_used given = is_type_error given - || given `elemVarSet` needed_givens_ignoring_default_methods + || given `elemVarSet` need || (in_instance_decl && is_improving (idType given)) minimal_givens = mkMinimalBySCs evVarPred givens -- See (TRC2) @@ -611,113 +604,105 @@ checkBadTelescope (Implic { ic_info = info | otherwise = go (later_skols `extendVarSet` one_skol) earlier_skols -neededEvVars :: Implication -> TcS Implication --- Find all the evidence variables that are "needed", --- /and/ delete dead evidence bindings +computeSolvedStatus :: Implication -> TcS ImplicStatus +-- Given a fully-solved implication, +-- - Figure out the right IC_Solved fields +-- - Delete unused evidence bindings -- -- See Note [Tracking redundant constraints] -- See Note [Delete dead Given evidence bindings] --- --- - Start from initial_seeds (from nested implications) --- --- - Add free vars of RHS of all Wanted evidence bindings --- and coercion variables accumulated in tcvs (all Wanted) --- --- - Generate 'needed', the needed set of EvVars, by doing transitive --- closure through Given bindings --- e.g. Needed {a,b} --- Given a = sc_sel a2 --- Then a2 is needed too --- --- - Prune out all Given bindings that are not needed - -neededEvVars implic@(Implic { ic_info = info +computeSolvedStatus (Implic { ic_info = info , ic_binds = ev_binds_var - , ic_wanted = WC { wc_impl = implics } - , ic_need_implic = old_need_implic -- See (TRC1) - }) - = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var - ; used_cos <- TcS.getTcEvTyCoVars ev_binds_var - - ; let -- Find the variables needed by `implics` - new_need_implic@(ENS { ens_dms = dm_seeds, ens_fvs = other_seeds }) - = foldr add_implic old_need_implic implics - -- Start from old_need_implic! See (TRC1) - - -- Get the variables needed by the solved bindings - -- (It's OK to use a non-deterministic fold here - -- because add_wanted is commutative.) - used_covars = coVarsOfCos used_cos - seeds_w = nonDetStrictFoldEvBindMap add_wanted used_covars ev_binds - - need_ignoring_dms = findNeededGivenEvVars ev_binds (other_seeds `unionVarSet` seeds_w) - need_from_dms = findNeededGivenEvVars ev_binds dm_seeds - need_full = need_ignoring_dms `unionVarSet` need_from_dms - - -- `need`: the Givens from outer scopes that are used in this implication - -- is_dm_skol: see (TRC5) - need | is_dm_skol info = ENS { ens_dms = trim ev_binds need_full - , ens_fvs = emptyVarSet } - | otherwise = ENS { ens_dms = trim ev_binds need_from_dms - , ens_fvs = trim ev_binds need_ignoring_dms } - - -- Delete dead Given evidence bindings + , ic_given = givens + , ic_wanted = WC { wc_impl = implics } }) + = do { ev_binds_state <- TcS.getTcEvBindsState ev_binds_var + + ; let EBS { ebs_binds = ev_binds, ebs_needs = local_needs } = ev_binds_state + + -- Gather the raw needed EvIds, from the + -- current evidence bindings `local_needs`, and the `implics` + (need_dm, need_non_dm) = foldr add_implic (emptyVarSet, local_needs) implics + + -- Do transitive closure through the evidence bindings + -- and delete all EvIds bound by the bindings + need_dm1 = findNeededGivenEvVars ev_binds need_dm + need_non_dm1 = findNeededGivenEvVars ev_binds need_non_dm + + -- Compute the redundant Givens + dead_givens = findRedundantGivens info need_non_dm1 givens + + -- Delete variables bound by ev_binds or by givens + need_dm2 = trim_needs need_dm1 + need_non_dm2 = trim_needs need_non_dm1 + + trim_needs :: NeededEvIds -> NeededEvIds + trim_needs needs = (needs `varSetMinusEvBindsMap` ev_binds) + `delVarSetList` givens + + -- Prune dead Given evidence bindings -- See Note [Delete dead Given evidence bindings] - ; let live_ev_binds = filterEvBindMap (needed_ev_bind need_full) ev_binds - ; TcS.setTcEvBindsMap ev_binds_var live_ev_binds - - ; traceTcS "neededEvVars" $ - vcat [ text "old_need_implic:" <+> ppr old_need_implic - , text "new_need_implic:" <+> ppr new_need_implic - , text "used_covars:" <+> ppr used_covars - , text "need_ignoring_dms:" <+> ppr need_ignoring_dms - , text "need_from_dms:" <+> ppr need_from_dms - , text "need:" <+> ppr need + ; let need_full = need_dm1 `unionVarSet` need_non_dm1 + pruned_ev_binds = filterEvBindsMap (keep_ev_bind need_full) ev_binds + ; TcS.setTcEvBindsMap ev_binds_var pruned_ev_binds + + ; traceTcS "computeSolvedStatus" $ + vcat [ text "local_needs:" <+> ppr local_needs + , text "need_dm:" <+> ppr need_dm + , text "need_non_dm:" <+> ppr need_non_dm + , text "need_dm1:" <+> ppr need_dm1 + , text "need_non_dm1:" <+> ppr need_non_dm1 + , text "need_dm2:" <+> ppr need_dm2 + , text "need_non_dm2:" <+> ppr need_non_dm2 , text "ev_binds:" <+> ppr ev_binds - , text "live_ev_binds:" <+> ppr live_ev_binds ] - ; return (implic { ic_need = need - , ic_need_implic = new_need_implic }) } - where - trim :: EvBindMap -> VarSet -> VarSet - -- Delete variables bound by Givens or bindings - trim ev_binds needs = needs `varSetMinusEvBindMap` ev_binds + , text "deleted ev_binds:" + <+> ppr (filterEvBindsMap (not . keep_ev_bind need_full) ev_binds) ] - add_implic :: Implication -> EvNeedSet -> EvNeedSet - add_implic (Implic { ic_given = givens, ic_need = need }) acc - = (need `delGivensFromEvNeedSet` givens) `unionEvNeedSet` acc + ; if is_dm_skol info + then return (IC_Solved { ics_dead = dead_givens + , ics_dm = need_dm2 `unionVarSet` need_non_dm2 + , ics_non_dm = emptyVarSet }) - needed_ev_bind needed (EvBind { eb_lhs = ev_var, eb_info = info }) + else return (IC_Solved { ics_dead = dead_givens + , ics_dm = need_dm2 + , ics_non_dm = need_non_dm2 }) } + where + add_implic :: Implication -> (NeededEvIds, NeededEvIds) -> (NeededEvIds, NeededEvIds) + add_implic (Implic { ic_status = status}) (dm2, non_dm2) + | IC_Solved { ics_dm = dm1, ics_non_dm = non_dm1 } <- status + = (dm1 `unionVarSet` dm2, non_dm1 `unionVarSet` non_dm2) + | otherwise + = pprPanic "computeSolvedStatus" (ppr implics) + + keep_ev_bind :: NeededEvIds -> EvBind -> Bool + -- False => we can discard this unused Given evidence binding + -- We always keep all the Wanted bindings + keep_ev_bind needed (EvBind { eb_lhs = ev_var, eb_info = info }) | EvBindGiven{} <- info = ev_var `elemVarSet` needed | otherwise = True -- Keep all wanted bindings - add_wanted :: EvBind -> VarSet -> VarSet - add_wanted (EvBind { eb_info = info, eb_rhs = rhs }) needs - | EvBindGiven{} <- info = needs -- Add the rhs vars of the Wanted bindings only - | otherwise = nestedEvIdsOfTerm rhs `unionVarSet` needs - is_dm_skol :: SkolemInfoAnon -> Bool is_dm_skol (MethSkol _ is_dm) = is_dm is_dm_skol _ = False -findNeededGivenEvVars :: EvBindMap -> VarSet -> VarSet +findNeededGivenEvVars :: EvBindsMap -> NeededEvIds -> NeededEvIds -- Find all the Given evidence needed by seeds, -- looking transitively through bindings for Givens (only) findNeededGivenEvVars ev_binds seeds = transCloVarSet also_needs seeds where - also_needs :: VarSet -> VarSet - also_needs needs = nonDetStrictFoldUniqSet add emptyVarSet needs - -- It's OK to use a non-deterministic fold here because we immediately - -- forget about the ordering by creating a set - - add :: Var -> VarSet -> VarSet - add v needs - | Just ev_bind <- lookupEvBind ev_binds v - , EvBind { eb_info = EvBindGiven, eb_rhs = rhs } <- ev_bind - -- Look at Given bindings only - = nestedEvIdsOfTerm rhs `unionVarSet` needs - | otherwise - = needs + also_needs :: VarSet -> VarSet + also_needs needs = nonDetStrictFoldUniqSet add emptyVarSet needs + -- It's OK to use a non-deterministic fold here because we immediately + -- forget about the ordering by creating a set + + add :: Var -> VarSet -> VarSet + add v needs + | Just ev_bind <- lookupEvBind ev_binds v + , EvBind { eb_info = EvBindGiven, eb_rhs = rhs } <- ev_bind + -- Look at Given bindings only + = nestedEvIdsOfTerm rhs `unionVarSet` needs + | otherwise + = needs ------------------------------------------------- simplifyDelayedErrors :: Bag DelayedError -> TcS (Bag DelayedError) @@ -949,7 +934,7 @@ Wrinkles: and because of the degnerate instance for `Show (T a)`, we don't need the `Eq a` constraint. But we don't want to report it as redundant! -(TRC5) Consider this (#25992), where `op2` has a default method +(TRC5) Default methods. Consider this (#25992), where `op2` has a default method class C a where { op1, op2 :: a -> a ; op2 = op1 . op1 } instance C a => C [a] where @@ -960,10 +945,12 @@ Wrinkles: $dmop2 = op1 . op1 $fCList :: forall a. C a => C [a] - $fCList @a (d::C a) = MkC (\(x:a).x) ($dmop2 @a d) + $fCList @a (d::C a) = MkC (\(x:a).x) + ($dmop2 @[a] ($fCList @a d)) - Notice that `d` gets passed to `$dmop`: it is "needed". But it's only - /really/ needed if some /other/ method (in this case `op1`) uses it. + Notice that `d` gets passed, indirectly to `$dmop`: it appears to be + "needed". But it's only /really/ needed if some /other/ method or + superclass (in this case `op1`) uses it. So, rather than one set of "needed Givens" we use `EvNeedSet` to track a /pair/ of sets: @@ -1645,10 +1632,12 @@ solveWantedQCI mode ct@(CQuantCan (QCI { qci_ev = ev, qci_tvs = tvs -- carrying a record of which evidence variables are used -- See Note [Free vars of EvFun] in GHC.Tc.Types.Evidence do { setWantedDict dest EvCanonical $ - EvFun { et_tvs = skol_tvs, et_given = given_ev_vars + EvFun { et_tvs = skol_tvs + , et_given = given_ev_vars , et_binds = TcEvBinds ev_binds_var - , et_body = wantedCtEvEvId wanted_ev } + , et_body = wantedCtEvEvId wanted_ev } + ; traceTcS "solveWantedQCI" (ppr imp') ; return (Right imp') } } ===================================== compiler/GHC/Tc/Types/Constraint.hs ===================================== @@ -65,7 +65,6 @@ module GHC.Tc.Types.Constraint ( ImplicStatus(..), isInsolubleStatus, isSolvedStatus, UserGiven, getGivensFromImplics, HasGivenEqs(..), checkImplicationInvariants, - EvNeedSet(..), emptyEvNeedSet, unionEvNeedSet, extendEvNeedSet, delGivensFromEvNeedSet, -- CtLocEnv CtLocEnv(..), setCtLocEnvLoc, setCtLocEnvLvl, getCtLocEnvLoc, getCtLocEnvLvl, ctLocEnvInGeneratedCode, @@ -1564,45 +1563,9 @@ data Implication ic_binds :: EvBindsVar, -- Points to the place to fill in the -- abstraction and bindings. - -- The ic_need fields keep track of which Given evidence - -- is used by this implication or its children - -- See Note [Tracking redundant constraints] - -- NB: these sets include stuff used by fully-solved nested implications - -- that have since been discarded - ic_need :: EvNeedSet, -- All needed Given evidence, from this implication - -- or outer ones - -- That is, /after/ deleting the binders of ic_binds, - -- but /before/ deleting ic_givens - - ic_need_implic :: EvNeedSet, -- Union of of the ic_need of all implications in ic_wanted - -- /including/ any fully-solved implications that have been - -- discarded by `pruneImplications`. This discarding is why - -- we need to keep this field in the first place. - ic_status :: ImplicStatus } -data EvNeedSet = ENS { ens_dms :: VarSet -- Needed only by default methods - , ens_fvs :: VarSet -- Needed by things /other than/ default methods - -- See (TRC5) in Note [Tracking redundant constraints] - } - -emptyEvNeedSet :: EvNeedSet -emptyEvNeedSet = ENS { ens_dms = emptyVarSet, ens_fvs = emptyVarSet } - -unionEvNeedSet :: EvNeedSet -> EvNeedSet -> EvNeedSet -unionEvNeedSet (ENS { ens_dms = dm1, ens_fvs = fv1 }) - (ENS { ens_dms = dm2, ens_fvs = fv2 }) - = ENS { ens_dms = dm1 `unionVarSet` dm2, ens_fvs = fv1 `unionVarSet` fv2 } - -extendEvNeedSet :: EvNeedSet -> Var -> EvNeedSet -extendEvNeedSet ens@(ENS { ens_fvs = fvs }) v = ens { ens_fvs = fvs `extendVarSet` v } - -delGivensFromEvNeedSet :: EvNeedSet -> [Var] -> EvNeedSet -delGivensFromEvNeedSet (ENS { ens_dms = dms, ens_fvs = fvs }) givens - = ENS { ens_dms = dms `delVarSetList` givens - , ens_fvs = fvs `delVarSetList` givens } - implicationPrototype :: CtLocEnv -> Implication implicationPrototype ct_loc_env = Implic { -- These fields must be initialised @@ -1619,14 +1582,21 @@ implicationPrototype ct_loc_env , ic_given = [] , ic_wanted = emptyWC , ic_given_eqs = MaybeGivenEqs - , ic_status = IC_Unsolved - , ic_need = emptyEvNeedSet - , ic_need_implic = emptyEvNeedSet } + , ic_status = IC_Unsolved } data ImplicStatus = IC_Solved -- All wanteds in the tree are solved, all the way down - { ics_dead :: [EvVar] } -- Subset of ic_given that are not needed - -- See Note [Tracking redundant constraints] in GHC.Tc.Solver + { ics_dead :: [EvVar] -- Subset of ic_given that are not needed + + , ics_dm :: NeededEvIds -- Enclosing Given EvIds that are needed by + -- calls to default methods (typically empty) + + , ics_non_dm :: NeededEvIds -- Enclosing Given EvIds that are needed, other than + -- calls to default methods + } + -- Reporting redundant givens: use ics_non_dm + -- Pruning evidence bindings: use ics_dm `union` ics_non_dm + -- See Note [Tracking redundant constraints] in GHC.Tc.Solver | IC_Insoluble -- At least one insoluble Wanted constraint in the tree @@ -1715,7 +1685,6 @@ instance Outputable Implication where , ic_given = given, ic_given_eqs = given_eqs , ic_wanted = wanted, ic_status = status , ic_binds = binds - , ic_need = need, ic_need_implic = need_implic , ic_info = info }) = hang (text "Implic" <+> lbrace) 2 (sep [ text "TcLevel =" <+> ppr tclvl @@ -1725,21 +1694,17 @@ instance Outputable Implication where , hang (text "Given =") 2 (pprEvVars given) , hang (text "Wanted =") 2 (ppr wanted) , text "Binds =" <+> ppr binds - , text "need =" <+> ppr need - , text "need_implic =" <+> ppr need_implic , pprSkolInfo info ] <+> rbrace) -instance Outputable EvNeedSet where - ppr (ENS { ens_dms = dms, ens_fvs = fvs }) - = text "ENS" <> braces (sep [text "ens_dms =" <+> ppr dms - , text "ens_fvs =" <+> ppr fvs]) - instance Outputable ImplicStatus where ppr IC_Insoluble = text "Insoluble" ppr IC_BadTelescope = text "Bad telescope" ppr IC_Unsolved = text "Unsolved" - ppr (IC_Solved { ics_dead = dead }) - = text "Solved" <+> (braces (text "Dead givens =" <+> ppr dead)) + ppr (IC_Solved { ics_dead = dead, ics_dm = dm, ics_non_dm = non_dm }) + = text "Solved" <> (braces $ + vcat [ text "Dead givens =" <+> ppr dead + , text "need_dm =" <+> ppr dm + , text "need_non_dm =" <+> ppr non_dm ]) checkTelescopeSkol :: SkolemInfoAnon -> Bool -- See Note [Checking telescopes] ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -14,14 +14,15 @@ module GHC.Tc.Types.Evidence ( optSubTypeHsWrapper, -- * Evidence bindings - TcEvBinds(..), EvBindsVar(..), - EvBindMap(..), emptyEvBindMap, extendEvBinds, unionEvBindMap, + TcEvBinds(..), EvBindsVar(..), NeededEvIds, + EvBindsState(..), emptyEvBindsState, unionEvBindsState, addCoVarsEBS, + EvBindsMap(..), emptyEvBindsMap, extendEvBinds, unionEvBindsMap, lookupEvBind, evBindMapBinds, - foldEvBindMap, nonDetStrictFoldEvBindMap, - filterEvBindMap, - isEmptyEvBindMap, + foldEvBindsMap, nonDetStrictFoldEvBindsMap, + filterEvBindsMap, + isEmptyEvBindsMap, evBindMapToVarSet, - varSetMinusEvBindMap, + varSetMinusEvBindsMap, EvBindInfo(..), EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind, evBindVar, isCoEvBindsVar, @@ -725,12 +726,12 @@ data EvBindsVar ebv_uniq :: Unique, -- The Unique is for debug printing only - ebv_binds :: IORef EvBindMap, + ebv_binds :: IORef EvBindsState -- The main payload: the value-level evidence bindings -- (dictionaries etc) -- Some Given, some Wanted - ebv_tcvs :: IORef [TcCoercion] +-- ebv_needs :: IORef VarSet -- When we solve a Wanted by filling in a CoercionHole, it is as -- if we were adding an evidence binding -- co_hole := coercion @@ -745,10 +746,35 @@ data EvBindsVar | CoEvBindsVar { -- See Note [Coercion evidence only] -- See above for comments on ebv_uniq, ebv_tcvs - ebv_uniq :: Unique, - ebv_tcvs :: IORef [TcCoercion] + ebv_uniq :: Unique, + ebv_needs :: IORef NeededEvIds } +type NeededEvIds = VarSet + +data EvBindsState = EBS { ebs_binds :: EvBindsMap + , ebs_needs :: NeededEvIds } + +emptyEvBindsState :: EvBindsState +emptyEvBindsState = EBS { ebs_binds = emptyEvBindsMap + , ebs_needs = emptyVarSet } + +unionEvBindsState :: EvBindsState -> EvBindsState -> EvBindsState +unionEvBindsState (EBS { ebs_binds = bs1, ebs_needs = n1 }) + (EBS { ebs_binds = bs2, ebs_needs = n2 }) + = EBS { ebs_binds = bs1 `unionEvBindsMap` bs2 + , ebs_needs = n1 `unionVarSet` n2 } + +addCoVarsEBS :: VarSet -> EvBindsState -> EvBindsState +addCoVarsEBS n1 ebs@(EBS { ebs_needs = n2 }) + = ebs { ebs_needs = n1 `unionVarSet` n2 } + +instance Outputable EvBindsState where + ppr (EBS { ebs_binds = bs, ebs_needs = needs }) + = text "EBS" <> (braces $ + sep [ text "needs =" <+> ppr needs + , text "binds =" <+> ppr bs ]) + instance Data.Data TcEvBinds where -- Placeholder; we can't traverse into TcEvBinds toConstr _ = abstractConstr "TcEvBinds" @@ -778,8 +804,8 @@ isCoEvBindsVar (CoEvBindsVar {}) = True isCoEvBindsVar (EvBindsVar {}) = False ----------------- -newtype EvBindMap - = EvBindMap { +newtype EvBindsMap + = EvBindsMap { ev_bind_varenv :: DVarEnv EvBind } -- Map from evidence variables to evidence terms -- We use @DVarEnv@ here to get deterministic ordering when we @@ -801,50 +827,50 @@ newtype EvBindMap -- See Note [Deterministic UniqFM] in GHC.Types.Unique.DFM for explanation why -- @UniqFM@ can lead to nondeterministic order. -emptyEvBindMap :: EvBindMap -emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyDVarEnv } +emptyEvBindsMap :: EvBindsMap +emptyEvBindsMap = EvBindsMap { ev_bind_varenv = emptyDVarEnv } -extendEvBinds :: EvBindMap -> EvBind -> EvBindMap +extendEvBinds :: EvBindsMap -> EvBind -> EvBindsMap extendEvBinds bs ev_bind - = EvBindMap { ev_bind_varenv = extendDVarEnv (ev_bind_varenv bs) + = EvBindsMap { ev_bind_varenv = extendDVarEnv (ev_bind_varenv bs) (eb_lhs ev_bind) ev_bind } -- | Union two evidence binding maps -unionEvBindMap :: EvBindMap -> EvBindMap -> EvBindMap -unionEvBindMap (EvBindMap env1) (EvBindMap env2) = - EvBindMap { ev_bind_varenv = plusDVarEnv env1 env2 } +unionEvBindsMap :: EvBindsMap -> EvBindsMap -> EvBindsMap +unionEvBindsMap (EvBindsMap env1) (EvBindsMap env2) = + EvBindsMap { ev_bind_varenv = plusDVarEnv env1 env2 } -isEmptyEvBindMap :: EvBindMap -> Bool -isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m +isEmptyEvBindsMap :: EvBindsMap -> Bool +isEmptyEvBindsMap (EvBindsMap m) = isEmptyDVarEnv m -lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind +lookupEvBind :: EvBindsMap -> EvVar -> Maybe EvBind lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs) -evBindMapBinds :: EvBindMap -> Bag EvBind -evBindMapBinds = foldEvBindMap consBag emptyBag +evBindMapBinds :: EvBindsMap -> Bag EvBind +evBindMapBinds = foldEvBindsMap consBag emptyBag -foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a -foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs) +foldEvBindsMap :: (EvBind -> a -> a) -> a -> EvBindsMap -> a +foldEvBindsMap k z bs = foldDVarEnv k z (ev_bind_varenv bs) -- See Note [Deterministic UniqFM] to learn about nondeterminism. -- If you use this please provide a justification why it doesn't introduce -- nondeterminism. -nonDetStrictFoldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a -nonDetStrictFoldEvBindMap k z bs = nonDetStrictFoldDVarEnv k z (ev_bind_varenv bs) +nonDetStrictFoldEvBindsMap :: (EvBind -> a -> a) -> a -> EvBindsMap -> a +nonDetStrictFoldEvBindsMap k z bs = nonDetStrictFoldDVarEnv k z (ev_bind_varenv bs) -filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap -filterEvBindMap k (EvBindMap { ev_bind_varenv = env }) - = EvBindMap { ev_bind_varenv = filterDVarEnv k env } +filterEvBindsMap :: (EvBind -> Bool) -> EvBindsMap -> EvBindsMap +filterEvBindsMap k (EvBindsMap { ev_bind_varenv = env }) + = EvBindsMap { ev_bind_varenv = filterDVarEnv k env } -evBindMapToVarSet :: EvBindMap -> VarSet -evBindMapToVarSet (EvBindMap dve) = unsafeUFMToUniqSet (mapUFM evBindVar (udfmToUfm dve)) +evBindMapToVarSet :: EvBindsMap -> VarSet +evBindMapToVarSet (EvBindsMap dve) = unsafeUFMToUniqSet (mapUFM evBindVar (udfmToUfm dve)) -varSetMinusEvBindMap :: VarSet -> EvBindMap -> VarSet -varSetMinusEvBindMap vs (EvBindMap dve) = vs `uniqSetMinusUDFM` dve +varSetMinusEvBindsMap :: VarSet -> EvBindsMap -> VarSet +varSetMinusEvBindsMap vs (EvBindsMap dve) = vs `uniqSetMinusUDFM` dve -instance Outputable EvBindMap where - ppr (EvBindMap m) = ppr m +instance Outputable EvBindsMap where + ppr (EvBindsMap m) = ppr m data EvBindInfo = EvBindGiven { -- See Note [Tracking redundant constraints] in GHC.Tc.Solver ===================================== compiler/GHC/Tc/Utils/Monad.hs ===================================== @@ -104,9 +104,10 @@ module GHC.Tc.Utils.Monad( -- * Type constraints newTcEvBinds, newNoTcEvBinds, cloneEvBindsVar, - addTcEvBind, addTcEvBinds, addTopEvBinds, - getTcEvBindsMap, setTcEvBindsMap, updTcEvBinds, - getTcEvTyCoVars, chooseUniqueOccTc, + addTcEvCoBind, addTcEvBind, addTopEvBinds, + getTcEvBindsMap, getTcEvBindsState, + setTcEvBindsMap, combineTcEvBinds, + chooseUniqueOccTc, getConstraintVar, setConstraintVar, emitConstraints, emitSimple, emitSimples, emitImplication, emitImplications, ensureReflMultiplicityCo, @@ -118,6 +119,7 @@ module GHC.Tc.Utils.Monad( getLclTypeEnv, setLclTypeEnv, traceTcConstraints, emitNamedTypeHole, IsExtraConstraint(..), emitAnonTypeHole, + fillCoercionHole, -- * Template Haskell context recordThUse, recordThNeededRuntimeDeps, @@ -187,12 +189,13 @@ import GHC.Unit.Module.Warnings import GHC.Unit.Home.PackageTable import GHC.Core.UsageEnv - import GHC.Core.Coercion ( isReflCo ) import GHC.Core.Multiplicity import GHC.Core.InstEnv import GHC.Core.FamInstEnv import GHC.Core.Type( mkNumLitTy ) +import GHC.Core.TyCo.Rep( CoercionHole(..) ) +import GHC.Core.TyCo.FVs( coVarsOfCo ) import GHC.Core.TyCon ( TyCon ) import GHC.Driver.Env @@ -230,6 +233,7 @@ import GHC.Types.SafeHaskell import GHC.Types.Id import GHC.Types.TypeEnv import GHC.Types.Var.Env +import GHC.Types.Var.Set import GHC.Types.SrcLoc import GHC.Types.Name.Env import GHC.Types.Name.Set @@ -1660,6 +1664,105 @@ tryTcDiscardingErrs' validate recover_invalid recover_error thing_inside recover_error } +{- Note [Constraints and errors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this (#12124): + + foo :: Maybe Int + foo = return (case Left 3 of + Left -> 1 -- Hard error here! + _ -> 0) + +The call to 'return' will generate a (Monad m) wanted constraint; but +then there'll be "hard error" (i.e. an exception in the TcM monad), from +the unsaturated Left constructor pattern. + +We'll recover in tcPolyBinds, using recoverM. But then the final +tcSimplifyTop will see that (Monad m) constraint, with 'm' utterly +un-filled-in, and will emit a misleading error message. + +The underlying problem is that an exception interrupts the constraint +gathering process. Bottom line: if we have an exception, it's best +simply to discard any gathered constraints. Hence in 'attemptM' we +capture the constraints in a fresh variable, and only emit them into +the surrounding context if we exit normally. If an exception is +raised, simply discard the collected constraints... we have a hard +error to report. So this capture-the-emit dance isn't as stupid as it +looks :-). + +However suppose we throw an exception inside an invocation of +captureConstraints, and discard all the constraints. Some of those +constraints might be "variable out of scope" Hole constraints, and that +might have been the actual original cause of the exception! For +example (#12529): + f = p @ Int +Here 'p' is out of scope, so we get an insoluble Hole constraint. But +the visible type application fails in the monad (throws an exception). +We must not discard the out-of-scope error. + +It's distressingly delicate though: + +* If we discard too /many/ constraints we may fail to report the error + that led us to interrupt the constraint gathering process. + + One particular example "variable out of scope" Hole constraints. For + example (#12529): + f = p @ Int + Here 'p' is out of scope, so we get an insoluble Hole constraint. But + the visible type application fails in the monad (throws an exception). + We must not discard the out-of-scope error. + + Also GHC.Tc.Solver.simplifyAndEmitFlatConstraints may fail having + emitted some constraints with skolem-escape problems. + +* If we discard too /few/ constraints, we may get the misleading + class constraints mentioned above. + + We may /also/ end up taking constraints built at some inner level, and + emitting them (via the exception catching in `tryCaptureConstraints`) at some + outer level, and then breaking the TcLevel invariants See Note [TcLevel + invariants] in GHC.Tc.Utils.TcType + +So `dropMisleading` has a horridly ad-hoc structure: + +* It keeps only /insoluble/ flat constraints (which are unlikely to very visibly + trip up on the TcLevel invariant) + +* But it keeps all /implication/ constraints (except the class constraints + inside them). The implication constraints are OK because they set the ambient + level before attempting to solve any inner constraints. + +Ugh! I hate this. But it seems to work. + +Other wrinkles + +(CERR1) Note that freshly-generated constraints like (Int ~ Bool), or + ((a -> b) ~ Int) are all CNonCanonical, and hence won't be flagged as + insoluble. The constraint solver does that. So they'll be discarded. + That's probably ok; but see th/5358 as a not-so-good example: + t1 :: Int + t1 x = x -- Manifestly wrong + + foo = $(...raises exception...) + We report the exception, but not the bug in t1. Oh well. Possible + solution: make GHC.Tc.Utils.Unify.uType spot manifestly-insoluble constraints. + +(CERR2) In #26015 I found that from the constraints + [W] alpha ~ Int -- A class constraint + [W] F alpha ~# Bool -- An equality constraint + we were dropping the first (becuase it's a class constraint) but not the + second, and then getting a misleading error message from the second. As + #25607 shows, we can get not just one but a zillion bogus messages, which + conceal the one genuine error. Boo. + + For now I have added an even more ad-hoc "drop class constraints except + equality classes (~) and (~~)"; see `dropMisleading`. That just kicks the can + down the road; but this problem seems somewhat rare anyway. The code in + `dropMisleading` hasn't changed for years. + +It would be great to have a more systematic solution to this entire mess. +-} + {- ************************************************************************ * * @@ -1854,108 +1957,112 @@ debugTc thing addTopEvBinds :: Bag EvBind -> TcM a -> TcM a addTopEvBinds new_ev_binds thing_inside - =updGblEnv upd_env thing_inside + = updGblEnv upd_env thing_inside where upd_env tcg_env = tcg_env { tcg_ev_binds = tcg_ev_binds tcg_env `unionBags` new_ev_binds } newTcEvBinds :: TcM EvBindsVar -newTcEvBinds = do { binds_ref <- newTcRef emptyEvBindMap - ; tcvs_ref <- newTcRef [] +newTcEvBinds = do { binds_ref <- newTcRef emptyEvBindsState ; uniq <- newUnique ; traceTc "newTcEvBinds" (text "unique =" <+> ppr uniq) ; return (EvBindsVar { ebv_binds = binds_ref - , ebv_tcvs = tcvs_ref , ebv_uniq = uniq }) } -- | Creates an EvBindsVar incapable of holding any bindings. It still --- tracks covar usages (see comments on ebv_tcvs in "GHC.Tc.Types.Evidence"), thus +-- tracks covar usages (see comments on ebv_needs in "GHC.Tc.Types.Evidence"), thus -- must be made monadically newNoTcEvBinds :: TcM EvBindsVar newNoTcEvBinds - = do { tcvs_ref <- newTcRef [] + = do { tcvs_ref <- newTcRef emptyVarSet ; uniq <- newUnique ; traceTc "newNoTcEvBinds" (text "unique =" <+> ppr uniq) - ; return (CoEvBindsVar { ebv_tcvs = tcvs_ref - , ebv_uniq = uniq }) } + ; return (CoEvBindsVar { ebv_needs = tcvs_ref + , ebv_uniq = uniq }) } cloneEvBindsVar :: EvBindsVar -> TcM EvBindsVar -- Clone the refs, so that any binding created when -- solving don't pollute the original cloneEvBindsVar ebv@(EvBindsVar {}) - = do { binds_ref <- newTcRef emptyEvBindMap - ; tcvs_ref <- newTcRef [] - ; return (ebv { ebv_binds = binds_ref - , ebv_tcvs = tcvs_ref }) } + = do { binds_ref <- newTcRef emptyEvBindsState + ; uniq <- newUnique + ; return (ebv { ebv_uniq = uniq + , ebv_binds = binds_ref }) } cloneEvBindsVar ebv@(CoEvBindsVar {}) - = do { tcvs_ref <- newTcRef [] - ; return (ebv { ebv_tcvs = tcvs_ref }) } + = do { tcvs_ref <- newTcRef emptyVarSet + ; return (ebv { ebv_needs = tcvs_ref }) } -getTcEvTyCoVars :: EvBindsVar -> TcM [TcCoercion] -getTcEvTyCoVars ev_binds_var - = readTcRef (ebv_tcvs ev_binds_var) +getTcEvBindsMap :: EvBindsVar -> TcM EvBindsMap +getTcEvBindsMap ebv = do { EBS { ebs_binds = bs } <- getTcEvBindsState ebv + ; return bs } -getTcEvBindsMap :: EvBindsVar -> TcM EvBindMap -getTcEvBindsMap (EvBindsVar { ebv_binds = ev_ref }) +getTcEvBindsState :: EvBindsVar -> TcM EvBindsState +getTcEvBindsState (EvBindsVar { ebv_binds = ev_ref }) = readTcRef ev_ref -getTcEvBindsMap (CoEvBindsVar {}) - = return emptyEvBindMap - -setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcM () -setTcEvBindsMap (EvBindsVar { ebv_binds = ev_ref }) binds - = writeTcRef ev_ref binds -setTcEvBindsMap v@(CoEvBindsVar {}) ev_binds - | isEmptyEvBindMap ev_binds - = return () - | otherwise - = pprPanic "setTcEvBindsMap" (ppr v $$ ppr ev_binds) - -updTcEvBinds :: EvBindsVar -> EvBindsVar -> TcM () -updTcEvBinds (EvBindsVar { ebv_binds = old_ebv_ref, ebv_tcvs = old_tcv_ref }) - (EvBindsVar { ebv_binds = new_ebv_ref, ebv_tcvs = new_tcv_ref }) +getTcEvBindsState (CoEvBindsVar { ebv_needs = needs_ref }) + = do { needs <- readTcRef needs_ref + ; return (EBS { ebs_binds = emptyEvBindsMap, ebs_needs = needs }) } + +setTcEvBindsMap :: EvBindsVar -> EvBindsMap -> TcM () +setTcEvBindsMap (EvBindsVar { ebv_binds = ev_ref }) ev_binds + = updTcRef ev_ref (\ebs -> ebs { ebs_binds = ev_binds }) +setTcEvBindsMap (CoEvBindsVar {}) ev_binds + = assertPpr (isEmptyEvBindsMap ev_binds) (ppr ev_binds) $ + return () + +combineTcEvBinds :: EvBindsVar -> EvBindsVar -> TcM () +combineTcEvBinds (EvBindsVar { ebv_binds = old_ebv_ref }) + (EvBindsVar { ebv_binds = new_ebv_ref }) = do { new_ebvs <- readTcRef new_ebv_ref - ; updTcRef old_ebv_ref (`unionEvBindMap` new_ebvs) - ; new_tcvs <- readTcRef new_tcv_ref - ; updTcRef old_tcv_ref (new_tcvs ++) } -updTcEvBinds (EvBindsVar { ebv_tcvs = old_tcv_ref }) - (CoEvBindsVar { ebv_tcvs = new_tcv_ref }) + ; updTcRef old_ebv_ref (`unionEvBindsState` new_ebvs) } +combineTcEvBinds (EvBindsVar { ebv_binds = old_tcv_ref }) + (CoEvBindsVar { ebv_needs = new_tcv_ref }) = do { new_tcvs <- readTcRef new_tcv_ref - ; updTcRef old_tcv_ref (new_tcvs ++) } -updTcEvBinds (CoEvBindsVar { ebv_tcvs = old_tcv_ref }) - (CoEvBindsVar { ebv_tcvs = new_tcv_ref }) + ; updTcRef old_tcv_ref (addCoVarsEBS new_tcvs) } +combineTcEvBinds (CoEvBindsVar { ebv_needs = old_tcv_ref }) + (CoEvBindsVar { ebv_needs = new_tcv_ref }) = do { new_tcvs <- readTcRef new_tcv_ref - ; updTcRef old_tcv_ref (new_tcvs ++) } -updTcEvBinds old_var new_var - = pprPanic "updTcEvBinds" (ppr old_var $$ ppr new_var) + ; updTcRef old_tcv_ref (unionVarSet new_tcvs) } +combineTcEvBinds old_var new_var + = pprPanic "combineTcEvBinds" (ppr old_var $$ ppr new_var) -- Terms inside types, no good +addTcEvCoBind :: EvBindsVar -> CoercionHole -> CoercionPlusHoles -> TcM () +addTcEvCoBind ebv hole co_plus_holes@(CPH { cph_co = co }) + = do { fillCoercionHole hole co_plus_holes + -- Record usage of the free vars of this coercion + ; let fvs = coVarsOfCo co + ; case ebv of + EvBindsVar { ebv_binds = bs_ref } + -> updTcRef bs_ref (addCoVarsEBS fvs) + CoEvBindsVar { ebv_needs = need_ref } + -> updTcRef need_ref (unionVarSet fvs) } + addTcEvBind :: EvBindsVar -> EvBind -> TcM () -- Add a binding to the TcEvBinds by side effect -addTcEvBind (EvBindsVar { ebv_binds = ev_ref, ebv_uniq = u }) ev_bind - = do { bnds <- readTcRef ev_ref - ; let bnds' = extendEvBinds bnds ev_bind +addTcEvBind (EvBindsVar { ebv_binds = ev_ref, ebv_uniq = u }) + ev_bind@(EvBind { eb_info = info, eb_rhs = rhs }) + = do { EBS { ebs_binds = bnds, ebs_needs = needs } <- readTcRef ev_ref + ; let bnds' = extendEvBinds bnds ev_bind + needs' = case info of + EvBindWanted {} -> nestedEvIdsOfTerm rhs + `unionVarSet` needs + EvBindGiven {} -> needs + ; traceTc "addTcEvBind" $ vcat [ text "EvBindsVar:" <+> ppr u , text "ev_bind:" <+> ppr ev_bind , text "bnds:" <+> ppr bnds - , text "bnds':" <+> ppr bnds' ] - ; writeTcRef ev_ref bnds' } + , text "bnds':" <+> ppr bnds' + , text "needs" <+> ppr needs + , text "needs'" <+> ppr needs' ] + + ; writeTcRef ev_ref $ + EBS { ebs_binds = bnds', ebs_needs = needs' } } + addTcEvBind (CoEvBindsVar { ebv_uniq = u }) ev_bind = pprPanic "addTcEvBind CoEvBindsVar" (ppr ev_bind $$ ppr u) -addTcEvBinds :: EvBindsVar -> EvBindMap -> TcM () --- ^ Add a collection of binding to the TcEvBinds by side effect -addTcEvBinds _ new_ev_binds - | isEmptyEvBindMap new_ev_binds - = return () -addTcEvBinds (EvBindsVar { ebv_binds = ev_ref, ebv_uniq = u }) new_ev_binds - = do { traceTc "addTcEvBinds" $ ppr u $$ - ppr new_ev_binds - ; old_bnds <- readTcRef ev_ref - ; writeTcRef ev_ref (old_bnds `unionEvBindMap` new_ev_binds) } -addTcEvBinds (CoEvBindsVar { ebv_uniq = u }) new_ev_binds - = pprPanic "addTcEvBinds CoEvBindsVar" (ppr new_ev_binds $$ ppr u) - chooseUniqueOccTc :: (OccSet -> OccName) -> TcM OccName chooseUniqueOccTc fn = do { env <- getGblEnv @@ -2137,111 +2244,22 @@ emitNamedTypeHole (name, tv) where occ = nameOccName name -{- Note [Constraints and errors] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider this (#12124): - - foo :: Maybe Int - foo = return (case Left 3 of - Left -> 1 -- Hard error here! - _ -> 0) - -The call to 'return' will generate a (Monad m) wanted constraint; but -then there'll be "hard error" (i.e. an exception in the TcM monad), from -the unsaturated Left constructor pattern. - -We'll recover in tcPolyBinds, using recoverM. But then the final -tcSimplifyTop will see that (Monad m) constraint, with 'm' utterly -un-filled-in, and will emit a misleading error message. - -The underlying problem is that an exception interrupts the constraint -gathering process. Bottom line: if we have an exception, it's best -simply to discard any gathered constraints. Hence in 'attemptM' we -capture the constraints in a fresh variable, and only emit them into -the surrounding context if we exit normally. If an exception is -raised, simply discard the collected constraints... we have a hard -error to report. So this capture-the-emit dance isn't as stupid as it -looks :-). - -However suppose we throw an exception inside an invocation of -captureConstraints, and discard all the constraints. Some of those -constraints might be "variable out of scope" Hole constraints, and that -might have been the actual original cause of the exception! For -example (#12529): - f = p @ Int -Here 'p' is out of scope, so we get an insoluble Hole constraint. But -the visible type application fails in the monad (throws an exception). -We must not discard the out-of-scope error. - -It's distressingly delicate though: - -* If we discard too /many/ constraints we may fail to report the error - that led us to interrupt the constraint gathering process. - - One particular example "variable out of scope" Hole constraints. For - example (#12529): - f = p @ Int - Here 'p' is out of scope, so we get an insoluble Hole constraint. But - the visible type application fails in the monad (throws an exception). - We must not discard the out-of-scope error. - - Also GHC.Tc.Solver.simplifyAndEmitFlatConstraints may fail having - emitted some constraints with skolem-escape problems. - -* If we discard too /few/ constraints, we may get the misleading - class constraints mentioned above. - - We may /also/ end up taking constraints built at some inner level, and - emitting them (via the exception catching in `tryCaptureConstraints` at some - outer level, and then breaking the TcLevel invariants See Note [TcLevel - invariants] in GHC.Tc.Utils.TcType - -So `dropMisleading` has a horridly ad-hoc structure: - -* It keeps only /insoluble/ flat constraints (which are unlikely to very visibly - trip up on the TcLevel invariant - -* But it keeps all /implication/ constraints (except the class constraints - inside them). The implication constraints are OK because they set the ambient - level before attempting to solve any inner constraints. - -Ugh! I hate this. But it seems to work. - -Other wrinkles - -(CERR1) Note that freshly-generated constraints like (Int ~ Bool), or - ((a -> b) ~ Int) are all CNonCanonical, and hence won't be flagged as - insoluble. The constraint solver does that. So they'll be discarded. - That's probably ok; but see th/5358 as a not-so-good example: - t1 :: Int - t1 x = x -- Manifestly wrong - - foo = $(...raises exception...) - We report the exception, but not the bug in t1. Oh well. Possible - solution: make GHC.Tc.Utils.Unify.uType spot manifestly-insoluble constraints. - -(CERR2) In #26015 I found that from the constraints - [W] alpha ~ Int -- A class constraint - [W] F alpha ~# Bool -- An equality constraint - we were dropping the first (becuase it's a class constraint) but not the - second, and then getting a misleading error message from the second. As - #25607 shows, we can get not just one but a zillion bogus messages, which - conceal the one genuine error. Boo. +-- | Put a value in a coercion hole +fillCoercionHole :: CoercionHole -> CoercionPlusHoles -> TcM () +fillCoercionHole (CH { ch_ref = ref, ch_co_var = cv }) co + = do { when debugIsOn $ + do { cts <- readTcRef ref + ; whenIsJust cts $ \old_co -> + pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co) } + ; traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co) + ; writeTcRef ref (Just co) } - For now I have added an even more ad-hoc "drop class constraints except - equality classes (~) and (~~)"; see `dropMisleading`. That just kicks the can - down the road; but this problem seems somewhat rare anyway. The code in - `dropMisleading` hasn't changed for years. - -It would be great to have a more systematic solution to this entire mess. - -************************************************************************ +{- ********************************************************************* * * Template Haskell context * * -************************************************************************ --} +********************************************************************* -} recordThUse :: TcM () recordThUse = do { env <- getGblEnv; writeTcRef (tcg_th_used env) True } ===================================== compiler/GHC/Tc/Utils/TcMType.hs ===================================== @@ -341,31 +341,13 @@ newImplication (implicationPrototype (mkCtLocEnv env)) { ic_warn_inaccessible = warn_inaccessible && not in_gen_code } -{- -************************************************************************ -* * - Coercion holes -* * -************************************************************************ --} - newCoercionHole :: TcPredType -> TcM CoercionHole -- For the Bool, see (EIK2) in Note [Equalities with heterogeneous kinds] newCoercionHole pred_ty = do { co_var <- newEvVar pred_ty ; traceTc "New coercion hole:" (ppr co_var <+> dcolon <+> ppr pred_ty) ; ref <- newMutVar Nothing - ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } } - --- | Put a value in a coercion hole -fillCoercionHole :: CoercionHole -> CoercionPlusHoles -> TcM () -fillCoercionHole (CoercionHole { ch_ref = ref, ch_co_var = cv }) co - = do { when debugIsOn $ - do { cts <- readTcRef ref - ; whenIsJust cts $ \old_co -> - pprPanic "Filling a filled coercion hole" (ppr cv $$ ppr co $$ ppr old_co) } - ; traceTc "Filling coercion hole" (ppr cv <+> text ":=" <+> ppr co) - ; writeTcRef ref (Just co) } + ; return $ CH { ch_co_var = co_var, ch_ref = ref } } {- ********************************************************************** * ===================================== compiler/GHC/Tc/Utils/Unify.hs ===================================== @@ -418,7 +418,8 @@ Some examples: -} tcSkolemiseGeneral - :: DeepSubsumptionFlag + :: HasDebugCallStack + => DeepSubsumptionFlag -> UserTypeCtxt -> TcType -> TcType -- top_ty and expected_ty -- Here, top_ty is the type we started to skolemise; used only in SigSkol @@ -446,15 +447,16 @@ tcSkolemiseGeneral ds_flag ctxt top_ty expected_ty thing_inside ; skol_info <- mkSkolemInfo sig_skol } ; let skol_tvs = map (binderVar . snd) tv_prs - ; traceTc "tcSkolemiseGeneral" (pprUserTypeCtxt ctxt <+> ppr skol_tvs <+> ppr given) + ; traceTc "tcSkolemiseGeneral {" (pprUserTypeCtxt ctxt <+> ppr skol_tvs <+> ppr given) ; (ev_binds, result) <- checkConstraints sig_skol skol_tvs given $ thing_inside tv_prs rho_ty + ; traceTc "tcSkolemiseGeneral }" (ppr ev_binds $$ traceCallStackDoc) ; return (wrap <.> mkWpLet ev_binds, result) } -- The ev_binds returned by checkConstraints is very -- often empty, in which case mkWpLet is a no-op -tcSkolemiseCompleteSig :: TcCompleteSig +tcSkolemiseCompleteSig :: HasDebugCallStack => TcCompleteSig -> ([ExpPatType] -> TcRhoType -> TcM result) -> TcM (HsWrapper, result) -- ^ The wrapper has type: spec_ty ~~> expected_ty @@ -471,7 +473,7 @@ tcSkolemiseCompleteSig (CSig { sig_bndr = poly_id, sig_ctxt = ctxt, sig_loc = lo tcExtendNameTyVarEnv (map (fmap binderVar) tv_prs) $ thing_inside (map (mkInvisExpPatType . snd) tv_prs) rho_ty } -tcSkolemiseExpectedType :: TcSigmaType +tcSkolemiseExpectedType :: HasDebugCallStack => TcSigmaType -> ([ExpPatType] -> TcRhoType -> TcM result) -> TcM (HsWrapper, result) -- Just like tcSkolemiseCompleteSig, except that we don't have a user-written @@ -483,14 +485,15 @@ tcSkolemiseExpectedType exp_ty thing_inside = tcSkolemiseGeneral Shallow GenSigCtxt exp_ty exp_ty $ \tv_prs rho_ty -> thing_inside (map (mkInvisExpPatType . snd) tv_prs) rho_ty -tcSkolemise :: DeepSubsumptionFlag -> UserTypeCtxt -> TcSigmaType +tcSkolemise :: HasDebugCallStack => DeepSubsumptionFlag -> UserTypeCtxt -> TcSigmaType -> (TcRhoType -> TcM result) -> TcM (HsWrapper, result) tcSkolemise ds_flag ctxt expected_ty thing_inside = tcSkolemiseGeneral ds_flag ctxt expected_ty expected_ty $ \_ rho_ty -> thing_inside rho_ty -checkConstraints :: SkolemInfoAnon +checkConstraints :: HasDebugCallStack + => SkolemInfoAnon -> [TcTyVar] -- Skolems -> [EvVar] -- Given -> TcM result @@ -504,14 +507,16 @@ checkConstraints skol_info skol_tvs given thing_inside ; if implication_needed then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted - ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs) + ; traceTc "checkConstraints A" (ppr tclvl $$ ppr skol_tvs $$ traceCallStackDoc) ; emitImplications implics ; return (ev_binds, result) } else -- Fast path. We check every function argument with tcCheckPolyExpr, -- which uses tcTopSkolemise and hence checkConstraints. -- So this fast path is well-exercised - do { res <- thing_inside + do { traceTc "checkConstraints B" (ppr skol_tvs $$ ppr given $$ ppr skol_info $$ + traceCallStackDoc) + ; res <- thing_inside ; return (emptyTcEvBinds, res) } } checkTvConstraints :: SkolemInfo ===================================== compiler/GHC/Tc/Zonk/TcType.hs ===================================== @@ -236,7 +236,7 @@ zonkCo :: Coercion -> ZonkM Coercion , tcm_tycon = zonkTcTyCon } where hole :: () -> CoercionHole -> ZonkM Coercion - hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv }) + hole _ hole@(CH { ch_ref = ref, ch_co_var = cv }) = do { contents <- readTcRef ref ; case contents of Just (CPH { cph_co = co }) @@ -617,7 +617,7 @@ instance Monoid UnfilledCoercionHoleMonoid where -- | Is a coercion hole filled in? isFilledCoercionHole :: CoercionHole -> ZonkM Bool -isFilledCoercionHole (CoercionHole { ch_ref = ref }) +isFilledCoercionHole (CH { ch_ref = ref }) = isJust <$> readTcRef ref -- | Retrieve the contents of a coercion hole. Panics if the hole @@ -631,7 +631,7 @@ unpackCoercionHole hole -- | Retrieve the contents of a coercion hole, if it is filled unpackCoercionHole_maybe :: CoercionHole -> ZonkM (Maybe CoercionPlusHoles) -unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref +unpackCoercionHole_maybe (CH { ch_ref = ref }) = readTcRef ref {- ===================================== compiler/GHC/Tc/Zonk/Type.hs ===================================== @@ -485,7 +485,7 @@ zonkCoVarOcc cv _ -> mkCoVarCo <$> (lift $ liftZonkM $ zonkCoVar cv) } zonkCoHole :: CoercionHole -> ZonkTcM Coercion -zonkCoHole hole@(CoercionHole { ch_ref = ref, ch_co_var = cv }) +zonkCoHole hole@(CH { ch_ref = ref, ch_co_var = cv }) = do { contents <- readTcRef ref ; case contents of Just (CPH { cph_co = co }) @@ -1910,8 +1910,9 @@ zonk_tc_ev_binds (EvBinds bs) = zonkEvBinds bs zonkEvBindsVar :: EvBindsVar -> ZonkBndrTcM (Bag EvBind) zonkEvBindsVar (EvBindsVar { ebv_binds = ref }) - = do { bs <- readTcRef ref + = do { EBS { ebs_binds = bs } <- readTcRef ref ; zonkEvBinds (evBindMapBinds bs) } + zonkEvBindsVar (CoEvBindsVar {}) = return emptyBag zonkEvBinds :: Bag EvBind -> ZonkBndrTcM (Bag EvBind) ===================================== compiler/GHC/Utils/Trace.hs ===================================== @@ -11,6 +11,7 @@ module GHC.Utils.Trace , warnPprTraceM , pprTraceUserWarning , trace + , traceCallStackDoc ) where View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/22f6f55efff888690adc4d2b8ef394c5... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/22f6f55efff888690adc4d2b8ef394c5... You're receiving this email because of your account on gitlab.haskell.org.