diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 6b37e80a3da62cbd8cef3400913aff205961b1e5..f32215b315259ba1d113133e5804eec840428578 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/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
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index d3000a651a6376d024052d47fc549e3903b19e78..53b492d3e660e1b72f6ec505010039e4d77eaed5 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/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
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index 630f2b47da71b462fc7aab62e92913097ba1c02a..b594fe02f63af3615d60ef742c02d82867a8c41e 100644
--- a/docs/users_guide/glasgow_exts.xml
+++ b/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>
 
diff --git a/testsuite/tests/typecheck/should_fail/T10194.stderr b/testsuite/tests/typecheck/should_fail/T10194.stderr
index 53ee74b93c832ca954c63757f745177785bef790..7bc79b2e6faa860d73a1b153646555d014006f9a 100644
--- a/testsuite/tests/typecheck/should_fail/T10194.stderr
+++ b/testsuite/tests/typecheck/should_fail/T10194.stderr
@@ -1,7 +1,7 @@
 
-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 = (.)
diff --git a/testsuite/tests/typecheck/should_fail/T2538.stderr b/testsuite/tests/typecheck/should_fail/T2538.stderr
index 884eafb27170758770fc811d8eb8be6937899e6d..94583a42b4f462c1db72da107ab7981e1df9cab4 100644
--- a/testsuite/tests/typecheck/should_fail/T2538.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2538.stderr
@@ -1,14 +1,14 @@
 
-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
diff --git a/testsuite/tests/typecheck/should_fail/T7809.stderr b/testsuite/tests/typecheck/should_fail/T7809.stderr
index e306f8dcd39a0634b64774b407df7540d4d9ff70..153c4d1c1f74cd7ded10921d4aa73cf3204dae48 100644
--- a/testsuite/tests/typecheck/should_fail/T7809.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7809.stderr
@@ -1,5 +1,5 @@
 
-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
diff --git a/testsuite/tests/typecheck/should_fail/tcfail127.stderr b/testsuite/tests/typecheck/should_fail/tcfail127.stderr
index d05a234010a8ec3a72cf952af9b203be6545df32..32af3d838210c54d5899c7485a8304ce6172afe8 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail127.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail127.stderr
@@ -1,5 +1,5 @@
 
-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)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail197.stderr b/testsuite/tests/typecheck/should_fail/tcfail197.stderr
index 35d24e490c58a829ab45fd04330caf608877469f..c15af6032921d046a5008d6e406df994b21d2179 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail197.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail197.stderr
@@ -1,5 +1,5 @@
 
-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