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

30 files changed, 260 insertions, 197 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
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index edfdc849bf..8a1c9ec468 100644
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -4442,15 +4442,16 @@ class type variable, thus:
     elem     :: Eq a => a -> s a -> Bool
 </programlisting>
 The type of <literal>elem</literal> is illegal in Haskell 98, because it
-contains the constraint <literal>Eq a</literal>, constrains only the
+contains the constraint <literal>Eq a</literal>, which constrains only the
 class type variable (in this case <literal>a</literal>).
-GHC lifts this restriction (flag <option>-XConstrainedClassMethods</option>).
 </para>
-
-
+<para>
+GHC lifts this restriction with language extension <option>-XConstrainedClassMethods</option>.
+The restriction is a pretty stupid one in the first place, 
+so <option>-XConstrainedClassMethods</option> is implied by <option>-XMultiParamTypeClasses</option>.
+</para>
 </sect3>
 
-
 <sect3 id="class-default-signatures">
 <title>Default method signatures</title>
 
diff --git a/libraries/base/GHC/IP.hs b/libraries/base/GHC/IP.hs
index 9a4a0ec009..b85c382a43 100644
--- a/libraries/base/GHC/IP.hs
+++ b/libraries/base/GHC/IP.hs
@@ -4,6 +4,8 @@
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}  
+  -- ip :: IP x a => a  is strictly speaking ambiguous, but IP is magic
 
 -- | @since 4.6.0.0
 module GHC.IP (IP(..)) where
diff --git a/testsuite/tests/indexed-types/should_compile/T2715.hs b/testsuite/tests/indexed-types/should_compile/T2715.hs
index 0fae15eaf8..c283467b82 100644
--- a/testsuite/tests/indexed-types/should_compile/T2715.hs
+++ b/testsuite/tests/indexed-types/should_compile/T2715.hs
@@ -3,6 +3,8 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+    -- The type of 'empty' is indeed ambiguous
 
 module T2715 where
 
@@ -14,9 +16,8 @@ type instance Domain Interval = Interval
 
 type family Value (d :: * -> *) :: *
 
-
 class IDomain d where
-   empty   :: (Ord (Value d), Enum (Value d)) => (Domain d) (Value d)
+   empty   :: (Ord (Value d), Enum (Value d)) => Domain d (Value d)
 
 class (IDomain d1) -- (IDomain d1, IDomain d2, Value d1 ~ Value d2) 
    => IIDomain (d1 :: * -> *) (d2 :: * -> * ) where
@@ -25,7 +26,7 @@ class (IDomain d1) -- (IDomain d1, IDomain d2, Value d1 ~ Value d2)
 
 instance Ord (Value Interval) 
       => IDomain Interval where
-   empty                   = Intv (toEnum 1, toEnum 0)
+   empty = Intv (toEnum 1, toEnum 0)
 
 instance Ord (Value Interval) 
       => IIDomain Interval Interval where
