Drop support for kind constraints.wip/p547

This implements proposal 547 and closes ticket #22298.
See the proposal and ticket for motivation.

Compiler perf improves a bit

Metrics: compile_time/bytes allocated
-------------------------------------
  CoOpt_Singletons(normal)   -2.4% GOOD
            T12545(normal)   +1.0%
            T13035(normal)  -13.5% GOOD
            T18478(normal)   +0.9%
            T9872d(normal)   -2.2% GOOD

                 geo. mean   -0.2%
                 minimum    -13.5%
                 maximum     +1.0%

Metric Decrease:
    CoOpt_Singletons
    T13035
    T9872d

22 files changed, 40 insertions, 160 deletions

diff --git a/testsuite/tests/dependent/should_compile/all.T b/testsuite/tests/dependent/should_compile/all.T
index 965e57dd16..5401a11e73 100644
--- a/testsuite/tests/dependent/should_compile/all.T
+++ b/testsuite/tests/dependent/should_compile/all.T
@@ -41,7 +41,6 @@ test('T14556', normal, compile, [''])
 test('T14720', normal, compile, [''])
 test('T14066a', normal, compile, [''])
 test('T14749', js_broken(22364), compile, [''])
-test('T14845_compile', normal, compile, [''])
 test('T14991', normal, compile, [''])
 test('DkNameRes', normal, compile, [''])
 test('T15346', normal, compile, [''])
diff --git a/testsuite/tests/dependent/should_fail/T13780a.stderr b/testsuite/tests/dependent/should_fail/T13780a.stderr
index 35ec45a24b..60edf6bc25 100644
--- a/testsuite/tests/dependent/should_fail/T13780a.stderr
+++ b/testsuite/tests/dependent/should_fail/T13780a.stderr
@@ -1,10 +1,7 @@
 
-T13780a.hs:9:40: error: [GHC-25897]
-    • Couldn't match kind ‘a’ with ‘Bool’
-      Expected kind ‘Foo a’, but ‘MkFoo’ has kind ‘Foo Bool’
-      ‘a’ is a rigid type variable bound by
-        a family instance declaration
-        at T13780a.hs:9:20-31
+T13780a.hs:9:40: error: [GHC-88634]
+    • Data constructor ‘MkFoo’ cannot be used here
+        (it has an unpromotable context ‘a ~ Bool’)
     • In the second argument of ‘(~)’, namely ‘MkFoo’
       In the definition of data constructor ‘SMkFoo’
       In the data instance declaration for ‘Sing’
diff --git a/testsuite/tests/dependent/should_compile/T14845_compile.hs b/testsuite/tests/dependent/should_fail/T14845_compile.hs
index c059f1d5e9..c059f1d5e9 100644
--- a/testsuite/tests/dependent/should_compile/T14845_compile.hs
+++ b/testsuite/tests/dependent/should_fail/T14845_compile.hs
diff --git a/testsuite/tests/dependent/should_fail/T14845_compile.stderr b/testsuite/tests/dependent/should_fail/T14845_compile.stderr
new file mode 100644
index 0000000000..cfe062ae38
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T14845_compile.stderr
@@ -0,0 +1,7 @@
+
+T14845_compile.hs:15:15: error: [GHC-88634]
+    • Data constructor ‘MkA1’ cannot be used here
+        (it has an unpromotable context ‘a ~ Int’)
+    • In the first argument of ‘SA’, namely ‘MkA1’
+      In the type ‘SA MkA1’
+      In the definition of data constructor ‘SMkA1’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 5de2070a0e..64e5341f8e 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -27,6 +27,7 @@ test('T14066f', normal, compile_fail, [''])
 test('T14066g', normal, compile_fail, [''])
 test('T14845_fail1', normal, compile_fail, [''])
 test('T14845_fail2', normal, compile_fail, [''])
+test('T14845_compile', normal, compile_fail, [''])
 test('T15245', normal, compile_fail, [''])
 test('T15215', normal, compile_fail, [''])
 test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds'])
diff --git a/testsuite/tests/polykinds/T16902.stderr b/testsuite/tests/polykinds/T16902.stderr
index a918f90b95..baa9777849 100644
--- a/testsuite/tests/polykinds/T16902.stderr
+++ b/testsuite/tests/polykinds/T16902.stderr
@@ -1,9 +1,4 @@
 
