X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=ghc%2Fcompiler%2Ftypecheck%2FTcUnify.lhs;h=bc6f537b4d1f4dc9846d78e2d037096d7bcd4612;hb=a180ee15dfe2eb0da03cd92ca89475765cd080d9;hp=c136846e14fddf0d5a9402bc2c770946cf88eac2;hpb=d133b73a4d4717892ced072d05e039a54ede0ceb;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index c136846..bc6f537 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -8,36 +8,33 @@ updatable substitution). \begin{code} module TcUnify ( unifyTauTy, unifyTauTyList, unifyTauTyLists, - unifyFunTy, unifyListTy, unifyTupleTy, unifyUnboxedTupleTy, - unifyKind, unifyKinds, unifyTypeKind + unifyFunTy, unifyListTy, unifyTupleTy, + unifyKind, unifyKinds, unifyOpenTypeKind ) where #include "HsVersions.h" -- friends: import TcMonad -import Type ( Type(..), tyVarsOfType, funTyCon, - mkFunTy, splitFunTy_maybe, splitTyConApp_maybe, - isNotUsgTy, - Kind, boxedTypeKind, typeCon, anyBoxCon, anyBoxKind, - splitAppTy_maybe, +import TypeRep ( Type(..), PredType(..) ) -- friend +import Type ( funTyCon, Kind, unboxedTypeKind, boxedTypeKind, openTypeKind, + superBoxity, typeCon, openKindCon, hasMoreBoxityInfo, + tyVarsOfType, typeKind, + mkTyVarTy, mkFunTy, splitFunTy_maybe, splitTyConApp_maybe, + isNotUsgTy, splitAppTy_maybe, mkTyConApp, tidyOpenType, tidyOpenTypes, tidyTyVar ) -import TyCon ( TyCon, isTupleTyCon, isUnboxedTupleTyCon, - tyConArity ) -import Name ( hasBetterProv ) +import TyCon ( TyCon, isTupleTyCon, tupleTyConBoxity, tyConArity ) import Var ( TyVar, tyVarKind, varName, isSigTyVar ) -import VarEnv import VarSet ( varSetElems ) -import TcType ( TcType, TcTauType, TcTyVar, TcKind, - newTyVarTy, newOpenTypeKind, newTyVarTy_OpenKind, - tcGetTyVar, tcPutTyVar, zonkTcType, tcTypeKind +import TcType ( TcType, TcTauType, TcTyVar, TcKind, newBoxityVar, + newTyVarTy, newTyVarTys, tcGetTyVar, tcPutTyVar, zonkTcType ) +import Name ( isSystemName ) + -- 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} @@ -51,18 +48,39 @@ import Outputable \begin{code} unifyKind :: TcKind -- Expected -> TcKind -- Actual - -> TcM s () + -> TcM () unifyKind k1 k2 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $ uTys k1 k1 k2 k2 -unifyKinds :: [TcKind] -> [TcKind] -> TcM s () +unifyKinds :: [TcKind] -> [TcKind] -> TcM () unifyKinds [] [] = returnTc () unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_` unifyKinds ks1 ks2 unifyKinds _ _ = panic "unifyKinds: length mis-match" \end{code} +\begin{code} +unifyOpenTypeKind :: TcKind -> TcM () +-- Ensures that the argument kind is of the form (Type bx) +-- for some boxity bx + +unifyOpenTypeKind ty@(TyVarTy tyvar) + = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty -> + case maybe_ty of + Just ty' -> unifyOpenTypeKind ty' + other -> unify_open_kind_help ty + +unifyOpenTypeKind ty + = case splitTyConApp_maybe ty of + Just (tycon, [_]) | tycon == typeCon -> returnTc () + other -> unify_open_kind_help ty + +unify_open_kind_help ty -- Revert to ordinary unification + = newBoxityVar `thenNF_Tc` \ boxity -> + unifyKind ty (mkTyConApp typeCon [boxity]) +\end{code} + %************************************************************************ %* * @@ -76,7 +94,7 @@ non-exported generic functions. Unify two @TauType@s. Dead straightforward. \begin{code} -unifyTauTy :: TcTauType -> TcTauType -> TcM s () +unifyTauTy :: TcTauType -> TcTauType -> TcM () unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $ uTys ty1 ty1 ty2 ty2 @@ -88,7 +106,7 @@ of equal length. We charge down the list explicitly so that we can complain if their lengths differ. \begin{code} -unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM s () +unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM () unifyTauTyLists [] [] = returnTc () unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_` unifyTauTyLists tys1 tys2 @@ -100,7 +118,7 @@ all together. It is used, for example, when typechecking explicit lists, when all the elts should be of the same type. \begin{code} -unifyTauTyList :: [TcTauType] -> TcM s () +unifyTauTyList :: [TcTauType] -> TcM () unifyTauTyList [] = returnTc () unifyTauTyList [ty] = returnTc () unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_` @@ -123,8 +141,11 @@ We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''. \begin{code} uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1 + -- ty1 is the *expected* type + -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2 - -> TcM s () + -- ty2 is the *actual* type + -> TcM () -- Always expand synonyms (see notes at end) -- (this also throws away FTVs and usage annots) @@ -136,20 +157,26 @@ uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1 -- "True" means args swapped + -- Predicates +uTys _ (PredTy (IParam n1 t1)) _ (PredTy (IParam n2 t2)) + | n1 == n2 = uTys t1 t1 t2 t2 +uTys _ (PredTy (Class c1 tys1)) _ (PredTy (Class c2 tys2)) + | c1 == c2 = unifyTauTyLists tys1 tys2 + -- Functions; just check the two parts uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2) = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2 -- Type constructors must match uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2) - = checkTcM (cons_match && length tys1 == length tys2) - (unifyMisMatch ps_ty1 ps_ty2) `thenTc_` - unifyTauTyLists tys1 tys2 - where - -- The AnyBox wild card matches anything - cons_match = con1 == con2 - || con1 == anyBoxCon - || con2 == anyBoxCon + | con1 == con2 && length tys1 == length tys2 + = unifyTauTyLists tys1 tys2 + + | con1 == openKindCon + -- When we are doing kind checking, we might match a kind '?' + -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and + -- (CCallable Int) and (CCallable Int#) are both OK + = unifyOpenTypeKind ps_ty2 -- Applications need a bit of care! -- They can match FunTy and TyConApp, so use splitAppTy_maybe @@ -243,7 +270,7 @@ uVar :: Bool -- False => tyvar is the "expected" -- True => ty is the "expected" thing -> TcTyVar -> TcTauType -> TcTauType -- printing and real versions - -> TcM s () + -> TcM () uVar swapped tv1 ps_ty2 ty2 = tcGetTyVar tv1 `thenNF_Tc` \ maybe_ty1 -> @@ -271,34 +298,58 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2) case maybe_ty2 of Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2' - Nothing -> checkKinds swapped tv1 ty2 `thenTc_` + Nothing | tv1_dominates_tv2 + + -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) ) + tcPutTyVar tv2 (TyVarTy tv1) `thenNF_Tc_` + returnTc () + | otherwise - if tv1 `dominates` tv2 then - tcPutTyVar tv2 (TyVarTy tv1) `thenNF_Tc_` - returnTc () - else - ASSERT( isNotUsgTy ps_ty2 ) - tcPutTyVar tv1 ps_ty2 `thenNF_Tc_` - returnTc () + -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) ) + (ASSERT( isNotUsgTy ps_ty2 ) + tcPutTyVar tv1 ps_ty2 `thenNF_Tc_` + returnTc ()) where - tv1 `dominates` tv2 = isSigTyVar tv1 + k1 = tyVarKind tv1 + k2 = tyVarKind tv2 + tv1_dominates_tv2 = isSigTyVar tv1 -- Don't unify a signature type variable if poss - || varName tv1 `hasBetterProv` varName tv2 + || k2 == openTypeKind + -- Try to get rid of open type variables as soon as poss + || isSystemName (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 - | non_var_ty2 == anyBoxKind - -- If the - = returnTc () - - | otherwise = 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 ps_ty2 `thenNF_Tc_` + + warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1)) + ((ppr tv1 <+> ppr (tyVarKind tv1)) $$ + (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2))) `thenNF_Tc_` + + 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_` @@ -316,21 +367,22 @@ uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2 other -> returnTc () checkKinds swapped tv1 ty2 +-- We're about to unify a type variable tv1 with a non-tyvar-type ty2. +-- We need to check that we don't unify a boxed type variable with an +-- unboxed type: e.g. (id 3#) is illegal + | tk1 == boxedTypeKind && tk2 == unboxedTypeKind = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $ - - -- We have to use tcTypeKind not just typeKind to get the - -- kind of ty2, because there might be mutable kind variables - -- in the way. For example, suppose that ty2 :: (a b), and - -- the kind of 'a' is a kind variable 'k' that has (presumably) - -- been unified with 'k1 -> k2'. - tcTypeKind ty2 `thenNF_Tc` \ k2 -> - - if swapped then - unifyKind k2 (tyVarKind tv1) - else - unifyKind (tyVarKind tv1) k2 + unifyMisMatch k1 k2 + | otherwise + = returnTc () + where + (k1,k2) | swapped = (tk2,tk1) + | otherwise = (tk1,tk2) + tk1 = tyVarKind tv1 + tk2 = typeKind ty2 \end{code} + %************************************************************************ %* * \subsection[Unify-fun]{@unifyFunTy@} @@ -341,7 +393,7 @@ checkKinds swapped tv1 ty2 \begin{code} unifyFunTy :: TcType -- Fail if ty isn't a function type - -> TcM s (TcType, TcType) -- otherwise return arg and result types + -> TcM (TcType, TcType) -- otherwise return arg and result types unifyFunTy ty@(TyVarTy tyvar) = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty -> @@ -355,15 +407,15 @@ unifyFunTy ty Nothing -> unify_fun_ty_help ty unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification - = newTyVarTy_OpenKind `thenNF_Tc` \ arg -> - newTyVarTy_OpenKind `thenNF_Tc` \ res -> + = newTyVarTy openTypeKind `thenNF_Tc` \ arg -> + newTyVarTy openTypeKind `thenNF_Tc` \ res -> unifyTauTy ty (mkFunTy arg res) `thenTc_` returnTc (arg,res) \end{code} \begin{code} unifyListTy :: TcType -- expected list type - -> TcM s TcType -- list element type + -> TcM TcType -- list element type unifyListTy ty@(TyVarTy tyvar) = tcGetTyVar tyvar `thenNF_Tc` \ maybe_ty -> @@ -383,65 +435,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) +unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType] +unifyTupleTy boxity 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 + Just ty' -> unifyTupleTy boxity arity ty' + other -> unify_tuple_ty_help boxity arity ty -unifyTupleTy arity ty +unifyTupleTy boxity 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_` + 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 + = newTyVarTys arity kind `thenNF_Tc` \ arg_tys -> + unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_` returnTc arg_tys -\end{code} - -\begin{code} -unifyUnboxedTupleTy :: Arity -> TcType -> TcM s [TcType] -unifyUnboxedTupleTy 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 - -unifyUnboxedTupleTy 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_` - returnTc arg_tys -\end{code} - -Make sure a kind is of the form (Type b) for some boxity b. - -\begin{code} -unifyTypeKind :: TcKind -> TcM s () -unifyTypeKind kind@(TyVarTy kv) - = tcGetTyVar kv `thenNF_Tc` \ maybe_kind -> - case maybe_kind of - Just kind' -> unifyTypeKind kind' - Nothing -> unify_type_kind_help kind - -unifyTypeKind kind - = case splitTyConApp_maybe kind of - Just (tycon, [_]) | tycon == typeCon -> returnTc () - other -> unify_type_kind_help kind - -unify_type_kind_help kind - = newOpenTypeKind `thenNF_Tc` \ expected_kind -> - unifyKind expected_kind kind + where + kind | isBoxed boxity = boxedTypeKind + | otherwise = openTypeKind \end{code} @@ -470,15 +486,19 @@ unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2] unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred - = returnNF_Tc (env2, ptext SLIT("When matching types") <+> - sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual]) + -- tv1 is zonked already + = zonkTcType ty2 `thenNF_Tc` \ ty2' -> + returnNF_Tc (err ty2') where - (pp_expected, pp_actual) | swapped = (pp2, pp1) - | otherwise = (pp1, pp2) - (env1, tv1') = tidyTyVar tidy_env tv1 - (env2, ty2') = tidyOpenType env1 ty2 - pp1 = ppr tv1' - pp2 = ppr ty2' + err ty2 = (env2, ptext SLIT("When matching types") <+> + sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual]) + where + (pp_expected, pp_actual) | swapped = (pp2, pp1) + | otherwise = (pp1, pp2) + (env1, tv1') = tidyTyVar tidy_env tv1 + (env2, ty2') = tidyOpenType env1 ty2 + pp1 = ppr tv1' + pp2 = ppr ty2' unifyMisMatch ty1 ty2 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->