Disallow constraints in KindSigCtxtwip/T18714-T18715

This patch cleans up how `GHC.Tc.Validity` classifies `UserTypeCtxt`s
that can only refer to kind-level positions, which is important for
rejecting certain classes of programs. In particular, this patch:

* Introduces a new `TypeOrKindCtxt` data type and
  `typeOrKindCtxt :: UserTypeCtxt -> TypeOrKindCtxt` function, which
  determines whether a `UserTypeCtxt` can refer to type-level
  contexts, kind-level contexts, or both.
* Defines the existing `allConstraintsAllowed` and `vdqAllowed`
  functions in terms of `typeOrKindCtxt`, which avoids code
  duplication and ensures that they stay in sync in the future.

The net effect of this patch is that it fixes #18714, in which it was
discovered that `allConstraintsAllowed` incorrectly returned `True`
for `KindSigCtxt`. Because `typeOrKindCtxt` now correctly classifies
`KindSigCtxt` as a kind-level context, this bug no longer occurs.

4 files changed, 94 insertions, 40 deletions

diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs
index 946d1bf9e9..f89ec4d966 100644
--- a/compiler/GHC/Tc/Validity.hs
+++ b/compiler/GHC/Tc/Validity.hs
@@ -470,18 +470,81 @@ forAllAllowed ArbitraryRank             = True
 forAllAllowed (LimitedRank forall_ok _) = forall_ok
 forAllAllowed _                         = False
 
