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.

9 files changed, 41 insertions, 81 deletions

diff --git a/libraries/base/Data/Data.hs b/libraries/base/Data/Data.hs
index 0ce830742a..a8dfa61115 100644
--- a/libraries/base/Data/Data.hs
+++ b/libraries/base/Data/Data.hs
@@ -1,10 +1,10 @@
 {-# LANGUAGE BangPatterns #-}
-{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
diff --git a/libraries/base/Data/Dynamic.hs b/libraries/base/Data/Dynamic.hs
index 8478f0e680..5a4f3f9a08 100644
--- a/libraries/base/Data/Dynamic.hs
+++ b/libraries/base/Data/Dynamic.hs
@@ -1,9 +1,9 @@
-{-# LANGUAGE ExplicitForAll #-}
-{-# LANGUAGE GADTs #-}
+{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ExplicitForAll #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeApplications #-}
 
 -----------------------------------------------------------------------------
diff --git a/libraries/base/Data/Fixed.hs b/libraries/base/Data/Fixed.hs
index 17e5141b33..232175a1ab 100644
--- a/libraries/base/Data/Fixed.hs
+++ b/libraries/base/Data/Fixed.hs
@@ -1,9 +1,7 @@
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -43,7 +41,6 @@ module Data.Fixed
 import Data.Data
 import GHC.TypeLits (KnownNat, natVal)
 import GHC.Read
-import Data.Kind (Type, Constraint)
 import Text.ParserCombinators.ReadPrec
 import Text.Read.Lex
 
@@ -64,8 +61,7 @@ mod' n d = n - (fromInteger f) * d where
     f = div' n d
 
 -- | The type parameter should be an instance of 'HasResolution'.
-type    Fixed :: forall k. k -> Type
-newtype Fixed a = MkFixed Integer
+newtype Fixed (a :: k) = MkFixed Integer
         deriving ( Eq  -- ^ @since 2.01
                  , Ord -- ^ @since 2.01
                  )
@@ -84,8 +80,7 @@ instance (Typeable k,Typeable a) => Data (Fixed (a :: k)) where
     dataTypeOf _ = tyFixed
     toConstr _ = conMkFixed
 
-type  HasResolution :: forall k. k -> Constraint
-class HasResolution a where
+class HasResolution (a :: k) where
     resolution :: p a -> Integer
 
 -- | For example, @Fixed 1000@ will give you a 'Fixed' with a resolution of 1000.
diff --git a/libraries/base/Data/Functor/Compose.hs b/libraries/base/Data/Functor/Compose.hs
index 225d16283b..d8369ebc05 100644
--- a/libraries/base/Data/Functor/Compose.hs
+++ b/libraries/base/Data/Functor/Compose.hs
@@ -3,7 +3,6 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE Trustworthy #-}
 {-# LANGUAGE TypeOperators #-}
 -----------------------------------------------------------------------------
@@ -27,7 +26,6 @@ module Data.Functor.Compose (
 
 import Data.Functor.Classes
 
-import Data.Kind (Type)
 import Control.Applicative
 import Data.Coerce (coerce)
 import Data.Data (Data)
@@ -40,9 +38,6 @@ infixr 9 `Compose`
 -- | Right-to-left composition of functors.
 -- The composition of applicative functors is always applicative,
 -- but the composition of monads is not always a monad.
---
--- Kinds `k2` and `k1` explicitly quantified since 4.15.0.0.
-type    Compose :: forall k2 k1. (k2 -> Type) -> (k1 -> k2) -> (k1 -> Type)
 newtype Compose f g a = Compose { getCompose :: f (g a) }
   deriving ( Data     -- ^ @since 4.9.0.0
            , Generic  -- ^ @since 4.9.0.0
@@ -131,7 +126,7 @@ instance (Alternative f, Applicative g) => Alternative (Compose f g) where
 -- | The deduction (via generativity) that if @g x :~: g y@ then @x :~: y@.
 --
 -- @since 4.14.0.0
-instance TestEquality f => TestEquality (Compose f g) where
+instance (TestEquality f) => TestEquality (Compose f g) where
   testEquality (Compose x) (Compose y) =
     case testEquality x y of -- :: Maybe (g x :~: g y)
       Just Refl -> Just Refl -- :: Maybe (x :~: y)
diff --git a/libraries/base/Data/Functor/Const.hs b/libraries/base/Data/Functor/Const.hs
index dd1880e30b..651041f15b 100644
--- a/libraries/base/Data/Functor/Const.hs
+++ b/libraries/base/Data/Functor/Const.hs
@@ -2,9 +2,7 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE StandaloneKindSignatures #-}
 {-# LANGUAGE Trustworthy #-}
 
 -----------------------------------------------------------------------------
@@ -38,9 +36,6 @@ import GHC.Read (Read(readsPrec), readParen, lex)
 import GHC.Show (Show(showsPrec), showParen, showString)
 
 -- | The 'Const' functor.
---
--- Kind `k` explicitly quantified since 4.15.0.0.
-type    Const :: forall k. Type -> k -> Type
 newtype Const a b = Const { getConst :: a }
     deriving ( Bits       -- ^ @since 4.9.0.0
              , Bounded    -- ^ @since 4.9.0.0
diff --git a/libraries/base/Data/Functor/Product.hs b/libraries/base/Data/Functor/Product.hs
index 266a72d75e..a3678e910e 100644
--- a/libraries/base/Data/Functor/Product.hs
+++ b/libraries/base/Data/Functor/Product.hs
@@ -1,9 +1,7 @@
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE Safe #-}
-{-# LANGUAGE StandaloneKindSignatures #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Functor.Product
@@ -28,15 +26,11 @@ import Control.Monad (MonadPlus(..))
 import Control.Monad.Fix (MonadFix(..))
 import Control.Monad.Zip (MonadZip(mzipWith))
 import Data.Data (Data)
-import Data.Kind (Type)
 import Data.Functor.Classes
 import GHC.Generics (Generic, Generic1)
 import Text.Read (Read(..), readListDefault, readListPrecDefault)
 
 -- | Lifted product of functors.
---
--- Kind `k` explicitly quantified since 4.15.0.0.
-type Product :: forall k. (k -> Type) -> (k -> Type) -> (k -> Type)
 data Product f g a = Pair (f a) (g a)
   deriving ( Data     -- ^ @since 4.9.0.0
            , Generic  -- ^ @since 4.9.0.0
diff --git a/libraries/base/Data/Functor/Sum.hs b/libraries/base/Data/Functor/Sum.hs
index cca541fe5e..f7d6178a2b 100644
--- a/libraries/base/Data/Functor/Sum.hs
+++ b/libraries/base/Data/Functor/Sum.hs
@@ -1,9 +1,7 @@
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE Safe #-}
-{-# LANGUAGE StandaloneKindSignatures #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Functor.Sum
@@ -25,15 +23,11 @@ module Data.Functor.Sum (
 
 import Control.Applicative ((<|>))
 import Data.Data (Data)
-import Data.Kind (Type)
 import Data.Functor.Classes
 import GHC.Generics (Generic, Generic1)
 import Text.Read (Read(..), readListDefault, readListPrecDefault)
 
 -- | Lifted sum of functors.
---
--- Kind `k` explicitly quantified since 4.15.0.0.
-type Sum :: forall k. (k -> Type) -> (k -> Type) -> (k -> Type)
 data Sum f g a = InL (f a) | InR (g a)
   deriving ( Data     -- ^ @since 4.9.0.0
            , Generic  -- ^ @since 4.9.0.0
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