Reject linearity in kinds in checkValidType (#18780)

Patch taken from https://gitlab.haskell.org/ghc/ghc/-/issues/18624#note_300673

8 files changed, 58 insertions, 16 deletions

diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 9c778a1b4b..d23c09fd09 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -1041,11 +1041,8 @@ tc_hs_type _ ty@(HsSpliceTy {}) _exp_kind
   = failWithTc (text "Unexpected type splice:" <+> ppr ty)
 
 ---------- Functions and applications
-tc_hs_type mode ty@(HsFunTy _ mult ty1 ty2) exp_kind
-  | mode_tyki mode == KindLevel && not (isUnrestricted mult)
-    = failWithTc (text "Linear arrows disallowed in kinds:" <+> ppr ty)
-  | otherwise
-    = tc_fun_type mode mult ty1 ty2 exp_kind
+tc_hs_type mode (HsFunTy _ mult ty1 ty2) exp_kind
+  = tc_fun_type mode mult ty1 ty2 exp_kind
 
 tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
   | op `hasKey` funTyConKey
diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index e00b39b20e..540480147c 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -525,9 +525,7 @@ typeOrKindCtxt (GhciCtxt {})  = BothTypeAndKindCtxt
   -- GHCi's :kind command accepts both types and kinds
 
 -- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
--- context for a kind of a type, where the arbitrary use of constraints is
--- currently disallowed.
--- (See @Note [Constraints in kinds]@ in "GHC.Core.TyCo.Rep".)
+-- context for a kind of a type.
 -- If the 'UserTypeCtxt' can refer to both types and kinds, this function
 -- conservatively returns 'True'.
 --
@@ -535,13 +533,26 @@ typeOrKindCtxt (GhciCtxt {})  = BothTypeAndKindCtxt
 -- @Show a => a -> a@ in @type Foo :: Show a => a -> a@. On the other hand, the
 -- same type in @foo :: Show a => a -> a@ is unambiguously the type of a term,
 -- not the kind of a type, so it is permitted.
-allConstraintsAllowed :: UserTypeCtxt -> Bool
-allConstraintsAllowed ctxt = case typeOrKindCtxt ctxt of
+typeLevelUserTypeCtxt :: UserTypeCtxt -> Bool
+typeLevelUserTypeCtxt ctxt = case typeOrKindCtxt ctxt of
   OnlyTypeCtxt        -> True
   OnlyKindCtxt        -> False
   BothTypeAndKindCtxt -> True
 
 -- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
+-- context for a kind of a type, where the arbitrary use of constraints is
+-- currently disallowed.
+-- (See @Note [Constraints in kinds]@ in "GHC.Core.TyCo.Rep".)
+allConstraintsAllowed :: UserTypeCtxt -> Bool
+allConstraintsAllowed = typeLevelUserTypeCtxt
+
+-- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
+-- context for a kind of a type, where all function arrows currently
+-- must be unrestricted.
+linearityAllowed :: UserTypeCtxt -> Bool
+linearityAllowed = typeLevelUserTypeCtxt
+
+-- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
 -- context for the type of a term, where visible, dependent quantification is
 -- currently disallowed. If the 'UserTypeCtxt' can refer to both types and
 -- kinds, this function conservatively returns 'True'.
@@ -744,8 +755,12 @@ check_type ve@(ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
     (theta, tau)  = tcSplitPhiTy phi
     (env', tvbs') = tidyTyCoVarBinders env tvbs
 
-check_type (ve@ValidityEnv{ve_rank = rank}) (FunTy _ _ arg_ty res_ty)
-  = do  { check_type (ve{ve_rank = arg_rank}) arg_ty
+check_type (ve@ValidityEnv{ ve_tidy_env = env, ve_ctxt = ctxt
+                          , ve_rank = rank })
+           ty@(FunTy _ mult arg_ty res_ty)
+  = do  { failIfTcM (not (linearityAllowed ctxt) && not (isManyDataConTy mult))
+                     (linearFunKindErr env ty)
+        ; check_type (ve{ve_rank = arg_rank}) arg_ty
         ; check_type (ve{ve_rank = res_rank}) res_ty }
   where
     (arg_rank, res_rank) = funArgResRank rank
@@ -993,6 +1008,11 @@ illegalVDQTyErr env ty =
        2 (ppr_tidy env ty)
   , text "(GHC does not yet support this)" ] )
 
+-- | Reject uses of linear function arrows in kinds.
+linearFunKindErr :: TidyEnv -> Type -> (TidyEnv, SDoc)
+linearFunKindErr env ty =
+  (env, text "Illegal linear function in a kind:" <+> ppr_tidy env ty)
+
 {-
 Note [Liberal type synonyms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/testsuite/tests/linear/should_fail/LinearKind.stderr b/testsuite/tests/linear/should_fail/LinearKind.stderr
index 9ba3f744cf..c70e90a1b5 100644
--- a/testsuite/tests/linear/should_fail/LinearKind.stderr
+++ b/testsuite/tests/linear/should_fail/LinearKind.stderr
@@ -1,5 +1,4 @@
 
-LinearKind.hs:4:11: error:
-    • Linear arrows disallowed in kinds: * %1 -> *
-    • In the kind ‘* %1 -> *’
-      In the data type declaration for ‘A’
+LinearKind.hs:4:1: error:
+    • Illegal linear function in a kind: * %1 -> *
+    • In the data type declaration for ‘A’
diff --git a/testsuite/tests/linear/should_fail/LinearKind2.hs b/testsuite/tests/linear/should_fail/LinearKind2.hs
new file mode 100644
index 0000000000..402b67efc4
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearKind2.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE LinearTypes, KindSignatures, DataKinds #-}
+module LinearKind2 where -- T18780
+
+import GHC.Exts
+import GHC.Types
+
+data Two :: FUN One Type Type
diff --git a/testsuite/tests/linear/should_fail/LinearKind2.stderr b/testsuite/tests/linear/should_fail/LinearKind2.stderr
new file mode 100644
index 0000000000..0bdf1b0d19
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearKind2.stderr
@@ -0,0 +1,4 @@
+
+LinearKind2.hs:7:1: error:
+    • Illegal linear function in a kind: * %1 -> *
+    • In the data type declaration for ‘Two’
diff --git a/testsuite/tests/linear/should_fail/LinearKind3.hs b/testsuite/tests/linear/should_fail/LinearKind3.hs
new file mode 100644
index 0000000000..7d85cb6e96
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearKind3.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE LinearTypes, KindSignatures, DataKinds #-}
+module LinearKind3 where -- T18780
+
+import GHC.Exts
+import GHC.Types
+
+type K = Type %1 -> Type
+data T :: K
diff --git a/testsuite/tests/linear/should_fail/LinearKind3.stderr b/testsuite/tests/linear/should_fail/LinearKind3.stderr
new file mode 100644
index 0000000000..8e16996baf
--- /dev/null
+++ b/testsuite/tests/linear/should_fail/LinearKind3.stderr
@@ -0,0 +1,5 @@
+
+LinearKind3.hs:8:1: error:
+    • Illegal linear function in a kind: * %1 -> *
+    • In the expansion of type synonym ‘K’
+      In the data type declaration for ‘T’
diff --git a/testsuite/tests/linear/should_fail/all.T b/testsuite/tests/linear/should_fail/all.T
index bcba344268..272e9e2a35 100644
--- a/testsuite/tests/linear/should_fail/all.T
+++ b/testsuite/tests/linear/should_fail/all.T
@@ -20,6 +20,8 @@ test('LinearPatSyn', normal, compile_fail, [''])
 test('LinearGADTNewtype', normal, compile_fail, [''])
 test('LinearPartialSig', normal, compile_fail, [''])
 test('LinearKind', normal, compile_fail, [''])
+test('LinearKind2', normal, compile_fail, [''])
+test('LinearKind3', normal, compile_fail, [''])
 test('LinearVar', normal, compile_fail, ['-XLinearTypes'])
 test('LinearErrOrigin', normal, compile_fail, ['-XLinearTypes'])
 test('LinearPolyType', normal, compile_fail, [''])  # not supported yet (#390)