X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=e5e16fc392fbe49fe5ccc9e0fed9e149d79a4e22;hp=84d79f679db5ff92dc5575e42826d1173b111822;hb=9a4ef343a46e823bcf949af8501c13cc8ca98fb1;hpb=b19ba85c6ec3504a66b33243cfb43599d8c298a7 diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 84d79f6..e5e16fc 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -6,13 +6,6 @@ Type subsumption and unification \begin{code} -{-# OPTIONS -w #-} --- The above warning supression flag is a temporary kludge. --- While working on this module you are encouraged to remove it and fix --- any warnings in the module. See --- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings --- for details - module TcUnify ( -- Full-blown subsumption tcSubExp, tcGen, @@ -21,7 +14,6 @@ module TcUnify ( -- Various unifications unifyType, unifyTypeList, unifyTheta, unifyKind, unifyKinds, unifyFunKind, - checkExpectedKind, preSubType, boxyMatchTypes, -------------------------------- @@ -59,7 +51,6 @@ import Maybes import BasicTypes import Util import Outputable -import Unique import FastString import Control.Monad @@ -84,10 +75,12 @@ tcInfer tc_infer = withBox openTypeKind tc_infer %************************************************************************ \begin{code} -subFunTys :: SDoc -- Somthing like "The function f has 3 arguments" +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 @@ -116,7 +109,7 @@ subFunTys :: SDoc -- Somthing 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 @@ -129,8 +122,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 $ \ _ res_ty -> + loop n args_so_far res_ty ; return (gen_fn <.> co_fn, res) } loop 0 args_so_far res_ty @@ -143,7 +136,7 @@ subFunTys error_herald n_pats res_ty thing_inside ; return (co_fn', res) } -- Try to normalise synonym families and defer if that's not possible - loop n args_so_far ty@(TyConApp tc tys) + loop n args_so_far ty@(TyConApp tc _) | isOpenSynTyCon tc = do { (coi1, ty') <- tcNormaliseFamInst ty ; case coi1 of @@ -190,7 +183,7 @@ subFunTys error_herald n_pats res_ty thing_inside -- Note argTypeKind: the args can have an unboxed type, -- but not an unboxed tuple. - loop n args_so_far res_ty = bale_out args_so_far + loop _ args_so_far _ = bale_out args_so_far -- Build a template type a1 -> ... -> an -> b and defer an equality -- between that template and the expected result type res_ty; then, @@ -322,7 +315,7 @@ boxySplitAppTy orig_ty = do { (coi1, ty') <- tcNormaliseFamInst ty ; case coi1 of IdCo -> defer -- no progress, but maybe solvable => defer - ACo co -> -- progress: so lets try again + ACo _ -> -- progress: so lets try again do { (args, coi2) <- loop ty' ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1) } @@ -364,6 +357,7 @@ boxySplitAppTy orig_ty mk_res_ty _other = panic "TcUnify.mk_res_ty2" ------------------ +boxySplitFailure :: TcType -> TcType -> TcM (a, CoercionI) boxySplitFailure actual_ty expected_ty = failWithMisMatch actual_ty expected_ty ------------------ @@ -479,7 +473,7 @@ boxySubMatchType tmpl_tvs tmpl_ty boxy_ty | Just t_ty' <- tcView t_ty = go t_tvs t_ty' b_tvs b_ty | Just b_ty' <- tcView b_ty = go t_tvs t_ty b_tvs b_ty' - go t_tvs (TyVarTy _) b_tvs b_ty = emptyTvSubst -- Rule S-ANY; no bindings + go _ (TyVarTy _) _ _ = emptyTvSubst -- Rule S-ANY; no bindings -- Rule S-ANY covers (a) type variables and (b) boxy types -- in the template. Both look like a TyVarTy. -- See Note [Sub-match] below @@ -552,12 +546,14 @@ boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys boxy_match_s tmpl_tvs tmpl_tys emptyVarSet boxy_tys emptyTvSubst -- ToDo: add error context? -boxy_match_s tmpl_tvs [] boxy_tvs [] subst +boxy_match_s :: TcTyVarSet -> [TcType] -> TcTyVarSet -> [BoxySigmaType] + -> TvSubst -> TvSubst +boxy_match_s _ [] _ [] subst = subst boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst = boxy_match tmpl_tvs t_ty boxy_tvs b_ty $ boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys subst -boxy_match_s tmpl_tvs _ boxy_tvs _ subst +boxy_match_s _ _ _ _ _ = panic "boxy_match_s" -- Lengths do not match @@ -614,7 +610,10 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst Nothing -> orig_boxy_ty Just ty -> ty `boxyLub` orig_boxy_ty - go _ (TyVarTy tv) | isMetaTyVar tv + go _ (TyVarTy tv) | isTcTyVar tv && isMetaTyVar tv + -- NB: A TyVar (not TcTyVar) is possible here, representing + -- a skolem, because in this pure boxy_match function + -- we don't instantiate foralls to TcTyVars; cf Trac #2714 = subst -- Don't fail if the template has more info than the target! -- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta) -- would fail to instantiate 'a', because the meta-type-variable @@ -644,11 +643,11 @@ boxyLub orig_ty1 orig_ty2 | tc1 == tc2, length ts1 == length ts2 = TyConApp tc1 (zipWith boxyLub ts1 ts2) - go (TyVarTy tv1) ty2 -- This is the whole point; + go (TyVarTy tv1) _ -- This is the whole point; | isTcTyVar tv1, isBoxyTyVar tv1 -- choose ty2 if ty2 is a box = orig_ty2 - go ty1 (TyVarTy tv2) -- Symmetrical case + go _ (TyVarTy tv2) -- Symmetrical case | isTcTyVar tv2, isBoxyTyVar tv2 = orig_ty1 @@ -657,7 +656,7 @@ boxyLub orig_ty1 orig_ty2 | Just ty2' <- tcView ty1 = go ty1 ty2' -- For now, we don't look inside ForAlls, PredTys - go ty1 ty2 = orig_ty1 -- Default + go _ _ = orig_ty1 -- Default \end{code} Note [Matching kinds] @@ -735,6 +734,8 @@ tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty -- This indirection is just here to make -- it easy to insert a debug trace! +tc_sub1 :: InstOrigin -> BoxySigmaType -> BoxySigmaType -> InBox + -> BoxySigmaType -> Type -> TcM HsWrapper tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty | Just exp_ty' <- tcView exp_ty = tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty' tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty @@ -771,7 +772,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) } } @@ -786,7 +787,7 @@ tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty -- expected_ty: Int -> Int -- co_fn e = e Int dOrdInt -tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty +tc_sub1 orig _ actual_ty exp_ib exp_sty expected_ty -- Implements the new SPEC rule in the Appendix of the paper -- "Boxy types: inference for higher rank types and impredicativity" -- (This appendix isn't in the published version.) @@ -821,7 +822,7 @@ tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty ----------------------------------- -- Function case (rule F1) -tc_sub1 orig act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res) +tc_sub1 orig _ (FunTy act_arg act_res) exp_ib _ (FunTy exp_arg exp_res) = do { traceTc (text "tc_sub1 - case 4") ; tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res } @@ -837,7 +838,7 @@ tc_sub1 orig act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv) ; tc_sub_funs orig act_arg act_res True arg_ty res_ty } } where mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty' - mk_res_ty other = panic "TcUnify.mk_res_ty3" + mk_res_ty _ = panic "TcUnify.mk_res_ty3" fun_kinds = [argTypeKind, openTypeKind] -- Everything else: defer to boxy matching @@ -852,6 +853,8 @@ tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty } ----------------------------------- +defer_to_boxy_matching :: InstOrigin -> TcType -> TcType -> InBox + -> TcType -> TcType -> TcM HsWrapper defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty = do { coi <- addSubCtxt orig act_sty exp_sty $ u_tys (Unify True act_sty exp_sty) @@ -859,6 +862,8 @@ defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty ; return $ coiToHsWrapper coi } ----------------------------------- +tc_sub_funs :: InstOrigin -> TcType -> BoxySigmaType -> InBox + -> TcType -> BoxySigmaType -> TcM HsWrapper tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res = do { arg_coi <- addSubCtxt orig act_arg exp_arg $ uTysOuter False act_arg exp_ib exp_arg @@ -893,26 +898,21 @@ wrapFunResCoercion arg_tys co_fn_res %************************************************************************ \begin{code} -tcGen :: BoxySigmaType -- expected_ty - -> TcTyVarSet -- Extra tyvars that the universally - -- quantified tyvars of expected_ty - -- must not be unified +tcGen :: BoxySigmaType -- expected_ty + -> TcTyVarSet -- Extra tyvars that the universally + -- quantified tyvars of expected_ty + -- must not be unified + -> Maybe UserTypeCtxt -- Just ctxt => this polytype arose directly + -- from a user type sig + -- Nothing => a higher order situation -> ([TcTyVar] -> 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) <- instantiate expected_ty ; when debugIsOn $ traceTc (text "tcGen" <+> vcat [ @@ -923,7 +923,8 @@ 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 $ + thing_inside tvs' rho' -- Check that the "forall_tvs" havn't been constrained -- The interesting bit here is that we must include the free variables @@ -950,6 +951,23 @@ 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) + instantiate expected_ty + | Just ctxt <- mb_ctxt -- This case split is the wohle reason for mb_ctxt + = do { let skol_info = SigSkol ctxt + ; stuff <- tcInstSigType True skol_info expected_ty + ; return (stuff, skol_info) } + + | 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} @@ -995,7 +1013,7 @@ unifyTheta :: TcThetaType -> TcThetaType -> TcM [CoercionI] unifyTheta theta1 theta2 = do { checkTc (equalLength theta1 theta2) (vcat [ptext (sLit "Contexts differ in length"), - nest 2 $ parens $ ptext (sLit "Use -fglasgow-exts to allow this")]) + nest 2 $ parens $ ptext (sLit "Use -XRelaxedPolyRec to allow this")]) ; uList unifyPred theta1 theta2 } @@ -1005,12 +1023,12 @@ uList :: (a -> a -> TcM b) -- Unify corresponding elements of two lists of types, which -- should be of equal length. We charge down the list explicitly so that -- we can complain if their lengths differ. -uList unify [] [] = return [] +uList _ [] [] = return [] uList unify (ty1:tys1) (ty2:tys2) = do { x <- unify ty1 ty2; ; xs <- uList unify tys1 tys2 ; return (x:xs) } -uList unify ty1s ty2s = panic "Unify.uList: mismatched type lists!" +uList _ _ _ = panic "Unify.uList: mismatched type lists!" \end{code} @unifyTypeList@ takes a single list of @TauType@s and unifies them @@ -1020,7 +1038,7 @@ lists, when all the elts should be of the same type. \begin{code} unifyTypeList :: [TcTauType] -> TcM () unifyTypeList [] = return () -unifyTypeList [ty] = return () +unifyTypeList [_] = return () unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2 ; unifyTypeList tys } \end{code} @@ -1083,11 +1101,11 @@ uTys nb1 ty1 nb2 ty2 uTys_s :: InBox -> [TcType] -- tys1 are the *actual* types -> InBox -> [TcType] -- tys2 are the *expected* types -> TcM [CoercionI] -uTys_s nb1 [] nb2 [] = return [] +uTys_s _ [] _ [] = return [] uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2 ; cois <- uTys_s nb1 tys1 nb2 tys2 ; return (coi:cois) } -uTys_s nb1 ty1s nb2 ty2s = panic "Unify.uTys_s: mismatched type lists!" +uTys_s _ _ _ _ = panic "Unify.uTys_s: mismatched type lists!" -------------- u_tys :: Outer @@ -1121,13 +1139,13 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 go :: Outer -> TcType -> TcType -> TcType -> TcType -> TcM CoercionI -- Always expand synonyms: see Note [Unification and synonyms] -- (this also throws away FTVs) - go outer sty1 ty1 sty2 ty2 + go _ sty1 ty1 sty2 ty2 | Just ty1' <- tcView ty1 = go (Unify False ty1' ty2 ) sty1 ty1' sty2 ty2 | Just ty2' <- tcView ty2 = go (Unify False ty1 ty2') sty1 ty1 sty2 ty2' -- Variables; go for uVar - go outer sty1 (TyVarTy tyvar1) sty2 ty2 = uVar outer False tyvar1 nb2 sty2 ty2 - go outer sty1 ty1 sty2 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 sty1 ty1 + go outer _ (TyVarTy tyvar1) sty2 ty2 = uVar outer False tyvar1 nb2 sty2 ty2 + go outer sty1 ty1 _ (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 sty1 ty1 -- "True" means args swapped -- The case for sigma-types must *follow* the variable cases @@ -1150,7 +1168,7 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do { unless (equalLength theta1 theta2) (bale_out outer) - ; cois <- uPreds outer nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois + ; _cois <- uPreds outer nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois ; traceTc (text "TOMDO!") ; coi <- uTys nb1 tau1 nb2 tau2 @@ -1176,13 +1194,13 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 go outer _ (PredTy p1) _ (PredTy p2) = uPred outer nb1 p1 nb2 p2 - -- Type constructors must match + -- Non-synonym type constructors must match go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2) | con1 == con2 && not (isOpenSynTyCon con1) = do { cois <- uTys_s nb1 tys1 nb2 tys2 ; return $ mkTyConAppCoI con1 tys1 cois } - -- See Note [TyCon app] + -- Family synonyms See Note [TyCon app] | con1 == con2 && identicalOpenSynTyConApp = do { cois <- uTys_s nb1 tys1' nb2 tys2' ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois) @@ -1194,6 +1212,29 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2 -- See Note [OpenSynTyCon app] + -- If we can reduce a family app => proceed with reduct + -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must + -- defer oversaturated applications! + go outer sty1 ty1@(TyConApp con1 _) sty2 ty2 + | isOpenSynTyCon con1 + = do { (coi1, ty1') <- tcNormaliseFamInst ty1 + ; case coi1 of + IdCo -> defer -- no reduction, see [Deferred Unification] + _ -> liftM (coi1 `mkTransCoI`) $ go outer sty1 ty1' sty2 ty2 + } + + -- If we can reduce a family app => proceed with reduct + -- NB: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must + -- defer oversaturated applications! + go outer sty1 ty1 sty2 ty2@(TyConApp con2 _) + | isOpenSynTyCon con2 + = do { (coi2, ty2') <- tcNormaliseFamInst ty2 + ; case coi2 of + IdCo -> defer -- no reduction, see [Deferred Unification] + _ -> liftM (`mkTransCoI` mkSymCoI coi2) $ + go outer sty1 ty1 sty2 ty2' + } + -- Functions; just check the two parts go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2) = do { coi_l <- uTys nb1 fun1 nb2 fun2 @@ -1219,56 +1260,35 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 ; coi_t <- uTys nb1 t1 nb2 t2 ; return $ mkAppTyCoI s1 coi_s t1 coi_t } - -- One or both outermost constructors are type family applications. - -- If we can normalise them away, proceed as usual; otherwise, we - -- need to defer unification by generating a wanted equality constraint. - go outer sty1 ty1 sty2 ty2 - | ty1_is_fun || ty2_is_fun - = do { (coi1, ty1') <- if ty1_is_fun then tcNormaliseFamInst ty1 - else return (IdCo, ty1) - ; (coi2, ty2') <- if ty2_is_fun then tcNormaliseFamInst ty2 - else return (IdCo, ty2) - ; coi <- if isOpenSynTyConApp ty1' || isOpenSynTyConApp ty2' - then do { -- One type family app can't be reduced yet - -- => defer - ; ty1'' <- zonkTcType ty1' - ; ty2'' <- zonkTcType ty2' - ; if tcEqType ty1'' ty2'' - then return IdCo - else -- see [Deferred Unification] - defer_unification outer False orig_ty1 orig_ty2 - } - else -- unification can proceed - go outer sty1 ty1' sty2 ty2' - ; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2) - } - where - ty1_is_fun = isOpenSynTyConApp ty1 - ty2_is_fun = isOpenSynTyConApp ty2 - -- Anything else fails go outer _ _ _ _ = bale_out outer + defer = defer_unification outer False orig_ty1 orig_ty2 + + ---------- -uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2) +uPred :: Outer -> InBox -> PredType -> InBox -> PredType -> TcM CoercionI +uPred _ nb1 (IParam n1 t1) nb2 (IParam n2 t2) | n1 == n2 = do { coi <- uTys nb1 t1 nb2 t2 ; return $ mkIParamPredCoI n1 coi } -uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2) +uPred _ nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2) | c1 == c2 = do { cois <- uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check ; return $ mkClassPPredCoI c1 tys1 cois } -uPred outer _ p1 _ p2 = unifyMisMatch outer +uPred outer _ _ _ _ = unifyMisMatch outer -uPreds outer nb1 [] nb2 [] = return [] +uPreds :: Outer -> InBox -> [PredType] -> InBox -> [PredType] + -> TcM [CoercionI] +uPreds _ _ [] _ [] = return [] uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) = do { coi <- uPred outer nb1 p1 nb2 p2 ; cois <- uPreds outer nb1 ps1 nb2 ps2 ; return (coi:cois) } -uPreds outer nb1 ps1 nb2 ps2 = panic "uPreds" +uPreds _ _ _ _ _ = panic "uPreds" \end{code} Note [TyCon app] @@ -1276,8 +1296,8 @@ Note [TyCon app] When we find two TyConApps, the argument lists are guaranteed equal length. Reason: intially the kinds of the two types to be unified is the same. The only way it can become not the same is when unifying two -AppTys (f1 a1):=:(f2 a2). In that case there can't be a TyConApp in -the f1,f2 (because it'd absorb the app). If we unify f1:=:f2 first, +AppTys (f1 a1)~(f2 a2). In that case there can't be a TyConApp in +the f1,f2 (because it'd absorb the app). If we unify f1~f2 first, which we do, that ensures that f1,f2 have the same kind; and that means a1,a2 have the same kind. And now the argument repeats. @@ -1389,14 +1409,14 @@ uUnfilledVar :: Outer -> TcM CoercionI -- Invariant: tyvar 1 is not unified with anything -uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2 +uUnfilledVar _ swapped tv1 details1 ps_ty2 ty2 | Just ty2' <- tcView ty2 = -- Expand synonyms; ignore FTVs let outer' | swapped = Unify False ty2' (mkTyVarTy tv1) | otherwise = Unify False (mkTyVarTy tv1) ty2' in uUnfilledVar outer' swapped tv1 details1 ps_ty2 ty2' -uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2) +uUnfilledVar outer swapped tv1 details1 _ (TyVarTy tv2) | tv1 == tv2 -- Same type variable => no-op (but watch out for the boxy case) = case details1 of MetaTv BoxTv ref1 -- A boxy type variable meets itself; @@ -1405,7 +1425,7 @@ uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2) ; updateMeta tv1 ref1 (mkTyVarTy tau_tv) ; return IdCo } - other -> return IdCo -- No-op + _ -> return IdCo -- No-op | otherwise -- Distinct type variables = do { lookup2 <- lookupTcTyVar tv2 @@ -1503,7 +1523,7 @@ uMetaVar :: Outer -- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau) -- ty2 is not a type variable -uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 non_var_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 -- @@ -1512,18 +1532,24 @@ uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 non_var_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 info1 ref1 ps_ty2 non_var_ty2 +uMetaVar outer swapped tv1 _ ref1 ps_ty2 _ = do { -- Occurs check + monotype check ; mb_final_ty <- checkTauTvUpdate tv1 ps_ty2 ; case mb_final_ty of @@ -1535,6 +1561,18 @@ uMetaVar outer swapped tv1 info1 ref1 ps_ty2 non_var_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 @@ -1549,13 +1587,13 @@ uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (SkolemTv _) = -- see [Deferred Unification] defer_unification outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2) -uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (SkolemTv _) +uUnfilledVars _ swapped tv1 (MetaTv _ ref1) tv2 (SkolemTv _) = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2) >> return IdCo -uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (MetaTv info2 ref2) +uUnfilledVars _ swapped tv1 (SkolemTv _) tv2 (MetaTv _ ref2) = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) >> return IdCo -- ToDo: this function seems too long for what it acutally does! -uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) +uUnfilledVars _ swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) = case (info1, info2) of (BoxTv, BoxTv) -> box_meets_box >> return IdCo @@ -1626,7 +1664,7 @@ 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) +refineBoxToTau (TyVarTy box_tv) | isMetaTyVar box_tv , MetaTv BoxTv ref <- tcTyVarDetails box_tv = do { cts <- readMutVar ref @@ -1679,6 +1717,7 @@ unBox (TyVarTy tv) | otherwise -- Skolems, and meta-tau-variables = return (TyVarTy tv) +unBoxPred :: PredType -> TcM PredType unBoxPred (ClassP cls tys) = do { tys' <- mapM unBox tys; return (ClassP cls tys') } unBoxPred (IParam ip ty) = do { ty' <- unBox ty; return (IParam ip ty') } unBoxPred (EqPred ty1 ty2) = do { ty1' <- unBox ty1; ty2' <- unBox ty2; return (EqPred ty1' ty2') } @@ -1703,6 +1742,7 @@ popUnifyCtxt (Unify True _ _) thing = popErrCtxt thing popUnifyCtxt (Unify False _ _) thing = thing ----------------------- +unifyCtxt :: TcType -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc) unifyCtxt act_ty exp_ty tidy_env = do { act_ty' <- zonkTcType act_ty ; exp_ty' <- zonkTcType exp_ty @@ -1711,6 +1751,7 @@ unifyCtxt act_ty exp_ty tidy_env ; return (env2, mkExpectedActualMsg act_ty'' exp_ty'') } ---------------- +mkExpectedActualMsg :: Type -> Type -> SDoc mkExpectedActualMsg act_ty exp_ty = nest 2 (vcat [ text "Expected type" <> colon <+> ppr exp_ty, text "Inferred type" <> colon <+> ppr act_ty ]) @@ -1718,6 +1759,7 @@ mkExpectedActualMsg act_ty exp_ty ---------------- -- If an error happens we try to figure out whether the function -- function has been given too many or too few arguments, and say so. +addSubCtxt :: InstOrigin -> TcType -> TcType -> TcM a -> TcM a addSubCtxt orig actual_res_ty expected_res_ty thing_inside = addErrCtxtM mk_err thing_inside where @@ -1736,7 +1778,7 @@ addSubCtxt orig actual_res_ty expected_res_ty thing_inside OccurrenceOf fun | len_exp_args < len_act_args -> wrongArgsCtxt "too few" fun | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun - other -> mkExpectedActualMsg act_ty'' exp_ty'' + _ -> mkExpectedActualMsg act_ty'' exp_ty'' ; return (env2, message) } wrongArgsCtxt too_many_or_few fun @@ -1745,6 +1787,7 @@ addSubCtxt orig actual_res_ty expected_res_ty thing_inside <+> ptext (sLit "arguments") ------------------ +unifyForAllCtxt :: [TyVar] -> Type -> Type -> TidyEnv -> TcM (TidyEnv, SDoc) unifyForAllCtxt tvs phi1 phi2 env = return (env2, msg) where @@ -1817,18 +1860,19 @@ uUnboundKVar swapped kv1 non_var_k2 ; writeKindVar kv1 k2'' } ---------------- +kindOccurCheck :: TyVar -> Type -> TcM () kindOccurCheck kv1 k2 -- k2 is zonked = checkTc (not_in k2) (kindOccurCheckErr kv1 k2) where - not_in (TyVarTy kv2) = kv1 /= kv2 + not_in (TyVarTy kv2) = kv1 /= kv2 not_in (FunTy a2 r2) = not_in a2 && not_in r2 - not_in other = True + not_in _ = True kindSimpleKind :: Bool -> Kind -> TcM SimpleKind -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k -- If the flag is False, it requires k <: sk -- E.g. kindSimpleKind False ?? = * --- What about (kv -> *) :=: ?? -> * +-- What about (kv -> *) ~ ?? -> * kindSimpleKind orig_swapped orig_kind = go orig_swapped orig_kind where @@ -1838,11 +1882,11 @@ kindSimpleKind orig_swapped orig_kind go True k | isOpenTypeKind k = return liftedTypeKind | isArgTypeKind k = return liftedTypeKind - go sw k + go _ k | isLiftedTypeKind k = return liftedTypeKind | isUnliftedTypeKind k = return unliftedTypeKind - go sw k@(TyVarTy _) = return k -- KindVars are always simple - go swapped kind = failWithTc (ptext (sLit "Unexpected kind unification failure:") + go _ k@(TyVarTy _) = return k -- KindVars are always simple + go _ _ = failWithTc (ptext (sLit "Unexpected kind unification failure:") <+> ppr orig_swapped <+> ppr orig_kind) -- I think this can't actually happen @@ -1850,6 +1894,7 @@ kindSimpleKind orig_swapped orig_kind -- T v w = MkT (v -> w) v must not be an umboxed tuple ---------------- +kindOccurCheckErr :: Var -> Type -> SDoc kindOccurCheckErr tyvar ty = hang (ptext (sLit "Occurs check: cannot construct the infinite kind:")) 2 (sep [ppr tyvar, char '=', ppr ty]) @@ -1870,76 +1915,7 @@ unifyFunKind (TyVarTy kvar) = do ; return (Just (arg_kind,res_kind)) } unifyFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind)) -unifyFunKind other = return Nothing -\end{code} - -%************************************************************************ -%* * - Checking kinds -%* * -%************************************************************************ - ---------------------------- --- We would like to get a decent error message from --- (a) Under-applied type constructors --- f :: (Maybe, Maybe) --- (b) Over-applied type constructors --- f :: Int x -> Int x --- - -\begin{code} -checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM () --- A fancy wrapper for 'unifyKind', which tries --- to give decent error messages. --- (checkExpectedKind ty act_kind exp_kind) --- checks that the actual kind act_kind is compatible --- with the expected kind exp_kind --- The first argument, ty, is used only in the error message generation -checkExpectedKind ty act_kind exp_kind - | act_kind `isSubKind` exp_kind -- Short cut for a very common case - = return () - | otherwise = do - (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind) - case mb_r of - Just r -> return () ; -- Unification succeeded - Nothing -> do - - -- So there's definitely an error - -- Now to find out what sort - exp_kind <- zonkTcKind exp_kind - act_kind <- zonkTcKind act_kind - - env0 <- tcInitTidyEnv - let (exp_as, _) = splitKindFunTys exp_kind - (act_as, _) = splitKindFunTys act_kind - n_exp_as = length exp_as - n_act_as = length act_as - - (env1, tidy_exp_kind) = tidyKind env0 exp_kind - (env2, tidy_act_kind) = tidyKind env1 act_kind - - err | n_exp_as < n_act_as -- E.g. [Maybe] - = quotes (ppr ty) <+> ptext (sLit "is not applied to enough type arguments") - - -- Now n_exp_as >= n_act_as. In the next two cases, - -- n_exp_as == 0, and hence so is n_act_as - | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind - = ptext (sLit "Expecting a lifted type, but") <+> quotes (ppr ty) - <+> ptext (sLit "is unlifted") - - | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind - = ptext (sLit "Expecting an unlifted type, but") <+> quotes (ppr ty) - <+> ptext (sLit "is lifted") - - | otherwise -- E.g. Monad [Int] - = ptext (sLit "Kind mis-match") - - more_info = sep [ ptext (sLit "Expected kind") <+> - quotes (pprKind tidy_exp_kind) <> comma, - ptext (sLit "but") <+> quotes (ppr ty) <+> - ptext (sLit "has kind") <+> quotes (pprKind tidy_act_kind)] - - failWithTcM (env2, err $$ more_info) +unifyFunKind _ = return Nothing \end{code} %************************************************************************ @@ -1992,10 +1968,10 @@ check_sig_tyvars -> [TcTyVar] -- Universally-quantified type variables in the signature -- Guaranteed to be skolems -> TcM () -check_sig_tyvars extra_tvs [] +check_sig_tyvars _ [] = return () check_sig_tyvars extra_tvs sig_tvs - = ASSERT( all isSkolemTyVar sig_tvs ) + = ASSERT( all isTcTyVar sig_tvs && all isSkolemTyVar sig_tvs ) do { gbl_tvs <- tcGetGlobalTyVars ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs, text "gbl_tvs" <+> ppr gbl_tvs, @@ -2031,6 +2007,7 @@ bleatEscapedTvs globals sig_tvs zonked_tvs ; return (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) } ----------------------- +escape_msg :: Var -> Var -> [SDoc] -> SDoc escape_msg sig_tv zonked_tv globs | notNull globs = vcat [sep [msg, ptext (sLit "is mentioned in the environment:")],