From 469c3333ae5954cee58cdb1575b41fb1a3c34f06 Mon Sep 17 00:00:00 2001 From: simonpj Date: Thu, 28 Feb 2002 12:17:22 +0000 Subject: [PATCH] [project @ 2002-02-28 12:17:19 by simonpj] --------------------------------- Fix a rather obscure bug in tcGen --------------------------------- This bug concerns deciding when a type variable "escapes", and hence we can't generalise it. Our new subsumption-checking machinery for higher-ranked types requires a slightly more general approach than I had before. The main excitement is in TcUnify.checkSigTyVars and its friends. As usual, I moved functions around and cleaned things up a bit; hence the multi-module commit. --- ghc/compiler/typecheck/TcBinds.lhs | 4 +- ghc/compiler/typecheck/TcClassDcl.lhs | 18 ++-- ghc/compiler/typecheck/TcEnv.lhs | 4 +- ghc/compiler/typecheck/TcExpr.lhs | 10 ++- ghc/compiler/typecheck/TcForeign.lhs | 5 +- ghc/compiler/typecheck/TcHsSyn.lhs | 11 ++- ghc/compiler/typecheck/TcInstDcls.lhs | 5 +- ghc/compiler/typecheck/TcMType.lhs | 12 +-- ghc/compiler/typecheck/TcMatches.lhs | 43 ++++++--- ghc/compiler/typecheck/TcPat.lhs | 7 +- ghc/compiler/typecheck/TcType.lhs | 59 ++++++------- ghc/compiler/typecheck/TcUnify.lhs | 155 ++++++++++++++------------------- 12 files changed, 158 insertions(+), 175 deletions(-) diff --git a/ghc/compiler/typecheck/TcBinds.lhs b/ghc/compiler/typecheck/TcBinds.lhs index 8dad853..b677fe9 100644 --- a/ghc/compiler/typecheck/TcBinds.lhs +++ b/ghc/compiler/typecheck/TcBinds.lhs @@ -26,7 +26,7 @@ import Inst ( LIE, emptyLIE, mkLIE, plusLIE, InstOrigin(..), newDicts, instToId ) import TcEnv ( tcExtendLocalValEnv, newLocalName ) -import TcUnify ( unifyTauTyLists, checkSigTyVars, sigCtxt ) +import TcUnify ( unifyTauTyLists, checkSigTyVarsWrt, sigCtxt ) import TcSimplify ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyRestricted, tcSimplifyToDicts ) import TcMonoType ( tcHsSigType, UserTypeCtxt(..), TcSigInfo(..), tcTySig, maybeSig, tcAddScopedTyVars @@ -495,7 +495,7 @@ checkSigsTyVars sigs = mapTc_ check_one sigs tcAddErrCtxt (ptext SLIT("When checking the type signature for") <+> quotes (ppr id)) $ tcAddErrCtxtM (sigCtxt sig_tyvars sig_theta sig_tau) $ - checkSigTyVars sig_tyvars (idFreeTyVars id) + checkSigTyVarsWrt (idFreeTyVars id) sig_tyvars \end{code} @getTyVarsToGen@ decides what type variables to generalise over. diff --git a/ghc/compiler/typecheck/TcClassDcl.lhs b/ghc/compiler/typecheck/TcClassDcl.lhs index a89895a..3f32e87 100644 --- a/ghc/compiler/typecheck/TcClassDcl.lhs +++ b/ghc/compiler/typecheck/TcClassDcl.lhs @@ -25,8 +25,8 @@ import TcHsSyn ( TcMonoBinds ) import Inst ( Inst, InstOrigin(..), LIE, emptyLIE, plusLIE, plusLIEs, instToId, newDicts, newMethod ) -import TcEnv ( TyThingDetails(..), - tcLookupClass, tcExtendTyVarEnvForMeths, tcExtendGlobalTyVars, +import TcEnv ( TyThingDetails(..), tcExtendGlobalTyVars, + tcLookupClass, tcExtendTyVarEnvForMeths, tcExtendLocalValEnv, tcExtendTyVarEnv ) import TcBinds ( tcBindWithSigs, tcSpecSigs ) @@ -52,7 +52,6 @@ import NameEnv ( NameEnv, lookupNameEnv, emptyNameEnv, unitNameEnv, plusNameEnv import NameSet ( emptyNameSet ) import Outputable import Var ( TyVar ) -import VarSet ( mkVarSet, emptyVarSet ) import CmdLineOpts import ErrUtils ( dumpIfSet ) import Util ( count, isSingleton, lengthIs, equalLength ) @@ -438,10 +437,10 @@ tcDefMeth clas tyvars binds_in prags op_item@(sel_id, DefMeth dm_name) (ptext SLIT("class") <+> ppr clas) clas_tyvars [this_dict] - insts_needed `thenTc` \ (const_lie, dict_binds) -> + insts_needed `thenTc` \ (const_lie, dict_binds) -> -- Simplification can do unification - checkSigTyVars clas_tyvars emptyVarSet `thenTc` \ clas_tyvars' -> + checkSigTyVars clas_tyvars `thenTc` \ clas_tyvars' -> let full_bind = AbsBinds @@ -508,8 +507,9 @@ tcMethodBind clas origin inst_tyvars inst_tys inst_theta ) `thenTc` \ meth_bind -> -- Check the bindings; first add inst_tyvars to the envt -- so that we don't quantify over them in nested places - -- The *caller* put the class/inst decl tyvars into the envt - tcExtendGlobalTyVars (mkVarSet inst_tyvars) + -- The *caller* put the class/inst decl tyvars into the tyvar envt, + -- but not into the global tyvars, so that the call to checkSigTyVars below works ok + tcExtendGlobalTyVars inst_tyvars (tcAddErrCtxt (methodCtxt sel_id) $ tcBindWithSigs NotTopLevel meth_bind [sig_info] meth_prags NonRecursive @@ -531,9 +531,9 @@ tcMethodBind clas origin inst_tyvars inst_tys inst_theta -- ...and this is why the call to tcExtendGlobalTyVars must be here -- rather than in the caller tcAddErrCtxt (ptext SLIT("When checking the type of class method") - <+> quotes (ppr sel_id)) $ + <+> quotes (ppr sel_id)) $ tcAddErrCtxtM (sigCtxt inst_tyvars inst_theta (idType meth_id)) $ - checkSigTyVars inst_tyvars emptyVarSet `thenTc_` + checkSigTyVars inst_tyvars `thenTc_` returnTc (binds `AndMonoBinds` prag_binds1 `AndMonoBinds` prag_binds2, insts `plusLIE` prag_lie', diff --git a/ghc/compiler/typecheck/TcEnv.lhs b/ghc/compiler/typecheck/TcEnv.lhs index 5dc8b8b..fdcd99f 100644 --- a/ghc/compiler/typecheck/TcEnv.lhs +++ b/ghc/compiler/typecheck/TcEnv.lhs @@ -442,8 +442,8 @@ tcExtendLocalValEnv names_w_ids thing_inside \begin{code} tcExtendGlobalTyVars extra_global_tvs thing_inside - = tcGetEnv `thenNF_Tc` \ env -> - tc_extend_gtvs (tcTyVars env) extra_global_tvs `thenNF_Tc` \ gtvs' -> + = tcGetEnv `thenNF_Tc` \ env -> + tc_extend_gtvs (tcTyVars env) (mkVarSet extra_global_tvs) `thenNF_Tc` \ gtvs' -> tcSetEnv (env {tcTyVars = gtvs'}) thing_inside tc_extend_gtvs gtvs extra_global_tvs diff --git a/ghc/compiler/typecheck/TcExpr.lhs b/ghc/compiler/typecheck/TcExpr.lhs index 81614cb..252d995 100644 --- a/ghc/compiler/typecheck/TcExpr.lhs +++ b/ghc/compiler/typecheck/TcExpr.lhs @@ -52,7 +52,7 @@ import DataCon ( dataConFieldLabels, dataConSig, import Name ( Name ) import TyCon ( TyCon, tyConTyVars, isAlgTyCon, tyConDataCons ) import Subst ( mkTopTyVarSubst, substTheta, substTy ) -import VarSet ( elemVarSet ) +import VarSet ( emptyVarSet, elemVarSet ) import TysWiredIn ( boolTy, mkListTy, mkPArrTy, listTyCon, parrTyCon ) import PrelNames ( cCallableClassName, cReturnableClassName, @@ -85,7 +85,9 @@ tcExpr expr expected_ty = tcMonoExpr expr expected_ty | otherwise - = tcGen expected_ty (tcMonoExpr expr) `thenTc` \ (gen_fn, expr', lie) -> + = tcGen expected_ty emptyVarSet ( + tcMonoExpr expr + ) `thenTc` \ (gen_fn, expr', lie) -> returnTc (gen_fn <$> expr', lie) \end{code} @@ -129,12 +131,12 @@ tcMonoExpr (HsIPVar ip) res_ty \begin{code} tcMonoExpr in_expr@(ExprWithTySig expr poly_ty) res_ty = tcHsSigType ExprSigCtxt poly_ty `thenTc` \ sig_tc_ty -> - tcAddErrCtxt (exprSigCtxt in_expr) $ tcExpr expr sig_tc_ty `thenTc` \ (expr', lie1) -> -- Must instantiate the outer for-alls of sig_tc_ty -- else we risk instantiating a ? res_ty to a forall-type -- which breaks the invariant that tcMonoExpr only returns phi-types + tcAddErrCtxt (exprSigCtxt in_expr) $ tcInstCall SignatureOrigin sig_tc_ty `thenNF_Tc` \ (inst_fn, lie2, inst_sig_ty) -> tcSub res_ty inst_sig_ty `thenTc` \ (co_fn, lie3) -> @@ -1011,7 +1013,7 @@ caseScrutCtxt expr = hang (ptext SLIT("In the scrutinee of a case expression:")) 4 (ppr expr) exprSigCtxt expr - = hang (ptext SLIT("In an expression with a type signature:")) + = hang (ptext SLIT("When checking the type signature of the expression:")) 4 (ppr expr) listCtxt expr diff --git a/ghc/compiler/typecheck/TcForeign.lhs b/ghc/compiler/typecheck/TcForeign.lhs index b5a2de9..c943b44 100644 --- a/ghc/compiler/typecheck/TcForeign.lhs +++ b/ghc/compiler/typecheck/TcForeign.lhs @@ -26,7 +26,6 @@ import HsSyn ( HsDecl(..), ForeignDecl(..), HsExpr(..), import RnHsSyn ( RenamedHsDecl, RenamedForeignDecl ) import TcMonad -import TcEnv ( newLocalName ) import TcMonoType ( tcHsSigType, UserTypeCtxt(..) ) import TcHsSyn ( TcMonoBinds, TypecheckedForeignDecl, TcForeignExportDecl ) import TcExpr ( tcExpr ) @@ -38,7 +37,7 @@ import PrimRep ( getPrimRepSize, isFloatingRep ) import Module ( Module ) import Type ( typePrimRep ) import OccName ( mkForeignExportOcc ) -import Name ( Name(..), NamedThing(..), mkGlobalName ) +import Name ( NamedThing(..), mkGlobalName ) import TcType ( Type, tcSplitFunTys, tcSplitTyConApp_maybe, tcSplitForAllTys, isFFIArgumentTy, isFFIImportResultTy, @@ -46,7 +45,7 @@ import TcType ( Type, tcSplitFunTys, tcSplitTyConApp_maybe, isFFIExternalTy, isFFIDynArgumentTy, isFFIDynResultTy, isForeignPtrTy ) -import ForeignCall ( CCallSpec(..), CExportSpec(..), CCallTarget(..), +import ForeignCall ( CExportSpec(..), CCallTarget(..), isDynamicTarget, isCasmTarget ) import CStrings ( CLabelString, isCLabelString ) import PrelNames ( hasKey, ioTyConKey ) diff --git a/ghc/compiler/typecheck/TcHsSyn.lhs b/ghc/compiler/typecheck/TcHsSyn.lhs index d691ab4..2d01c49 100644 --- a/ghc/compiler/typecheck/TcHsSyn.lhs +++ b/ghc/compiler/typecheck/TcHsSyn.lhs @@ -48,8 +48,8 @@ import TcEnv ( tcLookupGlobal_maybe, tcExtendGlobalValEnv, TcEnv, TcId ) import TcMonad import Type ( Type ) -import TcType ( TcType ) -import TcMType ( zonkTcTypeToType, zonkTcTyVarToTyVar, zonkTcType, zonkTcSigTyVars ) +import TcType ( TcType, tcGetTyVar ) +import TcMType ( zonkTcTypeToType, zonkTcTyVarToTyVar, zonkTcType, zonkTcTyVars ) import TysPrim ( charPrimTy, intPrimTy, floatPrimTy, doublePrimTy, addrPrimTy ) @@ -352,9 +352,12 @@ zonkMonoBinds (AbsBinds tyvars dicts exports inlines val_bind) new_globals) where zonkExport (tyvars, global, local) - = zonkTcSigTyVars tyvars `thenNF_Tc` \ new_tyvars -> + = zonkTcTyVars tyvars `thenNF_Tc` \ tys -> + let + new_tyvars = map (tcGetTyVar "zonkExport") tys -- This isn't the binding occurrence of these tyvars - -- but they should *be* tyvars. Hence zonkTcSigTyVars. + -- but they should *be* tyvars. Hence tcGetTyVar. + in zonkIdBndr global `thenNF_Tc` \ new_global -> zonkIdOcc local `thenNF_Tc` \ new_local -> returnNF_Tc (new_tyvars, new_global, new_local) diff --git a/ghc/compiler/typecheck/TcInstDcls.lhs b/ghc/compiler/typecheck/TcInstDcls.lhs index d0335bc..97de0f2 100644 --- a/ghc/compiler/typecheck/TcInstDcls.lhs +++ b/ghc/compiler/typecheck/TcInstDcls.lhs @@ -52,7 +52,6 @@ import Subst ( substTheta ) import DataCon ( classDataCon ) import Class ( Class, classBigSig ) import Var ( idName, idType ) -import VarSet ( emptyVarSet ) import Id ( setIdLocalExported ) import MkId ( mkDictFunId, unsafeCoerceId, eRROR_ID ) import FunDeps ( checkInstFDs ) @@ -612,9 +611,9 @@ tcInstDecl2 (InstInfo { iDFunId = dfun_id, iBinds = monobinds, iPrags = uprags } dfun_arg_dicts -- NB! Don't include this_dict here, else the sc_dicts -- get bound by just selecting from this_dict!! (mkLIE sc_dicts) - ) `thenTc` \ (const_lie2, lie_binds2) -> + ) `thenTc` \ (const_lie2, lie_binds2) -> - checkSigTyVars inst_tyvars' emptyVarSet `thenNF_Tc` \ zonked_inst_tyvars -> + checkSigTyVars inst_tyvars' `thenNF_Tc` \ zonked_inst_tyvars -> -- Create the result bindings let diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index 49ef3f9..d91312d 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -31,7 +31,7 @@ module TcMType ( -------------------------------- -- Zonking - zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars, + zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType, zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv, @@ -49,7 +49,7 @@ import TcType ( TcType, TcThetaType, TcTauType, TcPredType, tcEqType, tcCmpPred, tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tcSplitForAllTys, - tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy, + tcIsTyVarTy, tcSplitSigmaTy, isUnLiftedType, isIPPred, mkAppTy, mkTyVarTy, mkTyVarTys, @@ -343,14 +343,6 @@ zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys -> zonkTcTyVar :: TcTyVar -> NF_TcM TcType zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar - -zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar] --- This guy is to zonk the tyvars we're about to feed into tcSimplify --- Usually this job is done by checkSigTyVars, but in a couple of places --- that is overkill, so we use this simpler chap -zonkTcSigTyVars tyvars - = zonkTcTyVars tyvars `thenNF_Tc` \ tys -> - returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys) \end{code} ----------------- Types diff --git a/ghc/compiler/typecheck/TcMatches.lhs b/ghc/compiler/typecheck/TcMatches.lhs index a99f936..7b02308 100644 --- a/ghc/compiler/typecheck/TcMatches.lhs +++ b/ghc/compiler/typecheck/TcMatches.lhs @@ -23,17 +23,18 @@ import TcHsSyn ( TcMatch, TcGRHSs, TcStmt, TcDictBinds, TypecheckedPat ) import TcMonad import TcMonoType ( tcAddScopedTyVars, tcHsSigType, UserTypeCtxt(..) ) import Inst ( LIE, isEmptyLIE, plusLIE, emptyLIE, plusLIEs, lieToList ) -import TcEnv ( TcId, tcLookupLocalIds, tcExtendLocalValEnv, tcExtendGlobalTyVars ) +import TcEnv ( TcId, tcLookupLocalIds, tcExtendLocalValEnv ) import TcPat ( tcPat, tcMonoPatBndr ) -import TcMType ( newTyVarTy ) -import TcType ( TcType, TcTyVar, tyVarsOfType, +import TcMType ( newTyVarTy, zonkTcType ) +import TcType ( TcType, TcTyVar, tyVarsOfType, tidyOpenTypes, tidyOpenType, mkFunTy, isOverloadedTy, liftedTypeKind, openTypeKind ) import TcBinds ( tcBindsAndThen ) -import TcUnify ( subFunTy, checkSigTyVars, tcSub, isIdCoercion, (<$>), sigPatCtxt ) +import TcUnify ( subFunTy, checkSigTyVarsWrt, tcSub, isIdCoercion, (<$>) ) import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns ) import Name ( Name ) import TysWiredIn ( boolTy ) import Id ( idType ) +import CoreFVs ( idFreeTyVars ) import BasicTypes ( RecFlag(..) ) import VarSet import Var ( Id ) @@ -109,11 +110,11 @@ tcMatches :: [(Name,Id)] -> TcType -> TcM ([TcMatch], LIE) -tcMatches xve fun_or_case matches expected_ty +tcMatches xve ctxt matches expected_ty = mapAndUnzipTc tc_match matches `thenTc` \ (matches, lies) -> returnTc (matches, plusLIEs lies) where - tc_match match = tcMatch xve fun_or_case match expected_ty + tc_match match = tcMatch xve ctxt match expected_ty \end{code} @@ -224,8 +225,8 @@ tcMatchPats pats expected_ty thing_inside in tcExtendLocalValEnv xve (thing_inside pats' rhs_ty) `thenTc` \ (result, lie_req2) -> - returnTc (rhs_ty, lie_req1, ex_tvs, pat_ids, lie_avail, result, lie_req2) - ) `thenTc` \ (rhs_ty, lie_req1, ex_tvs, pat_ids, lie_avail, result, lie_req2) -> + returnTc (lie_req1, ex_tvs, pat_ids, lie_avail, result, lie_req2) + ) `thenTc` \ (lie_req1, ex_tvs, pat_ids, lie_avail, result, lie_req2) -> -- STEP 4: Check for existentially bound type variables -- Do this *outside* the scope of the tcAddScopedTyVars, else checkSigTyVars @@ -260,8 +261,7 @@ tcCheckExistentialPat ids ex_tvs lie_avail lie_req match_ty returnTc (lie_req, EmptyMonoBinds) | otherwise - = tcExtendGlobalTyVars (tyVarsOfType match_ty) $ - tcAddErrCtxtM (sigPatCtxt tv_list ids) $ + = tcAddErrCtxtM (sigPatCtxt tv_list ids match_ty) $ -- In case there are any polymorpic, overloaded binders in the pattern -- (which can happen in the case of rank-2 type signatures, or data constructors @@ -270,7 +270,7 @@ tcCheckExistentialPat ids ex_tvs lie_avail lie_req match_ty -- Deal with overloaded functions bound by the pattern tcSimplifyCheck doc tv_list (lieToList lie_avail) lie1 `thenTc` \ (lie2, dict_binds) -> - checkSigTyVars tv_list emptyVarSet `thenTc_` + checkSigTyVarsWrt (tyVarsOfType match_ty) tv_list `thenTc_` returnTc (lie2, dict_binds `AndMonoBinds` inst_binds) where @@ -447,9 +447,26 @@ sameNoOfArgs matches = isSingleton (nub (map args_in_match matches)) \end{code} \begin{code} +varyingArgsErr name matches + = sep [ptext SLIT("Varying number of arguments for function"), quotes (ppr name)] + matchCtxt ctxt match = hang (pprMatchContext ctxt <> colon) 4 (pprMatch ctxt match) stmtCtxt do_or_lc stmt = hang (pprMatchContext do_or_lc <> colon) 4 (ppr stmt) -varyingArgsErr name matches - = sep [ptext SLIT("Varying number of arguments for function"), quotes (ppr name)] +sigPatCtxt bound_tvs bound_ids match_ty tidy_env + = zonkTcType match_ty `thenNF_Tc` \ match_ty' -> + let + (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids) + (env2, tidy_mty) = tidyOpenType env1 match_ty' + in + returnNF_Tc (env1, + sep [ptext SLIT("When checking an existential match that binds"), + nest 4 (vcat (zipWith ppr_id show_ids tidy_tys)), + ptext SLIT("and whose type is") <+> ppr tidy_mty]) + where + show_ids = filter is_interesting bound_ids + is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs + + ppr_id id ty = ppr id <+> dcolon <+> ppr ty + -- Don't zonk the types so we get the separate, un-unified versions \end{code} diff --git a/ghc/compiler/typecheck/TcPat.lhs b/ghc/compiler/typecheck/TcPat.lhs index 0e57a0c..a662f3c 100644 --- a/ghc/compiler/typecheck/TcPat.lhs +++ b/ghc/compiler/typecheck/TcPat.lhs @@ -150,8 +150,9 @@ tcPat tc_bndr WildPatIn pat_ty tcPat tc_bndr (ParPatIn parend_pat) pat_ty = tcPat tc_bndr parend_pat pat_ty -tcPat tc_bndr (SigPatIn pat sig) pat_ty - = tcHsSigType PatSigCtxt sig `thenTc` \ sig_ty -> +tcPat tc_bndr pat_in@(SigPatIn pat sig) pat_ty + = tcAddErrCtxt (patCtxt pat_in) $ + tcHsSigType PatSigCtxt sig `thenTc` \ sig_ty -> tcSubPat sig_ty pat_ty `thenTc` \ (co_fn, lie_sig) -> tcPat tc_bndr pat sig_ty `thenTc` \ (pat', lie_req, tvs, ids, lie_avail) -> returnTc (co_fn <$> pat', lie_req `plusLIE` lie_sig, tvs, ids, lie_avail) @@ -487,7 +488,7 @@ tcSubPat sig_ty exp_ty %************************************************************************ \begin{code} -patCtxt pat = hang (ptext SLIT("In the pattern:")) +patCtxt pat = hang (ptext SLIT("When checking the pattern:")) 4 (ppr pat) badFieldCon :: Name -> Name -> SDoc diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index b8f0878..1752026 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -46,6 +46,7 @@ module TcType ( isDoubleTy, isFloatTy, isIntTy, isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy, isTauTy, tcIsTyVarTy, tcIsForAllTy, + allDistinctTyVars, --------------------------------- -- Misc type manipulators @@ -74,7 +75,6 @@ module TcType ( --------------------------------- -- Unifier and matcher unifyTysX, unifyTyListsX, unifyExtendTysX, - allDistinctTyVars, matchTy, matchTys, match, -------------------------------- @@ -453,6 +453,31 @@ tcSplitDFunTy ty (tvs, theta, clas, tys) }} \end{code} +(allDistinctTyVars tys tvs) = True + iff +all the types tys are type variables, +distinct from each other and from tvs. + +This is useful when checking that unification hasn't unified signature +type variables. For example, if the type sig is + f :: forall a b. a -> b -> b +we want to check that 'a' and 'b' havn't + (a) been unified with a non-tyvar type + (b) been unified with each other (all distinct) + (c) been unified with a variable free in the environment + +\begin{code} +allDistinctTyVars :: [Type] -> TyVarSet -> Bool + +allDistinctTyVars [] acc + = True +allDistinctTyVars (ty:tys) acc + = case tcGetTyVar_maybe ty of + Nothing -> False -- (a) + Just tv | tv `elemVarSet` acc -> False -- (b) or (c) + | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv) +\end{code} + %************************************************************************ %* * @@ -886,38 +911,6 @@ boxedMarshalableTyCon tc %* * %************************************************************************ -(allDistinctTyVars tys tvs) = True - iff -all the types tys are type variables, -distinct from each other and from tvs. - -This is useful when checking that unification hasn't unified signature -type variables. For example, if the type sig is - f :: forall a b. a -> b -> b -we want to check that 'a' and 'b' havn't - (a) been unified with a non-tyvar type - (b) been unified with each other (all distinct) - (c) been unified with a variable free in the environment - -\begin{code} -allDistinctTyVars :: [Type] -> TyVarSet -> Bool - -allDistinctTyVars [] acc - = True -allDistinctTyVars (ty:tys) acc - = case tcGetTyVar_maybe ty of - Nothing -> False -- (a) - Just tv | tv `elemVarSet` acc -> False -- (b) or (c) - | otherwise -> allDistinctTyVars tys (acc `extendVarSet` tv) -\end{code} - - -%************************************************************************ -%* * -\subsection{Unification with an explicit substitution} -%* * -%************************************************************************ - Unify types with an explicit substitution and no monad. Ignore usage annotations. diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index 593a735..2cf985e 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -7,7 +7,7 @@ module TcUnify ( -- Full-blown subsumption tcSub, tcGen, subFunTy, - checkSigTyVars, sigCtxt, sigPatCtxt, + checkSigTyVars, checkSigTyVarsWrt, sigCtxt, -- Various unifications unifyTauTy, unifyTauTyList, unifyTauTyLists, @@ -25,8 +25,7 @@ module TcUnify ( import HsSyn ( HsExpr(..) ) -import TcHsSyn ( TypecheckedHsExpr, TcPat, - mkHsDictApp, mkHsTyApp, mkHsLet ) +import TcHsSyn ( TypecheckedHsExpr, TcPat, mkHsLet ) import TypeRep ( Type(..), SourceType(..), TyNote(..), openKindCon, typeCon ) @@ -36,34 +35,33 @@ import TcType ( TcKind, TcType, TcSigmaType, TcPhiType, TcTyVar, TcTauType, isTauTy, isSigmaTy, tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tcGetTyVar_maybe, tcGetTyVar, - mkTyConApp, mkTyVarTys, mkFunTy, tyVarsOfType, mkRhoTy, + mkTyConApp, mkFunTy, tyVarsOfType, mkRhoTy, typeKind, tcSplitFunTy_maybe, mkForAllTys, - isHoleTyVar, isSkolemTyVar, isUserTyVar, allDistinctTyVars, + isHoleTyVar, isSkolemTyVar, isUserTyVar, tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars, eqKind, openTypeKind, liftedTypeKind, isTypeKind, - hasMoreBoxityInfo, tyVarBindingInfo + hasMoreBoxityInfo, tyVarBindingInfo, allDistinctTyVars ) import qualified Type ( getTyVar_maybe ) -import Inst ( LIE, emptyLIE, plusLIE, mkLIE, +import Inst ( LIE, emptyLIE, plusLIE, newDicts, instToId, tcInstCall ) import TcMType ( getTcTyVar, putTcTyVar, tcInstType, newTyVarTy, newTyVarTys, newBoxityVar, newHoleTyVarTy, - zonkTcType, zonkTcTyVars, zonkTcTyVar ) + zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcTyVar ) import TcSimplify ( tcSimplifyCheck ) import TysWiredIn ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy ) -import TcEnv ( TcTyThing(..), tcExtendGlobalTyVars, tcGetGlobalTyVars, tcLEnvElts ) +import TcEnv ( TcTyThing(..), tcGetGlobalTyVars, tcLEnvElts ) import TyCon ( tyConArity, isTupleTyCon, tupleTyConBoxity ) import PprType ( pprType ) -import CoreFVs ( idFreeTyVars ) import Id ( mkSysLocal, idType ) import Var ( Var, varName, tyVarKind ) -import VarSet ( elemVarSet, varSetElems ) +import VarSet ( emptyVarSet, unionVarSet, elemVarSet, varSetElems ) import VarEnv import Name ( isSystemName, getSrcLoc ) import ErrUtils ( Message ) import BasicTypes ( Boxity, Arity, isBoxed ) -import Util ( isSingleton, equalLength ) +import Util ( equalLength ) import Maybe ( isNothing ) import Outputable \end{code} @@ -147,7 +145,9 @@ tc_sub _ (TyVarTy tv) act_sty act_ty tc_sub exp_sty expected_ty act_sty actual_ty | isSigmaTy expected_ty - = tcGen expected_ty ( + = tcGen expected_ty (tyVarsOfType actual_ty) ( + -- It's really important to check for escape wrt the free vars of + -- both expected_ty *and* actual_ty \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty ) `thenTc` \ (gen_fn, co_fn, lie) -> returnTc (gen_fn <.> co_fn, lie) @@ -262,12 +262,15 @@ imitateFun tv ty \begin{code} tcGen :: TcSigmaType -- expected_ty + -> TcTyVarSet -- Extra tyvars that the universally + -- quantified tyvars of expected_ty + -- must not be unified -> (TcPhiType -> TcM (result, LIE)) -- spec_ty -> TcM (ExprCoFn, result, LIE) -- The expression has type: spec_ty -> expected_ty -tcGen expected_ty thing_inside -- We expect expected_ty to be a forall-type - -- If not, the call is a no-op +tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type + -- If not, the call is a no-op = tcInstType expected_ty `thenNF_Tc` \ (forall_tvs, theta, phi_ty) -> -- Type-check the arg and unify with poly type @@ -284,12 +287,9 @@ tcGen expected_ty thing_inside -- We expect expected_ty to be a forall-type -- Conclusion: include the free vars of the expected_ty in the -- list of "free vars" for the signature check. - tcExtendGlobalTyVars free_tvs $ - tcAddErrCtxtM (sigCtxt forall_tvs theta phi_ty) $ - newDicts SignatureOrigin theta `thenNF_Tc` \ dicts -> tcSimplifyCheck sig_msg forall_tvs dicts lie `thenTc` \ (free_lie, inst_binds) -> - checkSigTyVars forall_tvs free_tvs `thenTc` \ zonked_tvs -> + checkSigTyVarsWrt free_tvs forall_tvs `thenTc` \ zonked_tvs -> let -- This HsLet binds any Insts which came out of the simplification. @@ -300,7 +300,7 @@ tcGen expected_ty thing_inside -- We expect expected_ty to be a forall-type in returnTc (mkCoercion co_fn, result, free_lie) where - free_tvs = tyVarsOfType expected_ty + free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs sig_msg = ptext SLIT("When generalising the type of an expression") \end{code} @@ -1000,20 +1000,32 @@ So we revert to ordinary type variables for signatures, and try to give a helpful message in checkSigTyVars. \begin{code} -checkSigTyVars :: [TcTyVar] -- Universally-quantified type variables in the signature - -> TcTyVarSet -- Tyvars that are free in the type signature - -- Not necessarily zonked - -- These should *already* be in the free-in-env set, - -- and are used here only to improve the error message - -> TcM [TcTyVar] -- Zonked signature type variables - -checkSigTyVars [] free = returnTc [] -checkSigTyVars sig_tyvars free_tyvars - = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys -> - tcGetGlobalTyVars `thenNF_Tc` \ globals -> - - checkTcM (allDistinctTyVars sig_tys globals) - (complain sig_tys globals) `thenTc_` +checkSigTyVars :: [TcTyVar] -> TcM [TcTyVar] +checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs + +checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM [TcTyVar] +checkSigTyVarsWrt extra_tvs sig_tvs + = zonkTcTyVarsAndFV (varSetElems extra_tvs) `thenNF_Tc` \ extra_tvs' -> + check_sig_tyvars extra_tvs' sig_tvs + +check_sig_tyvars + :: TcTyVarSet -- Global type variables. The universally quantified + -- tyvars should not mention any of these + -- Guaranteed already zonked. + -> [TcTyVar] -- Universally-quantified type variables in the signature + -- Not guaranteed zonked. + -> TcM [TcTyVar] -- Zonked signature type variables + +check_sig_tyvars extra_tvs [] + = returnTc [] +check_sig_tyvars extra_tvs sig_tvs + = zonkTcTyVars sig_tvs `thenNF_Tc` \ sig_tys -> + tcGetGlobalTyVars `thenNF_Tc` \ gbl_tvs -> + let + env_tvs = gbl_tvs `unionVarSet` extra_tvs + in + checkTcM (allDistinctTyVars sig_tys env_tvs) + (complain sig_tys env_tvs) `thenTc_` returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys) @@ -1024,9 +1036,9 @@ checkSigTyVars sig_tyvars free_tyvars (env2, emptyVarEnv, []) (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) -> - failWithTcM (env3, main_msg $$ vcat msgs) + failWithTcM (env3, main_msg $$ nest 4 (vcat msgs)) where - (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars + (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs (env2, tidy_tys) = tidyOpenTypes env1 sig_tys main_msg = ptext SLIT("Inferred type is less polymorphic than expected") @@ -1053,18 +1065,19 @@ checkSigTyVars sig_tyvars free_tyvars if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes -- The least comprehensible, so put it last -- Game plan: - -- a) get the local TcIds and TyVars from the environment, + -- get the local TcIds and TyVars from the environment, -- and pass them to find_globals (they might have tv free) - -- b) similarly, find any free_tyvars that mention tv - then tcGetEnv `thenNF_Tc` \ ve -> - find_globals tv tidy_env (tcLEnvElts ve) `thenNF_Tc` \ (tidy_env1, globs) -> - find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) -> - returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs) + then tcGetEnv `thenNF_Tc` \ ve -> + find_globals tv tidy_env (tcLEnvElts ve) `thenNF_Tc` \ (tidy_env1, globs) -> + returnNF_Tc (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs) else -- All OK returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs) }} +\end{code} + +\begin{code} ----------------------- -- find_globals looks at the value environment and finds values -- whose types mention the offending type variable. It has to be @@ -1108,7 +1121,7 @@ find_thing ignore_it tidy_env (ATyVar tv) else let (tidy_env1, tv1) = tidyOpenTyVar tidy_env tv (tidy_env2, tidy_ty) = tidyOpenType tidy_env1 tv_ty - msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at] + msg = sep [ppr tv1 <+> eq_stuff, nest 2 bound_at] eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty | otherwise = equals <+> ppr tv_ty @@ -1119,42 +1132,19 @@ find_thing ignore_it tidy_env (ATyVar tv) returnNF_Tc (tidy_env2, Just msg) ----------------------- -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') = tidyOpenTyVar 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 +escape_msg sig_tv tv globs = mk_msg sig_tv <+> ptext SLIT("escapes") $$ if not (null globs) then vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"), nest 2 (vcat 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 + -- all the time. One bad case is an existential pattern match. + -- We rely on the "When..." context to help. where - 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 - vcat_first 0 (x:xs) = text "...others omitted..." - vcat_first n (x:xs) = x $$ vcat_first (n-1) xs - unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv) @@ -1165,29 +1155,16 @@ These two context are used with checkSigTyVars \begin{code} sigCtxt :: [TcTyVar] -> TcThetaType -> TcTauType -> TidyEnv -> NF_TcM (TidyEnv, Message) -sigCtxt sig_tyvars sig_theta sig_tau tidy_env +sigCtxt sig_tvs sig_theta sig_tau tidy_env = zonkTcType sig_tau `thenNF_Tc` \ actual_tau -> let - (env1, tidy_sig_tyvars) = tidyOpenTyVars tidy_env sig_tyvars - (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau) - (env3, tidy_actual_tau) = tidyOpenType env2 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 + (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs + (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau) + (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau + sub_msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho), + ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau ] + msg = ptext SLIT("When trying to generalise an inferred type") $$ nest 4 sub_msg in returnNF_Tc (env3, msg) - -sigPatCtxt bound_tvs bound_ids tidy_env - = returnNF_Tc (env1, - sep [ptext SLIT("When checking a pattern that binds"), - nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))]) - where - show_ids = filter is_interesting bound_ids - is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs - - (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids) - ppr_id id ty = ppr id <+> dcolon <+> ppr ty - -- Don't zonk the types so we get the separate, un-unified versions \end{code} - - -- 1.7.10.4