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.

20 files changed, 89 insertions, 68 deletions

diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 1d639d7f73..6cbe61b2b0 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -16,7 +16,7 @@ import GhcPrelude
 import TcRnTypes
 import TcRnMonad
 import TcMType
-import TcUnify( occCheckForErrors, OccCheckResult(..) )
+import TcUnify( occCheckForErrors, MetaTyVarUpdateResult(..) )
 import TcEnv( tcInitTidyEnv )
 import TcType
 import RnUnbound ( unknownNameSuggestions )
@@ -1632,7 +1632,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
         , report
         ]
 
-  | OC_Occurs <- occ_check_expand
+  | MTVU_Occurs <- occ_check_expand
     -- We report an "occurs check" even for  a ~ F t a, where F is a type
     -- function; it's not insoluble (because in principle F could reduce)
     -- but we have certainly been unable to solve it
@@ -1657,10 +1657,10 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
        ; mkErrorMsgFromCt ctxt ct $
          mconcat [important main_msg, extra2, extra3, report] }
 
-  | OC_Bad <- occ_check_expand
+  | MTVU_Bad <- occ_check_expand
   = do { let msg = vcat [ text "Cannot instantiate unification variable"
                           <+> quotes (ppr tv1)
-                        , hang (text "with a" <+> what <+> text "involving foralls:") 2 (ppr ty2)
+                        , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2)
                         , nest 2 (text "GHC doesn't yet support impredicative polymorphism") ]
        -- Unlike the other reports, this discards the old 'report_important'
        -- instead of augmenting it.  This is because the details are not likely
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index d8b1edf492..cbf98d888c 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -31,7 +31,7 @@ module TcUnify (
   matchActualFunTys, matchActualFunTysPart,
   matchExpectedFunKind,
 
-  metaTyVarUpdateOK, occCheckForErrors, OccCheckResult(..)
+  metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..)
 
   ) where
 
@@ -2115,43 +2115,43 @@ with (forall k. k->*)
 
 -}
 
-data OccCheckResult a
-  = OC_OK a
-  | OC_Bad     -- Forall or type family
-  | OC_Occurs
+data MetaTyVarUpdateResult a
+  = MTVU_OK a
+  | MTVU_Bad     -- Forall, predicate, or type family
+  | MTVU_Occurs
 
-instance Functor OccCheckResult where
+instance Functor MetaTyVarUpdateResult where
       fmap = liftM
 
-instance Applicative OccCheckResult where
-      pure = OC_OK
+instance Applicative MetaTyVarUpdateResult where
+      pure = MTVU_OK
       (<*>) = ap
 
-instance Monad OccCheckResult where
-  OC_OK x    >>= k = k x
-  OC_Bad     >>= _ = OC_Bad
-  OC_Occurs  >>= _ = OC_Occurs
+instance Monad MetaTyVarUpdateResult where
+  MTVU_OK x    >>= k = k x
+  MTVU_Bad     >>= _ = MTVU_Bad
+  MTVU_Occurs  >>= _ = MTVU_Occurs
 
-occCheckForErrors :: DynFlags -> TcTyVar -> Type -> OccCheckResult ()
--- Just for error-message generation; so we return OccCheckResult
+occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult ()
+-- Just for error-message generation; so we return MetaTyVarUpdateResult
 -- so the caller can report the right kind of error
 -- Check whether
 --   a) the given variable occurs in the given type.
 --   b) there is a forall in the type (unless we have -XImpredicativeTypes)
 occCheckForErrors dflags tv ty
   = case preCheck dflags True tv ty of
-      OC_OK _   -> OC_OK ()
-      OC_Bad    -> OC_Bad
-      OC_Occurs -> case occCheckExpand [tv] ty of
-                     Nothing -> OC_Occurs
-                     Just _  -> OC_OK ()
+      MTVU_OK _   -> MTVU_OK ()
+      MTVU_Bad    -> MTVU_Bad
+      MTVU_Occurs -> case occCheckExpand [tv] ty of
+                       Nothing -> MTVU_Occurs
+                       Just _  -> MTVU_OK ()
 
 ----------------
 metaTyVarUpdateOK :: DynFlags
                   -> TcTyVar             -- tv :: k1
                   -> TcType              -- ty :: k2
                   -> Maybe TcType        -- possibly-expanded ty
