diff options
-rw-r--r-- | compiler/typecheck/TcCanonical.hs | 2 | ||||
-rw-r--r-- | compiler/typecheck/TcFlatten.hs | 22 | ||||
-rw-r--r-- | compiler/typecheck/TcInteract.hs | 24 | ||||
-rw-r--r-- | testsuite/tests/indexed-types/should_compile/GADT1.hs | 14 | ||||
-rw-r--r-- | testsuite/tests/perf/compiler/all.T | 6 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr | 2 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T7856.hs | 4 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_fail/T8603.stderr | 2 |
8 files changed, 52 insertions, 24 deletions
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 5232e77782..13aa8e724f 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -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, diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index 10adc9432a..01d5a101ab 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -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 diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index a9ed64acfb..c6e9fb6324 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -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] diff --git a/testsuite/tests/indexed-types/should_compile/GADT1.hs b/testsuite/tests/indexed-types/should_compile/GADT1.hs index 7761eafe97..5d09713c9b 100644 --- a/testsuite/tests/indexed-types/should_compile/GADT1.hs +++ b/testsuite/tests/indexed-types/should_compile/GADT1.hs @@ -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 diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T index 4add8e4bf0..0023ce83c1 100644 --- a/testsuite/tests/perf/compiler/all.T +++ b/testsuite/tests/perf/compiler/all.T @@ -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']) diff --git a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr index d8bec07269..1261408eb8 100644 --- a/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr +++ b/testsuite/tests/typecheck/should_fail/FrozenErrorTests.stderr @@ -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) diff --git a/testsuite/tests/typecheck/should_fail/T7856.hs b/testsuite/tests/typecheck/should_fail/T7856.hs index 825bc0bd2f..21bd41701d 100644 --- a/testsuite/tests/typecheck/should_fail/T7856.hs +++ b/testsuite/tests/typecheck/should_fail/T7856.hs @@ -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 diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr index d9d2aafd53..4e79b012a9 100644 --- a/testsuite/tests/typecheck/should_fail/T8603.stderr +++ b/testsuite/tests/typecheck/should_fail/T8603.stderr @@ -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 |