Improve error reporting for impredicative types

Don't suggest -XImpredicativeTypes; and document its flakiness
Fixes Trac #10325

compiler/typecheck/TcErrors.hs

@@ -919,7 +919,7 @@ mkTyVarEqErr dflags ctxt extra ct oriented tv1 ty2
   = do { let msg = vcat [ ptext (sLit "Cannot instantiate unification variable")
                           <+> quotes (ppr tv1)
                         , hang (ptext (sLit "with a type involving foralls:")) 2 (ppr ty2)
-                        , nest 2 (ptext (sLit "Perhaps you want ImpredicativeTypes")) ]
+                        , nest 2 (ptext (sLit "GHC doesn't yet support impredicative polymorphism")) ]
        ; mkErrorMsgFromCt ctxt ct msg }
 
   -- If the immediately-enclosing implication has 'tv' a skolem, and

compiler/typecheck/TcValidity.hs

@@ -360,7 +360,7 @@ data Rank = ArbitraryRank         -- Any rank ok
 
 rankZeroMonoType, tyConArgMonoType, synArgMonoType :: Rank
 rankZeroMonoType = MonoType (ptext (sLit "Perhaps you intended to use RankNTypes or Rank2Types"))
-tyConArgMonoType = MonoType (ptext (sLit "Perhaps you intended to use ImpredicativeTypes"))
+tyConArgMonoType = MonoType (ptext (sLit "GHC doesn't yet support impredicative polymorphism"))
 synArgMonoType   = MonoType (ptext (sLit "Perhaps you intended to use LiberalTypeSynonyms"))
 
 funArgResRank :: Rank -> (Rank, Rank)             -- Function argument and result

docs/users_guide/glasgow_exts.xml

@@ -8220,9 +8220,9 @@ for rank-2 types.
 <sect2 id="impredicative-polymorphism">
 <title>Impredicative polymorphism
 </title>
-<para>GHC supports <emphasis>impredicative polymorphism</emphasis>,
+<para>GHC has extremely flaky support for <emphasis>impredicative polymorphism</emphasis>,
 enabled with <option>-XImpredicativeTypes</option>.
-This means
+If it worked, this would mean
 that you can call a polymorphic function at a polymorphic type, and
 parameterise data structures over polymorphic types.  For example:
 <programlisting>
@@ -8233,11 +8233,11 @@ parameterise data structures over polymorphic types.  For example:
 Notice here that the <literal>Maybe</literal> type is parameterised by the
 <emphasis>polymorphic</emphasis> type <literal>(forall a. [a] ->
 [a])</literal>.
-</para>
-<para>The technical details of this extension are described in the paper
-<ulink url="http://research.microsoft.com/%7Esimonpj/papers/boxy/">Boxy types:
-type inference for higher-rank types and impredicativity</ulink>,
-which appeared at ICFP 2006.
+However <emphasis>the extension should be considered highly experimental, and certainly un-supported</emphasis>.
+You are welcome to try it, but please don't rely on it working consistently, or
+working the same in subsequent releases.  See 
+<ulink url="https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism">this wiki page</ulink>
+for more details.
 </para>
 </sect2>
 

testsuite/tests/typecheck/should_fail/T10194.stderr

 
-T10194.hs:7:8:
+T10194.hs:7:8: error:
     Cannot instantiate unification variable ‘b0’
     with a type involving foralls: X
-      Perhaps you want ImpredicativeTypes
+      GHC doesn't yet support impredicative polymorphism
     In the expression: (.)
     In an equation for ‘comp’: comp = (.)

testsuite/tests/typecheck/should_fail/T2538.stderr

 
-T2538.hs:6:6:
+T2538.hs:6:6: error:
     Illegal polymorphic or qualified type: Eq a => a -> a
     Perhaps you intended to use RankNTypes or Rank2Types
     In the type signature for ‘f’: f :: (Eq a => a -> a) -> Int
 
-T2538.hs:9:6:
+T2538.hs:9:6: error:
     Illegal polymorphic or qualified type: Eq a => a -> a
-    Perhaps you intended to use ImpredicativeTypes
+    GHC doesn't yet support impredicative polymorphism
     In the type signature for ‘g’: g :: [Eq a => a -> a] -> Int
 
-T2538.hs:12:6:
+T2538.hs:12:6: error:
     Illegal polymorphic or qualified type: Eq a => a -> a
     In the type signature for ‘h’: h :: Ix (Eq a => a -> a) => Int

testsuite/tests/typecheck/should_fail/T7809.stderr

 
-T7809.hs:8:8:
+T7809.hs:8:8: error:
     Illegal polymorphic or qualified type: PolyId
-    Perhaps you intended to use ImpredicativeTypes
+    GHC doesn't yet support impredicative polymorphism
     In the type signature for ‘foo’: foo :: F PolyId

testsuite/tests/typecheck/should_fail/tcfail127.stderr

 
-tcfail127.hs:3:8:
+tcfail127.hs:3:8: error:
     Illegal polymorphic or qualified type: Num a => a -> a
-    Perhaps you intended to use ImpredicativeTypes
+    GHC doesn't yet support impredicative polymorphism
     In the type signature for ‘foo’: foo :: IO (Num a => a -> a)

testsuite/tests/typecheck/should_fail/tcfail197.stderr

 
-tcfail197.hs:5:8:
+tcfail197.hs:5:8: error:
     Illegal polymorphic or qualified type: forall a. a
-    Perhaps you intended to use ImpredicativeTypes
+    GHC doesn't yet support impredicative polymorphism
     In the type signature for ‘foo’: foo :: [forall a. a] -> Int