\section[TcMonoType]{Typechecking user-specified @MonoTypes@}
\begin{code}
-module TcMonoType ( tcHsType, tcHsTypeKind, tcHsTopType, tcHsTopBoxedType,
- tcContext, tcHsTyVar, kcHsTyVar,
+module TcMonoType ( tcHsType, tcHsSigType, tcHsTypeKind, tcHsTopType, tcHsTopBoxedType, tcHsTopTypeKind,
+ tcContext, tcHsTyVar, kcHsTyVar, kcHsType,
tcExtendTyVarScope, tcExtendTopTyVarScope,
- TcSigInfo(..), tcTySig, mkTcSig, noSigs, maybeSig,
+ TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
checkSigTyVars, sigCtxt, sigPatCtxt
) where
#include "HsVersions.h"
-import HsSyn ( HsType(..), HsTyVar(..), Sig(..), pprClassAssertion, pprParendHsType )
+import HsSyn ( HsType(..), HsTyVar(..), MonoUsageAnn(..),
+ Sig(..), HsPred(..), pprHsPred, pprParendHsType )
import RnHsSyn ( RenamedHsType, RenamedContext, RenamedSig )
import TcHsSyn ( TcId )
import TcMonad
import TcEnv ( tcExtendTyVarEnv, tcLookupTy, tcGetValueEnv, tcGetInScopeTyVars,
- tcGetGlobalTyVars, TcTyThing(..)
+ tcExtendUVarEnv, tcLookupUVar,
+ tcGetGlobalTyVars, valueEnvIds, TcTyThing(..)
)
import TcType ( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
- typeToTcType, tcInstTcType, kindToTcKind,
- newKindVar,
- zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType
+ typeToTcType, kindToTcKind,
+ newKindVar, tcInstSigVar,
+ zonkTcKindToKind, zonkTcTypeToType, zonkTcTyVars, zonkTcType, zonkTcTyVar
)
import Inst ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr )
import TcUnify ( unifyKind, unifyKinds, unifyTypeKind )
-import Type ( Type, ThetaType,
- mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, zipFunTys,
- mkSigmaTy, mkDictTy, mkTyConApp, mkAppTys, splitRhoTy,
+import Type ( Type, PredType(..), ThetaType, UsageAnn(..),
+ mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, mkUsgTy,
+ mkUsForAllTy, zipFunTys, hoistForAllTys,
+ mkSigmaTy, mkDictTy, mkPredTy, mkTyConApp,
+ mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
boxedTypeKind, unboxedTypeKind, tyVarsOfType,
mkArrowKinds, getTyVar_maybe, getTyVar,
- tidyOpenType, tidyOpenTypes, tidyTyVar
+ tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
+ tyVarsOfType, tyVarsOfTypes, mkForAllTys
)
-import Id ( mkUserId, idName, idType, idFreeTyVars )
-import Var ( TyVar, mkTyVar )
+import PprType ( pprConstraint, pprType )
+import Subst ( mkTopTyVarSubst, substTy )
+import Id ( mkVanillaId, idName, idType, idFreeTyVars )
+import Var ( TyVar, mkTyVar, mkNamedUVar, varName )
import VarEnv
import VarSet
import Bag ( bagToList )
import TyCon ( TyCon )
import Name ( Name, OccName, isLocallyDefined )
import TysWiredIn ( mkListTy, mkTupleTy, mkUnboxedTupleTy )
+import UniqFM ( elemUFM, foldUFM )
import SrcLoc ( SrcLoc )
import Unique ( Unique, Uniquable(..) )
-import UniqFM ( eltsUFM )
-import Util ( zipWithEqual, zipLazy, mapAccumL )
+import Util ( mapAccumL, isSingleton )
import Outputable
\end{code}
tcHsType checks that the type really is of kind Type!
\begin{code}
+kcHsType :: RenamedHsType -> TcM c ()
+ -- Kind-check the type
+kcHsType ty = tc_type ty `thenTc_`
+ returnTc ()
+
+tcHsSigType :: RenamedHsType -> TcM s TcType
+ -- Used for type sigs written by the programmer
+ -- Hoist any inner for-alls to the top
+tcHsSigType ty
+ = tcHsType ty `thenTc` \ ty' ->
+ returnTc (hoistForAllTys ty')
+
tcHsType :: RenamedHsType -> TcM s TcType
tcHsType ty
= -- tcAddErrCtxt (typeCtxt ty) $
tcHsTopType ty
= -- tcAddErrCtxt (typeCtxt ty) $
tc_type ty `thenTc` \ ty' ->
- forkNF_Tc (zonkTcTypeToType ty')
+ forkNF_Tc (zonkTcTypeToType ty') `thenTc` \ ty'' ->
+ returnTc (hoistForAllTys ty'')
tcHsTopBoxedType :: RenamedHsType -> TcM s Type
tcHsTopBoxedType ty
= -- tcAddErrCtxt (typeCtxt ty) $
tc_boxed_type ty `thenTc` \ ty' ->
- forkNF_Tc (zonkTcTypeToType ty')
+ forkNF_Tc (zonkTcTypeToType ty') `thenTc` \ ty'' ->
+ returnTc (hoistForAllTys ty'')
+
+tcHsTopTypeKind :: RenamedHsType -> TcM s (TcKind, Type)
+tcHsTopTypeKind ty
+ = -- tcAddErrCtxt (typeCtxt ty) $
+ tc_type_kind ty `thenTc` \ (kind, ty') ->
+ forkNF_Tc (zonkTcTypeToType ty') `thenTc` \ zonked_ty ->
+ returnNF_Tc (kind, hoistForAllTys zonked_ty)
\end{code}
tc_type_kind :: RenamedHsType -> TcM s (TcKind, Type)
tc_type_kind ty@(MonoTyVar name)
= tc_app ty []
-
+
tc_type_kind (MonoListTy ty)
= tc_boxed_type ty `thenTc` \ tau_ty ->
returnTc (boxedTypeKind, mkListTy tau_ty)
tc_type_kind (MonoTyApp ty1 ty2)
= tc_app ty1 [ty2]
+tc_type_kind (MonoIParamTy n ty)
+ = tc_type ty `thenTc` \ tau ->
+ returnTc (boxedTypeKind, mkPredTy (IParam n tau))
+
tc_type_kind (MonoDictTy class_name tys)
- = tcClassAssertion (class_name, tys) `thenTc` \ (clas, arg_tys) ->
+ = tcClassAssertion (HsPClass class_name tys) `thenTc` \ (Class clas arg_tys) ->
returnTc (boxedTypeKind, mkDictTy clas arg_tys)
-tc_type_kind (HsForAllTy tv_names context ty)
- = tcExtendTyVarScope tv_names $ \ tyvars ->
+tc_type_kind (MonoUsgTy usg ty)
+ = newUsg usg `thenTc` \ usg' ->
+ tc_type_kind ty `thenTc` \ (kind, tc_ty) ->
+ returnTc (kind, mkUsgTy usg' tc_ty)
+ where
+ newUsg usg = case usg of
+ MonoUsOnce -> returnTc UsOnce
+ MonoUsMany -> returnTc UsMany
+ MonoUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
+ returnTc (UsVar uv)
+
+tc_type_kind (MonoUsgForAllTy uv_name ty)
+ = let
+ uv = mkNamedUVar uv_name
+ in
+ tcExtendUVarEnv uv_name uv $
+ tc_type_kind ty `thenTc` \ (kind, tc_ty) ->
+ returnTc (kind, mkUsForAllTy uv tc_ty)
+
+tc_type_kind (HsForAllTy (Just tv_names) context ty)
+ = tcExtendTyVarScope tv_names $ \ tyvars ->
tcContext context `thenTc` \ theta ->
- tc_boxed_type ty `thenTc` \ tau ->
- -- Body of a for-all is a boxed type!
- returnTc (boxedTypeKind, mkSigmaTy tyvars theta tau)
+ tc_type_kind ty `thenTc` \ (kind, tau) ->
+ tcGetInScopeTyVars `thenTc` \ in_scope_vars ->
+ let
+ body_kind | null theta = kind
+ | otherwise = boxedTypeKind
+ -- Context behaves like a function type
+ -- This matters. Return-unboxed-tuple analysis can
+ -- give overloaded functions like
+ -- f :: forall a. Num a => (# a->a, a->a #)
+ -- And we want these to get through the type checker
+ check ct@(Class c tys) | ambiguous = failWithTc (ambigErr (c,tys) tau)
+ where ct_vars = tyVarsOfTypes tys
+ forall_tyvars = map varName in_scope_vars
+ tau_vars = tyVarsOfType tau
+ ambig ct_var = (varName ct_var `elem` forall_tyvars) &&
+ not (ct_var `elemUFM` tau_vars)
+ ambiguous = foldUFM ((||) . ambig) False ct_vars
+ check _ = returnTc ()
+ in
+ mapTc check theta `thenTc_`
+ returnTc (body_kind, mkSigmaTy tyvars theta tau)
\end{code}
Help functions for type applications
mapTc tcClassAssertion context
where
- check_naughty (class_name, _)
+ check_naughty (HsPClass class_name _)
= checkTc (not (getUnique class_name `elem` cCallishClassKeys))
(naughtyCCallContextErr class_name)
+ check_naughty (HsPIParam _ _) = returnTc ()
-tcClassAssertion assn@(class_name, tys)
- = tcAddErrCtxt (appKindCtxt (pprClassAssertion assn)) $
+tcClassAssertion assn@(HsPClass class_name tys)
+ = tcAddErrCtxt (appKindCtxt (pprHsPred assn)) $
mapAndUnzipTc tc_type_kind tys `thenTc` \ (arg_kinds, arg_tys) ->
tcLookupTy class_name `thenTc` \ (kind, ~(Just arity), thing) ->
case thing of
-- Check with kind mis-match
checkTc (arity == n_tys) err `thenTc_`
unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind) `thenTc_`
- returnTc (clas, arg_tys)
+ returnTc (Class clas arg_tys)
where
n_tys = length tys
err = arityErr "Class" class_name arity n_tys
+tcClassAssertion assn@(HsPIParam name ty)
+ = tcAddErrCtxt (appKindCtxt (pprHsPred assn)) $
+ tc_type_kind ty `thenTc` \ (arg_kind, arg_ty) ->
+ returnTc (IParam name arg_ty)
\end{code}
SrcLoc -- Of the signature
+instance Outputable TcSigInfo where
+ ppr (TySigInfo nm id tyvars theta tau _ inst loc) =
+ ppr nm <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
-- Search for a particular signature
maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
| name == sig_name = Just sig
| otherwise = maybeSig sigs name
-
--- This little helper is useful to pass to tcPat
-noSigs :: Name -> Maybe TcId
-noSigs name = Nothing
\end{code}
tcTySig (Sig v ty src_loc)
= tcAddSrcLoc src_loc $
- tcHsType ty `thenTc` \ sigma_tc_ty ->
- mkTcSig (mkUserId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
+ tcHsSigType ty `thenTc` \ sigma_tc_ty ->
+ mkTcSig (mkVanillaId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig ->
returnTc sig
mkTcSig :: TcId -> SrcLoc -> NF_TcM s TcSigInfo
-- the tyvars *do* get unified with something, we want to carry on
-- typechecking the rest of the program with the function bound
-- to a pristine type, namely sigma_tc_ty
- tcInstTcType (idType poly_id) `thenNF_Tc` \ (tyvars, rho) ->
let
- (theta, tau) = splitRhoTy rho
- -- This splitSigmaTy tries hard to make sure that tau' is a type synonym
+ (tyvars, rho) = splitForAllTys (idType poly_id)
+ in
+ mapNF_Tc tcInstSigVar tyvars `thenNF_Tc` \ tyvars' ->
+ -- Make *signature* type variables
+
+ let
+ tyvar_tys' = mkTyVarTys tyvars'
+ rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
+ -- mkTopTyVarSubst because the tyvars' are fresh
+ (theta', tau') = splitRhoTy rho'
+ -- This splitRhoTy tries hard to make sure that tau' is a type synonym
-- wherever possible, which can improve interface files.
in
newMethodWithGivenTy SignatureOrigin
poly_id
- (mkTyVarTys tyvars)
- theta tau `thenNF_Tc` \ inst ->
+ tyvar_tys'
+ theta' tau' `thenNF_Tc` \ inst ->
-- We make a Method even if it's not overloaded; no harm
- returnNF_Tc (TySigInfo name poly_id tyvars theta tau (instToIdBndr inst) inst src_loc)
+ returnNF_Tc (TySigInfo name poly_id tyvars' theta' tau' (instToIdBndr inst) inst src_loc)
where
name = idName poly_id
\end{code}
give a helpful message in checkSigTyVars.
\begin{code}
-checkSigTyVars :: [TcTyVar] -- The original signature type variables
+checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature
+ -> TcTyVarSet -- Tyvars that are free in the type signature
+ -- These should *already* be in the global-var set, and are
+ -- used here only to improve the error message
-> TcM s [TcTyVar] -- Zonked signature type variables
-checkSigTyVars [] = returnTc []
+checkSigTyVars [] free = returnTc []
-checkSigTyVars sig_tyvars
+checkSigTyVars sig_tyvars free_tyvars
= zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys ->
tcGetGlobalTyVars `thenNF_Tc` \ globals ->
if tv `elemVarSet` globals -- Error (c)! Type variable escapes
-- The least comprehensible, so put it last
- then tcGetValueEnv `thenNF_Tc` \ ve ->
- find_globals tv env (eltsUFM ve) `thenNF_Tc` \ (env1, globs) ->
- returnNF_Tc (env1, acc, escape_msg sig_tyvar tv globs : msgs)
+ then tcGetValueEnv `thenNF_Tc` \ ve ->
+ find_globals tv env [] (valueEnvIds ve) `thenNF_Tc` \ (env1, globs) ->
+ find_frees tv env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (env2, frees) ->
+ returnNF_Tc (env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
else -- All OK
returnNF_Tc (env, extendVarEnv acc tv sig_tyvar, msgs)
-- whose types mention the offending type variable. It has to be
-- careful to zonk the Id's type first, so it has to be in the monad.
-- We must be careful to pass it a zonked type variable, too.
-find_globals tv tidy_env ids
- | null ids
- = returnNF_Tc (tidy_env, [])
+find_globals tv tidy_env acc []
+ = returnNF_Tc (tidy_env, acc)
-find_globals tv tidy_env (id:ids)
+find_globals tv tidy_env acc (id:ids)
| not (isLocallyDefined id) ||
isEmptyVarSet (idFreeTyVars id)
- = find_globals tv tidy_env ids
+ = find_globals tv tidy_env acc ids
| otherwise
= zonkTcType (idType id) `thenNF_Tc` \ id_ty ->
if tv `elemVarSet` tyVarsOfType id_ty then
let
(tidy_env', id_ty') = tidyOpenType tidy_env id_ty
+ acc' = (idName id, id_ty') : acc
in
- find_globals tv tidy_env' ids `thenNF_Tc` \ (tidy_env'', globs) ->
- returnNF_Tc (tidy_env'', (idName id, id_ty') : globs)
+ find_globals tv tidy_env' acc' ids
else
- find_globals tv tidy_env ids
-
-escape_msg sig_tv tv globs
- = vcat [mk_msg sig_tv <+> ptext SLIT("escapes"),
- pp_escape,
- ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
- nest 4 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
- ]
+ find_globals tv tidy_env acc ids
+
+find_frees tv tidy_env acc []
+ = returnNF_Tc (tidy_env, acc)
+find_frees tv tidy_env acc (ftv:ftvs)
+ = zonkTcTyVar ftv `thenNF_Tc` \ ty ->
+ if tv `elemVarSet` tyVarsOfType ty then
+ let
+ (tidy_env', ftv') = tidyTyVar tidy_env ftv
+ in
+ find_frees tv tidy_env' (ftv':acc) ftvs
+ else
+ find_frees tv tidy_env acc ftvs
+
+
+escape_msg sig_tv tv globs frees
+ = mk_msg sig_tv <+> ptext SLIT("escapes") $$
+ if not (null globs) then
+ vcat [pp_it <+> ptext SLIT("is mentioned in the environment"),
+ ptext SLIT("The following variables in the environment mention") <+> quotes (ppr tv),
+ nest 2 (vcat_first 10 [ppr name <+> dcolon <+> ppr ty | (name,ty) <- globs])
+ ]
+ else if not (null frees) then
+ vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees,
+ nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature"))
+ ]
+ else
+ empty -- Sigh. It's really hard to give a good error message
+ -- all the time. One bad case is an existential pattern match
where
- pp_escape | sig_tv /= tv = ptext SLIT("It unifies with") <+>
- quotes (ppr tv) <> comma <+>
- ptext SLIT("which is mentioned in the environment")
- | otherwise = ptext SLIT("It is mentioned in the environment")
+ is_are | isSingleton frees = ptext SLIT("is")
+ | otherwise = ptext SLIT("are")
+ pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which")
+ | otherwise = ptext SLIT("It")
vcat_first :: Int -> [SDoc] -> SDoc
vcat_first n [] = empty
These two context are used with checkSigTyVars
\begin{code}
-sigCtxt :: (Type -> Message) -> Type
+sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
-> TidyEnv -> NF_TcM s (TidyEnv, Message)
-sigCtxt mk_msg sig_ty tidy_env
- = let
- (env1, tidy_sig_ty) = tidyOpenType tidy_env sig_ty
+sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
+ = zonkTcType sig_tau `thenNF_Tc` \ actual_tau ->
+ let
+ (env1, tidy_sig_tyvars) = tidyTyVars tidy_env sig_tyvars
+ (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau)
+ (env3, tidy_actual_tau) = tidyOpenType env1 actual_tau
+ msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho),
+ ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau,
+ when
+ ]
in
- returnNF_Tc (env1, mk_msg tidy_sig_ty)
+ returnNF_Tc (env3, msg)
sigPatCtxt bound_tvs bound_ids tidy_env
= returnNF_Tc (env1,
tyVarAsClassErr name
= ptext SLIT("Type variable used as a class:") <+> ppr name
+
+ambigErr (c, ts) ty
+ = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprConstraint c ts),
+ nest 4 (ptext SLIT("for the type:") <+> ppr ty),
+ nest 4 (ptext SLIT("Each forall'd type variable mentioned by the constraint must appear after the =>."))]
\end{code}