[Git][ghc/ghc][wip/revert-type-faster] 2 commits: Revert "Revert "Make type-equality on synonyms a bit faster""
Matthew Pickering (@mpickering)
gitlab at gitlab.haskell.org
Fri Jul 19 15:09:56 UTC 2024
Matthew Pickering pushed to branch wip/revert-type-faster at Glasgow Haskell Compiler / GHC
Commits:
87cedc4e by Matthew Pickering at 2024-07-19T15:41:12+01:00
Revert "Revert "Make type-equality on synonyms a bit faster""
This reverts commit 7c5b9cddf4ab3e85526e7d6a963fc049b1e14dc1.
- - - - -
59381637 by Matthew Pickering at 2024-07-19T16:08:37+01:00
Add test for T25094
This test is minimised from hashtables library, before the revert it
fails with:
```
T25094.hs:84:18: warning:
Type of case alternatives not the same as the annotation on case:
Actual type: ST s_a12L (Bucket s_a12L Any Any)
Annotation on case: ST s_a12L (Bucket s_a12L k_a12M v_a12N)
```
See #25094
- - - - -
9 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
- + testsuite/tests/deSugar/should_compile/T25094.hs
- testsuite/tests/deSugar/should_compile/all.T
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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
testsuite/tests/deSugar/should_compile/T25094.hs
=====================================
@@ -0,0 +1,99 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE MagicHash #-}
+
+module T29054 where
+
+
+------------------------------------------------------------------------------
+import Control.Monad.ST (ST)
+import Data.Maybe (fromMaybe)
+import Data.STRef
+import GHC.Exts (Any, reallyUnsafePtrEquality#, (==#), isTrue#)
+import Unsafe.Coerce
+import Control.Monad.ST
+
+data MutableArray s a = MutableArray
+
+newArray :: Int -> a -> ST s (MutableArray s a)
+newArray = undefined
+
+readArray :: MutableArray s a -> Int -> ST s a
+readArray = undefined
+
+writeArray :: MutableArray s a -> Int -> a -> ST s ()
+writeArray = undefined
+
+
+type Key a = Any
+
+------------------------------------------------------------------------------
+-- Type signatures
+emptyRecord :: Key a
+deletedRecord :: Key a
+keyIsEmpty :: Key a -> Bool
+toKey :: a -> Key a
+fromKey :: Key a -> a
+
+
+data TombStone = EmptyElement
+ | DeletedElement
+
+{-# NOINLINE emptyRecord #-}
+emptyRecord = unsafeCoerce EmptyElement
+
+{-# NOINLINE deletedRecord #-}
+deletedRecord = unsafeCoerce DeletedElement
+
+{-# INLINE keyIsEmpty #-}
+keyIsEmpty a = isTrue# (x# ==# 1#)
+ where
+ !x# = reallyUnsafePtrEquality# a emptyRecord
+
+{-# INLINE toKey #-}
+toKey = unsafeCoerce
+
+{-# INLINE fromKey #-}
+fromKey = unsafeCoerce
+
+
+type Bucket s k v = Key (Bucket_ s k v)
+
+------------------------------------------------------------------------------
+data Bucket_ s k v = Bucket { _bucketSize :: {-# UNPACK #-} !Int
+ , _highwater :: {-# UNPACK #-} !(STRef s Int)
+ , _keys :: {-# UNPACK #-} !(MutableArray s k)
+ , _values :: {-# UNPACK #-} !(MutableArray s v)
+ }
+
+
+------------------------------------------------------------------------------
+emptyWithSize :: Int -> ST s (Bucket s k v)
+emptyWithSize !sz = undefined
+
+------------------------------------------------------------------------------
+expandArray :: a -- ^ default value
+ -> Int -- ^ new size
+ -> Int -- ^ number of elements to copy
+ -> MutableArray s a -- ^ old array
+ -> ST s (MutableArray s a)
+expandArray def !sz !hw !arr = undefined
+
+------------------------------------------------------------------------------
+growBucketTo :: Int -> Bucket s k v -> ST s (Bucket s k v)
+growBucketTo !sz bk | keyIsEmpty bk = emptyWithSize sz
+ | otherwise = do
+ if osz >= sz
+ then return bk
+ else do
+ hw <- readSTRef hwRef
+ k' <- expandArray undefined sz hw keys
+ v' <- expandArray undefined sz hw values
+ return $ toKey $ Bucket sz hwRef k' v'
+
+ where
+ bucket = fromKey bk
+ osz = _bucketSize bucket
+ hwRef = _highwater bucket
+ keys = _keys bucket
+ values = _values bucket
+
=====================================
testsuite/tests/deSugar/should_compile/all.T
=====================================
@@ -115,3 +115,4 @@ test('T19883', normal, compile, [''])
test('T22719', normal, compile, ['-ddump-simpl -dsuppress-uniques -dno-typeable-binds'])
test('T23550', normal, compile, [''])
test('T24489', normal, compile, ['-O'])
+test('T25094', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/7c5b9cddf4ab3e85526e7d6a963fc049b1e14dc1...59381637958771f74e5139a67e7b6c869fc7fcd8
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/7c5b9cddf4ab3e85526e7d6a963fc049b1e14dc1...59381637958771f74e5139a67e7b6c869fc7fcd8
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/20240719/d1db6bd3/attachment-0001.html>
More information about the ghc-commits
mailing list