Allow recursive unwrapping of data families
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 24 Jun 2015 21:54:27 +0000 (22:54 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 26 Jun 2015 07:33:05 +0000 (08:33 +0100)
When doing strictness analysis, we need to look inside products.
To avoid unpacking infinitely, we must be careful about
infinite types.  That in turn is controlled by TyCon.checkRecTc.

For data families like
   data instance T (a,b) = MkT a (T b)
we want to unpack the thing recursively for types like
  T (Int, (Int, (Int, Int)))

This patch elaborates the checkRecTc mechanism in TyCon, to
maintain a *count* of how many times a TyCon has shown up,
rather than just a boolean.

A simple change, and a useful one.  Fixes Trac #10482.

compiler/typecheck/FamInst.hs
compiler/types/Coercion.hs
compiler/types/FamInstEnv.hs
compiler/types/TyCon.hs

index 684ab4f..9b7acac 100644 (file)
@@ -242,22 +242,28 @@ tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
   , match : _ <- lookupFamInstEnv fam_inst_envs tc tc_args
   , FamInstMatch { fim_instance = rep_fam
                  , fim_tys      = rep_args } <- match
-  , let co_tc  = famInstAxiom rep_fam
+  , let ax     = famInstAxiom rep_fam
         rep_tc = dataFamInstRepTyCon rep_fam
-        co     = mkUnbranchedAxInstCo Representational co_tc rep_args
+        co     = mkUnbranchedAxInstCo Representational ax rep_args
   = Just (rep_tc, rep_args, co)
 
   | otherwise
   = Nothing
 
--- | Get rid of top-level newtypes, potentially looking through newtype
--- instances. Only unwraps newtypes that are in scope. This is used
--- for solving for `Coercible` in the solver. This version is careful
--- not to unwrap data/newtype instances if it can't continue unwrapping.
--- Such care is necessary for proper error messages.
+-- | 'tcTopNormaliseNewTypeTF_maybe' gets rid of top-level newtypes,
+-- potentially looking through newtype instances.
 --
--- Does not look through type families. Does not normalise arguments to a
--- tycon.
+-- It is only used by the type inference engine (specifically, when
+-- soliving 'Coercible' instances), and hence it is careful to unwrap
+-- only if the relevant data constructor is in scope.  That's why
+-- it get a GlobalRdrEnv argument.
+--
+-- It is careful not to unwrap data/newtype instances if it can't
+-- continue unwrapping.  Such care is necessary for proper error
+-- messages.
+--
+-- It does not look through type families.
+-- It does not normalise arguments to a tycon.
 --
 -- Always produces a representational coercion.
 tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs
@@ -268,15 +274,16 @@ tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
 -- cf. FamInstEnv.topNormaliseType_maybe and Coercion.topNormaliseNewType_maybe
   = fmap (first TcCoercion) $ topNormaliseTypeX_maybe stepper ty
   where
-    stepper
-      = unwrap_newtype
-        `composeSteppers`
-        \ rec_nts tc tys ->
-        case tcLookupDataFamInst_maybe faminsts tc tys of
-          Just (tc', tys', co) ->
-            modifyStepResultCo (co `mkTransCo`)
-                               (unwrap_newtype rec_nts tc' tys')
-          Nothing -> NS_Done
+    stepper = unwrap_newtype `composeSteppers` unwrap_newtype_instance
+
+    -- For newtype instances we take a double step or nothing, so that
+    -- we don't return the reprsentation type of the newtype instance,
+    -- which would lead to terrible error messages
+    unwrap_newtype_instance rec_nts tc tys
+      | Just (tc', tys', co) <- tcLookupDataFamInst_maybe faminsts tc tys
+      = modifyStepResultCo (co `mkTransCo`) $
+        unwrap_newtype rec_nts tc' tys'
+      | otherwise = NS_Done
 
     unwrap_newtype rec_nts tc tys
       | data_cons_in_scope tc
index 75750b4..80fdcc6 100644 (file)
@@ -1282,9 +1282,9 @@ type NormaliseStepper = RecTcChecker
 -- | The result of stepping in a normalisation function.
 -- See 'topNormaliseTypeX_maybe'.
 data NormaliseStepResult
-  = NS_Done   -- ^ nothing more to do
-  | NS_Abort  -- ^ utter failure. The outer function should fail too.
-  | NS_Step RecTcChecker Type Coercion  -- ^ we stepped, yielding new bits;
+  = NS_Done   -- ^ Nothing more to do
+  | NS_Abort  -- ^ Utter failure. The outer function should fail too.
+  | NS_Step RecTcChecker Type Coercion  -- ^ We stepped, yielding new bits;
                                         -- ^ co :: old type ~ new type
 
 modifyStepResultCo :: (Coercion -> Coercion)
@@ -1292,8 +1292,9 @@ modifyStepResultCo :: (Coercion -> Coercion)
 modifyStepResultCo f (NS_Step rec_nts ty co) = NS_Step rec_nts ty (f co)
 modifyStepResultCo _ result                  = result
 
--- | Try one stepper and then try the next, if the first doesn't make
--- progress.
+-- | Try one stepper and then try the next,
+-- if the first doesn't make progress.
+-- So if it returns NS_Done, it means that both steppers are satisfied
 composeSteppers :: NormaliseStepper -> NormaliseStepper
                 -> NormaliseStepper
 composeSteppers step1 step2 rec_nts tc tys
index 6c54b57..98071e8 100644 (file)
@@ -889,27 +889,26 @@ topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
 
 -- ^ Get rid of *outermost* (or toplevel)
 --      * type function redex
+--      * data family redex
 --      * newtypes
--- using appropriate coercions.  Specifically, if
+-- returning an appropriate Representaitonal coercion.  Specifically, if
 --   topNormaliseType_maybe env ty = Maybe (co, ty')
 -- then
---   (a) co :: ty ~ ty'
---   (b) ty' is not a newtype, and is not a type-family redex
+--   (a) co :: ty ~R ty'
+--   (b) ty' is not a newtype, and is not a type-family or data-family redex
 --
 -- However, ty' can be something like (Maybe (F ty)), where
 -- (F ty) is a redex.
 --
 -- Its a bit like Type.repType, but handles type families too
--- The coercion returned is always an R coercion
 
 topNormaliseType_maybe env ty
   = topNormaliseTypeX_maybe stepper ty
   where
-    stepper
-      = unwrapNewTypeStepper
-        `composeSteppers`
-        \ rec_nts tc tys ->
-        let (args_co, ntys) = normaliseTcArgs env Representational tc tys in
+    stepper = unwrapNewTypeStepper `composeSteppers` tyFamStepper
+
+    tyFamStepper rec_nts tc tys  -- Try to step a type/data familiy
+      = let (args_co, ntys) = 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)
           Nothing        -> NS_Done
index c572828..1cacf2e 100644 (file)
@@ -104,7 +104,7 @@ import BasicTypes
 import DynFlags
 import ForeignCall
 import Name
-import NameSet
+import NameEnv
 import CoAxiom
 import PrelNames
 import Maybes
@@ -1827,9 +1827,10 @@ the key examples:
   Id (Id Int)    Int
   Fix Id         NO NO NO
 
-Notice that we can expand T, even though it's recursive.
-And we can expand Id (Id Int), even though the Id shows up
-twice at the outer level.
+Notice that
+ * We can expand T, even though it's recursive.
+ * We can expand Id (Id Int), even though the Id shows up
+   twice at the outer level, because Id is non-recursive
 
 So, when expanding, we keep track of when we've seen a recursive
 newtype at outermost level; and bale out if we see it again.
@@ -1837,20 +1838,37 @@ newtype at outermost level; and bale out if we see it again.
 We sometimes want to do the same for product types, so that the
 strictness analyser doesn't unbox infinitely deeply.
 
-The function that manages this is checkRecTc.
+More precisely, we keep a *count* of how many times we've seen it.
+This is to account for
+   data instance T (a,b) = MkT (T a) (T b)
+Then (Trac #10482) if we have a type like
+        T (Int,(Int,(Int,(Int,Int))))
+we can still unbox deeply enough during strictness analysis.
+We have to treat T as potentially recursive, but it's still
+good to be able to unwrap multiple layers.
+
+The function that manages all this is checkRecTc.
 -}
 
-newtype RecTcChecker = RC NameSet
+data RecTcChecker = RC !Int (NameEnv Int)
+  -- The upper bound, and the number of times
+  -- we have encountered each TyCon
 
 initRecTc :: RecTcChecker
-initRecTc = RC emptyNameSet
+-- Intialise with a fixed max bound of 100
+-- We should probably have a flag for this
+initRecTc = RC 100 emptyNameEnv
 
 checkRecTc :: RecTcChecker -> TyCon -> Maybe RecTcChecker
 -- Nothing      => Recursion detected
 -- Just rec_tcs => Keep going
-checkRecTc (RC rec_nts) tc
-  | not (isRecursiveTyCon tc)     = Just (RC rec_nts)
-  | tc_name `elemNameSet` rec_nts = Nothing
-  | otherwise                     = Just (RC (extendNameSet rec_nts tc_name))
+checkRecTc rc@(RC bound rec_nts) tc
+  | not (isRecursiveTyCon tc)
+  = Just rc  -- Tuples are a common example here
+  | otherwise
+  = case lookupNameEnv rec_nts tc_name of
+      Just n | n >= bound -> Nothing
+             | otherwise  -> Just (RC bound (extendNameEnv rec_nts tc_name (n+1)))
+      Nothing             -> Just (RC bound (extendNameEnv rec_nts tc_name 1))
   where
     tc_name = tyConName tc