Wibbles to yesterday's "Simplify kind generalisation" patch
[ghc.git] / compiler / typecheck / TcSimplify.lhs
index 09a5b11..2cbb5af 100644 (file)
@@ -7,8 +7,9 @@
 -- for details
 
 module TcSimplify( 
-       simplifyInfer, simplifyAmbiguityCheck,
-       simplifyDefault, simplifyDeriv, 
+       simplifyInfer, quantifyPred,
+       simplifyAmbiguityCheck,
+       simplifyDefault, 
        simplifyRule, simplifyTop, simplifyInteractive,
        solveWantedsTcM
   ) where
@@ -18,11 +19,12 @@ module TcSimplify(
 import TcRnTypes
 import TcRnMonad
 import TcErrors
-import TcMType
+import TcMType as TcM
 import TcType 
-import TcSMonad 
+import TcSMonad as TcS
 import TcInteract 
 import Inst
+import FunDeps  ( growThetaTyVars )
 import Type     ( classifyPredType, PredTree(..), getClassPredTys_maybe )
 import Class    ( Class )
 import Var
@@ -30,7 +32,6 @@ import Unique
 import VarSet
 import VarEnv 
 import TcEvidence
-import TypeRep
 import Name
 import Bag
 import ListSetOps
@@ -75,7 +76,13 @@ simplifyTop wanteds
     simpl_top :: WantedConstraints -> TcS WantedConstraints
     simpl_top wanteds
       = do { wc_first_go <- nestTcS (solve_wanteds_and_drop wanteds)
-           ; applyTyVarDefaulting wc_first_go 
+           ; free_tvs <- TcS.zonkTyVarsAndFV (tyVarsOfWC wc_first_go) 
+           ; let meta_tvs = filterVarSet isMetaTyVar free_tvs
+                   -- zonkTyVarsAndFV: the wc_first_go is not yet zonked
+                   -- filter isMetaTyVar: we might have runtime-skolems in GHCi, 
+                   -- and we definitely don't want to try to assign to those!
+
+           ; mapM_ defaultTyVar (varSetElems meta_tvs)   -- Has unification side effects
            ; simpl_top_loop wc_first_go }
     
     simpl_top_loop wc
@@ -130,7 +137,7 @@ go with option (i), implemented at SimplifyTop. Namely:
 Now, that has to do with class defaulting. However there exists type variable /kind/
 defaulting. Again this is done at the top-level and the plan is:
      - At the top-level, once you had a go at solving the constraint, do 
-       figure out /all/ the touchable unification variables of the wanted contraints.
+       figure out /all/ the touchable unification variables of the wanted constraints.
      - Apply defaulting to their kinds
 
 More details in Note [DefaultTyVar].
@@ -171,153 +178,12 @@ simplifyDefault theta
 \end{code}
 
 
-***********************************************************************************
-*                                                                                 * 
-*                            Deriving                                             *
-*                                                                                 *
-***********************************************************************************
-
-\begin{code}
-simplifyDeriv :: CtOrigin
-              -> PredType
-             -> [TyVar]        
-             -> ThetaType              -- Wanted
-             -> TcM ThetaType  -- Needed
--- Given  instance (wanted) => C inst_ty 
--- Simplify 'wanted' as much as possibles
--- Fail if not possible
-simplifyDeriv orig pred tvs theta 
-  = do { (skol_subst, tvs_skols) <- tcInstSkolTyVars tvs -- Skolemize
-               -- The constraint solving machinery 
-               -- expects *TcTyVars* not TyVars.  
-               -- We use *non-overlappable* (vanilla) skolems
-               -- See Note [Overlap and deriving]
-
-       ; let subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
-             skol_set   = mkVarSet tvs_skols
-            doc = ptext (sLit "deriving") <+> parens (ppr pred)
-
-       ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
-
-       ; traceTc "simplifyDeriv" $ 
-         vcat [ pprTvBndrs tvs $$ ppr theta $$ ppr wanted, doc ]
-       ; (residual_wanted, _ev_binds1)
-             <- solveWantedsTcM (mkFlatWC wanted)
-                -- Post: residual_wanted are already zonked
-
-       ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
-                         -- See Note [Exotic derived instance contexts]
-             get_good :: Ct -> Either PredType Ct
-             get_good ct | validDerivPred skol_set p 
-                         , isWantedCt ct  = Left p 
-                         -- NB: residual_wanted may contain unsolved
-                         -- Derived and we stick them into the bad set
-                         -- so that reportUnsolved may decide what to do with them
-                         | otherwise = Right ct
-                         where p = ctPred ct
-
-       -- We never want to defer these errors because they are errors in the
-       -- compiler! Hence the `False` below
-       ; reportAllUnsolved (residual_wanted { wc_flat = bad })
-
-       ; let min_theta = mkMinimalBySCs (bagToList good)
-       ; return (substTheta subst_skol min_theta) }
-\end{code}
-
-Note [Overlap and deriving]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider some overlapping instances:
-  data Show a => Show [a] where ..
-  data Show [Char] where ...
-
-Now a data type with deriving:
-  data T a = MkT [a] deriving( Show )
-
-We want to get the derived instance
-  instance Show [a] => Show (T a) where...
-and NOT
-  instance Show a => Show (T a) where...
-so that the (Show (T Char)) instance does the Right Thing
-
-It's very like the situation when we're inferring the type
-of a function
-   f x = show [x]
-and we want to infer
-   f :: Show [a] => a -> String
-
-BOTTOM LINE: use vanilla, non-overlappable skolems when inferring
-             the context for the derived instance. 
-            Hence tcInstSkolTyVars not tcInstSuperSkolTyVars
-
-Note [Exotic derived instance contexts]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In a 'derived' instance declaration, we *infer* the context.  It's a
-bit unclear what rules we should apply for this; the Haskell report is
-silent.  Obviously, constraints like (Eq a) are fine, but what about
-       data T f a = MkT (f a) deriving( Eq )
-where we'd get an Eq (f a) constraint.  That's probably fine too.
-
-One could go further: consider
-       data T a b c = MkT (Foo a b c) deriving( Eq )
-       instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
-
-Notice that this instance (just) satisfies the Paterson termination 
-conditions.  Then we *could* derive an instance decl like this:
-
-       instance (C Int a, Eq b, Eq c) => Eq (T a b c) 
-even though there is no instance for (C Int a), because there just
-*might* be an instance for, say, (C Int Bool) at a site where we
-need the equality instance for T's.  
-
-However, this seems pretty exotic, and it's quite tricky to allow
-this, and yet give sensible error messages in the (much more common)
-case where we really want that instance decl for C.
-
-So for now we simply require that the derived instance context
-should have only type-variable constraints.
-
-Here is another example:
-       data Fix f = In (f (Fix f)) deriving( Eq )
-Here, if we are prepared to allow -XUndecidableInstances we
-could derive the instance
-       instance Eq (f (Fix f)) => Eq (Fix f)
-but this is so delicate that I don't think it should happen inside
-'deriving'. If you want this, write it yourself!
-
-NB: if you want to lift this condition, make sure you still meet the
-termination conditions!  If not, the deriving mechanism generates
-larger and larger constraints.  Example:
-  data Succ a = S a
-  data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
-
-Note the lack of a Show instance for Succ.  First we'll generate
-  instance (Show (Succ a), Show a) => Show (Seq a)
-and then
-  instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
-and so on.  Instead we want to complain of no instance for (Show (Succ a)).
-
-The bottom line
-~~~~~~~~~~~~~~~
-Allow constraints which consist only of type variables, with no repeats.
-
 *********************************************************************************
 *                                                                                 * 
 *                            Inference
 *                                                                                 *
 ***********************************************************************************
 
-Note [Which variables to quantify]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose the inferred type of a function is
-   T kappa (alpha:kappa) -> Int
-where alpha is a type unification variable and 
-      kappa is a kind unification variable
-Then we want to quantify over *both* alpha and kappa.  But notice that
-kappa appears "at top level" of the type, as well as inside the kind
-of alpha.  So it should be fine to just look for the "top level"
-kind/type variables of the type, without looking transitively into the
-kinds of those type variables.
-
 \begin{code}
 simplifyInfer :: Bool
               -> Bool                  -- Apply monomorphism restriction
@@ -332,22 +198,14 @@ simplifyInfer :: Bool
                       TcEvBinds)    -- ... binding these evidence variables
 simplifyInfer _top_lvl apply_mr name_taus wanteds
   | isEmptyWC wanteds
