Switch off lazy flattening (fix Trac #3064)

See Note [Lazy flattening] in TcFlatten.

Lazy flattening was an apparently good idea which actually made
the type inference engine go a LOTS slower in T3064.  So I switched
it off again.

compiler/typecheck/TcBinds.lhs

@@ -682,12 +682,15 @@ mkInferredPolyId poly_name qtvs theta mono_ty
   = do { fam_envs <- tcGetFamInstEnvs
 
        ; let (_co, norm_mono_ty) = normaliseType fam_envs Nominal mono_ty
-               -- Unification may not have normalised the type, so do it
+               -- Unification may not have normalised the type,
+               -- (see Note [Lazy flattening] in TcFlatten) so do it
                -- here to make it as uncomplicated as possible.
                -- Example: f :: [F Int] -> Bool
                -- should be rewritten to f :: [Char] -> Bool, if possible
+
              my_tvs2 = closeOverKinds (growThetaTyVars theta (tyVarsOfType norm_mono_ty))
                   -- Include kind variables!  Trac #7916
+
              my_tvs   = filter (`elemVarSet` my_tvs2) qtvs   -- Maintain original order
              my_theta = filter (quantifyPred my_tvs2) theta
              inferred_poly_ty = mkSigmaTy my_tvs my_theta norm_mono_ty

compiler/typecheck/TcCanonical.lhs

@@ -676,9 +676,11 @@ canEqTyVar ev swapped tv1 ty2 ps_ty2              -- ev :: tv ~ s2
                                Stop ev s           -> return (Stop ev s)
                                ContinueWith new_ev -> can_eq_nc new_ev ty1 ty1 ty2 ps_ty2 }
 
-           Left tv1' -> do { let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
+           Left tv1' -> do { -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten
+                             -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
                                  -- Flatten the RHS less vigorously, to avoid gratuitous flattening
                                  -- True <=> xi2 should not itself be a type-function application
+                             let fmode = FE { fe_ev = ev, fe_mode = FM_FlattenAll }
                            ; (xi2, co2) <- flatten fmode ps_ty2 -- co2 :: xi2 ~ ps_ty2
                                            -- Use ps_ty2 to preserve type synonyms if poss
                            ; dflags <- getDynFlags

compiler/typecheck/TcFlatten.lhs

@@ -19,6 +19,7 @@ import TypeRep
 import Kind( isSubKind )
 import Var
 import VarEnv
+import NameEnv
 import Outputable
 import VarSet
 import TcSMonad as TcS
@@ -571,7 +572,8 @@ data FlattenEnv
 data FlattenMode  -- Postcondition for all three: inert wrt the type substitution
   = FM_FlattenAll          -- Postcondition: function-free
 
-  | FM_Avoid TcTyVar Bool  -- Postcondition:
+  | FM_Avoid TcTyVar Bool  -- See Note [Lazy flattening]
+                           -- Postcondition:
                            --  * tyvar is only mentioned in result under a rigid path
                            --    e.g.   [a] is ok, but F a won't happen
                            --  * If flat_top is True, top level is not a function application
@@ -580,6 +582,29 @@ data FlattenMode  -- Postcondition for all three: inert wrt the type substitutio
   | FM_SubstOnly           -- See Note [Flattening under a forall]
 \end{code}
 
+Note [Lazy flattening]
+~~~~~~~~~~~~~~~~~~~~~~
+The idea of FM_Avoid mode is to flatten less aggressively.  If we have
+       a ~ [F Int]
+there seems to be no great merit in lifting out (F Int).  But if it was
+       a ~ [G a Int]
+then we *do* want to lift it out, in case (G a Int) reduces to Bool, say,
+which gets rid of the occurs-check problem.  (For the flat_top Bool, see
+comments above and at call sites.)
+
+HOWEVER, the lazy flattening actually seems to make type inference go
+*slower*, not faster.  perf/compiler/T3064 is a case in point; it gets
+*dramatically* worse with FM_Avoid.  I think it may be because
+floating the types out means we normalise them, and that often makes
+them smaller and perhaps allows more re-use of previously solved
+goals.  But to be honest I'm not absolutely certain, so I am leaving
+FM_Avoid in the code base.  What I'm removing is the unique place
+where it is *used*, namely in TcCanonical.canEqTyVar.
+
+Bottom line: FM_Avoid is unused for now (Nov 14).
+Note: T5321Fun got faster when I disabled FM_Avoid
+      T5837 did too, but it's pathalogical anyway
+
 \begin{code}
 -- Flatten a bunch of types all at once.
 flattenMany :: FlattenEnv -> [Type] -> TcS ([Xi], [TcCoercion])
@@ -641,12 +666,13 @@ flatten fmode (TyConApp tc tys)
   -- For * a normal data type application
   --     * data family application
   -- we just recursively flatten the arguments.
-  | otherwise  -- Switch off the flat_top bit in FM_Avoid
-  , let fmode' = case fmode of
-                   FE { fe_mode = FM_Avoid tv _ }
-                     -> fmode { fe_mode = FM_Avoid tv False }
-                   _ -> fmode
-  = flattenTyConApp fmode' tc tys
+  | otherwise
+-- FM_Avoid stuff commented out; see Note [Lazy flattening]
+--  , let fmode' = case fmode of  -- Switch off the flat_top bit in FM_Avoid
+--                   FE { fe_mode = FM_Avoid tv _ }
+--                     -> fmode { fe_mode = FM_Avoid tv False }
+--                   _ -> fmode
+  = flattenTyConApp fmode tc tys
 
 flatten fmode ty@(ForAllTy {})
 -- We allow for-alls when, but only when, no type function
@@ -728,6 +754,8 @@ flattenFamApp fmode tc tys  -- Can be over-saturated
 
 flattenExactFamApp fmode tc tys
   = case fe_mode fmode of
+       FM_FlattenAll -> flattenExactFamApp_fully fmode tc tys
+
        FM_SubstOnly -> do { (xis, cos) <- flattenMany fmode tys
                           ; return ( mkTyConApp tc xis
                                    , mkTcTyConAppCo Nominal tc cos ) }
@@ -737,7 +765,6 @@ flattenExactFamApp fmode tc tys
                                     then flattenExactFamApp_fully fmode tc tys
                                     else return ( mkTyConApp tc xis
                                                 , mkTcTyConAppCo Nominal tc cos ) }
