Commit 3540d1e1 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Avoid exponential blowup in FamInstEnv.normaliseType

Trac #13035 showed up a nasty case where we took exponentially
long to normalise a (actually rather simple) type.  Fortunately
it was easy to fix: see Note [Normalisation and type synonyms].
parent e6aefd6e
......@@ -1197,6 +1197,22 @@ coercion. Because coercions are irrelevant anyway, there is no point in doing
this. So, whenever we encounter a coercion, we just say that it won't change.
That's what the CoercionTy case is doing within normalise_type.
Note [Normalisation and type synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We need to be a bit careful about normalising in the presence of type
synonyms (Trac #13035). Suppose S is a type synonym, and we have
S t1 t2
If S is family-free (on its RHS) we can just normalise t1 and t2 and
reconstruct (S t1' t2'). Expanding S could not reveal any new redexes
because type families are saturated.
But if S has a type family on its RHS we expand /before/ normalising
the args t1, t2. If we normalise t1, t2 first, we'll re-normalise them
after expansion, and that can lead to /exponential/ behavour; see Trac #13035.
Notice, though, that expanding first can in principle duplicate t1,t2,
which might contain redexes. I'm sure you could conjure up an exponential
case by that route too, but it hasn't happened in practice yet!
-}
topNormaliseType :: FamInstEnvs -> Type -> Type
......@@ -1248,18 +1264,24 @@ normaliseTcApp env role tc tys
-- See Note [Normalising types] about the LiftingContext
normalise_tc_app :: TyCon -> [Type] -> NormM (Coercion, Type)
normalise_tc_app tc tys
= do { (args_co, ntys) <- normalise_tc_args tc tys
; case expandSynTyCon_maybe tc ntys of
{ Just (tenv, rhs, ntys') ->
do { (co2, ninst_rhs)
<- normalise_type (substTy (mkTvSubstPrs tenv) rhs)
; return $
if isReflCo co2
then (args_co, mkTyConApp tc ntys)
else (args_co `mkTransCo` co2, mkAppTys ninst_rhs ntys') }
; Nothing ->
| Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
, not (isFamFreeTyCon tc) -- Expand and try again
= -- A synonym with type families in the RHS
-- Expand and try again
-- See Note [Normalisation and type synonyms]
normalise_type (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
| not (isTypeFamilyTyCon tc)
= -- A synonym with no type families in the RHS; or data type etc
-- Just normalise the arguments and rebuild
do { (args_co, ntys) <- normalise_tc_args tc tys
; return (args_co, mkTyConApp tc ntys) }
| otherwise
= -- A type-family application
do { env <- getEnv
; role <- getRole
; (args_co, ntys) <- normalise_tc_args tc tys
; case reduceTyFamApp_maybe env role tc ntys of
Just (first_co, ty')
-> do { (rest_co,nty) <- normalise_type ty'
......@@ -1267,7 +1289,7 @@ normalise_tc_app tc tys
, nty ) }
_ -> -- No unique matching family instance exists;
-- we do not do anything
return (args_co, mkTyConApp tc ntys) }}}
return (args_co, mkTyConApp tc ntys) }
---------------
-- | Normalise arguments to a tycon
......@@ -1309,8 +1331,8 @@ normalise_type :: Type -- old type
-- See Note [Normalising types]
-- Try to not to disturb type synonyms if possible
normalise_type
= go
normalise_type ty
= go ty
where
go (TyConApp tc tys) = normalise_tc_app tc tys
go ty@(LitTy {}) = do { r <- getRole
......
{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, TypeFamilies, GADTs, PartialTypeSignatures #-}
module T13035 where
newtype MyAttr a b = MyAttr { _unMyAttr :: MyFun (a b) }
type MyRec a b = Rec (MyAttr a) b
type family MyFun (a :: k1) :: k2
data GY (a :: k1) (b :: k2) (c :: k1 -> k3) (d :: k1)
data GNone (a :: k1)
type family GYTF a where
GYTF (GY a b _ a) = b
GYTF (GY _ _ c d) = MyFun (c d)
type instance MyFun (GY a b c d) = GYTF (GY a b c d)
type family GNoneTF (a :: k1) :: k2 where
type instance MyFun (GNone a) = GNoneTF a
type (a :: k1) =: (b :: k2) = a `GY` b
type (a :: j1 -> j2) $ (b :: j1) = a b
infixr 0 $
infixr 9 =:
data FConst (a :: *) (b :: Fields)
data FApply (a :: * -> * -> *) b c (d :: Fields)
data FMap (a :: * -> *) b (d :: Fields)
type instance MyFun (FConst a b) = a
type instance MyFun (FApply b c d a) = b (MyFun (c a)) (MyFun (d a))
type instance MyFun (FMap b c a) = b (MyFun (c a))
data Fields = Name
| Author
| Image
| Description
| Ingredients
| Instructions
| CookTime
| PrepTime
| TotalTime
| Yield
| Nutrition
| Tags
| Url
| Section
| Items
| Subsections
| Calories
| Carbohydrates
| Cholesterol
| Fat
| Fiber
| Protien
| SaturatedFat
| Sodium
| Sugar
| TransFat
| UnsaturatedFat
| ServingSize
data Rec :: (u -> *) -> [u] -> * where
RNil :: Rec f '[]
(:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs)
data family Sing (a :: k)
data instance Sing (z_a6bn :: Fields)
= z_a6bn ~ Name => SName |
z_a6bn ~ Author => SAuthor |
z_a6bn ~ Image => SImage |
z_a6bn ~ Description => SDescription |
z_a6bn ~ Ingredients => SIngredients |
z_a6bn ~ Instructions => SInstructions |
z_a6bn ~ CookTime => SCookTime |
z_a6bn ~ PrepTime => SPrepTime |
z_a6bn ~ TotalTime => STotalTime |
z_a6bn ~ Yield => SYield |
z_a6bn ~ Nutrition => SNutrition |
z_a6bn ~ Tags => STags |
z_a6bn ~ Url => SUrl |
z_a6bn ~ Section => SSection |
z_a6bn ~ Items => SItems |
z_a6bn ~ Subsections => SSubsections |
z_a6bn ~ Calories => SCalories |
z_a6bn ~ Carbohydrates => SCarbohydrates |
z_a6bn ~ Cholesterol => SCholesterol |
z_a6bn ~ Fat => SFat |
z_a6bn ~ Fiber => SFiber |
z_a6bn ~ Protien => SProtien |
z_a6bn ~ SaturatedFat => SSaturatedFat |
z_a6bn ~ Sodium => SSodium |
z_a6bn ~ Sugar => SSugar |
z_a6bn ~ TransFat => STransFat |
z_a6bn ~ UnsaturatedFat => SUnsaturatedFat |
z_a6bn ~ ServingSize => SServingSize
(=::) :: sing f -> MyFun (a f) -> MyAttr a f
_ =:: x = MyAttr x
type NutritionT
= Calories =: Maybe Int
$ Carbohydrates =: Maybe Int
$ Cholesterol =: Maybe Int
$ Fat =: Maybe Int
$ Fiber =: Maybe Int
$ Protien =: Maybe Int
$ SaturatedFat =: Maybe Int
$ Sodium =: Maybe Int
$ Sugar =: Maybe Int
$ TransFat =: Maybe Int
$ UnsaturatedFat =: Maybe Int
$ ServingSize =: String
$ GNone
type NutritionRec = MyRec NutritionT ['Calories, 'Carbohydrates,
'Cholesterol, 'Fat, 'Fiber,
'Protien, 'SaturatedFat, 'Sodium,
'Sugar, 'TransFat, 'UnsaturatedFat,
'ServingSize]
type RecipeT
= Name =: String
$ Author =: String
$ Image =: String
$ Description =: String
$ CookTime =: Maybe Int
$ PrepTime =: Maybe Int
$ TotalTime =: Maybe Int
$ Yield =: String
$ Nutrition =: NutritionRec
$ Tags =: [String]
$ Url =: String
$ GNone
type RecipeFormatter = FApply (->) (FConst [String]) (FMap IO RecipeT)
g :: MyRec RecipeFormatter _ --'[ 'Author ] Uncomment to prevent loop
g = SAuthor =:: (\a -> return "Hi")
:& RNil
......@@ -898,3 +898,14 @@ test('T12234',
],
compile,
[''])
test('T13035',
[ only_ways(['normal']),
compiler_stats_num_field('bytes allocated',
[(wordsize(64), 90595208, 5),
# 2017-01-05 90595208 initial
]),
],
compile,
[''] )
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment