#include "HsVersions.h"
-import {-# SOURCE #-} TcExpr( tcExpr )
+import {-# SOURCE #-} TcExpr( tcCheckSigma )
import HsSyn ( HsLit(..), HsOverLit(..), HsExpr(..) )
import TcHsSyn ( TcExpr, TcId, TcIdSet,
import TcRnMonad
import TcEnv ( tcGetInstEnv, tcLookupId, tcLookupTyCon, checkWellStaged, topIdLvl )
import InstEnv ( InstLookupResult(..), lookupInstEnv )
-import TcMType ( zonkTcType, zonkTcTypes, zonkTcPredType, zapToType,
+import TcMType ( zonkTcType, zonkTcTypes, zonkTcPredType,
zonkTcThetaType, tcInstTyVar, tcInstType, tcInstTyVars
)
import TcType ( Type, TcType, TcThetaType, TcTyVarSet,
-> HsOverLit
-> TcType
-> TcM TcExpr
-newOverloadedLit orig lit expected_ty
- = zapToType expected_ty `thenM_`
- -- The expected type might be a 'hole' type variable,
- -- in which case we must zap it to an ordinary type variable
- new_over_lit orig lit expected_ty
-
-new_over_lit orig lit@(HsIntegral i fi) expected_ty
+newOverloadedLit orig lit@(HsIntegral i fi) expected_ty
| fi /= fromIntegerName -- Do not generate a LitInst for rebindable
-- syntax. Reason: tcSyntaxName does unification
-- which is very inconvenient in tcSimplify
| otherwise
= newLitInst orig lit expected_ty
-new_over_lit orig lit@(HsFractional r fr) expected_ty
+newOverloadedLit orig lit@(HsFractional r fr) expected_ty
| fr /= fromRationalName -- c.f. HsIntegral case
= tcSyntaxName orig expected_ty fromRationalName fr `thenM` \ (expr, _) ->
mkRatLit r `thenM` \ rat_lit ->
-- C.f. newMethodAtLoc
([tv], _, tau) = tcSplitSigmaTy (idType std_id)
tau1 = substTyWith [tv] [ty] tau
+ -- Actually, the "tau-type" might be a sigma-type in the
+ -- case of locally-polymorphic methods.
in
addErrCtxtM (syntaxNameCtxt user_nm orig tau1) $
- tcExpr (HsVar user_nm) tau1 `thenM` \ user_fn ->
+ tcCheckSigma (HsVar user_nm) tau1 `thenM` \ user_fn ->
returnM (user_fn, tau1)
syntaxNameCtxt name orig ty tidy_env
#include "HsVersions.h"
import {-# SOURCE #-} TcMatches ( tcGRHSs, tcMatchesFun )
-import {-# SOURCE #-} TcExpr ( tcExpr, tcMonoExpr )
+import {-# SOURCE #-} TcExpr ( tcCheckSigma, tcCheckRho )
import CmdLineOpts ( DynFlag(Opt_NoMonomorphismRestriction) )
import HsSyn ( HsExpr(..), HsBinds(..), MonoBinds(..), Sig(..),
import TcRnMonad
import Inst ( InstOrigin(..), newDicts, newIPDict, instToId )
import TcEnv ( tcExtendLocalValEnv, tcExtendLocalValEnv2, newLocalName )
-import TcUnify ( unifyTauTyLists, checkSigTyVarsWrt, sigCtxt )
+import TcUnify ( Expected(..), newHole, unifyTauTyLists, checkSigTyVarsWrt, sigCtxt )
import TcSimplify ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyRestricted,
tcSimplifyToDicts, tcSimplifyIPs )
import TcMonoType ( tcHsSigType, UserTypeCtxt(..), TcSigInfo(..),
)
import TcPat ( tcPat, tcSubPat, tcMonoPatBndr )
import TcSimplify ( bindInstsOfLocalFuns )
-import TcMType ( newTyVar, newTyVarTy, newHoleTyVarTy,
- zonkTcTyVarToTyVar, readHoleResult
- )
+import TcMType ( newTyVar, newTyVarTy, zonkTcTyVarToTyVar )
import TcType ( TcTyVar, mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType,
mkPredTy, mkForAllTy, isUnLiftedType,
unliftedTypeKind, liftedTypeKind, openTypeKind, eqKind
= newTyVarTy openTypeKind `thenM` \ ty ->
getSrcLocM `thenM` \ loc ->
newIPDict (IPBind ip) ip ty `thenM` \ (ip', ip_inst) ->
- tcMonoExpr expr ty `thenM` \ expr' ->
+ tcCheckRho expr ty `thenM` \ expr' ->
returnM (ip_inst, (ip', expr'))
tc_binds_and_then top_lvl combiner (MonoBind bind sigs is_rec) do_next
-- the RHS has the appropriate type (with outer for-alls stripped off)
mono_id = tcSigMonoId sig
mono_ty = idType mono_id
- complete_it = addSrcLoc locn $
- tcMatchesFun name mono_ty matches `thenM` \ matches' ->
+ complete_it = addSrcLoc locn $
+ tcMatchesFun name matches (Check mono_ty) `thenM` \ matches' ->
returnM (FunMonoBind mono_id inf matches' locn,
unitBag (name, mono_id))
in
newTyVarTy openTypeKind `thenM` \ mono_ty ->
let
mono_id = mkLocalId mono_name mono_ty
- complete_it = addSrcLoc locn $
- tcMatchesFun name mono_ty matches `thenM` \ matches' ->
+ complete_it = addSrcLoc locn $
+ tcMatchesFun name matches (Check mono_ty) `thenM` \ matches' ->
returnM (FunMonoBind mono_id inf matches' locn,
unitBag (name, mono_id))
in
| otherwise -- (c) No type signature, and non-recursive
= let -- So we can use a 'hole' type to infer a higher-rank type
complete_it
- = addSrcLoc locn $
- newHoleTyVarTy `thenM` \ fun_ty ->
- tcMatchesFun name fun_ty matches `thenM` \ matches' ->
- readHoleResult fun_ty `thenM` \ fun_ty' ->
- newLocalName name `thenM` \ mono_name ->
+ = addSrcLoc locn $
+ newHole `thenM` \ hole ->
+ tcMatchesFun name matches (Infer hole) `thenM` \ matches' ->
+ readMutVar hole `thenM` \ fun_ty ->
+ newLocalName name `thenM` \ mono_name ->
let
- mono_id = mkLocalId mono_name fun_ty'
+ mono_id = mkLocalId mono_name fun_ty
in
returnM (FunMonoBind mono_id inf matches' locn,
unitBag (name, mono_id))
-- The type variables are brought into scope in tc_binds_and_then,
-- so we don't have to do anything here.
- newHoleTyVarTy `thenM` \ pat_ty ->
- tcPat tc_pat_bndr pat pat_ty `thenM` \ (pat', tvs, ids, lie_avail) ->
- readHoleResult pat_ty `thenM` \ pat_ty' ->
+ newHole `thenM` \ hole ->
+ tcPat tc_pat_bndr pat (Infer hole) `thenM` \ (pat', tvs, ids, lie_avail) ->
+ readMutVar hole `thenM` \ pat_ty ->
-- Don't know how to deal with pattern-bound existentials yet
checkTc (isEmptyBag tvs && null lie_avail)
(existentialExplode bind) `thenM_`
let
- complete_it = addSrcLoc locn $
- addErrCtxt (patMonoBindsCtxt bind) $
- tcGRHSs PatBindRhs grhss pat_ty' `thenM` \ grhss' ->
+ complete_it = addSrcLoc locn $
+ addErrCtxt (patMonoBindsCtxt bind) $
+ tcGRHSs PatBindRhs grhss (Check pat_ty) `thenM` \ grhss' ->
returnM (PatMonoBind pat' grhss' locn, ids)
in
returnM (complete_it, if isRec is_rec then ids else emptyBag)
-- Check that f has a more general type, and build a RHS for
-- the spec-pragma-id at the same time
- getLIE (tcExpr (HsVar name) sig_ty) `thenM` \ (spec_expr, spec_lie) ->
+ getLIE (tcCheckSigma (HsVar name) sig_ty) `thenM` \ (spec_expr, spec_lie) ->
-- Squeeze out any Methods (see comments with tcSimplifyToDicts)
tcSimplifyToDicts spec_lie `thenM` \ spec_binds ->
module TcExpr where
-tcExpr ::
+tcCheckSigma ::
RnHsSyn.RenamedHsExpr
-> TcType.TcType
-> TcRnTypes.TcM TcHsSyn.TcExpr
-tcMonoExpr ::
+tcCheckRho ::
RnHsSyn.RenamedHsExpr
-> TcType.TcType
-> TcRnTypes.TcM TcHsSyn.TcExpr
+
+tcMonoExpr ::
+ RnHsSyn.RenamedHsExpr
+ -> TcUnify.Expected TcType.TcType
+ -> TcRnTypes.TcM TcHsSyn.TcExpr
\section[TcExpr]{Typecheck an expression}
\begin{code}
-module TcExpr ( tcExpr, tcExpr_id, tcMonoExpr ) where
+module TcExpr ( tcCheckSigma, tcCheckRho, tcInferRho, tcMonoExpr ) where
#include "HsVersions.h"
import RnHsSyn ( RenamedHsExpr, RenamedRecordBinds )
import TcHsSyn ( TcExpr, TcRecordBinds, hsLitType, mkHsDictApp, mkHsTyApp, mkHsLet, (<$>) )
import TcRnMonad
-import TcUnify ( tcSubExp, tcGen,
- unifyTauTy, unifyFunTy, unifyListTy, unifyPArrTy, unifyTupleTy )
+import TcUnify ( Expected(..), newHole, zapExpectedType, zapExpectedTo, tcSubExp, tcGen,
+ unifyFunTy, zapToListTy, zapToPArrTy, zapToTupleTy )
import BasicTypes ( isMarkedStrict )
import Inst ( InstOrigin(..),
newOverloadedLit, newMethodFromName, newIPDict,
import TcMatches ( tcMatchesCase, tcMatchLambda, tcDoStmts, tcThingWithSig )
import TcMonoType ( tcHsSigType, UserTypeCtxt(..) )
import TcPat ( badFieldCon )
-import TcMType ( tcInstTyVars, tcInstType, newHoleTyVarTy, zapToType,
- newTyVarTy, newTyVarTys, zonkTcType, readHoleResult )
+import TcMType ( tcInstTyVars, tcInstType, newTyVarTy, newTyVarTys, zonkTcType )
import TcType ( TcType, TcSigmaType, TcRhoType, TyVarDetails(VanillaTv),
tcSplitFunTys, tcSplitTyConApp, mkTyVarTys,
isSigmaTy, mkFunTy, mkFunTys,
%************************************************************************
\begin{code}
-tcExpr :: RenamedHsExpr -- Expession to type check
- -> TcSigmaType -- Expected type (could be a polytpye)
- -> TcM TcExpr -- Generalised expr with expected type
+-- tcCheckSigma does type *checking*; it's passed the expected type of the result
+tcCheckSigma :: RenamedHsExpr -- Expession to type check
+ -> TcSigmaType -- Expected type (could be a polytpye)
+ -> TcM TcExpr -- Generalised expr with expected type
-tcExpr expr expected_ty
+tcCheckSigma expr expected_ty
= traceTc (text "tcExpr" <+> (ppr expected_ty $$ ppr expr)) `thenM_`
tc_expr' expr expected_ty
-tc_expr' expr expected_ty
- | not (isSigmaTy expected_ty) -- Monomorphic case
- = tcMonoExpr expr expected_ty
-
- | otherwise
- = tcGen expected_ty emptyVarSet (
- tcMonoExpr expr
+tc_expr' expr sigma_ty
+ | isSigmaTy sigma_ty
+ = tcGen sigma_ty emptyVarSet (
+ \ rho_ty -> tcCheckRho expr rho_ty
) `thenM` \ (gen_fn, expr') ->
returnM (gen_fn <$> expr')
+
+tc_expr' expr rho_ty -- Monomorphic case
+ = tcCheckRho expr rho_ty
+\end{code}
+
+Typecheck expression which in most cases will be an Id.
+The expression can return a higher-ranked type, such as
+ (forall a. a->a) -> Int
+so we must create a hole to pass in as the expected tyvar.
+
+\begin{code}
+tcCheckRho :: RenamedHsExpr -> TcRhoType -> TcM TcExpr
+tcCheckRho expr rho_ty = tcMonoExpr expr (Check rho_ty)
+
+tcInferRho :: RenamedHsExpr -> TcM (TcExpr, TcRhoType)
+tcInferRho (HsVar name) = tcId name
+tcInferRho expr = newHole `thenM` \ hole ->
+ tcMonoExpr expr (Infer hole) `thenM` \ expr' ->
+ readMutVar hole `thenM` \ rho_ty ->
+ returnM (expr', rho_ty)
\end{code}
+
%************************************************************************
%* *
\subsection{The TAUT rules for variables}
\begin{code}
tcMonoExpr :: RenamedHsExpr -- Expession to type check
- -> TcRhoType -- Expected type (could be a type variable)
+ -> Expected TcRhoType -- Expected type (could be a type variable)
-- Definitely no foralls at the top
-- Can be a 'hole'.
-> TcM TcExpr
tcMonoExpr in_expr@(ExprWithTySig expr poly_ty) res_ty
= addErrCtxt (exprSigCtxt in_expr) $
tcHsSigType ExprSigCtxt poly_ty `thenM` \ sig_tc_ty ->
- tcThingWithSig sig_tc_ty (tcMonoExpr expr) res_ty `thenM` \ (co_fn, expr') ->
+ tcThingWithSig sig_tc_ty (tcCheckRho expr) res_ty `thenM` \ (co_fn, expr') ->
returnM (co_fn <$> expr')
tcMonoExpr (HsType ty) res_ty
\begin{code}
tcMonoExpr (HsLit lit) res_ty = tcLit lit res_ty
-tcMonoExpr (HsOverLit lit) res_ty = newOverloadedLit (LiteralOrigin lit) lit res_ty
+tcMonoExpr (HsOverLit lit) res_ty = zapExpectedType res_ty `thenM` \ res_ty' ->
+ newOverloadedLit (LiteralOrigin lit) lit res_ty'
tcMonoExpr (HsPar expr) res_ty = tcMonoExpr expr res_ty `thenM` \ expr' ->
returnM (HsPar expr')
tcMonoExpr (HsSCC lbl expr) res_ty = tcMonoExpr expr res_ty `thenM` \ expr' ->
-- op e
tcMonoExpr in_expr@(SectionL arg1 op) res_ty
- = tcExpr_id op `thenM` \ (op', op_ty) ->
+ = tcInferRho op `thenM` \ (op', op_ty) ->
split_fun_ty op_ty 2 {- two args -} `thenM` \ ([arg1_ty, arg2_ty], op_res_ty) ->
tcArg op (arg1, arg1_ty, 1) `thenM` \ arg1' ->
addErrCtxt (exprCtxt in_expr) $
-- \ x -> op x expr
tcMonoExpr in_expr@(SectionR op arg2) res_ty
- = tcExpr_id op `thenM` \ (op', op_ty) ->
+ = tcInferRho op `thenM` \ (op', op_ty) ->
split_fun_ty op_ty 2 {- two args -} `thenM` \ ([arg1_ty, arg2_ty], op_res_ty) ->
tcArg op (arg2, arg2_ty, 2) `thenM` \ arg2' ->
addErrCtxt (exprCtxt in_expr) $
-- equivalent to (op e1) e2:
tcMonoExpr in_expr@(OpApp arg1 op fix arg2) res_ty
- = tcExpr_id op `thenM` \ (op', op_ty) ->
+ = tcInferRho op `thenM` \ (op', op_ty) ->
split_fun_ty op_ty 2 {- two args -} `thenM` \ ([arg1_ty, arg2_ty], op_res_ty) ->
tcArg op (arg1, arg1_ty, 1) `thenM` \ arg1' ->
tcArg op (arg2, arg2_ty, 2) `thenM` \ arg2' ->
-- case (map f) of
-- (x:xs) -> ...
-- will report that map is applied to too few arguments
- --
- -- Not only that, but it's better to check the matches on their
- -- own, so that we get the expected results for scoped type variables.
- -- f x = case x of
- -- (p::a, q::b) -> (q,p)
- -- The above should work: the match (p,q) -> (q,p) is polymorphic as
- -- claimed by the pattern signatures. But if we typechecked the
- -- match with x in scope and x's type as the expected type, we'd be hosed.
tcMatchesCase matches res_ty `thenM` \ (scrut_ty, matches') ->
addErrCtxt (caseScrutCtxt scrut) (
- tcMonoExpr scrut scrut_ty
+ tcCheckRho scrut scrut_ty
) `thenM` \ scrut' ->
returnM (HsCase scrut' matches' src_loc)
tcMonoExpr (HsIf pred b1 b2 src_loc) res_ty
= addSrcLoc src_loc $
addErrCtxt (predCtxt pred) (
- tcMonoExpr pred boolTy ) `thenM` \ pred' ->
+ tcCheckRho pred boolTy ) `thenM` \ pred' ->
- zapToType res_ty `thenM` \ res_ty' ->
+ zapExpectedType res_ty `thenM` \ res_ty' ->
-- C.f. the call to zapToType in TcMatches.tcMatches
- tcMonoExpr b1 res_ty' `thenM` \ b1' ->
- tcMonoExpr b2 res_ty' `thenM` \ b2' ->
+ tcCheckRho b1 res_ty' `thenM` \ b1' ->
+ tcCheckRho b2 res_ty' `thenM` \ b2' ->
returnM (HsIf pred' b1' b2' src_loc)
tcMonoExpr (HsDo do_or_lc stmts method_names _ src_loc) res_ty
- = addSrcLoc src_loc $
- tcDoStmts do_or_lc stmts method_names res_ty `thenM` \ (binds, stmts', methods') ->
- returnM (mkHsLet binds (HsDo do_or_lc stmts' methods' res_ty src_loc))
+ = addSrcLoc src_loc $
+ zapExpectedType res_ty `thenM` \ res_ty' ->
+ -- All comprehensions yield a monotype
+ tcDoStmts do_or_lc stmts method_names res_ty' `thenM` \ (binds, stmts', methods') ->
+ returnM (mkHsLet binds (HsDo do_or_lc stmts' methods' res_ty' src_loc))
tcMonoExpr in_expr@(ExplicitList _ exprs) res_ty -- Non-empty list
- = unifyListTy res_ty `thenM` \ elt_ty ->
+ = zapToListTy res_ty `thenM` \ elt_ty ->
mappM (tc_elt elt_ty) exprs `thenM` \ exprs' ->
returnM (ExplicitList elt_ty exprs')
where
tc_elt elt_ty expr
= addErrCtxt (listCtxt expr) $
- tcMonoExpr expr elt_ty
+ tcCheckRho expr elt_ty
tcMonoExpr in_expr@(ExplicitPArr _ exprs) res_ty -- maybe empty
- = unifyPArrTy res_ty `thenM` \ elt_ty ->
+ = zapToPArrTy res_ty `thenM` \ elt_ty ->
mappM (tc_elt elt_ty) exprs `thenM` \ exprs' ->
returnM (ExplicitPArr elt_ty exprs')
where
tc_elt elt_ty expr
= addErrCtxt (parrCtxt expr) $
- tcMonoExpr expr elt_ty
+ tcCheckRho expr elt_ty
tcMonoExpr (ExplicitTuple exprs boxity) res_ty
- = unifyTupleTy boxity (length exprs) res_ty `thenM` \ arg_tys ->
- tcMonoExprs exprs arg_tys `thenM` \ exprs' ->
+ = zapToTupleTy boxity (length exprs) res_ty `thenM` \ arg_tys ->
+ tcCheckRhos exprs arg_tys `thenM` \ exprs' ->
returnM (ExplicitTuple exprs' boxity)
\end{code}
| otherwise = [1..length args]
in
newTyVarTys (length tv_idxs) openTypeKind `thenM` \ arg_tys ->
- tcMonoExprs args arg_tys `thenM` \ args' ->
+ tcCheckRhos args arg_tys `thenM` \ args' ->
-- The argument types can be unlifted or lifted; the result
-- type must, however, be lifted since it's an argument to the IO
let
io_result_ty = mkTyConApp ioTyCon [result_ty]
in
- unifyTauTy res_ty io_result_ty `thenM_`
+ zapExpectedTo res_ty io_result_ty `thenM_`
-- Construct the extra insts, which encode the
-- constraints on the argument and result types.
(tycon, ty_args) = tcSplitTyConApp record_ty
in
ASSERT( isAlgTyCon tycon )
- unifyTauTy res_ty record_ty `thenM_`
+ zapExpectedTo res_ty record_ty `thenM_`
-- Check that the record bindings match the constructor
-- con_name is syntactically constrained to be a data constructor
- tcLookupDataCon con_name `thenM` \ data_con ->
+ tcLookupDataCon con_name `thenM` \ data_con ->
let
bad_fields = badFields rbinds data_con
in
let
result_record_ty = mkTyConApp tycon result_inst_tys
in
- unifyTauTy res_ty result_record_ty `thenM_`
+ zapExpectedTo res_ty result_record_ty `thenM_`
tcRecordBinds tycon result_inst_tys rbinds `thenM` \ rbinds' ->
-- STEP 4
let
record_ty = mkTyConApp tycon inst_tys
in
- tcMonoExpr record_expr record_ty `thenM` \ record_expr' ->
+ tcCheckRho record_expr record_ty `thenM` \ record_expr' ->
-- STEP 6
-- Figure out the LIE we need. We have to generate some
\begin{code}
tcMonoExpr (ArithSeqIn seq@(From expr)) res_ty
- = unifyListTy res_ty `thenM` \ elt_ty ->
- tcMonoExpr expr elt_ty `thenM` \ expr' ->
+ = zapToListTy res_ty `thenM` \ elt_ty ->
+ tcCheckRho expr elt_ty `thenM` \ expr' ->
newMethodFromName (ArithSeqOrigin seq)
elt_ty enumFromName `thenM` \ enum_from ->
tcMonoExpr in_expr@(ArithSeqIn seq@(FromThen expr1 expr2)) res_ty
= addErrCtxt (arithSeqCtxt in_expr) $
- unifyListTy res_ty `thenM` \ elt_ty ->
- tcMonoExpr expr1 elt_ty `thenM` \ expr1' ->
- tcMonoExpr expr2 elt_ty `thenM` \ expr2' ->
+ zapToListTy res_ty `thenM` \ elt_ty ->
+ tcCheckRho expr1 elt_ty `thenM` \ expr1' ->
+ tcCheckRho expr2 elt_ty `thenM` \ expr2' ->
newMethodFromName (ArithSeqOrigin seq)
elt_ty enumFromThenName `thenM` \ enum_from_then ->
tcMonoExpr in_expr@(ArithSeqIn seq@(FromTo expr1 expr2)) res_ty
= addErrCtxt (arithSeqCtxt in_expr) $
- unifyListTy res_ty `thenM` \ elt_ty ->
- tcMonoExpr expr1 elt_ty `thenM` \ expr1' ->
- tcMonoExpr expr2 elt_ty `thenM` \ expr2' ->
+ zapToListTy res_ty `thenM` \ elt_ty ->
+ tcCheckRho expr1 elt_ty `thenM` \ expr1' ->
+ tcCheckRho expr2 elt_ty `thenM` \ expr2' ->
newMethodFromName (ArithSeqOrigin seq)
elt_ty enumFromToName `thenM` \ enum_from_to ->
tcMonoExpr in_expr@(ArithSeqIn seq@(FromThenTo expr1 expr2 expr3)) res_ty
= addErrCtxt (arithSeqCtxt in_expr) $
- unifyListTy res_ty `thenM` \ elt_ty ->
- tcMonoExpr expr1 elt_ty `thenM` \ expr1' ->
- tcMonoExpr expr2 elt_ty `thenM` \ expr2' ->
- tcMonoExpr expr3 elt_ty `thenM` \ expr3' ->
+ zapToListTy res_ty `thenM` \ elt_ty ->
+ tcCheckRho expr1 elt_ty `thenM` \ expr1' ->
+ tcCheckRho expr2 elt_ty `thenM` \ expr2' ->
+ tcCheckRho expr3 elt_ty `thenM` \ expr3' ->
newMethodFromName (ArithSeqOrigin seq)
elt_ty enumFromThenToName `thenM` \ eft ->
tcMonoExpr in_expr@(PArrSeqIn seq@(FromTo expr1 expr2)) res_ty
= addErrCtxt (parrSeqCtxt in_expr) $
- unifyPArrTy res_ty `thenM` \ elt_ty ->
- tcMonoExpr expr1 elt_ty `thenM` \ expr1' ->
- tcMonoExpr expr2 elt_ty `thenM` \ expr2' ->
+ zapToPArrTy res_ty `thenM` \ elt_ty ->
+ tcCheckRho expr1 elt_ty `thenM` \ expr1' ->
+ tcCheckRho expr2 elt_ty `thenM` \ expr2' ->
newMethodFromName (PArrSeqOrigin seq)
elt_ty enumFromToPName `thenM` \ enum_from_to ->
tcMonoExpr in_expr@(PArrSeqIn seq@(FromThenTo expr1 expr2 expr3)) res_ty
= addErrCtxt (parrSeqCtxt in_expr) $
- unifyPArrTy res_ty `thenM` \ elt_ty ->
- tcMonoExpr expr1 elt_ty `thenM` \ expr1' ->
- tcMonoExpr expr2 elt_ty `thenM` \ expr2' ->
- tcMonoExpr expr3 elt_ty `thenM` \ expr3' ->
+ zapToPArrTy res_ty `thenM` \ elt_ty ->
+ tcCheckRho expr1 elt_ty `thenM` \ expr1' ->
+ tcCheckRho expr2 elt_ty `thenM` \ expr2' ->
+ tcCheckRho expr3 elt_ty `thenM` \ expr3' ->
newMethodFromName (PArrSeqOrigin seq)
elt_ty enumFromThenToPName `thenM` \ eft ->
tcMonoExpr (HsReify (Reify flavour name)) res_ty
= addErrCtxt (ptext SLIT("At the reification of") <+> ppr name) $
- tcMetaTy tycon_name `thenM` \ reify_ty ->
- unifyTauTy res_ty reify_ty `thenM_`
+ tcMetaTy tycon_name `thenM` \ reify_ty ->
+ zapExpectedTo res_ty reify_ty `thenM_`
returnM (HsReify (ReifyOut flavour name))
where
tycon_name = case flavour of
\begin{code}
tcApp :: RenamedHsExpr -> [RenamedHsExpr] -- Function and args
- -> TcType -- Expected result type of application
+ -> Expected TcRhoType -- Expected result type of application
-> TcM TcExpr -- Translated fun and args
tcApp (HsApp e1 e2) args res_ty
tcApp fun args res_ty
= -- First type-check the function
- tcExpr_id fun `thenM` \ (fun', fun_ty) ->
+ tcInferRho fun `thenM` \ (fun', fun_ty) ->
addErrCtxt (wrongArgsCtxt "too many" fun args) (
traceTc (text "tcApp" <+> (ppr fun $$ ppr fun_ty)) `thenM_`
-- If an error happens we try to figure out whether the
-- function has been given too many or too few arguments,
--- and say so
-checkArgsCtxt fun args expected_res_ty actual_res_ty tidy_env
+-- and say so.
+-- The ~(Check...) is because in the Infer case the tcSubExp
+-- definitely won't fail, so we can be certain we're in the Check branch
+checkArgsCtxt fun args ~(Check expected_res_ty) actual_res_ty tidy_env
= zonkTcType expected_res_ty `thenM` \ exp_ty' ->
zonkTcType actual_res_ty `thenM` \ act_ty' ->
let
returnM (env2, message)
-split_fun_ty :: TcType -- The type of the function
+split_fun_ty :: TcRhoType -- The type of the function
-> Int -- Number of arguments
-> TcM ([TcType], -- Function argument types
TcType) -- Function result types
tcArg the_fun (arg, expected_arg_ty, arg_no)
= addErrCtxt (funAppCtxt the_fun arg arg_no) $
- tcExpr arg expected_arg_ty
+ tcCheckSigma arg expected_arg_ty
\end{code}
b) perhaps fewer separated lambdas
\begin{code}
-tcId :: Name -> TcM (TcExpr, TcType)
+tcId :: Name -> TcM (TcExpr, TcRhoType)
tcId name -- Look up the Id and instantiate its type
= -- First check whether it's a DataCon
-- Reason: we must not forget to chuck in the
mkFunTys arg_tys result_ty)
\end{code}
-Typecheck expression which in most cases will be an Id.
-The expression can return a higher-ranked type, such as
- (forall a. a->a) -> Int
-so we must create a HoleTyVarTy to pass in as the expected tyvar.
-
-\begin{code}
-tcExpr_id :: RenamedHsExpr -> TcM (TcExpr, TcType)
-tcExpr_id (HsVar name) = tcId name
-tcExpr_id expr = newHoleTyVarTy `thenM` \ id_ty ->
- tcMonoExpr expr id_ty `thenM` \ expr' ->
- readHoleResult id_ty `thenM` \ id_ty' ->
- returnM (expr', id_ty')
-\end{code}
-
-
%************************************************************************
%* *
\subsection{Record bindings}
-- The caller of tcRecordBinds has already checked
-- that all the fields come from the same type
- tcExpr rhs field_ty `thenM` \ rhs' ->
+ tcCheckSigma rhs field_ty `thenM` \ rhs' ->
returnM (sel_id, rhs')
%************************************************************************
%* *
-\subsection{@tcMonoExprs@ typechecks a {\em list} of expressions}
+\subsection{@tcCheckRhos@ typechecks a {\em list} of expressions}
%* *
%************************************************************************
\begin{code}
-tcMonoExprs :: [RenamedHsExpr] -> [TcType] -> TcM [TcExpr]
+tcCheckRhos :: [RenamedHsExpr] -> [TcType] -> TcM [TcExpr]
-tcMonoExprs [] [] = returnM []
-tcMonoExprs (expr:exprs) (ty:tys)
- = tcMonoExpr expr ty `thenM` \ expr' ->
- tcMonoExprs exprs tys `thenM` \ exprs' ->
+tcCheckRhos [] [] = returnM []
+tcCheckRhos (expr:exprs) (ty:tys)
+ = tcCheckRho expr ty `thenM` \ expr' ->
+ tcCheckRhos exprs tys `thenM` \ exprs' ->
returnM (expr':exprs')
\end{code}
Overloaded literals.
\begin{code}
-tcLit :: HsLit -> TcType -> TcM TcExpr
+tcLit :: HsLit -> Expected TcRhoType -> TcM TcExpr
tcLit (HsLitLit s _) res_ty
- = tcLookupClass cCallableClassName `thenM` \ cCallableClass ->
+ = zapExpectedType res_ty `thenM` \ res_ty' ->
+ tcLookupClass cCallableClassName `thenM` \ cCallableClass ->
newDicts (LitLitOrigin (unpackFS s))
- [mkClassPred cCallableClass [res_ty]] `thenM` \ dicts ->
+ [mkClassPred cCallableClass [res_ty']] `thenM` \ dicts ->
extendLIEs dicts `thenM_`
- returnM (HsLit (HsLitLit s res_ty))
+ returnM (HsLit (HsLitLit s res_ty'))
tcLit lit res_ty
- = unifyTauTy res_ty (hsLitType lit) `thenM_`
+ = zapExpectedTo res_ty (hsLitType lit) `thenM_`
returnM (HsLit lit)
\end{code}
import TcRnMonad
import TcMonoType ( tcHsSigType, UserTypeCtxt(..) )
import TcHsSyn ( TcMonoBinds, TypecheckedForeignDecl, TcForeignDecl )
-import TcExpr ( tcExpr )
+import TcExpr ( tcCheckSigma )
import ErrUtils ( Message )
import Id ( Id, mkLocalId, mkVanillaGlobal, setIdLocalExported )
addErrCtxt (foreignDeclCtxt fo) $
tcHsSigType (ForSigCtxt nm) hs_ty `thenM` \ sig_ty ->
- tcExpr (HsVar nm) sig_ty `thenM` \ rhs ->
+ tcCheckSigma (HsVar nm) sig_ty `thenM` \ rhs ->
tcCheckFEType sig_ty spec `thenM_`
putTcTyVar, getTcTyVar,
newMutTyVar, readMutTyVar, writeMutTyVar,
- newHoleTyVarTy, readHoleResult, zapToType,
-
--------------------------------
-- Instantiation
tcInstTyVar, tcInstTyVars, tcInstType,
tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
tcSplitTyConApp_maybe, tcSplitForAllTys,
tcIsTyVarTy, tcSplitSigmaTy, mkTyConApp,
- isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy,
+ isUnLiftedType, isIPPred, isTyVarTy,
mkAppTy, mkTyVarTy, mkTyVarTys,
tyVarsOfPred, getClassPredTys_maybe,
import Name ( Name, setNameUnique, mkSystemTvNameEncoded )
import VarSet
import CmdLineOpts ( dopt, DynFlag(..) )
-import Util ( nOfThem, isSingleton, equalLength, notNull )
+import Util ( nOfThem, isSingleton, equalLength, notNull, lengthExceeds )
import ListSetOps ( equivClasses, removeDups )
import Outputable
\end{code}
%************************************************************************
%* *
-\subsection{'hole' type variables}
-%* *
-%************************************************************************
-
-\begin{code}
-newHoleTyVarTy :: TcM TcType
- = newUnique `thenM` \ uniq ->
- newMutTyVar (mkSystemTvNameEncoded uniq FSLIT("h")) openTypeKind HoleTv `thenM` \ tv ->
- returnM (TyVarTy tv)
-
-readHoleResult :: TcType -> TcM TcType
--- Read the answer out of a hole, constructed by newHoleTyVarTy
-readHoleResult (TyVarTy tv)
- = ASSERT( isHoleTyVar tv )
- getTcTyVar tv `thenM` \ maybe_res ->
- case maybe_res of
- Just ty -> returnM ty
- Nothing -> pprPanic "readHoleResult: empty" (ppr tv)
-readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
-
-zapToType :: TcType -> TcM TcType
-zapToType (TyVarTy tv)
- | isHoleTyVar tv
- = getTcTyVar tv `thenM` \ maybe_res ->
- case maybe_res of
- Nothing -> newTyVarTy openTypeKind `thenM` \ ty ->
- putTcTyVar tv ty `thenM_`
- returnM ty
- Just ty -> returnM ty -- No need to loop; we never
- -- have chains of holes
-
-zapToType other_ty = returnM other_ty
-\end{code}
-
-%************************************************************************
-%* *
\subsection{Type instantiation}
%* *
%************************************************************************
module TcMatches where
-tcGRHSs :: HsExpr.HsMatchContext Name.Name
+tcGRHSs :: HsExpr.HsMatchContext Name.Name
-> RnHsSyn.RenamedGRHSs
- -> TcType.TcType
+ -> TcUnify.Expected TcType.TcType
-> TcRnTypes.TcM TcHsSyn.TcGRHSs
tcMatchesFun :: Name.Name
- -> TcType.TcType
-> [RnHsSyn.RenamedMatch]
+ -> TcUnify.Expected TcType.TcType
-> TcRnTypes.TcM [TcHsSyn.TcMatch]
#include "HsVersions.h"
-import {-# SOURCE #-} TcExpr( tcMonoExpr )
+import {-# SOURCE #-} TcExpr( tcCheckRho, tcMonoExpr )
import HsSyn ( HsExpr(..), HsBinds(..), Match(..), GRHSs(..), GRHS(..),
MonoBinds(..), Stmt(..), HsMatchContext(..), HsStmtContext(..),
import Inst ( tcSyntaxName, tcInstCall )
import TcEnv ( TcId, tcLookupLocalIds, tcLookupId, tcExtendLocalValEnv, tcExtendLocalValEnv2 )
import TcPat ( tcPat, tcMonoPatBndr )
-import TcMType ( newTyVarTy, newTyVarTys, zonkTcType, zapToType )
+import TcMType ( newTyVarTy, newTyVarTys, zonkTcType )
import TcType ( TcType, TcTyVar, TcSigmaType, TcRhoType,
tyVarsOfType, tidyOpenTypes, tidyOpenType, isSigmaTy,
mkFunTy, isOverloadedTy, liftedTypeKind, openTypeKind,
mkArrowKind, mkAppTy )
import TcBinds ( tcBindsAndThen )
-import TcUnify ( unifyPArrTy,subFunTy, unifyListTy, unifyTauTy,
+import TcUnify ( Expected(..), newHole, zapExpectedType, zapExpectedBranches, readExpectedType,
+ unifyTauTy, subFunTy, unifyPArrTy, unifyListTy, unifyFunTy,
checkSigTyVarsWrt, tcSubExp, tcGen )
import TcSimplify ( tcSimplifyCheck, bindInstsOfLocalFuns )
import Name ( Name )
\begin{code}
tcMatchesFun :: Name
- -> TcType -- Expected type
-> [RenamedMatch]
+ -> Expected TcRhoType -- Expected type
-> TcM [TcMatch]
-tcMatchesFun fun_name expected_ty matches@(first_match:_)
+tcMatchesFun fun_name matches@(first_match:_) expected_ty
= -- Check that they all have the same no of arguments
-- Set the location to that of the first equation, so that
-- any inter-equation error messages get some vaguely
\begin{code}
tcMatchesCase :: [RenamedMatch] -- The case alternatives
- -> TcType -- Type of whole case expressions
- -> TcM (TcType, -- Inferred type of the scrutinee
- [TcMatch]) -- Translated alternatives
+ -> Expected TcRhoType -- Type of whole case expressions
+ -> TcM (TcRhoType, -- Inferred type of the scrutinee
+ [TcMatch]) -- Translated alternatives
+
+tcMatchesCase matches (Check expr_ty)
+ = -- This case is a bit yukky, because it prevents the
+ -- scrutinee being higher-ranked, which might just possible
+ -- matter if we were seq'ing on it. But it's awkward to fix.
+ newTyVarTy openTypeKind `thenM` \ scrut_ty ->
+ tcMatches CaseAlt matches (Check (mkFunTy scrut_ty expr_ty)) `thenM` \ matches' ->
+ returnM (scrut_ty, matches')
-tcMatchesCase matches expr_ty
- = newTyVarTy openTypeKind `thenM` \ scrut_ty ->
- tcMatches CaseAlt matches (mkFunTy scrut_ty expr_ty) `thenM` \ matches' ->
+tcMatchesCase matches (Infer hole)
+ = newHole `thenM` \ fun_hole ->
+ tcMatches CaseAlt matches (Infer fun_hole) `thenM` \ matches' ->
+ readMutVar fun_hole `thenM` \ fun_ty ->
+ -- The result of tcMatches is bound to be a function type
+ unifyFunTy fun_ty `thenM` \ (scrut_ty, res_ty) ->
+ writeMutVar hole res_ty `thenM_`
returnM (scrut_ty, matches')
+
-tcMatchLambda :: RenamedMatch -> TcType -> TcM TcMatch
+tcMatchLambda :: RenamedMatch -> Expected TcRhoType -> TcM TcMatch
tcMatchLambda match res_ty = tcMatch LambdaExpr match res_ty
\end{code}
\begin{code}
tcMatches :: RenamedMatchContext
-> [RenamedMatch]
- -> TcType
+ -> Expected TcRhoType
-> TcM [TcMatch]
-tcMatches ctxt matches expected_ty
- = -- If there is more than one branch, and expected_ty is a 'hole',
+tcMatches ctxt matches exp_ty
+ = -- If there is more than one branch, and exp_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
- returnM expected_ty) `thenM` \ expected_ty' ->
-
- mappM (tc_match expected_ty') matches
+ -- order in which we check them would affect the result.
+ zapExpectedBranches matches exp_ty `thenM` \ exp_ty' ->
+ mappM (tc_match exp_ty') matches
where
- tc_match expected_ty match = tcMatch ctxt match expected_ty
+ tc_match exp_ty match = tcMatch ctxt match exp_ty
\end{code}
\begin{code}
tcMatch :: RenamedMatchContext
-> RenamedMatch
- -> TcType -- Expected result-type of the Match.
+ -> Expected TcRhoType -- Expected result-type of the Match.
-- Early unification with this guy gives better error messages
-- We regard the Match as having type
-- (ty1 -> ... -> tyn -> result_ty)
Just sig -> tcAddScopedTyVars [sig] $
-- Bring into scope the type variables in the signature
- tcHsSigType ResSigCtxt sig `thenM` \ sig_ty ->
- tcThingWithSig sig_ty (tcGRHSs ctxt grhss) rhs_ty `thenM` \ (co_fn, grhss') ->
- returnM (lift_grhss co_fn rhs_ty grhss')
-
--- lift_grhss pushes the coercion down to the right hand sides,
--- because there is no convenient place to hang it otherwise.
-lift_grhss co_fn rhs_ty grhss
- | isIdCoercion co_fn = grhss
+ tcHsSigType ResSigCtxt sig `thenM` \ sig_ty ->
+ tcThingWithSig sig_ty (tcGRHSs ctxt grhss . Check) rhs_ty `thenM` \ (co_fn, grhss') ->
+
+ -- Pushes the coercion down to the right hand sides,
+ -- because there is no convenient place to hang it otherwise.
+ if isIdCoercion co_fn then
+ returnM grhss'
+ else
+ readExpectedType rhs_ty `thenM` \ rhs_ty' ->
+ returnM (lift_grhss co_fn rhs_ty' grhss')
+
lift_grhss co_fn rhs_ty (GRHSs grhss binds ty)
= GRHSs (map lift_grhs grhss) binds rhs_ty -- Change the type, since the coercion does
where
tcGRHSs :: RenamedMatchContext -> RenamedGRHSs
- -> TcType
+ -> Expected TcRhoType
-> TcM TcGRHSs
-tcGRHSs ctxt (GRHSs grhss binds _) expected_ty
- = tcBindsAndThen glue_on binds (tc_grhss grhss)
- where
- m_ty = (\ty -> ty, expected_ty)
-
- tc_grhss grhss
- = mappM tc_grhs grhss `thenM` \ grhss' ->
- returnM (GRHSs grhss' EmptyBinds expected_ty)
-
- tc_grhs (GRHS guarded locn)
+ -- Special case when there is just one equation with a degenerate
+ -- guard; then we pass in the full Expected type, so that we get
+ -- good inference from simple things like
+ -- f = \(x::forall a.a->a) -> <stuff>
+ -- This is a consequence of the fact that tcStmts takes a TcType,
+ -- not a Expected TcType, a decision we could revisit if necessary
+tcGRHSs ctxt (GRHSs [GRHS [ResultStmt rhs loc1] loc2] binds _) exp_ty
+ = tcBindsAndThen glue_on binds $
+ tcMonoExpr rhs exp_ty `thenM` \ rhs' ->
+ readExpectedType exp_ty `thenM` \ exp_ty' ->
+ returnM (GRHSs [GRHS [ResultStmt rhs' loc1] loc2] EmptyBinds exp_ty')
+
+tcGRHSs ctxt (GRHSs grhss binds _) exp_ty
+ = tcBindsAndThen glue_on binds $
+ zapExpectedType exp_ty `thenM` \ exp_ty' ->
+ -- Even if there is only one guard, we zap the RHS type to
+ -- a monotype. Reason: it makes tcStmts much easier,
+ -- and even a one-armed guard has a notional second arm
+ let
+ tc_grhs (GRHS guarded locn)
= addSrcLoc locn $
tcStmts (PatGuard ctxt) m_ty guarded `thenM` \ guarded' ->
returnM (GRHS guarded' locn)
+
+ m_ty = (\ty -> ty, exp_ty')
+ in
+ mappM tc_grhs grhss `thenM` \ grhss' ->
+ returnM (GRHSs grhss' EmptyBinds exp_ty')
\end{code}
\begin{code}
tcThingWithSig :: TcSigmaType -- Type signature
-> (TcRhoType -> TcM r) -- How to type check the thing inside
- -> TcRhoType -- Overall expected result type
+ -> Expected TcRhoType -- Overall expected result type
-> TcM (ExprCoFn, r)
-- Used for expressions with a type signature, and for result type signatures
\begin{code}
tcMatchPats
- :: [RenamedPat] -> TcType
- -> (TcType -> TcM a)
+ :: [RenamedPat] -> Expected TcRhoType
+ -> (Expected TcRhoType -> TcM a)
-> TcM ([TcPat], a, TcHsBinds)
-- Typecheck the patterns, extend the environment to bind the variables,
-- do the thing inside, use any existentially-bound dictionaries to
-- 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 ex_tvs ex_ids ex_lie lie_req expected_ty `thenM` \ ex_binds ->
- -- NB: we *must* pass "expected_ty" not "result_ty" to tcCheckExistentialPat
+ readExpectedType expected_ty `thenM` \ exp_ty ->
+ tcCheckExistentialPat ex_tvs ex_ids ex_lie lie_req exp_ty `thenM` \ ex_binds ->
+ -- NB: we *must* pass "exp_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
%************************************************************************
\begin{code}
-tcDoStmts :: HsStmtContext Name -> [RenamedStmt] -> [Name] -> TcType
+tcDoStmts :: HsStmtContext Name -> [RenamedStmt] -> [Name]
+ -> TcRhoType -- To keep it simple, we don't have an "expected" type here
-> TcM (TcMonoBinds, [TcStmt], [Id])
tcDoStmts PArrComp stmts method_names res_ty
= unifyPArrTy res_ty `thenM` \elt_ty ->
:: (TcStmt -> thing -> thing) -- Combiner
-> HsStmtContext Name
-> (TcType -> TcType, TcType) -- m, the relationship type of pat and rhs in pat <- rhs
- -- elt_ty, where type of the comprehension is (m elt_ty)
+ -- res_ty, the type of the entire comprehension
+ -- used at the end for the type of (return x)
+ -- or the final expression in do-notation
-> [RenamedStmt]
-> TcM thing
-> TcM thing
thing_inside
tcStmtAndThen combine do_or_lc m_ty@(m,elt_ty) stmt@(BindStmt pat exp src_loc) thing_inside
- = addSrcLoc src_loc $
- addErrCtxt (stmtCtxt do_or_lc stmt) $
- newTyVarTy liftedTypeKind `thenM` \ pat_ty ->
- tcMonoExpr exp (m pat_ty) `thenM` \ exp' ->
- tcMatchPats [pat] (mkFunTy pat_ty (m elt_ty)) (\ _ ->
+ = addSrcLoc src_loc $
+ addErrCtxt (stmtCtxt do_or_lc stmt) $
+ newTyVarTy liftedTypeKind `thenM` \ pat_ty ->
+ tcCheckRho exp (m pat_ty) `thenM` \ exp' ->
+ tcMatchPats [pat] (Check (mkFunTy pat_ty (m elt_ty))) (\ _ ->
popErrCtxt thing_inside
) `thenM` \ ([pat'], thing, dict_binds) ->
returnM (combine (BindStmt pat' exp' src_loc)
-- Unify the types of the "final" Ids with those of "knot-tied" Ids
tc_ret (rec_name, mono_ty)
- = tcLookupId rec_name `thenM` \ poly_id ->
+ = tcLookupId rec_name `thenM` \ poly_id ->
-- poly_id may have a polymorphic type
-- but mono_ty is just a monomorphic type variable
- tcSubExp mono_ty (idType poly_id) `thenM` \ co_fn ->
+ tcSubExp (Check mono_ty) (idType poly_id) `thenM` \ co_fn ->
returnM (co_fn <$> HsVar poly_id)
-- ExprStmt
-tcStmtAndThen combine do_or_lc m_ty@(m, res_elt_ty) stmt@(ExprStmt exp _ locn) thing_inside
+tcStmtAndThen combine do_or_lc m_ty@(m, _) stmt@(ExprStmt exp _ locn) thing_inside
= addErrCtxt (stmtCtxt do_or_lc stmt) (
if isDoExpr do_or_lc then
newTyVarTy openTypeKind `thenM` \ any_ty ->
- tcMonoExpr exp (m any_ty) `thenM` \ exp' ->
+ tcCheckRho exp (m any_ty) `thenM` \ exp' ->
returnM (ExprStmt exp' any_ty locn)
else
- tcMonoExpr exp boolTy `thenM` \ exp' ->
+ tcCheckRho exp boolTy `thenM` \ exp' ->
returnM (ExprStmt exp' boolTy locn)
) `thenM` \ stmt' ->
tcStmtAndThen combine do_or_lc m_ty@(m, res_elt_ty) stmt@(ResultStmt exp locn) thing_inside
= addErrCtxt (resCtxt do_or_lc stmt) (
if isDoExpr do_or_lc then
- tcMonoExpr exp (m res_elt_ty)
+ tcCheckRho exp (m res_elt_ty)
else
- tcMonoExpr exp res_elt_ty
+ tcCheckRho exp res_elt_ty
) `thenM` \ exp' ->
thing_inside `thenM` \ thing ->
newMethodFromName, newOverloadedLit, newDicts,
instToId, tcInstDataCon, tcSyntaxName
)
-import Id ( mkLocalId, mkSysLocal )
+import Id ( idType, mkLocalId, mkSysLocal )
import Name ( Name )
import FieldLabel ( fieldLabelName )
import TcEnv ( tcLookupClass, tcLookupDataCon, tcLookupId )
-import TcMType ( newTyVarTy, zapToType, arityErr )
+import TcMType ( newTyVarTy, arityErr )
import TcType ( TcType, TcTyVar, TcSigmaType,
mkClassPred, liftedTypeKind )
-import TcUnify ( tcSubOff, TcHoleType,
- unifyTauTy, unifyListTy, unifyPArrTy, unifyTupleTy )
+import TcUnify ( tcSubOff, Expected(..), readExpectedType, zapExpectedType,
+ unifyTauTy, zapToListTy, zapToPArrTy, zapToTupleTy )
import TcMonoType ( tcHsSigType, UserTypeCtxt(..) )
import TysWiredIn ( stringTy )
%************************************************************************
\begin{code}
-type BinderChecker = Name -> TcSigmaType -> TcM (PatCoFn, TcId)
+type BinderChecker = Name -> Expected TcSigmaType -> TcM (PatCoFn, TcId)
-- How to construct a suitable (monomorphic)
-- Id for variables found in the pattern
-- The TcSigmaType is the expected type
-- so there's no polymorphic guy to worry about
tcMonoPatBndr binder_name pat_ty
- = zapToType pat_ty `thenM` \ pat_ty' ->
+ = zapExpectedType pat_ty `thenM` \ 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*
tcPat :: BinderChecker
-> RenamedPat
- -> 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.
+ -> Expected TcSigmaType -- Expected type derived from the context
+ -- In the case of a function with a rank-2 signature,
+ -- this type might be a forall type.
-> TcM (TcPat,
Bag TcTyVar, -- TyVars bound by the pattern
returnM (LazyPat pat', tvs, ids, lie_avail)
tcPat tc_bndr pat_in@(AsPat name pat) pat_ty
- = tc_bndr name pat_ty `thenM` \ (co_fn, bndr_id) ->
- tcPat tc_bndr pat pat_ty `thenM` \ (pat', tvs, ids, lie_avail) ->
+ = tc_bndr name pat_ty `thenM` \ (co_fn, bndr_id) ->
+ tcPat tc_bndr pat (Check (idType bndr_id)) `thenM` \ (pat', tvs, ids, lie_avail) ->
+ -- NB: if we have:
+ -- \ (y@(x::forall a. a->a)) = e
+ -- we'll fail. The as-pattern infers a monotype for 'y', which then
+ -- fails to unify with the polymorphic type for 'x'. This could be
+ -- fixed, but only with a bit more work.
returnM (co_fn <$> (AsPat bndr_id pat'),
tvs, (name, bndr_id) `consBag` ids, lie_avail)
tcPat tc_bndr (WildPat _) pat_ty
- = zapToType pat_ty `thenM` \ pat_ty' ->
+ = zapExpectedType pat_ty `thenM` \ pat_ty' ->
-- We might have an incoming 'hole' type variable; no annotation
-- so zap it to a type. Rather like tcMonoPatBndr.
returnM (WildPat pat_ty', emptyBag, emptyBag, [])
= addErrCtxt (patCtxt pat_in) $
tcHsSigType PatSigCtxt sig `thenM` \ sig_ty ->
tcSubPat sig_ty pat_ty `thenM` \ co_fn ->
- tcPat tc_bndr pat sig_ty `thenM` \ (pat', tvs, ids, lie_avail) ->
+ tcPat tc_bndr pat (Check sig_ty) `thenM` \ (pat', tvs, ids, lie_avail) ->
returnM (co_fn <$> pat', tvs, ids, lie_avail)
\end{code}
\begin{code}
tcPat tc_bndr pat_in@(ListPat pats _) pat_ty
= addErrCtxt (patCtxt pat_in) $
- unifyListTy pat_ty `thenM` \ elem_ty ->
+ zapToListTy pat_ty `thenM` \ elem_ty ->
tcPats tc_bndr pats (repeat elem_ty) `thenM` \ (pats', tvs, ids, lie_avail) ->
returnM (ListPat pats' elem_ty, tvs, ids, lie_avail)
tcPat tc_bndr pat_in@(PArrPat pats _) pat_ty
= addErrCtxt (patCtxt pat_in) $
- unifyPArrTy pat_ty `thenM` \ elem_ty ->
+ zapToPArrTy pat_ty `thenM` \ elem_ty ->
tcPats tc_bndr pats (repeat elem_ty) `thenM` \ (pats', tvs, ids, lie_avail) ->
returnM (PArrPat pats' elem_ty, tvs, ids, lie_avail)
tcPat tc_bndr pat_in@(TuplePat pats boxity) pat_ty
= addErrCtxt (patCtxt pat_in) $
- unifyTupleTy boxity arity pat_ty `thenM` \ arg_tys ->
+ zapToTupleTy boxity arity pat_ty `thenM` \ arg_tys ->
tcPats tc_bndr pats arg_tys `thenM` \ (pats', tvs, ids, lie_avail) ->
-- possibly do the "make all tuple-pats irrefutable" test:
\begin{code}
tcPat tc_bndr (LitPat lit@(HsLitLit s _)) pat_ty
-- cf tcExpr on LitLits
- = tcLookupClass cCallableClassName `thenM` \ cCallableClass ->
+ = zapExpectedType pat_ty `thenM` \ pat_ty' ->
+ tcLookupClass cCallableClassName `thenM` \ cCallableClass ->
newDicts (LitLitOrigin (unpackFS s))
- [mkClassPred cCallableClass [pat_ty]] `thenM` \ dicts ->
+ [mkClassPred cCallableClass [pat_ty']] `thenM` \ dicts ->
extendLIEs dicts `thenM_`
- returnM (LitPat (HsLitLit s pat_ty), emptyBag, emptyBag, [])
+ returnM (LitPat (HsLitLit s pat_ty'), emptyBag, emptyBag, [])
tcPat tc_bndr pat@(LitPat lit@(HsString _)) pat_ty
- = unifyTauTy pat_ty stringTy `thenM_`
+ = zapExpectedType pat_ty `thenM` \ pat_ty' ->
+ unifyTauTy pat_ty' stringTy `thenM_`
tcLookupId eqStringName `thenM` \ eq_id ->
returnM (NPatOut lit stringTy (HsVar eq_id `HsApp` HsLit lit),
- emptyBag, emptyBag, [])
+ emptyBag, emptyBag, [])
tcPat tc_bndr (LitPat simple_lit) pat_ty
- = unifyTauTy pat_ty (hsLitType simple_lit) `thenM_`
+ = zapExpectedType pat_ty `thenM` \ pat_ty' ->
+ unifyTauTy pat_ty' (hsLitType simple_lit) `thenM_`
returnM (LitPat simple_lit, emptyBag, emptyBag, [])
tcPat tc_bndr pat@(NPatIn over_lit mb_neg) pat_ty
- = newOverloadedLit origin over_lit pat_ty `thenM` \ pos_lit_expr ->
- newMethodFromName origin pat_ty eqName `thenM` \ eq ->
+ = zapExpectedType pat_ty `thenM` \ pat_ty' ->
+ newOverloadedLit origin over_lit pat_ty' `thenM` \ pos_lit_expr ->
+ newMethodFromName origin pat_ty' eqName `thenM` \ eq ->
(case mb_neg of
Nothing -> returnM pos_lit_expr -- Positive literal
Just neg -> -- Negative literal
-- The 'negate' is re-mappable syntax
- tcSyntaxName origin pat_ty negateName neg `thenM` \ (neg_expr, _) ->
+ tcSyntaxName origin pat_ty' negateName neg `thenM` \ (neg_expr, _) ->
returnM (HsApp neg_expr pos_lit_expr)
) `thenM` \ lit_expr ->
- returnM (NPatOut lit' pat_ty (HsApp (HsVar eq) lit_expr),
- emptyBag, emptyBag, [])
- where
- origin = PatOrigin pat
-
+ let
-- The literal in an NPatIn is always positive...
-- But in NPat, the literal is used to find identical patterns
-- so we must negate the literal when necessary!
- lit' = case (over_lit, mb_neg) of
- (HsIntegral i _, Nothing) -> HsInteger i
- (HsIntegral i _, Just _) -> HsInteger (-i)
- (HsFractional f _, Nothing) -> HsRat f pat_ty
- (HsFractional f _, Just _) -> HsRat (-f) pat_ty
+ lit' = case (over_lit, mb_neg) of
+ (HsIntegral i _, Nothing) -> HsInteger i
+ (HsIntegral i _, Just _) -> HsInteger (-i)
+ (HsFractional f _, Nothing) -> HsRat f pat_ty'
+ (HsFractional f _, Just _) -> HsRat (-f) pat_ty'
+ in
+ returnM (NPatOut lit' pat_ty' (HsApp (HsVar eq) lit_expr),
+ emptyBag, emptyBag, [])
+ where
+ origin = PatOrigin pat
\end{code}
%************************************************************************
\begin{code}
tcPat tc_bndr pat@(NPlusKPatIn name lit@(HsIntegral i _) minus_name) pat_ty
- = tc_bndr name pat_ty `thenM` \ (co_fn, bndr_id) ->
- newOverloadedLit origin lit pat_ty `thenM` \ over_lit_expr ->
- newMethodFromName origin pat_ty geName `thenM` \ ge ->
+ = tc_bndr name pat_ty `thenM` \ (co_fn, bndr_id) ->
+ let
+ pat_ty' = idType bndr_id
+ in
+ newOverloadedLit origin lit pat_ty' `thenM` \ over_lit_expr ->
+ newMethodFromName origin pat_ty' geName `thenM` \ ge ->
-- The '-' part is re-mappable syntax
- tcSyntaxName origin pat_ty minusName minus_name `thenM` \ (minus_expr, _) ->
+ tcSyntaxName origin pat_ty' minusName minus_name `thenM` \ (minus_expr, _) ->
returnM (NPlusKPatOut bndr_id i
(SectionR (HsVar ge) over_lit_expr)
origin = PatOrigin pat
\end{code}
+
%************************************************************************
%* *
\subsection{Lists of patterns}
tcPats tc_bndr [] tys = returnM ([], emptyBag, emptyBag, [])
-tcPats tc_bndr (ty:tys) (pat:pats)
- = tcPat tc_bndr ty pat `thenM` \ (pat', tvs1, ids1, lie_avail1) ->
- tcPats tc_bndr tys pats `thenM` \ (pats', tvs2, ids2, lie_avail2) ->
+tcPats tc_bndr (pat:pats) (ty:tys)
+ = tcPat tc_bndr pat (Check ty) `thenM` \ (pat', tvs1, ids1, lie_avail1) ->
+ tcPats tc_bndr pats tys `thenM` \ (pats', tvs2, ids2, lie_avail2) ->
returnM (pat':pats',
tvs1 `unionBags` tvs2, ids1 `unionBags` ids2,
(arityErr "Constructor" data_con con_arity 2) `thenM_`
-- Check arguments
- tcPat tc_bndr p1 ty1 `thenM` \ (p1', tvs1, ids1, lie_avail1) ->
- tcPat tc_bndr p2 ty2 `thenM` \ (p2', tvs2, ids2, lie_avail2) ->
+ tcPat tc_bndr p1 (Check ty1) `thenM` \ (p1', tvs1, ids1, lie_avail1) ->
+ tcPat tc_bndr p2 (Check ty2) `thenM` \ (p2', tvs2, ids2, lie_avail2) ->
returnM (InfixCon p1' p2',
tvs1 `unionBags` tvs2, ids1 `unionBags` ids2,
returnM (sel_id, pat_ty)
) `thenM` \ (sel_id, pat_ty) ->
- tcPat tc_bndr rhs_pat pat_ty `thenM` \ (rhs_pat', tvs2, ids2, lie_avail2) ->
+ tcPat tc_bndr rhs_pat (Check pat_ty) `thenM` \ (rhs_pat', tvs2, ids2, lie_avail2) ->
returnM ((sel_id, rhs_pat') : rpats',
tvs1 `unionBags` tvs2,
(forall a. a->a in the example)
\begin{code}
-tcSubPat :: TcSigmaType -> TcHoleType -> TcM PatCoFn
+tcSubPat :: TcSigmaType -> Expected TcSigmaType -> TcM PatCoFn
tcSubPat sig_ty exp_ty
= tcSubOff sig_ty exp_ty `thenM` \ co_fn ->
returnM idCoercion
else
newUnique `thenM` \ uniq ->
+ readExpectedType exp_ty `thenM` \ exp_ty' ->
let
- arg_id = mkSysLocal FSLIT("sub") uniq exp_ty
+ arg_id = mkSysLocal FSLIT("sub") uniq exp_ty'
the_fn = DictLam [arg_id] (co_fn <$> HsVar arg_id)
- pat_co_fn p = SigPatOut p exp_ty the_fn
+ pat_co_fn p = SigPatOut p exp_ty' the_fn
in
returnM (mkCoercion pat_co_fn)
\end{code}
zonkTopExpr, zonkTopBndrs
)
-import TcExpr ( tcExpr_id )
+import TcExpr ( tcInferRho )
import TcRnMonad
import TcMType ( newTyVarTy, zonkTcType )
import TcType ( Type, liftedTypeKind,
-- Now typecheck the expression;
-- it might have a rank-2 type (e.g. :t runST)
- -- Hence the hole type (c.f. TcExpr.tcExpr_id)
- ((tc_expr, res_ty), lie) <- getLIE (tcExpr_id rn_expr) ;
+ ((tc_expr, res_ty), lie) <- getLIE (tcInferRho rn_expr) ;
((qtvs, _, dict_ids), lie_top) <- getLIE (tcSimplifyInfer smpl_doc (tyVarsOfType res_ty) lie) ;
tcSimplifyTop lie_top ;
-- $main :: IO () = runIO main
let { rhs = HsApp (HsVar runIOName) (HsVar main_name) } ;
- (main_expr, ty) <- tcExpr_id rhs ;
+ (main_expr, ty) <- tcInferRho rhs ;
let { dollar_main_id = setIdLocalExported (mkLocalId dollarMainName ty) ;
main_bind = VarMonoBind dollar_main_id main_expr ;
import TcRnMonad
import TcSimplify ( tcSimplifyToDicts, tcSimplifyInferCheck )
import TcMType ( newTyVarTy )
+import TcUnify ( Expected(..) )
import TcType ( tyVarsOfTypes, openTypeKind )
import TcIfaceSig ( tcCoreExpr, tcCoreLamBndrs )
import TcMonoType ( tcHsSigType, UserTypeCtxt(..), tcAddScopedTyVars )
-import TcExpr ( tcMonoExpr )
+import TcExpr ( tcCheckRho )
import TcEnv ( tcExtendLocalValEnv, tcLookupGlobalId, tcLookupId )
import Inst ( instToId )
import Id ( idType, mkLocalId )
tcExtendLocalValEnv ids $
-- Now LHS and RHS
- getLIE (tcMonoExpr lhs rule_ty) `thenM` \ (lhs', lhs_lie) ->
- getLIE (tcMonoExpr rhs rule_ty) `thenM` \ (rhs', rhs_lie) ->
+ getLIE (tcCheckRho lhs rule_ty) `thenM` \ (lhs', lhs_lie) ->
+ getLIE (tcCheckRho rhs rule_ty) `thenM` \ (rhs', rhs_lie) ->
returnM (ids, lhs', rhs', lhs_lie, rhs_lie)
) `thenM` \ (ids, lhs', rhs', lhs_lie, rhs_lie) ->
import RnExpr ( rnExpr )
import RdrHsSyn ( RdrNameHsExpr, RdrNameHsDecl )
import RnHsSyn ( RenamedHsExpr )
-import TcExpr ( tcMonoExpr )
+import TcExpr ( tcCheckRho )
import TcHsSyn ( TcExpr, TypecheckedHsExpr, mkHsLet, zonkTopExpr )
import TcSimplify ( tcSimplifyTop, tcSimplifyBracket )
import TcUnify ( unifyTauTy )
tc_bracket :: HsBracket Name -> TcM TcType
tc_bracket (ExpBr expr)
- = newTyVarTy openTypeKind `thenM` \ any_ty ->
- tcMonoExpr expr any_ty `thenM_`
+ = newTyVarTy openTypeKind `thenM` \ any_ty ->
+ tcCheckRho expr any_ty `thenM_`
tcMetaTy exprTyConName
-- Result type is Expr (= Q Exp)
tcMetaTy exprTyConName `thenM` \ meta_exp_ty ->
setStage (Splice next_level) (
setLIEVar lie_var $
- tcMonoExpr expr meta_exp_ty
+ tcCheckRho expr meta_exp_ty
) `thenM` \ expr' ->
-- Write the pending splice into the bucket
-- Note that we do not decrement the level (to -1) before
-- typechecking the expression. For example:
-- f x = $( ...$(g 3) ... )
--- The recursive call to tcMonoExpr will simply expand the
+-- The recursive call to tcCheckRho will simply expand the
-- inner escape before dealing with the outer one
tcTopSplice expr res_ty
initRn SourceMode (rnExpr expr2) `thenM` \ (exp3, fvs) ->
importSupportingDecls fvs `thenM` \ env ->
- setGblEnv env (tcMonoExpr exp3 res_ty)
+ setGblEnv env (tcCheckRho exp3 res_ty)
tcTopSpliceExpr :: RenamedHsExpr -> TcType -> TcM TypecheckedHsExpr
setStage topSpliceStage $
-- Typecheck the expression
- getLIE (tcMonoExpr expr meta_ty) `thenM` \ (expr', lie) ->
+ getLIE (tcCheckRho expr meta_ty) `thenM` \ (expr', lie) ->
-- Solve the constraints
tcSimplifyTop lie `thenM` \ const_binds ->
--------------------------------
-- TyVarDetails
- TyVarDetails(..), isUserTyVar, isSkolemTyVar, isHoleTyVar,
+ TyVarDetails(..), isUserTyVar, isSkolemTyVar,
tyVarBindingInfo,
--------------------------------
\begin{code}
data TyVarDetails
- = HoleTv -- Used *only* by the type checker when passing in a type
- -- variable that should be side-effected to the result type.
- -- Always has kind openTypeKind.
- -- Never appears in types
-
- | SigTv -- Introduced when instantiating a type signature,
+ = SigTv -- Introduced when instantiating a type signature,
-- prior to checking that the defn of a fn does
-- have the expected type. Should not be instantiated.
--
InstTv -> True
oteher -> False
-isHoleTyVar :: TcTyVar -> Bool
--- NB: the hole might be filled in by now, and this
--- function does not check for that
-isHoleTyVar tv = ASSERT( isMutTyVar tv )
- case mutTyVarDetails tv of
- HoleTv -> True
- other -> False
-
tyVarBindingInfo :: TyVar -> SDoc -- Used in checkSigTyVars
tyVarBindingInfo tv
| isMutTyVar tv
details ClsTv = ptext SLIT("class declaration")
details InstTv = ptext SLIT("instance declaration")
details PatSigTv = ptext SLIT("pattern type signature")
- details HoleTv = ptext SLIT("//hole//") -- Should not happen
details VanillaTv = ptext SLIT("//vanilla//") -- Ditto
\end{code}
\begin{code}
module TcUnify (
-- Full-blown subsumption
- tcSubOff, tcSubExp, tcGen, subFunTy, TcHoleType,
+ tcSubOff, tcSubExp, tcGen,
checkSigTyVars, checkSigTyVarsWrt, sigCtxt, findGlobals,
-- Various unifications
unifyTauTy, unifyTauTyList, unifyTauTyLists,
- unifyFunTy, unifyListTy, unifyPArrTy, unifyTupleTy,
- unifyKind, unifyKinds, unifyOpenTypeKind, unifyFunKind
+ unifyKind, unifyKinds, unifyOpenTypeKind, unifyFunKind,
+
+ --------------------------------
+ -- Holes
+ Expected(..), newHole, readExpectedType,
+ zapExpectedType, zapExpectedTo, zapExpectedBranches,
+ subFunTy, unifyFunTy,
+ zapToListTy, unifyListTy,
+ zapToPArrTy, unifyPArrTy,
+ zapToTupleTy, unifyTupleTy
) where
tcGetTyVar_maybe, tcGetTyVar,
mkFunTy, tyVarsOfType, mkPhiTy,
typeKind, tcSplitFunTy_maybe, mkForAllTys,
- isHoleTyVar, isSkolemTyVar, isUserTyVar,
+ isSkolemTyVar, isUserTyVar,
tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars,
eqKind, openTypeKind, liftedTypeKind, isTypeKind, mkArrowKind,
hasMoreBoxityInfo, allDistinctTyVars
)
import Inst ( newDicts, instToId, tcInstCall )
-import TcMType ( getTcTyVar, putTcTyVar, tcInstType, readHoleResult, newKindVar,
- newTyVarTy, newTyVarTys, newOpenTypeKind, newHoleTyVarTy,
+import TcMType ( getTcTyVar, putTcTyVar, tcInstType, newKindVar,
+ newTyVarTy, newTyVarTys, newOpenTypeKind,
zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV )
import TcSimplify ( tcSimplifyCheck )
import TysWiredIn ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy )
import Name ( isSystemName )
import ErrUtils ( Message )
import BasicTypes ( Boxity, Arity, isBoxed )
-import Util ( equalLength, notNull )
+import Util ( equalLength, lengthExceeds, notNull )
import Outputable
\end{code}
%************************************************************************
%* *
+\subsection{'hole' type variables}
+%* *
+%************************************************************************
+
+\begin{code}
+data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference
+ | Check ty -- The type to check during type checking
+
+newHole :: TcM (TcRef ty)
+newHole = newMutVar (error "Empty hole in typechecker")
+
+readExpectedType :: Expected ty -> TcM ty
+readExpectedType (Infer hole) = readMutVar hole
+readExpectedType (Check ty) = returnM ty
+
+zapExpectedType :: Expected TcType -> TcM TcTauType
+-- In the inference case, ensure we have a monotype
+zapExpectedType (Infer hole)
+ = do { ty <- newTyVarTy openTypeKind ;
+ writeMutVar hole ty ;
+ return ty }
+
+zapExpectedType (Check ty) = return ty
+
+zapExpectedTo :: Expected TcType -> TcTauType -> TcM ()
+zapExpectedTo (Infer hole) ty2 = writeMutVar hole ty2
+zapExpectedTo (Check ty1) ty2 = unifyTauTy ty1 ty2
+
+zapExpectedBranches :: [a] -> Expected TcType -> TcM (Expected TcType)
+-- Zap the expected type to a monotype if there is more than one branch
+zapExpectedBranches branches exp_ty
+ | lengthExceeds branches 1 = zapExpectedType exp_ty `thenM` \ exp_ty' ->
+ return (Check exp_ty')
+ | otherwise = returnM exp_ty
+
+instance Outputable ty => Outputable (Expected ty) where
+ ppr (Check ty) = ptext SLIT("Expected type") <+> ppr ty
+ ppr (Infer hole) = ptext SLIT("Inferring type")
+\end{code}
+
+
+%************************************************************************
+%* *
+\subsection[Unify-fun]{@unifyFunTy@}
+%* *
+%************************************************************************
+
+@subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
+creation of type variables.
+
+* subFunTy is used when we might be faced with a "hole" type variable,
+ in which case we should create two new holes.
+
+* unifyFunTy is used when we expect to encounter only "ordinary"
+ type variables, so we should create new ordinary type variables
+
+\begin{code}
+subFunTy :: Expected TcRhoType -- Fail if ty isn't a function type
+ -- If it's a hole, make two holes, feed them to...
+ -> (Expected TcRhoType -> Expected TcRhoType -> TcM a) -- the thing inside
+ -> TcM a -- and bind the function type to the hole
+
+subFunTy (Infer hole) thing_inside
+ = -- This is the interesting case
+ newHole `thenM` \ arg_hole ->
+ newHole `thenM` \ res_hole ->
+
+ -- Do the business
+ thing_inside (Infer arg_hole) (Infer res_hole) `thenM` \ answer ->
+
+ -- Extract the answers
+ readMutVar arg_hole `thenM` \ arg_ty ->
+ readMutVar res_hole `thenM` \ res_ty ->
+
+ -- Write the answer into the incoming hole
+ writeMutVar hole (mkFunTy arg_ty res_ty) `thenM_`
+
+ -- And return the answer
+ returnM answer
+
+subFunTy (Check ty) thing_inside
+ = unifyFunTy ty `thenM` \ (arg,res) ->
+ thing_inside (Check arg) (Check res)
+
+
+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 `thenM` \ maybe_ty ->
+ case maybe_ty of
+ Just ty' -> unifyFunTy ty'
+ Nothing -> unify_fun_ty_help ty
+
+unifyFunTy ty
+ = case tcSplitFunTy_maybe ty of
+ Just arg_and_res -> returnM arg_and_res
+ Nothing -> unify_fun_ty_help ty
+
+unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
+ = newTyVarTy openTypeKind `thenM` \ arg ->
+ newTyVarTy openTypeKind `thenM` \ res ->
+ unifyTauTy ty (mkFunTy arg res) `thenM_`
+ returnM (arg,res)
+\end{code}
+
+\begin{code}
+zapToListTy :: Expected TcType -- expected list type
+ -> TcM TcType -- list element type
+
+zapToListTy (Check ty) = unifyListTy ty
+zapToListTy (Infer hole) = do { elt_ty <- newTyVarTy liftedTypeKind ;
+ writeMutVar hole (mkListTy elt_ty) ;
+ return elt_ty }
+
+unifyListTy :: TcType -> TcM TcType
+unifyListTy ty@(TyVarTy tyvar)
+ = getTcTyVar tyvar `thenM` \ maybe_ty ->
+ case maybe_ty of
+ Just ty' -> unifyListTy ty'
+ other -> unify_list_ty_help ty
+
+unifyListTy ty
+ = case tcSplitTyConApp_maybe ty of
+ Just (tycon, [arg_ty]) | tycon == listTyCon -> returnM arg_ty
+ other -> unify_list_ty_help ty
+
+unify_list_ty_help ty -- Revert to ordinary unification
+ = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
+ unifyTauTy ty (mkListTy elt_ty) `thenM_`
+ returnM elt_ty
+
+-- variant for parallel arrays
+--
+zapToPArrTy :: Expected TcType -- Expected list type
+ -> TcM TcType -- List element type
+
+zapToPArrTy (Check ty) = unifyPArrTy ty
+zapToPArrTy (Infer hole) = do { elt_ty <- newTyVarTy liftedTypeKind ;
+ writeMutVar hole (mkPArrTy elt_ty) ;
+ return elt_ty }
+
+unifyPArrTy :: TcType -> TcM TcType
+
+unifyPArrTy ty@(TyVarTy tyvar)
+ = getTcTyVar tyvar `thenM` \ maybe_ty ->
+ case maybe_ty of
+ Just ty' -> unifyPArrTy ty'
+ _ -> unify_parr_ty_help ty
+unifyPArrTy ty
+ = case tcSplitTyConApp_maybe ty of
+ Just (tycon, [arg_ty]) | tycon == parrTyCon -> returnM arg_ty
+ _ -> unify_parr_ty_help ty
+
+unify_parr_ty_help ty -- Revert to ordinary unification
+ = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
+ unifyTauTy ty (mkPArrTy elt_ty) `thenM_`
+ returnM elt_ty
+\end{code}
+
+\begin{code}
+zapToTupleTy :: Boxity -> Arity -> Expected TcType -> TcM [TcType]
+zapToTupleTy boxity arity (Check ty) = unifyTupleTy boxity arity ty
+zapToTupleTy boxity arity (Infer hole) = do { (tup_ty, arg_tys) <- new_tuple_ty boxity arity ;
+ writeMutVar hole tup_ty ;
+ return arg_tys }
+
+unifyTupleTy boxity arity ty@(TyVarTy tyvar)
+ = getTcTyVar tyvar `thenM` \ maybe_ty ->
+ case maybe_ty of
+ Just ty' -> unifyTupleTy boxity arity ty'
+ other -> unify_tuple_ty_help boxity arity ty
+
+unifyTupleTy boxity arity ty
+ = case tcSplitTyConApp_maybe ty of
+ Just (tycon, arg_tys)
+ | isTupleTyCon tycon
+ && tyConArity tycon == arity
+ && tupleTyConBoxity tycon == boxity
+ -> returnM arg_tys
+ other -> unify_tuple_ty_help boxity arity ty
+
+unify_tuple_ty_help boxity arity ty
+ = new_tuple_ty boxity arity `thenM` \ (tup_ty, arg_tys) ->
+ unifyTauTy ty tup_ty `thenM_`
+ returnM arg_tys
+
+new_tuple_ty boxity arity
+ = newTyVarTys arity kind `thenM` \ arg_tys ->
+ return (mkTupleTy boxity arity arg_tys, arg_tys)
+ where
+ kind | isBoxed boxity = liftedTypeKind
+ | otherwise = openTypeKind
+\end{code}
+
+
+%************************************************************************
+%* *
\subsection{Subsumption}
%* *
%************************************************************************
expected_ty.
\begin{code}
-type TcHoleType = TcSigmaType -- Either a TcSigmaType,
- -- or else a hole
-
-tcSubExp :: TcHoleType -> TcSigmaType -> TcM ExprCoFn
-tcSubOff :: TcSigmaType -> TcHoleType -> TcM ExprCoFn
-tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn
+tcSubExp :: Expected TcRhoType -> TcRhoType -> TcM ExprCoFn
+tcSubOff :: TcSigmaType -> Expected TcSigmaType -> TcM ExprCoFn
\end{code}
These two check for holes
-- 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 `thenM` \ maybe_ty ->
- case maybe_ty of
- Just ty -> thing_inside ty other_ty
- Nothing -> traceTc (text "checkHole" <+> ppr tv) `thenM_`
- putTcTyVar tv other_ty `thenM_`
- returnM idCoercion
+checkHole (Infer hole) other_ty thing_inside
+ = do { writeMutVar hole other_ty; return idCoercion }
-checkHole ty other_ty thing_inside
+checkHole (Check 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 :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn -- Locally used only
tcSub expected_ty actual_ty
= traceTc (text "tcSub" <+> details) `thenM_`
addErrCtxtM (unifyCtxt "type" expected_ty actual_ty)
-- I'm not quite sure what to do about this!
tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv)
- = ASSERT( not (isHoleTyVar tv) )
- getTcTyVar tv `thenM` \ maybe_ty ->
+ = getTcTyVar tv `thenM` \ maybe_ty ->
case maybe_ty of
Just ty -> tc_sub exp_sty exp_ty ty ty
Nothing -> imitateFun tv exp_sty `thenM` \ (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)
- = ASSERT( not (isHoleTyVar tv) )
- getTcTyVar tv `thenM` \ maybe_ty ->
+ = getTcTyVar tv `thenM` \ maybe_ty ->
case maybe_ty of
Just ty -> tc_sub ty ty act_sty act_ty
Nothing -> imitateFun tv act_sty `thenM` \ (exp_arg, exp_res) ->
imitateFun :: TcTyVar -> TcType -> TcM (TcType, TcType)
imitateFun tv ty
- = ASSERT( not (isHoleTyVar tv) )
- -- NB: tv is an *ordinary* tyvar and so are the new ones
+ = -- NB: tv is an *ordinary* tyvar and so are the new ones
-- Check that tv isn't a type-signature type variable
-- (This would be found later in checkSigTyVars, but
%************************************************************************
%* *
-\subsection[Unify-fun]{@unifyFunTy@}
-%* *
-%************************************************************************
-
-@subFunTy@ and @unifyFunTy@ is used to avoid the fruitless
-creation of type variables.
-
-* subFunTy is used when we might be faced with a "hole" type variable,
- in which case we should create two new holes.
-
-* unifyFunTy is used when we expect to encounter only "ordinary"
- type variables, so we should create new ordinary type variables
-
-\begin{code}
-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 `thenM` \ maybe_ty ->
- case maybe_ty of {
- Just ty' -> subFunTy ty' thing_inside ;
- Nothing ->
-
- newHoleTyVarTy `thenM` \ arg_ty ->
- newHoleTyVarTy `thenM` \ res_ty ->
-
- -- Do the business
- thing_inside arg_ty res_ty `thenM` \ answer ->
-
- -- Extract the answers
- readHoleResult arg_ty `thenM` \ arg_ty' ->
- readHoleResult res_ty `thenM` \ res_ty' ->
-
- -- Write the answer into the incoming hole
- putTcTyVar tyvar (mkFunTy arg_ty' res_ty') `thenM_`
-
- -- And return the answer
- returnM answer }
-
-subFunTy ty thing_inside
- = unifyFunTy ty `thenM` \ (arg,res) ->
- thing_inside arg res
-
-
-unifyFunTy :: TcRhoType -- Fail if ty isn't a function type
- -> TcM (TcType, TcType) -- otherwise return arg and result types
-
-unifyFunTy ty@(TyVarTy tyvar)
- = ASSERT( not (isHoleTyVar tyvar) )
- getTcTyVar tyvar `thenM` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyFunTy ty'
- Nothing -> unify_fun_ty_help ty
-
-unifyFunTy ty
- = case tcSplitFunTy_maybe ty of
- Just arg_and_res -> returnM arg_and_res
- Nothing -> unify_fun_ty_help ty
-
-unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
- = newTyVarTy openTypeKind `thenM` \ arg ->
- newTyVarTy openTypeKind `thenM` \ res ->
- unifyTauTy ty (mkFunTy arg res) `thenM_`
- returnM (arg,res)
-\end{code}
-
-\begin{code}
-unifyListTy :: TcType -- expected list type
- -> TcM TcType -- list element type
-
-unifyListTy ty@(TyVarTy tyvar)
- = getTcTyVar tyvar `thenM` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyListTy ty'
- other -> unify_list_ty_help ty
-
-unifyListTy ty
- = case tcSplitTyConApp_maybe ty of
- Just (tycon, [arg_ty]) | tycon == listTyCon -> returnM arg_ty
- other -> unify_list_ty_help ty
-
-unify_list_ty_help ty -- Revert to ordinary unification
- = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
- unifyTauTy ty (mkListTy elt_ty) `thenM_`
- returnM elt_ty
-
--- variant for parallel arrays
---
-unifyPArrTy :: TcType -- expected list type
- -> TcM TcType -- list element type
-
-unifyPArrTy ty@(TyVarTy tyvar)
- = getTcTyVar tyvar `thenM` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyPArrTy ty'
- _ -> unify_parr_ty_help ty
-unifyPArrTy ty
- = case tcSplitTyConApp_maybe ty of
- Just (tycon, [arg_ty]) | tycon == parrTyCon -> returnM arg_ty
- _ -> unify_parr_ty_help ty
-
-unify_parr_ty_help ty -- Revert to ordinary unification
- = newTyVarTy liftedTypeKind `thenM` \ elt_ty ->
- unifyTauTy ty (mkPArrTy elt_ty) `thenM_`
- returnM elt_ty
-\end{code}
-
-\begin{code}
-unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
-unifyTupleTy boxity arity ty@(TyVarTy tyvar)
- = getTcTyVar tyvar `thenM` \ maybe_ty ->
- case maybe_ty of
- Just ty' -> unifyTupleTy boxity arity ty'
- other -> unify_tuple_ty_help boxity arity ty
-
-unifyTupleTy boxity arity ty
- = case tcSplitTyConApp_maybe ty of
- Just (tycon, arg_tys)
- | isTupleTyCon tycon
- && tyConArity tycon == arity
- && tupleTyConBoxity tycon == boxity
- -> returnM arg_tys
- other -> unify_tuple_ty_help boxity arity ty
-
-unify_tuple_ty_help boxity arity ty
- = newTyVarTys arity kind `thenM` \ arg_tys ->
- unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenM_`
- returnM arg_tys
- where
- kind | isBoxed boxity = liftedTypeKind
- | otherwise = openTypeKind
-\end{code}
-
-
-%************************************************************************
-%* *
\subsection{Kind unification}
%* *
%************************************************************************
projects / ghc-hetmet.git / commitdiff