tidyOccNames: Rename variables fairlywip/T12382

So that
> :t (id,id,id)
produces
(id,id,id) :: (a3 -> a3, a2 -> a2, a1 -> a1)
instead of
(id,id,id) :: (a2 -> a2, a1 -> a1, a -> a)

12 files changed, 78 insertions, 25 deletions

diff --git a/compiler/basicTypes/OccName.hs b/compiler/basicTypes/OccName.hs
index c17bd06a4f..8dfeb7f05c 100644
--- a/compiler/basicTypes/OccName.hs
+++ b/compiler/basicTypes/OccName.hs
@@ -98,7 +98,9 @@ module OccName (
         filterOccSet,
 
         -- * Tidying up
-        TidyOccEnv, emptyTidyOccEnv, tidyOccNames, tidyOccName, initTidyOccEnv,
+        TidyOccEnv, emptyTidyOccEnv, initTidyOccEnv,
+        tidyOccName,
+        tidyOccNames, avoidClashesOccEnv,
 
         -- FsEnv
         FastStringEnv, emptyFsEnv, lookupFsEnv, extendFsEnv, mkFsEnv
@@ -810,6 +812,36 @@ So we use the TidyOccEnv mapping for "a" (not "a7" or "a8") as our base for
 starting the search; and we make sure to update the starting point for "a"
 after we allocate a new one.
 
+
+Node [Tidying multiple names at once]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Consider
+
+    > :t (id,id,id)
+
+Every id contributes a type variable to the type signature, and all of them are
+"a". If we tidy them one by one, we get
+
+    (id,id,id) :: (a2 -> a2, a1 -> a1, a -> a)
+
+which is a bit unfortunate, as it unfairly renames only one of them. What we
+would like to see is
+
+    (id,id,id) :: (a3 -> a3, a2 -> a2, a1 -> a1)
+
+This is achieved in tidyOccNames. It still uses tidyOccName to rename each name
+on its own, but it prepares the TidyEnv (using avoidClashesOccEnv), by “blocking” every
+name that occurs twice in the map. This way, none of the "a"s will get the
+priviledge of keeping this name, and all of them will get a suitable numbery by
+tidyOccName.
+
+It may be inappropriate to use tidyOccNames if the caller needs access to the
+intermediate environments (e.g. to tidy the tyVarKind of a type variable). In that
+case, avoidClashesOccEnv should be used directly, and tidyOccName afterwards.
+
+This is #12382.
+
 -}
 
 type TidyOccEnv = UniqFM Int    -- The in-scope OccNames
@@ -823,16 +855,29 @@ initTidyOccEnv = foldl add emptyUFM
   where
     add env (OccName _ fs) = addToUFM env fs 1
 
+-- see Note [Tidying multiple names at once]
 tidyOccNames :: TidyOccEnv -> [OccName] -> (TidyOccEnv, [OccName])
-tidyOccNames env occs = mapAccumL tidyOccName env occs
+tidyOccNames env occs = mapAccumL tidyOccName env' occs
+  where
+    env' = avoidClashesOccEnv env occs
+
+avoidClashesOccEnv :: TidyOccEnv -> [OccName] -> TidyOccEnv
+avoidClashesOccEnv env occs = go env emptyUFM occs
+  where
+    go env _        [] = env
+    go env seenOnce ((OccName _ fs):occs)
+      | fs `elemUFM` env      = go env seenOnce                  occs
+      | fs `elemUFM` seenOnce = go (addToUFM env fs 1) seenOnce  occs
+      | otherwise             = go env (addToUFM seenOnce fs ()) occs
 
 tidyOccName :: TidyOccEnv -> OccName -> (TidyOccEnv, OccName)
 tidyOccName env occ@(OccName occ_sp fs)
