Fix #11407.

This removes the `defer_me` check that was in checkTauTvUpdate
and uses only a type family check instead. The old defer_me check
repeated work done by fast_check in occurCheckExpand.

There is also some error message improvement, necessitated by
the terrible error message that the test case produced, even when
it didn't consume all of memory.

test case: dependent/should_fail/T11407

[skip ci]

8 files changed, 70 insertions, 48 deletions

diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 48c036117f..0b0dae4e71 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -1179,7 +1179,20 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
                            hang (text "Occurs check: cannot construct the infinite" <+> what <> colon)
                               2 (sep [ppr ty1, char '~', ppr ty2])
              extra2 = important $ mkEqInfoMsg ct ty1 ty2
-       ; mkErrorMsgFromCt ctxt ct $ mconcat [occCheckMsg, extra2, report] }
+
+             interesting_tyvars
+               = filter (not . isEmptyVarSet . tyCoVarsOfType . tyVarKind) $
+                 filter isTyVar $
+                 varSetElems $
+                 tyCoVarsOfType ty1 `unionVarSet` tyCoVarsOfType ty2
+             extra3 = relevant_bindings $
+                      ppWhen (not (null interesting_tyvars)) $
+                      hang (text "Type variable kinds:") 2 $
+                      vcat (map (tyvar_binding . tidyTyVarOcc (cec_tidy ctxt))
+                                interesting_tyvars)
+
+             tyvar_binding tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
+       ; mkErrorMsgFromCt ctxt ct $ mconcat [occCheckMsg, extra2, extra3, report] }
 
   | OC_Forall <- occ_check_expand
   = do { let msg = vcat [ text "Cannot instantiate unification variable"
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 77651c8568..a87f30479e 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -50,7 +50,7 @@ import TyCon
 import TysWiredIn
 import Var
 import VarEnv
-import VarSet
+import NameEnv
 import ErrUtils
 import DynFlags
 import BasicTypes
@@ -1449,53 +1449,28 @@ checkTauTvUpdate dflags origin t_or_k tv ty
   | otherwise
   = do { ty   <- zonkTcType ty
        ; co_k <- uType kind_origin KindLevel (typeKind ty) (tyVarKind tv)
-       ; if | defer_me ty ->  -- Quick test
-                -- Failed quick test so try harder
-                case occurCheckExpand dflags tv ty of
-                   OC_OK ty2 | defer_me ty2 -> return Nothing
-                             | otherwise    -> return (Just (ty2, co_k))
-                   _                        -> return Nothing
-            | otherwise   -> return (Just (ty, co_k)) }
+       ; return $ case occurCheckExpand dflags tv ty of
+           OC_OK ty2 | type_fam_free ty2 -> Just (ty2, co_k)
+           _                             -> Nothing }
+
   where
     kind_origin   = KindEqOrigin (mkTyVarTy tv) (Just ty) origin (Just t_or_k)
     details       = tcTyVarDetails tv
     info          = mtv_info details
-    impredicative = canUnifyWithPolyType dflags details
 
-    defer_me :: TcType -> Bool
-    -- Checks for (a) occurrence of tv
-    --            (b) type family applications
-    --            (c) foralls
     -- See Note [Conservative unification check]
-    defer_me (LitTy {})        = False
-    defer_me (TyVarTy tv')     = tv == tv'
-    defer_me (TyConApp tc tys) = isTypeFamilyTyCon tc || any defer_me tys
-                                 || not (impredicative || isTauTyCon tc)
-    defer_me (ForAllTy bndr t) = defer_me (binderType bndr) || defer_me t
-                                 || (isNamedBinder bndr && not impredicative)
-    defer_me (AppTy fun arg)   = defer_me fun || defer_me arg
-    defer_me (CastTy ty co)    = defer_me ty || defer_me_co co
-    defer_me (CoercionTy co)   = defer_me_co co
-
-      -- We don't really care if there are type families in a coercion,
-      -- but we still can't have an occurs-check failure
-    defer_me_co co = tv `elemVarSet` tyCoVarsOfCo co
+    type_fam_free :: TcType -> Bool
+    type_fam_free = not . any isTypeFamilyTyCon . nameEnvElts . tyConsOfType
 
 {-
 Note [Conservative unification check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 When unifying (tv ~ rhs), w try to avoid creating deferred constraints
-only for efficiency.  However, we do not unify (the defer_me check) if
-  a) There's an occurs check (tv is in fvs(rhs))
+only for efficiency.  However, we do not unify if
+  a) There's an occurs check (tv is in fvs(rhs)) (established by occurCheckExpand)
+     (see Note [Type synonyms and the occur check])
   b) There's a type-function call in 'rhs'
 
-If we fail defer_me we use occurCheckExpand to try to make it pass,
-(see Note [Type synonyms and the occur check]) and then use defer_me
-again to check.  Example: Trac #4917)
-       a ~ Const a b
-where type Const a b = a.  We can solve this immediately, even when
-'a' is a skolem, just by expanding the synonym.
-
 We always defer type-function calls, even if it's be perfectly safe to
 unify, eg (a ~ F [b]).  Reason: this ensures that the constraint
 solver gets to see, and hence simplify the type-function call, which
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index 4c60b6e54f..78adcd2901 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -126,6 +126,7 @@ module TyCoRep (
 import {-# SOURCE #-} DataCon( dataConTyCon, dataConFullSig
                               , DataCon, eqSpecTyVar )
 import {-# SOURCE #-} Type( isPredTy, isCoercionTy, mkAppTy
+                          , tyCoVarsOfTypesWellScoped, varSetElemsWellScoped
                           , partitionInvisibles, coreView, typeKind )
    -- Transitively pulls in a LOT of stuff, better to break the loop
 
@@ -2867,7 +2868,7 @@ tidyFreeTyCoVars :: TidyEnv -> TyCoVarSet -> TidyEnv
 -- ^ Add the free 'TyVar's to the env in tidy form,
 -- so that we can tidy the type they are free in
 tidyFreeTyCoVars (full_occ_env, var_env) tyvars
-  = fst (tidyOpenTyCoVars (full_occ_env, var_env) (varSetElems tyvars))
+  = fst (tidyOpenTyCoVars (full_occ_env, var_env) (varSetElemsWellScoped tyvars))
 
         ---------------
 tidyOpenTyCoVars :: TidyEnv -> [TyCoVar] -> (TidyEnv, [TyCoVar])
@@ -2885,9 +2886,9 @@ tidyOpenTyCoVar env@(_, subst) tyvar
 
 ---------------
 tidyTyVarOcc :: TidyEnv -> TyVar -> TyVar
-tidyTyVarOcc (_, subst) tv
+tidyTyVarOcc env@(_, subst) tv
   = case lookupVarEnv subst tv of
-        Nothing  -> tv
+        Nothing  -> updateTyVarKind (tidyType env) tv
         Just tv' -> tv'
 
 ---------------
@@ -2913,19 +2914,21 @@ tidyType env (CoercionTy co)      = CoercionTy $! (tidyCo env co)
 ---------------
 -- | Grabs the free type variables, tidies them
 -- and then uses 'tidyType' to work over the type itself
-tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
-tidyOpenType env ty
-  = (env', tidyType (trimmed_occ_env, var_env) ty)
+tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
+tidyOpenTypes env tys
+  = (env', tidyTypes (trimmed_occ_env, var_env) tys)
   where
-    (env'@(_, var_env), tvs') = tidyOpenTyCoVars env (tyCoVarsOfTypeList ty)
+    (env'@(_, var_env), tvs') = tidyOpenTyCoVars env $
+                                tyCoVarsOfTypesWellScoped tys
     trimmed_occ_env = initTidyOccEnv (map getOccName tvs')
       -- The idea here was that we restrict the new TidyEnv to the
-      -- _free_ vars of the type, so that we don't gratuitously rename
-      -- the _bound_ variables of the type.
+      -- _free_ vars of the types, so that we don't gratuitously rename
+      -- the _bound_ variables of the types.
 
 ---------------
-tidyOpenTypes :: TidyEnv -> [Type] -> (TidyEnv, [Type])
-tidyOpenTypes env tys = mapAccumL tidyOpenType env tys
+tidyOpenType :: TidyEnv -> Type -> (TidyEnv, Type)
+tidyOpenType env ty = let (env', [ty']) = tidyOpenTypes env [ty] in
+                      (env', ty')
 
 ---------------
 -- | Calls 'tidyType' on a top-level type (i.e. with an empty tidying environment)
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index b71bba315d..a3efac0250 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -127,6 +127,7 @@ module Type (
 
         -- * Well-scoped lists of variables
         varSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped,
+        tyCoVarsOfTypesWellScoped,
 
         -- * Type comparison
         eqType, eqTypeX, eqTypes, cmpType, cmpTypes, cmpTypeX, cmpTypesX, cmpTc,
@@ -1872,6 +1873,10 @@ varSetElemsWellScoped = toposortTyVars . varSetElems
 tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
 tyCoVarsOfTypeWellScoped = toposortTyVars . tyCoVarsOfTypeList
 
+-- | Get the free vars of types in scoped order
+tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
+tyCoVarsOfTypesWellScoped = toposortTyVars . tyCoVarsOfTypesList
+
 {-
 ************************************************************************
 *                                                                      *
@@ -2271,7 +2276,9 @@ tyConsOfType ty
      go_prov (PhantomProv co)    = go_co co
      go_prov (ProofIrrelProv co) = go_co co
      go_prov (PluginProv _)      = emptyNameEnv
-     go_prov (HoleProv h)        = pprPanic "tyConsOfType hit a hole" (ppr h)
+     go_prov (HoleProv _)        = emptyNameEnv
+        -- this last case can happen from the tyConsOfType used from
+        -- checkTauTvUpdate
 
      go_s tys     = foldr (plusNameEnv . go)     emptyNameEnv tys
      go_cos cos   = foldr (plusNameEnv . go_co)  emptyNameEnv cos
diff --git a/compiler/types/Type.hs-boot b/compiler/types/Type.hs-boot
index abddc24b25..aecfc7fa22 100644
--- a/compiler/types/Type.hs-boot
+++ b/compiler/types/Type.hs-boot
@@ -1,5 +1,7 @@
 module Type where
 import TyCon
+import Var ( TyVar, TyCoVar )
+import VarSet ( TyCoVarSet )
 import {-# SOURCE #-} TyCoRep( Type, Kind )
 
 isPredTy :: Type -> Bool
@@ -16,3 +18,6 @@ coreViewOneStarKind :: Type -> Maybe Type
 partitionInvisibles :: TyCon -> (a -> Type) -> [a] -> ([a], [a])
 
 coreView :: Type -> Maybe Type
+
+tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
+varSetElemsWellScoped :: TyCoVarSet -> [TyCoVar]
diff --git a/testsuite/tests/dependent/should_fail/T11407.hs b/testsuite/tests/dependent/should_fail/T11407.hs
new file mode 100644
index 0000000000..533870f94b
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T11407.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+module T11407 where
+
+import Data.Kind
+
+type Const a b = a
+
+data family UhOh (f :: k1) (a :: k2) (b :: k3)
+data instance UhOh (f :: * -> * -> *) (a :: x a) (b :: Const * a) = UhOh
diff --git a/testsuite/tests/dependent/should_fail/T11407.stderr b/testsuite/tests/dependent/should_fail/T11407.stderr
new file mode 100644
index 0000000000..b5d95bf2a1
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T11407.stderr
@@ -0,0 +1,8 @@
+
+T11407.hs:10:40: error:
+    • Occurs check: cannot construct the infinite kind: k0 ~ x a
+    • In the second argument of ‘UhOh’, namely ‘(a :: x a)’
+      In the data instance declaration for ‘UhOh’
+    • Type variable kinds:
+        a :: k0
+        x :: k0 -> *
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 8f9c9d0016..08f6cf653d 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -8,3 +8,4 @@ test('PromotedClass', normal, compile_fail, [''])
 test('SelfDep', normal, compile_fail, [''])
 test('BadTelescope4', normal, compile_fail, [''])
 test('RenamingStar', normal, compile_fail, [''])
+test('T11407', normal, compile_fail, [''])