Commit f903e551 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Fix corner case in typeKind, plus refactoring

This is a continuation of

    commit 9d600ea6
    Author: Simon Peyton Jones <simonpj@microsoft.com>
    Date:   Fri Jun 1 16:36:57 2018 +0100

        Expand type synonyms when Linting a forall

That patch pointed out that there was a lurking hole in
typeKind, where it could return an ill-scoped kind, because
of not expanding type synonyms enough.

This patch fixes it, quite nicely

* Use occCheckExpand to expand those synonyms (it was always
  designed for that exact purpose), and call it from
         Type.typeKind
         CoreUtils.coreAltType
         CoreLint.lintTYpe

* Consequently, move occCheckExpand from TcUnify.hs to
  Type.hs, and generalise it to take a list of type variables.

I also tidied up lintType a bit.
parent 807ab222
......@@ -715,8 +715,7 @@ lintCoreExpr (Cast expr co)
= do { expr_ty <- markAllJoinsBad $ lintCoreExpr expr
; co' <- applySubstCo co
; (_, k2, from_ty, to_ty, r) <- lintCoercion co'
; lintL (classifiesTypeWithValues k2)
(text "Target of cast not # or *:" <+> ppr co)
; checkValueKind k2 (text "target of cast" <+> quotes (ppr co))
; lintRole co' Representational r
; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
; return to_ty }
......@@ -1296,8 +1295,9 @@ lintInTy ty
= addLoc (InType ty) $
do { ty' <- applySubstTy ty
; k <- lintType ty'
-- No need to lint k, because lintType
-- guarantees that k is linted
; lintKind k -- The kind returned by lintType is already
-- a LintedKind but we also want to check that
-- k :: *, which lintKind does
; return (ty', k) }
checkTyCon :: TyCon -> LintM ()
......@@ -1357,18 +1357,13 @@ lintType t@(ForAllTy (TvBndr tv _vis) ty)
= do { lintL (isTyVar tv) (text "Covar bound in type:" <+> ppr t)
; lintTyBndr tv $ \tv' ->
do { k <- lintType ty
; lintL (classifiesTypeWithValues k)
(text "Non-* and non-# kind in forall:" <+> ppr t)
; if (not (tv' `elemVarSet` tyCoVarsOfType k))
then return k
else
do { -- See Note [Stupid type synonyms]
let k' = expandTypeSynonyms k
; lintL (not (tv' `elemVarSet` tyCoVarsOfType k'))
(hang (text "Variable escape in forall:")
2 (vcat [ text "type:" <+> ppr t
, text "kind:" <+> ppr k' ]))
; return k' }}}
; checkValueKind k (text "the body of forall:" <+> ppr t)
; case occCheckExpand [tv'] k of -- See Note [Stupid type synonyms]
Just k' -> return k'
Nothing -> failWithL (hang (text "Variable escape in forall:")
2 (vcat [ text "type:" <+> ppr t
, text "kind:" <+> ppr k ]))
}}
lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
......@@ -1429,9 +1424,9 @@ lintKind k = do { sk <- lintType k
2 (text "has kind:" <+> ppr sk))) }
-----------------
-- confirms that a type is really *
lintStar :: SDoc -> OutKind -> LintM ()
lintStar doc k
-- Confirms that a type is really *, #, Constraint etc
checkValueKind :: OutKind -> SDoc -> LintM ()
checkValueKind k doc
= lintL (classifiesTypeWithValues k)
(text "Non-*-like kind when *-like expected:" <+> ppr k $$
text "when checking" <+> doc)
......@@ -1618,8 +1613,8 @@ lintInCo co
lintStarCoercion :: OutCoercion -> LintM (LintedType, LintedType)
lintStarCoercion g
= do { (k1, k2, t1, t2, r) <- lintCoercion g
; lintStar (text "the kind of the left type in" <+> ppr g) k1
; lintStar (text "the kind of the right type in" <+> ppr g) k2
; checkValueKind k1 (text "the kind of the left type in" <+> ppr g)
; checkValueKind k2 (text "the kind of the right type in" <+> ppr g)
; lintRole g Nominal r
; return (t1, t2) }
......
......@@ -130,13 +130,13 @@ exprType other = pprTrace "exprType" (pprCoreExpr other) alphaTy
coreAltType :: CoreAlt -> Type
-- ^ Returns the type of the alternatives right hand side
coreAltType (_,bs,rhs)
| any bad_binder bs = expandTypeSynonyms ty
| otherwise = ty -- Note [Existential variables and silly type synonyms]
coreAltType alt@(_,bs,rhs)
= case occCheckExpand bs rhs_ty of
-- Note [Existential variables and silly type synonyms]
Just ty -> ty
Nothing -> pprPanic "coreAltType" (pprCoreAlt alt $$ ppr rhs_ty)
where
ty = exprType rhs
free_tvs = tyCoVarsOfType ty
bad_binder b = b `elemVarSet` free_tvs
rhs_ty = exprType rhs
coreAltsType :: [CoreAlt] -> Type
-- ^ Returns the type of the first alternative, which should be the same as for all alternatives
......
......@@ -14,7 +14,6 @@ import GhcPrelude
import TcRnTypes
import TcType
import Type
import TcUnify( occCheckExpand )
import TcEvidence
import TyCon
import TyCoRep -- performs delicate algorithm on types
......@@ -1994,7 +1993,7 @@ unflattenWanteds tv_eqs funeqs
-- to observe the occurs check. Zonking will eliminate it
-- altogether in due course
rhs' <- zonkTcType (mkTyConApp tc xis)
; case occCheckExpand fmv rhs' of
; case occCheckExpand [fmv] rhs' of
Just rhs'' -- Normal case: fill the tyvar
-> do { setReflEvidence ev NomEq rhs''
; unflattenFmv fmv rhs''
......@@ -2092,7 +2091,7 @@ tryFill ev tv rhs
, tv == tv' -- tv == rhs
-> return True
_ | Just rhs'' <- occCheckExpand tv rhs'
_ | Just rhs'' <- occCheckExpand [tv] rhs'
-> do { -- Fill the tyvar
unifyTyVar tv rhs''
; return True }
......
......@@ -31,8 +31,7 @@ module TcUnify (
matchActualFunTys, matchActualFunTysPart,
matchExpectedFunKind,
occCheckExpand, metaTyVarUpdateOK,
occCheckForErrors, OccCheckResult(..)
metaTyVarUpdateOK, occCheckForErrors, OccCheckResult(..)
) where
......@@ -61,7 +60,6 @@ import DynFlags
import BasicTypes
import Bag
import Util
import Pair( pFst )
import qualified GHC.LanguageExtensions as LangExt
import Outputable
......@@ -1985,34 +1983,8 @@ matchExpectedFunKind hs_ty = go
********************************************************************* -}
{- Note [Occurs check expansion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
of occurrences of tv outside type function arguments, if that is
possible; otherwise, it returns Nothing.
For example, suppose we have
type F a b = [a]
Then
occCheckExpand b (F Int b) = Just [Int]
but
occCheckExpand a (F a Int) = Nothing
We don't promise to do the absolute minimum amount of expanding
necessary, but we try not to do expansions we don't need to. We
prefer doing inner expansions first. For example,
type F a b = (a, Int, a, [a])
type G b = Char
We have
occCheckExpand b (F (G b)) = Just (F Char)
even though we could also expand F to get rid of b.
The two variants of the function are to support TcUnify.checkTauTvUpdate,
which wants to prevent unification with type families. For more on this
point, see Note [Prevent unification with type families] in TcUnify.
Note [Occurrence checking: look inside kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
{- 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?),
......@@ -2083,7 +2055,7 @@ occCheckForErrors dflags tv ty
= case preCheck dflags True tv ty of
OC_OK _ -> OC_OK ()
OC_Bad -> OC_Bad
OC_Occurs -> case occCheckExpand tv ty of
OC_Occurs -> case occCheckExpand [tv] ty of
Nothing -> OC_Occurs
Just _ -> OC_OK ()
......@@ -2121,7 +2093,7 @@ metaTyVarUpdateOK dflags tv ty
-- See Note [Prevent unification with type families]
OC_OK _ -> Just ty
OC_Bad -> Nothing -- forall or type function
OC_Occurs -> occCheckExpand tv ty
OC_Occurs -> occCheckExpand [tv] ty
preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult ()
-- A quick check for
......@@ -2182,121 +2154,6 @@ preCheck dflags ty_fam_ok tv ty
| not (ty_fam_ok || isFamFreeTyCon tc) = True
| otherwise = False
occCheckExpand :: TcTyVar -> TcType -> Maybe TcType
-- See Note [Occurs check expansion]
-- We may have needed to do some type synonym unfolding in order to
-- get rid of the variable (or forall), so we also return the unfolded
-- version of the type, which is guaranteed to be syntactically free
-- of the given type variable. If the type is already syntactically
-- free of the variable, then the same type is returned.
occCheckExpand tv ty
= go emptyVarEnv ty
where
go :: VarEnv TyVar -> Type -> Maybe Type
-- The VarEnv carries mappings necessary
-- because of kind expansion
go env (TyVarTy tv')
| tv == tv' = Nothing
| Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'')
| otherwise = do { tv'' <- go_var env tv'
; return (mkTyVarTy tv'') }
go _ ty@(LitTy {}) = return ty
go env (AppTy ty1 ty2) = do { ty1' <- go env ty1
; ty2' <- go env ty2
; return (mkAppTy ty1' ty2') }
go env (FunTy ty1 ty2) = do { ty1' <- go env ty1
; ty2' <- go env ty2
; return (mkFunTy ty1' ty2') }
go env ty@(ForAllTy (TvBndr tv' vis) body_ty)
| tv == tv' = return ty
| otherwise = do { ki' <- go env (tyVarKind tv')
; let tv'' = setTyVarKind tv' ki'
env' = extendVarEnv env tv' tv''
; body' <- go env' body_ty
; return (ForAllTy (TvBndr tv'' vis) body') }
-- For a type constructor application, first try expanding away the
-- offending variable from the arguments. If that doesn't work, next
-- see if the type constructor is a type synonym, and if so, expand
-- it and try again.
go env ty@(TyConApp tc tys)
= case mapM (go env) tys of
Just tys' -> return (mkTyConApp tc tys')
Nothing | Just ty' <- tcView ty -> go env ty'
| otherwise -> Nothing
-- Failing that, try to expand a synonym
go env (CastTy ty co) = do { ty' <- go env ty
; co' <- go_co env co
; return (mkCastTy ty' co') }
go env (CoercionTy co) = do { co' <- go_co env co
; return (mkCoercionTy co') }
------------------
go_var env v = do { k' <- go env (varType v)
; return (setVarType v k') }
-- Works for TyVar and CoVar
-- See Note [Occurrence checking: look inside kinds]
------------------
go_co env (Refl r ty) = do { ty' <- go env ty
; return (mkReflCo r ty') }
-- Note: Coercions do not contain type synonyms
go_co env (TyConAppCo r tc args) = do { args' <- mapM (go_co env) args
; return (mkTyConAppCo r tc args') }
go_co env (AppCo co arg) = do { co' <- go_co env co
; arg' <- go_co env arg
; return (mkAppCo co' arg') }
go_co env co@(ForAllCo tv' kind_co body_co)
| tv == tv' = return co
| otherwise = do { kind_co' <- go_co env kind_co
; let tv'' = setTyVarKind tv' $
pFst (coercionKind kind_co')
env' = extendVarEnv env tv' tv''
; body' <- go_co env' body_co
; return (ForAllCo tv'' kind_co' body') }
go_co env (FunCo r co1 co2) = do { co1' <- go_co env co1
; co2' <- go_co env co2
; return (mkFunCo r co1' co2') }
go_co env (CoVarCo c) = do { c' <- go_var env c
; return (mkCoVarCo c') }
go_co env (HoleCo h) = do { c' <- go_var env (ch_co_var h)
; return (HoleCo (h { ch_co_var = c' })) }
go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args
; return (mkAxiomInstCo ax ind args') }
go_co env (UnivCo p r ty1 ty2) = do { p' <- go_prov env p
; ty1' <- go env ty1
; ty2' <- go env ty2
; return (mkUnivCo p' r ty1' ty2') }
go_co env (SymCo co) = do { co' <- go_co env co
; return (mkSymCo co') }
go_co env (TransCo co1 co2) = do { co1' <- go_co env co1
; co2' <- go_co env co2
; return (mkTransCo co1' co2') }
go_co env (NthCo r n co) = do { co' <- go_co env co
; return (mkNthCo r n co') }
go_co env (LRCo lr co) = do { co' <- go_co env co
; return (mkLRCo lr co') }
go_co env (InstCo co arg) = do { co' <- go_co env co
; arg' <- go_co env arg
; return (mkInstCo co' arg') }
go_co env (CoherenceCo co1 co2) = do { co1' <- go_co env co1
; co2' <- go_co env co2
; return (mkCoherenceCo co1' co2') }
go_co env (KindCo co) = do { co' <- go_co env co
; return (mkKindCo co') }
go_co env (SubCo co) = do { co' <- go_co env co
; return (mkSubCo co') }
go_co env (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co env) cs
; return (mkAxiomRuleCo ax cs') }
------------------
go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv
go_prov env (PhantomProv co) = PhantomProv <$> go_co env co
go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co
go_prov _ p@(PluginProv _) = return p
canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool
canUnifyWithPolyType dflags details
= case details of
......
......@@ -32,6 +32,7 @@ mkCoherenceCo :: Coercion -> Coercion -> Coercion
mkKindCo :: Coercion -> Coercion
mkSubCo :: Coercion -> Coercion
mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
isReflCo :: Coercion -> Bool
isReflexiveCo :: Coercion -> Bool
......
......@@ -133,7 +133,7 @@ module Type (
noFreeVarsOfType,
splitVisVarsOfType, splitVisVarsOfTypes,
expandTypeSynonyms,
typeSize,
typeSize, occCheckExpand,
-- * Well-scoped lists of variables
dVarSetElemsWellScoped, toposortTyVars, tyCoVarsOfTypeWellScoped,
......@@ -2320,16 +2320,20 @@ nonDetCmpTc tc1 tc2
-}
typeKind :: HasDebugCallStack => Type -> Kind
typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
typeKind (AppTy fun arg) = typeKind_apps fun [arg]
typeKind (LitTy l) = typeLiteralKind l
typeKind (FunTy {}) = liftedTypeKind
typeKind (TyVarTy tyvar) = tyVarKind tyvar
typeKind (CastTy _ty co) = pSnd $ coercionKind co
typeKind (CoercionTy co) = coercionType co
typeKind (ForAllTy _ ty) = typeKind ty -- Urk. See Note [Stupid type synonyms]
-- in CoreLint. Maybe we should do
-- something similar here...
typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
typeKind (AppTy fun arg) = typeKind_apps fun [arg]
typeKind (LitTy l) = typeLiteralKind l
typeKind (FunTy {}) = liftedTypeKind
typeKind (TyVarTy tyvar) = tyVarKind tyvar
typeKind (CastTy _ty co) = pSnd $ coercionKind co
typeKind (CoercionTy co) = coercionType co
typeKind ty@(ForAllTy {}) = case occCheckExpand tvs k of
Just k' -> k'
Nothing -> pprPanic "typeKind"
(ppr ty $$ ppr k $$ ppr tvs $$ ppr body)
where
(tvs, body) = splitForAllTys ty
k = typeKind body
typeKind_apps :: HasDebugCallStack => Type -> [Type] -> Kind
-- The sole purpose of the function is to accumulate
......@@ -2370,6 +2374,153 @@ isTypeLevPoly = go
resultIsLevPoly :: Type -> Bool
resultIsLevPoly = isTypeLevPoly . snd . splitPiTys
{- **********************************************************************
* *
Occurs check expansion
%* *
%********************************************************************* -}
{- Note [Occurs check expansion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(occurCheckExpand tv xi) expands synonyms in xi just enough to get rid
of occurrences of tv outside type function arguments, if that is
possible; otherwise, it returns Nothing.
For example, suppose we have
type F a b = [a]
Then
occCheckExpand b (F Int b) = Just [Int]
but
occCheckExpand a (F a Int) = Nothing
We don't promise to do the absolute minimum amount of expanding
necessary, but we try not to do expansions we don't need to. We
prefer doing inner expansions first. For example,
type F a b = (a, Int, a, [a])
type G b = Char
We have
occCheckExpand b (F (G b)) = Just (F Char)
even though we could also expand F to get rid of b.
-}
occCheckExpand :: [Var] -> Type -> Maybe Type
-- See Note [Occurs check expansion]
-- We may have needed to do some type synonym unfolding in order to
-- get rid of the variable (or forall), so we also return the unfolded
-- version of the type, which is guaranteed to be syntactically free
-- of the given type variable. If the type is already syntactically
-- free of the variable, then the same type is returned.
occCheckExpand vs_to_avoid ty
= go (mkVarSet vs_to_avoid, emptyVarEnv) ty
where
go :: (VarSet, VarEnv TyVar) -> Type -> Maybe Type
-- 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 _ ty@(LitTy {}) = return ty
go cxt (AppTy ty1 ty2) = do { ty1' <- go cxt ty1
; ty2' <- go cxt ty2
; return (mkAppTy ty1' ty2') }
go cxt (FunTy ty1 ty2) = do { ty1' <- go cxt ty1
; ty2' <- go cxt ty2
; return (mkFunTy ty1' ty2') }
go cxt@(as, env) (ForAllTy (TvBndr tv vis) body_ty)
= do { ki' <- go cxt (tyVarKind tv)
; let tv' = setTyVarKind tv ki'
env' = extendVarEnv env tv tv'
as' = as `delVarSet` tv
; body' <- go (as', env') body_ty
; return (ForAllTy (TvBndr tv' vis) body') }
-- For a type constructor application, first try expanding away the
-- offending variable from the arguments. If that doesn't work, next
-- see if the type constructor is a type synonym, and if so, expand
-- it and try again.
go cxt ty@(TyConApp tc tys)
= case mapM (go cxt) tys of
Just tys' -> return (mkTyConApp tc tys')
Nothing | Just ty' <- tcView ty -> go cxt ty'
| otherwise -> Nothing
-- Failing that, try to expand a synonym
go cxt (CastTy ty co) = do { ty' <- go cxt ty
; co' <- go_co cxt co
; return (mkCastTy ty' co') }
go cxt (CoercionTy co) = do { co' <- go_co cxt co
; return (mkCoercionTy co') }
------------------
go_var cxt v = do { k' <- go cxt (varType v)
; return (setVarType v k') }
-- Works for TyVar and CoVar
-- See Note [Occurrence checking: look inside kinds]
------------------
go_co cxt (Refl r ty) = do { ty' <- go cxt ty
; return (mkReflCo r ty') }
-- Note: Coercions do not contain type synonyms
go_co cxt (TyConAppCo r tc args) = do { args' <- mapM (go_co cxt) args
; return (mkTyConAppCo r tc args') }
go_co cxt (AppCo co arg) = do { co' <- go_co cxt co
; arg' <- go_co cxt arg
; return (mkAppCo co' arg') }
go_co cxt@(as, env) (ForAllCo tv kind_co body_co)
= do { kind_co' <- go_co cxt kind_co
; let tv' = setTyVarKind tv $
pFst (coercionKind kind_co')
env' = extendVarEnv env tv tv'
as' = as `delVarSet` tv
; body' <- go_co (as', env') body_co
; return (ForAllCo tv' kind_co' body') }
go_co cxt (FunCo r co1 co2) = do { co1' <- go_co cxt co1
; co2' <- go_co cxt co2
; return (mkFunCo r co1' co2') }
go_co cxt (CoVarCo c) = 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' })) }
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
; ty1' <- go cxt ty1
; ty2' <- go cxt ty2
; return (mkUnivCo p' r ty1' ty2') }
go_co cxt (SymCo co) = do { co' <- go_co cxt co
; return (mkSymCo co') }
go_co cxt (TransCo co1 co2) = do { co1' <- go_co cxt co1
; co2' <- go_co cxt co2
; return (mkTransCo co1' co2') }
go_co cxt (NthCo r n co) = do { co' <- go_co cxt co
; return (mkNthCo r n co') }
go_co cxt (LRCo lr co) = do { co' <- go_co cxt co
; return (mkLRCo lr co') }
go_co cxt (InstCo co arg) = do { co' <- go_co cxt co
; arg' <- go_co cxt arg
; return (mkInstCo co' arg') }
go_co cxt (CoherenceCo co1 co2) = do { co1' <- go_co cxt co1
; co2' <- go_co cxt co2
; return (mkCoherenceCo co1' co2') }
go_co cxt (KindCo co) = do { co' <- go_co cxt co
; return (mkKindCo co') }
go_co cxt (SubCo co) = do { co' <- go_co cxt co
; return (mkSubCo co') }
go_co cxt (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co cxt) cs
; return (mkAxiomRuleCo ax cs') }
------------------
go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv
go_prov cxt (PhantomProv co) = PhantomProv <$> go_co cxt co
go_prov cxt (ProofIrrelProv co) = ProofIrrelProv <$> go_co cxt co
go_prov _ p@(PluginProv _) = return p
{-
%************************************************************************
%* *
......
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