Commit ba205046 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Marge Bot
Browse files

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].
parent c1f4f81d
......@@ -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
......
......@@ -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
......
......@@ -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
......
{-# 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
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
{-# 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"
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]
{-# 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"
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]
......@@ -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, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment