diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index d4d495271143118a49da0ee6003f0ff0ed3491bc..f3105c8d45c46730295ac39170cc6e5fc061d4b0 100644
--- a/compiler/typecheck/TcMType.lhs
+++ b/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)
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 59860812a7d0802fa833a3b32e2c73718cb3b85a..c63a31f7fc1ee59d3ad16b6eb3bf277e795fe999 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -1,5 +1,5 @@
\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]
diff --git a/compiler/typecheck/TcType.lhs b/compiler/typecheck/TcType.lhs
index 74b4e1a066af7aeb868d18a048a447b3dcaf9dc3..95a83c9204c6bb99112d61482a64c174fa0ceb77 100644
--- a/compiler/typecheck/TcType.lhs
+++ b/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