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)

24 files changed, 700 insertions, 0 deletions

diff --git a/testsuite/tests/impredicative/Base1.hs b/testsuite/tests/impredicative/Base1.hs
new file mode 100644
index 0000000000..5e3b377ee2
--- /dev/null
+++ b/testsuite/tests/impredicative/Base1.hs
@@ -0,0 +1,33 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+
+-- Sept 16: now failing, because I've further reduced the scop
+--          of impredicative types
+
+module Base1 where
+-- basic examples of impredicative instantiation of variables
+
+data MEither a b = MLeft a
+                 | MRight b
+                 | MEmpty
+
+type Sid = forall a. a -> a
+
+-- no need for impredicativity
+test0 = MRight id
+
+-- requires impredicativity
+test1 :: Sid -> MEither Sid b
+test1 fid = MLeft fid
+
+test2 :: MEither b Sid -> Maybe (Sid,Sid)
+test2 m = case (test1 id) of
+             MLeft x -> case m of
+                          MRight y -> Just (x,y)
+                          _ -> Nothing
+             _ -> Nothing
+
+test3 :: MEither a b -> b
+test3 (MRight x) = x
+
+test4 = test3 (test1 id)
+
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/impredicative/Compose.hs b/testsuite/tests/impredicative/Compose.hs
new file mode 100644
index 0000000000..f3d3a10b28
--- /dev/null
+++ b/testsuite/tests/impredicative/Compose.hs
@@ -0,0 +1,26 @@
+{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags -XEmptyDataDecls -XGADTs #-}
+
+-- #1118
+
+module Compose where
+
+data Z
+data S n
+
+data List n a where
+    Nil :: List Z a
+    (:-) :: a -> List n a -> List (S n) a
+
+data Hold a = Hold (forall m . a m -> a (S m))
+
+compose' :: List n (Hold a) -> a (S Z) -> a (S n)
+compose' Nil x = x
+compose' ((Hold f) :- fs) x = f (compose' fs x)
+
+compose :: List n (forall m . a m -> a (S m)) -> a (S Z) -> a (S n)
+compose Nil x = x
+compose (f :- fs) x = f (compose fs x)
+
+composeS :: [forall m . a m -> a m] -> a n -> a n
+composeS [] x = x
+composeS (f:fs) x = f (composeS fs x)
diff --git a/testsuite/tests/impredicative/Makefile b/testsuite/tests/impredicative/Makefile
new file mode 100644
index 0000000000..9a36a1c5fe
--- /dev/null
+++ b/testsuite/tests/impredicative/Makefile
@@ -0,0 +1,3 @@
+TOP=../..
+include $(TOP)/mk/boilerplate.mk
+include $(TOP)/mk/test.mk
diff --git a/testsuite/tests/impredicative/PList1.hs b/testsuite/tests/impredicative/PList1.hs
new file mode 100644
index 0000000000..27cedc1f49
--- /dev/null
+++ b/testsuite/tests/impredicative/PList1.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+
+module PList1 where
+-- Polymorphic lists 1: requires smart-app-res
+
+type Sid = forall a . a -> a
+
+ids :: [Sid]
+ids = []
+
+-- requires smart-app-res
+test0 :: [Sid]
+test0 = (\x->x) : ids
+
+test1 :: [Sid]  -- SLPJ added
+test1 = ids ++ test0
+
+test2 :: [Sid]
+test2 = tail test1
+
+
+test3 :: [Sid]  -- SLPJ added
+test3 = reverse test2
+test4 = (tail::([Sid]->[Sid])) test2
+
+test5 = (head::([Sid]->Sid)) test2
diff --git a/testsuite/tests/impredicative/PList2.hs b/testsuite/tests/impredicative/PList2.hs
new file mode 100644
index 0000000000..316e8792ae
--- /dev/null
+++ b/testsuite/tests/impredicative/PList2.hs
@@ -0,0 +1,27 @@
+{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags #-}
+
+module PList2 where
+-- Polymorphic lists 2: require smart-app-arg & smart-app-res: Should fail w/o smart-app-arg
+
+type Sid = forall a. a -> a
+
+ids :: [Sid]
+ids = []
+
+test0 :: [Sid]
+test0 = (\x -> x):ids  -- requires smart-app-res
+
+test1 :: [Sid]  -- Added SLPJ
+test1 = ids ++ test0
+
+test2 :: [Sid]
+test2 = tail test1 -- requires smart-app-arg
+
+test3 :: [Sid]  -- Added SLPJ
+test3 = reverse test2
+
+test4 :: Sid
+test4 = head ids  --requires smart-app-arg
+
+test5 :: Sid
+test5 = head ids  -- still requires smart-app-arg
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/impredicative/T2193.hs b/testsuite/tests/impredicative/T2193.hs
new file mode 100644
index 0000000000..dee542c65c
--- /dev/null
+++ b/testsuite/tests/impredicative/T2193.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE ImpredicativeTypes  #-}
+
+-- Sept 16: now scraping through with -XImpredicateTypes
+
+module Main where
+
+data Foo x y = Foo {foo1 :: x, foo2 :: y}
+instance Functor (Foo x) where
+    fmap f (Foo x y) = Foo x (f y)
+
+bar :: a -> Foo (forall s. s) a
+bar a = Foo undefined a
+
+main = print (foo2 (fmap (*2) (bar 2)))
+
diff --git a/testsuite/tests/impredicative/T2193.stdout b/testsuite/tests/impredicative/T2193.stdout
new file mode 100644
index 0000000000..b8626c4cff
--- /dev/null
+++ b/testsuite/tests/impredicative/T2193.stdout
@@ -0,0 +1 @@
+4
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/impredicative/boxy.hs b/testsuite/tests/impredicative/boxy.hs
new file mode 100644
index 0000000000..475b5c1c5e
--- /dev/null
+++ b/testsuite/tests/impredicative/boxy.hs
@@ -0,0 +1,93 @@
+{-# LANGUAGE ImpredicativeTypes, ScopedTypeVariables, TypeApplications #-}
+
+module ShouldCompile where
+
+
+{-------- Examples from the paper ---------}
+
+f :: (forall a. [a] -> a) -> (Int, Char)
+f get = (get [1,2], get ['a', 'b', 'c'])
+
+g :: Maybe (forall a. [a] -> a) -> (Int, Char)
+g Nothing = (0, '0')
+g (Just get) = (get [1,2], get ['a','b','c'])
+
+sing x = [x]
+
+id1 :: forall a. a -> a
+id1 = id
+
+ids :: [forall a. a -> a]
+ids = [id1,id1]
+
+t1 :: [forall a. a -> a]
+t1 = tail ids
+
+t2 :: [forall a. a -> a]
+t2 = sing id
+
+t3 :: forall a. a -> a
+t3 = head ids
+
+{--------------- Examples from QMLF paper -------------------}
+
+qF :: (forall a. a -> a -> a) -> (Bool, Char)
+qF choose = (choose True False, choose 'a' 'b')
+
+qG :: (forall a. a -> a -> a) -> (forall a. a -> a) -> (forall g. (g -> g) -> (g -> g))
+qG choose id = choose id
+
+qH :: (forall a. a -> a -> a) -> (forall a. a -> a) -> (forall b. b -> b) -> (forall b. b -> b)
+qH choose id = choose id
+
+choose :: forall a. a -> a -> a
+choose x y = x
+
+impred1 :: (Bool, Char)
+impred1 = ($) qF choose  --- impredicative instantiation for $
+
+impred2 :: (forall a. a -> a -> a) -> (Bool, Char)
+impred2 = id qF
+
+{------ Examples for Garrique/Remy paper -------}
+
+--- all of these currently work in GHC with higher-rank types
+
+self1 :: (forall a. a -> a) -> (forall a. a -> a)
+self1 f = f f
+
+self2 :: (forall a. a -> a) -> b -> b
+self2 f = f f
+
+gr1 = self1 id
+
+gr2 = self2 id
+
+gr3 = (\(u :: (forall a. a -> a) -> (forall a. a -> a)) -> u id) self1
+
+{------- fix for higher rank types ---------}
+
+data Tree a = Branch a (Tree (a,a)) | Leaf
+
+type MapTree = forall a b. (a -> b) -> Tree a -> Tree b
+cross f (a,b) = (f a,f b)
+
+-- I think this should work in GHC now, but it doesn't
+-- fix specialized to higher-rank type
+fixMT :: (MapTree -> MapTree) -> MapTree
+fixMT f = f (fixMT f)
+
+mapTree' = fixMT (\ (mapTree :: MapTree) -> \f tree -> case tree of
+                            Branch a t -> Branch (f a) (mapTree (cross f) t)
+                            Leaf -> Leaf)
+
+-- polymorphic fix
+fix :: (a -> a) -> a
+fix f = f (fix f)
+
+
+-- mapTree'' :: MapTree
+mapTree'' = (fix :: (MapTree -> MapTree) -> MapTree)
+               (\ mapTree -> \f tree -> case tree of
+                            Branch a t -> Branch (f a) (mapTree (cross f) t)
+                            Leaf -> 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