--- (metaTyFVarUpdateOK tv ty)
+-- (metaTyVarUpdateOK tv ty)
 -- We are about to update the meta-tyvar tv with ty
 -- Check (a) that tv doesn't occur in ty (occurs check)
 --       (b) that ty does not have any foralls
@@ -2178,17 +2178,18 @@ metaTyVarUpdateOK dflags tv ty
   = case preCheck dflags False tv ty of
          -- False <=> type families not ok
          -- See Note [Prevent unification with type families]
-      OC_OK _   -> Just ty
-      OC_Bad    -> Nothing  -- forall or type function
-      OC_Occurs -> occCheckExpand [tv] ty
+      MTVU_OK _   -> Just ty
+      MTVU_Bad    -> Nothing  -- forall, predicate, or type function
+      MTVU_Occurs -> occCheckExpand [tv] ty
 
-preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult ()
+preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult ()
 -- A quick check for
---   (a) a forall type (unless -XImpredivativeTypes)
---   (b) a type family
---   (c) an occurrence of the type variable (occurs check)
+--   (a) a forall type (unless -XImpredicativeTypes)
+--   (b) a predicate type (unless -XImpredicativeTypes)
+--   (c) a type family
+--   (d) an occurrence of the type variable (occurs check)
 --
--- For (a) and (b) we check only the top level of the type, NOT
+-- For (a), (b), and (c) we check only the top level of the type, NOT
 -- inside the kinds of variables it mentions.  But for (c) we do
 -- look in the kinds of course.
 
@@ -2198,25 +2199,28 @@ preCheck dflags ty_fam_ok tv ty
     details          = tcTyVarDetails tv
     impredicative_ok = canUnifyWithPolyType dflags details
 
-    ok :: OccCheckResult ()
-    ok = OC_OK ()
+    ok :: MetaTyVarUpdateResult ()
+    ok = MTVU_OK ()
 
-    fast_check :: TcType -> OccCheckResult ()
+    fast_check :: TcType -> MetaTyVarUpdateResult ()
     fast_check (TyVarTy tv')
-      | tv == tv' = OC_Occurs
+      | tv == tv' = MTVU_Occurs
       | otherwise = fast_check_occ (tyVarKind tv')
            -- See Note [Occurrence checking: look inside kinds]
 
     fast_check (TyConApp tc tys)
-      | bad_tc tc              = OC_Bad
+      | bad_tc tc              = MTVU_Bad
       | otherwise              = mapM fast_check tys >> ok
     fast_check (LitTy {})      = ok
-    fast_check (FunTy _ a r)   = fast_check a   >> fast_check r
+    fast_check (FunTy{ft_af = af, ft_arg = a, ft_res = r})
+      | InvisArg <- af
+      , not impredicative_ok   = MTVU_Bad
+      | otherwise              = fast_check a   >> fast_check r
     fast_check (AppTy fun arg) = fast_check fun >> fast_check arg
     fast_check (CastTy ty co)  = fast_check ty  >> fast_check_co co
     fast_check (CoercionTy co) = fast_check_co co
     fast_check (ForAllTy (Bndr tv' _) ty)
-       | not impredicative_ok = OC_Bad
+       | not impredicative_ok = MTVU_Bad
        | tv == tv'            = ok
        | otherwise = do { fast_check_occ (tyVarKind tv')
                         ; fast_check_occ ty }
@@ -2226,13 +2230,13 @@ preCheck dflags ty_fam_ok tv ty
      -- For kinds, we only do an occurs check; we do not worry
      -- about type families or foralls
      -- See Note [Checking for foralls]
-    fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = OC_Occurs
+    fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = MTVU_Occurs
                      | otherwise                        = ok
 
      -- For coercions, we are only doing an occurs check here;
      -- no bother about impredicativity in coercions, as they're
      -- inferred
-    fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = OC_Occurs
+    fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = MTVU_Occurs
                      | otherwise                       = ok
 
     bad_tc :: TyCon -> Bool
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, [''])