Simon Peyton Jones pushed to branch wip/T26115 at Glasgow Haskell Compiler / GHC Commits: 592bf1aa by Simon Peyton Jones at 2025-06-25T15:37:39+01:00 More improvements - - - - - 12 changed files: - compiler/GHC/HsToCore/Binds.hs - compiler/GHC/Tc/Gen/Sig.hs - compiler/GHC/Tc/Solver.hs - compiler/GHC/Tc/Solver/Default.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/Solver/Solve.hs-boot - compiler/GHC/Tc/Types/Evidence.hs - compiler/GHC/Tc/Zonk/Type.hs - testsuite/tests/typecheck/should_compile/T23171.hs Changes: ===================================== compiler/GHC/HsToCore/Binds.hs ===================================== @@ -1896,10 +1896,10 @@ dsEvTerm (EvExpr e) = return e dsEvTerm (EvTypeable ty ev) = dsEvTypeable ty ev dsEvTerm (EvFun { et_tvs = tvs, et_given = given , et_binds = ev_binds, et_body = wanted_id }) - = do { dsTcEvBinds ev_binds $ \ds_ev_binds -> do - { return $ (mkLams (tvs ++ given) $ + = do { dsEvBinds ev_binds $ \ds_ev_binds -> + return $ (mkLams (tvs ++ given) $ mkCoreLets ds_ev_binds $ - Var wanted_id) } } + Var wanted_id) } {-********************************************************************** ===================================== compiler/GHC/Tc/Gen/Sig.hs ===================================== @@ -39,7 +39,7 @@ import GHC.Tc.Gen.HsType import GHC.Tc.Solver( reportUnsolvedEqualities, pushLevelAndSolveEqualitiesX , emitResidualConstraints ) import GHC.Tc.Solver.Solve( solveWanteds ) -import GHC.Tc.Solver.Monad( runTcS, runTcSSpecPrag ) +import GHC.Tc.Solver.Monad( runTcS, runTcSWithEvBinds ) import GHC.Tc.Validity ( checkValidType ) import GHC.Tc.Utils.Monad @@ -1042,7 +1042,7 @@ tcSpecPrag poly_id (SpecSigE nm rule_bndrs spec_e inl) -- (2) Solve the resulting wanteds in TcSSpecPrag mode. ; ev_binds_var <- newTcEvBinds ; spec_e_wanted <- setTcLevel rhs_tclvl $ - runTcSSpecPrag ev_binds_var $ + runTcSWithEvBinds ev_binds_var $ solveWanteds spec_e_wanted ; spec_e_wanted <- liftZonkM $ zonkWC spec_e_wanted ===================================== compiler/GHC/Tc/Solver.hs ===================================== @@ -1036,8 +1036,7 @@ findInferredDiff annotated_theta inferred_theta -- See `Note [Quantification and partial signatures]` Wrinkle 2 ; return (map (box_pred . ctPred) $ - bagToList $ - wc_simple residual) } + bagToList residual) } where box_pred :: PredType -> PredType box_pred pred = case classifyPredType pred of ===================================== compiler/GHC/Tc/Solver/Default.hs ===================================== @@ -1188,8 +1188,8 @@ tryDefaultGroup wanteds (Proposal assignments) ; new_wanteds <- sequence [ new_wtd_ct wtd | CtWanted wtd <- map ctEvidence wanteds ] - ; residual_wc <- solveSimpleWanteds (listToBag new_wanteds) - ; return $ if isEmptyWC residual_wc then Just (tvs, subst) else Nothing } + ; residual <- solveSimpleWanteds (listToBag new_wanteds) + ; return $ if isEmptyBag residual then Just (tvs, subst) else Nothing } | otherwise = return Nothing ===================================== compiler/GHC/Tc/Solver/Dict.hs ===================================== @@ -702,10 +702,10 @@ tryInertDicts :: DictCt -> SolverStage () tryInertDicts dict_ct = Stage $ do { inerts <- getInertCans ; mode <- getTcSMode - -- In TcSSpecPrag mode we do not look at Givens; that's the point + -- In TcSShortCut 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 () + TcSShortCut -> continueWith () _other -> try_inert_dicts inerts dict_ct } try_inert_dicts :: InertCans -> DictCt -> TcS (StopOrContinue ()) @@ -774,9 +774,9 @@ tryShortCutSolver try_short_cut dict_w@(DictCt { di_ev = ev_w }) -> 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 { wc <- solveSimpleWanteds (unitBag (CDictCan dict_w)) - ; return (isSolvedWC wc) } + setTcSMode TcSShortCut $ + do { residual <- solveSimpleWanteds (unitBag (CDictCan dict_w)) + ; return (isEmptyBag residual) } | otherwise -> return False } ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -11,7 +11,6 @@ module GHC.Tc.Solver.InertSet ( extendWorkListEq, extendWorkListChildEqs, extendWorkListRewrittenEqs, appendWorkList, - extendWorkListImplic, extendWorkListImplics, workListSize, -- * The inert set @@ -155,17 +154,6 @@ So we arrange to put these particular class constraints in the wl_eqs. NB: since we do not currently apply the substitution to the inert_solved_dicts, the knot-tying still seems a bit fragile. But this makes it better. - -Note [Residual implications] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The wl_implics in the WorkList are the residual implication -constraints that are generated while solving or canonicalising the -current worklist. Specifically, when canonicalising - (forall a. t1 ~ forall a. t2) -from which we get the implication - (forall a. t1 ~ t2) -See GHC.Tc.Solver.Monad.deferTcSForAllEq - -} -- See Note [WorkList priorities] @@ -187,8 +175,6 @@ data WorkList -- in GHC.Tc.Types.Constraint for more details. , wl_rest :: [Ct] - - , wl_implics :: Bag Implication -- See Note [Residual implications] } isNominalEqualityCt :: Ct -> Bool @@ -203,15 +189,12 @@ isNominalEqualityCt ct appendWorkList :: WorkList -> WorkList -> WorkList appendWorkList - (WL { wl_eqs_N = eqs1_N, wl_eqs_X = eqs1_X, wl_rw_eqs = rw_eqs1 - , wl_rest = rest1, wl_implics = implics1 }) - (WL { wl_eqs_N = eqs2_N, wl_eqs_X = eqs2_X, wl_rw_eqs = rw_eqs2 - , wl_rest = rest2, wl_implics = implics2 }) + (WL { wl_eqs_N = eqs1_N, wl_eqs_X = eqs1_X, wl_rw_eqs = rw_eqs1, wl_rest = rest1 }) + (WL { wl_eqs_N = eqs2_N, wl_eqs_X = eqs2_X, wl_rw_eqs = rw_eqs2, wl_rest = rest2 }) = WL { wl_eqs_N = eqs1_N ++ eqs2_N , wl_eqs_X = eqs1_X ++ eqs2_X , wl_rw_eqs = rw_eqs1 ++ rw_eqs2 - , wl_rest = rest1 ++ rest2 - , wl_implics = implics1 `unionBags` implics2 } + , wl_rest = rest1 ++ rest2 } workListSize :: WorkList -> Int workListSize (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs, wl_rest = rest }) @@ -269,12 +252,6 @@ extendWorkListNonEq :: Ct -> WorkList -> WorkList -- Extension by non equality extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl } -extendWorkListImplic :: Implication -> WorkList -> WorkList -extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl } - -extendWorkListImplics :: Bag Implication -> WorkList -> WorkList -extendWorkListImplics implics wl = wl { wl_implics = implics `unionBags` wl_implics wl } - extendWorkListCt :: Ct -> WorkList -> WorkList -- Agnostic about what kind of constraint extendWorkListCt ct wl @@ -298,18 +275,18 @@ extendWorkListCts :: Cts -> WorkList -> WorkList extendWorkListCts cts wl = foldr extendWorkListCt wl cts isEmptyWorkList :: WorkList -> Bool -isEmptyWorkList (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs - , wl_rest = rest, wl_implics = implics }) - = null eqs_N && null eqs_X && null rw_eqs && null rest && isEmptyBag implics +isEmptyWorkList (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X + , wl_rw_eqs = rw_eqs, wl_rest = rest }) + = null eqs_N && null eqs_X && null rw_eqs && null rest emptyWorkList :: WorkList emptyWorkList = WL { wl_eqs_N = [], wl_eqs_X = [] - , wl_rw_eqs = [], wl_rest = [], wl_implics = emptyBag } + , wl_rw_eqs = [], wl_rest = [] } -- Pretty printing instance Outputable WorkList where - ppr (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs - , wl_rest = rest, wl_implics = implics }) + ppr (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X + , wl_rw_eqs = rw_eqs, wl_rest = rest }) = text "WL" <+> (braces $ vcat [ ppUnless (null eqs_N) $ text "Eqs_N =" <+> vcat (map ppr eqs_N) @@ -319,9 +296,6 @@ instance Outputable WorkList where text "RwEqs =" <+> vcat (map ppr rw_eqs) , ppUnless (null rest) $ text "Non-eqs =" <+> vcat (map ppr rest) - , ppUnless (isEmptyBag implics) $ - ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics))) - (text "(Implics omitted)") ]) {- ********************************************************************* ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -17,12 +17,10 @@ module GHC.Tc.Solver.Monad ( -- The TcS monad TcS(..), TcSEnv(..), runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts, - runTcSSpecPrag, failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS, runTcSEqualities, nestTcS, nestImplicTcS, tryTcS, setEvBindsTcS, setTcLevelTcS, - emitImplicationTcS, emitTvImplicationTcS, emitFunDepWanteds, selectNextWorkItem, @@ -746,8 +744,7 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts }) -- We only want Givens from this level; see (3a) in -- Note [The superclass story] in GHC.Tc.Solver.Dict -getUnsolvedInerts :: TcS ( Bag Implication - , Cts ) -- All simple constraints +getUnsolvedInerts :: TcS Cts -- All simple constraints -- Return all the unsolved [Wanted] constraints -- -- Post-condition: the returned simple constraints are all fully zonked @@ -767,20 +764,17 @@ getUnsolvedInerts unsolved_dicts = foldDicts (add_if_unsolved CDictCan) idicts emptyCts unsolved_qcis = foldr (add_if_unsolved CQuantCan) emptyCts qcis - ; implics <- getWorkListImplics - ; traceTcS "getUnsolvedInerts" $ vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs , text "fun eqs =" <+> ppr unsolved_fun_eqs , text "dicts =" <+> ppr unsolved_dicts - , text "irreds =" <+> ppr unsolved_irreds - , text "implics =" <+> ppr implics ] - - ; return ( implics, unsolved_tv_eqs `unionBags` - unsolved_fun_eqs `unionBags` - unsolved_irreds `unionBags` - unsolved_dicts `unionBags` - unsolved_qcis ) } + , text "irreds =" <+> ppr unsolved_irreds ] + + ; return ( unsolved_tv_eqs `unionBags` + unsolved_fun_eqs `unionBags` + unsolved_irreds `unionBags` + unsolved_dicts `unionBags` + unsolved_qcis ) } where add_if_unsolved :: (a -> Ct) -> a -> Cts -> Cts add_if_unsolved mk_ct thing cts @@ -938,7 +932,7 @@ data TcSMode = TcSVanilla -- ^ Normal constraint solving | TcSPMCheck -- ^ Used when doing patterm match overlap checks | TcSEarlyAbort -- ^ Abort early on insoluble constraints - | TcSSpecPrag -- ^ Fully solve all constraints + | TcSShortCut -- ^ Fully solve all constraints, without using local Givens deriving (Eq) {- Note [TcSMode] @@ -1135,10 +1129,6 @@ runTcSEarlyAbort tcs -- | Run the 'TcS' monad in 'TcSSpecPrag' mode, which either fully solves -- individual Wanted quantified constraints or leaves them alone. -- --- See Note [TcSSpecPrag]. -runTcSSpecPrag :: EvBindsVar -> TcS a -> TcM a -runTcSSpecPrag ev_binds_var tcs - = runTcSWithEvBinds' TcSSpecPrag ev_binds_var tcs {- Note [TcSSpecPrag] ~~~~~~~~~~~~~~~~~~~~~ @@ -1390,46 +1380,6 @@ updateInertsWith current_inerts = current_inerts { inert_solved_dicts = new_solved , inert_safehask = new_safehask } -emitImplicationTcS :: TcLevel -> SkolemInfoAnon - -> [TcTyVar] -- Skolems - -> [EvVar] -- Givens - -> Cts -- Wanteds - -> TcS TcEvBinds --- Add an implication to the TcS monad work-list -emitImplicationTcS new_tclvl skol_info skol_tvs givens wanteds - = do { let wc = emptyWC { wc_simple = wanteds } - ; imp <- wrapTcS $ - do { ev_binds_var <- TcM.newTcEvBinds - ; imp <- TcM.newImplication - ; return (imp { ic_tclvl = new_tclvl - , ic_skols = skol_tvs - , ic_given = givens - , ic_wanted = wc - , ic_binds = ev_binds_var - , ic_info = skol_info }) } - - ; updWorkListTcS (extendWorkListImplic imp) - ; return (TcEvBinds (ic_binds imp)) } - -emitTvImplicationTcS :: TcLevel -> SkolemInfoAnon - -> [TcTyVar] -- Skolems - -> Cts -- Wanteds - -> TcS () --- Just like emitImplicationTcS but no givens and no bindings -emitTvImplicationTcS new_tclvl skol_info skol_tvs wanteds - = do { let wc = emptyWC { wc_simple = wanteds } - ; imp <- wrapTcS $ - do { ev_binds_var <- TcM.newNoTcEvBinds - ; imp <- TcM.newImplication - ; return (imp { ic_tclvl = new_tclvl - , ic_skols = skol_tvs - , ic_wanted = wc - , ic_binds = ev_binds_var - , ic_info = skol_info }) } - - ; updWorkListTcS (extendWorkListImplic imp) } - - {- Note [Propagate the solved dictionaries] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ It's really quite important that nestTcS does not discard the solved @@ -1795,12 +1745,6 @@ getWorkList :: TcS WorkList getWorkList = do { wl_var <- getTcSWorkListRef ; readTcRef wl_var } -getWorkListImplics :: TcS (Bag Implication) -getWorkListImplics - = do { wl_var <- getTcSWorkListRef - ; wl_curr <- readTcRef wl_var - ; return (wl_implics wl_curr) } - updWorkListTcS :: (WorkList -> WorkList) -> TcS () updWorkListTcS f = do { wl_var <- getTcSWorkListRef @@ -2017,7 +1961,7 @@ instFlexiXTcM subst (tv:tvs) matchGlobalInst :: DynFlags -> Class -> [Type] -> CtLoc -> TcS TcM.ClsInstResult matchGlobalInst dflags cls tys loc = do { mode <- getTcSMode - ; let short_cut = mode == TcSSpecPrag + ; let short_cut = mode == TcSShortCut ; wrapTcS $ TcM.matchGlobalInst dflags short_cut cls tys (Just loc) } tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcS (Subst, [TcTyVar]) ===================================== compiler/GHC/Tc/Solver/Solve.hs ===================================== @@ -94,6 +94,7 @@ solveWanteds wc@(WC { wc_errors = errs }) ; bb <- TcS.getTcEvBindsMap ev_binds_var ; traceTcS "solveWanteds }" $ vcat [ text "final wc =" <+> ppr final_wc + , text "ev_binds_var =" <+> ppr ev_binds_var , text "current evbinds =" <+> ppr (evBindMapBinds bb) ] ; return final_wc } @@ -118,19 +119,17 @@ simplify_loop n limit definitely_redo_implications , int (lengthBag simples) <+> text "simples to solve" ]) ; traceTcS "simplify_loop: wc =" (ppr wc) - ; (unifs1, wc1) <- reportUnifications $ -- See Note [Superclass iteration] - solveSimpleWanteds simples + ; (unifs1, simples1) <- reportUnifications $ -- See Note [Superclass iteration] + solveSimpleWanteds simples -- Any insoluble constraints are in 'simples' and so get rewritten -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet ; wc2 <- if not definitely_redo_implications -- See Note [Superclass iteration] && unifs1 == 0 -- for this conditional - && isEmptyBag (wc_impl wc1) - then return (wc { wc_simple = wc_simple wc1 }) -- Short cut - else do { implics2 <- solveNestedImplications $ - implics `unionBags` (wc_impl wc1) - ; return (wc { wc_simple = wc_simple wc1 - , wc_impl = implics2 }) } + then return (wc { wc_simple = simples1 }) -- Short cut + else do { implics1 <- solveNestedImplications implics + ; return (wc { wc_simple = simples1 + , wc_impl = implics1 }) } ; unif_happened <- resetUnificationFlag ; csTraceTcS $ text "unif_happened" <+> ppr unif_happened @@ -978,30 +977,32 @@ solveSimpleGivens givens -- for use by subsequent calls of nestImplicTcS ; updInertSet (\is -> is { inert_givens = inert_cans is }) - ; traceTcS "End solveSimpleGivens }" empty } + ; cans <- getInertCans + ; traceTcS "End solveSimpleGivens }" (ppr cans) } where go givens = do { solveSimples (listToBag givens) ; new_givens <- runTcPluginsGiven ; when (notNull new_givens) $ go new_givens } -solveSimpleWanteds :: Cts -> TcS WantedConstraints +solveSimpleWanteds :: Cts -> TcS Cts -- The result is not necessarily zonked solveSimpleWanteds simples = do { traceTcS "solveSimpleWanteds {" (ppr simples) ; dflags <- getDynFlags - ; (n,wc) <- go 1 (solverIterations dflags) (emptyWC { wc_simple = simples }) + ; (n,wc) <- go 1 (solverIterations dflags) simples ; traceTcS "solveSimpleWanteds end }" $ vcat [ text "iterations =" <+> ppr n , text "residual =" <+> ppr wc ] ; return wc } where - go :: Int -> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints) + go :: Int -> IntWithInf -> Cts -> TcS (Int, Cts) -- See Note [The solveSimpleWanteds loop] go n limit wc | n `intGtLimit` limit - = failTcS $ TcRnSimplifierTooManyIterations simples limit wc - | isEmptyBag (wc_simple wc) + = failTcS $ TcRnSimplifierTooManyIterations + simples limit (emptyWC { wc_simple = wc }) + | isEmptyBag wc = return (n,wc) | otherwise = do { -- Solve @@ -1018,17 +1019,13 @@ solveSimpleWanteds simples else return (n, wc2) } -- Done -solve_simple_wanteds :: WantedConstraints -> TcS WantedConstraints +solve_simple_wanteds :: Cts -> TcS Cts -- 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, wc_errors = errs }) - = nestTcS $ - do { solveSimples simples1 - ; (implics2, unsolved) <- getUnsolvedInerts - ; return (WC { wc_simple = unsolved - , wc_impl = implics1 `unionBags` implics2 - , wc_errors = errs }) } +solve_simple_wanteds simples + = nestTcS $ do { solveSimples simples + ; getUnsolvedInerts } {- Note [The solveSimpleWanteds loop] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1379,13 +1376,14 @@ 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) + ; traceTcS "solveForAll }" (ppr solved) + ; evbs <- TcS.getTcEvBindsMap ev_binds_var ; if not solved then do { addInertForAll qci ; stopWith (CtWanted wtd) "Wanted forall-constraint:unsolved" } else do { setWantedEvTerm dest EvCanonical $ EvFun { et_tvs = skol_tvs, et_given = given_ev_vars - , et_binds = TcEvBinds ev_binds_var, et_body = w_id } + , et_binds = evBindMapBinds evbs, et_body = w_id } ; stopWith (CtWanted wtd) "Wanted forall-constraint:solved" } } where loc_env = ctLocEnv ct_loc @@ -1596,13 +1594,13 @@ runTcPluginsGiven -- work) and a bag of insolubles. The boolean indicates whether -- 'solveSimpleWanteds' should feed the updated wanteds back into the -- main solver. -runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints) -runTcPluginsWanted wc@(WC { wc_simple = simples1 }) +runTcPluginsWanted :: Cts -> TcS (Bool, Cts) +runTcPluginsWanted simples1 | isEmptyBag simples1 - = return (False, wc) + = return (False, simples1) | otherwise = do { solvers <- getTcPluginSolvers - ; if null solvers then return (False, wc) else + ; if null solvers then return (False, simples1) else do { given <- getInertGivens ; wanted <- TcS.zonkSimples simples1 -- Plugin requires zonked inputs @@ -1624,8 +1622,7 @@ runTcPluginsWanted wc@(WC { wc_simple = simples1 }) ; mapM_ setEv solved_wanted ; traceTcS "Finished plugins }" (ppr new_wanted) - ; return ( notNull (pluginNewCts p) - , wc { wc_simple = all_new_wanted } ) } } + ; return ( notNull (pluginNewCts p), all_new_wanted ) } } where setEv :: (EvTerm,Ct) -> TcS () setEv (ev,ct) = case ctEvidence ct of ===================================== compiler/GHC/Tc/Solver/Solve.hs-boot ===================================== @@ -2,7 +2,7 @@ module GHC.Tc.Solver.Solve where import Prelude( Bool ) import GHC.Tc.Solver.Monad( TcS ) -import GHC.Tc.Types.Constraint( WantedConstraints, Cts, Implication ) +import GHC.Tc.Types.Constraint( Cts, Implication ) -solveSimpleWanteds :: Cts -> TcS WantedConstraints +solveSimpleWanteds :: Cts -> TcS Cts trySolveImplication :: Implication -> TcS Bool ===================================== compiler/GHC/Tc/Types/Evidence.hs ===================================== @@ -509,8 +509,8 @@ data EvTerm | EvFun -- /\as \ds. let binds in v { et_tvs :: [TyVar] , et_given :: [EvVar] - , et_binds :: TcEvBinds -- This field is why we need an EvFun - -- constructor, and can't just use EvExpr + , et_binds :: Bag EvBind -- This field is why we need an EvFun + -- constructor, and can't just use EvExpr , et_body :: EvVar } deriving Data.Data @@ -876,7 +876,11 @@ relevantEvVar v = isInternalName (varName v) evVarsOfTerm :: EvTerm -> VarSet evVarsOfTerm (EvExpr e) = exprSomeFreeVars relevantEvVar e evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev -evVarsOfTerm (EvFun {}) = emptyVarSet -- See Note [Free vars of EvFun] +evVarsOfTerm (EvFun { et_tvs = tvs, et_given = given, et_binds = binds, et_body = v }) + = fvs `delVarSetList` bndrs + where + fvs = foldr (unionVarSet . evVarsOfTerm . eb_rhs) (unitVarSet v) binds + bndrs = foldr ((:) . eb_lhs) (tvs ++ given) binds evVarsOfTerms :: [EvTerm] -> VarSet evVarsOfTerms = mapUnionVarSet evVarsOfTerm ===================================== compiler/GHC/Tc/Zonk/Type.hs ===================================== @@ -1764,7 +1764,7 @@ zonkEvTerm (EvFun { et_tvs = tvs, et_given = evs , et_binds = ev_binds, et_body = body_id }) = runZonkBndrT (zonkTyBndrsX tvs) $ \ new_tvs -> runZonkBndrT (zonkEvBndrsX evs) $ \ new_evs -> - runZonkBndrT (zonkTcEvBinds ev_binds) $ \ new_ev_binds -> + runZonkBndrT (zonkEvBinds ev_binds) $ \ new_ev_binds -> do { new_body_id <- zonkIdOcc body_id ; return (EvFun { et_tvs = new_tvs, et_given = new_evs , et_binds = new_ev_binds, et_body = new_body_id }) } ===================================== testsuite/tests/typecheck/should_compile/T23171.hs ===================================== @@ -33,7 +33,7 @@ tried :: forall (e :: Type). (forall m. C1T e m) => e -> () tried = try @e -- From the call to "try", we get [W] D (T e). --- After using the instance for D, we get the QC [G] C3 m ==> [W] C1 (T e) m. +-- After using the instance for D, we get the QC [W] (forall m. C3 m ==> C1 (T e) m) -- -- The Given "[G] C3 m" thus arises from superclass expansion -- from "D (T e)", which contains a type family application, T. @@ -41,3 +41,16 @@ tried = try @e -- expanding the superclasses of C3 (in this case, C2); in particular -- ltPatersonSize needs to handle a type family in its second argument. +{- [G] forall m. C1T e m + --> sc + [G] forall m. C1 (T e) m <<--- aJT + + [W] D (T e) +--> instance + [W] (forall m. C3 m => C1 (T e) m) + + ---- Implication: forall m2 --- + [G] C3 m2 + [W] C1 (T e) m2 + --> solve via qci +-} View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/592bf1aad69ed7fef07abd24393f0711... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/592bf1aad69ed7fef07abd24393f0711... You're receiving this email because of your account on gitlab.haskell.org.