Scoped kind variables (#16635)wip/scoped-kind-variables

7 files changed, 43 insertions, 2 deletions

diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index 755ed206f0..1b1079d275 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -563,8 +563,9 @@ rnHsTyKi env t@(HsKindSig _ ty k)
   = do { checkPolyKinds env t
        ; kind_sigs_ok <- xoptM LangExt.KindSignatures
        ; unless kind_sigs_ok (badKindSigErr (rtke_ctxt env) ty)
-       ; (ty', fvs1) <- rnLHsTyKi env ty
        ; (k', fvs2)  <- rnLHsTyKi (env { rtke_level = KindLevel }) k
+       ; (ty', fvs1) <- bindSigTyVarsFV (hsScopedKvs k') $
+                        rnLHsTyKi env ty
        ; return (HsKindSig noExt ty' k', fvs1 `plusFV` fvs2) }
 
 -- Unboxed tuples are allowed to have poly-typed arguments.  These
@@ -646,6 +647,10 @@ rnHsTyKi env (HsWildCardTy _)
   = do { checkAnonWildCard env
        ; return (HsWildCardTy noExt, emptyFVs) }
 
+hsScopedKvs :: LHsType GhcRn -> [Name]
+hsScopedKvs (L _ (HsForAllTy { hst_bndrs = tvs })) = hsLTyVarNames tvs
+hsScopedKvs _ = []
+
 --------------
 rnTyVar :: RnTyKiEnv -> RdrName -> RnM Name
 rnTyVar env rdr_name
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index c58a585356..21b9ee4bcb 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -587,7 +587,8 @@ tc_infer_hs_type mode (HsKindSig _ ty sig)
                  -- things like instantiate its foralls, so it needs
                  -- to be fully determined (#14904)
        ; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
-       ; ty' <- tc_lhs_type mode ty sig'
+       ; ty' <- tcExtendTyVarEnv (fst (tcSplitForAllTys sig')) $
+                tc_lhs_type mode ty sig'
        ; return (ty', sig') }
 
 -- HsSpliced is an annotation produced by 'RnSplice.rnSpliceType' to communicate
diff --git a/testsuite/tests/rename/should_fail/T16635a.hs b/testsuite/tests/rename/should_fail/T16635a.hs
new file mode 100644
index 0000000000..80fdb409e3
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T16635a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE NoScopedTypeVariables, ExplicitForAll #-}
+{-# LANGUAGE DataKinds, PolyKinds, TypeApplications #-}
+
+module T16635a where
+
+data Unit = U
+data P a = MkP
+
+-- ScopedTypeVariables are disabled.
+-- Fails because because @a is not in scope.
+type F = (Just @a :: forall a. a -> Maybe a) U
diff --git a/testsuite/tests/rename/should_fail/T16635a.stderr b/testsuite/tests/rename/should_fail/T16635a.stderr
new file mode 100644
index 0000000000..798cce837a
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T16635a.stderr
@@ -0,0 +1,2 @@
+
+T16635a.hs:11:17: error: Not in scope: type variable ‘a’
diff --git a/testsuite/tests/rename/should_fail/T16635b.hs b/testsuite/tests/rename/should_fail/T16635b.hs
new file mode 100644
index 0000000000..9be9d686da
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T16635b.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DataKinds, PolyKinds, TypeApplications #-}
+
+module T16635b where
+
+data Unit = U
+data P a = MkP
+
+-- OK.
+f =      (Just @a :: forall a. a -> Maybe a) U
+
+-- Fails because we cannot generalize to (/\a. Just @a)
+--            but NOT because @a is not in scope.
+type F = (Just @a :: forall a. a -> Maybe a) U
diff --git a/testsuite/tests/rename/should_fail/T16635b.stderr b/testsuite/tests/rename/should_fail/T16635b.stderr
new file mode 100644
index 0000000000..a9aa272c99
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/T16635b.stderr
@@ -0,0 +1,6 @@
+
+T16635b.hs:14:11: error:
+    • Expected kind ‘forall a. a -> Maybe a’,
+        but ‘Just @a’ has kind ‘a -> Maybe a’
+    • In the type ‘(Just @a :: forall a. a -> Maybe a) U’
+      In the type declaration for ‘F’
diff --git a/testsuite/tests/rename/should_fail/all.T b/testsuite/tests/rename/should_fail/all.T
index 52a4f45a04..ccdbfd0355 100644
--- a/testsuite/tests/rename/should_fail/all.T
+++ b/testsuite/tests/rename/should_fail/all.T
@@ -149,3 +149,5 @@ test('ExplicitForAllRules2', normal, compile_fail, [''])
 test('T15957_Fail', normal, compile_fail, ['-Werror -Wall -Wno-missing-signatures'])
 test('T16385', normal, compile_fail, [''])
 test('T16504', normal, compile_fail, [''])
+test('T16635a', normal, compile_fail, [''])
+test('T16635b', normal, compile_fail, [''])