-  = case lookupUFM env fs of
-      Nothing -> (addToUFM env fs 1, occ)   -- Desired OccName is free
-      Just {} -> case lookupUFM env base1 of
-                   Nothing -> (addToUFM env base1 2, OccName occ_sp base1)
-                   Just n  -> find 1 n
+  | not (fs `elemUFM` env)
+  = (addToUFM env fs 1, occ)   -- Desired OccName is free
+  | otherwise
+  = case lookupUFM env base1 of
+       Nothing -> (addToUFM env base1 2, OccName occ_sp base1)
+       Just n  -> find 1 n
   where
     base :: String  -- Drop trailing digits (see Note [TidyOccEnv])
     base  = dropWhileEndLE isDigit (unpackFS fs)
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index ab07f33d8c..3d9d73d061 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -3104,7 +3104,15 @@ ppSuggestExplicitKinds
 --
 -- It doesn't change the uniques at all, just the print names.
 tidyTyCoVarBndrs :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
-tidyTyCoVarBndrs tidy_env tvs = mapAccumL tidyTyCoVarBndr tidy_env tvs
+tidyTyCoVarBndrs (occ_env, subst) tvs
+    = mapAccumL tidyTyCoVarBndr tidy_env' tvs
+  where
+    -- Seed the occ_env with clashes among the names, see
+    -- Node [Tidying multiple names at once] in OccName
+    -- Se still go through tidyTyCoVarBndr so that each kind variable is tidied
+    -- with the correct tidy_env
+    occs = map getHelpfulOccName tvs
+    tidy_env' = (avoidClashesOccEnv occ_env occs, subst)
 
 tidyTyCoVarBndr :: TidyEnv -> TyCoVar -> (TidyEnv, TyCoVar)
 tidyTyCoVarBndr tidy_env@(occ_env, subst) tyvar
diff --git a/testsuite/tests/ado/ado004.stderr b/testsuite/tests/ado/ado004.stderr
index ec2ebbc50d..20f04d01e7 100644
--- a/testsuite/tests/ado/ado004.stderr
+++ b/testsuite/tests/ado/ado004.stderr
@@ -18,17 +18,17 @@ TYPE SIGNATURES
     (Num b, Num t, Functor f) =>
     (t -> f b) -> f b
   test3 ::
-    forall a t (m :: * -> *) t1.
-    (Num t1, Monad m) =>
-    (t1 -> m t) -> (t -> t -> m a) -> m a
+    forall a t1 (m :: * -> *) t2.
+    (Num t2, Monad m) =>
+    (t2 -> m t1) -> (t1 -> t1 -> m a) -> m a
   test4 ::
-    forall a a1 (m :: * -> *) t.
+    forall a1 a2 (m :: * -> *) t.
     (Num t, Monad m) =>
-    (t -> m a1) -> (a1 -> a1 -> m a) -> m a
+    (t -> m a2) -> (a2 -> a2 -> m a1) -> m a1
   test5 ::
-    forall a a1 (m :: * -> *) t.
+    forall a1 a2 (m :: * -> *) t.
     (Num t, Monad m) =>
-    (t -> m a1) -> (a1 -> a1 -> m a) -> m a
+    (t -> m a2) -> (a2 -> a2 -> m a1) -> m a1
   test6 ::
     forall a (m :: * -> *) t.
     (Num (m a), Monad m) =>
diff --git a/testsuite/tests/driver/werror.stderr b/testsuite/tests/driver/werror.stderr
index ae18bb62f0..67c8112ee3 100644
--- a/testsuite/tests/driver/werror.stderr
+++ b/testsuite/tests/driver/werror.stderr
@@ -18,7 +18,7 @@ werror.hs:10:1: warning: [-Wunused-top-binds (in -Wextra, -Wunused-binds)]
 
 werror.hs:10:1: warning: [-Wmissing-signatures (in -Wall)]
     Top-level binding with no type signature:
-      f :: forall a a1. [a1] -> [a]
+      f :: forall a1 a2. [a2] -> [a1]
 
 werror.hs:10:1: warning: [-Wincomplete-patterns (in -Wextra)]
     Pattern match(es) are non-exhaustive
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index 048f45d288..9184aff580 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -49,7 +49,7 @@
 
 <interactive>:60:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Kind variable ‘k2’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       PolyKindVars '[] = '[] -- Defined at <interactive>:60:15
