Commit 8d49ef16 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Use new TcHsType.zonkSigType to establish Type invariants

Finally (I hope) fixes Trac #7903.

See Note [Zonking inside the knot] in TcHsSyn
parent 5949ff2d
......@@ -346,7 +346,7 @@ mkPrimTyConName occ key tycon = mkWiredInName gHC_PRIM (mkTcOccFS occ)
\begin{code}
kindTyConType :: TyCon -> Type
kindTyConType kind = TyConApp kind []
kindTyConType kind = TyConApp kind [] -- mkTyConApp isn't defined yet
-- | See "Type#kind_subtyping" for details of the distinction between these 'Kind's
anyKind, liftedTypeKind, unliftedTypeKind, openTypeKind, constraintKind, superKind :: Kind
......@@ -471,7 +471,7 @@ keep different state threads separate. It is represented by nothing at all.
\begin{code}
mkStatePrimTy :: Type -> Type
mkStatePrimTy ty = mkNakedTyConApp statePrimTyCon [ty]
mkStatePrimTy ty = TyConApp statePrimTyCon [ty]
statePrimTyCon :: TyCon -- See Note [The State# TyCon]
statePrimTyCon = pcPrimTyCon statePrimTyConName 1 VoidRep
......@@ -517,17 +517,17 @@ arrayArrayPrimTyCon = pcPrimTyCon0 arrayArrayPrimTyConName PtrRe
mutableArrayArrayPrimTyCon = pcPrimTyCon mutableArrayArrayPrimTyConName 1 PtrRep
mkArrayPrimTy :: Type -> Type
mkArrayPrimTy elt = mkNakedTyConApp arrayPrimTyCon [elt]
mkArrayPrimTy elt = TyConApp arrayPrimTyCon [elt]
byteArrayPrimTy :: Type
byteArrayPrimTy = mkTyConTy byteArrayPrimTyCon
mkArrayArrayPrimTy :: Type
mkArrayArrayPrimTy = mkTyConTy arrayArrayPrimTyCon
mkMutableArrayPrimTy :: Type -> Type -> Type
mkMutableArrayPrimTy s elt = mkNakedTyConApp mutableArrayPrimTyCon [s, elt]
mkMutableArrayPrimTy s elt = TyConApp mutableArrayPrimTyCon [s, elt]
mkMutableByteArrayPrimTy :: Type -> Type
mkMutableByteArrayPrimTy s = mkNakedTyConApp mutableByteArrayPrimTyCon [s]
mkMutableByteArrayPrimTy s = TyConApp mutableByteArrayPrimTyCon [s]
mkMutableArrayArrayPrimTy :: Type -> Type
mkMutableArrayArrayPrimTy s = mkNakedTyConApp mutableArrayArrayPrimTyCon [s]
mkMutableArrayArrayPrimTy s = TyConApp mutableArrayArrayPrimTyCon [s]
\end{code}
%************************************************************************
......@@ -541,7 +541,7 @@ mutVarPrimTyCon :: TyCon
mutVarPrimTyCon = pcPrimTyCon mutVarPrimTyConName 2 PtrRep
mkMutVarPrimTy :: Type -> Type -> Type
mkMutVarPrimTy s elt = mkNakedTyConApp mutVarPrimTyCon [s, elt]
mkMutVarPrimTy s elt = TyConApp mutVarPrimTyCon [s, elt]
\end{code}
%************************************************************************
......@@ -555,7 +555,7 @@ mVarPrimTyCon :: TyCon
mVarPrimTyCon = pcPrimTyCon mVarPrimTyConName 2 PtrRep
mkMVarPrimTy :: Type -> Type -> Type
mkMVarPrimTy s elt = mkNakedTyConApp mVarPrimTyCon [s, elt]
mkMVarPrimTy s elt = TyConApp mVarPrimTyCon [s, elt]
\end{code}
%************************************************************************
......@@ -569,7 +569,7 @@ tVarPrimTyCon :: TyCon
tVarPrimTyCon = pcPrimTyCon tVarPrimTyConName 2 PtrRep
mkTVarPrimTy :: Type -> Type -> Type
mkTVarPrimTy s elt = mkNakedTyConApp tVarPrimTyCon [s, elt]
mkTVarPrimTy s elt = TyConApp tVarPrimTyCon [s, elt]
\end{code}
%************************************************************************
......@@ -583,7 +583,7 @@ stablePtrPrimTyCon :: TyCon
stablePtrPrimTyCon = pcPrimTyCon stablePtrPrimTyConName 1 AddrRep
mkStablePtrPrimTy :: Type -> Type
mkStablePtrPrimTy ty = mkNakedTyConApp stablePtrPrimTyCon [ty]
mkStablePtrPrimTy ty = TyConApp stablePtrPrimTyCon [ty]
\end{code}
%************************************************************************
......@@ -597,7 +597,7 @@ stableNamePrimTyCon :: TyCon
stableNamePrimTyCon = pcPrimTyCon stableNamePrimTyConName 1 PtrRep
mkStableNamePrimTy :: Type -> Type
mkStableNamePrimTy ty = mkNakedTyConApp stableNamePrimTyCon [ty]
mkStableNamePrimTy ty = TyConApp stableNamePrimTyCon [ty]
\end{code}
%************************************************************************
......@@ -624,7 +624,7 @@ weakPrimTyCon :: TyCon
weakPrimTyCon = pcPrimTyCon weakPrimTyConName 1 PtrRep
mkWeakPrimTy :: Type -> Type
mkWeakPrimTy v = mkNakedTyConApp weakPrimTyCon [v]
mkWeakPrimTy v = TyConApp weakPrimTyCon [v]
\end{code}
%************************************************************************
......@@ -742,7 +742,7 @@ anyTyCon = mkSynTyCon anyTyConName kind [kKiVar]
-}
anyTypeOfKind :: Kind -> Type
anyTypeOfKind kind = mkNakedTyConApp anyTyCon [kind]
anyTypeOfKind kind = TyConApp anyTyCon [kind]
\end{code}
%************************************************************************
......
......@@ -1324,7 +1324,9 @@ zonkTcTypeToType env ty
= go ty
where
go (TyConApp tc tys) = do tys' <- mapM go tys
return (TyConApp tc tys')
return (mkTyConApp tc tys')
-- Establish Type invariants
-- See Note [Zonking inside the knot] in TcHsType
go (LitTy n) = return (LitTy n)
......
......@@ -45,7 +45,6 @@ import {-# SOURCE #-} TcSplice( tcSpliceType )
#endif
import HsSyn
import TcHsSyn ( zonkTcTypeToType, emptyZonkEnv )
import TcRnMonad
import TcEvidence( HsWrapper )
import TcEnv
......@@ -55,8 +54,8 @@ import TcUnify
import TcIface
import TcType
import Type
import TypeRep( Type(..) ) -- For the mkNakedXXX stuff
import Kind
import TypeRep( mkNakedTyConApp )
import Var
import VarSet
import TyCon
......@@ -185,7 +184,7 @@ tcHsSigTypeNC ctxt (L loc hs_ty)
; ty <- tcCheckHsTypeAndGen hs_ty kind
-- Zonk to expose kind information to checkValidType
; ty <- zonkTcType ty
; ty <- zonkSigType ty
; checkValidType ctxt ty
; return ty }
......@@ -197,7 +196,7 @@ tcHsInstHead user_ctxt lhs_ty@(L loc hs_ty)
do { inst_ty <- tc_inst_head hs_ty
; kvs <- zonkTcTypeAndFV inst_ty
; kvs <- kindGeneralize kvs
; inst_ty <- zonkTcType (mkForAllTys kvs inst_ty)
; inst_ty <- zonkSigType (mkForAllTys kvs inst_ty)
; checkValidInstance user_ctxt lhs_ty inst_ty }
tc_inst_head :: HsType Name -> TcM TcType
......@@ -219,7 +218,7 @@ tcHsDeriv hs_ty
-- Funny newtype deriving form
-- forall a. C [a]
-- where C has arity 2. Hence any-kinded result
; ty <- zonkTcType ty
; ty <- zonkSigType ty
; let (tvs, pred) = splitForAllTys ty
; case getClassPredTys_maybe pred of
Just (cls, tys) -> return (tvs, cls, tys)
......@@ -255,7 +254,7 @@ tcClassSigType :: LHsType Name -> TcM Type
tcClassSigType lhs_ty@(L _ hs_ty)
= addTypeCtxt lhs_ty $
do { ty <- tcCheckHsTypeAndGen hs_ty liftedTypeKind
; zonkTcTypeToType emptyZonkEnv ty }
; zonkSigType ty }
tcHsConArgType :: NewOrData -> LHsType Name -> TcM Type
-- Permit a bang, but discard it
......@@ -378,11 +377,11 @@ tc_hs_type hs_ty@(HsOpTy ty1 (_, l_op@(L _ op)) ty2) exp_kind
-- mkNakedAppTys: see Note [Zonking inside the knot]
tc_hs_type hs_ty@(HsAppTy ty1 ty2) exp_kind
| L _ (HsTyVar fun) <- fun_ty
, fun `hasKey` funTyConKey
, [fty1,fty2] <- arg_tys
= tc_fun_type hs_ty fty1 fty2 exp_kind
| otherwise
-- | L _ (HsTyVar fun) <- fun_ty
-- , fun `hasKey` funTyConKey
-- , [fty1,fty2] <- arg_tys
-- = tc_fun_type hs_ty fty1 fty2 exp_kind
-- | otherwise
= do { (fun_ty', fun_kind) <- tc_infer_lhs_type fun_ty
; arg_tys' <- tcCheckApps hs_ty fun_ty fun_kind arg_tys exp_kind
; return (mkNakedAppTys fun_ty' arg_tys') }
......@@ -704,10 +703,76 @@ can't change it. So we must traverse the type.
BUT the parent TyCon is knot-tied, so we can't look at it yet.
So we must be careful not to use "smart constructors" for types that
look at the TyCon or Class involved. Hence the use of mkNakedXXX
functions.
look at the TyCon or Class involved.
* Hence the use of mkNakedXXX functions. These do *not* enforce
the invariants (for example that we use (FunTy s t) rather
than (TyConApp (->) [s,t])).
* Ditto in zonkTcType (which may be applied more than once, eg to
squeeze out kind meta-variables), we are careful not to look at
the TyCon.
* We arrange to call zonkSigType *once* right at the end, and it
does establish the invariants. But in exchange we can't look
at the result (not even its structure) until we have emerged
from the "knot".
* TcHsSyn.zonkTcTypeToType also can safely check/establish
invariants.
This is sadly delicate.
This is horribly delicate. I hate it. A good example of how
delicate it is can be seen in Trac #7903.
\begin{code}
mkNakedTyConApp :: TyCon -> [Type] -> Type
-- Builds a TyConApp
-- * without being strict in TyCon,
-- * without satisfying the invariants of TyConApp
-- A subsequent zonking will establish the invariants
mkNakedTyConApp tc tys = TyConApp tc tys
mkNakedAppTys :: Type -> [Type] -> Type
mkNakedAppTys ty1 [] = ty1
mkNakedAppTys (TyConApp tc tys1) tys2 = mkNakedTyConApp tc (tys1 ++ tys2)
mkNakedAppTys ty1 tys2 = foldl AppTy ty1 tys2
zonkSigType :: TcType -> TcM TcType
-- Zonk the result of type-checking a user-written type signature
-- It may have kind varaibles in it, but no meta type variables
-- Because of knot-typing (see Note [Zonking inside the knot])
-- it may need to establish the Type invariants;
-- hence the use of mkTyConApp and mkAppTy
zonkSigType ty
= go ty
where
go (TyConApp tc tys) = do tys' <- mapM go tys
return (mkTyConApp tc tys')
-- Key point: establish Type invariants!
-- See Note [Zonking inside the knot]
go (LitTy n) = return (LitTy n)
go (FunTy arg res) = do arg' <- go arg
res' <- go res
return (FunTy arg' res')
go (AppTy fun arg) = do fun' <- go fun
arg' <- go arg
return (mkAppTy fun' arg')
-- NB the mkAppTy; we might have instantiated a
-- type variable to a type constructor, so we need
-- to pull the TyConApp to the top.
-- The two interesting cases!
go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
| otherwise = TyVarTy <$> updateTyVarKindM go tyvar
-- Ordinary (non Tc) tyvars occur inside quantified types
go (ForAllTy tv ty) = do { tv' <- zonkTcTyVarBndr tv
; ty' <- go ty
; return (ForAllTy tv' ty') }
\end{code}
Note [Body kind of a forall]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -1180,7 +1245,7 @@ tcHsPatSigType ctxt (HsWB { hswb_cts = hs_ty, hswb_kvs = sig_kvs, hswb_tvs = sig
; let ktv_binds = (sig_kvs `zip` kvs) ++ (sig_tvs `zip` tvs)
; sig_ty <- tcExtendTyVarEnv2 ktv_binds $
tcHsLiftedType hs_ty
; sig_ty <- zonkTcType sig_ty
; sig_ty <- zonkSigType sig_ty
; checkValidType ctxt sig_ty
; return (sig_ty, ktv_binds) }
where
......
......@@ -53,7 +53,7 @@ module TcMType (
skolemiseSigTv, skolemiseUnboundMetaTyVar,
zonkTcTyVar, zonkTcTyVars, zonkTyVarsAndFV, zonkTcTypeAndFV,
zonkQuantifiedTyVar, quantifyTyVars,
zonkTcType, zonkTcTypes, zonkTcThetaType,
zonkTcTyVarBndr, zonkTcType, zonkTcTypes, zonkTcThetaType,
zonkTcKind, defaultKindVarToStar,
zonkEvVar, zonkWC, zonkId, zonkCt, zonkCts, zonkSkolemInfo,
......@@ -932,6 +932,9 @@ zonkTcType ty
where
go (TyConApp tc tys) = do tys' <- mapM go tys
return (TyConApp tc tys')
-- Do NOT establish Type invariants, because
-- doing so is strict in the TyCOn.
-- See Note [Zonking inside the knot] in TcHsType
go (LitTy n) = return (LitTy n)
......@@ -945,6 +948,9 @@ zonkTcType ty
-- NB the mkAppTy; we might have instantiated a
-- type variable to a type constructor, so we need
-- to pull the TyConApp to the top.
-- OK to do this because only strict in the structure
-- not in the TyCon.
-- See Note [Zonking inside the knot] in TcHsType
-- The two interesting cases!
go (TyVarTy tyvar) | isTcTyVar tyvar = zonkTcTyVar tyvar
......
......@@ -22,7 +22,7 @@ module Type (
-- ** Constructing and deconstructing types
mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe,
mkAppTy, mkAppTys, mkNakedAppTys, splitAppTy, splitAppTys,
mkAppTy, mkAppTys, splitAppTy, splitAppTys,
splitAppTy_maybe, repSplitAppTy_maybe,
mkFunTy, mkFunTys, splitFunTy, splitFunTy_maybe,
......@@ -350,11 +350,6 @@ mkAppTys ty1 [] = ty1
mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
mkAppTys ty1 tys2 = foldl AppTy ty1 tys2
mkNakedAppTys :: Type -> [Type] -> Type
mkNakedAppTys ty1 [] = ty1
mkNakedAppTys (TyConApp tc tys1) tys2 = mkNakedTyConApp tc (tys1 ++ tys2)
mkNakedAppTys ty1 tys2 = foldl AppTy ty1 tys2
-------------
splitAppTy_maybe :: Type -> Maybe (Type, Type)
-- ^ Attempt to take a type application apart, whether it is a
......
......@@ -33,7 +33,7 @@ module TypeRep (
PredType, ThetaType, -- Synonyms
-- Functions over types
mkNakedTyConApp, mkTyConTy, mkTyVarTy, mkTyVarTys,
mkTyConTy, mkTyVarTy, mkTyVarTys,
isLiftedTypeKind, isSuperKind, isTypeVar, isKindVar,
-- Pretty-printing
......@@ -280,14 +280,6 @@ mkTyVarTy = TyVarTy
mkTyVarTys :: [TyVar] -> [Type]
mkTyVarTys = map mkTyVarTy -- a common use of mkTyVarTy
mkNakedTyConApp :: TyCon -> [Type] -> Type
-- Builds a TyConApp
-- * without being strict in TyCon,
-- * the TyCon should never be a saturated FunTyCon
-- Type.mkTyConApp is the usual one
mkNakedTyConApp tc tys
= TyConApp (ASSERT( not (isFunTyCon tc && length tys == 2) ) tc) tys
-- | Create the plain type constructor type which has been applied to no type arguments at all.
mkTyConTy :: TyCon -> Type
mkTyConTy tycon = TyConApp tycon []
......
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