Remove some redundant validity checks.

This commit also consolidates documentation in the user
manual around UndecidableSuperClasses, UndecidableInstances,
and FlexibleContexts.

Close #19186.
Close #19187.

Test case: typecheck/should_compile/T19186,
typecheck/should_fail/T19187{,a}

40 files changed, 114 insertions, 218 deletions

diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 7a83bfc573..f66c768c57 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -1182,7 +1182,7 @@ check_pred_help under_syn env dflags ctxt pred
               -- in Note [Lift equality constraints when quantifying] in GHC.Tc.Utils.TcType
 
       ForAllPred _ theta head -> check_quant_pred env dflags ctxt pred theta head
-      IrredPred {}            -> check_irred_pred under_syn env dflags ctxt pred
+      IrredPred {}            -> check_irred_pred under_syn env dflags pred
 
 check_eq_pred :: TidyEnv -> DynFlags -> PredType -> TcM ()
 check_eq_pred env dflags pred
@@ -1224,30 +1224,17 @@ check_tuple_pred under_syn env dflags ctxt pred ts
     -- This case will not normally be executed because without
     -- -XConstraintKinds tuple types are only kind-checked as *
 
-check_irred_pred :: Bool -> TidyEnv -> DynFlags -> UserTypeCtxt -> PredType -> TcM ()
-check_irred_pred under_syn env dflags ctxt pred
+check_irred_pred :: Bool -> TidyEnv -> DynFlags -> PredType -> TcM ()
+check_irred_pred under_syn env dflags pred
     -- The predicate looks like (X t1 t2) or (x t1 t2) :: Constraint
     -- where X is a type function
-  = do { -- If it looks like (x t1 t2), require ConstraintKinds
+  =      -- If it looks like (x t1 t2), require ConstraintKinds
          --   see Note [ConstraintKinds in predicates]
          -- But (X t1 t2) is always ok because we just require ConstraintKinds
          -- at the definition site (#9838)
-        failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags)
-                                && hasTyVarHead pred)
-                  (predIrredErr env pred)
-
-         -- Make sure it is OK to have an irred pred in this context
-         -- See Note [Irreducible predicates in superclasses]
-       ; failIfTcM (is_superclass ctxt
-                    && not (xopt LangExt.UndecidableInstances dflags)
-                    && has_tyfun_head pred)
-                   (predSuperClassErr env pred) }
-  where
-    is_superclass ctxt = case ctxt of { ClassSCCtxt _ -> True; _ -> False }
-    has_tyfun_head ty
-      = case tcSplitTyConApp_maybe ty of
-          Just (tc, _) -> isTypeFamilyTyCon tc
-          Nothing      -> False
+    failIfTcM (not under_syn && not (xopt LangExt.ConstraintKinds dflags)
+                            && hasTyVarHead pred)
+              (predIrredErr env pred)
 
 {- Note [ConstraintKinds in predicates]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1258,19 +1245,7 @@ e.g.   module A where
        module B where
           import A
           f :: C a => a -> a        -- Does *not* need -XConstraintKinds
-
-Note [Irreducible predicates in superclasses]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Allowing type-family calls in class superclasses is somewhat dangerous
-because we can write:
-
- type family Fooish x :: * -> Constraint
- type instance Fooish () = Foo
- class Fooish () a => Foo a where
-
-This will cause the constraint simplifier to loop because every time we canonicalise a
-(Foo a) class constraint we add a (Fooish () a) constraint which will be immediately
-solved to add+canonicalise another (Foo a) constraint.  -}
+-}
 
 -------------------------
 check_class_pred :: TidyEnv -> DynFlags -> UserTypeCtxt
@@ -1294,10 +1269,9 @@ check_class_pred env dflags ctxt pred cls tys
 
     -- Check the arguments of a class constraint
     flexible_contexts = xopt LangExt.FlexibleContexts     dflags
-    undecidable_ok    = xopt LangExt.UndecidableInstances dflags
     arg_tys_ok = case ctxt of
         SpecInstCtxt -> True    -- {-# SPECIALISE instance Eq (T Int) #-} is fine
-        InstDeclCtxt {} -> checkValidClsArgs (flexible_contexts || undecidable_ok) cls tys
+        InstDeclCtxt {} -> checkValidClsArgs flexible_contexts cls tys
                                 -- Further checks on head and theta
                                 -- in checkInstTermination
         _               -> checkValidClsArgs flexible_contexts cls tys
@@ -1431,7 +1405,7 @@ checkThetaCtxt ctxt theta env
                   , text "While checking" <+> pprUserTypeCtxt ctxt ] )
 
 eqPredTyErr, predTupleErr, predIrredErr,
