Simplify simplifyInfer quite a lot

Work in progress, on branch

compiler/typecheck/TcMType.lhs

@@ -1212,7 +1212,7 @@ check_pred_ty' dflags ctxt (ClassPred cls tys)
 
 		-- Check the form of the argument types
        ; mapM_ checkValidMonoType tys
-       ; checkTc (check_class_pred_tys dflags ctxt tys)
+       ; checkTc (check_class_pred_tys dflags ctxt cls tys)
 		 (predTyVarErr (mkClassPred cls tys) $$ how_to_allow)
        }
   where
@@ -1285,16 +1285,15 @@ check_pred_ty' dflags ctxt (IrredPred pred)
                      (predIrredBadCtxtErr pred)
 
 -------------------------
-check_class_pred_tys :: DynFlags -> UserTypeCtxt -> [KindOrType] -> Bool
-check_class_pred_tys dflags ctxt kts
+check_class_pred_tys :: DynFlags -> UserTypeCtxt -> Class -> [KindOrType] -> Bool
+check_class_pred_tys dflags ctxt cls kts
   = case ctxt of
 	SpecInstCtxt -> True	-- {-# SPECIALISE instance Eq (T Int) #-} is fine
-	InstDeclCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
+	InstDeclCtxt -> flexible_contexts || undecidable_ok || isTyVarClassApp cls kts
 				-- Further checks on head and theta in
 				-- checkInstTermination
-	_             -> flexible_contexts || all tyvar_head tys
+	_             -> flexible_contexts || isTyVarHeadClassApp cls kts
   where
-    (_, tys) = span isKind kts  -- see Note [Kind polymorphic type classes]
     flexible_contexts = xopt Opt_FlexibleContexts dflags
     undecidable_ok = xopt Opt_UndecidableInstances dflags
 
@@ -1309,7 +1308,6 @@ class C f where
 
 MultiParam:
 ~~~~~~~~~~~
-
 instance C Maybe where
   empty = Nothing
 
@@ -1318,7 +1316,6 @@ type class.
 
 Flexible:
 ~~~~~~~~~
-
 data D a = D
 -- D :: forall k. k -> *
 
@@ -1329,15 +1326,6 @@ The dictionary gets type [C * (D *)]. IA0_TODO it should be
 generalized actually.
 
 -}
-
--------------------------
-tyvar_head :: Type -> Bool
-tyvar_head ty			-- Haskell 98 allows predicates of form 
-  | tcIsTyVarTy ty = True	-- 	C (a ty1 .. tyn)
-  | otherwise			-- where a is a type variable
-  = case tcSplitAppTy_maybe ty of
-	Just (ty, _) -> tyvar_head ty
-	Nothing	     -> False
 \end{code}
 
 Check for ambiguity