diff --git a/testsuite/tests/indexed-types/should_compile/T4160.hs b/testsuite/tests/indexed-types/should_compile/T4160.hs
index f13aafa103..ee95e8c874 100644
--- a/testsuite/tests/indexed-types/should_compile/T4160.hs
+++ b/testsuite/tests/indexed-types/should_compile/T4160.hs
@@ -1,4 +1,7 @@
 {-# LANGUAGE FlexibleContexts, MultiParamTypeClasses, TypeFamilies #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+    -- The type of sizeT is indeed ambiguous
+
 module Foo where
 
 data P f g r = f r :*: g r
diff --git a/testsuite/tests/indexed-types/should_compile/T4200.hs b/testsuite/tests/indexed-types/should_compile/T4200.hs
index feb91e8d8b..a9a1a5bd63 100644
--- a/testsuite/tests/indexed-types/should_compile/T4200.hs
+++ b/testsuite/tests/indexed-types/should_compile/T4200.hs
@@ -5,9 +5,9 @@ module T4200 where
 
 class C a where
   type In a :: *
-  op :: In a -> Int
+  op :: In a -> a -> Int
 
 -- Should be ok; no -XUndecidableInstances required
 instance (In c ~ Int) => C [c] where 
   type In [c] = In c
-  op x = 3
+  op _ _ = 3
diff --git a/testsuite/tests/indexed-types/should_compile/T9582.hs b/testsuite/tests/indexed-types/should_compile/T9582.hs
index f86d723319..d906205834 100644
--- a/testsuite/tests/indexed-types/should_compile/T9582.hs
+++ b/testsuite/tests/indexed-types/should_compile/T9582.hs
@@ -3,12 +3,12 @@ module T9582 where
 
 class C a where
   type T a
-  m :: T a
+  m :: a -> T a
 
 instance C Int where
   type T Int = String
-  m :: String
-  m = "bla"
+  m :: Int -> String
+  m _ = "bla"
 
 -- Method signature does not match class; it should be m :: T Int
 --    In the instance declaration for ‘C Int’
diff --git a/testsuite/tests/indexed-types/should_fail/T1900.stderr b/testsuite/tests/indexed-types/should_fail/T1900.stderr
index 0d02a52f11..f986888cfd 100644
--- a/testsuite/tests/indexed-types/should_fail/T1900.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T1900.stderr
@@ -1,12 +1,13 @@
-
-T1900.hs:13:10:
-    Couldn't match type ‘Depend s0’ with ‘Depend s’
-    NB: ‘Depend’ is a type function, and may not be injective
-    The type variable ‘s0’ is ambiguous
-    Expected type: Depend s -> Bool
-      Actual type: Depend s0 -> Bool
-    In the ambiguity check for the type signature for ‘check’:
-      check :: forall s. Bug s => Depend s -> Bool
-    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
-    In the type signature for ‘check’:
-      check :: (Bug s) => Depend s -> Bool
+

+T1900.hs:7:3:

+    Couldn't match type ‘Depend s0’ with ‘Depend s’

+    NB: ‘Depend’ is a type function, and may not be injective

+    The type variable ‘s0’ is ambiguous

+    Expected type: Depend s -> Depend s

+      Actual type: Depend s0 -> Depend s0

+    In the ambiguity check for the type signature for ‘trans’:

+      trans :: forall s. Bug s => Depend s -> Depend s

+    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes

+    When checking the class method:

+      trans :: forall s. Bug s => Depend s -> Depend s

+    In the class declaration for ‘Bug’

diff --git a/testsuite/tests/indexed-types/should_fail/T2544.hs b/testsuite/tests/indexed-types/should_fail/T2544.hs
index 3653a42317..0e98910055 100644
--- a/testsuite/tests/indexed-types/should_fail/T2544.hs
+++ b/testsuite/tests/indexed-types/should_fail/T2544.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE TypeOperators, TypeFamilies #-}

+{-# LANGUAGE AllowAmbiguousTypes #-}

+    -- The type of 'empty' is indeed ambiguous

 

 module T2544 where

 

diff --git a/testsuite/tests/indexed-types/should_fail/T2544.stderr b/testsuite/tests/indexed-types/should_fail/T2544.stderr
index 6c5230800c..7a1f564c56 100644
--- a/testsuite/tests/indexed-types/should_fail/T2544.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2544.stderr
@@ -1,11 +1,11 @@
 

-T2544.hs:15:12:

+T2544.hs:17:12:

     Couldn't match type ‘IxMap l’ with ‘IxMap i0’

     NB: ‘IxMap’ is a type function, and may not be injective

     The type variable ‘i0’ is ambiguous

     Expected type: IxMap (l :|: r) [Int]

       Actual type: BiApp (IxMap i0) (IxMap i1) [Int]

     Relevant bindings include

-      empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:15:4)

+      empty :: IxMap (l :|: r) [Int] (bound at T2544.hs:17:4)

     In the expression: BiApp empty empty

     In an equation for ‘empty’: empty = BiApp empty empty

diff --git a/testsuite/tests/module/all.T b/testsuite/tests/module/all.T
index c86a5f8806..1507ffb0d5 100644
--- a/testsuite/tests/module/all.T
+++ b/testsuite/tests/module/all.T
@@ -57,7 +57,7 @@ test('mod35', normal, compile, [''])
 test('mod36', normal, compile_fail, [''])
 test('mod37', normal, compile, [''])
 test('mod38', normal, compile_fail, [''])
-test('mod39', normal, compile, [''])
+test('mod39', normal, compile_fail, [''])
 test('mod40', normal, compile_fail, [''])
 test('mod41', normal, compile_fail, [''])
 test('mod42', normal, compile_fail, [''])
diff --git a/testsuite/tests/module/mod39.stderr b/testsuite/tests/module/mod39.stderr
new file mode 100644
index 0000000000..3c049f2532
--- /dev/null
+++ b/testsuite/tests/module/mod39.stderr
@@ -0,0 +1,7 @@
+

+mod39.hs:3:17:

+    Constraint ‘Eq a’ in the type of ‘f’

+      constrains only the class type variables

+    Use ConstrainedClassMethods to allow it

+    When checking the class method: f :: forall a. (C a, Eq a) => a

+    In the class declaration for ‘C’

diff --git a/testsuite/tests/polykinds/T8566.hs b/testsuite/tests/polykinds/T8566.hs
index ee5892ce25..248febb586 100644
--- a/testsuite/tests/polykinds/T8566.hs
+++ b/testsuite/tests/polykinds/T8566.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}  -- 'c' is ambiguous
 
 module T8566 where
 