-T16902.hs:12:10: error: [GHC-25897]
-    • Expected a type, but found something with kind ‘a’
-      ‘a’ is a rigid type variable bound by
-        the type signature for ‘MkF’
-        at T16902.hs:12:3-12
-    • In the type ‘F a’
-      In the definition of data constructor ‘MkF’
-      In the data declaration for ‘F’
+T16902.hs:11:1: error: [GHC-01259]
+    • Illegal constraint in a kind: (a ~~ k) => *
+    • In the data type declaration for ‘F’
diff --git a/testsuite/tests/polykinds/T18522-ppr.script b/testsuite/tests/polykinds/T18522-ppr.script
index 54d3619c6e..e91cc1ce88 100644
--- a/testsuite/tests/polykinds/T18522-ppr.script
+++ b/testsuite/tests/polykinds/T18522-ppr.script
@@ -1,4 +1,4 @@
-:set -XPolyKinds -XDataKinds -XRankNTypes -XTypeFamilies
+:set -XPolyKinds -XDataKinds -XRankNTypes -XTypeFamilies -fprint-explicit-foralls
 import Data.Kind (Type)
-type family T :: forall k -> (k ~ k) => forall j -> k -> j -> Type
+type family T :: forall a -> ()
 :k T
diff --git a/testsuite/tests/polykinds/T18522-ppr.stdout b/testsuite/tests/polykinds/T18522-ppr.stdout
index 241530bbed..ce5cea6b49 100644
--- a/testsuite/tests/polykinds/T18522-ppr.stdout
+++ b/testsuite/tests/polykinds/T18522-ppr.stdout
@@ -1 +1 @@
-T :: forall k -> (k ~ k) => forall j -> k -> j -> *
+T :: forall {k}. forall (a :: k) -> ()
diff --git a/testsuite/tests/saks/should_compile/all.T b/testsuite/tests/saks/should_compile/all.T
index 78eb3e2331..29c43b4ae1 100644
--- a/testsuite/tests/saks/should_compile/all.T
+++ b/testsuite/tests/saks/should_compile/all.T
@@ -6,7 +6,6 @@ test('saks003', normal, compile, [''])
 test('saks004', normal, compile, [''])
 test('saks005', normal, compile, [''])
 test('saks006', normal, compile, [''])
-test('saks007', normal, compile, [''])
 test('saks008', normal, compile, [''])
 test('saks009', normal, compile, [''])
 test('saks010', normal, compile, [''])
