Improve TcFlatten.flattenTyVar
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 15 Apr 2016 15:17:54 +0000 (16:17 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 15 Apr 2016 15:33:43 +0000 (16:33 +0100)
This patch tides up the structure, simplifying FlattenTvResult.

It also replaces a use of zonkTcType (which I hated) with
coercionKind, in that same function.  Happily, the result is
little faster, maybe even a percentage point or two, which is
a lot for a compiler.

This also removes the line
   || not (map binderVisibility bndrs1 == map binderVisibility bndrs2)
from TcCanonical.can_eq_nc', in the ForAllTy/ForAllTy case.

Why? Becuase I can't see why binder-visiblity should matter, and
when we use coercionKind instead of zonkTcType in flattenTyVar,
this case pops up and rejects a program that should pass.  I did
discuss this with Richard.

compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcFlatten.hs
testsuite/tests/perf/compiler/all.T

index 4bbf2e0..4ff046f 100644 (file)
@@ -599,8 +599,11 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel
  = do { let (bndrs1,body1) = tcSplitNamedPiTys s1
             (bndrs2,body2) = tcSplitNamedPiTys s2
       ; if not (equalLength bndrs1 bndrs2)
-           || not (map binderVisibility bndrs1 == map binderVisibility bndrs2)
-        then canEqHardFailure ev s1 s2
+        then do { traceTcS "Forall failure" $
+                     vcat [ ppr s1, ppr s2, ppr bndrs1, ppr bndrs2
+                          , ppr (map binderVisibility bndrs1)
+                          , ppr (map binderVisibility bndrs2) ]
+                ; canEqHardFailure ev s1 s2 }
         else
           do { traceTcS "Creating implication for polytype equality" $ ppr ev
              ; kind_cos <- zipWithM (unifyWanted loc Nominal)
index 89e663f..6737106 100644 (file)
@@ -815,7 +815,7 @@ input to the flattener) might not be zonked. After zonking everything,
 (co :: xi ~ ty) will be true, however. It is for this reason that we
 occasionally have to explicitly zonk, when (co :: xi ~ ty) is important
 even before we zonk the whole program. (In particular, this is why the
-zonk in flatten_tyvar3 is necessary.)
+zonk in flattenTyVar is necessary.)
 
 Flattening a type also means flattening its kind. In the case of a type
 variable whose kind mentions a type family, this might mean that the result
@@ -916,23 +916,7 @@ flatten_one xi@(LitTy {})
        ; return (xi, mkReflCo role xi) }
 
 flatten_one (TyVarTy tv)
