Commit a2fcf3aa authored by simonpj@microsoft.com's avatar simonpj@microsoft.com
Browse files

Add left-to-right impredicative instantiation

People keep complaining, with some justification, that

	runST $ foo

doesn't work.  So I've finally caved in.  The difficulty with the above
is that we need to decide how to instantiate ($)'s type arguments based 
on the first argument (runST), and then use that info to check the second
argumnent.  There is a left-to-right flow of information.

It's not hard to implement this, and it's clearly useful.  The main 
change is in TcExpr.tcArgs, with some knock-on effects elsewhere.

I was finally provoked into this by Trac #981, which turned out, after some
head-scratching, to be another instance of the same problem.

(There was some bug-fixing too; a type like ((?x::Int) => ...) is a polytype
even though it has no leading for-alls, but the new TcUnify code was not 
treating it right.)

Test for this is tc222
parent e119cde9
......@@ -228,10 +228,12 @@ tcExpr in_expr@(SectionR lop@(L loc op) arg2) res_ty
where
doc = ptext SLIT("The section") <+> quotes (ppr in_expr)
<+> ptext SLIT("takes one argument")
tc_args arg1_ty' [arg1_ty, arg2_ty]
= do { boxyUnify arg1_ty' arg1_ty
; tcArg lop (arg2, arg2_ty, 2) }
tc_args arg1_ty' other = panic "tcExpr SectionR"
tc_args arg1_ty' qtvs qtys [arg1_ty, arg2_ty]
= do { boxyUnify arg1_ty' (substTyWith qtvs qtys arg1_ty)
; arg2' <- tcArg lop 2 arg2 qtvs qtys arg2_ty
; qtys' <- mapM refineBox qtys -- c.f. tcArgs
; return (qtys', arg2') }
tc_args arg1_ty' _ _ _ = panic "tcExpr SectionR"
\end{code}
\begin{code}
......@@ -321,12 +323,15 @@ tcExpr expr@(RecordCon (L loc con_name) _ rbinds) res_ty
; checkMissingFields data_con rbinds
; let arity = dataConSourceArity data_con
check_fields arg_tys
= do { rbinds' <- tcRecordBinds data_con arg_tys rbinds
; mapM unBox arg_tys
; return rbinds' }
-- The unBox ensures that all the boxes in arg_tys are indeed
check_fields qtvs qtys arg_tys
= do { let arg_tys' = substTys (zipOpenTvSubst qtvs qtys) arg_tys
; rbinds' <- tcRecordBinds data_con arg_tys' rbinds
; qtys' <- mapM refineBoxToTau qtys
; return (qtys', rbinds') }
-- The refineBoxToTau ensures that all the boxes in arg_tys are indeed
-- filled, which is the invariant expected by tcIdApp
-- How could this not be the case? Consider a record construction
-- that does not mention all the fields.
; (con_expr, rbinds') <- tcIdApp con_name arity check_fields res_ty
......@@ -571,9 +576,9 @@ tcExpr other _ = pprPanic "tcMonoExpr" (ppr other)
---------------------------
tcApp :: HsExpr Name -- Function
-> Arity -- Number of args reqd
-> ([BoxySigmaType] -> TcM arg_results) -- Argument type-checker
-> ArgChecker results
-> BoxyRhoType -- Result type
-> TcM (HsExpr TcId, arg_results)
-> TcM (HsExpr TcId, results)
-- (tcFun fun n_args arg_checker res_ty)
-- The argument type checker, arg_checker, will be passed exactly n_args types
......@@ -582,19 +587,18 @@ tcApp (HsVar fun_name) n_args arg_checker res_ty
= tcIdApp fun_name n_args arg_checker res_ty
tcApp fun n_args arg_checker res_ty -- The vanilla case (rula APP)
= do { arg_boxes <- newBoxyTyVars (replicate n_args argTypeKind)
; fun' <- tcExpr fun (mkFunTys (mkTyVarTys arg_boxes) res_ty)
; arg_tys' <- mapM readFilledBox arg_boxes
; args' <- arg_checker arg_tys'
= do { arg_boxes <- newBoxyTyVars (replicate n_args argTypeKind)
; fun' <- tcExpr fun (mkFunTys (mkTyVarTys arg_boxes) res_ty)
; arg_tys' <- mapM readFilledBox arg_boxes
; (_, args') <- arg_checker [] [] arg_tys' -- Yuk
; return (fun', args') }
---------------------------
tcIdApp :: Name -- Function
-> Arity -- Number of args reqd
-> ([BoxySigmaType] -> TcM arg_results) -- Argument type-checker
-- The arg-checker guarantees to fill all boxes in the arg types
-> ArgChecker results -- The arg-checker guarantees to fill all boxes in the arg types
-> BoxyRhoType -- Result type
-> TcM (HsExpr TcId, arg_results)
-> TcM (HsExpr TcId, results)
-- Call (f e1 ... en) :: res_ty
-- Type f :: forall a b c. theta => fa_1 -> ... -> fa_k -> fres
......@@ -627,23 +631,16 @@ tcIdApp fun_name n_args arg_checker res_ty
; let extra_arg_tys' = mkTyVarTys extra_arg_boxes
res_ty' = mkFunTys extra_arg_tys' res_ty
; qtys' <- preSubType qtvs tau_qtvs fun_res_ty res_ty'
; let arg_subst = zipOpenTvSubst qtvs qtys'
fun_arg_tys' = substTys arg_subst fun_arg_tys
-- Typecheck the arguments!
-- Doing so will fill arg_qtvs and extra_arg_tys'
; args' <- arg_checker (fun_arg_tys' ++ extra_arg_tys')
; (qtys'', args') <- arg_checker qtvs qtys' (fun_arg_tys ++ extra_arg_tys')
-- Strip boxes from the qtvs that have been filled in by the arg checking
-- AND any variables that are mentioned in neither arg nor result
-- the latter are mentioned only in constraints; stripBoxyType will
-- fill them with a monotype
; let strip qtv qty' | qtv `elemVarSet` arg_qtvs = stripBoxyType qty'
| otherwise = return qty'
; qtys'' <- zipWithM strip qtvs qtys'
; extra_arg_tys'' <- mapM readFilledBox extra_arg_boxes
-- Result subsumption
-- This fills in res_qtvs
; let res_subst = zipOpenTvSubst qtvs qtys''
fun_res_ty'' = substTy res_subst fun_res_ty
res_ty'' = mkFunTys extra_arg_tys'' res_ty
......@@ -653,7 +650,7 @@ tcIdApp fun_name n_args arg_checker res_ty
-- By applying the coercion just to the *function* we can make
-- tcFun work nicely for OpApp and Sections too
; fun' <- instFun orig fun res_subst tv_theta_prs
; co_fn' <- wrapFunResCoercion fun_arg_tys' co_fn
; co_fn' <- wrapFunResCoercion (substTys res_subst fun_arg_tys) co_fn
; return (mkHsWrap co_fn' fun', args') }
\end{code}
......@@ -818,19 +815,45 @@ This gets a bit less sharing, but
a) it's better for RULEs involving overloaded functions
b) perhaps fewer separated lambdas
Note [Left to right]
~~~~~~~~~~~~~~~~~~~~
tcArgs implements a left-to-right order, which goes beyond what is described in the
impredicative type inference paper. In particular, it allows
runST $ foo
where runST :: (forall s. ST s a) -> a
When typechecking the application of ($)::(a->b) -> a -> b, we first check that
runST has type (a->b), thereby filling in a=forall s. ST s a. Then we un-box this type
before checking foo. The left-to-right order really helps here.
\begin{code}
tcArgs :: LHsExpr Name -- The function (for error messages)
-> [LHsExpr Name] -> [TcSigmaType] -- Actual arguments and expected arg types
-> TcM [LHsExpr TcId] -- Resulting args
-> [LHsExpr Name] -- Actual args
-> ArgChecker [LHsExpr TcId]
tcArgs fun args expected_arg_tys
= mapM (tcArg fun) (zip3 args expected_arg_tys [1..])
type ArgChecker results
= [TyVar] -> [TcSigmaType] -- Current instantiation
-> [TcSigmaType] -- Expected arg types (**before** applying the instantiation)
-> TcM ([TcSigmaType], results) -- Resulting instaniation and args
tcArg :: LHsExpr Name -- The function (for error messages)
-> (LHsExpr Name, BoxySigmaType, Int) -- Actual argument and expected arg type
-> TcM (LHsExpr TcId) -- Resulting argument
tcArg fun (arg, ty, arg_no) = addErrCtxt (funAppCtxt fun arg arg_no) $
tcPolyExprNC arg ty
tcArgs fun args qtvs qtys arg_tys
= go 1 qtys args arg_tys
where
go n qtys [] [] = return (qtys, [])
go n qtys (arg:args) (arg_ty:arg_tys)
= do { arg' <- tcArg fun n arg qtvs qtys arg_ty
; qtys' <- mapM refineBox qtys -- Exploit new info
; (qtys'', args') <- go (n+1) qtys' args arg_tys
; return (qtys'', arg':args') }
tcArg :: LHsExpr Name -- The function
-> Int -- and arg number (for error messages)
-> LHsExpr Name
-> [TyVar] -> [TcSigmaType] -- Instantiate the arg type like this
-> BoxySigmaType
-> TcM (LHsExpr TcId) -- Resulting argument
tcArg fun arg_no arg qtvs qtys ty
= addErrCtxt (funAppCtxt fun arg arg_no) $
tcPolyExprNC arg (substTyWith qtvs qtys ty)
\end{code}
......
......@@ -62,7 +62,6 @@ module TcMType (
import TypeRep
import TcType
import Type
import Type
import Coercion
import Class
import TyCon
......@@ -360,7 +359,7 @@ data LookupTyVarResult -- The result of a lookupTcTyVar call
lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
lookupTcTyVar tyvar
= ASSERT( isTcTyVar tyvar )
= ASSERT2( isTcTyVar tyvar, ppr tyvar )
case details of
SkolemTv _ -> return (DoneTv details)
MetaTv _ ref -> do { meta_details <- readMutVar ref
......
......@@ -19,7 +19,7 @@ module TcUnify (
--------------------------------
-- Holes
tcInfer, subFunTys, unBox, stripBoxyType, withBox,
tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox,
boxyUnify, boxyUnifyList, zapToMonotype,
boxySplitListTy, boxySplitTyConApp, boxySplitAppTy,
wrapFunResCoercion
......@@ -607,7 +607,8 @@ tc_sub :: SubCtxt -- How to add an error-context
-- e.g. in the SPEC rule where we just use splitSigmaTy
tc_sub sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
= tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
= traceTc (text "tc_sub" <+> ppr act_ty $$ ppr exp_ty) >>
tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
-- This indirection is just here to make
-- it easy to insert a debug trace!
......@@ -637,9 +638,11 @@ tc_sub1 sub_ctxt act_sty (TyVarTy tv) exp_ib exp_sty exp_ty
-- Consider f g !
tc_sub1 sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
| not exp_ib, -- SKOL does not apply if exp_ty is inside a box
isSigmaTy exp_ty
= do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty ->
| isSigmaTy exp_ty
= if exp_ib then -- SKOL does not apply if exp_ty is inside a box
defer_to_boxy_matching sub_ctxt act_sty act_ty exp_ib exp_sty exp_ty
else do
{ (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty ->
tc_sub sub_ctxt act_sty act_ty False body_exp_ty body_exp_ty
; return (gen_fn <.> co_fn) }
where
......@@ -713,11 +716,14 @@ tc_sub1 sub_ctxt act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_t
-- Everything else: defer to boxy matching
tc_sub1 sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
= defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
-----------------------------------
defer_to_boxy_matching sub_ctxt act_sty actual_ty exp_ib exp_sty expected_ty
= do { addSubCtxt sub_ctxt act_sty exp_sty $
u_tys True False act_sty actual_ty exp_ib exp_sty expected_ty
; return idHsWrapper }
-----------------------------------
tc_sub_funs act_arg act_res exp_ib exp_arg exp_res
= do { uTys False act_arg exp_ib exp_arg
......@@ -942,8 +948,45 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
go outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2
go outer ty1 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 orig_ty1 ty1
-- "True" means args swapped
-- The case for sigma-types must *follow* the variable cases
-- because a boxy variable can be filed with a polytype;
-- but must precede FunTy, because ((?x::Int) => ty) look
-- like a FunTy; there isn't necy a forall at the top
go _ ty1 ty2
| isSigmaTy ty1 || isSigmaTy ty2
= do { checkM (equalLength tvs1 tvs2)
(unifyMisMatch outer False orig_ty1 orig_ty2)
; tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
-- Get location from monad, not from tvs1
; let tys = mkTyVarTys tvs
in_scope = mkInScopeSet (mkVarSet tvs)
subst1 = mkTvSubst in_scope (zipTyEnv tvs1 tys)
subst2 = mkTvSubst in_scope (zipTyEnv tvs2 tys)
(theta1,tau1) = tcSplitPhiTy (substTy subst1 body1)
(theta2,tau2) = tcSplitPhiTy (substTy subst2 body2)
; checkM (equalLength theta1 theta2)
(unifyMisMatch outer False orig_ty1 orig_ty2)
; uPreds False nb1 theta1 nb2 theta2
; uTys nb1 tau1 nb2 tau2
-- If both sides are inside a box, we are in a "box-meets-box"
-- situation, and we should not have a polytype at all.
-- If we get here we have two boxes, already filled with
-- the same polytype... but it should be a monotype.
-- This check comes last, because the error message is
-- extremely unhelpful.
; ifM (nb1 && nb2) (notMonoType ty1)
}
where
(tvs1, body1) = tcSplitForAllTys ty1
(tvs2, body2) = tcSplitForAllTys ty2
-- Predicates
go outer (PredTy p1) (PredTy p2) = uPred outer nb1 p1 nb2 p2
go outer (PredTy p1) (PredTy p2) = uPred False nb1 p1 nb2 p2
-- Type constructors must match
go _ (TyConApp con1 tys1) (TyConApp con2 tys2)
......@@ -969,27 +1012,6 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2
| Just (s1,t1) <- tcSplitAppTy_maybe ty1
= do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 }
go _ ty1@(ForAllTy _ _) ty2@(ForAllTy _ _)
| length tvs1 == length tvs2
= do { tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo
-- Get location from monad, not from tvs1
; let tys = mkTyVarTys tvs
in_scope = mkInScopeSet (mkVarSet tvs)
subst1 = mkTvSubst in_scope (zipTyEnv tvs1 tys)
subst2 = mkTvSubst in_scope (zipTyEnv tvs2 tys)
; uTys nb1 (substTy subst1 body1) nb2 (substTy subst2 body2)
-- If both sides are inside a box, we are in a "box-meets-box"
-- situation, and we should not have a polytype at all.
-- If we get here we have two boxes, already filled with
-- the same polytype... but it should be a monotype.
-- This check comes last, because the error message is
-- extremely unhelpful.
; ifM (nb1 && nb2) (notMonoType ty1)
}
where
(tvs1, body1) = tcSplitForAllTys ty1
(tvs2, body2) = tcSplitForAllTys ty2
-- Anything else fails
go outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2
......@@ -1000,6 +1022,10 @@ uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2)
uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2)
| c1 == c2 = uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check
uPred outer _ p1 _ p2 = unifyMisMatch outer False (mkPredTy p1) (mkPredTy p2)
uPreds outer nb1 [] nb2 [] = return ()
uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) = uPred outer nb1 p1 nb2 p2 >> uPreds outer nb1 ps1 nb2 ps2
uPreds outer nb1 ps1 nb2 ps2 = panic "uPreds"
\end{code}
Note [Tycon app]
......@@ -1380,16 +1406,27 @@ But we should not reject the program, because A t = ().
Rather, we should bind t to () (= non_var_ty2).
\begin{code}
stripBoxyType :: BoxyType -> TcM TcType
-- Strip all boxes from the input type, returning a non-boxy type.
-- It's fine for there to be a polytype inside a box (c.f. unBox)
-- All of the boxes should have been filled in by now;
-- hence we return a TcType
stripBoxyType ty = zonkType strip_tv ty
where
strip_tv tv = ASSERT( not (isBoxyTyVar tv) ) return (TyVarTy tv)
-- strip_tv will be called for *Flexi* meta-tyvars
-- There should not be any Boxy ones; hence the ASSERT
refineBox :: TcType -> TcM TcType
-- Unbox the outer box of a boxy type (if any)
refineBox ty@(TyVarTy box_tv)
| isMetaTyVar box_tv
= do { cts <- readMetaTyVar box_tv
; case cts of
Flexi -> return ty
Indirect ty -> return ty }
refineBox other_ty = return other_ty
refineBoxToTau :: TcType -> TcM TcType
-- Unbox the outer box of a boxy type, filling with a monotype if it is empty
-- Like refineBox except for the "fill with monotype" part.
refineBoxToTau ty@(TyVarTy box_tv)
| isMetaTyVar box_tv
, MetaTv BoxTv ref <- tcTyVarDetails box_tv
= do { cts <- readMutVar ref
; case cts of
Flexi -> fillBoxWithTau box_tv ref
Indirect ty -> return ty }
refineBoxToTau other_ty = return other_ty
zapToMonotype :: BoxySigmaType -> TcM TcTauType
-- Subtle... we must zap the boxy res_ty
......
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