Simon Peyton Jones pushed to branch wip/T26115 at Glasgow Haskell Compiler / GHC Commits: ff3f98d1 by Simon Peyton Jones at 2025-06-24T16:16:23+01:00 More progress - - - - - 7 changed files: - compiler/GHC/HsToCore/Binds.hs - compiler/GHC/Tc/Errors.hs - compiler/GHC/Tc/Solver/Dict.hs - compiler/GHC/Tc/Solver/InertSet.hs - compiler/GHC/Tc/Solver/Monad.hs - compiler/GHC/Tc/Solver/Solve.hs - compiler/GHC/Tc/Types/Evidence.hs Changes: ===================================== compiler/GHC/HsToCore/Binds.hs ===================================== @@ -1181,8 +1181,8 @@ dsSpec_help poly_nm poly_id poly_rhs spec_inl orig_bndrs ds_call mk_spec_body fn_body = mkLets (rn_binds ++ picked_binds) $ mkApps fn_body rule_lhs_args - -- ToDo: not mkCoreApps! That uses exprType on fun which - -- fails in specUnfolding, sigh + -- NB: not mkCoreApps! That uses exprType on fun + -- which fails in specUnfolding, sigh poly_name = idName poly_id spec_occ = mkSpecOcc (getOccName poly_name) ===================================== compiler/GHC/Tc/Errors.hs ===================================== @@ -622,7 +622,8 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics -- report2: we suppress these if there are insolubles elsewhere in the tree report2 = [ ("Implicit params", is_ip, False, mkGroupReporter mkIPErr) , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr) - , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ] + , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) + , ("Quantified", is_qc, False, mkGroupReporter mkQCErr) ] -- report3: suppressed errors should be reported as categorized by either report1 -- or report2. Keep this in sync with the suppress function above @@ -681,6 +682,9 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics is_irred _ (IrredPred {}) = True is_irred _ _ = False + is_qc _ (ForAllPred {}) = True + is_qc _ _ = False + -- See situation (1) of Note [Suppressing confusing errors] is_ww_fundep item _ = is_ww_fundep_item item is_ww_fundep_item = isWantedWantedFunDepOrigin . errorItemOrigin @@ -2175,6 +2179,13 @@ Warn of loopy local equalities that were dropped. ************************************************************************ -} +mkQCErr :: HasDebugCallStack => SolverReportErrCtxt -> NonEmpty ErrorItem -> TcM SolverReport +mkQCErr ctxt items + = do { let msg = mkPlainMismatchMsg $ + CouldNotDeduce (getUserGivens ctxt) items Nothing + ; return $ important ctxt msg } + + mkDictErr :: HasDebugCallStack => SolverReportErrCtxt -> NonEmpty ErrorItem -> TcM SolverReport mkDictErr ctxt orig_items = do { inst_envs <- tcGetInstEnvs @@ -2192,8 +2203,8 @@ mkDictErr ctxt orig_items ; return $ SolverReport { sr_important_msg = SolverReportWithCtxt ctxt err - , sr_supplementary = - [ SupplementaryImportErrors imps | imps <- maybeToList (NE.nonEmpty imp_errs) ] + , sr_supplementary = [ SupplementaryImportErrors imps + | imps <- maybeToList (NE.nonEmpty imp_errs) ] , sr_hints = hints } } ===================================== compiler/GHC/Tc/Solver/Dict.hs ===================================== @@ -701,7 +701,12 @@ and Given/instance fundeps entirely. tryInertDicts :: DictCt -> SolverStage () tryInertDicts dict_ct = Stage $ do { inerts <- getInertCans - ; try_inert_dicts inerts dict_ct } + ; mode <- getTcSMode + -- In TcSSpecPrag mode we do not look at Givens; that's the point + -- Looking at Wanteds would be OK but no real benefit + ; case mode of + TcSSpecPrag -> continueWith () + _other -> try_inert_dicts inerts dict_ct } try_inert_dicts :: InertCans -> DictCt -> TcS (StopOrContinue ()) try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys }) @@ -767,22 +772,15 @@ tryShortCutSolver try_short_cut dict_w@(DictCt { di_ev = ev_w }) -- Enabled by the -fsolve-constant-dicts flag -> tryTcS $ -- tryTcS tries to completely solve some contraints + -- Inherit the current solved_dicts, so that one invocation of + -- tryShortCutSolver can benefit from the work of earlier invocations setTcSMode TcSSpecPrag $ - do { updInertSet zap_cans - ; solveSimpleWanteds (unitBag (CDictCan dict_w)) } + do { wc <- solveSimpleWanteds (unitBag (CDictCan dict_w)) + ; return (isSolvedWC wc) } | otherwise -> return False } - where - zap_cans :: InertSet -> InertSet - -- Zap the inert Givens (so we don't try to use them for solving) - -- and any inert Wanteds (no harm but not much benefit either. - -- But preserve the current solved_dicts, so that one invocation of - -- tryShortCutSolver can benefit from the work of earlier invocations - zap_cans inerts@(IS { inert_cans = cans }) - = inerts { inert_cans = emptyInertCans (inert_given_eq_lvl cans) } - {- ******************************************************************* * * ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -27,7 +27,6 @@ module GHC.Tc.Solver.InertSet ( foldTyEqs, delEq, findEq, partitionInertEqs, partitionFunEqs, filterInertEqs, filterFunEqs, - inertGivens, foldFunEqs, addEqToCans, -- * Inert Dicts @@ -347,6 +346,10 @@ data InertSet -- Canonical Given, Wanted -- Sometimes called "the inert set" + , inert_givens :: InertCans + -- A subset of inert_cans, containing only Givens + -- Used to initialise inert_cans when recursing inside implications + , inert_cycle_breakers :: CycleBreakerVarStack , inert_famapp_cache :: FunEqMap Reduction @@ -399,11 +402,14 @@ emptyInertCans given_eq_lvl emptyInertSet :: TcLevel -> InertSet emptyInertSet given_eq_lvl - = IS { inert_cans = emptyInertCans given_eq_lvl + = IS { inert_cans = empty_cans + , inert_givens = empty_cans , inert_cycle_breakers = emptyBag :| [] , inert_famapp_cache = emptyFunEqs , inert_solved_dicts = emptyDictMap - , inert_safehask = emptyDictMap } + , inert_safehask = emptyDictMap } + where + empty_cans = emptyInertCans given_eq_lvl {- Note [Solved dictionaries] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2129,43 +2135,3 @@ Wrong! The level-check ensures that the inner implicit parameter wins. that this chain of events won't happen, but that's very fragile.) -} -{- ********************************************************************* -* * - Extracting Givens from the inert set -* * -********************************************************************* -} - - --- | Extract only Given constraints from the inert set. -inertGivens :: InertSet -> InertSet -inertGivens is@(IS { inert_cans = cans, inert_safehask = safehask }) = - is { inert_cans = givens_cans - , inert_safehask = safehask_givens - , inert_solved_dicts = emptyDictMap - } - where - - isGivenEq :: EqCt -> Bool - isGivenEq eq = isGiven (ctEvidence (CEqCan eq)) - isGivenDict :: DictCt -> Bool - isGivenDict dict = isGiven (ctEvidence (CDictCan dict)) - isGivenIrred :: IrredCt -> Bool - isGivenIrred irred = isGiven (ctEvidence (CIrredCan irred)) - - -- Filter the inert constraints for Givens - (eq_givens_list, _) = partitionInertEqs isGivenEq (inert_eqs cans) - (funeq_givens_list, _) = partitionFunEqs isGivenEq (inert_funeqs cans) - dict_givens = filterDicts isGivenDict (inert_dicts cans) - safehask_givens = filterDicts isGivenDict safehask - irreds_givens = filterBag isGivenIrred (inert_irreds cans) - - eq_givens = foldr addInertEqs emptyTyEqs eq_givens_list - funeq_givens = foldr addFunEqs emptyFunEqs funeq_givens_list - - givens_cans = - cans - { inert_eqs = eq_givens - , inert_funeqs = funeq_givens - , inert_dicts = dict_givens - , inert_irreds = irreds_givens - } ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -1293,27 +1293,21 @@ nestImplicTcS :: EvBindsVar -> TcLevel -> TcS a -> TcS a nestImplicTcS ref inner_tclvl (TcS thing_inside) - = TcS $ \ TcSEnv { tcs_unified = unified_var - , tcs_inerts = old_inert_var - , tcs_count = count - , tcs_unif_lvl = unif_lvl - , tcs_mode = mode - } -> + = TcS $ \ env@(TcSEnv { tcs_inerts = old_inert_var }) -> do { inerts <- TcM.readTcRef old_inert_var + + -- Initialise the inert_cans from the inert_givens of the parent + -- so that the child is not polluted with the parent's inert Wanteds ; let nest_inert = inerts { inert_cycle_breakers = pushCycleBreakerVarStack (inert_cycle_breakers inerts) - , inert_cans = (inert_cans inerts) + , inert_cans = (inert_givens inerts) { inert_given_eqs = False } } -- All other InertSet fields are inherited ; new_inert_var <- TcM.newTcRef nest_inert ; new_wl_var <- TcM.newTcRef emptyWorkList - ; let nest_env = TcSEnv { tcs_count = count -- Inherited - , tcs_unif_lvl = unif_lvl -- Inherited - , tcs_ev_binds = ref - , tcs_unified = unified_var - , tcs_inerts = new_inert_var - , tcs_mode = mode - , tcs_worklist = new_wl_var } + ; let nest_env = env { tcs_ev_binds = ref + , tcs_inerts = new_inert_var + , tcs_worklist = new_wl_var } ; res <- TcM.setTcLevel inner_tclvl $ thing_inside nest_env @@ -1339,6 +1333,7 @@ nestTcS (TcS thing_inside) ; new_wl_var <- TcM.newTcRef emptyWorkList ; let nest_env = env { tcs_inerts = new_inert_var , tcs_worklist = new_wl_var } + -- Inherit tcs_ev_binds from caller ; res <- thing_inside nest_env @@ -1347,18 +1342,17 @@ nestTcS (TcS thing_inside) ; return res } -tryTcS :: TcS WantedConstraints -> TcS Bool +tryTcS :: TcS Bool -> TcS Bool -- Like nestTcS, but -- (a) be a no-op if the nested computation returns Nothing -- (b) if (but only if) success, propagate nested bindings to the caller tryTcS (TcS thing_inside) = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var - , tcs_ev_binds = old_ev_binds_var - , tcs_worklist = wl_var }) -> + , tcs_ev_binds = old_ev_binds_var }) -> do { old_inerts <- TcM.readTcRef inerts_var ; new_inert_var <- TcM.newTcRef old_inerts ; new_wl_var <- TcM.newTcRef emptyWorkList - ; new_ev_binds_var <- TcM.newTcEvBinds + ; new_ev_binds_var <- TcM.cloneEvBindsVar old_ev_binds_var ; let nest_env = env { tcs_ev_binds = new_ev_binds_var , tcs_inerts = new_inert_var , tcs_worklist = new_wl_var } @@ -1367,10 +1361,10 @@ tryTcS (TcS thing_inside) vcat [ text "old_ev_binds:" <+> ppr old_ev_binds_var , text "new_ev_binds:" <+> ppr new_ev_binds_var , ppr old_inerts ] - ; wc <- thing_inside nest_env - ; TcM.traceTc "tryTcS }" (ppr wc) + ; solved <- thing_inside nest_env + ; TcM.traceTc "tryTcS }" (ppr solved) - ; if not (isSolvedWC wc) + ; if not solved then return False else do { -- Successfully solved -- Add the new bindings to the existing ones @@ -1382,17 +1376,12 @@ tryTcS (TcS thing_inside) ; TcM.traceTc "tryTcS update" (ppr (inert_solved_dicts new_inerts)) - -- We **must not** drop solved implications, due - -- to Note [Free vars of EvFun] in GHC.Tc.Types.Evidence; - -- so we re-emit them here. - ; TcM.updTcRef wl_var (extendWorkListImplics (wc_impl wc)) - ; return True } } updateInertsWith :: InertSet -> InertSet -> InertSet -- Update the current inert set with bits from a nested solve, -- that finished with a new inert set --- In particular, propagage: +-- In particular, propagate: -- - solved dictionaires; see Note [Propagate the solved dictionaries] -- - Safe Haskell failures updateInertsWith current_inerts ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -280,6 +280,20 @@ solveNestedImplications implics ; return unsolved_implics } +trySolveImplication :: Implication -> TcS Bool +trySolveImplication (Implic { ic_tclvl = tclvl + , ic_binds = ev_binds_var + , ic_given = given_ids + , ic_wanted = wanteds + , ic_env = ct_loc_env + , ic_info = info }) + = nestImplicTcS ev_binds_var tclvl $ + do { let loc = mkGivenLoc tclvl info ct_loc_env + givens = mkGivens loc given_ids + ; solveSimpleGivens givens + ; residual_wanted <- solveWanteds wanteds + ; return (isSolvedWC residual_wanted) } + solveImplication :: Implication -- Wanted -> TcS Implication -- Simplified implication -- Precondition: The TcS monad contains an empty worklist and given-only inerts @@ -289,6 +303,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl , ic_given = given_ids , ic_wanted = wanteds , ic_info = info + , ic_env = ct_loc_env , ic_status = status }) | isSolvedStatus status = return imp -- Do nothing @@ -306,7 +321,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl -- Solve the nested constraints ; (has_given_eqs, given_insols, residual_wanted) <- nestImplicTcS ev_binds_var tclvl $ - do { let loc = mkGivenLoc tclvl info (ic_env imp) + do { let loc = mkGivenLoc tclvl info ct_loc_env givens = mkGivens loc given_ids ; solveSimpleGivens givens @@ -958,6 +973,11 @@ solveSimpleGivens givens | otherwise = do { traceTcS "solveSimpleGivens {" (ppr givens) ; go givens + + -- Capture the Givens in the inert_givens of the inert set + -- for use by subsequent calls of nestImplicTcS + ; updInertSet (\is -> is { inert_givens = inert_cans is }) + ; traceTcS "End solveSimpleGivens }" empty } where go givens = do { solveSimples (listToBag givens) @@ -1348,7 +1368,7 @@ solveWantedForAll qci tvs theta body_pred ; return ( wantedCtEvEvId wanted_ev , unitBag (mkNonCanonical $ CtWanted wanted_ev)) } - ; traceTcS "solveForAll" (ppr given_ev_vars $$ ppr wanteds $$ ppr w_id) + ; traceTcS "solveForAll {" (ppr skol_tvs $$ ppr given_ev_vars $$ ppr wanteds $$ ppr w_id) ; ev_binds_var <- TcS.newTcEvBinds ; solved <- trySolveImplication $ (implicationPrototype loc_env) @@ -1359,6 +1379,7 @@ solveWantedForAll qci tvs theta body_pred , ic_skols = skol_tvs , ic_given = given_ev_vars , ic_wanted = emptyWC { wc_simple = wanteds } } + ; traceTcS "sllveForAll }" (ppr solved) ; if not solved then do { addInertForAll qci ; stopWith (CtWanted wtd) "Wanted forall-constraint:unsolved" } @@ -1379,34 +1400,6 @@ solveWantedForAll qci tvs theta body_pred ClassPred cls tys -> pSizeClassPred cls tys _ -> pSizeType pred -trySolveImplication :: Implication -> TcS Bool -trySolveImplication imp - = tryTcS $ - do { imp' <- solveImplication imp - ; return (emptyWC { wc_impl = unitBag imp' }) } - -- ToDo: this emptyWC bit is somewhat clumsy - -{- -solveWantedForAll_spec :: WantedCtEvidence -> TcS (StopOrContinue Void) --- Solve this implication constraint completely or not at all -solveWantedForAll_spec wtd - = do { traceTcS "solveWantedForAll {" (ppr wtd) - ; fully_solved <- tryTcS (setTcSMode TcSVanilla $ - solveWanteds (mkSimpleWC [ev])) - -- It's crucial to call solveWanteds here, not solveSimpleWanteds, - -- because solving `ev` will land in solveWantedForAll_norm, - -- which emits an implication, which we must then solve - ; if fully_solved - then do { traceTcS "solveWantedForAll: fully solved }" (ppr wtd) - ; return $ Stop ev (text "Fully solved:" <+> ppr wtd) } - else do { traceTcS "solveWantedForAll: not fully solved }" (ppr wtd) - ; updInertIrreds (IrredCt ev IrredShapeReason) - -- Stash the unsolved quantified constraint in the irreds - ; return $ Stop ev (text "Not fully solved:" <+> ppr wtd) } } - where - ev = CtWanted wtd --} - {- Note [Solving a Wanted forall-constraint] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Solving a wanted forall (quantified) constraint ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -894,7 +894,7 @@ evVarsOfTypeable ev = ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Finding the free vars of an EvFun is made tricky by the fact the bindings et_binds may be a mutable variable. Fortunately, we -can just squeeze by. Here's how. +ocan just squeeze by. Here's how. * evVarsOfTerm is used only by GHC.Tc.Solver.neededEvVars. * Each EvBindsVar in an et_binds field of an EvFun is /also/ in the View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ff3f98d14fdc75e6d7c9fca4685901c9... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ff3f98d14fdc75e6d7c9fca4685901c9... You're receiving this email because of your account on gitlab.haskell.org.