Track type variable scope more carefully.

The main job of this commit is to track more accurately the scope
of tyvars introduced by user-written foralls. For example, it would
be to have something like this:

  forall a. Int -> (forall k (b :: k). Proxy '[a, b]) -> Bool

In that type, a's kind must be k, but k isn't in scope. We had a
terrible way of doing this before (not worth repeating or describing
here, but see the old tcImplicitTKBndrs and friends), but now
we have a principled approach: make an Implication when kind-checking
a forall. Doing so then hooks into the existing machinery for
preventing skolem-escape, performing floating, etc. This also means
that we bump the TcLevel whenever going into a forall.

The new behavior is done in TcHsType.scopeTyVars, but see also
TcHsType.tc{Im,Ex}plicitTKBndrs, which have undergone significant
rewriting. There are several Notes near there to guide you. Of
particular interest there is that Implication constraints can now
have skolems that are out of order; this situation is reported in
TcErrors.

A major consequence of this is a slightly tweaked process for type-
checking type declarations. The new Note [Use SigTvs in kind-checking
pass] in TcTyClsDecls lays it out.

The error message for dependent/should_fail/TypeSkolEscape has become
noticeably worse. However, this is because the code in TcErrors goes to
some length to preserve pre-8.0 error messages for kind errors. It's time
to rip off that plaster and get rid of much of the kind-error-specific
error messages. I tried this, and doing so led to a lovely error message
for TypeSkolEscape. So: I'm accepting the error message quality regression
for now, but will open up a new ticket to fix it, along with a larger
error-message improvement I've been pondering. This applies also to
dependent/should_fail/{BadTelescope2,T14066,T14066e}, polykinds/T11142.

Other minor changes:
 - isUnliftedTypeKind didn't look for tuples and sums. It does now.

 - check_type used check_arg_type on both sides of an AppTy. But the left
   side of an AppTy isn't an arg, and this was causing a bad error message.
   I've changed it to use check_type on the left-hand side.

 - Some refactoring around when we print (TYPE blah) in error messages.
   The changes decrease the times when we do so, to good effect.
   Of course, this is still all controlled by
   -fprint-explicit-runtime-reps

Fixes #14066 #14749

Test cases: dependent/should_compile/{T14066a,T14749},
            dependent/should_fail/T14066{,c,d,e,f,g,h}

24 files changed, 193 insertions, 30 deletions

diff --git a/testsuite/tests/dependent/should_fail/BadTelescope.stderr b/testsuite/tests/dependent/should_fail/BadTelescope.stderr
index 2fbc35a9ba..5fa8efd502 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope.stderr
@@ -1,9 +1,6 @@
 
 BadTelescope.hs:9:1: error:
-    • These kind and type variables: (a :: k)
-                                     k
-                                     (b :: k)
-                                     (c :: SameKind a b)
+    • These kind and type variables: a k (b :: k) (c :: SameKind a b)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k) (c :: SameKind a b)
     • In the data type declaration for ‘X’
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
index 2a9dc76310..55a484910c 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope2.stderr
@@ -3,14 +3,11 @@ BadTelescope2.hs:10:8: error:
     • These kind and type variables: a k (b :: k)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k)
-    • In the type signature:
-        foo :: forall a k (b :: k). SameKind a b
+    • In the type signature: foo :: forall a k (b :: k). SameKind a b
 
-BadTelescope2.hs:13:8: error:
-    • The kind of variable ‘b’, namely ‘Proxy a’,
-      depends on variable ‘a’ from an inner scope
-      Perhaps bind ‘b’ sometime after binding ‘a’
-      NB: Implicitly-bound variables always come before other ones.
-    • In the type signature:
+BadTelescope2.hs:13:70: error:
+    • Expected kind ‘k0’, but ‘d’ has kind ‘Proxy a’
+    • In the second argument of ‘SameKind’, namely ‘d’
+      In the type signature:
         bar :: forall a (c :: Proxy b) (d :: Proxy a).
                Proxy c -> SameKind b d
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope3.stderr b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
index 4ea7458bb2..1137f28c4d 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope3.stderr
@@ -1,6 +1,6 @@
 
 BadTelescope3.hs:9:1: error:
