X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcUnify.lhs;h=8cd2a0b73890a5ec6683b06da32270d4009380c1;hb=ac10f8408520a30e8437496d320b8b86afda2e8f;hp=56ae76492deb3b2a14b7aee832f19218edec44db;hpb=10fcd78ccde892feccda3f5eacd221c1de75feea;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index 56ae764..8cd2a0b 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -6,136 +6,525 @@ \begin{code} module TcUnify ( -- Full-blown subsumption - tcSub, tcGen, subFunTy, - checkSigTyVars, sigCtxt, sigPatCtxt, + tcSubExp, tcGen, + checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt, -- Various unifications - unifyTauTy, unifyTauTyList, unifyTauTyLists, - unifyFunTy, unifyListTy, unifyPArrTy, unifyTupleTy, - unifyKind, unifyKinds, unifyOpenTypeKind, - - -- Coercions - Coercion, ExprCoFn, PatCoFn, - (<$>), (<.>), mkCoercion, - idCoercion, isIdCoercion - + unifyType, unifyTypeList, unifyTheta, + unifyKind, unifyKinds, unifyFunKind, + checkExpectedKind, + boxySubMatchType, boxyMatchTypes, + + -------------------------------- + -- Holes + 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 ( TypecheckedHsExpr, TcPat, - mkHsDictApp, mkHsTyApp, mkHsLet ) -import TypeRep ( Type(..), SourceType(..), - openKindCon, typeCon ) - -import TcMonad -- TcType, amongst others -import TcType ( TcKind, TcType, TcSigmaType, TcPhiType, TcTyVar, TcTauType, - TcTyVarSet, TcThetaType, - isTauTy, isSigmaTy, - tcSplitAppTy_maybe, tcSplitTyConApp_maybe, - tcGetTyVar_maybe, tcGetTyVar, - mkTyConApp, mkTyVarTys, mkFunTy, tyVarsOfType, mkRhoTy, - typeKind, tcSplitFunTy_maybe, mkForAllTys, - isHoleTyVar, isSkolemTyVar, isUserTyVar, allDistinctTyVars, - tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars, - eqKind, openTypeKind, liftedTypeKind, unliftedTypeKind, isTypeKind, - hasMoreBoxityInfo, tyVarBindingInfo - ) -import qualified Type ( getTyVar_maybe ) -import Inst ( LIE, emptyLIE, plusLIE, mkLIE, - newDicts, instToId - ) -import TcMType ( getTcTyVar, putTcTyVar, tcInstType, - newTyVarTy, newTyVarTys, newBoxityVar, newHoleTyVarTy, - zonkTcType, zonkTcTyVars, zonkTcTyVar ) +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 ( TcTyThing(..), tcExtendGlobalTyVars, tcGetGlobalTyVars, tcLEnvElts ) -import TyCon ( tyConArity, isTupleTyCon, tupleTyConBoxity ) -import PprType ( pprType ) -import CoreFVs ( idFreeTyVars ) -import Id ( mkSysLocal, idType ) -import Var ( Var, varName, tyVarKind ) -import VarSet ( elemVarSet, varSetElems ) +import TcEnv ( tcGetGlobalTyVars, findGlobals ) +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, isTcTyVar, tcTyVarDetails ) +import VarSet ( emptyVarSet, mkVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems, + extendVarSet, intersectsVarSet ) import VarEnv -import Name ( isSystemName, getSrcLoc ) +import Name ( isSystemName ) import ErrUtils ( Message ) -import BasicTypes ( Boxity, Arity, isBoxed ) -import Util ( isSingleton, equalLength ) -import Maybe ( isNothing ) +import Maybes ( fromJust ) +import BasicTypes ( Arity ) +import UniqSupply ( uniqsFromSupply ) +import Util ( notNull, equalLength ) import Outputable + +-- Assertion imports +#ifdef DEBUG +import TcType ( isBoxyTy, isFlexi ) +#endif \end{code} +%************************************************************************ +%* * +\subsection{'hole' type variables} +%* * +%************************************************************************ + +\begin{code} +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{Subsumption} + subFunTys %* * %************************************************************************ \begin{code} -tcSub :: TcSigmaType -- expected_ty; can be a type scheme; - -- can be a "hole" type variable - -> TcSigmaType -- actual_ty; can be a type scheme - -> TcM (ExprCoFn, LIE) -\end{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 -(tcSub expected_ty actual_ty) checks that - actual_ty <= expected_ty -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 :: actual_ty -> expected_ty -which takes an HsExpr of type actual_ty into one of type -expected_ty. +{- Error messages from subFunTys + + The abstraction `\Just 1 -> ...' has two arguments + but its type `Maybe a -> a' has only one + + The equation(s) for `f' have two arguments + but its type `Maybe a -> a' has only one + + The section `(f 3)' requires 'f' to take two arguments + but its type `Int -> Int' has only one + + The function 'f' is applied to two arguments + but its type `Int -> Int' has only one +-} + + +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} \begin{code} -tcSub expected_ty actual_ty - = traceTc (text "tcSub" <+> details) `thenNF_Tc_` - tcAddErrCtxtM (unifyCtxt "type" expected_ty actual_ty) - (tc_sub expected_ty expected_ty actual_ty actual_ty) +---------------------- +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 - details = vcat [text "Expected:" <+> ppr expected_ty, - text "Actual: " <+> ppr actual_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) + | 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 } + + +---------------------- +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 + 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} -tc_sub carries the types before and after expanding type synonyms + +-------------------------------- +-- withBoxes: the key utility function +-------------------------------- \begin{code} -tc_sub :: TcSigmaType -- expected_ty, before expanding synonyms - -> TcSigmaType -- ..and after - -> TcSigmaType -- actual_ty, before - -> TcSigmaType -- ..and after - -> TcM (ExprCoFn, LIE) +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} ------------------------------------ --- 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 ------------------------------------ --- "Hole type variable" case --- Do this case before unwrapping for-alls in the actual_ty +%************************************************************************ +%* * + Approximate boxy matching +%* * +%************************************************************************ + +\begin{code} +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 + 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} + + +%************************************************************************ +%* * + Subsumption checking +%* * +%************************************************************************ + +All the tcSub calls have the form + + tcSub expected_ty offered_ty +which checks + offered_ty <= expected_ty + +That is, that a value of type offered_ty is acceptable in +a place expecting a value of type expected_ty. -tc_sub _ (TyVarTy tv) act_sty act_ty - | isHoleTyVar tv - = -- It's a "hole" type variable - getTcTyVar tv `thenNF_Tc` \ maybe_ty -> - case maybe_ty of +It returns a coercion function + co_fn :: offered_ty -> expected_ty +which takes an HsExpr of type offered_ty into one of type +expected_ty. - Just ty -> -- Already been assigned - tc_sub ty ty act_sty act_ty ; +\begin{code} +----------------- +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" 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] - Nothing -> -- Assign it - putTcTyVar tv act_sty `thenNF_Tc_` - returnTc (idCoercion, emptyLIE) +----------------- +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 ----------------------------------- --- Generalisation case +-- 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 } + +----------------------------------- +-- 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 @@ -145,122 +534,78 @@ tc_sub _ (TyVarTy tv) act_sty act_ty -- g :: Ord b => b->b -- Consider f g ! -tc_sub exp_sty expected_ty act_sty actual_ty - | isSigmaTy expected_ty - = tcGen expected_ty ( - \ body_exp_ty -> tc_sub body_exp_ty body_exp_ty act_sty actual_ty - ) `thenTc` \ (gen_fn, co_fn, lie) -> - returnTc (gen_fn <.> co_fn, lie) +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 - = tcInstType actual_ty `thenNF_Tc` \ (tvs, theta, body_ty) -> - newDicts orig theta `thenNF_Tc` \ dicts -> - let - inst_fn e = mkHsDictApp (mkHsTyApp e (mkTyVarTys tvs)) - (map instToId dicts) - in - tc_sub exp_sty expected_ty body_ty body_ty `thenTc` \ (co_fn, lie) -> - returnTc (co_fn <.> mkCoercion inst_fn, lie `plusLIE` mkLIE dicts) - where - orig = Rank2Origin + = 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! - -tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ (TyVarTy tv) - = getTcTyVar tv `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - Just ty -> tc_sub exp_sty exp_ty ty ty - Nothing -> imitateFun tv exp_sty `thenNF_Tc` \ (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 `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - Just ty -> tc_sub ty ty act_sty act_ty - Nothing -> imitateFun tv act_sty `thenNF_Tc` \ (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 `thenTc_` - returnTc (idCoercion, emptyLIE) -\end{code} - -%************************************************************************ -%* * -\subsection{Functions} -%* * -%************************************************************************ - -\begin{code} -tcSub_fun exp_arg exp_res act_arg act_res - = tcSub act_arg exp_arg `thenTc` \ (co_fn_arg, lie1) -> - tcSub exp_res act_res `thenTc` \ (co_fn_res, lie2) -> - tcGetUnique `thenNF_Tc` \ 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 SLIT("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 - returnTc (coercion, lie1 `plusLIE` lie2) - -imitateFun :: TcTyVar -> TcType -> NF_TcM (TcType, TcType) -imitateFun tv ty - = ASSERT( not (isHoleTyVar tv) ) - -- 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.) - checkTcM (not (isSkolemTyVar tv)) - (failWithTcM (unifyWithSigErr tv ty)) `thenTc_` - - newTyVarTy openTypeKind `thenNF_Tc` \ arg -> - newTyVarTy openTypeKind `thenNF_Tc` \ res -> - putTcTyVar tv (mkFunTy arg res) `thenNF_Tc_` - returnNF_Tc (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} @@ -268,17 +613,36 @@ imitateFun tv ty %************************************************************************ \begin{code} -tcGen :: TcSigmaType -- expected_ty - -> (TcPhiType -> TcM (result, LIE)) -- spec_ty - -> TcM (ExprCoFn, result, LIE) +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) -- The expression has type: spec_ty -> expected_ty -tcGen expected_ty thing_inside -- We expect expected_ty to be a forall-type - -- If not, the call is a no-op - = tcInstType expected_ty `thenNF_Tc` \ (forall_tvs, theta, phi_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 + -- 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 - thing_inside phi_ty `thenTc` \ (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 @@ -291,106 +655,92 @@ tcGen expected_ty thing_inside -- We expect expected_ty to be a forall-type -- Conclusion: include the free vars of the expected_ty in the -- list of "free vars" for the signature check. - tcExtendGlobalTyVars free_tvs $ - tcAddErrCtxtM (sigCtxt forall_tvs theta phi_ty) $ + ; dicts <- newDicts (SigOrigin skol_info) theta + ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie - newDicts SignatureOrigin theta `thenNF_Tc` \ dicts -> - tcSimplifyCheck sig_msg forall_tvs dicts lie `thenTc` \ (free_lie, inst_binds) -> - checkSigTyVars forall_tvs free_tvs `thenTc` \ zonked_tvs -> + ; checkSigTyVarsWrt free_tvs forall_tvs + ; traceTc (text "tcGen:done") - 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 - returnTc (mkCoercion co_fn, result, free_lie) + 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 - sig_msg = ptext SLIT("When generalising the type of an expression") + free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs + sig_msg = ptext SLIT("expected type of an expression") \end{code} %************************************************************************ %* * -\subsection{Coercion functions} -%* * -%************************************************************************ - -\begin{code} -type Coercion a = Maybe (a -> a) - -- Nothing => identity fn - -type ExprCoFn = Coercion TypecheckedHsExpr -type PatCoFn = Coercion TcPat - -(<.>) :: Coercion a -> Coercion a -> Coercion a -- Composition -Nothing <.> Nothing = Nothing -Nothing <.> Just f = Just f -Just f <.> Nothing = Just f -Just f1 <.> Just f2 = Just (f1 . f2) - -(<$>) :: Coercion a -> a -> a -Just f <$> e = f e -Nothing <$> e = e - -mkCoercion :: (a -> a) -> Coercion a -mkCoercion f = Just f - -idCoercion :: Coercion a -idCoercion = Nothing - -isIdCoercion :: Coercion a -> Bool -isIdCoercion = isNothing -\end{code} - -%************************************************************************ -%* * -\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 ) - tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $ - uTys ty1 ty1 ty2 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 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 [] [] = returnTc () -unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_` - 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 [] = returnTc () -unifyTauTyList [ty] = returnTc () -unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_` - unifyTauTyList tys +unifyTypeList :: [TcTauType] -> TcM () +unifyTypeList [] = returnM () +unifyTypeList [ty] = returnM () +unifyTypeList (ty1:tys@(ty2:_)) = do { unifyType ty1 ty2 + ; unifyTypeList tys } \end{code} %************************************************************************ @@ -408,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 `thenTc_` 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 `thenTc_` 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 `thenTc_` 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 ~~~~~~~~~~~~~~~~~ @@ -483,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 @@ -540,291 +931,458 @@ 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)) `thenNF_Tc_` - getTcTyVar tv1 `thenNF_Tc` \ 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 - = returnTc () + = returnM () -- Distinct type variables - -- ASSERT maybe_ty1 /= Just | otherwise - = getTcTyVar tv2 `thenNF_Tc` \ 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) `thenNF_Tc_` - returnTc () - | 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 `thenNF_Tc_` - returnTc () - 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 - checkTcM (not (isSkolemTyVar tv1)) - (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_` - - -- Check that the kinds match - zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' -> - checkKinds swapped tv1 ps_ty2' `thenTc_` - - -- Occurs 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). - -- - -- That's why we have this two-state occurs-check - if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then - putTcTyVar tv1 ps_ty2' `thenNF_Tc_` - returnTc () - else - zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' -> - if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then - -- This branch rarely succeeds, except in strange cases - -- like that in the example above - putTcTyVar tv1 non_var_ty2' `thenNF_Tc_` - returnTc () - else - failWithTcM (unifyOccurCheck tv1 ps_ty2') - + k1_sub_k2 = k1 `isSubKind` k2 + k2_sub_k1 = k2 `isSubKind` k1 + 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. - - | tk2 `hasMoreBoxityInfo` tk1 = returnTc () +-- 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 - = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $ - unifyMisMatch k1 k2 - + = 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 -> 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} +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 -%************************************************************************ -%* * -\subsection[Unify-fun]{@unifyFunTy@} -%* * -%************************************************************************ +But consider + type A a = () -@subFunTy@ and @unifyFunTy@ is used to avoid the fruitless -creation of type variables. + f :: (A a -> a -> ()) -> () + f = \ _ -> () -* subFunTy is used when we might be faced with a "hole" type variable, - in which case we should create two new holes. + x :: () + x = f (\ x p -> p x) -* unifyFunTy is used when we expect to encounter only "ordinary" - type variables, so we should create new ordinary type variables +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} -subFunTy :: TcSigmaType -- Fail if ty isn't a function type - -> TcM (TcType, TcType) -- otherwise return arg and result types -subFunTy ty@(TyVarTy tyvar) - - = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - Just ty -> subFunTy ty - Nothing | isHoleTyVar tyvar - -> newHoleTyVarTy `thenNF_Tc` \ arg -> - newHoleTyVarTy `thenNF_Tc` \ res -> - putTcTyVar tyvar (mkFunTy arg res) `thenNF_Tc_` - returnTc (arg,res) - | otherwise - -> unify_fun_ty_help ty - -subFunTy ty - = case tcSplitFunTy_maybe ty of - Just arg_and_res -> returnTc arg_and_res - Nothing -> unify_fun_ty_help ty - - -unifyFunTy :: TcPhiType -- Fail if ty isn't a function type - -> TcM (TcType, TcType) -- otherwise return arg and result types - -unifyFunTy ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenNF_Tc` \ 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 -> returnTc arg_and_res - Nothing -> unify_fun_ty_help ty - -unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification - = newTyVarTy openTypeKind `thenNF_Tc` \ arg -> - newTyVarTy openTypeKind `thenNF_Tc` \ res -> - unifyTauTy ty (mkFunTy arg res) `thenTc_` - returnTc (arg,res) -\end{code} - -\begin{code} -unifyListTy :: TcType -- expected list type - -> TcM TcType -- list element type - -unifyListTy ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenNF_Tc` \ 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 -> returnTc arg_ty - other -> unify_list_ty_help ty - -unify_list_ty_help ty -- Revert to ordinary unification - = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty -> - unifyTauTy ty (mkListTy elt_ty) `thenTc_` - returnTc elt_ty - --- variant for parallel arrays +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 +-- +-- 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 -- -unifyPArrTy :: TcType -- expected list type - -> TcM TcType -- list element type - -unifyPArrTy ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenNF_Tc` \ 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 -> returnTc arg_ty - _ -> unify_parr_ty_help ty - -unify_parr_ty_help ty -- Revert to ordinary unification - = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty -> - unifyTauTy ty (mkPArrTy elt_ty) `thenTc_` - returnTc elt_ty +-- Compare this wth checkTauTvUpdate +-- +-- 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} -\begin{code} -unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType] -unifyTupleTy boxity arity ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenNF_Tc` \ 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 - -> returnTc arg_tys - other -> unify_tuple_ty_help boxity arity ty - -unify_tuple_ty_help boxity arity ty - = newTyVarTys arity kind `thenNF_Tc` \ arg_tys -> - unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_` - returnTc arg_tys - where - kind | isBoxed boxity = liftedTypeKind - | otherwise = openTypeKind -\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 - = tcAddErrCtxtM (unifyCtxt "kind" 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 [] [] = returnTc () -unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_` +unifyKinds [] [] = returnM () +unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenM_` unifyKinds ks1 ks2 -unifyKinds _ _ = panic "unifyKinds: length mis-match" +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} -unifyOpenTypeKind :: TcKind -> TcM () --- Ensures that the argument kind is of the form (Type bx) --- for some boxity bx - -unifyOpenTypeKind ty@(TyVarTy tyvar) - = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty -> - case maybe_ty of - Just ty' -> unifyOpenTypeKind ty' - other -> unify_open_kind_help ty - -unifyOpenTypeKind ty - | isTypeKind ty = returnTc () - | otherwise = unify_open_kind_help ty - -unify_open_kind_help ty -- Revert to ordinary unification - = newBoxityVar `thenNF_Tc` \ boxity -> - unifyKind ty (mkTyConApp typeCon [boxity]) +unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind)) +-- Like unifyFunTy, but does not fail; instead just returns Nothing + +unifyFunKind (KindVar kvar) + = readKindVar kvar `thenM` \ maybe_kind -> + 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)) } + +unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind)) +unifyFunKind other = returnM Nothing \end{code} - %************************************************************************ %* * \subsection[Unify-context]{Errors and contexts} @@ -835,63 +1393,148 @@ Errors ~~~~~~ \begin{code} -unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred - = zonkTcType ty1 `thenNF_Tc` \ ty1' -> - zonkTcType ty2 `thenNF_Tc` \ ty2' -> - returnNF_Tc (err ty1' ty2') +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 `thenNF_Tc` \ ty2' -> - returnNF_Tc (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 `thenNF_Tc` \ ty1' -> - zonkTcType ty2 `thenNF_Tc` \ 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 - -unifyOccurCheck tyvar ty - = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:")) - 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 = 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} %************************************************************************ %* * @@ -899,18 +1542,10 @@ unifyOccurCheck 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] - - (b) Still all distinct - eg matching signature [(a,b)] against inferred type [(p,p)] - [then a and b will be unified together] +@checkSigTyVars@ checks that a set of universally quantified type varaibles +are not mentioned in the environment. In particular: - (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 @@ -933,217 +1568,95 @@ 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] -- Universally-quantified type variables in the signature - -> TcTyVarSet -- Tyvars that are free in the type signature - -- Not necessarily zonked - -- These should *already* be in the free-in-env set, - -- and are used here only to improve the error message - -> TcM [TcTyVar] -- Zonked signature type variables - -checkSigTyVars [] free = returnTc [] -checkSigTyVars sig_tyvars free_tyvars - = zonkTcTyVars sig_tyvars `thenNF_Tc` \ sig_tys -> - tcGetGlobalTyVars `thenNF_Tc` \ globals -> - - checkTcM (allDistinctTyVars sig_tys globals) - (complain sig_tys globals) `thenTc_` - - returnTc (map (tcGetTyVar "checkSigTyVars") sig_tys) - +checkSigTyVars :: [TcTyVar] -> TcM () +checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs + +checkSigTyVarsWrt :: TcTyVarSet -> [TcTyVar] -> TcM () +-- The extra_tvs can include boxy type variables; +-- e.g. TcMatches.tcCheckExistentialPat +checkSigTyVarsWrt 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 + -- Guaranteed to be skolems + -> TcM () +check_sig_tyvars extra_tvs [] + = returnM () +check_sig_tyvars extra_tvs sig_tvs + = 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])) + + ; 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 - foldlNF_Tc check - (env2, emptyVarEnv, []) - (tidy_tvs `zip` tidy_tys) `thenNF_Tc` \ (env3, _, msgs) -> + main_msg = ptext SLIT("Inferred type is less polymorphic than expected") - failWithTcM (env3, main_msg $$ vcat msgs) - where - (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tyvars - (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)! - returnNF_Tc (tidy_env, acc, unify_msg sig_tyvar (quotes (ppr ty)) : msgs) ; - - Just tv -> - - case lookupVarEnv acc tv of { - Just sig_tyvar' -> -- Error (b)! - returnNF_Tc (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: - -- a) get the local TcIds and TyVars from the environment, - -- and pass them to find_globals (they might have tv free) - -- b) similarly, find any free_tyvars that mention tv - then tcGetEnv `thenNF_Tc` \ ve -> - find_globals tv tidy_env (tcLEnvElts ve) `thenNF_Tc` \ (tidy_env1, globs) -> - find_frees tv tidy_env1 [] (varSetElems free_tyvars) `thenNF_Tc` \ (tidy_env2, frees) -> - returnNF_Tc (tidy_env2, acc, escape_msg sig_tyvar tv globs frees : msgs) - - else -- All OK - returnNF_Tc (tidy_env, extendVarEnv acc tv sig_tyvar, msgs) - }} + 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) } ----------------------- --- find_globals looks at the value environment and finds values --- whose types mention the offending type variable. It has to be --- careful to zonk the Id's type first, so it has to be in the monad. --- We must be careful to pass it a zonked type variable, too. - -find_globals :: Var - -> TidyEnv - -> [TcTyThing] - -> NF_TcM (TidyEnv, [SDoc]) - -find_globals tv tidy_env things - = go tidy_env [] things - where - go tidy_env acc [] = returnNF_Tc (tidy_env, acc) - go tidy_env acc (thing : things) - = find_thing ignore_it tidy_env thing `thenNF_Tc` \ (tidy_env1, maybe_doc) -> - case maybe_doc of - Just d -> go tidy_env1 (d:acc) things - Nothing -> go tidy_env1 acc things - - ignore_it ty = not (tv `elemVarSet` tyVarsOfType ty) - ------------------------ -find_thing ignore_it tidy_env (ATcId id) - = zonkTcType (idType id) `thenNF_Tc` \ id_ty -> - if ignore_it id_ty then - returnNF_Tc (tidy_env, Nothing) - else let - (tidy_env', tidy_ty) = tidyOpenType tidy_env id_ty - msg = sep [ppr id <+> dcolon <+> ppr tidy_ty, - nest 2 (parens (ptext SLIT("bound at") <+> - ppr (getSrcLoc id)))] - in - returnNF_Tc (tidy_env', Just msg) - -find_thing ignore_it tidy_env (ATyVar tv) - = zonkTcTyVar tv `thenNF_Tc` \ tv_ty -> - if ignore_it tv_ty then - returnNF_Tc (tidy_env, Nothing) - else let - (tidy_env1, tv1) = tidyOpenTyVar tidy_env tv - (tidy_env2, tidy_ty) = tidyOpenType tidy_env1 tv_ty - msg = sep [ptext SLIT("Type variable") <+> quotes (ppr tv1) <+> eq_stuff, nest 2 bound_at] - - eq_stuff | Just tv' <- Type.getTyVar_maybe tv_ty, tv == tv' = empty - | otherwise = equals <+> ppr tv_ty - -- It's ok to use Type.getTyVar_maybe because ty is zonked by now - - bound_at = tyVarBindingInfo tv - in - returnNF_Tc (tidy_env2, Just msg) - ------------------------ -find_frees tv tidy_env acc [] - = returnNF_Tc (tidy_env, acc) -find_frees tv tidy_env acc (ftv:ftvs) - = zonkTcTyVar ftv `thenNF_Tc` \ ty -> - if tv `elemVarSet` tyVarsOfType ty then - let - (tidy_env', ftv') = tidyOpenTyVar tidy_env ftv - in - find_frees tv tidy_env' (ftv':acc) ftvs - else - find_frees tv tidy_env acc ftvs - - -escape_msg sig_tv tv globs frees - = mk_msg sig_tv <+> ptext SLIT("escapes") $$ - if not (null globs) then - vcat [pp_it <+> ptext SLIT("is mentioned in the environment:"), - nest 2 (vcat globs)] - else if not (null frees) then - vcat [ptext SLIT("It is reachable from the type variable(s)") <+> pprQuotedList frees, - nest 2 (ptext SLIT("which") <+> is_are <+> ptext SLIT("free in the signature")) - ] - else - empty -- Sigh. It's really hard to give a good error message - -- all the time. One bad case is an existential pattern match +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 - is_are | isSingleton frees = ptext SLIT("is") - | otherwise = ptext SLIT("are") - pp_it | sig_tv /= tv = ptext SLIT("It unifies with") <+> quotes (ppr tv) <> comma <+> ptext SLIT("which") - | otherwise = ptext SLIT("It") - - vcat_first :: Int -> [SDoc] -> SDoc - vcat_first n [] = empty - vcat_first 0 (x:xs) = text "...others omitted..." - vcat_first n (x:xs) = x $$ vcat_first (n-1) xs - - -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 \begin{code} -sigCtxt :: [TcTyVar] -> TcThetaType -> TcTauType - -> TidyEnv -> NF_TcM (TidyEnv, Message) -sigCtxt sig_tyvars sig_theta sig_tau tidy_env - = zonkTcType sig_tau `thenNF_Tc` \ actual_tau -> +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 -> let - (env1, tidy_sig_tyvars) = tidyOpenTyVars tidy_env sig_tyvars - (env2, tidy_sig_rho) = tidyOpenType env1 (mkRhoTy sig_theta sig_tau) - (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau - msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tyvars tidy_sig_rho), - ptext SLIT("Type to generalise:") <+> pprType tidy_actual_tau + (env1, tidy_sig_tvs) = tidyOpenTyVars tidy_env sig_tvs + (env2, tidy_sig_rho) = tidyOpenType env1 (mkPhiTy sig_theta sig_tau) + (env3, tidy_actual_tau) = tidyOpenType env2 actual_tau + sub_msg = vcat [ptext SLIT("Signature type: ") <+> pprType (mkForAllTys tidy_sig_tvs tidy_sig_rho), + 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 2 sub_msg] in - returnNF_Tc (env3, msg) - -sigPatCtxt bound_tvs bound_ids tidy_env - = returnNF_Tc (env1, - sep [ptext SLIT("When checking a pattern that binds"), - nest 4 (vcat (zipWith ppr_id show_ids tidy_tys))]) - where - show_ids = filter is_interesting bound_ids - is_interesting id = any (`elemVarSet` idFreeTyVars id) bound_tvs - - (env1, tidy_tys) = tidyOpenTypes tidy_env (map idType show_ids) - ppr_id id ty = ppr id <+> dcolon <+> ppr ty - -- Don't zonk the types so we get the separate, un-unified versions + returnM (env3, msg) \end{code} - -