Commit 1d44261c authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Revise the inert-set invariants again

In particular this patch

- Accepts that rewriting with the inert CTyEqCans should be done recursively
  (hence removing the Bool result from flattenTyVarOuter)

- Refines the kick-out criterion, in paticular to avoid kick-out of (a -f-> ty)
  when f cannot rewrite f.  This is true of Wanteds and hence reduces kick-outs
  of Wanteds, perhaps by a lot

This stuff is not fully documented because the details are still settling, but
it's looking good.

(And it validates.)

This patch includes the testsuite wibbles.  perf/compiler/T5030 and
T5837 both improve in bytes-allocated (by 11% and 13% resp), which is
good.  I'm not sure which of today's short series of patches is
responsible, nor do I mind much.  (One could find out if necessary.)
parent d64e6828
......@@ -670,7 +670,7 @@ canEqTyVar ev swapped tv1 ty2 ps_ty2 -- ev :: tv ~ s2
= do { traceTcS "canEqTyVar" (ppr tv1 $$ ppr ty2 $$ ppr swapped)
; mb_yes <- flattenTyVarOuter ev tv1
; case mb_yes of
Right (ty1, co1, _) -- co1 :: ty1 ~ tv1
Right (ty1, co1) -- co1 :: ty1 ~ tv1
-> do { mb <- rewriteEqEvidence ev swapped ty1 ps_ty2
co1 (mkTcNomReflCo ps_ty2)
; traceTcS "canEqTyVar2" (vcat [ppr tv1, ppr ty2, ppr swapped, ppr ty1,
......
......@@ -826,11 +826,7 @@ flattenTyVar fmode tv
where
ty' = mkTyVarTy tv'
Right (ty1, co1, True) -- No need to recurse
-> do { traceTcS "flattenTyVar2" (ppr tv $$ ppr ty1)
; return (ty1, co1) }
Right (ty1, co1, False) -- Recurse
Right (ty1, co1) -- Recurse
-> do { (ty2, co2) <- flatten fmode ty1
; traceTcS "flattenTyVar3" (ppr tv $$ ppr ty2)
; return (ty2, co2 `mkTcTransCo` co1) }
......@@ -838,14 +834,13 @@ flattenTyVar fmode tv
flattenTyVarOuter, flattenTyVarFinal
:: CtEvidence -> TcTyVar
-> TcS (Either TyVar (TcType, TcCoercion, Bool))
-> TcS (Either TyVar (TcType, TcCoercion))
-- Look up the tyvar in
-- a) the internal MetaTyVar box
-- b) the tyvar binds
-- c) the inerts
-- Return (Left tv') if it is not found, tv' has a properly zonked kind
-- (Right (ty, co, is_flat)) if found, with co :: ty ~ tv;
-- is_flat says if the result is guaranteed flattened
-- Return (Left tv') if it is not found, tv' has a properly zonked kind
-- (Right (ty, co) if found, with co :: ty ~ tv;
flattenTyVarOuter ctxt_ev tv
| not (isTcTyVar tv) -- Happens when flatten under a (forall a. ty)
......@@ -854,7 +849,7 @@ flattenTyVarOuter ctxt_ev tv
= do { mb_ty <- isFilledMetaTyVar_maybe tv
; case mb_ty of {
Just ty -> do { traceTcS "Following filled tyvar" (ppr tv <+> equals <+> ppr ty)
; return (Right (ty, mkTcNomReflCo ty, False)) } ;
; return (Right (ty, mkTcNomReflCo ty)) } ;
Nothing ->
-- Try in the inert equalities
......@@ -866,7 +861,7 @@ flattenTyVarOuter ctxt_ev tv
| CTyEqCan { cc_ev = ctev, cc_tyvar = tv, cc_rhs = rhs_ty } <- ct
, eqCanRewrite ctev ctxt_ev
-> do { traceTcS "Following inert tyvar" (ppr tv <+> equals <+> ppr rhs_ty $$ ppr ctev)
; return (Right (rhs_ty, mkTcSymCo (ctEvCoercion ctev), True)) }
; return (Right (rhs_ty, mkTcSymCo (ctEvCoercion ctev))) }
-- NB: ct is Derived then (fe_ev fmode) must be also, hence
-- we are not going to touch the returned coercion
-- so ctEvCoercion is fine.
......@@ -884,9 +879,12 @@ flattenTyVarFinal ctxt_ev tv
{-
Note [Applying the inert substitution]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- NB: 8 Dec 14: These notes are now not correct
-- Need to rewrite then when matters have settled
The inert CTyEqCans (a ~ ty), inert_eqs, can be treated as a
substitution, and indeed flattenTyVarOuter applies it to the type
being flattened. It has the following properties:
being flattened (recursively). This process should terminate.
* 'a' is not in fvs(ty)
* They are *inert*; that is the eqCanRewrite relation is everywhere false
......
......@@ -42,7 +42,7 @@ import Data.List( partition, foldl', deleteFirstsBy )
import VarEnv
import Control.Monad( when, unless, forM, foldM )
import Control.Monad
import Pair (Pair(..))
import Unique( hasKey )
import FastString ( sLit )
......@@ -952,7 +952,9 @@ kickOutRewritable new_ev new_tv
; unless (isEmptyWorkList kicked_out) $
csTraceTcS $
hang (ptext (sLit "Kick out, tv =") <+> ppr new_tv)
2 (ppr kicked_out)
2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
, text "n-kept fun-eqs =" <+> int (sizeFunEqMap (inert_funeqs ics'))
, ppr kicked_out ])
; return (workListSize kicked_out) }
kick_out :: CtEvidence -> TcTyVar -> InertCans -> (WorkList, InertCans)
......@@ -987,8 +989,10 @@ kick_out new_ev new_tv (IC { inert_eqs = tv_eqs
-- Kick out even insolubles; see Note [Kick out insolubles]
kick_out_ct :: Ct -> Bool
kick_out_ct ct = eqCanRewrite new_ev (ctEvidence ct)
&& new_tv `elemVarSet` tyVarsOfCt ct
kick_out_ct ct = kick_out_ctev (ctEvidence ct)
kick_out_ctev ev = eqCanRewrite new_ev ev
&& new_tv `elemVarSet` tyVarsOfType (ctEvPred ev)
-- See Note [Kicking out inert constraints]
kick_out_irred :: Ct -> Bool
......@@ -1003,7 +1007,17 @@ kick_out new_ev new_tv (IC { inert_eqs = tv_eqs
[] -> acc_in
(eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in)
where
(eqs_out, eqs_in) = partition kick_out_ct eqs
(eqs_out, eqs_in) = partition kick_out_eq eqs
kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev })
= eqCanRewrite new_ev ev
&& (tv == new_tv
|| (ev `eqCanRewrite` ev && new_tv `elemVarSet` tyVarsOfType rhs_ty)
|| case getTyVar_maybe rhs_ty of { Just tv_r -> tv_r == new_tv; Nothing -> False })
kick_out_eq ct = pprPanic "kick_out_eq" (ppr ct)
-- SLPJ new piece: Don't kick out a constraint unless it can rewrite itself,
-- If not, it can't rewrite anything else, so no point in
-- kicking it out
{-
Note [Kicking out inert constraints]
......
......@@ -25,3 +25,17 @@ plus_zero Zero = EQUIV
plus_zero (Succ n) = case plus_zero n of
EQUIV -> EQUIV
{-
From Succ branch of plus_zero
[G] n ~ SUCC n1 -- n1 existentially bound
[G] PLUS n1 ZERO ~ n1
[W] PLUS n ZERO ~ n
--> [W] PLUS (SUCC n1) ZERO ~ SUCC n1
--> [W] SUCC (PLUS n1 ZERO) ~ SUCC n1
--> [W] SUCC n1 ~ SUCC n1
-}
\ No newline at end of file
......@@ -314,7 +314,7 @@ test('T5030',
# previous: 196457520
# 2012-10-08: 259547660 (x86/Linux, new codegen)
# 2013-11-21: 198573456 (x86 Windows, 64 bit machine)
(wordsize(64), 385152728, 10)]),
(wordsize(64), 340969128, 10)]),
# Previously 530000000 (+/- 10%)
# 17/1/13: 602993184 (x86_64/Linux)
# (new demand analyser)
......@@ -327,6 +327,7 @@ test('T5030',
# 2014-07-17 409314320 (amd64/Linux)
# general round of updates
# 2014-09-10 385152728 post-AMP-cleanup
# 2014-12-08 340969128 constraint solver perf improvements (esp kick-out)
only_ways(['normal'])
],
......@@ -464,7 +465,7 @@ test('T5837',
# 2014-09-03: 37096484 (Windows laptop, w/w for INLINABLE things
# 2014-12-01: 135914136 (Windows laptop, regression see below)
(wordsize(64), 271028976, 10)])
(wordsize(64), 234790312, 10)])
# sample: 3926235424 (amd64/Linux, 15/2/2012)
# 2012-10-02 81879216
# 2012-09-20 87254264 amd64/Linux
......@@ -475,6 +476,7 @@ test('T5837',
# 2014-10-08 73639840 amd64/Linux, Burning Bridges and other small changes
# 2014-11-06 271028976 Linux, Accept big regression;
# See Note [An alternative story for the inert substitution] in TcFlatten
# 2014-12-08 234790312 Constraint solver perf improvements (esp kick-out)
],
compile_fail,['-ftype-function-depth=50'])
......
......@@ -27,7 +27,7 @@ FrozenErrorTests.hs:29:15:
In an equation for ‘test2’: test2 = goo2 (goo1 False undefined)
FrozenErrorTests.hs:30:9:
Couldn't match type ‘Int’ with ‘[Int]
Couldn't match type ‘[Int]’ with ‘Int’
Expected type: [[Int]]
Actual type: F [Int] Bool
In the expression: goo1 False (goo2 undefined)
......
......@@ -6,8 +6,8 @@ tmp = sequence_ lst
-- sequence_ :: Monad m => [m a] -> m ()
{- m () ~ (->) String (IO ())
m a ~ IO ()
{- m () ~ (->) String (IO ()) -- From result of sequence_
m a ~ IO () -- From argument of sequence_
Depends which one gets treated first.
m := IO
......
......@@ -16,7 +16,7 @@ T8603.hs:29:17:
return False }
T8603.hs:29:22:
Couldn't match type ‘StateT s RV t0’ with ‘RV a0’
Couldn't match type ‘RV a0’ with ‘StateT s RV t0’
Expected type: [a0] -> StateT s RV t0
Actual type: [a0] -> RV a0
Relevant bindings include
......
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