Revert "Specify kind variables for inferred kinds in base."wip/revert-MR3132

As noted in !3132, this has rather severe knock-on consequences in
user-code. We'll need to revisit this before merging something along
these lines.

This reverts commit 9749fe1223d182b1f8e7e4f7378df661c509f396.

2 files changed, 31 insertions, 44 deletions

diff --git a/libraries/base/Data/Type/Coercion.hs b/libraries/base/Data/Type/Coercion.hs
index a3c920d8e4..694bedec01 100644
--- a/libraries/base/Data/Type/Coercion.hs
+++ b/libraries/base/Data/Type/Coercion.hs
@@ -1,16 +1,14 @@
-{-# LANGUAGE DeriveGeneric            #-}
-{-# LANGUAGE FlexibleInstances        #-}
-{-# LANGUAGE GADTs                    #-}
-{-# LANGUAGE MagicHash                #-}
-{-# LANGUAGE NoImplicitPrelude        #-}
-{-# LANGUAGE PolyKinds                #-}
-{-# LANGUAGE RankNTypes               #-}
-{-# LANGUAGE ScopedTypeVariables      #-}
-{-# LANGUAGE StandaloneDeriving       #-}
-{-# LANGUAGE StandaloneKindSignatures #-}
-{-# LANGUAGE TypeApplications         #-}
-{-# LANGUAGE TypeFamilies             #-}
-{-# LANGUAGE TypeOperators            #-}
+{-# LANGUAGE DeriveGeneric       #-}
+{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE TypeFamilies        #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE GADTs               #-}
+{-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE StandaloneDeriving  #-}
+{-# LANGUAGE NoImplicitPrelude   #-}
+{-# LANGUAGE PolyKinds           #-}
+{-# LANGUAGE RankNTypes          #-}
+{-# LANGUAGE MagicHash           #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -49,10 +47,9 @@ import GHC.Base
 -- To use this equality in practice, pattern-match on the @Coercion a b@ to get out
 -- the @Coercible a b@ instance, and then use 'coerce' to apply it.
 --
--- @since 4.7.0.0. Kind `k` explicitly quantified since 4.15.0.0.
-type Coercion :: forall k. k -> k -> Type
+-- @since 4.7.0.0
 data Coercion a b where
-  Coercion :: Coercible @k a b => Coercion @k a b
+  Coercion :: Coercible a b => Coercion a b
 
 -- with credit to Conal Elliott for 'ty', Erik Hesselink & Martijn van
 -- Steenbergen for 'type-equality', Edward Kmett for 'eq', and Gabor Greif
@@ -81,13 +78,13 @@ repr :: (a Eq.:~: b) -> Coercion a b
 repr Eq.Refl = Coercion
 
 -- | @since 4.7.0.0
-deriving instance Eq (Coercion a b)
+deriving instance Eq   (Coercion a b)
 
 -- | @since 4.7.0.0
 deriving instance Show (Coercion a b)
 
 -- | @since 4.7.0.0
-deriving instance Ord (Coercion a b)
+deriving instance Ord  (Coercion a b)
 
 -- | @since 4.7.0.0
 deriving instance Coercible a b => Read (Coercion a b)
@@ -105,13 +102,9 @@ deriving instance Coercible a b => Bounded (Coercion a b)
 -- | This class contains types where you can learn the equality of two types
 -- from information contained in /terms/. Typically, only singleton types should
 -- inhabit this class.
---
--- Kind `k` explicitly quantified since 4.15.0.0.
-type  TestCoercion :: forall k. (k -> Type) -> Constraint
-class TestCoercion (f :: k -> Type) where
+class TestCoercion f where
   -- | Conditionally prove the representational equality of @a@ and @b@.
-  testCoercion :: forall (a :: k) (b :: k).
-    f a -> f b -> Maybe (Coercion @k a b)
+  testCoercion :: f a -> f b -> Maybe (Coercion a b)
 
 -- | @since 4.7.0.0
 instance TestCoercion ((Eq.:~:) a) where
diff --git a/libraries/base/Data/Type/Equality.hs b/libraries/base/Data/Type/Equality.hs
index aa19ae3064..ab321ba011 100644
--- a/libraries/base/Data/Type/Equality.hs
+++ b/libraries/base/Data/Type/Equality.hs
@@ -1,20 +1,19 @@
-{-# LANGUAGE DataKinds              #-}
 {-# LANGUAGE DeriveGeneric          #-}
-{-# LANGUAGE ExplicitNamespaces     #-}
-{-# LANGUAGE FlexibleInstances      #-}
-{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE TypeOperators          #-}
 {-# LANGUAGE GADTs                  #-}
-{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE StandaloneDeriving     #-}
 {-# LANGUAGE NoImplicitPrelude      #-}
-{-# LANGUAGE PolyKinds              #-}
 {-# LANGUAGE RankNTypes             #-}
-{-# LANGUAGE StandaloneDeriving     #-}
-{-# LANGUAGE StandaloneKindSignatures #-}
-{-# LANGUAGE Trustworthy            #-}
-{-# LANGUAGE TypeApplications       #-}
 {-# LANGUAGE TypeFamilies           #-}
-{-# LANGUAGE TypeOperators          #-}
 {-# LANGUAGE UndecidableInstances   #-}
+{-# LANGUAGE ExplicitNamespaces     #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE Trustworthy            #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -62,8 +61,7 @@ infix 4 :~:, :~~:
 -- in practice, pattern-match on the @a :~: b@ to get out the @Refl@ constructor;
 -- in the body of the pattern-match, the compiler knows that @a ~ b@.
 --
--- @since 4.7.0.0. Kind `k` explicitly quantified since 4.15.0.0.
-type (:~:) :: forall k. k -> k -> Type
+-- @since 4.7.0.0
 data a :~: b where  -- See Note [The equality types story] in GHC.Builtin.Types.Prim
   Refl :: a :~: a
 
@@ -124,9 +122,8 @@ deriving instance a ~ b => Bounded (a :~: b)
 -- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is
 -- inhabited by a terminating value if and only if @a@ is the same type as @b@.
 --
--- @since 4.10.0.0. Kinds `k1` and `k2` explicitly quantified since
--- 4.15.0.0.
-type (:~~:) :: forall k1 k2. k1 -> k2 -> Type
+-- @since 4.10.0.0
+type (:~~:) :: k1 -> k2 -> Type
 data a :~~: b where
    HRefl :: a :~~: a
 
@@ -153,9 +150,6 @@ deriving instance a ~~ b => Bounded (a :~~: b)
 -- | This class contains types where you can learn the equality of two types
 -- from information contained in /terms/. Typically, only singleton types should
 -- inhabit this class.
---
--- Kind `k` explicitly quantified since 4.15.0.0.
-type  TestEquality :: forall k. (k -> Type) -> Constraint
 class TestEquality f where
   -- | Conditionally prove the equality of @a@ and @b@.
   testEquality :: f a -> f b -> Maybe (a :~: b)
@@ -171,7 +165,7 @@ instance TestEquality ((:~~:) a) where
 infix 4 ==
 
 -- | A type family to compute Boolean equality.
-type (==) :: forall k. k -> k -> Bool
+type (==) :: k -> k -> Bool
 type family a == b where
   f a == g b = f == g && a == b
   a == a = 'True