Commit b10d7d07 authored by simonpj@microsoft.com's avatar simonpj@microsoft.com

Tidy-up sweep, following the Great Skolemisation Simplification

parent 9a0d8e2b
......@@ -48,7 +48,7 @@ tcProc pat cmd exp_ty
do { (coi, (exp_ty1, res_ty)) <- matchExpectedAppTy exp_ty
; (coi1, (arr_ty, arg_ty)) <- matchExpectedAppTy exp_ty1
; let cmd_env = CmdEnv { cmd_arr = arr_ty }
; (pat', cmd') <- tcPat ProcExpr pat arg_ty res_ty $
; (pat', cmd') <- tcPat ProcExpr pat arg_ty $
tcCmdTop cmd_env cmd [] res_ty
; let res_coi = mkTransCoI coi (mkAppTyCoI coi1 (IdCo res_ty))
; return (pat', cmd', res_coi) }
......@@ -180,8 +180,8 @@ tc_cmd env cmd@(HsLam (MatchGroup [L mtch_loc (match@(Match pats _maybe_rhs_sig
(kappaUnderflow cmd)
-- Check the patterns, and the GRHSs inside
; (pats', grhss') <- setSrcSpan mtch_loc $
tcPats LambdaExpr pats cmd_stk res_ty $
; (pats', grhss') <- setSrcSpan mtch_loc $
tcPats LambdaExpr pats cmd_stk $
tc_grhss grhss res_ty
; let match' = L mtch_loc (Match pats' Nothing grhss')
......@@ -241,10 +241,9 @@ tc_cmd env cmd@(HsArrForm expr fixity cmd_args) (cmd_stk, res_ty)
-- -> a ((w,t1) .. tn) t
; let e_ty = mkFunTys [mkAppTys b [tup,s] | (_,_,b,tup,s) <- cmds_w_tys]
e_res_ty
free_tvs = tyVarsOfTypes (res_ty:cmd_stk)
-- Check expr
; (inst_binds, expr') <- checkConstraints ArrowSkol free_tvs [w_tv] [] $
; (inst_binds, expr') <- checkConstraints ArrowSkol [w_tv] [] $
escapeArrowScope (tcMonoExpr expr e_ty)
-- OK, now we are in a position to unscramble
......
......@@ -130,14 +130,12 @@ tcLocalBinds (HsValBinds binds) thing_inside
tcLocalBinds (HsIPBinds (IPBinds ip_binds _)) thing_inside
= do { (given_ips, ip_binds') <- mapAndUnzipM (wrapLocSndM tc_ip_bind) ip_binds
; let ip_tvs = foldr (unionVarSet . tyVarsOfType . idType) emptyVarSet given_ips
-- If the binding binds ?x = E, we must now
-- discharge any ?x constraints in expr_lie
-- See Note [Implicit parameter untouchables]
; (ev_binds, result) <- checkConstraints (IPSkol ips)
ip_tvs -- See Note [Implicit parameter untouchables]
[] given_ips $
thing_inside
[] given_ips thing_inside
; return (HsIPBinds (IPBinds ip_binds' ev_binds), result) }
where
......@@ -164,6 +162,9 @@ doesn't float that solved constraint out (it's not an unsolved
wanted. Result disaster: the (Num alpha) is again solved, this
time by defaulting. No no no.
However [Oct 10] this is all handled automatically by the
untouchable-range idea.
\begin{code}
tcValBinds :: TopLevelFlag
-> HsValBinds Name -> TcM thing
......@@ -393,7 +394,7 @@ tcPolyCheck sig@(TcSigInfo { sig_id = id, sig_tvs = tvs, sig_scoped = scoped
; let skol_info = SigSkol (FunSigCtxt (idName id))
; (ev_binds, (binds', [mono_info]))
<- checkConstraints skol_info emptyVarSet tvs ev_vars $
<- checkConstraints skol_info tvs ev_vars $
tcExtendTyVarEnv2 (scoped `zip` mkTyVarTys tvs) $
tcMonoBinds (\_ -> Just sig) LetLclBndr rec_tc bind_list
......
......@@ -35,7 +35,6 @@ import MkId
import Id
import Name
import Var
import VarSet
import NameEnv
import NameSet
import Outputable
......@@ -255,7 +254,7 @@ tcInstanceMethodBody skol_info tyvars dfun_ev_vars
-- NB: the binding is always a FunBind
; (ev_binds, (tc_bind, _))
<- checkConstraints skol_info emptyVarSet tyvars full_given $
<- checkConstraints skol_info tyvars full_given $
tcExtendIdEnv [local_meth_id] $
tcPolyBinds TopLevel meth_sig_fn no_prag_fn
NonRecursive NonRecursive
......
......@@ -82,7 +82,7 @@ tcPolyExpr expr res_ty
tcPolyExprNC expr res_ty
= do { traceTc "tcPolyExprNC" (ppr res_ty)
; (gen_fn, expr') <- tcGen (GenSkol res_ty) emptyVarSet res_ty $ \ _ rho ->
; (gen_fn, expr') <- tcGen (GenSkol res_ty) res_ty $ \ _ rho ->
tcMonoExprNC expr rho
; return (mkLHsWrap gen_fn expr') }
......@@ -191,7 +191,7 @@ tcExpr (ExprWithTySig expr sig_ty) res_ty
-- Remember to extend the lexical type-variable environment
; (gen_fn, expr')
<- tcGen (SigSkol ExprSigCtxt) emptyVarSet sig_tc_ty $ \ skol_tvs res_ty ->
<- tcGen (SigSkol ExprSigCtxt) sig_tc_ty $ \ skol_tvs res_ty ->
tcExtendTyVarEnv2 (hsExplicitTvs sig_ty `zip` mkTyVarTys skol_tvs) $
-- See Note [More instantiated than scoped] in TcBinds
tcMonoExprNC expr res_ty
......
......@@ -33,7 +33,6 @@ import TyCon
import DataCon
import Class
import Var
import VarSet ( emptyVarSet )
import CoreUtils ( mkPiTypes )
import CoreUnfold ( mkDFunUnfolding )
import CoreSyn ( Expr(Var) )
......@@ -638,7 +637,7 @@ tc_inst_decl2 dfun_id inst_binds
mapAndUnzipM tc_sc (sc_sels `zip` sc_dicts)
-- NOT FINISHED!
; (_eq_sc_binds, sc_eq_vars) <- checkConstraints InstSkol emptyVarSet
; (_eq_sc_binds, sc_eq_vars) <- checkConstraints InstSkol
inst_tyvars' dfun_ev_vars $
emitWanteds ScOrigin sc_eqs
......@@ -707,7 +706,7 @@ tcSuperClass tyvars dicts
self_ev_bind@(EvBind self_dict _)
(sc_sel, sc_pred)
= do { (ev_binds, wanted, sc_dict)
<- newImplication InstSkol emptyVarSet tyvars dicts $
<- newImplication InstSkol tyvars dicts $
emitWanted ScOrigin sc_pred
; simplifySuperClass self_dict wanted
......@@ -970,7 +969,7 @@ tcInstanceMethods dfun_id clas tyvars dfun_ev_vars inst_tys
-- by the constraint solver, since the <context> may be
-- user-specified.
= do { rep_d_stuff <- checkConstraints InstSkol emptyVarSet tyvars dfun_ev_vars $
= do { rep_d_stuff <- checkConstraints InstSkol tyvars dfun_ev_vars $
emitWanted ScOrigin rep_pred
; mapAndUnzipM (tc_item rep_d_stuff) op_items }
......
......@@ -32,7 +32,6 @@ import TyCon
import TysPrim
import Coercion ( mkSymCoI )
import Outputable
import VarSet
import BasicTypes ( Arity )
import Util
import SrcLoc
......@@ -76,7 +75,7 @@ tcMatchesFun fun_name inf matches exp_ty
; checkArgs fun_name matches
; (wrap_gen, (wrap_fun, group))
<- tcGen (SigSkol (FunSigCtxt fun_name)) emptyVarSet exp_ty $ \ _ exp_rho ->
<- tcGen (SigSkol (FunSigCtxt fun_name)) exp_ty $ \ _ exp_rho ->
-- Note [Polymorphic expected type for tcMatchesFun]
matchFunTys herald arity exp_rho $ \ pat_tys rhs_ty ->
tcMatches match_ctxt pat_tys rhs_ty matches
......@@ -186,7 +185,7 @@ tcMatch ctxt pat_tys rhs_ty match
where
tc_match ctxt pat_tys rhs_ty match@(Match pats maybe_rhs_sig grhss)
= add_match_ctxt match $
do { (pats', grhss') <- tcPats (mc_what ctxt) pats pat_tys rhs_ty $
do { (pats', grhss') <- tcPats (mc_what ctxt) pats pat_tys $
tc_grhss ctxt maybe_rhs_sig grhss rhs_ty
; return (Match pats' Nothing grhss') }
......@@ -345,7 +344,7 @@ tcGuardStmt _ (ExprStmt guard _ _) res_ty thing_inside
tcGuardStmt ctxt (BindStmt pat rhs _ _) res_ty thing_inside
= do { (rhs', rhs_ty) <- tcInferRhoNC rhs -- Stmt has a context already
; (pat', thing) <- tcPat (StmtCtxt ctxt) pat rhs_ty res_ty $
; (pat', thing) <- tcPat (StmtCtxt ctxt) pat rhs_ty $
thing_inside res_ty
; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) }
......@@ -363,7 +362,7 @@ tcLcStmt :: TyCon -- The list/Parray type constructor ([] or PArray)
tcLcStmt m_tc ctxt (BindStmt pat rhs _ _) res_ty thing_inside
= do { pat_ty <- newFlexiTyVarTy liftedTypeKind
; rhs' <- tcMonoExpr rhs (mkTyConApp m_tc [pat_ty])
; (pat', thing) <- tcPat (StmtCtxt ctxt) pat pat_ty res_ty $
; (pat', thing) <- tcPat (StmtCtxt ctxt) pat pat_ty $
thing_inside res_ty
; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) }
......@@ -516,7 +515,7 @@ tcDoStmt ctxt (BindStmt pat rhs bind_op fail_op) res_ty thing_inside
else tcSyntaxOp DoOrigin fail_op (mkFunTy stringTy new_res_ty)
; rhs' <- tcMonoExprNC rhs rhs_ty
; (pat', thing) <- tcPat (StmtCtxt ctxt) pat pat_ty new_res_ty $
; (pat', thing) <- tcPat (StmtCtxt ctxt) pat pat_ty $
thing_inside new_res_ty
; return (BindStmt pat' rhs' bind_op' fail_op', thing) }
......@@ -600,7 +599,7 @@ tcMDoStmt :: (LHsExpr Name -> TcM (LHsExpr TcId, TcType)) -- RHS inference
-> TcStmtChecker
tcMDoStmt tc_rhs ctxt (BindStmt pat rhs _ _) res_ty thing_inside
= do { (rhs', pat_ty) <- tc_rhs rhs
; (pat', thing) <- tcPat (StmtCtxt ctxt) pat pat_ty res_ty $
; (pat', thing) <- tcPat (StmtCtxt ctxt) pat pat_ty $
thing_inside res_ty
; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) }
......
......@@ -32,7 +32,6 @@ import Coercion
import StaticFlags
import TyCon
import DataCon
import VarSet ( emptyVarSet )
import PrelNames
import BasicTypes hiding (SuccessFlag(..))
import DynFlags
......@@ -59,14 +58,13 @@ tcLetPat :: TcSigFun -> LetBndrSpec
tcLetPat sig_fn no_gen pat pat_ty thing_inside
= tc_lpat pat pat_ty penv thing_inside
where
penv = PE { pe_res_tvs = emptyVarSet, pe_lazy = True
penv = PE { pe_lazy = True
, pe_ctxt = LetPat sig_fn no_gen }
-----------------
tcPats :: HsMatchContext Name
-> [LPat Name] -- Patterns,
-> [TcSigmaType] -- and their types
-> TcRhoType -- Result type,
-> TcM a -- and the checker for the body
-> TcM ([LPat TcId], a)
......@@ -81,39 +79,27 @@ tcPats :: HsMatchContext Name
-- 3. Check the body
-- 4. Check that no existentials escape
tcPats ctxt pats pat_tys res_ty thing_inside
tcPats ctxt pats pat_tys thing_inside
= tc_lpats penv pats pat_tys thing_inside
where
penv = PE { pe_res_tvs = tyVarsOfTypes (res_ty : pat_tys)
, pe_lazy = False
, pe_ctxt = LamPat ctxt }
penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt }
tcPat :: HsMatchContext Name
-> LPat Name -> TcSigmaType
-> TcRhoType -- Result type
-> TcM a -- Checker for body, given
-- its result type
-> TcM (LPat TcId, a)
tcPat ctxt pat pat_ty res_ty thing_inside
tcPat ctxt pat pat_ty thing_inside
= tc_lpat pat pat_ty penv thing_inside
where
penv = PE { pe_res_tvs = tyVarsOfTypes [res_ty, pat_ty]
, pe_lazy = False
, pe_ctxt = LamPat ctxt }
penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt }
-----------------
data PatEnv
= PE { pe_res_tvs :: TcTyVarSet
-- For existential escape check; see Note [Existential check]
-- Nothing <=> inside a "~"
-- Just tvs <=> unification tvs free in the result
-- (which should be made untouchable in
-- any existentials we encounter in the pattern)
, pe_lazy :: Bool -- True <=> lazy context, so no existentials allowed
= PE { pe_lazy :: Bool -- True <=> lazy context, so no existentials allowed
, pe_ctxt :: PatCtxt -- Context in which the whole pattern appears
}
}
data PatCtxt
= LamPat -- Used for lambdas, case etc
......@@ -188,7 +174,7 @@ Note [Existential check]
Lazy patterns can't bind existentials. They arise in two ways:
* Let bindings let { C a b = e } in b
* Twiddle patterns f ~(C a b) = e
The pe_res_tvs field of PatEnv says whether we are inside a lazy
The pe_lazy field of PatEnv says whether we are inside a lazy
pattern (perhaps deeply)
If we aren't inside a lazy pattern then we can bind existentials,
......@@ -736,17 +722,8 @@ tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside
-- should require the GADT language flag
; given <- newEvVars theta'
; let free_tvs = pe_res_tvs penv
-- Since we have done checkExistentials,
-- pe_res_tvs can only be Just at this point
--
-- Nor do we need pat_ty, because we've put all the
-- unification variables in right at the start when
-- initialising the PatEnv; and the pattern itself
-- only adds skolems.
; (ev_binds, (arg_pats', res))
<- checkConstraints skol_info free_tvs ex_tvs' given $
<- checkConstraints skol_info ex_tvs' given $
tcConArgs data_con arg_tys' arg_pats penv thing_inside
; let res_pat = ConPatOut { pat_con = L con_span data_con,
......
......@@ -28,7 +28,7 @@ module TcRnTypes(
ArrowCtxt(NoArrowCtxt), newArrowScope, escapeArrowScope,
-- Constraints
Untouchables(..), inTouchableRange,
Untouchables(..), inTouchableRange, isNoUntouchables,
WantedConstraints, emptyWanteds, andWanteds, extendWanteds,
WantedConstraint(..), WantedEvVar(..), wantedEvVarLoc,
wantedEvVarToVar, wantedEvVarPred, splitWanteds,
......@@ -698,6 +698,10 @@ instance Outputable Untouchables where
ppr (TouchableRange low high) = ptext (sLit "Touchable range:") <+>
ppr low <+> char '-' <+> ppr high
isNoUntouchables :: Untouchables -> Bool
isNoUntouchables NoUntouchables = True
isNoUntouchables (TouchableRange {}) = False
inTouchableRange :: Untouchables -> TcTyVar -> Bool
inTouchableRange NoUntouchables _ = True
inTouchableRange (TouchableRange low high) tv
......
......@@ -395,7 +395,7 @@ tc_bracket _ (DecBrG decls)
tc_bracket _ (PatBr pat)
= do { any_ty <- newFlexiTyVarTy liftedTypeKind
; _ <- tcPat ThPatQuote pat any_ty unitTy $
; _ <- tcPat ThPatQuote pat any_ty $
return ()
; tcMetaTy patQTyConName }
-- Result type is PatQ (= Q Pat)
......
......@@ -304,9 +304,8 @@ tcSubType :: CtOrigin -> SkolemInfo -> TcSigmaType -> TcSigmaType -> TcM HsWrapp
-- Returns a wrapper of shape ty_actual ~ ty_expected
tcSubType origin skol_info ty_actual ty_expected
| isSigmaTy ty_actual
= do { let extra_tvs = tyVarsOfType ty_actual
; (sk_wrap, inst_wrap)
<- tcGen skol_info extra_tvs ty_expected $ \ _ sk_rho -> do
= do { (sk_wrap, inst_wrap)
<- tcGen skol_info ty_expected $ \ _ sk_rho -> do
{ (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual
; coi <- unifyType in_rho sk_rho
; return (coiToHsWrapper coi <.> in_wrap) }
......@@ -354,14 +353,14 @@ wrapFunResCoercion arg_tys co_fn_res
%************************************************************************
\begin{code}
tcGen :: SkolemInfo -> TcTyVarSet -> TcType
tcGen :: SkolemInfo -> TcType
-> ([TcTyVar] -> TcRhoType -> TcM result)
-> TcM (HsWrapper, result)
-- The expression has type: spec_ty -> expected_ty
tcGen skol_info extra_tvs
expected_ty thing_inside -- We expect expected_ty to be a forall-type
-- If not, the call is a no-op
tcGen skol_info expected_ty thing_inside
-- We expect expected_ty to be a forall-type
-- If not, the call is a no-op
= do { traceTc "tcGen" empty
; (wrap, tvs', given, rho') <- deeplySkolemise skol_info expected_ty
......@@ -370,7 +369,7 @@ tcGen skol_info extra_tvs
text "expected_ty" <+> ppr expected_ty,
text "inst ty" <+> ppr tvs' <+> ppr rho' ]
-- In 'free_tvs' we must check that the "forall_tvs" havn't been constrained
-- Generally we must check that the "forall_tvs" havn't been constrained
-- The interesting bit here is that we must include the free variables
-- of the expected_ty. Here's an example:
-- runST (newVar True)
......@@ -378,10 +377,12 @@ tcGen skol_info extra_tvs
-- for (newVar True), with s fresh. Then we unify with the runST's arg type
-- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool.
-- So now s' isn't unconstrained because it's linked to a.
-- Conclusion: pass the free vars of the expected_ty to checkConsraints
; let free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
--
-- However [Oct 10] now that the untouchables are a range of
-- TcTyVars, all tihs is handled automatically with no need for
-- extra faffing around
; (ev_binds, result) <- checkConstraints skol_info free_tvs tvs' given $
; (ev_binds, result) <- checkConstraints skol_info tvs' given $
thing_inside tvs' rho'
; return (wrap <.> mkWpLet ev_binds, result) }
......@@ -389,36 +390,30 @@ tcGen skol_info extra_tvs
-- often empty, in which case mkWpLet is a no-op
checkConstraints :: SkolemInfo
-> TcTyVarSet -- Free variables (other than the type envt)
-- for the skolem escape check
-> [TcTyVar] -- Skolems
-> [EvVar] -- Given
-> TcM result
-> TcM (TcEvBinds, result)
checkConstraints skol_info free_tvs skol_tvs given thing_inside
checkConstraints skol_info skol_tvs given thing_inside
| null skol_tvs && null given
= do { res <- thing_inside; return (emptyTcEvBinds, res) }
-- Just for efficiency. We check every function argument with
-- tcPolyExpr, which uses tcGen and hence checkConstraints.
| otherwise
= do { (ev_binds, wanted, result) <- newImplication skol_info free_tvs
= do { (ev_binds, wanted, result) <- newImplication skol_info
skol_tvs given thing_inside
; emitConstraints wanted
; return (ev_binds, result) }
newImplication :: SkolemInfo -> TcTyVarSet -> [TcTyVar]
newImplication :: SkolemInfo -> [TcTyVar]
-> [EvVar] -> TcM result
-> TcM (TcEvBinds, WantedConstraints, result)
newImplication skol_info _free_tvs skol_tvs given thing_inside
newImplication skol_info skol_tvs given thing_inside
= ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs )
ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs )
do { -- gbl_tvs <- tcGetGlobalTyVars
-- ; free_tvs <- zonkTcTyVarsAndFV free_tvs
-- ; let untch = gbl_tvs `unionVarSet` free_tvs
; ((result, untch), wanted) <- captureConstraints $
do { ((result, untch), wanted) <- captureConstraints $
captureUntouchables $
thing_inside
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment