X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=e038888950569c980a1a55a3fb5e07c8ad1ff13e;hb=302e2e29f2e1074bfba561e077a484dc4e1d15f6;hp=367536babb20ae4b185b1ad0f259d7adf094a5ec;hpb=aaed05e88978688e37dc74177dd4eba51a6ab4d0;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 367536b..e038888 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -14,7 +14,6 @@ module TcUnify ( -- Various unifications unifyType, unifyTypeList, unifyTheta, unifyKind, unifyKinds, unifyFunKind, - checkExpectedKind, preSubType, boxyMatchTypes, -------------------------------- @@ -579,9 +578,10 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst go ty1 ty2 -- C.f. the isSigmaTy case for boxySubMatchType | isSigmaTy ty1 - , (tvs1, _, tau1) <- tcSplitSigmaTy ty1 - , (tvs2, _, tau2) <- tcSplitSigmaTy ty2 + , (tvs1, ps1, tau1) <- tcSplitSigmaTy ty1 + , (tvs2, ps2, tau2) <- tcSplitSigmaTy ty2 , equalLength tvs1 tvs2 + , equalLength ps1 ps2 = boxy_match (tmpl_tvs `delVarSetList` tvs1) tau1 (boxy_tvs `extendVarSetList` tvs2) tau2 subst @@ -611,7 +611,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 @@ -1037,8 +1040,8 @@ lists, when all the elts should be of the same type. unifyTypeList :: [TcTauType] -> TcM () unifyTypeList [] = return () unifyTypeList [_] = return () -unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2 - ; unifyTypeList tys } +unifyTypeList (ty1:tys@(ty2:_)) = do { _ <- unifyType ty1 ty2 + ; unifyTypeList tys } \end{code} %************************************************************************ @@ -1085,7 +1088,7 @@ uTysOuter :: InBox -> TcType -- ty1 is the *actual* type -> TcM CoercionI -- We've just pushed a context describing ty1,ty2 uTysOuter nb1 ty1 nb2 ty2 - = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2) + = do { traceTc (text "uTysOuter" <+> sep [ppr ty1, ppr ty2]) ; u_tys (Unify True ty1 ty2) nb1 ty1 ty1 nb2 ty2 ty2 } uTys :: InBox -> TcType -> InBox -> TcType -> TcM CoercionI @@ -1096,14 +1099,19 @@ uTys nb1 ty1 nb2 ty2 -------------- -uTys_s :: InBox -> [TcType] -- tys1 are the *actual* types +uTys_s :: Outer + -> InBox -> [TcType] -- tys1 are the *actual* types -> InBox -> [TcType] -- tys2 are the *expected* types -> TcM [CoercionI] -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 _ _ _ _ = panic "Unify.uTys_s: mismatched type lists!" +uTys_s outer nb1 tys1 nb2 tys2 + = go tys1 tys2 + where + go [] [] = return [] + go (ty1:tys1) (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2 + ; cois <- go tys1 tys2 + ; return (coi:cois) } + go _ _ = unifyMisMatch outer + -- See Note [Mismatched type lists and application decomposition] -------------- u_tys :: Outer @@ -1192,15 +1200,17 @@ 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 - go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2) + -- Non-synonym type constructors must match + go outer _ (TyConApp con1 tys1) _ (TyConApp con2 tys2) | con1 == con2 && not (isOpenSynTyCon con1) - = do { cois <- uTys_s nb1 tys1 nb2 tys2 + = do { traceTc (text "utys1" <+> ppr con1 <+> (ppr tys1 $$ ppr tys2)) + ; cois <- uTys_s outer 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' + = do { traceTc (text "utys2" <+> ppr con1 <+> (ppr tys1' $$ ppr tys2')) + ; cois <- uTys_s outer nb1 tys1' nb2 tys2' ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois) } where @@ -1221,9 +1231,10 @@ u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 -- They can match FunTy and TyConApp, so use splitAppTy_maybe -- NB: we've already dealt with type variables and Notes, -- so if one type is an App the other one jolly well better be too + -- See Note [Mismatched type lists and application decomposition] go outer _ (AppTy s1 t1) _ ty2 | Just (s2,t2) <- tcSplitAppTy_maybe ty2 - = do { coi_s <- go outer s1 s1 s2 s2 -- NB recurse into go + = do { coi_s <- go outer s1 s1 s2 s2 -- NB recurse into go... ; coi_t <- uTys nb1 t1 nb2 t2 -- See Note [Unifying AppTy] ; return $ mkAppTyCoI s1 coi_s t1 coi_t } @@ -1235,48 +1246,47 @@ 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) + -- If we can reduce a family app => proceed with reduct + -- NB1: We use isOpenSynTyCon, not isOpenSynTyConApp as we also must + -- defer oversaturated applications! + -- + -- NB2: Do this *after* trying decomposing applications, so that decompose + -- (m a) ~ (F Int b) + -- where F has arity 1 + go _ _ ty1@(TyConApp con1 _) _ ty2 + | isOpenSynTyCon con1 + = do { (coi1, ty1') <- tcNormaliseFamInst ty1 + ; case coi1 of + IdCo -> defer -- no reduction, see [Deferred Unification] + _ -> liftM (coi1 `mkTransCoI`) $ uTys nb1 ty1' nb2 ty2 + } + + go _ _ ty1 _ ty2@(TyConApp con2 _) + | isOpenSynTyCon con2 + = do { (coi2, ty2') <- tcNormaliseFamInst ty2 + ; case coi2 of + IdCo -> defer -- no reduction, see [Deferred Unification] + _ -> liftM (`mkTransCoI` mkSymCoI coi2) $ + uTys nb1 ty1 nb2 ty2' } - 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 -> 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 _ 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 - } + | n1 == n2 + = do { coi <- uTys nb1 t1 nb2 t2 + ; return $ mkIParamPredCoI n1 coi } +uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2) + | c1 == c2 + = do { traceTc (text "utys3" <+> ppr c1 <+> (ppr tys2 $$ ppr tys2)) + ; cois <- uTys_s outer nb1 tys1 nb2 tys2 + ; return $ mkClassPPredCoI c1 tys1 cois } uPred outer _ _ _ _ = unifyMisMatch outer uPreds :: Outer -> InBox -> [PredType] -> InBox -> [PredType] @@ -1290,15 +1300,23 @@ uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) = uPreds _ _ _ _ _ = panic "uPreds" \end{code} -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, -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. +Note [Mismatched type lists and application decomposition] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When we find two TyConApps, you might think that the argument lists +are guaranteed equal length. But they aren't. Consider matching + w (T x) ~ Foo (T x y) +We do match (w ~ Foo) first, but in some circumstances we simply create +a deferred constraint; and then go ahead and match (T x ~ T x y). +This came up in Trac #3950. + +So either + (a) either we must check for identical argument kinds + when decomposing applications, + + (b) or we must be prepared for ill-kinded unification sub-problems + +Currently we adopt (b) since it seems more robust -- no need to maintain +a global invariant. Note [OpenSynTyCon app] ~~~~~~~~~~~~~~~~~~~~~~~ @@ -1680,7 +1698,7 @@ zapToMonotype :: BoxySigmaType -> TcM TcTauType -- with that type. zapToMonotype res_ty = do { res_tau <- newFlexiTyVarTy liftedTypeKind - ; boxyUnify res_tau res_ty + ; _ <- boxyUnify res_tau res_ty ; return res_tau } unBox :: BoxyType -> TcM TcType @@ -1871,7 +1889,7 @@ 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 @@ -1919,75 +1937,6 @@ unifyFunKind _ = return Nothing %************************************************************************ %* * - 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 _ -> 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) -\end{code} - -%************************************************************************ -%* * \subsection{Checking signature type variables} %* * %************************************************************************ @@ -2039,7 +1988,7 @@ check_sig_tyvars 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,