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.

1 files changed, 39 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