-    • These kind and type variables: (a :: k) k (b :: k)
+    • These kind and type variables: a k (b :: k)
       are out of dependency order. Perhaps try this ordering:
         k (a :: k) (b :: k)
     • In the type synonym declaration for ‘S’
diff --git a/testsuite/tests/dependent/should_fail/BadTelescope4.stderr b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
index 2394f896ad..f7c281e983 100644
--- a/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
+++ b/testsuite/tests/dependent/should_fail/BadTelescope4.stderr
@@ -1,6 +1,6 @@
 
 BadTelescope4.hs:9:1: error:
-    • These kind and type variables: (a :: k)
+    • These kind and type variables: a
                                      (c :: Proxy b)
                                      (d :: Proxy a)
                                      (x :: SameKind b d)
@@ -11,5 +11,5 @@ BadTelescope4.hs:9:1: error:
         (c :: Proxy b)
         (d :: Proxy a)
         (x :: SameKind b d)
-      NB: Implicitly declared kind variables are put first.
+      NB: Implicitly declared variables come before others.
     • In the data type declaration for ‘Bad’
diff --git a/testsuite/tests/dependent/should_fail/InferDependency.stderr b/testsuite/tests/dependent/should_fail/InferDependency.stderr
index 7fa900a889..cc852ee58c 100644
--- a/testsuite/tests/dependent/should_fail/InferDependency.stderr
+++ b/testsuite/tests/dependent/should_fail/InferDependency.stderr
@@ -1,8 +1,10 @@
 
-InferDependency.hs:6:1: error:
-    • Invalid declaration for ‘Proxy2’; you must explicitly
-      declare which variables are dependent on which others.
-      Inferred variable kinds:
+InferDependency.hs:6:13: error:
+    • Type constructor argument ‘k’ is used dependently.
+      Any dependent arguments must be obviously so, not inferred
+      by the type-checker.
+      Inferred argument kinds:
         k :: *
         a :: k
+      Suggestion: use ‘k’ in a kind to make the dependency clearer.
     • In the data type declaration for ‘Proxy2’
diff --git a/testsuite/tests/dependent/should_fail/T13601.stderr b/testsuite/tests/dependent/should_fail/T13601.stderr
index c1c9803e5a..bc2877c3e6 100644
--- a/testsuite/tests/dependent/should_fail/T13601.stderr
+++ b/testsuite/tests/dependent/should_fail/T13601.stderr
@@ -1,6 +1,5 @@
 
 T13601.hs:18:16: error:
