Commit aaed1181 authored by simonpj's avatar simonpj
Browse files

[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
parent d225c28b
......@@ -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}
......@@ -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
......
......@@ -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}
......
......@@ -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)
......@@ -131,6 +128,42 @@ newBoxityVar
\end{code}
%************************************************************************
%* *
\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}
......
......@@ -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)
......
......@@ -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
......
......@@ -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
%************************************************************************