testsuite: Do not require CUSKs

Numerous tests make use of CUSKs (complete user-supplied kinds),
a legacy feature scheduled for deprecation. In order to proceed
with the said deprecation, the tests have been updated to use SAKS
instead (standalone kind signatures).

This also allows us to remove the Haskell2010 language pragmas that
were added in 115cd3c8 to work around the lack of CUSKs in GHC2021.

testsuite/tests/dependent/should_compile/Dep2.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE PolyKinds, GADTs #-}
 
 module Dep2 where
 
-data G (a :: k) where
+import Data.Kind (Type)
+
+type G :: k -> Type
+data G a where
   G1 :: G Int
   G2 :: G Maybe

testsuite/tests/dependent/should_compile/DkNameRes.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
 
 module DkNameRes where
@@ -6,5 +5,6 @@ module DkNameRes where
 import Data.Proxy
 import Data.Kind
 
-type family IfK (e :: Proxy (j :: Bool)) :: Type where
+type IfK :: Proxy (j :: Bool) -> Type
+type family IfK e where
    IfK (_ :: Proxy True) = ()

testsuite/tests/dependent/should_compile/KindEqualities2.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE DataKinds, GADTs, PolyKinds, TypeFamilies, ExplicitForAll,
              TemplateHaskell, UndecidableInstances, ScopedTypeVariables #-}
 
@@ -16,7 +15,8 @@ data Ty :: Kind -> Type where
   TApp :: Ty (Arr k1 k2) -> Ty k1 -> Ty k2
 
 
-data TyRep (k :: Kind) (t :: Ty k) where
+type TyRep :: forall (k :: Kind) -> Ty k -> Type
+data TyRep k t where
   TyInt :: TyRep Star TInt
   TyBool :: TyRep Star TBool
   TyMaybe :: TyRep (Arr Star Star) TMaybe

