Work in progress on better generalisation technologywip/T8995-level-generalisation

There's a long explanation in Trac #8995.  This branch just
captures where I'm up to.

10 files changed, 116 insertions, 97 deletions

diff --git a/compiler/typecheck/FunDeps.lhs b/compiler/typecheck/FunDeps.lhs
index 1dc96aa037..5ff7cdadb6 100644
--- a/compiler/typecheck/FunDeps.lhs
+++ b/compiler/typecheck/FunDeps.lhs
@@ -13,7 +13,7 @@ module FunDeps (
         Equation(..), pprEquation,
         improveFromInstEnv, improveFromAnother,
         checkInstCoverage, checkFunDeps,
-        growThetaTyVars, pprFundeps
+        pprFundeps
     ) where
 
 #include "HsVersions.h"
@@ -38,46 +38,6 @@ import Data.Maybe       ( isJust )
 
 %************************************************************************
 %*                                                                      *
-\subsection{Close type variables}
-%*                                                                      *
-%************************************************************************
-
-Note [Growing the tau-tvs using constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-(growThetaTyVars insts tvs) is the result of extending the set
-    of tyvars tvs using all conceivable links from pred
-
-E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
-Then growThetaTyVars preds tvs = {a,b,c}
-
-Notice that
-   growThetaTyVars is conservative       if v might be fixed by vs
-                                         => v `elem` grow(vs,C)
-
-\begin{code}
-growThetaTyVars :: ThetaType -> TyVarSet -> TyVarSet
--- See Note [Growing the tau-tvs using constraints]
-growThetaTyVars theta tvs
-  | null theta = tvs
-  | otherwise  = fixVarSet mk_next tvs
-  where
-    mk_next tvs = foldr grow_one tvs theta
-    grow_one pred tvs = growPredTyVars pred tvs `unionVarSet` tvs
-
-growPredTyVars :: PredType
-               -> TyVarSet      -- The set to extend
-               -> TyVarSet      -- TyVars of the predicate if it intersects the set,
-growPredTyVars pred tvs
-   | isIPPred pred                   = pred_tvs   -- Always quantify over implicit parameers
-   | pred_tvs `intersectsVarSet` tvs = pred_tvs
-   | otherwise                       = emptyVarSet
-  where
-    pred_tvs = tyVarsOfType pred
-\end{code}
-
-
-%************************************************************************
-%*                                                                      *
 \subsection{Generate equations from functional dependencies}
 %*                                                                      *
 %************************************************************************
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index 8b2928c8c8..5713125c83 100644
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -30,7 +30,6 @@ import TcMType
 import PatSyn
 import ConLike
 import Type( tidyOpenType )
-import FunDeps( growThetaTyVars )
 import TyCon
 import TcType
 import TysPrim
@@ -553,7 +552,8 @@ tcPolyInfer
   -> [(Origin, LHsBind Name)]
   -> TcM (LHsBinds TcId, [TcId], TopLevelFlag)
 tcPolyInfer rec_tc prag_fn tc_sig_fn mono closed bind_list
-  = do { ((binds', mono_infos), wanted)
+  = tcPushUntouchables $
+    do { ((binds', mono_infos), wanted)
              <- captureConstraints $
                 tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
 
@@ -609,10 +609,9 @@ mkExport prag_fn qtvs theta (poly_name, mb_sig, mono_id)
               -- In the inference case (no signature) this stuff figures out
               -- the right type variables and theta to quantify over
               -- See Note [Impedence matching]
-              my_tvs2 = closeOverKinds (growThetaTyVars theta (tyVarsOfType mono_ty))
+              (my_tvs2, my_theta) = growThetaTyVars (const True) (tyVarsOfType mono_ty) theta
+              my_tvs   = filter (`elemVarSet` closeOverKinds my_tvs2) qtvs   -- Maintain original order
                             -- 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 mono_ty
 
         ; poly_id <- addInlinePrags poly_id prag_sigs
diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index b9f3d259fc..dac807e98a 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -284,7 +284,7 @@ newSigTyVar name kind
 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
 newMetaDetails info 
   = do { ref <- newMutVar Flexi
-       ; untch <- getUntouchables
+       ; untch <- tcGetUntouchables
        ; return (MetaTv { mtv_info = info, mtv_ref = ref, mtv_untch = untch }) }
 \end{code}
 
@@ -755,7 +755,7 @@ zonkEvVar var = do { ty' <- zonkTcType (varType var)
 zonkWC :: EvBindsVar -- May add new bindings for wanted family equalities in here
        -> WantedConstraints -> TcM WantedConstraints
 zonkWC binds_var wc
-  = do { untch <- getUntouchables
+  = do { untch <- tcGetUntouchables
        ; zonkWCRec binds_var untch wc }
 
 zonkWCRec :: EvBindsVar
diff --git a/compiler/typecheck/TcRnDriver.lhs b/compiler/typecheck/TcRnDriver.lhs
index 90d7151c69..667355938a 100644
--- a/compiler/typecheck/TcRnDriver.lhs
+++ b/compiler/typecheck/TcRnDriver.lhs
@@ -1794,8 +1794,9 @@ tcRnExpr hsc_env rdr_expr
         -- it might have a rank-2 type (e.g. :t runST)
     uniq <- newUnique ;
     let { fresh_it  = itName uniq (getLoc rdr_expr) } ;
-    ((_tc_expr, res_ty), lie) <- captureConstraints $ 
-                                 tcInferRho rn_expr ;
+    (((_tc_expr, res_ty), _), lie) <- captureConstraints $ 
+                                      captureUntouchables $
+                                      tcInferRho rn_expr ;
     ((qtvs, dicts, _, _), lie_top) <- captureConstraints $
                                       {-# SCC "simplifyInfer" #-}
                                       simplifyInfer True {- Free vars are closed -}
diff --git a/compiler/typecheck/TcRnMonad.lhs b/compiler/typecheck/TcRnMonad.lhs
index b3d37f6178..6dd4df9859 100644
--- a/compiler/typecheck/TcRnMonad.lhs
+++ b/compiler/typecheck/TcRnMonad.lhs
@@ -1126,12 +1126,18 @@ captureUntouchables thing_inside
                 thing_inside
        ; return (res, untch') }
 
-getUntouchables :: TcM Untouchables
-getUntouchables = do { env <- getLclEnv
+tcPushUntouchables :: TcM a -> TcM a
+tcPushUntouchables thing_inside
+  = do { env <- getLclEnv
+       ; let untch' = pushUntouchables (tcl_untch env)
+       ; setLclEnv (env { tcl_untch = untch' }) thing_inside }
+
+tcGetUntouchables :: TcM Untouchables
+tcGetUntouchables = do { env <- getLclEnv
                      ; return (tcl_untch env) }
 
-setUntouchables :: Untouchables -> TcM a -> TcM a
-setUntouchables untch thing_inside 
+tcSetUntouchables :: Untouchables -> TcM a -> TcM a
+tcSetUntouchables untch thing_inside 
   = updLclEnv (\env -> env { tcl_untch = untch }) thing_inside
 
 isTouchableTcM :: TcTyVar -> TcM Bool
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index b7faf153ca..229ab6b239 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -1125,7 +1125,7 @@ nestImplicTcS ref inner_untch inerts (TcS thing_inside)
                                , tcs_implics     = panic "nextImplicTcS: implics"
                                -- NB: Both these are initialised by withWorkList
                                }
-       ; res <- TcM.setUntouchables inner_untch $
+       ; res <- TcM.tcSetUntouchables inner_untch $
                 thing_inside nest_env
 
 #ifdef DEBUG
@@ -1250,7 +1250,7 @@ getTcEvBinds :: TcS EvBindsVar
 getTcEvBinds = TcS (return . tcs_ev_binds)
 
 getUntouchables :: TcS Untouchables
-getUntouchables = wrapTcS TcM.getUntouchables
+getUntouchables = wrapTcS TcM.tcGetUntouchables
 
 getGivenInfo :: TcS a -> TcS (Bool, [TcTyVar], a)
 -- Run thing_inside, returning info on
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 64ef3fed4b..f97c3abc1d 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -1,6 +1,6 @@
 \begin{code}
 module TcSimplify(
-       simplifyInfer, quantifyPred,
+       simplifyInfer, growThetaTyVars,
        simplifyAmbiguityCheck,
        simplifyDefault,
        simplifyRule, simplifyTop, simplifyInteractive,
@@ -18,7 +18,6 @@ import TcSMonad as TcS
 import TcInteract
 import Kind     ( isKind, defaultKind_maybe )
 import Inst
-import FunDeps  ( growThetaTyVars )
 import Type     ( classifyPredType, PredTree(..), getClassPredTys_maybe )
 import Class    ( Class )
 import Var
@@ -266,7 +265,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
        ; quant_pred_candidates   -- Fully zonked
            <- if insolubleWC wanted_transformed_incl_derivs
               then return []   -- See Note [Quantification with errors]
-                               -- NB: must include derived errors in this test, 
+                               -- NB: must include derived errors in this test,
                                --     hence "incl_derivs"
 
               else do { let quant_cand = approximateWC wanted_transformed
@@ -276,7 +275,7 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
                             -- Miminise quant_cand.  We are not interested in any evidence
                             -- produced, because we are going to simplify wanted_transformed
                             -- again later. All we want here is the predicates over which to
-                            -- quantify.  
+                            -- quantify.
                             --
                             -- If any meta-tyvar unifications take place (unlikely), we'll
                             -- pick that up later.
@@ -291,10 +290,10 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
                                   filterBag isWantedCt flats
                            -- The quant_cand were already fully zonked, so this zonkFlats
                            -- really only unflattens the flattening that solveInteract
-                           -- may have done (Trac #8889).  
+                           -- may have done (Trac #8889).
                            -- E.g. quant_cand = F a, where F :: * -> Constraint
                            --      We'll flatten to   (alpha, F a ~ alpha)
-                           -- fail to make any further progress and must unflatten again 
+                           -- fail to make any further progress and must unflatten again
 
                       ; return (map ctPred $ bagToList flats') }
 
@@ -302,33 +301,46 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
        --     unifications that may have happened
        ; gbl_tvs        <- tcGetGlobalTyVars
        ; zonked_tau_tvs <- TcM.zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
-       ; let poly_qtvs = growThetaTyVars quant_pred_candidates zonked_tau_tvs
-                         `minusVarSet` gbl_tvs
-             pbound    = filter (quantifyPred poly_qtvs) quant_pred_candidates
+       ; let constrained_tvs
+                | apply_mr  = tyVarsOfTypes quant_pred_candidates
+                | otherwise = tyVarsOfTypes (snd (growThetaTyVars (const True) gbl_tvs (filter isEqPred quant_pred_candidates)))
+
+             all_constrained_tvs = gbl_tvs `unionVarSet` constrained_tvs
+
+             (poly_qtvs, bound)
+                 | apply_mr  = (zonked_tau_tvs `minusVarSet` all_constrained_tvs, [])
+                 | otherwise = growThetaTyVars (\tv -> not (tv `elemVarSet` all_constrained_tvs))
+                                               zonked_tau_tvs quant_pred_candidates
 
              -- Monomorphism restriction
-             constrained_tvs = tyVarsOfTypes pbound `unionVarSet` gbl_tvs
-             mr_bites        = apply_mr && not (null pbound)
+             mr_bites = not (constrained_tvs `subVarSet` gbl_tvs)
+
+#ifdef DEBUG
+       ; let check_untch str bad_tvs
+               = WARN( not (null bad_tvs),
+                       hang (text ("Bad generalisation: " ++ str))
+                          2 (vcat [ppr untch, ppr bad_tvs]) )
+                 return ()
 
-       ; (qtvs, bound) <- if mr_bites
-                          then do { qtvs <- quantifyTyVars constrained_tvs zonked_tau_tvs
-                                  ; return (qtvs, []) }
-                          else do { qtvs <- quantifyTyVars gbl_tvs poly_qtvs
-                                  ; return (qtvs, pbound) }
+       ; check_untch "gbl tvs" (filter (isTouchableMetaTyVar untch) (varSetElems gbl_tvs))
+       ; check_untch "qtvs"    (filterOut (isTouchableMetaTyVar untch) (varSetElems poly_qtvs))
+#endif
+
+       ; qtvs <- quantifyTyVars all_constrained_tvs poly_qtvs
 
        ; traceTc "simplifyWithApprox" $
          vcat [ ptext (sLit "quant_pred_candidates =") <+> ppr quant_pred_candidates
+              , ptext (sLit "mr_bites =") <+> ppr mr_bites
               , ptext (sLit "gbl_tvs=") <+> ppr gbl_tvs
               , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs
-              , ptext (sLit "pbound =") <+> ppr pbound
-              , ptext (sLit "bbound =") <+> ppr bound
+              , ptext (sLit "bound =") <+> ppr bound
               , ptext (sLit "poly_qtvs =") <+> ppr poly_qtvs
               , ptext (sLit "constrained_tvs =") <+> ppr constrained_tvs
-              , ptext (sLit "mr_bites =") <+> ppr mr_bites
               , ptext (sLit "qtvs =") <+> ppr qtvs ]
 
        ; if null qtvs && null bound
          then do { traceTc "} simplifyInfer/no implication needed" empty
+                 ; mapM_ (promoteTyVarTcM (popUntouchables untch)) (varSetElems constrained_tvs)
                  ; emitConstraints wanted_transformed
                     -- Includes insolubles (if -fdefer-type-errors)
                     -- as well as flats and implications
@@ -345,7 +357,12 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
                         -- tidied uniformly
 
        ; minimal_bound_ev_vars <- mapM TcM.newEvVar minimal_flat_preds
-       ; let implic = Implic { ic_untch    = pushUntouchables untch
+
+       ; mapM_ (promoteTyVarTcM (popUntouchables untch)) $
+         varSetElems ((zonked_tau_tvs `unionVarSet` tyVarsOfTypes minimal_flat_preds) `minusVarSet` poly_qtvs)
+
+       ; unless (isEmptyWC wanted_transformed) $
+         do { let implic = Implic { ic_untch    = untch
                              , ic_skols    = qtvs
                              , ic_no_eqs   = False
                              , ic_fsks     = []  -- wanted_tansformed arose only from solveWanteds
@@ -356,25 +373,47 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
                              , ic_binds    = ev_binds_var
                              , ic_info     = skol_info
                              , ic_env      = tc_lcl_env }
-       ; emitImplication implic
 
-       ; traceTc "} simplifyInfer/produced residual implication for quantification" $
-             vcat [ ptext (sLit "implic =") <+> ppr implic
-                       -- ic_skols, ic_given give rest of result
-                  , ptext (sLit "qtvs =") <+> ppr qtvs
-                  , ptext (sLit "spb =") <+> ppr quant_pred_candidates
-                  , ptext (sLit "bound =") <+> ppr bound ]
+            ; emitImplication implic
+            ; traceTc "} simplifyInfer/produced residual implication for quantification" $
+                  vcat [ ptext (sLit "implic =") <+> ppr implic
+                            -- ic_skols, ic_given give rest of result
+                       , ptext (sLit "qtvs =") <+> ppr qtvs
+                       , ptext (sLit "spb =") <+> ppr quant_pred_candidates
+                       , ptext (sLit "bound =") <+> ppr bound ] }
 
        ; return ( qtvs, minimal_bound_ev_vars
                 , mr_bites,  TcEvBinds ev_binds_var) } }
 
-quantifyPred :: TyVarSet           -- Quantifying over these
-             -> PredType -> Bool   -- True <=> quantify over this wanted
-quantifyPred qtvs pred
-  | isIPPred pred = True  -- Note [Inheriting implicit parameters]
-  | otherwise     = tyVarsOfType pred `intersectsVarSet` qtvs
+growThetaTyVars :: (TcTyVar -> Bool) -> TyVarSet -> ThetaType -> (TyVarSet, ThetaType)
+-- See Note [Growing the tau-tvs using constraints]
+growThetaTyVars quantify_tv tvs theta
+  = go (filterVarSet quantify_tv tvs) [] [] theta
+  where
+    go tvs _           q_preds [] = (tvs, q_preds)
+    go tvs non_q_preds q_preds (pred:preds)
+      | not quantify_me          = go tvs (pred:non_q_preds) q_preds preds
+      | pred_tvs `subVarSet` tvs = go tvs non_q_preds (pred:q_preds) preds
+      | otherwise                = go (tvs `unionVarSet` pred_tvs)
+                                      [] (pred:q_preds)
+                                      (non_q_preds ++ preds)
+      where
+        pred_tvs = filterVarSet quantify_tv (tyVarsOfType pred)
+        quantify_me = isIPPred pred || pred_tvs `intersectsVarSet` tvs
 \end{code}
 
+Note [Growing the tau-tvs using constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(growThetaTyVars insts tvs) is the result of extending the set
+    of tyvars tvs using all conceivable links from pred
+
+E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
+Then growThetaTyVars preds tvs = {a,b,c}
+
+Notice that
+   growThetaTyVars is conservative       if v might be fixed by vs
+                                         => v `elem` grow(vs,C)
+
 Note [Inheriting implicit parameters]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this:
@@ -860,6 +899,15 @@ promoteTyVar untch tv
   | otherwise
   = return ()
 
+promoteTyVarTcM :: Untouchables -> TcTyVar  -> TcM ()
+promoteTyVarTcM untch tv
+  | isFloatedTouchableMetaTyVar untch tv
+  = do { cloned_tv <- TcM.cloneMetaTyVar tv
+       ; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch
+       ; writeMetaTyVar tv (mkTyVarTy rhs_tv) }
+  | otherwise
+  = return ()
+
 promoteAndDefaultTyVar :: Untouchables -> TcTyVarSet -> TyVar -> TcS ()
 -- See Note [Promote _and_ default when inferring]
 promoteAndDefaultTyVar untch gbl_tvs tv
@@ -1155,14 +1203,16 @@ with two implications and a class with a functional dependency.
     class C x y | x -> y
     instance C [a] [a]
 
-    (I1)      [untch=beta]forall b. 0 => F Int ~ [beta]
-    (I2)      [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
+    (I1)      forall(1) b. 0 => F Int ~ [beta(0)]
+    (I2)      forall(1) c. 0 => F Int ~ [[alpha(1)]] /\ C beta(0) [c]
 
 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
 They may react to yield that (beta := [alpha]) which can then be pushed inwards
-the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
-(alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
-beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
+the leftover of I2 to get (C [alpha] [c]) which, using the FunDep, will mean that
+(alpha := c). In the end we will have the skolem 'c' escaping. By promoting alpha
+to level 0, we stop this happening.
+
+Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
 
     class C x y | x -> y where
      op :: x -> y -> ()
diff --git a/compiler/typecheck/TcTyClsDecls.lhs b/compiler/typecheck/TcTyClsDecls.lhs
index 3a589a9ce1..fc0f3500f3 100644
--- a/compiler/typecheck/TcTyClsDecls.lhs
+++ b/compiler/typecheck/TcTyClsDecls.lhs
@@ -29,7 +29,7 @@ import TcEnv
 import TcValidity
 import TcHsSyn
 import TcBinds( tcRecSelBinds )
-import FunDeps( growThetaTyVars )
+import TcSimplify( growThetaTyVars )
 import TcTyDecls
 import TcClassDcl
 import TcHsType
@@ -1619,7 +1619,7 @@ checkValidClass cls
                 -- Here, MonadState has a fundep m->b, so newBoard is fine
                 -- The check is disabled for nullary type classes,
                 -- since there is no possible ambiguity
-        ; let grown_tyvars = growThetaTyVars theta (mkVarSet tyvars)
+        ; let (grown_tyvars, _) = growThetaTyVars (const True) (mkVarSet tyvars) theta
         ; checkTc (arity == 0 || tyVarsOfType tau `intersectsVarSet` grown_tyvars)
                   (noClassTyVarErr cls sel_id)
 
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 08c7a627ce..907ef451cb 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/compiler/typecheck/TcType.lhs
@@ -22,7 +22,7 @@ module TcType (
   TcTyVar, TcTyVarSet, TcKind, TcCoVar,
 
   -- Untouchables
-  Untouchables(..), noUntouchables, pushUntouchables, isTouchable,
+  Untouchables(..), noUntouchables, pushUntouchables, popUntouchables, isTouchable,
 
   --------------------------------
   -- MetaDetails
@@ -435,6 +435,9 @@ noUntouchables = Untouchables 0   -- 0 = outermost level
 pushUntouchables :: Untouchables -> Untouchables
 pushUntouchables (Untouchables us) = Untouchables (us+1)
 
+popUntouchables :: Untouchables -> Untouchables
+popUntouchables (Untouchables us) = ASSERT( us > 0 ) Untouchables (us-1)
+
 isFloatedTouchable :: Untouchables -> Untouchables -> Bool
 isFloatedTouchable (Untouchables ctxt_untch) (Untouchables tv_untch)
   = ctxt_untch < tv_untch
diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs
index 94b6aebeb5..d1d897fb44 100644
--- a/compiler/typecheck/TcUnify.lhs
+++ b/compiler/typecheck/TcUnify.lhs
@@ -557,7 +557,7 @@ uType_defer origin ty1 ty2
 --------------
 -- unify_np (short for "no push" on the origin stack) does the work
 uType origin orig_ty1 orig_ty2
-  = do { untch <- getUntouchables
+  = do { untch <- tcGetUntouchables
        ; traceTc "u_tys " $ vcat 
               [ text "untch" <+> ppr untch
               , sep [ ppr orig_ty1, text "~", ppr orig_ty2]