[Git][ghc/ghc][wip/T22194-flags] Performance tweaks
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Sat Mar 25 23:00:56 UTC 2023
Simon Peyton Jones pushed to branch wip/T22194-flags at Glasgow Haskell Compiler / GHC
Commits:
b1c87de8 by Simon Peyton Jones at 2023-03-25T23:02:05+00:00
Performance tweaks
- - - - -
6 changed files:
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Type.hs-boot
- compiler/GHC/Tc/Solver/Rewrite.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/indexed-types/should_compile/T3208b.stderr
Changes:
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -23,7 +23,7 @@ module GHC.Core.TyCo.FVs
almostDevoidCoVarOfCo,
-- Injective free vars
- injectiveVarsOfType, injectiveVarsOfTypes,
+ injectiveVarsOfType, injectiveVarsOfTypes, isInjectiveInType,
invisibleVarsOfType, invisibleVarsOfTypes,
-- Any and No Free vars
@@ -53,7 +53,7 @@ module GHC.Core.TyCo.FVs
import GHC.Prelude
-import {-# SOURCE #-} GHC.Core.Type( partitionInvisibleTypes, coreView )
+import {-# SOURCE #-} GHC.Core.Type( partitionInvisibleTypes, coreView, rewriterView )
import {-# SOURCE #-} GHC.Core.Coercion( coercionLKind )
import GHC.Builtin.Types.Prim( funTyFlagTyCon )
@@ -806,6 +806,28 @@ visVarsOfTypes = foldMap visVarsOfType
* *
********************************************************************* -}
+isInjectiveInType :: TyVar -> Type -> Bool
+-- True <=> tv /definitely/ appears injectively in ty
+-- A bit more efficient that (tv `elemVarSet` injectiveTyVarsOfType ty)
+-- Ignore occurence in coercions, and even in injective positions of
+-- type families.
+isInjectiveInType tv ty
+ = go ty
+ where
+ go ty | Just ty' <- rewriterView ty = go ty'
+ go (TyVarTy tv') = tv' == tv
+ go (AppTy f a) = go f || go a
+ go (FunTy _ w ty1 ty2) = go w || go ty1 || go ty2
+ go (TyConApp tc tys) = go_tc tc tys
+ go (ForAllTy (Bndr tv' _) ty) = go (tyVarKind tv')
+ || (tv /= tv' && go ty)
+ go LitTy{} = False
+ go (CastTy ty _) = go ty
+ go CoercionTy{} = False
+
+ go_tc tc tys | isTypeFamilyTyCon tc = False
+ | otherwise = any go tys
+
-- | Returns the free variables of a 'Type' that are in injective positions.
-- Specifically, it finds the free variables while:
--
@@ -836,15 +858,15 @@ injectiveVarsOfType :: Bool -- ^ Should we look under injective type families?
-> Type -> FV
injectiveVarsOfType look_under_tfs = go
where
- go ty | Just ty' <- coreView ty = go ty'
- go (TyVarTy v) = unitFV v `unionFV` go (tyVarKind v)
- go (AppTy f a) = go f `unionFV` go a
- go (FunTy _ w ty1 ty2) = go w `unionFV` go ty1 `unionFV` go ty2
- go (TyConApp tc tys) = go_tc tc tys
- go (ForAllTy (Bndr tv _) ty) = go (tyVarKind tv) `unionFV` delFV tv (go ty)
- go LitTy{} = emptyFV
- go (CastTy ty _) = go ty
- go CoercionTy{} = emptyFV
+ go ty | Just ty' <- rewriterView ty = go ty'
+ go (TyVarTy v) = unitFV v `unionFV` go (tyVarKind v)
+ go (AppTy f a) = go f `unionFV` go a
+ go (FunTy _ w ty1 ty2) = go w `unionFV` go ty1 `unionFV` go ty2
+ go (TyConApp tc tys) = go_tc tc tys
+ go (ForAllTy (Bndr tv _) ty) = go (tyVarKind tv) `unionFV` delFV tv (go ty)
+ go LitTy{} = emptyFV
+ go (CastTy ty _) = go ty
+ go CoercionTy{} = emptyFV
go_tc tc tys
| isTypeFamilyTyCon tc
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -184,7 +184,7 @@ module GHC.Core.Type (
seqType, seqTypes,
-- * Other views onto Types
- coreView, coreFullView,
+ coreView, coreFullView, rewriterView,
tyConsOfType,
@@ -361,6 +361,19 @@ import GHC.Data.Maybe ( orElse, isJust )
************************************************************************
-}
+rewriterView :: Type -> Maybe Type
+-- Unwrap a type synonym only when either:
+-- The type synonym is forgetful, or
+-- the type synonym mentions a type family in its expansion
+-- See Note [Rewriting synonyms]
+{-# INLINE rewriterView #-}
+rewriterView (TyConApp tc tys)
+ | isTypeSynonymTyCon tc
+ , isForgetfulSynTyCon tc || not (isFamFreeTyCon tc)
+ = expandSynTyConApp_maybe tc tys
+rewriterView _other
+ = Nothing
+
coreView :: Type -> Maybe Type
-- ^ This function strips off the /top layer only/ of a type synonym
-- application (if any) its underlying representation type.
@@ -402,7 +415,7 @@ expandSynTyConApp_maybe :: TyCon -> [Type] -> Maybe Type
expandSynTyConApp_maybe tc arg_tys
| Just (tvs, rhs) <- synTyConDefn_maybe tc
, arg_tys `saturates` tyConArity tc
- = Just (expand_syn tvs rhs arg_tys)
+ = Just $! (expand_syn tvs rhs arg_tys)
| otherwise
= Nothing
=====================================
compiler/GHC/Core/Type.hs-boot
=====================================
@@ -21,7 +21,8 @@ piResultTy :: HasDebugCallStack => Type -> Type -> Type
typeKind :: HasDebugCallStack => Type -> Type
typeTypeOrConstraint :: HasDebugCallStack => Type -> TypeOrConstraint
-coreView :: Type -> Maybe Type
+coreView :: Type -> Maybe Type
+rewriterView :: Type -> Maybe Type
isRuntimeRepTy :: Type -> Bool
isLevityTy :: Type -> Bool
isMultiplicityTy :: Type -> Bool
=====================================
compiler/GHC/Tc/Solver/Rewrite.hs
=====================================
@@ -665,16 +665,6 @@ rewrite_vector ki roles tys
{-# INLINE rewrite_vector #-}
--- Unwrap a type synonym only when either:
--- The type synonym is forgetful, or
--- the type synonym mentions a type family in its expansion
--- See Note [Rewriting synonyms]
-rewriterView :: TcType -> Maybe TcType
-rewriterView ty@(TyConApp tc _)
- | isForgetfulSynTyCon tc || (isTypeSynonymTyCon tc && not (isFamFreeTyCon tc))
- = coreView ty
-rewriterView _other = Nothing
-
{- Note [Do not rewrite newtypes]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We flirted with unwrapping newtypes in the rewriter -- see GHC.Tc.Solver.Canonical
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -37,7 +37,7 @@ module GHC.Tc.Utils.Unify (
checkTyEqRhs, recurseIntoTyConApp,
PuResult(..), failCheckWith, okCheckRefl, mapCheck,
TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker,
- famAppArgFlags, occursCheckTv, simpleUnifyCheck, checkPromoteFreeVars,
+ famAppArgFlags, simpleUnifyCheck, checkPromoteFreeVars,
) where
import GHC.Prelude
@@ -58,8 +58,8 @@ import GHC.Types.Name( Name, isSystemName )
import GHC.Core.Type
import GHC.Core.TyCo.Rep
-import GHC.Core.TyCo.FVs( injectiveVarsOfType )
-import GHC.Core.TyCo.Ppr( debugPprType, pprTyVar )
+import GHC.Core.TyCo.FVs( isInjectiveInType )
+import GHC.Core.TyCo.Ppr( debugPprType {- pprTyVar -} )
import GHC.Core.TyCon
import GHC.Core.Coercion
import GHC.Core.Multiplicity
@@ -74,7 +74,6 @@ import GHC.Types.Var.Env
import GHC.Types.Basic
import GHC.Types.Unique.Set (nonDetEltsUniqSet)
-import GHC.Utils.FV( fvVarSet )
import GHC.Utils.Error
import GHC.Utils.Misc
import GHC.Utils.Outputable as Outputable
@@ -86,6 +85,7 @@ import GHC.Data.Bag
import GHC.Data.FastString( fsLit )
import Control.Monad
+import Data.Monoid as DM ( Any(..) )
import qualified Data.Semigroup as S ( (<>) )
{- *********************************************************************
@@ -1062,7 +1062,7 @@ definitely_poly ty
| (tvs, theta, tau) <- tcSplitSigmaTy ty
, (tv:_) <- tvs -- At least one tyvar
, null theta -- No constraints; see (DP1)
- , tv `elemVarSet` fvVarSet (injectiveVarsOfType True tau)
+ , tv `isInjectiveInType` tau
-- The tyvar actually occurs (DP2),
-- and occurs in an injective position (DP3).
= True
@@ -2075,30 +2075,27 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
-- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
-- Here we don't know about given equalities here; so we treat
-- /any/ level outside this one as untouchable. Hence cur_lvl.
- ; if not (touchabilityAndShapeTest cur_lvl tv1 ty2)
+ ; if not (touchabilityAndShapeTest cur_lvl tv1 ty2
+ && simpleUnifyCheck False tv1 ty2)
then not_ok_so_defer
else
- do { check_result <- uTypeCheckTouchableTyVarEq tv1 ty2
- ; case check_result of {
- PuFail {} -> not_ok_so_defer ;
- PuOK ty2' _ ->
- do { co_k <- uType KindLevel kind_origin (typeKind ty2') (tyVarKind tv1)
+ do { co_k <- uType KindLevel kind_origin (typeKind ty2) (tyVarKind tv1)
; traceTc "uUnfilledVar2 ok" $
vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
- , ppr ty2 <+> dcolon <+> ppr (typeKind ty2')
+ , ppr ty2 <+> dcolon <+> ppr (typeKind ty2)
, ppr (isReflCo co_k), ppr co_k ]
; if isReflCo co_k
-- Only proceed if the kinds match
-- NB: tv1 should still be unfilled, despite the kind unification
-- because tv1 is not free in ty2' (or, hence, in its kind)
- then do { writeMetaTyVar tv1 ty2'
- ; return (mkNomReflCo ty2') }
+ then do { writeMetaTyVar tv1 ty2
+ ; return (mkNomReflCo ty2) }
else defer -- This cannot be solved now. See GHC.Tc.Solver.Canonical
-- Note [Equalities with incompatible kinds] for how
-- this will be dealt with in the solver
- }}}}
+ }}
where
ty1 = mkTyVarTy tv1
kind_origin = KindEqOrigin ty1 ty2 origin (Just t_or_k)
@@ -2526,6 +2523,7 @@ matchExpectedFunKind hs_ty n k = go n k
* *
********************************************************************* -}
+{-
uTypeCheckTouchableTyVarEq :: TcTyVar -> TcType -> TcM (PuResult () TcType)
-- The check may expand type synonyms to avoid an occurs check,
-- so we must use the return type
@@ -2555,10 +2553,10 @@ uTypeCheckTouchableTyVarEq lhs_tv rhs
| otherwise
= pprPanic "uTypeCheckTouchableTyVarEq" (ppr lhs_tv)
-- TEFA_Fail: See Note [Prevent unification with type families]
-
+-}
simpleUnifyCheck :: Bool -> TcTyVar -> TcType -> Bool
--- A fast check that confirms that unification is OK
+-- A fast check: True <=> unification is OK
-- If it says 'False' then unification might still be OK, but
-- it'll take more work to do -- use the full checkTypeEq
--
@@ -2567,21 +2565,25 @@ simpleUnifyCheck :: Bool -> TcTyVar -> TcType -> Bool
-- * Rejects a non-concrete type if lhs_tv is concrete
-- * Rejects type families unless fam_ok=True
-- * Does a level-check for type variables
+--
+-- This function is pretty heavily used, so it's optimised not to allocate
simpleUnifyCheck fam_ok lhs_tv rhs
= go rhs
where
+ !(occ_in_ty, occ_in_co) = mkOccFolders lhs_tv
+
lhs_tv_lvl = tcTyVarLevel lhs_tv
lhs_tv_is_concrete = isConcreteTyVar lhs_tv
forall_ok = case tcTyVarDetails lhs_tv of
- MetaTv { mtv_info = RuntimeUnkTv } -> True
- _ -> False
+ MetaTv { mtv_info = RuntimeUnkTv } -> True
+ _ -> False
go (TyVarTy tv)
- | lhs_tv == tv = False
- | tcTyVarLevel tv > lhs_tv_lvl = False
- | lhs_tv_is_concrete, not (isConcreteTyVar tv) = False
- | lhs_tv `elemVarSet` tyCoVarsOfType (tyVarKind tv) = False
- | otherwise = True
+ | lhs_tv == tv = False
+ | tcTyVarLevel tv > lhs_tv_lvl = False
+ | lhs_tv_is_concrete, not (isConcreteTyVar tv) = False
+ | occ_in_ty $! (tyVarKind tv) = False
+ | otherwise = True
go (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
| isInvisibleFunArg af, not forall_ok = False
@@ -2594,20 +2596,33 @@ simpleUnifyCheck fam_ok lhs_tv rhs
| otherwise = all go tys
go (AppTy t1 t2) = go t1 && go t2
- go (ForAllTy _ ty)
- | forall_ok = go ty -- To be really kosher we should worry about when
- -- the bound var = lhs_tv. But this only matters in the
- -- GHCi debugger, and is unlikely to matter, so for now
- -- I have just ignored the problem.
+ go (ForAllTy (Bndr tv _) ty)
+ | forall_ok = go (tyVarKind tv) && (tv == lhs_tv || go ty)
| otherwise = False
- go (CastTy ty co) = go_co co && go ty
- go (CoercionTy co) = go_co co
+ go (CastTy ty co) = not (occ_in_co co) && go ty
+ go (CoercionTy co) = not (occ_in_co co)
go (LitTy {}) = True
- go_co co = not (lhs_tv `elemVarSet` tyCoVarsOfCo co)
- && not (hasCoercionHoleCo co)
+mkOccFolders :: TcTyVar -> (TcType -> Bool, TcCoercion -> Bool)
+-- These functions return True
+-- * if lhs_tv occurs (incl deeply, in the kind of variable)
+-- * if there is a coercion hole
+-- No expansion of type synonyms
+mkOccFolders lhs_tv = (getAny . check_ty, getAny . check_co)
+ where
+ !(check_ty, _, check_co, _) = foldTyCo occ_folder emptyVarSet
+ occ_folder = TyCoFolder { tcf_view = noView -- Don't expand synonyms
+ , tcf_tyvar = do_tcv, tcf_covar = do_tcv
+ , tcf_hole = do_hole
+ , tcf_tycobinder = do_bndr }
+
+ do_tcv is v = Any (not (v `elemVarSet` is) && v == lhs_tv)
+ `mappend` check_ty (varType v)
+
+ do_bndr is tcv _faf = extendVarSet is tcv
+ do_hole _is _hole = DM.Any True -- Reject coercion holes
{- *********************************************************************
* *
@@ -2767,9 +2782,11 @@ mapCheck f xs
-- unzipRedns :: [Reduction] -> Reductions
occursCheckTv :: TcTyVar -> TcTyVar -> Bool
+-- True <=> occurs-check fires
occursCheckTv lhs_tv occ_tv
- = lhs_tv == occ_tv
- || lhs_tv `elemVarSet` tyCoVarsOfType (tyVarKind occ_tv)
+ = lhs_tv == occ_tv || check_kind (tyVarKind occ_tv)
+ where
+ (check_kind, _) = mkOccFolders lhs_tv
-----------------------------
data TyEqFlags a
@@ -2988,12 +3005,11 @@ checkTyConApp flags@(TEF { tef_unifying = unifying, tef_foralls = foralls_ok })
; traceTc "Over-sat" (ppr tc <+> ppr tys $$ ppr arity $$ pprPur fun_res $$ pprPur extra_res)
; return (mkAppRedns <$> fun_res <*> extra_res) }
- | not (isFamFreeTyCon tc) || isForgetfulSynTyCon tc
+ | Just ty' <- rewriterView tc_app
-- e.g. S a where type S a = F [a]
-- or type S a = Int
-- See Note [Forgetful synonyms in checkTyConApp]
- , Just ty' <- coreView tc_app -- Only synonyms and type families reply
- = checkTyEqRhs flags ty' -- False to isFamFreeTyCon
+ = checkTyEqRhs flags ty'
| not (isTauTyCon tc || foralls_ok)
= failCheckWith impredicativeProblem
@@ -3184,6 +3200,7 @@ touchabilityAndShapeTest :: TcLevel -> TcTyVar -> TcType -> Bool
-- This is the key test for untouchability:
-- See Note [Unification preconditions] in GHC.Tc.Utils.Unify
-- and Note [Solve by unification] in GHC.Tc.Solver.Interact
+-- True <=> touchability and shape are OK
touchabilityAndShapeTest given_eq_lvl tv rhs
| MetaTv { mtv_info = info, mtv_tclvl = tv_lvl } <- tcTyVarDetails tv
, checkTopShape info rhs
=====================================
testsuite/tests/indexed-types/should_compile/T3208b.stderr
=====================================
@@ -1,6 +1,6 @@
T3208b.hs:15:10: error: [GHC-05617]
- • Could not deduce ‘OTerm o0 ~ STerm a’ arising from a use of ‘fce’
+ • Could not deduce ‘STerm o0 ~ OTerm a’ arising from a use of ‘fce’
from the context: (OTerm a ~ STerm a, OBJECT a, SUBST a)
bound by the type signature for:
fce' :: forall a c.
@@ -15,7 +15,7 @@ T3208b.hs:15:10: error: [GHC-05617]
fce' :: a -> c (bound at T3208b.hs:15:1)
T3208b.hs:15:15: error: [GHC-05617]
- • Could not deduce ‘STerm o0 ~ STerm a’
+ • Could not deduce ‘OTerm o0 ~ OTerm a’
arising from a use of ‘apply’
from the context: (OTerm a ~ STerm a, OBJECT a, SUBST a)
bound by the type signature for:
@@ -23,7 +23,7 @@ T3208b.hs:15:15: error: [GHC-05617]
(OTerm a ~ STerm a, OBJECT a, SUBST a) =>
a -> c
at T3208b.hs:14:1-56
- NB: ‘STerm’ is a non-injective type family
+ NB: ‘OTerm’ is a non-injective type family
The type variable ‘o0’ is ambiguous
• In the first argument of ‘fce’, namely ‘(apply f)’
In the expression: fce (apply f)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b1c87de83cfbff51557e7d544f78cfe71f7e812f
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b1c87de83cfbff51557e7d544f78cfe71f7e812f
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/20230325/bf8d2762/attachment-0001.html>
More information about the ghc-commits
mailing list