X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=11c0f3fdd89f49ac0020af32baf2ef04f5570299;hb=f16dbbbe59cf3aa19c5fd384560a1b89076d7bc8;hp=1aa0bf62bb614ebba605b303b7088becc7f8d2cc;hpb=cd6658d04b5451d9b7c5c3b758bff8a0b5a63e7a;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 1aa0bf6..11c0f3f 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -79,7 +79,9 @@ tcInfer tc_infer = withBox openTypeKind tc_infer subFunTys :: SDoc -- Something like "The function f has 3 arguments" -- or "The abstraction (\x.e) takes 1 argument" -> Arity -- Expected # of args - -> BoxyRhoType -- res_ty + -> BoxySigmaType -- res_ty + -> Maybe UserTypeCtxt -- Whether res_ty arises from a user signature + -- Only relevant if we encounter a sigma-type -> ([BoxySigmaType] -> BoxyRhoType -> TcM a) -> TcM (HsWrapper, a) -- Attempt to decompse res_ty to have enough top-level arrows to @@ -108,7 +110,7 @@ subFunTys :: SDoc -- Something like "The function f has 3 arguments" -} -subFunTys error_herald n_pats res_ty thing_inside +subFunTys error_herald n_pats res_ty mb_ctxt thing_inside = loop n_pats [] res_ty where -- In 'loop', the parameter 'arg_tys' accumulates @@ -121,8 +123,8 @@ subFunTys error_herald n_pats res_ty thing_inside | isSigmaTy res_ty -- Do this before checking n==0, because we -- guarantee to return a BoxyRhoType, not a -- BoxySigmaType - = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' -> - loop n args_so_far res_ty' + = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet mb_ctxt $ + loop n args_so_far ; return (gen_fn <.> co_fn, res) } loop 0 args_so_far res_ty @@ -768,7 +770,7 @@ tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty if exp_ib then -- SKOL does not apply if exp_ty is inside a box defer_to_boxy_matching orig act_sty act_ty exp_ib exp_sty exp_ty else do - { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty -> + { (gen_fn, co_fn) <- tcGen exp_ty act_tvs Nothing $ \ body_exp_ty -> tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty ; return (gen_fn <.> co_fn) } } @@ -898,22 +900,17 @@ tcGen :: BoxySigmaType -- expected_ty -> TcTyVarSet -- Extra tyvars that the universally -- quantified tyvars of expected_ty -- must not be unified - -> ([TcTyVar] -> BoxyRhoType -> TcM result) + -> Maybe UserTypeCtxt -- Just ctxt => this polytype arose directly from + -- a user type sig; bring tyvars into scope + -- Nothing => a higher order situation + -> (BoxyRhoType -> TcM result) -> TcM (HsWrapper, result) -- The expression has type: spec_ty -> expected_ty -tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type - -- If not, the call is a no-op +tcGen expected_ty extra_tvs mb_ctxt thing_inside -- We expect expected_ty to be a forall-type + -- If not, the call is a no-op = do { traceTc (text "tcGen") - -- We want the GenSkol info in the skolemised type variables to - -- mention the *instantiated* tyvar names, so that we get a - -- good error message "Rigid variable 'a' is bound by (forall a. a->a)" - -- Hence the tiresome but innocuous fixM - ; ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) -> - do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty - -- Get loation from monad, not from expected_ty - ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) - ; return ((forall_tvs, theta, rho_ty), skol_info) }) + ; ((tvs', theta', rho'), skol_info, scoped_tvs) <- instantiate expected_ty ; when debugIsOn $ traceTc (text "tcGen" <+> vcat [ @@ -924,7 +921,11 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a text "free_tvs" <+> ppr free_tvs]) -- Type-check the arg and unify with poly type - ; (result, lie) <- getLIE (thing_inside tvs' rho') + ; (result, lie) <- getLIE $ + tcExtendTyVarEnv2 (scoped_tvs `zip` mkTyVarTys tvs') $ + -- Extend the lexical type-variable environment + -- if we're in a user-type context + thing_inside rho' -- Check that the "forall_tvs" havn't been constrained -- The interesting bit here is that we must include the free variables @@ -951,6 +952,24 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a ; return (co_fn, result) } where free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs + + instantiate :: TcType -> TcM (([TcTyVar],ThetaType,TcRhoType), SkolemInfo, [Name]) + instantiate expected_ty + | Just ctxt <- mb_ctxt + = do { let skol_info = SigSkol ctxt + tv_names = map tyVarName (fst (tcSplitForAllTys expected_ty)) + ; stuff <- tcInstSigType True skol_info expected_ty + ; return (stuff, skol_info, tv_names) } + + | otherwise -- We want the GenSkol info in the skolemised type variables to + -- mention the *instantiated* tyvar names, so that we get a + -- good error message "Rigid variable 'a' is bound by (forall a. a->a)" + -- Hence the tiresome but innocuous fixM + = fixM $ \ ~(_, skol_info, _) -> + do { stuff@(forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty + -- Get loation from *monad*, not from expected_ty + ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) + ; return (stuff, skol_info, []) } \end{code} @@ -1507,7 +1526,7 @@ uMetaVar :: Outer -- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau) -- ty2 is not a type variable -uMetaVar _ swapped tv1 BoxTv ref1 ps_ty2 _ +uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 ty2 = -- tv1 is a BoxTv. So we must unbox ty2, to ensure -- that any boxes in ty2 are filled with monotypes -- @@ -1516,15 +1535,21 @@ uMetaVar _ swapped tv1 BoxTv ref1 ps_ty2 _ -- it does, the unbox operation will fill it, and the debug code -- checks for that. do { final_ty <- unBox ps_ty2 - ; when debugIsOn $ do - { meta_details <- readMutVar ref1 - ; case meta_details of - Indirect ty -> WARN( True, ppr tv1 <+> ppr ty ) - return () -- This really should *not* happen - Flexi -> return () - } - ; checkUpdateMeta swapped tv1 ref1 final_ty - ; return IdCo + ; meta_details <- readMutVar ref1 + ; case meta_details of + Indirect _ -> -- This *can* happen due to an occurs check, + -- just as it can in checkTauTvUpdate in the next + -- equation of uMetaVar; see Trac #2414 + -- Note [Occurs check] + -- Go round again. Probably there's an immediate + -- error, but maybe not (a type function might discard + -- its argument). Next time round we'll end up in the + -- TauTv case of uMetaVar. + uVar outer swapped tv1 False ps_ty2 ty2 + -- Setting for nb2::InBox is irrelevant + + Flexi -> do { checkUpdateMeta swapped tv1 ref1 final_ty + ; return IdCo } } uMetaVar outer swapped tv1 _ ref1 ps_ty2 _ @@ -1539,6 +1564,18 @@ uMetaVar outer swapped tv1 _ ref1 ps_ty2 _ } } +{- Note [Occurs check] + ~~~~~~~~~~~~~~~~~~~ +An eager occurs check is made in checkTauTvUpdate, deferring tricky +cases by calling defer_unification (see notes with +checkTauTvUpdate). An occurs check can also (and does) happen in the +BoxTv case, but unBox doesn't check for occurrences, and in any case +doesn't have the type-function-related complexity that +checkTauTvUpdate has. So we content ourselves with spotting the potential +occur check (by the fact that tv1 is now filled), and going round again. +Next time round we'll get the TauTv case of uMetaVar. +-} + ---------------- uUnfilledVars :: Outer -> SwapFlag @@ -1912,7 +1949,7 @@ checkExpectedKind ty act_kind exp_kind | otherwise = do (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind) case mb_r of - Just _ -> return () ; -- Unification succeeded + Just _ -> return () -- Unification succeeded Nothing -> do -- So there's definitely an error