-  = do { gbl_tvs     <- tcGetGlobalTyVars            -- Already zonked
-       ; zonked_taus <- zonkTcTypes (map snd name_taus)
-       ; let tvs_to_quantify = varSetElems (tyVarsOfTypes zonked_taus `minusVarSet` gbl_tvs)
-                                      -- tvs_to_quantify can contain both kind and type vars
-                                      -- See Note [Which variables to quantify]
-       ; qtvs <- zonkQuantifiedTyVars tvs_to_quantify
-       ; return (qtvs, [], False, emptyTcEvBinds) }
+  = do { gbl_tvs <- tcGetGlobalTyVars
+       ; qtkvs <- quantifyTyVars gbl_tvs (tyVarsOfTypes (map snd name_taus))
+       ; traceTc "simplifyInfer: emtpy WC" (ppr name_taus $$ ppr qtkvs) 
+       ; return (qtkvs, [], False, emptyTcEvBinds) }
 
   | otherwise
-  = do { zonked_tau_tvs <- zonkTyVarsAndFV (tyVarsOfTypes (map snd name_taus))
-
-       ; ev_binds_var <- newTcEvBinds
-       ; traceTc "simplifyInfer {"  $ vcat
-             [ ptext (sLit "names =") <+> ppr (map fst name_taus)
-             , ptext (sLit "taus =") <+> ppr (map snd name_taus)
-             , ptext (sLit "tau_tvs (zonked) =") <+> ppr zonked_tau_tvs
+  = do { traceTc "simplifyInfer {"  $ vcat
+             [ ptext (sLit "binds =") <+> ppr name_taus
              , ptext (sLit "closed =") <+> ppr _top_lvl
              , ptext (sLit "apply_mr =") <+> ppr apply_mr
              , ptext (sLit "(unzonked) wanted =") <+> ppr wanteds
@@ -367,6 +225,8 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
               -- calling solveWanteds will side-effect their evidence
               -- bindings, so we can't just revert to the input
               -- constraint.
+
+       ; ev_binds_var <- newTcEvBinds
        ; wanted_transformed <- solveWantedsTcMWithEvBinds ev_binds_var wanteds $
                                solve_wanteds_and_drop
                                -- Post: wanted_transformed are zonked
@@ -381,76 +241,74 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
               -- We discard bindings, insolubles etc, because all we are
               -- care aout it
 
-       ; (quant_pred_candidates, _extra_binds)   
-             <- if insolubleWC wanted_transformed 
-                then return ([], emptyBag)   -- See Note [Quantification with errors]
-                else runTcS $ 
-                do { let quant_candidates = approximateWC wanted_transformed
-                   ; traceTcS "simplifyWithApprox" $
-                     text "quant_candidates = " <+> ppr quant_candidates
-                   ; promoteTyVars quant_candidates
-                   ; _implics <- solveInteract quant_candidates
-                   ; (flats, _insols) <- getInertUnsolved
+       ; tc_lcl_env <- TcRnMonad.getLclEnv
+       ; let untch = tcl_untch tc_lcl_env
+       ; quant_pred_candidates   -- Fully zonked
+           <- if insolubleWC wanted_transformed 
+              then return []   -- See Note [Quantification with errors]
+              else do { gbl_tvs <- tcGetGlobalTyVars
+                      ; let quant_cand = approximateWC wanted_transformed
+                            meta_tvs   = filter isMetaTyVar (varSetElems (tyVarsOfCts quant_cand)) 
+                      ; ((flats, _insols), _extra_binds) <- runTcS $ 
+                        do { mapM_ (promoteAndDefaultTyVar untch gbl_tvs) meta_tvs
+                                 -- See Note [Promote _and_ default when inferring]
+                           ; _implics <- solveInteract quant_cand
+                           ; getInertUnsolved }
+                      ; return (map ctPred $ filter isWantedCt (bagToList flats)) }
                    -- NB: Dimitrios is slightly worried that we will get
                    -- family equalities (F Int ~ alpha) in the quantification
                    -- candidates, as we have performed no further unflattening
                    -- at this point. Nothing bad, but inferred contexts might
                    -- look complicated.
-                   ; return (map ctPred $ filter isWantedCt (bagToList flats)) }
 
-             -- NB: quant_pred_candidates is already the fixpoint of any 
-             --     unifications that may have happened
-                  
-       ; gbl_tvs        <- tcGetGlobalTyVars -- TODO: can we just use untch instead of gbl_tvs?
-       ; zonked_tau_tvs <- zonkTyVarsAndFV zonked_tau_tvs
-       
-       ; let init_tvs  = zonked_tau_tvs `minusVarSet` gbl_tvs
-             poly_qtvs = growThetaTyVars quant_pred_candidates init_tvs 
+       -- NB: quant_pred_candidates is already the fixpoint of any 
+       --     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
              
             -- Monomorphism restriction
-             mr_qtvs        = init_tvs `minusVarSet` constrained_tvs
-             constrained_tvs = tyVarsOfTypes quant_pred_candidates
+             constrained_tvs = tyVarsOfTypes pbound `unionVarSet` gbl_tvs
             mr_bites        = apply_mr && not (null pbound)
 
-             (qtvs, bound) | mr_bites  = (mr_qtvs,   [])
-                           | otherwise = (poly_qtvs, pbound)
+       ; (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) }
              
        ; traceTc "simplifyWithApprox" $
          vcat [ ptext (sLit "quant_pred_candidates =") <+> ppr quant_pred_candidates
               , ptext (sLit "gbl_tvs=") <+> ppr gbl_tvs
               , ptext (sLit "zonked_tau_tvs=") <+> ppr zonked_tau_tvs
               , ptext (sLit "pbound =") <+> ppr pbound
-              , ptext (sLit "init_qtvs =") <+> ppr init_tvs 
-              , ptext (sLit "poly_qtvs =") <+> ppr poly_qtvs ]
-
-       ; if isEmptyVarSet qtvs && null bound
-         then do { traceTc "} simplifyInfer/no quantification" empty                   
+              , ptext (sLit "bbound =") <+> 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                   
                  ; emitConstraints wanted_transformed
                     -- Includes insolubles (if -fdefer-type-errors)
                     -- as well as flats and implications
                  ; return ([], [], mr_bites, TcEvBinds ev_binds_var) }
          else do
 
-       { traceTc "simplifyApprox" $ 
-         ptext (sLit "bound are =") <+> ppr bound 
-         
-            -- Step 4, zonk quantified variables 
-       ; let minimal_flat_preds = mkMinimalBySCs bound
+      {     -- Step 7) Emit an implication
+         let minimal_flat_preds = mkMinimalBySCs bound
              skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
                                    | (name, ty) <- name_taus ]
                         -- Don't add the quantified variables here, because
                         -- they are also bound in ic_skols and we want them to be
                         -- tidied uniformly
 
-       ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
-
-            -- Step 7) Emit an implication
-       ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
-       ; lcl_env <- TcRnMonad.getLclEnv
-       ; let implic = Implic { ic_untch    = pushUntouchables (tcl_untch lcl_env)
-                             , ic_skols    = qtvs_to_return
+       ; minimal_bound_ev_vars <- mapM TcM.newEvVar minimal_flat_preds
+       ; let implic = Implic { ic_untch    = pushUntouchables untch
+                             , ic_skols    = qtvs
                              , ic_fsks     = []  -- wanted_tansformed arose only from solveWanteds
                                                  -- hence no flatten-skolems (which come from givens)
                              , ic_given    = minimal_bound_ev_vars
@@ -458,20 +316,53 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
                              , ic_insol    = False
                              , ic_binds    = ev_binds_var
                              , ic_info     = skol_info
-                             , ic_env      = lcl_env }
+                             , 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_to_return
+                  , ptext (sLit "qtvs =") <+> ppr qtvs
                   , ptext (sLit "spb =") <+> ppr quant_pred_candidates
                   , ptext (sLit "bound =") <+> ppr bound ]
 
-       ; return ( qtvs_to_return, minimal_bound_ev_vars
+       ; 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
 \end{code}
 
+Note [Inheriting implicit parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this:
+
+       f x = (x::Int) + ?y
+
+where f is *not* a top-level binding.
+From the RHS of f we'll get the constraint (?y::Int).
+There are two types we might infer for f:
+
+       f :: Int -> Int
+
+(so we get ?y from the context of f's definition), or
+
+       f :: (?y::Int) => Int -> Int
+
+At first you might think the first was better, because then
+?y behaves like a free variable of the definition, rather than
+having to be passed at each call site.  But of course, the WHOLE
+IDEA is that ?y should be passed at each call site (that's what
+dynamic binding means) so we'd better infer the second.
+
+BOTTOM LINE: when *inferring types* you must quantify over implicit
+parameters, *even if* they don't mention the bound type variables.
+Reason: because implicit parameters, uniquely, have local instance
+declarations. See the predicate quantifyPred.
+
 Note [Quantification with errors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If we find that the RHS of the definition has some absolutely-insoluble
@@ -548,7 +439,7 @@ situations like
 When inferring a type for 'g', we don't want to apply the
 instance decl, because then we can't satisfy (C t).  So we
 just notice that g isn't quantified over 't' and partition
-the contraints before simplifying.
+the constraints before simplifying.
 
 This only half-works, but then let-generalisation only half-works.
 
@@ -605,7 +496,8 @@ simplifyRule name lhs_wanted rhs_wanted
        ; traceTc "simplifyRule" $
          vcat [ ptext (sLit "LHS of rule") <+> doubleQuotes (ftext name)
               , text "zonked_lhs_flats" <+> ppr zonked_lhs_flats 
-              , text "q_cts"      <+> ppr q_cts ]
+              , text "q_cts"      <+> ppr q_cts
+              , text "non_q_cts"  <+> ppr non_q_cts ]
 
        ; return ( map (ctEvId . ctEvidence) (bagToList q_cts)
                 , lhs_wanted { wc_flat = non_q_cts }) }
@@ -652,7 +544,7 @@ to compile, and it will run fine unless we evaluate `a`. This is what
 
 It does this by keeping track of which errors correspond to which coercion
 in TcErrors (with ErrEnv). TcErrors.reportTidyWanteds does not print the errors
-and does not fail if -fwarn-type-errors is on, so that we can continue
+and does not fail if -fdefer-type-errors is on, so that we can continue
 compilation. The errors are turned into warnings in `reportUnsolved`.
 
 Note [Zonk after solving]
@@ -797,8 +689,7 @@ solveImplication inerts
                  , ic_wanted = wanteds
                  , ic_info   = info
                  , ic_env    = env })
-  = 
-    do { traceTcS "solveImplication {" (ppr imp) 
+  = do { traceTcS "solveImplication {" (ppr imp) 
 
          -- Solve the nested constraints
          -- NB: 'inerts' has empty inert_fsks
@@ -845,57 +736,82 @@ floatEqualities skols can_given wanteds@(WC { wc_flat = flats })
   = return (emptyBag, wanteds)   -- Note [Float Equalities out of Implications]
   | otherwise 
   = do { let (float_eqs, remaining_flats) = partitionBag is_floatable flats
-       ; promoteTyVars float_eqs
+       ; untch <- TcS.getUntouchables
+       ; mapM_ (promoteTyVar untch) (varSetElems (tyVarsOfCts float_eqs))
+             -- See Note [Promoting unification variables]
        ; ty_binds <- getTcSTyBindsMap
-       ; traceTcS "floatEqualities" (vcat [ text "Floated eqs =" <+> ppr float_eqs
+       ; traceTcS "floatEqualities" (vcat [ text "Flats =" <+> ppr flats
+                                          , text "Floated eqs =" <+> ppr float_eqs
                                           , text "Ty binds =" <+> ppr ty_binds])
        ; return (float_eqs, wanteds { wc_flat = remaining_flats }) }
   where 
-    skol_set = growSkols wanteds (mkVarSet skols)
+      -- See Note [Float equalities from under a skolem binding]
+    skol_set = fixVarSet mk_next (mkVarSet skols)
+    mk_next tvs = foldrBag grow_one tvs flats
+    grow_one (CFunEqCan { cc_tyargs = xis, cc_rhs = rhs }) tvs
+       | intersectsVarSet tvs (tyVarsOfTypes xis) 
+       = tvs `unionVarSet` tyVarsOfType rhs
+    grow_one _ tvs = tvs
 
     is_floatable :: Ct -> Bool
-    is_floatable ct
-       = isEqPred pred && skol_set `disjointVarSet` tyVarsOfType pred
+    is_floatable ct = isEqPred pred && skol_set `disjointVarSet` tyVarsOfType pred
        where
          pred = ctPred ct
 
-promoteTyVars :: Cts -> TcS ()
--- When we float a constraint out of an implication we
--- must restore (MetaTvInv) in Note [Untouchable type variables]
--- in TcType
-promoteTyVars cts
-  = do { untch <- TcSMonad.getUntouchables
-       ; mapM_ (promote_tv untch) (varSetElems (tyVarsOfCts cts)) }
-  where
-    promote_tv untch tv 
-      | isFloatedTouchableMetaTyVar untch tv
-      = do { cloned_tv <- TcSMonad.cloneMetaTyVar tv
-           ; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch
-           ; setWantedTyBind tv (mkTyVarTy rhs_tv) }
-      | otherwise
-      = return ()
-
-growSkols :: WantedConstraints -> VarSet -> VarSet
--- Find all the type variables that might possibly be unified
--- with a type that mentions a skolem.  This test is very conservative.
--- I don't *think* we need look inside the implications, because any 
--- relevant unification variables in there are untouchable.
-growSkols (WC { wc_flat = flats }) skols
-  = growThetaTyVars theta skols
+promoteTyVar :: Untouchables -> TcTyVar  -> TcS ()
+-- When we float a constraint out of an implication we must restore
+-- invariant (MetaTvInv) in Note [Untouchable type variables] in TcType
+-- See Note [Promoting unification variables]
+promoteTyVar untch tv 
+  | isFloatedTouchableMetaTyVar untch tv
+  = do { cloned_tv <- TcS.cloneMetaTyVar tv
+       ; let rhs_tv = setMetaTyVarUntouchables cloned_tv untch
+       ; setWantedTyBind tv (mkTyVarTy rhs_tv) }
+  | otherwise
+  = return ()
+
+promoteAndDefaultTyVar :: Untouchables -> TcTyVarSet -> TyVar -> TcS ()
+-- See Note [Promote _and_ default when inferring]
+promoteAndDefaultTyVar untch gbl_tvs tv
+  = do { tv1 <- if tv `elemVarSet` gbl_tvs 
+                then return tv
+                else defaultTyVar tv
+       ; promoteTyVar untch tv1 }
+
+defaultTyVar :: TcTyVar -> TcS TcTyVar
+-- Precondition: MetaTyVars only
+-- See Note [DefaultTyVar]
+defaultTyVar the_tv
+  | not (k `eqKind` default_k)
+  = do { tv' <- TcS.cloneMetaTyVar the_tv
+       ; let new_tv = setTyVarKind tv' default_k
+       ; traceTcS "defaultTyVar" (ppr the_tv <+> ppr new_tv)
+       ; setWantedTyBind the_tv (mkTyVarTy new_tv)
+       ; return new_tv }
+             -- Why not directly derived_pred = mkTcEqPred k default_k?
+             -- See Note [DefaultTyVar]
+             -- We keep the same Untouchables on tv'
+
+  | otherwise = return the_tv   -- The common case
   where
-    theta = foldrBag ((:) . ctPred) [] flats
+    k = tyVarKind the_tv
+    default_k = defaultKind k
 
 approximateWC :: WantedConstraints -> Cts
 -- Postcondition: Wanted or Derived Cts 
-approximateWC wc = float_wc emptyVarSet wc
+approximateWC wc 
+  = float_wc emptyVarSet wc
   where 
     float_wc :: TcTyVarSet -> WantedConstraints -> Cts
-    float_wc skols (WC { wc_flat = flat, wc_impl = implic }) = floats1 `unionBags` floats2
-      where floats1 = do_bag (float_flat skols) flat
-            floats2 = do_bag (float_implic skols) implic
+    float_wc skols (WC { wc_flat = flats, wc_impl = implics }) 
+      = do_bag (float_flat skols)   flats  `unionBags` 
+        do_bag (float_implic skols) implics
                                  
     float_implic :: TcTyVarSet -> Implication -> Cts
     float_implic skols imp
+      | hasEqualities (ic_given imp)  -- Don't float out of equalities
+      = emptyCts                      -- cf floatEqualities
+      | otherwise                     -- See Note [approximateWC]
       = float_wc skols' (ic_wanted imp)
       where
         skols' = skols `extendVarSetList` ic_skols imp `extendVarSetList` ic_fsks imp
@@ -910,6 +826,77 @@ approximateWC wc = float_wc emptyVarSet wc
     do_bag f = foldrBag (unionBags.f) emptyBag
 \end{code}
 
+Note [ApproximateWC]
+~~~~~~~~~~~~~~~~~~~~
+approximateWC takes a constraint, typically arising from the RHS of a
+let-binding whose type we are *inferring*, and extracts from it some
+*flat* constraints that we might plausibly abstract over.  Of course
+the top-level flat constraints are plausible, but we also float constraints
+out from inside, if the are not captured by skolems.
+
+However we do *not* float anything out if the implication binds equality
+constriants, because that defeats the OutsideIn story.  Consider
+   data T a where
+     TInt :: T Int
+     MkT :: T a
+
+   f TInt = 3::Int
+
+We get the implication (a ~ Int => res ~ Int), where so far we've decided 
+  f :: T a -> res
+We don't want to float (res~Int) out because then we'll infer  
+  f :: T a -> Int
+which is only on of the possible types. (GHC 7.6 accidentally *did*
+float out of such implications, which meant it would happily infer
+non-principal types.)
+
+Note [DefaultTyVar]
+~~~~~~~~~~~~~~~~~~~
+defaultTyVar is used on any un-instantiated meta type variables to
+default the kind of OpenKind and ArgKind etc to *.  This is important 
+to ensure that instance declarations match.  For example consider
+
+     instance Show (a->b)
+     foo x = show (\_ -> True)
+
+Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,
+and that won't match the typeKind (*) in the instance decl.  See tests
+tc217 and tc175.
+
+We look only at touchable type variables. No further constraints
+are going to affect these type variables, so it's time to do it by
+hand.  However we aren't ready to default them fully to () or
+whatever, because the type-class defaulting rules have yet to run.
+
+An important point is that if the type variable tv has kind k and the
+default is default_k we do not simply generate [D] (k ~ default_k) because:
+
+   (1) k may be ArgKind and default_k may be * so we will fail
+
+   (2) We need to rewrite all occurrences of the tv to be a type
+       variable with the right kind and we choose to do this by rewriting 
+       the type variable /itself/ by a new variable which does have the 
+       right kind.
+
+Note [Promote _and_ default when inferring]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we are inferring a type, we simplify the constraint, and then use
+approximateWC to produce a list of candidate constraints.  Then we MUST
+
+  a) Promote any meta-tyvars that have been floated out by 
+     approximateWC, to restore invariant (MetaTvInv) described in 
+     Note [Untouchable type variables] in TcType.
+
+  b) Default the kind of any meta-tyyvars that are not mentioned in
+     in the environment.
+
+To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
+have an instance (C ((x:*) -> Int)).  The instance doesn't match -- but it
+should!  If we don't solve the constraint, we'll stupidly quantify over 
+(C (a->Int)) and, worse, in doing so zonkQuantifiedTyVar will quantify over
+(b:*) instead of (a:OpenKind), which can lead to disaster; see Trac #7332.
+Trac #7641 is a simpler example.
+
 Note [Float Equalities out of Implications]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
 For ordinary pattern matches (including existentials) we float 
@@ -955,6 +942,49 @@ Consequence: classes with functional dependencies don't matter (since there is
 no evidence for a fundep equality), but equality superclasses do matter (since 
 they carry evidence).
 
+Note [Float equalities from under a skolem binding]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+You might worry about skolem escape with all this floating.
+For example, consider
+    [2] forall a. (a ~ F beta[2] delta, 
+                   Maybe beta[2] ~ gamma[1])
+
+The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and
+solve with gamma := beta. But what if later delta:=Int, and 
+  F b Int = b.  
+Then we'd get a ~ beta[2], and solve to get beta:=a, and now the
+skolem has escaped!
+
+But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2]
+to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be.
+
+Previously we tried to "grow" the skol_set with the constraints, to get
+all the tyvars that could *conceivably* unify with the skolems, but that
+was far too conservative (Trac #7804). Example: this should be fine:
+    f :: (forall a. a -> Proxy x -> Proxy (F x)) -> Int
+    f = error "Urk" :: (forall a. a -> Proxy x -> Proxy (F x)) -> Int
+
+BUT (sigh) we have to be careful.  Here are some edge cases:
+
+a)    [2]forall a. (F a delta[1] ~ beta[2],   delta[1] ~ Maybe beta[2])
+b)    [2]forall a. (F b ty ~ beta[2],         G beta[2] ~ gamma[2])
+c)    [2]forall a. (F a ty ~ beta[2],         delta[1] ~ Maybe beta[2])
+
+In (a) we *must* float out the second equality, 
+       else we can't solve at all (Trac #7804).
+
+In (b) we *must not* float out the second equality.  
+       It will ultimately be solved (by flattening) in situ, but if we
+       float it we'll promote beta,gamma, and render the first equality insoluble.
+
+In (c) it would be OK to float the second equality but better not to.
+       If we flatten we see (delta[1] ~ Maybe (F a ty)), which is a 
+       skolem-escape problem.  If we float the secodn equality we'll 
+       end up with (F a ty ~ beta'[1]), which is a less explicable error.
+
+Hence we start with the skolems, grow them by the CFunEqCans, and
+float ones that don't mention the grown variables.  Seems very ad hoc.
+
 Note [Promoting unification variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When we float an equality out of an implication we must "promote" free
@@ -1028,6 +1058,7 @@ in TcMType.
 *                          Defaulting and disamgiguation                        *
 *                                                                               *
 *********************************************************************************
+
 \begin{code}
 applyDefaultingRules :: Cts -> TcS Bool
   -- True <=> I did some defaulting, reflected in ty_binds
@@ -1052,85 +1083,7 @@ applyDefaultingRules wanteds
        ; return (or something_happeneds) }
 \end{code}
 
-Note [tryTcS in defaulting]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-defaultTyVar and disambigGroup create new evidence variables for
-default equations, and hence update the EvVar cache. However, after
-applyDefaultingRules we will try to solve these default equations
-using solveInteractCts, which will consult the cache and solve those
-EvVars from themselves! That's wrong.
-
-To avoid this problem we guard defaulting under a @tryTcS@ which leaves
-the original cache unmodified.
-
-There is a second reason for @tryTcS@ in defaulting: disambGroup does
-some constraint solving to determine if a default equation is
-``useful'' in solving some wanted constraints, but we want to
-discharge all evidence and unifications that may have happened during
-this constraint solving.
-
-Finally, @tryTcS@ importantly does not inherit the original cache from
-the higher level but makes up a new cache, the reason is that disambigGroup
-will call solveInteractCts so the new derived and the wanteds must not be 
-in the cache!
-
-
-\begin{code}
-applyTyVarDefaulting :: WantedConstraints -> TcS ()
-applyTyVarDefaulting wc 
-  = do { let tvs = filter isMetaTyVar (varSetElems (tyVarsOfWC wc))
-                   -- tyVarsOfWC: post-simplification the WC should reflect
-                   --             all unifications that have happened
-                   -- filter isMetaTyVar: we might have runtime-skolems in GHCi, 
-                   -- and we definitely don't want to try to assign to those!
-
-       ; traceTcS "applyTyVarDefaulting {" (ppr tvs)
-       ; mapM_ defaultTyVar tvs
-       ; traceTcS "applyTyVarDefaulting end }" empty }
-
-defaultTyVar :: TcTyVar -> TcS ()
-defaultTyVar the_tv
-  | not (k `eqKind` default_k)
-  = do { tv' <- TcSMonad.cloneMetaTyVar the_tv
-       ; let rhs_ty = mkTyVarTy (setTyVarKind tv' default_k)
-       ; setWantedTyBind the_tv rhs_ty }
-             -- Why not directly derived_pred = mkTcEqPred k default_k?
-             -- See Note [DefaultTyVar]
-             -- We keep the same Untouchables on tv'
-
-  | otherwise = return ()       -- The common case
-  where
-    k = tyVarKind the_tv
-    default_k = defaultKind k
-\end{code}
-
-Note [DefaultTyVar]
-~~~~~~~~~~~~~~~~~~~
-defaultTyVar is used on any un-instantiated meta type variables to
-default the kind of OpenKind and ArgKind etc to *.  This is important 
-to ensure that instance declarations match.  For example consider
-
-     instance Show (a->b)
-     foo x = show (\_ -> True)
-
-Then we'll get a constraint (Show (p ->q)) where p has kind ArgKind,
-and that won't match the typeKind (*) in the instance decl.  See tests
-tc217 and tc175.
-
-We look only at touchable type variables. No further constraints
-are going to affect these type variables, so it's time to do it by
-hand.  However we aren't ready to default them fully to () or
-whatever, because the type-class defaulting rules have yet to run.
-
-An important point is that if the type variable tv has kind k and the
-default is default_k we do not simply generate [D] (k ~ default_k) because:
-
-   (1) k may be ArgKind and default_k may be * so we will fail
 
-   (2) We need to rewrite all occurrences of the tv to be a type
-       variable with the right kind and we choose to do this by rewriting 
-       the type variable /itself/ by a new variable which does have the 
-       right kind.
 
 \begin{code}
 findDefaultableGroups 
@@ -1192,29 +1145,26 @@ disambigGroup :: [Type]                  -- The default types
 disambigGroup []  _grp
   = return False
 disambigGroup (default_ty:default_tys) group
-  = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
-       ; success <- tryTcS $ -- Why tryTcS? See Note [tryTcS in defaulting]
+  = do { traceTcS "disambigGroup {" (ppr group $$ ppr default_ty)
+       ; success <- tryTcS $ -- Why tryTcS? If this attempt fails, we want to 
+                             -- discard all side effects from the attempt
                     do { setWantedTyBind the_tv default_ty
-                       ; traceTcS "disambigGroup (solving) {" $
-                         text "trying to solve constraints along with default equations ..."
                        ; implics_from_defaulting <- solveInteract wanteds
                        ; MASSERT (isEmptyBag implics_from_defaulting)
                            -- I am not certain if any implications can be generated
                            -- but I am letting this fail aggressively if this ever happens.
                                      
-                       ; all_solved <- checkAllSolved
-                       ; traceTcS "disambigGroup (solving) }" $
-                         text "disambigGroup solved =" <+> ppr all_solved
-                       ; return all_solved }
+                       ; checkAllSolved }
+
        ; if success then
              -- Success: record the type variable binding, and return
              do { setWantedTyBind the_tv default_ty
                 ; wrapWarnTcS $ warnDefaulting wanteds default_ty
-                ; traceTcS "disambigGroup succeeded" (ppr default_ty)
+                ; traceTcS "disambigGroup succeeded }" (ppr default_ty)
                 ; return True }
          else
              -- Failure: try with the next type
-             do { traceTcS "disambigGroup failed, will try other default types"
+             do { traceTcS "disambigGroup failed, will try other default types }"
                            (ppr default_ty)
                 ; disambigGroup default_tys group } }
   where
@@ -1235,23 +1185,3 @@ dealing with the (Num a) context arising from f's definition;
 we try to unify a with Int (to default it), but find that it's
 already been unified with the rigid variable from g's type sig
 
-
-
-*********************************************************************************
-*                                                                               * 
-*                   Utility functions
-*                                                                               *
-*********************************************************************************
-
-\begin{code}
-newFlatWanteds :: CtOrigin -> ThetaType -> TcM [Ct]
-newFlatWanteds orig theta
-  = do { loc <- getCtLoc orig
-       ; mapM (inst_to_wanted loc) theta }
-  where 
-    inst_to_wanted loc pty 
-          = do { v <- TcMType.newWantedEvVar pty 
-               ; return $ mkNonCanonical loc $
-                 CtWanted { ctev_evar = v
-                          , ctev_pred = pty } }
-\end{code}