Reject nested predicates in impredicativity checking

When GHC attempts to unify a metavariable with a type containing
foralls, it will be rejected as an occurrence of impredicativity.
GHC was /not/ extending the same treatment to predicate types, such
as in the following (erroneous) example from #11514:

```haskell
foo :: forall a. (Show a => a -> a) -> ()
foo = undefined
```

This will attempt to instantiate `undefined` at
`(Show a => a -> a) -> ()`, which is impredicative. This patch
catches impredicativity arising from predicates in this fashion.

Since GHC is pickier about impredicative instantiations, some test
cases needed to be updated to be updated so as not to fall afoul of
the new validity check. (There were a surprising number of
impredicative uses of `undefined`!) Moreover, the `T14828` test case
now has slightly less informative types shown with `:print`. This is
due to a a much deeper issue with the GHCi debugger (see #14828).

Fixes #11514.

18 files changed, 44 insertions, 27 deletions

diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.hs b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
index c998f0967c..1188bf17d4 100644
--- a/testsuite/tests/dependent/should_compile/dynamic-paper.hs
+++ b/testsuite/tests/dependent/should_compile/dynamic-paper.hs
@@ -34,7 +34,7 @@ fromInteger = Prelude.fromInteger
 
 insertStore = undefined
 schema = undefined
-withTypeable = undefined
+withTypeable _ _ = undefined
 throw# = undefined
 
 toDynamicST = undefined
diff --git a/testsuite/tests/dependent/should_compile/dynamic-paper.stderr b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
index a170d29c46..56da989d37 100644
--- a/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
+++ b/testsuite/tests/dependent/should_compile/dynamic-paper.stderr
@@ -12,4 +12,4 @@ Simplifier ticks exhausted
   simplifier non-termination has been judged acceptable.
    
   To see detailed counts use -ddump-simpl-stats
-  Total ticks: 140007
+  Total ticks: 140086
diff --git a/testsuite/tests/ghci.debugger/scripts/print027.stdout b/testsuite/tests/ghci.debugger/scripts/print027.stdout
index 3117eace87..eb5b363693 100644
--- a/testsuite/tests/ghci.debugger/scripts/print027.stdout
+++ b/testsuite/tests/ghci.debugger/scripts/print027.stdout
@@ -1,6 +1,6 @@
-+ = (_t1::Num a => a -> a -> a)
-print = (_t2::Show a1 => a1 -> IO ())
-log = (_t3::Floating a2 => a2 -> a2)
-head = (_t4::[a4] -> a4)
-tail = (_t5::[a7] -> [a7])
-fst = (_t6::(a11, b) -> a11)
++ = (_t1::t1)
+print = (_t2::t1)
+log = (_t3::t1)
+head = (_t4::[a] -> a)
+tail = (_t5::[a1] -> [a1])
+fst = (_t6::(a2, b) -> a2)
diff --git a/testsuite/tests/ghci/scripts/T12447.script b/testsuite/tests/ghci/scripts/T12447.script
index 6003a43838..3bdd3f4b73 100644
--- a/testsuite/tests/ghci/scripts/T12447.script
+++ b/testsuite/tests/ghci/scripts/T12447.script
@@ -4,6 +4,6 @@ import Data.Typeable
 
 class Deferrable p where deferEither :: proxy p -> (p => r) -> Either String r
 
-instance (Typeable a, Typeable b) => Deferrable (a ~ b) where deferEither = undefined
+instance (Typeable a, Typeable b) => Deferrable (a ~ b) where deferEither _ _ = undefined
 
 :t deferEither @(_ ~ _)
diff --git a/testsuite/tests/ghci/scripts/T14828.stdout b/testsuite/tests/ghci/scripts/T14828.stdout
index 3ef2e602ec..9ccea0ceec 100644
--- a/testsuite/tests/ghci/scripts/T14828.stdout
+++ b/testsuite/tests/ghci/scripts/T14828.stdout
@@ -6,7 +6,7 @@ return :: Monad m => a -> m a
 return = (_t3::t1)
 pure :: Applicative f => a -> f a
 pure = (_t4::t1)
-mempty = (_t5::Monoid a => a)
-mappend = (_t6::Monoid a => a -> a -> a)
+mempty = (_t5::t1)
+mappend = (_t6::t1)
 foldl' = (_t7::t1)
 f = (_t8::t1)
diff --git a/testsuite/tests/indexed-types/should_compile/T4358.hs b/testsuite/tests/indexed-types/should_compile/T4358.hs
index 0c05576812..cb05a1c1aa 100644
--- a/testsuite/tests/indexed-types/should_compile/T4358.hs
+++ b/testsuite/tests/indexed-types/should_compile/T4358.hs
@@ -6,6 +6,6 @@ type family T a
 
 t2 :: forall a. ((T a ~ a) => a) -> a
 t2 = t
-  
+
 t :: forall a. ((T a ~ a) => a) -> a
-t = undefined
+t _ = undefined
diff --git a/testsuite/tests/indexed-types/should_fail/T5934.stderr b/testsuite/tests/indexed-types/should_fail/T5934.stderr
index 21af0d868a..e7448a9722 100644
--- a/testsuite/tests/indexed-types/should_fail/T5934.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5934.stderr
@@ -1,7 +1,7 @@
 
 T5934.hs:12:7: error:
     • Cannot instantiate unification variable ‘a0’
-      with a type involving foralls: (forall s. GenST s) -> Int
+      with a type involving polytypes: (forall s. GenST s) -> Int
         GHC doesn't yet support impredicative polymorphism
     • In the expression: 0
       In an equation for ‘run’: run = 0
diff --git a/testsuite/tests/polykinds/T11142.stderr b/testsuite/tests/polykinds/T11142.stderr
index a3b40c1222..4f5c5fcf29 100644
--- a/testsuite/tests/polykinds/T11142.stderr
+++ b/testsuite/tests/polykinds/T11142.stderr
@@ -7,7 +7,7 @@ T11142.hs:9:49: error:
 
 T11142.hs:10:7: error:
     • Cannot instantiate unification variable ‘a0’
-      with a type involving foralls:
+      with a type involving polytypes:
         (forall k1 (a :: k1). SameKind a b) -> ()
         GHC doesn't yet support impredicative polymorphism
     • In the expression: undefined
diff --git a/testsuite/tests/polykinds/T14270.hs b/testsuite/tests/polykinds/T14270.hs
index 3eed83c657..d578be344e 100644
--- a/testsuite/tests/polykinds/T14270.hs
+++ b/testsuite/tests/polykinds/T14270.hs
@@ -76,7 +76,7 @@ splitApp rep@(TrFun _ a b) = Just (IsApp (mkTrApp arr a) b)
 splitApp (TrTyCon{})       = Nothing
 
 withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r
-withTypeable = undefined
+withTypeable _ _ = undefined
 
 eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
              TypeRep a -> TypeRep b -> Maybe (a :~~: b)
diff --git a/testsuite/tests/polykinds/T9569.hs b/testsuite/tests/polykinds/T9569.hs
index 1b8bb68c75..634d742803 100644
--- a/testsuite/tests/polykinds/T9569.hs
+++ b/testsuite/tests/polykinds/T9569.hs
@@ -11,7 +11,7 @@ class Deferrable (c :: Constraint) where
 
 deferPair :: (Deferrable c1, Deferrable c2) =>
                   Proxy (c1,c2) -> ((c1,c2) => a) -> a
-deferPair = undefined
+deferPair _ _ = undefined
 
 instance (Deferrable c1, Deferrable c2) => Deferrable (c1,c2) where
     -- defer p f = deferPair p f     -- Succeeds
diff --git a/testsuite/tests/th/T11452.stderr b/testsuite/tests/th/T11452.stderr
index 32064a9c78..e4f1cc604d 100644
--- a/testsuite/tests/th/T11452.stderr
+++ b/testsuite/tests/th/T11452.stderr
@@ -8,7 +8,7 @@ T11452.hs:6:14: error:
 
 T11452.hs:6:14: error:
     • Cannot instantiate unification variable ‘p0’
-      with a type involving foralls: forall a. a -> a
+      with a type involving polytypes: forall a. a -> a
         GHC doesn't yet support impredicative polymorphism
     • In the Template Haskell quotation [|| \ _ -> () ||]
       In the expression: [|| \ _ -> () ||]
diff --git a/testsuite/tests/typecheck/should_compile/T12427a.stderr b/testsuite/tests/typecheck/should_compile/T12427a.stderr
index 05e926067f..efc87a1fc3 100644
--- a/testsuite/tests/typecheck/should_compile/T12427a.stderr
+++ b/testsuite/tests/typecheck/should_compile/T12427a.stderr
@@ -3,7 +3,8 @@ T12427a.hs:17:29: error:
     • Couldn't match expected type ‘p’
                   with actual type ‘(forall b. [b] -> [b]) -> Int’
       ‘p’ is a rigid type variable bound by
-        the inferred type of h11 :: T -> p at T12427a.hs:17:1-29
+        the inferred type of h11 :: T -> p
+        at T12427a.hs:17:1-29
     • In the expression: v
       In a case alternative: T1 _ v -> v
       In the expression: case y of { T1 _ v -> v }
@@ -12,7 +13,7 @@ T12427a.hs:17:29: error:
 
 T12427a.hs:28:6: error:
     • Cannot instantiate unification variable ‘p0’
-      with a type involving foralls: (forall b. [b] -> [b]) -> Int
+      with a type involving polytypes: (forall b. [b] -> [b]) -> Int
         GHC doesn't yet support impredicative polymorphism
     • In the pattern: T1 _ x1
       In a pattern binding: T1 _ x1 = undefined
diff --git a/testsuite/tests/typecheck/should_fail/T10194.stderr b/testsuite/tests/typecheck/should_fail/T10194.stderr
index 7bc79b2e6f..aeaad79440 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: error:
-    Cannot instantiate unification variable ‘b0’
-    with a type involving foralls: X
-      GHC doesn't yet support impredicative polymorphism
-    In the expression: (.)
-    In an equation for ‘comp’: comp = (.)
+    • Cannot instantiate unification variable ‘b0’
+      with a type involving polytypes: X
+        GHC doesn't yet support impredicative polymorphism
+    • In the expression: (.)
+      In an equation for ‘comp’: comp = (.)
diff --git a/testsuite/tests/typecheck/should_fail/T11514.hs b/testsuite/tests/typecheck/should_fail/T11514.hs
new file mode 100644
index 0000000000..f0dc07a22c
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T11514.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE RankNTypes #-}
+
+module T11514 where
+
+foo :: forall a. (Show a => a -> a) -> ()
+foo = undefined
diff --git a/testsuite/tests/typecheck/should_fail/T11514.stderr b/testsuite/tests/typecheck/should_fail/T11514.stderr
new file mode 100644
index 0000000000..62acf15b73
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T11514.stderr
@@ -0,0 +1,9 @@
+
+T11514.hs:6:7: error:
+    • Cannot instantiate unification variable ‘a0’
+      with a type involving polytypes: (Show a => a -> a) -> ()
+        GHC doesn't yet support impredicative polymorphism
+    • In the expression: undefined
+      In an equation for ‘foo’: foo = undefined
+    • Relevant bindings include
+        foo :: (Show a => a -> a) -> () (bound at T11514.hs:6:1)
diff --git a/testsuite/tests/typecheck/should_fail/T12563.stderr b/testsuite/tests/typecheck/should_fail/T12563.stderr
index f32e99d1f0..e6619aa1da 100644
--- a/testsuite/tests/typecheck/should_fail/T12563.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12563.stderr
@@ -1,7 +1,7 @@
 
 T12563.hs:7:15: error:
     • Cannot instantiate unification variable ‘p0’
-      with a type involving foralls: (forall a. f0 a) -> f0 r0
+      with a type involving polytypes: (forall a. f0 a) -> f0 r0
         GHC doesn't yet support impredicative polymorphism
     • In the first argument of ‘foo’, namely ‘g’
       In the expression: foo g
diff --git a/testsuite/tests/typecheck/should_fail/T12589.stderr b/testsuite/tests/typecheck/should_fail/T12589.stderr
index 5e92f3af86..3f380e47a4 100644
--- a/testsuite/tests/typecheck/should_fail/T12589.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12589.stderr
@@ -3,7 +3,7 @@ T12589.hs:13:3: error: Variable not in scope: (&) :: t1 -> t0 -> t
 
 T12589.hs:13:5: error:
     • Cannot instantiate unification variable ‘t0’
-      with a type involving foralls:
+      with a type involving polytypes:
         (forall a. Bounded a => f0 a) -> h0 f0 xs0
         GHC doesn't yet support impredicative polymorphism
     • In the second argument of ‘(&)’, namely ‘hcpure (Proxy @Bounded)’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 6344d74c7a..d155ca0e8c 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -390,6 +390,7 @@ test('T11347', normal, compile_fail, [''])
 test('T11356', normal, compile_fail, [''])
 test('T11355', normal, compile_fail, [''])
 test('T11464', normal, compile_fail, [''])
+test('T11514', normal, compile_fail, [''])
 test('T11563', normal, compile_fail, [''])
 test('T11541', normal, compile_fail, [''])
 test('T11313', normal, compile_fail, [''])