#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