+-- | Indicates whether a 'UserTypeCtxt' represents type-level contexts,
+-- kind-level contexts, or both.
+data TypeOrKindCtxt
+  = OnlyTypeCtxt
+    -- ^ A 'UserTypeCtxt' that only represents type-level positions.
+  | OnlyKindCtxt
+    -- ^ A 'UserTypeCtxt' that only represents kind-level positions.
+  | BothTypeAndKindCtxt
+    -- ^ A 'UserTypeCtxt' that can represent both type- and kind-level positions.
+  deriving Eq
+
+instance Outputable TypeOrKindCtxt where
+  ppr ctxt = text $ case ctxt of
+    OnlyTypeCtxt        -> "OnlyTypeCtxt"
+    OnlyKindCtxt        -> "OnlyKindCtxt"
+    BothTypeAndKindCtxt -> "BothTypeAndKindCtxt"
+
+-- | Determine whether a 'UserTypeCtxt' can represent type-level contexts,
+-- kind-level contexts, or both.
+typeOrKindCtxt :: UserTypeCtxt -> TypeOrKindCtxt
+typeOrKindCtxt (FunSigCtxt {})      = OnlyTypeCtxt
+typeOrKindCtxt (InfSigCtxt {})      = OnlyTypeCtxt
+typeOrKindCtxt (ExprSigCtxt {})     = OnlyTypeCtxt
+typeOrKindCtxt (TypeAppCtxt {})     = OnlyTypeCtxt
+typeOrKindCtxt (PatSynCtxt {})      = OnlyTypeCtxt
+typeOrKindCtxt (PatSigCtxt {})      = OnlyTypeCtxt
+typeOrKindCtxt (RuleSigCtxt {})     = OnlyTypeCtxt
+typeOrKindCtxt (ForSigCtxt {})      = OnlyTypeCtxt
+typeOrKindCtxt (DefaultDeclCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (InstDeclCtxt {})    = OnlyTypeCtxt
+typeOrKindCtxt (SpecInstCtxt {})    = OnlyTypeCtxt
+typeOrKindCtxt (GenSigCtxt {})      = OnlyTypeCtxt
+typeOrKindCtxt (ClassSCCtxt {})     = OnlyTypeCtxt
+typeOrKindCtxt (SigmaCtxt {})       = OnlyTypeCtxt
+typeOrKindCtxt (DataTyCtxt {})      = OnlyTypeCtxt
+typeOrKindCtxt (DerivClauseCtxt {}) = OnlyTypeCtxt
+typeOrKindCtxt (ConArgCtxt {})      = OnlyTypeCtxt
+  -- Although data constructors can be promoted with DataKinds, we always
+  -- validity-check them as though they are the types of terms. We may need
+  -- to revisit this decision if we ever allow visible dependent quantification
+  -- in the types of data constructors.
+
+typeOrKindCtxt (KindSigCtxt {})           = OnlyKindCtxt
+typeOrKindCtxt (StandaloneKindSigCtxt {}) = OnlyKindCtxt
+typeOrKindCtxt (TyVarBndrKindCtxt {})     = OnlyKindCtxt
+typeOrKindCtxt (DataKindCtxt {})          = OnlyKindCtxt
+typeOrKindCtxt (TySynKindCtxt {})         = OnlyKindCtxt
+typeOrKindCtxt (TyFamResKindCtxt {})      = OnlyKindCtxt
+
+typeOrKindCtxt (TySynCtxt {}) = BothTypeAndKindCtxt
+  -- Type synonyms can have types and kinds on their RHSs
+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".)
+-- If the 'UserTypeCtxt' can refer to both types and kinds, this function
+-- conservatively returns 'True'.
+--
+-- An example of something that is unambiguously the kind of a type is the
+-- @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
--- We don't allow arbitrary constraints in kinds
-allConstraintsAllowed (TyVarBndrKindCtxt {}) = False
-allConstraintsAllowed (DataKindCtxt {})      = False
-allConstraintsAllowed (TySynKindCtxt {})     = False
-allConstraintsAllowed (TyFamResKindCtxt {})  = False
-allConstraintsAllowed (StandaloneKindSigCtxt {}) = False
-allConstraintsAllowed _ = True
+allConstraintsAllowed ctxt = case typeOrKindCtxt ctxt of
+  OnlyTypeCtxt        -> True
+  OnlyKindCtxt        -> False
+  BothTypeAndKindCtxt -> True
 
 -- | Returns 'True' if the supplied 'UserTypeCtxt' is unambiguously not the
 -- context for the type of a term, where visible, dependent quantification is
--- currently disallowed.
+-- currently disallowed. If the 'UserTypeCtxt' can refer to both types and
+-- kinds, this function conservatively returns 'True'.
 --
 -- An example of something that is unambiguously the type of a term is the
 -- @forall a -> a -> a@ in @foo :: forall a -> a -> a@. On the other hand, the
@@ -494,38 +557,10 @@ allConstraintsAllowed _ = True
 -- @testsuite/tests/dependent/should_fail/T16326_Fail*.hs@ (for places where
 -- VDQ is disallowed).
 vdqAllowed :: UserTypeCtxt -> Bool
--- Currently allowed in the kinds of types...
-vdqAllowed (KindSigCtxt {}) = True
-vdqAllowed (StandaloneKindSigCtxt {}) = True
-vdqAllowed (TySynCtxt {}) = True
-vdqAllowed (GhciCtxt {}) = True
-vdqAllowed (TyVarBndrKindCtxt {}) = True
-vdqAllowed (DataKindCtxt {}) = True
-vdqAllowed (TySynKindCtxt {}) = True
-vdqAllowed (TyFamResKindCtxt {}) = True
--- ...but not in the types of terms.
-vdqAllowed (ConArgCtxt {}) = False
-  -- We could envision allowing VDQ in data constructor types so long as the
-  -- constructor is only ever used at the type level, but for now, GHC adopts
-  -- the stance that VDQ is never allowed in data constructor types.
-vdqAllowed (FunSigCtxt {}) = False
-vdqAllowed (InfSigCtxt {}) = False
-vdqAllowed (ExprSigCtxt {}) = False
-vdqAllowed (TypeAppCtxt {}) = False
-vdqAllowed (PatSynCtxt {}) = False
-vdqAllowed (PatSigCtxt {}) = False
-vdqAllowed (RuleSigCtxt {}) = False
-vdqAllowed (ForSigCtxt {}) = False
-vdqAllowed (DefaultDeclCtxt {}) = False
--- We count class constraints as "types of terms". All of the cases below deal
--- with class constraints.
-vdqAllowed (InstDeclCtxt {}) = False
-vdqAllowed (SpecInstCtxt {}) = False
-vdqAllowed (GenSigCtxt {}) = False
-vdqAllowed (ClassSCCtxt {}) = False
-vdqAllowed (SigmaCtxt {}) = False
-vdqAllowed (DataTyCtxt {}) = False
-vdqAllowed (DerivClauseCtxt {}) = False
+vdqAllowed ctxt = case typeOrKindCtxt ctxt of
+  OnlyTypeCtxt        -> False
+  OnlyKindCtxt        -> True
+  BothTypeAndKindCtxt -> True
 
 {-
 Note [Correctness and performance of type synonym validity checking]
diff --git a/testsuite/tests/typecheck/should_fail/T18714.hs b/testsuite/tests/typecheck/should_fail/T18714.hs
new file mode 100644
index 0000000000..9a111a2cc2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18714.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+module T18714 where
+
+import GHC.Exts
+
+type Id a = a
+
+type F = Id (Any :: forall a. Show a => a -> a)
diff --git a/testsuite/tests/typecheck/should_fail/T18714.stderr b/testsuite/tests/typecheck/should_fail/T18714.stderr
new file mode 100644
index 0000000000..e038e603e1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18714.stderr
@@ -0,0 +1,7 @@
+
+T18714.hs:11:14: error:
+    • Illegal constraint in a kind: forall a. Show a => a -> a
+    • In the first argument of ‘Id’, namely
+        ‘(Any :: forall a. Show a => a -> a)’
+      In the type ‘Id (Any :: forall a. Show a => a -> a)’
+      In the type declaration for ‘F’
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 49a3cb8cec..6b10777f12 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -579,3 +579,4 @@ test('T18357a', normal, compile_fail, [''])
 test('T18357b', normal, compile_fail, [''])
 test('T18455', normal, compile_fail, [''])
 test('T18534', normal, compile_fail, [''])
+test('T18714', normal, compile_fail, [''])