Commit 221b6b69 authored by simonpj's avatar simonpj
Browse files

[project @ 2003-04-16 13:34:13 by simonpj]

----------------------------------
 Use the Infer/Check idea for typechecking higher-rank types
	----------------------------------

The main idea is that

	data Expected ty = Infer (TcRef ty) | Check ty

	tcMonoExpr :: Expr -> Expected TcRhoType -> TcM Expra


This "Expected" type tells tcMonoExpr whether it's doing inference or
checking.  It replaces the "HoleTv" flavour of type variable.

This actually leads to slightly more lines of code, but it's much
clearer, and the new type distinctions showed up several subtle bugs
in the previous implementation.  It all arose out of writing the
prototype implementation for the paper.

Error messages wibble around a little bit.  I'm not quite certain why!  But the
changes look like improvements to me.
parent 91af47d4
......@@ -36,7 +36,7 @@ module Inst (
#include "HsVersions.h"
import {-# SOURCE #-} TcExpr( tcExpr )
import {-# SOURCE #-} TcExpr( tcCheckSigma )
import HsSyn ( HsLit(..), HsOverLit(..), HsExpr(..) )
import TcHsSyn ( TcExpr, TcId, TcIdSet,
......@@ -46,7 +46,7 @@ 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,
......@@ -353,13 +353,7 @@ newOverloadedLit :: InstOrigin
-> 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
......@@ -372,7 +366,7 @@ new_over_lit orig lit@(HsIntegral i fi) expected_ty
| 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 ->
......@@ -665,9 +659,11 @@ tcSyntaxName orig ty std_nm user_nm
-- 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
......
......@@ -9,7 +9,7 @@ module TcBinds ( tcBindsAndThen, tcTopBinds, tcMonoBinds, tcSpecSigs ) where
#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(..),
......@@ -23,7 +23,7 @@ import TcHsSyn ( TcHsBinds, TcMonoBinds, TcId, zonkId, mkHsLet )
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(..),
......@@ -31,9 +31,7 @@ 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
......@@ -141,7 +139,7 @@ tc_binds_and_then top_lvl combiner (IPBinds binds is_with) do_next
= 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
......@@ -660,8 +658,8 @@ tcMonoBinds mbinds tc_ty_sigs is_rec
-- 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
......@@ -676,8 +674,8 @@ tcMonoBinds mbinds tc_ty_sigs is_rec
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
......@@ -686,13 +684,13 @@ tcMonoBinds mbinds tc_ty_sigs is_rec
| 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))
......@@ -710,18 +708,18 @@ tcMonoBinds mbinds tc_ty_sigs is_rec
-- 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)
......@@ -800,7 +798,7 @@ tcSpecSigs (SpecSig name poly_ty src_loc : sigs)
-- 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
This diff is collapsed.
......@@ -28,7 +28,7 @@ import RnHsSyn ( RenamedForeignDecl )
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 )
......@@ -197,7 +197,7 @@ tcFExport fo@(ForeignExport nm hs_ty spec isDeprec src_loc) =
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_`
......
......@@ -18,8 +18,6 @@ module TcMType (
putTcTyVar, getTcTyVar,
newMutTyVar, readMutTyVar, writeMutTyVar,
newHoleTyVarTy, readHoleResult, zapToType,
--------------------------------
-- Instantiation
tcInstTyVar, tcInstTyVars, tcInstType,
......@@ -54,7 +52,7 @@ import TcType ( TcType, TcThetaType, TcTauType, TcPredType,
tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
tcSplitTyConApp_maybe, tcSplitForAllTys,
tcIsTyVarTy, tcSplitSigmaTy, mkTyConApp,
isUnLiftedType, isIPPred, isHoleTyVar, isTyVarTy,
isUnLiftedType, isIPPred, isTyVarTy,
mkAppTy, mkTyVarTy, mkTyVarTys,
tyVarsOfPred, getClassPredTys_maybe,
......@@ -85,7 +83,7 @@ import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
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}
......@@ -139,42 +137,6 @@ newOpenTypeKind
\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]
......@@ -10,7 +10,7 @@ module TcMatches ( tcMatchesFun, tcMatchesCase, tcMatchLambda,
#include "HsVersions.h"
import {-# SOURCE #-} TcExpr( tcMonoExpr )
import {-# SOURCE #-} TcExpr( tcCheckRho, tcMonoExpr )
import HsSyn ( HsExpr(..), HsBinds(..), Match(..), GRHSs(..), GRHS(..),
MonoBinds(..), Stmt(..), HsMatchContext(..), HsStmtContext(..),
......@@ -29,13 +29,14 @@ import TcMonoType ( tcAddScopedTyVars, tcHsSigType, UserTypeCtxt(..) )
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 )
......@@ -66,11 +67,11 @@ same number of arguments before using @tcMatches@ to do the work.
\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
......@@ -95,16 +96,29 @@ parser guarantees that each equation has exactly one argument.
\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}
......@@ -112,21 +126,17 @@ tcMatchLambda match res_ty = tcMatch LambdaExpr match res_ty
\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}
......@@ -139,7 +149,7 @@ tcMatches ctxt matches expected_ty
\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)
......@@ -160,14 +170,17 @@ tcMatch ctxt match@(Match pats maybe_rhs_sig grhss) expected_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
......@@ -183,29 +196,44 @@ glue_on binds1 (GRHSs grhss binds2 ty)
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
......@@ -235,8 +263,8 @@ tcThingWithSig sig_ty thing_inside res_ty
\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
......@@ -260,8 +288,9 @@ tcMatchPats pats expected_ty thing_inside
-- I'm a bit concerned that lie_req1 from an 'inner' pattern in the list
-- might need (via lie_req2) something made available from an 'outer'
-- pattern. But it's inconvenient to deal with, and I can't find an example
tcCheckExistentialPat 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
......@@ -341,7 +370,8 @@ tcCheckExistentialPat ex_tvs ex_ids ex_lie lie_req match_ty
%************************************************************************
\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 ->
......@@ -425,7 +455,9 @@ tcStmtsAndThen
:: (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
......@@ -446,11 +478,11 @@ tcStmtAndThen combine do_or_lc m_ty (LetStmt binds) thing_inside
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)
......@@ -499,21 +531,21 @@ tcStmtAndThen combine do_or_lc m_ty (RecStmt recNames stmts _) thing_inside
-- 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' ->
......@@ -525,9 +557,9 @@ tcStmtAndThen combine do_or_lc m_ty@(m, res_elt_ty) stmt@(ExprStmt exp _ locn) t
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 ->
......
......@@ -21,15 +21,15 @@ import Inst ( InstOrigin(..),
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 )
......@@ -50,7 +50,7 @@ import FastString
%************************************************************************
\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
......@@ -67,7 +67,7 @@ tcMonoPatBndr :: BinderChecker
-- 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*
......@@ -91,9 +91,9 @@ tcMonoPatBndr binder_name pat_ty
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
......@@ -129,13 +129,18 @@ tcPat tc_bndr (LazyPat pat) pat_ty
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)