X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcUnify.lhs;h=ba131c09d5a33afa9a1df03a72f065a6ddd10eef;hb=ff755dd9a0a0ad2f106c323852553ea247f16141;hp=a6bf468fd31f6ffad5d4279682aaf33185de066c;hpb=7e602b0a11e567fcb035d1afd34015aebcf9a577;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index a6bf468..ba131c0 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -8,7 +8,7 @@ updatable substitution). \begin{code} module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists, - unifyFunTy, unifyListTy, unifyTupleTy, unifyUnboxedTupleTy, + unifyFunTy, unifyListTy, unifyTupleTy, unifyKind, unifyKinds, unifyTypeKind ) where @@ -16,27 +16,27 @@ module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists, -- friends: import TcMonad -import Type ( Type(..), tyVarsOfType, funTyCon, - mkFunTy, splitFunTy_maybe, splitTyConApp_maybe, +import TypeRep ( Type(..), funTyCon, Kind, boxedTypeKind, typeCon, anyBoxCon, anyBoxKind, + ) -- friend +import Type ( tyVarsOfType, + mkFunTy, splitFunTy_maybe, splitTyConApp_maybe, + isNotUsgTy, splitAppTy_maybe, tidyOpenType, tidyOpenTypes, tidyTyVar ) -import TyCon ( TyCon, isTupleTyCon, isUnboxedTupleTyCon, - tyConArity ) -import Name ( isSysLocalName ) -import Var ( TyVar, tyVarKind, varName ) -import VarEnv +import TyCon ( TyCon, isTupleTyCon, tupleTyConBoxity, tyConArity ) +import Name ( hasBetterProv ) +import Var ( TyVar, tyVarKind, varName, isSigTyVar ) import VarSet ( varSetElems ) import TcType ( TcType, TcTauType, TcTyVar, TcKind, newTyVarTy, newOpenTypeKind, newTyVarTy_OpenKind, tcGetTyVar, tcPutTyVar, zonkTcType, tcTypeKind ) + -- others: -import BasicTypes ( Arity ) -import TysWiredIn ( listTyCon, mkListTy, mkTupleTy, mkUnboxedTupleTy ) -import PprType () -- Instances -import Util +import BasicTypes ( Arity, Boxity, isBoxed ) +import TysWiredIn ( listTyCon, mkListTy, mkTupleTy ) import Outputable \end{code} @@ -126,6 +126,7 @@ uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1 -> TcM s () -- Always expand synonyms (see notes at end) + -- (this also throws away FTVs and usage annots) uTys ps_ty1 (NoteTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2 uTys ps_ty1 ty1 ps_ty2 (NoteTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2 @@ -141,7 +142,7 @@ uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2) -- Type constructors must match uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2) = checkTcM (cons_match && length tys1 == length tys2) - (failWithTcM (unifyMisMatch ps_ty1 ps_ty2)) `thenTc_` + (unifyMisMatch ps_ty1 ps_ty2) `thenTc_` unifyTauTyLists tys1 tys2 where -- The AnyBox wild card matches anything @@ -156,21 +157,21 @@ uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2) uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2 = case splitAppTy_maybe ty2 of Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2 - Nothing -> failWithTcM (unifyMisMatch ps_ty1 ps_ty2) + Nothing -> unifyMisMatch ps_ty1 ps_ty2 -- Now the same, but the other way round -- Don't swap the types, because the error messages get worse uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2) = case splitAppTy_maybe ty1 of Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2 - Nothing -> failWithTcM (unifyMisMatch ps_ty1 ps_ty2) + Nothing -> unifyMisMatch ps_ty1 ps_ty2 -- Not expecting for-alls in unification -- ... but the error message from the unifyMisMatch more informative -- than a panic message! -- Anything else fails -uTys ps_ty1 ty1 ps_ty2 ty2 = failWithTcM (unifyMisMatch ps_ty1 ps_ty2) +uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2 \end{code} Notes on synonyms @@ -250,7 +251,7 @@ uVar swapped tv1 ps_ty2 ty2 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2 - -- Expand synonyms + -- Expand synonyms; ignore FTVs; ignore usage annots uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy _ ty2) = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2 @@ -271,14 +272,18 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2) Nothing -> checkKinds swapped tv1 ty2 `thenTc_` - -- Try to update sys-y type variables in preference to sig-y ones - -- (the latter respond False to isSysLocalName) - if isSysLocalName (varName tv2) then - tcPutTyVar tv2 (TyVarTy tv1) `thenNF_Tc_` + if tv1 `dominates` tv2 then + tcPutTyVar tv2 (TyVarTy tv1) `thenNF_Tc_` returnTc () else - tcPutTyVar tv1 ps_ty2 `thenNF_Tc_` + ASSERT( isNotUsgTy ps_ty2 ) + tcPutTyVar tv1 ps_ty2 `thenNF_Tc_` returnTc () + where + tv1 `dominates` tv2 = isSigTyVar tv1 + -- Don't unify a signature type variable if poss + || varName tv1 `hasBetterProv` varName tv2 + -- Try to update sys-y type variables in preference to sig-y ones -- Second one isn't a type variable uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2 @@ -287,9 +292,31 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2 = returnTc () | otherwise - = checkKinds swapped tv1 non_var_ty2 `thenTc_` - occur_check non_var_ty2 `thenTc_` - tcPutTyVar tv1 ps_ty2 `thenNF_Tc_` + = checkKinds swapped tv1 non_var_ty2 `thenTc_` + occur_check non_var_ty2 `thenTc_` + ASSERT( isNotUsgTy ps_ty2 ) + checkTcM (not (isSigTyVar tv1)) + (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_` + + tcPutTyVar tv1 non_var_ty2 `thenNF_Tc_` + -- This used to say "ps_ty2" instead of "non_var_ty2" + + -- But that led to an infinite loop in the type checker! + -- Consider + -- type A a = () + -- + -- f :: (A a -> a -> ()) -> () + -- f = \ _ -> () + -- + -- x :: () + -- x = f (\ x p -> p x) + -- + -- Here, we try to match "t" with "A t", and succeed + -- because the unifier looks through synonyms. The occurs + -- check doesn't kick in because we are "really" binding "t" to "()", + -- but we *actually* bind "t" to "A t" if we store ps_ty2. + -- That leads the typechecker into an infinite loop later. + returnTc () where occur_check ty = mapTc occur_check_tv (varSetElems (tyVarsOfType ty)) `thenTc_` @@ -374,45 +401,29 @@ unify_list_ty_help ty -- Revert to ordinary unification \end{code} \begin{code} -unifyTupleTy :: Arity -> TcType -> TcM s [TcType] -unifyTupleTy arity ty@(TyVarTy tyvar) - = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - Just ty' -> unifyTupleTy arity ty' - other -> unify_tuple_ty_help arity ty - -unifyTupleTy arity ty - = case splitTyConApp_maybe ty of - Just (tycon, arg_tys) | isTupleTyCon tycon - && tyConArity tycon == arity - -> returnTc arg_tys - other -> unify_tuple_ty_help arity ty - -unify_tuple_ty_help arity ty - = mapNF_Tc (\ _ -> newTyVarTy boxedTypeKind) [1..arity] `thenNF_Tc` \ arg_tys -> - unifyTauTy ty (mkTupleTy arity arg_tys) `thenTc_` - returnTc arg_tys -\end{code} - -\begin{code} -unifyUnboxedTupleTy :: Arity -> TcType -> TcM s [TcType] -unifyUnboxedTupleTy arity ty@(TyVarTy tyvar) +unifyTupleTy :: Boxity -> Arity -> TcType -> TcM s [TcType] +unifyTupleTy boxity arity ty@(TyVarTy tyvar) = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty -> case maybe_ty of - Just ty' -> unifyUnboxedTupleTy arity ty' - other -> unify_unboxed_tuple_ty_help arity ty + Just ty' -> unifyTupleTy boxity arity ty' + other -> unify_tuple_ty_help boxity arity ty -unifyUnboxedTupleTy arity ty +unifyTupleTy boxity arity ty = case splitTyConApp_maybe ty of - Just (tycon, arg_tys) | isUnboxedTupleTyCon tycon - && tyConArity tycon == arity - -> returnTc arg_tys - other -> unify_tuple_ty_help arity ty - -unify_unboxed_tuple_ty_help arity ty - = mapNF_Tc (\ _ -> newTyVarTy_OpenKind) [1..arity] `thenNF_Tc` \ arg_tys -> - unifyTauTy ty (mkUnboxedTupleTy arity arg_tys) `thenTc_` + Just (tycon, arg_tys) + | isTupleTyCon tycon + && tyConArity tycon == arity + && tupleTyConBoxity tycon == boxity + -> returnTc arg_tys + other -> unify_tuple_ty_help boxity arity ty + +unify_tuple_ty_help boxity arity ty + = mapNF_Tc new_tyvar [1..arity] `thenNF_Tc` \ arg_tys -> + unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_` returnTc arg_tys + where + new_tyvar _ | isBoxed boxity = newTyVarTy boxedTypeKind + | otherwise = newTyVarTy_OpenKind \end{code} Make sure a kind is of the form (Type b) for some boxity b. @@ -472,11 +483,23 @@ unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 infer pp2 = ppr ty2' unifyMisMatch ty1 ty2 - = (env2, hang (ptext SLIT("Couldn't match")) - 4 (sep [quotes (ppr tidy_ty1), ptext SLIT("against"), quotes (ppr tidy_ty2)])) + = zonkTcType ty1 `thenNF_Tc` \ ty1' -> + zonkTcType ty2 `thenNF_Tc` \ ty2' -> + let + (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2'] + msg = hang (ptext SLIT("Couldn't match")) + 4 (sep [quotes (ppr tidy_ty1), + ptext SLIT("against"), + quotes (ppr tidy_ty2)]) + in + failWithTcM (env, msg) + +unifyWithSigErr tyvar ty + = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar)) + 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty))) where - (env1, tidy_ty1) = tidyOpenType emptyTidyEnv ty1 - (env2, tidy_ty2) = tidyOpenType env1 ty2 + (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar + (env2, tidy_ty) = tidyOpenType env1 ty unifyOccurCheck tyvar ty = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))