diff --git a/testsuite/tests/polykinds/T8566.stderr b/testsuite/tests/polykinds/T8566.stderr
index 096f058791..168e890404 100644
--- a/testsuite/tests/polykinds/T8566.stderr
+++ b/testsuite/tests/polykinds/T8566.stderr
@@ -1,19 +1,19 @@
-
-T8566.hs:31:9:
-    Could not deduce (C ('AA (t (I a ps)) as) ps fs0)
-      arising from a use of ‘c’
-    from the context: C ('AA (t (I a ps)) as) ps fs
-      bound by the instance declaration at T8566.hs:29:10-67
-    or from: 'AA t (a : as) ~ 'AA t1 as1
-      bound by a pattern with constructor:
-                 A :: forall (r :: [*]) (k :: BOX) (t :: k) (as :: [U *]).
-                      I ('AA t as) r,
-               in an equation for ‘c’
-      at T8566.hs:31:5
-    The type variable ‘fs0’ is ambiguous
-    Relevant bindings include
-      c :: I ('AA t (a : as)) ps -> I ('AA t (a : as)) ps
-        (bound at T8566.hs:31:3)
-    In the expression: c undefined
-    In an equation for ‘c’: c A = c undefined
-    In the instance declaration for ‘C ('AA t (a : as)) ps fs’
+

+T8566.hs:32:9:

+    Could not deduce (C ('AA (t (I a ps)) as) ps fs0)

+      arising from a use of ‘c’

+    from the context: C ('AA (t (I a ps)) as) ps fs

+      bound by the instance declaration at T8566.hs:30:10-67

+    or from: 'AA t (a : as) ~ 'AA t1 as1

+      bound by a pattern with constructor:

+                 A :: forall (r :: [*]) (k :: BOX) (t :: k) (as :: [U *]).

+                      I ('AA t as) r,

+               in an equation for ‘c’

+      at T8566.hs:32:5

+    The type variable ‘fs0’ is ambiguous

+    Relevant bindings include

+      c :: I ('AA t (a : as)) ps -> I ('AA t (a : as)) ps

+        (bound at T8566.hs:32:3)

+    In the expression: c undefined

+    In an equation for ‘c’: c A = c undefined

+    In the instance declaration for ‘C ('AA t (a : as)) ps fs’

diff --git a/testsuite/tests/polykinds/T9200.hs b/testsuite/tests/polykinds/T9200.hs
index ca050661a2..740536a516 100644
--- a/testsuite/tests/polykinds/T9200.hs
+++ b/testsuite/tests/polykinds/T9200.hs
@@ -2,12 +2,13 @@
              TypeFamilies #-}
 
 module T9200 where
+import Data.Proxy
 
 ------
 -- test CUSK on classes
 
 class C (f :: k) (a :: k2) where
-  c_meth :: D a => ()
+  c_meth :: D a => Proxy f -> Proxy a -> ()
   
 class C () a => D a
 
diff --git a/testsuite/tests/roles/should_compile/Roles3.hs b/testsuite/tests/roles/should_compile/Roles3.hs
index 4c26f0d986..3df74ec8e2 100644
--- a/testsuite/tests/roles/should_compile/Roles3.hs
+++ b/testsuite/tests/roles/should_compile/Roles3.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE TypeFamilies, MultiParamTypeClasses #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}  -- meth3, meth4 are ambiguous
 
 module Roles3 where
 
diff --git a/testsuite/tests/th/TH_tf2.hs b/testsuite/tests/th/TH_tf2.hs
index 94be291324..399731a7f6 100644
--- a/testsuite/tests/th/TH_tf2.hs
+++ b/testsuite/tests/th/TH_tf2.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}  -- 'bar' is ambiguous
 
 module TH_tf2 where
 
diff --git a/testsuite/tests/typecheck/should_compile/tc165.hs b/testsuite/tests/typecheck/should_compile/tc165.hs
index ea2fa08ec1..0533c80ca8 100644
--- a/testsuite/tests/typecheck/should_compile/tc165.hs
+++ b/testsuite/tests/typecheck/should_compile/tc165.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE ConstrainedClassMethods #-}
 {-# OPTIONS_GHC -dcore-lint #-}
 
 -- Fails GHC 5.04.2 with -dcore-lint
diff --git a/testsuite/tests/typecheck/should_compile/tc199.hs b/testsuite/tests/typecheck/should_compile/tc199.hs
index d530cfd6d0..dfa2c1f230 100644
--- a/testsuite/tests/typecheck/should_compile/tc199.hs
+++ b/testsuite/tests/typecheck/should_compile/tc199.hs
@@ -1,7 +1,8 @@
-{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE MultiParamTypeClasses, AllowAmbiguousTypes #-}
 
 -- This code defines a default method with a highly dubious type,
 -- because 'v' is not mentioned, and there are no fundeps
+-- Hence needing AllowAmbiguousTypes
 --
 -- However, arguably the instance declaration should be accepted,
 -- beause it's equivalent to 
diff --git a/testsuite/tests/typecheck/should_compile/tc200.hs b/testsuite/tests/typecheck/should_compile/tc200.hs
index bb6a00e1ae..ef799c61d1 100644
--- a/testsuite/tests/typecheck/should_compile/tc200.hs
+++ b/testsuite/tests/typecheck/should_compile/tc200.hs
@@ -1,4 +1,5 @@
 {-# OPTIONS_GHC -w #-}
+{-# LANGUAGE ConstrainedClassMethods #-}  -- Needed for 'baz'
 
 -- A nasty case that crashed GHC 6.4 with a Lint error; 
 -- see Note [Multiple instantiation] in TcExpr
diff --git a/testsuite/tests/typecheck/should_compile/tc235.hs b/testsuite/tests/typecheck/should_compile/tc235.hs
index 55a1a5855d..4973ec1b33 100644
--- a/testsuite/tests/typecheck/should_compile/tc235.hs
+++ b/testsuite/tests/typecheck/should_compile/tc235.hs
@@ -1,6 +1,8 @@
 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 {-# LANGUAGE FlexibleInstances, UndecidableInstances,
              MultiParamTypeClasses, FunctionalDependencies #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+    -- 'x' and 'v' are ambiguous
 
 -- Trac #1564
 
diff --git a/testsuite/tests/typecheck/should_compile/tc259.hs b/testsuite/tests/typecheck/should_compile/tc259.hs
index 776bd8416b..6ece4a29ca 100644
--- a/testsuite/tests/typecheck/should_compile/tc259.hs
+++ b/testsuite/tests/typecheck/should_compile/tc259.hs
@@ -1,5 +1,8 @@
 -- Test we don't get a cycle for "phantom" superclasses
 {-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, FlexibleContexts #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+    -- 'meth' is ambiguous
+
 module TcOK where
 
 class A cls c where
diff --git a/testsuite/tests/typecheck/should_compile/tc260.hs b/testsuite/tests/typecheck/should_compile/tc260.hs
index 29baeee903..3a4d9b0d8d 100644
--- a/testsuite/tests/typecheck/should_compile/tc260.hs
+++ b/testsuite/tests/typecheck/should_compile/tc260.hs
@@ -1,6 +1,9 @@
 -- Test we don't get a cycle for "phantom" superclasses,
 -- even if the phantomness is behind a type synonym
 {-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, FlexibleContexts #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+    -- 'meth' is ambiguous
+
 module TcOK where
 
 class A ctxt c where
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 60c709760e..20eede0f96 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -133,7 +133,7 @@ test('tcfail146', normal, compile_fail, [''])
 test('tcfail147', normal, compile_fail, [''])
 test('tcfail148', normal, compile_fail, [''])
 test('tcfail149', normal, compile_and_run, [''])
-test('tcfail150', normal, compile, [''])
+test('tcfail150', normal, compile_fail, [''])
 test('tcfail151', normal, compile_fail, [''])
 test('tcfail152', normal, compile_fail, [''])
 test('tcfail153', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail116.stderr b/testsuite/tests/typecheck/should_fail/tcfail116.stderr
index 0136173201..abefc61eb8 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail116.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail116.stderr
@@ -1,6 +1,12 @@
-
-tcfail116.hs:5:1:
-    The class method ‘bug’
-    mentions none of the type or kind variables of the class ‘Foo a’
-    When checking the class method: bug :: ()
-    In the class declaration for ‘Foo’
+

+tcfail116.hs:6:5:

+    Could not deduce (Foo a0)

+    from the context: Foo a

+      bound by the type signature for: bug :: Foo a => ()

+      at tcfail116.hs:6:5-13

+    The type variable ‘a0’ is ambiguous

+    In the ambiguity check for the type signature for ‘bug’:

+      bug :: forall a. Foo a => ()

+    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes

+    When checking the class method: bug :: forall a. Foo a => ()

+    In the class declaration for ‘Foo’

diff --git a/testsuite/tests/typecheck/should_fail/tcfail149.hs b/testsuite/tests/typecheck/should_fail/tcfail149.hs
index 2479ed75c8..090db8de22 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail149.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail149.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE ConstrainedClassMethods #-}
+
 module Main where
 
 class C a where
diff --git a/testsuite/tests/typecheck/should_fail/tcfail150.stderr b/testsuite/tests/typecheck/should_fail/tcfail150.stderr
index e69de29bb2..c91d404c13 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail150.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail150.stderr
@@ -0,0 +1,8 @@
+

+tcfail150.hs:6:3:

+    Constraint ‘Eq a’ in the type of ‘op’

+      constrains only the class type variables

+    Use ConstrainedClassMethods to allow it

+    When checking the class method:

+      op :: forall a. (Foo a, Eq a) => a -> a

+    In the class declaration for ‘Foo’

diff --git a/testsuite/tests/typecheck/should_fail/tcfail151.hs b/testsuite/tests/typecheck/should_fail/tcfail151.hs
index 00578a1eb2..51cf65d5cd 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail151.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail151.hs
@@ -2,7 +2,7 @@
 module ShouldFail where
 
 class (Show a, Eq a, Monad m) => Name m a where 
-    hashName :: a -> Int 
+    hashName :: a -> m Int 
     newName :: m a 
  
 data Name a => Exp a = MkExp a