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.

4 files changed, 116 insertions, 26 deletions

diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs
index 2c9762c57a..e59c4ce125 100644
--- a/compiler/types/Unify.hs
+++ b/compiler/types/Unify.hs
@@ -1047,11 +1047,9 @@ uUnrefined env tv1 ty2 ty2' kco
              b2  = tvBindFlagR env tv2
              ty1 = mkTyVarTy tv1
        ; case (b1, b2) of
-           (BindMe, _) -> do { checkRnEnvR env ty2 -- make sure ty2 is not a local
-                             ; extendTvEnv tv1 (ty2 `mkCastTy` mkSymCo kco) }
+           (BindMe, _) -> bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco)
            (_, BindMe) | um_unif env
-                       -> do { checkRnEnvL env ty1 -- ditto for ty1
-                             ; extendTvEnv tv2 (ty1 `mkCastTy` kco) }
+                       -> bindTv (umSwapRn env) tv2 (ty1 `mkCastTy` kco)
 
            _ | tv1' == tv2' -> return ()
              -- How could this happen? If we're only matching and if
@@ -1060,25 +1058,36 @@ uUnrefined env tv1 ty2 ty2' kco
            _ -> maybeApart -- See Note [Unification with skolems]
   }}}}
 
-uUnrefined env tv1 ty2 ty2' kco -- ty2 is not a type variable
-  = do { occurs <- elemNiSubstSet tv1 (tyCoVarsOfType ty2')
-       ; if um_unif env && occurs  -- See Note [Self-substitution when matching]
-         then maybeApart       -- Occurs check, see Note [Fine-grained unification]
-         else bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco) }
-            -- Bind tyvar to the synonym if poss
+uUnrefined env tv1 ty2 _ kco -- ty2 is not a type variable
+  = case tvBindFlagL env tv1 of
+      Skolem -> maybeApart  -- See Note [Unification with skolems]
+      BindMe -> bindTv env tv1 (ty2 `mkCastTy` mkSymCo kco)
 
-elemNiSubstSet :: TyVar -> TyCoVarSet -> UM Bool
-elemNiSubstSet v set
+bindTv :: UMEnv -> TyVar -> Type -> UM ()
+-- OK, so we want to extend the substitution with tv := ty
+-- But first, we must do a couple of checks
+bindTv env tv1 ty2
+  = do  { let free_tvs2 = tyCoVarsOfType ty2
+
+        -- Make sure tys mentions no local variables
+        -- E.g.  (forall a. b) ~ (forall a. [a])
+        -- We should not unify b := [a]!
+        ; checkRnEnvR env free_tvs2
+
+        -- Occurs check, see Note [Fine-grained unification]
+        ; occurs <- occursCheck env tv1 free_tvs2
+
+        ; if occurs then maybeApart
+                    else extendTvEnv tv1 ty2 }
+
+occursCheck :: UMEnv -> TyVar -> VarSet -> UM Bool
+occursCheck env tv free_tvs
+  | um_unif env
   = do { tsubst <- getTvSubstEnv
-       ; return $ v `elemVarSet` niSubstTvSet tsubst set }
+       ; return (tv `elemVarSet` niSubstTvSet tsubst free_tvs) }
 
-bindTv :: UMEnv -> TyVar -> Type -> UM ()
-bindTv env tv ty    -- ty is not a variable
-  = do  { checkRnEnvR env ty -- make sure ty mentions no local variables
-        ; case tvBindFlagL env tv of
-            Skolem -> maybeApart  -- See Note [Unification with skolems]
-            BindMe -> extendTvEnv tv ty
-        }
+  | otherwise      -- Matching; no occurs check
+  = return False   -- See Note [Self-substitution when matching]
 
 {-
 %************************************************************************
@@ -1195,7 +1204,8 @@ checkRnEnv get_set env varset = UM $ \ state ->
      -- means we don't have to calculate the free vars of
      -- the type, often saving quite a bit of allocation.
   then Unifiable  (state, ())
-  else MaybeApart (state, ())
+  else MaybeApart (state, ())   -- ToDo: why MaybeApart
+                                -- I think SurelyApart would be right
 
 -- | Converts any SurelyApart to a MaybeApart
 don'tBeSoSure :: UM () -> UM ()
@@ -1204,11 +1214,8 @@ don'tBeSoSure um = UM $ \ state ->
     SurelyApart -> MaybeApart (state, ())
     other       -> other
 
-checkRnEnvR :: UMEnv -> Type -> UM ()
-checkRnEnvR env ty = checkRnEnv rnEnvR env (tyCoVarsOfType ty)
-
-checkRnEnvL :: UMEnv -> Type -> UM ()
-checkRnEnvL env ty = checkRnEnv rnEnvL env (tyCoVarsOfType ty)
+checkRnEnvR :: UMEnv -> VarSet -> UM ()
+checkRnEnvR env fvs = checkRnEnv rnEnvR env fvs
 
 checkRnEnvRCo :: UMEnv -> Coercion -> UM ()
 checkRnEnvRCo env co = checkRnEnv rnEnvR env (tyCoVarsOfCo co)
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, [''])