A raft of small changes associated with -XConstrainedClassMethods

See Trac #7854.  Specifically:

* Major clean up and simplification of check_op in checkValidClass;
  specifically
     - use checkValidType on the entire method-selector type to detect
       ambiguity
     - put a specific test for -XConstrainedClassMethods

* Make -XConstrainedClassMethods be implied by -XMultiParamTypeClasses
  (a bit ad-hoc but see #7854), and document in the user manual.

* Do the checkAmbiguity test just once in TcValidity.checkValidType,
  rather than repeatedly at every level. See Note [When to call checkAmbiguity]

* Add -XAllowAmbiguousTypes in GHC.IP, since 'ip' really is ambiguous.
  (It's a rather magic function.)

* Improve location info for check_op in checkValidClass

* Update quite a few tests, which had genuinely-ambiguous class
  method signatures.  Some I fixed by making them unambiguous; some
  by adding -XAllowAmbiguousTypes

3 files changed, 155 insertions, 140 deletions

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index 6d6670cb32..ef9b4e658f 100644
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -3234,6 +3234,7 @@ impliedXFlags
     , (Opt_ExistentialQuantification, turnOn, Opt_ExplicitForAll)
     , (Opt_FlexibleInstances,         turnOn, Opt_TypeSynonymInstances)
     , (Opt_FunctionalDependencies,    turnOn, Opt_MultiParamTypeClasses)
+    , (Opt_MultiParamTypeClasses,     turnOn, Opt_ConstrainedClassMethods)  -- c.f. Trac #7854
 
     , (Opt_RebindableSyntax, turnOff, Opt_ImplicitPrelude)      -- NB: turn off!
 
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index f6d4085c38..6eb23b0700 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -28,7 +28,6 @@ import TcRnMonad
 import TcEnv
 import TcValidity
 import TcHsSyn
-import TcSimplify( growThetaTyVars )
 import TcBinds( tcRecSelBinds )
 import TcTyDecls
 import TcClassDcl
@@ -1665,30 +1664,25 @@ checkValidClass cls
           mapM_ (check_op constrained_class_methods) op_stuff
 
         -- Check the associated type defaults are well-formed and instantiated
-        ; mapM_ check_at_defs at_stuff  }
+        ; mapM_ check_at at_stuff  }
   where
     (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
     cls_arity = count isTypeVar tyvars    -- Ignore kind variables
     cls_tv_set = mkVarSet tyvars
 
     check_op constrained_class_methods (sel_id, dm)
-      = addErrCtxt (classOpCtxt sel_id tau) $ do
-        { checkValidTheta ctxt (tail theta)
-                -- The 'tail' removes the initial (C a) from the
-                -- class itself, leaving just the method type
-
-        ; traceTc "class op type" (ppr op_ty <+> ppr tau)
-        ; checkValidType ctxt tau
-
-                -- Check that the method type mentions a class variable
-                -- But actually check that the variables *reachable from*
-                -- the method type include a class variable.
+      = setSrcSpan (getSrcSpan sel_id) $
+        addErrCtxt (classOpCtxt sel_id op_ty) $ do
+        { traceTc "class op type" (ppr op_ty)
+        ; checkValidType ctxt op_ty
+                -- This implements the ambiguity check, among other things
                 -- Example: tc223
                 --   class Error e => Game b mv e | b -> mv e where
                 --      newBoard :: MonadState b m => m ()
                 -- Here, MonadState has a fundep m->b, so newBoard is fine
-        ; check_mentions (growThetaTyVars theta (tyVarsOfType tau))
-                         (ptext (sLit "class method") <+> quotes (ppr sel_id))
+
+        ; unless constrained_class_methods $
+          mapM_ check_constraint (tail (theta1 ++ theta2)) 
 
         ; case dm of
             GenDefMeth dm_name -> do { dm_id <- tcLookupId dm_name
@@ -1700,28 +1694,20 @@ checkValidClass cls
           op_name = idName sel_id
           op_ty   = idType sel_id
           (_,theta1,tau1) = tcSplitSigmaTy op_ty
-          (_,theta2,tau2) = tcSplitSigmaTy tau1
-          (theta,tau) | constrained_class_methods = (theta1 ++ theta2, tau2)
-                      | otherwise = (theta1, mkPhiTy (tail theta1) tau1)
-                -- Ugh!  The function might have a type like
-                --      op :: forall a. C a => forall b. (Eq b, Eq a) => tau2
-                -- With -XConstrainedClassMethods, we want to allow this, even though the inner
-                -- forall has an (Eq a) constraint.  Whereas in general, each constraint
-                -- in the context of a for-all must mention at least one quantified
-                -- type variable.  What a mess!
-
-    check_at_defs (ATI fam_tc _)
-      = check_mentions (mkVarSet (tyConTyVars fam_tc))
-                       (ptext (sLit "associated type") <+> quotes (ppr fam_tc))
-
-    check_mentions :: TyVarSet -> SDoc -> TcM ()
-       -- Check that the thing (method or associated type) mentions at least
-       -- one of the class type variables
-       -- The check is disabled for nullary type classes,
-       -- since there is no possible ambiguity (Trac #10020)
-    check_mentions thing_tvs thing_doc
-      = checkTc (cls_arity == 0 || thing_tvs `intersectsVarSet` cls_tv_set)
-                (noClassTyVarErr cls thing_doc)
+          (_,theta2,_)    = tcSplitSigmaTy tau1
+
+          check_constraint :: TcPredType -> TcM ()
+          check_constraint pred
+            = when (tyVarsOfType pred `subVarSet` cls_tv_set)
+                   (addErrTc (badMethPred sel_id pred))
+
+    check_at (ATI fam_tc _)
+      | cls_arity > 0   -- Check that the associated type mentions at least
+                        -- one of the class type variables
+      = checkTc (any (`elemVarSet` cls_tv_set) (tyConTyVars fam_tc))
+                (noClassTyVarErr cls fam_tc)
+      | otherwise       -- The check is disabled for nullary type classes,
+      = return ()       -- since there is no possible ambiguity (Trac #10020)
 
 checkFamFlag :: Name -> TcM ()
 -- Check that we don't use families without -XTypeFamilies
@@ -2154,10 +2140,17 @@ classFunDepsErr cls
   = vcat [ptext (sLit "Fundeps in class") <+> quotes (ppr cls),
           parens (ptext (sLit "Use FunctionalDependencies to allow fundeps"))]
 
-noClassTyVarErr :: Class -> SDoc -> SDoc
-noClassTyVarErr clas what
-  = sep [ptext (sLit "The") <+> what,
-         ptext (sLit "mentions none of the type or kind variables of the class") <+>
+badMethPred :: Id -> TcPredType -> SDoc
+badMethPred sel_id pred
+  = vcat [ hang (ptext (sLit "Constraint") <+> quotes (ppr pred) 
+                 <+> ptext (sLit "in the type of") <+> quotes (ppr sel_id))
+              2 (ptext (sLit "constrains only the class type variables"))
+         , ptext (sLit "Use ConstrainedClassMethods to allow it") ]
+
+noClassTyVarErr :: Class -> TyCon -> SDoc
+noClassTyVarErr clas fam_tc
+  = sep [ ptext (sLit "The associated type") <+> quotes (ppr fam_tc)
+        , ptext (sLit "mentions none of the type or kind variables of the class") <+>
                 quotes (ppr clas <+> hsep (map ppr (classTyVars clas)))]
 
 recSynErr :: [LTyClDecl Name] -> TcRn ()
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index f6067e61ab..3988af47b2 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -56,6 +56,122 @@ import Data.List        ( (\\) )
           Checking for ambiguity
 *                                                                      *
 ************************************************************************
+
+Note [The ambiguity check for type signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+checkAmbiguity is a check on *user-supplied type signatures*.  It is
+*purely* there to report functions that cannot possibly be called.  So for
+example we want to reject:
+   f :: C a => Int
+The idea is there can be no legal calls to 'f' because every call will
+give rise to an ambiguous constraint.  We could soundly omit the
+ambiguity check on type signatures entirely, at the expense of
+delaying ambiguity errors to call sites.  Indeed, the flag
+-XAllowAmbiguousTypes switches off the ambiguity check.
+
+What about things like this:
+   class D a b | a -> b where ..
+   h :: D Int b => Int
+The Int may well fix 'b' at the call site, so that signature should
+not be rejected.  Moreover, using *visible* fundeps is too
+conservative.  Consider
+   class X a b where ...
+   class D a b | a -> b where ...
+   instance D a b => X [a] b where...
+   h :: X a b => a -> a
+Here h's type looks ambiguous in 'b', but here's a legal call:
+   ...(h [True])...
+That gives rise to a (X [Bool] beta) constraint, and using the
+instance means we need (D Bool beta) and that fixes 'beta' via D's
+fundep!
+
+Behind all these special cases there is a simple guiding principle.
+Consider
+
+  f :: <type>
+  f = ...blah...
+
+  g :: <type>
+  g = f
+
+You would think that the definition of g would surely typecheck!
+After all f has exactly the same type, and g=f. But in fact f's type
+is instantiated and the instantiated constraints are solved against
+the originals, so in the case an ambiguous type it won't work.
+Consider our earlier example f :: C a => Int.  Then in g's definition,
+we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a),
+and fail.
+
+So in fact we use this as our *definition* of ambiguity.  We use a
+very similar test for *inferred* types, to ensure that they are
+unambiguous. See Note [Impedence matching] in TcBinds.
+
+This test is very conveniently implemented by calling
+    tcSubType <type> <type>
+This neatly takes account of the functional dependecy stuff above,
+and implicit parameter (see Note [Implicit parameters and ambiguity]).
+And this is what checkAmbiguity does.
+
+What about this, though?
+   g :: C [a] => Int
+Is every call to 'g' ambiguous?  After all, we might have
+   intance C [a] where ...
+at the call site.  So maybe that type is ok!  Indeed even f's
+quintessentially ambiguous type might, just possibly be callable:
+with -XFlexibleInstances we could have
+  instance C a where ...
+and now a call could be legal after all!  Well, we'll reject this
+unless the instance is available *here*.
+
+Note [When to call checkAmbiguity]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We call checkAmbiguity 
+   (a) on user-specified type signatures
+   (b) in checkValidType
+
+Conncerning (b), you might wonder about nested foralls.  What about
+    f :: (forall a. Eq a => Int) -> Int
+The nested forall is ambiguous.  Originally we called checkAmbiguity
+in the forall case of check_type, but that had a bad consequence:
+we got two error messages about (Eq b) in a nested forall like this:
+    g :: forall a. Eq a => forall b. Eq b => a -> a
+To avoid this, we call checkAmbiguity once, at the top, in checkValidType.
+
+In fact, because of the co/contra-variance implemented in tcSubType, 
+this *does* catch function f above. too.
+
+Concerning (a) the ambiguity check is only used for *user* types, not
+for types coming from inteface files.  The latter can legitimately
+have ambiguous types. Example
+
+   class S a where s :: a -> (Int,Int)
+   instance S Char where s _ = (1,1)
+   f:: S a => [a] -> Int -> (Int,Int)
+   f (_::[a]) x = (a*x,b)
+        where (a,b) = s (undefined::a)
+
+Here the worker for f gets the type
+        fw :: forall a. S a => Int -> (# Int, Int #)
+
+
+Note [Implicit parameters and ambiguity]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Only a *class* predicate can give rise to ambiguity
+An *implicit parameter* cannot.  For example:
+        foo :: (?x :: [a]) => Int
+        foo = length ?x
+is fine.  The call site will suppply a particular 'x'
+
+Furthermore, the type variables fixed by an implicit parameter
+propagate to the others.  E.g.
+        foo :: (Show a, ?x::[a]) => Int
+        foo = show (?x++?x)
+The type of foo looks ambiguous.  But it isn't, because at a call site
+we might have
+        let ?x = 5::Int in foo
+and all is well.  In effect, implicit parameters are, well, parameters,
+so we can take their type variables into account as part of the
+"tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
 -}
 
 checkAmbiguity :: UserTypeCtxt -> Type -> TcM ()
@@ -179,6 +295,9 @@ checkValidType ctxt ty
         -- the kind of an ill-formed type such as (a~Int)
        ; check_kind ctxt ty
 
+       -- Check for ambiguous types.  See Note [When to call checkAmbiguity]
+       ; checkAmbiguity ctxt ty
+
        ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
 
 checkValidMonoType :: Type -> TcM ()
@@ -273,8 +392,7 @@ check_type ctxt rank ty
                 -- Reject e.g. (Maybe (?x::Int => Int)),
                 -- with a decent error message
         ; check_valid_theta ctxt theta
-        ; check_type ctxt rank tau      -- Allow foralls to right of arrow
-        ; checkAmbiguity ctxt ty }
+        ; check_type ctxt rank tau }      -- Allow foralls to right of arrow
   where
     (tvs, theta, tau) = tcSplitSigmaTy ty
 
@@ -644,103 +762,6 @@ Flexibility check:
 
   The dictionary gets type [C * (D *)]. IA0_TODO it should be
   generalized actually.
-
-Note [The ambiguity check for type signatures]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-checkAmbiguity is a check on user-supplied type signatures.  It is
-*purely* there to report functions that cannot possibly be called.  So for
-example we want to reject:
-   f :: C a => Int
-The idea is there can be no legal calls to 'f' because every call will
-give rise to an ambiguous constraint.  We could soundly omit the
-ambiguity check on type signatures entirely, at the expense of
-delaying ambiguity errors to call sites.  Indeed, the flag
--XAllowAmbiguousTypes switches off the ambiguity check.
-
-What about things like this:
-   class D a b | a -> b where ..
-   h :: D Int b => Int
-The Int may well fix 'b' at the call site, so that signature should
-not be rejected.  Moreover, using *visible* fundeps is too
-conservative.  Consider
-   class X a b where ...
-   class D a b | a -> b where ...
-   instance D a b => X [a] b where...
-   h :: X a b => a -> a
-Here h's type looks ambiguous in 'b', but here's a legal call:
-   ...(h [True])...
-That gives rise to a (X [Bool] beta) constraint, and using the
-instance means we need (D Bool beta) and that fixes 'beta' via D's
-fundep!
-
-Behind all these special cases there is a simple guiding principle.
-Consider
-
-  f :: <type>
-  f = ...blah...
-
-  g :: <type>
-  g = f
-
-You would think that the definition of g would surely typecheck!
-After all f has exactly the same type, and g=f. But in fact f's type
-is instantiated and the instantiated constraints are solved against
-the originals, so in the case an ambiguous type it won't work.
-Consider our earlier example f :: C a => Int.  Then in g's definition,
-we'll instantiate to (C alpha) and try to deduce (C alpha) from (C a),
-and fail.
-
-So in fact we use this as our *definition* of ambiguity.  We use a
-very similar test for *inferred* types, to ensure that they are
-unambiguous. See Note [Impedence matching] in TcBinds.
-
-This test is very conveniently implemented by calling
-    tcSubType <type> <type>
-This neatly takes account of the functional dependecy stuff above,
-and implicit parameter (see Note [Implicit parameters and ambiguity]).
-
-What about this, though?
-   g :: C [a] => Int
-Is every call to 'g' ambiguous?  After all, we might have
-   intance C [a] where ...
-at the call site.  So maybe that type is ok!  Indeed even f's
-quintessentially ambiguous type might, just possibly be callable:
-with -XFlexibleInstances we could have
-  instance C a where ...
-and now a call could be legal after all!  Well, we'll reject this
-unless the instance is available *here*.
-
-Side note: the ambiguity check is only used for *user* types, not for
-types coming from inteface files.  The latter can legitimately have
-ambiguous types. Example
-
-   class S a where s :: a -> (Int,Int)
-   instance S Char where s _ = (1,1)
-   f:: S a => [a] -> Int -> (Int,Int)
-   f (_::[a]) x = (a*x,b)
-        where (a,b) = s (undefined::a)
-
-Here the worker for f gets the type
-        fw :: forall a. S a => Int -> (# Int, Int #)
-
-Note [Implicit parameters and ambiguity]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Only a *class* predicate can give rise to ambiguity
-An *implicit parameter* cannot.  For example:
-        foo :: (?x :: [a]) => Int
-        foo = length ?x
-is fine.  The call site will suppply a particular 'x'
-
-Furthermore, the type variables fixed by an implicit parameter
-propagate to the others.  E.g.
-        foo :: (Show a, ?x::[a]) => Int
-        foo = show (?x++?x)
-The type of foo looks ambiguous.  But it isn't, because at a call site
-we might have
-        let ?x = 5::Int in foo
-and all is well.  In effect, implicit parameters are, well, parameters,
-so we can take their type variables into account as part of the
-"tau-tvs" stuff.  This is done in the function 'FunDeps.grow'.
 -}
 
 checkThetaCtxt :: UserTypeCtxt -> ThetaType -> SDoc