-       FM_FlattenAll -> flattenExactFamApp_fully fmode tc tys
 
 flattenExactFamApp_fully fmode tc tys
   = do { (xis, cos) <- flattenMany (fmode { fe_mode = FM_FlattenAll })tys

testsuite/tests/indexed-types/should_fail/T2664.stderr

 
-T2664.hs:31:33:
-    Could not deduce (Dual b ~ Dual a)
+T2664.hs:31:52:
+    Could not deduce (a ~ b)
     from the context ((a :*: b) ~ Dual c, c ~ Dual (a :*: b))
       bound by the type signature for
                  newPChan :: ((a :*: b) ~ Dual c, c ~ Dual (a :*: b)) =>
                              IO (PChan (a :*: b), PChan c)
       at T2664.hs:23:5-12
-    NB: ‘Dual’ is a type function, and may not be injective
-    Expected type: PChan c
-      Actual type: PChan (Dual b :+: Dual a)
+      ‘a’ is a rigid type variable bound by
+          the instance declaration at T2664.hs:22:10
+      ‘b’ is a rigid type variable bound by
+          the instance declaration at T2664.hs:22:10
+    Expected type: Dual (Dual a)
+      Actual type: b
     Relevant bindings include
       v :: MVar (Either (PChan a) (PChan b)) (bound at T2664.hs:24:9)
       newPChan :: IO (PChan (a :*: b), PChan c) (bound at T2664.hs:23:5)
+    In the third argument of ‘pchoose’, namely ‘newPChan’
+    In the first argument of ‘E’, namely ‘(pchoose Right v newPChan)’
     In the expression:
       E (pchoose Right v newPChan) (pchoose Left v newPChan)
-    In the first argument of ‘return’, namely
-      ‘(O $ takeMVar v, 
-        E (pchoose Right v newPChan) (pchoose Left v newPChan))’

testsuite/tests/indexed-types/should_fail/T7010.stderr

 
 T7010.hs:53:27:
-    Couldn't match type ‘IO Float’ with ‘Serial (ValueTuple Float)’
+    Couldn't match type ‘IO Float’ with ‘Serial (IO Float)’
     Expected type: (Float, ValueTuple Vector)
       Actual type: (Float, ValueTuple Float)
     In the first argument of ‘withArgs’, namely ‘plug’

testsuite/tests/indexed-types/should_fail/T8518.stderr

-
-T8518.hs:17:78:
-    Couldn't match expected type ‘F a1’
-                with actual type ‘Z a1 -> B a1 -> F a1’
-    Relevant bindings include
-      c'' :: a1 (bound at T8518.hs:17:30)
-      b' :: B a1 (bound at T8518.hs:17:21)
-      z' :: Z a1 (bound at T8518.hs:17:18)
-      c' :: a1 (bound at T8518.hs:17:15)
-      rpt :: a -> a1 -> Z a1 -> B a1 -> F a1 (bound at T8518.hs:16:9)
-    In the expression: rpt (i - 1) c''
-    In the expression:
-      let c'' = fromJust (snd <$> (continue c' z' b')) in rpt (i - 1) c''
+
+T8518.hs:14:18:
+    Couldn't match expected type ‘Maybe (F c)’ with actual type ‘F c’
+    Relevant bindings include
+      b :: B c (bound at T8518.hs:14:14)
+      z :: Z c (bound at T8518.hs:14:12)
+      c :: c (bound at T8518.hs:14:10)
+      callCont :: c -> Z c -> B c -> Maybe (F c) (bound at T8518.hs:14:1)
+    In the expression: rpt (4 :: Int) c z b
+    In an equation for ‘callCont’:
+        callCont c z b
+          = rpt (4 :: Int) c z b
+          where
+              rpt 0 c' z' b' = fromJust (fst <$> (continue c' z' b'))
+              rpt i c' z' b' = let ... in rpt (i - 1) c''
+
+T8518.hs:17:78:
+    Couldn't match expected type ‘F a1’
+                with actual type ‘Z a1 -> B a1 -> F a1’
+    Relevant bindings include
+      c'' :: a1 (bound at T8518.hs:17:30)
+      b' :: B a1 (bound at T8518.hs:17:21)
+      z' :: Z a1 (bound at T8518.hs:17:18)
+      c' :: a1 (bound at T8518.hs:17:15)
+      rpt :: a -> a1 -> Z a1 -> B a1 -> F a1 (bound at T8518.hs:16:9)
+    In the expression: rpt (i - 1) c''
+    In the expression:
+      let c'' = fromJust (snd <$> (continue c' z' b')) in rpt (i - 1) c''

testsuite/tests/perf/compiler/all.T

@@ -393,14 +393,14 @@ test('T5321Fun',
              # 2012-10-08: 344416344 x86/Linux
              #  (increase due to new codegen)
              # 2014-09-03: 299656164     (specialisation and inlining)
-            (wordsize(64), 601629032, 10)])
+            (wordsize(64), 541287000, 10)])
              # prev:       585521080
              # 29/08/2012: 713385808     #  (increase due to new codegen)
              # 15/05/2013: 628341952     #  (reason for decrease unknown)
              # 24/06/2013: 694019152     #  (reason for re-increase unknown)
              # 12/05/2014: 614409344     #  (specialisation and inlining changes)
              # 10/09/2014: 601629032     #  post-AMP-cleanp
-
+             # 06/11/2014: 541287000     #  Simon's flat-skol changes to the constraint solver
       ],
       compile,[''])
 
@@ -457,7 +457,7 @@ test('T5837',
              # 40000000 (x86/Linux)
              # 2013-11-13: 45520936 (x86/Windows, 64bit machine)
              # 2041-09-03: 37096484 (Windows laptop, w/w for INLINABLE things
-           (wordsize(64), 651924880, 10)])
+           (wordsize(64), 271028976, 10)])
              # sample: 3926235424 (amd64/Linux, 15/2/2012)
              # 2012-10-02 81879216
              # 2012-09-20 87254264 amd64/Linux
@@ -466,7 +466,7 @@ test('T5837',
              #                                  for constraints solving
              # 2014-08-29 73639840 amd64/Linux, w/w for INLINABLE things
              # 2014-10-08 73639840 amd64/Linux, Burning Bridges and other small changes
-             # 2014-11-02 651924880      Linux, Accept big regression;
+             # 2014-11-06 271028976       Linux, Accept big regression;
              #   See Note [An alternative story for the inert substitution] in TcFlatten
       ],
       compile_fail,['-ftype-function-depth=50'])