I'm dubious of the coercionRole refactor, as it undoes a refactoring I
#11735: Optimize coercionKind -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: Compile-time | Unknown/Multiple performance bug | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by tdammers): Replying to [comment:16 simonpj]: put in a few years ago, for performance reasons.
I looked at what code would be needed for `coercionRole` and its a
remarkably short and simple function. Tobias, would to like to post the code? Of course. Here's the patch: {{{ diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index e1a5b7cde0..36874a4c4d 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -1783,77 +1783,53 @@ coercionKinds tys = sequenceA $ map coercionKind tys -- | Get a coercion's kind and role. -- Why both at once? See Note [Computing a coercion kind and role] coercionKindRole :: Coercion -> (Pair Type, Role) -coercionKindRole = go +coercionKindRole co = (coercionKind co, coercionRole co) + +-- | Retrieve the role from a coercion. +coercionRole :: Coercion -> Role +coercionRole = go where - go (Refl r ty) = (Pair ty ty, r) - go (TyConAppCo r tc cos) - = (mkTyConApp tc <$> (sequenceA $ map coercionKind cos), r) - go (AppCo co1 co2) - = let (tys1, r1) = go co1 in - (mkAppTy <$> tys1 <*> coercionKind co2, r1) - go (ForAllCo tv1 k_co co) - = let Pair _ k2 = coercionKind k_co - tv2 = setTyVarKind tv1 k2 - (Pair ty1 ty2, r) = go co - subst = zipTvSubst [tv1] [TyVarTy tv2 `mkCastTy` mkSymCo k_co] - ty2' = substTyAddInScope subst ty2 in - -- We need free vars of ty2 in scope to satisfy the invariant - -- from Note [The substitution invariant] - -- This is doing repeated substitutions and probably doesn't - -- need to, see #11735 - (mkInvForAllTy <$> Pair tv1 tv2 <*> Pair ty1 ty2', r) - go (FunCo r co1 co2) - = (mkFunTy <$> coercionKind co1 <*> coercionKind co2, r) + go (Refl r _) = r + go (TyConAppCo r _ _) = r + go (AppCo co1 _) = go co1 + go (ForAllCo _ _ co) = go co + go (FunCo r _ _) = r go (CoVarCo cv) = go_var cv go (HoleCo h) = go_var (coHoleCoVar h) - go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax) - go (UnivCo _ r ty1 ty2) = (Pair ty1 ty2, r) - go (SymCo co) = first swap $ go co - go (TransCo co1 co2) - = let (tys1, r) = go co1 in - (Pair (pFst tys1) (pSnd $ coercionKind co2), r) + go (AxiomInstCo ax _ _) = coAxiomRole ax + go (UnivCo _ r _ _) = r + go (SymCo co) = go co + go (TransCo co1 co2) = go co1 go (NthCo d co) | Just (tv1, _) <- splitForAllTy_maybe ty1 = ASSERT( d == 0 ) - let (tv2, _) = splitForAllTy ty2 in - (tyVarKind <$> Pair tv1 tv2, Nominal) + Nominal | otherwise = let (tc1, args1) = splitTyConApp ty1 (_tc2, args2) = splitTyConApp ty2 in ASSERT2( tc1 == _tc2, ppr d $$ ppr tc1 $$ ppr _tc2 ) - ((`getNth` d) <$> Pair args1 args2, nthRole r tc1 d) + (nthRole r tc1 d) where - (Pair ty1 ty2, r) = go co - go co@(LRCo {}) = (coercionKind co, Nominal) + (Pair ty1 ty2, r) = coercionKindRole co + go (LRCo {}) = Nominal go (InstCo co arg) = go_app co [arg] - go (CoherenceCo co1 co2) - = let (Pair t1 t2, r) = go co1 in - (Pair (t1 `mkCastTy` co2) t2, r) - go co@(KindCo {}) = (coercionKind co, Nominal) - go (SubCo co) = (coercionKind co, Representational) - go co@(AxiomRuleCo ax _) = (coercionKind co, coaxrRole ax) + go (CoherenceCo co1 _) = go co1 + go (KindCo {}) = Nominal + go (SubCo _) = Representational + go (AxiomRuleCo ax _) = coaxrRole ax ------------- - go_var cv = (coVarTypes cv, coVarRole cv) + go_var = coVarRole ------------- - go_app :: Coercion -> [Coercion] -> (Pair Type, Role) + go_app :: Coercion -> [Coercion] -> Role -- Collect up all the arguments and apply all at once -- See Note [Nested InstCos] go_app (InstCo co arg) args = go_app co (arg:args) - go_app co args - = let (pair, r) = go co in - (piResultTys <$> pair <*> (sequenceA $ map coercionKind args), r) - --- | Retrieve the role from a coercion. -coercionRole :: Coercion -> Role -coercionRole = snd . coercionKindRole - -- There's not a better way to do this, because NthCo needs the *kind* - -- and role of its argument. Luckily, laziness should generally avoid - -- the need for computing kinds in other cases. + go_app co args = go co {- Note [Nested InstCos] }}} Or, for increased clarity, just the new version of `coercionRole`: {{{ -- | Retrieve the role from a coercion. coercionRole :: Coercion -> Role coercionRole = go where go (Refl r _) = r go (TyConAppCo r _ _) = r go (AppCo co1 _) = go co1 go (ForAllCo _ _ co) = go co go (FunCo r _ _) = r go (CoVarCo cv) = go_var cv go (HoleCo h) = go_var (coHoleCoVar h) go (AxiomInstCo ax _ _) = coAxiomRole ax go (UnivCo _ r _ _) = r go (SymCo co) = go co go (TransCo co1 co2) = go co1 go (NthCo d co) | Just (tv1, _) <- splitForAllTy_maybe ty1 = ASSERT( d == 0 ) Nominal | otherwise = let (tc1, args1) = splitTyConApp ty1 (_tc2, args2) = splitTyConApp ty2 in ASSERT2( tc1 == _tc2, ppr d $$ ppr tc1 $$ ppr _tc2 ) (nthRole r tc1 d) where (Pair ty1 ty2, r) = coercionKindRole co go (LRCo {}) = Nominal go (InstCo co arg) = go_app co [arg] go (CoherenceCo co1 _) = go co1 go (KindCo {}) = Nominal go (SubCo _) = Representational go (AxiomRuleCo ax _) = coaxrRole ax ------------- go_var = coVarRole ------------- go_app :: Coercion -> [Coercion] -> Role -- Collect up all the arguments and apply all at once -- See Note [Nested InstCos] go_app (InstCo co arg) args = go_app co (arg:args) go_app co args = go co }}} I didn't make an effort at completely understanding what this is supposed to do, really; what I did, in a nutshell, was: - Rename `coercionKindRole` to `coercionRole` and change its type - Remove the first tuple element from each returned value - Fix recursive calls and local functions to not take the now-redundant first parameter and not return the first tuple element - Write a new `coercionKindRole` function that simply calls `coercionKind` and `coercionRole` and tuples up the results So it's entirely possible that I did something wrong somewhere. Anyway, I don't know if this would qualify as "remarkably short", but it is fairly simple.
Richard, did you have a concrete reason for that refactoring? Or just a
general worry? I believe the explanation is in the note at the bottom: {{{ Note [Nested InstCos] ~~~~~~~~~~~~~~~~~~~~~ In Trac #5631 we found that 70% of the entire compilation time was being spent in coercionKind! The reason was that we had (g @ ty1 @ ty2 .. @ ty100) -- The "@s" are InstCos where g :: forall a1 a2 .. a100. phi If we deal with the InstCos one at a time, we'll do this: 1. Find the kind of (g @ ty1 .. @ ty99) : forall a100. phi' 2. Substitute phi'[ ty100/a100 ], a single tyvar->type subst But this is a *quadratic* algorithm, and the blew up Trac #5631. So it's very important to do the substitution simultaneously; cf Type.piResultTys (which in fact we call here). }}} I'm not entirely sure whether this still applies though; I would expect the separate `coercionRole` and `coercionKinds` functions to perform better individually than the combined one, except when both are actually needed in concert. And even then, I'm skeptical; the recursive calls would drag along both data structures (kinds and role). Is it possible that this particular bit of code looked crucially different back when #5631 was ongoing? Or did I un-refactor in a way that doesn't replicate a crucial problem from the original code? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11735#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler