Clone the binders of a SAKS where necessarywip/T19093

Given a kind signature

   type T :: forall k. k -> forall k. k -> blah
   data T a b = ...

where those k's have the same unique (which is possible;
see #19093) we were giving the tyConBinders in tycon T the same
unique, which caused chaos.

Fix is simple: ensure uniqueness when decomposing the kind signature.
See GHC.Tc.Gen.HsType.zipBinders

7 files changed, 117 insertions, 28 deletions

diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs
index bc6632f1bf..7ea61bdae2 100644
--- a/compiler/GHC/Core/TyCo/Subst.hs
+++ b/compiler/GHC/Core/TyCo/Subst.hs
@@ -46,6 +46,7 @@ module GHC.Core.TyCo.Subst
         substTyVarBndr, substTyVarBndrs,
         substCoVarBndr,
         substTyVar, substTyVars, substTyCoVars,
+        substTyCoBndr,
         substForAllCoBndr,
         substVarBndrUsing, substForAllCoBndrUsing,
         checkValidSubst, isValidTCvSubst,
@@ -1054,3 +1055,10 @@ cloneTyVarBndrs subst (t:ts)  usupply = (subst'', tv:tvs)
     (uniq, usupply') = takeUniqFromSupply usupply
     (subst' , tv )   = cloneTyVarBndr subst t uniq
     (subst'', tvs)   = cloneTyVarBndrs subst' ts usupply'
+
+substTyCoBndr :: TCvSubst -> TyCoBinder -> (TCvSubst, TyCoBinder)
+substTyCoBndr subst (Anon af ty)          = (subst, Anon af (substScaledTy subst ty))
+substTyCoBndr subst (Named (Bndr tv vis)) = (subst', Named (Bndr tv' vis))
+                                          where
+                                            (subst', tv') = substVarBndr subst tv
+
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index e5d0da93fd..af92b92e52 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -212,6 +212,7 @@ module GHC.Core.Type (
         substCoUnchecked, substCoWithUnchecked,
         substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars,
         substVarBndr, substVarBndrs,
+        substTyCoBndr,
         cloneTyVarBndr, cloneTyVarBndrs, lookupTyVar,
 
         -- * Tidying type related things up for printing
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index ecd4e82304..ac6c95d954 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -2438,7 +2438,7 @@ kcCheckDeclHeader_sig kisig name flav
                      --               ^^^^^^^^^
                      -- We do it here because at this point the environment has been
                      -- extended with both 'implicit_tcv_prs' and 'explicit_tv_prs'.
-                   ; ctx_k <- kc_res_ki
+                   ; ctx_k    <- kc_res_ki
                    ; m_res_ki <- case ctx_k of
                                   AnyKind -> return Nothing
                                   _ -> Just <$> newExpectedKind ctx_k
@@ -2466,12 +2466,12 @@ kcCheckDeclHeader_sig kisig name flav
 
                    ; return (invis_binders, r_ki) }
 
-        -- Zonk the implicitly quantified variables.
-        ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs
-
         -- Convert each invisible TyCoBinder to TyConBinder for tyConBinders.
         ; invis_tcbs <- mapM invis_to_tcb invis_binders
 
+        -- Zonk the implicitly quantified variables.
+        ; implicit_tvs <- mapM zonkTcTyVarToTyVar implicit_tvs
+
         -- Build the final, generalized TcTyCon
         ; let tcbs            = vis_tcbs ++ invis_tcbs
               implicit_tv_prs = implicit_nms `zip` implicit_tvs
@@ -2589,34 +2589,34 @@ kcCheckDeclHeader_sig kisig name flav
       in splitInvisPiTysN n_inst sig_ki
 
 -- A quantifier from a kind signature zipped with a user-written binder for it.
-data ZippedBinder =
-  ZippedBinder TyBinder (Maybe (LHsTyVarBndr () GhcRn))
+data ZippedBinder = ZippedBinder TyBinder (Maybe (LHsTyVarBndr () GhcRn))
 
 -- See Note [Arity inference in kcCheckDeclHeader_sig]
 zipBinders
-  :: Kind                      -- kind signature
-  -> [LHsTyVarBndr () GhcRn]   -- user-written binders
-  -> ([ZippedBinder],          -- zipped binders
-      [LHsTyVarBndr () GhcRn], -- remaining user-written binders
-      Kind)                    -- remainder of the kind signature
-zipBinders = zip_binders []
+  :: Kind                      -- Kind signature
+  -> [LHsTyVarBndr () GhcRn]   -- User-written binders
+  -> ( [ZippedBinder]          -- Zipped binders
+     , [LHsTyVarBndr () GhcRn] -- Leftover user-written binders
+     , Kind )                  -- Remainder of the kind signature
+zipBinders = zip_binders [] emptyTCvSubst
   where
-    zip_binders acc ki [] = (reverse acc, [], ki)
-    zip_binders acc ki (b:bs) =
-      case tcSplitPiTy_maybe ki of
-        Nothing -> (reverse acc, b:bs, ki)
-        Just (tb, ki') ->
-          let
-            (zb, bs') | zippable  = (ZippedBinder tb (Just b),  bs)
-                      | otherwise = (ZippedBinder tb Nothing, b:bs)
-            zippable =
-              case tb of
-                Named (Bndr _ (Invisible _)) -> False
-                Named (Bndr _ Required)      -> True
-                Anon InvisArg _ -> False
-                Anon VisArg   _ -> True
-          in
-            zip_binders (zb:acc) ki' bs'
+    -- subst: we substitute as we go, to ensure that the resulting
+    -- binders in the [ZippedBndr] all have distinct uniques.
+    -- If not, the TyCon may get multiple binders with the same unique,
+    -- which results in chaos (see #19092,3,4)
+    -- (The incoming kind might be forall k. k -> forall k. k -> Type
+    --  where those two k's have the same unique. Without the substitution
+    --  we'd get a repeated 'k'.)
+    zip_binders acc subst ki bs
+      | (b:bs') <- bs  -- Stop as soon as 'bs' becomes empty
+      , Just (tb,ki') <- tcSplitPiTy_maybe ki
+      , let (subst', tb') = substTyCoBndr subst tb
+      = if isInvisibleBinder tb
+        then zip_binders (ZippedBinder tb' Nothing  : acc) subst' ki' bs
+        else zip_binders (ZippedBinder tb' (Just b) : acc) subst' ki' bs'
+
+      | otherwise
+      = (reverse acc, bs, substTy subst ki)
 
 tooManyBindersErr :: Kind -> [LHsTyVarBndr () GhcRn] -> SDoc
 tooManyBindersErr ki bndrs =
diff --git a/testsuite/tests/polykinds/T19092.hs b/testsuite/tests/polykinds/T19092.hs
new file mode 100644
index 0000000000..d63db880ea
--- /dev/null
+++ b/testsuite/tests/polykinds/T19092.hs
@@ -0,0 +1,29 @@
+{-# Language RankNTypes, TypeApplications, PolyKinds, DataKinds, TypeOperators, StandaloneKindSignatures, TypeFamilies, FlexibleInstances, MultiParamTypeClasses #-}
+
+module T19092 where
+
+import Data.Type.Equality
+import Data.Kind
+
+type PolyKinded :: Type -> Type
+type PolyKinded res = (forall (k :: Type). k -> res)
+
+infix 4
+ ===
+type
+ (===) :: PolyKinded (PolyKinded Bool)
+type family
+ a === b where
+ a === a = True
+ _ === _ = False
+
+type  TryUnify :: Bool -> forall k. k -> forall j. j -> Constraint
+class (a === b) ~ cond
+   => TryUnify cond a b
+instance (a === b) ~ False
+      => TryUnify False @k a @j b
+instance {-# Incoherent #-}
+         ( (a === b) ~ True
+         , a ~~ b
+         )
+      => TryUnify True @k a @j b
diff --git a/testsuite/tests/polykinds/T19093.hs b/testsuite/tests/polykinds/T19093.hs
new file mode 100644
index 0000000000..4e322e1108
--- /dev/null
+++ b/testsuite/tests/polykinds/T19093.hs
@@ -0,0 +1,19 @@
+{-# Language RankNTypes, TypeApplications, PolyKinds, DataKinds,
+             TypeOperators, StandaloneKindSignatures, TypeFamilies,
+             FlexibleInstances, MultiParamTypeClasses #-}
+
+module T19093 where
+
+import Data.Proxy
+import Data.Type.Equality
+import Data.Kind
+
+type PolyKinded :: Type -> Type
+type PolyKinded res = (forall (k :: Type). k -> res)
+
+
+type  TryUnify :: PolyKinded (PolyKinded Constraint)
+-- type TryUnify :: Bool -> forall k. k -> forall k. k -> Constraint
+-- type TryUnify :: Bool -> PolyKinded (forall k. k -> Constraint)
+
+class TryUnify a b where
diff --git a/testsuite/tests/polykinds/T19094.hs b/testsuite/tests/polykinds/T19094.hs
new file mode 100644
index 0000000000..7b2b03e713
--- /dev/null
+++ b/testsuite/tests/polykinds/T19094.hs
@@ -0,0 +1,29 @@
+{-# Language RankNTypes, TypeApplications, PolyKinds, DataKinds, TypeOperators, StandaloneKindSignatures, TypeFamilies, FlexibleInstances, MultiParamTypeClasses #-}
+
+module T19094 where
+
+import Data.Type.Equality
+import Data.Kind
+
+type PolyKinded :: Type -> Type
+type PolyKinded res = (forall (k :: Type). k -> res)
+
+infix 4
+ ===
+type
+ (===) :: PolyKinded (PolyKinded Bool)
+type family
+ a === b where
+ a === a = True
+ _ === _ = False
+
+type  TryUnify :: Bool -> PolyKinded (PolyKinded Constraint)
+class (a === b) ~ cond
+   => TryUnify cond a b
+instance (a === b) ~ False
+      => TryUnify False @k a @j b
+instance {-# Incoherent #-}
+         ( (a === b) ~ True
+         , a ~~ b
+         )
+      => TryUnify True @k a @j b
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 35d4df559d..52529f882a 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -230,3 +230,6 @@ test('T18451a', normal, compile_fail, [''])
 test('T18451b', normal, compile_fail, [''])
 test('T18522-ppr', normal, ghci_script, ['T18522-ppr.script'])
 test('T18855', normal, compile, [''])
+test('T19092', normal, compile, [''])
+test('T19093', normal, compile, [''])
+test('T19094', normal, compile, [''])