testsuite/tests/dependent/should_compile/RaeBlogPost.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE DataKinds, PolyKinds, GADTs, TypeOperators, TypeFamilies #-}
 {-# OPTIONS_GHC -fwarn-unticked-promoted-constructors #-}
 
@@ -23,7 +22,8 @@ data E :: D c -> Type
 -- note that E :: forall (a :: A) (b :: B a) (c :: C b). D c -> Type
 
 -- a kind-indexed GADT
-data TypeRep (a :: k) where
+type TypeRep :: k -> Type
+data TypeRep a where
   TInt   :: TypeRep Int
   TMaybe :: TypeRep Maybe
   TApp   :: TypeRep a -> TypeRep b -> TypeRep (a b)
@@ -37,13 +37,15 @@ type family a + b where
   'Zero     + b = b
   ('Succ a) + b = 'Succ (a + b)
 
-data Vec :: Type -> Nat -> Type where
+type Vec :: Type -> Nat -> Type
+data Vec a n where
   Nil  :: Vec a 'Zero
   (:>) :: a -> Vec a n -> Vec a ('Succ n)
 infixr 5 :>
 
 -- promoted GADT, and using + as a "kind family":
-type family (x :: Vec a n) ++ (y :: Vec a m) :: Vec a (n + m) where
+type (++) :: Vec a n -> Vec a m -> Vec a (n + m)
+type family x ++ y where
   'Nil      ++ y = y
   (h ':> t) ++ y = h ':> (t ++ y)
 

testsuite/tests/dependent/should_compile/RaeJobTalk.hs

-{-# LANGUAGE Haskell2010 #-}
 {- Copyright (c) 2016 Richard Eisenberg
  -}
 
@@ -27,7 +26,8 @@ import qualified GHC.Exts as Exts
 -- Utilities
 
 -- Heterogeneous propositional equality
-data (a :: k1) :~~: (b :: k2) where
+type (:~~:) :: k1 -> k2 -> Type
+data a :~~: b where
   HRefl :: a :~~: a
 
 -- Type-level inequality
@@ -76,7 +76,8 @@ Nil %:++ x = x
 -- Type-indexed type representations
 -- Based on "A reflection on types"
 
-data TyCon (a :: k) where
+type TyCon :: k -> Type
+data TyCon a where
   Int :: TyCon Int
   Bool :: TyCon Bool
   Char :: TyCon Char
@@ -110,7 +111,8 @@ type family Primitive (a :: k) :: Constraint where
   Primitive (_ _) = ('False ~ 'True)
   Primitive _     = (() :: Constraint)
 
-data TypeRep (a :: k) where
+type TypeRep :: k -> Type
+data TypeRep a where
   TyCon :: forall k (a :: k). (Primitive a, Typeable k) => TyCon a -> TypeRep a
   TyApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
 

testsuite/tests/dependent/should_compile/T11711.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
@@ -11,19 +10,22 @@
 
 module T11711 where
 
-import Data.Kind (Type)
+import Data.Kind (Type, Constraint)
 
-data (:~~:) (a :: k1) (b :: k2) where
+type (:~~:) :: k1 -> k2 -> Type
+data (:~~:) a b where
     HRefl :: a :~~: a
 
-data TypeRep (a :: k) where
+type TypeRep :: k -> Type
+data TypeRep a where
     TrTyCon :: String -> TypeRep k -> TypeRep (a :: k)
     TrApp   :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
                TypeRep (a :: k1 -> k2)
             -> TypeRep (b :: k1)
             -> TypeRep (a b)
 
-class Typeable (a :: k) where
+type Typeable :: k -> Constraint
+class Typeable a where
     typeRep :: TypeRep a
 
 data SomeTypeRep where

testsuite/tests/dependent/should_compile/T12442.hs

-{-# LANGUAGE Haskell2010 #-}
 -- Based on https://github.com/idris-lang/Idris-dev/blob/v0.9.10/libs/effects/Effects.idr
 
 {-# LANGUAGE DataKinds, PolyKinds, ScopedTypeVariables, TypeOperators,
@@ -34,9 +33,9 @@ data EffElem :: (Type ~> Type ~> Type ~> Type) -> Type -> [EFFECT] -> Type where
 data instance Sing (elem :: EffElem x a xs) where
   SHere :: Sing Here
 
-type family UpdateResTy (b :: Type) (t :: Type)
-                        (xs :: [EFFECT]) (elem :: EffElem e a xs)
-                        (thing :: e @@ a @@ b @@ t) :: [EFFECT] where
+type UpdateResTy :: forall e a. forall b t xs ->
+                    EffElem e a xs -> e @@ a @@ b @@ t -> [EFFECT]
+type family UpdateResTy b t xs elem thing where
   UpdateResTy b _ (MkEff a e ': xs) Here n = MkEff b e ': xs
 
 data EffM :: (Type ~> Type) -> [EFFECT] -> [EFFECT] -> Type -> Type

testsuite/tests/dependent/should_compile/T14066a.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, ExplicitForAll, GADTs,
              UndecidableInstances, RankNTypes, ScopedTypeVariables #-}
 
@@ -32,7 +31,8 @@ type family G x a where
 
 -- this last example just checks that GADT pattern-matching on kinds still works.
 -- nothing new here.
-data T (a :: k) where
+type T :: k -> Type
+data T a where
   MkT :: T (a :: Type -> Type)
 
 data S (a :: Type -> Type) where
@@ -54,9 +54,12 @@ type P k a = Proxy (a :: k)
 -- Naively, we don't know about c's kind early enough.
 
 data SameKind :: forall k. k -> k -> Type
-type family IfK (e :: Proxy (j :: Bool)) (f :: m) (g :: n) :: If j m n where
+
+type IfK :: Proxy (j :: Bool) -> m -> n -> If j m n
+type family IfK e f g where
    IfK (_ :: Proxy True)  f _ = f
    IfK (_ :: Proxy False) _ g = g
+
 x :: forall c. (forall a b (d :: a). SameKind (IfK c b d) d) -> (Proxy (c :: Proxy True))
 x _ = Proxy
 

testsuite/tests/dependent/should_compile/T14066a.stderr

 
-T14066a.hs:14:3: warning: [GHC-28129] [-Winaccessible-code (in -Wdefault)]
+T14066a.hs:13:3: warning: [GHC-28129] [-Winaccessible-code (in -Wdefault)]
     Type family instance equation is overlapped:
       forall {c} {x :: c} {d} {y :: d}.
-        Bar x y = Bool -- Defined at T14066a.hs:14:3
+        Bar x y = Bool -- Defined at T14066a.hs:13:3

testsuite/tests/dependent/should_compile/T14556.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# Language UndecidableInstances, DataKinds, TypeOperators, PolyKinds,
              TypeFamilies, GADTs, LambdaCase, ScopedTypeVariables #-}
 
@@ -10,8 +9,8 @@ import Data.Proxy
 data Fn a b where
   IdSym :: Fn Type Type
 
-type family
-  (@@) (f::Fn k k') (a::k)::k' where
+type (@@) :: Fn k k' -> k -> k'
+type family f @@ a where
   IdSym @@ a = a
 
 data KIND = X | FNARR KIND KIND
@@ -20,19 +19,20 @@ data TY :: KIND -> Type where
   ID    :: TY (FNARR X X)
   FNAPP :: TY (FNARR k k') -> TY k -> TY k'
 
-data TyRep (kind::KIND) :: TY kind -> Type where
+type TyRep :: forall (kind::KIND) -> TY kind -> Type
+data TyRep k t where
   TID    :: TyRep (FNARR X X)  ID
   TFnApp :: TyRep (FNARR k k') f
          -> TyRep k            a
          -> TyRep k'           (FNAPP f a)
 
-type family
-  IK (kind::KIND) :: Type where
+type IK :: KIND -> Type
+type family IK k where
   IK X            = Type
   IK (FNARR k k') = Fn (IK k) (IK k')
 
-type family
-  IT (ty::TY kind) :: IK kind where
+type IT :: TY kind -> IK kind
+type family IT t where
   IT ID          = IdSym
   IT (FNAPP f x) = IT f @@ IT x
 

testsuite/tests/dependent/should_compile/T14749.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies, PolyKinds, TypeFamilyDependencies #-}
 
 module T14749 where
@@ -15,11 +14,13 @@ type family IK (k :: KIND) = (res :: Type) where
   IK STAR   = Type
   IK (a:>b) = IK a -> IK b
 
-type family I (t :: Ty k) = (res :: IK k)  where
+type I :: Ty k -> IK k
+type family I t = res where
   I TMaybe     = Maybe
   I (TApp f a) = (I f) (I a)
 
-data TyRep (k :: KIND) (t :: Ty k) where
+type TyRep :: forall (k :: KIND) -> Ty k -> Type
+data TyRep k t where
   TyMaybe :: TyRep (STAR:>STAR) TMaybe
   TyApp   :: TyRep (a:>b) f -> TyRep a x -> TyRep b (TApp f x)
 

testsuite/tests/dependent/should_compile/T16326_Compile1.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
@@ -21,14 +20,9 @@ type DComp a
            (x :: a) =
   f (g x)
 
--- Ensure that ElimList has a CUSK, beuas it is
--- is used polymorphically its RHS (c.f. #16344)
-type family ElimList (a :: Type)
-                     (p :: [a] -> Type)
-                     (s :: [a])
-                     (pNil :: p '[])
-                     (pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs))
-                  :: p s where
+type ElimList :: forall (a :: Type) (p :: [a] -> Type) (s :: [a]) ->
+  p '[] -> (forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs)) -> p s
+type family ElimList a p s pNil pCons where
   forall a p pNil (pCons :: forall (x :: a) (xs :: [a]) -> p xs -> p (x:xs)).
     ElimList a p '[] pNil pCons =
       pNil

testsuite/tests/dependent/should_compile/TypeLevelVec.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE DataKinds, PolyKinds, UnicodeSyntax, GADTs, NoImplicitPrelude,
              TypeOperators, TypeFamilies #-}
 {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
@@ -21,7 +20,8 @@ data Vec ∷ ℕ → Type → Type where
   (:>) ∷ a → Vec n a → Vec (S n) a
 infixr 8 :>
 
-type family (x ∷ Vec n a) ++ (y ∷ Vec m a) ∷ Vec (n + m) a where
+type (++) ∷ Vec n a → Vec m a → Vec (n + m) a
+type family x ++ y where
   Nil       ++ y = y
   (x :> xs) ++ y = x :> (xs ++ y)
 infixl 5 ++

testsuite/tests/dependent/should_compile/dynamic-paper.hs

-{-# LANGUAGE Haskell2010 #-}
 {- This is the code extracted from "A reflection on types", by Simon PJ,
 Stephanie Weirich, Richard Eisenberg, and Dimitrios Vytiniotis, 2016. -}
 
@@ -186,7 +185,8 @@ dynFst (Dyn (rpab :: TypeRep pab) (x :: pab))
 eqT :: forall k1 k2 (a :: k1) (b :: k2).
        TypeRep a -> TypeRep b -> Maybe (a :~: b)
 
-data (a :: k1) :~: (b :: k2) where
+type (:~:) :: k1 -> k2 -> Type
+data a :~: b where
   Refl :: forall k (a :: k). a :~: a
 
 castDance :: (Typeable a, Typeable b)  => a -> Maybe b
@@ -236,7 +236,8 @@ data OrderingT a b where
   EQT  :: OrderingT t t
   GTT  :: OrderingT a b
 
-data TypeRep (a :: k) where
+type TypeRep :: k -> Type
+data TypeRep a where
   TrApp    :: TypeRep a -> TypeRep b -> TypeRep (a b)
   TrTyCon  :: TyCon -> TypeRep k -> TypeRep (a :: k)
 

testsuite/tests/dependent/should_compile/mkGADTVars.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE GADTs, PolyKinds, RankNTypes #-}
 
 module GADTVars where
@@ -6,5 +5,6 @@ module GADTVars where
 import Data.Kind
 import Data.Proxy
 
-data T (k1 :: Type) (k2 :: Type) (a :: k2) (b :: k2) where
+type T :: Type -> forall (k2 :: Type) -> k2 -> k2 -> Type
+data T k1 k2 a b where
   MkT :: T x1 Type (Proxy (y :: x1), z) z

testsuite/tests/dependent/should_fail/T13601.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE TypeFamilies, DataKinds, PolyKinds #-}
 
 import GHC.Exts
@@ -16,25 +15,32 @@ type family
   -- Rep PtrRepUnlifted = IntRep
   -- Rep PtrRepLifted   = PtrRepLifted
 
+type Eq :: TYPE rep -> Constraint
 class Boolean (Logic a) => Eq (a :: TYPE rep) where
   type Logic (a :: TYPE rep) :: TYPE (Rep rep)
   (==) :: a -> a -> Logic a
 
+type POrd :: TYPE rep -> Constraint
 class Eq a => POrd (a :: TYPE rep) where
   inf :: a -> a -> a
 
+type MinBound :: TYPE rep -> Constraint
 class POrd a => MinBound (a :: TYPE rep) where
   minBound :: () -> a
 
+type Lattice :: TYPE rep -> Constraint
 class POrd a => Lattice (a :: TYPE rep) where
   sup :: a -> a -> a
 
+type Bounded :: TYPE rep -> Constraint
 class (Lattice a, MinBound a) => Bounded (a :: TYPE rep) where
   maxBound :: () -> a
 
+type Complemented :: TYPE rep -> Constraint
 class Bounded a => Complemented (a :: TYPE rep) where
   not :: a -> a
 
+type Heyting :: TYPE rep -> Constraint
 class Bounded a => Heyting (a :: TYPE rep) where
   infixr 3 ==>
   (==>) :: a -> a -> a

testsuite/tests/dependent/should_fail/T13780c.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE DataKinds, PolyKinds #-}
@@ -7,7 +6,7 @@ module T13780c where
 import Data.Kind
 import T13780b
 
-type family ElimBool (p :: Bool -> Type) (b :: Bool) (s :: Sing b)
-                     (pFalse :: p False) (pTrue :: p True) :: p b where
+type ElimBool :: (Bool -> Type) -> forall (b :: Bool) -> Sing b -> p False -> p True -> p b
+type family ElimBool p b s pFalse pTrue where
   ElimBool _ _ SFalse pFalse _ = pFalse
   ElimBool _ _ STrue  _ pTrue  = pTrue

testsuite/tests/dependent/should_fail/T13780c.stderr

 [1 of 2] Compiling T13780b          ( T13780b.hs, T13780b.o )
 [2 of 2] Compiling T13780c          ( T13780c.hs, T13780c.o )
 
-T13780c.hs:12:16: error: [GHC-64578]
+T13780c.hs:11:16: error: [GHC-64578]
     • Data constructor ‘SFalse’ cannot be used here
         (it comes from a data family instance)
     • In the third argument of ‘ElimBool’, namely ‘SFalse’
       In the type family declaration for ‘ElimBool’
 
-T13780c.hs:13:16: error: [GHC-64578]
+T13780c.hs:12:16: error: [GHC-64578]
     • Data constructor ‘STrue’ cannot be used here
         (it comes from a data family instance)
     • In the third argument of ‘ElimBool’, namely ‘STrue’

testsuite/tests/dependent/should_fail/T15380.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE DataKinds #-}
@@ -14,7 +13,8 @@ class Generic a where
 class PGeneric a where
   type To a (x :: Rep a) :: a
 
-type family MDefault (x :: a) :: a where
+type MDefault :: a -> a
+type family MDefault x where
   MDefault x = To (M x)
 
 class C a where

testsuite/tests/ghci/scripts/T7939.hs

-{-# LANGUAGE Haskell2010 #-}
 {-# LANGUAGE TypeFamilies, PolyKinds, DataKinds, TypeOperators #-}
 module T7939 where
 import Data.Kind (Type)
@@ -23,6 +22,7 @@ type family K a where
   K '[] = Nothing
   K (h ': t) = Just h
 
-type family L (a :: k) (b :: Type) :: k where
+type L :: k -> Type -> k
+type family L a b where
   L Int Int = Bool
   L Maybe Bool = IO