summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2020-06-19 15:56:24 +0100
committerSimon Peyton Jones <simonpj@microsoft.com>2020-06-26 09:46:21 +0100
commite5cdb1c8035f2447017867f96873aa71e6835906 (patch)
treeb65db16256741f570fbb2509694be11abfbcea7e
parenta3d69dc6c2134afe239caf4f881ba5542d2c2be0 (diff)
downloadhaskell-e5cdb1c8035f2447017867f96873aa71e6835906.tar.gz
Better loop detection in findTypeShapewip/T18304
Andreas pointed out, in !3466, that my fix for #18304 was not quite right. This patch fixes it properly, by having just one RecTcChecker rather than (implicitly) two nested ones, in findTypeShape.
-rw-r--r--compiler/GHC/Core/FamInstEnv.hs42
-rw-r--r--compiler/GHC/Core/Opt/WorkWrap/Utils.hs20
-rw-r--r--compiler/GHC/HsToCore/PmCheck/Oracle.hs13
3 files changed, 41 insertions, 34 deletions
diff --git a/compiler/GHC/Core/FamInstEnv.hs b/compiler/GHC/Core/FamInstEnv.hs
index a35f49b78f..8408bc5406 100644
--- a/compiler/GHC/Core/FamInstEnv.hs
+++ b/compiler/GHC/Core/FamInstEnv.hs
@@ -32,8 +32,8 @@ module GHC.Core.FamInstEnv (
-- Normalisation
topNormaliseType, topNormaliseType_maybe,
- normaliseType, normaliseTcApp, normaliseTcArgs,
- reduceTyFamApp_maybe,
+ normaliseType, normaliseTcApp,
+ topReduceTyFamApp_maybe, reduceTyFamApp_maybe,
-- Flattening
flattenTys
@@ -1100,7 +1100,7 @@ reduceTyFamApp_maybe :: FamInstEnvs
-- the role we seek is representational
-- It does *not* normalise the type arguments first, so this may not
-- go as far as you want. If you want normalised type arguments,
--- use normaliseTcArgs first.
+-- use topReduceTyFamApp_maybe
--
-- The TyCon can be oversaturated.
-- Works on both open and closed families
@@ -1308,10 +1308,9 @@ topNormaliseType_maybe env ty
-- to the normalised type's kind
tyFamStepper :: NormaliseStepper (Coercion, MCoercionN)
tyFamStepper rec_nts tc tys -- Try to step a type/data family
- = let (args_co, ntys, res_co) = normaliseTcArgs env Representational tc tys in
- case reduceTyFamApp_maybe env Representational tc ntys of
- Just (co, rhs) -> NS_Step rec_nts rhs (args_co `mkTransCo` co, MCo res_co)
- _ -> NS_Done
+ = case topReduceTyFamApp_maybe env tc tys of
+ Just (co, rhs, res_co) -> NS_Step rec_nts rhs (co, MCo res_co)
+ _ -> NS_Done
---------------
normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type)
@@ -1366,18 +1365,23 @@ normalise_tc_app tc tys
final_co = mkCoherenceRightCo r nty (mkSymCo kind_co) orig_to_nty
---------------
--- | Normalise arguments to a tycon
-normaliseTcArgs :: FamInstEnvs -- ^ env't with family instances
- -> Role -- ^ desired role of output coercion
- -> TyCon -- ^ tc
- -> [Type] -- ^ tys
- -> (Coercion, [Type], CoercionN)
- -- ^ co :: tc tys ~ tc new_tys
- -- NB: co might not be homogeneous
- -- last coercion :: kind(tc tys) ~ kind(tc new_tys)
-normaliseTcArgs env role tc tys
- = initNormM env role (tyCoVarsOfTypes tys) $
- normalise_tc_args tc tys
+-- | Try to simplify a type-family application, by *one* step
+-- If topReduceTyFamApp_maybe env r F tys = Just (co, rhs, res_co)
+-- then co :: F tys ~R# rhs
+-- res_co :: typeKind(F tys) ~ typeKind(rhs)
+-- Type families and data families; always Representational role
+topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type]
+ -> Maybe (Coercion, Type, Coercion)
+topReduceTyFamApp_maybe envs fam_tc arg_tys
+ | isFamilyTyCon fam_tc -- type families and data families
+ , Just (co, rhs) <- reduceTyFamApp_maybe envs role fam_tc ntys
+ = Just (args_co `mkTransCo` co, rhs, res_co)
+ | otherwise
+ = Nothing
+ where
+ role = Representational
+ (args_co, ntys, res_co) = initNormM envs role (tyCoVarsOfTypes arg_tys) $
+ normalise_tc_args fam_tc arg_tys
normalise_tc_args :: TyCon -> [Type] -- tc tys
-> NormM (Coercion, [Type], CoercionN)
diff --git a/compiler/GHC/Core/Opt/WorkWrap/Utils.hs b/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
index 2357c4e3e3..1885de98f2 100644
--- a/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
+++ b/compiler/GHC/Core/Opt/WorkWrap/Utils.hs
@@ -1025,7 +1025,19 @@ findTypeShape fam_envs ty
= TsFun (go rec_tc res)
| Just (tc, tc_args) <- splitTyConApp_maybe ty
- , Just con <- isDataProductTyCon_maybe tc
+ = go_tc rec_tc tc tc_args
+
+ | Just (_, ty') <- splitForAllTy_maybe ty
+ = go rec_tc ty'
+
+ | otherwise
+ = TsUnk
+
+ go_tc rec_tc tc tc_args
+ | Just (_, rhs, _) <- topReduceTyFamApp_maybe fam_envs tc tc_args
+ = go rec_tc rhs
+
+ | Just con <- isDataProductTyCon_maybe tc
, Just rec_tc <- if isTupleTyCon tc
then Just rec_tc
else checkRecTc rec_tc tc
@@ -1033,10 +1045,8 @@ findTypeShape fam_envs ty
-- Maybe we should do so in checkRecTc.
= TsProd (map (go rec_tc . scaledThing) (dataConInstArgTys con tc_args))
- | Just (_, ty') <- splitForAllTy_maybe ty
- = go rec_tc ty'
-
- | Just (_, ty') <- topNormaliseType_maybe fam_envs ty
+ | Just (ty', _) <- instNewTyCon_maybe tc tc_args
+ , Just rec_tc <- checkRecTc rec_tc tc
= go rec_tc ty'
| otherwise
diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
index db56ecc98c..80a844ad19 100644
--- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
@@ -372,16 +372,9 @@ pmTopNormaliseType (TySt inert) typ
tyFamStepper :: FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a)
tyFamStepper env rec_nts tc tys -- Try to step a type/data family
- = let (_args_co, ntys, _res_co) = normaliseTcArgs env Representational tc tys in
- -- NB: It's OK to use normaliseTcArgs here instead of
- -- normalise_tc_args (which takes the LiftingContext described
- -- in Note [Normalising types]) because the reduceTyFamApp below
- -- works only at top level. We'll never recur in this function
- -- after reducing the kind of a bound tyvar.
-
- case reduceTyFamApp_maybe env Representational tc ntys of
- Just (_co, rhs) -> NS_Step rec_nts rhs ((rhs:), id)
- _ -> NS_Done
+ = case topReduceTyFamApp_maybe env tc tys of
+ Just (_, rhs, _) -> NS_Step rec_nts rhs ((rhs:), id)
+ _ -> NS_Done
-- | Returns 'True' if the argument 'Type' is a fully saturated application of
-- a closed type constructor.