Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC
Commits:
-
5eea3311
by Simon Peyton Jones at 2025-07-06T23:09:47+01:00
4 changed files:
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Solve.hs
Changes:
| ... | ... | @@ -413,7 +413,7 @@ solveEqualityDict ev cls tys |
| 413 | 413 | do { let loc = ctEvLoc ev
|
| 414 | 414 | sc_pred = classMethodInstTy sel_id tys
|
| 415 | 415 | ev_expr = EvExpr $ Var sel_id `mkTyApps` tys `App` evId ev_id
|
| 416 | - ; given_ev <- newGivenEvVar loc (sc_pred, ev_expr)
|
|
| 416 | + ; given_ev <- newGivenEv loc (sc_pred, ev_expr)
|
|
| 417 | 417 | ; startAgainWith (mkNonCanonical $ CtGiven given_ev) }
|
| 418 | 418 | | otherwise
|
| 419 | 419 | = pprPanic "solveEqualityDict" (ppr cls)
|
| ... | ... | @@ -1403,8 +1403,8 @@ now!). |
| 1403 | 1403 | Note [FunDep and implicit parameter reactions]
|
| 1404 | 1404 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
| 1405 | 1405 | Currently, our story of interacting two dictionaries (or a dictionary
|
| 1406 | -and top-level instances) for functional dependencies, and implicit
|
|
| 1407 | -parameters, is that we simply produce new Wanted equalities. So for example
|
|
| 1406 | +and top-level instances) for functional dependencies (including implicit
|
|
| 1407 | +parameters), is that we simply produce new Wanted equalities. So for example
|
|
| 1408 | 1408 | |
| 1409 | 1409 | class D a b | a -> b where ...
|
| 1410 | 1410 | Inert:
|
| ... | ... | @@ -1663,43 +1663,46 @@ doTopFunDepImprovement cts |
| 1663 | 1663 | inst_pred inst_loc
|
| 1664 | 1664 | |
| 1665 | 1665 | doLocalFunDepImprovement :: Bag DictCt -> TcS (Cts,Bool)
|
| 1666 | --- Add wanted constraints from type-class functional dependencies
|
|
| 1667 | --- against Givens
|
|
| 1668 | -doLocalFunDepImprovement cts
|
|
| 1666 | +-- Using functional dependencies, interact the unsolved Wanteds
|
|
| 1667 | +-- against each other and the inert Givens, to produce new equalities
|
|
| 1668 | +doLocalFunDepImprovement wanted
|
|
| 1669 | 1669 | = do { inerts <- getInertCans -- The inert_dicts are all Givens
|
| 1670 | - ; do_dict_fundeps (do_one (inert_dicts inerts)) cts }
|
|
| 1670 | + ; let all_dicts :: DictMap DictCt -- Both Givens and Wanteds
|
|
| 1671 | + all_dicts = foldr addDict (inert_dicts inerts) wanted
|
|
| 1672 | + ; do_dict_fundeps (do_one all_dicts) wanted }
|
|
| 1671 | 1673 | where
|
| 1672 | - do_one givens (DictCt { di_cls = cls, di_ev = wanted_ev })
|
|
| 1673 | - = do_dict_fundeps do_one_given (findDictsByClass givens cls)
|
|
| 1674 | + -- all_dicts are all the Givens and all the Wanteds
|
|
| 1675 | + do_one all_dicts (DictCt { di_cls = cls, di_ev = wanted_ev })
|
|
| 1676 | + = do_dict_fundeps do_interaction (findDictsByClass all_dicts cls)
|
|
| 1674 | 1677 | where
|
| 1675 | 1678 | wanted_pred = ctEvPred wanted_ev
|
| 1676 | 1679 | wanted_loc = ctEvLoc wanted_ev
|
| 1677 | 1680 | |
| 1678 | - do_one_given :: DictCt -> TcS (Cts,Bool)
|
|
| 1679 | - do_one_given (DictCt { di_ev = given_ev })
|
|
| 1681 | + do_interaction :: DictCt -> TcS (Cts,Bool)
|
|
| 1682 | + do_interaction (DictCt { di_ev = all_ev }) -- This can be Given or Wanted
|
|
| 1680 | 1683 | = do { traceTcS "doLocalFunDepImprovement" $
|
| 1681 | 1684 | vcat [ ppr wanted_ev
|
| 1682 | 1685 | , pprCtLoc wanted_loc, ppr (isGivenLoc wanted_loc)
|
| 1683 | - , pprCtLoc given_loc, ppr (isGivenLoc given_loc)
|
|
| 1686 | + , pprCtLoc all_loc, ppr (isGivenLoc all_loc)
|
|
| 1684 | 1687 | , pprCtLoc deriv_loc, ppr (isGivenLoc deriv_loc) ]
|
| 1685 | 1688 | |
| 1686 | 1689 | ; unifyFunDepWanteds wanted_ev $
|
| 1687 | - improveFromAnother (deriv_loc, given_rewriters)
|
|
| 1688 | - given_pred wanted_pred }
|
|
| 1690 | + improveFromAnother (deriv_loc, all_rewriters)
|
|
| 1691 | + all_pred wanted_pred }
|
|
| 1689 | 1692 | where
|
| 1690 | - given_pred = ctEvPred given_ev
|
|
| 1691 | - given_loc = ctEvLoc given_ev
|
|
| 1692 | - given_rewriters = ctEvRewriters given_ev
|
|
| 1693 | + all_pred = ctEvPred all_ev
|
|
| 1694 | + all_loc = ctEvLoc all_ev
|
|
| 1695 | + all_rewriters = ctEvRewriters all_ev
|
|
| 1693 | 1696 | deriv_loc = wanted_loc { ctl_depth = deriv_depth
|
| 1694 | 1697 | , ctl_origin = deriv_origin }
|
| 1695 | 1698 | deriv_depth = ctl_depth wanted_loc `maxSubGoalDepth`
|
| 1696 | - ctl_depth given_loc
|
|
| 1699 | + ctl_depth all_loc
|
|
| 1697 | 1700 | deriv_origin = FunDepOrigin1 wanted_pred
|
| 1698 | 1701 | (ctLocOrigin wanted_loc)
|
| 1699 | 1702 | (ctLocSpan wanted_loc)
|
| 1700 | - given_pred
|
|
| 1701 | - (ctLocOrigin given_loc)
|
|
| 1702 | - (ctLocSpan given_loc)
|
|
| 1703 | + all_pred
|
|
| 1704 | + (ctLocOrigin all_loc)
|
|
| 1705 | + (ctLocSpan all_loc)
|
|
| 1703 | 1706 | |
| 1704 | 1707 | do_dict_fundeps :: (DictCt -> TcS (Cts,Bool)) -> Bag DictCt -> TcS (Cts,Bool)
|
| 1705 | 1708 | do_dict_fundeps do_dict_fundep cts
|
| ... | ... | @@ -2047,7 +2050,7 @@ mk_strict_superclasses fuel rec_clss ev@(CtGiven (GivenCt { ctev_evar = evar })) |
| 2047 | 2050 | = -- See Note [Equality superclasses in quantified constraints]
|
| 2048 | 2051 | return []
|
| 2049 | 2052 | | otherwise
|
| 2050 | - = do { given_ev <- newGivenEvVar sc_loc $
|
|
| 2053 | + = do { given_ev <- newGivenEv sc_loc $
|
|
| 2051 | 2054 | mk_given_desc sel_id sc_pred
|
| 2052 | 2055 | ; assertFuelPrecondition fuel $
|
| 2053 | 2056 | mk_superclasses fuel rec_clss (CtGiven given_ev) tvs theta sc_pred }
|
| ... | ... | @@ -780,12 +780,12 @@ can_eq_app ev s1 t1 s2 t2 |
| 780 | 780 | = do { let co = mkCoVarCo evar
|
| 781 | 781 | co_s = mkLRCo CLeft co
|
| 782 | 782 | co_t = mkLRCo CRight co
|
| 783 | - ; evar_s <- newGivenEvVar loc ( mkTcEqPredLikeEv ev s1 s2
|
|
| 784 | - , evCoercion co_s )
|
|
| 785 | - ; evar_t <- newGivenEvVar loc ( mkTcEqPredLikeEv ev t1 t2
|
|
| 786 | - , evCoercion co_t )
|
|
| 787 | - ; emitWorkNC [CtGiven evar_t]
|
|
| 788 | - ; startAgainWith (mkNonCanonical $ CtGiven evar_s) }
|
|
| 783 | + ; ev_s <- newGivenEv loc ( mkTcEqPredLikeEv ev s1 s2
|
|
| 784 | + , evCoercion co_s )
|
|
| 785 | + ; ev_t <- newGivenEv loc ( mkTcEqPredLikeEv ev t1 t2
|
|
| 786 | + , evCoercion co_t )
|
|
| 787 | + ; emitWorkNC [CtGiven ev_t]
|
|
| 788 | + ; startAgainWith (mkNonCanonical $ CtGiven ev_s) }
|
|
| 789 | 789 | |
| 790 | 790 | where
|
| 791 | 791 | loc = ctEvLoc ev
|
| ... | ... | @@ -1632,7 +1632,7 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 |
| 1632 | 1632 | -> do { let kind_co = mkKindCo (mkCoVarCo evar)
|
| 1633 | 1633 | pred_ty = unSwap swapped mkNomEqPred ki1 ki2
|
| 1634 | 1634 | kind_loc = mkKindEqLoc xi1 xi2 loc
|
| 1635 | - ; kind_ev <- newGivenEvVar kind_loc (pred_ty, evCoercion kind_co)
|
|
| 1635 | + ; kind_ev <- newGivenEv kind_loc (pred_ty, evCoercion kind_co)
|
|
| 1636 | 1636 | ; emitWorkNC [CtGiven kind_ev]
|
| 1637 | 1637 | ; finish emptyRewriterSet (givenCtEvCoercion kind_ev) }
|
| 1638 | 1638 | |
| ... | ... | @@ -2597,7 +2597,7 @@ rewriteEqEvidence new_rewriters old_ev swapped (Reduction lhs_co nlhs) (Reductio |
| 2597 | 2597 | = do { let new_tm = evCoercion ( mkSymCo lhs_co
|
| 2598 | 2598 | `mkTransCo` maybeSymCo swapped (mkCoVarCo old_evar)
|
| 2599 | 2599 | `mkTransCo` rhs_co)
|
| 2600 | - ; CtGiven <$> newGivenEvVar loc (new_pred, new_tm) }
|
|
| 2600 | + ; CtGiven <$> newGivenEv loc (new_pred, new_tm) }
|
|
| 2601 | 2601 | |
| 2602 | 2602 | | CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rewriters }) <- old_ev
|
| 2603 | 2603 | = do { let rewriters' = rewriters S.<> new_rewriters
|
| ... | ... | @@ -3044,6 +3044,7 @@ equality with the template on the left. Delicate, but it works. |
| 3044 | 3044 | -}
|
| 3045 | 3045 | |
| 3046 | 3046 | --------------------
|
| 3047 | + |
|
| 3047 | 3048 | tryFunDeps :: EqCt -> SolverStage ()
|
| 3048 | 3049 | tryFunDeps work_item@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel })
|
| 3049 | 3050 | | NomEq <- eq_rel
|
| ... | ... | @@ -3253,7 +3254,7 @@ improveWantedLocalFunEqs |
| 3253 | 3254 | -> TyCon -> [TcType] -> CtEvidence -> Xi -- Work item (Wanted)
|
| 3254 | 3255 | -> TcS Bool -- True <=> some unifications
|
| 3255 | 3256 | -- Emit improvement equalities for a Wanted constraint, by comparing
|
| 3256 | --- the current work item with inert CFunEqs (boh Given and Wanted)
|
|
| 3257 | +-- the current work item with inert CFunEqs (both Given and Wanted)
|
|
| 3257 | 3258 | -- E.g. x + y ~ z, x + y' ~ z => [W] y ~ y'
|
| 3258 | 3259 | --
|
| 3259 | 3260 | -- See Note [FunDep and implicit parameter reactions]
|
| ... | ... | @@ -57,7 +57,7 @@ module GHC.Tc.Solver.Monad ( |
| 57 | 57 | unifyTyVar, reportUnifications,
|
| 58 | 58 | setEvBind, setWantedEq,
|
| 59 | 59 | setWantedEvTerm, setEvBindIfWanted,
|
| 60 | - newEvVar, newGivenEvVar, emitNewGivens,
|
|
| 60 | + newEvVar, newGivenEv, emitNewGivens,
|
|
| 61 | 61 | checkReductionDepth,
|
| 62 | 62 | getSolvedDicts, setSolvedDicts,
|
| 63 | 63 | |
| ... | ... | @@ -2081,12 +2081,12 @@ newNoTcEvBinds = wrapTcS TcM.newNoTcEvBinds |
| 2081 | 2081 | newEvVar :: TcPredType -> TcS EvVar
|
| 2082 | 2082 | newEvVar pred = wrapTcS (TcM.newEvVar pred)
|
| 2083 | 2083 | |
| 2084 | -newGivenEvVar :: CtLoc -> (TcPredType, EvTerm) -> TcS GivenCtEvidence
|
|
| 2084 | +newGivenEv :: CtLoc -> (TcPredType, EvTerm) -> TcS GivenCtEvidence
|
|
| 2085 | 2085 | -- Make a new variable of the given PredType,
|
| 2086 | 2086 | -- immediately bind it to the given term
|
| 2087 | 2087 | -- and return its CtEvidence
|
| 2088 | 2088 | -- See Note [Bind new Givens immediately] in GHC.Tc.Types.Constraint
|
| 2089 | -newGivenEvVar loc (pred, rhs)
|
|
| 2089 | +newGivenEv loc (pred, rhs)
|
|
| 2090 | 2090 | = do { new_ev <- newBoundEvVarId pred rhs
|
| 2091 | 2091 | ; return $ GivenCt { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc } }
|
| 2092 | 2092 | |
| ... | ... | @@ -2101,7 +2101,7 @@ newBoundEvVarId pred rhs |
| 2101 | 2101 | emitNewGivens :: CtLoc -> [(Role,TcCoercion)] -> TcS ()
|
| 2102 | 2102 | emitNewGivens loc pts
|
| 2103 | 2103 | = do { traceTcS "emitNewGivens" (ppr pts)
|
| 2104 | - ; gs <- mapM (newGivenEvVar loc) $
|
|
| 2104 | + ; gs <- mapM (newGivenEv loc) $
|
|
| 2105 | 2105 | [ (mkEqPredRole role ty1 ty2, evCoercion co)
|
| 2106 | 2106 | | (role, co) <- pts
|
| 2107 | 2107 | , let Pair ty1 ty2 = coercionKind co
|
| ... | ... | @@ -2484,7 +2484,7 @@ checkTypeEq ev eq_rel lhs rhs = |
| 2484 | 2484 | ---------------------------
|
| 2485 | 2485 | mk_new_given :: (TcTyVar, TcType) -> TcS Ct
|
| 2486 | 2486 | mk_new_given (new_tv, fam_app)
|
| 2487 | - = mkNonCanonical . CtGiven <$> newGivenEvVar cb_loc (given_pred, given_term)
|
|
| 2487 | + = mkNonCanonical . CtGiven <$> newGivenEv cb_loc (given_pred, given_term)
|
|
| 2488 | 2488 | where
|
| 2489 | 2489 | new_ty = mkTyVarTy new_tv
|
| 2490 | 2490 | given_pred = mkNomEqPred fam_app new_ty
|
| ... | ... | @@ -1563,7 +1563,7 @@ finish_rewrite |
| 1563 | 1563 | new_tm = assert (coercionRole co == ev_rw_role)
|
| 1564 | 1564 | mkEvCast (evId old_evar)
|
| 1565 | 1565 | (downgradeRole Representational ev_rw_role co)
|
| 1566 | - ; new_ev <- newGivenEvVar loc (new_pred, new_tm)
|
|
| 1566 | + ; new_ev <- newGivenEv loc (new_pred, new_tm)
|
|
| 1567 | 1567 | ; continueWith $ CtGiven new_ev }
|
| 1568 | 1568 | |
| 1569 | 1569 | finish_rewrite
|