Improve out-of-order inferred type variables

  Don't instantiate type variables for :type in
  `GHC.Tc.Gen.App.tcInstFun`, to avoid inconsistently instantianting
  `r1` but not `r2` in the type

    forall {r1} (a :: TYPE r1) {r2} (b :: TYPE r2). ...

  This fixes #21088.

  This patch also changes the primop pretty-printer to ensure
  that we put all the inferred type variables first. For example,
  the type of reallyUnsafePtrEquality# is now

    forall {l :: Levity} {k :: Levity}
           (a :: TYPE (BoxedRep l))
           (b :: TYPE (BoxedRep k)).
      a -> b -> Int#

  This means we avoid running into issue #21088 entirely with
  the types of primops. Users can still write a type signature where
  the inferred type variables don't come first, however.

  This change to primops had a knock-on consequence, revealing that
  we were sometimes performing eta reduction on keepAlive#.
  This patch updates tryEtaReduce to avoid eta reducing functions
  with no binding, bringing it in line with tryEtaReducePrep,
  and thus fixing #21090.

21 files changed, 270 insertions, 120 deletions

diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs
index baefb7712b..03e2ecee55 100644
--- a/compiler/GHC/Core/Utils.hs
+++ b/compiler/GHC/Core/Utils.hs
@@ -38,7 +38,7 @@ module GHC.Core.Utils (
         diffBinds,
 
         -- * Lambdas and eta reduction
-        tryEtaReduce,
+        tryEtaReduce, canEtaReduceToArity,
 
         -- * Manipulating data constructors and types
         exprToType, exprToCoercion_maybe,
@@ -2448,17 +2448,10 @@ tryEtaReduce bndrs body
     ok_fun _fun                = False
 
     ---------------
-    ok_fun_id fun = -- There are arguments to reduce
+    ok_fun_id fun = -- There are arguments to reduce...
                     fun_arity fun >= incoming_arity &&
-                    -- We always want args for join points so
-                    -- we should never eta-reduce to a trivial expression.
-                    -- See Note [Invariants on join points] in GHC.Core, and #20599
-                    not (isJoinId fun) &&
-                    -- And the function doesn't require visible arguments as part of
-                    -- it's calling convention. See Note [Strict Worker Ids]
-                    idCbvMarkArity fun == 0
-
-
+                    -- ... and the function can be eta reduced to arity 0
+                    canEtaReduceToArity fun 0 0
     ---------------
     fun_arity fun             -- See Note [Arity care]
        | isLocalId fun
@@ -2505,6 +2498,28 @@ tryEtaReduce bndrs body
 
     ok_arg _ _ _ _ = Nothing
 
+-- | Can we eta-reduce the given function to the specified arity?
+-- See Note [Eta reduction conditions].
+canEtaReduceToArity :: Id -> JoinArity -> Arity -> Bool
+canEtaReduceToArity fun dest_join_arity dest_arity =
+  not $
+        hasNoBinding fun
+       -- Don't undersaturate functions with no binding.
+
+    ||  ( isJoinId fun && dest_join_arity < idJoinArity fun )
+       -- Don't undersaturate join points.
+       -- See Note [Invariants on join points] in GHC.Core, and #20599
+
+    || ( dest_arity < idCbvMarkArity fun )
+       -- Don't undersaturate StrictWorkerIds.
+       -- See Note [Strict Worker Ids] in GHC.CoreToStg.Prep.
+
+    ||  isLinearType (idType fun)
+       -- Don't perform eta reduction on linear types.
+       -- If `f :: A %1-> B` and `g :: A -> B`,
+       -- then `g x = f x` is OK but `g = f` is not.
+       -- See Note [Eta reduction conditions].
+
 {-
 Note [Eta reduction of an eval'd function]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/CoreToStg/Prep.hs b/compiler/GHC/CoreToStg/Prep.hs
index 2e998bf94e..b8593b47a0 100644
--- a/compiler/GHC/CoreToStg/Prep.hs
+++ b/compiler/GHC/CoreToStg/Prep.hs
@@ -1054,9 +1054,9 @@ cpeApp top_env expr
             (Var f)
             args
         | Just KeepAliveOp <- isPrimOpId_maybe f
-        , CpeApp (Type arg_rep)
-          : CpeApp (Type arg_ty)
+        , CpeApp (Type arg_lev)
           : CpeApp (Type _result_rep)
+          : CpeApp (Type arg_ty)
           : CpeApp (Type result_ty)
           : CpeApp arg
           : CpeApp s0
@@ -1070,13 +1070,14 @@ cpeApp top_env expr
                   _          -> cpe_app env k (CpeApp s0 : rest)
              ; let touchId = primOpId TouchOp
                    expr = Case k' y result_ty [Alt DEFAULT [] rhs]
-                   rhs = let scrut = mkApps (Var touchId) [Type arg_rep, Type arg_ty, arg, Var realWorldPrimId]
+                   rhs = let scrut = mkApps (Var touchId) [Type arg_lev, Type arg_ty, arg, Var realWorldPrimId]
                          in Case scrut s2 result_ty [Alt DEFAULT [] (Var y)]
              ; (floats', expr') <- cpeBody env expr
              ; return (floats `appendFloats` floats', expr')
              }
         | Just KeepAliveOp <- isPrimOpId_maybe f
-        = panic "invalid keepAlive# application"
+        = pprPanic "invalid keepAlive# application" $
+            vcat [ text "args:" <+> ppr args ]
 
     -- runRW# magic
     cpe_app env (Var f) (CpeApp _runtimeRep@Type{} : CpeApp _type@Type{} : CpeApp arg : rest)
@@ -1651,16 +1652,7 @@ tryEtaReducePrep bndrs expr@(App _ _)
     ok bndr (Var arg) = bndr == arg
     ok _    _         = False
 
-    -- We can't eta reduce something which must be saturated.
-    ok_to_eta_reduce (Var f) =  not (hasNoBinding f) &&
-                                not (isLinearType (idType f)) && -- Unsure why this is unsafe.
-                                (not (isJoinId f) || idJoinArity f <= n_remaining) &&
-                                -- Don't undersaturate join points.
-                                -- See Note [Invariants on join points] in GHC.Core, and #20599
-                                (idCbvMarkArity f <= n_remaining_vals)
-                                -- Similar for StrictWorkerIds. See Note [Strict Worker Ids]
-
-
+    ok_to_eta_reduce (Var f) = canEtaReduceToArity f n_remaining n_remaining_vals
     ok_to_eta_reduce _       = False -- Safe. ToDo: generalise
 
 
diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs
index a6e505db96..ddf94f1410 100644
--- a/compiler/GHC/Tc/Gen/App.hs
+++ b/compiler/GHC/Tc/Gen/App.hs
@@ -754,18 +754,23 @@ tcInstFun do_ql inst_final (rn_fun, fun_ctxt) fun_sigma rn_args
           HsUnboundVar {} -> True
           _               -> False
 
-    inst_all :: ArgFlag -> Bool
+    inst_all, inst_inferred, inst_none :: ArgFlag -> Bool
     inst_all (Invisible {}) = True
     inst_all Required       = False
 
-    inst_inferred :: ArgFlag -> Bool
     inst_inferred (Invisible InferredSpec)  = True
     inst_inferred (Invisible SpecifiedSpec) = False
     inst_inferred Required                  = False
 
+    inst_none _ = False
+
     inst_fun :: [HsExprArg 'TcpRn] -> ArgFlag -> Bool
     inst_fun [] | inst_final  = inst_all
-                | otherwise   = inst_inferred
+                | otherwise   = inst_none
+                -- Using `inst_none` for `:type` avoids
+                -- `forall {r1} (a :: TYPE r1) {r2} (b :: TYPE r2). a -> b`
+                -- turning into `forall a {r2} (b :: TYPE r2). a -> b`.
+                -- See #21088.
     inst_fun (EValArg {} : _) = inst_all
     inst_fun _                = inst_inferred
 
diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs
index aa43b7e4e0..aa4be8e76e 100644
--- a/compiler/GHC/Tc/Module.hs
+++ b/compiler/GHC/Tc/Module.hs
@@ -2467,8 +2467,8 @@ tcGhciStmts stmts
 
       ; traceTc "GHC.Tc.Module.tcGhciStmts: done" empty
 
-      -- rec_expr is the expression
-      --      returnIO @ [()] [unsafeCoerce# () x, ..,  unsafeCorece# () z]
+      -- ret_expr is the expression
+      --      returnIO @[()] [unsafeCoerce# () x, ..,  unsafeCoerce# () z]
       --
       -- Despite the inconvenience of building the type applications etc,
       -- this *has* to be done in type-annotated post-typecheck form
diff --git a/docs/users_guide/9.4.1-notes.rst b/docs/users_guide/9.4.1-notes.rst
index 594d1035c2..0f92ab6eb5 100644
--- a/docs/users_guide/9.4.1-notes.rst
+++ b/docs/users_guide/9.4.1-notes.rst
@@ -151,6 +151,10 @@ Compiler
   enabled with :ghc-flag:`-Wall` (:ghc-ticket:`20531`), as a part of
   long-term push towards Dependent Haskell.
 
+- In GHCi, the :ghci-cmd:`:type` command no longer instantiates quantified
+  type variables when given a polymorphic type. (It used to instantiate
+  inferred type variables.)
+
 ``base`` library
 ~~~~~~~~~~~~~~~~
 
@@ -240,13 +244,13 @@ Compiler
   For example, the full type of ``newMutVar#`` is now: ::
 
         newMutVar#
-          :: forall s {l :: Levity} (a :: TYPE (BoxedRep l)).
+          :: forall {l :: Levity} s (a :: TYPE (BoxedRep l)).
              a -> State# s -> (# State# s, MVar# s a #)
 
   and the full type of ``writeSmallArray#`` is: ::
 
         writeSmallArray#
-          :: forall s {l :: Levity} (a :: TYPE (BoxedRep l)).
+          :: forall {l :: Levity} s (a :: TYPE (BoxedRep l)).
              SmallMutableArray# s a -> Int# -> a -> State# s -> State# s
 
 - ``ArrayArray#` and ``MutableArrayArray#`` have been moved from ``GHC.Prim`` to ``GHC.Exts``.
@@ -258,8 +262,9 @@ Compiler
   representation-polymorphic. For instance: ::
 
         mkWeakNoFinalizer#
-          :: forall {l :: Levity} (a :: TYPE (BoxedRep l))
-                    {k :: Levity} (b :: TYPE (BoxedRep k)).
+          :: forall {l :: Levity} {k :: Levity}
+                    (a :: TYPE (BoxedRep l))
+                    (b :: TYPE (BoxedRep k)).
              a -> b -> State# RealWorld -> (# State# RealWorld, Weak# b #)
 
   That is, the type signature now quantifies over the ``GHC.Exts.Levity`` of ``a``
@@ -272,8 +277,9 @@ Compiler
   than before. For example, ``catch#`` now has type: ::
 
         catch#
-          :: forall {r :: RuntimeRep} (a :: TYPE r)
-                    {l :: Levity} (b :: TYPE (BoxedRep l)).
+          :: forall {r :: RuntimeRep} {l :: Levity}
+                    (a :: TYPE r)
+                    (b :: TYPE (BoxedRep l)).
               ( State# RealWorld -> (# State# RealWorld, a #) )
           -> ( b -> State# RealWorld -> (# State# RealWorld, a #) )
           -> State# RealWorld -> (# State# RealWorld, a #)
@@ -289,8 +295,9 @@ Compiler
   Note in particular that ``raise#`` is now both representation-polymorphic
   (with an inferred `RuntimeRep` argument) and levity-polymorphic, with type: ::
 
-      raise# :: forall {l :: Levity} (a :: TYPE (BoxedRep l))
-                       {r :: RuntimeRep} (b :: TYPE r).
+      raise# :: forall {l :: Levity} {r :: RuntimeRep}
+                       (a :: TYPE (BoxedRep l))
+                       (b :: TYPE r).
                 a -> b
 
 - ``fork#`` and ``forkOn#`` are now representation-polymorphic. For example, ``fork#``
@@ -304,8 +311,9 @@ Compiler
   both levity-polymorphic and heterogeneous: ::
 
         reallyUnsafePtrEquality#
-          :: forall {l :: Levity} (a :: TYPE (BoxedRep l))
-                    {k :: Levity} (b :: TYPE (BoxedRep k))
+          :: forall {l :: Levity} {k :: Levity}
+                    (a :: TYPE (BoxedRep l))
+                    (b :: TYPE (BoxedRep k))
           . a -> b -> Int#
 
   This means that ``GHC.Exts.reallyUnsafePtrEquality#`` can be used
diff --git a/docs/users_guide/ghci.rst b/docs/users_guide/ghci.rst
index c26dedb5c3..bdce8d5933 100644
--- a/docs/users_guide/ghci.rst
+++ b/docs/users_guide/ghci.rst
@@ -2979,10 +2979,10 @@ commonly used commands.
 
 .. ghci-cmd:: :type; ⟨expression⟩
 
-    Infers and prints the type of ⟨expression⟩.  For polymorphic types
-    it instantiates the 'inferred' forall quantifiers (but not the
-    'specified' ones; see :ref:`inferred-vs-specified`), solves constraints,
-    re-generalises, and then reduces type families as much as possible.
+    Infers and prints the type of ⟨expression⟩, solving constraints and
+    reducing type families as much as possible.
+    For polymorphic types, it does not instantiate any forall quantified
+    variables.
 
     .. code-block:: none
 
@@ -2992,7 +2992,7 @@ commonly used commands.
     Type family reduction is skipped if the function is not fully instantiated,
     as this has been observed to give more intuitive results.
     You may want to use :ghci-cmd:`:info` if you are not applying any arguments,
-    as that will return the original type of the function without instantiating.
+    as that will return the original type of the function.
 
 .. ghci-cmd:: :type +d; ⟨expression⟩
 
diff --git a/libraries/ghc-prim/changelog.md b/libraries/ghc-prim/changelog.md
index 372018290b..0485c633af 100644
--- a/libraries/ghc-prim/changelog.md
+++ b/libraries/ghc-prim/changelog.md
@@ -96,7 +96,7 @@
 
   ```
   newMutVar#
-    :: forall s {l :: Levity} (a :: TYPE (BoxedRep l)).
+    :: forall {l :: Levity} s (a :: TYPE (BoxedRep l)).
        a -> State# s -> (# State# s, MVar# s a #)
   ```
 
@@ -104,7 +104,7 @@
 
   ```
   writeSmallArray#
-    :: forall s {l :: Levity} (a :: TYPE ('BoxedRep l)).
+    :: forall {l :: Levity} s (a :: TYPE ('BoxedRep l)).
        SmallMutableArray# s a -> Int# -> a -> State# s -> State# s
   ```
 
@@ -117,8 +117,9 @@
 
   ```
   mkWeakNoFinalizer#
-    :: forall {l :: Levity} (a :: TYPE ('BoxedRep l))
-              {k :: Levity} (b :: TYPE ('BoxedRep k)).
+    :: forall {l :: Levity} {k :: Levity}
+              (a :: TYPE ('BoxedRep l))
+              (b :: TYPE ('BoxedRep k)).
        a -> b -> State# RealWorld -> (# State# RealWorld, Weak# b #)
   ```
 
@@ -133,8 +134,9 @@
 
   ```
   catch#
-    :: forall {r :: RuntimeRep} (a :: TYPE r)
-              {l :: Levity} (b :: TYPE ('BoxedRep l)).
+    :: forall {r :: RuntimeRep} {l :: Levity}
+              (a :: TYPE r)
+              (b :: TYPE ('BoxedRep l)).
         ( State# RealWorld -> (# State# RealWorld, a #) )
     -> ( b -> State# RealWorld -> (# State# RealWorld, a #) )
     -> State# RealWorld -> (# State# RealWorld, a #)
@@ -152,8 +154,9 @@
   (with an inferred `RuntimeRep` argument) and levity-polymorphic, with type:
 
   ```
-  raise# :: forall {l :: Levity} (a :: TYPE (BoxedRep l))
-                   {r :: RuntimeRep} (b :: TYPE r).
+  raise# :: forall {l :: Levity} {r :: RuntimeRep}
+                   (a :: TYPE (BoxedRep l))
+                   (b :: TYPE r).
             a -> b
   ```
 
@@ -169,8 +172,9 @@
 
   ```
   reallyUnsafePtrEquality#
-    :: forall {l :: Levity} (a :: TYPE (BoxedRep l))
-              {k :: Levity} (b :: TYPE (BoxedRep k))
+    :: forall {l :: Levity} {k :: Levity}
+              (a :: TYPE (BoxedRep l))
+              (b :: TYPE (BoxedRep k))
     . a -> b -> Int#
   ```
 
diff --git a/testsuite/tests/corelint/LintEtaExpand.hs b/testsuite/tests/corelint/LintEtaExpand.hs
index 065dcb4041..1f3d7a540b 100644
--- a/testsuite/tests/corelint/LintEtaExpand.hs
+++ b/testsuite/tests/corelint/LintEtaExpand.hs
@@ -68,11 +68,11 @@ test_exprs  =
       mkApps (Var coerceId)
         [ Type runtimeRep1Ty ]
   , ("raise# OK", ) $
-      -- raise# @Lifted @Int @LiftedRep @(z -> z), where z :: TYPE r
+      -- raise# @Lifted @LiftedRep @Int @(z -> z), where z :: TYPE r
       mkApps (Var $ primOpId RaiseOp)
         [ Type liftedDataConTy
-        , Type intTy
         , Type liftedRepTy
+        , Type intTy
         , Type $ mkVisFunTyMany openAlphaTy openAlphaTy
         ]
   ]
diff --git a/testsuite/tests/ghci/scripts/T12550.stdout b/testsuite/tests/ghci/scripts/T12550.stdout
index 48a1b8e11c..d753d4f666 100644
--- a/testsuite/tests/ghci/scripts/T12550.stdout
+++ b/testsuite/tests/ghci/scripts/T12550.stdout
@@ -62,7 +62,8 @@ instance Functor (URec Int) -- Defined in ‘GHC.Generics’
 instance Functor (URec Word) -- Defined in ‘GHC.Generics’
 instance Functor V1 -- Defined in ‘GHC.Generics’
 datatypeName
-  ∷ ∀ d k1 (t ∷ ★ → (k1 → ★) → k1 → ★) (f ∷ k1 → ★) (a ∷ k1).
+  ∷ ∀ {k} (d ∷ k) k1 (t ∷ k → (k1 → ★) → k1 → ★) (f ∷ k1 → ★)
+      (a ∷ k1).
     Datatype d ⇒
     t d f a → [Char]
 type Datatype :: ∀ {k}. k → Constraint
diff --git a/testsuite/tests/ghci/scripts/T21088.hs b/testsuite/tests/ghci/scripts/T21088.hs
new file mode 100644
index 0000000000..efe4e8ab93
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T21088.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE PolyKinds, DataKinds, ScopedTypeVariables #-}
+
+module T21088 where
+
+import Data.Proxy
+  ( Proxy(..) )
+import GHC.Exts
+  ( TYPE, RuntimeRep )
+
+-- We don't change the order of quantification,
+-- so we check we are not instantiating `r1` but not `r2`,
+-- which would be quite confusing.
+foo :: forall {r1 :: RuntimeRep} (a1 :: TYPE r1)
+              {r2 :: RuntimeRep} (a2 :: TYPE r2)
+    .  Proxy a1 -> Proxy a2
+foo _ = Proxy
+
+bar :: forall {r1 :: RuntimeRep} {r2 :: RuntimeRep}
+              (a1 :: TYPE r1)    (a2 :: TYPE r2)
+    .  Proxy a1 -> Proxy a2
+bar _ = Proxy
+
+baz :: forall {k1} (a1 :: k1) {k2} (a2 :: k2)
+    .  Proxy a1 -> Proxy a2
+baz _ = Proxy
+
+quux :: forall {k1} {k2} (a1 :: k1) (a2 :: k2)
+     .  Proxy a1 -> Proxy a2
+quux _ = Proxy
diff --git a/testsuite/tests/ghci/scripts/T21088.script b/testsuite/tests/ghci/scripts/T21088.script
new file mode 100644
index 0000000000..fe809b1970
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T21088.script
@@ -0,0 +1,11 @@
+:l T21088
+:type foo
+:type bar
+:type baz
+:type quux
+
+:set -fprint-explicit-kinds -fprint-explicit-runtime-reps -fprint-explicit-foralls
+:type foo
+:type bar
+:type baz
+:type quux
diff --git a/testsuite/tests/ghci/scripts/T21088.stdout b/testsuite/tests/ghci/scripts/T21088.stdout
new file mode 100644
index 0000000000..ca3c4ddcc7
--- /dev/null
+++ b/testsuite/tests/ghci/scripts/T21088.stdout
@@ -0,0 +1,19 @@
+foo :: Proxy a1 -> Proxy a2
+bar :: Proxy a1 -> Proxy a2
+baz :: forall {k1} (a1 :: k1) {k2} (a2 :: k2). Proxy a1 -> Proxy a2
+quux
+  :: forall {k1} {k2} (a1 :: k1) (a2 :: k2). Proxy a1 -> Proxy a2
+foo
+  :: forall {r1 :: RuntimeRep} (a1 :: TYPE r1) {r2 :: RuntimeRep}
+            (a2 :: TYPE r2).
+     Proxy @{TYPE r1} a1 -> Proxy @{TYPE r2} a2
+bar
+  :: forall {r1 :: RuntimeRep} {r2 :: RuntimeRep} (a1 :: TYPE r1)
+            (a2 :: TYPE r2).
+     Proxy @{TYPE r1} a1 -> Proxy @{TYPE r2} a2
+baz
+  :: forall {k1} (a1 :: k1) {k2} (a2 :: k2).
+     Proxy @{k1} a1 -> Proxy @{k2} a2
+quux
+  :: forall {k1} {k2} (a1 :: k1) (a2 :: k2).
+     Proxy @{k1} a1 -> Proxy @{k2} a2
diff --git a/testsuite/tests/ghci/scripts/all.T b/testsuite/tests/ghci/scripts/all.T
index bccfa977e5..0f6ed54ddb 100755
--- a/testsuite/tests/ghci/scripts/all.T
+++ b/testsuite/tests/ghci/scripts/all.T
@@ -363,3 +363,4 @@ test('T20587', [extra_files(['../shell.hs'])], ghci_script,
 test('T20909', normal, ghci_script, ['T20909.script'])
 test('T20150', normal, ghci_script, ['T20150.script'])
 test('T20974', normal, ghci_script, ['T20974.script'])
+test('T21088', normal, ghci_script, ['T21088.script'])
diff --git a/testsuite/tests/numeric/should_compile/T19769.stderr-ws-32 b/testsuite/tests/numeric/should_compile/T19769.stderr-ws-32
index 21e9fa465c..33a23630ff 100644
--- a/testsuite/tests/numeric/should_compile/T19769.stderr-ws-32
+++ b/testsuite/tests/numeric/should_compile/T19769.stderr-ws-32
@@ -1,21 +1,21 @@
 
 ==================== Tidy Core ====================
 Result size of Tidy Core
-  = {terms: 68, types: 58, coercions: 0, joins: 0/0}
+  = {terms: 84, types: 66, coercions: 0, joins: 0/0}
 
-wi8 = word8ToInt8#
+wi8 = \ x -> word8ToInt8# x
 
-wi16 = word16ToInt16#
+wi16 = \ x -> word16ToInt16# x
 
-wi32 = word32ToInt32#
+wi32 = \ x -> word32ToInt32# x
 
 wi64 = \ x -> intToInt64# (word2Int# (word64ToWord# x))
 
-iw8 = int8ToWord8#
+iw8 = \ x -> int8ToWord8# x
 
-iw16 = int16ToWord16#
+iw16 = \ x -> int16ToWord16# x
 
-iw32 = int32ToWord32#
+iw32 = \ x -> int32ToWord32# x
 
 iw64 = \ x -> wordToWord64# (int2Word# (int64ToInt# x))
 
@@ -43,9 +43,9 @@ wiw64 = \ x -> x
 
 iwi64 = \ x -> x
 
-ww64i = word2Int#
+ww64i = \ x -> word2Int# x
 
-ii64w = int2Word#
+ii64w = \ x -> int2Word# x
 
 
 
diff --git a/testsuite/tests/numeric/should_compile/T19769.stderr-ws-64 b/testsuite/tests/numeric/should_compile/T19769.stderr-ws-64
index c5620bbf4b..99793137a2 100644
--- a/testsuite/tests/numeric/should_compile/T19769.stderr-ws-64
+++ b/testsuite/tests/numeric/should_compile/T19769.stderr-ws-64
@@ -1,23 +1,23 @@
 
 ==================== Tidy Core ====================
 Result size of Tidy Core
-  = {terms: 54, types: 54, coercions: 0, joins: 0/0}
+  = {terms: 74, types: 64, coercions: 0, joins: 0/0}
 
-wi8 = word8ToInt8#
+wi8 = \ x -> word8ToInt8# x
 
-wi16 = word16ToInt16#
+wi16 = \ x -> word16ToInt16# x
 
-wi32 = word32ToInt32#
+wi32 = \ x -> word32ToInt32# x
 
-wi64 = word64ToInt64#
+wi64 = \ x -> word64ToInt64# x
 
-iw8 = int8ToWord8#
+iw8 = \ x -> int8ToWord8# x
 
-iw16 = int16ToWord16#
+iw16 = \ x -> int16ToWord16# x
 
-iw32 = int32ToWord32#
+iw32 = \ x -> int32ToWord32# x
 
-iw64 = int64ToWord64#
+iw64 = \ x -> int64ToWord64# x
 
 i8 = \ x -> x
 
@@ -43,9 +43,9 @@ wiw64 = w64
 
 iwi64 = i64
 
-ww64i = word2Int#
+ww64i = \ x -> word2Int# x
 
-ii64w = int2Word#
+ii64w = \ x -> int2Word# x
 
 
 
diff --git a/testsuite/tests/numeric/should_compile/T20347.stderr b/testsuite/tests/numeric/should_compile/T20347.stderr
index e4e80ada00..6fcb0b0722 100644
--- a/testsuite/tests/numeric/should_compile/T20347.stderr
+++ b/testsuite/tests/numeric/should_compile/T20347.stderr
@@ -1,7 +1,7 @@
 
 ==================== Tidy Core ====================
 Result size of Tidy Core
-  = {terms: 20, types: 15, coercions: 0, joins: 0/0}
+  = {terms: 24, types: 17, coercions: 0, joins: 0/0}
 
 foo0 = \ x -> -# 10# x
 
@@ -9,7 +9,7 @@ foo1 = \ _ -> 10#
 
 foo2 = \ x -> +# 10# x
 
-foo3 = *#
+foo3 = \ x y -> *# x y
 
 foo4 = \ x -> *# -10# x
 
diff --git a/testsuite/tests/primops/should_compile/KeepAliveWrapper.hs b/testsuite/tests/primops/should_compile/KeepAliveWrapper.hs
new file mode 100644
index 0000000000..504af81bf7
--- /dev/null
+++ b/testsuite/tests/primops/should_compile/KeepAliveWrapper.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE MagicHash #-}
+
+module KeepAliveWrapper where
+
+import GHC.Exts ( State#, RealWorld, keepAlive# )
+
+keepAliveWrapper :: v -> State# RealWorld -> (State# (RealWorld) -> p) -> p
+keepAliveWrapper a1 a2 a3 = keepAlive# a1 a2 a3
diff --git a/testsuite/tests/primops/should_compile/all.T b/testsuite/tests/primops/should_compile/all.T
index 023eeaedce..5b4dcd82df 100644
--- a/testsuite/tests/primops/should_compile/all.T
+++ b/testsuite/tests/primops/should_compile/all.T
@@ -3,4 +3,5 @@ test('T16293a', normal, compile, [''])
 test('T19851', normal, compile, ['-O'])
 test('LevPolyPtrEquality3', normal, compile, [''])
 test('UnliftedMutVar_Comp', normal, compile, [''])
-test('UnliftedStableName', normal, compile, [''])
\ No newline at end of file
+test('UnliftedStableName', normal, compile, [''])
+test('KeepAliveWrapper', normal, compile, ['-O'])
diff --git a/testsuite/tests/stranal/should_compile/T18122.stderr b/testsuite/tests/stranal/should_compile/T18122.stderr
index f94751fb55..8fe91fc57a 100644
--- a/testsuite/tests/stranal/should_compile/T18122.stderr
+++ b/testsuite/tests/stranal/should_compile/T18122.stderr
@@ -1,7 +1,7 @@
 
 ==================== Tidy Core ====================
 Result size of Tidy Core
-  = {terms: 35, types: 27, coercions: 0, joins: 0/0}
+  = {terms: 39, types: 29, coercions: 0, joins: 0/0}
 
 -- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
 Lib.$trModule4 :: GHC.Prim.Addr#
@@ -38,40 +38,42 @@ Lib.$trModule :: GHC.Types.Module
          WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
 Lib.$trModule = GHC.Types.Module Lib.$trModule3 Lib.$trModule1
 
--- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 5, types: 2, coercions: 0, joins: 0/0}
 Lib.$wfoo [InlPrag=NOINLINE]
   :: GHC.Prim.Int# -> GHC.Prim.Int# -> GHC.Prim.Int#
-[GblId, Arity=2, Str=<L,U><L,U>, Unf=OtherCon []]
-Lib.$wfoo = GHC.Prim.+#
+[GblId, Arity=2, Str=<L><L>, Unf=OtherCon []]
+Lib.$wfoo
+  = \ (ww_sF3 :: GHC.Prim.Int#) (ww1_sF9 :: GHC.Prim.Int#) ->
+      GHC.Prim.+# ww_sF3 ww1_sF9
 
 -- RHS size: {terms: 18, types: 14, coercions: 0, joins: 0/0}
-foo [InlPrag=NOUSERINLINE[final]] :: (Int, Int) -> Int -> Int
+foo [InlPrag=[final]] :: (Int, Int) -> Int -> Int
 [GblId,
  Arity=2,
- Str=<S(SL),1*U(1*U(U),A)><S,1*U(U)>,
- Cpr=m1,
+ Str=<1!P(1!L,A)><1!L>,
+ Cpr=1,
  Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
          WorkFree=True, Expandable=True,
          Guidance=ALWAYS_IF(arity=2,unsat_ok=True,boring_ok=False)
-         Tmpl= \ (w_sEf [Occ=Once1!] :: (Int, Int))
-                 (w1_sEg [Occ=Once1!] :: Int) ->
-                 case w_sEf of { (ww1_sEj [Occ=Once1!], _ [Occ=Dead]) ->
-                 case ww1_sEj of { GHC.Types.I# ww4_sEm [Occ=Once1] ->
-                 case w1_sEg of { GHC.Types.I# ww6_sEs [Occ=Once1] ->
-                 case Lib.$wfoo ww4_sEm ww6_sEs of ww7_sEw [Occ=Once1]
+         Tmpl= \ (ds_sEZ [Occ=Once1!] :: (Int, Int))
+                 (z_sF7 [Occ=Once1!] :: Int) ->
+                 case ds_sEZ of { (ww_sF1 [Occ=Once1!], _ [Occ=Dead]) ->
+                 case ww_sF1 of { GHC.Types.I# ww2_sF3 [Occ=Once1] ->
+                 case z_sF7 of { GHC.Types.I# ww3_sF9 [Occ=Once1] ->
+                 case Lib.$wfoo ww2_sF3 ww3_sF9 of ww4_sFe [Occ=Once1]
                  { __DEFAULT ->
-                 GHC.Types.I# ww7_sEw
+                 GHC.Types.I# ww4_sFe
                  }
                  }
                  }
                  }}]
 foo
-  = \ (w_sEf :: (Int, Int)) (w1_sEg :: Int) ->
-      case w_sEf of { (ww1_sEj, ww2_sEo) ->
-      case ww1_sEj of { GHC.Types.I# ww4_sEm ->
-      case w1_sEg of { GHC.Types.I# ww6_sEs ->
-      case Lib.$wfoo ww4_sEm ww6_sEs of ww7_sEw { __DEFAULT ->
-      GHC.Types.I# ww7_sEw
+  = \ (ds_sEZ :: (Int, Int)) (z_sF7 :: Int) ->
+      case ds_sEZ of { (ww_sF1, ww1_sF5) ->
+      case ww_sF1 of { GHC.Types.I# ww2_sF3 ->
+      case z_sF7 of { GHC.Types.I# ww3_sF9 ->
+      case Lib.$wfoo ww2_sF3 ww3_sF9 of ww4_sFe { __DEFAULT ->
+      GHC.Types.I# ww4_sFe
       }
       }
       }
diff --git a/utils/genprimopcode/Main.hs b/utils/genprimopcode/Main.hs
index 2e0886e59b..a3bdfc8fd7 100644
--- a/utils/genprimopcode/Main.hs
+++ b/utils/genprimopcode/Main.hs
@@ -502,8 +502,10 @@ gen_latex_doc (Info defaults entries)
                    foralls = if tvars == [] then "" else "%forall " ++ (tbinds tvars)
                    tvars = tvars_of typ
                    tbinds [] = ". "
-                   tbinds ("o":tbs) = "(o::?) " ++ (tbinds tbs)
-                   tbinds ("p":tbs) = "(p::?) " ++ (tbinds tbs)
+                   tbinds ("o":tbs) = "(o::TYPE q) " ++ (tbinds tbs)
+                   tbinds ("p":tbs) = "(p::TYPE r) " ++ (tbinds tbs)
+                   tbinds ("v":tbs) = "(v::TYPE (BoxedRep l)) " ++ (tbinds tbs)
+                   tbinds ("w":tbs) = "(w::TYPE (BoxedRep k)) " ++ (tbinds tbs)
                    tbinds (tv:tbs) = tv ++ " " ++ (tbinds tbs)
            tvars_of (TyF t1 t2) = tvars_of t1 `union` tvars_of t2
            tvars_of (TyC t1 t2) = tvars_of t1 `union` tvars_of t2
@@ -639,12 +641,14 @@ gen_wrappers (Info _ entries)
         f spec = let args = map (\n -> "a" ++ show n) [1 .. arity (ty spec)]
                      src_name = wrap (name spec)
                      lhs = src_name ++ " " ++ unwords args
-                     rhs = "(GHC.Prim." ++ name spec ++ ") " ++ unwords args
+                     rhs = wrapQual (name spec) ++ " " ++ unwords args
                  in ["{-# NOINLINE " ++ src_name ++ " #-}",
                      src_name ++ " :: " ++ pprTy (ty spec),
                      lhs ++ " = " ++ rhs]
         wrap nm | isLower (head nm) = nm
                 | otherwise = "(" ++ nm ++ ")"
+        wrapQual nm | isLower (head nm) = "GHC.Prim." ++ nm
+                    | otherwise         = "(GHC.Prim." ++ nm ++ ")"
 
         dodgy spec
            = name spec `elem`
@@ -837,25 +841,74 @@ mkPOI_RHS_text i
                  _ -> error "Type error in comparison op"
         GenPrimOp
            -> let (argTys, resTy) = flatTys (ty i)
-                  tvs = nub (tvsIn (ty i))
+                  tvs = tvsIn (ty i)
+                  (infBndrs,bndrs) = ppTyVarBinders tvs
               in
                   "mkGenPrimOp " ++ sl_name i ++ " "
-                      ++ listify (map ppTyVar tvs) ++ " "
+                      ++ listify (infBndrs ++ bndrs) ++ " "
                       ++ listify (map ppType argTys) ++ " "
                       ++ "(" ++ ppType resTy ++ ")"
 
 sl_name :: Entry -> String
 sl_name i = "(fsLit \"" ++ name i ++ "\") "
 
-ppTyVar :: String -> String
-ppTyVar "a" = "alphaTyVarSpec"
-ppTyVar "b" = "betaTyVarSpec"
-ppTyVar "c" = "gammaTyVarSpec"
-ppTyVar "s" = "deltaTyVarSpec"
-ppTyVar "o" = "runtimeRep1TyVarInf, openAlphaTyVarSpec"
-ppTyVar "p" = "runtimeRep2TyVarInf, openBetaTyVarSpec"
-ppTyVar "v" = "levity1TyVarInf, levPolyAlphaTyVarSpec"
-ppTyVar "w" = "levity2TyVarInf, levPolyBetaTyVarSpec"
+
+-- | A 'PrimOpTyVarBndr' specifies the textual name of a built-in 'TyVarBinder'
+-- (usually from "GHC.Builtin.Types.Prim"), in the 'primOpTyVarBinder' field.
+--
+-- The kind of the type variable stored in the 'primOpTyVarBinder' field
+-- might also depend on some other type variables, for example in
+-- @a :: TYPE r@, the kind of @a@ depends on @r@.
+--
+-- Invariant: if the kind of the type variable stored in the 'primOpTyyVarBinder'
+-- field depends on other type variables, such variables must be inferred type variables
+-- and they must be stored in the associated 'inferredTyVarBinders' field.
+data PrimOpTyVarBinder
+   = PrimOpTyVarBinder
+   { inferredTyVarBinders :: [TyVarBinder]
+   , primOpTyVarBinder    :: TyVarBinder }
+
+nonDepTyVarBinder :: TyVarBinder -> PrimOpTyVarBinder
+nonDepTyVarBinder bndr
+  = PrimOpTyVarBinder
+    { inferredTyVarBinders = []
+    , primOpTyVarBinder    = bndr }
+
+-- | Pretty-print a collection of type variables,
+-- putting all the inferred type variables first,
+-- and removing any duplicate type variables.
+--
+-- This assumes that such a re-ordering makes sense: the kinds of the inferred
+-- type variables may not depend on any of the other type variables.
+ppTyVarBinders :: [TyVar] -> ([TyVarBinder], [TyVarBinder])
+ppTyVarBinders names = case go names of { (infs, bndrs) -> (nub infs, nub bndrs) }
+  where
+     go [] = ([], [])
+     go (tv:tvs)
+       | PrimOpTyVarBinder
+          { inferredTyVarBinders = infs
+          , primOpTyVarBinder    = bndr }
+            <- ppTyVar tv
+       , (other_infs, bndrs) <- ppTyVarBinders tvs
+       = (infs ++ other_infs, bndr : bndrs)
+
+ppTyVar :: TyVar -> PrimOpTyVarBinder
+ppTyVar "a" = nonDepTyVarBinder "alphaTyVarSpec"
+ppTyVar "b" = nonDepTyVarBinder "betaTyVarSpec"
+ppTyVar "c" = nonDepTyVarBinder "gammaTyVarSpec"
+ppTyVar "s" = nonDepTyVarBinder "deltaTyVarSpec"
+ppTyVar "o" = PrimOpTyVarBinder
+              { inferredTyVarBinders = ["runtimeRep1TyVarInf"]
+              , primOpTyVarBinder    = "openAlphaTyVarSpec" }
+ppTyVar "p" = PrimOpTyVarBinder
+              { inferredTyVarBinders = ["runtimeRep2TyVarInf"]
+              , primOpTyVarBinder    = "openBetaTyVarSpec" }
+ppTyVar "v" = PrimOpTyVarBinder
+              { inferredTyVarBinders = ["levity1TyVarInf"]
+              , primOpTyVarBinder    = "levPolyAlphaTyVarSpec" }
+ppTyVar "w" = PrimOpTyVarBinder
+              { inferredTyVarBinders = ["levity2TyVarInf"]
+              , primOpTyVarBinder    = "levPolyBetaTyVarSpec" }
 ppTyVar _   = error "Unknown type var"
 -- o, p, v and w have a special meaning. See primops.txt.pp
 -- Note [Levity and representation polymorphic primops]
diff --git a/utils/genprimopcode/Syntax.hs b/utils/genprimopcode/Syntax.hs
index e215a89478..947c6f0392 100644
--- a/utils/genprimopcode/Syntax.hs
+++ b/utils/genprimopcode/Syntax.hs
@@ -74,11 +74,12 @@ data Ty
    | TyC    Ty Ty -- We only allow one constraint, keeps the grammar simpler
    | TyApp  TyCon [Ty]
    | TyVar  TyVar
-   | TyUTup [Ty]   -- unboxed tuples; just a TyCon really, 
+   | TyUTup [Ty]   -- unboxed tuples; just a TyCon really,
                    -- but convenient like this
    deriving (Eq,Show)
 
 type TyVar = String
+type TyVarBinder = String
 
 data TyCon = TyCon String
            | SCALAR
@@ -115,9 +116,9 @@ data SourceText = SourceText String
 {- Do some simple sanity checks:
     * all the default field names are unique
     * for each PrimOpSpec, all override field names are unique
-    * for each PrimOpSpec, all overridden field names   
+    * for each PrimOpSpec, all overridden field names
           have a corresponding default value
-    * that primop types correspond in certain ways to the 
+    * that primop types correspond in certain ways to the
       Category: eg if Comparison, the type must be of the form
          T -> T -> Bool.
    Dies with "error" if there's a problem, else returns ().
@@ -153,7 +154,7 @@ sanityPrimOp def_names p
          else ()
 
 sane_ty :: Category -> Ty -> Bool
-sane_ty Compare (TyF t1 (TyF t2 td)) 
+sane_ty Compare (TyF t1 (TyF t2 td))
    | t1 == t2 && td == TyApp (TyCon "Int#") []  = True
 sane_ty GenPrimOp _
    = True
@@ -170,7 +171,7 @@ get_attrib_name (OptionFixity _) = "fixity"
 
 lookup_attrib :: String -> [Option] -> Maybe Option
 lookup_attrib _ [] = Nothing
-lookup_attrib nm (a:as) 
+lookup_attrib nm (a:as)
     = if get_attrib_name a == nm then Just a else lookup_attrib nm as
 
 is_vector :: Entry -> Bool