X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcUnify.lhs;h=97487ce6b24c3599a9e50f12224dfbc2ab8e977f;hb=f2e730f34ab0134391c88fe58f9f9e94b736da91;hp=b080809575b4ac2c626cd388d745171fe5224b88;hpb=d551dbfef0b710f5ede21ee0c54ee7e80dd53b64;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index b080809..97487ce 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -26,9 +26,9 @@ module TcUnify ( #include "HsVersions.h" --- gaw 2004 -import HsSyn ( HsExpr(..) , MatchGroup(..), hsLMatchPats ) -import TcHsSyn ( mkHsLet, mkHsDictLam, +import HsSyn ( HsExpr(..) , MatchGroup(..), HsMatchContext(..), + hsLMatchPats, pprMatches, pprMatchContext ) +import TcHsSyn ( mkHsDictLet, mkHsDictLam, ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) ) import TypeRep ( Type(..), PredType(..), TyNote(..) ) @@ -36,12 +36,12 @@ import TcRnMonad -- TcType, amongst others import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType, TcTyVarSet, TcThetaType, Expected(..), TcTyVarDetails(..), SkolemInfo( GenSkol ), MetaDetails(..), - pprTcTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp, - tcSplitAppTy_maybe, tcSplitTyConApp_maybe, - tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, + pprTcTyVar, isTauTy, isSigmaTy, mkFunTy, mkFunTys, mkTyConApp, + tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tcEqType, + tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, isMetaTyVar, typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy, tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars, - pprType, tidySkolemTyVar, isSkolemTyVar ) + pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar ) import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind, openTypeKind, liftedTypeKind, mkArrowKind, isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind, @@ -52,14 +52,15 @@ import TcMType ( condLookupTcTyVar, LookupTyVarResult(..), newTyFlexiVarTy, zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV, readKindVar, writeKindVar ) import TcSimplify ( tcSimplifyCheck ) +import TcIface ( checkWiredInTyCon ) import TcEnv ( tcGetGlobalTyVars, findGlobals ) -import TyCon ( TyCon, tyConArity, tyConTyVars ) +import TyCon ( TyCon, tyConArity, tyConTyVars, isFunTyCon ) import TysWiredIn ( listTyCon ) import Id ( Id, mkSysLocal ) import Var ( Var, varName, tyVarKind ) import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems ) import VarEnv -import Name ( isSystemName, mkSysTvName ) +import Name ( Name, isSystemName, mkSysTvName ) import ErrUtils ( Message ) import SrcLoc ( noLoc ) import BasicTypes ( Arity ) @@ -150,12 +151,13 @@ creation of type variables. type variables, so we should create new ordinary type variables \begin{code} -subFunTys :: MatchGroup name +subFunTys :: HsMatchContext Name + -> MatchGroup Name -> Expected TcRhoType -- Fail if ty isn't a function type -> ([Expected TcRhoType] -> Expected TcRhoType -> TcM a) -> TcM a -subFunTys (MatchGroup (match:null_matches) _) (Infer hole) thing_inside +subFunTys ctxt (MatchGroup (match:null_matches) _) (Infer hole) thing_inside = -- This is the interesting case ASSERT( null null_matches ) do { pat_holes <- mapM (\ _ -> newHole) (hsLMatchPats match) @@ -174,13 +176,24 @@ subFunTys (MatchGroup (match:null_matches) _) (Infer hole) thing_inside -- And return the answer ; return res } -subFunTys (MatchGroup (match:matches) _) (Check ty) thing_inside - = ASSERT( all ((== length (hsLMatchPats match)) . length . hsLMatchPats) matches ) +subFunTys ctxt group@(MatchGroup (match:matches) _) (Check ty) thing_inside + = ASSERT( all ((== n_pats) . length . hsLMatchPats) matches ) -- Assertion just checks that all the matches have the same number of pats - do { (pat_tys, res_ty) <- unifyFunTys (length (hsLMatchPats match)) ty + do { (pat_tys, res_ty) <- unifyFunTys msg n_pats ty ; thing_inside (map Check pat_tys) (Check res_ty) } - -unifyFunTys :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType) + where + n_pats = length (hsLMatchPats match) + msg = case ctxt of + FunRhs fun -> ptext SLIT("The equation(s) for") <+> quotes (ppr fun) + <+> ptext SLIT("have") <+> speakNOf n_pats (ptext SLIT("argument")) + LambdaExpr -> sep [ ptext SLIT("The lambda expression") + <+> quotes (pprSetDepth 1 $ pprMatches ctxt group), + -- The pprSetDepth makes the abstraction print briefly + ptext SLIT("has") <+> speakNOf n_pats (ptext SLIT("arguments"))] + other -> pprPanic "subFunTys" (pprMatchContext ctxt) + + +unifyFunTys :: SDoc -> Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType) -- Fail if ty isn't a function type, otherwise return arg and result types -- The result types are guaranteed wobbly if the argument is wobbly -- @@ -193,12 +206,44 @@ unifyFunTys :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType) -- -- (b) GADTs: if the argument is not wobbly we do not want the result to be -unifyFunTys arity ty = unify_fun_ty True arity ty +{- + Error messages from unifyFunTys + The first line is passed in as error_herald + + The abstraction `\Just 1 -> ...' has two arguments + but its type `Maybe a -> a' has only one + + The equation(s) for `f' have two arguments + but its type `Maybe a -> a' has only one + + The section `(f 3)' requires 'f' to take two arguments + but its type `Int -> Int' has only one + + The function 'f' is applied to two arguments + but its type `Int -> Int' has only one +-} + +unifyFunTys error_herald arity ty + -- error_herald is the whole first line of the error message above + = do { (ok, args, res) <- unify_fun_ty True arity ty + ; if ok then return (args, res) + else failWithTc (mk_msg (length args)) } + where + mk_msg n_actual + = error_herald <> comma $$ + sep [ptext SLIT("but its type") <+> quotes (pprType ty), + if n_actual == 0 then ptext SLIT("has none") + else ptext SLIT("has only") <+> speakN n_actual] + +unify_fun_ty :: Bool -> Arity -> TcRhoType + -> TcM (Bool, -- Arity satisfied? + [TcSigmaType], -- Arg types found; length <= arity + TcRhoType) -- Result type unify_fun_ty use_refinement arity ty | arity == 0 = do { res_ty <- wobblify use_refinement ty - ; return ([], ty) } + ; return (True, [], ty) } unify_fun_ty use_refinement arity (NoteTy _ ty) = unify_fun_ty use_refinement arity ty @@ -207,24 +252,38 @@ unify_fun_ty use_refinement arity ty@(TyVarTy tv) = do { details <- condLookupTcTyVar use_refinement tv ; case details of IndirectTv use' ty' -> unify_fun_ty use' arity ty' - other -> unify_fun_help arity ty + DoneTv (MetaTv ref) -> ASSERT( liftedTypeKind `isSubKind` tyVarKind tv ) + -- The argument to unifyFunTys is always a type + -- Occurs check can't happen, of course + do { args <- mappM newTyFlexiVarTy (replicate arity argTypeKind) + ; res <- newTyFlexiVarTy openTypeKind + ; writeMutVar ref (Indirect (mkFunTys args res)) + ; return (True, args, res) } + DoneTv skol -> return (False, [], ty) } unify_fun_ty use_refinement arity ty - = case tcSplitFunTy_maybe ty of - Just (arg,res) -> do { arg' <- wobblify use_refinement arg - ; (args', res') <- unify_fun_ty use_refinement (arity-1) res - ; return (arg':args', res') } - - Nothing -> unify_fun_help arity ty - -- Usually an error, but ty could be (a Int Bool), which can match - -unify_fun_help :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType) -unify_fun_help arity ty - = do { args <- mappM newTyFlexiVarTy (replicate arity argTypeKind) - ; res <- newTyFlexiVarTy openTypeKind - ; unifyTauTy ty (mkFunTys args res) - ; return (args, res) } + | Just (arg,res) <- tcSplitFunTy_maybe ty + = do { arg' <- wobblify use_refinement arg + ; (ok, args', res') <- unify_fun_ty use_refinement (arity-1) res + ; return (ok, arg':args', res') } + +unify_fun_ty use_refinement arity ty +-- Common cases are all done by now +-- At this point we usually have an error, but ty could +-- be (a Int Bool), or (a Bool), which can match +-- So just use the unifier. But catch any error so we just +-- return the success/fail boolean + = do { arg <- newTyFlexiVarTy argTypeKind + ; res <- newTyFlexiVarTy openTypeKind + ; let fun_ty = mkFunTy arg res + ; (_, mb_unit) <- tryTc (uTys True ty ty True fun_ty fun_ty) + ; case mb_unit of { + Nothing -> return (False, [], ty) ; + Just _ -> + do { (ok, args', res') <- unify_fun_ty use_refinement (arity-1) res + ; return (ok, arg:args', res') + } } } \end{code} \begin{code} @@ -233,12 +292,18 @@ zapToTyConApp :: TyCon -- T :: k1 -> ... -> kn -> * -> Expected TcSigmaType -- Expected type (T a b c) -> TcM [TcType] -- Element types, a b c -- Insists that the Expected type is not a forall-type - + -- It's used for wired-in tycons, so we call checkWiredInTyCOn + -- Precondition: never called with FunTyCon zapToTyConApp tc (Check ty) - = unifyTyConApp tc ty -- NB: fails for a forall-type + = ASSERT( not (isFunTyCon tc) ) -- Never called with FunTyCon + do { checkWiredInTyCon tc ; unifyTyConApp tc ty } -- NB: fails for a forall-type + zapToTyConApp tc (Infer hole) - = do { (tc_app, elt_tys) <- newTyConApp tc + = do { (_, elt_tys, _) <- tcInstTyVars (tyConTyVars tc) + ; let tc_app = mkTyConApp tc elt_tys ; writeMutVar hole tc_app + ; traceTc (text "zap" <+> ppr tc) + ; checkWiredInTyCon tc ; return elt_tys } zapToListTy :: Expected TcType -> TcM TcType -- Special case for lists @@ -247,40 +312,48 @@ zapToListTy exp_ty = do { [elt_ty] <- zapToTyConApp listTyCon exp_ty ---------------------- unifyTyConApp :: TyCon -> TcType -> TcM [TcType] -unifyTyConApp tc ty = unify_tc_app True tc ty - -- Add a boolean flag to remember whether to use - -- the type refinement or not +unifyTyConApp tc ty + = ASSERT( not (isFunTyCon tc) ) -- Never called with FunTyCon + unify_tc_app (tyConArity tc) True tc ty + -- Add a boolean flag to remember whether + -- to use the type refinement or not unifyListTy :: TcType -> TcM TcType -- Special case for lists unifyListTy exp_ty = do { [elt_ty] <- unifyTyConApp listTyCon exp_ty ; return elt_ty } ---------- -unify_tc_app use_refinement tc (NoteTy _ ty) - = unify_tc_app use_refinement tc ty - -unify_tc_app use_refinement tc ty@(TyVarTy tyvar) - = do { details <- condLookupTcTyVar use_refinement tyvar +unify_tc_app n_args use_refinement tc (NoteTy _ ty) + = unify_tc_app n_args use_refinement tc ty + +unify_tc_app n_args use_refinement tc (TyConApp tycon arg_tys) + | tycon == tc + = ASSERT( n_args == length arg_tys ) -- ty::* + mapM (wobblify use_refinement) arg_tys + +unify_tc_app n_args use_refinement tc (AppTy fun_ty arg_ty) + = do { arg_ty' <- wobblify use_refinement arg_ty + ; arg_tys <- unify_tc_app (n_args - 1) use_refinement tc fun_ty + ; return (arg_tys ++ [arg_ty']) } + +unify_tc_app n_args use_refinement tc ty@(TyVarTy tyvar) + = do { traceTc (text "unify_tc_app: tyvar" <+> pprTcTyVar tyvar) + ; details <- condLookupTcTyVar use_refinement tyvar ; case details of - IndirectTv use' ty' -> unify_tc_app use' tc ty' - other -> unify_tc_app_help tc ty + IndirectTv use' ty' -> unify_tc_app n_args use' tc ty' + other -> unify_tc_app_help n_args tc ty } -unify_tc_app use_refinement tc ty - | Just (tycon, arg_tys) <- tcSplitTyConApp_maybe ty, - tycon == tc - = ASSERT( tyConArity tycon == length arg_tys ) -- ty::* - mapM (wobblify use_refinement) arg_tys - -unify_tc_app use_refinement tc ty = unify_tc_app_help tc ty +unify_tc_app n_args use_refinement tc ty = unify_tc_app_help n_args tc ty -unify_tc_app_help tc ty -- Revert to ordinary unification - = do { (tc_app, arg_tys) <- newTyConApp tc +unify_tc_app_help n_args tc ty -- Revert to ordinary unification + = do { (_, elt_tys, _) <- tcInstTyVars (take n_args (tyConTyVars tc)) + ; let tc_app = mkTyConApp tc elt_tys ; if not (isTauTy ty) then -- Can happen if we call zapToTyConApp tc (forall a. ty) unifyMisMatch ty tc_app else do { unifyTauTy ty tc_app - ; returnM arg_tys } } + ; returnM elt_tys } } ---------------------- @@ -320,17 +393,16 @@ wobblify :: Bool -- True <=> don't wobblify -> TcM TcTauType -- Return a wobbly type. At the moment we do that by -- allocating a fresh meta type variable. -wobblify True ty = return ty +wobblify True ty = return ty -- Don't wobblify + +wobblify False ty@(TyVarTy tv) + | isMetaTyVar tv = return ty -- Already wobbly + wobblify False ty = do { uniq <- newUnique ; tv <- newMetaTyVar (mkSysTvName uniq FSLIT("w")) (typeKind ty) (Indirect ty) ; return (mkTyVarTy tv) } - ----------------------- -newTyConApp :: TyCon -> TcM (TcTauType, [TcTauType]) -newTyConApp tc = do { (tvs, args, _) <- tcInstTyVars (tyConTyVars tc) - ; return (mkTyConApp tc args, args) } \end{code} @@ -382,20 +454,31 @@ tcSubPat :: TcSigmaType -- Pattern type signature -- See Note [Pattern coercions] in TcPat -- However, we can't call unify directly, because both types might be -- polymorphic; hence the call to tcSub, followed by a check for --- the identity coercion +-- equal types. (We can't just check for the identity coercion, because +-- in the polymorphic case we might get back something eta-equivalent to +-- the identity coercion, but that's not easy to tell.) tcSubPat sig_ty (Infer hole) = do { sig_ty' <- zonkTcType sig_ty ; writeMutVar hole sig_ty' -- See notes with tcSubExp above ; return () } +-- This tcSub followed by tcEqType checks for identical types +-- It'd be done more neatly by augmenting the unifier to deal with +-- (identically shaped) for-all types. + tcSubPat sig_ty (Check exp_ty) = do { co_fn <- tcSub sig_ty exp_ty - - ; if isIdCoercion co_fn then + ; sig_ty' <- zonkTcType sig_ty + ; exp_ty' <- zonkTcType exp_ty + ; if tcEqType sig_ty' exp_ty' then return () - else - unifyMisMatch sig_ty exp_ty } + else do + { (env, msg) <- misMatchMsg sig_ty' exp_ty' + ; failWithTcM (env, msg $$ extra) } } + where + extra | isTauTy sig_ty = empty + | otherwise = ptext SLIT("Polymorphic types must match exactly in patterns") \end{code} @@ -498,11 +581,11 @@ tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res) -- I'm not quite sure what to do about this! tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ act_ty - = do { ([act_arg], act_res) <- unifyFunTys 1 act_ty + = do { (act_arg, act_res) <- unify_fun act_ty ; tcSub_fun exp_arg exp_res act_arg act_res } tc_sub _ exp_ty act_sty act_ty@(FunTy act_arg act_res) - = do { ([exp_arg], exp_res) <- unifyFunTys 1 exp_ty + = do { (exp_arg, exp_res) <- unify_fun exp_ty ; tcSub_fun exp_arg exp_res act_arg act_res } ----------------------------------- @@ -511,6 +594,15 @@ tc_sub _ exp_ty act_sty act_ty@(FunTy act_arg act_res) tc_sub exp_sty expected_ty act_sty actual_ty = uTys True exp_sty expected_ty True act_sty actual_ty `thenM_` returnM idCoercion + +----------------------------------- +-- A helper to make a function type match +-- The error message isn't very good, but that's a problem with +-- all of this subsumption code +unify_fun ty + = do { (ok, args, res) <- unify_fun_ty True 1 ty + ; if ok then return (head args, res) + else failWithTc (ptext SLIT("Expecting a function type, but found") <+> quotes (ppr ty))} \end{code} \begin{code} @@ -599,7 +691,7 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall -- It's a bit out of place here, but using AbsBind involves inventing -- a couple of new names which seems worse. dict_ids = map instToId dicts - co_fn e = TyLam forall_tvs (mkHsDictLam dict_ids (mkHsLet inst_binds (noLoc e))) + co_fn e = TyLam forall_tvs (mkHsDictLam dict_ids (mkHsDictLet inst_binds (noLoc e))) ; returnM (mkCoercion co_fn, result) } where free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs @@ -1179,12 +1271,15 @@ unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 infer pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2) unifyMisMatch ty1 ty2 + = do { (env, msg) <- misMatchMsg ty1 ty2 + ; failWithTcM (env, msg) } + +misMatchMsg ty1 ty2 = do { (env1, pp1, extra1) <- ppr_ty emptyTidyEnv ty1 ; (env2, pp2, extra2) <- ppr_ty env1 ty2 - ; let msg = sep [sep [ptext SLIT("Couldn't match") <+> pp1, nest 7 (ptext SLIT("against") <+> pp2)], - nest 2 extra1, nest 2 extra2] - in - failWithTcM (env2, msg) } + ; return (env2, sep [sep [ptext SLIT("Couldn't match") <+> pp1, + nest 7 (ptext SLIT("against") <+> pp2)], + nest 2 extra1, nest 2 extra2]) } ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc) ppr_ty env ty @@ -1237,9 +1332,9 @@ checkExpectedKind ty act_kind exp_kind | act_kind `isSubKind` exp_kind -- Short cut for a very common case = returnM () | otherwise - = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) -> + = tryTc (unifyKind exp_kind act_kind) `thenM` \ (_errs, mb_r) -> case mb_r of { - Just _ -> returnM () ; -- Unification succeeded + Just r -> returnM () ; -- Unification succeeded Nothing -> -- So there's definitely an error @@ -1251,6 +1346,9 @@ checkExpectedKind ty act_kind exp_kind (act_as, _) = splitKindFunTys act_kind n_exp_as = length exp_as n_act_as = length act_as + + (env1, tidy_exp_kind) = tidyKind emptyTidyEnv 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") @@ -1266,11 +1364,14 @@ checkExpectedKind ty act_kind exp_kind <+> ptext SLIT("is lifted") | otherwise -- E.g. Monad [Int] - = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma, - ptext SLIT("but") <+> quotes (ppr ty) <+> - ptext SLIT("has kind") <+> quotes (pprKind act_kind)] + = 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)] in - failWithTc (ptext SLIT("Kind error:") <+> err) + failWithTcM (env2, err $$ more_info) } \end{code}