-   predSuperClassErr, badQuantHeadErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
+   badQuantHeadErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
 badQuantHeadErr env pred
   = ( env
     , hang (text "Quantified predicate must have a class or type variable head:")
@@ -1448,11 +1422,6 @@ predIrredErr env pred
   = ( env
     , hang (text "Illegal constraint:" <+> ppr_tidy env pred)
          2 (parens constraintKindsMsg) )
-predSuperClassErr env pred
-  = ( env
-    , hang (text "Illegal constraint" <+> quotes (ppr_tidy env pred)
-            <+> text "in a superclass context")
-         2 (parens undecidableMsg) )
 
 predTyVarErr :: TidyEnv -> PredType -> (TidyEnv, SDoc)
 predTyVarErr env pred
diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst
index 717da75c33..a38e334cd6 100644
--- a/docs/users_guide/9.2.1-notes.rst
+++ b/docs/users_guide/9.2.1-notes.rst
@@ -47,6 +47,10 @@ Language
         -- Alternatively,
         -- type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> Type)
 
+* Previously, ``-XUndecidableInstances`` accidentally implied ``-XFlexibleContexts``.
+  This is now fixed, but it means that some programs will newly require
+  ``-XFlexibleContexts``.
+        
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/exts/constraints.rst b/docs/users_guide/exts/constraints.rst
index 6011dd6ea7..d52392b3b8 100644
--- a/docs/users_guide/exts/constraints.rst
+++ b/docs/users_guide/exts/constraints.rst
@@ -4,6 +4,7 @@ Constraints
 .. toctree::
     :maxdepth: 1
 
+    flexible_contexts
     equality_constraints
     constraint_kind
     quantified_constraints
diff --git a/docs/users_guide/exts/flexible_contexts.rst b/docs/users_guide/exts/flexible_contexts.rst
index 7823a36bec..9bfccfda2a 100644
--- a/docs/users_guide/exts/flexible_contexts.rst
+++ b/docs/users_guide/exts/flexible_contexts.rst
@@ -1,54 +1,26 @@
-.. _superclass-rules:
+.. _flexible-contexts:
 
-Flexible contexts
------------------
+Loosening restrictions on class contexts
+----------------------------------------
 
 .. extension:: FlexibleContexts
-    :shortdesc: Enable flexible contexts.
+    :shortdesc: Remove some restrictions on class contexts
 
     :since: 6.8.1
 
-    Allow the use of complex constraints in class declaration contexts.
+    Remove the type-variable restriction on class contexts.
 
-In Haskell 98 the context of a class declaration (which introduces
-superclasses) must be simple; that is, each predicate must consist of a
-class applied to type variables. The extension :extension:`FlexibleContexts`
-(:ref:`flexible-contexts`) lifts this restriction, so that the only
-restriction on the context in a class declaration is that the class
-hierarchy must be acyclic. So these class declarations are OK: ::
-
-      class Functor (m k) => FiniteMap m k where
-        ...
-
-      class (Monad m, Monad (t m)) => Transform t m where
-        lift :: m a -> (t m) a
-
-As in Haskell 98, the class hierarchy must be acyclic. However, the
-definition of "acyclic" involves only the superclass relationships. For
-example, this is okay: ::
-
-      class C a where
-        op :: D b => a -> b -> b
-
-      class C a => D a where ...
-
-Here, ``C`` is a superclass of ``D``, but it's OK for a class operation
-``op`` of ``C`` to mention ``D``. (It would not be OK for ``D`` to be a
-superclass of ``C``.)
-
-With the extension that adds a :ref:`kind of
-constraints <constraint-kind>`, you can write more exotic superclass
-definitions. The superclass cycle check is even more liberal in these
-cases. For example, this is OK: ::
-
-      class A cls c where
-        meth :: cls c => c -> c
-
-      class A B c => B c where
-
-A superclass context for a class ``C`` is allowed if, after expanding
-type synonyms to their right-hand-sides, and uses of classes (other than
-``C``) to their superclasses, ``C`` does not occur syntactically in the
-context.
+The :extension:`FlexibleContexts` extension lifts the Haskell 98 restriction that
+the type-class constraints (anywhere they appear) must have the form *(class
+type-variable)* or *(class (type-variable type1 type2 ... typen))*. With
+:extension:`FlexibleContexts` these type signatures are perfectly okay::
 