@@ -1504,10 +1492,14 @@ checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()
 checkValidInstHead ctxt clas cls_args
   = do { dflags <- getDynFlags
 
-           -- Check language restrictions; 
-           -- but not for SPECIALISE isntance pragmas
-       ; let ty_args = dropWhile isKind cls_args
-       ; unless spec_inst_prag $
+       ; let ty_args = classTyArgs clas cls_args
+              --     class C f where { empty :: f a }
+              --     instance C Maybe where ...
+              -- So C :: forall k. k -> Constraint
+              -- The dictionary gets type [C * Maybe] which is ok even if it's 
+              -- not a MultiParam type class.
+
+       ; unless spec_inst_prag $  -- Not for SPECIALISE instance pragmas
          do { checkTc (xopt Opt_TypeSynonymInstances dflags ||
                        all tcInstHeadTyNotSynonym ty_args)
                  (instTypeErr pp_pred head_type_synonym_msg)

compiler/typecheck/TcSimplify.lhs

 \begin{code}
-{-# OPTIONS -fno-warn-tabs #-}
+{-# OPTIONS -fno-warn-tabs -Wwarn #-}
 -- The above warning supression flag is a temporary kludge.
 -- While working on this module you are encouraged to remove it and
 -- detab the module (please do the detabbing in a separate patch). See
@@ -20,9 +20,10 @@ import TcMType
 import TcType 
 import TcSMonad 
 import TcInteract 
+import InstEnv  ( lookupInstEnv )
 import Inst
 import Unify	( niFixTvSubst, niSubstTvSet )
-import Type     ( classifyPredType, PredTree(..) )
+import Type     ( classifyPredType, getClassPredTys, getClassPredTys_maybe, PredTree(..) )
 import Var
 import VarSet
 import VarEnv 
@@ -42,7 +43,6 @@ import Outputable
 import FastString
 import TrieMap () -- DV: for now
 import DynFlags
-
 \end{code}
 
 
@@ -236,7 +236,7 @@ simplifyInfer :: Bool
 		      		    --   so the results type is not as general as
 				    --   it could be
                       TcEvBinds)    -- ... binding these evidence variables
-simplifyInfer _top_lvl apply_mr name_taus wanteds
+simplifyInfer top_lvl apply_mr name_taus wanteds
   | isEmptyWC wanteds
   = do { gbl_tvs     <- tcGetGlobalTyVars            -- Already zonked
        ; zonked_taus <- zonkTcTypes (map snd name_taus)
@@ -257,11 +257,72 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
              , ptext (sLit "taus =") <+> ppr (map snd name_taus)
              , ptext (sLit "tau_tvs (zonked) =") <+> ppr zonked_tau_tvs
              , ptext (sLit "gbl_tvs =") <+> ppr gbl_tvs
-             , ptext (sLit "closed =") <+> ppr _top_lvl
+             , ptext (sLit "closed =") <+> ppr top_lvl
              , ptext (sLit "apply_mr =") <+> ppr apply_mr
              , ptext (sLit "wanted =") <+> ppr zonked_wanteds
              ]
 
+
+            -- Step 2 
+            -- Now simplify the possibly-bound constraints
+       ; let ctxt = SimplInfer (ppr (map fst name_taus))
+       ; (simpl_results, _binds)
+             <- runTcS ctxt NoUntouchables emptyInert emptyWorkList $ 
+                simplifyWithApprox zonked_wanteds
+
+            -- Step 3 
+            -- Split again simplified_perhaps_bound, because some unifications 
+            -- may have happened, and emit the free constraints. 
+       ; gbl_tvs        <- tcGetGlobalTyVars
+       ; zonked_tau_tvs <- zonkTyVarsAndFV zonked_tau_tvs
+       ; zonked_results <- zonkWC simpl_results
+       ; (quantifiable_preds, rest_wc) <- quantifiablePreds apply_mr zonked_results
+       ; let full_gbl_tvs = gbl_tvs `unionVarSet` tyVarsOfWC rest_wc
+             init_tvs = zonked_tau_tvs `minusVarSet` full_gbl_tvs
+             qtvs     = growPreds1 full_gbl_tvs quantifiable_preds init_tvs
+	     minimal_flat_preds = filter (quantifyMe qtvs) quantifiable_preds
+
+	     -- Monomorphism restriction bites if the natural polymorphsim
+             --   (tau_tvs - gbl_tvs) is not the same as the actual polymorphism
+	     mr_bites = not ((zonked_tau_tvs `minusVarSet` gbl_tvs) `subVarSet` qtvs)
+
+       ; let  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)
+       ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
+       ; ev_binds_var <- newTcEvBinds
+       ; lcl_env <- getLclTypeEnv
+       ; gloc <- getCtLoc skol_info
+       ; let implic = Implic { ic_untch    = NoUntouchables
+                             , ic_env      = lcl_env
+                             , ic_skols    = qtvs_to_return
+                             , ic_given    = minimal_bound_ev_vars
+                             , ic_wanted   = wanteds
+                             , ic_insol    = False
+                             , ic_binds    = ev_binds_var
+                             , ic_loc      = gloc }
+       ; 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 "qtvs_to_return =") <+> ppr qtvs_to_return
+                  , ptext (sLit "init_tvs =") <+> ppr init_tvs
+                  , ptext (sLit "full_gbl_tvs =") <+> ppr full_gbl_tvs
+                  , ptext (sLit "rest_wc =") <+> ppr rest_wc
+                  , ptext (sLit "spb =") <+> ppr quantifiable_preds
+                  , ptext (sLit "bound =") <+> ppr minimal_flat_preds ]
+
+
+
+       ; return ( qtvs_to_return, minimal_bound_ev_vars
+                , mr_bites,  TcEvBinds ev_binds_var) } 
+------------
+{-
              -- Step 1
              -- Make a guess at the quantified type variables
 	     -- Then split the constraints on the baisis of those tyvars
@@ -329,8 +390,9 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
 
             -- Step 5
             -- Minimize `bound' and emit an implication
-       ; let minimal_flat_preds = predsToQuantify bound
-             skol_info = InferSkol [ (name, mkSigmaTy [] minimal_flat_preds ty)
+       ; minimal_flat_preds <- predsToQuantify bound
+}
+       ; let  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
@@ -362,19 +424,31 @@ simplifyInfer _top_lvl apply_mr name_taus wanteds
 
        ; return ( qtvs_to_return, minimal_bound_ev_vars
                 , mr_bites,  TcEvBinds ev_binds_var) } }
+-}
 
-predsToQuantify :: Cts -> [PredType]
+quantifiablePreds :: Bool -> WantedConstraints -> TcM ([PredType], WantedConstraints)
 -- From a bunch of (non-insoluble) flat constraints, pick the ones to generalise
 -- an inferred type over.  In particular:
 --    * Omit superclasses:         (Eq a, Ord a) --->  Ord a
 --    * Reject non-tyvar clases:   (Eq a, Show (Tree b)) --> Eq a
-predsToQuantify bound
-  = non_cls_preds ++ mkMinimalBySCs (filter isTyVarClassPred cls_preds)
-  where
-    (cls_preds, non_cls_preds) = partition isClassPred $
-                                 map ctPred $ bagToList bound
-\end{code}
+quantifiablePreds apply_mr wc
+  | apply_mr 
+  = return ([], wc)
+  | otherwise
+  = do { inst_envs <- tcGetInstEnvs
+       ; let (quant_flats, non_quant_flats) = partitionBag quantifiable (wc_flat wc)
+
+             quantifiable ct
+               | Just (cls, tys) <- getClassPredTys_maybe (ctPred ct)
+               = isTyVarClassApp cls tys 
+                 || case lookupInstEnv inst_envs cls tys of
+                      ([], [], _) -> False
+                      (_,  _,  _) -> True
+               | otherwise
+               = True
 
+       ; return (map ctPred (bagToList quant_flats), wc { wc_flat = non_quant_flats }) }
+\end{code}
 
 Note [Minimize by Superclasses]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
@@ -476,15 +550,20 @@ growPreds gbl_tvs get_pred items tvs
     extend item tvs = tvs `unionVarSet`
                       (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs)
 
+growPreds1 :: TyVarSet -> [PredType] -> TyVarSet -> TyVarSet
+growPreds1 gbl_tvs items tvs
+  = foldr extend tvs items
+  where
+    extend item tvs = tvs `unionVarSet`
+                      (growPredTyVars item tvs `minusVarSet` gbl_tvs)
+
 --------------------
 quantifyMe :: TyVarSet      -- Quantifying over these
-	   -> Ct
+	   -> PredType
 	   -> Bool	    -- True <=> quantify over this wanted
-quantifyMe qtvs ct
+quantifyMe qtvs pred
   | isIPPred pred = True  -- Note [Inheriting implicit parameters]
   | otherwise	  = tyVarsOfType pred `intersectsVarSet` qtvs
-  where
-    pred = ctPred ct
 \end{code}
 
 Note [Avoid unecessary constraint simplification]

compiler/typecheck/TcType.lhs

@@ -65,8 +65,9 @@ module TcType (
   isIntegerTy, isBoolTy, isUnitTy, isCharTy,
   isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, 
   isSynFamilyTyConApp,
-  isPredTy, isTyVarClassPred,
-  shallowPredTypePredTree,
+  isPredTy, 
+  isTyVarClassPred, isTyVarClassApp, isTyVarHeadClassPred, isTyVarHeadClassApp, 
+  classTyArgs, shallowPredTypePredTree,
   
   ---------------------------------
   -- Misc type manipulators
@@ -1102,8 +1103,33 @@ shallowPredTypePredTree ev_ty
 
 isTyVarClassPred :: PredType -> Bool
 isTyVarClassPred ty = case getClassPredTys_maybe ty of
-    Just (_, tys) -> all isTyVarTy tys
-    _             -> False
+    Just (cls, tks) -> isTyVarClassApp cls tks
+    _               -> False
+
+isTyVarClassApp :: Class -> [KindOrType] -> Bool
+isTyVarClassApp cls tks
+  = all tcIsTyVarTy (classTyArgs cls tks)
+
+isTyVarHeadClassPred :: PredType -> Bool
+isTyVarHeadClassPred ty = case getClassPredTys_maybe ty of
+    Just (cls, tks) -> isTyVarHeadClassApp cls tks
+    _               -> False
+
+isTyVarHeadClassApp :: Class -> [KindOrType] -> Bool
+isTyVarHeadClassApp cls tks
+  = all hasTyVarHead (classTyArgs cls tks)
+
+classTyArgs :: Class -> [KindOrType] -> [Type]
+-- Drop the initial kind arguments of a class
+classTyArgs cls kts = drop (count isKindVar (classTyVars cls)) kts  
+
+hasTyVarHead :: Type -> Bool
+hasTyVarHead ty			-- Haskell 98 allows predicates of form 
+  | tcIsTyVarTy ty = True	-- 	C (a ty1 .. tyn)
+  | otherwise			-- where a is a type variable
+  = case tcSplitAppTy_maybe ty of
+	Just (ty, _) -> hasTyVarHead ty
+	Nothing	     -> False
 
 evVarPred_maybe :: EvVar -> Maybe PredType
 evVarPred_maybe v = if isPredTy ty then Just ty else Nothing