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,
(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)
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
-> 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}
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,
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)
-- 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)
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
import TcHsSyn ( TcExpr, TcRecordBinds, simpleHsLitTy )
import TcMonad
-import TcUnify ( tcSub, tcGen, (<$>),
+import TcUnify ( tcSubExp, tcGen, (<$>),
unifyTauTy, unifyFunTy, unifyListTy, unifyPArrTy,
unifyTupleTy )
import BasicTypes ( RecFlag(..), isMarkedStrict )
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,
\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
-- 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}
-- 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}
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
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:
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}
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}
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) ->
-- (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)
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}
--------------------------------
-- 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,
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,
= 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)
%************************************************************************
%* *
+\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}
%* *
%************************************************************************
([], 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}
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 )
import VarSet
import Var ( Id )
import Bag
-import Util ( isSingleton )
+import Util ( isSingleton, lengthExceeds )
import Outputable
import List ( nub )
-> 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}
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,
\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
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
-- 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}
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)
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(..) )
-- 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*
-- 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}
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.
(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
module TcType (
--------------------------------
-- Types
- TcType, TcSigmaType, TcPhiType, TcTauType, TcPredType, TcThetaType,
+ TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
TcTyVar, TcTyVarSet, TcKind,
--------------------------------
--------------------------------
-- 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,
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
-- 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
\begin{code}
type SigmaType = Type
-type PhiType = Type
+type RhoType = Type
type TauType = Type
\end{code}
type TcPredType = PredType
type TcThetaType = ThetaType
type TcSigmaType = TcType
-type TcPhiType = TcType
+type TcRhoType = TcType
type TcTauType = TcType
type TcKind = TcType
\end{code}
%************************************************************************
\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}
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)
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
\begin{code}
module TcUnify (
-- Full-blown subsumption
- tcSub, tcGen, subFunTy,
+ tcSubOff, tcSubExp, tcGen, subFunTy, TcHoleType,
checkSigTyVars, checkSigTyVarsWrt, sigCtxt,
-- Various unifications
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,
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 )
import Outputable
\end{code}
+Notes on holes
+~~~~~~~~~~~~~~
+* A hole is always filled in with an ordinary type, not another hole.
%************************************************************************
%* *
%* *
%************************************************************************
-\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)
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
-- 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) ->
\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
-> 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
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
= 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
projects / ghc-hetmet.git / commitdiff