X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=aa9282970f3de401680fd8c483a9bd799d755871;hp=5b02241ce280556563de705a96334e3c273282d1;hb=ac0099f771c165d349d19f89102612215164a0f5;hpb=e33c65e18c77b1c21bd3b10a594b6ad61171ecb0 diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index 5b02241..aa92829 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -1,84 +1,68 @@ % +% (c) The University of Glasgow 2006 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 % -\section{Type subsumption and unification} + +Type subsumption and unification \begin{code} +{-# OPTIONS -w #-} +-- The above warning supression flag is a temporary kludge. +-- While working on this module you are encouraged to remove it and fix +-- any warnings in the module. See +-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings +-- for details + module TcUnify ( -- Full-blown subsumption - tcSubExp, tcFunResTy, tcGen, + tcSubExp, tcGen, checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt, -- Various unifications unifyType, unifyTypeList, unifyTheta, unifyKind, unifyKinds, unifyFunKind, checkExpectedKind, - preSubType, boxyMatchTypes, + preSubType, boxyMatchTypes, -------------------------------- -- Holes - tcInfer, subFunTys, unBox, stripBoxyType, withBox, + tcInfer, subFunTys, unBox, refineBox, refineBoxToTau, withBox, boxyUnify, boxyUnifyList, zapToMonotype, - boxySplitListTy, boxySplitTyConApp, boxySplitAppTy, + boxySplitListTy, boxySplitPArrTy, boxySplitTyConApp, boxySplitAppTy, wrapFunResCoercion ) where #include "HsVersions.h" -import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion, (<.>) ) -import TypeRep ( Type(..), PredType(..) ) - -import TcMType ( lookupTcTyVar, LookupTyVarResult(..), - tcInstSkolType, tcInstBoxyTyVar, newKindVar, newMetaTyVar, - newBoxyTyVar, newBoxyTyVarTys, readFilledBox, - readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy, - tcInstSkolTyVars, tcInstTyVar, - zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV, - readKindVar, writeKindVar ) -import TcSimplify ( tcSimplifyCheck ) -import TcEnv ( tcGetGlobalTyVars, findGlobals ) -import TcIface ( checkWiredInTyCon ) +import HsSyn +import TypeRep + +import TcMType +import TcSimplify +import TcEnv +import TcTyFuns +import TcIface import TcRnMonad -- TcType, amongst others -import TcType ( TcKind, TcType, TcTyVar, BoxyTyVar, TcTauType, - BoxySigmaType, BoxyRhoType, BoxyType, - TcTyVarSet, TcThetaType, TcTyVarDetails(..), BoxInfo(..), - SkolemInfo( GenSkol, UnkSkol ), MetaDetails(..), isImmutableTyVar, - pprSkolTvBinding, isTauTy, isTauTyCon, isSigmaTy, - mkFunTy, mkFunTys, mkTyConApp, isMetaTyVar, - tcSplitForAllTys, tcSplitAppTy_maybe, tcSplitFunTys, mkTyVarTys, - tcSplitSigmaTy, tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, - typeKind, mkForAllTys, mkAppTy, isBoxyTyVar, - tcView, exactTyVarsOfType, - tidyOpenType, tidyOpenTyVar, tidyOpenTyVars, - pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, isSigTyVar, - TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst, - substTy, substTheta, - lookupTyVar, extendTvSubst ) -import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind, - openTypeKind, liftedTypeKind, unliftedTypeKind, - mkArrowKind, defaultKind, - isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind, - isSubKind, pprKind, splitKindFunTys ) -import TysPrim ( alphaTy, betaTy ) -import Inst ( newDicts, instToId ) -import TyCon ( TyCon, tyConArity, tyConTyVars, isSynTyCon ) -import TysWiredIn ( listTyCon ) -import Id ( Id, mkSysLocal ) -import Var ( Var, varName, tyVarKind, isTcTyVar, tcTyVarDetails ) +import TcType +import Type +import Coercion +import TysPrim +import Inst +import TyCon +import TysWiredIn +import Var import VarSet import VarEnv -import Name ( Name, isSystemName ) -import ErrUtils ( Message ) -import Maybes ( expectJust, isNothing ) -import BasicTypes ( Arity ) -import UniqSupply ( uniqsFromSupply ) -import Util ( notNull, equalLength ) +import Name +import ErrUtils +import Maybes +import BasicTypes +import Util import Outputable +import Unique +import FastString --- Assertion imports -#ifdef DEBUG -import TcType ( isBoxyTy, isFlexi ) -#endif +import Control.Monad \end{code} %************************************************************************ @@ -89,12 +73,8 @@ import TcType ( isBoxyTy, isFlexi ) \begin{code} tcInfer :: (BoxyType -> TcM a) -> TcM (a, TcType) -tcInfer tc_infer - = do { box <- newBoxyTyVar openTypeKind - ; res <- tc_infer (mkTyVarTy box) - ; res_ty <- readFilledBox box -- Guaranteed filled-in by now - ; return (res, res_ty) } -\end{code} +tcInfer tc_infer = withBox openTypeKind tc_infer +\end{code} %************************************************************************ @@ -109,13 +89,13 @@ subFunTys :: SDoc -- Somthing like "The function f has 3 arguments" -> Arity -- Expected # of args -> BoxyRhoType -- res_ty -> ([BoxySigmaType] -> BoxyRhoType -> TcM a) - -> TcM (ExprCoFn, a) + -> TcM (HsWrapper, a) -- Attempt to decompse res_ty to have enough top-level arrows to -- match the number of patterns in the match group -- -- If (subFunTys n_args res_ty thing_inside) = (co_fn, res) -- and the inner call to thing_inside passes args: [a1,...,an], b --- then co_fn :: (a1 -> ... -> an -> b) -> res_ty +-- then co_fn :: (a1 -> ... -> an -> b) ~ res_ty -- -- Note that it takes a BoxyRho type, and guarantees to return a BoxyRhoType @@ -141,43 +121,68 @@ subFunTys error_herald n_pats res_ty thing_inside where -- In 'loop', the parameter 'arg_tys' accumulates -- the arg types so far, in *reverse order* + -- INVARIANT: res_ty :: * loop n args_so_far res_ty | Just res_ty' <- tcView res_ty = loop n args_so_far res_ty' loop n args_so_far res_ty | isSigmaTy res_ty -- Do this before checking n==0, because we - -- guarantee to return a BoxyRhoType, not a BoxySigmaType - = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ res_ty' -> + -- guarantee to return a BoxyRhoType, not a + -- BoxySigmaType + = do { (gen_fn, (co_fn, res)) <- tcGen res_ty emptyVarSet $ \ _ res_ty' -> loop n args_so_far res_ty' ; return (gen_fn <.> co_fn, res) } loop 0 args_so_far res_ty = do { res <- thing_inside (reverse args_so_far) res_ty - ; return (idCoercion, res) } + ; return (idHsWrapper, res) } loop n args_so_far (FunTy arg_ty res_ty) = do { (co_fn, res) <- loop (n-1) (arg_ty:args_so_far) res_ty ; co_fn' <- wrapFunResCoercion [arg_ty] co_fn ; return (co_fn', res) } + -- Try to normalise synonym families and defer if that's not possible + loop n args_so_far ty@(TyConApp tc tys) + | isOpenSynTyCon tc + = do { (coi1, ty') <- tcNormaliseFamInst ty + ; case coi1 of + IdCo -> defer n args_so_far ty + -- no progress, but maybe solvable => defer + ACo _ -> -- progress: so lets try again + do { (co_fn, res) <- loop n args_so_far ty' + ; return $ (co_fn <.> coiToHsWrapper (mkSymCoI coi1), res) + } + } + -- res_ty might have a type variable at the head, such as (a b c), -- in which case we must fill in with (->). Simplest thing to do -- is to use boxyUnify, but we catch failure and generate our own -- error message on failure loop n args_so_far res_ty@(AppTy _ _) = do { [arg_ty',res_ty'] <- newBoxyTyVarTys [argTypeKind, openTypeKind] - ; (_, mb_unit) <- tryTcErrs $ boxyUnify res_ty (FunTy arg_ty' res_ty') - ; if isNothing mb_unit then bale_out args_so_far - else loop n args_so_far (FunTy arg_ty' res_ty') } + ; (_, mb_coi) <- tryTcErrs $ + boxyUnify res_ty (FunTy arg_ty' res_ty') + ; if isNothing mb_coi then bale_out args_so_far + else do { let coi = expectJust "subFunTys" mb_coi + ; (co_fn, res) <- loop n args_so_far (FunTy arg_ty' + res_ty') + ; return (co_fn <.> coiToHsWrapper coi, res) + } + } - loop n args_so_far (TyVarTy tv) - | not (isImmutableTyVar tv) + loop n args_so_far ty@(TyVarTy tv) + | isTyConableTyVar tv = do { cts <- readMetaTyVar tv ; case cts of Indirect ty -> loop n args_so_far ty - Flexi -> do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty - ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty - ; return (idCoercion, res) } } + Flexi -> + do { (res_ty:arg_tys) <- withMetaTvs tv kinds mk_res_ty + ; res <- thing_inside (reverse args_so_far ++ arg_tys) + res_ty + ; return (idHsWrapper, res) } } + | otherwise -- defer as tyvar may be refined by equalities + = defer n args_so_far ty where mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty' mk_res_ty [] = panic "TcUnify.mk_res_ty1" @@ -187,6 +192,21 @@ subFunTys error_herald n_pats res_ty thing_inside loop n args_so_far res_ty = bale_out args_so_far + -- Build a template type a1 -> ... -> an -> b and defer an equality + -- between that template and the expected result type res_ty; then, + -- use the template to type the thing_inside + defer n args_so_far ty + = do { arg_tys <- newFlexiTyVarTys n argTypeKind + ; res_ty' <- newFlexiTyVarTy openTypeKind + ; let fun_ty = mkFunTys arg_tys res_ty' + err = error_herald <> comma $$ + text "which does not match its type" + ; coi <- addErrCtxt err $ + defer_unification (Unify False fun_ty ty) False fun_ty ty + ; res <- thing_inside (reverse args_so_far ++ arg_tys) res_ty' + ; return (coiToHsWrapper coi, res) + } + bale_out args_so_far = do { env0 <- tcInitTidyEnv ; res_ty' <- zonkTcType res_ty @@ -204,8 +224,9 @@ subFunTys error_herald n_pats res_ty thing_inside ---------------------- boxySplitTyConApp :: TyCon -- T :: k1 -> ... -> kn -> * -> BoxyRhoType -- Expected type (T a b c) - -> TcM [BoxySigmaType] -- Element types, a b c - -- It's used for wired-in tycons, so we call checkWiredInTyCOn + -> TcM ([BoxySigmaType], -- Element types, a b c + CoercionI) -- T a b c ~ orig_ty + -- It's used for wired-in tycons, so we call checkWiredInTyCon -- Precondition: never called with FunTyCon -- Precondition: input type :: * @@ -216,38 +237,74 @@ boxySplitTyConApp tc orig_ty loop n_req args_so_far ty | Just ty' <- tcView ty = loop n_req args_so_far ty' - loop n_req args_so_far (TyConApp tycon args) + loop n_req args_so_far ty@(TyConApp tycon args) | tc == tycon = ASSERT( n_req == length args) -- ty::* - return (args ++ args_so_far) + return (args ++ args_so_far, IdCo) + + | isOpenSynTyCon tycon -- try to normalise type family application + = do { (coi1, ty') <- tcNormaliseFamInst ty + ; traceTc $ text "boxySplitTyConApp:" <+> + ppr ty <+> text "==>" <+> ppr ty' + ; case coi1 of + IdCo -> defer -- no progress, but maybe solvable => defer + ACo _ -> -- progress: so lets try again + do { (args, coi2) <- loop n_req args_so_far ty' + ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1) + } + } loop n_req args_so_far (AppTy fun arg) - = loop (n_req - 1) (arg:args_so_far) fun + | n_req > 0 + = do { (args, coi) <- loop (n_req - 1) (arg:args_so_far) fun + ; return (args, mkAppTyCoI fun coi arg IdCo) + } loop n_req args_so_far (TyVarTy tv) - | not (isImmutableTyVar tv) + | isTyConableTyVar tv + , res_kind `isSubKind` tyVarKind tv = do { cts <- readMetaTyVar tv ; case cts of Indirect ty -> loop n_req args_so_far ty - Flexi -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty - ; return (arg_tys ++ args_so_far) } - } + Flexi -> do { arg_tys <- withMetaTvs tv arg_kinds mk_res_ty + ; return (arg_tys ++ args_so_far, IdCo) } + } + | otherwise -- defer as tyvar may be refined by equalities + = defer where - mk_res_ty arg_tys' = mkTyConApp tc arg_tys' - arg_kinds = map tyVarKind (take n_req (tyConTyVars tc)) + (arg_kinds, res_kind) = splitKindFunTysN n_req (tyConKind tc) - loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) orig_ty + loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) + orig_ty + + -- defer splitting by generating an equality constraint + defer = boxySplitDefer arg_kinds mk_res_ty orig_ty + where + (arg_kinds, _) = splitKindFunTys (tyConKind tc) + + -- apply splitted tycon to arguments + mk_res_ty = mkTyConApp tc ---------------------- -boxySplitListTy :: BoxyRhoType -> TcM BoxySigmaType -- Special case for lists -boxySplitListTy exp_ty = do { [elt_ty] <- boxySplitTyConApp listTyCon exp_ty - ; return elt_ty } +boxySplitListTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI) +-- Special case for lists +boxySplitListTy exp_ty + = do { ([elt_ty], coi) <- boxySplitTyConApp listTyCon exp_ty + ; return (elt_ty, coi) } +---------------------- +boxySplitPArrTy :: BoxyRhoType -> TcM (BoxySigmaType, CoercionI) +-- Special case for parrs +boxySplitPArrTy exp_ty + = do { ([elt_ty], coi) <- boxySplitTyConApp parrTyCon exp_ty + ; return (elt_ty, coi) } ---------------------- boxySplitAppTy :: BoxyRhoType -- Type to split: m a - -> TcM (BoxySigmaType, BoxySigmaType) -- Returns m, a --- Assumes (m: * -> k), where k is the kind of the incoming type + -> TcM ((BoxySigmaType, BoxySigmaType), -- Returns m, a + CoercionI) +-- If the incoming type is a mutable type variable of kind k, then +-- boxySplitAppTy returns a new type variable (m: * -> k); note the *. -- If the incoming type is boxy, then so are the result types; and vice versa boxySplitAppTy orig_ty @@ -258,18 +315,29 @@ boxySplitAppTy orig_ty loop ty | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty - = return (fun_ty, arg_ty) + = return ((fun_ty, arg_ty), IdCo) + + loop ty@(TyConApp tycon _args) + | isOpenSynTyCon tycon -- try to normalise type family application + = do { (coi1, ty') <- tcNormaliseFamInst ty + ; case coi1 of + IdCo -> defer -- no progress, but maybe solvable => defer + ACo co -> -- progress: so lets try again + do { (args, coi2) <- loop ty' + ; return $ (args, coi2 `mkTransCoI` mkSymCoI coi1) + } + } loop (TyVarTy tv) - | not (isImmutableTyVar tv) + | isTyConableTyVar tv = do { cts <- readMetaTyVar tv ; case cts of Indirect ty -> loop ty - Flexi -> do { [fun_ty,arg_ty] <- withMetaTvs tv kinds mk_res_ty - ; return (fun_ty, arg_ty) } } + Flexi -> do { [fun_ty, arg_ty] <- withMetaTvs tv kinds mk_res_ty + ; return ((fun_ty, arg_ty), IdCo) } } + | otherwise -- defer as tyvar may be refined by equalities + = defer where - mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty' - mk_res_ty other = panic "TcUnify.mk_res_ty2" tv_kind = tyVarKind tv kinds = [mkArrowKind liftedTypeKind (defaultKind tv_kind), -- m :: * -> k @@ -281,11 +349,34 @@ boxySplitAppTy orig_ty loop _ = boxySplitFailure (mkAppTy alphaTy betaTy) orig_ty + -- defer splitting by generating an equality constraint + defer = do { ([ty1, ty2], coi) <- boxySplitDefer arg_kinds mk_res_ty orig_ty + ; return ((ty1, ty2), coi) + } + where + orig_kind = typeKind orig_ty + arg_kinds = [mkArrowKind liftedTypeKind (defaultKind orig_kind), + -- m :: * -> k + liftedTypeKind] -- arg type :: * + + -- build type application + mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty' + mk_res_ty _other = panic "TcUnify.mk_res_ty2" + +------------------ +boxySplitFailure actual_ty expected_ty = failWithMisMatch actual_ty expected_ty + ------------------ -boxySplitFailure actual_ty expected_ty - = unifyMisMatch False False actual_ty expected_ty - -- "outer" is False, so we don't pop the context - -- which is what we want since we have not pushed one! +boxySplitDefer :: [Kind] -- kinds of required arguments + -> ([TcType] -> TcTauType) -- construct lhs from argument tyvars + -> BoxyRhoType -- type to split + -> TcM ([TcType], CoercionI) +boxySplitDefer kinds mk_ty orig_ty + = do { tau_tys <- mapM newFlexiTyVarTy kinds + ; let ty1 = mk_ty tau_tys + ; coi <- defer_unification (Unify False ty1 orig_ty) False ty1 orig_ty + ; return (tau_tys, coi) + } \end{code} @@ -323,9 +414,9 @@ withMetaTvs tv kinds mk_res_ty withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType) -- Allocate a *boxy* tyvar withBox kind thing_inside - = do { box_tv <- newMetaTyVar BoxTv kind + = do { box_tv <- newBoxyTyVar kind ; res <- thing_inside (mkTyVarTy box_tv) - ; ty <- readFilledBox box_tv + ; ty <- {- pprTrace "with_box" (ppr (mkTyVarTy box_tv)) $ -} readFilledBox box_tv ; return (res, ty) } \end{code} @@ -498,7 +589,9 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst (boxy_tvs `extendVarSetList` tvs2) tau2 subst go (TyConApp tc1 tys1) (TyConApp tc2 tys2) - | tc1 == tc2 = go_s tys1 tys2 + | tc1 == tc2 + , not $ isOpenSynTyCon tc1 + = go_s tys1 tys2 go (FunTy arg1 res1) (FunTy arg2 res2) = go_s [arg1,res1] [arg2,res2] @@ -511,7 +604,7 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst go (TyVarTy tv) b_ty | tv `elemVarSet` tmpl_tvs -- Template type variable in the template - , not (intersectsVarSet boxy_tvs (tyVarsOfType orig_boxy_ty)) + , boxy_tvs `disjointVarSet` tyVarsOfType orig_boxy_ty , typeKind b_ty `isSubKind` tyVarKind tv -- See Note [Matching kinds] = extendTvSubst subst tv boxy_ty' | otherwise @@ -521,6 +614,12 @@ boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst Nothing -> orig_boxy_ty Just ty -> ty `boxyLub` orig_boxy_ty + go _ (TyVarTy tv) | isMetaTyVar tv + = subst -- Don't fail if the template has more info than the target! + -- Otherwise, with tmpl_tvs = [a], matching (a -> Int) ~ (Bool -> beta) + -- would fail to instantiate 'a', because the meta-type-variable + -- beta is as yet un-filled-in + go _ _ = emptyTvSubst -- It's important to *fail* by returning the empty substitution -- Example: Tree a ~ Maybe Int -- We do not want to bind (a |-> Int) in pre-matching, because that can give very @@ -549,6 +648,10 @@ boxyLub orig_ty1 orig_ty2 | isTcTyVar tv1, isBoxyTyVar tv1 -- choose ty2 if ty2 is a box = orig_ty2 + go ty1 (TyVarTy tv2) -- Symmetrical case + | isTcTyVar tv2, isBoxyTyVar tv2 + = orig_ty1 + -- Look inside type synonyms, but only if the naive version fails go ty1 ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 | Just ty2' <- tcView ty1 = go ty1 ty2' @@ -579,42 +682,46 @@ Later stuff will fail. All the tcSub calls have the form - tcSub expected_ty offered_ty + tcSub actual_ty expected_ty which checks - offered_ty <= expected_ty + actual_ty <= expected_ty -That is, that a value of type offered_ty is acceptable in +That is, that a value of type actual_ty is acceptable in a place expecting a value of type expected_ty. It returns a coercion function - co_fn :: offered_ty -> expected_ty -which takes an HsExpr of type offered_ty into one of type + co_fn :: actual_ty ~ expected_ty +which takes an HsExpr of type actual_ty into one of type expected_ty. \begin{code} ----------------- -tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only +tcSubExp :: InstOrigin -> BoxySigmaType -> BoxySigmaType -> TcM HsWrapper -- (tcSub act exp) checks that -- act <= exp -tcSubExp actual_ty expected_ty +tcSubExp orig actual_ty expected_ty = -- addErrCtxtM (unifyCtxt actual_ty expected_ty) $ -- Adding the error context here leads to some very confusing error - -- messages, such as "can't match foarall a. a->a with forall a. a->a" - -- So instead I'm adding it when moving from tc_sub to u_tys - tc_sub Nothing actual_ty actual_ty False expected_ty expected_ty - -tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only -tcFunResTy fun actual_ty expected_ty - = tc_sub (Just fun) actual_ty actual_ty False expected_ty expected_ty - + -- messages, such as "can't match forall a. a->a with forall a. a->a" + -- Example is tcfail165: + -- do var <- newEmptyMVar :: IO (MVar (forall a. Show a => a -> String)) + -- putMVar var (show :: forall a. Show a => a -> String) + -- Here the info does not flow from the 'var' arg of putMVar to its 'show' arg + -- but after zonking it looks as if it does! + -- + -- So instead I'm adding the error context when moving from tc_sub to u_tys + + traceTc (text "tcSubExp" <+> ppr actual_ty <+> ppr expected_ty) >> + tc_sub orig actual_ty actual_ty False expected_ty expected_ty + ----------------- -tc_sub :: Maybe Name -- Just fun => we're looking at a function result type +tc_sub :: InstOrigin -> BoxySigmaType -- actual_ty, before expanding synonyms -> BoxySigmaType -- ..and after -> InBox -- True <=> expected_ty is inside a box -> BoxySigmaType -- expected_ty, before -> BoxySigmaType -- ..and after - -> TcM ExprCoFn + -> TcM HsWrapper -- The acual_ty is never inside a box -- IMPORTANT pre-condition: if the args contain foralls, the bound type -- variables are visible non-monadically @@ -622,24 +729,30 @@ tc_sub :: Maybe Name -- Just fun => we're looking at a function result type -- This invariant is needed so that we can "see" the foralls, ad -- e.g. in the SPEC rule where we just use splitSigmaTy -tc_sub mb_fun act_sty act_ty exp_ib exp_sty exp_ty - = tc_sub1 mb_fun act_sty act_ty exp_ib exp_sty exp_ty +tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty + = traceTc (text "tc_sub" <+> ppr act_ty $$ ppr exp_ty) >> + tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty -- This indirection is just here to make -- it easy to insert a debug trace! -tc_sub1 mb_fun act_sty act_ty exp_ib exp_sty exp_ty - | Just exp_ty' <- tcView exp_ty = tc_sub mb_fun act_sty act_ty exp_ib exp_sty exp_ty' -tc_sub1 mb_fun act_sty act_ty exp_ib exp_sty exp_ty - | Just act_ty' <- tcView act_ty = tc_sub mb_fun act_sty act_ty' exp_ib exp_sty exp_ty +tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty + | Just exp_ty' <- tcView exp_ty = tc_sub orig act_sty act_ty exp_ib exp_sty exp_ty' +tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty + | Just act_ty' <- tcView act_ty = tc_sub orig act_sty act_ty' exp_ib exp_sty exp_ty ----------------------------------- -- Rule SBOXY, plus other cases when act_ty is a type variable -- Just defer to boxy matching -- This rule takes precedence over SKOL! -tc_sub1 mb_fun act_sty (TyVarTy tv) exp_ib exp_sty exp_ty - = do { addErrCtxtM (subCtxt mb_fun act_sty exp_sty) $ - uVar True False tv exp_ib exp_sty exp_ty - ; return idCoercion } +tc_sub1 orig act_sty (TyVarTy tv) exp_ib exp_sty exp_ty + = do { traceTc (text "tc_sub1 - case 1") + ; coi <- addSubCtxt orig act_sty exp_sty $ + uVar (Unify True act_sty exp_sty) False tv exp_ib exp_sty exp_ty + ; traceTc (case coi of + IdCo -> text "tc_sub1 (Rule SBOXY) IdCo" + ACo co -> text "tc_sub1 (Rule SBOXY) ACo" <+> ppr co) + ; return $ coiToHsWrapper coi + } ----------------------------------- -- Skolemisation case (rule SKOL) @@ -652,12 +765,16 @@ tc_sub1 mb_fun act_sty (TyVarTy tv) exp_ib exp_sty exp_ty -- g :: Ord b => b->b -- Consider f g ! -tc_sub1 mb_fun act_sty act_ty exp_ib exp_sty exp_ty - | not exp_ib, -- SKOL does not apply if exp_ty is inside a box - isSigmaTy exp_ty - = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ body_exp_ty -> - tc_sub mb_fun act_sty act_ty False body_exp_ty body_exp_ty +tc_sub1 orig act_sty act_ty exp_ib exp_sty exp_ty + | isSigmaTy exp_ty = do + { traceTc (text "tc_sub1 - case 2") ; + if exp_ib then -- SKOL does not apply if exp_ty is inside a box + defer_to_boxy_matching orig act_sty act_ty exp_ib exp_sty exp_ty + else do + { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ _ body_exp_ty -> + tc_sub orig act_sty act_ty False body_exp_ty body_exp_ty ; return (gen_fn <.> co_fn) } + } where act_tvs = tyVarsOfType act_ty -- It's really important to check for escape wrt @@ -669,7 +786,7 @@ tc_sub1 mb_fun act_sty act_ty exp_ib exp_sty exp_ty -- expected_ty: Int -> Int -- co_fn e = e Int dOrdInt -tc_sub1 mb_fun act_sty actual_ty exp_ib exp_sty expected_ty +tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty -- Implements the new SPEC rule in the Appendix of the paper -- "Boxy types: inference for higher rank types and impredicativity" -- (This appendix isn't in the published version.) @@ -678,7 +795,8 @@ tc_sub1 mb_fun act_sty actual_ty exp_ib exp_sty expected_ty -- Pre-subsumpion finds a|->Int, and that works fine, whereas -- just running full subsumption would fail. | isSigmaTy actual_ty - = do { -- Perform pre-subsumption, and instantiate + = do { traceTc (text "tc_sub1 - case 3") + ; -- Perform pre-subsumption, and instantiate -- the type with info from the pre-subsumption; -- boxy tyvars if pre-subsumption gives no info let (tyvars, theta, tau) = tcSplitSigmaTy actual_ty @@ -695,58 +813,75 @@ tc_sub1 mb_fun act_sty actual_ty exp_ib exp_sty expected_ty ; traceTc (text "tc_sub_spec" <+> vcat [ppr actual_ty, ppr tyvars <+> ppr theta <+> ppr tau, ppr tau']) - ; co_fn <- tc_sub mb_fun tau' tau' exp_ib exp_sty expected_ty + ; co_fn2 <- tc_sub orig tau' tau' exp_ib exp_sty expected_ty -- Deal with the dictionaries - ; dicts <- newDicts InstSigOrigin (substTheta subst' theta) - ; extendLIEs dicts - ; let inst_fn = CoApps (CoTyApps CoHole inst_tys) - (map instToId dicts) - ; return (co_fn <.> inst_fn) } + ; co_fn1 <- instCall orig inst_tys (substTheta subst' theta) + ; return (co_fn2 <.> co_fn1) } ----------------------------------- -- Function case (rule F1) -tc_sub1 mb_fun _ (FunTy act_arg act_res) exp_ib _ (FunTy exp_arg exp_res) - = tc_sub_funs mb_fun act_arg act_res exp_ib exp_arg exp_res +tc_sub1 orig act_sty (FunTy act_arg act_res) exp_ib exp_sty (FunTy exp_arg exp_res) + = do { traceTc (text "tc_sub1 - case 4") + ; tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res + } -- Function case (rule F2) -tc_sub1 mb_fun act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv) +tc_sub1 orig act_sty act_ty@(FunTy act_arg act_res) _ exp_sty (TyVarTy exp_tv) | isBoxyTyVar exp_tv - = do { cts <- readMetaTyVar exp_tv + = do { traceTc (text "tc_sub1 - case 5") + ; cts <- readMetaTyVar exp_tv ; case cts of - Indirect ty -> tc_sub mb_fun act_sty act_ty True exp_sty ty - Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty - ; tc_sub_funs mb_fun act_arg act_res True arg_ty res_ty } } + Indirect ty -> tc_sub orig act_sty act_ty True exp_sty ty + Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty + ; tc_sub_funs orig act_arg act_res True arg_ty res_ty } } where mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty' mk_res_ty other = panic "TcUnify.mk_res_ty3" fun_kinds = [argTypeKind, openTypeKind] -- Everything else: defer to boxy matching -tc_sub1 mb_fun act_sty actual_ty exp_ib exp_sty expected_ty - = do { addErrCtxtM (subCtxt mb_fun act_sty exp_sty) $ - u_tys True False act_sty actual_ty exp_ib exp_sty expected_ty - ; return idCoercion } +tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty@(TyVarTy exp_tv) + = do { traceTc (text "tc_sub1 - case 6a" <+> ppr [isBoxyTyVar exp_tv, isMetaTyVar exp_tv, isSkolemTyVar exp_tv, isExistentialTyVar exp_tv,isSigTyVar exp_tv] ) + ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty + } + +tc_sub1 orig act_sty actual_ty exp_ib exp_sty expected_ty + = do { traceTc (text "tc_sub1 - case 6") + ; defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty + } +----------------------------------- +defer_to_boxy_matching orig act_sty actual_ty exp_ib exp_sty expected_ty + = do { coi <- addSubCtxt orig act_sty exp_sty $ + u_tys (Unify True act_sty exp_sty) + False act_sty actual_ty exp_ib exp_sty expected_ty + ; return $ coiToHsWrapper coi } ----------------------------------- -tc_sub_funs mb_fun act_arg act_res exp_ib exp_arg exp_res - = do { uTys False act_arg exp_ib exp_arg - ; co_fn_res <- tc_sub mb_fun act_res act_res exp_ib exp_res exp_res - ; wrapFunResCoercion [exp_arg] co_fn_res } +tc_sub_funs orig act_arg act_res exp_ib exp_arg exp_res + = do { arg_coi <- addSubCtxt orig act_arg exp_arg $ + uTysOuter False act_arg exp_ib exp_arg + ; co_fn_res <- tc_sub orig act_res act_res exp_ib exp_res exp_res + ; wrapper1 <- wrapFunResCoercion [exp_arg] co_fn_res + ; let wrapper2 = case arg_coi of + IdCo -> idHsWrapper + ACo co -> WpCo $ FunTy co act_res + ; return (wrapper1 <.> wrapper2) } ----------------------------------- wrapFunResCoercion :: [TcType] -- Type of args - -> ExprCoFn -- HsExpr a -> HsExpr b - -> TcM ExprCoFn -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b) + -> HsWrapper -- HsExpr a -> HsExpr b + -> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b) wrapFunResCoercion arg_tys co_fn_res - | isIdCoercion co_fn_res = return idCoercion - | null arg_tys = return co_fn_res - | otherwise - = do { us <- newUniqueSupply - ; let arg_ids = zipWith (mkSysLocal FSLIT("sub")) (uniqsFromSupply us) arg_tys - ; return (CoLams arg_ids (co_fn_res <.> (CoApps CoHole arg_ids))) } + | isIdHsWrapper co_fn_res + = return idHsWrapper + | null arg_tys + = return co_fn_res + | otherwise + = do { arg_ids <- newSysLocalIds FSLIT("sub") arg_tys + ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpApps arg_ids) } \end{code} @@ -762,32 +897,33 @@ tcGen :: BoxySigmaType -- expected_ty -> TcTyVarSet -- Extra tyvars that the universally -- quantified tyvars of expected_ty -- must not be unified - -> (BoxyRhoType -> TcM result) -- spec_ty - -> TcM (ExprCoFn, result) + -> ([TcTyVar] -> BoxyRhoType -> TcM result) + -> TcM (HsWrapper, result) -- The expression has type: spec_ty -> expected_ty tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type -- If not, the call is a no-op - = do { -- We want the GenSkol info in the skolemised type variables to + = do { traceTc (text "tcGen") + -- We want the GenSkol info in the skolemised type variables to -- mention the *instantiated* tyvar names, so that we get a -- good error message "Rigid variable 'a' is bound by (forall a. a->a)" -- Hence the tiresome but innocuous fixM - ((forall_tvs, theta, rho_ty), skol_info) <- fixM (\ ~(_, skol_info) -> + ; ((tvs', theta', rho'), skol_info) <- fixM (\ ~(_, skol_info) -> do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty - ; span <- getSrcSpanM - ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span + -- Get loation from monad, not from expected_ty + ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) ; return ((forall_tvs, theta, rho_ty), skol_info) }) -#ifdef DEBUG - ; traceTc (text "tcGen" <+> vcat [text "extra_tvs" <+> ppr extra_tvs, - text "expected_ty" <+> ppr expected_ty, - text "inst ty" <+> ppr forall_tvs <+> ppr theta <+> ppr rho_ty, - text "free_tvs" <+> ppr free_tvs, - text "forall_tvs" <+> ppr forall_tvs]) -#endif + ; when debugIsOn $ + traceTc (text "tcGen" <+> vcat [ + text "extra_tvs" <+> ppr extra_tvs, + text "expected_ty" <+> ppr expected_ty, + text "inst ty" <+> ppr tvs' <+> ppr theta' + <+> ppr rho', + text "free_tvs" <+> ppr free_tvs]) -- Type-check the arg and unify with poly type - ; (result, lie) <- getLIE (thing_inside rho_ty) + ; (result, lie) <- getLIE (thing_inside tvs' rho') -- Check that the "forall_tvs" havn't been constrained -- The interesting bit here is that we must include the free variables @@ -800,23 +936,21 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall -- Conclusion: include the free vars of the expected_ty in the -- list of "free vars" for the signature check. - ; dicts <- newDicts (SigOrigin skol_info) theta - ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie + ; loc <- getInstLoc (SigOrigin skol_info) + ; dicts <- newDictBndrs loc theta' -- Includes equalities + ; inst_binds <- tcSimplifyCheck loc tvs' dicts lie - ; checkSigTyVarsWrt free_tvs forall_tvs + ; checkSigTyVarsWrt free_tvs tvs' ; traceTc (text "tcGen:done") ; let - -- This HsLet binds any Insts which came out of the simplification. - -- 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 = CoTyLams forall_tvs $ CoLams dict_ids $ CoLet inst_binds CoHole - ; returnM (co_fn, result) } + -- The WpLet binds any Insts which came out of the simplification. + dict_vars = map instToVar dicts + co_fn = mkWpTyLams tvs' <.> mkWpLams dict_vars <.> WpLet inst_binds + ; return (co_fn, result) } where free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs - sig_msg = ptext SLIT("expected type of an expression") -\end{code} +\end{code} @@ -830,20 +964,19 @@ The exported functions are all defined as versions of some non-exported generic functions. \begin{code} -boxyUnify :: BoxyType -> BoxyType -> TcM () +boxyUnify :: BoxyType -> BoxyType -> TcM CoercionI -- Acutal and expected, respectively -boxyUnify ty1 ty2 - = addErrCtxtM (unifyCtxt ty1 ty2) $ - uTysOuter False ty1 False ty2 +boxyUnify ty1 ty2 = addErrCtxtM (unifyCtxt ty1 ty2) $ + uTysOuter False ty1 False ty2 --------------- -boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM () +boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM [CoercionI] -- Arguments should have equal length -- Acutal and expected types boxyUnifyList tys1 tys2 = uList boxyUnify tys1 tys2 --------------- -unifyType :: TcTauType -> TcTauType -> TcM () +unifyType :: TcTauType -> TcTauType -> TcM CoercionI -- No boxes expected inside these types -- Acutal and expected types unifyType ty1 ty2 -- ty1 expected, ty2 inferred @@ -853,26 +986,30 @@ unifyType ty1 ty2 -- ty1 expected, ty2 inferred uTysOuter True ty1 True ty2 --------------- -unifyPred :: PredType -> PredType -> TcM () +unifyPred :: PredType -> PredType -> TcM CoercionI -- Acutal and expected types -unifyPred p1 p2 = addErrCtxtM (unifyCtxt (mkPredTy p1) (mkPredTy p2)) $ - uPred True True p1 True p2 +unifyPred p1 p2 = uPred (Unify False (mkPredTy p1) (mkPredTy p2)) True p1 True p2 -unifyTheta :: TcThetaType -> TcThetaType -> TcM () +unifyTheta :: TcThetaType -> TcThetaType -> TcM [CoercionI] -- Acutal and expected types unifyTheta theta1 theta2 = do { checkTc (equalLength theta1 theta2) - (ptext SLIT("Contexts differ in length")) - ; uList unifyPred theta1 theta2 } + (vcat [ptext SLIT("Contexts differ in length"), + nest 2 $ parens $ ptext SLIT("Use -fglasgow-exts to allow this")]) + ; uList unifyPred theta1 theta2 + } --------------- -uList :: (a -> a -> TcM ()) - -> [a] -> [a] -> TcM () +uList :: (a -> a -> TcM b) + -> [a] -> [a] -> TcM [b] -- Unify corresponding elements of two lists of types, which --- should be f equal length. We charge down the list explicitly so that +-- should be of equal length. We charge down the list explicitly so that -- we can complain if their lengths differ. -uList unify [] [] = return () -uList unify (ty1:tys1) (ty2:tys2) = do { unify ty1 ty2; uList unify tys1 tys2 } +uList unify [] [] = return [] +uList unify (ty1:tys1) (ty2:tys2) = do { x <- unify ty1 ty2; + ; xs <- uList unify tys1 tys2 + ; return (x:xs) + } uList unify ty1s ty2s = panic "Unify.uList: mismatched type lists!" \end{code} @@ -882,8 +1019,8 @@ lists, when all the elts should be of the same type. \begin{code} unifyTypeList :: [TcTauType] -> TcM () -unifyTypeList [] = returnM () -unifyTypeList [ty] = returnM () +unifyTypeList [] = return () +unifyTypeList [ty] = return () unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2 ; unifyTypeList tys } \end{code} @@ -894,8 +1031,8 @@ unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2 %* * %************************************************************************ -@uTys@ is the heart of the unifier. Each arg happens twice, because -we want to report errors in terms of synomyms if poss. The first of +@uTys@ is the heart of the unifier. Each arg occurs twice, because +we want to report errors in terms of synomyms if possible. The first of the pair is used in error messages only; it is always the same as the second, except that if the first is a synonym then the second may be a de-synonym'd version. This way we get better error messages. @@ -903,6 +1040,10 @@ de-synonym'd version. This way we get better error messages. We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''. \begin{code} +type SwapFlag = Bool + -- False <=> the two args are (actual, expected) respectively + -- True <=> the two args are (expected, actual) respectively + type InBox = Bool -- True <=> we are inside a box -- False <=> we are outside a box -- The importance of this is that if we get "filled-box meets @@ -910,110 +1051,227 @@ type InBox = Bool -- True <=> we are inside a box -- we must not allow polytypes. But if we are in a box on -- just one side, then we can allow polytypes -type Outer = Bool -- True <=> this is the outer level of a unification - -- so that the types being unified are the - -- very ones we began with, not some sub - -- component or synonym expansion --- The idea is that if Outer is true then unifyMisMatch should --- pop the context to remove the "Expected/Acutal" context +data Outer = Unify Bool TcType TcType + -- If there is a unification error, report these types as mis-matching + -- Bool = True <=> the context says "Expected = ty1, Acutal = ty2" + -- for this particular ty1,ty2 + +instance Outputable Outer where + ppr (Unify c ty1 ty2) = pp_c <+> pprParendType ty1 <+> ptext SLIT("~") + <+> pprParendType ty2 + where + pp_c = if c then ptext SLIT("Top") else ptext SLIT("NonTop") + + +------------------------- +uTysOuter :: InBox -> TcType -- ty1 is the *actual* type + -> InBox -> TcType -- ty2 is the *expected* type + -> TcM CoercionI +-- We've just pushed a context describing ty1,ty2 +uTysOuter nb1 ty1 nb2 ty2 + = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2) + ; u_tys (Unify True ty1 ty2) nb1 ty1 ty1 nb2 ty2 ty2 } -uTysOuter, uTys - :: InBox -> TcType -- ty1 is the *expected* type - -> InBox -> TcType -- ty2 is the *actual* type - -> TcM () -uTysOuter nb1 ty1 nb2 ty2 = u_tys True nb1 ty1 ty1 nb2 ty2 ty2 -uTys nb1 ty1 nb2 ty2 = u_tys False nb1 ty1 ty1 nb2 ty2 ty2 +uTys :: InBox -> TcType -> InBox -> TcType -> TcM CoercionI +-- The context does not describe ty1,ty2 +uTys nb1 ty1 nb2 ty2 + = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2) + ; u_tys (Unify False ty1 ty2) nb1 ty1 ty1 nb2 ty2 ty2 } -------------- -uTys_s :: InBox -> [TcType] -- ty1 is the *actual* types - -> InBox -> [TcType] -- ty2 is the *expected* types - -> TcM () -uTys_s nb1 [] nb2 [] = returnM () -uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { uTys nb1 ty1 nb2 ty2 - ; uTys_s nb1 tys1 nb2 tys2 } +uTys_s :: InBox -> [TcType] -- tys1 are the *actual* types + -> InBox -> [TcType] -- tys2 are the *expected* types + -> TcM [CoercionI] +uTys_s nb1 [] nb2 [] = return [] +uTys_s nb1 (ty1:tys1) nb2 (ty2:tys2) = do { coi <- uTys nb1 ty1 nb2 ty2 + ; cois <- uTys_s nb1 tys1 nb2 tys2 + ; return (coi:cois) } uTys_s nb1 ty1s nb2 ty2s = panic "Unify.uTys_s: mismatched type lists!" -------------- u_tys :: Outer -> InBox -> TcType -> TcType -- ty1 is the *actual* type -> InBox -> TcType -> TcType -- ty2 is the *expected* type - -> TcM () + -> TcM CoercionI u_tys outer nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 - = go outer ty1 ty2 + = do { traceTc (text "u_tys " <+> vcat [sep [ braces (ppr orig_ty1 <+> text "/" <+> ppr ty1), + text "~", + braces (ppr orig_ty2 <+> text "/" <+> ppr ty2)], + ppr outer]) + ; coi <- go outer orig_ty1 ty1 orig_ty2 ty2 + ; traceTc (case coi of + ACo co -> text "u_tys yields coercion:" <+> ppr co + IdCo -> text "u_tys yields no coercion") + ; return coi + } where - - -- Always expand synonyms (see notes at end) + bale_out :: Outer -> TcM a + bale_out outer = unifyMisMatch outer + -- We report a mis-match in terms of the original arugments to + -- u_tys, even though 'go' has recursed inwards somewhat + -- + -- Note [Unifying AppTy] + -- A case in point is unifying (m Int) ~ (IO Int) + -- where m is a unification variable that is now bound to (say) (Bool ->) + -- Then we want to report "Can't unify (Bool -> Int) with (IO Int) + -- and not "Can't unify ((->) Bool) with IO" + + go :: Outer -> TcType -> TcType -> TcType -> TcType -> TcM CoercionI + -- Always expand synonyms: see Note [Unification and synonyms] -- (this also throws away FTVs) - go outer ty1 ty2 - | Just ty1' <- tcView ty1 = go False ty1' ty2 - | Just ty2' <- tcView ty2 = go False ty1 ty2' + go outer sty1 ty1 sty2 ty2 + | Just ty1' <- tcView ty1 = go (Unify False ty1' ty2 ) sty1 ty1' sty2 ty2 + | Just ty2' <- tcView ty2 = go (Unify False ty1 ty2') sty1 ty1 sty2 ty2' -- Variables; go for uVar - go outer (TyVarTy tyvar1) ty2 = uVar outer False tyvar1 nb2 orig_ty2 ty2 - go outer ty1 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 orig_ty1 ty1 + go outer sty1 (TyVarTy tyvar1) sty2 ty2 = uVar outer False tyvar1 nb2 sty2 ty2 + go outer sty1 ty1 sty2 (TyVarTy tyvar2) = uVar outer True tyvar2 nb1 sty1 ty1 -- "True" means args swapped + + -- The case for sigma-types must *follow* the variable cases + -- because a boxy variable can be filed with a polytype; + -- but must precede FunTy, because ((?x::Int) => ty) look + -- like a FunTy; there isn't necy a forall at the top + go _ _ ty1 _ ty2 + | isSigmaTy ty1 || isSigmaTy ty2 + = do { traceTc (text "We have sigma types: equalLength" <+> ppr tvs1 <+> ppr tvs2) + ; unless (equalLength tvs1 tvs2) (bale_out outer) + ; traceTc (text "We're past the first length test") + ; tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo + -- Get location from monad, not from tvs1 + ; let tys = mkTyVarTys tvs + in_scope = mkInScopeSet (mkVarSet tvs) + phi1 = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1 + phi2 = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2 + (theta1,tau1) = tcSplitPhiTy phi1 + (theta2,tau2) = tcSplitPhiTy phi2 + + ; addErrCtxtM (unifyForAllCtxt tvs phi1 phi2) $ do + { unless (equalLength theta1 theta2) (bale_out outer) + ; cois <- uPreds outer nb1 theta1 nb2 theta2 -- TOMDO: do something with these pred_cois + ; traceTc (text "TOMDO!") + ; coi <- uTys nb1 tau1 nb2 tau2 + + -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a) + ; free_tvs <- zonkTcTyVarsAndFV (varSetElems (tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2)) + ; when (any (`elemVarSet` free_tvs) tvs) + (bleatEscapedTvs free_tvs tvs tvs) + + -- If both sides are inside a box, we are in a "box-meets-box" + -- situation, and we should not have a polytype at all. + -- If we get here we have two boxes, already filled with + -- the same polytype... but it should be a monotype. + -- This check comes last, because the error message is + -- extremely unhelpful. + ; when (nb1 && nb2) (notMonoType ty1) + ; return coi + }} + where + (tvs1, body1) = tcSplitForAllTys ty1 + (tvs2, body2) = tcSplitForAllTys ty2 + -- Predicates - go outer (PredTy p1) (PredTy p2) = uPred outer nb1 p1 nb2 p2 + go outer _ (PredTy p1) _ (PredTy p2) + = uPred outer nb1 p1 nb2 p2 -- Type constructors must match - go _ (TyConApp con1 tys1) (TyConApp con2 tys2) - | con1 == con2 = uTys_s nb1 tys1 nb2 tys2 + go _ _ (TyConApp con1 tys1) _ (TyConApp con2 tys2) + | con1 == con2 && not (isOpenSynTyCon con1) + = do { cois <- uTys_s nb1 tys1 nb2 tys2 + ; return $ mkTyConAppCoI con1 tys1 cois + } -- See Note [TyCon app] + | con1 == con2 && identicalOpenSynTyConApp + = do { cois <- uTys_s nb1 tys1' nb2 tys2' + ; return $ mkTyConAppCoI con1 tys1 (replicate n IdCo ++ cois) + } + where + n = tyConArity con1 + (idxTys1, tys1') = splitAt n tys1 + (idxTys2, tys2') = splitAt n tys2 + identicalOpenSynTyConApp = idxTys1 `tcEqTypes` idxTys2 + -- See Note [OpenSynTyCon app] -- Functions; just check the two parts - go _ (FunTy fun1 arg1) (FunTy fun2 arg2) - = do { uTys nb1 fun1 nb2 fun2 - ; uTys nb1 arg1 nb2 arg2 } + go _ _ (FunTy fun1 arg1) _ (FunTy fun2 arg2) + = do { coi_l <- uTys nb1 fun1 nb2 fun2 + ; coi_r <- uTys nb1 arg1 nb2 arg2 + ; return $ mkFunTyCoI fun1 coi_l arg1 coi_r + } -- Applications need a bit of care! -- They can match FunTy and TyConApp, so use splitAppTy_maybe -- NB: we've already dealt with type variables and Notes, -- so if one type is an App the other one jolly well better be too - go outer (AppTy s1 t1) ty2 + go outer _ (AppTy s1 t1) _ ty2 | Just (s2,t2) <- tcSplitAppTy_maybe ty2 - = do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 } + = do { coi_s <- go outer s1 s1 s2 s2 -- NB recurse into go + ; coi_t <- uTys nb1 t1 nb2 t2 -- See Note [Unifying AppTy] + ; return $ mkAppTyCoI s1 coi_s t1 coi_t } -- Now the same, but the other way round -- Don't swap the types, because the error messages get worse - go outer ty1 (AppTy s2 t2) + go outer _ ty1 _ (AppTy s2 t2) | Just (s1,t1) <- tcSplitAppTy_maybe ty1 - = do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 } - - go _ ty1@(ForAllTy _ _) ty2@(ForAllTy _ _) - | length tvs1 == length tvs2 - = do { tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo - ; let tys = mkTyVarTys tvs - in_scope = mkInScopeSet (mkVarSet tvs) - subst1 = mkTvSubst in_scope (zipTyEnv tvs1 tys) - subst2 = mkTvSubst in_scope (zipTyEnv tvs2 tys) - ; uTys nb1 (substTy subst1 body1) nb2 (substTy subst2 body2) - - -- If both sides are inside a box, we are in a "box-meets-box" - -- situation, and we should not have a polytype at all. - -- If we get here we have two boxes, already filled with - -- the same polytype... but it should be a monotype. - -- This check comes last, because the error message is - -- extremely unhelpful. - ; ifM (nb1 && nb2) (notMonoType ty1) - } - where - (tvs1, body1) = tcSplitForAllTys ty1 - (tvs2, body2) = tcSplitForAllTys ty2 + = do { coi_s <- go outer s1 s1 s2 s2 + ; coi_t <- uTys nb1 t1 nb2 t2 + ; return $ mkAppTyCoI s1 coi_s t1 coi_t } + + -- One or both outermost constructors are type family applications. + -- If we can normalise them away, proceed as usual; otherwise, we + -- need to defer unification by generating a wanted equality constraint. + go outer sty1 ty1 sty2 ty2 + | ty1_is_fun || ty2_is_fun + = do { (coi1, ty1') <- if ty1_is_fun then tcNormaliseFamInst ty1 + else return (IdCo, ty1) + ; (coi2, ty2') <- if ty2_is_fun then tcNormaliseFamInst ty2 + else return (IdCo, ty2) + ; coi <- if isOpenSynTyConApp ty1' || isOpenSynTyConApp ty2' + then do { -- One type family app can't be reduced yet + -- => defer + ; ty1'' <- zonkTcType ty1' + ; ty2'' <- zonkTcType ty2' + ; if tcEqType ty1'' ty2'' + then return IdCo + else -- see [Deferred Unification] + defer_unification outer False orig_ty1 orig_ty2 + } + else -- unification can proceed + go outer sty1 ty1' sty2 ty2' + ; return $ coi1 `mkTransCoI` coi `mkTransCoI` (mkSymCoI coi2) + } + where + ty1_is_fun = isOpenSynTyConApp ty1 + ty2_is_fun = isOpenSynTyConApp ty2 - -- Anything else fails - go outer _ _ = unifyMisMatch outer False orig_ty1 orig_ty2 + -- Anything else fails + go outer _ _ _ _ = bale_out outer ---------- uPred outer nb1 (IParam n1 t1) nb2 (IParam n2 t2) - | n1 == n2 = uTys nb1 t1 nb2 t2 + | n1 == n2 = + do { coi <- uTys nb1 t1 nb2 t2 + ; return $ mkIParamPredCoI n1 coi + } uPred outer nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2) - | c1 == c2 = uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check -uPred outer _ p1 _ p2 = unifyMisMatch outer False (mkPredTy p1) (mkPredTy p2) + | c1 == c2 = + do { cois <- uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check + ; return $ mkClassPPredCoI c1 tys1 cois + } +uPred outer _ p1 _ p2 = unifyMisMatch outer + +uPreds outer nb1 [] nb2 [] = return [] +uPreds outer nb1 (p1:ps1) nb2 (p2:ps2) = + do { coi <- uPred outer nb1 p1 nb2 p2 + ; cois <- uPreds outer nb1 ps1 nb2 ps2 + ; return (coi:cois) + } +uPreds outer nb1 ps1 nb2 ps2 = panic "uPreds" \end{code} -Note [Tycon app] +Note [TyCon app] ~~~~~~~~~~~~~~~~ When we find two TyConApps, the argument lists are guaranteed equal length. Reason: intially the kinds of the two types to be unified is @@ -1023,9 +1281,20 @@ the f1,f2 (because it'd absorb the app). If we unify f1:=:f2 first, which we do, that ensures that f1,f2 have the same kind; and that means a1,a2 have the same kind. And now the argument repeats. +Note [OpenSynTyCon app] +~~~~~~~~~~~~~~~~~~~~~~~ +Given -Notes on synonyms -~~~~~~~~~~~~~~~~~ + type family T a :: * -> * + +the two types (T () a) and (T () Int) must unify, even if there are +no type instances for T at all. Should we just turn them into an +equality (T () a ~ T () Int)? I don't think so. We currently try to +eagerly unify everything we can before generating equalities; otherwise, +we could turn the unification of [Int] with [a] into an equality, too. + +Note [Unification and synonyms] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ If you are tempted to make a short cut on synonyms, as in this pseudocode... @@ -1089,19 +1358,19 @@ back into @uTys@ if it turns out that the variable is already bound. \begin{code} uVar :: Outer - -> Bool -- False => tyvar is the "expected" - -- True => ty is the "expected" thing + -> SwapFlag -- False => tyvar is the "actual" (ty is "expected") + -- True => ty is the "actual" (tyvar is "expected") -> TcTyVar -> InBox -- True <=> definitely no boxes in t2 -> TcTauType -> TcTauType -- printing and real versions - -> TcM () + -> TcM CoercionI uVar outer swapped tv1 nb2 ps_ty2 ty2 = do { let expansion | showSDoc (ppr ty2) == showSDoc (ppr ps_ty2) = empty | otherwise = brackets (equals <+> ppr ty2) - ; traceTc (text "uVar" <+> ppr swapped <+> + ; traceTc (text "uVar" <+> ppr outer <+> ppr swapped <+> sep [ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1 ), - nest 2 (ptext SLIT(" :=: ")), + nest 2 (ptext SLIT(" <-> ")), ppr ps_ty2 <+> dcolon <+> ppr (typeKind ty2) <+> expansion]) ; details <- lookupTcTyVar tv1 ; case details of @@ -1114,16 +1383,18 @@ uVar outer swapped tv1 nb2 ps_ty2 ty2 ---------------- uUnfilledVar :: Outer - -> Bool -- Args are swapped + -> SwapFlag -> TcTyVar -> TcTyVarDetails -- Tyvar 1 -> TcTauType -> TcTauType -- Type 2 - -> TcM () + -> TcM CoercionI -- Invariant: tyvar 1 is not unified with anything uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2 | Just ty2' <- tcView ty2 = -- Expand synonyms; ignore FTVs - uUnfilledVar False swapped tv1 details1 ps_ty2 ty2' + let outer' | swapped = Unify False ty2' (mkTyVarTy tv1) + | otherwise = Unify False (mkTyVarTy tv1) ty2' + in uUnfilledVar outer' swapped tv1 details1 ps_ty2 ty2' uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2) | tv1 == tv2 -- Same type variable => no-op (but watch out for the boxy case) @@ -1131,94 +1402,179 @@ uUnfilledVar outer swapped tv1 details1 ps_ty2 (TyVarTy tv2) MetaTv BoxTv ref1 -- A boxy type variable meets itself; -- this is box-meets-box, so fill in with a tau-type -> do { tau_tv <- tcInstTyVar tv1 - ; updateMeta tv1 ref1 (mkTyVarTy tau_tv) } - other -> returnM () -- No-op + ; updateMeta tv1 ref1 (mkTyVarTy tau_tv) + ; return IdCo + } + other -> return IdCo -- No-op - -- Distinct type variables - | otherwise + | otherwise -- Distinct type variables = do { lookup2 <- lookupTcTyVar tv2 ; case lookup2 of - IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 ty2' ty2' + IndirectTv ty2' -> uUnfilledVar outer swapped tv1 details1 ty2' ty2' DoneTv details2 -> uUnfilledVars outer swapped tv1 details1 tv2 details2 } -uUnfilledVar outer swapped tv1 details1 ps_ty2 non_var_ty2 -- ty2 is not a type variable - = case details1 of - MetaTv (SigTv _) ref1 -> mis_match -- Can't update a skolem with a non-type-variable - MetaTv info ref1 -> uMetaVar swapped tv1 info ref1 ps_ty2 non_var_ty2 - skolem_details -> mis_match +uUnfilledVar outer swapped tv1 details1 ps_ty2 non_var_ty2 + = -- ty2 is not a type variable + case details1 of + MetaTv (SigTv _) _ -> rigid_variable + MetaTv info ref1 -> uMetaVar outer swapped tv1 info ref1 ps_ty2 non_var_ty2 + SkolemTv _ -> rigid_variable where - mis_match = unifyMisMatch outer swapped (TyVarTy tv1) ps_ty2 + rigid_variable + | isOpenSynTyConApp non_var_ty2 + = -- 'non_var_ty2's outermost constructor is a type family, + -- which we may may be able to normalise + do { (coi2, ty2') <- tcNormaliseFamInst non_var_ty2 + ; case coi2 of + IdCo -> -- no progress, but maybe after other instantiations + defer_unification outer swapped (TyVarTy tv1) ps_ty2 + ACo co -> -- progress: so lets try again + do { traceTc $ + ppr co <+> text "::"<+> ppr non_var_ty2 <+> text "~" <+> + ppr ty2' + ; coi <- uUnfilledVar outer swapped tv1 details1 ps_ty2 ty2' + ; let coi2' = (if swapped then id else mkSymCoI) coi2 + ; return $ coi2' `mkTransCoI` coi + } + } + | SkolemTv RuntimeUnkSkol <- details1 + -- runtime unknown will never match + = unifyMisMatch outer + | otherwise -- defer as a given equality may still resolve this + = defer_unification outer swapped (TyVarTy tv1) ps_ty2 +\end{code} + +Note [Deferred Unification] +~~~~~~~~~~~~~~~~~~~~ +We may encounter a unification ty1 = ty2 that cannot be performed syntactically, +and yet its consistency is undetermined. Previously, there was no way to still +make it consistent. So a mismatch error was issued. + +Now these unfications are deferred until constraint simplification, where type +family instances and given equations may (or may not) establish the consistency. +Deferred unifications are of the form + F ... ~ ... +or x ~ ... +where F is a type function and x is a type variable. +E.g. + id :: x ~ y => x -> y + id e = e + +involves the unfication x = y. It is deferred until we bring into account the +context x ~ y to establish that it holds. + +If available, we defer original types (rather than those where closed type +synonyms have already been expanded via tcCoreView). This is, as usual, to +improve error messages. + +We need to both 'unBox' and zonk deferred types. We need to unBox as +functions, such as TcExpr.tcMonoExpr promise to fill boxes in the expected +type. We need to zonk as the types go into the kind of the coercion variable +`cotv' and those are not zonked in Inst.zonkInst. (Maybe it would be better +to zonk in zonInst instead. Would that be sufficient?) + +\begin{code} +defer_unification :: Outer + -> SwapFlag + -> TcType + -> TcType + -> TcM CoercionI +defer_unification outer True ty1 ty2 + = defer_unification outer False ty2 ty1 +defer_unification outer False ty1 ty2 + = do { ty1' <- unBox ty1 >>= zonkTcType -- unbox *and* zonk.. + ; ty2' <- unBox ty2 >>= zonkTcType -- ..see preceding note + ; traceTc $ text "deferring:" <+> ppr ty1 <+> text "~" <+> ppr ty2 + ; cotv <- newMetaCoVar ty1' ty2' + -- put ty1 ~ ty2 in LIE + -- Left means "wanted" + ; inst <- popUnifyCtxt outer $ + mkEqInst (EqPred ty1' ty2') (Left cotv) + ; extendLIE inst + ; return $ ACo $ TyVarTy cotv } ---------------- -uMetaVar :: Bool +uMetaVar :: Outer + -> SwapFlag -> TcTyVar -> BoxInfo -> IORef MetaDetails -> TcType -> TcType - -> TcM () + -> TcM CoercionI -- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau) -- ty2 is not a type variable -uMetaVar swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2 +uMetaVar outer swapped tv1 BoxTv ref1 ps_ty2 non_var_ty2 = -- tv1 is a BoxTv. So we must unbox ty2, to ensure -- that any boxes in ty2 are filled with monotypes -- -- It should not be the case that tv1 occurs in ty2 -- (i.e. no occurs check should be needed), but if perchance - -- it does, the unbox operation will fill it, and the DEBUG + -- it does, the unbox operation will fill it, and the debug code -- checks for that. - do { final_ty <- unBox ps_ty2 -#ifdef DEBUG - ; meta_details <- readMutVar ref1 - ; case meta_details of - Indirect ty -> WARN( True, ppr tv1 <+> ppr ty ) - return () -- This really should *not* happen - Flexi -> return () -#endif - ; checkUpdateMeta swapped tv1 ref1 final_ty } - -uMetaVar swapped tv1 info1 ref1 ps_ty2 non_var_ty2 - = do { final_ty <- checkTauTvUpdate tv1 ps_ty2 -- Occurs check + monotype check - ; checkUpdateMeta swapped tv1 ref1 final_ty } + do { final_ty <- unBox ps_ty2 + ; when debugIsOn $ do + { meta_details <- readMutVar ref1 + ; case meta_details of + Indirect ty -> WARN( True, ppr tv1 <+> ppr ty ) + return () -- This really should *not* happen + Flexi -> return () + } + ; checkUpdateMeta swapped tv1 ref1 final_ty + ; return IdCo + } + +uMetaVar outer swapped tv1 info1 ref1 ps_ty2 non_var_ty2 + = do { -- Occurs check + monotype check + ; mb_final_ty <- checkTauTvUpdate tv1 ps_ty2 + ; case mb_final_ty of + Nothing -> -- tv1 occured in type family parameter + defer_unification outer swapped (mkTyVarTy tv1) ps_ty2 + Just final_ty -> + do { checkUpdateMeta swapped tv1 ref1 final_ty + ; return IdCo + } + } ---------------- uUnfilledVars :: Outer - -> Bool -- Args are swapped + -> SwapFlag -> TcTyVar -> TcTyVarDetails -- Tyvar 1 -> TcTyVar -> TcTyVarDetails -- Tyvar 2 - -> TcM () + -> TcM CoercionI -- Invarant: The type variables are distinct, -- Neither is filled in yet -- They might be boxy or not uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (SkolemTv _) - = unifyMisMatch outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2) + = -- see [Deferred Unification] + defer_unification outer swapped (mkTyVarTy tv1) (mkTyVarTy tv2) uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (SkolemTv _) - = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2) + = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2) >> return IdCo uUnfilledVars outer swapped tv1 (SkolemTv _) tv2 (MetaTv info2 ref2) - = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) + = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) >> return IdCo -- ToDo: this function seems too long for what it acutally does! uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) = case (info1, info2) of - (BoxTv, BoxTv) -> box_meets_box + (BoxTv, BoxTv) -> box_meets_box >> return IdCo -- If a box meets a TauTv, but the fomer has the smaller kind -- then we must create a fresh TauTv with the smaller kind - (_, BoxTv) | k1_sub_k2 -> update_tv2 - | otherwise -> box_meets_box - (BoxTv, _ ) | k2_sub_k1 -> update_tv1 - | otherwise -> box_meets_box + (_, BoxTv) | k1_sub_k2 -> update_tv2 >> return IdCo + | otherwise -> box_meets_box >> return IdCo + (BoxTv, _ ) | k2_sub_k1 -> update_tv1 >> return IdCo + | otherwise -> box_meets_box >> return IdCo -- Avoid SigTvs if poss - (SigTv _, _ ) | k1_sub_k2 -> update_tv2 - (_, SigTv _) | k2_sub_k1 -> update_tv1 + (SigTv _, _ ) | k1_sub_k2 -> update_tv2 >> return IdCo + (_, SigTv _) | k2_sub_k1 -> update_tv1 >> return IdCo (_, _) | k1_sub_k2 -> if k2_sub_k1 && nicer_to_update_tv1 - then update_tv1 -- Same kinds - else update_tv2 - | k2_sub_k1 -> update_tv1 - | otherwise -> kind_err + then update_tv1 >> return IdCo -- Same kinds + else update_tv2 >> return IdCo + | k2_sub_k1 -> update_tv1 >> return IdCo + | otherwise -> kind_err >> return IdCo -- Update the variable with least kind info -- See notes on type inference in Kind.lhs @@ -1250,156 +1606,34 @@ uUnfilledVars outer swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) k1_sub_k2 = k1 `isSubKind` k2 k2_sub_k1 = k2 `isSubKind` k1 - nicer_to_update_tv1 = isSystemName (varName tv1) + nicer_to_update_tv1 = isSystemName (Var.varName tv1) -- Try to update sys-y type variables in preference to ones -- gotten (say) by instantiating a polymorphic function with -- a user-written type sig - ----------------- -checkUpdateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM () --- Update tv1, which is flexi; occurs check is alrady done --- The 'check' version does a kind check too --- We do a sub-kind check here: we might unify (a b) with (c d) --- where b::*->* and d::*; this should fail - -checkUpdateMeta swapped tv1 ref1 ty2 - = do { checkKinds swapped tv1 ty2 - ; updateMeta tv1 ref1 ty2 } - -updateMeta :: TcTyVar -> IORef MetaDetails -> TcType -> TcM () -updateMeta tv1 ref1 ty2 - = ASSERT( isMetaTyVar tv1 ) - ASSERT( isBoxyTyVar tv1 || isTauTy ty2 ) - do { ASSERTM2( do { details <- readMetaTyVar tv1; return (isFlexi details) }, ppr tv1 ) - ; traceTc (text "updateMeta" <+> ppr tv1 <+> text ":=" <+> ppr ty2) - ; writeMutVar ref1 (Indirect ty2) } - ----------------- -checkKinds swapped tv1 ty2 --- We're about to unify a type variable tv1 with a non-tyvar-type ty2. --- ty2 has been zonked at this stage, which ensures that --- its kind has as much boxity information visible as possible. - | tk2 `isSubKind` tk1 = returnM () - - | otherwise - -- Either the kinds aren't compatible - -- (can happen if we unify (a b) with (c d)) - -- or we are unifying a lifted type variable with an - -- unlifted type: e.g. (id 3#) is illegal - = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $ - unifyKindMisMatch k1 k2 - where - (k1,k2) | swapped = (tk2,tk1) - | otherwise = (tk1,tk2) - tk1 = tyVarKind tv1 - tk2 = typeKind ty2 - ----------------- -checkTauTvUpdate :: TcTyVar -> TcType -> TcM TcType --- (checkTauTvUpdate tv ty) --- We are about to update the TauTv tv with ty. --- Check (a) that tv doesn't occur in ty (occurs check) --- (b) that ty is a monotype --- Furthermore, in the interest of (b), if you find an --- empty box (BoxTv that is Flexi), fill it in with a TauTv --- --- Returns the (non-boxy) type to update the type variable with, or fails - -checkTauTvUpdate orig_tv orig_ty - = go orig_ty - where - go (TyConApp tc tys) - | isSynTyCon tc = go_syn tc tys - | otherwise = do { tys' <- mappM go tys; return (TyConApp tc tys') } - go (NoteTy _ ty2) = go ty2 -- Discard free-tyvar annotations - go (PredTy p) = do { p' <- go_pred p; return (PredTy p') } - go (FunTy arg res) = do { arg' <- go arg; res' <- go res; return (FunTy arg' res') } - go (AppTy fun arg) = do { fun' <- go fun; arg' <- go arg; return (mkAppTy fun' arg') } - -- NB the mkAppTy; we might have instantiated a - -- type variable to a type constructor, so we need - -- to pull the TyConApp to the top. - go (ForAllTy tv ty) = notMonoType orig_ty -- (b) - - go (TyVarTy tv) - | orig_tv == tv = occurCheck tv orig_ty -- (a) - | isTcTyVar tv = go_tyvar tv (tcTyVarDetails tv) - | otherwise = return (TyVarTy tv) - -- Ordinary (non Tc) tyvars - -- occur inside quantified types - - go_pred (ClassP c tys) = do { tys' <- mapM go tys; return (ClassP c tys') } - go_pred (IParam n ty) = do { ty' <- go ty; return (IParam n ty') } - - go_tyvar tv (SkolemTv _) = return (TyVarTy tv) - go_tyvar tv (MetaTv box ref) - = do { cts <- readMutVar ref - ; case cts of - Indirect ty -> go ty - Flexi -> case box of - BoxTv -> fillBoxWithTau tv ref - other -> return (TyVarTy tv) - } - - -- go_syn is called for synonyms only - -- See Note [Type synonyms and the occur check] - go_syn tc tys - | not (isTauTyCon tc) - = notMonoType orig_ty -- (b) again - | otherwise - = do { (msgs, mb_tys') <- tryTc (mapM go tys) - ; case mb_tys' of - Just tys' -> return (TyConApp tc tys') - -- Retain the synonym (the common case) - Nothing -> go (expectJust "checkTauTvUpdate" - (tcView (TyConApp tc tys))) - -- Try again, expanding the synonym - } - -fillBoxWithTau :: BoxyTyVar -> IORef MetaDetails -> TcM TcType --- (fillBoxWithTau tv ref) fills ref with a freshly allocated --- tau-type meta-variable, whose print-name is the same as tv --- Choosing the same name is good: when we instantiate a function --- we allocate boxy tyvars with the same print-name as the quantified --- tyvar; and then we often fill the box with a tau-tyvar, and again --- we want to choose the same name. -fillBoxWithTau tv ref - = do { tv' <- tcInstTyVar tv -- Do not gratuitously forget - ; let tau = mkTyVarTy tv' -- name of the type variable - ; writeMutVar ref (Indirect tau) - ; return tau } \end{code} -Note [Type synonyms and the occur check] -~~~~~~~~~~~~~~~~~~~~ -Basically we want to update tv1 := ps_ty2 -because ps_ty2 has type-synonym info, which improves later error messages - -But consider - type A a = () - - f :: (A a -> a -> ()) -> () - f = \ _ -> () - - x :: () - x = f (\ x p -> p x) - -In the application (p x), we try to match "t" with "A t". If we go -ahead and bind t to A t (= ps_ty2), we'll lead the type checker into -an infinite loop later. -But we should not reject the program, because A t = (). -Rather, we should bind t to () (= non_var_ty2). - \begin{code} -stripBoxyType :: BoxyType -> TcM TcType --- Strip all boxes from the input type, returning a non-boxy type. --- It's fine for there to be a polytype inside a box (c.f. unBox) --- All of the boxes should have been filled in by now; --- hence we return a TcType -stripBoxyType ty = zonkType strip_tv ty - where - strip_tv tv = ASSERT( not (isBoxyTyVar tv) ) return (TyVarTy tv) - -- strip_tv will be called for *Flexi* meta-tyvars - -- There should not be any Boxy ones; hence the ASSERT +refineBox :: TcType -> TcM TcType +-- Unbox the outer box of a boxy type (if any) +refineBox ty@(TyVarTy box_tv) + | isMetaTyVar box_tv + = do { cts <- readMetaTyVar box_tv + ; case cts of + Flexi -> return ty + Indirect ty -> return ty } +refineBox other_ty = return other_ty + +refineBoxToTau :: TcType -> TcM TcType +-- Unbox the outer box of a boxy type, filling with a monotype if it is empty +-- Like refineBox except for the "fill with monotype" part. +refineBoxToTau ty@(TyVarTy box_tv) + | isMetaTyVar box_tv + , MetaTv BoxTv ref <- tcTyVarDetails box_tv + = do { cts <- readMutVar ref + ; case cts of + Flexi -> fillBoxWithTau box_tv ref + Indirect ty -> return ty } +refineBoxToTau other_ty = return other_ty zapToMonotype :: BoxySigmaType -> TcM TcTauType -- Subtle... we must zap the boxy res_ty @@ -1425,7 +1659,6 @@ unBox :: BoxyType -> TcM TcType -- -- For once, it's safe to treat synonyms as opaque! -unBox (NoteTy n ty) = do { ty' <- unBox ty; return (NoteTy n ty') } unBox (TyConApp tc tys) = do { tys' <- mapM unBox tys; return (TyConApp tc tys') } unBox (AppTy f a) = do { f' <- unBox f; a' <- unBox a; return (mkAppTy f' a') } unBox (FunTy f a) = do { f' <- unBox f; a' <- unBox a; return (FunTy f' a') } @@ -1437,7 +1670,7 @@ unBox (TyVarTy tv) , MetaTv BoxTv ref <- tcTyVarDetails tv -- NB: non-TcTyVars are possible = do { cts <- readMutVar ref -- under nested quantifiers ; case cts of - Flexi -> fillBoxWithTau tv ref + Flexi -> fillBoxWithTau tv ref Indirect ty -> do { non_boxy_ty <- unBox ty ; if isTauTy non_boxy_ty then return non_boxy_ty @@ -1448,20 +1681,28 @@ unBox (TyVarTy tv) unBoxPred (ClassP cls tys) = do { tys' <- mapM unBox tys; return (ClassP cls tys') } unBoxPred (IParam ip ty) = do { ty' <- unBox ty; return (IParam ip ty') } +unBoxPred (EqPred ty1 ty2) = do { ty1' <- unBox ty1; ty2' <- unBox ty2; return (EqPred ty1' ty2') } \end{code} %************************************************************************ %* * -\subsection[Unify-context]{Errors and contexts} + Errors and contexts %* * %************************************************************************ -Errors -~~~~~~ - \begin{code} +unifyMisMatch :: Outer -> TcM a +unifyMisMatch (Unify is_outer ty1 ty2) + | is_outer = popErrCtxt $ failWithMisMatch ty1 ty2 -- This is the whole point of the 'outer' stuff + | otherwise = failWithMisMatch ty1 ty2 + +popUnifyCtxt :: Outer -> TcM a -> TcM a +popUnifyCtxt (Unify True _ _) thing = popErrCtxt thing +popUnifyCtxt (Unify False _ _) thing = thing + +----------------------- unifyCtxt act_ty exp_ty tidy_env = do { act_ty' <- zonkTcType act_ty ; exp_ty' <- zonkTcType exp_ty @@ -1477,98 +1718,45 @@ mkExpectedActualMsg act_ty exp_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. -subCtxt mb_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'' +addSubCtxt orig actual_res_ty expected_res_ty thing_inside + = addErrCtxtM mk_err thing_inside + where + mk_err 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 + len_act_args = length act_args + len_exp_args = length exp_args - message = case mb_fun of - Just fun | len_exp_args < len_act_args -> wrongArgsCtxt "too few" fun - | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun - other -> mkExpectedActualMsg act_ty'' exp_ty'' - ; return (env2, message) } + message = case orig of + OccurrenceOf fun + | len_exp_args < len_act_args -> wrongArgsCtxt "too few" fun + | len_exp_args > len_act_args -> wrongArgsCtxt "too many" fun + other -> 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 +unifyForAllCtxt tvs phi1 phi2 env + = return (env2, 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 || isSigTyVar 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") <+> quotes (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:") + (env', tvs') = tidyOpenTyVars env tvs -- NB: not tidyTyVarBndrs + (env1, phi1') = tidyOpenType env' phi1 + (env2, phi2') = tidyOpenType env1 phi2 + msg = vcat [ptext SLIT("When matching") <+> quotes (ppr (mkForAllTys tvs' phi1')), + ptext SLIT(" and") <+> quotes (ppr (mkForAllTys tvs' phi2'))] \end{code} + %************************************************************************ %* * Kind unification @@ -1581,46 +1769,41 @@ Unifying kinds is much, much simpler than unifying types. unifyKind :: TcKind -- Expected -> TcKind -- Actual -> TcM () -unifyKind LiftedTypeKind LiftedTypeKind = returnM () -unifyKind UnliftedTypeKind UnliftedTypeKind = returnM () +unifyKind (TyConApp kc1 []) (TyConApp kc2 []) + | isSubKindCon kc2 kc1 = return () -unifyKind OpenTypeKind k2 | isOpenTypeKind k2 = returnM () -unifyKind ArgTypeKind k2 | isArgTypeKind k2 = returnM () - -- Respect sub-kinding - -unifyKind (FunKind a1 r1) (FunKind a2 r2) - = do { unifyKind a2 a1; unifyKind r1 r2 } +unifyKind (FunTy a1 r1) (FunTy a2 r2) + = do { unifyKind a2 a1; unifyKind r1 r2 } -- Notice the flip in the argument, -- so that the sub-kinding works right - -unifyKind (KindVar kv1) k2 = uKVar False kv1 k2 -unifyKind k1 (KindVar kv2) = uKVar True kv2 k1 +unifyKind (TyVarTy kv1) k2 = uKVar False kv1 k2 +unifyKind k1 (TyVarTy kv2) = uKVar True kv2 k1 unifyKind k1 k2 = unifyKindMisMatch k1 k2 unifyKinds :: [TcKind] -> [TcKind] -> TcM () -unifyKinds [] [] = returnM () -unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_` - unifyKinds ks1 ks2 -unifyKinds _ _ = panic "unifyKinds: length mis-match" +unifyKinds [] [] = return () +unifyKinds (k1:ks1) (k2:ks2) = do unifyKind k1 k2 + unifyKinds ks1 ks2 +unifyKinds _ _ = panic "unifyKinds: length mis-match" ---------------- uKVar :: Bool -> KindVar -> TcKind -> TcM () uKVar swapped kv1 k2 = do { mb_k1 <- readKindVar kv1 ; case mb_k1 of - Nothing -> uUnboundKVar swapped kv1 k2 - Just k1 | swapped -> unifyKind k2 k1 - | otherwise -> unifyKind k1 k2 } + Flexi -> uUnboundKVar swapped kv1 k2 + Indirect k1 | swapped -> unifyKind k2 k1 + | otherwise -> unifyKind k1 k2 } ---------------- uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM () -uUnboundKVar swapped kv1 k2@(KindVar kv2) - | kv1 == kv2 = returnM () +uUnboundKVar swapped kv1 k2@(TyVarTy kv2) + | kv1 == kv2 = return () | otherwise -- Distinct kind variables = do { mb_k2 <- readKindVar kv2 ; case mb_k2 of - Just k2 -> uUnboundKVar swapped kv1 k2 - Nothing -> writeKindVar kv1 k2 } + Indirect k2 -> uUnboundKVar swapped kv1 k2 + Flexi -> writeKindVar kv1 k2 } uUnboundKVar swapped kv1 non_var_k2 = do { k2' <- zonkTcKind non_var_k2 @@ -1637,9 +1820,9 @@ uUnboundKVar swapped kv1 non_var_k2 kindOccurCheck kv1 k2 -- k2 is zonked = checkTc (not_in k2) (kindOccurCheckErr kv1 k2) where - not_in (KindVar kv2) = kv1 /= kv2 - not_in (FunKind a2 r2) = not_in a2 && not_in r2 - not_in other = True + not_in (TyVarTy kv2) = kv1 /= kv2 + not_in (FunTy a2 r2) = not_in a2 && not_in r2 + not_in other = True kindSimpleKind :: Bool -> Kind -> TcM SimpleKind -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k @@ -1649,14 +1832,16 @@ kindSimpleKind :: Bool -> Kind -> TcM SimpleKind kindSimpleKind orig_swapped orig_kind = go orig_swapped orig_kind where - go sw (FunKind k1 k2) = do { k1' <- go (not sw) k1 - ; k2' <- go sw k2 - ; return (FunKind k1' k2') } - go True OpenTypeKind = return liftedTypeKind - go True ArgTypeKind = return liftedTypeKind - go sw LiftedTypeKind = return liftedTypeKind - go sw UnliftedTypeKind = return unliftedTypeKind - go sw k@(KindVar _) = return k -- KindVars are always simple + go sw (FunTy k1 k2) = do { k1' <- go (not sw) k1 + ; k2' <- go sw k2 + ; return (mkArrowKind k1' k2') } + go True k + | isOpenTypeKind k = return liftedTypeKind + | isArgTypeKind k = return liftedTypeKind + go sw k + | isLiftedTypeKind k = return liftedTypeKind + | isUnliftedTypeKind k = return unliftedTypeKind + go sw k@(TyVarTy _) = return k -- KindVars are always simple go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:") <+> ppr orig_swapped <+> ppr orig_kind) -- I think this can't actually happen @@ -1668,34 +1853,24 @@ kindSimpleKind orig_swapped orig_kind kindOccurCheckErr tyvar ty = hang (ptext SLIT("Occurs check: cannot construct the infinite kind:")) 2 (sep [ppr tyvar, char '=', ppr ty]) - -unifyKindMisMatch ty1 ty2 - = zonkTcKind ty1 `thenM` \ ty1' -> - zonkTcKind ty2 `thenM` \ ty2' -> - let - msg = hang (ptext SLIT("Couldn't match kind")) - 2 (sep [quotes (ppr ty1'), - ptext SLIT("against"), - quotes (ppr ty2')]) - in - failWithTc msg \end{code} \begin{code} unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind)) -- Like unifyFunTy, but does not fail; instead just returns Nothing -unifyFunKind (KindVar kvar) - = readKindVar kvar `thenM` \ maybe_kind -> +unifyFunKind (TyVarTy kvar) = do + maybe_kind <- readKindVar kvar case maybe_kind of - Just fun_kind -> unifyFunKind fun_kind - Nothing -> do { arg_kind <- newKindVar - ; res_kind <- newKindVar - ; writeKindVar kvar (mkArrowKind arg_kind res_kind) - ; returnM (Just (arg_kind,res_kind)) } + Indirect fun_kind -> unifyFunKind fun_kind + Flexi -> + do { arg_kind <- newKindVar + ; res_kind <- newKindVar + ; writeKindVar kvar (mkArrowKind arg_kind res_kind) + ; return (Just (arg_kind,res_kind)) } -unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind)) -unifyFunKind other = returnM Nothing +unifyFunKind (FunTy arg_kind res_kind) = return (Just (arg_kind,res_kind)) +unifyFunKind other = return Nothing \end{code} %************************************************************************ @@ -1716,52 +1891,55 @@ unifyFunKind other = returnM Nothing checkExpectedKind :: Outputable a => a -> TcKind -> TcKind -> TcM () -- A fancy wrapper for 'unifyKind', which tries -- to give decent error messages. +-- (checkExpectedKind ty act_kind exp_kind) +-- checks that the actual kind act_kind is compatible +-- with the expected kind exp_kind +-- The first argument, ty, is used only in the error message generation 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) -> - case mb_r of { - Just r -> returnM () ; -- Unification succeeded - Nothing -> + = return () + | otherwise = do + (_errs, mb_r) <- tryTc (unifyKind exp_kind act_kind) + case mb_r of + Just r -> return () ; -- Unification succeeded + Nothing -> do -- So there's definitely an error -- Now to find out what sort - zonkTcKind exp_kind `thenM` \ exp_kind -> - zonkTcKind act_kind `thenM` \ act_kind -> - - tcInitTidyEnv `thenM` \ env0 -> - let (exp_as, _) = splitKindFunTys exp_kind - (act_as, _) = splitKindFunTys act_kind - n_exp_as = length exp_as - n_act_as = length act_as - - (env1, tidy_exp_kind) = tidyKind env0 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") - - -- Now n_exp_as >= n_act_as. In the next two cases, - -- n_exp_as == 0, and hence so is n_act_as - | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind - = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty) - <+> ptext SLIT("is unlifted") - - | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind - = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty) - <+> ptext SLIT("is lifted") - - | otherwise -- E.g. Monad [Int] - = 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 - failWithTcM (env2, err $$ more_info) - } + exp_kind <- zonkTcKind exp_kind + act_kind <- zonkTcKind act_kind + + env0 <- tcInitTidyEnv + let (exp_as, _) = splitKindFunTys exp_kind + (act_as, _) = splitKindFunTys act_kind + n_exp_as = length exp_as + n_act_as = length act_as + + (env1, tidy_exp_kind) = tidyKind env0 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") + + -- Now n_exp_as >= n_act_as. In the next two cases, + -- n_exp_as == 0, and hence so is n_act_as + | isLiftedTypeKind exp_kind && isUnliftedTypeKind act_kind + = ptext SLIT("Expecting a lifted type, but") <+> quotes (ppr ty) + <+> ptext SLIT("is unlifted") + + | isUnliftedTypeKind exp_kind && isLiftedTypeKind act_kind + = ptext SLIT("Expecting an unlifted type, but") <+> quotes (ppr ty) + <+> ptext SLIT("is lifted") + + | otherwise -- E.g. Monad [Int] + = 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)] + + failWithTcM (env2, err $$ more_info) \end{code} %************************************************************************ @@ -1815,7 +1993,7 @@ check_sig_tyvars -- Guaranteed to be skolems -> TcM () check_sig_tyvars extra_tvs [] - = returnM () + = return () check_sig_tyvars extra_tvs sig_tvs = ASSERT( all isSkolemTyVar sig_tvs ) do { gbl_tvs <- tcGetGlobalTyVars @@ -1824,8 +2002,8 @@ check_sig_tyvars extra_tvs sig_tvs text "extra_tvs" <+> ppr extra_tvs])) ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs - ; ifM (any (`elemVarSet` env_tvs) sig_tvs) - (bleatEscapedTvs env_tvs sig_tvs sig_tvs) + ; when (any (`elemVarSet` env_tvs) sig_tvs) + (bleatEscapedTvs env_tvs sig_tvs sig_tvs) } bleatEscapedTvs :: TcTyVarSet -- The global tvs @@ -1850,7 +2028,7 @@ bleatEscapedTvs globals sig_tvs zonked_tvs | not (zonked_tv `elemVarSet` globals) = return (tidy_env, msgs) | otherwise = do { (tidy_env1, globs) <- findGlobals (unitVarSet zonked_tv) tidy_env - ; returnM (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) } + ; return (tidy_env1, escape_msg sig_tv zonked_tv globs : msgs) } ----------------------- escape_msg sig_tv zonked_tv globs @@ -1874,8 +2052,8 @@ These two context are used with checkSigTyVars \begin{code} sigCtxt :: Id -> [TcTyVar] -> TcThetaType -> TcTauType -> TidyEnv -> TcM (TidyEnv, Message) -sigCtxt id sig_tvs sig_theta sig_tau tidy_env - = zonkTcType sig_tau `thenM` \ actual_tau -> +sigCtxt id sig_tvs sig_theta sig_tau tidy_env = do + actual_tau <- zonkTcType sig_tau let (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau) @@ -1885,6 +2063,6 @@ sigCtxt id sig_tvs sig_theta sig_tau tidy_env ] msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id), nest 2 sub_msg] - in - returnM (env3, msg) + + return (env3, msg) \end{code}