Recover after an error in an implication constraint
[ghc-hetmet.git] / compiler / typecheck / TcSimplify.lhs
index d8be2d1..bb76c1d 100644 (file)
@@ -18,6 +18,8 @@ import TcInteract
 import Inst
 import Var
 import VarSet
+import VarEnv ( varEnvElts ) 
+
 import Name
 import NameEnv ( emptyNameEnv )
 import Bag
@@ -198,26 +200,50 @@ simplifyInfer apply_mr tau_tvs wanted
              , ptext (sLit "tau_tvs =") <+> ppr tau_tvs
              ]
 
-       ; (simple_wanted, tc_binds) 
-              <- simplifyAsMuchAsPossible SimplInfer zonked_wanted
+            -- Make a guess at the quantified type variables
+            -- Then split the constraints on the baisis of those tyvars
+            -- to avoid unnecessarily simplifying a class constraint
+            -- See Note [Avoid unecessary constraint simplification]
+       ; gbl_tvs <- tcGetGlobalTyVars
+       ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
+       ; let proto_qtvs = growWanteds gbl_tvs zonked_wanted $
+                          zonked_tau_tvs `minusVarSet` gbl_tvs
+             (perhaps_bound, surely_free) 
+                  = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted
+      
+       ; emitConstraints surely_free
+       ; traceTc "sinf"  $ vcat
+             [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
+             , ptext (sLit "surely_free   =") <+> ppr surely_free
+             ]
+
+                     -- Now simplify the possibly-bound constraints
+       ; (simplified_perhaps_bound, tc_binds) 
+              <- simplifyAsMuchAsPossible SimplInfer perhaps_bound
 
+             -- Sigh: must re-zonk because because simplifyAsMuchAsPossible
+             --       may have done some unification
        ; gbl_tvs <- tcGetGlobalTyVars
        ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
-       ; zonked_simples <- mapBagM zonkWantedEvVar simple_wanted
-       ; let qtvs = findQuantifiedTyVars apply_mr zonked_simples zonked_tau_tvs gbl_tvs
-             (bound, free) | apply_mr  = (emptyBag, zonked_simples)
-                           | otherwise = partitionBag (quantifyMe qtvs) zonked_simples
+       ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound
+       ; let init_tvs       = zonked_tau_tvs `minusVarSet` gbl_tvs
+             mr_qtvs        = init_tvs `minusVarSet` constrained_tvs
+             constrained_tvs = tyVarsOfWantedEvVars zonked_simples
+             qtvs            = growWantedEVs gbl_tvs zonked_simples init_tvs
+             (final_qtvs, (bound, free))
+                | apply_mr  = (mr_qtvs, (emptyBag, zonked_simples))
+                | otherwise = (qtvs,    partitionBag (quantifyMe qtvs) zonked_simples)
 
        ; traceTc "end simplifyInfer }" $
               vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
                    , text "wanted = " <+> ppr zonked_wanted
-                   , text "qtvs =   " <+> ppr qtvs
+                   , text "qtvs =   " <+> ppr final_qtvs
                    , text "free =   " <+> ppr free
                    , text "bound =  " <+> ppr bound ]
 
        -- Turn the quantified meta-type variables into real type variables 
        ; emitConstraints (mapBag WcEvVar free)
-       ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs) 
+       ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs) 
        ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
        ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
 
@@ -227,7 +253,7 @@ simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
 -- We use this function when inferring the type of a function
 -- The wanted constraints are already zonked
 simplifyAsMuchAsPossible ctxt wanteds
