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}

23 files changed, 62 insertions, 23 deletions

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