[Git][ghc/ghc][wip/cfuneqcan-refactor] 3 commits: Make the fast path work without roles
Richard Eisenberg
gitlab at gitlab.haskell.org
Tue Nov 24 03:50:05 UTC 2020
Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC
Commits:
f8237cf7 by Richard Eisenberg at 2020-11-23T22:08:58+00:00
Make the fast path work without roles
- - - - -
e5353131 by Richard Eisenberg at 2020-11-24T01:31:09+00:00
Use MCo
- - - - -
62d06215 by Richard Eisenberg at 2020-11-24T01:37:58+00:00
Remove unused parameter
- - - - -
4 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/FamInstEnv.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Flatten.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -70,8 +70,9 @@ module GHC.Core.Coercion (
isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
isReflCoVar_maybe, isGReflMCo, mkGReflLeftMCo, mkGReflRightMCo,
+ mkCoherenceRightMCo,
- coToMCo, mkTransMCo, mkTransMCoL, mkCastTyMCo, mkSymMCo,
+ coToMCo, mkTransMCo, mkTransMCoL, mkCastTyMCo, mkSymMCo, isReflMCo,
-- ** Coercion variables
mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
@@ -352,6 +353,15 @@ mkGReflRightMCo :: Role -> Type -> MCoercionN -> Coercion
mkGReflRightMCo r ty MRefl = mkReflCo r ty
mkGReflRightMCo r ty (MCo co) = mkGReflRightCo r ty co
+-- | Like 'mkCoherenceRightCo', but with an 'MCoercion'
+mkCoherenceRightMCo :: Role -> Type -> MCoercionN -> Coercion -> Coercion
+mkCoherenceRightMCo _ _ MRefl co2 = co2
+mkCoherenceRightMCo r ty (MCo co) co2 = mkCoherenceRightCo r ty co co2
+
+isReflMCo :: MCoercion -> Bool
+isReflMCo MRefl = True
+isReflMCo _ = False
+
{-
%************************************************************************
%* *
@@ -2939,7 +2949,7 @@ simplifyArgsWorker :: [TyCoBinder] -> Kind
-> [(Type, Coercion)] -- flattened type arguments, arg
-- each comes with the coercion used to flatten it,
-- with co :: flattened_type ~ original_type
- -> ([Type], [Coercion], CoercionN)
+ -> ([Type], [Coercion], MCoercionN)
-- Returns (xis, cos, res_co), where each co :: xi ~ arg,
-- and res_co :: kind (f xis) ~ kind (f tys), where f is the function applied to the args
-- Precondition: if f :: forall bndrs. inner_ki (where bndrs and inner_ki are passed in),
@@ -2961,14 +2971,15 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
-> Kind -- Unsubsted result kind of function (not a Pi-type)
-> [Role] -- Roles at which to flatten these ...
-> [(Type, Coercion)] -- flattened arguments, with their flattening coercions
- -> ([Type], [Coercion], CoercionN)
+ -> ([Type], [Coercion], MCoercionN)
go acc_xis acc_cos !lc binders inner_ki _ []
-- The !lc makes the function strict in the lifting context
-- which means GHC can unbox that pair. A modest win.
= (reverse acc_xis, reverse acc_cos, kind_co)
where
final_kind = mkPiTys binders inner_ki
- kind_co = liftCoSubst Nominal lc final_kind
+ kind_co | noFreeVarsOfType final_kind = MRefl
+ | otherwise = MCo $ liftCoSubst Nominal lc final_kind
go acc_xis acc_cos lc (binder:binders) inner_ki (role:roles) ((xi,co):args)
= -- By Note [Flattening] in GHC.Tc.Solver.Flatten invariant (F2),
@@ -3024,7 +3035,7 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
(xis_out, cos_out, res_co_out)
= go acc_xis acc_cos zapped_lc bndrs new_inner roles casted_args
in
- (xis_out, cos_out, res_co_out `mkTransCo` res_co)
+ (xis_out, cos_out, res_co_out `mkTransMCoL` res_co)
go _ _ _ _ _ _ _ = panic
"simplifyArgsWorker wandered into deeper water than usual"
=====================================
compiler/GHC/Core/FamInstEnv.hs
=====================================
@@ -1319,7 +1319,7 @@ topNormaliseType_maybe env ty
tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
tyFamStepper rec_nts tc tys -- Try to step a type/data family
= case topReduceTyFamApp_maybe env tc tys of
- Just (co, rhs, res_co) -> NS_Step rec_nts rhs (co, MCo res_co)
+ Just (co, rhs, res_co) -> NS_Step rec_nts rhs (co, res_co)
_ -> NS_Done
---------------
@@ -1365,14 +1365,14 @@ normalise_tc_app tc tys
assemble_result :: Role -- r, ambient role in NormM monad
-> Type -- nty, result type, possibly of changed kind
-> Coercion -- orig_ty ~r nty, possibly heterogeneous
- -> CoercionN -- typeKind(orig_ty) ~N typeKind(nty)
+ -> MCoercionN -- typeKind(orig_ty) ~N typeKind(nty)
-> (Coercion, Type) -- (co :: orig_ty ~r nty_casted, nty_casted)
-- where nty_casted has same kind as orig_ty
assemble_result r nty orig_to_nty kind_co
= ( final_co, nty_old_kind )
where
- nty_old_kind = nty `mkCastTy` mkSymCo kind_co
- final_co = mkCoherenceRightCo r nty (mkSymCo kind_co) orig_to_nty
+ nty_old_kind = nty `mkCastTyMCo` mkSymMCo kind_co
+ final_co = mkCoherenceRightMCo r nty (mkSymMCo kind_co) orig_to_nty
---------------
-- | Try to simplify a type-family application, by *one* step
@@ -1381,7 +1381,7 @@ normalise_tc_app tc tys
-- res_co :: typeKind(F tys) ~ typeKind(rhs)
-- Type families and data families; always Representational role
topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type]
- -> Maybe (Coercion, Type, Coercion)
+ -> Maybe (Coercion, Type, MCoercion)
topReduceTyFamApp_maybe envs fam_tc arg_tys
| isFamilyTyCon fam_tc -- type families and data families
, Just (co, rhs) <- reduceTyFamApp_maybe envs role fam_tc ntys
@@ -1394,7 +1394,7 @@ topReduceTyFamApp_maybe envs fam_tc arg_tys
normalise_tc_args fam_tc arg_tys
normalise_tc_args :: TyCon -> [Type] -- tc tys
- -> NormM (Coercion, [Type], CoercionN)
+ -> NormM (Coercion, [Type], MCoercionN)
-- (co, new_tys), where
-- co :: tc tys ~ tc new_tys; might not be homogeneous
-- res_co :: typeKind(tc tys) ~N typeKind(tc new_tys)
@@ -1477,14 +1477,14 @@ normalise_type ty
; role <- getRole
; let nty = mkAppTys nfun nargs
nco = mkAppCos fun_co args_cos
- nty_casted = nty `mkCastTy` mkSymCo res_co
- final_co = mkCoherenceRightCo role nty (mkSymCo res_co) nco
+ nty_casted = nty `mkCastTyMCo` mkSymMCo res_co
+ final_co = mkCoherenceRightMCo role nty (mkSymMCo res_co) nco
; return (final_co, nty_casted) } }
normalise_args :: Kind -- of the function
-> [Role] -- roles at which to normalise args
-> [Type] -- args
- -> NormM ([Coercion], [Type], Coercion)
+ -> NormM ([Coercion], [Type], MCoercion)
-- returns (cos, xis, res_co), where each xi is the normalised
-- version of the corresponding type, each co is orig_arg ~ xi,
-- and the res_co :: kind(f orig_args) ~ kind(f xis)
@@ -1494,7 +1494,7 @@ normalise_args :: Kind -- of the function
normalise_args fun_ki roles args
= do { normed_args <- zipWithM normalise1 roles args
; let (xis, cos, res_co) = simplifyArgsWorker ki_binders inner_ki fvs roles normed_args
- ; return (map mkSymCo cos, xis, mkSymCo res_co) }
+ ; return (map mkSymCo cos, xis, mkSymMCo res_co) }
where
(ki_binders, inner_ki) = splitPiTys fun_ki
fvs = tyCoVarsOfTypes args
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -200,8 +200,7 @@ canClass :: CtEvidence
canClass ev cls tys pend_sc
= -- all classes do *nominal* matching
ASSERT2( ctEvRole ev == Nominal, ppr ev $$ ppr cls $$ ppr tys )
- do { (xis, cos, _kind_co) <- flattenArgsNom ev cls_tc tys
- ; MASSERT( isTcReflCo _kind_co )
+ do { (xis, cos) <- flattenArgsNom ev cls_tc tys
; let co = mkTcTyConAppCo Nominal cls_tc cos
xi = mkClassPred cls xis
mk_ct new_ev = CDictCan { cc_ev = new_ev
=====================================
compiler/GHC/Tc/Solver/Flatten.hs
=====================================
@@ -127,6 +127,7 @@ setEqRel new_eq_rel thing_inside
if new_eq_rel == fe_eq_rel env
then runFlatM thing_inside env
else runFlatM thing_inside (env { fe_eq_rel = new_eq_rel })
+{-# INLINE setEqRel #-}
-- | Make sure that flattening actually produces a coercion (in other
-- words, make sure our flavour is not Derived)
@@ -237,23 +238,24 @@ flattenKind loc flav ty
; return (ty', co) }
-- See Note [Flattening]
-flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion], TcCoercionN)
+flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion])
-- Externally-callable, hence runFlatten
-- Flatten a vector of types all at once; in fact they are
-- always the arguments of type family or class, so
-- ctEvFlavour ev = Nominal
-- and we want to flatten all at nominal role
-- The kind passed in is the kind of the type family or class, call it T
--- The last coercion returned has type (tcTypeKind(T xis) ~N tcTypeKind(T tys))
+-- The kind of T args must be constant (i.e. not depend on the args)
--
-- For Derived constraints the returned coercion may be undefined
-- because flattening may use a Derived equality ([D] a ~ ty)
flattenArgsNom ev tc tys
= do { traceTcS "flatten_args {" (vcat (map ppr tys))
; (tys', cos, kind_co)
- <- runFlattenCtEv ev (flatten_args_tc tc (repeat Nominal) tys)
+ <- runFlattenCtEv ev (flatten_args_tc tc Nothing tys)
+ ; MASSERT( isReflMCo kind_co )
; traceTcS "flatten }" (vcat (map ppr tys'))
- ; return (tys', cos, kind_co) }
+ ; return (tys', cos) }
-- | Flatten a type w.r.t. nominal equality. This is useful to rewrite
-- a type w.r.t. any givens. It does not do type-family reduction. This
@@ -381,14 +383,15 @@ we skip adding to the cache here.
{-# INLINE flatten_args_tc #-}
flatten_args_tc
:: TyCon -- T
- -> [Role] -- Role r
+ -> Maybe [Role] -- Nothing: ambient role is Nominal; all args are Nominal
+ -- Otherwise: no assumptions; use roles provided
-> [Type] -- Arg types [t1,..,tn]
-> FlatM ( [Xi] -- List of flattened args [x1,..,xn]
-- 1-1 corresp with [t1,..,tn]
, [Coercion] -- List of arg coercions [co1,..,con]
-- 1-1 corresp with [t1,..,tn]
-- coi :: xi ~r ti
- , CoercionN) -- Result coercion, rco
+ , MCoercionN) -- Result coercion, rco
-- rco : (T t1..tn) ~N (T (x1 |> co1) .. (xn |> con))
flatten_args_tc tc = flatten_args all_bndrs any_named_bndrs inner_ki emptyVarSet
-- NB: TyCon kinds are always closed
@@ -406,8 +409,9 @@ flatten_args_tc tc = flatten_args all_bndrs any_named_bndrs inner_ki emptyVarSet
flatten_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are
-- named.
-> Kind -> TcTyCoVarSet -- function kind; kind's free vars
- -> [Role] -> [Type] -- these are in 1-to-1 correspondence
- -> FlatM ([Xi], [Coercion], CoercionN)
+ -> Maybe [Role] -> [Type] -- these are in 1-to-1 correspondence
+ -- Nothing: use all Nominal
+ -> FlatM ([Xi], [Coercion], MCoercionN)
-- Coercions :: Xi ~ Type, at roles given
-- Third coercion :: tcTypeKind(fun xis) ~N tcTypeKind(fun tys)
-- That is, the third coercion relates the kind of some function (whose kind is
@@ -419,15 +423,12 @@ flatten_args orig_binders
any_named_bndrs
orig_inner_ki
orig_fvs
- orig_roles
+ orig_m_roles
orig_tys
- = if any_named_bndrs
- then flatten_args_slow orig_binders
- orig_inner_ki
- orig_fvs
- orig_roles
- orig_tys
- else flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
+ = case (orig_m_roles, any_named_bndrs) of
+ (Nothing, False) -> flatten_args_fast orig_tys
+ _ -> flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
+ where orig_roles = fromMaybe (repeat Nominal) orig_m_roles
{-# INLINE flatten_args_fast #-}
-- | fast path flatten_args, in which none of the binders are named and
@@ -435,75 +436,30 @@ flatten_args orig_binders
-- There are many bang patterns in here. It's been observed that they
-- greatly improve performance of an optimized build.
-- The T9872 test cases are good witnesses of this fact.
-flatten_args_fast :: [TyCoBinder]
- -> Kind
- -> [Role]
- -> [Type]
- -> FlatM ([Xi], [Coercion], CoercionN)
-flatten_args_fast orig_binders orig_inner_ki orig_roles orig_tys
- = fmap finish (iterate orig_tys orig_roles orig_binders)
+flatten_args_fast :: [Type]
+ -> FlatM ([Xi], [Coercion], MCoercionN)
+flatten_args_fast orig_tys
+ = fmap finish (iterate orig_tys)
where
iterate :: [Type]
- -> [Role]
- -> [TyCoBinder]
- -> FlatM ([Xi], [Coercion], [TyCoBinder])
- iterate (ty:tys) (role:roles) (_:binders) = do
- (xi, co) <- go role ty
- (xis, cos, binders) <- iterate tys roles binders
- pure (xi : xis, co : cos, binders)
- iterate [] _ binders = pure ([], [], binders)
- iterate _ _ _ = pprPanic
- "flatten_args wandered into deeper water than usual" (vcat [])
- -- This debug information is commented out because leaving it in
- -- causes a ~2% increase in allocations in T9872{a,c,d}.
- {-
- (vcat [ppr orig_binders,
- ppr orig_inner_ki,
- ppr (take 10 orig_roles), -- often infinite!
- ppr orig_tys])
- -}
-
- {-# INLINE go #-}
- go :: Role
- -> Type
- -> FlatM (Xi, Coercion)
- go role ty
- = case role of
- -- In the slow path we bind the Xi and Coercion from the recursive
- -- call and then use it such
- --
- -- let kind_co = mkTcSymCo $ mkReflCo Nominal (tyBinderType binder)
- -- casted_xi = xi `mkCastTy` kind_co
- -- casted_co = xi |> kind_co ~r xi ; co
- --
- -- but this isn't necessary:
- -- mkTcSymCo (Refl a b) = Refl a b,
- -- mkCastTy x (Refl _ _) = x
- -- mkTcGReflLeftCo _ ty (Refl _ _) `mkTransCo` co = co
- --
- -- Also, no need to check isAnonTyCoBinder or isNamedBinder, since
- -- we've already established that they're all anonymous.
- Nominal -> setEqRel NomEq $ flatten_one ty
- Representational -> setEqRel ReprEq $ flatten_one ty
- Phantom -> -- See Note [Phantoms in the flattener]
- do { ty <- liftTcS $ zonkTcType ty
- ; return (ty, mkReflCo Phantom ty) }
-
+ -> FlatM ([Xi], [Coercion])
+ iterate (ty:tys) = do
+ (xi, co) <- flatten_one ty
+ (xis, cos) <- iterate tys
+ pure (xi : xis, co : cos)
+ iterate [] = pure ([], [])
{-# INLINE finish #-}
- finish :: ([Xi], [Coercion], [TyCoBinder]) -> ([Xi], [Coercion], CoercionN)
- finish (xis, cos, binders) = (xis, cos, kind_co)
- where
- final_kind = mkPiTys binders orig_inner_ki
- kind_co = mkNomReflCo final_kind
+ finish :: ([Xi], [Coercion]) -> ([Xi], [Coercion], MCoercionN)
+ finish (xis, cos) = (xis, cos, MRefl)
{-# INLINE flatten_args_slow #-}
-- | Slow path, compared to flatten_args_fast, because this one must track
-- a lifting context.
flatten_args_slow :: [TyCoBinder] -> Kind -> TcTyCoVarSet
-> [Role] -> [Type]
- -> FlatM ([Xi], [Coercion], CoercionN)
+ -> FlatM ([Xi], [Coercion], MCoercionN)
flatten_args_slow binders inner_ki fvs roles tys
-- Arguments used dependently must be flattened with proper coercions, but
-- we're not guaranteed to get a proper coercion when flattening with the
@@ -671,7 +627,9 @@ flatten_app_ty_args fun_xi fun_co arg_tys
flatten_ty_con_app :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
flatten_ty_con_app tc tys
= do { role <- getRole
- ; (xis, cos, kind_co) <- flatten_args_tc tc (tyConRolesX role tc) tys
+ ; let m_roles | Nominal <- role = Nothing
+ | otherwise = Just $ tyConRolesX role tc
+ ; (xis, cos, kind_co) <- flatten_args_tc tc m_roles tys
; let tyconapp_xi = mkTyConApp tc xis
tyconapp_co = mkTyConAppCo role tc cos
; return (homogenise_result tyconapp_xi tyconapp_co role kind_co) }
@@ -680,15 +638,12 @@ flatten_ty_con_app tc tys
homogenise_result :: Xi -- a flattened type
-> Coercion -- :: xi ~r original ty
-> Role -- r
- -> CoercionN -- kind_co :: tcTypeKind(xi) ~N tcTypeKind(ty)
+ -> MCoercionN -- kind_co :: tcTypeKind(xi) ~N tcTypeKind(ty)
-> (Xi, Coercion) -- (xi |> kind_co, (xi |> kind_co)
-- ~r original ty)
-homogenise_result xi co r kind_co
- -- the explicit pattern match here improves the performance of T9872a, b, c by
- -- ~2%
- | isGReflCo kind_co = (xi `mkCastTy` kind_co, co)
- | otherwise = (xi `mkCastTy` kind_co
- , (mkSymCo $ GRefl r xi (MCo kind_co)) `mkTransCo` co)
+homogenise_result xi co _ MRefl = (xi, co)
+homogenise_result xi co r mco@(MCo kind_co)
+ = (xi `mkCastTy` kind_co, (mkSymCo $ GRefl r xi mco) `mkTransCo` co)
{-# INLINE homogenise_result #-}
-- Flatten a vector (list of arguments).
@@ -696,7 +651,7 @@ flatten_vector :: Kind -- of the function being applied to these arguments
-> [Role] -- If we're flatten w.r.t. ReprEq, what roles do the
-- args have?
-> [Type] -- the args to flatten
- -> FlatM ([Xi], [Coercion], CoercionN)
+ -> FlatM ([Xi], [Coercion], MCoercionN)
flatten_vector ki roles tys
= do { eq_rel <- getEqRel
; case eq_rel of
@@ -704,17 +659,17 @@ flatten_vector ki roles tys
any_named_bndrs
inner_ki
fvs
- (repeat Nominal)
+ Nothing
tys
ReprEq -> flatten_args bndrs
any_named_bndrs
inner_ki
fvs
- roles
+ (Just roles)
tys
}
where
- (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki
+ (bndrs, inner_ki, any_named_bndrs) = split_pi_tys' ki -- "RAE" fix
fvs = tyCoVarsOfType ki
{-# INLINE flatten_vector #-}
@@ -840,10 +795,14 @@ flatten_exact_fam_app tc tys
; Nothing ->
-- That didn't work. So reduce the arguments, in STEP 3.
- do { (xis, cos, kind_co) <- flatten_args_tc tc (repeat Nominal) tys
+ do { eq_rel <- getEqRel
+ -- checking eq_rel == NomEq saves ~0.5% in T9872a
+ ; (xis, cos, kind_co) <- if eq_rel == NomEq
+ then flatten_args_tc tc Nothing tys
+ else setEqRel NomEq $
+ flatten_args_tc tc Nothing tys
-- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys)
- ; eq_rel <- getEqRel
; let role = eqRelRole eq_rel
args_co = mkTyConAppCo role tc cos
-- args_co :: F xis ~r F tys
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f2bbcc402adb211c78cf185e0cda194e6f8d87b1...62d06215790ee056fbca69e6724a096bec00f8b0
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/f2bbcc402adb211c78cf185e0cda194e6f8d87b1...62d06215790ee056fbca69e6724a096bec00f8b0
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20201123/3f4db9e2/attachment-0001.html>
More information about the ghc-commits
mailing list