[GHC] #11735: Optimize coercionKind
GHC
ghc-devs at haskell.org
Wed Jan 24 19:21:37 UTC 2018
#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]:
> > I'm dubious of the coercionRole refactor, as it undoes a refactoring I
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
More information about the ghc-tickets
mailing list