Adam Gundry pushed to branch wip/amg/castz at Glasgow Haskell Compiler / GHC
Commits:
-
e7c9343f
by Adam Gundry at 2025-07-23T20:53:56+01:00
-
79d86db2
by Adam Gundry at 2025-07-23T20:53:56+01:00
6 changed files:
- compiler/GHC/HsToCore/Binds.hs
- compiler/GHC/Iface/Ext/Ast.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Zonk/Type.hs
- testsuite/tests/ghci/scripts/ghci024.stdout
Changes:
| ... | ... | @@ -1783,6 +1783,7 @@ dsEvBind (EvBind { eb_lhs = v, eb_rhs = r, eb_info = info }) = do |
| 1783 | 1783 | |
| 1784 | 1784 | dsEvTerm :: EvTerm -> DsM CoreExpr
|
| 1785 | 1785 | dsEvTerm (EvExpr e) = return e
|
| 1786 | +dsEvTerm (EvCastExpr e co _) = return (Cast e co)
|
|
| 1786 | 1787 | dsEvTerm (EvTypeable ty ev) = dsEvTypeable ty ev
|
| 1787 | 1788 | dsEvTerm (EvFun { et_tvs = tvs, et_given = given
|
| 1788 | 1789 | , et_binds = ev_binds, et_body = wanted_id })
|
| ... | ... | @@ -30,6 +30,7 @@ import GHC.Types.Avail ( Avails ) |
| 30 | 30 | import GHC.Data.Bag ( Bag, bagToList )
|
| 31 | 31 | import GHC.Types.Basic
|
| 32 | 32 | import GHC.Data.BooleanFormula
|
| 33 | +import GHC.Core ( Expr(Cast) )
|
|
| 33 | 34 | import GHC.Core.Class ( className, classSCSelIds )
|
| 34 | 35 | import GHC.Core.ConLike ( conLikeName )
|
| 35 | 36 | import GHC.Core.FVs
|
| ... | ... | @@ -674,6 +675,7 @@ instance ToHie (Context (Located (WithUserRdr Name))) where |
| 674 | 675 | |
| 675 | 676 | evVarsOfTermList :: EvTerm -> [EvId]
|
| 676 | 677 | evVarsOfTermList (EvExpr e) = exprSomeFreeVarsList isEvVar e
|
| 678 | +evVarsOfTermList (EvCastExpr e co _ty) = exprSomeFreeVarsList isEvVar (Cast e co) -- TODO really
|
|
| 677 | 679 | evVarsOfTermList (EvTypeable _ ev) =
|
| 678 | 680 | case ev of
|
| 679 | 681 | EvTypeableTyCon _ e -> concatMap evVarsOfTermList e
|
| ... | ... | @@ -36,8 +36,8 @@ import GHC.Core.Predicate |
| 36 | 36 | import GHC.Core.Reduction
|
| 37 | 37 | import GHC.Core.Coercion
|
| 38 | 38 | import GHC.Core.Class( classHasSCs )
|
| 39 | -import GHC.Core.TyCo.FVs
|
|
| 40 | -import GHC.Core.TyCo.Rep (Coercion(..))
|
|
| 39 | +-- import GHC.Core.TyCo.FVs
|
|
| 40 | +-- import GHC.Core.TyCo.Rep (Coercion(..))
|
|
| 41 | 41 | |
| 42 | 42 | import GHC.Types.Id( idType )
|
| 43 | 43 | import GHC.Types.Var( EvVar, tyVarKind )
|
| ... | ... | @@ -52,7 +52,7 @@ import GHC.Utils.Panic |
| 52 | 52 | import GHC.Utils.Misc
|
| 53 | 53 | |
| 54 | 54 | import GHC.Driver.Session
|
| 55 | -import GHC.Driver.DynFlags ( hasZapCasts )
|
|
| 55 | +-- import GHC.Driver.DynFlags ( hasZapCasts )
|
|
| 56 | 56 | |
| 57 | 57 | import Data.List( deleteFirstsBy )
|
| 58 | 58 | |
| ... | ... | @@ -1457,12 +1457,12 @@ finish_rewrite |
| 1457 | 1457 | (Reduction co new_pred)
|
| 1458 | 1458 | rewriters
|
| 1459 | 1459 | = assert (isEmptyRewriterSet rewriters) $ -- this is a Given, not a wanted
|
| 1460 | - do { zap_casts <- hasZapCasts <$> getDynFlags
|
|
| 1460 | + do { -- zap_casts <- hasZapCasts <$> getDynFlags
|
|
| 1461 | 1461 | ; let loc = ctEvLoc ev
|
| 1462 | 1462 | -- mkEvCast optimises ReflCo
|
| 1463 | 1463 | ev_rw_role = ctEvRewriteRole ev
|
| 1464 | 1464 | new_tm = assert (coercionRole co == ev_rw_role)
|
| 1465 | - evCastCo (evId old_evar) (mkCastCoercion zap_casts new_pred (downgradeRole Representational ev_rw_role co))
|
|
| 1465 | + evCastCo (evId old_evar) (downgradeRole Representational ev_rw_role co) new_pred
|
|
| 1466 | 1466 | ; new_ev <- newGivenEvVar loc (new_pred, new_tm)
|
| 1467 | 1467 | ; continueWith $ CtGiven new_ev }
|
| 1468 | 1468 | |
| ... | ... | @@ -1470,14 +1470,14 @@ finish_rewrite |
| 1470 | 1470 | ev@(CtWanted (WantedCt { ctev_pred = old_pred, ctev_rewriters = rewriters, ctev_dest = dest }))
|
| 1471 | 1471 | (Reduction co new_pred)
|
| 1472 | 1472 | new_rewriters
|
| 1473 | - = do { zap_casts <- hasZapCasts <$> getDynFlags
|
|
| 1473 | + = do { -- zap_casts <- hasZapCasts <$> getDynFlags
|
|
| 1474 | 1474 | ; let loc = ctEvLoc ev
|
| 1475 | 1475 | rewriters' = rewriters S.<> new_rewriters
|
| 1476 | 1476 | ev_rw_role = ctEvRewriteRole ev
|
| 1477 | 1477 | ; mb_new_ev <- newWanted loc rewriters' new_pred
|
| 1478 | 1478 | ; massert (coercionRole co == ev_rw_role)
|
| 1479 | 1479 | ; setWantedEvTerm dest EvCanonical $
|
| 1480 | - evCastCo (getEvExpr mb_new_ev) (mkCastCoercion zap_casts old_pred (downgradeRole Representational ev_rw_role (mkSymCo co)))
|
|
| 1480 | + evCastCo (getEvExpr mb_new_ev) (downgradeRole Representational ev_rw_role (mkSymCo co)) old_pred
|
|
| 1481 | 1481 | ; case mb_new_ev of
|
| 1482 | 1482 | Fresh new_ev -> continueWith $ CtWanted new_ev
|
| 1483 | 1483 | Cached _ -> stopWith ev "Cached wanted" }
|
| ... | ... | @@ -1492,10 +1492,10 @@ finish_rewrite |
| 1492 | 1492 | --
|
| 1493 | 1493 | -- See Note [Zapped casts] in GHC.Core.TyCo.Rep.
|
| 1494 | 1494 | --
|
| 1495 | -mkCastCoercion :: Bool -> Type -> Coercion -> CastCoercion
|
|
| 1496 | -mkCastCoercion zap_casts lhs_ty co
|
|
| 1497 | - | isSmallCo co || not zap_casts = CCoercion co
|
|
| 1498 | - | otherwise = ZCoercion lhs_ty (shallowCoVarsOfCo co)
|
|
| 1495 | +-- mkCastCoercion :: Bool -> Type -> Coercion -> CastCoercion
|
|
| 1496 | +-- mkCastCoercion zap_casts lhs_ty co
|
|
| 1497 | +-- | isSmallCo co || not zap_casts = CCoercion co
|
|
| 1498 | +-- | otherwise = ZCoercion lhs_ty (shallowCoVarsOfCo co)
|
|
| 1499 | 1499 | |
| 1500 | 1500 | -- | Is this coercion probably smaller than its type? This is a rough heuristic,
|
| 1501 | 1501 | -- but crucially we treat axioms (perhaps wrapped in Sym/Sub/etc.) as small
|
| ... | ... | @@ -1505,24 +1505,24 @@ mkCastCoercion zap_casts lhs_ty co |
| 1505 | 1505 | --
|
| 1506 | 1506 | -- so we want to cast by `CCoercion (axF <Int>)` rather than `ZCoercion SomeVeryBigType []`.
|
| 1507 | 1507 | --
|
| 1508 | -isSmallCo :: Coercion -> Bool
|
|
| 1509 | -isSmallCo Refl{} = True
|
|
| 1510 | -isSmallCo GRefl{} = True
|
|
| 1511 | -isSmallCo AxiomCo{} = True
|
|
| 1512 | -isSmallCo CoVarCo{} = True
|
|
| 1513 | -isSmallCo (SymCo co) = isSmallCo co
|
|
| 1514 | -isSmallCo (KindCo co) = isSmallCo co
|
|
| 1515 | -isSmallCo (SubCo co) = isSmallCo co
|
|
| 1516 | -isSmallCo TyConAppCo{} = False
|
|
| 1517 | -isSmallCo AppCo{} = False
|
|
| 1518 | -isSmallCo ForAllCo{} = False
|
|
| 1519 | -isSmallCo FunCo{} = False
|
|
| 1520 | -isSmallCo UnivCo{} = False
|
|
| 1521 | -isSmallCo TransCo{} = False
|
|
| 1522 | -isSmallCo SelCo{} = False
|
|
| 1523 | -isSmallCo LRCo{} = False
|
|
| 1524 | -isSmallCo InstCo{} = False
|
|
| 1525 | -isSmallCo HoleCo{} = False
|
|
| 1508 | +-- isSmallCo :: Coercion -> Bool
|
|
| 1509 | +-- isSmallCo Refl{} = True
|
|
| 1510 | +-- isSmallCo GRefl{} = True
|
|
| 1511 | +-- isSmallCo AxiomCo{} = True
|
|
| 1512 | +-- isSmallCo CoVarCo{} = True
|
|
| 1513 | +-- isSmallCo (SymCo co) = isSmallCo co
|
|
| 1514 | +-- isSmallCo (KindCo co) = isSmallCo co
|
|
| 1515 | +-- isSmallCo (SubCo co) = isSmallCo co
|
|
| 1516 | +-- isSmallCo TyConAppCo{} = False
|
|
| 1517 | +-- isSmallCo AppCo{} = False
|
|
| 1518 | +-- isSmallCo ForAllCo{} = False
|
|
| 1519 | +-- isSmallCo FunCo{} = False
|
|
| 1520 | +-- isSmallCo UnivCo{} = False
|
|
| 1521 | +-- isSmallCo TransCo{} = False
|
|
| 1522 | +-- isSmallCo SelCo{} = False
|
|
| 1523 | +-- isSmallCo LRCo{} = False
|
|
| 1524 | +-- isSmallCo InstCo{} = False
|
|
| 1525 | +-- isSmallCo HoleCo{} = False
|
|
| 1526 | 1526 | |
| 1527 | 1527 | |
| 1528 | 1528 | {- *******************************************************************
|
| ... | ... | @@ -502,6 +502,8 @@ mkGivenEvBind ev tm = EvBind { eb_info = EvBindGiven, eb_lhs = ev, eb_rhs = tm } |
| 502 | 502 | data EvTerm
|
| 503 | 503 | = EvExpr EvExpr
|
| 504 | 504 | |
| 505 | + | EvCastExpr EvExpr TcCastCoercion TcType
|
|
| 506 | + |
|
| 505 | 507 | | EvTypeable Type EvTypeable -- Dictionary for (Typeable ty)
|
| 506 | 508 | |
| 507 | 509 | | EvFun -- /\as \ds. let binds in v
|
| ... | ... | @@ -530,10 +532,10 @@ evCoercion co = EvExpr (Coercion co) |
| 530 | 532 | -- | d |> co
|
| 531 | 533 | evCast :: EvExpr -> TcCoercion -> EvTerm
|
| 532 | 534 | evCast et tc | isReflCo tc = EvExpr et
|
| 533 | - | otherwise = evCastCo et (CCoercion tc)
|
|
| 535 | + | otherwise = EvExpr (Cast et (CCoercion tc))
|
|
| 534 | 536 | |
| 535 | -evCastCo :: EvExpr -> TcCastCoercion -> EvTerm
|
|
| 536 | -evCastCo et tc = EvExpr (Cast et tc)
|
|
| 537 | +evCastCo :: EvExpr -> TcCoercion -> TcType -> EvTerm
|
|
| 538 | +evCastCo et co co_res_ty = EvCastExpr et (CCoercion co) co_res_ty
|
|
| 537 | 539 | |
| 538 | 540 | -- Dictionary instance application
|
| 539 | 541 | evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm
|
| ... | ... | @@ -889,6 +891,7 @@ findNeededEvVars ev_binds seeds |
| 889 | 891 | |
| 890 | 892 | evVarsOfTerm :: EvTerm -> VarSet
|
| 891 | 893 | evVarsOfTerm (EvExpr e) = exprSomeFreeVars isEvVar e
|
| 894 | +evVarsOfTerm (EvCastExpr e co _ty) = exprSomeFreeVars isEvVar (Cast e co) -- TODO safe to ignore ty here?
|
|
| 892 | 895 | evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev
|
| 893 | 896 | evVarsOfTerm (EvFun {}) = emptyVarSet -- See Note [Free vars of EvFun]
|
| 894 | 897 | |
| ... | ... | @@ -985,6 +988,7 @@ instance Outputable EvBind where |
| 985 | 988 | |
| 986 | 989 | instance Outputable EvTerm where
|
| 987 | 990 | ppr (EvExpr e) = ppr e
|
| 991 | + ppr (EvCastExpr e co ty) = text "EvCastExpr" <+> ppr e <+> ppr co <+> ppr ty
|
|
| 988 | 992 | ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
|
| 989 | 993 | ppr (EvFun { et_tvs = tvs, et_given = gs, et_binds = bs, et_body = w })
|
| 990 | 994 | = hang (text "\\" <+> sep (map pprLamBndr (tvs ++ gs)) <+> arrow)
|
| ... | ... | @@ -59,6 +59,7 @@ import GHC.Tc.Zonk.TcType |
| 59 | 59 | ( tcInitTidyEnv, tcInitOpenTidyEnv
|
| 60 | 60 | , writeMetaTyVarRef
|
| 61 | 61 | , checkCoercionHole
|
| 62 | + , unpackCoercionHole_maybe
|
|
| 62 | 63 | , zonkCoVar )
|
| 63 | 64 | |
| 64 | 65 | import GHC.Core.Type
|
| ... | ... | @@ -97,6 +98,9 @@ import Control.Monad |
| 97 | 98 | import Control.Monad.Trans.Class ( lift )
|
| 98 | 99 | import Data.List.NonEmpty ( NonEmpty )
|
| 99 | 100 | import Data.Foldable ( toList )
|
| 101 | +import Data.Semigroup
|
|
| 102 | + |
|
| 103 | +import GHC.Driver.DynFlags ( getDynFlags, hasZapCasts )
|
|
| 100 | 104 | |
| 101 | 105 | {- Note [What is zonking?]
|
| 102 | 106 | ~~~~~~~~~~~~~~~~~~~~~~~~~~
|
| ... | ... | @@ -1762,9 +1766,49 @@ Wrinkles: |
| 1762 | 1766 | ************************************************************************
|
| 1763 | 1767 | -}
|
| 1764 | 1768 | |
| 1769 | +zonkShallowCoVarsOfCo :: TcCoercion -> ZonkTcM CoVarSet
|
|
| 1770 | +zonkShallowCoVarsOfCo co
|
|
| 1771 | + = unZCVSM $ go_co co
|
|
| 1772 | + where
|
|
| 1773 | + go_hole :: CoercionHole -> ZonkTcM CoVarSet
|
|
| 1774 | + go_hole hole
|
|
| 1775 | + = do { m_co <- lift $ liftZonkM $ unpackCoercionHole_maybe hole
|
|
| 1776 | + ; case m_co of
|
|
| 1777 | + Nothing -> return emptyVarSet -- Not filled (TODO emit log message?)
|
|
| 1778 | + Just co -> unZCVSM (go_co co) } -- Filled: look inside
|
|
| 1779 | + |
|
| 1780 | + go_co :: Coercion -> ZonkCoVarSetMonoid
|
|
| 1781 | + (_, _, go_co, _) = foldTyCo folder ()
|
|
| 1782 | + |
|
| 1783 | + folder :: TyCoFolder () ZonkCoVarSetMonoid
|
|
| 1784 | + folder = TyCoFolder { tcf_view = noView
|
|
| 1785 | + , tcf_tyvar = \ _ _ -> mempty
|
|
| 1786 | + , tcf_covar = \ _ cv -> ZCVSM (pure (unitVarSet cv))
|
|
| 1787 | + , tcf_hole = \ _ -> ZCVSM . go_hole
|
|
| 1788 | + , tcf_tycobinder = \ _ _ _ -> () }
|
|
| 1789 | + |
|
| 1790 | +newtype ZonkCoVarSetMonoid = ZCVSM { unZCVSM :: ZonkTcM CoVarSet }
|
|
| 1791 | + |
|
| 1792 | +instance Semigroup ZonkCoVarSetMonoid where
|
|
| 1793 | + ZCVSM l <> ZCVSM r = ZCVSM (unionVarSet <$> l <*> r)
|
|
| 1794 | + |
|
| 1795 | +instance Monoid ZonkCoVarSetMonoid where
|
|
| 1796 | + mempty = ZCVSM (return emptyVarSet)
|
|
| 1797 | + |
|
| 1798 | + |
|
| 1799 | + |
|
| 1765 | 1800 | zonkEvTerm :: EvTerm -> ZonkTcM EvTerm
|
| 1766 | 1801 | zonkEvTerm (EvExpr e)
|
| 1767 | 1802 | = EvExpr <$> zonkCoreExpr e
|
| 1803 | +zonkEvTerm (EvCastExpr e (CCoercion co) co_res_ty)
|
|
| 1804 | + = do { zap_casts <- hasZapCasts <$> lift getDynFlags
|
|
| 1805 | + ; co_res_ty' <- zonkTcTypeToTypeX co_res_ty
|
|
| 1806 | + ; if zap_casts
|
|
| 1807 | + then EvCastExpr <$> zonkCoreExpr e <*> (ZCoercion co_res_ty' <$> zonkShallowCoVarsOfCo co) <*> pure co_res_ty'
|
|
| 1808 | + else EvExpr <$> zonkCoreExpr (Cast e (CCoercion co))
|
|
| 1809 | + }
|
|
| 1810 | +zonkEvTerm ev@(EvCastExpr _ (ZCoercion{}) _)
|
|
| 1811 | + = pprPanic "zonkEvTerm: ZCoercion" (ppr ev)
|
|
| 1768 | 1812 | zonkEvTerm (EvTypeable ty ev)
|
| 1769 | 1813 | = EvTypeable <$> zonkTcTypeToTypeX ty <*> zonkEvTypeable ev
|
| 1770 | 1814 | zonkEvTerm (EvFun { et_tvs = tvs, et_given = evs
|
| ... | ... | @@ -15,6 +15,7 @@ other dynamic, non-language, flag settings: |
| 15 | 15 | -fshow-warning-groups
|
| 16 | 16 | -fprefer-byte-code
|
| 17 | 17 | -fbreak-points
|
| 18 | + -fno-zap-casts
|
|
| 18 | 19 | warning settings:
|
| 19 | 20 | -Wpattern-namespace-specifier
|
| 20 | 21 | ~~~~~~~~~~ Testing :set -a
|