-  = do { let untch = emptyVarSet
+  = do { let untch = NoUntouchables
                 -- We allow ourselves to unify environment 
                 -- variables; hence *no untouchables*
 
@@ -308,25 +334,29 @@ approximateImplications impls
 \end{code}
 
 \begin{code}
-findQuantifiedTyVars :: Bool           -- Apply the MR
-                     -> Bag WantedEvVar        -- Simplified constraints from RHS
-                     -> TyVarSet       -- Free in tau-type of definition
-                     -> TyVarSet       -- Free in the envt
-                    -> TyVarSet        -- Quantify over these
-
-findQuantifiedTyVars apply_mr wanteds tau_tvs gbl_tvs
-  | isEmptyBag wanteds = init_tvs
-  | apply_mr           = init_tvs `minusVarSet` constrained_tvs
-  | otherwise          = fixVarSet mk_next init_tvs
+growWantedEVs :: TyVarSet -> Bag WantedEvVar      -> TyVarSet -> TyVarSet
+growWanteds   :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet
+growWanteds   gbl_tvs ws tvs
+  | isEmptyBag ws = tvs
+  | otherwise     = fixVarSet (\tvs -> foldrBag (growWanted   gbl_tvs) tvs ws) tvs
+growWantedEVs gbl_tvs ws tvs 
+  | isEmptyBag ws = tvs
+  | otherwise     = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs
+
+growWantedEV :: TyVarSet -> WantedEvVar      -> TyVarSet -> TyVarSet
+growWanted   :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet
+-- (growX gbls wanted tvs) grows a seed 'tvs' against the 
+-- X-constraint 'wanted', nuking the 'gbls' at each stage
+growWantedEV gbl_tvs wev tvs
+  = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs)
   where
-    init_tvs    = tau_tvs `minusVarSet` gbl_tvs
-    mk_next tvs = foldrBag grow_one tvs wanteds
+    ev_tvs = growPredTyVars (wantedEvVarPred wev) tvs
 
-    grow_one wev tvs = tvs `unionVarSet` (extra_tvs `minusVarSet` gbl_tvs)
-       where
-         extra_tvs = growPredTyVars (wantedEvVarPred wev) tvs
-
-    constrained_tvs = tyVarsOfWantedEvVars wanteds
+growWanted gbl_tvs (WcEvVar wev) tvs
+  = growWantedEV gbl_tvs wev tvs
+growWanted gbl_tvs (WcImplic implic) tvs
+  = foldrBag (growWanted (gbl_tvs `unionVarSet` ic_skols implic)) 
+             tvs (ic_wanted implic)
 
 --------------------
 quantifyMe :: TyVarSet      -- Quantifying over these
@@ -337,8 +367,32 @@ quantifyMe qtvs wev
   | otherwise    = tyVarsOfPred pred `intersectsVarSet` qtvs
   where
     pred = wantedEvVarPred wev
+
+quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
+quantifyMeWC qtvs (WcImplic implic)
+  = anyBag (quantifyMeWC (qtvs `minusVarSet` ic_skols implic)) (ic_wanted implic)
+quantifyMeWC qtvs (WcEvVar wev)
+  = quantifyMe qtvs wev
 \end{code}
 
+Note [Avoid unecessary constraint simplification]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When inferring the type of a let-binding, with simplifyInfer,
+try to avoid unnecessariliy simplifying class constraints.
+Doing so aids sharing, but it also helps with delicate 
+situations like
+   instance C t => C [t] where ..
+   f :: C [t] => ....
+   f x = let g y = ...(constraint C [t])... 
+         in ...
+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.
+
+This only half-works, but then let-generalisation only half-works.
+
+
 Note [Inheriting implicit parameters]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this:
@@ -403,9 +457,9 @@ simplifySuperClass self wanteds
   = do { wanteds <- mapBagM zonkWanted wanteds
        ; loc <- getCtLoc NoScSkol
        ; (unsolved, ev_binds) 
-             <- runTcS SimplCheck emptyVarSet $
+             <- runTcS SimplCheck NoUntouchables $
                do { can_self <- canGivens loc [self]
-                  ; let inert = foldlBag extendInertSet emptyInert can_self
+                  ; let inert = foldlBag updInertSet emptyInert can_self
                     -- No need for solveInteract; we know it's inert
 
                   ; solveWanteds inert wanteds }
@@ -512,7 +566,7 @@ simplifyRule name tv_bndrs lhs_wanted rhs_wanted
        ; rhs_binds_var@(EvBindsVar evb_ref _)  <- newTcEvBinds
        ; loc        <- getCtLoc (RuleSkol name)
        ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $ 
-             Implic { ic_untch = emptyVarSet     -- No untouchables
+             Implic { ic_untch = NoUntouchables
                    , ic_env = emptyNameEnv
                    , ic_skols = mkVarSet tv_bndrs
                    , ic_scoped = panic "emitImplication"
@@ -556,7 +610,7 @@ simplifyCheck ctxt wanteds
        ; traceTc "simplifyCheck {" (vcat
              [ ptext (sLit "wanted =") <+> ppr wanteds ])
 
-       ; (unsolved, ev_binds) <- runTcS ctxt emptyVarSet $
+       ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
                                  solveWanteds emptyInert wanteds
 
        ; traceTc "simplifyCheck }" $
@@ -581,10 +635,13 @@ solveWanteds inert wanteds
                       , text "inert =" <+> ppr inert ]
        ; (unsolved_flats, unsolved_implics) 
                <- simpl_loop 1 can_flats implic_wanteds
+       ; bb <- getTcEvBindsBag 
        ; traceTcS "solveWanteds }" $
                  vcat [ text "wanteds =" <+> ppr wanteds
                       , text "unsolved_flats =" <+> ppr unsolved_flats
-                      , text "unsolved_implics =" <+> ppr unsolved_implics ]
+                      , text "unsolved_implics =" <+> ppr unsolved_implics 
+                      , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
+                      ] 
        ; return (unsolved_flats, unsolved_implics)  }
   where
     simpl_loop :: Int 
@@ -649,6 +706,10 @@ solveImplication inert
                  , ic_wanted = wanteds
                  , ic_loc    = loc })
   = nestImplicTcS ev_binds untch $