-  = do { mb_yes <- flatten_tyvar tv
-       ; role <- getRole
-       ; case mb_yes of
-           FTRCasted tv' kco -> -- Done
-                       do { -- traceFlat "flattenTyVar1"
-                            --   (pprTvBndr tv' $$
-                            --    ppr kco <+> dcolon <+> ppr (coercionKind kco))
-                          ; return (ty', mkReflCo role ty
-                                         `mkCoherenceLeftCo` mkSymCo kco) }
-                    where
-                       ty  = mkTyVarTy tv'
-                       ty' = ty `mkCastTy` mkSymCo kco
-
-           FTRFollowed ty1 co1  -- Recur
-                    -> do { (ty2, co2) <- flatten_one ty1
-                          -- ; traceFlat "flattenTyVar2" (ppr tv $$ ppr ty2)
-                          ; return (ty2, co2 `mkTransCo` co1) } }
+  = flattenTyVar tv
 
 flatten_one (AppTy ty1 ty2)
   = do { (xi1,co1) <- flatten_one ty1
@@ -1270,25 +1254,56 @@ have any knowledge as to *why* these facts are true.
 
 -- | The result of flattening a tyvar "one step".
 data FlattenTvResult
-  = FTRCasted TyVar Coercion
-      -- ^ Flattening the tyvar's kind produced a cast.
-      -- co :: new kind ~N old kind;
-      -- The 'TyVar' in there might have a new, zonked kind
+  = FTRNotFollowed
+      -- ^ The inert set doesn't make the tyvar equal to anything else
+
   | FTRFollowed TcType Coercion
       -- ^ The tyvar flattens to a not-necessarily flat other type.
       -- co :: new type ~r old type, where the role is determined by
       -- the FlattenEnv
 
-flatten_tyvar :: TcTyVar -> FlatM FlattenTvResult
+flattenTyVar :: TyVar -> FlatM (Xi, Coercion)
+flattenTyVar tv
+  = do { mb_yes <- flatten_tyvar1 tv
+       ; case mb_yes of
+           FTRFollowed ty1 co1  -- Recur
+             -> do { (ty2, co2) <- flatten_one ty1
+                   -- ; traceFlat "flattenTyVar2" (ppr tv $$ ppr ty2)
+                   ; return (ty2, co2 `mkTransCo` co1) }
+
+           FTRNotFollowed   -- Done
+             -> do { let orig_kind = tyVarKind tv
+                   ; (_new_kind, kind_co) <- setMode FM_SubstOnly $
+                                             flattenKinds $
+                                             flatten_one orig_kind
+                     ; let Pair _ zonked_kind = coercionKind kind_co
+             -- NB: kind_co :: _new_kind ~ zonked_kind
+             -- But zonked_kind is not necessarily the same as orig_kind
+             -- because that may have filled-in metavars.
+             -- Moreover the returned Xi type must be well-kinded
+             -- (e.g. in canEqTyVarTyVar we use getCastedTyVar_maybe)
+             -- If you remove it, then e.g. dependent/should_fail/T11407 panics
+             -- See also Note [Flattening]
+             -- An alternative would to use (zonkTcType orig_kind),
+             -- but some simple measurements suggest that's a little slower
+                    ; let tv'    = setTyVarKind tv zonked_kind
+                          tv_ty' = mkTyVarTy tv'
+                          ty'    = tv_ty' `mkCastTy` mkSymCo kind_co
+
+                    ; role <- getRole
+                    ; return (ty', mkReflCo role tv_ty'
+                                   `mkCoherenceLeftCo` mkSymCo kind_co) } }
+
+flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult
 -- "Flattening" a type variable means to apply the substitution to it
 -- Specifically, look up the tyvar in
 --   * the internal MetaTyVar box
 --   * the inerts
 -- See also the documentation for FlattenTvResult
 
-flatten_tyvar tv
+flatten_tyvar1 tv
   | not (isTcTyVar tv)             -- Happens when flatten under a (forall a. ty)
-  = flatten_tyvar3 tv
+  = return FTRNotFollowed
           -- So ty contains references to the non-TcTyVar a
 
   | otherwise
@@ -1312,7 +1327,7 @@ flatten_tyvar2 tv fr@(flavour, eq_rel)
            Just (CTyEqCan { cc_rhs = rhs })
              -> return (FTRFollowed rhs (pprPanic "flatten_tyvar2" (ppr tv $$ ppr rhs)))
                               -- Evidence is irrelevant for Derived contexts
-           _ -> flatten_tyvar3 tv }
+           _ -> return FTRNotFollowed }
 
   | otherwise   -- For non-derived equalities, consult the inert_eqs (only)
   = do { ieqs <- liftTcS $ getInertEqs
@@ -1336,28 +1351,7 @@ flatten_tyvar2 tv fr@(flavour, eq_rel)
                     -- we are not going to touch the returned coercion
                     -- so ctEvCoercion is fine.
 
-           _other -> flatten_tyvar3 tv }
-
-flatten_tyvar3 :: TcTyVar -> FlatM FlattenTvResult
--- Always returns FTRCasted!
-flatten_tyvar3 tv
-  = -- Done, but make sure the kind is zonked
-    do { let kind = tyVarKind tv
-       ; (_new_kind, kind_co)
-           <- setMode FM_SubstOnly $
-              flattenKinds $
-              flatten_one kind
---       ; traceFlat "flattenTyVarFinal"
---           (vcat [ ppr tv <+> dcolon <+> ppr (tyVarKind tv)
---                 , ppr _new_kind
---                 , ppr kind_co <+> dcolon <+> ppr (coercionKind kind_co) ])
-       ; orig_kind <- liftTcS $ zonkTcType kind
-             -- NB: orig_kind is *not* the kind returned from flatten
-             -- This zonk is necessary because we might later see the tv's kind
-             -- in canEqTyVarTyVar (where we use getCastedTyVar_maybe).
-             -- If you remove it, then e.g. dependent/should_fail/T11407 panics
-             -- See also Note [Flattening]
-       ; return (FTRCasted (setTyVarKind tv orig_kind) kind_co) }
+           _other -> return FTRNotFollowed }
 
 {-
 Note [An alternative story for the inert substitution]
index 46d6478..765c48b 100644 (file)
@@ -300,7 +300,7 @@ test('T3064',
             # 2014-12-22: 122836340 (Windows) Death to silent superclasses
             # 2016-04-06: 153261024 (x86/Linux) probably wildcard refactor
 
-           (wordsize(64), 304344936, 5)]),
+           (wordsize(64), 287460128, 5)]),
             # (amd64/Linux) (28/06/2011):  73259544
             # (amd64/Linux) (07/02/2013): 224798696
             # (amd64/Linux) (02/08/2013): 236404384, increase from roles
@@ -321,6 +321,8 @@ test('T3064',
             #                                        Tracked as #11151.
             # (amd64/Linux) (11/12/2015): 304344936, Regression due to TypeInType
             #                                        Tracked as #11196
+            # (amd64/Linux) (15/4/2016): 287460128   Improvement due to using coercionKind instead
+            #                                        of zonkTcType (Trac #11882)
 
 ###################################
 # deactivated for now, as this metric became too volatile recently