Commit c1edbdfd authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Do proper depth checking in the flattener to avoid looping.

This implements (roughly) the plan put forward in comment:14:ticket:7788,
fixing #7788, #8550, #9554, #10139, and addressing concerns raised in #10079.
There are some regressions w.r.t. GHC 7.8, but only with pathological type
families (like F a = F a). This also (hopefully -- don't have a test case)
fixes #10158. Unsolved problems include #10184 and #10185, which are both
known deficiencies of the approach used here.

As part of this change, the plumbing around detecting infinite loops has
changed. Instead of -fcontext-stack and -ftype-function-depth, we now have
one combined -freduction-depth parameter. Setting it to 0 disbales the
check, which is now the recommended way to get (terminating) code to
typecheck in releases. (The number of reduction steps may well change between
minor GHC releases!)

This commit also introduces a new IntWithInf type in BasicTypes
that represents an integer+infinity. This type is used in a few
places throughout the code.

Tests in
  indexed-types/should_fail/T7788
  indexed-types/should_fail/T8550
  indexed-types/should_fail/T9554
  indexed-types/should_compile/T10079
  indexed-types/should_compile/T10139
  typecheck/should_compile/T10184  (expected broken)
  typecheck/should_compile/T10185  (expected broken)

This commit also changes performance testsuite numbers, for the better.
parent 0f03a843
......@@ -86,7 +86,9 @@ module BasicTypes(
HValue(..),
SourceText
SourceText,
IntWithInf, infinity, treatZeroAsInf, mkIntWithInf
) where
import FastString
......@@ -1113,3 +1115,68 @@ instance Outputable FractionalLit where
ppr = text . fl_text
newtype HValue = HValue Any
{-
************************************************************************
* *
IntWithInf
* *
************************************************************************
Represents an integer or positive infinity
-}
-- | An integer or infinity
data IntWithInf = Int {-# UNPACK #-} !Int
| Infinity
deriving Eq
-- | A representation of infinity
infinity :: IntWithInf
infinity = Infinity
instance Ord IntWithInf where
compare Infinity Infinity = EQ
compare (Int _) Infinity = LT
compare Infinity (Int _) = GT
compare (Int a) (Int b) = a `compare` b
instance Outputable IntWithInf where
ppr Infinity = char '∞'
ppr (Int n) = int n
instance Num IntWithInf where
(+) = plusWithInf
(*) = mulWithInf
abs Infinity = Infinity
abs (Int n) = Int (abs n)
signum Infinity = Int 1
signum (Int n) = Int (signum n)
fromInteger = Int . fromInteger
(-) = panic "subtracting IntWithInfs"
-- | Add two 'IntWithInf's
plusWithInf :: IntWithInf -> IntWithInf -> IntWithInf
plusWithInf Infinity _ = Infinity
plusWithInf _ Infinity = Infinity
plusWithInf (Int a) (Int b) = Int (a + b)
-- | Multiply two 'IntWithInf's
mulWithInf :: IntWithInf -> IntWithInf -> IntWithInf
mulWithInf Infinity _ = Infinity
mulWithInf _ Infinity = Infinity
mulWithInf (Int a) (Int b) = Int (a * b)
-- | Turn a positive number into an 'IntWithInf', where 0 represents infinity
treatZeroAsInf :: Int -> IntWithInf
treatZeroAsInf 0 = Infinity
treatZeroAsInf n = Int n
-- | Inject any integer into an 'IntWithInf'
mkIntWithInf :: Int -> IntWithInf
mkIntWithInf = Int
......@@ -17,13 +17,10 @@ mAX_TUPLE_SIZE :: Int
mAX_TUPLE_SIZE = 62 -- Should really match the number
-- of decls in Data.Tuple
mAX_CONTEXT_REDUCTION_DEPTH :: Int
mAX_CONTEXT_REDUCTION_DEPTH = 100
-- Trac #5395 reports at least one library that needs depth 37 here
mAX_TYPE_FUNCTION_REDUCTION_DEPTH :: Int
mAX_TYPE_FUNCTION_REDUCTION_DEPTH = 200
-- Needs to be much higher than mAX_CONTEXT_REDUCTION_DEPTH; see Trac #5395
-- | Default maximum depth for both class instance search and type family
-- reduction. See also Trac #5395.
mAX_REDUCTION_DEPTH :: Int
mAX_REDUCTION_DEPTH = 200
wORD64_SIZE :: Int
wORD64_SIZE = 8
......
......@@ -168,6 +168,7 @@ import Maybes
import MonadUtils
import qualified Pretty
import SrcLoc
import BasicTypes ( IntWithInf, treatZeroAsInf )
import FastString
import Outputable
#ifdef GHCI
......@@ -692,8 +693,7 @@ data DynFlags = DynFlags {
importPaths :: [FilePath],
mainModIs :: Module,
mainFunIs :: Maybe String,
ctxtStkDepth :: Int, -- ^ Typechecker context stack depth
tyFunStkDepth :: Int, -- ^ Typechecker type function stack depth
reductionDepth :: IntWithInf, -- ^ Typechecker maximum stack depth
thisPackage :: PackageKey, -- ^ name of package currently being compiled
......@@ -1451,8 +1451,7 @@ defaultDynFlags mySettings =
importPaths = ["."],
mainModIs = mAIN,
mainFunIs = Nothing,
ctxtStkDepth = mAX_CONTEXT_REDUCTION_DEPTH,
tyFunStkDepth = mAX_TYPE_FUNCTION_REDUCTION_DEPTH,
reductionDepth = treatZeroAsInf mAX_REDUCTION_DEPTH,
thisPackage = mainPackageKey,
......@@ -2610,10 +2609,16 @@ dynamic_flags = [
(noArg (\d -> d{ liberateCaseThreshold = Nothing }))
, defFlag "frule-check"
(sepArg (\s d -> d{ ruleCheck = Just s }))
, defFlag "freduction-depth"
(intSuffix (\n d -> d{ reductionDepth = treatZeroAsInf n }))
, defFlag "fcontext-stack"
(intSuffix (\n d -> d{ ctxtStkDepth = n }))
(intSuffixM (\n d ->
do { deprecate $ "use -freduction-depth=" ++ show n ++ " instead"
; return $ d{ reductionDepth = treatZeroAsInf n } }))
, defFlag "ftype-function-depth"
(intSuffix (\n d -> d{ tyFunStkDepth = n }))
(intSuffixM (\n d ->
do { deprecate $ "use -freduction-depth=" ++ show n ++ " instead"
; return $ d{ reductionDepth = treatZeroAsInf n } }))
, defFlag "fstrictness-before"
(intSuffix (\n d -> d{ strictnessBefore = n : strictnessBefore d }))
, defFlag "ffloat-lam-args"
......@@ -3566,6 +3571,9 @@ sepArg fn = SepArg (upd . fn)
intSuffix :: (Int -> DynFlags -> DynFlags) -> OptKind (CmdLineP DynFlags)
intSuffix fn = IntSuffix (\n -> upd (fn n))
intSuffixM :: (Int -> DynFlags -> DynP DynFlags) -> OptKind (CmdLineP DynFlags)
intSuffixM fn = IntSuffix (\n -> updM (fn n))
floatSuffix :: (Float -> DynFlags -> DynFlags) -> OptKind (CmdLineP DynFlags)
floatSuffix fn = FloatSuffix (\n -> upd (fn n))
......
......@@ -30,6 +30,7 @@ import Outputable
import FastString
import MonadUtils
import ErrUtils
import BasicTypes ( IntWithInf, treatZeroAsInf, mkIntWithInf )
import Control.Monad ( when, liftM, ap )
{-
......@@ -52,11 +53,10 @@ newtype SimplM result
-- we only need IO here for dump output
data SimplTopEnv
= STE { st_flags :: DynFlags
, st_max_ticks :: Int -- Max #ticks in this simplifier run
-- Zero means infinity!
, st_rules :: RuleBase
, st_fams :: (FamInstEnv, FamInstEnv) }
= STE { st_flags :: DynFlags
, st_max_ticks :: IntWithInf -- Max #ticks in this simplifier run
, st_rules :: RuleBase
, st_fams :: (FamInstEnv, FamInstEnv) }
initSmpl :: DynFlags -> RuleBase -> (FamInstEnv, FamInstEnv)
-> UniqSupply -- No init count; set to 0
......@@ -73,14 +73,15 @@ initSmpl dflags rules fam_envs us size m
, st_max_ticks = computeMaxTicks dflags size
, st_fams = fam_envs }
computeMaxTicks :: DynFlags -> Int -> Int
computeMaxTicks :: DynFlags -> Int -> IntWithInf
-- Compute the max simplifier ticks as
-- (base-size + pgm-size) * magic-multiplier * tick-factor/100
-- where
-- magic-multiplier is a constant that gives reasonable results
-- base-size is a constant to deal with size-zero programs
computeMaxTicks dflags size
= fromInteger ((toInteger (size + base_size)
= treatZeroAsInf $
fromInteger ((toInteger (size + base_size)
* toInteger (tick_factor * magic_multiplier))
`div` 100)
where
......@@ -195,7 +196,7 @@ tick t = SM (\st_env us sc -> let sc' = doSimplTick (st_flags st_env) t sc
checkedTick :: Tick -> SimplM ()
-- Try to take a tick, but fail if too many
checkedTick t
= SM (\st_env us sc -> if st_max_ticks st_env <= simplCountN sc
= SM (\st_env us sc -> if st_max_ticks st_env <= mkIntWithInf (simplCountN sc)
then pprPanic "Simplifier ticks exhausted" (msg sc)
else let sc' = doSimplTick (st_flags st_env) t sc
in sc' `seq` return ((), us, sc'))
......
......@@ -224,13 +224,13 @@ tcInstNewTyCon_maybe tc tys = fmap (second TcCoercion) $
-- | Like 'tcLookupDataFamInst_maybe', but returns the arguments back if
-- there is no data family to unwrap.
tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType]
-> (TyCon, [TcType], TcCoercion)
-> (TyCon, [TcType], Coercion)
tcLookupDataFamInst fam_inst_envs tc tc_args
| Just (rep_tc, rep_args, co)
<- tcLookupDataFamInst_maybe fam_inst_envs tc tc_args
= (rep_tc, rep_args, TcCoercion co)
= (rep_tc, rep_args, co)
| otherwise
= (tc, tc_args, mkTcRepReflCo (mkTyConApp tc tc_args))
= (tc, tc_args, mkReflCo Representational (mkTyConApp tc tc_args))
tcLookupDataFamInst_maybe :: FamInstEnvs -> TyCon -> [TcType]
-> Maybe (TyCon, [TcType], Coercion)
......
This diff is collapsed.
......@@ -1678,21 +1678,23 @@ are created by in RtClosureInspect.zonkRTTIType.
************************************************************************
-}
solverDepthErrorTcS :: SubGoalCounter -> CtEvidence -> TcM a
solverDepthErrorTcS cnt ev
solverDepthErrorTcS :: CtLoc -> TcType -> TcM a
solverDepthErrorTcS loc ty
= setCtLoc loc $
do { pred <- zonkTcType (ctEvPred ev)
do { ty <- zonkTcType ty
; env0 <- tcInitTidyEnv
; let tidy_env = tidyFreeTyVars env0 (tyVarsOfType pred)
tidy_pred = tidyType tidy_env pred
; failWithTcM (tidy_env, hang (msg cnt) 2 (ppr tidy_pred)) }
; let tidy_env = tidyFreeTyVars env0 (tyVarsOfType ty)
tidy_ty = tidyType tidy_env ty
msg
= vcat [ text "Reduction stack overflow; size =" <+> ppr depth
, hang (text "When simplifying the following type:")
2 (ppr tidy_ty)
, note ]
; failWithTcM (tidy_env, msg) }
where
loc = ctEvLoc ev
depth = ctLocDepth loc
value = subGoalCounterValue cnt depth
msg CountConstraints =
vcat [ ptext (sLit "Context reduction stack overflow; size =") <+> int value
, ptext (sLit "Use -fcontext-stack=N to increase stack size to N") ]
msg CountTyFunApps =
vcat [ ptext (sLit "Type function application stack overflow; size =") <+> int value
, ptext (sLit "Use -ftype-function-depth=N to increase stack size to N") ]
note = vcat
[ text "Use -freduction-depth=0 to disable this check"
, text "(any upper bound you could choose might fail unpredictably with"
, text " minor updates to GHC, so disabling the check is recommended if"
, text " you're sure that type checking should terminate)" ]
......@@ -1070,7 +1070,7 @@ instance Outputable EvBind where
= sep [ pp_gw <+> ppr v
, nest 2 $ equals <+> ppr e ]
where
pp_gw = brackets (if is_given then ptext (sLit "[G]") else ptext (sLit "[W]"))
pp_gw = brackets (if is_given then char 'G' else char 'W')
-- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
instance Outputable EvTerm where
......
......@@ -1212,7 +1212,7 @@ tcTagToEnum loc fun_name arg res_ty
; let fun' = L loc (HsWrap (WpTyApp rep_ty) (HsVar fun))
rep_ty = mkTyConApp rep_tc rep_args
; return (mkHsWrapCoR (mkTcSymCo coi) $ HsApp fun' arg') }
; return (mkHsWrapCoR (mkTcSymCo $ TcCoercion coi) $ HsApp fun' arg') }
-- coi is a Representational coercion
where
doc1 = vcat [ ptext (sLit "Specify the type by giving a type signature")
......
This diff is collapsed.
......@@ -171,20 +171,20 @@ solveSimples :: Cts -> TcS ()
solveSimples cts
= {-# SCC "solveSimples" #-}
do { dyn_flags <- getDynFlags
; updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
; solve_loop (maxSubGoalDepth dyn_flags) }
do { updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
; solve_loop }
where
solve_loop max_depth
solve_loop
= {-# SCC "solve_loop" #-}
do { sel <- selectNextWorkItem max_depth
do { sel <- selectNextWorkItem
; case sel of
NoWorkRemaining -- Done, successfuly (modulo frozen)
-> return ()
MaxDepthExceeded cnt ct -- Failure, depth exceeded
-> wrapErrTcS $ solverDepthErrorTcS cnt (ctEvidence ct)
MaxDepthExceeded ct -- Failure, depth exceeded
-> wrapErrTcS $ solverDepthErrorTcS (ctLoc ct) (ctPred ct)
NextWorkItem ct -- More work, loop around!
-> do { runSolverPipeline thePipeline ct; solve_loop max_depth } }
-> do { runSolverPipeline thePipeline ct
; solve_loop } }
-- | Extract the (inert) givens and invoke the plugins on them.
......@@ -312,26 +312,26 @@ type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
data SelectWorkItem
= NoWorkRemaining -- No more work left (effectively we're done!)
| MaxDepthExceeded SubGoalCounter Ct
| MaxDepthExceeded Ct
-- More work left to do but this constraint has exceeded
-- the maximum depth for one of the subgoal counters and we
-- must stop
-- the maximum depth and we must stop
| NextWorkItem Ct -- More work left, here's the next item to look at
selectNextWorkItem :: SubGoalDepth -- Max depth allowed
-> TcS SelectWorkItem
selectNextWorkItem max_depth
= updWorkListTcS_return pick_next
selectNextWorkItem :: TcS SelectWorkItem
selectNextWorkItem
= do { dflags <- getDynFlags
; updWorkListTcS_return (pick_next dflags) }
where
pick_next :: WorkList -> (SelectWorkItem, WorkList)
pick_next wl
pick_next :: DynFlags -> WorkList -> (SelectWorkItem, WorkList)
pick_next dflags wl
= case selectWorkItem wl of
(Nothing,_)
-> (NoWorkRemaining,wl) -- No more work
(Just ct, new_wl)
| Just cnt <- subGoalDepthExceeded max_depth (ctLocDepth (ctLoc ct)) -- Depth exceeded
-> (MaxDepthExceeded cnt ct,new_wl)
(Just ct, new_wl)
| subGoalDepthExceeded dflags (ctLocDepth (ctLoc ct))
-> (MaxDepthExceeded ct,new_wl) -- Depth exceeded
| otherwise
-> (NextWorkItem ct, new_wl) -- New workitem and worklist
runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
......@@ -616,7 +616,7 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
, isWanted ev_w
, Just mkEvCs <- isCallStackIP (ctEvLoc ev_w) cls ty
= do let ev_cs =
case lookupInertDict inerts (ctEvLoc ev_w) cls tys of
case lookupInertDict inerts cls tys of
Just ev | isGiven ev -> mkEvCs (ctEvTerm ev)
_ -> mkEvCs (EvCallStack EvCsEmpty)
......@@ -629,7 +629,7 @@ interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs
setWantedEvBind (ctEvId ev_w) ev_tm
stopWith ev_w "Wanted CallStack IP"
| Just ctev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
| Just ctev_i <- lookupInertDict inerts cls tys
= do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
; case inert_effect of
IRKeep -> return ()
......@@ -1272,7 +1272,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
| not (isWanted fl) -- Never use instances for Given or Derived constraints
= try_fundeps_and_return
| Just ev <- lookupSolvedDict inerts dict_loc cls xis -- Cached
| Just ev <- lookupSolvedDict inerts cls xis -- Cached
= do { setWantedEvBind dict_id (ctEvTerm ev);
; stopWith fl "Dict/Top (cached)" }
......@@ -1287,7 +1287,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
dict_pred = mkClassPred cls xis
dict_loc = ctEvLoc fl
dict_origin = ctLocOrigin dict_loc
deeper_loc = bumpCtLocDepth CountConstraints dict_loc
deeper_loc = bumpCtLocDepth dict_loc
solve_from_instance :: [CtEvidence] -> EvTerm -> TcS (StopOrContinue Ct)
-- Precondition: evidence term matches the predicate workItem
......@@ -1298,7 +1298,8 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
; setWantedEvBind dict_id ev_term
; stopWith fl "Dict/Top (solved, no new work)" }
| otherwise
= do { traceTcS "doTopReact/found non-nullary instance for" $
= do { checkReductionDepth deeper_loc dict_pred
; traceTcS "doTopReact/found non-nullary instance for" $
ppr dict_id
; setWantedEvBind dict_id ev_term
; let mk_new_wanted ev
......@@ -1382,7 +1383,7 @@ doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
; stopWith old_ev "Fun/Top (wanted)" } } }
where
loc = ctEvLoc old_ev
deeper_loc = bumpCtLocDepth CountTyFunApps loc
deeper_loc = bumpCtLocDepth loc
try_improvement
| Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
......@@ -1400,7 +1401,6 @@ shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
shortCutReduction old_ev fsk ax_co fam_tc tc_args
| isGiven old_ev
= ASSERT( ctEvEqRel old_ev == NomEq )
runFlatten $
do { (xis, cos) <- flattenManyNom old_ev tc_args
-- ax_co :: F args ~ G tc_args
-- cos :: xis ~ tc_args
......@@ -1414,7 +1414,7 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
`mkTcTransCo` ctEvCoercion old_ev) )
; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
; emitFlatWork new_ct
; emitWorkCt new_ct
; stopWith old_ev "Fun/Top (given, shortcut)" }
| otherwise
......@@ -1434,11 +1434,11 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args
`mkTcTransCo` ctEvCoercion new_ev))
; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
; emitFlatWork new_ct
; emitWorkCt new_ct
; stopWith old_ev "Fun/Top (wanted, shortcut)" }
where
loc = ctEvLoc old_ev
deeper_loc = bumpCtLocDepth CountTyFunApps loc
deeper_loc = bumpCtLocDepth loc
dischargeFmv :: EvVar -> TcTyVar -> TcCoercion -> TcType -> TcS ()
-- (dischargeFmv x fmv co ty)
......
......@@ -16,7 +16,7 @@ For state that is global and should be returned at the end (e.g not part
of the stack mechanism), you should use an TcRef (= IORef) to store them.
-}
{-# LANGUAGE CPP, ExistentialQuantification #-}
{-# LANGUAGE CPP, ExistentialQuantification, GeneralizedNewtypeDeriving #-}
module TcRnTypes(
TcRnIf, TcRn, TcM, RnM, IfM, IfL, IfG, -- The monad is opaque outside this module
......@@ -57,16 +57,15 @@ module TcRnTypes(
ctEvidence, ctLoc, ctPred, ctFlavour, ctEqRel,
mkNonCanonical, mkNonCanonicalCt,
ctEvPred, ctEvLoc, ctEvEqRel,
ctEvTerm, ctEvCoercion, ctEvId, ctEvCheckDepth,
ctEvTerm, ctEvCoercion, ctEvId,
WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC,
andWC, unionsWC, addSimples, addImplics, mkSimpleWC, addInsols,
dropDerivedWC, insolubleImplic, trulyInsoluble,
Implication(..), ImplicStatus(..), isInsolubleStatus,
SubGoalCounter(..),
SubGoalDepth, initialSubGoalDepth, maxSubGoalDepth,
bumpSubGoalDepth, subGoalCounterValue, subGoalDepthExceeded,
SubGoalDepth, initialSubGoalDepth,
bumpSubGoalDepth, subGoalDepthExceeded,
CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,
ctLocDepth, bumpCtLocDepth,
setCtLocOrigin, setCtLocEnv, setCtLocSpan,
......@@ -109,7 +108,6 @@ import TyCon ( TyCon )
import ConLike ( ConLike(..) )
import DataCon ( DataCon, dataConUserType, dataConOrigArgTys )
import PatSyn ( PatSyn, patSynType )
import TysWiredIn ( coercibleClass )
import TcType
import Annotations
import InstEnv
......@@ -1747,31 +1745,30 @@ ctEvFlavour (CtDerived {}) = Derived
Note [SubGoalDepth]
~~~~~~~~~~~~~~~~~~~
The 'SubGoalCounter' takes care of stopping the constraint solver from looping.
Because of the different use-cases of regular constaints and type function
applications, there are two independent counters. Therefore, this datatype is
abstract. See Note [WorkList]
The 'SubGoalDepth' takes care of stopping the constraint solver from looping.
Each counter starts at zero and increases.
The counter starts at zero and increases. It includes dictionary constraints,
equality simplification, and type family reduction. (Why combine these? Because
it's actually quite easy to mistake one for another, in sufficiently involved
scenarios, like ConstraintKinds.)
* The "dictionary constraint counter" counts the depth of type class
instance declarations. Example:
The flag -fcontext-stack=n (not very well named!) fixes the maximium
level.
* The counter includes the depth of type class instance declarations. Example:
[W] d{7} : Eq [Int]
That is d's dictionary-constraint depth is 7. If we use the instance
$dfEqList :: Eq a => Eq [a]
to simplify it, we get
d{7} = $dfEqList d'{8}
where d'{8} : Eq Int, and d' has dictionary-constraint depth 8.
where d'{8} : Eq Int, and d' has depth 8.
For civilised (decidable) instance declarations, each increase of
depth removes a type constructor from the type, so the depth never
gets big; i.e. is bounded by the structural depth of the type.
The flag -fcontext-stack=n (not very well named!) fixes the maximium
level.
* The "type function reduction counter" does the same thing when resolving
* qualities involving type functions. Example:
* The counter also increments when resolving
equalities involving type functions. Example:
Assume we have a wanted at depth 7:
[W] d{7} : F () ~ a
If thre is an type function equation "F () = Int", this would be rewritten to
......@@ -1779,79 +1776,37 @@ Each counter starts at zero and increases.
and remembered as having depth 8.
Again, without UndecidableInstances, this counter is bounded, but without it
can resolve things ad infinitum. Hence there is a maximum level. But we use a
different maximum, as we expect possibly many more type function reductions
in sensible programs than type class constraints.
can resolve things ad infinitum. Hence there is a maximum level.
The flag -ftype-function-depth=n fixes the maximium level.
-}
* Lastly, every time an equality is rewritten, the counter increases. Again,
rewriting an equality constraint normally makes progress, but it's possible
the "progress" is just the reduction of an infinitely-reducing type family.
Hence we need to track the rewrites.
data SubGoalCounter = CountConstraints | CountTyFunApps
When compiling a program requires a greater depth, then GHC recommends turning
off this check entirely by setting -freduction-depth=0. This is because the
exact number that works is highly variable, and is likely to change even between
minor releases. Because this check is solely to prevent infinite compilation
times, it seems safe to disable it when a user has ascertained that their program
doesn't loop at the type level.
data SubGoalDepth -- See Note [SubGoalDepth]
= SubGoalDepth
{-# UNPACK #-} !Int -- Dictionary constraints
{-# UNPACK #-} !Int -- Type function reductions
deriving (Eq, Ord)
-}
instance Outputable SubGoalDepth where
ppr (SubGoalDepth c f) = angleBrackets $
char 'C' <> colon <> int c <> comma <>
char 'F' <> colon <> int f
-- | See Note [SubGoalDepth]
newtype SubGoalDepth = SubGoalDepth Int
deriving (Eq, Ord, Outputable)
initialSubGoalDepth :: SubGoalDepth
initialSubGoalDepth = SubGoalDepth 0 0
maxSubGoalDepth :: DynFlags -> SubGoalDepth
maxSubGoalDepth dflags = SubGoalDepth (ctxtStkDepth dflags) (tyFunStkDepth dflags)
bumpSubGoalDepth :: SubGoalCounter -> SubGoalDepth -> SubGoalDepth
bumpSubGoalDepth CountConstraints (SubGoalDepth c f) = SubGoalDepth (c+1) f
bumpSubGoalDepth CountTyFunApps (SubGoalDepth c f) = SubGoalDepth c (f+1)
subGoalCounterValue :: SubGoalCounter -> SubGoalDepth -> Int
subGoalCounterValue CountConstraints (SubGoalDepth c _) = c
subGoalCounterValue CountTyFunApps (SubGoalDepth _ f) = f
subGoalDepthExceeded :: SubGoalDepth -> SubGoalDepth -> Maybe SubGoalCounter
subGoalDepthExceeded (SubGoalDepth mc mf) (SubGoalDepth c f)
| c > mc = Just CountConstraints
| f > mf = Just CountTyFunApps
| otherwise = Nothing
-- | Checks whether the evidence can be used to solve a goal with the given minimum depth
-- See Note [Preventing recursive dictionaries]
ctEvCheckDepth :: Class -> CtLoc -> CtEvidence -> Bool
ctEvCheckDepth cls target ev
| isWanted ev
, cls == coercibleClass -- The restriction applies only to Coercible
= ctLocDepth target <= ctLocDepth (ctEvLoc ev)
| otherwise = True
initialSubGoalDepth = SubGoalDepth 0
{-
Note [Preventing recursive dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
NB: this will go away when we start treating Coercible as an equality.
We have some classes where it is not very useful to build recursive
dictionaries (Coercible, at the moment). So we need the constraint solver to
prevent that. We conservatively ensure this property using the subgoal depth of
the constraints: When solving a Coercible constraint at depth d, we do not
consider evidence from a depth <= d as suitable.
Therefore we need to record the minimum depth allowed to solve a CtWanted. This
is done in the SubGoalDepth field of CtWanted. Most code now uses mkCtWanted,
which initializes it to initialSubGoalDepth (i.e. 0); but when requesting a
Coercible instance (requestCoercible in TcInteract), we bump the current depth
by one and use that.
There are two spots where wanted contraints attempted to be solved
using existing constraints: lookupInertDict and lookupSolvedDict in
TcSMonad. Both use ctEvCheckDepth to make the check. That function
ensures that a Given constraint can always be used to solve a goal
(i.e. they are at depth infinity, for our purposes)
bumpSubGoalDepth :: SubGoalDepth -> SubGoalDepth
bumpSubGoalDepth (SubGoalDepth n) = SubGoalDepth (n + 1)
subGoalDepthExceeded :: DynFlags -> SubGoalDepth -> Bool
subGoalDepthExceeded dflags (SubGoalDepth d)
= mkIntWithInf d > reductionDepth dflags