-    • Expected kind ‘TYPE (Rep 'LiftedRep)’,
-        but ‘Logic a’ has kind ‘TYPE (Rep rep)’
+    • Expected a type, but ‘Logic a’ has kind ‘TYPE (Rep rep)’
     • In the first argument of ‘Boolean’, namely ‘(Logic a)’
       In the class declaration for ‘Eq’
diff --git a/testsuite/tests/dependent/should_fail/T13780c.stderr b/testsuite/tests/dependent/should_fail/T13780c.stderr
index f91d7a3236..065c700dfc 100644
--- a/testsuite/tests/dependent/should_fail/T13780c.stderr
+++ b/testsuite/tests/dependent/should_fail/T13780c.stderr
@@ -2,7 +2,7 @@
 [2 of 2] Compiling T13780c          ( T13780c.hs, T13780c.o )
 
 T13780c.hs:11:16: error:
-    • Expected kind ‘Sing _’, but ‘SFalse’ has kind ‘Sing 'False’
+    • Expected kind ‘Sing _1’, but ‘SFalse’ has kind ‘Sing 'False’
     • In the third argument of ‘ElimBool’, namely ‘SFalse’
       In the type family declaration for ‘ElimBool’
 
diff --git a/testsuite/tests/dependent/should_fail/T14066.hs b/testsuite/tests/dependent/should_fail/T14066.hs
new file mode 100644
index 0000000000..58396df591
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE KindSignatures #-}
+
+module T14066 where
+
+import Data.Kind ( Type )
+import Data.Type.Equality
+import Data.Proxy
+import GHC.Exts
+
+data SameKind :: k -> k -> Type
+
+f (x :: Proxy a) = let g :: forall k (b :: k). SameKind a b
+                       g = undefined
+                   in ()
diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr
new file mode 100644
index 0000000000..cd0142f5c1
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066.stderr
@@ -0,0 +1,11 @@
+
+T14066.hs:15:59: error:
+    • Expected kind ‘k0’, but ‘b’ has kind ‘k’
+    • In the second argument of ‘SameKind’, namely ‘b’
+      In the type signature: g :: forall k (b :: k). SameKind a b
+      In the expression:
+        let
+          g :: forall k (b :: k). SameKind a b
+          g = undefined
+        in ()
+    • Relevant bindings include x :: Proxy a (bound at T14066.hs:15:4)
diff --git a/testsuite/tests/dependent/should_fail/T14066c.hs b/testsuite/tests/dependent/should_fail/T14066c.hs
new file mode 100644
index 0000000000..b4597d2cec
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066c.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, TypeInType, UndecidableInstances #-}
+
+module T14066c where
+
+type family H a b where
+  H a b = H b a
+
+type X = H True Nothing  -- this should fail to kind-check.
+                         -- if it's accepted, then we've inferred polymorphic recursion for H
diff --git a/testsuite/tests/dependent/should_fail/T14066c.stderr b/testsuite/tests/dependent/should_fail/T14066c.stderr
new file mode 100644
index 0000000000..dc5ba30a4f
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066c.stderr
@@ -0,0 +1,6 @@
+
+T14066c.hs:8:17: error:
+    • Expected kind ‘Bool’, but ‘Nothing’ has kind ‘Maybe a0’
+    • In the second argument of ‘H’, namely ‘Nothing’
+      In the type ‘H True Nothing’
+      In the type declaration for ‘X’
diff --git a/testsuite/tests/dependent/should_fail/T14066d.hs b/testsuite/tests/dependent/should_fail/T14066d.hs
new file mode 100644
index 0000000000..ea47644688
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066d.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeInType #-}
+
+module T14066d where
+
+import Data.Proxy
+
+g :: (forall c b (a :: c). (Proxy a, Proxy c, b)) -> ()
+g _ = ()
+
+f :: forall b. b -> (Proxy Maybe, ())
+f x = (fstOf3 y :: Proxy Maybe, g y)
+  where
+    y :: (Proxy a, Proxy c, b)  -- this should NOT generalize over b
+                                -- meaning the call to g is ill-typed
+    y = (Proxy, Proxy, x)
+
+fstOf3 (x, _, _) = x
diff --git a/testsuite/tests/dependent/should_fail/T14066d.stderr b/testsuite/tests/dependent/should_fail/T14066d.stderr
new file mode 100644
index 0000000000..3a8b90edce
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066d.stderr
@@ -0,0 +1,21 @@
+
+T14066d.hs:11:35: error:
+    • Couldn't match type ‘b’ with ‘b1’
+      ‘b’ is a rigid type variable bound by
+        the type signature for:
+          f :: forall b. b -> (Proxy Maybe, ())
+        at T14066d.hs:10:1-37
+      ‘b1’ is a rigid type variable bound by
+        a type expected by the context:
+          forall c b1 (a :: c). (Proxy a, Proxy c, b1)
+        at T14066d.hs:11:33-35
+      Expected type: (Proxy a, Proxy c, b1)
+        Actual type: (Proxy a, Proxy c, b)
+    • In the first argument of ‘g’, namely ‘y’
+      In the expression: g y
+      In the expression: (fstOf3 y :: Proxy Maybe, g y)
+    • Relevant bindings include
+        y :: forall k1 k2 (a :: k2) (c :: k1). (Proxy a, Proxy c, b)
+          (bound at T14066d.hs:15:5)
+        x :: b (bound at T14066d.hs:11:3)
+        f :: b -> (Proxy Maybe, ()) (bound at T14066d.hs:11:1)
diff --git a/testsuite/tests/dependent/should_fail/T14066e.hs b/testsuite/tests/dependent/should_fail/T14066e.hs
new file mode 100644
index 0000000000..9b799e542c
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066e.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE MonoLocalBinds, TypeInType, ScopedTypeVariables #-}
+
+module T14066e where
+
+import Data.Proxy
+
+-- this should fail because the dependency between b and c can't be
+-- determined in the type signature
+h :: forall a. a -> ()
+h x = ()
+  where
+    j :: forall c b. Proxy a -> Proxy b -> Proxy c -> Proxy b
+    j _ (p1 :: Proxy b') (p2 :: Proxy c') = (p1 :: Proxy (b' :: c'))
diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr
new file mode 100644
index 0000000000..504ca5a80e
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066e.stderr
@@ -0,0 +1,11 @@
+
+T14066e.hs:13:59: error:
+    • Expected kind ‘c’, but ‘b'’ has kind ‘k0’
+    • In the first argument of ‘Proxy’, namely ‘(b' :: c')’
+      In an expression type signature: Proxy (b' :: c')
+      In the expression: (p1 :: Proxy (b' :: c'))
+    • Relevant bindings include
+        p2 :: Proxy c (bound at T14066e.hs:13:27)
+        p1 :: Proxy b (bound at T14066e.hs:13:10)
+        j :: Proxy a -> Proxy b -> Proxy c -> Proxy b
+          (bound at T14066e.hs:13:5)
diff --git a/testsuite/tests/dependent/should_fail/T14066f.hs b/testsuite/tests/dependent/should_fail/T14066f.hs
new file mode 100644
index 0000000000..ccb7ceac0e
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066f.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE TypeInType #-}
+
+module T14066f where
+
+import Data.Proxy
+
+-- a can't come before k.
+type P a k = Proxy (a :: k)
diff --git a/testsuite/tests/dependent/should_fail/T14066f.stderr b/testsuite/tests/dependent/should_fail/T14066f.stderr
new file mode 100644
index 0000000000..44c4ed293c
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066f.stderr
@@ -0,0 +1,6 @@
+
+T14066f.hs:8:1: error:
+    • These kind and type variables: a k
+      are out of dependency order. Perhaps try this ordering:
+        k (a :: k)
+    • In the type synonym declaration for ‘P’
diff --git a/testsuite/tests/dependent/should_fail/T14066g.hs b/testsuite/tests/dependent/should_fail/T14066g.hs
new file mode 100644
index 0000000000..df0e03b173
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066g.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeInType #-}
+
+module T14066g where
+
+import Data.Kind
+
+data SameKind :: k -> k -> Type
+
+data Q a (b :: a) (d :: SameKind c b)
diff --git a/testsuite/tests/dependent/should_fail/T14066g.stderr b/testsuite/tests/dependent/should_fail/T14066g.stderr
new file mode 100644
index 0000000000..22ca786343
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066g.stderr
@@ -0,0 +1,7 @@
+
+T14066g.hs:9:1: error:
+    • These kind and type variables: a (b :: a) (d :: SameKind c b)
+      are out of dependency order. Perhaps try this ordering:
+        a (c :: a) (b :: a) (d :: SameKind c b)
+      NB: Implicitly declared variables come before others.
+    • In the data type declaration for ‘Q’
diff --git a/testsuite/tests/dependent/should_fail/T14066h.hs b/testsuite/tests/dependent/should_fail/T14066h.hs
new file mode 100644
index 0000000000..7e7ecd31c9
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066h.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE ScopedTypeVariables, TypeInType, MonoLocalBinds #-}
+
+module T14066h where
+
+import Data.Proxy
+
+f :: forall b. b -> (Proxy Int, Proxy Maybe)
+f x = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+  where
+    y :: (Proxy a, b)  -- MonoLocalBinds means this won't generalize over the kind of a
+    y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_fail/T14066h.stderr b/testsuite/tests/dependent/should_fail/T14066h.stderr
new file mode 100644
index 0000000000..bfd33693b6
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14066h.stderr
@@ -0,0 +1,16 @@
+
+T14066h.hs:8:28: error:
+    • Couldn't match kind ‘* -> *’ with ‘*’
+      When matching types
+        a0 :: *
+        Maybe :: * -> *
+      Expected type: Proxy Maybe
+        Actual type: Proxy a0
+    • In the expression: fst y :: Proxy Maybe
+      In the expression: (fst y :: Proxy Int, fst y :: Proxy Maybe)
+      In an equation for ‘f’:
+          f x
+            = (fst y :: Proxy Int, fst y :: Proxy Maybe)
+            where
+                y :: (Proxy a, b)
+                y = (Proxy, x)
diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
index bbec037487..02b7737499 100644
--- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE RankNTypes, PolyKinds, TypeInType #-}
+-- NB: -fprint-explicit-runtime-reps enabled in all.T
 
 module TypeSkolEscape where
 
diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
index 88539858cf..e2ef266914 100644
--- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.stderr
@@ -1,7 +1,5 @@
 
-TypeSkolEscape.hs:8:1: error:
-    • Quantified type's kind mentions quantified type variable
-      (skolem escape)
-           type: forall (a1 :: TYPE v1). a1
-        of kind: TYPE v
-    • In the type synonym declaration for ‘Bad’
+TypeSkolEscape.hs:9:52: error:
+    • Expected kind ‘k0’, but ‘a’ has kind ‘TYPE v’
+    • In the type ‘forall (v :: RuntimeRep) (a :: TYPE v). a’
+      In the type declaration for ‘Bad’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index e28b2df5cd..7273445548 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -1,6 +1,6 @@
 test('DepFail1', normal, compile_fail, [''])
 test('RAE_T32a', normal, compile_fail, [''])
-test('TypeSkolEscape', normal, compile_fail, [''])
+test('TypeSkolEscape', normal, compile_fail, ['-fprint-explicit-runtime-reps'])
 test('BadTelescope', normal, compile_fail, [''])
 test('BadTelescope2', normal, compile_fail, [''])
 test('BadTelescope3', normal, compile_fail, [''])
@@ -10,7 +10,6 @@ test('BadTelescope4', normal, compile_fail, [''])
 test('RenamingStar', normal, compile_fail, [''])
 test('T11407', normal, compile_fail, [''])
 test('T11334b', normal, compile_fail, [''])
-test('InferDependency', normal, compile_fail, [''])
 test('KindLevelsB', normal, compile_fail, [''])
 test('T11473', normal, compile_fail, [''])
 test('T11471', normal, compile_fail, [''])
@@ -21,3 +20,11 @@ test('T13601', normal, compile_fail, [''])
 test('T13780a', normal, compile_fail, [''])
 test('T13780c', [extra_files(['T13780b.hs'])],
                 multimod_compile_fail, ['T13780c', ''])
+test('T14066', normal, compile_fail, [''])
+test('T14066c', normal, compile_fail, [''])
+test('T14066d', normal, compile_fail, [''])
+test('T14066e', normal, compile_fail, [''])
+test('T14066f', normal, compile_fail, [''])
+test('T14066g', normal, compile_fail, [''])
+test('T14066h', normal, compile_fail, [''])
+test('InferDependency', normal, compile_fail, [''])