+\subsection[Unify-context]{Errors and contexts}
+%* *
+%************************************************************************
+
+Errors
+~~~~~~
+
+\begin{code}
+unifyCtxt act_ty exp_ty tidy_env
+ = do { act_ty' <- zonkTcType act_ty
+ ; exp_ty' <- zonkTcType exp_ty
+ ; let (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
+ (env2, act_ty'') = tidyOpenType env1 act_ty'
+ ; return (env2, mkExpectedActualMsg act_ty'' exp_ty'') }
+
+----------------
+mkExpectedActualMsg act_ty exp_ty
+ = nest 2 (vcat [ text "Expected type" <> colon <+> ppr exp_ty,
+ text "Inferred type" <> colon <+> ppr act_ty ])
+
+----------------
+-- If an error happens we try to figure out whether the function
+-- function has been given too many or too few arguments, and say so.
+checkFunResCtxt fun actual_res_ty expected_res_ty tidy_env
+ = do { exp_ty' <- zonkTcType expected_res_ty
+ ; act_ty' <- zonkTcType actual_res_ty
+ ; let
+ (env1, exp_ty'') = tidyOpenType tidy_env exp_ty'
+ (env2, act_ty'') = tidyOpenType env1 act_ty'
+ (exp_args, _) = tcSplitFunTys exp_ty''
+ (act_args, _) = tcSplitFunTys act_ty''
+
+ len_act_args = length act_args
+ len_exp_args = length exp_args
+
+ message | len_exp_args < len_act_args = wrongArgsCtxt "too few" fun
+ | len_exp_args > len_act_args = wrongArgsCtxt "too many" fun
+ | otherwise = mkExpectedActualMsg act_ty'' exp_ty''
+ ; return (env2, message) }
+
+ where
+ wrongArgsCtxt too_many_or_few fun
+ = ptext SLIT("Probable cause:") <+> quotes (ppr fun)
+ <+> ptext SLIT("is applied to") <+> text too_many_or_few
+ <+> ptext SLIT("arguments")
+
+------------------
+unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
+ -- tv1 and ty2 are zonked already
+ = returnM msg
+ where
+ msg = (env2, ptext SLIT("When matching the kinds of") <+>
+ sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
+
+ (pp_expected, pp_actual) | swapped = (pp2, pp1)
+ | otherwise = (pp1, pp2)
+ (env1, tv1') = tidyOpenTyVar tidy_env tv1
+ (env2, ty2') = tidyOpenType env1 ty2
+ pp1 = ppr tv1' <+> dcolon <+> ppr (tyVarKind tv1)
+ pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2)
+
+unifyMisMatch outer swapped ty1 ty2
+ = do { (env, msg) <- if swapped then misMatchMsg ty1 ty2
+ else misMatchMsg ty2 ty1
+
+ -- This is the whole point of the 'outer' stuff
+ ; if outer then popErrCtxt (failWithTcM (env, msg))
+ else failWithTcM (env, msg)
+ }
+
+misMatchMsg ty1 ty2
+ = do { env0 <- tcInitTidyEnv
+ ; (env1, pp1, extra1) <- ppr_ty env0 ty1
+ ; (env2, pp2, extra2) <- ppr_ty env1 ty2
+ ; return (env2, sep [sep [ptext SLIT("Couldn't match expected type") <+> pp1,
+ nest 7 (ptext SLIT("against inferred type") <+> pp2)],
+ nest 2 extra1, nest 2 extra2]) }
+
+ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc)
+ppr_ty env ty
+ = do { ty' <- zonkTcType ty
+ ; let (env1,tidy_ty) = tidyOpenType env ty'
+ simple_result = (env1, quotes (ppr tidy_ty), empty)
+ ; case tidy_ty of
+ TyVarTy tv
+ | isSkolemTyVar tv -> return (env2, pp_rigid tv',
+ pprSkolTvBinding tv')
+ | otherwise -> return simple_result
+ where
+ (env2, tv') = tidySkolemTyVar env1 tv
+ other -> return simple_result }
+ where
+ pp_rigid tv = quotes (ppr tv) <+> parens (ptext SLIT("a rigid variable"))
+
+
+notMonoType ty
+ = do { ty' <- zonkTcType ty
+ ; env0 <- tcInitTidyEnv
+ ; let (env1, tidy_ty) = tidyOpenType env0 ty'
+ msg = ptext SLIT("Cannot match a monotype with") <+> ppr tidy_ty
+ ; failWithTcM (env1, msg) }
+
+occurCheck tyvar ty
+ = do { env0 <- tcInitTidyEnv
+ ; ty' <- zonkTcType ty
+ ; let (env1, tidy_tyvar) = tidyOpenTyVar env0 tyvar
+ (env2, tidy_ty) = tidyOpenType env1 ty'
+ extra = sep [ppr tidy_tyvar, char '=', ppr tidy_ty]
+ ; failWithTcM (env2, hang msg 2 extra) }
+ where
+ msg = ptext SLIT("Occurs check: cannot construct the infinite type:")
+\end{code}
+
+
+%************************************************************************
+%* *