From 9fe510d19e48f1cefdf3591c8669cd74a63867b7 Mon Sep 17 00:00:00 2001 From: simonpj Date: Mon, 11 Jul 2005 09:54:44 +0000 Subject: [PATCH] [project @ 2005-07-11 09:54:43 by simonpj] Improve the error message from unifyFunTys. Previously we got a really horrible message from this: t = ((\Just x -> x) :: Maybe a -> a) (Just 1) Try.hs:1:6: Couldn't match the rigid variable `a' against `t -> t1' Expected type: a Inferred type: t -> t1 Now it's much better: Try.hs:14:6: The lambda expression `\ Just x -> ...' has two arguments, but its type `Maybe a -> a' has only one In the expression: (\ Just x -> x) :: Maybe a -> a tcfail140 tests some cases --- ghc/compiler/hsSyn/HsExpr.lhs | 6 +- ghc/compiler/typecheck/TcExpr.lhs | 34 ++++++--- ghc/compiler/typecheck/TcMType.lhs | 2 +- ghc/compiler/typecheck/TcMatches.lhs | 8 +-- ghc/compiler/typecheck/TcUnify.lhs | 125 ++++++++++++++++++++++++++-------- 5 files changed, 130 insertions(+), 45 deletions(-) diff --git a/ghc/compiler/hsSyn/HsExpr.lhs b/ghc/compiler/hsSyn/HsExpr.lhs index 3f06196..2f4ab1b 100644 --- a/ghc/compiler/hsSyn/HsExpr.lhs +++ b/ghc/compiler/hsSyn/HsExpr.lhs @@ -319,7 +319,7 @@ ppr_expr (SectionL expr op) pp_prefixly = hang (hsep [text " \\ x_ ->", ppr op]) 4 (hsep [pp_expr, ptext SLIT("x_ )")]) - pp_infixly v = parens (sep [pp_expr, ppr v]) + pp_infixly v = parens (sep [pp_expr, pprInfix v]) ppr_expr (SectionR op expr) = case unLoc op of @@ -331,7 +331,7 @@ ppr_expr (SectionR op expr) pp_prefixly = hang (hsep [text "( \\ x_ ->", ppr op, ptext SLIT("x_")]) 4 ((<>) pp_expr rparen) pp_infixly v - = parens (sep [ppr v, pp_expr]) + = parens (sep [pprInfix v, pp_expr]) ppr_expr (HsLam matches) = pprMatches LambdaExpr matches @@ -647,7 +647,7 @@ pprMatch :: OutputableBndr id => HsMatchContext id -> Match id -> SDoc pprMatch ctxt (Match pats maybe_ty grhss) = pp_name ctxt <+> sep [sep (map ppr pats), ppr_maybe_ty, - nest 2 (pprGRHSs ctxt grhss)] + nest 2 (pprDeeper (pprGRHSs ctxt grhss))] where pp_name (FunRhs fun) = ppr fun -- Not pprBndr; the AbsBinds will -- have printed the signature diff --git a/ghc/compiler/typecheck/TcExpr.lhs b/ghc/compiler/typecheck/TcExpr.lhs index 4cdf5b5..ebe95e4 100644 --- a/ghc/compiler/typecheck/TcExpr.lhs +++ b/ghc/compiler/typecheck/TcExpr.lhs @@ -240,7 +240,7 @@ a type error will occur if they aren't. tcExpr in_expr@(SectionL arg1 op) res_ty = tcInferRho op `thenM` \ (op', op_ty) -> - unifyFunTys 2 op_ty {- two args -} `thenM` \ ([arg1_ty, arg2_ty], op_res_ty) -> + unifyInfixTy op in_expr op_ty `thenM` \ ([arg1_ty, arg2_ty], op_res_ty) -> tcArg op (arg1, arg1_ty, 1) `thenM` \ arg1' -> addErrCtxt (exprCtxt in_expr) $ tcSubExp res_ty (mkFunTy arg2_ty op_res_ty) `thenM` \ co_fn -> @@ -251,7 +251,7 @@ tcExpr in_expr@(SectionL arg1 op) res_ty tcExpr in_expr@(SectionR op arg2) res_ty = tcInferRho op `thenM` \ (op', op_ty) -> - unifyFunTys 2 op_ty {- two args -} `thenM` \ ([arg1_ty, arg2_ty], op_res_ty) -> + unifyInfixTy op in_expr op_ty `thenM` \ ([arg1_ty, arg2_ty], op_res_ty) -> tcArg op (arg2, arg2_ty, 2) `thenM` \ arg2' -> addErrCtxt (exprCtxt in_expr) $ tcSubExp res_ty (mkFunTy arg1_ty op_res_ty) `thenM` \ co_fn -> @@ -261,7 +261,7 @@ tcExpr in_expr@(SectionR op arg2) res_ty tcExpr in_expr@(OpApp arg1 op fix arg2) res_ty = tcInferRho op `thenM` \ (op', op_ty) -> - unifyFunTys 2 op_ty {- two args -} `thenM` \ ([arg1_ty, arg2_ty], op_res_ty) -> + unifyInfixTy op in_expr op_ty `thenM` \ ([arg1_ty, arg2_ty], op_res_ty) -> tcArg op (arg1, arg1_ty, 1) `thenM` \ arg1' -> tcArg op (arg2, arg2_ty, 2) `thenM` \ arg2' -> addErrCtxt (exprCtxt in_expr) $ @@ -628,14 +628,16 @@ tcApp (L _ (HsApp e1 e2)) args res_ty = tcApp e1 (e2:args) res_ty -- Accumulate the arguments tcApp fun args res_ty - = do { (fun', fun_tvs, fun_tau) <- tcFun fun -- Type-check the function + = do { let n_args = length args + ; (fun', fun_tvs, fun_tau) <- tcFun fun -- Type-check the function -- Extract its argument types ; (expected_arg_tys, actual_res_ty) - <- addErrCtxt (wrongArgsCtxt "too many" fun args) $ do - { traceTc (text "tcApp" <+> (ppr fun $$ ppr fun_tau)) - ; unifyFunTys (length args) fun_tau } - + <- do { traceTc (text "tcApp" <+> (ppr fun $$ ppr fun_tau)) + ; let msg = sep [ptext SLIT("The function") <+> quotes (ppr fun), + ptext SLIT("is applied to") + <+> speakN n_args <+> ptext SLIT("arguments")] + ; unifyFunTys msg n_args fun_tau } ; case res_ty of Check _ -> do -- Connect to result type first @@ -738,6 +740,20 @@ checkArgsCtxt fun args (Check expected_res_ty) actual_res_ty tidy_env | otherwise = appCtxt fun args in returnM (env2, message) + +---------------- +unifyInfixTy :: LHsExpr Name -> HsExpr Name -> TcType + -> TcM ([TcType], TcType) +-- This wrapper just prepares the error message for unifyFunTys +unifyInfixTy op expr op_ty + = unifyFunTys msg 2 op_ty + where + msg = sep [herald <+> quotes (ppr expr), + ptext SLIT("requires") <+> quotes (ppr op) + <+> ptext SLIT("to take two arguments")] + herald = case expr of + OpApp _ _ _ _ -> ptext SLIT("The infix expression") + other -> ptext SLIT("The operator section") \end{code} @@ -934,6 +950,7 @@ tcRecordBinds tycon ty_args rbinds tyConFieldType :: TyCon -> FieldLabel -> Type tyConFieldType tycon field_lbl = case [ty | (f,ty,_) <- tyConFields tycon, f == field_lbl] of + [] -> panic "tyConFieldType" (ty:other) -> ASSERT( null other) ty -- This lookup and assertion will surely succeed, because -- we check that the fields are indeed record selectors @@ -998,6 +1015,7 @@ tcCheckRhos (expr:exprs) (ty:tys) = tcCheckRho expr ty `thenM` \ expr' -> tcCheckRhos exprs tys `thenM` \ exprs' -> returnM (expr':exprs') +tcCheckRhos exprs tys = pprPanic "tcCheckRhos" (ppr exprs $$ ppr tys) \end{code} diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs index d8e4c0e..a2dae5e 100644 --- a/ghc/compiler/typecheck/TcMType.lhs +++ b/ghc/compiler/typecheck/TcMType.lhs @@ -294,7 +294,7 @@ We return Nothing iff the original box was unbound. \begin{code} data LookupTyVarResult -- The result of a lookupTcTyVar call - = DoneTv TcTyVarDetails + = DoneTv TcTyVarDetails -- Unrefined SkolemTv or virgin MetaTv/SigSkolTv | IndirectTv Bool TcType -- True => This is a non-wobbly type refinement, -- gotten from GADT match unification diff --git a/ghc/compiler/typecheck/TcMatches.lhs b/ghc/compiler/typecheck/TcMatches.lhs index 5aeb1dd..d7cbd78 100644 --- a/ghc/compiler/typecheck/TcMatches.lhs +++ b/ghc/compiler/typecheck/TcMatches.lhs @@ -88,12 +88,12 @@ tcMatchesFun fun_name matches exp_ty -- The point is that if expected_y is a "hole", we want -- to make pat_tys and rhs_ty as "holes" too. ; exp_ty' <- zapExpectedBranches matches exp_ty - ; subFunTys matches exp_ty' $ \ pat_tys rhs_ty -> + ; subFunTys ctxt matches exp_ty' $ \ pat_tys rhs_ty -> tcMatches match_ctxt pat_tys rhs_ty matches } where - match_ctxt = MC { mc_what = FunRhs fun_name, - mc_body = tcMonoExpr } + ctxt = FunRhs fun_name + match_ctxt = MC { mc_what = ctxt, mc_body = tcMonoExpr } \end{code} @tcMatchesCase@ doesn't do the argument-count check because the @@ -112,7 +112,7 @@ tcMatchesCase ctxt scrut_ty matches exp_ty tcMatchLambda :: MatchGroup Name -> Expected TcRhoType -> TcM (MatchGroup TcId) tcMatchLambda match exp_ty -- One branch so no unifyBranches needed - = subFunTys match exp_ty $ \ pat_tys rhs_ty -> + = subFunTys LambdaExpr match exp_ty $ \ pat_tys rhs_ty -> tcMatches match_ctxt pat_tys rhs_ty match where match_ctxt = MC { mc_what = LambdaExpr, diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index c11ae24..0e5052a 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -26,7 +26,8 @@ module TcUnify ( #include "HsVersions.h" -import HsSyn ( HsExpr(..) , MatchGroup(..), hsLMatchPats ) +import HsSyn ( HsExpr(..) , MatchGroup(..), HsMatchContext(..), + hsLMatchPats, pprMatches, pprMatchContext ) import TcHsSyn ( mkHsLet, mkHsDictLam, ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) ) import TypeRep ( Type(..), PredType(..), TyNote(..) ) @@ -35,7 +36,7 @@ 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, + pprTcTyVar, isTauTy, isSigmaTy, mkFunTy, mkFunTys, mkTyConApp, tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy, @@ -59,7 +60,7 @@ 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") <+> speakN n_pats <+> ptext SLIT("arguments") + LambdaExpr -> sep [ ptext SLIT("The lambda expression") + <+> quotes (pprSetDepth 1 $ pprMatches ctxt group), + -- The pprSetDepth makes the abstraction print briefly + ptext SLIT("has") <+> speakN 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,43 @@ 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), + 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 +251,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} @@ -501,11 +559,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 } ----------------------------------- @@ -514,6 +572,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} -- 1.7.10.4