[commit: ghc] wip/new-flatten-skolems-Aug14: Esablish the flattening invariant for CTyEqCan (e94d2ab)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/new-flatten-skolems-Aug14
Link       : http://ghc.haskell.org/trac/ghc/changeset/e94d2ab2b23a494bb47ac25b2a1fbeb46739f3c4/ghc

>---------------------------------------------------------------

commit e94d2ab2b23a494bb47ac25b2a1fbeb46739f3c4
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Thu Oct 2 17:50:48 2014 +0100

    Esablish the flattening invariant for CTyEqCan


>---------------------------------------------------------------

e94d2ab2b23a494bb47ac25b2a1fbeb46739f3c4
 compiler/typecheck/TcCanonical.lhs | 37 +++++++++++++++++++++++--------------
 1 file changed, 23 insertions(+), 14 deletions(-)

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index fd07c5c..79f1eb1 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -458,10 +458,16 @@ data FlattenEnv
   = FE { fe_mode :: FlattenMode
        , fe_ev   :: CtEvidence }
 
-data FlattenMode
-  = FM_FlattenAll     -- Flatten all type functions
-  | FM_Avoid TcTyVar  -- Flatten type functions to avoid this type variable
-  | FM_SubstOnly      -- See Note [Flattening under a forall]
+data FlattenMode  -- Postcondition for all three: inert wrt the type substitution
+  = FM_FlattenAll          -- Postcondition: function-free
+
+  | FM_Avoid TcTyVar Bool  -- 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
+                           --   (but under type constructors is ok e.g. [F a])
+
+  | FM_SubstOnly           -- See Note [Flattening under a forall]
 
 -- Flatten a bunch of types all at once.
 flattenMany :: FlattenEnv -> [Type] -> TcS ([Xi], [TcCoercion])
@@ -522,11 +528,13 @@ flatten fmode (TyConApp tc tys)
 
   -- For * a normal data type application
   --     * data family application
-  --     * type synonym application whose RHS does not mention type families
-  --             See Note [Flattening synonyms]
   -- we just recursively flatten the arguments.
-  | otherwise
-  = flattenTyConApp fmode tc tys
+  | 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
 
 flatten fmode ty@(ForAllTy {})
 -- We allow for-alls when, but only when, no type function
@@ -605,11 +613,11 @@ flattenExactFamApp fmode tc tys
                           ; return ( mkTyConApp tc xis
                                    , mkTcTyConAppCo Nominal tc cos ) }
 
-       FM_Avoid tv -> do { (xis, cos) <- flattenMany fmode tys
-                         ; if tv `elemVarSet` tyVarsOfTypes xis
-                           then flattenExactFamApp_fully fmode tc tys
-                           else return ( mkTyConApp tc xis
-                                       , mkTcTyConAppCo Nominal tc cos ) }
+       FM_Avoid tv flat_top -> do { (xis, cos) <- flattenMany fmode tys
+                                  ; if flat_top || tv `elemVarSet` tyVarsOfTypes xis
+                                    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
@@ -1157,7 +1165,8 @@ canEqTyVar ev swapped tv1 ty2 ps_ty2              -- ev :: tv ~ s2
                                       Nothing     -> return Stop
                                       Just 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' }
+           Left tv1' -> do { let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True }
+                                 -- Flatten the RHS less vigorously, to avoid gratuitous
                            ; (xi2, co2) <- flatten fmode ps_ty2 -- co2 :: xi2 ~ ps_ty2
                                            -- Use ps_ty2 to preserve type synonyms if poss
                            ; dflags <- getDynFlags