Implement Quick Look impredicativity

This patch implements Quick Look impredicativity (#18126), sticking
very closely to the design in
    A quick look at impredicativity, Serrano et al, ICFP 2020

The main change is that a big chunk of GHC.Tc.Gen.Expr has been
extracted to two new modules
    GHC.Tc.Gen.App
    GHC.Tc.Gen.Head
which deal with typechecking n-ary applications, and the head of
such applications, respectively.  Both contain a good deal of
documentation.

Three other loosely-related changes are in this patch:

* I implemented (partly by accident) points (2,3)) of the accepted GHC
  proposal "Clean up printing of foralls", namely
  https://github.com/ghc-proposals/ghc-proposals/blob/
        master/proposals/0179-printing-foralls.rst
  (see #16320).

  In particular, see Note [TcRnExprMode] in GHC.Tc.Module
  - :type instantiates /inferred/, but not /specified/, quantifiers
  - :type +d instantiates /all/ quantifiers
  - :type +v is killed off

  That completes the implementation of the proposal,
  since point (1) was done in
    commit df08468113ab46832b7ac0a7311b608d1b418c4d
    Author: Krzysztof Gogolewski <krzysztof.gogolewski@tweag.io>
    Date:   Mon Feb 3 21:17:11 2020 +0100
    Always display inferred variables using braces

* HsRecFld (which the renamer introduces for record field selectors),
  is now preserved by the typechecker, rather than being rewritten
  back to HsVar.  This is more uniform, and turned out to be more
  convenient in the new scheme of things.

* The GHCi debugger uses a non-standard unification that allows the
  unification variables to unify with polytypes.  We used to hack
  this by using ImpredicativeTypes, but that doesn't work anymore
  so I introduces RuntimeUnkTv.  See Note [RuntimeUnkTv] in
  GHC.Runtime.Heap.Inspect

Updates haddock submodule.

WARNING: this patch won't validate on its own.  It was too
hard to fully disentangle it from the following patch, on
type errors and kind generalisation.

Changes to tests

* Fixes #9730 (test added)

* Fixes #7026 (test added)

* Fixes most of #8808, except function `g2'` which uses a
  section (which doesn't play with QL yet -- see #18126)
  Test added

* Fixes #1330. NB Church1.hs subsumes Church2.hs, which is now deleted

* Fixes #17332 (test added)

* Fixes #4295

* This patch makes typecheck/should_run/T7861 fail.
  But that turns out to be a pre-existing bug: #18467.
  So I have just made T7861 into expect_broken(18467)

58 files changed, 580 insertions, 258 deletions

diff --git a/testsuite/tests/boxy/Base1.stderr b/testsuite/tests/boxy/Base1.stderr
deleted file mode 100644
index e9b2144533..0000000000
--- a/testsuite/tests/boxy/Base1.stderr
+++ /dev/null
@@ -1,20 +0,0 @@
-
-Base1.hs:20:13: error:
-    • Couldn't match type: a0 -> a0
-                     with: forall a. a -> a
-      Expected: MEither Sid b
-        Actual: MEither (a0 -> a0) b
-    • In the expression: MLeft fid
-      In an equation for ‘test1’: test1 fid = MLeft fid
-
-Base1.hs:25:39: error:
-    • Couldn't match type: a1 -> a1
-                     with: forall a. a -> a
-      Expected: Maybe (Sid, Sid)
-        Actual: Maybe (a1 -> a1, a2 -> a2)
-    • In the expression: Just (x, y)
-      In a case alternative: MRight y -> Just (x, y)
-      In the expression:
-        case m of
-          MRight y -> Just (x, y)
-          _ -> Nothing
diff --git a/testsuite/tests/boxy/Church1.hs b/testsuite/tests/boxy/Church1.hs
deleted file mode 100644
index fccaac7d8c..0000000000
--- a/testsuite/tests/boxy/Church1.hs
+++ /dev/null
@@ -1,28 +0,0 @@
-{-# LANGUAGE RankNTypes #-}
-
-module Church1 where 
--- Church numerals w/o extra type constructors 
-
-type CNat = forall a. (a->a) -> a -> a 
-
-n0 :: CNat 
-n0 = \f z -> z
-
-n1 :: CNat 
-n1 = \f z -> f z 
-
-nsucc :: CNat -> CNat 
-nsucc n = \f z -> f (n f z)
-
-add, mul :: CNat -> CNat -> CNat
-add m n = \f -> \a -> m f (n f a)
-mul m n = \f -> \a -> m (n f) a
-
--- already works with GHC 6.4 
-exp0 :: CNat -> CNat -> CNat 
-exp0 m n = n m
-
-
-exp1 :: CNat -> CNat -> CNat 
-exp1 m n = (n::((CNat -> CNat) -> CNat -> CNat)) (mul m) n1  -- checks with app rule 
-
diff --git a/testsuite/tests/boxy/Church2.hs b/testsuite/tests/boxy/Church2.hs
deleted file mode 100644
index c360bb3a8b..0000000000
--- a/testsuite/tests/boxy/Church2.hs
+++ /dev/null
@@ -1,27 +0,0 @@
-{-# LANGUAGE RankNTypes #-}
-
-module Church2 where 
--- Church numerals w/o extra type constructors: Should fail
-
-type CNat = forall a. (a->a) -> a -> a 
-
-n0 :: CNat 
-n0 = \f z -> z
-
-n1 :: CNat 
-n1 = \f z -> f z 
-
-nsucc :: CNat -> CNat 
-nsucc n = \f z -> f (n f z)
-
-add, mul :: CNat -> CNat -> CNat
-add m n = \f -> \a -> m f (n f a)
-mul m n = \f -> \a -> m (n f) a
-
--- already works with GHC 6.4 
-exp0 :: CNat -> CNat -> CNat 
-exp0 m n = n m
-
--- should fail! 
-exp2 :: CNat -> CNat -> CNat 
-exp2 m n = n (mul m) n1 
diff --git a/testsuite/tests/boxy/Church2.stderr b/testsuite/tests/boxy/Church2.stderr
deleted file mode 100644
index ea7613733b..0000000000
--- a/testsuite/tests/boxy/Church2.stderr
+++ /dev/null
@@ -1,12 +0,0 @@
-
-Church2.hs:27:14:
-    Couldn't match expected type `CNat'
-	   against inferred type `(a -> a) -> a -> a'
-    In the first argument of `n', namely `(mul m)'
-    In the expression: n (mul m) n1
-    In the definition of `exp2': exp2 m n = n (mul m) n1
-
-*** This error message is not helpful,
-*** and the test should fail, not pass
-*** These comments are here to make sure the output
-*** doesn't match!
diff --git a/testsuite/tests/boxy/SystemF.hs b/testsuite/tests/boxy/SystemF.hs
deleted file mode 100644
index 3f5b4b957a..0000000000
--- a/testsuite/tests/boxy/SystemF.hs
+++ /dev/null
@@ -1,21 +0,0 @@
-{-# LANGUAGE Rank2Types #-}
-
-module SystemF where 
--- System-F examples 
-
-
-type Sid = forall a. a -> a 
-
-apply :: forall a b . (a -> b) -> a -> b 
-apply f g = f g 
-
-hr :: (forall a. a -> a) -> (Int,Bool)
-hr f = (f 3,f True)
-
-test0 = apply hr id   -- requires smart-app-arg 
-
-selfApp :: Sid -> Sid 
-selfApp x = (x::(Sid -> Sid)) x 
-
-
-
diff --git a/testsuite/tests/boxy/all.T b/testsuite/tests/boxy/all.T
deleted file mode 100644
index 99ab5367f2..0000000000
--- a/testsuite/tests/boxy/all.T
+++ /dev/null
@@ -1,11 +0,0 @@
-# Boxy-type tests
-
-test('Base1',    normal, compile_fail, [''])
-test('Church1',  expect_broken(4295), compile, [''])
-test('Church2',  expect_broken(1330), compile_fail, [''])
-test('PList1',   expect_broken(4295), compile, [''])
-test('PList2',   expect_broken(4295), compile, [''])
-test('SystemF',  expect_broken(4295), compile, [''])
-test('boxy',     expect_broken(4295), compile, [''])
-test('Compose',  normal, compile, [''])
-test('T2193',    normal, compile_and_run, [''])
diff --git a/testsuite/tests/dependent/ghci/T11549.stdout b/testsuite/tests/dependent/ghci/T11549.stdout
index 5e23c0da99..b1edea905d 100644
--- a/testsuite/tests/dependent/ghci/T11549.stdout
+++ b/testsuite/tests/dependent/ghci/T11549.stdout
@@ -3,17 +3,20 @@
 ($) :: (a -> b) -> a -> b 	-- Defined in ‘GHC.Base’
 infixr 0 $
 TYPE :: RuntimeRep -> *
-error :: [Char] -> a
+error :: GHC.Stack.Types.HasCallStack => [Char] -> a
 error :: GHC.Stack.Types.HasCallStack => [Char] -> a
   	-- Defined in ‘GHC.Err’
 
 -fprint-explicit-runtime-reps
-($) :: (a -> b) -> a -> b
+($) :: forall (r :: RuntimeRep) a (b :: TYPE r). (a -> b) -> a -> b
 ($) :: forall (r :: RuntimeRep) a (b :: TYPE r). (a -> b) -> a -> b
   	-- Defined in ‘GHC.Base’
 infixr 0 $
 TYPE :: RuntimeRep -> *
-error :: [Char] -> a
+error
+  :: forall (r :: RuntimeRep) (a :: TYPE r).
+     GHC.Stack.Types.HasCallStack =>
+     [Char] -> a
 error ::
   forall (r :: RuntimeRep) (a :: TYPE r).
   GHC.Stack.Types.HasCallStack =>
diff --git a/testsuite/tests/dependent/ghci/T11786.script b/testsuite/tests/dependent/ghci/T11786.script
index 61e3141843..ada3d7b6ca 100644
--- a/testsuite/tests/dependent/ghci/T11786.script
+++ b/testsuite/tests/dependent/ghci/T11786.script
@@ -1,11 +1,9 @@
 :set -fno-print-explicit-runtime-reps
 :t ($)
 :t (($))
-:t +v ($)
 :i ($)
 
 :set -fprint-explicit-runtime-reps
 :t ($)
 :t (($))
-:t +v ($)
 :i ($)
diff --git a/testsuite/tests/dependent/ghci/T11786.stdout b/testsuite/tests/dependent/ghci/T11786.stdout
index 93616ed750..b43290bd2a 100644
--- a/testsuite/tests/dependent/ghci/T11786.stdout
+++ b/testsuite/tests/dependent/ghci/T11786.stdout
@@ -1,13 +1,13 @@
 ($) :: (a -> b) -> a -> b
 (($)) :: (a -> b) -> a -> b
-($) :: (a -> b) -> a -> b
 ($) :: (a -> b) -> a -> b 	-- Defined in ‘GHC.Base’
 infixr 0 $
-($) :: (a -> b) -> a -> b
-(($)) :: (a -> b) -> a -> b
 ($)
   :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
      (a -> b) -> a -> b
+(($))
+  :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
+     (a -> b) -> a -> b
 ($) ::
   forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
   (a -> b) -> a -> b
diff --git a/testsuite/tests/ghci/scripts/T11376.stdout b/testsuite/tests/ghci/scripts/T11376.stdout
index 01e749a22c..3c7674774c 100644
--- a/testsuite/tests/ghci/scripts/T11376.stdout
+++ b/testsuite/tests/ghci/scripts/T11376.stdout
@@ -1,6 +1,6 @@
-bar @Int :: Int -> b -> Int
-bar @Int :: forall {b}. Int -> b -> Int
-prox :: forall {k} {a :: k}. Prox @{k} a
+bar @Int :: Show Int => Int -> b -> Int
+bar @Int :: forall b. Show Int => Int -> b -> Int
+prox :: forall {k} (a :: k). Prox @{k} a
 prox @Int :: Prox @{*} Int
-Prox :: forall {k} {a :: k}. Prox @{k} a
+Prox :: forall {k} (a :: k). Prox @{k} a
 Prox @Int :: Prox @{*} Int
diff --git a/testsuite/tests/ghci/scripts/T11721.script b/testsuite/tests/ghci/scripts/T11721.script
index 11fa313e3c..840f28d613 100644
--- a/testsuite/tests/ghci/scripts/T11721.script
+++ b/testsuite/tests/ghci/scripts/T11721.script
@@ -2,6 +2,6 @@
 :set -fprint-explicit-foralls
 import Data.Proxy
 data X a where { MkX :: b -> Proxy a -> X a }
-:type +v MkX
-:type +v MkX @Int
-:type +v MkX @Int @Maybe
+:type MkX
+:type MkX @Int
+:type MkX @Int @Maybe
diff --git a/testsuite/tests/ghci/scripts/T11975.script b/testsuite/tests/ghci/scripts/T11975.script
index 80061ef97b..72b1a5caff 100644
--- a/testsuite/tests/ghci/scripts/T11975.script
+++ b/testsuite/tests/ghci/scripts/T11975.script
@@ -1,9 +1,5 @@
 :set -fprint-explicit-foralls
 :type mapM
-:type +v mapM
-:t +v mapM
 let foo :: (Show a, Num b) => a -> b; foo = undefined
 :set -XTypeApplications
 :type foo @Int
-:type +v foo @Int
-:t +v foo @Int
diff --git a/testsuite/tests/ghci/scripts/T11975.stdout b/testsuite/tests/ghci/scripts/T11975.stdout
index 56d8d4180d..86d44bd223 100644
--- a/testsuite/tests/ghci/scripts/T11975.stdout
+++ b/testsuite/tests/ghci/scripts/T11975.stdout
@@ -1,15 +1,5 @@
 mapM
-  :: forall {t :: * -> *} {m :: * -> *} {a} {b}.
-     (Traversable t, Monad m) =>
-     (a -> m b) -> t a -> m (t b)
-mapM
-  :: forall (t :: * -> *) (m :: * -> *) a b.
-     (Traversable t, Monad m) =>
-     (a -> m b) -> t a -> m (t b)
-mapM
   :: forall (t :: * -> *) (m :: * -> *) a b.
      (Traversable t, Monad m) =>
      (a -> m b) -> t a -> m (t b)
-foo @Int :: forall {b}. Num b => Int -> b
-foo @Int :: forall b. (Show Int, Num b) => Int -> b
 foo @Int :: forall b. (Show Int, Num b) => Int -> b
diff --git a/testsuite/tests/ghci/scripts/T12550.stdout b/testsuite/tests/ghci/scripts/T12550.stdout
index a3117d02c2..fb0bf4c697 100644
--- a/testsuite/tests/ghci/scripts/T12550.stdout
+++ b/testsuite/tests/ghci/scripts/T12550.stdout
@@ -1,16 +1,16 @@
-f :: forall {a :: * -> *} {b}. C a => a b
-f :: forall {a :: * -> *} {b}. C a => a b
-f :: forall {a :: * -> *} {b}. C a => a b
-f :: forall {a :: * -> *} {b}. C a => a b
-f :: forall {a :: * -> *} {b}. C a => a b
-f :: forall {a :: * -> *} {b}. C a => a b
-f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
-f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
-f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
-f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
-f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
-f ∷ ∀ {a ∷ ★ → ★} {b}. C a ⇒ a b
-fmap ∷ ∀ {f ∷ ★ → ★} {a} {b}. Functor f ⇒ (a → b) → f a → f b
+f :: forall (a :: * -> *) b. C a => a b
+f :: forall (a :: * -> *) b. C a => a b
+f :: forall (a :: * -> *) b. C a => a b
+f :: forall (a :: * -> *) b. C a => a b
+f :: forall (a :: * -> *) b. C a => a b
+f :: forall (a :: * -> *) b. C a => a b
+f ∷ ∀ (a ∷ ★ → ★) b. C a ⇒ a b
+f ∷ ∀ (a ∷ ★ → ★) b. C a ⇒ a b
+f ∷ ∀ (a ∷ ★ → ★) b. C a ⇒ a b
+f ∷ ∀ (a ∷ ★ → ★) b. C a ⇒ a b
+f ∷ ∀ (a ∷ ★ → ★) b. C a ⇒ a b
+f ∷ ∀ (a ∷ ★ → ★) b. C a ⇒ a b
+fmap ∷ ∀ (f ∷ ★ → ★) a b. Functor f ⇒ (a → b) → f a → f b
 type Functor :: (★ → ★) → Constraint
 class Functor f where
   fmap ∷ ∀ a b. (a → b) → f a → f b
@@ -57,7 +57,7 @@ instance ∀ a b c. Functor ((,,,) a b c) -- Defined in ‘GHC.Base’
 instance ∀ a b. Functor ((,,) a b) -- Defined in ‘GHC.Base’
 instance ∀ a. Functor ((,) a) -- Defined in ‘GHC.Base’
 datatypeName
-  ∷ ∀ {d} {t ∷ ★ → (★ → ★) → ★ → ★} {f ∷ ★ → ★} {a}.
+  ∷ ∀ d k1 (t ∷ ★ → (k1 → ★) → k1 → ★) (f ∷ k1 → ★) (a ∷ k1).
     Datatype d ⇒
     t d f a → [Char]
 type Datatype :: ∀ {k}. k → Constraint
@@ -67,6 +67,7 @@ class Datatype d where
                  t d f a → [Char]
   ...
   	-- Defined in ‘GHC.Generics’
-(:*:) ∷ ∀ {f ∷ ★ → ★} {p} {g ∷ ★ → ★}. f p → g p → (:*:) f g p
+(:*:)
+  ∷ ∀ k (f ∷ k → ★) (g ∷ k → ★) (p ∷ k). f p → g p → (:*:) f g p
 Rep ∷ ★ → ★ → ★
 M1 ∷ ∀ k. ★ → Meta → (k → ★) → k → ★
diff --git a/testsuite/tests/ghci/scripts/T13988.script b/testsuite/tests/ghci/scripts/T13988.script
index 06aa686ed5..ac18e578be 100644
--- a/testsuite/tests/ghci/scripts/T13988.script
+++ b/testsuite/tests/ghci/scripts/T13988.script
@@ -1,2 +1,2 @@
 :load T13988
-:type +v MkFoo
+:type MkFoo
diff --git a/testsuite/tests/ghci/scripts/T16804.stdout b/testsuite/tests/ghci/scripts/T16804.stdout
index 1c2d73b3c8..1bde0be8e7 100644
--- a/testsuite/tests/ghci/scripts/T16804.stdout
+++ b/testsuite/tests/ghci/scripts/T16804.stdout
@@ -6,7 +6,7 @@ Collecting type info for 3 module(s) ...
 %        ^~~~~~^
 > 
 % output:
-undefined :: forall {a}. a
+undefined :: forall a. GHC.Stack.Types.HasCallStack => a
 
 % executing: ":uses T16804a.hs  1  8  1 14"
 % file snippet:
@@ -22,7 +22,7 @@ undefined :: forall {a}. a
 %        ^~~^
 > 
 % output:
-undefined :: forall {a}. a
+undefined :: forall a. GHC.Stack.Types.HasCallStack => a
 
 % executing: ":type-at T16804a.hs  3  8  3 18 undefined"
 % file snippet:
@@ -31,7 +31,7 @@ undefined :: forall {a}. a
 %        ^~~~~~~~~~^
 > 
 % output:
-undefined :: forall {a}. a
+undefined :: forall a. GHC.Stack.Types.HasCallStack => a
 
 % executing: ":type-at T16804a.hs  3 13  3 18 undefined"
 % file snippet:
@@ -40,7 +40,7 @@ undefined :: forall {a}. a
 %             ^~~~~^
 > 
 % output:
-undefined :: forall {a}. a
+undefined :: forall a. GHC.Stack.Types.HasCallStack => a
 
 % executing: ":uses T16804a.hs  3  8  3 11"
 % file snippet:
@@ -73,7 +73,7 @@ undefined :: forall {a}. a
 %      ^~~^
 >   deriving (Show)
 % output:
-undefined :: forall {a}. a
+undefined :: forall a. GHC.Stack.Types.HasCallStack => a
 
 % executing: ":type-at T16804a.hs  5 13  5 13 undefined"
 % file snippet:
@@ -82,7 +82,7 @@ undefined :: forall {a}. a
 %             ^
 >   deriving (Show)
 % output:
-undefined :: forall {a}. a
+undefined :: forall a. GHC.Stack.Types.HasCallStack => a
 
 % executing: ":type-at T16804a.hs  5 15  5 15 undefined"
 % file snippet:
@@ -91,7 +91,7 @@ undefined :: forall {a}. a
 %               ^
 >   deriving (Show)
 % output:
-undefined :: forall {a}. a
+undefined :: forall a. GHC.Stack.Types.HasCallStack => a
 
 % executing: ":type-at T16804a.hs  5 17  5 17 undefined"
 % file snippet:
@@ -100,7 +100,7 @@ undefined :: forall {a}. a
 %                 ^
 >   deriving (Show)
 % output:
-undefined :: forall {a}. a
+undefined :: forall a. GHC.Stack.Types.HasCallStack => a
 
 % executing: ":type-at T16804a.hs  6 13  6 16 undefined"
 % file snippet:
@@ -160,7 +160,7 @@ T16804a.hs:(6,13)-(6,16)
 %          ^~~~~^
 >   mempty = A
 % output:
-undefined :: forall {a}. a
+undefined :: forall a. GHC.Stack.Types.HasCallStack => a
 
 % executing: ":type-at T16804a.hs  7 17  7 20 undefined"
 % file snippet:
@@ -169,7 +169,7 @@ undefined :: forall {a}. a
 %                 ^~~^
 >   mempty = A
 % output:
-undefined :: forall {a}. a
+undefined :: forall a. GHC.Stack.Types.HasCallStack => a
 
 % executing: ":type-at T16804a.hs  7 10  7 20 undefined"
 % file snippet:
@@ -249,7 +249,7 @@ T16804a.hs:(8,3)-(8,8)
 % ^~~~~~~~~~~^
 > testFunction A B = True
 % output:
-undefined :: forall {a}. a
+undefined :: forall a. GHC.Stack.Types.HasCallStack => a
 
 % executing: ":type-at T16804a.hs 13  1 13 12 undefined"
 % file snippet:
@@ -566,7 +566,7 @@ undefined :: Test
 >   B <> _   = B
 %     ^^
 % output:
-undefined :: forall {a}. a
+undefined :: forall a. GHC.Stack.Types.HasCallStack => a
 
 % executing: ":type-at T16804a.hs 29  8 29  8 undefined"
 % file snippet:
diff --git a/testsuite/tests/ghci/scripts/T17403.script b/testsuite/tests/ghci/scripts/T17403.script
index ad0f9cd83f..624e6a5c2d 100644
--- a/testsuite/tests/ghci/scripts/T17403.script
+++ b/testsuite/tests/ghci/scripts/T17403.script
@@ -1,2 +1,2 @@
 :load T17403
-:type +v f
+:type f
diff --git a/testsuite/tests/ghci/scripts/T17403.stdout b/testsuite/tests/ghci/scripts/T17403.stdout
index c543c3d0e5..deff4906ac 100644
--- a/testsuite/tests/ghci/scripts/T17403.stdout
+++ b/testsuite/tests/ghci/scripts/T17403.stdout
@@ -1 +1 @@
-f :: (() :: Constraint) => String
+f :: String
diff --git a/testsuite/tests/ghci/scripts/TypeAppData.stdout b/testsuite/tests/ghci/scripts/TypeAppData.stdout
index dd548c85da..19e541d4b4 100644
--- a/testsuite/tests/ghci/scripts/TypeAppData.stdout
+++ b/testsuite/tests/ghci/scripts/TypeAppData.stdout
@@ -1,13 +1,13 @@
-P1 :: forall {k} {a :: k}. P1 a
-P2 :: forall {k} {a :: k}. P2 a
-P3 :: forall {k} {a :: k}. P3 k a
-P4 :: forall {k} {a :: k}. P1 a -> P4 a
-P5 :: forall {k} {a :: k}. P1 a -> P5
-P6 :: forall {k} {a :: k}. P1 a -> P6
-P7 :: forall {k} {a :: k}. P1 a
-P8 :: forall {k} {a :: k}. P1 a
-P9 :: forall {k} {a :: k}. P1 a
-P11 :: forall {k} {a :: k}. P1 a -> P5
-P12 :: forall {k} {a :: k}. P1 a -> P5
-P13 :: forall {k} {a :: k}. P1 a -> P5
-P14 :: forall {k} {a :: k}. P1 a -> P5
+P1 :: forall {k} (a :: k). P1 a
+P2 :: forall k (a :: k). P2 a
+P3 :: forall k (a :: k). P3 k a
+P4 :: forall {k} (a :: k). P1 a -> P4 a
+P5 :: forall {k} (a :: k). P1 a -> P5
+P6 :: forall k (a :: k). P1 a -> P6
+P7 :: forall {k} (a :: k). P1 a
+P8 :: forall {k} (a :: k). P1 a
+P9 :: forall k (a :: k). P1 a
+P11 :: forall {k} (a :: k). P1 a -> P5
+P12 :: forall {k} (a :: k). P1 a -> P5
+P13 :: forall k (a :: k). P1 a -> P5
+P14 :: forall k (a :: k). P1 a -> P5
diff --git a/testsuite/tests/ghci/should_run/T12549.stdout b/testsuite/tests/ghci/should_run/T12549.stdout
index 8143b156c8..07332c3eca 100644
--- a/testsuite/tests/ghci/should_run/T12549.stdout
+++ b/testsuite/tests/ghci/should_run/T12549.stdout
@@ -1,3 +1,3 @@
-f :: forall {k1} {k2} {a :: k1 -> k2 -> *} {b :: k1} {c :: k2}.
+f :: forall {k1} {k2} (a :: k1 -> k2 -> *) (b :: k1) (c :: k2).
      C a =>
      a b c
diff --git a/testsuite/tests/ghci/should_run/T14125a.script b/testsuite/tests/ghci/should_run/T14125a.script
index 1667349160..224aa23f73 100644
--- a/testsuite/tests/ghci/should_run/T14125a.script
+++ b/testsuite/tests/ghci/should_run/T14125a.script
@@ -4,5 +4,4 @@ data instance Foo Int = FooInt Int
 :kind! Foo Int
 let f (FooInt i) = i
 :info    f
-:type +v f
 :type    f
diff --git a/testsuite/tests/ghci/should_run/T14125a.stdout b/testsuite/tests/ghci/should_run/T14125a.stdout
index 7b4e85edd3..7946386098 100644
--- a/testsuite/tests/ghci/should_run/T14125a.stdout
+++ b/testsuite/tests/ghci/should_run/T14125a.stdout
@@ -2,4 +2,3 @@ Foo Int :: *
 = Foo Int
 f :: Foo Int -> Int 	-- Defined at <interactive>:5:5
 f :: Foo Int -> Int
-f :: Foo Int -> Int
diff --git a/testsuite/tests/ghci/should_run/T15806.stderr b/testsuite/tests/ghci/should_run/T15806.stderr
index b7e0b4be56..c25e90fe3a 100644
--- a/testsuite/tests/ghci/should_run/T15806.stderr
+++ b/testsuite/tests/ghci/should_run/T15806.stderr
@@ -1,3 +1,4 @@
+
 <interactive>:1:1: error:
     Illegal polymorphic type: forall a. a -> a
-    GHC doesn't yet support impredicative polymorphism
\ No newline at end of file
+    Perhaps you intended to use ImpredicativeTypes
diff --git a/testsuite/tests/boxy/Base1.hs b/testsuite/tests/impredicative/Base1.hs
index 7e33069199..5e3b377ee2 100644
--- a/testsuite/tests/boxy/Base1.hs
+++ b/testsuite/tests/impredicative/Base1.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-}
+{-# LANGUAGE ImpredicativeTypes #-}
 
 -- Sept 16: now failing, because I've further reduced the scop
 --          of impredicative types
diff --git a/testsuite/tests/impredicative/Church1.hs b/testsuite/tests/impredicative/Church1.hs
new file mode 100644
index 0000000000..e5af210385
--- /dev/null
+++ b/testsuite/tests/impredicative/Church1.hs
@@ -0,0 +1,35 @@
+{-# LANGUAGE ImpredicativeTypes, RankNTypes, ScopedTypeVariables, TypeApplications #-}
+
+module Church1 where
+-- Church numerals w/o extra type constructors
+
+type CNat = forall a. (a->a) -> a -> a
+
+n0 :: CNat
+n0 = \f z -> z
+
+n1 :: CNat
+n1 = \f z -> f z
+
+nsucc :: CNat -> CNat
+nsucc n = \f z -> f (n f z)
+
+add, mul :: CNat -> CNat -> CNat
+add m n = \f -> \a -> m f (n f a)
+mul m n = \f -> \a -> m (n f) a
+
+-- already works with GHC 6.4
+exp0 :: CNat -> CNat -> CNat
+exp0 m n = n m
+
+exp1 :: CNat -> CNat -> CNat
+exp1 m n = n (mul m) n1
+
+foldNat :: CNat -> (a -> a) -> a -> a
+foldNat n = n
+
+idC :: CNat -> CNat
+idC x = foldNat @CNat x (\y -> nsucc y) n0
+
+inc :: CNat -> CNat
+inc x = foldNat x nsucc n1
diff --git a/testsuite/tests/boxy/Compose.hs b/testsuite/tests/impredicative/Compose.hs
index f3d3a10b28..f3d3a10b28 100644
--- a/testsuite/tests/boxy/Compose.hs
+++ b/testsuite/tests/impredicative/Compose.hs
diff --git a/testsuite/tests/boxy/Makefile b/testsuite/tests/impredicative/Makefile
index 9a36a1c5fe..9a36a1c5fe 100644
--- a/testsuite/tests/boxy/Makefile
+++ b/testsuite/tests/impredicative/Makefile
diff --git a/testsuite/tests/boxy/PList1.hs b/testsuite/tests/impredicative/PList1.hs
index 6869d904cc..27cedc1f49 100644
--- a/testsuite/tests/boxy/PList1.hs
+++ b/testsuite/tests/impredicative/PList1.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-}
+{-# LANGUAGE ImpredicativeTypes #-}
 
 module PList1 where
 -- Polymorphic lists 1: requires smart-app-res
diff --git a/testsuite/tests/boxy/PList2.hs b/testsuite/tests/impredicative/PList2.hs
index 316e8792ae..316e8792ae 100644
--- a/testsuite/tests/boxy/PList2.hs
+++ b/testsuite/tests/impredicative/PList2.hs
diff --git a/testsuite/tests/impredicative/SystemF.hs b/testsuite/tests/impredicative/SystemF.hs
new file mode 100644
index 0000000000..b1f7f0ede9
--- /dev/null
+++ b/testsuite/tests/impredicative/SystemF.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+
+module SystemF where
+-- System-F examples
+
+
+type Sid = forall a. a -> a
+
+apply :: forall a b . (a -> b) -> a -> b
+apply f g = f g
+
+hr :: (forall a. a -> a) -> (Int,Bool)
+hr f = (f 3,f True)
+
+test0 = apply hr id   -- requires smart-app-arg
+
+selfApp :: Sid -> Sid
+selfApp x = (x::(Sid -> Sid)) x
diff --git a/testsuite/tests/impredicative/T17332.hs b/testsuite/tests/impredicative/T17332.hs
new file mode 100644
index 0000000000..7b83651740
--- /dev/null
+++ b/testsuite/tests/impredicative/T17332.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+module Bug where
+
+import GHC.Exts
+
+data Dict c where
+  MkDict :: c => Dict c
+
+aux :: Dict (forall a. a)
+aux = MkDict
+
+{-
+[W] forall (c:: Constraint). c
+==>
+  forall c. [W] c
+-}
diff --git a/testsuite/tests/impredicative/T17332.stderr b/testsuite/tests/impredicative/T17332.stderr
new file mode 100644
index 0000000000..24bb0e2aee
--- /dev/null
+++ b/testsuite/tests/impredicative/T17332.stderr
@@ -0,0 +1,5 @@
+
+T17332.hs:13:7: error:
+    • Could not deduce: a arising from a use of ‘MkDict’
+    • In the expression: MkDict
+      In an equation for ‘aux’: aux = MkDict
diff --git a/testsuite/tests/impredicative/T17372.hs b/testsuite/tests/impredicative/T17372.hs
new file mode 100644
index 0000000000..c8a79f3a9e
--- /dev/null
+++ b/testsuite/tests/impredicative/T17372.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE ImpredicativeTypes, ConstraintKinds, GADTs, AllowAmbiguousTypes #-}
+
+module T17372 where
+
+-- This typechecks
+x1 = () :: ((Show a => Num a => Int) ~ ((Show a, Num a) => Int)) => ()
+
+-- -> replace `Num a` with `(Eq a, Ord a)`
+
+-- This doesn't typecheck
+-- Couldn't match type ‘Ord a0 => Int’ with ‘Int’
+x2 = () :: ((Show a => (Eq a, Ord a) => Int) ~ ((Show a, (Eq a, Ord a)) => Int)) => ()
+
+type A a = (Eq a, Ord a)
+
+-- This typechecks
+x3 = () :: (Eq a, Ord a) ~ A a => ()
+
+-- This doesn't typecheck
+-- Couldn't match type ‘()’ with ‘Ord a0 -> ()’
+x4 = () :: (A a => ()) ~ ((Eq a, Ord a) => ()) => ()
+
+-- -> replace `Num a` with `A a` instead
+
+-- This typechecks
+x5 = () :: ((Show a => A a => Int) ~ ((Show a, A a) => Int)) => ()
+
+-- Let's make a type synonym out of the entire constraint
+type C c a = ((Show a => c => Int) ~ ((Show a, c) => Int))
+
+-- Now all of these typecheck:
+x6 = () :: C (Num a) a => ()
+x7 = () :: C (Eq a, Ord a) a => ()
+x8 = () :: C (A a) a => ()
+
+-- This doesn't typecheck
+x9 = () :: ((() => () => Int) ~ (((), ()) => Int)) => ()
+
+-- Let's turn this constraint into a different type synonym
+type B a b = ((a => b => Int) ~ ((a, b) => Int))
+
+-- These both typecheck now:
+x10 = () :: B (Show a) (Num a) => ()
+x11 = () :: B () () => ()
diff --git a/testsuite/tests/impredicative/T18126-1.hs b/testsuite/tests/impredicative/T18126-1.hs
new file mode 100644
index 0000000000..bbc3a6ec40
--- /dev/null
+++ b/testsuite/tests/impredicative/T18126-1.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE ImplicitParams, TypeApplications, ScopedTypeVariables, QuantifiedConstraints, ImpredicativeTypes #-}
+
+module Foo where
+
+import Control.Monad
+import GHC.Stack
+
+wcs :: (?callStack :: CallStack) => ( (?callStack :: CallStack) => a ) -> a
+wcs x = error "urk"
+
+info :: IO ()
+info  = wcs $ (when True $ return ())
diff --git a/testsuite/tests/impredicative/T18126-nasty.hs b/testsuite/tests/impredicative/T18126-nasty.hs
new file mode 100644
index 0000000000..0169a59baf
--- /dev/null
+++ b/testsuite/tests/impredicative/T18126-nasty.hs
@@ -0,0 +1,61 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Bug where
+
+
+-- This nasty example fails with quick-look
+-- (which here is switched on by ($))
+-- beecause of a very subtle issue where we instantiate an
+-- instantiation variable with (F alpha), where F is a type function
+--
+-- It's a stripped-down version of T5490
+
+register :: forall rs op_ty.
+           (HDrop rs ~ HSingle (WaitOpResult op_ty))
+        => rs -> op_ty
+        -> Maybe (WaitOpResult (WaitOps rs))
+        -> Int
+register _ _ ev
+      = ($) -- (px -> qx) -> px -> qx   px=a_a2iT   qx=b_a2iU
+                (foo ev)   -- Instantiate at ax=a2iW bx=a2iX;
+                                  --    (ax,bx) -> Int
+                                  -- ql on arg ev   bx := WaitOpResult (WaitOps rs) = [rs]
+                   -- px := (ax,bx)
+                   -- qx := Int
+                (inj 3)        -- instantiate lx=l_a2iZ;
+                               -- res_ty    (HNth n lx, [lx])
+                   -- res_ty px = (ax,bx) ~ (HNth n lx, [lx])
+                   -- ax := HNth n lx
+                   -- bx := [lx]
+          -- Result ql: WaitOpResult op_ty ~ ax = HNth n lx
+
+{-
+    ($) @(HNth l0, WR (WO rs))
+        @Int
+        (foo ev)
+        (inj 3)
+-}
+
+
+foo :: forall a b . Maybe b -> (a,b) -> Int
+foo = error "urk"
+
+inj :: Int -> (HNth l, [l])
+inj = error "urk"
+
+data HSingle a
+type family HHead l
+type instance HHead (HSingle h) = h
+
+data WaitOps rs
+type family WaitOpResult op
+type instance WaitOpResult (WaitOps rs) = [rs]
+
+type family HDrop l
+
+type HNth l = HHead (HDrop l)
+
+
+
diff --git a/testsuite/tests/boxy/T2193.hs b/testsuite/tests/impredicative/T2193.hs
index c36503eae7..dee542c65c 100644
--- a/testsuite/tests/boxy/T2193.hs
+++ b/testsuite/tests/impredicative/T2193.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-}
+{-# LANGUAGE ImpredicativeTypes  #-}
 
 -- Sept 16: now scraping through with -XImpredicateTypes
 
diff --git a/testsuite/tests/boxy/T2193.stdout b/testsuite/tests/impredicative/T2193.stdout
index b8626c4cff..b8626c4cff 100644
--- a/testsuite/tests/boxy/T2193.stdout
+++ b/testsuite/tests/impredicative/T2193.stdout
diff --git a/testsuite/tests/impredicative/T7026.hs b/testsuite/tests/impredicative/T7026.hs
new file mode 100644
index 0000000000..3ef6ae277b
--- /dev/null
+++ b/testsuite/tests/impredicative/T7026.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE ImplicitParams, ImpredicativeTypes #-}
+
+module Bug where
+
+    f1 :: Maybe ((?a :: Bool) => Char)
+    f1 = Just 'C'
+
+    f2 :: Maybe ((?a :: Bool) => Bool)
+    f2 = Just ?a
diff --git a/testsuite/tests/impredicative/T8808.hs b/testsuite/tests/impredicative/T8808.hs
new file mode 100644
index 0000000000..8b33064a15
--- /dev/null
+++ b/testsuite/tests/impredicative/T8808.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE ImpredicativeTypes, NoMonomorphismRestriction #-}
+
+module Test where
+
+f1 :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
+f1 (Just g) = Just (g [3], g "hello")
+f1 Nothing  = Nothing
+
+f2 :: [forall a. [a] -> [a]] -> Maybe ([Int], [Char])
+f2 [g] = Just (g [3], g "hello")
+f2 []  = Nothing
+
+g1  = (f1 . Just) reverse
+
+g1' = f1 (Just reverse)
+
+g2   = f2 [reverse]
+
+-- Left sections not working yet
+-- g2'  = f2 ((: []) reverse)
+
+g2'' = f2 (reverse : [])
diff --git a/testsuite/tests/impredicative/T9730.hs b/testsuite/tests/impredicative/T9730.hs
new file mode 100644
index 0000000000..7a05cb8e63
--- /dev/null
+++ b/testsuite/tests/impredicative/T9730.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE ImpredicativeTypes, RankNTypes #-}
+
+module T9730 where
+
+class A a where
+
+class B b where
+
+class C c where
+a2b :: (forall a. A a => a) -> (forall b. B b => b)
+a2b = undefined
+
+b2c :: (forall b. B b => b) -> (forall c. C c => c)
+b2c = undefined
+
+a2c :: (forall a. A a => a) -> (forall c. C c => c)
+a2c = b2c . a2b
diff --git a/testsuite/tests/impredicative/all.T b/testsuite/tests/impredicative/all.T
new file mode 100644
index 0000000000..2f23210f6b
--- /dev/null
+++ b/testsuite/tests/impredicative/all.T
@@ -0,0 +1,22 @@
+# Impredicativity tests
+
+test('Church2',  expect_broken(1330), compile_fail, [''])
+
+test('PList1',   normal, compile, [''])
+test('PList2',   normal, compile, [''])
+test('SystemF',  normal, compile, [''])
+test('Base1',    normal, compile, [''])
+test('Church1',  normal, compile, [''])
+test('boxy',     normal, compile, [''])
+test('Compose',  normal, compile, [''])
+test('T2193',    normal, compile_and_run, [''])
+test('icfp20-ok',     normal, compile, [''])
+test('icfp20-fail',   normal, compile_fail, [''])
+test('T18126-1',      normal, compile, [''])
+test('T18126-nasty',  normal, compile, [''])
+test('cabal-example', normal, compile, [''])
+test('T9730', normal, compile, [''])
+test('T7026', normal, compile, [''])
+test('T8808', normal, compile, [''])
+test('T17332', normal, compile_fail, [''])
+test('expr-sig', normal, compile, [''])
diff --git a/testsuite/tests/boxy/boxy.hs b/testsuite/tests/impredicative/boxy.hs
index c4835b1c62..475b5c1c5e 100644
--- a/testsuite/tests/boxy/boxy.hs
+++ b/testsuite/tests/impredicative/boxy.hs
@@ -1,4 +1,4 @@
-{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags -XScopedTypeVariables #-}
+{-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables, TypeApplications #-}
 
 module ShouldCompile where
 
@@ -17,7 +17,6 @@ sing x = [x]
 id1 :: forall a. a -> a
 id1 = id
 
-{-
 ids :: [forall a. a -> a]
 ids = [id1,id1]
 
@@ -29,7 +28,6 @@ t2 = sing id
 
 t3 :: forall a. a -> a
 t3 = head ids
--}
 
 {--------------- Examples from QMLF paper -------------------}
 
@@ -45,13 +43,11 @@ qH choose id = choose id
 choose :: forall a. a -> a -> a
 choose x y = x
 
-{-
 impred1 :: (Bool, Char)
-impred1 = qF $ choose  --- impredicative instantiation for $
+impred1 = ($) qF choose  --- impredicative instantiation for $
 
 impred2 :: (forall a. a -> a -> a) -> (Bool, Char)
 impred2 = id qF
--}
 
 {------ Examples for Garrique/Remy paper -------}
 
@@ -69,33 +65,6 @@ gr2 = self2 id
 
 gr3 = (\(u :: (forall a. a -> a) -> (forall a. a -> a)) -> u id) self1
 
-{------------ Church numerals ----------}
-
-type Church = forall a. a -> (a -> a) -> a
-
-z :: Church
-z = \z -> \f -> z
-
-s :: Church -> Church
-s = \n -> \z -> \f -> f (n z f)
-
-fold :: Church -> a -> (a -> a) -> a
-fold n f z = n f z
-
-{-
-mul :: Church -> Church -> Church
-mul m n = \f -> \a -> m (n f) a
-
-exp :: Church -> Church -> Church
-exp m n = n (mul m) (s z)
-
-idC :: Church -> Church
-idC x = fold x s z
-
-inc :: Church -> Church
-inc x = fold x s (s z)
--}
-
 {------- fix for higher rank types ---------}
 
 data Tree a = Branch a (Tree (a,a)) | Leaf
diff --git a/testsuite/tests/impredicative/cabal-example.hs b/testsuite/tests/impredicative/cabal-example.hs
new file mode 100644
index 0000000000..1da77bf0dd
--- /dev/null
+++ b/testsuite/tests/impredicative/cabal-example.hs
@@ -0,0 +1,47 @@
+{- This example illustrates a nasty case of "vacuous" abstraction
+   It comes from Cabal library Distribution.Simple.Utils
+
+Consider this
+
+  type HCS = (?callStack :: CallStack)
+  wcs :: forall a. (HCS => a) -> a
+  foo :: Int
+  ($) :: forall p q. (p->q) -> p -> q
+
+The call:      wcs $ foo
+
+From QL on the first arg of $ we instantiate wcs with a:=kappa.  Then
+we can work out what p and q must instantiate to.  (the (p->q) arg of
+($) is guarded): get p := (HCS => kappa), q := kappa
+
+But alas, the second arg of $, namely foo, satisfies our
+fiv(rho_r)=empty condition.  (Here rho_r is Int.)  So we try to mgu(
+HCS => kappa, Int ), and fail.
+
+The basic problem is this: we said in 5.4 of the Quick Look paper we
+didn’t about vacuous type abstraction, but we clearly do care about
+type-class abstraction.
+
+How does this work in GHC today, with the built-in rule?  It works
+because we are order-dependent: we look at the first argument first.
+
+The same would work here.  If we applied the QL substitution as we go,
+by the time we got to the second argument, the expected type would
+look like (HCS => kappa), and we would abandon QL on it (App-lightning
+only applies to rho).  But the price is order-dependence.
+-}
+
+module CabalEx where
+
+import GHC.Stack( withFrozenCallStack )
+
+-- withFrozenCallStack :: HasCallStack
+--                     => ( HasCallStack => a )
+--                     -> a
+
+printRawCommandAndArgsAndEnv :: Int -> IO ()
+printRawCommandAndArgsAndEnv = error "urk"
+
+printRawCommandAndArgs :: Int -> IO ()
+printRawCommandAndArgs verbosity
+  = withFrozenCallStack $ printRawCommandAndArgsAndEnv verbosity
diff --git a/testsuite/tests/impredicative/expr-sig.hs b/testsuite/tests/impredicative/expr-sig.hs
new file mode 100644
index 0000000000..7e155ad600
--- /dev/null
+++ b/testsuite/tests/impredicative/expr-sig.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE ImpredicativeTypes, RankNTypes #-}
+
+module ExprSig where
+
+import Data.Kind
+
+f :: [forall a. a->a] -> Int
+f x = error "urk"
+
+g1 = f undefined
+
+-- This should be accepted (and wasn't)
+g2 = f (undefined :: forall b. b)
+
+f3 :: [forall a. a->a] -> b
+f3 x = error "urk"
+
+g3 = f3 (undefined :: forall b. b)
+
diff --git a/testsuite/tests/impredicative/icfp20-fail.hs b/testsuite/tests/impredicative/icfp20-fail.hs
new file mode 100644
index 0000000000..2e077d7ec1
--- /dev/null
+++ b/testsuite/tests/impredicative/icfp20-fail.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE ScopedTypeVariables, TypeApplications, RankNTypes, ImpredicativeTypes #-}
+
+module ICFP20 where
+
+import Control.Monad.ST( ST, runST )
+
+type SId = forall a. a->a
+
+choose :: a -> a -> a
+choose x y = x
+
+single :: a -> [a]
+single x = [x]
+
+auto'2 :: SId -> b -> b
+auto'2 x = id @SId x
+
+-- Fails, and should fail
+auto'1 :: SId -> b -> b
+auto'1 = id
+
+-- Fails, and should do so
+a6 = id auto'2
+
+-- Fails, and should do so
+a8 = choose id auto'2
+
+-- Fails, and should do so
+st2 :: forall a. (forall s. ST s a) -> a
+st2 x = id runST x
diff --git a/testsuite/tests/impredicative/icfp20-fail.stderr b/testsuite/tests/impredicative/icfp20-fail.stderr
new file mode 100644
index 0000000000..c9e06b10cc
--- /dev/null
+++ b/testsuite/tests/impredicative/icfp20-fail.stderr
@@ -0,0 +1,42 @@
+
+icfp20-fail.hs:20:10: error:
+    • Couldn't match type: forall a. a -> a
+                     with: b -> b
+      Expected: SId -> b -> b
+        Actual: SId -> SId
+    • In the expression: id
+      In an equation for ‘auto'1’: auto'1 = id
+    • Relevant bindings include
+        auto'1 :: SId -> b -> b (bound at icfp20-fail.hs:20:1)
+
+icfp20-fail.hs:23:9: error:
+    • Couldn't match expected type ‘a0’
+                  with actual type ‘SId -> b0 -> b0’
+      Cannot instantiate unification variable ‘a0’
+      with a type involving polytypes: SId -> b0 -> b0
+    • In the first argument of ‘id’, namely ‘auto'2’
+      In the expression: id auto'2
+      In an equation for ‘a6’: a6 = id auto'2
+    • Relevant bindings include a6 :: a0 (bound at icfp20-fail.hs:23:1)
+
+icfp20-fail.hs:26:16: error:
+    • Couldn't match type ‘SId’ with ‘b -> b’
+      Expected: (b -> b) -> b -> b
+        Actual: SId -> b -> b
+    • In the second argument of ‘choose’, namely ‘auto'2’
+      In the expression: choose id auto'2
+      In an equation for ‘a8’: a8 = choose id auto'2
+    • Relevant bindings include
+        a8 :: (b -> b) -> b -> b (bound at icfp20-fail.hs:26:1)
+
+icfp20-fail.hs:30:12: error:
+    • Couldn't match type: forall s. ST s a
+                     with: ST s0 a
+      Expected: ST s0 a -> a
+        Actual: (forall s. ST s a) -> a
+    • In the first argument of ‘id’, namely ‘runST’
+      In the expression: id runST x
+      In an equation for ‘st2’: st2 x = id runST x
+    • Relevant bindings include
+        x :: forall s. ST s a (bound at icfp20-fail.hs:30:5)
+        st2 :: (forall s. ST s a) -> a (bound at icfp20-fail.hs:30:1)
diff --git a/testsuite/tests/impredicative/icfp20-ok.hs b/testsuite/tests/impredicative/icfp20-ok.hs
new file mode 100644
index 0000000000..c5b5e6acfc
--- /dev/null
+++ b/testsuite/tests/impredicative/icfp20-ok.hs
@@ -0,0 +1,74 @@
+{-# LANGUAGE ScopedTypeVariables, TypeApplications, RankNTypes, ImpredicativeTypes #-}
+
+module ICFP20 where
+
+import Control.Monad.ST( ST, runST )
+
+type SId = forall a. a->a
+
+ids :: [SId]
+ids = [id,id]
+
+choose :: a -> a -> a
+choose x y = x
+
+auto :: SId -> SId
+auto = id
+
+single :: a -> [a]
+single x = [x]
+
+auto'2 :: SId -> b -> b
+auto'2 x = id @SId x
+
+auto3 :: SId -> b -> b
+auto3 x = id x
+
+poly :: SId -> (Int,Bool)
+poly f = (f (3::Int), f True)
+
+f :: (a->a) -> [a] -> a
+f g xs = g (head xs)
+
+inc :: Int -> Int
+inc x = x+1
+
+app :: (a->b) -> a -> b
+app f x = f x
+
+revapp :: a -> (a->b) -> b
+revapp x f = f x
+
+a3 = choose [] ids
+a5 = id auto
+a7 = choose id auto
+a9 = f (choose id) ids
+a10 = poly id
+a11 = poly (\x -> x)
+a12 = id poly (\x -> x)
+
+c1 = length ids
+c2 = tail ids
+c3 = head ids
+c4 = single id :: [SId]
+c5 = id : ids
+c6 = id : id : ids
+c7 = single inc ++ single id
+c8a = ids ++ single id
+c8b = single id ++ ids
+c9 = map poly (single id)
+
+argST :: forall s. ST s Int
+argST = error "urk"
+
+d1a = poly $ id
+d1b = app poly id
+d2 = revapp id poly
+d3 = runST argST
+d4 = runST $ argST
+
+st1 :: forall a. (forall s. ST s a) -> a
+st1 x = id (runST @a) x
+
+-- Not in the paper's table
+c10 = head ids True
diff --git a/testsuite/tests/linear/should_run/LinearGhci.script b/testsuite/tests/linear/should_run/LinearGhci.script
index 78f81ef8d2..cd55fe73bd 100644
--- a/testsuite/tests/linear/should_run/LinearGhci.script
+++ b/testsuite/tests/linear/should_run/LinearGhci.script
@@ -1,11 +1,11 @@
 data T a = MkT a
-:type +v MkT
+:type MkT
 :set -XLinearTypes
-:type +v MkT
+:type MkT
 :set -XGADTs
 data T a where MkT :: a #-> a -> T a
 :info T
 data T a b m n r = MkT a b m n r
 :set -fprint-explicit-foralls
 -- check that user variables are not renamed (see dataConMulVars)
-:type +v MkT
+:type MkT
diff --git a/testsuite/tests/polykinds/KindVarOrder.script b/testsuite/tests/polykinds/KindVarOrder.script
index c4b4165dcf..945313a6e3 100644
--- a/testsuite/tests/polykinds/KindVarOrder.script
+++ b/testsuite/tests/polykinds/KindVarOrder.script
@@ -4,6 +4,6 @@ data Proxy (a :: k)
 f :: Proxy (a :: k) -> Proxy (b :: j) -> (); f = f
 g :: Proxy (b :: j) -> Proxy (a :: (Proxy :: (k -> Type) -> Type) Proxy) -> (); g = g
 h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> (); h = h
-:t +v f
-:t +v g
-:t +v h
+:t f
+:t g
+:t h
diff --git a/testsuite/tests/typecheck/should_fail/T11355.stderr b/testsuite/tests/typecheck/should_fail/T11355.stderr
index 5310989327..c922e4db93 100644
--- a/testsuite/tests/typecheck/should_fail/T11355.stderr
+++ b/testsuite/tests/typecheck/should_fail/T11355.stderr
@@ -1,7 +1,7 @@
 
 T11355.hs:5:7: error:
     • Illegal polymorphic type: forall a. a
-      GHC doesn't yet support impredicative polymorphism
+      Perhaps you intended to use ImpredicativeTypes
     • In the expression:
         const @_ @((forall a. a) -> forall a. a) () (id @(forall a. a))
       In an equation for ‘foo’:
diff --git a/testsuite/tests/typecheck/should_fail/T2538.stderr b/testsuite/tests/typecheck/should_fail/T2538.stderr
index 18c82bd992..726ac8fd71 100644
--- a/testsuite/tests/typecheck/should_fail/T2538.stderr
+++ b/testsuite/tests/typecheck/should_fail/T2538.stderr
@@ -2,17 +2,14 @@
 T2538.hs:6:6: error:
     • Illegal qualified type: Eq a => a -> a
       Perhaps you intended to use RankNTypes
-    • In the type signature:
-        f :: (Eq a => a -> a) -> Int
+    • In the type signature: f :: (Eq a => a -> a) -> Int
 
 T2538.hs:9:6: error:
     • Illegal qualified type: Eq a => a -> a
-      GHC doesn't yet support impredicative polymorphism
-    • In the type signature:
-        g :: [Eq a => a -> a] -> Int
+      Perhaps you intended to use ImpredicativeTypes
+    • In the type signature: g :: [Eq a => a -> a] -> Int
 
 T2538.hs:12:6: error:
     • Illegal qualified type: Eq a => a -> a
-      GHC doesn't yet support impredicative polymorphism
-    • In the type signature:
-        h :: Ix (Eq a => a -> a) => Int
+      Perhaps you intended to use ImpredicativeTypes
+    • In the type signature: 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 9ec32b3ff6..0e0c867659 100644
--- a/testsuite/tests/typecheck/should_fail/T7809.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7809.stderr
@@ -1,6 +1,6 @@
 
 T7809.hs:8:8: error:
     • Illegal polymorphic type: forall a. a -> a
-      GHC doesn't yet support impredicative polymorphism
+      Perhaps you intended to use ImpredicativeTypes
     • In the expansion of type synonym ‘PolyId’
       In the type signature: foo :: F PolyId
diff --git a/testsuite/tests/typecheck/should_fail/tcfail127.stderr b/testsuite/tests/typecheck/should_fail/tcfail127.stderr
index 6716724860..a262e0113e 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail127.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail127.stderr
@@ -1,6 +1,5 @@
 
 tcfail127.hs:3:8: error:
     • Illegal qualified type: Num a => a -> a
-      GHC doesn't yet support impredicative polymorphism
-    • In the type signature:
-        foo :: IO (Num a => a -> a)
+      Perhaps you intended to use ImpredicativeTypes
+    • In the type signature: foo :: IO (Num a => a -> a)
diff --git a/testsuite/tests/typecheck/should_fail/tcfail196.stderr b/testsuite/tests/typecheck/should_fail/tcfail196.stderr
index 57370d4014..313e7cbdd4 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail196.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail196.stderr
@@ -1,6 +1,5 @@
 
 tcfail196.hs:5:8: error:
     • Illegal polymorphic type: forall a. a
-      GHC doesn't yet support impredicative polymorphism
-    • In the type signature:
-        bar :: Num (forall a. a) => Int -> Int
+      Perhaps you intended to use ImpredicativeTypes
+    • In the type signature: bar :: Num (forall a. a) => Int -> Int
diff --git a/testsuite/tests/typecheck/should_fail/tcfail197.stderr b/testsuite/tests/typecheck/should_fail/tcfail197.stderr
index 1d5f455968..cfbc3fd0dd 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail197.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail197.stderr
@@ -1,6 +1,5 @@
 
 tcfail197.hs:5:8: error:
     • Illegal polymorphic type: forall a. a
-      GHC doesn't yet support impredicative polymorphism
-    • In the type signature:
-        foo :: [forall a. a] -> Int
+      Perhaps you intended to use ImpredicativeTypes
+    • In the type signature: foo :: [forall a. a] -> Int
diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T
index f69cc71352..ef8ae9136d 100755
--- a/testsuite/tests/typecheck/should_run/all.T
+++ b/testsuite/tests/typecheck/should_run/all.T
@@ -58,7 +58,7 @@ test('tcrun038', [extra_files(['TcRun038_B.hs'])], multimod_compile_and_run, ['t
 test('tcrun039', normal, compile_and_run, [''])
 test('tcrun040', normal, compile_and_run, [''])
 test('tcrun041', omit_ways(['ghci']), compile_and_run, [''])
-test('tcrun042', normal, compile, [''])
+test('tcrun042', normal, compile_fail, [''])
 test('tcrun043', normal, compile_and_run, [''])
 test('tcrun044', normal, compile_and_run, [''])
 test('tcrun045', normal, compile_fail, [''])
@@ -96,7 +96,7 @@ test('T6117', normal, compile_and_run, [''])
 test('T5751', normal, compile_and_run, [''])
 test('T5913', normal, compile_and_run, [''])
 test('T7748', normal, compile_and_run, [''])
-test('T7861', [omit_ways(['debug']), exit_code(1)], compile_and_run, [''])
+test('T7861', [expect_broken(18467),omit_ways(['debug']), exit_code(1)], compile_and_run, [''])
 test('TcTypeNatSimpleRun', normal, compile_and_run, [''])
 test('TcTypeSymbolSimpleRun', normal, compile_and_run, [''])
 test('T8119', normal, ghci_script, ['T8119.script'])
diff --git a/testsuite/tests/typecheck/should_run/tcrun042.hs b/testsuite/tests/typecheck/should_run/tcrun042.hs
index ba809a16ba..30c67601ed 100644
--- a/testsuite/tests/typecheck/should_run/tcrun042.hs
+++ b/testsuite/tests/typecheck/should_run/tcrun042.hs
@@ -7,6 +7,11 @@
 --
 -- Apr 20: Works again.  NB: the ImpredicativeTypes flag
 --
+-- July 20: Fails again.  Under Quick Look this now fails, because
+--          we don't have a special typing rule for ExplicitTuples
+--          We could, and it would improve the typing for tuple sections.
+--          But for now I'm just letting it fail, until someone yells.
+--
 -- The test was added by Max in 5e8ff849, apparently to test tuple sections
 
 module Main where
diff --git a/testsuite/tests/typecheck/should_run/tcrun042.stderr b/testsuite/tests/typecheck/should_run/tcrun042.stderr
new file mode 100644
index 0000000000..dcf0854d47
--- /dev/null
+++ b/testsuite/tests/typecheck/should_run/tcrun042.stderr
@@ -0,0 +1,10 @@
+
+tcrun042.hs:20:5: error:
+    • Couldn't match type ‘t0’ with ‘forall b. b -> b -> b’
+      Expected: a
+                -> (forall b. b -> b -> b) -> (a, String, forall c. c -> c -> c)
+        Actual: a -> t0 -> (a, [Char], t0)
+      Cannot instantiate unification variable ‘t0’
+      with a type involving polytypes: forall b. b -> b -> b
+    • In the expression: (, "Hello" ++ "World",)
+      In an equation for ‘e’: e = (, "Hello" ++ "World",)