Care with occCheckExpand in kind of occurrences

Issue #18451 showed that we could get an infinite type, through
over-use of occCheckExpand in the kind of an /occurrence/ of a
type variable.

See Note [Occurrence checking: look inside kinds] in GHC.Core.Type

This patch fixes the problem by making occCheckExpand less eager
to expand synonyms in kinds.

It also improves pretty printing of kinds, by *not* suppressing
the kind on a tyvar-binder like
    (a :: Const Type b)
where type Const p q = p.  Even though the kind of 'a' is Type,
we don't want to suppress the kind ascription.  Example: the
error message for polykinds/T18451{a,b}. See GHC.Core.TyCo.Ppr
Note [Suppressing * kinds].

10 files changed, 170 insertions, 40 deletions

diff --git a/compiler/GHC/Core/TyCo/Ppr.hs b/compiler/GHC/Core/TyCo/Ppr.hs
index e08afc0d95..ea9417e360 100644
--- a/compiler/GHC/Core/TyCo/Ppr.hs
+++ b/compiler/GHC/Core/TyCo/Ppr.hs
@@ -34,10 +34,9 @@ import {-# SOURCE #-} GHC.CoreToIface
    , toIfaceTyCon, toIfaceTcArgs, toIfaceCoercionX )
 
 import {-# SOURCE #-} GHC.Core.DataCon
-   ( dataConFullSig , dataConUserTyVarBinders
-   , DataCon )
+   ( dataConFullSig , dataConUserTyVarBinders, DataCon )
 
-import GHC.Core.Type ( isLiftedTypeKind, pattern One, pattern Many )
+import GHC.Core.Type ( pickyIsLiftedTypeKind, pattern One, pattern Many )
 
 import GHC.Core.TyCon
 import GHC.Core.TyCo.Rep
@@ -192,11 +191,35 @@ pprTyVar :: TyVar -> SDoc
 -- pprIfaceTvBndr is minimal, and the loss of uniques etc in
 -- debug printing is disastrous
 pprTyVar tv
-  | isLiftedTypeKind kind = ppr tv
-  | otherwise             = parens (ppr tv <+> dcolon <+> ppr kind)
+  | pickyIsLiftedTypeKind kind = ppr tv  -- See Note [Suppressing * kinds]
+  | otherwise                  = parens (ppr tv <+> dcolon <+> ppr kind)
   where
     kind = tyVarKind tv
 
+{- Note [Suppressing * kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Generally we want to print
+      forall a. a->a
+not   forall (a::*). a->a
+or    forall (a::Type). a->a
+That is, for brevity we suppress a kind ascription of '*' (or Type).
+
+But what if the kind is (Const Type x)?
+   type Const p q = p
+
+Then (Const Type x) is just a long way of saying Type.  But it may be
+jolly confusing to suppress the 'x'.  Suppose we have (polykinds/T18451a)
+   foo :: forall a b (c :: Const Type b). Proxy '[a, c]
+
+Then this error message
+    • These kind and type variables: a b (c :: Const Type b)
+      are out of dependency order. Perhaps try this ordering:
+        (b :: k) (a :: Const (*) b) (c :: Const (*) b)
+would be much less helpful if we suppressed the kind ascription on 'a'.
+
+Hence the use of pickyIsLiftedTypeKind.
+-}
+
 -----------------
 debugPprType :: Type -> SDoc
 -- ^ debugPprType is a simple pretty printer that prints a type
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 5471c645e6..c00c818ca5 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -120,7 +120,7 @@ module GHC.Core.Type (
 
         -- *** Levity and boxity
         isLiftedType_maybe,
-        isLiftedTypeKind, isUnliftedTypeKind,
+        isLiftedTypeKind, isUnliftedTypeKind, pickyIsLiftedTypeKind,
         isLiftedRuntimeRep, isUnliftedRuntimeRep,
         isUnliftedType, mightBeUnliftedType, isUnboxedTupleType, isUnboxedSumType,
         isAlgType, isDataFamilyAppType,
@@ -554,6 +554,23 @@ isLiftedTypeKind kind
       Just rep -> isLiftedRuntimeRep rep
       Nothing  -> False
 
+pickyIsLiftedTypeKind :: Kind -> Bool
+-- Checks whether the kind is literally
+--      TYPE LiftedRep
+-- or   Type
+-- without expanding type synonyms or anything
+-- Used only when deciding whether to suppress the ":: *" in
+-- (a :: *) when printing kinded type variables
+-- See Note [Suppressing * kinds] in GHC.Core.TyCo.Ppr
+pickyIsLiftedTypeKind kind
+  | TyConApp tc [arg] <- kind
+  , tc `hasKey` tYPETyConKey
+  , TyConApp rr_tc [] <- arg
+  , rr_tc `hasKey` liftedRepDataConKey = True
+  | TyConApp tc [] <- kind
+  , tc `hasKey` liftedTypeKindTyConKey = True
+  | otherwise                          = False
+
 isLiftedRuntimeRep :: Type -> Bool
 -- isLiftedRuntimeRep is true of LiftedRep :: RuntimeRep
 -- False of type variables (a :: RuntimeRep)
@@ -2619,6 +2636,46 @@ prefer doing inner expansions first.  For example,
 We have
   occCheckExpand b (F (G b)) = Just (F Char)
 even though we could also expand F to get rid of b.
+
+Note [Occurrence checking: look inside kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are considering unifying
+   (alpha :: *)  ~  Int -> (beta :: alpha -> alpha)
+This may be an error (what is that alpha doing inside beta's kind?),
+but we must not make the mistake of actually unifying or we'll
+build an infinite data structure.  So when looking for occurrences
+of alpha in the rhs, we must look in the kinds of type variables
+that occur there.
+
+occCheckExpand tries to expand type synonyms to remove
+unnecessary occurrences of a variable, and thereby get past an
+occurs-check failure.  This is good; but
+     we can't do it in the /kind/ of a variable /occurrence/
+
+For example #18451 built an infinite type:
+    type Const a b = a
+    data SameKind :: k -> k -> Type
+    type T (k :: Const Type a) = forall (b :: k). SameKind a b
+
+We have
+  b :: k
+  k :: Const Type a
+  a :: k   (must be same as b)
+
+So if we aren't careful, a's kind mentions a, which is bad.
+And expanding an /occurrence/ of 'a' doesn't help, because the
+/binding site/ is the master copy and all the occurrences should
+match it.
+
+Here's a related example:
+   f :: forall a b (c :: Const Type b). Proxy '[a, c]
+
+The list means that 'a' gets the same kind as 'c'; but that
+kind mentions 'b', so the binders are out of order.
+
+Bottom line: in occCheckExpand, do not expand inside the kinds
+of occurrences.  See bad_var_occ in occCheckExpand.  And
+see #18451 for more debate.
 -}
 
 occCheckExpand :: [Var] -> Type -> Maybe Type
@@ -2639,11 +2696,10 @@ occCheckExpand vs_to_avoid ty
           -- The VarSet is the set of variables we are trying to avoid
           -- The VarEnv carries mappings necessary
           -- because of kind expansion
-    go cxt@(as, env) (TyVarTy tv')
-      | tv' `elemVarSet` as               = Nothing
-      | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
-      | otherwise                         = do { tv'' <- go_var cxt tv'
-                                               ; return (mkTyVarTy tv'') }
+    go (as, env) ty@(TyVarTy tv)
+      | Just tv' <- lookupVarEnv env tv = return (mkTyVarTy tv')
+      | bad_var_occ as tv               = Nothing
+      | otherwise                       = return ty
 
     go _   ty@(LitTy {}) = return ty
     go cxt (AppTy ty1 ty2) = do { ty1' <- go cxt ty1
@@ -2656,7 +2712,7 @@ occCheckExpand vs_to_avoid ty
             ; return (ty { ft_mult = w', ft_arg = ty1', ft_res = ty2' }) }
     go cxt@(as, env) (ForAllTy (Bndr tv vis) body_ty)
        = do { ki' <- go cxt (varType tv)
-            ; let tv' = setVarType tv ki'
+            ; let tv'  = setVarType tv ki'
                   env' = extendVarEnv env tv tv'
                   as'  = as `delVarSet` tv
             ; body' <- go (as', env') body_ty
@@ -2680,9 +2736,12 @@ occCheckExpand vs_to_avoid ty
                                 ; return (mkCoercionTy co') }
 
     ------------------
-    go_var cxt v = updateVarTypeM (go cxt) v
-           -- Works for TyVar and CoVar
-           -- See Note [Occurrence checking: look inside kinds]
+    bad_var_occ :: VarSet -> Var -> Bool
+    -- Works for TyVar and CoVar
+    -- See Note [Occurrence checking: look inside kinds]
+    bad_var_occ vs_to_avoid v
+       =  v                          `elemVarSet`       vs_to_avoid
+       || tyCoVarsOfType (varType v) `intersectsVarSet` vs_to_avoid
 
     ------------------
     go_mco _   MRefl = return MRefl
@@ -2712,13 +2771,15 @@ occCheckExpand vs_to_avoid ty
                                              ; co2' <- go_co cxt co2
                                              ; w' <- go_co cxt w
                                              ; return (mkFunCo r w' co1' co2') }
-    go_co cxt@(as,env) (CoVarCo c)
-      | c `elemVarSet` as               = Nothing
+    go_co (as,env) co@(CoVarCo c)
       | Just c' <- lookupVarEnv env c   = return (mkCoVarCo c')
-      | otherwise                       = do { c' <- go_var cxt c
-                                             ; return (mkCoVarCo c') }
-    go_co cxt (HoleCo h)                = do { c' <- go_var cxt (ch_co_var h)
-                                             ; return (HoleCo (h { ch_co_var = c' })) }
+      | bad_var_occ as c                = Nothing
+      | otherwise                       = return co
+
+    go_co (as,_) co@(HoleCo h)
+      | bad_var_occ as (ch_co_var h)    = Nothing
+      | otherwise                       = return co
+
     go_co cxt (AxiomInstCo ax ind args) = do { args' <- mapM (go_co cxt) args
                                              ; return (mkAxiomInstCo ax ind args') }
     go_co cxt (UnivCo p r ty1 ty2)      = do { p' <- go_prov cxt p
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index bf933127b8..2aa47748cb 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -1879,21 +1879,8 @@ matchExpectedFunKind hs_ty n k = go n k
 ********************************************************************* -}
 
 
-{-  Note [Occurrence checking: look inside kinds]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we are considering unifying
-   (alpha :: *)  ~  Int -> (beta :: alpha -> alpha)
-This may be an error (what is that alpha doing inside beta's kind?),
-but we must not make the mistake of actually unifying or we'll
-build an infinite data structure.  So when looking for occurrences
-of alpha in the rhs, we must look in the kinds of type variables
-that occur there.
-
-NB: we may be able to remove the problem via expansion; see
-    Note [Occurs check expansion].  So we have to try that.
-
-Note [Checking for foralls]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{-  Note [Checking for foralls]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Unless we have -XImpredicativeTypes (which is a totally unsupported
 feature), we do not want to unify
     alpha ~ (forall a. a->a) -> Int
@@ -1906,10 +1893,10 @@ Consider
    (alpha :: forall k. k->*)  ~  (beta :: forall k. k->*)
 This is legal; e.g. dependent/should_compile/T11635.
 
-We don't want to reject it because of the forall in beta's kind,
-but (see Note [Occurrence checking: look inside kinds]) we do
-need to look in beta's kind.  So we carry a flag saying if a 'forall'
-is OK, and switch the flag on when stepping inside a kind.
+We don't want to reject it because of the forall in beta's kind, but
+(see Note [Occurrence checking: look inside kinds] in GHC.Core.Type)
+we do need to look in beta's kind.  So we carry a flag saying if a
+'forall' is OK, and switch the flag on when stepping inside a kind.
 
 Why is it OK?  Why does it not count as impredicative polymorphism?
 The reason foralls are bad is because we reply on "seeing" foralls
@@ -2030,6 +2017,7 @@ preCheck dflags ty_fam_ok tv ty
       | tv == tv' = MTVU_Occurs
       | otherwise = fast_check_occ (tyVarKind tv')
            -- See Note [Occurrence checking: look inside kinds]
+           -- in GHC.Core.Type
 
     fast_check (TyConApp tc tys)
       | bad_tc tc              = MTVU_Bad
diff --git a/testsuite/tests/polykinds/T18451.hs b/testsuite/tests/polykinds/T18451.hs
new file mode 100644
index 0000000000..da14360ea5
--- /dev/null
+++ b/testsuite/tests/polykinds/T18451.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+
+type Const a b = a
+data SameKind :: k -> k -> Type
+
+type T (k :: Const Type a) = forall (b :: k). SameKind a b
diff --git a/testsuite/tests/polykinds/T18451.stderr b/testsuite/tests/polykinds/T18451.stderr
new file mode 100644
index 0000000000..5f61afcbbe
--- /dev/null
+++ b/testsuite/tests/polykinds/T18451.stderr
@@ -0,0 +1,9 @@
+
+T18451.hs:10:58: error:
+    • Expected kind ‘k0’, but ‘b’ has kind ‘k’
+    • In the second argument of ‘SameKind’, namely ‘b’
+      In the type ‘forall (b :: k). SameKind a b’
+      In the type declaration for ‘T’
+    • Type variable kinds:
+        a :: k0
+        k :: Const (*) a
diff --git a/testsuite/tests/polykinds/T18451a.hs b/testsuite/tests/polykinds/T18451a.hs
new file mode 100644
index 0000000000..9b5248c30f
--- /dev/null
+++ b/testsuite/tests/polykinds/T18451a.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+import Data.Proxy
+
+type Const a b = a
+
+foo :: forall a b (c :: Const Type b). Proxy '[a, c]
+foo = error "ruk"
diff --git a/testsuite/tests/polykinds/T18451a.stderr b/testsuite/tests/polykinds/T18451a.stderr
new file mode 100644
index 0000000000..fbfd3ce288
--- /dev/null
+++ b/testsuite/tests/polykinds/T18451a.stderr
@@ -0,0 +1,7 @@
+
+T18451a.hs:10:8: error:
+    • These kind and type variables: a b (c :: Const Type b)
+      are out of dependency order. Perhaps try this ordering:
+        (b :: k) (a :: Const (*) b) (c :: Const (*) b)
+    • In the type signature:
+        foo :: forall a b (c :: Const Type b). Proxy '[a, c]
diff --git a/testsuite/tests/polykinds/T18451b.hs b/testsuite/tests/polykinds/T18451b.hs
new file mode 100644
index 0000000000..9b5248c30f
--- /dev/null
+++ b/testsuite/tests/polykinds/T18451b.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeInType #-}
+module Bug where
+
+import Data.Kind
+import Data.Proxy
+
+type Const a b = a
+
+foo :: forall a b (c :: Const Type b). Proxy '[a, c]
+foo = error "ruk"
diff --git a/testsuite/tests/polykinds/T18451b.stderr b/testsuite/tests/polykinds/T18451b.stderr
new file mode 100644
index 0000000000..d12d9b382a
--- /dev/null
+++ b/testsuite/tests/polykinds/T18451b.stderr
@@ -0,0 +1,7 @@
+
+T18451b.hs:10:8: error:
+    • These kind and type variables: a b (c :: Const Type b)
+      are out of dependency order. Perhaps try this ordering:
+        (b :: k) (a :: Const (*) b) (c :: Const (*) b)
+    • In the type signature:
+        foo :: forall a b (c :: Const Type b). Proxy '[a, c]
diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T
index 00856b8dc3..436bb9dbce 100644
--- a/testsuite/tests/polykinds/all.T
+++ b/testsuite/tests/polykinds/all.T
@@ -220,3 +220,6 @@ test('CuskFam', normal, compile, [''])
 test('T17841', normal, compile_fail, [''])
 test('T17963', normal, compile_fail, [''])
 test('T18300', normal, compile_fail, [''])
+test('T18451', normal, compile_fail, [''])
+test('T18451a', normal, compile_fail, [''])
+test('T18451b', normal, compile_fail, [''])