[Git][ghc/ghc][master] Make type-equality on synonyms a bit faster
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Fri Jul 12 15:44:51 UTC 2024
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
280e4bf5 by Simon Peyton Jones at 2024-07-12T11:43:59-04:00
Make type-equality on synonyms a bit faster
This MR make equality fast for (S tys1 `eqType` S tys2),
where S is a non-forgetful type synonym.
It doesn't affect compile-time allocation much, but then comparison doesn't
allocate anyway. But it seems like a Good Thing anyway.
See Note [Comparing type synonyms] in GHC.Core.TyCo.Compare
and Note [Forgetful type synonyms] in GHC.Core.TyCon
Addresses #25009.
- - - - -
7 changed files:
- compiler/GHC/Core/Map/Type.hs
- compiler/GHC/Core/TyCo/Compare.hs
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Core/Map/Type.hs
=====================================
@@ -38,6 +38,7 @@ import GHC.Prelude
import GHC.Core.Type
import GHC.Core.Coercion
import GHC.Core.TyCo.Rep
+import GHC.Core.TyCon( isForgetfulSynTyCon )
import GHC.Core.TyCo.Compare( eqForAllVis )
import GHC.Data.TrieMap
@@ -228,10 +229,11 @@ eqDeBruijnType env_t1@(D env1 t1) env_t2@(D env2 t2) =
andEq TEQX e = hasCast e
andEq TEQ e = e
- -- See Note [Comparing nullary type synonyms] in GHC.Core.TyCo.Compare
- go (D _ (TyConApp tc1 [])) (D _ (TyConApp tc2 []))
- | tc1 == tc2
- = TEQ
+ -- See Note [Comparing type synonyms] in GHC.Core.TyCo.Compare
+ go (D env1 (TyConApp tc1 tys1)) (D env2 (TyConApp tc2 tys2))
+ | tc1 == tc2, not (isForgetfulSynTyCon tc1)
+ = gos env1 env2 tys1 tys2
+
go env_t@(D env t) env_t'@(D env' t')
| Just new_t <- coreView t = go (D env new_t) env_t'
| Just new_t' <- coreView t' = go env_t (D env' new_t')
=====================================
compiler/GHC/Core/TyCo/Compare.hs
=====================================
@@ -138,35 +138,52 @@ But the left is an AppTy while the right is a TyConApp. The solution is
to use splitAppTyNoView_maybe to break up the TyConApp into its pieces and
then continue. Easy to do, but also easy to forget to do.
-Note [Comparing nullary type synonyms]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Comparing type synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the task of testing equality between two 'Type's of the form
- TyConApp tc []
+ TyConApp tc tys1 = TyConApp tc tys2
-where @tc@ is a type synonym. A naive way to perform this comparison these
+where `tc` is a type synonym. A naive way to perform this comparison these
would first expand the synonym and then compare the resulting expansions.
-However, this is obviously wasteful and the RHS of @tc@ may be large; it is
-much better to rather compare the TyCons directly. Consequently, before
-expanding type synonyms in type comparisons we first look for a nullary
-TyConApp and simply compare the TyCons if we find one. Of course, if we find
-that the TyCons are *not* equal then we still need to perform the expansion as
-their RHSs may still be equal.
+However, this is obviously wasteful and the RHS of `tc` may be large. We'd
+prefer to compare `tys1 = tys2`. When is that sound? Precisely when the
+synonym is not /forgetful/; that is, all its type variables appear in its
+RHS -- see `GHC.Core.TyCon.isForgetfulSynTyCon`.
+
+Of course, if we find that the TyCons are *not* equal then we still need to
+perform the expansion as their RHSs may still be equal.
+
+This works fine for /equality/, but not for /comparison/. Consider
+ type S a b = (b, a)
+Now consider
+ S Int Bool `compare` S Char Char
+The ordering may depend on whether we expand the synonym or not, and we
+don't want the result to depend on that. So for comparison we stick to
+/nullary/ synonyms only, which is still useful.
We perform this optimisation in a number of places:
- * GHC.Core.Types.eqType
- * GHC.Core.Types.nonDetCmpType
- * GHC.Core.Unify.unify_ty
- * GHC.Tc.Solver.Equality.can_eq_nc'
- * TcUnify.uType
+ * GHC.Core.TyCo.Compare.eqType (works for non-nullary synonyms)
+ * GHC.Core.Map.TYpe.eqDeBruijnType (works for non-nullary synonyms)
+ * GHC.Core.Types.nonDetCmpType (nullary only)
This optimisation is especially helpful for the ubiquitous GHC.Types.Type,
since GHC prefers to use the type synonym over @TYPE 'LiftedRep@ applications
whenever possible. See Note [Using synonyms to compress types] in
GHC.Core.Type for details.
+Currently-missed opportunity (#25009):
+* In the case of forgetful synonyms, we could still compare the args, pairwise,
+ and then compare the RHS's with a suitably extended RnEnv2. That would avoid
+ comparing the same arg repeatedly. e.g.
+ type S a b = (a,a)
+ Compare S <big> y ~ S <big> y
+ If we expand, we end up compare <big> with itself twice.
+
+ But since forgetful synonyms are rare, we have not tried this.
+
Note [Type comparisons using object pointer comparisons]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Quite often we substitute the type from a definition site into
@@ -341,16 +358,26 @@ inline_generic_eq_type_x syn_flag mult_flag mb_env
= \ t1 t2 -> t1 `seq` t2 `seq`
let go = generic_eq_type_x syn_flag mult_flag mb_env
-- Abbreviation for recursive calls
+
+ gos [] [] = True
+ gos (t1:ts1) (t2:ts2) = go t1 t2 && gos ts1 ts2
+ gos _ _ = False
+
in case (t1,t2) of
_ | 1# <- reallyUnsafePtrEquality# t1 t2 -> True
-- See Note [Type comparisons using object pointer comparisons]
- (TyConApp tc1 [], TyConApp tc2 []) | tc1 == tc2 -> True
- -- See Note [Comparing nullary type synonyms]
+ (TyConApp tc1 tys1, TyConApp tc2 tys2)
+ | tc1 == tc2, not (isForgetfulSynTyCon tc1) -- See Note [Comparing type synonyms]
+ -> gos tys1 tys2
_ | ExpandSynonyms <- syn_flag, Just t1' <- coreView t1 -> go t1' t2
| ExpandSynonyms <- syn_flag, Just t2' <- coreView t2 -> go t1 t2'
+ (TyConApp tc1 ts1, TyConApp tc2 ts2)
+ | tc1 == tc2 -> gos ts1 ts2
+ | otherwise -> False
+
(TyVarTy tv1, TyVarTy tv2)
-> case mb_env of
Nothing -> tv1 == tv2
@@ -381,14 +408,6 @@ inline_generic_eq_type_x syn_flag mult_flag mb_env
| Just (s1, t1') <- tcSplitAppTyNoView_maybe t1
-> go s1 s2 && go t1' t2'
- (TyConApp tc1 ts1, TyConApp tc2 ts2)
- | tc1 == tc2 -> gos ts1 ts2
- | otherwise -> False
- where
- gos [] [] = True
- gos (t1:ts1) (t2:ts2) = go t1 t2 && gos ts1 ts2
- gos _ _ = False
-
(ForAllTy (Bndr tv1 vis1) body1, ForAllTy (Bndr tv2 vis2) body2)
-> case mb_env of
Nothing -> generic_eq_type_x syn_flag mult_flag
@@ -666,10 +685,11 @@ nonDetCmpTypeX env orig_t1 orig_t2 =
-- Returns both the resulting ordering relation between
-- the two types and whether either contains a cast.
go :: RnEnv2 -> Type -> Type -> TypeOrdering
- -- See Note [Comparing nullary type synonyms]
+
go _ (TyConApp tc1 []) (TyConApp tc2 [])
| tc1 == tc2
- = TEQ
+ = TEQ -- See Note [Comparing type synonyms]
+
go env t1 t2
| Just t1' <- coreView t1 = go env t1' t2
| Just t2' <- coreView t2 = go env t1 t2'
@@ -758,8 +778,10 @@ mayLookIdentical orig_ty1 orig_ty2
orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
go :: RnEnv2 -> Type -> Type -> Bool
- -- See Note [Comparing nullary type synonyms]
- go _ (TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 = True
+
+ go env (TyConApp tc1 ts1) (TyConApp tc2 ts2)
+ | tc1 == tc2, not (isForgetfulSynTyCon tc1) -- See Note [Comparing type synonyms]
+ = gos env (tyConBinders tc1) ts1 ts2
go env t1 t2 | Just t1' <- coreView t1 = go env t1' t2
go env t1 t2 | Just t2' <- coreView t2 = go env t1 t2'
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -841,7 +841,8 @@ data TyConDetails =
-- are fine), again after expanding any
-- nested synonyms
- synIsForgetful :: Bool, -- True <= at least one argument is not mentioned
+ synIsForgetful :: Bool, -- See Note [Forgetful type synonyms]
+ -- True <= at least one argument is not mentioned
-- in the RHS (or is mentioned only under
-- forgetful synonyms)
-- Test is conservative, so True does not guarantee
@@ -2121,11 +2122,43 @@ isFamFreeTyCon (TyCon { tyConDetails = details })
-- True. Thus, False means that all bound variables appear on the RHS;
-- True may not mean anything, as the test to set this flag is
-- conservative.
+--
+-- See Note [Forgetful type synonyms]
isForgetfulSynTyCon :: TyCon -> Bool
isForgetfulSynTyCon (TyCon { tyConDetails = details })
| SynonymTyCon { synIsForgetful = forget } <- details = forget
| otherwise = False
+{- Note [Forgetful type synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A type synonyms is /forgetful/ if its RHS fails to mention one (or more) of its bound variables.
+
+Forgetfulness is conservative:
+ * A non-forgetful synonym /guarantees/ to mention all its bound variables in its RHS.
+ * It is always safe to classify a synonym as forgetful.
+
+Examples:
+ type R = Int -- Not forgetful
+ type S a = Int -- Forgetful
+ type T1 a = Int -> S a -- Forgetful
+ type T2 a = a -> S a -- Not forgetful
+ type T3 a = Int -> F a -- Not forgetful
+ where type family F a
+
+* R shows that nullary synonyms are not forgetful.
+
+* T2 shows that forgetfulness needs to account for uses of forgetful
+ synonyms. `a` appears on the RHS, but only under a forgetful S
+
+* T3 shows that non-forgetfulness is not the same as injectivity. T3 mentions its
+ bound variable on its RHS, but under a type family. So it is entirely possible
+ that T3 Int ~ T3 Bool
+
+* Since type synonyms are non-recursive, we don't need a fixpoint analysis to
+ determine forgetfulness. It's rather easy -- see `GHC.Core.Type.buildSynTyCon`,
+ which is a bit over-conservative for over-saturated synonyms.
+-}
+
-- As for newtypes, it is in some contexts important to distinguish between
-- closed synonyms and synonym families, as synonym families have no unique
-- right hand side to which a synonym family application can expand.
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -2327,7 +2327,7 @@ buildSynTyCon name binders res_kind roles rhs
is_forgetful = not (all ((`elemVarSet` rhs_tyvars) . binderVar) binders) ||
uniqSetAny isForgetfulSynTyCon rhs_tycons
-- NB: is_forgetful is allowed to be conservative, returning True more often
- -- than it should. See comments on GHC.Core.TyCon.isForgetfulSynTyCon
+ -- than it should. See Note [Forgetful type synonyms] in GHC.Core.TyCon
rhs_tycons = tyConsOfType rhs
rhs_tyvars = tyCoVarsOfType rhs
@@ -3275,8 +3275,9 @@ efficient. Specifically, we strive to
Goal (b) is particularly useful as it makes traversals (e.g. free variable
traversal, substitution, and comparison) more efficient.
Comparison in particular takes special advantage of nullary type synonym
-applications (e.g. things like @TyConApp typeTyCon []@), Note [Comparing
-nullary type synonyms] in "GHC.Core.Type".
+applications (e.g. things like @TyConApp typeTyCon []@). See
+* Note [Comparing type synonyms] in "GHC.Core.TyCo.Compare"
+* Note [Unifying type synonyms] in "GHC.Core.Unify"
To accomplish these we use a number of tricks, implemented by mkTyConApp.
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -1089,6 +1089,47 @@ of arity n:
If we couldn't decompose in the previous step, we return SurelyApart.
Afterwards, the rest of the code doesn't have to worry about type families.
+
+Note [Unifying type synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the task of unifying two 'Type's of the form
+
+ TyConApp tc [] ~ TyConApp tc []
+
+where `tc` is a type synonym. A naive way to perform this comparison these
+would first expand the synonym and then compare the resulting expansions.
+
+However, this is obviously wasteful and the RHS of `tc` may be large; it is
+much better to rather compare the TyCons directly. Consequently, before
+expanding type synonyms in type comparisons we first look for a nullary
+TyConApp and simply compare the TyCons if we find one.
+
+Of course, if we find that the TyCons are *not* equal then we still need to
+perform the expansion as their RHSs may still be unifiable. E.g
+ type T = S (a->a)
+ type S a = [a]
+and consider
+ T Int ~ S (Int -> Int)
+
+We can't decompose non-nullary synonyms. E.g.
+ type R a = F a -- Where F is a type family
+and consider
+ R (a->a) ~ R Int
+We can't conclude that (a->) ~ Int. (There is a currently-missed opportunity
+here; if we knew that R was /injective/, perhaps we could decompose.)
+
+We perform the nullary-type-synonym optimisation in a number of places:
+
+ * GHC.Core.Unify.unify_ty
+ * GHC.Tc.Solver.Equality.can_eq_nc'
+ * GHC.Tc.Utils.Unify.uType
+
+This optimisation is especially helpful for the ubiquitous GHC.Types.Type,
+since GHC prefers to use the type synonym over @TYPE 'LiftedRep@ applications
+whenever possible. See Note [Using synonyms to compress types] in
+GHC.Core.Type for details.
+
+c.f. Note [Comparing type synonyms] in GHC.Core.TyCo.Compare
-}
-------------- unify_ty: the main workhorse -----------
@@ -1107,7 +1148,7 @@ unify_ty :: UMEnv
-- Respects newtypes, PredTypes
-- See Note [Computing equality on types] in GHC.Core.Type
unify_ty _env (TyConApp tc1 []) (TyConApp tc2 []) _kco
- -- See Note [Comparing nullary type synonyms] in GHC.Core.TyCo.Compare
+ -- See Note [Unifying type synonyms]
| tc1 == tc2
= return ()
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -305,7 +305,7 @@ can_eq_nc
-> Type -> Type -- RHS, after and before type-synonym expansion, resp
-> TcS (StopOrContinue (Either IrredCt EqCt))
--- See Note [Comparing nullary type synonyms] in GHC.Core.TyCo.Compare
+-- See Note [Unifying type synonyms] in GHC.Core.Unify
can_eq_nc _flat _rdr_env _envs ev eq_rel ty1@(TyConApp tc1 []) _ps_ty1 (TyConApp tc2 []) _ps_ty2
| tc1 == tc2
= canEqReflexive ev eq_rel ty1
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -2187,11 +2187,12 @@ uType env@(UE { u_role = role }) orig_ty1 orig_ty2
; uType env orig_ty1 ty2 }
Nothing -> uUnfilledVar env IsSwapped tv2 ty1 }
- -- See Note [Expanding synonyms during unification]
+ -- See Note [Unifying type synonyms] in GHC.Core.Unify
go ty1@(TyConApp tc1 []) (TyConApp tc2 [])
| tc1 == tc2
= return $ mkReflCo role ty1
+ -- Now expand synonyms
-- See Note [Expanding synonyms during unification]
--
-- Also NB that we recurse to 'go' so that we don't push a
@@ -2349,7 +2350,7 @@ We expand synonyms during unification, but:
* The problem case immediately above can happen only with arguments
to the tycon. So we check for nullary tycons *before* expanding.
This is particularly helpful when checking (* ~ *), because * is
- now a type synonym.
+ now a type synonym. See Note [Unifying type synonyms] in GHC.Core.Unify.
Note [Deferred unification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/280e4bf5ca62ec51eaeedd04b0db78b085257ab8
--
This project does not include diff previews in email notifications.
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/280e4bf5ca62ec51eaeedd04b0db78b085257ab8
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/20240712/0e461528/attachment-0001.html>
More information about the ghc-commits
mailing list