Fix a nasty bug in the pure unifier

The pure unifier was building an infinite type, through a defective
occurs check.  So GHC went into an infinite loop.

Reason: we were neglecting the 'kco' part of the type, which
'unify_ty' maintains.  Yikes.

The fix is easy.  I refactored a bit to make it harder to
go wrong in future.

3 files changed, 83 insertions, 0 deletions

diff --git a/testsuite/tests/polykinds/T14846.hs b/testsuite/tests/polykinds/T14846.hs
new file mode 100644
index 0000000000..ad17841daa
--- /dev/null
+++ b/testsuite/tests/polykinds/T14846.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeInType #-}
+module T14846 where
+
+import Data.Kind
+import Data.Proxy
+
+type Cat ob = ob -> ob -> Type
+
+data Struct :: (k -> Constraint) -> Type where
+  S :: Proxy (a::k) -> Struct (cls::k -> Constraint)
+
+type Structured a cls = (S ('Proxy :: Proxy a)::Struct cls)
+
+data AStruct :: Struct cls -> Type where
+  AStruct :: cls a => AStruct (Structured a cls)
+
+class StructI xx (structured::Struct (cls :: k -> Constraint)) where
+  struct :: AStruct structured
+
+instance (Structured xx cls ~ structured, cls xx) => StructI xx structured where
+  struct :: AStruct (Structured xx cls)
+  struct = AStruct
+
+data Hom :: Cat k -> Cat (Struct cls) where
+
+class Category (cat::Cat ob) where
+  i :: StructI xx a => ríki a a
+
+instance Category ríki => Category (Hom ríki :: Cat (Struct cls)) where
+  i :: forall xx a. StructI xx a => Hom ríki a a
+  i = case struct :: AStruct (Structured a cls) of
diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr
new file mode 100644
index 0000000000..5e6af2ccd6
--- /dev/null
+++ b/testsuite/tests/polykinds/T14846.stderr
@@ -0,0 +1,43 @@
+
+T14846.hs:38:8: error:
+    • Couldn't match kind ‘cls1’ with ‘cls0’
+      ‘cls1’ is a rigid type variable bound by
+        the type signature for:
+          i :: forall k5 (cls1 :: k5
+                                  -> Constraint) k6 (xx :: k6) (a :: Struct cls1) (ríki1 :: Struct
+                                                                                              cls1
+                                                                                            -> Struct
+                                                                                                 cls1
+                                                                                            -> *).
+               StructI xx a =>
+               ríki1 a a
+        at T14846.hs:38:8-48
+      When matching types
+        a0 :: Struct cls0
+        a :: Struct cls1
+      Expected type: ríki1 a a
+        Actual type: Hom ríki a0 a0
+    • When checking that instance signature for ‘i’
+        is more general than its signature in the class
+        Instance sig: forall (xx :: k0) (a :: Struct cls0).
+                      StructI xx a =>
+                      Hom ríki a a
+           Class sig: forall k1 (cls :: k1
+                                        -> Constraint) k2 (xx :: k2) (a :: Struct
+                                                                             cls) (ríki :: Struct
+                                                                                             cls
+                                                                                           -> Struct
+                                                                                                cls
+                                                                                           -> *).
+                      StructI xx a =>
+                      ríki a a
+      In the instance declaration for ‘Category (Hom ríki)’
+
+T14846.hs:39:44: error:
+    • Expected kind ‘Struct cls0 -> Constraint’,
+        but ‘cls’ has kind ‘k4 -> Constraint’
+    • In the second argument of ‘Structured’, namely ‘cls’
+      In the first argument of ‘AStruct’, namely ‘(Structured a cls)’
+      In an expression type signature: AStruct (Structured a cls)
+    • Relevant bindings include
+        i :: Hom ríki a a (bound at T14846.hs:39:3)
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 79991a2cef..36eb07be07 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -184,4 +184,5 @@ test('T14561', normal, compile_fail, [''])
 test('T14580', normal, compile_fail, [''])
 test('T14515', normal, compile, [''])
 test('T14723', normal, compile, [''])
+test('T14846', normal, compile_fail, [''])