From aaed11810cfb0f8890376142740e731cdf84c001 Mon Sep 17 00:00:00 2001 From: simonpj Date: Mon, 25 Mar 2002 15:08:39 +0000 Subject: [PATCH] [project @ 2002-03-25 15:08:38 by simonpj] ------------------------------- Fix bugs in rank-N polymorphism ------------------------------- Discussion with Mark showed up some bugs in the rank-N polymorphism stuff, especally concerning the treatment of 'hole' type variables. See especially TcMType: newHoleTyVar readHoleResult zapToType Also the treatment of conditionals and case branches is done right now, using zapToType --- ghc/compiler/typecheck/Inst.lhs | 8 +- ghc/compiler/typecheck/TcBinds.lhs | 9 +- ghc/compiler/typecheck/TcExpr.lhs | 35 ++++---- ghc/compiler/typecheck/TcMType.lhs | 53 +++++++++--- ghc/compiler/typecheck/TcMatches.lhs | 129 ++++++++++++++------------- ghc/compiler/typecheck/TcPat.lhs | 26 +++--- ghc/compiler/typecheck/TcType.lhs | 28 +++--- ghc/compiler/typecheck/TcUnify.lhs | 158 +++++++++++++++++++++------------- 8 files changed, 263 insertions(+), 183 deletions(-) diff --git a/ghc/compiler/typecheck/Inst.lhs b/ghc/compiler/typecheck/Inst.lhs index 09f9b51..ed0e665 100644 --- a/ghc/compiler/typecheck/Inst.lhs +++ b/ghc/compiler/typecheck/Inst.lhs @@ -47,7 +47,7 @@ import TcMType ( zonkTcType, zonkTcTypes, zonkTcPredType, import TcType ( Type, TcType, TcThetaType, TcPredType, TcTauType, TcTyVarSet, SourceType(..), PredType, ThetaType, TyVarDetails(VanillaTv), tcSplitForAllTys, tcSplitForAllTys, - tcSplitMethodTy, tcSplitRhoTy, tcFunArgTy, + tcSplitMethodTy, tcSplitPhiTy, tcFunArgTy, isIntTy,isFloatTy, isIntegerTy, isDoubleTy, tcIsTyVarTy, mkPredTy, mkTyVarTy, mkTyVarTys, tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tidyPred, @@ -399,7 +399,7 @@ newMethodAtLoc inst_loc real_id tys (tyvars,rho) = tcSplitForAllTys (idType real_id) rho_ty = ASSERT( equalLength tyvars tys ) substTy (mkTopTyVarSubst tyvars tys) rho - (theta, tau) = tcSplitRhoTy rho_ty + (theta, tau) = tcSplitPhiTy rho_ty in newMethodWith inst_loc real_id tys theta tau `thenNF_Tc` \ meth_inst -> returnNF_Tc (meth_inst, instToId meth_inst) @@ -565,7 +565,7 @@ lookupInst dict@(Dict _ (ClassP clas tys) loc) mapNF_Tc mk_ty_arg tyvars `thenNF_Tc` \ ty_args -> let dfun_rho = substTy (mkTyVarSubst tyvars ty_args) rho - (theta, _) = tcSplitRhoTy dfun_rho + (theta, _) = tcSplitPhiTy dfun_rho ty_app = mkHsTyApp (HsVar dfun_id) ty_args in if null theta then @@ -635,7 +635,7 @@ lookupSimpleInst clas tys -> returnNF_Tc (Just (substTheta (mkSubst emptyInScopeSet tenv) theta)) where (_, rho) = tcSplitForAllTys (idType dfun) - (theta,_) = tcSplitRhoTy rho + (theta,_) = tcSplitPhiTy rho other -> returnNF_Tc Nothing \end{code} diff --git a/ghc/compiler/typecheck/TcBinds.lhs b/ghc/compiler/typecheck/TcBinds.lhs index 7cda6b9..1d1e53e 100644 --- a/ghc/compiler/typecheck/TcBinds.lhs +++ b/ghc/compiler/typecheck/TcBinds.lhs @@ -34,7 +34,7 @@ import TcMonoType ( tcHsSigType, UserTypeCtxt(..), TcSigInfo(..), import TcPat ( tcPat, tcSubPat, tcMonoPatBndr ) import TcSimplify ( bindInstsOfLocalFuns ) import TcMType ( newTyVar, newTyVarTy, newHoleTyVarTy, - zonkTcTyVarToTyVar + zonkTcTyVarToTyVar, readHoleResult ) import TcType ( mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType, mkPredTy, mkForAllTy, isUnLiftedType, @@ -647,7 +647,7 @@ tcMonoBinds mbinds tc_ty_sigs is_rec let bndr_ty = idType bndr_id complete_it xve = tcAddSrcLoc locn $ - tcMatchesFun xve name bndr_ty matches `thenTc` \ (matches', lie) -> + tcMatchesFun xve name bndr_ty matches `thenTc` \ (matches', lie) -> returnTc (FunMonoBind bndr_id inf matches' locn, lie) in returnTc (complete_it, emptyLIE, emptyBag, unitBag (name, bndr_id), emptyLIE) @@ -665,11 +665,12 @@ tcMonoBinds mbinds tc_ty_sigs is_rec -- so we don't have to do anything here. tcPat tc_pat_bndr pat pat_ty `thenTc` \ (pat', lie_req, tvs, ids, lie_avail) -> + readHoleResult pat_ty `thenTc` \ pat_ty' -> let complete_it xve = tcAddSrcLoc locn $ tcAddErrCtxt (patMonoBindsCtxt bind) $ tcExtendLocalValEnv2 xve $ - tcGRHSs PatBindRhs grhss pat_ty `thenTc` \ (grhss', lie) -> + tcGRHSs PatBindRhs grhss pat_ty' `thenTc` \ (grhss', lie) -> returnTc (PatMonoBind pat' grhss' locn, lie) in returnTc (complete_it, lie_req, tvs, ids, lie_avail) @@ -689,7 +690,7 @@ tcMonoBinds mbinds tc_ty_sigs is_rec tcMonoPatBndr bndr_name pat_ty Just sig -> tcAddSrcLoc (getSrcLoc name) $ - tcSubPat pat_ty (idType mono_id) `thenTc` \ (co_fn, lie) -> + tcSubPat (idType mono_id) pat_ty `thenTc` \ (co_fn, lie) -> returnTc (co_fn, lie, mono_id) where mono_id = tcSigMonoId sig diff --git a/ghc/compiler/typecheck/TcExpr.lhs b/ghc/compiler/typecheck/TcExpr.lhs index d04eaea..e766564 100644 --- a/ghc/compiler/typecheck/TcExpr.lhs +++ b/ghc/compiler/typecheck/TcExpr.lhs @@ -15,7 +15,7 @@ import RnHsSyn ( RenamedHsExpr, RenamedRecordBinds ) import TcHsSyn ( TcExpr, TcRecordBinds, simpleHsLitTy ) import TcMonad -import TcUnify ( tcSub, tcGen, (<$>), +import TcUnify ( tcSubExp, tcGen, (<$>), unifyTauTy, unifyFunTy, unifyListTy, unifyPArrTy, unifyTupleTy ) import BasicTypes ( RecFlag(..), isMarkedStrict ) @@ -33,9 +33,9 @@ import TcMatches ( tcMatchesCase, tcMatchLambda, tcStmts ) import TcMonoType ( tcHsSigType, UserTypeCtxt(..) ) import TcPat ( badFieldCon ) import TcSimplify ( tcSimplifyIPs ) -import TcMType ( tcInstTyVars, tcInstType, newHoleTyVarTy, - newTyVarTy, newTyVarTys, zonkTcType ) -import TcType ( TcType, TcSigmaType, TcPhiType, TyVarDetails(VanillaTv), +import TcMType ( tcInstTyVars, tcInstType, newHoleTyVarTy, zapToType, + newTyVarTy, newTyVarTys, zonkTcType, readHoleResult ) +import TcType ( TcType, TcSigmaType, TcRhoType, TyVarDetails(VanillaTv), tcSplitFunTys, tcSplitTyConApp, mkTyVarTys, isSigmaTy, mkFunTy, mkAppTy, mkTyConTy, mkTyConApp, mkClassPred, tcFunArgTy, @@ -100,14 +100,14 @@ tcExpr expr expected_ty \begin{code} tcMonoExpr :: RenamedHsExpr -- Expession to type check - -> TcPhiType -- Expected type (could be a type variable) + -> TcRhoType -- Expected type (could be a type variable) -- Definitely no foralls at the top -- Can be a 'hole'. -> TcM (TcExpr, LIE) tcMonoExpr (HsVar name) res_ty = tcId name `thenNF_Tc` \ (expr', lie1, id_ty) -> - tcSub res_ty id_ty `thenTc` \ (co_fn, lie2) -> + tcSubExp res_ty id_ty `thenTc` \ (co_fn, lie2) -> returnTc (co_fn <$> expr', lie1 `plusLIE` lie2) tcMonoExpr (HsIPVar ip) res_ty @@ -117,7 +117,7 @@ tcMonoExpr (HsIPVar ip) res_ty -- be a tau-type.) newTyVarTy openTypeKind `thenNF_Tc` \ ip_ty -> newIPDict (IPOcc ip) ip ip_ty `thenNF_Tc` \ (ip', inst) -> - tcSub res_ty ip_ty `thenTc` \ (co_fn, lie) -> + tcSubExp res_ty ip_ty `thenTc` \ (co_fn, lie) -> returnNF_Tc (co_fn <$> HsIPVar ip', lie `plusLIE` unitLIE inst) \end{code} @@ -138,7 +138,7 @@ tcMonoExpr in_expr@(ExprWithTySig expr poly_ty) res_ty -- 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) -> + tcSubExp res_ty inst_sig_ty `thenTc` \ (co_fn, lie3) -> returnTc (co_fn <$> inst_fn expr', lie1 `plusLIE` lie2 `plusLIE` lie3) \end{code} @@ -182,7 +182,7 @@ tcMonoExpr in_expr@(SectionL arg1 op) res_ty split_fun_ty op_ty 2 {- two args -} `thenTc` \ ([arg1_ty, arg2_ty], op_res_ty) -> tcArg op (arg1, arg1_ty, 1) `thenTc` \ (arg1',lie2) -> tcAddErrCtxt (exprCtxt in_expr) $ - tcSub res_ty (mkFunTy arg2_ty op_res_ty) `thenTc` \ (co_fn, lie3) -> + tcSubExp res_ty (mkFunTy arg2_ty op_res_ty) `thenTc` \ (co_fn, lie3) -> returnTc (co_fn <$> SectionL arg1' op', lie1 `plusLIE` lie2 `plusLIE` lie3) -- Right sections, equivalent to \ x -> x op expr, or @@ -193,7 +193,7 @@ tcMonoExpr in_expr@(SectionR op arg2) res_ty split_fun_ty op_ty 2 {- two args -} `thenTc` \ ([arg1_ty, arg2_ty], op_res_ty) -> tcArg op (arg2, arg2_ty, 2) `thenTc` \ (arg2',lie2) -> tcAddErrCtxt (exprCtxt in_expr) $ - tcSub res_ty (mkFunTy arg1_ty op_res_ty) `thenTc` \ (co_fn, lie3) -> + tcSubExp res_ty (mkFunTy arg1_ty op_res_ty) `thenTc` \ (co_fn, lie3) -> returnTc (co_fn <$> SectionR op' arg2', lie1 `plusLIE` lie2 `plusLIE` lie3) -- equivalent to (op e1) e2: @@ -204,7 +204,7 @@ tcMonoExpr in_expr@(OpApp arg1 op fix arg2) res_ty tcArg op (arg1, arg1_ty, 1) `thenTc` \ (arg1',lie2a) -> tcArg op (arg2, arg2_ty, 2) `thenTc` \ (arg2',lie2b) -> tcAddErrCtxt (exprCtxt in_expr) $ - tcSub res_ty op_res_ty `thenTc` \ (co_fn, lie3) -> + tcSubExp res_ty op_res_ty `thenTc` \ (co_fn, lie3) -> returnTc (OpApp arg1' op' fix arg2', lie1 `plusLIE` lie2a `plusLIE` lie2b `plusLIE` lie3) \end{code} @@ -313,8 +313,11 @@ tcMonoExpr (HsIf pred b1 b2 src_loc) res_ty tcAddErrCtxt (predCtxt pred) ( tcMonoExpr pred boolTy ) `thenTc` \ (pred',lie1) -> - tcMonoExpr b1 res_ty `thenTc` \ (b1',lie2) -> - tcMonoExpr b2 res_ty `thenTc` \ (b2',lie3) -> + zapToType res_ty `thenTc` \ res_ty' -> + -- C.f. the call to zapToType in TcMatches.tcMatches + + tcMonoExpr b1 res_ty' `thenTc` \ (b1',lie2) -> + tcMonoExpr b2 res_ty' `thenTc` \ (b2',lie3) -> returnTc (HsIf pred' b1' b2' src_loc, plusLIE lie1 (plusLIE lie2 lie3)) \end{code} @@ -639,6 +642,7 @@ tcApp fun args res_ty tcExpr_id fun `thenTc` \ (fun', lie_fun, fun_ty) -> tcAddErrCtxt (wrongArgsCtxt "too many" fun args) ( + traceTc (text "tcApp" <+> (ppr fun $$ ppr fun_ty)) `thenNF_Tc_` split_fun_ty fun_ty (length args) ) `thenTc` \ (expected_arg_tys, actual_result_ty) -> @@ -652,7 +656,7 @@ tcApp fun args res_ty -- (One can think of cases when the opposite order would give -- a better error message.) tcAddErrCtxtM (checkArgsCtxt fun args res_ty actual_result_ty) - (tcSub res_ty actual_result_ty) `thenTc` \ (co_fn, lie_res) -> + (tcSubExp res_ty actual_result_ty) `thenTc` \ (co_fn, lie_res) -> returnTc (co_fn <$> foldl HsApp fun' args', lie_res `plusLIE` lie_fun `plusLIE` plusLIEs lie_args_s) @@ -781,7 +785,8 @@ tcExpr_id :: RenamedHsExpr -> TcM (TcExpr, LIE, TcType) tcExpr_id (HsVar name) = tcId name tcExpr_id expr = newHoleTyVarTy `thenNF_Tc` \ id_ty -> tcMonoExpr expr id_ty `thenTc` \ (expr', lie_id) -> - returnTc (expr', lie_id, id_ty) + readHoleResult id_ty `thenTc` \ id_ty' -> + returnTc (expr', lie_id, id_ty') \end{code} diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index c64e405..451e3fc 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -11,12 +11,14 @@ module TcMType ( -------------------------------- -- Creating new mutable type variables - newTyVar, newHoleTyVarTy, + newTyVar, newTyVarTy, -- Kind -> NF_TcM TcType newTyVarTys, -- Int -> Kind -> NF_TcM [TcType] newKindVar, newKindVars, newBoxityVar, putTcTyVar, getTcTyVar, + newHoleTyVarTy, readHoleResult, zapToType, + -------------------------------- -- Instantiation tcInstTyVar, tcInstTyVars, tcInstType, @@ -45,10 +47,10 @@ import TypeRep ( Type(..), SourceType(..), TyNote(..), -- Friend; can see repr import TcType ( TcType, TcThetaType, TcTauType, TcPredType, TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..), tcEqType, tcCmpPred, - tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, + tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tcSplitForAllTys, tcIsTyVarTy, tcSplitSigmaTy, - isUnLiftedType, isIPPred, + isUnLiftedType, isIPPred, isHoleTyVar, mkAppTy, mkTyVarTy, mkTyVarTys, tyVarsOfPred, getClassPredTys_maybe, @@ -106,11 +108,6 @@ newTyVarTy kind = newTyVar kind `thenNF_Tc` \ tc_tyvar -> returnNF_Tc (TyVarTy tc_tyvar) -newHoleTyVarTy :: NF_TcM TcType - = tcGetUnique `thenNF_Tc` \ uniq -> - tcNewMutTyVar (mkSystemName uniq FSLIT("h")) openTypeKind HoleTv `thenNF_Tc` \ tv -> - returnNF_Tc (TyVarTy tv) - newTyVarTys :: Int -> Kind -> NF_TcM [TcType] newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind) @@ -133,6 +130,42 @@ newBoxityVar %************************************************************************ %* * +\subsection{'hole' type variables} +%* * +%************************************************************************ + +\begin{code} +newHoleTyVarTy :: NF_TcM TcType + = tcGetUnique `thenNF_Tc` \ uniq -> + tcNewMutTyVar (mkSystemName uniq FSLIT("h")) openTypeKind HoleTv `thenNF_Tc` \ tv -> + returnNF_Tc (TyVarTy tv) + +readHoleResult :: TcType -> NF_TcM TcType +-- Read the answer out of a hole, constructed by newHoleTyVarTy +readHoleResult (TyVarTy tv) + = ASSERT( isHoleTyVar tv ) + getTcTyVar tv `thenNF_Tc` \ maybe_res -> + case maybe_res of + Just ty -> returnNF_Tc ty + Nothing -> pprPanic "readHoleResult: empty" (ppr tv) +readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty) + +zapToType :: TcType -> NF_TcM TcType +zapToType (TyVarTy tv) + | isHoleTyVar tv + = getTcTyVar tv `thenNF_Tc` \ maybe_res -> + case maybe_res of + Nothing -> newTyVarTy openTypeKind `thenNF_Tc` \ ty -> + putTcTyVar tv ty `thenNF_Tc_` + returnNF_Tc ty + Just ty -> returnNF_Tc ty -- No need to loop; we never + -- have chains of holes + +zapToType other_ty = returnNF_Tc other_ty +\end{code} + +%************************************************************************ +%* * \subsection{Type instantiation} %* * %************************************************************************ @@ -175,13 +208,13 @@ tcInstType tv_details ty ([], rho) -> -- There may be overloading despite no type variables; -- (?x :: Int) => Int -> Int let - (theta, tau) = tcSplitRhoTy rho + (theta, tau) = tcSplitPhiTy rho in returnNF_Tc ([], theta, tau) (tyvars, rho) -> tcInstTyVars tv_details tyvars `thenNF_Tc` \ (tyvars', _, tenv) -> let - (theta, tau) = tcSplitRhoTy (substTy tenv rho) + (theta, tau) = tcSplitPhiTy (substTy tenv rho) in returnNF_Tc (tyvars', theta, tau) \end{code} diff --git a/ghc/compiler/typecheck/TcMatches.lhs b/ghc/compiler/typecheck/TcMatches.lhs index bd223b4..f8f2f4b 100644 --- a/ghc/compiler/typecheck/TcMatches.lhs +++ b/ghc/compiler/typecheck/TcMatches.lhs @@ -25,11 +25,11 @@ import TcMonoType ( tcAddScopedTyVars, tcHsSigType, UserTypeCtxt(..) ) import Inst ( LIE, isEmptyLIE, plusLIE, emptyLIE, plusLIEs, lieToList ) import TcEnv ( TcId, tcLookupLocalIds, tcExtendLocalValEnv2 ) import TcPat ( tcPat, tcMonoPatBndr ) -import TcMType ( newTyVarTy, zonkTcType ) +import TcMType ( newTyVarTy, zonkTcType, zapToType ) import TcType ( TcType, TcTyVar, tyVarsOfType, tidyOpenTypes, tidyOpenType, mkFunTy, isOverloadedTy, liftedTypeKind, openTypeKind ) import TcBinds ( tcBindsAndThen ) -import TcUnify ( subFunTy, checkSigTyVarsWrt, tcSub, isIdCoercion, (<$>) ) +import TcUnify ( subFunTy, checkSigTyVarsWrt, tcSubExp, isIdCoercion, (<$>) ) import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns ) import Name ( Name ) import TysWiredIn ( boolTy ) @@ -39,7 +39,7 @@ import BasicTypes ( RecFlag(..) ) import VarSet import Var ( Id ) import Bag -import Util ( isSingleton ) +import Util ( isSingleton, lengthExceeds ) import Outputable import List ( nub ) @@ -111,10 +111,18 @@ tcMatches :: [(Name,Id)] -> TcM ([TcMatch], LIE) tcMatches xve ctxt matches expected_ty - = mapAndUnzipTc tc_match matches `thenTc` \ (matches, lies) -> + = -- If there is more than one branch, and expected_ty is a 'hole', + -- all branches must be types, not type schemes, otherwise the + -- in which we check them would affect the result. + (if lengthExceeds matches 1 then + zapToType expected_ty + else + returnNF_Tc expected_ty) `thenNF_Tc` \ expected_ty' -> + + mapAndUnzipTc (tc_match expected_ty') matches `thenTc` \ (matches, lies) -> returnTc (matches, plusLIEs lies) where - tc_match match = tcMatch xve ctxt match expected_ty + tc_match expected_ty match = tcMatch xve ctxt match expected_ty \end{code} @@ -138,25 +146,23 @@ tcMatch :: [(Name,Id)] tcMatch xve1 ctxt match@(Match pats maybe_rhs_sig grhss) expected_ty = tcAddSrcLoc (getMatchLoc match) $ -- At one stage I removed this; tcAddErrCtxt (matchCtxt ctxt match) $ -- I'm not sure why, so I put it back - - tcMatchPats pats expected_ty tc_grhss `thenTc` \ ((pats', grhss'), lie, ex_binds) -> + tcMatchPats pats expected_ty tc_grhss `thenTc` \ (pats', grhss', lie, ex_binds) -> returnTc (Match pats' Nothing (glue_on Recursive ex_binds grhss'), lie) where - tc_grhss pats' rhs_ty + tc_grhss rhs_ty = tcExtendLocalValEnv2 xve1 $ -- Deal with the result signature case maybe_rhs_sig of - Nothing -> tcGRHSs ctxt grhss rhs_ty `thenTc` \ (grhss', lie) -> - returnTc ((pats', grhss'), lie) + Nothing -> tcGRHSs ctxt grhss rhs_ty Just sig -> tcAddScopedTyVars [sig] $ -- Bring into scope the type variables in the signature tcHsSigType ResSigCtxt sig `thenTc` \ sig_ty -> tcGRHSs ctxt grhss sig_ty `thenTc` \ (grhss', lie1) -> - tcSub rhs_ty sig_ty `thenTc` \ (co_fn, lie2) -> - returnTc ((pats', lift_grhss co_fn rhs_ty grhss'), + tcSubExp rhs_ty sig_ty `thenTc` \ (co_fn, lie2) -> + returnTc (lift_grhss co_fn rhs_ty grhss', lie1 `plusLIE` lie2) -- lift_grhss pushes the coercion down to the right hand sides, @@ -204,8 +210,8 @@ tcGRHSs ctxt (GRHSs grhss binds _) expected_ty \begin{code} tcMatchPats :: [RenamedPat] -> TcType - -> ([TypecheckedPat] -> TcType -> TcM (a, LIE)) - -> TcM (a, LIE, TcDictBinds) + -> (TcType -> TcM (a, LIE)) + -> TcM ([TypecheckedPat], a, LIE, TcDictBinds) -- Typecheck the patterns, extend the environment to bind the variables, -- do the thing inside, use any existentially-bound dictionaries to -- discharge parts of the returning LIE, and deal with pattern type @@ -216,17 +222,10 @@ tcMatchPats pats expected_ty thing_inside tcAddScopedTyVars (collectSigTysFromPats pats) ( -- STEP 2: Typecheck the patterns themselves, gathering all the stuff - tc_match_pats pats expected_ty `thenTc` \ (rhs_ty, pats', lie_req1, ex_tvs, pat_bndrs, lie_avail) -> - - -- STEP 3: Extend the environment, and do the thing inside - let - xve = bagToList pat_bndrs - pat_ids = map snd xve - in - tcExtendLocalValEnv2 xve (thing_inside pats' rhs_ty) `thenTc` \ (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) -> + -- then do the thing inside + tc_match_pats pats expected_ty thing_inside + + ) `thenTc` \ (pats', lie_req, ex_tvs, ex_ids, ex_lie, result) -> -- STEP 4: Check for existentially bound type variables -- Do this *outside* the scope of the tcAddScopedTyVars, else checkSigTyVars @@ -235,66 +234,77 @@ tcMatchPats pats expected_ty thing_inside -- I'm a bit concerned that lie_req1 from an 'inner' pattern in the list -- might need (via lie_req2) something made available from an 'outer' -- pattern. But it's inconvenient to deal with, and I can't find an example - tcCheckExistentialPat pat_ids ex_tvs lie_avail lie_req2 expected_ty `thenTc` \ (lie_req2', ex_binds) -> + tcCheckExistentialPat ex_tvs ex_ids ex_lie lie_req expected_ty `thenTc` \ (lie_req', ex_binds) -> -- NB: we *must* pass "expected_ty" not "result_ty" to tcCheckExistentialPat -- For example, we must reject this program: -- data C = forall a. C (a -> Int) -- f (C g) x = g x -- Here, result_ty will be simply Int, but expected_ty is (a -> Int). - returnTc (result, lie_req1 `plusLIE` lie_req2', ex_binds) + returnTc (pats', result, lie_req', ex_binds) + +tc_match_pats [] expected_ty thing_inside + = thing_inside expected_ty `thenTc` \ (answer, lie) -> + returnTc ([], lie, emptyBag, [], emptyLIE, answer) + +tc_match_pats (pat:pats) expected_ty thing_inside + = subFunTy expected_ty $ \ arg_ty rest_ty -> + -- This is the unique place we call subFunTy + -- The point is that if expected_y is a "hole", we want + -- to make arg_ty and rest_ty as "holes" too. + tcPat tcMonoPatBndr pat arg_ty `thenTc` \ (pat', lie_req, ex_tvs, pat_bndrs, ex_lie) -> + let + xve = bagToList pat_bndrs + ex_ids = [id | (_, id) <- xve] + -- ex_ids is all the pattern-bound Ids, a superset + -- of the existential Ids used in checkExistentialPat + in + tcExtendLocalValEnv2 xve $ + tc_match_pats pats rest_ty thing_inside `thenTc` \ (pats', lie_reqs, exs_tvs, exs_ids, exs_lie, answer) -> + returnTc ( pat':pats', + lie_req `plusLIE` lie_reqs, + ex_tvs `unionBags` exs_tvs, + ex_ids ++ exs_ids, + ex_lie `plusLIE` exs_lie, + answer + ) + -tcCheckExistentialPat :: [TcId] -- Ids bound by this pattern - -> Bag TcTyVar -- Existentially quantified tyvars bound by pattern +tcCheckExistentialPat :: Bag TcTyVar -- Existentially quantified tyvars bound by pattern + -> [TcId] -- Ids bound by this pattern; used + -- (a) by bindsInstsOfLocalFuns + -- (b) to generate helpful error messages -> LIE -- and context -> LIE -- Required context -> TcType -- and type of the Match; vars in here must not escape -> TcM (LIE, TcDictBinds) -- LIE to float out and dict bindings -tcCheckExistentialPat ids ex_tvs lie_avail lie_req match_ty - | isEmptyBag ex_tvs && all not_overloaded ids +tcCheckExistentialPat ex_tvs ex_ids ex_lie lie_req match_ty + | isEmptyBag ex_tvs && all not_overloaded ex_ids -- Short cut for case when there are no existentials -- and no polymorphic overloaded variables -- e.g. f :: (forall a. Ord a => a -> a) -> Int -> Int -- f op x = .... -- Here we must discharge op Methods - = ASSERT( isEmptyLIE lie_avail ) + = ASSERT( isEmptyLIE ex_lie ) returnTc (lie_req, EmptyMonoBinds) | otherwise - = tcAddErrCtxtM (sigPatCtxt tv_list ids match_ty) $ + = tcAddErrCtxtM (sigPatCtxt tv_list ex_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 -- with polymorphic arguments), we must do a bindInstsOfLocalFns here - bindInstsOfLocalFuns lie_req ids `thenTc` \ (lie1, inst_binds) -> + bindInstsOfLocalFuns lie_req ex_ids `thenTc` \ (lie1, inst_binds) -> -- Deal with overloaded functions bound by the pattern - tcSimplifyCheck doc tv_list (lieToList lie_avail) lie1 `thenTc` \ (lie2, dict_binds) -> - checkSigTyVarsWrt (tyVarsOfType match_ty) tv_list `thenTc_` + tcSimplifyCheck doc tv_list (lieToList ex_lie) lie1 `thenTc` \ (lie2, dict_binds) -> + checkSigTyVarsWrt (tyVarsOfType match_ty) tv_list `thenTc_` returnTc (lie2, dict_binds `AndMonoBinds` inst_binds) where doc = text ("the existential context of a data constructor") tv_list = bagToList ex_tvs not_overloaded id = not (isOverloadedTy (idType id)) - -tc_match_pats [] expected_ty - = returnTc (expected_ty, [], emptyLIE, emptyBag, emptyBag, emptyLIE) - -tc_match_pats (pat:pats) expected_ty - = subFunTy expected_ty `thenTc` \ (arg_ty, rest_ty) -> - -- This is the unique place we call subFunTy - -- The point is that if expected_y is a "hole", we want - -- to make arg_ty and rest_ty as "holes" too. - tcPat tcMonoPatBndr pat arg_ty `thenTc` \ (pat', lie_req, pat_tvs, pat_ids, lie_avail) -> - tc_match_pats pats rest_ty `thenTc` \ (rhs_ty, pats', lie_reqs, pats_tvs, pats_ids, lie_avails) -> - returnTc ( rhs_ty, - pat':pats', - lie_req `plusLIE` lie_reqs, - pat_tvs `unionBags` pats_tvs, - pat_ids `unionBags` pats_ids, - lie_avail `plusLIE` lie_avails - ) \end{code} @@ -359,12 +369,11 @@ tcStmtAndThen combine do_or_lc m_ty@(m,elt_ty) stmt@(BindStmt pat exp src_loc) t tcAddErrCtxt (stmtCtxt do_or_lc stmt) $ newTyVarTy liftedTypeKind `thenNF_Tc` \ pat_ty -> tcMonoExpr exp (m pat_ty) `thenTc` \ (exp', exp_lie) -> - tcMatchPats [pat] (mkFunTy pat_ty (m elt_ty)) (\ [pat'] _ -> - tcPopErrCtxt $ - thing_inside `thenTc` \ (thing, lie) -> - returnTc ((BindStmt pat' exp' src_loc, thing), lie) - ) `thenTc` \ ((stmt', thing), lie, dict_binds) -> - returnTc (combine stmt' (glue_binds combine Recursive dict_binds thing), + tcMatchPats [pat] (mkFunTy pat_ty (m elt_ty)) (\ _ -> + tcPopErrCtxt thing_inside + ) `thenTc` \ ([pat'], thing, lie, dict_binds) -> + returnTc (combine (BindStmt pat' exp' src_loc) + (glue_binds combine Recursive dict_binds thing), lie `plusLIE` exp_lie) diff --git a/ghc/compiler/typecheck/TcPat.lhs b/ghc/compiler/typecheck/TcPat.lhs index 9f7dbc0..cb08317 100644 --- a/ghc/compiler/typecheck/TcPat.lhs +++ b/ghc/compiler/typecheck/TcPat.lhs @@ -23,12 +23,13 @@ import Id ( mkLocalId, mkSysLocal ) import Name ( Name ) import FieldLabel ( fieldLabelName ) import TcEnv ( tcLookupClass, tcLookupDataCon, tcLookupGlobalId, tcLookupId ) -import TcMType ( tcInstTyVars, newTyVarTy, getTcTyVar, putTcTyVar ) +import TcMType ( tcInstTyVars, newTyVarTy, getTcTyVar, putTcTyVar, zapToType ) import TcType ( TcType, TcTyVar, TcSigmaType, TyVarDetails(VanillaTv), mkTyConApp, mkClassPred, liftedTypeKind, tcGetTyVar_maybe, isHoleTyVar, openTypeKind ) -import TcUnify ( tcSub, unifyTauTy, unifyListTy, unifyPArrTy, - unifyTupleTy, mkCoercion, idCoercion, isIdCoercion, +import TcUnify ( tcSubOff, TcHoleType, + unifyTauTy, unifyListTy, unifyPArrTy, unifyTupleTy, + mkCoercion, idCoercion, isIdCoercion, (<$>), PatCoFn ) import TcMonoType ( tcHsSigType, UserTypeCtxt(..) ) @@ -69,8 +70,7 @@ tcMonoPatBndr :: BinderChecker -- so there's no polymorphic guy to worry about tcMonoPatBndr binder_name pat_ty - | Just tv <- tcGetTyVar_maybe pat_ty, - isHoleTyVar tv + = zapToType pat_ty `thenNF_Tc` \ pat_ty' -> -- If there are *no constraints* on the pattern type, we -- revert to good old H-M typechecking, making -- the type of the binder into an *ordinary* @@ -79,14 +79,8 @@ tcMonoPatBndr binder_name pat_ty -- What we are trying to avoid here is giving a binder -- a type that is a 'hole'. The only place holes should -- appear is as an argument to tcPat and tcExpr/tcMonoExpr. - = getTcTyVar tv `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - Just ty -> tcMonoPatBndr binder_name ty - Nothing -> newTyVarTy openTypeKind `thenNF_Tc` \ ty -> - putTcTyVar tv ty `thenNF_Tc_` - returnTc (idCoercion, emptyLIE, mkLocalId binder_name ty) - | otherwise - = returnTc (idCoercion, emptyLIE, mkLocalId binder_name pat_ty) + + returnTc (idCoercion, emptyLIE, mkLocalId binder_name pat_ty') \end{code} @@ -100,7 +94,7 @@ tcMonoPatBndr binder_name pat_ty tcPat :: BinderChecker -> RenamedPat - -> TcSigmaType -- Expected type derived from the context + -> TcHoleType -- Expected type derived from the context -- In the case of a function with a rank-2 signature, -- this type might be a forall type. @@ -461,10 +455,10 @@ tcSubPat does the work (forall a. a->a in the example) \begin{code} -tcSubPat :: TcSigmaType -> TcSigmaType -> TcM (PatCoFn, LIE) +tcSubPat :: TcSigmaType -> TcHoleType -> TcM (PatCoFn, LIE) tcSubPat sig_ty exp_ty - = tcSub sig_ty exp_ty `thenTc` \ (co_fn, lie) -> + = tcSubOff sig_ty exp_ty `thenTc` \ (co_fn, lie) -> -- co_fn is a coercion on *expressions*, and we -- need to make a coercion on *patterns* if isIdCoercion co_fn then diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs index 3bcb389..27abbd5 100644 --- a/ghc/compiler/typecheck/TcType.lhs +++ b/ghc/compiler/typecheck/TcType.lhs @@ -17,7 +17,7 @@ is the principal client. module TcType ( -------------------------------- -- Types - TcType, TcSigmaType, TcPhiType, TcTauType, TcPredType, TcThetaType, + TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType, TcTyVar, TcTyVarSet, TcKind, -------------------------------- @@ -27,12 +27,12 @@ module TcType ( -------------------------------- -- Builders - mkRhoTy, mkSigmaTy, + mkPhiTy, mkSigmaTy, -------------------------------- -- Splitters -- These are important because they do not look through newtypes - tcSplitForAllTys, tcSplitRhoTy, + tcSplitForAllTys, tcSplitPhiTy, tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs, tcSplitAppTy_maybe, tcSplitAppTy, tcSplitSigmaTy, @@ -155,7 +155,7 @@ import Outputable The type checker divides the generic Type world into the following more structured beasts: -sigma ::= forall tyvars. theta => phi +sigma ::= forall tyvars. phi -- A sigma type is a qualified type -- -- Note that even if 'tyvars' is empty, theta @@ -166,7 +166,9 @@ sigma ::= forall tyvars. theta => phi -- A 'phi' type has no foralls to the right of -- an arrow -phi ::= sigma -> phi +phi :: theta => rho + +rho ::= sigma -> rho | tau -- A 'tau' type has no quantification anywhere @@ -182,7 +184,7 @@ tau ::= tyvar \begin{code} type SigmaType = Type -type PhiType = Type +type RhoType = Type type TauType = Type \end{code} @@ -199,7 +201,7 @@ type TcType = Type -- A TcType can have mutable type variables type TcPredType = PredType type TcThetaType = ThetaType type TcSigmaType = TcType -type TcPhiType = TcType +type TcRhoType = TcType type TcTauType = TcType type TcKind = TcType \end{code} @@ -287,10 +289,10 @@ tyVarBindingInfo tv %************************************************************************ \begin{code} -mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau) +mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkPhiTy theta tau) -mkRhoTy :: [SourceType] -> Type -> Type -mkRhoTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta +mkPhiTy :: [SourceType] -> Type -> Type +mkPhiTy theta ty = foldr (\p r -> FunTy (mkPredTy p) r) ty theta \end{code} @@ -348,8 +350,8 @@ tcIsForAllTy (ForAllTy tv ty) = True tcIsForAllTy (NoteTy n ty) = tcIsForAllTy ty tcIsForAllTy t = False -tcSplitRhoTy :: Type -> ([PredType], Type) -tcSplitRhoTy ty = split ty ty [] +tcSplitPhiTy :: Type -> ([PredType], Type) +tcSplitPhiTy ty = split ty ty [] where split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of Just p -> split res res (p:ts) @@ -358,7 +360,7 @@ tcSplitRhoTy ty = split ty ty [] split orig_ty ty ts = (reverse ts, orig_ty) tcSplitSigmaTy ty = case tcSplitForAllTys ty of - (tvs, rho) -> case tcSplitRhoTy rho of + (tvs, rho) -> case tcSplitPhiTy rho of (theta, tau) -> (tvs, theta, tau) tcTyConAppTyCon :: Type -> TyCon diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index bf553bb..03a3d81 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -6,7 +6,7 @@ \begin{code} module TcUnify ( -- Full-blown subsumption - tcSub, tcGen, subFunTy, + tcSubOff, tcSubExp, tcGen, subFunTy, TcHoleType, checkSigTyVars, checkSigTyVarsWrt, sigCtxt, -- Various unifications @@ -30,12 +30,12 @@ import TypeRep ( Type(..), SourceType(..), TyNote(..), openKindCon, typeCon ) import TcMonad -- TcType, amongst others -import TcType ( TcKind, TcType, TcSigmaType, TcPhiType, TcTyVar, TcTauType, +import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType, TcTyVarSet, TcThetaType, TyVarDetails(SigTv), isTauTy, isSigmaTy, tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tcGetTyVar_maybe, tcGetTyVar, - mkTyConApp, mkFunTy, tyVarsOfType, mkRhoTy, + mkTyConApp, mkFunTy, tyVarsOfType, mkPhiTy, typeKind, tcSplitFunTy_maybe, mkForAllTys, isHoleTyVar, isSkolemTyVar, isUserTyVar, tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars, @@ -46,7 +46,7 @@ import qualified Type ( getTyVar_maybe ) import Inst ( LIE, emptyLIE, plusLIE, newDicts, instToId, tcInstCall ) -import TcMType ( getTcTyVar, putTcTyVar, tcInstType, +import TcMType ( getTcTyVar, putTcTyVar, tcInstType, readHoleResult, newTyVarTy, newTyVarTys, newBoxityVar, newHoleTyVarTy, zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcTyVar ) import TcSimplify ( tcSimplifyCheck ) @@ -66,6 +66,9 @@ import Maybe ( isNothing ) import Outputable \end{code} +Notes on holes +~~~~~~~~~~~~~~ +* A hole is always filled in with an ordinary type, not another hole. %************************************************************************ %* * @@ -73,24 +76,59 @@ import Outputable %* * %************************************************************************ -\begin{code} -tcSub :: TcSigmaType -- expected_ty; can be a type scheme; - -- can be a "hole" type variable - -> TcSigmaType -- actual_ty; can be a type scheme - -> TcM (ExprCoFn, LIE) -\end{code} +All the tcSub calls have the form + + tcSub expected_ty offered_ty +which checks + offered_ty <= expected_ty -(tcSub expected_ty actual_ty) checks that - actual_ty <= expected_ty -That is, that a value of type actual_ty is acceptable in +That is, that a value of type offered_ty is acceptable in a place expecting a value of type expected_ty. It returns a coercion function - co_fn :: actual_ty -> expected_ty -which takes an HsExpr of type actual_ty into one of type + co_fn :: offered_ty -> expected_ty +which takes an HsExpr of type offered_ty into one of type expected_ty. \begin{code} +type TcHoleType = TcSigmaType -- Either a TcSigmaType, + -- or else a hole + +tcSubExp :: TcHoleType -> TcSigmaType -> TcM (ExprCoFn, LIE) +tcSubOff :: TcSigmaType -> TcHoleType -> TcM (ExprCoFn, LIE) +tcSub :: TcSigmaType -> TcSigmaType -> TcM (ExprCoFn, LIE) +\end{code} + +These two check for holes + +\begin{code} +tcSubExp expected_ty offered_ty + = checkHole expected_ty offered_ty tcSub + +tcSubOff expected_ty offered_ty + = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off) + +-- checkHole looks for a hole in its first arg; +-- If so, and it is uninstantiated, it fills in the hole +-- with its second arg +-- Otherwise it calls thing_inside, passing the two args, looking +-- through any instantiated hole + +checkHole (TyVarTy tv) other_ty thing_inside + | isHoleTyVar tv + = getTcTyVar tv `thenNF_Tc` \ maybe_ty -> + case maybe_ty of + Just ty -> thing_inside ty other_ty + Nothing -> putTcTyVar tv other_ty `thenNF_Tc_` + returnTc (idCoercion, emptyLIE) + +checkHole ty other_ty thing_inside + = thing_inside ty other_ty +\end{code} + +No holes expected now. Add some error-check context info. + +\begin{code} tcSub expected_ty actual_ty = traceTc (text "tcSub" <+> details) `thenNF_Tc_` tcAddErrCtxtM (unifyCtxt "type" expected_ty actual_ty) @@ -115,24 +153,6 @@ tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_ty ----------------------------------- --- "Hole type variable" case --- Do this case before unwrapping for-alls in the actual_ty - -tc_sub _ (TyVarTy tv) act_sty act_ty - | isHoleTyVar tv - = -- It's a "hole" type variable - getTcTyVar tv `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - - Just ty -> -- Already been assigned - tc_sub ty ty act_sty act_ty ; - - Nothing -> -- Assign it - putTcTyVar tv act_sty `thenNF_Tc_` - returnTc (idCoercion, emptyLIE) - - ------------------------------------ -- Generalisation case -- actual_ty: d:Eq b => b->b -- expected_ty: forall a. Ord a => a->a @@ -185,14 +205,16 @@ tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res) -- is perfectly fine! tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv) - = getTcTyVar tv `thenNF_Tc` \ maybe_ty -> + = ASSERT( not (isHoleTyVar tv) ) + getTcTyVar tv `thenNF_Tc` \ maybe_ty -> case maybe_ty of Just ty -> tc_sub exp_sty exp_ty ty ty Nothing -> imitateFun tv exp_sty `thenNF_Tc` \ (act_arg, act_res) -> tcSub_fun exp_arg exp_res act_arg act_res tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res) - = getTcTyVar tv `thenNF_Tc` \ maybe_ty -> + = ASSERT( not (isHoleTyVar tv) ) + getTcTyVar tv `thenNF_Tc` \ maybe_ty -> case maybe_ty of Just ty -> tc_sub ty ty act_sty act_ty Nothing -> imitateFun tv act_sty `thenNF_Tc` \ (exp_arg, exp_res) -> @@ -214,9 +236,9 @@ tc_sub exp_sty expected_ty act_sty actual_ty \begin{code} tcSub_fun exp_arg exp_res act_arg act_res - = tcSub act_arg exp_arg `thenTc` \ (co_fn_arg, lie1) -> - tcSub exp_res act_res `thenTc` \ (co_fn_res, lie2) -> - tcGetUnique `thenNF_Tc` \ uniq -> + = tc_sub act_arg act_arg exp_arg exp_arg `thenTc` \ (co_fn_arg, lie1) -> + tc_sub exp_res exp_res act_res act_res `thenTc` \ (co_fn_res, lie2) -> + tcGetUnique `thenNF_Tc` \ uniq -> let -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg -- co_fn_res :: HsExpr act_res -> HsExpr exp_res @@ -265,7 +287,7 @@ 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 + -> (TcRhoType -> TcM (result, LIE)) -- spec_ty -> TcM (ExprCoFn, result, LIE) -- The expression has type: spec_ty -> expected_ty @@ -713,32 +735,46 @@ creation of type variables. type variables, so we should create new ordinary type variables \begin{code} -subFunTy :: TcSigmaType -- Fail if ty isn't a function type - -> TcM (TcType, TcType) -- otherwise return arg and result types -subFunTy ty@(TyVarTy tyvar) - - = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - Just ty -> subFunTy ty - Nothing | isHoleTyVar tyvar - -> newHoleTyVarTy `thenNF_Tc` \ arg -> - newHoleTyVarTy `thenNF_Tc` \ res -> - putTcTyVar tyvar (mkFunTy arg res) `thenNF_Tc_` - returnTc (arg,res) - | otherwise - -> unify_fun_ty_help ty - -subFunTy ty - = case tcSplitFunTy_maybe ty of - Just arg_and_res -> returnTc arg_and_res - Nothing -> unify_fun_ty_help ty +subFunTy :: TcHoleType -- Fail if ty isn't a function type + -- If it's a hole, make two holes, feed them to... + -> (TcHoleType -> TcHoleType -> TcM a) -- the thing inside + -> TcM a -- and bind the function type to the hole + +subFunTy ty@(TyVarTy tyvar) thing_inside + | isHoleTyVar tyvar + = -- This is the interesting case + getTcTyVar tyvar `thenNF_Tc` \ maybe_ty -> + case maybe_ty of { + Just ty' -> subFunTy ty' thing_inside ; + Nothing -> + + newHoleTyVarTy `thenNF_Tc` \ arg_ty -> + newHoleTyVarTy `thenNF_Tc` \ res_ty -> + + -- Do the business + thing_inside arg_ty res_ty `thenTc` \ answer -> + + -- Extract the answers + readHoleResult arg_ty `thenNF_Tc` \ arg_ty' -> + readHoleResult res_ty `thenNF_Tc` \ res_ty' -> + + -- Write the answer into the incoming hole + putTcTyVar tyvar (mkFunTy arg_ty' res_ty') `thenNF_Tc_` + + -- And return the answer + returnTc answer } + +subFunTy ty thing_inside + = unifyFunTy ty `thenTc` \ (arg,res) -> + thing_inside arg res -unifyFunTy :: TcPhiType -- Fail if ty isn't a function type +unifyFunTy :: TcRhoType -- Fail if ty isn't a function type -> TcM (TcType, TcType) -- otherwise return arg and result types unifyFunTy ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty -> + = ASSERT( not (isHoleTyVar tyvar) ) + getTcTyVar tyvar `thenNF_Tc` \ maybe_ty -> case maybe_ty of Just ty' -> unifyFunTy ty' Nothing -> unify_fun_ty_help ty @@ -1159,7 +1195,7 @@ sigCtxt id sig_tvs sig_theta sig_tau tidy_env = zonkTcType sig_tau `thenNF_Tc` \ actual_tau -> let (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs - (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau) + (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy 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 -- 1.7.10.4