[Git][ghc/ghc][master] Care with occCheckExpand in kind of occurrences
Marge Bot
gitlab at gitlab.haskell.org
Fri Jul 24 22:13:41 UTC 2020
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
ba205046 by Simon Peyton Jones at 2020-07-24T18:13:35-04:00
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 changed files:
- compiler/GHC/Core/TyCo/Ppr.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Tc/Utils/Unify.hs
- + testsuite/tests/polykinds/T18451.hs
- + testsuite/tests/polykinds/T18451.stderr
- + testsuite/tests/polykinds/T18451a.hs
- + testsuite/tests/polykinds/T18451a.stderr
- + testsuite/tests/polykinds/T18451b.hs
- + testsuite/tests/polykinds/T18451b.stderr
- testsuite/tests/polykinds/all.T
Changes:
=====================================
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
=====================================
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
=====================================
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
=====================================
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
=====================================
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
=====================================
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"
=====================================
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]
=====================================
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"
=====================================
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]
=====================================
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, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ba205046e4f2ea94b1c978c050b917de4daaf092
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ba205046e4f2ea94b1c978c050b917de4daaf092
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200724/af9b445b/attachment-0001.html>
More information about the ghc-commits
mailing list