diff --git a/testsuite/tests/ghci/scripts/T7587.stdout b/testsuite/tests/ghci/scripts/T7587.stdout
index 776eb6d223..95e68c0d3f 100644
--- a/testsuite/tests/ghci/scripts/T7587.stdout
+++ b/testsuite/tests/ghci/scripts/T7587.stdout
@@ -1 +1 @@
-A :: k -> k1 -> *
+A :: k1 -> k2 -> *
diff --git a/testsuite/tests/ghci/scripts/T7730.stdout b/testsuite/tests/ghci/scripts/T7730.stdout
index fcf9e4c1d2..e96e909413 100644
--- a/testsuite/tests/ghci/scripts/T7730.stdout
+++ b/testsuite/tests/ghci/scripts/T7730.stdout
@@ -1,7 +1,7 @@
 type role A phantom phantom
 data A (x :: k) (y :: k1)
   	-- Defined at <interactive>:2:1
-A :: k -> k1 -> *
+A :: k1 -> k2 -> *
 type role T phantom
 data T (a :: k) where
   MkT :: forall k (a :: k) a1. a1 -> T a
diff --git a/testsuite/tests/ghci/scripts/ghci013.stdout b/testsuite/tests/ghci/scripts/ghci013.stdout
index 695aaafc53..dacff446f5 100644
--- a/testsuite/tests/ghci/scripts/ghci013.stdout
+++ b/testsuite/tests/ghci/scripts/ghci013.stdout
@@ -1 +1 @@
-f :: Monad m => (m a, b) -> m b1
+f :: Monad m => (m a, b1) -> m b2
diff --git a/testsuite/tests/partial-sigs/should_compile/Uncurry.stderr b/testsuite/tests/partial-sigs/should_compile/Uncurry.stderr
index ce7372f061..f9bcf3a307 100644
--- a/testsuite/tests/partial-sigs/should_compile/Uncurry.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/Uncurry.stderr
@@ -1,5 +1,5 @@
 TYPE SIGNATURES
-  unc :: forall w w1 w2. (w2 -> w1 -> w) -> (w2, w1) -> w
+  unc :: forall w1 w2 w3. (w3 -> w2 -> w1) -> (w3, w2) -> w1
 TYPE CONSTRUCTORS
 COERCION AXIOMS
 Dependent modules: []
diff --git a/testsuite/tests/typecheck/should_compile/tc168.stderr b/testsuite/tests/typecheck/should_compile/tc168.stderr
index 5bcce5b457..121d95f2d2 100644
--- a/testsuite/tests/typecheck/should_compile/tc168.stderr
+++ b/testsuite/tests/typecheck/should_compile/tc168.stderr
@@ -9,4 +9,4 @@ tc168.hs:17:1: error:
     • In the ambiguity check for the inferred type for ‘g’
       To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
       When checking the inferred type
-        g :: forall b a a1. C a1 (a, b) => a1 -> a
+        g :: forall b a1 a2. C a2 (a1, b) => a2 -> a1
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index a8f857237d..11c665ac4f 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -69,7 +69,7 @@ T6018fail.hs:59:10: error:
 
 T6018fail.hs:62:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Kind variable ‘k2’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       PolyKindVars '[] = '[] -- Defined at T6018fail.hs:62:15
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
index 7a0146d7d7..3ceb044591 100644
--- a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
@@ -24,11 +24,11 @@ T6018failclosed.hs:19:5: error:
 
 T6018failclosed.hs:25:5: error:
     • Type family equation violates injectivity annotation.
-      Type and kind variables ‘k1’, ‘b’
+      Type and kind variables ‘k2’, ‘b’
       cannot be inferred from the right-hand side.
       Use -fprint-explicit-kinds to see the kind arguments
       In the type family equation:
-        forall k k1 (c :: k) (b :: k1).
+        forall k1 k2 (c :: k1) (b :: k2).
           JClosed Int b c = Char -- Defined at T6018failclosed.hs:25:5
     • In the equations for closed type family ‘JClosed’
       In the type family declaration for ‘JClosed’