+      g :: Eq [a] => ...
+      g :: Ord (T a ()) => ...
 
+This extension does not affect equality constraints in an instance
+context; they are permitted by :extension:`TypeFamilies` or :extension:`GADTs`.
+      
+Note that :extension:`FlexibleContexts` affects usages of class constraints,
+in type signatures and other contexts. In contrast, :extension:`FlexibleInstances`
+loosens a similar restriction in place when declaring a new instance.
diff --git a/docs/users_guide/exts/flexible_contexts_signature.rst b/docs/users_guide/exts/flexible_contexts_signature.rst
deleted file mode 100644
index cd2bd2866b..0000000000
--- a/docs/users_guide/exts/flexible_contexts_signature.rst
+++ /dev/null
@@ -1,19 +0,0 @@
-.. _flexible-contexts:
-
-The context of a type signature
--------------------------------
-
-The :extension:`FlexibleContexts` extension lifts the Haskell 98 restriction that
-the type-class constraints in a type signature must have the form *(class
-type-variable)* or *(class (type-variable type1 type2 ... typen))*. With
-:extension:`FlexibleContexts` these type signatures are perfectly okay
-::
-
-      g :: Eq [a] => ...
-      g :: Ord (T a ()) => ...
-
-The flag :extension:`FlexibleContexts` also lifts the corresponding restriction
-on class declarations (:ref:`superclass-rules`) and instance
-declarations (:ref:`instance-rules`).
-
-
diff --git a/docs/users_guide/exts/instances.rst b/docs/users_guide/exts/instances.rst
index 4dfb7e1ecb..01655bb05b 100644
--- a/docs/users_guide/exts/instances.rst
+++ b/docs/users_guide/exts/instances.rst
@@ -173,27 +173,8 @@ syntactically allowed. Some further various observations about this grammar:
   instance, ``instance (C a)`` is accepted, as is ``instance forall a. (C a)``.
 
 .. _instance-rules:
-
-Relaxed rules for instance contexts
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-In Haskell 98, the class constraints in the context of the instance
-declaration must be of the form ``C a`` where ``a`` is a type variable
-that occurs in the head.
-
-The :extension:`FlexibleContexts` extension relaxes this rule, as well as relaxing
-the corresponding rule for type signatures (see
-:ref:`flexible-contexts`). Specifically, :extension:`FlexibleContexts`, allows
-(well-kinded) class constraints of form ``(C t1 ... tn)`` in the context
-of an instance declaration.
-
-Notice that the extension does not affect equality constraints in an instance
-context; they are permitted by :extension:`TypeFamilies` or :extension:`GADTs`.
-
-However, the instance declaration must still conform to the rules for
-instance termination: see :ref:`instance-termination`.
-
 .. _instance-termination:
+.. _undecidable-instances:
 
 Instance termination rules
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -284,60 +265,6 @@ because the derived instance
 
 conforms to the above rules.
 
-A useful idiom permitted by the above rules is as follows. If one allows
-overlapping instance declarations then it's quite convenient to have a
-"default instance" declaration that applies if something more specific
-does not:
-
-::
-
-      instance C a where
-        op = ... -- Default
-
-.. _undecidable-instances:
-
-Undecidable instances
-~~~~~~~~~~~~~~~~~~~~~
-
-.. index::
-   single: -XUndecidableInstances
-
-Sometimes even the termination rules of :ref:`instance-termination` are
-too onerous. So GHC allows you to experiment with more liberal rules: if
-you use the experimental extension :extension:`UndecidableInstances`, both the Paterson
-Conditions and the Coverage
-Condition (described in :ref:`instance-termination`) are lifted.
-Termination is still ensured by having a fixed-depth recursion stack. If
-you exceed the stack depth you get a sort of backtrace, and the
-opportunity to increase the stack depth with
-``-freduction-depth=⟨n⟩``. However, if you should exceed the default
-reduction depth limit, it is probably best just to disable depth
-checking, with ``-freduction-depth=0``. The exact depth your program
-requires depends on minutiae of your code, and it may change between
-minor GHC releases. The safest bet for released code -- if you're sure
-that it should compile in finite time -- is just to disable the check.
-
-For example, sometimes you might want to use the following to get the
-effect of a "class synonym":
-
-::
-
-      class (C1 a, C2 a, C3 a) => C a where { }
-
-      instance (C1 a, C2 a, C3 a) => C a where { }
-
-This allows you to write shorter signatures:
-
-::
-
-      f :: C a => ...
-
-instead of
-
-::
-
-      f :: (C1 a, C2 a, C3 a) => ...
-
 The restrictions on functional dependencies
 (:ref:`functional-dependencies`) are particularly troublesome. It is
 tempting to introduce type variables in the context that do not appear
@@ -509,6 +436,7 @@ As a more substantial example of the rules in action, consider ::
       instance {-# OVERLAPPABLE #-} context3 => C a   [b]   where ...  -- (C)
       instance {-# OVERLAPPING  #-} context4 => C Int [Int] where ...  -- (D)
 
+(These all need :extension:`FlexibleInstances`.)
 Now suppose that the type inference engine needs to solve the constraint
 ``C Int [Int]``. This constraint matches instances (A), (C) and (D), but
 the last is more specific, and hence is chosen.
@@ -521,7 +449,7 @@ accepted and (A) or (C) would be chosen arbitrarily.
 An instance declaration is *more specific* than another iff the head of
 former is a substitution instance of the latter. For example (D) is
 "more specific" than (C) because you can get from (C) to (D) by
-substituting ``a := Int``.
+substituting ``a := Int`` and ``b := Int``.
 
 The final bullet (about unifying instances)
 makes GHC conservative about committing to an
@@ -549,8 +477,8 @@ the type ::
       f :: C b [b] => [b] -> [b]
 
 That postpones the question of which instance to pick to the call site
-for ``f`` by which time more is known about the type ``b``. You can
-write this type signature yourself if you use the
+for ``f`` by which time more is known about the type ``b``. You
+will need the
 :extension:`FlexibleContexts` extension.
 
 Exactly the same situation can arise in instance declarations
@@ -571,7 +499,7 @@ declaration, thus: ::
       instance C Int [b] => Foo [b] where
          f x = ...
 
-(You need :extension:`FlexibleInstances` to do this.)
+(You need :extension:`FlexibleContexts` to do this.)
 
 In the unification check in the final bullet, GHC also uses the
 "in-scope given constraints".  Consider for example ::
diff --git a/docs/users_guide/exts/type_signatures.rst b/docs/users_guide/exts/type_signatures.rst
index 19eec9d27f..9d0fcdc5bb 100644
--- a/docs/users_guide/exts/type_signatures.rst
+++ b/docs/users_guide/exts/type_signatures.rst
@@ -7,7 +7,6 @@ Type signatures
     :maxdepth: 1
 
     explicit_forall
-    flexible_contexts_signature
     ambiguous_types
     kind_signatures
     scoped_type_variables
diff --git a/docs/users_guide/exts/typeclasses.rst b/docs/users_guide/exts/typeclasses.rst
index f3f63f6f5d..41aa4d985e 100644
--- a/docs/users_guide/exts/typeclasses.rst
+++ b/docs/users_guide/exts/typeclasses.rst
@@ -13,7 +13,6 @@ space <http://research.microsoft.com/~simonpj/Papers/type-class-design-space/>`_
     :maxdepth: 1
 
     multi_param_type_classes
-    flexible_contexts
     undecidable_super_classes
     constrained_class_methods
     default_signatures
diff --git a/docs/users_guide/exts/undecidable_super_classes.rst b/docs/users_guide/exts/undecidable_super_classes.rst
index c984b375d8..ed55da29a9 100644
--- a/docs/users_guide/exts/undecidable_super_classes.rst
+++ b/docs/users_guide/exts/undecidable_super_classes.rst
@@ -1,3 +1,5 @@
+.. _superclass-rules:
+
 Undecidable (or recursive) superclasses
 ---------------------------------------
 
diff --git a/testsuite/tests/deriving/should_fail/T11509_1.hs b/testsuite/tests/deriving/should_fail/T11509_1.hs
index ee088c3876..861d39453e 100644
--- a/testsuite/tests/deriving/should_fail/T11509_1.hs
+++ b/testsuite/tests/deriving/should_fail/T11509_1.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE ConstraintKinds            #-}
+{-# LANGUAGE FlexibleContexts           #-}
 {-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE GADTs                      #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
diff --git a/testsuite/tests/deriving/should_fail/T11509_1.stderr b/testsuite/tests/deriving/should_fail/T11509_1.stderr
index a50310e50b..305e8e8307 100644
--- a/testsuite/tests/deriving/should_fail/T11509_1.stderr
+++ b/testsuite/tests/deriving/should_fail/T11509_1.stderr
@@ -1,5 +1,5 @@
 
-T11509_1.hs:52:1: error:
+T11509_1.hs:53:1: error:
     • Can't make a derived instance of ‘SC (Serializable (MyList a))’:
         ‘Serializable’ is a type class, and can only have a derived instance
         if DeriveAnyClass is enabled
diff --git a/testsuite/tests/deriving/should_fail/drvfail002.hs b/testsuite/tests/deriving/should_fail/drvfail002.hs
index 945ead493e..cdaaa5d6be 100644
--- a/testsuite/tests/deriving/should_fail/drvfail002.hs
+++ b/testsuite/tests/deriving/should_fail/drvfail002.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE UndecidableInstances,
+{-# LANGUAGE UndecidableInstances, FlexibleContexts,
              MultiParamTypeClasses, FunctionalDependencies #-}
 
 -- The Show instance for S would have form
@@ -17,4 +17,3 @@ instance X T c => Show T where
     show _ = ""
 
 data S = S T deriving Show
-
diff --git a/testsuite/tests/perf/compiler/T12227.hs b/testsuite/tests/perf/compiler/T12227.hs
index 9be515f083..8016987724 100644
--- a/testsuite/tests/perf/compiler/T12227.hs
+++ b/testsuite/tests/perf/compiler/T12227.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE ScopedTypeVariables #-}
diff --git a/testsuite/tests/polykinds/T7973.hs b/testsuite/tests/polykinds/T7973.hs
index 44e3ac0468..0053858d81 100644
--- a/testsuite/tests/polykinds/T7973.hs
+++ b/testsuite/tests/polykinds/T7973.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds, PolyKinds, KindSignatures #-}
-{-# LANGUAGE ExistentialQuantification, UndecidableInstances, TypeFamilies #-}
+{-# LANGUAGE ExistentialQuantification, UndecidableInstances, TypeFamilies,
+             FlexibleContexts #-}
 
 module Test where
 
diff --git a/testsuite/tests/polykinds/T8566.hs b/testsuite/tests/polykinds/T8566.hs
index 2ffdecfd6e..a31a54855f 100644
--- a/testsuite/tests/polykinds/T8566.hs
+++ b/testsuite/tests/polykinds/T8566.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
diff --git a/testsuite/tests/polykinds/T8566.stderr b/testsuite/tests/polykinds/T8566.stderr
index 0e4b6a8fff..d67f47c771 100644
--- a/testsuite/tests/polykinds/T8566.stderr
+++ b/testsuite/tests/polykinds/T8566.stderr
@@ -1,19 +1,19 @@
 
-T8566.hs:34:9: error:
+T8566.hs:35:9: error:
     • 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:32:10-67
+        bound by the instance declaration at T8566.hs:33:10-67
       or from: 'AA t (a : as) ~ 'AA t1 as1
         bound by a pattern with constructor:
                    A :: forall {v} (t :: v) (as :: [U (*)]) (r :: [*]).
                         I ('AA t as) r,
                  in an equation for ‘c’
-        at T8566.hs:34:5
+        at T8566.hs:35: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:34:3)
+          (bound at T8566.hs:35: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/programs/thurston-modular-arith/TypeVal.hs b/testsuite/tests/programs/thurston-modular-arith/TypeVal.hs
index 8562d89482..0e7219cbbd 100644
--- a/testsuite/tests/programs/thurston-modular-arith/TypeVal.hs
+++ b/testsuite/tests/programs/thurston-modular-arith/TypeVal.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts,
              UndecidableInstances, ExistentialQuantification,
              ScopedTypeVariables #-}
 
@@ -86,4 +86,3 @@ instance (ValToType a) => ValToType [a] where
                      case valToType xs of {Wrapper xs' ->
                      case xs' of {(_::xst) ->
                      Wrapper (undefined::CONS xt xst)}}}}
-
diff --git a/testsuite/tests/typecheck/should_compile/FD4.hs b/testsuite/tests/typecheck/should_compile/FD4.hs
index 88444772ec..67be08fdfc 100644
--- a/testsuite/tests/typecheck/should_compile/FD4.hs
+++ b/testsuite/tests/typecheck/should_compile/FD4.hs
@@ -3,7 +3,8 @@
     FunctionalDependencies,
     UndecidableInstances,
     FlexibleInstances,
-    EmptyDataDecls #-}
+    EmptyDataDecls,
+    FlexibleContexts #-}
 
 -- #1797
 
diff --git a/testsuite/tests/typecheck/should_compile/LoopOfTheDay1.hs b/testsuite/tests/typecheck/should_compile/LoopOfTheDay1.hs
index 713c6b3f29..fe3e259160 100644
--- a/testsuite/tests/typecheck/should_compile/LoopOfTheDay1.hs
+++ b/testsuite/tests/typecheck/should_compile/LoopOfTheDay1.hs
@@ -1,5 +1,6 @@
 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances,
+             FlexibleContexts #-}
 
 -- Compiles fine.
 -- Instance selection works fine.
diff --git a/testsuite/tests/typecheck/should_compile/LoopOfTheDay2.hs b/testsuite/tests/typecheck/should_compile/LoopOfTheDay2.hs
index dd17a9fcc9..9af9fb2d4b 100644
--- a/testsuite/tests/typecheck/should_compile/LoopOfTheDay2.hs
+++ b/testsuite/tests/typecheck/should_compile/LoopOfTheDay2.hs
@@ -1,5 +1,6 @@
 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, UndecidableInstances,
+             FlexibleContexts #-}
 
 -- Compilation loops in GHC 6.2!
 -- While LoopOfTheDay1.hs did compile and work,
diff --git a/testsuite/tests/typecheck/should_compile/LoopOfTheDay3.hs b/testsuite/tests/typecheck/should_compile/LoopOfTheDay3.hs
index f83b151cb1..61dc5e5db6 100644
--- a/testsuite/tests/typecheck/should_compile/LoopOfTheDay3.hs
+++ b/testsuite/tests/typecheck/should_compile/LoopOfTheDay3.hs
@@ -1,13 +1,13 @@
 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
 {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
-             UndecidableInstances #-}
+             UndecidableInstances, FlexibleContexts #-}
 
 -- Instances compile fine but instance selection loops in GHC 6.2.
 -- try: :t foo (T1a 1)
 -- This is essentially the same as LoopOfTheDay2.hs
 -- but with the innocent (?) use of overlapping instances.
 
-module ShouldCompile where 
+module ShouldCompile where
 
 data T1 = T1a Int | T1b T1
 
diff --git a/testsuite/tests/typecheck/should_compile/T19186.hs b/testsuite/tests/typecheck/should_compile/T19186.hs
new file mode 100644
index 0000000000..8d98a1b0d0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T19186.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, UndecidableSuperClasses #-}
+
+module T19186 where
+
+import Data.Kind
+
+type family F a :: Constraint
+
+class F a => C a
diff --git a/testsuite/tests/typecheck/should_compile/T3018.hs b/testsuite/tests/typecheck/should_compile/T3018.hs
index 77b656af17..42fcc49f10 100644
--- a/testsuite/tests/typecheck/should_compile/T3018.hs
+++ b/testsuite/tests/typecheck/should_compile/T3018.hs
@@ -1,6 +1,7 @@
 {-# OPTIONS_GHC -w #-}
 {-# LANGUAGE UndecidableInstances, EmptyDataDecls #-}
-{-# LANGUAGE RankNTypes, KindSignatures, MultiParamTypeClasses, FlexibleInstances #-}
+{-# LANGUAGE RankNTypes, KindSignatures, MultiParamTypeClasses, FlexibleInstances,
+             FlexibleContexts #-}
 
 -- Works with new constraint solver
 
diff --git a/testsuite/tests/typecheck/should_compile/T3108.hs b/testsuite/tests/typecheck/should_compile/T3108.hs
index 3611bbc02b..9d5e3045a1 100644
--- a/testsuite/tests/typecheck/should_compile/T3108.hs
+++ b/testsuite/tests/typecheck/should_compile/T3108.hs
@@ -1,6 +1,6 @@
 {-# OPTIONS_GHC -Wno-redundant-constraints -Wno-simplifiable-class-constraints #-}
 {-# LANGUAGE UndecidableInstances, MultiParamTypeClasses,
-             FunctionalDependencies, FlexibleInstances #-}
+             FunctionalDependencies, FlexibleInstances, FlexibleContexts #-}
 
 module T3108 where
 
diff --git a/testsuite/tests/typecheck/should_compile/T6055.hs b/testsuite/tests/typecheck/should_compile/T6055.hs
index 289c66475a..caf50dc94f 100644
--- a/testsuite/tests/typecheck/should_compile/T6055.hs
+++ b/testsuite/tests/typecheck/should_compile/T6055.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE FlexibleContexts #-}
 module T6055 where
 
 data Int1  = Int1
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 44e60ea55c..3842a1984c 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -706,6 +706,7 @@ test('T12926', reqlib('vector'), compile, ['-O2'])
 test('T17710', normal, compile, [''])
 test('T17792', normal, compile, [''])
 test('T17024', normal, compile, [''])
+test('T19186', normal, compile, [''])
 test('T17021a', normal, compile, [''])
 test('T18005', normal, compile, [''])
 test('T18023', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/tc177.hs b/testsuite/tests/typecheck/should_compile/tc177.hs
index c39481db90..90d462a5b0 100644
--- a/testsuite/tests/typecheck/should_compile/tc177.hs
+++ b/testsuite/tests/typecheck/should_compile/tc177.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE FlexibleInstances, UndecidableInstances,
+{-# LANGUAGE FlexibleInstances, UndecidableInstances, FlexibleContexts,
              MultiParamTypeClasses, FunctionalDependencies #-}
 
 -- This is a rather complicated program that uses functional
@@ -105,4 +105,3 @@ instance EqR (Succ n) Zero F where
 
 instance (EqR n1 n2 b) => EqR (Succ n1) (Succ n2) b where
     eqR (Succ n1) (Succ n2) = eqR n1 n2
-
diff --git a/testsuite/tests/typecheck/should_compile/tc180.hs b/testsuite/tests/typecheck/should_compile/tc180.hs
index 205a2225f9..4706bd2743 100644
--- a/testsuite/tests/typecheck/should_compile/tc180.hs
+++ b/testsuite/tests/typecheck/should_compile/tc180.hs
@@ -1,5 +1,5 @@
 {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts,
              FlexibleInstances, UndecidableInstances #-}
 
 -- This tests an aspect of functional dependencies, revealing a bug in GHC 6.0.1
diff --git a/testsuite/tests/typecheck/should_compile/tc229.hs b/testsuite/tests/typecheck/should_compile/tc229.hs
index cf6c98526c..406edf60a3 100644
--- a/testsuite/tests/typecheck/should_compile/tc229.hs
+++ b/testsuite/tests/typecheck/should_compile/tc229.hs
@@ -3,7 +3,7 @@
 -- trac #1406: Constraint doesn't reduce in the presence of quantified
 --             type variables
 
-{-# LANGUAGE FlexibleInstances, UndecidableInstances, RankNTypes,
+{-# LANGUAGE FlexibleInstances, UndecidableInstances, RankNTypes, FlexibleContexts,
              MultiParamTypeClasses, FunctionalDependencies #-}
 
 module Problem where
@@ -35,4 +35,3 @@ thP4' = thr' t_hPrefix
 thr :: (forall r. r -> a) -> a
 thr f = f undefined
 thP4 = thr t_hPrefix
-
diff --git a/testsuite/tests/typecheck/should_fail/ContextStack1.hs b/testsuite/tests/typecheck/should_fail/ContextStack1.hs
index 1515bbaeda..63e4b9e511 100644
--- a/testsuite/tests/typecheck/should_fail/ContextStack1.hs
+++ b/testsuite/tests/typecheck/should_fail/ContextStack1.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE UndecidableInstances, FlexibleInstances #-}
+{-# LANGUAGE UndecidableInstances, FlexibleInstances, FlexibleContexts #-}
 
 module ContextStack1 where
 
@@ -8,4 +8,3 @@ instance Cls [a] => Cls a
 
 t :: ()
 t = meth
-
diff --git a/testsuite/tests/typecheck/should_fail/T19187.hs b/testsuite/tests/typecheck/should_fail/T19187.hs
new file mode 100644
index 0000000000..52f0e11c69
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19187.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module T19187 where
+
+data T
+
+instance Eq Int => Eq T
diff --git a/testsuite/tests/typecheck/should_fail/T19187.stderr b/testsuite/tests/typecheck/should_fail/T19187.stderr
new file mode 100644
index 0000000000..637cd22c4d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19187.stderr
@@ -0,0 +1,5 @@
+
+T19187.hs:7:10: error:
+    • Non type-variable argument in the constraint: Eq Int
+      (Use FlexibleContexts to permit this)
+    • In the instance declaration for ‘Eq T’
diff --git a/testsuite/tests/typecheck/should_fail/T19187a.hs b/testsuite/tests/typecheck/should_fail/T19187a.hs
new file mode 100644
index 0000000000..ea7be4fec9
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19187a.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE FlexibleContexts #-}
+
+module T19187a where
+
+data T
+
+instance Eq Int => Eq T
diff --git a/testsuite/tests/typecheck/should_fail/T19187a.stderr b/testsuite/tests/typecheck/should_fail/T19187a.stderr
new file mode 100644
index 0000000000..32ddde3f39
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19187a.stderr
@@ -0,0 +1,6 @@
+
+T19187a.hs:7:10: error:
+    • The constraint ‘Eq Int’
+        is no smaller than the instance head ‘Eq T’
+      (Use UndecidableInstances to permit this)
+    • In the instance declaration for ‘Eq T’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index e191a736aa..052bdd9201 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -281,6 +281,8 @@ test('T7019', normal, compile_fail,[''])
 test('T7019a', normal, compile_fail,[''])
 test('T5978', normal, compile_fail, [''])
 test('TcMultiWayIfFail', [], compile_fail, [''])
+test('T19187', normal, compile_fail, [''])
+test('T19187a', normal, compile_fail, [''])
 test('T2534', normal, compile_fail, [''])
 test('T7175', normal, compile_fail, [''])
 test('T7210', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail133.hs b/testsuite/tests/typecheck/should_fail/tcfail133.hs
index f22feec9ae..4aded61a27 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail133.hs
+++ b/testsuite/tests/typecheck/should_fail/tcfail133.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE UndecidableInstances, FlexibleInstances, TypeOperators,
+{-# LANGUAGE UndecidableInstances, FlexibleInstances, TypeOperators, FlexibleContexts,
              MultiParamTypeClasses, FunctionalDependencies, DatatypeContexts #-}
 
 -- This one crashed GHC 6.3 due to an error in GHC.Tc.Solver.add_ors
diff --git a/testsuite/tests/typecheck/should_fail/tcfail213.stderr b/testsuite/tests/typecheck/should_fail/tcfail213.stderr
index d9648bf5ca..319a2b10e2 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail213.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail213.stderr
@@ -1,7 +1,7 @@
 
 tcfail213.hs:8:1: error:
-    • Illegal constraint ‘F a’ in a superclass context
-        (Use UndecidableInstances to permit this)
-    • In the context: F a
-      While checking the super-classes of class ‘C’
-      In the class declaration for ‘C’
+    • Potential superclass cycle for ‘C’
+        one of whose superclass constraints is headed by a type family:
+          ‘F a’
+      Use UndecidableSuperClasses to accept this
+    • In the class declaration for ‘C’
diff --git a/testsuite/tests/typecheck/should_run/T5913.hs b/testsuite/tests/typecheck/should_run/T5913.hs
index f5c94d2312..54182bfcd9 100644
--- a/testsuite/tests/typecheck/should_run/T5913.hs
+++ b/testsuite/tests/typecheck/should_run/T5913.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableInstances, FlexibleContexts #-}
 module Main where
 
 class         L0 a where l0 :: a -> a
diff --git a/testsuite/tests/typecheck/should_run/tcrun028.hs b/testsuite/tests/typecheck/should_run/tcrun028.hs
index f4f8fd9d61..4c4625c015 100644
--- a/testsuite/tests/typecheck/should_run/tcrun028.hs
+++ b/testsuite/tests/typecheck/should_run/tcrun028.hs
@@ -1,5 +1,5 @@
 {-# OPTIONS_GHC -dcore-lint #-}
-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies,
+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleContexts,
              FlexibleInstances, UndecidableInstances #-}
 
 -- This is a rather exotic functional-dependency test.
diff --git a/testsuite/tests/typecheck/testeq1/TypeEq.hs b/testsuite/tests/typecheck/testeq1/TypeEq.hs
index 599893cc09..7dcfae1a1a 100644
--- a/testsuite/tests/typecheck/testeq1/TypeEq.hs
+++ b/testsuite/tests/typecheck/testeq1/TypeEq.hs
@@ -1,5 +1,5 @@
 
-{-# LANGUAGE MultiParamTypeClasses,
+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts,
              FlexibleInstances, OverlappingInstances, UndecidableInstances #-}
 
 --