Control validity-checking of type synonym applications more carefully

Trac #16059 shows that when validity checking applications of type
synonyms, GHC sometimes wasn't checking the expanded type enough.
We must be careful, however, since checking both the expanded type as
well as the arguments to the type synonym can lead to exponential
blowup (see https://ghc.haskell.org/trac/ghc/ticket/16059#comment:4).
Nor can we omit checking either the expanded type or the argument for
correctness reasons.

The solution here is to introduce a new `ExpandMode` data type that
is plumbed through all of the type-validity-checking functions in
`TcValidity`. `ExpandMode` dictates whether we only check the
expanded type (`Expand`), only check the arguments (`NoExpand), or
both (`Both`). Importantly, if we check `Both` in the function for
validity checking type synonym applications, then we switch to
`NoExpand` when checking the arguments so as to avoid exponential
blowup. See `Note [Correctness and performance of type synonym validity
checking]` for the full story.

13 files changed, 86 insertions, 14 deletions

diff --git a/testsuite/tests/safeHaskell/unsafeLibs/Dep05.hs b/testsuite/tests/safeHaskell/unsafeLibs/Dep05.hs
index a5c13bb5aa..1d64daa5ae 100644
--- a/testsuite/tests/safeHaskell/unsafeLibs/Dep05.hs
+++ b/testsuite/tests/safeHaskell/unsafeLibs/Dep05.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE Safe #-}
 {-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE UnboxedTuples #-}
 module Dep05 where
 
 import GHC.Arr
diff --git a/testsuite/tests/safeHaskell/unsafeLibs/Dep05.stderr b/testsuite/tests/safeHaskell/unsafeLibs/Dep05.stderr
index a35d679f8d..4c93c907e8 100644
--- a/testsuite/tests/safeHaskell/unsafeLibs/Dep05.stderr
+++ b/testsuite/tests/safeHaskell/unsafeLibs/Dep05.stderr
@@ -1,3 +1,3 @@
 
-Dep05.hs:5:1:
+Dep05.hs:6:1: error:
     GHC.Arr: Can't be safely imported! The module itself isn't safe.
diff --git a/testsuite/tests/typecheck/should_fail/T16059a.hs b/testsuite/tests/typecheck/should_fail/T16059a.hs
new file mode 100644
index 0000000000..1eb9e67bcc
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059a.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T16059a where
+
+type Foo b = Eq b => b
+
+f :: forall b (a :: Eq b => b). Int
+f = 27
+
+g :: forall b (a :: Foo b). Int
+g = 42
diff --git a/testsuite/tests/typecheck/should_fail/T16059a.stderr b/testsuite/tests/typecheck/should_fail/T16059a.stderr
new file mode 100644
index 0000000000..2768220653
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059a.stderr
@@ -0,0 +1,9 @@
+
+T16059a.hs:8:6: error:
+    • Illegal constraint in a kind: Eq b => b
+    • In the type signature: f :: forall b (a :: Eq b => b). Int
+
+T16059a.hs:11:6: error:
+    • Illegal constraint in a kind: Eq b => b
+    • In the expansion of type synonym ‘Foo’
+      In the type signature: g :: forall b (a :: Foo b). Int
diff --git a/testsuite/tests/typecheck/should_fail/T16059b.hs b/testsuite/tests/typecheck/should_fail/T16059b.hs
new file mode 100644
index 0000000000..a8097b9951
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059b.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UnboxedTuples #-}
+module T16059b where
+
+type Foo = forall a. a
+type Bar = (# #)
diff --git a/testsuite/tests/typecheck/should_fail/T16059c.hs b/testsuite/tests/typecheck/should_fail/T16059c.hs
new file mode 100644
index 0000000000..d26c7db6d4
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059c.hs
@@ -0,0 +1,6 @@
+module T16059c where
+
+import T16059b
+
+f :: Foo -> a -> f
+f g x = g x
diff --git a/testsuite/tests/typecheck/should_fail/T16059c.stderr b/testsuite/tests/typecheck/should_fail/T16059c.stderr
new file mode 100644
index 0000000000..6c6113fb5f
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059c.stderr
@@ -0,0 +1,6 @@
+
+T16059c.hs:5:6: error:
+    • Illegal polymorphic type: forall a1. a1
+      Perhaps you intended to use RankNTypes
+    • In the expansion of type synonym ‘Foo’
+      In the type signature: f :: Foo -> a -> f
diff --git a/testsuite/tests/typecheck/should_fail/T16059d.hs b/testsuite/tests/typecheck/should_fail/T16059d.hs
new file mode 100644
index 0000000000..0c61136323
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059d.hs
@@ -0,0 +1,5 @@
+module T16059d where
+
+import T16059b
+
+type Bar' = Bar
diff --git a/testsuite/tests/typecheck/should_fail/T16059d.stderr b/testsuite/tests/typecheck/should_fail/T16059d.stderr
new file mode 100644
index 0000000000..7932d72858
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059d.stderr
@@ -0,0 +1,6 @@
+
+T16059d.hs:5:1: error:
+    • Illegal unboxed tuple type as function argument: (# #)
+      Perhaps you intended to use UnboxedTuples
+    • In the expansion of type synonym ‘Bar’
+      In the type synonym declaration for ‘Bar'’
diff --git a/testsuite/tests/typecheck/should_fail/T16059e.hs b/testsuite/tests/typecheck/should_fail/T16059e.hs
new file mode 100644
index 0000000000..4747edc302
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059e.hs
@@ -0,0 +1,15 @@
+module T16059e where
+
+import T16059b
+
+type Const a b = a
+
+-- This is accepted, since the rank-n type `Foo` never makes it into the type
+-- of `f` post-expansion...
+f :: Const Int Foo -> Int
+f _ = 42
+
+-- ...but this *is* rejected, since `Foo` does make it into the type of `g`
+-- post-expansion.
+g :: Const Foo Foo -> Int
+g _ = f 27
diff --git a/testsuite/tests/typecheck/should_fail/T16059e.stderr b/testsuite/tests/typecheck/should_fail/T16059e.stderr
new file mode 100644
index 0000000000..f5a6bb00ba
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T16059e.stderr
@@ -0,0 +1,7 @@
+
+T16059e.hs:14:6: error:
+    • Illegal polymorphic type: forall a. a
+      Perhaps you intended to use RankNTypes
+    • In the expansion of type synonym ‘Foo’
+      In the expansion of type synonym ‘Const’
+      In the type signature: g :: Const Foo Foo -> Int
diff --git a/testsuite/tests/typecheck/should_fail/T9858a.stderr b/testsuite/tests/typecheck/should_fail/T9858a.stderr
index a42339ed78..fcf76ef247 100644
--- a/testsuite/tests/typecheck/should_fail/T9858a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9858a.stderr
@@ -1,14 +1,6 @@
 
-T9858a.hs:28:18: error:
-    No instance for (Typeable
-                       ((() :: Constraint, () :: Constraint) => ()))
-      arising from a use of ‘cast’
-      (maybe you haven't applied a function to enough arguments?)
-    In the expression: cast e
-    In the expression: case cast e of { Just e' -> ecast e' }
-    In an equation for ‘supercast’:
-        supercast
-          = case cast e of { Just e' -> ecast e' }
-          where
-              e = Refl
-              e :: E PX PX
+T9858a.hs:20:18: error:
+    • Illegal qualified type:
+        (() :: Constraint, () :: Constraint) => ()
+    • In the expansion of type synonym ‘PX’
+      In the newtype instance declaration for ‘F’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index bac4d6b14e..9bd518f10c 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -501,3 +501,10 @@ test('T15797', normal, compile_fail, [''])
 test('T15799', normal, compile_fail, [''])
 test('T15801', normal, compile_fail, [''])
 test('T15816', normal, compile_fail, [''])
+test('T16059a', normal, compile_fail, [''])
+test('T16059c', [extra_files(['T16059b.hs'])], multimod_compile_fail,
+    ['T16059c', '-v0'])
+test('T16059d', [extra_files(['T16059b.hs'])], multimod_compile_fail,
+    ['T16059d', '-v0'])
+test('T16059e', [extra_files(['T16059b.hs'])], multimod_compile_fail,
+    ['T16059e', '-v0'])