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}

31 files changed, 74 insertions, 33 deletions

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 #-}
 
 --