[GHC] #11735: Optimize coercionKind

[GHC]

#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:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Let's just do this.  Pretty easy. Roughly like the `InstCo` case.  Here is
 an untested patch for `coercionKind`.
 {{{
 diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
 index 3f83b09..daebf35 100644
 --- a/compiler/types/Coercion.hs
 +++ b/compiler/types/Coercion.hs
 @@ -1707,17 +1707,13 @@ coercionKind co = go co
      go (Refl _ ty)          = Pair ty ty
      go (TyConAppCo _ tc cos)= mkTyConApp tc <$> (sequenceA $ map go cos)
      go (AppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2
 -    go (ForAllCo tv1 k_co co)
 -      = let Pair _ k2          = go k_co
 -            tv2                = setTyVarKind tv1 k2
 -            Pair ty1 ty2       = go co
 -            subst = zipTvSubst [tv1] [TyVarTy tv2 `mk_cast_ty` 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'
 +
 +    go co@(ForAllCo tv1 k_co co1)
 +       | isReflCo k_co            = mkInvForAllTy tv1 <$> go co1
 +       | otherwise                = go_forall empty_subst co
 +       where
 +         empty_subst = mkEmptyTCvSubst (mkInScopeSet $ tyCoVarsOfCo co)
 +
      go (FunCo _ co1 co2)    = mkFunTy <$> go co1 <*> go co2
      go (CoVarCo cv)         = coVarTypes cv
      go (HoleCo h)           = coVarTypes (coHoleCoVar h)
 @@ -1769,10 +1765,16 @@ coercionKind co = go co
      go_app (InstCo co arg) args = go_app co (arg:args)
      go_app co              args = piResultTys <$> go co <*> (sequenceA $
 map go args)

 -    -- The real mkCastTy is too slow, and we can easily have nested
 ForAllCos.
 -    mk_cast_ty :: Type -> Coercion -> Type
 -    mk_cast_ty ty (Refl {}) = ty
 -    mk_cast_ty ty co        = CastTy ty co
 +    go_forall subst (ForAllCo tv1 k_co co)
 +      = mkInvForAllTy <$> Pair tv1 tv2 <*> go_forall subst' co
 +      where
 +        Pair _ k2 = go k_co
 +        tv2       = setTyVarKind tv1 (substTy subst k2)
 +        subst' | isReflCo k_co = extendTCvInScope subst tv1
 +               | otherwise     = extendTvSubst (extendTCvInScope subst
 tv2) tv1 $
 +                                 TyVarTy tv2 `mkCastTy` mkSymCo k_co
 +    go_forall subst other_co
 +      = substTy subst `pLiftSnd` go other_co

  -- | Apply 'coercionKind' to multiple 'Coercion's
  coercionKinds :: [Coercion] -> Pair [Type]
 }}}
 '''Richard: can you check'''.

 We should do the same thing to `coercionKindRole`.  (Tiresomely.)

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11735#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler