Commit 0b7e538a authored by Simon Peyton Jones's avatar Simon Peyton Jones

Allow recursive unwrapping of data families

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.
parent ff8a6716
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
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