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.

2 files changed, 10 insertions, 5 deletions

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