X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FUnify.lhs;h=4e200006de22d7d5b564000ed79df086f50459f7;hb=2c8f04b5b883db74f449dfc8c224929fe28b027d;hp=c8edce0c9df5f2ad09fd63b9cdaa6bb30dad351c;hpb=7d61cb61daa5e433a0cb85b34b7f0c58b2f961ff;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/Unify.lhs b/ghc/compiler/typecheck/Unify.lhs index c8edce0..4e20000 100644 --- a/ghc/compiler/typecheck/Unify.lhs +++ b/ghc/compiler/typecheck/Unify.lhs @@ -7,27 +7,32 @@ The unifier is now squarely in the typechecker monad (because of the updatable substitution). \begin{code} -#include "HsVersions.h" - -module Unify ( unifyTauTy, unifyTauTyList, unifyTauTyLists, unifyFunTy ) where +module Unify ( unifyTauTy, unifyTauTyList, unifyTauTyLists, + unifyFunTy, unifyListTy, unifyTupleTy, + Subst, unifyTysX, unifyTyListsX + ) where -import Ubiq +#include "HsVersions.h" -- friends: import TcMonad -import Type ( GenType(..), getTypeKind, mkFunTy, getFunTy_maybe ) -import TyCon ( TyCon, mkFunTyCon ) -import TyVar ( GenTyVar(..), TyVar(..), getTyVarKind ) -import TcType ( TcType(..), TcMaybe(..), TcTauType(..), TcTyVar(..), +import Type ( GenType(..), Type, tyVarsOfType, + typeKind, mkFunTy, splitFunTy_maybe, splitTyConApp_maybe ) +import TyCon ( TyCon, mkFunTyCon, isTupleTyCon, tyConArity, Arity ) +import TyVar ( TyVar(..), GenTyVar(..), tyVarKind, tyVarFlexi, + TyVarEnv, lookupTyVarEnv, emptyTyVarEnv, addToTyVarEnv, + tyVarSetToList + ) +import TcType ( TcType, TcMaybe(..), TcTauType, TcTyVar, newTyVarTy, tcReadTyVar, tcWriteTyVar, zonkTcType ) -- others: -import Kind ( Kind, isSubKindOf, mkTypeKind ) -import Usage ( duffUsage ) -import PprType ( GenTyVar, GenType ) -- instances -import Pretty -import Unique ( Unique ) -- instances +import Kind ( Kind, hasMoreBoxityInfo, mkTypeKind, mkBoxedTypeKind ) +import TysWiredIn ( listTyCon, mkListTy, mkTupleTy ) +import Maybes ( maybeToBool ) +import PprType () -- Instances import Util +import Outputable \end{code} @@ -44,7 +49,7 @@ Unify two @TauType@s. Dead straightforward. \begin{code} unifyTauTy :: TcTauType s -> TcTauType s -> TcM s () -unifyTauTy ty1 ty2 +unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred = tcAddErrCtxtM (unifyCtxt ty1 ty2) $ uTys ty1 ty1 ty2 ty2 \end{code} @@ -59,7 +64,7 @@ unifyTauTyLists :: [TcTauType s] -> [TcTauType s] -> TcM s () unifyTauTyLists [] [] = returnTc () unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_` unifyTauTyLists tys1 tys2 -unifyTauTypeLists ty1s ty2s = panic "Unify.unifyTauTypeLists: mismatched type lists!" +unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!" \end{code} @unifyTauTyList@ takes a single list of @TauType@s and unifies them @@ -93,39 +98,54 @@ uTys :: TcTauType s -> TcTauType s -- Error reporting ty1 and real ty1 -> TcTauType s -> TcTauType s -- Error reporting ty2 and real ty2 -> TcM s () + -- Always expand synonyms (see notes at end) +uTys ps_ty1 (SynTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2 +uTys ps_ty1 ty1 ps_ty2 (SynTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2 + -- Variables; go for uVar uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar tyvar1 ps_ty2 ty2 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar tyvar2 ps_ty1 ty1 - -- Applications and functions; just check the two parts -uTys _ (FunTy fun1 arg1 _) _ (FunTy fun2 arg2 _) + -- 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) + = checkTc (con1 == con2 && length tys1 == length tys2) + (unifyMisMatch ps_ty1 ps_ty2) `thenTc_` + unifyTauTyLists tys1 tys2 + + -- Applications need a bit of care! + -- They can match FunTy and TyConApp uTys _ (AppTy s1 t1) _ (AppTy s2 t2) = uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2 - -- Special case: converts a -> b to (->) a b -uTys _ (AppTy s1 t1) _ (FunTy fun2 arg2 _) +uTys _ (AppTy s1 t1) _ (FunTy fun2 arg2) = uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2 where - s2 = AppTy (TyConTy mkFunTyCon duffUsage) fun2 + -- Converts a -> b to (->) a b + s2 = TyConApp mkFunTyCon [fun2] t2 = arg2 -uTys _ (FunTy fun1 arg1 _) _ (AppTy s2 t2) - = uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2 - where - s1 = AppTy (TyConTy mkFunTyCon duffUsage) fun1 - t1 = arg1 +uTys _ (AppTy s1 t1) _ (TyConApp tc tys@(_:_)) + = case snocView tys of + (ts2, t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2 + where + -- Not efficient, but simple + s2 = TyConApp tc ts2 - -- Type constructors must match -uTys ps_ty1 (TyConTy con1 _) ps_ty2 (TyConTy con2 _) - = checkTc (con1 == con2) (unifyMisMatch ps_ty1 ps_ty2) +uTys ps1 s1 ps2 s2@(AppTy _ _) = uTys ps2 s2 ps1 s1 + -- Swap arguments if the App is in the second argument - -- Always expand synonyms (see notes at end) -uTys ps_ty1 (SynTy con1 args1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2 -uTys ps_ty1 ty1 ps_ty2 (SynTy con2 args2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2 + -- Not expecting for-alls in unification +#ifdef DEBUG +uTys ps_ty1 (ForAllTy _ _) ps_ty2 ty2 = panic "Unify.uTys:ForAllTy (1st arg)" +uTys ps_ty1 ty1 ps_ty2 (ForAllTy _ _) = panic "Unify.uTys:ForAllTy (2nd arg)" +#endif -- Anything else fails -uTys ps_ty1 ty1 ps_ty2 ty2 = failTc (unifyMisMatch ps_ty1 ps_ty2) +uTys ps_ty1 ty1 ps_ty2 ty2 = failWithTc (unifyMisMatch ps_ty1 ps_ty2) \end{code} Notes on synonyms @@ -208,7 +228,7 @@ uVar tv1 ps_ty2 ty2 other -> uUnboundVar tv1 maybe_ty1 ps_ty2 ty2 -- Expand synonyms -uUnboundVar tv1 maybe_ty1 ps_ty2 (SynTy _ _ ty2) +uUnboundVar tv1 maybe_ty1 ps_ty2 (SynTy _ ty2) = uUnboundVar tv1 maybe_ty1 ps_ty2 ty2 @@ -226,47 +246,44 @@ uUnboundVar tv1@(TyVar uniq1 kind1 name1 box1) -- ASSERT maybe_ty1 /= BoundTo | otherwise = tcReadTyVar tv2 `thenNF_Tc` \ maybe_ty2 -> - case (maybe_ty1, maybe_ty2) of - (_, BoundTo ty2') -> uUnboundVar tv1 maybe_ty1 ty2' ty2' - - (DontBind,DontBind) - -> failTc (unifyDontBindErr tv1 ps_ty2) + case maybe_ty2 of + BoundTo ty2' -> uUnboundVar tv1 maybe_ty1 ty2' ty2' - (UnBound, _) | kind2 `isSubKindOf` kind1 - -> tcWriteTyVar tv1 ty2 `thenNF_Tc_` returnTc () + UnBound | (kind1 == kind2 && not (maybeToBool name1)) -- Same kinds and tv1 is anonymous + -- so update tv1 + -> tcWriteTyVar tv1 ps_ty2 `thenNF_Tc_` returnTc () - (_, UnBound) | kind1 `isSubKindOf` kind2 - -> tcWriteTyVar tv2 (TyVarTy tv1) `thenNF_Tc_` returnTc () + | kind1 `hasMoreBoxityInfo` kind2 -- Update tv2 if possible + -> tcWriteTyVar tv2 (TyVarTy tv1) `thenNF_Tc_` returnTc () - other -> failTc (unifyKindErr tv1 ps_ty2) + | kind2 `hasMoreBoxityInfo` kind1 -- Update tv1 if possible + -> tcWriteTyVar tv1 ps_ty2 `thenNF_Tc_` returnTc () + + other -> failWithTc (unifyKindErr tv1 ps_ty2) -- Second one isn't a type variable uUnboundVar tv1@(TyVar uniq1 kind1 name1 box1) maybe_ty1 ps_ty2 non_var_ty2 - = case maybe_ty1 of - DontBind -> failTc (unifyDontBindErr tv1 ps_ty2) + | typeKind non_var_ty2 `hasMoreBoxityInfo` kind1 + = occur_check non_var_ty2 `thenTc_` + tcWriteTyVar tv1 ps_ty2 `thenNF_Tc_` + returnTc () - UnBound | getTypeKind non_var_ty2 `isSubKindOf` kind1 - -> occur_check non_var_ty2 `thenTc_` - tcWriteTyVar tv1 ps_ty2 `thenNF_Tc_` - returnTc () + | otherwise + = failWithTc (unifyKindErr tv1 ps_ty2) - other -> failTc (unifyKindErr tv1 ps_ty2) where - occur_check (TyVarTy tv2@(TyVar uniq2 _ _ box2)) + occur_check ty = mapTc occur_check_tv (tyVarSetToList (tyVarsOfType ty)) `thenTc_` + returnTc () + + occur_check_tv tv2@(TyVar uniq2 _ _ box2) | uniq1 == uniq2 -- Same tyvar; fail - = failTc (unifyOccurCheck tv1 ps_ty2) + = failWithTc (unifyOccurCheck tv1 ps_ty2) | otherwise -- A different tyvar = tcReadTyVar tv2 `thenNF_Tc` \ maybe_ty2 -> case maybe_ty2 of BoundTo ty2' -> occur_check ty2' other -> returnTc () - - occur_check (AppTy fun arg) = occur_check fun `thenTc_` occur_check arg - occur_check (FunTy fun arg _) = occur_check fun `thenTc_` occur_check arg - occur_check (TyConTy _ _) = returnTc () - occur_check (SynTy _ _ ty2) = occur_check ty2 - occur_check other = panic "Unexpected Dict or ForAll in occurCheck" \end{code} %************************************************************************ @@ -285,18 +302,168 @@ unifyFunTy ty@(TyVarTy tyvar) = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty -> case maybe_ty of BoundTo ty' -> unifyFunTy ty' + other -> unify_fun_ty_help ty - UnBound -> newTyVarTy mkTypeKind `thenNF_Tc` \ arg -> - newTyVarTy mkTypeKind `thenNF_Tc` \ res -> - tcWriteTyVar tyvar (mkFunTy arg res) `thenNF_Tc_` - returnTc (arg,res) +unifyFunTy ty + = case splitFunTy_maybe ty of + Just arg_and_res -> returnTc arg_and_res + Nothing -> unify_fun_ty_help ty - DontBind -> failTc (expectedFunErr ty) +unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification + = newTyVarTy mkTypeKind `thenNF_Tc` \ arg -> + newTyVarTy mkTypeKind `thenNF_Tc` \ res -> + unifyTauTy ty (mkFunTy arg res) `thenTc_` + returnTc (arg,res) +\end{code} -unifyFunTy other_ty - = case getFunTy_maybe other_ty of - Just arg_and_res -> returnTc arg_and_res - Nothing -> failTc (expectedFunErr other_ty) +\begin{code} +unifyListTy :: TcType s -- expected list type + -> TcM s (TcType s) -- list element type + +unifyListTy ty@(TyVarTy tyvar) + = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty -> + case maybe_ty of + BoundTo ty' -> unifyListTy ty' + other -> unify_list_ty_help ty + +unifyListTy ty + = case splitTyConApp_maybe ty of + Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty + other -> unify_list_ty_help ty + +unify_list_ty_help ty -- Revert to ordinary unification + = newTyVarTy mkBoxedTypeKind `thenNF_Tc` \ elt_ty -> + unifyTauTy ty (mkListTy elt_ty) `thenTc_` + returnTc elt_ty +\end{code} + +\begin{code} +unifyTupleTy :: Arity -> TcType s -> TcM s [TcType s] +unifyTupleTy arity ty@(TyVarTy tyvar) + = tcReadTyVar tyvar `thenNF_Tc` \ maybe_ty -> + case maybe_ty of + BoundTo 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 mkBoxedTypeKind) [1..arity] `thenNF_Tc` \ arg_tys -> + unifyTauTy ty (mkTupleTy arity arg_tys) `thenTc_` + returnTc arg_tys +\end{code} + +%************************************************************************ +%* * +\subsection{Unification wih a explicit substitution} +%* * +%************************************************************************ + +Unify types with an explicit substitution and no monad. + +\begin{code} +type Subst = TyVarEnv (GenType Bool) -- Not necessarily idempotent + +unifyTysX :: GenType Bool + -> GenType Bool + -> Maybe Subst +unifyTysX ty1 ty2 = uTysX ty1 ty2 (\s -> Just s) emptyTyVarEnv + +unifyTyListsX :: [GenType Bool] -> [GenType Bool] -> Maybe Subst +unifyTyListsX tys1 tys2 = uTyListsX tys1 tys2 (\s -> Just s) emptyTyVarEnv + + +uTysX :: GenType Bool + -> GenType Bool + -> (Subst -> Maybe Subst) + -> Subst + -> Maybe Subst + +uTysX (SynTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst +uTysX ty1 (SynTy _ ty2) k subst = uTysX ty1 ty2 k subst + + -- Variables; go for uVar +uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst + | tyvar1 == tyvar2 + = k subst +uTysX (TyVarTy tyvar1) ty2 k subst + | tyVarFlexi tyvar1 + = uVarX tyvar1 ty2 k subst +uTysX ty1 (TyVarTy tyvar2) k subst + | tyVarFlexi tyvar2 + = uVarX tyvar2 ty1 k subst + + -- Functions; just check the two parts +uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst + = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst + + -- Type constructors must match +uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst + | (con1 == con2 && length tys1 == length tys2) + = uTyListsX tys1 tys2 k subst + + -- Applications need a bit of care! + -- They can match FunTy and TyConApp +uTysX (AppTy s1 t1) (AppTy s2 t2) k subst + = uTysX s1 s2 (uTysX t1 t2 k) subst + +uTysX (AppTy s1 t1) (FunTy fun2 arg2) k subst + = uTysX s1 s2 (uTysX t1 t2 k) subst + where + -- Converts a -> b to (->) a b + s2 = TyConApp mkFunTyCon [fun2] + t2 = arg2 + +uTysX (AppTy s1 t1) (TyConApp tc tys@(_:_)) k subst + = case snocView tys of + (ts2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst + where + -- Not efficient, but simple + s2 = TyConApp tc ts2 + +uTysX s1 s2@(AppTy _ _) k subst = uTysX s2 s1 k subst + -- Swap arguments if the App is in the second argument + + -- Not expecting for-alls in unification +#ifdef DEBUG +uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)" +uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)" +#endif + + -- Anything else fails +uTysX ty1 ty2 k subst = Nothing + + +uTyListsX [] [] k subst = k subst +uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst +uTyListsX tys1 tys2 k subst = Nothing -- Fail if the lists are different lengths +\end{code} + +\begin{code} +-- Invariant: tv1 is a unifiable variable +uVarX tv1 ty2 k subst + = case lookupTyVarEnv subst tv1 of + Just ty1 -> -- Already bound + uTysX ty1 ty2 k subst + + Nothing -- Not already bound + | typeKind ty2 `hasMoreBoxityInfo` tyVarKind tv1 + && occur_check_ok ty2 + -> -- No kind mismatch nor occur check + k (addToTyVarEnv subst tv1 ty2) + + | otherwise -> Nothing -- Fail if kind mis-match or occur check + where + occur_check_ok ty = all occur_check_ok_tv (tyVarSetToList (tyVarsOfType ty)) + occur_check_ok_tv tv | tv1 == tv = False + | otherwise = case lookupTyVarEnv subst tv of + Nothing -> True + Just ty -> occur_check_ok ty \end{code} @@ -310,38 +477,28 @@ Errors ~~~~~~ \begin{code} -unifyCtxt ty1 ty2 +unifyCtxt ty1 ty2 -- ty1 expected, ty2 inferred = zonkTcType ty1 `thenNF_Tc` \ ty1' -> zonkTcType ty2 `thenNF_Tc` \ ty2' -> returnNF_Tc (err ty1' ty2') where - err ty1' ty2' sty = ppAboves [ - ppCat [ppStr "When matching:", ppr sty ty1'], - ppCat [ppStr " against:", ppr sty ty2'] + err ty1' ty2' = vcat [ + hsep [ptext SLIT("Expected:"), ppr ty1'], + hsep [ptext SLIT("Inferred:"), ppr ty2'] ] -unifyMisMatch ty1 ty2 sty - = ppHang (ppStr "Couldn't match the type") - 4 (ppSep [ppr sty ty1, ppStr "against", ppr sty ty2]) - -expectedFunErr ty sty - = ppHang (ppStr "Function type expected, but found the type") - 4 (ppr sty ty) - -unifyKindErr tyvar ty sty - = ppHang (ppStr "Compiler bug: kind mis-match between") - 4 (ppSep [ppr sty tyvar, ppLparen, ppr sty (getTyVarKind tyvar), ppRparen, - ppStr "and", - ppr sty ty, ppLparen, ppr sty (getTypeKind ty), ppRparen]) - -unifyDontBindErr tyvar ty sty - = ppHang (ppStr "Couldn't match the *signature/existential* type variable") - 4 (ppSep [ppr sty tyvar, - ppStr "with the type", - ppr sty ty]) - -unifyOccurCheck tyvar ty sty - = ppHang (ppStr "Cannot construct the infinite type (occur check)") - 4 (ppSep [ppr sty tyvar, ppStr "=", ppr sty ty]) +unifyMisMatch ty1 ty2 + = hang (ptext SLIT("Couldn't match the type")) + 4 (sep [quotes (ppr ty1), ptext SLIT("against"), quotes (ppr ty2)]) + +unifyKindErr tyvar ty + = hang (ptext SLIT("Kind mis-match between")) + 4 (sep [quotes (hsep [ppr tyvar, ptext SLIT("::"), ppr (tyVarKind tyvar)]), + ptext SLIT("and"), + quotes (hsep [ppr ty, ptext SLIT("::"), ppr (typeKind ty)])]) + +unifyOccurCheck tyvar ty + = hang (ptext SLIT("Occurs check: cannot construct the infinite type:")) + 8 (sep [ppr tyvar, char '=', ppr ty]) \end{code}