Clone the binders of a SAKS where necessary

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

4 files changed, 80 insertions, 0 deletions

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, [''])