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}

3 files changed, 7 insertions, 5 deletions

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’