Tidy up treatment of FlexibleContexts

Previously (Trac #10351) we could get

    Non type-variable argument in the constraint: C [t]
    (Use FlexibleContexts to permit this)
    When checking that `f' has the inferred type
      f :: forall t. C [t] => t -> ()

which is a bit stupid: we have *inferred* a type that we
immediately *reject*.  This patch arranges that that the
generalisation mechanism (TcSimplify.decideQuantification)
doesn't pick a predicate that will be rejected by the
subsequent validity check.

This forced some minor refactoring, as usual.

5 files changed, 117 insertions, 92 deletions

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 094984be2e..f078c5162a 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -3264,11 +3264,6 @@ impliedXFlags
 
     , (Opt_ParallelArrays, turnOn, Opt_ParallelListComp)
 
-    -- An implicit parameter constraint, `?x::Int`, is desugared into
-    -- `IP "x" Int`, which requires a flexible context/instance.
-    , (Opt_ImplicitParams, turnOn, Opt_FlexibleContexts)
-    , (Opt_ImplicitParams, turnOn, Opt_FlexibleInstances)
-
     , (Opt_JavaScriptFFI, turnOn, Opt_InterruptibleFFI)
 
     , (Opt_DeriveTraversable, turnOn, Opt_DeriveFunctor)
diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs
index 17f60787c6..64333ebdb3 100644
--- a/compiler/typecheck/TcBinds.hs
+++ b/compiler/typecheck/TcBinds.hs
@@ -688,8 +688,9 @@ mkInferredPolyId poly_name qtvs theta mono_ty
              my_tvs2 = closeOverKinds (growThetaTyVars theta (tyVarsOfType norm_mono_ty))
                   -- Include kind variables!  Trac #7916
 
-             my_tvs   = filter (`elemVarSet` my_tvs2) qtvs   -- Maintain original order
-             my_theta = filter (quantifyPred my_tvs2) theta
+       ; my_theta <- pickQuantifiablePreds my_tvs2 theta
+
+       ; let my_tvs   = filter (`elemVarSet` my_tvs2) qtvs   -- Maintain original order
              inferred_poly_ty = mkSigmaTy my_tvs my_theta norm_mono_ty
 
        ; addErrCtxtM (mk_bind_msg True False poly_name inferred_poly_ty) $
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 5f9f417e1c..c1535f8733 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -2,7 +2,7 @@
 
 module TcSimplify(
        simplifyInfer,
-       quantifyPred, growThetaTyVars,
+       pickQuantifiablePreds, growThetaTyVars,
        simplifyAmbiguityCheck,
        simplifyDefault,
        simplifyTop, simplifyInteractive,
@@ -40,7 +40,7 @@ import Util
 import PrelInfo
 import PrelNames
 import Control.Monad    ( unless )
-import DynFlags         ( ExtensionFlag( Opt_AllowAmbiguousTypes ) )
+import DynFlags         ( ExtensionFlag( Opt_AllowAmbiguousTypes, Opt_FlexibleContexts ) )
 import Class            ( classKey )
 import Maybes           ( isNothing )
 import Outputable
@@ -424,8 +424,9 @@ If the monomorphism restriction does not apply, then we quantify as follows:
     (This actually unifies each quantifies meta-tyvar with a fresh skolem.)
     Result is qtvs.
 
-  * Filter the constraints using quantifyPred and the qtvs.  We have to
-    zonk the constraints first, so they "see" the freshly created skolems.
+  * Filter the constraints using pickQuantifyablePreds and the qtvs.
+    We have to zonk the constraints first, so they "see" the freshly
+    created skolems.
 
 If the MR does apply, mono_tvs includes all the constrained tyvars,
 and the quantified constraints are empty.
@@ -457,31 +458,43 @@ decideQuantification apply_mr constraints zonked_tau_tvs
               -- quantifyTyVars turned some meta tyvars into
               -- quantified skolems, so we have to zonk again
 
-       ; let theta     = filter (quantifyPred (mkVarSet qtvs)) constraints
-             min_theta = mkMinimalBySCs theta  -- See Note [Minimize by Superclasses]
+       ; theta <- pickQuantifiablePreds (mkVarSet qtvs) constraints
+       ; let min_theta = mkMinimalBySCs theta  -- See Note [Minimize by Superclasses]
+
        ; traceTc "decideQuantification 2" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs
                                                 , ppr tau_tvs_plus, ppr qtvs, ppr min_theta])
        ; return (qtvs, min_theta, False) }
 
 ------------------
-quantifyPred :: TyVarSet           -- Quantifying over these
-             -> PredType -> Bool   -- True <=> quantify over this wanted
+pickQuantifiablePreds :: TyVarSet         -- Quantifying over these
+                      -> TcThetaType      -- Proposed constraints to quantify
+                      -> TcM TcThetaType  -- A subset that we can actually quantify
 -- This function decides whether a particular constraint shoudl be
 -- quantified over, given the type variables that are being quantified
-quantifyPred qtvs pred
-  = case classifyPredType pred of
-      ClassPred cls tys
-         | isIPClass cls    -> True -- See note [Inheriting implicit parameters]
-         | otherwise        -> tyVarsOfTypes tys `intersectsVarSet` qtvs
-
-      EqPred NomEq ty1 ty2  -> quant_fun ty1 || quant_fun ty2
-        -- representational equality is like a class constraint
-      EqPred ReprEq ty1 ty2 -> tyVarsOfTypes [ty1, ty2] `intersectsVarSet` qtvs
-
-      IrredPred ty          -> tyVarsOfType ty `intersectsVarSet` qtvs
-      TuplePred {}          -> False
+pickQuantifiablePreds qtvs theta
+  = do { flex_ctxt <- xoptM Opt_FlexibleContexts
+       ; return (filter (pick_me flex_ctxt) theta) }
   where
-    -- See Note [Quantifying over equality constraints]
+    pick_me flex_ctxt pred
+      = case classifyPredType pred of
+          ClassPred cls tys
+             | isIPClass cls -> True -- See note [Inheriting implicit parameters]
+             | otherwise     -> pick_cls_pred flex_ctxt tys
+
+          EqPred ReprEq ty1 ty2 -> pick_cls_pred flex_ctxt [ty1, ty2]
+                -- Representational equality is like a class constraint
+
+          EqPred NomEq ty1 ty2  -> quant_fun ty1 || quant_fun ty2
+          IrredPred ty          -> tyVarsOfType ty `intersectsVarSet` qtvs
+          TuplePred {}          -> False
+
+    pick_cls_pred flex_ctxt tys
+      = tyVarsOfTypes tys `intersectsVarSet` qtvs
+        && (checkValidClsArgs flex_ctxt tys)
+           -- Only quantify over predicates that checkValidType
+           -- will pass!  See Trac #10351.
+
+        -- See Note [Quantifying over equality constraints]
     quant_fun ty
       = case tcSplitTyConApp_maybe ty of
           Just (tc, tys) | isTypeFamilyTyCon tc
@@ -558,7 +571,7 @@ 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.
+declarations. See the pickQuantifiablePreds.
 
 Note [Quantification with errors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 4185be8214..4d4f6823f2 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -69,6 +69,7 @@ module TcType (
   isIntegerTy, isBoolTy, isUnitTy, isCharTy,
   isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
   isPredTy, isTyVarClassPred, isTyVarExposed,
+  checkValidClsArgs, hasTyVarHead,
 
   ---------------------------------
   -- Misc type manipulators
@@ -1313,6 +1314,14 @@ straightforward.
 ************************************************************************
 
 Deconstructors and tests on predicate types
+
+Note [Kind polymorphic type classes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    class C f where...   -- C :: forall k. k -> Constraint
+    g :: forall (f::*). C f => f -> f
+
+Here the (C f) in the signature is really (C * f), and we 
+don't want to complain that the * isn't a type variable!
 -}
 
 isTyVarClassPred :: PredType -> Bool
@@ -1320,6 +1329,28 @@ isTyVarClassPred ty = case getClassPredTys_maybe ty of
     Just (_, tys) -> all isTyVarTy tys
     _             -> False
 
+-------------------------
+checkValidClsArgs :: Bool -> [KindOrType] -> Bool
+-- If the Bool is True (flexible contexts), return True (i.e. ok)
+-- Otherwise, check that the type (not kind) args are all headed by a tyvar
+--   E.g. (Eq a) accepted, (Eq (f a)) accepted, but (Eq Int) rejected
+-- This function is here rather than in TcValidity because it is
+-- called from TcSimplify, which itself is imported by TcValidity
+checkValidClsArgs flexible_contexts kts
+  | flexible_contexts = True
+  | otherwise         = all hasTyVarHead tys
+  where
+    (_, tys) = span isKind kts  -- see Note [Kind polymorphic type classes]
+   
+hasTyVarHead :: Type -> Bool
+-- Returns true of (a t1 .. tn), where 'a' is a type variable
+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
   where ty = varType v
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 53b492d3e6..3225b2848b 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -23,13 +23,14 @@ import TcSimplify ( simplifyAmbiguityCheck )
 import TypeRep
 import TcType
 import TcMType
-import TysWiredIn ( coercibleClass )
+import TysWiredIn ( coercibleClass, eqTyConName )
 import Type
 import Unify( tcMatchTyX )
 import Kind
 import CoAxiom
 import Class
 import TyCon
+import PrelNames( eqTyConKey )
 
 -- others:
 import HsSyn            -- HsType
@@ -44,6 +45,7 @@ import Util
 import ListSetOps
 import SrcLoc
 import Outputable
+import Unique           ( hasKey )
 import BasicTypes       ( IntWithInf, infinity )
 import FastString
 
@@ -593,6 +595,7 @@ check_valid_theta ctxt theta
   = do { dflags <- getDynFlags
        ; warnTc (wopt Opt_WarnDuplicateConstraints dflags &&
                  notNull dups) (dupPredWarn dups)
+       ; traceTc "check_valid_theta" (ppr theta)
        ; mapM_ (check_pred_ty dflags ctxt) theta }
   where
     (_,dups) = removeDups cmpPred theta
@@ -612,46 +615,29 @@ check_pred_help :: Bool    -- True <=> under a type synonym
                 -> DynFlags -> UserTypeCtxt
                 -> PredType -> TcM ()
 check_pred_help under_syn dflags ctxt pred
-  | Just pred' <- coreView pred
-  = check_pred_help True dflags ctxt pred'
+  | Just pred' <- coreView pred  -- Switch on under_syn when going under a
+                                 -- synonym (Trac #9838, yuk)
+  = check_pred_help True dflags ctxt pred'  
   | otherwise
-  = case classifyPredType pred of
-      ClassPred cls tys     -> check_class_pred dflags ctxt pred cls tys
-      EqPred NomEq _ _      -> check_eq_pred    dflags pred
-      EqPred ReprEq ty1 ty2 -> check_repr_eq_pred dflags ctxt pred ty1 ty2
-      TuplePred tys         -> check_tuple_pred under_syn dflags ctxt pred tys
-      IrredPred _           -> check_irred_pred under_syn dflags ctxt pred
-
-check_class_pred :: DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
-check_class_pred dflags ctxt pred cls tys
-  = do {        -- Class predicates are valid in all contexts
-       ; checkTc (arity == n_tys) arity_err
-
-       ; checkTc (not (isIPClass cls) || okIPCtxt ctxt)
-                 (badIPPred pred)
-
-                -- Check the form of the argument types
-       ; check_class_pred_tys dflags ctxt pred tys
-       }
-  where
-    class_name = className cls
-    arity      = classArity cls
-    n_tys      = length tys
-    arity_err  = arityErr "Class" class_name arity n_tys
-
-check_eq_pred :: DynFlags -> PredType -> TcM ()
-check_eq_pred dflags pred
+  = case splitTyConApp_maybe pred of
+      Just (tc, tys) | Just cls <- tyConClass_maybe tc
+                     -> check_class_pred dflags ctxt pred cls tys  -- Includes Coercible
+                     | tc `hasKey` eqTyConKey
+                     -> check_eq_pred dflags pred tys
+                     | isTupleTyCon tc
+                     -> check_tuple_pred under_syn dflags ctxt pred tys
+      _ -> check_irred_pred under_syn dflags ctxt pred
+
+check_eq_pred :: DynFlags -> PredType -> [TcType] -> TcM ()
+check_eq_pred dflags pred tys
   =         -- Equational constraints are valid in all contexts if type
             -- families are permitted
-    checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags)
-            (eqPredTyErr pred)
-
-check_repr_eq_pred :: DynFlags -> UserTypeCtxt -> PredType
-                   -> TcType -> TcType -> TcM ()
-check_repr_eq_pred dflags ctxt pred ty1 ty2
-  = check_class_pred_tys dflags ctxt pred tys
+    do { checkTc (n_tys == 3)
+                 (arityErr "Equality constraint" eqTyConName 3 n_tys)
+       ; checkTc (xopt Opt_TypeFamilies dflags || xopt Opt_GADTs dflags)
+                 (eqPredTyErr pred) }
   where
-    tys = [ty1, ty2]
+    n_tys = length tys
 
 check_tuple_pred :: Bool -> DynFlags -> UserTypeCtxt -> PredType -> [PredType] -> TcM ()
 check_tuple_pred under_syn dflags ctxt pred ts
@@ -670,7 +656,7 @@ check_irred_pred under_syn dflags ctxt pred
          --   see Note [ConstraintKinds in predicates]
          -- But (X t1 t2) is always ok because we just require ConstraintKinds
          -- at the definition site (Trac #9838)
-        checkTc (under_syn || xopt Opt_ConstraintKinds dflags || not (tyvar_head pred))
+        checkTc (under_syn || xopt Opt_ConstraintKinds dflags || not (hasTyVarHead pred))
                 (predIrredErr pred)
 
          -- Make sure it is OK to have an irred pred in this context
@@ -708,32 +694,30 @@ It is equally dangerous to allow them in instance heads because in that case the
 Paterson conditions may not detect duplication of a type variable or size change. -}
 
 -------------------------
-check_class_pred_tys :: DynFlags -> UserTypeCtxt
-                     -> PredType -> [KindOrType] -> TcM ()
-check_class_pred_tys dflags ctxt pred kts
-  = checkTc pred_ok (predTyVarErr pred $$ how_to_allow)
-  where
-    (_, tys) = span isKind kts  -- see Note [Kind polymorphic type classes]
-    flexible_contexts = xopt Opt_FlexibleContexts dflags
-    undecidable_ok = xopt Opt_UndecidableInstances dflags
+check_class_pred :: DynFlags -> UserTypeCtxt -> PredType -> Class -> [TcType] -> TcM ()
+check_class_pred dflags ctxt pred cls tys
+  | isIPClass cls
+  = do { checkTc (arity == n_tys) arity_err
+       ; checkTc (okIPCtxt ctxt)  (badIPPred pred) }
 
-    pred_ok = case ctxt of
-        SpecInstCtxt -> True    -- {-# SPECIALISE instance Eq (T Int) #-} is fine
-        InstDeclCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
-                                -- Further checks on head and theta in
-                                -- checkInstTermination
-        _             -> flexible_contexts || all tyvar_head tys
-    how_to_allow = parens (ptext (sLit "Use FlexibleContexts to permit this"))
+  | otherwise
+  = do { checkTc (arity == n_tys) arity_err
+       ; checkTc arg_tys_ok (predTyVarErr pred) }
+  where
+    class_name = className cls
+    arity      = classArity cls
+    n_tys      = length tys
+    arity_err  = arityErr "Class" class_name arity n_tys
 
+    flexible_contexts = xopt Opt_FlexibleContexts     dflags
+    undecidable_ok    = xopt Opt_UndecidableInstances dflags
 
--------------------------
-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
+    arg_tys_ok = case ctxt of
+        SpecInstCtxt -> True    -- {-# SPECIALISE instance Eq (T Int) #-} is fine
+        InstDeclCtxt -> checkValidClsArgs (flexible_contexts || undecidable_ok) tys
+                                -- Further checks on head and theta
+                                -- in checkInstTermination
+        _            -> checkValidClsArgs flexible_contexts tys
 
 -------------------------
 okIPCtxt :: UserTypeCtxt -> Bool
@@ -776,8 +760,9 @@ eqPredTyErr, predTyVarErr, predTupleErr, predIrredErr, predIrredBadCtxtErr :: Pr
 eqPredTyErr  pred = ptext (sLit "Illegal equational constraint") <+> pprType pred
                     $$
                     parens (ptext (sLit "Use GADTs or TypeFamilies to permit this"))
-predTyVarErr pred  = hang (ptext (sLit "Non type-variable argument"))
-                        2 (ptext (sLit "in the constraint:") <+> pprType pred)
+predTyVarErr pred  = vcat [ hang (ptext (sLit "Non type-variable argument"))
+                               2 (ptext (sLit "in the constraint:") <+> pprType pred)
+                          , parens (ptext (sLit "Use FlexibleContexts to permit this")) ]
 predTupleErr pred  = hang (ptext (sLit "Illegal tuple constraint:") <+> pprType pred)
                         2 (parens constraintKindsMsg)
 predIrredErr pred  = hang (ptext (sLit "Illegal constraint:") <+> pprType pred)