X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcUnify.lhs;h=8cd2a0b73890a5ec6683b06da32270d4009380c1;hb=ac10f8408520a30e8437496d320b8b86afda2e8f;hp=d5323d82b9785fe4296daf467cf6506b019027e8;hpb=16e4ce4c0c02650082f2e11982017c903c549ad5;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index d5323d8..8cd2a0b 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -6,68 +6,78 @@ \begin{code} module TcUnify ( -- Full-blown subsumption - tcSubOff, tcSubExp, tcGen, - checkSigTyVars, checkSigTyVarsWrt, sigCtxt, findGlobals, + tcSubExp, tcGen, + checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt, -- Various unifications - unifyTauTy, unifyTauTyList, unifyTauTyLists, - unifyKind, unifyKinds, unifyOpenTypeKind, unifyFunKind, + unifyType, unifyTypeList, unifyTheta, + unifyKind, unifyKinds, unifyFunKind, + checkExpectedKind, + boxySubMatchType, boxyMatchTypes, -------------------------------- -- Holes - Expected(..), newHole, readExpectedType, - zapExpectedType, zapExpectedTo, zapExpectedBranches, - subFunTys, unifyFunTy, - zapToListTy, unifyListTy, - zapToPArrTy, unifyPArrTy, - zapToTupleTy, unifyTupleTy - + tcInfer, subFunTys, unBox, stripBoxyType, withBox, + boxyUnify, boxyUnifyList, zapToMonotype, + boxySplitListTy, boxySplitTyConApp, boxySplitAppTy, + wrapFunResCoercion ) where #include "HsVersions.h" +import HsSyn ( ExprCoFn(..), idCoercion, isIdCoercion, (<.>) ) +import TypeRep ( Type(..), PredType(..) ) -import HsSyn ( HsExpr(..) ) -import TcHsSyn ( mkHsLet, - ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) ) -import TypeRep ( Type(..), SourceType(..), TyNote(..), openKindCon ) - -import TcRnMonad -- TcType, amongst others -import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType, - TcTyVarSet, TcThetaType, TyVarDetails(SigTv), - isTauTy, isSigmaTy, mkFunTys, - tcSplitAppTy_maybe, tcSplitTyConApp_maybe, - tcGetTyVar_maybe, tcGetTyVar, - mkFunTy, tyVarsOfType, mkPhiTy, - typeKind, tcSplitFunTy_maybe, mkForAllTys, - isSkolemTyVar, isUserTyVar, - tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars, - eqKind, openTypeKind, liftedTypeKind, isTypeKind, mkArrowKind, - hasMoreBoxityInfo, allDistinctTyVars - ) -import Inst ( newDicts, instToId, tcInstCall ) -import TcMType ( getTcTyVar, putTcTyVar, tcInstType, newKindVar, - newTyVarTy, newTyVarTys, newOpenTypeKind, - zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV ) +import TcMType ( lookupTcTyVar, LookupTyVarResult(..), + tcInstSkolType, newKindVar, newMetaTyVar, + tcInstBoxy, newBoxyTyVar, readFilledBox, + readMetaTyVar, writeMetaTyVar, newFlexiTyVarTy, + tcInstSkolTyVars, + zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV, + readKindVar, writeKindVar ) import TcSimplify ( tcSimplifyCheck ) -import TysWiredIn ( listTyCon, parrTyCon, mkListTy, mkPArrTy, mkTupleTy ) import TcEnv ( tcGetGlobalTyVars, findGlobals ) -import TyCon ( tyConArity, isTupleTyCon, tupleTyConBoxity ) -import PprType ( pprType ) +import TcIface ( checkWiredInTyCon ) +import TcRnMonad -- TcType, amongst others +import TcType ( TcKind, TcType, TcTyVar, TcTauType, + BoxySigmaType, BoxyRhoType, BoxyType, + TcTyVarSet, TcThetaType, TcTyVarDetails(..), BoxInfo(..), + SkolemInfo( GenSkol, UnkSkol ), MetaDetails(..), isImmutableTyVar, + pprSkolTvBinding, isTauTy, isTauTyCon, isSigmaTy, + mkFunTy, mkFunTys, mkTyConApp, isMetaTyVar, + tcSplitForAllTys, tcSplitAppTy_maybe, mkTyVarTys, + tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, + typeKind, mkForAllTys, mkAppTy, isBoxyTyVar, + tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars, + pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar, tcView, + TvSubst, mkTvSubst, zipTyEnv, substTy, emptyTvSubst, + lookupTyVar, extendTvSubst ) +import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind, + openTypeKind, liftedTypeKind, 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 ) -import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems ) +import Var ( Var, varName, tyVarKind, isTcTyVar, tcTyVarDetails ) +import VarSet ( emptyVarSet, mkVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems, + extendVarSet, intersectsVarSet ) import VarEnv import Name ( isSystemName ) import ErrUtils ( Message ) -import BasicTypes ( Boxity, Arity, isBoxed ) -import Util ( equalLength, lengthExceeds, notNull ) +import Maybes ( fromJust ) +import BasicTypes ( Arity ) +import UniqSupply ( uniqsFromSupply ) +import Util ( notNull, equalLength ) import Outputable -\end{code} -Notes on holes -~~~~~~~~~~~~~~ -* A hole is always filled in with an ordinary type, not another hole. +-- Assertion imports +#ifdef DEBUG +import TcType ( isBoxyTy, isFlexi ) +#endif +\end{code} %************************************************************************ %* * @@ -76,207 +86,393 @@ Notes on holes %************************************************************************ \begin{code} -data Expected ty = Infer (TcRef ty) -- The hole to fill in for type inference - | Check ty -- The type to check during type checking - -newHole :: TcM (TcRef ty) -newHole = newMutVar (error "Empty hole in typechecker") - -readExpectedType :: Expected ty -> TcM ty -readExpectedType (Infer hole) = readMutVar hole -readExpectedType (Check ty) = returnM ty - -zapExpectedType :: Expected TcType -> TcM TcTauType --- In the inference case, ensure we have a monotype -zapExpectedType (Infer hole) - = do { ty <- newTyVarTy openTypeKind ; - writeMutVar hole ty ; - return ty } - -zapExpectedType (Check ty) = return ty - -zapExpectedTo :: Expected TcType -> TcTauType -> TcM () -zapExpectedTo (Infer hole) ty2 = writeMutVar hole ty2 -zapExpectedTo (Check ty1) ty2 = unifyTauTy ty1 ty2 - -zapExpectedBranches :: [a] -> Expected TcType -> TcM (Expected TcType) --- Zap the expected type to a monotype if there is more than one branch -zapExpectedBranches branches exp_ty - | lengthExceeds branches 1 = zapExpectedType exp_ty `thenM` \ exp_ty' -> - return (Check exp_ty') - | otherwise = returnM exp_ty - -instance Outputable ty => Outputable (Expected ty) where - ppr (Check ty) = ptext SLIT("Expected type") <+> ppr ty - ppr (Infer hole) = ptext SLIT("Inferring type") +tcInfer :: (BoxyType -> TcM a) -> TcM (a, TcType) +tcInfer tc_infer + = do { box <- newBoxyTyVar + ; res <- tc_infer (mkTyVarTy box) + ; res_ty <- readFilledBox box -- Guaranteed filled-in by now + ; return (res, res_ty) } \end{code} %************************************************************************ %* * -\subsection[Unify-fun]{@unifyFunTy@} + subFunTys %* * %************************************************************************ -@subFunTy@ and @unifyFunTy@ is used to avoid the fruitless -creation of type variables. +\begin{code} +subFunTys :: SDoc -- Somthing like "The function f has 3 arguments" + -- or "The abstraction (\x.e) takes 1 argument" + -> Arity -- Expected # of args + -> BoxyRhoType -- res_ty + -> ([BoxySigmaType] -> BoxyRhoType -> TcM a) + -> TcM (ExprCoFn, 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 +-- +-- Note that it takes a BoxyRho type, and guarantees to return a BoxyRhoType + -* subFunTy is used when we might be faced with a "hole" type variable, - in which case we should create two new holes. +{- Error messages from subFunTys -* unifyFunTy is used when we expect to encounter only "ordinary" - type variables, so we should create new ordinary type variables + The abstraction `\Just 1 -> ...' has two arguments + but its type `Maybe a -> a' has only one -\begin{code} -subFunTys :: [pat] - -> Expected TcRhoType -- Fail if ty isn't a function type - -> ([(pat, Expected TcRhoType)] -> Expected TcRhoType -> TcM a) - -> TcM a + The equation(s) for `f' have two arguments + but its type `Maybe a -> a' has only one -subFunTys pats (Infer hole) thing_inside - = -- This is the interesting case - mapM new_pat_hole pats `thenM` \ pats_w_holes -> - newHole `thenM` \ res_hole -> + The section `(f 3)' requires 'f' to take two arguments + but its type `Int -> Int' has only one - -- Do the business - thing_inside pats_w_holes (Infer res_hole) `thenM` \ answer -> + The function 'f' is applied to two arguments + but its type `Int -> Int' has only one +-} - -- Extract the answers - mapM read_pat_hole pats_w_holes `thenM` \ arg_tys -> - readMutVar res_hole `thenM` \ res_ty -> - -- Write the answer into the incoming hole - writeMutVar hole (mkFunTys arg_tys res_ty) `thenM_` +subFunTys error_herald n_pats res_ty thing_inside + = loop n_pats [] res_ty + where + -- In 'loop', the parameter 'arg_tys' accumulates + -- the arg types so far, in *reverse order* + 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 first, because we 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) } + 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) } + + loop n args_so_far (TyVarTy tv) + | not (isImmutableTyVar 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) } } + where + mk_res_ty (res_ty' : arg_tys') = mkFunTys arg_tys' res_ty' + kinds = openTypeKind : take n (repeat argTypeKind) + -- Note argTypeKind: the args can have an unboxed type, + -- but not an unboxed tuple. + + loop n args_so_far res_ty + = failWithTc (mk_msg (length args_so_far)) + + mk_msg n_actual + = error_herald <> comma $$ + sep [ptext SLIT("but its type") <+> quotes (pprType res_ty), + if n_actual == 0 then ptext SLIT("has none") + else ptext SLIT("has only") <+> speakN n_actual] +\end{code} - -- And return the answer - returnM answer +\begin{code} +---------------------- +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 + -- Precondition: never called with FunTyCon + -- Precondition: input type :: * + +boxySplitTyConApp tc orig_ty + = do { checkWiredInTyCon tc + ; loop (tyConArity tc) [] orig_ty } where - new_pat_hole pat = newHole `thenM` \ hole -> return (pat, Infer hole) - read_pat_hole (pat, Infer hole) = readMutVar hole + 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) + | tc == tycon + = ASSERT( n_req == length args) -- ty::* + return (args ++ args_so_far) + + loop n_req args_so_far (AppTy fun arg) + = loop (n_req - 1) (arg:args_so_far) fun + + loop n_req args_so_far (TyVarTy tv) + | not (isImmutableTyVar 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) } + } + where + mk_res_ty arg_tys' = mkTyConApp tc arg_tys' + arg_kinds = map tyVarKind (take n_req (tyConTyVars tc)) + + loop _ _ _ = boxySplitFailure (mkTyConApp tc (mkTyVarTys (tyConTyVars tc))) orig_ty + +---------------------- +boxySplitListTy :: BoxyRhoType -> TcM BoxySigmaType -- Special case for lists +boxySplitListTy exp_ty = do { [elt_ty] <- boxySplitTyConApp listTyCon exp_ty + ; return elt_ty } -subFunTys pats (Check ty) thing_inside - = go pats ty `thenM` \ (pats_w_tys, res_ty) -> - thing_inside pats_w_tys res_ty + +---------------------- +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 +-- If the incoming type is boxy, then so are the result types; and vice versa + +boxySplitAppTy orig_ty + = loop orig_ty where - go [] ty = return ([], Check ty) - go (pat:pats) ty = unifyFunTy ty `thenM` \ (arg,res) -> - go pats res `thenM` \ (pats_w_tys, final_res) -> - return ((pat, Check arg) : pats_w_tys, final_res) - -unifyFunTy :: TcRhoType -- Fail if ty isn't a function type - -> TcM (TcType, TcType) -- otherwise return arg and result types - -unifyFunTy ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Just ty' -> unifyFunTy ty' - Nothing -> unify_fun_ty_help ty - -unifyFunTy ty - = case tcSplitFunTy_maybe ty of - Just arg_and_res -> returnM arg_and_res - Nothing -> unify_fun_ty_help ty - -unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification - = newTyVarTy openTypeKind `thenM` \ arg -> - newTyVarTy openTypeKind `thenM` \ res -> - unifyTauTy ty (mkFunTy arg res) `thenM_` - returnM (arg,res) + loop ty + | Just ty' <- tcView ty = loop ty' + + loop ty + | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty + = return (fun_ty, arg_ty) + + loop (TyVarTy tv) + | not (isImmutableTyVar 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) } } + where + mk_res_ty [fun_ty', arg_ty'] = mkAppTy fun_ty' arg_ty' + tv_kind = tyVarKind tv + kinds = [mkArrowKind liftedTypeKind (defaultKind tv_kind), + -- m :: * -> k + liftedTypeKind] -- arg type :: * + -- The defaultKind is a bit smelly. If you remove it, + -- try compiling f x = do { x } + -- and you'll get a kind mis-match. It smells, but + -- not enough to lose sleep over. + + loop _ = boxySplitFailure (mkAppTy alphaTy betaTy) orig_ty + +------------------ +boxySplitFailure actual_ty expected_ty + = unifyMisMatch False actual_ty expected_ty \end{code} + +-------------------------------- +-- withBoxes: the key utility function +-------------------------------- + \begin{code} -zapToListTy :: Expected TcType -- expected list type - -> TcM TcType -- list element type - -zapToListTy (Check ty) = unifyListTy ty -zapToListTy (Infer hole) = do { elt_ty <- newTyVarTy liftedTypeKind ; - writeMutVar hole (mkListTy elt_ty) ; - return elt_ty } - -unifyListTy :: TcType -> TcM TcType -unifyListTy ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Just ty' -> unifyListTy ty' - other -> unify_list_ty_help ty - -unifyListTy ty - = case tcSplitTyConApp_maybe ty of - Just (tycon, [arg_ty]) | tycon == listTyCon -> returnM arg_ty - other -> unify_list_ty_help ty - -unify_list_ty_help ty -- Revert to ordinary unification - = newTyVarTy liftedTypeKind `thenM` \ elt_ty -> - unifyTauTy ty (mkListTy elt_ty) `thenM_` - returnM elt_ty - --- variant for parallel arrays --- -zapToPArrTy :: Expected TcType -- Expected list type - -> TcM TcType -- List element type - -zapToPArrTy (Check ty) = unifyPArrTy ty -zapToPArrTy (Infer hole) = do { elt_ty <- newTyVarTy liftedTypeKind ; - writeMutVar hole (mkPArrTy elt_ty) ; - return elt_ty } - -unifyPArrTy :: TcType -> TcM TcType - -unifyPArrTy ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Just ty' -> unifyPArrTy ty' - _ -> unify_parr_ty_help ty -unifyPArrTy ty - = case tcSplitTyConApp_maybe ty of - Just (tycon, [arg_ty]) | tycon == parrTyCon -> returnM arg_ty - _ -> unify_parr_ty_help ty - -unify_parr_ty_help ty -- Revert to ordinary unification - = newTyVarTy liftedTypeKind `thenM` \ elt_ty -> - unifyTauTy ty (mkPArrTy elt_ty) `thenM_` - returnM elt_ty +withMetaTvs :: TcTyVar -- An unfilled-in, non-skolem, meta type variable + -> [Kind] -- Make fresh boxes (with the same BoxTv/TauTv setting as tv) + -> ([BoxySigmaType] -> BoxySigmaType) + -- Constructs the type to assign + -- to the original var + -> TcM [BoxySigmaType] -- Return the fresh boxes + +-- It's entirely possible for the [kind] to be empty. +-- For example, when pattern-matching on True, +-- we call boxySplitTyConApp passing a boolTyCon + +-- Invariant: tv is still Flexi + +withMetaTvs tv kinds mk_res_ty + | isBoxyTyVar tv + = do { box_tvs <- mapM (newMetaTyVar BoxTv) kinds + ; let box_tys = mkTyVarTys box_tvs + ; writeMetaTyVar tv (mk_res_ty box_tys) + ; return box_tys } + + | otherwise -- Non-boxy meta type variable + = do { tau_tys <- mapM newFlexiTyVarTy kinds + ; writeMetaTyVar tv (mk_res_ty tau_tys) -- Write it *first* + -- Sure to be a tau-type + ; return tau_tys } + +withBox :: Kind -> (BoxySigmaType -> TcM a) -> TcM (a, TcType) +-- Allocate a *boxy* tyvar +withBox kind thing_inside + = do { box_tv <- newMetaTyVar BoxTv kind + ; res <- thing_inside (mkTyVarTy box_tv) + ; ty <- readFilledBox box_tv + ; return (res, ty) } \end{code} + +%************************************************************************ +%* * + Approximate boxy matching +%* * +%************************************************************************ + \begin{code} -zapToTupleTy :: Boxity -> Arity -> Expected TcType -> TcM [TcType] -zapToTupleTy boxity arity (Check ty) = unifyTupleTy boxity arity ty -zapToTupleTy boxity arity (Infer hole) = do { (tup_ty, arg_tys) <- new_tuple_ty boxity arity ; - writeMutVar hole tup_ty ; - return arg_tys } - -unifyTupleTy boxity arity ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Just ty' -> unifyTupleTy boxity arity ty' - other -> unify_tuple_ty_help boxity arity ty - -unifyTupleTy boxity arity ty - = case tcSplitTyConApp_maybe ty of - Just (tycon, arg_tys) - | isTupleTyCon tycon - && tyConArity tycon == arity - && tupleTyConBoxity tycon == boxity - -> returnM arg_tys - other -> unify_tuple_ty_help boxity arity ty - -unify_tuple_ty_help boxity arity ty - = new_tuple_ty boxity arity `thenM` \ (tup_ty, arg_tys) -> - unifyTauTy ty tup_ty `thenM_` - returnM arg_tys - -new_tuple_ty boxity arity - = newTyVarTys arity kind `thenM` \ arg_tys -> - return (mkTupleTy boxity arity arg_tys, arg_tys) +boxySubMatchType + :: TcTyVarSet -> TcType -- The "template"; the tyvars are skolems + -> BoxyRhoType -- Type to match (note a *Rho* type) + -> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes + +boxyMatchTypes + :: TcTyVarSet -> [TcType] -- The "template"; the tyvars are skolems + -> [BoxySigmaType] -- Type to match + -> TvSubst -- Substitution of the [TcTyVar] to BoxySigmaTypes + +-- Find a *boxy* substitution that makes the template look as much +-- like the BoxySigmaType as possible. +-- It's always ok to return an empty substitution; +-- anything more is jam on the pudding +-- +-- NB1: This is a pure, non-monadic function. +-- It does no unification, and cannot fail +-- +-- Note [Matching kinds] +-- The target type might legitimately not be a sub-kind of template. +-- For example, suppose the target is simply a box with an OpenTypeKind, +-- and the template is a type variable with LiftedTypeKind. +-- Then it's ok (because the target type will later be refined). +-- We simply don't bind the template type variable. +-- +-- It might also be that the kind mis-match is an error. For example, +-- suppose we match the template (a -> Int) against (Int# -> Int), +-- where the template type variable 'a' has LiftedTypeKind. This +-- matching function does not fail; it simply doesn't bind the template. +-- Later stuff will fail. +-- +-- Precondition: the arg lengths are equal +-- Precondition: none of the template type variables appear in the [BoxySigmaType] +-- Precondition: any nested quantifiers in either type differ from +-- the template type variables passed as arguments +-- +-- Note [Sub-match] +-- ~~~~~~~~~~~~~~~~ +-- Consider this +-- head :: [a] -> a +-- |- head xs : +-- We will do a boxySubMatchType between a ~ +-- But we *don't* want to match [a |-> ] because +-- (a) The box should be filled in with a rho-type, but +-- but the returned substitution maps TyVars to boxy *sigma* +-- types +-- (b) In any case, the right final answer might be *either* +-- instantiate 'a' with a rho-type or a sigma type +-- head xs : Int vs head xs : forall b. b->b +-- So the matcher MUST NOT make a choice here. In general, we only +-- bind a template type variable in boxyMatchType, not in boxySubMatchType. + +boxySubMatchType tmpl_tvs tmpl_ty boxy_ty + = go tmpl_ty boxy_ty + where + go t_ty b_ty + | Just t_ty' <- tcView t_ty = go t_ty' b_ty + | Just b_ty' <- tcView b_ty = go t_ty b_ty' + + go (FunTy arg1 res1) (FunTy arg2 res2) + = do_match arg1 arg2 (go res1 res2) + -- Match the args, and sub-match the results + + go (TyVarTy _) b_ty = emptyTvSubst -- Do not bind! See Note [Sub-match] + + go t_ty b_ty = do_match t_ty b_ty emptyTvSubst -- Otherwise we are safe to bind + + do_match t_ty b_ty subst = boxy_match tmpl_tvs t_ty emptyVarSet b_ty subst + +------------ +boxyMatchTypes tmpl_tvs tmpl_tys boxy_tys + = ASSERT( length tmpl_tys == length boxy_tys ) + boxy_match_s tmpl_tvs tmpl_tys emptyVarSet boxy_tys emptyTvSubst + -- ToDo: add error context? + +boxy_match_s tmpl_tvs [] boxy_tvs [] subst + = subst +boxy_match_s tmpl_tvs (t_ty:t_tys) boxy_tvs (b_ty:b_tys) subst + = boxy_match_s tmpl_tvs t_tys boxy_tvs b_tys $ + boxy_match tmpl_tvs t_ty boxy_tvs b_ty subst + +------------ +boxy_match :: TcTyVarSet -> TcType -- Template + -> TcTyVarSet -- boxy_tvs: do not bind template tyvars to any of these + -> BoxySigmaType -- Match against this type + -> TvSubst + -> TvSubst + +-- The boxy_tvs argument prevents this match: +-- [a] forall b. a ~ forall b. b +-- We don't want to bind the template variable 'a' +-- to the quantified type variable 'b'! + +boxy_match tmpl_tvs orig_tmpl_ty boxy_tvs orig_boxy_ty subst + = go orig_tmpl_ty orig_boxy_ty where - kind | isBoxed boxity = liftedTypeKind - | otherwise = openTypeKind + go t_ty b_ty + | Just t_ty' <- tcView t_ty = go t_ty' b_ty + | Just b_ty' <- tcView b_ty = go t_ty b_ty' + + go (ForAllTy _ ty1) (ForAllTy tv2 ty2) + = boxy_match tmpl_tvs ty1 (boxy_tvs `extendVarSet` tv2) ty2 subst + + go (TyConApp tc1 tys1) (TyConApp tc2 tys2) + | tc1 == tc2 = go_s tys1 tys2 + + go (FunTy arg1 res1) (FunTy arg2 res2) + = go_s [arg1,res1] [arg2,res2] + + go t_ty b_ty + | Just (s1,t1) <- tcSplitAppTy_maybe t_ty, + Just (s2,t2) <- tcSplitAppTy_maybe b_ty, + typeKind t2 `isSubKind` typeKind t1 -- Maintain invariant + = go_s [s1,t1] [s2,t2] + + go (TyVarTy tv) b_ty + | tv `elemVarSet` tmpl_tvs -- Template type variable in the template + , not (intersectsVarSet boxy_tvs (tyVarsOfType orig_boxy_ty)) + , typeKind b_ty `isSubKind` tyVarKind tv + = extendTvSubst subst tv boxy_ty' + where + boxy_ty' = case lookupTyVar subst tv of + Nothing -> orig_boxy_ty + Just ty -> ty `boxyLub` orig_boxy_ty + + go _ _ = subst -- Always safe + + -------- + go_s tys1 tys2 = boxy_match_s tmpl_tvs tys1 boxy_tvs tys2 subst + + +boxyLub :: BoxySigmaType -> BoxySigmaType -> BoxySigmaType +-- Combine boxy information from the two types +-- If there is a conflict, return the first +boxyLub orig_ty1 orig_ty2 + = go orig_ty1 orig_ty2 + where + go (AppTy f1 a1) (AppTy f2 a2) = AppTy (boxyLub f1 f2) (boxyLub a1 a2) + go (FunTy f1 a1) (FunTy f2 a2) = AppTy (boxyLub f1 f2) (boxyLub a1 a2) + go (TyConApp tc1 ts1) (TyConApp tc2 ts2) + | tc1 == tc2, length ts1 == length ts2 + = TyConApp tc1 (zipWith boxyLub ts1 ts2) + + go (TyVarTy tv1) ty2 -- This is the whole point; + | isTcTyVar tv1, isMetaTyVar tv1 -- choose ty2 if ty2 is a box + = ty2 + + -- 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' + + -- For now, we don't look inside ForAlls, PredTys + go ty1 ty2 = orig_ty1 -- Default \end{code} %************************************************************************ %* * -\subsection{Subsumption} + Subsumption checking %* * %************************************************************************ @@ -295,62 +491,40 @@ which takes an HsExpr of type offered_ty into one of type expected_ty. \begin{code} -tcSubExp :: Expected TcRhoType -> TcRhoType -> TcM ExprCoFn -tcSubOff :: TcSigmaType -> Expected TcSigmaType -> TcM ExprCoFn -\end{code} - -These two check for holes - -\begin{code} -tcSubExp expected_ty offered_ty - = traceTc (text "tcSubExp" <+> (ppr expected_ty $$ ppr offered_ty)) `thenM_` - checkHole expected_ty offered_ty tcSub - -tcSubOff expected_ty offered_ty - = checkHole offered_ty expected_ty (\ off exp -> tcSub exp off) - --- checkHole looks for a hole in its first arg; --- If so, and it is uninstantiated, it fills in the hole --- with its second arg --- Otherwise it calls thing_inside, passing the two args, looking --- through any instantiated hole - -checkHole (Infer hole) other_ty thing_inside - = do { writeMutVar hole other_ty; return idCoercion } - -checkHole (Check ty) other_ty thing_inside - = thing_inside ty other_ty -\end{code} - -No holes expected now. Add some error-check context info. - -\begin{code} -tcSub :: TcSigmaType -> TcSigmaType -> TcM ExprCoFn -- Locally used only -tcSub expected_ty actual_ty +----------------- +tcSubExp :: BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn -- Locally used only + -- (tcSub act exp) checks that + -- act <= exp +tcSubExp actual_ty expected_ty = traceTc (text "tcSub" <+> details) `thenM_` - addErrCtxtM (unifyCtxt "type" expected_ty actual_ty) - (tc_sub expected_ty expected_ty actual_ty actual_ty) + addErrCtxtM (unifyCtxt "type" actual_ty expected_ty) + (tc_sub actual_ty actual_ty expected_ty expected_ty) where details = vcat [text "Expected:" <+> ppr expected_ty, text "Actual: " <+> ppr actual_ty] -\end{code} -tc_sub carries the types before and after expanding type synonyms - -\begin{code} -tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms - -> TcSigmaType -- ..and after - -> TcSigmaType -- actual_ty, before - -> TcSigmaType -- ..and after +----------------- +tc_sub :: BoxySigmaType -- actual_ty, before expanding synonyms + -> BoxySigmaType -- ..and after + -> BoxySigmaType -- expected_ty, before + -> BoxySigmaType -- ..and after -> TcM ExprCoFn +tc_sub act_sty act_ty exp_sty exp_ty + | Just exp_ty' <- tcView exp_ty = tc_sub act_sty act_ty exp_sty exp_ty' +tc_sub act_sty act_ty exp_sty exp_ty + | Just act_ty' <- tcView act_ty = tc_sub act_sty act_ty' exp_sty exp_ty + ----------------------------------- --- Expand synonyms -tc_sub exp_sty (NoteTy _ exp_ty) act_sty act_ty = tc_sub exp_sty exp_ty act_sty act_ty -tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty act_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_sub act_sty (TyVarTy tv) exp_sty exp_ty + = do { uVar False tv False exp_sty exp_ty + ; return idCoercion } ----------------------------------- --- Generalisation case +-- Skolemisation case (rule SKOL) -- actual_ty: d:Eq b => b->b -- expected_ty: forall a. Ord a => a->a -- co_fn e /\a. \d2:Ord a. let d = eqFromOrd d2 in e @@ -360,128 +534,78 @@ tc_sub exp_sty exp_ty act_sty (NoteTy _ act_ty) = tc_sub exp_sty exp_ty act_sty -- g :: Ord b => b->b -- Consider f g ! -tc_sub exp_sty expected_ty act_sty actual_ty - | isSigmaTy expected_ty - = tcGen expected_ty (tyVarsOfType actual_ty) ( - -- It's really important to check for escape wrt the free vars of - -- both expected_ty *and* actual_ty - \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty - ) `thenM` \ (gen_fn, co_fn) -> - returnM (gen_fn <.> co_fn) +tc_sub act_sty act_ty exp_sty exp_ty + | isSigmaTy exp_ty + = do { (gen_fn, co_fn) <- tcGen exp_ty act_tvs $ \ body_exp_ty -> + tc_sub act_sty act_ty 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 the free vars of + -- both expected_ty *and* actual_ty ----------------------------------- --- Specialisation case: +-- Specialisation case (rule ASPEC): -- actual_ty: forall a. Ord a => a->a -- expected_ty: Int -> Int -- co_fn e = e Int dOrdInt -tc_sub exp_sty expected_ty act_sty actual_ty +tc_sub act_sty actual_ty exp_sty expected_ty | isSigmaTy actual_ty - = tcInstCall Rank2Origin actual_ty `thenM` \ (inst_fn, body_ty) -> - tc_sub exp_sty expected_ty body_ty body_ty `thenM` \ co_fn -> - returnM (co_fn <.> inst_fn) + = do { (tyvars, theta, tau) <- tcInstBoxy actual_ty + ; dicts <- newDicts InstSigOrigin theta + ; extendLIEs dicts + ; let inst_fn = CoApps (CoTyApps CoHole (mkTyVarTys tyvars)) + (map instToId dicts) + ; co_fn <- tc_sub tau tau exp_sty expected_ty + ; return (co_fn <.> inst_fn) } ----------------------------------- --- Function case +-- Function case (rule F1) +tc_sub _ (FunTy act_arg act_res) _ (FunTy exp_arg exp_res) + = tc_sub_funs act_arg act_res exp_arg exp_res + +-- Function case (rule F2) +tc_sub act_sty act_ty@(FunTy act_arg act_res) exp_sty (TyVarTy exp_tv) + | isBoxyTyVar exp_tv + = do { cts <- readMetaTyVar exp_tv + ; case cts of + Indirect ty -> do { u_tys False act_sty act_ty True exp_sty ty + ; return idCoercion } + Flexi -> do { [arg_ty,res_ty] <- withMetaTvs exp_tv fun_kinds mk_res_ty + ; tc_sub_funs act_arg act_res arg_ty res_ty } } + where + mk_res_ty [arg_ty', res_ty'] = mkFunTy arg_ty' res_ty' + fun_kinds = [argTypeKind, openTypeKind] + +-- Everything else: defer to boxy matching +tc_sub act_sty actual_ty exp_sty expected_ty + = do { u_tys False act_sty actual_ty False exp_sty expected_ty + ; return idCoercion } -tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res) - = tcSub_fun exp_arg exp_res act_arg act_res ----------------------------------- --- Type variable meets function: imitate --- --- NB 1: we can't just unify the type variable with the type --- because the type might not be a tau-type, and we aren't --- allowed to instantiate an ordinary type variable with --- a sigma-type --- --- NB 2: can we short-cut to an error case? --- when the arg/res is not a tau-type? --- NO! e.g. f :: ((forall a. a->a) -> Int) -> Int --- then x = (f,f) --- is perfectly fine, because we can instantiat f's type to a monotype --- --- However, we get can get jolly unhelpful error messages. --- e.g. foo = id runST --- --- Inferred type is less polymorphic than expected --- Quantified type variable `s' escapes --- Expected type: ST s a -> t --- Inferred type: (forall s1. ST s1 a) -> a --- In the first argument of `id', namely `runST' --- In a right-hand side of function `foo': id runST --- --- I'm not quite sure what to do about this! - -tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv) - = getTcTyVar tv `thenM` \ maybe_ty -> - case maybe_ty of - Just ty -> tc_sub exp_sty exp_ty ty ty - Nothing -> imitateFun tv exp_sty `thenM` \ (act_arg, act_res) -> - tcSub_fun exp_arg exp_res act_arg act_res - -tc_sub _ (TyVarTy tv) act_sty act_ty@(FunTy act_arg act_res) - = getTcTyVar tv `thenM` \ maybe_ty -> - case maybe_ty of - Just ty -> tc_sub ty ty act_sty act_ty - Nothing -> imitateFun tv act_sty `thenM` \ (exp_arg, exp_res) -> - tcSub_fun exp_arg exp_res act_arg act_res +tc_sub_funs act_arg act_res exp_arg exp_res + = do { uTys False act_arg False exp_arg + ; co_fn_res <- tc_sub act_res act_res exp_res exp_res + ; wrapFunResCoercion [exp_arg] co_fn_res } ----------------------------------- --- Unification case --- If none of the above match, we revert to the plain unifier -tc_sub exp_sty expected_ty act_sty actual_ty - = uTys exp_sty expected_ty act_sty actual_ty `thenM_` - returnM idCoercion -\end{code} - -%************************************************************************ -%* * -\subsection{Functions} -%* * -%************************************************************************ - -\begin{code} -tcSub_fun exp_arg exp_res act_arg act_res - = tc_sub act_arg act_arg exp_arg exp_arg `thenM` \ co_fn_arg -> - tc_sub exp_res exp_res act_res act_res `thenM` \ co_fn_res -> - newUnique `thenM` \ uniq -> - let - -- co_fn_arg :: HsExpr exp_arg -> HsExpr act_arg - -- co_fn_res :: HsExpr act_res -> HsExpr exp_res - -- co_fn :: HsExpr (act_arg -> act_res) -> HsExpr (exp_arg -> exp_res) - arg_id = mkSysLocal FSLIT("sub") uniq exp_arg - coercion | isIdCoercion co_fn_arg, - isIdCoercion co_fn_res = idCoercion - | otherwise = mkCoercion co_fn - - co_fn e = DictLam [arg_id] - (co_fn_res <$> (HsApp e (co_fn_arg <$> (HsVar arg_id)))) - -- Slight hack; using a "DictLam" to get an ordinary simple lambda - -- HsVar arg_id :: HsExpr exp_arg - -- co_fn_arg $it :: HsExpr act_arg - -- HsApp e $it :: HsExpr act_res - -- co_fn_res $it :: HsExpr exp_res - in - returnM coercion - -imitateFun :: TcTyVar -> TcType -> TcM (TcType, TcType) -imitateFun tv ty - = -- NB: tv is an *ordinary* tyvar and so are the new ones - - -- Check that tv isn't a type-signature type variable - -- (This would be found later in checkSigTyVars, but - -- we get a better error message if we do it here.) - checkM (not (isSkolemTyVar tv)) - (failWithTcM (unifyWithSigErr tv ty)) `thenM_` - - newTyVarTy openTypeKind `thenM` \ arg -> - newTyVarTy openTypeKind `thenM` \ res -> - putTcTyVar tv (mkFunTy arg res) `thenM_` - returnM (arg,res) +wrapFunResCoercion + :: [TcType] -- Type of args + -> ExprCoFn -- HsExpr a -> HsExpr b + -> TcM ExprCoFn -- 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))) } \end{code} + %************************************************************************ %* * \subsection{Generalisation} @@ -489,20 +613,36 @@ imitateFun tv ty %************************************************************************ \begin{code} -tcGen :: TcSigmaType -- expected_ty +tcGen :: BoxySigmaType -- expected_ty -> TcTyVarSet -- Extra tyvars that the universally -- quantified tyvars of expected_ty -- must not be unified - -> (TcRhoType -> TcM result) -- spec_ty + -> (BoxyRhoType -> TcM result) -- spec_ty -> TcM (ExprCoFn, 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 - = tcInstType SigTv expected_ty `thenM` \ (forall_tvs, theta, phi_ty) -> + = do { -- 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) -> + do { (forall_tvs, theta, rho_ty) <- tcInstSkolType skol_info expected_ty + ; span <- getSrcSpanM + ; let skol_info = GenSkol forall_tvs (mkPhiTy theta rho_ty) span + ; 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 -- Type-check the arg and unify with poly type - getLIE (thing_inside phi_ty) `thenM` \ (result, lie) -> + ; (result, lie) <- getLIE (thing_inside rho_ty) -- Check that the "forall_tvs" havn't been constrained -- The interesting bit here is that we must include the free variables @@ -515,30 +655,19 @@ 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. - newDicts SignatureOrigin theta `thenM` \ dicts -> - tcSimplifyCheck sig_msg forall_tvs dicts lie `thenM` \ inst_binds -> + ; dicts <- newDicts (SigOrigin skol_info) theta + ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie -#ifdef DEBUG - zonkTcTyVars forall_tvs `thenM` \ forall_tys -> - 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 phi_ty, - text "free_tvs" <+> ppr free_tvs, - text "forall_tys" <+> ppr forall_tys]) `thenM_` -#endif + ; checkSigTyVarsWrt free_tvs forall_tvs + ; traceTc (text "tcGen:done") - checkSigTyVarsWrt free_tvs forall_tvs `thenM` \ zonked_tvs -> - - traceTc (text "tcGen:done") `thenM_` - - let + ; 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 e = TyLam zonked_tvs (DictLam dict_ids (mkHsLet inst_binds e)) - in - returnM (mkCoercion co_fn, result) + dict_ids = map instToId dicts + co_fn = CoTyLams forall_tvs $ CoLams dict_ids $ CoLet inst_binds CoHole + ; returnM (co_fn, result) } where free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs sig_msg = ptext SLIT("expected type of an expression") @@ -548,49 +677,70 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall %************************************************************************ %* * -\subsection[Unify-exported]{Exported unification functions} + Boxy unification %* * %************************************************************************ The exported functions are all defined as versions of some non-exported generic functions. -Unify two @TauType@s. Dead straightforward. - \begin{code} -unifyTauTy :: TcTauType -> TcTauType -> TcM () -unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred - = -- The unifier should only ever see tau-types - -- (no quantification whatsoever) - ASSERT2( isTauTy ty1, ppr ty1 ) - ASSERT2( isTauTy ty2, ppr ty2 ) +boxyUnify :: BoxyType -> BoxyType -> TcM () +-- Acutal and expected, respectively +boxyUnify ty1 ty2 + = addErrCtxtM (unifyCtxt "type" ty1 ty2) $ + uTys False ty1 False ty2 + +--------------- +boxyUnifyList :: [BoxyType] -> [BoxyType] -> TcM () +-- Arguments should have equal length +-- Acutal and expected types +boxyUnifyList tys1 tys2 = uList boxyUnify tys1 tys2 + +--------------- +unifyType :: TcTauType -> TcTauType -> TcM () +-- No boxes expected inside these types +-- Acutal and expected types +unifyType ty1 ty2 -- ty1 expected, ty2 inferred + = ASSERT2( not (isBoxyTy ty1), ppr ty1 ) + ASSERT2( not (isBoxyTy ty2), ppr ty2 ) addErrCtxtM (unifyCtxt "type" ty1 ty2) $ - uTys ty1 ty1 ty2 ty2 + uTys True ty1 True ty2 + +--------------- +unifyPred :: PredType -> PredType -> TcM () +-- Acutal and expected types +unifyPred p1 p2 = addErrCtxtM (unifyCtxt "type constraint" (mkPredTy p1) (mkPredTy p2)) $ + uPred True p1 True p2 + +unifyTheta :: TcThetaType -> TcThetaType -> TcM () +-- Acutal and expected types +unifyTheta theta1 theta2 + = do { checkTc (equalLength theta1 theta2) + (ptext SLIT("Contexts differ in length")) + ; uList unifyPred theta1 theta2 } + +--------------- +uList :: (a -> a -> TcM ()) + -> [a] -> [a] -> TcM () +-- Unify corresponding elements of two lists of types, which +-- should be f 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 ty1s ty2s = panic "Unify.uList: mismatched type lists!" \end{code} -@unifyTauTyList@ unifies corresponding elements of two lists of -@TauType@s. It uses @uTys@ to do the real work. The lists should be -of equal length. We charge down the list explicitly so that we can -complain if their lengths differ. - -\begin{code} -unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM () -unifyTauTyLists [] [] = returnM () -unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenM_` - unifyTauTyLists tys1 tys2 -unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!" -\end{code} - -@unifyTauTyList@ takes a single list of @TauType@s and unifies them +@unifyTypeList@ takes a single list of @TauType@s and unifies them all together. It is used, for example, when typechecking explicit lists, when all the elts should be of the same type. \begin{code} -unifyTauTyList :: [TcTauType] -> TcM () -unifyTauTyList [] = returnM () -unifyTauTyList [ty] = returnM () -unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenM_` - unifyTauTyList tys +unifyTypeList :: [TcTauType] -> TcM () +unifyTypeList [] = returnM () +unifyTypeList [ty] = returnM () +unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2 + ; unifyTypeList tys } \end{code} %************************************************************************ @@ -608,70 +758,111 @@ 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} -uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1 - -- ty1 is the *expected* type +type NoBoxes = Bool -- True <=> definitely no boxes in this type + -- False <=> there might be boxes (always safe) - -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2 - -- ty2 is the *actual* type +uTys :: NoBoxes -> TcType -- ty1 is the *expected* type + -> NoBoxes -> TcType -- ty2 is the *actual* type -> TcM () +uTys nb1 ty1 nb2 ty2 = u_tys nb1 ty1 ty1 nb2 ty2 ty2 + + +-------------- +uTys_s :: NoBoxes -> [TcType] -- ty1 is the *actual* types + -> NoBoxes -> [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 nb1 ty1s nb2 ty2s = panic "Unify.uTys_s: mismatched type lists!" + +-------------- +u_tys :: NoBoxes -> TcType -> TcType -- ty1 is the *actual* type + -> NoBoxes -> TcType -> TcType -- ty2 is the *expected* type + -> TcM () + +u_tys nb1 orig_ty1 ty1 nb2 orig_ty2 ty2 + = go ty1 ty2 + where -- Always expand synonyms (see notes at end) -- (this also throws away FTVs) -uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2 -uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2 + go ty1 ty2 + | Just ty1' <- tcView ty1 = go ty1' ty2 + | Just ty2' <- tcView ty2 = go ty1 ty2' -- Variables; go for uVar -uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2 -uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1 - -- "True" means args swapped - + go (TyVarTy tyvar1) ty2 = uVar False tyvar1 nb2 orig_ty2 ty2 + go ty1 (TyVarTy tyvar2) = uVar True tyvar2 nb1 orig_ty1 ty1 + -- "True" means args swapped -- Predicates -uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2)) - | n1 == n2 = uTys t1 t1 t2 t2 -uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2)) - | c1 == c2 = unifyTauTyLists tys1 tys2 -uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2)) - | tc1 == tc2 = unifyTauTyLists tys1 tys2 - - -- Functions; just check the two parts -uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2) - = uTys fun1 fun1 fun2 fun2 `thenM_` uTys arg1 arg1 arg2 arg2 + go (PredTy p1) (PredTy p2) = uPred nb1 p1 nb2 p2 -- Type constructors must match -uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2) - | con1 == con2 && equalLength tys1 tys2 - = unifyTauTyLists tys1 tys2 + go (TyConApp con1 tys1) (TyConApp con2 tys2) + | con1 == con2 = uTys_s nb1 tys1 nb2 tys2 + -- See Note [TyCon app] - | con1 == openKindCon - -- When we are doing kind checking, we might match a kind '?' - -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and - -- (CCallable Int) and (CCallable Int#) are both OK - = unifyOpenTypeKind ps_ty2 + -- Functions; just check the two parts + go (FunTy fun1 arg1) (FunTy fun2 arg2) + = do { uTys nb1 fun1 nb2 fun2 + ; uTys nb1 arg1 nb2 arg2 } -- 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 -uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2 - = case tcSplitAppTy_maybe ty2 of - Just (s2,t2) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2 - Nothing -> unifyMisMatch ps_ty1 ps_ty2 + go (AppTy s1 t1) ty2 + = case tcSplitAppTy_maybe ty2 of + Just (s2,t2) -> do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 } + Nothing -> unifyMisMatch False orig_ty1 orig_ty2 -- Now the same, but the other way round -- Don't swap the types, because the error messages get worse -uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2) - = case tcSplitAppTy_maybe ty1 of - Just (s1,t1) -> uTys s1 s1 s2 s2 `thenM_` uTys t1 t1 t2 t2 - Nothing -> unifyMisMatch ps_ty1 ps_ty2 - - -- Not expecting for-alls in unification - -- ... but the error message from the unifyMisMatch more informative - -- than a panic message! + go ty1 (AppTy s2 t2) + = case tcSplitAppTy_maybe ty1 of + Just (s1,t1) -> do { uTys nb1 s1 nb2 s2; uTys nb1 t1 nb2 t2 } + Nothing -> unifyMisMatch False orig_ty1 orig_ty2 + + 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 should not have + -- a polytype at all. 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 -- Anything else fails -uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2 + go _ _ = unifyMisMatch False orig_ty1 orig_ty2 + +---------- +uPred nb1 (IParam n1 t1) nb2 (IParam n2 t2) + | n1 == n2 = uTys nb1 t1 nb2 t2 +uPred nb1 (ClassP c1 tys1) nb2 (ClassP c2 tys2) + | c1 == c2 = uTys_s nb1 tys1 nb2 tys2 -- Guaranteed equal lengths because the kinds check +uPred _ p1 _ p2 = unifyMisMatch False (mkPredTy p1) (mkPredTy p2) \end{code} +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 +the same. The only way it can become not the same is when unifying two +AppTys (f1 a1):=:(f2 a2). In that case there can't be a TyConApp in +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. + Notes on synonyms ~~~~~~~~~~~~~~~~~ @@ -683,7 +874,7 @@ pseudocode... -- NO = if (con1 == con2) then -- NO -- Good news! Same synonym constructors, so we can shortcut -- NO -- by unifying their arguments and ignoring their expansions. --- NO unifyTauTypeLists args1 args2 +-- NO unifyTypepeLists args1 args2 -- NO else -- NO -- Never mind. Just expand them and try again -- NO uTys ty1 ty2 @@ -740,82 +931,168 @@ back into @uTys@ if it turns out that the variable is already bound. uVar :: Bool -- False => tyvar is the "expected" -- True => ty is the "expected" thing -> TcTyVar + -> NoBoxes -- True <=> definitely no boxes in t2 -> TcTauType -> TcTauType -- printing and real versions -> TcM () -uVar swapped tv1 ps_ty2 ty2 - = traceTc (text "uVar" <+> ppr swapped <+> ppr tv1 <+> (ppr ps_ty2 $$ ppr ty2)) `thenM_` - getTcTyVar tv1 `thenM` \ maybe_ty1 -> - case maybe_ty1 of - Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back - | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order - other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2 - - -- Expand synonyms; ignore FTVs -uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2) - = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2 - - - -- The both-type-variable case -uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2) - +uVar 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 <+> + sep [ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1 ), + nest 2 (ptext SLIT(" :=: ")), + ppr ps_ty2 <+> dcolon <+> ppr (typeKind ty2) <+> expansion]) + ; details <- lookupTcTyVar tv1 + ; case details of + IndirectTv ty1 + | swapped -> u_tys nb2 ps_ty2 ty2 True ty1 ty1 -- Swap back + | otherwise -> u_tys True ty1 ty1 nb2 ps_ty2 ty2 -- Same order + -- The 'True' here says that ty1 + -- is definitely box-free + DoneTv details1 -> uUnfilledVar swapped tv1 details1 nb2 ps_ty2 ty2 + } + +---------------- +uUnfilledVar :: Bool -- Args are swapped + -> TcTyVar -> TcTyVarDetails -- Tyvar 1 + -> NoBoxes -> TcTauType -> TcTauType -- Type 2 + -> TcM () +-- Invariant: tyvar 1 is not unified with anything + +uUnfilledVar swapped tv1 details1 nb2 ps_ty2 ty2 + | Just ty2' <- tcView ty2 + = -- Expand synonyms; ignore FTVs + uUnfilledVar swapped tv1 details1 nb2 ps_ty2 ty2' + +uUnfilledVar swapped tv1 details1 nb2 ps_ty2 ty2@(TyVarTy tv2) -- Same type variable => no-op | tv1 == tv2 = returnM () -- Distinct type variables - -- ASSERT maybe_ty1 /= Just | otherwise - = getTcTyVar tv2 `thenM` \ maybe_ty2 -> - case maybe_ty2 of - Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2' + = do { lookup2 <- lookupTcTyVar tv2 + ; case lookup2 of + IndirectTv ty2' -> uUnfilledVar swapped tv1 details1 True ty2' ty2' + DoneTv details2 -> uUnfilledVars swapped tv1 details1 tv2 details2 + } + +uUnfilledVar swapped tv1 details1 nb2 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 nb2 ps_ty2 non_var_ty2 + skolem_details -> mis_match + where + mis_match = unifyMisMatch swapped (TyVarTy tv1) ps_ty2 + +---------------- +uMetaVar :: Bool + -> TcTyVar -> BoxInfo -> IORef MetaDetails + -> NoBoxes -> TcType -> TcType + -> TcM () +-- tv1 is an un-filled-in meta type variable (maybe boxy, maybe tau) +-- ty2 is not a type variable + +uMetaVar swapped tv1 info1 ref1 nb2 ps_ty2 non_var_ty2 + = do { final_ty <- case info1 of + BoxTv -> unBox ps_ty2 -- No occurs check + other -> checkTauTvUpdate tv1 ps_ty2 -- Occurs check + monotype check + ; checkUpdateMeta swapped tv1 ref1 final_ty } + +---------------- +uUnfilledVars :: Bool -- Args are swapped + -> TcTyVar -> TcTyVarDetails -- Tyvar 1 + -> TcTyVar -> TcTyVarDetails -- Tyvar 2 + -> TcM () +-- Invarant: The type variables are distinct, +-- Neither is filled in yet +-- They might be boxy or not + +uUnfilledVars swapped tv1 (SkolemTv _) tv2 (SkolemTv _) + = unifyMisMatch swapped (mkTyVarTy tv1) (mkTyVarTy tv2) + +uUnfilledVars swapped tv1 (MetaTv info1 ref1) tv2 (SkolemTv _) + = checkUpdateMeta swapped tv1 ref1 (mkTyVarTy tv2) +uUnfilledVars swapped tv1 (SkolemTv _) tv2 (MetaTv info2 ref2) + = checkUpdateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) + +-- ToDo: this function seems too long for what it acutally does! +uUnfilledVars swapped tv1 (MetaTv info1 ref1) tv2 (MetaTv info2 ref2) + = case (info1, info2) of + (BoxTv, BoxTv) -> box_meets_box + + -- 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 + + -- Avoid SigTvs if poss + (SigTv _, _ ) | k1_sub_k2 -> update_tv2 + (_, SigTv _) | k2_sub_k1 -> update_tv1 + + (_, _) | 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 + + -- Update the variable with least kind info + -- See notes on type inference in Kind.lhs + -- The "nicer to" part only applies if the two kinds are the same, + -- so we can choose which to do. + where + -- Kinds should be guaranteed ok at this point + update_tv1 = updateMeta tv1 ref1 (mkTyVarTy tv2) + update_tv2 = updateMeta tv2 ref2 (mkTyVarTy tv1) - Nothing | update_tv2 + box_meets_box | k1_sub_k2 = fill_with k1 + | k2_sub_k1 = fill_with k2 + | otherwise = kind_err - -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) ) - putTcTyVar tv2 (TyVarTy tv1) `thenM_` - returnM () - | otherwise + fill_with kind = do { tau_ty <- newFlexiTyVarTy kind + ; updateMeta tv1 ref1 tau_ty + ; updateMeta tv2 ref2 tau_ty } + + kind_err = addErrCtxtM (unifyKindCtxt swapped tv1 (mkTyVarTy tv2)) $ + unifyKindMisMatch k1 k2 - -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) ) - putTcTyVar tv1 ps_ty2 `thenM_` - returnM () - where k1 = tyVarKind tv1 k2 = tyVarKind tv2 - update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2) - -- Try to get rid of open type variables as soon as poss - - nicer_to_update_tv2 = isUserTyVar tv1 - -- Don't unify a signature type variable if poss - || isSystemName (varName tv2) - -- Try to update sys-y type variables in preference to sig-y ones - - -- Second one isn't a type variable -uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2 - = -- Check that tv1 isn't a type-signature type variable - checkM (not (isSkolemTyVar tv1)) - (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenM_` - - -- Do the occurs check, and check that we are not - -- unifying a type variable with a polytype - -- Returns a zonked type ready for the update - checkValue tv1 ps_ty2 non_var_ty2 `thenM` \ ty2 -> - - -- Check that the kinds match - checkKinds swapped tv1 ty2 `thenM_` - - -- Perform the update - putTcTyVar tv1 ty2 `thenM_` - returnM () -\end{code} + k1_sub_k2 = k1 `isSubKind` k2 + k2_sub_k1 = k2 `isSubKind` k1 -\begin{code} + nicer_to_update_tv1 = isSystemName (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 `hasMoreBoxityInfo` tk1 = returnM () + | tk2 `isSubKind` tk1 = returnM () | otherwise -- Either the kinds aren't compatible @@ -823,142 +1100,287 @@ checkKinds swapped tv1 ty2 -- or we are unifying a lifted type variable with an -- unlifted type: e.g. (id 3#) is illegal = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $ - unifyMisMatch k1 k2 - + 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 -> do { tau <- newFlexiTyVarTy (tyVarKind tv) + ; writeMutVar ref (Indirect tau) + ; return tau } + 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 (fromJust (tcView (TyConApp tc tys))) + -- Try again, expanding the synonym + } \end{code} -\begin{code} -checkValue tv1 ps_ty2 non_var_ty2 --- Do the occurs check, and check that we are not --- unifying a type variable with a polytype --- Return the type to update the type variable with, or fail +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 --- 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 + +zapToMonotype :: BoxySigmaType -> TcM TcTauType +-- Subtle... we must zap the boxy res_ty +-- to kind * before using it to instantiate a LitInst +-- Calling unBox instead doesn't do the job, because the box +-- often has an openTypeKind, and we don't want to instantiate +-- with that type. +zapToMonotype res_ty + = do { res_tau <- newFlexiTyVarTy liftedTypeKind + ; boxyUnify res_tau res_ty + ; return res_tau } + +unBox :: BoxyType -> TcM TcType +-- unBox implements the judgement +-- |- s' ~ box(s) +-- with input s', and result s -- --- But consider --- type A a = () +-- It remove all boxes from the input type, returning a non-boxy type. +-- A filled box in the type can only contain a monotype; unBox fails if not +-- The type can have empty boxes, which unBox fills with a monotype -- --- f :: (A a -> a -> ()) -> () --- f = \ _ -> () +-- Compare this wth checkTauTvUpdate -- --- 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). --- --- That's why we have this two-state occurs-check - = zonkTcType ps_ty2 `thenM` \ ps_ty2' -> - case okToUnifyWith tv1 ps_ty2' of { - Nothing -> returnM ps_ty2' ; -- Success - other -> - - zonkTcType non_var_ty2 `thenM` \ non_var_ty2' -> - case okToUnifyWith tv1 non_var_ty2' of - Nothing -> -- This branch rarely succeeds, except in strange cases - -- like that in the example above - returnM non_var_ty2' - - Just problem -> failWithTcM (unifyCheck problem tv1 ps_ty2') - } - -data Problem = OccurCheck | NotMonoType - -okToUnifyWith :: TcTyVar -> TcType -> Maybe Problem --- (okToUnifyWith tv ty) checks whether it's ok to unify --- tv :=: ty --- Nothing => ok --- Just p => not ok, problem p - -okToUnifyWith tv ty - = ok ty - where - ok (TyVarTy tv') | tv == tv' = Just OccurCheck - | otherwise = Nothing - ok (AppTy t1 t2) = ok t1 `and` ok t2 - ok (FunTy t1 t2) = ok t1 `and` ok t2 - ok (TyConApp _ ts) = oks ts - ok (ForAllTy _ _) = Just NotMonoType - ok (SourceTy st) = ok_st st - ok (NoteTy (FTVNote _) t) = ok t - ok (NoteTy (SynNote t1) t2) = ok t1 `and` ok t2 - -- Type variables may be free in t1 but not t2 - -- A forall may be in t2 but not t1 - - oks ts = foldr (and . ok) Nothing ts - - ok_st (ClassP _ ts) = oks ts - ok_st (IParam _ t) = ok t - ok_st (NType _ ts) = oks ts - - Nothing `and` m = m - Just p `and` m = Just p +-- 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') } +unBox (PredTy p) = do { p' <- unBoxPred p; return (PredTy p') } +unBox (ForAllTy tv ty) = ASSERT( isImmutableTyVar tv ) + do { ty' <- unBox ty; return (ForAllTy tv ty') } +unBox (TyVarTy tv) + | isTcTyVar tv -- It's a boxy type variable + , MetaTv BoxTv ref <- tcTyVarDetails tv -- NB: non-TcTyVars are possible + = do { cts <- readMutVar ref -- under nested quantifiers + ; case cts of + Indirect ty -> do { non_boxy_ty <- unBox ty + ; if isTauTy non_boxy_ty + then return non_boxy_ty + else notMonoType non_boxy_ty } + Flexi -> do { tau <- newFlexiTyVarTy (tyVarKind tv) + ; writeMutVar ref (Indirect tau) + ; return tau } + } + | otherwise -- Skolems, and meta-tau-variables + = return (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') } \end{code} + + %************************************************************************ %* * -\subsection{Kind unification} + Kind unification %* * %************************************************************************ +Unifying kinds is much, much simpler than unifying types. + \begin{code} unifyKind :: TcKind -- Expected -> TcKind -- Actual -> TcM () -unifyKind k1 k2 = uTys k1 k1 k2 k2 +unifyKind LiftedTypeKind LiftedTypeKind = returnM () +unifyKind UnliftedTypeKind UnliftedTypeKind = returnM () + +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 } + -- 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 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" -\end{code} - -\begin{code} -unifyOpenTypeKind :: TcKind -> TcM () --- Ensures that the argument kind is of the form (Type bx) --- for some boxity bx - -unifyOpenTypeKind ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of - Just ty' -> unifyOpenTypeKind ty' - other -> unify_open_kind_help ty - -unifyOpenTypeKind ty - | isTypeKind ty = returnM () - | otherwise = unify_open_kind_help ty - -unify_open_kind_help ty -- Revert to ordinary unification - = newOpenTypeKind `thenM` \ open_kind -> - unifyKind ty open_kind +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 } + +---------------- +uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM () +uUnboundKVar swapped kv1 k2@(KindVar kv2) + | kv1 == kv2 = returnM () + | otherwise -- Distinct kind variables + = do { mb_k2 <- readKindVar kv2 + ; case mb_k2 of + Just k2 -> uUnboundKVar swapped kv1 k2 + Nothing -> writeKindVar kv1 k2 } + +uUnboundKVar swapped kv1 non_var_k2 + = do { k2' <- zonkTcKind non_var_k2 + ; kindOccurCheck kv1 k2' + ; k2'' <- kindSimpleKind swapped k2' + -- KindVars must be bound only to simple kinds + -- Polarities: (kindSimpleKind True ?) succeeds + -- returning *, corresponding to unifying + -- expected: ? + -- actual: kind-ver + ; writeKindVar kv1 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 + +kindSimpleKind :: Bool -> Kind -> TcM SimpleKind +-- (kindSimpleKind True k) returns a simple kind sk such that sk <: k +-- If the flag is False, it requires k <: sk +-- E.g. kindSimpleKind False ?? = * +-- What about (kv -> *) :=: ?? -> * +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 k@(KindVar _) = 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 + +-- T v = MkT v v must be a type +-- T v w = MkT (v -> w) v must not be an umboxed tuple + +---------------- +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 (TyVarTy tyvar) - = getTcTyVar tyvar `thenM` \ maybe_ty -> - case maybe_ty of +unifyFunKind (KindVar kvar) + = readKindVar kvar `thenM` \ maybe_kind -> + case maybe_kind of Just fun_kind -> unifyFunKind fun_kind - Nothing -> newKindVar `thenM` \ arg_kind -> - newKindVar `thenM` \ res_kind -> - putTcTyVar tyvar (mkArrowKind arg_kind res_kind) `thenM_` - returnM (Just (arg_kind,res_kind)) + Nothing -> do { arg_kind <- newKindVar + ; res_kind <- newKindVar + ; writeKindVar kvar (mkArrowKind arg_kind res_kind) + ; returnM (Just (arg_kind,res_kind)) } -unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind)) -unifyFunKind (NoteTy _ ty) = unifyFunKind ty -unifyFunKind other = returnM Nothing +unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind)) +unifyFunKind other = returnM Nothing \end{code} %************************************************************************ @@ -971,67 +1393,148 @@ Errors ~~~~~~ \begin{code} -unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred +unifyCtxt s ty1 ty2 tidy_env -- ty1 inferred, ty2 expected = zonkTcType ty1 `thenM` \ ty1' -> zonkTcType ty2 `thenM` \ ty2' -> returnM (err ty1' ty2') where err ty1 ty2 = (env1, - nest 4 + nest 2 (vcat [ - text "Expected" <+> text s <> colon <+> ppr tidy_ty1, - text "Inferred" <+> text s <> colon <+> ppr tidy_ty2 + text "Expected" <+> text s <> colon <+> ppr tidy_ty2, + text "Inferred" <+> text s <> colon <+> ppr tidy_ty1 ])) where (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2] unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred - -- tv1 is zonked already - = zonkTcType ty2 `thenM` \ ty2' -> - returnM (err ty2') + -- tv1 and ty2 are zonked already + = returnM msg where - err ty2 = (env2, ptext SLIT("When matching types") <+> - sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual]) - where - (pp_expected, pp_actual) | swapped = (pp2, pp1) - | otherwise = (pp1, pp2) - (env1, tv1') = tidyOpenTyVar tidy_env tv1 - (env2, ty2') = tidyOpenType env1 ty2 - pp1 = ppr tv1' - pp2 = ppr ty2' - -unifyMisMatch ty1 ty2 - = zonkTcType ty1 `thenM` \ ty1' -> - zonkTcType ty2 `thenM` \ ty2' -> - let - (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2'] - msg = hang (ptext SLIT("Couldn't match")) - 4 (sep [quotes (ppr tidy_ty1), - ptext SLIT("against"), - quotes (ppr tidy_ty2)]) - in - failWithTcM (env, msg) - -unifyWithSigErr tyvar ty - = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar)) - 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty))) + 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 swapped ty1 ty2 + = do { (env, msg) <- if swapped then misMatchMsg ty2 ty1 + else misMatchMsg ty1 ty2 + ; 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") <+> pp1, + nest 7 (ptext SLIT("against") <+> pp2)], + nest 2 extra1, nest 2 extra2]) } + +ppr_ty :: TidyEnv -> TcType -> TcM (TidyEnv, SDoc, SDoc) +ppr_ty env ty + = 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 - (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar - (env2, tidy_ty) = tidyOpenType env1 ty - -unifyCheck problem tyvar ty - = (env2, hang msg - 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty])) + pp_rigid tv = ptext SLIT("the rigid variable") <+> quotes (ppr tv) + + +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 - (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar - (env2, tidy_ty) = tidyOpenType env1 ty - - msg = case problem of - OccurCheck -> ptext SLIT("Occurs check: cannot construct the infinite type:") - NotMonoType -> ptext SLIT("Cannot unify a type variable with a type scheme:") + msg = ptext SLIT("Occurs check: cannot construct the infinite type:") \end{code} +%************************************************************************ +%* * + Checking kinds +%* * +%************************************************************************ + +--------------------------- +-- We would like to get a decent error message from +-- (a) Under-applied type constructors +-- f :: (Maybe, Maybe) +-- (b) Over-applied type constructors +-- f :: Int x -> Int x +-- + +\begin{code} +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 + | 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 -> + + -- 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) + } +\end{code} %************************************************************************ %* * @@ -1039,18 +1542,10 @@ unifyCheck problem tyvar ty %* * %************************************************************************ -@checkSigTyVars@ is used after the type in a type signature has been unified with -the actual type found. It then checks that the type variables of the type signature -are - (a) Still all type variables - eg matching signature [a] against inferred type [(p,q)] - [then a will be unified to a non-type variable] +@checkSigTyVars@ checks that a set of universally quantified type varaibles +are not mentioned in the environment. In particular: - (b) Still all distinct - eg matching signature [(a,b)] against inferred type [(p,p)] - [then a and b will be unified together] - - (c) Not mentioned in the environment + (a) Not mentioned in the type of a variable in the envt eg the signature for f in this: g x = ... where @@ -1073,127 +1568,77 @@ are Before doing this, the substitution is applied to the signature type variable. -We used to have the notion of a "DontBind" type variable, which would -only be bound to itself or nothing. Then points (a) and (b) were -self-checking. But it gave rise to bogus consequential error messages. -For example: - - f = (*) -- Monomorphic - - g :: Num a => a -> a - g x = f x x - -Here, we get a complaint when checking the type signature for g, -that g isn't polymorphic enough; but then we get another one when -dealing with the (Num x) context arising from f's definition; -we try to unify x with Int (to default it), but find that x has already -been unified with the DontBind variable "a" from g's signature. -This is really a problem with side-effecting unification; we'd like to -undo g's effects when its type signature fails, but unification is done -by side effect, so we can't (easily). - -So we revert to ordinary type variables for signatures, and try to -give a helpful message in checkSigTyVars. - \begin{code} -checkSigTyVars :: [TcTyVar] -> TcM [TcTyVar] +checkSigTyVars :: [TcTyVar] -> TcM () checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs -checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM [TcTyVar] +checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM () +-- The extra_tvs can include boxy type variables; +-- e.g. TcMatches.tcCheckExistentialPat checkSigTyVarsWrt extra_tvs sig_tvs - = zonkTcTyVarsAndFV (varSetElems extra_tvs) `thenM` \ extra_tvs' -> - check_sig_tyvars extra_tvs' sig_tvs + = do { extra_tvs' <- zonkTcTyVarsAndFV (varSetElems extra_tvs) + ; check_sig_tyvars extra_tvs' sig_tvs } check_sig_tyvars - :: TcTyVarSet -- Global type variables. The universally quantified - -- tyvars should not mention any of these - -- Guaranteed already zonked. - -> [TcTyVar] -- Universally-quantified type variables in the signature - -- Not guaranteed zonked. - -> TcM [TcTyVar] -- Zonked signature type variables - + :: TcTyVarSet -- Global type variables. The universally quantified + -- tyvars should not mention any of these + -- Guaranteed already zonked. + -> [TcTyVar] -- Universally-quantified type variables in the signature + -- Guaranteed to be skolems + -> TcM () check_sig_tyvars extra_tvs [] - = returnM [] + = returnM () check_sig_tyvars extra_tvs sig_tvs - = zonkTcTyVars sig_tvs `thenM` \ sig_tys -> - tcGetGlobalTyVars `thenM` \ gbl_tvs -> - let - env_tvs = gbl_tvs `unionVarSet` extra_tvs - in - traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tys, + = ASSERT( all isSkolemTyVar sig_tvs ) + do { gbl_tvs <- tcGetGlobalTyVars + ; traceTc (text "check_sig_tyvars" <+> (vcat [text "sig_tys" <+> ppr sig_tvs, text "gbl_tvs" <+> ppr gbl_tvs, - text "extra_tvs" <+> ppr extra_tvs])) `thenM_` - - checkM (allDistinctTyVars sig_tys env_tvs) - (complain sig_tys env_tvs) `thenM_` - - returnM (map (tcGetTyVar "checkSigTyVars") sig_tys) - + 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) + } + +bleatEscapedTvs :: TcTyVarSet -- The global tvs + -> [TcTyVar] -- The possibly-escaping type variables + -> [TcTyVar] -- The zonked versions thereof + -> TcM () +-- Complain about escaping type variables +-- We pass a list of type variables, at least one of which +-- escapes. The first list contains the original signature type variable, +-- while the second contains the type variable it is unified to (usually itself) +bleatEscapedTvs globals sig_tvs zonked_tvs + = do { env0 <- tcInitTidyEnv + ; let (env1, tidy_tvs) = tidyOpenTyVars env0 sig_tvs + (env2, tidy_zonked_tvs) = tidyOpenTyVars env1 zonked_tvs + + ; (env3, msgs) <- foldlM check (env2, []) (tidy_tvs `zip` tidy_zonked_tvs) + ; failWithTcM (env3, main_msg $$ nest 2 (vcat msgs)) } where - complain sig_tys globals - = -- "check" checks each sig tyvar in turn - foldlM check - (env2, emptyVarEnv, []) - (tidy_tvs `zip` tidy_tys) `thenM` \ (env3, _, msgs) -> + main_msg = ptext SLIT("Inferred type is less polymorphic than expected") - failWithTcM (env3, main_msg $$ nest 4 (vcat msgs)) - where - (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs - (env2, tidy_tys) = tidyOpenTypes env1 sig_tys - - main_msg = ptext SLIT("Inferred type is less polymorphic than expected") - - check (tidy_env, acc, msgs) (sig_tyvar,ty) - -- sig_tyvar is from the signature; - -- ty is what you get if you zonk sig_tyvar and then tidy it - -- - -- acc maps a zonked type variable back to a signature type variable - = case tcGetTyVar_maybe ty of { - Nothing -> -- Error (a)! - returnM (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ; - - Just tv -> - - case lookupVarEnv acc tv of { - Just sig_tyvar' -> -- Error (b)! - returnM (tidy_env, acc, unify_msg sig_tyvar thing : msgs) - where - thing = ptext SLIT("another quantified type variable") <+> quotes (ppr sig_tyvar') - - ; Nothing -> - - if tv `elemVarSet` globals -- Error (c) or (d)! Type variable escapes - -- The least comprehensible, so put it last - -- Game plan: - -- get the local TcIds and TyVars from the environment, - -- and pass them to find_globals (they might have tv free) - then findGlobals (unitVarSet tv) tidy_env `thenM` \ (tidy_env1, globs) -> - returnM (tidy_env1, acc, escape_msg sig_tyvar tv globs : msgs) - - else -- All OK - returnM (tidy_env, extendVarEnv acc tv sig_tyvar, msgs) - }} -\end{code} + check (tidy_env, msgs) (sig_tv, zonked_tv) + | 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) } - -\begin{code} ----------------------- -escape_msg sig_tv tv globs - = mk_msg sig_tv <+> ptext SLIT("escapes") $$ - if notNull globs then - vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"), - nest 2 (vcat globs)] - else - empty -- Sigh. It's really hard to give a good error message - -- all the time. One bad case is an existential pattern match. - -- We rely on the "When..." context to help. +escape_msg sig_tv zonked_tv globs + | notNull globs + = vcat [sep [msg, ptext SLIT("is mentioned in the environment:")], + nest 2 (vcat globs)] + | otherwise + = msg <+> ptext SLIT("escapes") + -- Sigh. It's really hard to give a good error message + -- all the time. One bad case is an existential pattern match. + -- We rely on the "When..." context to help. where - pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which") - | otherwise = ptext SLIT("It") - - -unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing -mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv) + msg = ptext SLIT("Quantified type variable") <+> quotes (ppr sig_tv) <+> is_bound_to + is_bound_to + | sig_tv == zonked_tv = empty + | otherwise = ptext SLIT("is unified with") <+> quotes (ppr zonked_tv) <+> ptext SLIT("which") \end{code} These two context are used with checkSigTyVars @@ -1211,7 +1656,7 @@ sigCtxt id sig_tvs sig_theta sig_tau tidy_env ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau ] msg = vcat [ptext SLIT("When trying to generalise the type inferred for") <+> quotes (ppr id), - nest 4 sub_msg] + nest 2 sub_msg] in returnM (env3, msg) \end{code}