+    recoverTcS (return (emptyBag, emptyBag)) $
+       -- Recover from nested failures.  Even the top level is
+       -- just a bunch of implications, so failing at the first
+       -- one is bad
     do { traceTcS "solveImplication {" (ppr imp) 
 
          -- Solve flat givens
@@ -753,13 +814,13 @@ applyDefaultingRules inert wanteds
   | isEmptyBag wanteds 
   = return emptyBag
   | otherwise
-  = do { untch <- getUntouchablesTcS
+  = do { untch <- getUntouchables
        ; tv_cts <- mapM (defaultTyVar untch) $
-                   varSetElems (tyVarsOfCanonicals wanteds)
+                   varSetElems (tyVarsOfCDicts wanteds) 
 
        ; info@(_, default_tys, _) <- getDefaultInfo
        ; let groups = findDefaultableGroups info untch wanteds
-       ; deflt_cts <- mapM (disambigGroup default_tys untch inert) groups
+       ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
 
        ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
                                  , text "Type defaults =" <+> ppr deflt_cts])
@@ -767,7 +828,7 @@ applyDefaultingRules inert wanteds
        ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) }
 
 ------------------
-defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts
+defaultTyVar :: Untouchables -> TcTyVar -> TcS CanonicalCts
 -- defaultTyVar is used on any un-instantiated meta type variables to
 -- default the kind of ? and ?? etc to *.  This is important to ensure
 -- that instance declarations match.  For example consider
@@ -783,10 +844,9 @@ defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts
 -- whatever, because the type-class defaulting rules have yet to run.
 
 defaultTyVar untch the_tv 
-  | isMetaTyVar the_tv
-  , not (the_tv `elemVarSet` untch)
+  | isTouchableMetaTyVar_InRange untch the_tv
   , not (k `eqKind` default_k)
-  = do { (ev, better_ty) <- TcSMonad.newKindConstraint (mkTyVarTy the_tv) default_k
+  = do { (ev, better_ty) <- TcSMonad.newKindConstraint the_tv default_k
        ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
                           -- 'DefaultOrigin' is strictly the declaration, but it's convenient
              wanted_eq  = CTyEqCan { cc_id     = ev
@@ -807,7 +867,7 @@ findDefaultableGroups
     :: ( SimplContext 
        , [Type]
        , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
-    -> TcTyVarSet      -- Untouchable
+    -> Untouchables    -- Untouchable
     -> CanonicalCts    -- Unsolved
     -> [[(CanonicalCt,TcTyVar)]]
 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) 
@@ -834,7 +894,7 @@ findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
     is_defaultable_group ds@((_,tv):_)
         = isTyConableTyVar tv  -- Note [Avoiding spurious errors]
         && not (tv `elemVarSet` bad_tvs)
-        && not (tv `elemVarSet` untch)    -- Non untouchable
+        && isTouchableMetaTyVar_InRange untch tv 
         && defaultable_classes [cc_class cc | (cc,_) <- ds]
     is_defaultable_group [] = panic "defaultable_group"
 
@@ -856,15 +916,14 @@ findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
 
 ------------------------------
 disambigGroup :: [Type]                    -- The default types 
-             -> TcTyVarSet                -- Untouchables
               -> InertSet                  -- Given inert 
               -> [(CanonicalCt, TcTyVar)]  -- All classes of the form (C a)
                                           --  sharing same type variable
               -> TcS CanonicalCts
 
-disambigGroup [] _inert _untch _grp 
+disambigGroup [] _inert _grp 
   = return emptyBag
-disambigGroup (default_ty:default_tys) untch inert group
+disambigGroup (default_ty:default_tys) inert group
   = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
        ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl 
                         -- We know this equality is canonical,
@@ -874,7 +933,7 @@ disambigGroup (default_ty:default_tys) untch inert group
                                         , cc_tyvar  = the_tv
                                 , cc_rhs    = default_ty }
 
-       ; success <- tryTcS (extendVarSet untch the_tv) $ 
+       ; success <- tryTcS $ 
                    do { given_inert <- solveOne inert given_eq
                       ; final_inert <- solveInteract given_inert (listToBag wanteds)
                       ; let (_, unsolved) = extractUnsolved final_inert
@@ -888,7 +947,7 @@ disambigGroup (default_ty:default_tys) untch inert group
                        ; return (unitBag given_eq) }
            False ->    -- Failure: try with the next type
                    do { traceTcS "disambigGoup succeeded" (ppr default_ty)
-                       ; disambigGroup default_tys untch inert group } }
+                       ; disambigGroup default_tys inert group } }
   where
     ((the_ct,the_tv):_) = group
     wanteds = map fst group