diff --git a/testsuite/tests/saks/should_compile/saks007.hs b/testsuite/tests/saks/should_compile/saks007.hs
deleted file mode 100644
index 0d3a94f9c9..0000000000
--- a/testsuite/tests/saks/should_compile/saks007.hs
+++ /dev/null
@@ -1,40 +0,0 @@
-{-# LANGUAGE StandaloneKindSignatures #-}
-{-# LANGUAGE TypeFamilies, GADTs, PolyKinds, DataKinds, ExplicitForAll #-}
-
--- See also: saks007_fail.hs
-module SAKS_007 where
-
-import Data.Kind (Type, Constraint)
-
-type family F a where { F Type = True; F _ = False }
-type family G a where { G Type = False; G _ = True }
-
-type X :: forall k1 k2. (F k1 ~ G k2) => k1 -> k2 -> Type
-data X a b where
-  MkX :: X Integer Maybe   -- OK: F Type ~ G (Type -> Type)
-                           --     True ~ True
-
-
-{-
-Let   co :: F Type ~ G (Type->Type)
-
-Wrapper data con type:
-  $WMkX :: X @Type @(Type->Type) @(Eq# co) Integer Maybe
-
-Worker data con's type:
-  MkX :: forall k1 k2 (c :: F k1 ~ G k2) (a :: k1) (b :: k2)
-      -> forall .   -- No existentials
-         ( k1 ~# Type, k2 ~# Type->Type     -- EqSpec
-         , a ~# Integer, b ~# Maybe )
-      => X k1 k2 c a b
-
-f :: forall k. (k ~ Type) => forall (a::k). a->a
-
-
-f :: forall (cv :: a ~# b) => ....ty|>co....
-
-
-X @kk1 @kk2 @(d :: F kk1 ~ G kk2) Integer Maybe
-
-
--}
\ No newline at end of file
diff --git a/testsuite/tests/saks/should_fail/T16758.hs b/testsuite/tests/saks/should_fail/T16758.hs
deleted file mode 100644
index 2798156f3c..0000000000
--- a/testsuite/tests/saks/should_fail/T16758.hs
+++ /dev/null
@@ -1,14 +0,0 @@
-{-# LANGUAGE StandaloneKindSignatures #-}
-{-# LANGUAGE ConstrainedClassMethods #-}
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ExplicitForAll #-}
-
-module T16758 where
-
-import Data.Kind
-
-type C :: forall (a :: Type) -> a ~ Int => Constraint
-class C a where
-  f :: C a => a -> Int
diff --git a/testsuite/tests/saks/should_fail/all.T b/testsuite/tests/saks/should_fail/all.T
index 98345aa2ca..a17eed6a2e 100644
--- a/testsuite/tests/saks/should_fail/all.T
+++ b/testsuite/tests/saks/should_fail/all.T
@@ -31,7 +31,6 @@ test('T16727b', normal, compile_fail, [''])
 test('T16725', normal, compile_fail, [''])
 test('T16826', normal, compile_fail, [''])
 test('T16756b', normal, compile_fail, [''])
-test('T16758', normal, compile_fail, [''])
 test('T18863a', normal, compile_fail, [''])
 test('T18863b', normal, compile_fail, [''])
 test('T20916', normal, compile_fail, [''])
diff --git a/testsuite/tests/saks/should_fail/saks007_fail.stderr b/testsuite/tests/saks/should_fail/saks007_fail.stderr
index a299c5be4a..f096aa5e18 100644
--- a/testsuite/tests/saks/should_fail/saks007_fail.stderr
+++ b/testsuite/tests/saks/should_fail/saks007_fail.stderr
@@ -1,8 +1,7 @@
 
-saks007_fail.hs:15:10: error: [GHC-83865]
-    • Couldn't match kind ‘True’ with ‘False’
-      Expected: G (*)
-        Actual: F (*)
-    • In the type ‘X Integer String’
-      In the definition of data constructor ‘MkX’
-      In the data declaration for ‘X’
+saks007_fail.hs:13:11: error: [GHC-01259]
+    • Illegal constraint in a kind: forall k1 k2.
+                                    (F k1 ~ G k2) =>
+                                    k1 -> k2 -> *
+    • In a standalone kind signature for ‘X’:
+        forall k1 k2. (F k1 ~ G k2) => k1 -> k2 -> Type
diff --git a/testsuite/tests/typecheck/should_compile/T15141.hs b/testsuite/tests/typecheck/should_compile/T15141.hs
deleted file mode 100644
index c0cb5d8488..0000000000
--- a/testsuite/tests/typecheck/should_compile/T15141.hs
+++ /dev/null
@@ -1,35 +0,0 @@
-{-# LANGUAGE PolyKinds, TypeFamilies, TypeFamilyDependencies,
-             ScopedTypeVariables, TypeOperators, GADTs,
-             DataKinds #-}
-
-module T15141 where
-
-import Data.Type.Equality
-import Data.Proxy
-
-type family F a = r | r -> a where
-  F () = Bool
-
-data Wumpus where
-  Unify :: k1 ~ F k2 => k1 -> k2 -> Wumpus
-
-f :: forall k (a :: k). k :~: Bool -> ()
-f Refl = let x :: Proxy ('Unify a b)
-             x = undefined
-         in ()
-
-{-
-We want this situation:
-
-forall[1] k[1].
-  [G] k ~ Bool
-  forall [2] ... . [W] k ~ F kappa[2]
-
-where the inner wanted can be solved only by taking the outer
-given into account. This means that the wanted needs to be floated out.
-More germane to this bug, we need *not* to generalize over kappa.
-
-The code above builds this scenario fairly exactly, and indeed fails
-without the logic in kindGeneralize that excludes constrained variables
-from generalization.
--}
diff --git a/testsuite/tests/typecheck/should_compile/T17021a.hs b/testsuite/tests/typecheck/should_compile/T17021a.hs
index aa78cb2959..41eb3f9d92 100644
--- a/testsuite/tests/typecheck/should_compile/T17021a.hs
+++ b/testsuite/tests/typecheck/should_compile/T17021a.hs
@@ -9,16 +9,5 @@ import GHC.Exts
 type family Id x where
   Id x = x
 
---type LevId :: TYPE (Id LiftedRep) -> TYPE (Id LiftedRep)
---newtype LevId x = MkLevId x
-
-type LevId2 :: (r ~ Id LiftedRep) => TYPE r -> TYPE r
-newtype LevId2 x = MkLevId2 x
-
-{-
-MkLevId2 :: forall (r :: RuntimeRep).
-            forall (c :: r ~ Id LiftedRep) ->    -- c is a TyVar
-            forall (x :: TYPE r).
-            x -> LevId2 @r @c x
-
--}
\ No newline at end of file
+type LevId :: TYPE (Id LiftedRep) -> TYPE (Id LiftedRep)
+newtype LevId x = MkLevId x
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 577ce86d65..0a1edfa866 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -588,7 +588,6 @@ test('T13785', normal, compile, [''])
 test('T13804', normal, compile, [''])
 test('T13822', js_broken(22364), compile, [''])
 test('T13848', normal, compile, [''])
-test('T13871', normal, compile, [''])
 test('T13879', normal, compile, [''])
 test('T13881', normal, compile, [''])
 test('T18851d', normal, compile, [''])
@@ -655,7 +654,6 @@ test('T15431', normal, compile, [''])
 test('T15431a', normal, compile, [''])
 test('T15428', normal, compile, [''])
 test('T15412', normal, compile, [''])
-test('T15141', normal, compile, [''])
 test('T15473', normal, compile_fail, [''])
 test('T15499', normal, compile, [''])
 test('T15586', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T12102.stderr b/testsuite/tests/typecheck/should_fail/T12102.stderr
new file mode 100644
index 0000000000..6fd539cfa1
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T12102.stderr
@@ -0,0 +1,6 @@
+
+T12102.hs:17:1: error: [GHC-01259]
+    • Illegal constraint in a kind: forall a.
+                                    (IsTypeLit a ~ True) =>
+                                    a -> *
+    • In the data type declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/T12102b.hs b/testsuite/tests/typecheck/should_fail/T12102b.hs
deleted file mode 100644
index 8478059c8f..0000000000
--- a/testsuite/tests/typecheck/should_fail/T12102b.hs
+++ /dev/null
@@ -1,21 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeFamilies #-}
-module T12102b where
-
-import Data.Kind
-import GHC.TypeLits
-
-type family IsTypeLit a where
-  IsTypeLit Nat    = 'True
-  IsTypeLit Symbol = 'True
-  IsTypeLit a      = 'False
-
-data T :: forall a. (IsTypeLit a ~ 'True) => a -> Type where
-  MkNat    :: T 42
-  MkSymbol :: T "Don't panic!"
-
-deriving instance Show (T a)
diff --git a/testsuite/tests/typecheck/should_compile/T13871.hs b/testsuite/tests/typecheck/should_fail/T13871.hs
index fa233247ca..fa233247ca 100644
--- a/testsuite/tests/typecheck/should_compile/T13871.hs
+++ b/testsuite/tests/typecheck/should_fail/T13871.hs
diff --git a/testsuite/tests/typecheck/should_fail/T13871.stderr b/testsuite/tests/typecheck/should_fail/T13871.stderr
new file mode 100644
index 0000000000..0961d5f750
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T13871.stderr
@@ -0,0 +1,7 @@
+
+T13871.hs:16:18: error: [GHC-88634]
+    • Data constructor ‘MkFoo’ cannot be used here
+        (it has an unpromotable context ‘(a ~ Int, b ~ Char)’)
+    • In the first argument of ‘SFoo’, namely ‘MkFoo’
+      In the type ‘SFoo MkFoo’
+      In the definition of data constructor ‘SMkFoo’
diff --git a/testsuite/tests/typecheck/should_fail/T15862.hs b/testsuite/tests/typecheck/should_fail/T15862.hs
index c98b5939d1..7890b18ce7 100644
--- a/testsuite/tests/typecheck/should_fail/T15862.hs
+++ b/testsuite/tests/typecheck/should_fail/T15862.hs
@@ -28,9 +28,3 @@ data Quux = MkQuux (# Bool | Int #)
 
 quux :: TypeRep MkQuux
 quux = typeRep
-
-data Quuz :: (Type ~ Type) => Type where
-  MkQuuz :: Quuz
-
-quuz :: TypeRep MkQuuz
-quuz = typeRep
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 7d7b7f0369..b15a50b228 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -421,9 +421,9 @@ test('T12063', [expect_broken(12063)], multimod_compile_fail, ['T12063', '-v0'])
 test('T12083a', normal, compile_fail, [''])
 test('T12083b', normal, compile_fail, [''])
 test('T11974b', normal, compile_fail, [''])
-test('T12102', normal, compile, [''])
-test('T12102b', normal, compile_fail, [''])
+test('T12102', normal, compile_fail, [''])
 test('T12151', normal, compile_fail, [''])
+test('T13871', normal, compile_fail, [''])
 test('T7437', normal, compile_fail, [''])
 test('T12177', normal, compile_fail, [''])
 test('T12406', normal, compile_fail, [''])