X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2Ftypecheck%2FTcUnify.lhs;h=97487ce6b24c3599a9e50f12224dfbc2ab8e977f;hb=7bb59f381da3728f53ae5ea1bf821154f53c3f94;hp=3163802fffefe0d0f44f8c4c4c06d8b56e4c33c0;hpb=23f40f0e9be6d4aa5cf9ea31d73f4013f8e7b4bd;p=ghc-hetmet.git diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs index 3163802..97487ce 100644 --- a/ghc/compiler/typecheck/TcUnify.lhs +++ b/ghc/compiler/typecheck/TcUnify.lhs @@ -6,11 +6,11 @@ \begin{code} module TcUnify ( -- Full-blown subsumption - tcSubPat, tcSubExp, tcGen, - checkSigTyVars, checkSigTyVarsWrt, sigCtxt, findGlobals, + tcSubPat, tcSubExp, tcSub, tcGen, + checkSigTyVars, checkSigTyVarsWrt, bleatEscapedTvs, sigCtxt, -- Various unifications - unifyTauTy, unifyTauTyList, + unifyTauTy, unifyTauTyList, unifyTheta, unifyKind, unifyKinds, unifyFunKind, checkExpectedKind, @@ -26,46 +26,45 @@ module TcUnify ( #include "HsVersions.h" --- gaw 2004 -import HsSyn ( HsExpr(..) , MatchGroup(..), hsLMatchPats ) -import TcHsSyn ( mkHsLet, mkHsDictLam, +import HsSyn ( HsExpr(..) , MatchGroup(..), HsMatchContext(..), + hsLMatchPats, pprMatches, pprMatchContext ) +import TcHsSyn ( mkHsDictLet, mkHsDictLam, ExprCoFn, idCoercion, isIdCoercion, mkCoercion, (<.>), (<$>) ) import TypeRep ( Type(..), PredType(..), TyNote(..) ) import TcRnMonad -- TcType, amongst others import TcType ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType, - TcTyVarSet, TcThetaType, + TcTyVarSet, TcThetaType, Expected(..), TcTyVarDetails(..), SkolemInfo( GenSkol ), MetaDetails(..), - pprSkolemTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp, - tcSplitAppTy_maybe, tcSplitTyConApp_maybe, - tyVarsOfType, mkPhiTy, mkTyVarTy, + pprTcTyVar, isTauTy, isSigmaTy, mkFunTy, mkFunTys, mkTyConApp, + tcSplitAppTy_maybe, tcSplitTyConApp_maybe, tcEqType, + tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy, isMetaTyVar, typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy, tidyOpenType, tidyOpenTypes, tidyOpenTyVar, tidyOpenTyVars, - pprType, isSkolemTyVar ) + pprType, tidyKind, tidySkolemTyVar, isSkolemTyVar ) import Kind ( Kind(..), SimpleKind, KindVar, isArgTypeKind, - openTypeKind, liftedTypeKind, mkArrowKind, kindFunResult, + openTypeKind, liftedTypeKind, mkArrowKind, isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind, isSubKind, pprKind, splitKindFunTys ) import Inst ( newDicts, instToId, tcInstCall ) import TcMType ( condLookupTcTyVar, LookupTyVarResult(..), - putMetaTyVar, tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar, - newTyFlexiVarTy, zonkTcKind, - zonkType, zonkTcType, zonkTcTyVars, zonkTcTyVarsAndFV, + tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar, + newTyFlexiVarTy, zonkTcKind, zonkType, zonkTcType, zonkTcTyVarsAndFV, readKindVar, writeKindVar ) import TcSimplify ( tcSimplifyCheck ) +import TcIface ( checkWiredInTyCon ) import TcEnv ( tcGetGlobalTyVars, findGlobals ) -import TyCon ( TyCon, tyConArity, tyConTyVars ) +import TyCon ( TyCon, tyConArity, tyConTyVars, isFunTyCon ) import TysWiredIn ( listTyCon ) import Id ( Id, mkSysLocal ) import Var ( Var, varName, tyVarKind ) -import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, - varSetElems, intersectsVarSet, mkVarSet ) +import VarSet ( emptyVarSet, unitVarSet, unionVarSet, elemVarSet, varSetElems ) import VarEnv -import Name ( isSystemName, mkSysTvName ) +import Name ( Name, isSystemName, mkSysTvName ) import ErrUtils ( Message ) import SrcLoc ( noLoc ) import BasicTypes ( Arity ) -import Util ( equalLength, notNull ) +import Util ( notNull, equalLength ) import Outputable \end{code} @@ -80,9 +79,6 @@ 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 = newMutVar (error "Empty hole in typechecker") tcInfer :: (Expected ty -> TcM a) -> TcM (a,ty) @@ -155,12 +151,13 @@ creation of type variables. type variables, so we should create new ordinary type variables \begin{code} -subFunTys :: MatchGroup name +subFunTys :: HsMatchContext Name + -> MatchGroup Name -> Expected TcRhoType -- Fail if ty isn't a function type -> ([Expected TcRhoType] -> Expected TcRhoType -> TcM a) -> TcM a -subFunTys (MatchGroup (match:null_matches) _) (Infer hole) thing_inside +subFunTys ctxt (MatchGroup (match:null_matches) _) (Infer hole) thing_inside = -- This is the interesting case ASSERT( null null_matches ) do { pat_holes <- mapM (\ _ -> newHole) (hsLMatchPats match) @@ -179,13 +176,24 @@ subFunTys (MatchGroup (match:null_matches) _) (Infer hole) thing_inside -- And return the answer ; return res } -subFunTys (MatchGroup (match:matches) _) (Check ty) thing_inside - = ASSERT( all ((== length (hsLMatchPats match)) . length . hsLMatchPats) matches ) +subFunTys ctxt group@(MatchGroup (match:matches) _) (Check ty) thing_inside + = ASSERT( all ((== n_pats) . length . hsLMatchPats) matches ) -- Assertion just checks that all the matches have the same number of pats - do { (pat_tys, res_ty) <- unifyFunTys (length (hsLMatchPats match)) ty + do { (pat_tys, res_ty) <- unifyFunTys msg n_pats ty ; thing_inside (map Check pat_tys) (Check res_ty) } - -unifyFunTys :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType) + where + n_pats = length (hsLMatchPats match) + msg = case ctxt of + FunRhs fun -> ptext SLIT("The equation(s) for") <+> quotes (ppr fun) + <+> ptext SLIT("have") <+> speakNOf n_pats (ptext SLIT("argument")) + LambdaExpr -> sep [ ptext SLIT("The lambda expression") + <+> quotes (pprSetDepth 1 $ pprMatches ctxt group), + -- The pprSetDepth makes the abstraction print briefly + ptext SLIT("has") <+> speakNOf n_pats (ptext SLIT("arguments"))] + other -> pprPanic "subFunTys" (pprMatchContext ctxt) + + +unifyFunTys :: SDoc -> Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType) -- Fail if ty isn't a function type, otherwise return arg and result types -- The result types are guaranteed wobbly if the argument is wobbly -- @@ -198,12 +206,44 @@ unifyFunTys :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType) -- -- (b) GADTs: if the argument is not wobbly we do not want the result to be -unifyFunTys arity ty = unify_fun_ty True arity ty +{- + Error messages from unifyFunTys + The first line is passed in as error_herald + + The abstraction `\Just 1 -> ...' has two arguments + but its type `Maybe a -> a' has only one + + The equation(s) for `f' have two arguments + but its type `Maybe a -> a' has only one + + The section `(f 3)' requires 'f' to take two arguments + but its type `Int -> Int' has only one + + The function 'f' is applied to two arguments + but its type `Int -> Int' has only one +-} + +unifyFunTys error_herald arity ty + -- error_herald is the whole first line of the error message above + = do { (ok, args, res) <- unify_fun_ty True arity ty + ; if ok then return (args, res) + else failWithTc (mk_msg (length args)) } + where + mk_msg n_actual + = error_herald <> comma $$ + sep [ptext SLIT("but its type") <+> quotes (pprType ty), + if n_actual == 0 then ptext SLIT("has none") + else ptext SLIT("has only") <+> speakN n_actual] + +unify_fun_ty :: Bool -> Arity -> TcRhoType + -> TcM (Bool, -- Arity satisfied? + [TcSigmaType], -- Arg types found; length <= arity + TcRhoType) -- Result type unify_fun_ty use_refinement arity ty | arity == 0 = do { res_ty <- wobblify use_refinement ty - ; return ([], ty) } + ; return (True, [], ty) } unify_fun_ty use_refinement arity (NoteTy _ ty) = unify_fun_ty use_refinement arity ty @@ -212,24 +252,38 @@ unify_fun_ty use_refinement arity ty@(TyVarTy tv) = do { details <- condLookupTcTyVar use_refinement tv ; case details of IndirectTv use' ty' -> unify_fun_ty use' arity ty' - other -> unify_fun_help arity ty + DoneTv (MetaTv ref) -> ASSERT( liftedTypeKind `isSubKind` tyVarKind tv ) + -- The argument to unifyFunTys is always a type + -- Occurs check can't happen, of course + do { args <- mappM newTyFlexiVarTy (replicate arity argTypeKind) + ; res <- newTyFlexiVarTy openTypeKind + ; writeMutVar ref (Indirect (mkFunTys args res)) + ; return (True, args, res) } + DoneTv skol -> return (False, [], ty) } unify_fun_ty use_refinement arity ty - = case tcSplitFunTy_maybe ty of - Just (arg,res) -> do { arg' <- wobblify use_refinement arg - ; (args', res') <- unify_fun_ty use_refinement (arity-1) res - ; return (arg':args', res') } - - Nothing -> unify_fun_help arity ty - -- Usually an error, but ty could be (a Int Bool), which can match - -unify_fun_help :: Arity -> TcRhoType -> TcM ([TcSigmaType], TcRhoType) -unify_fun_help arity ty - = do { args <- mappM newTyFlexiVarTy (replicate arity argTypeKind) - ; res <- newTyFlexiVarTy openTypeKind - ; unifyTauTy ty (mkFunTys args res) - ; return (args, res) } + | Just (arg,res) <- tcSplitFunTy_maybe ty + = do { arg' <- wobblify use_refinement arg + ; (ok, args', res') <- unify_fun_ty use_refinement (arity-1) res + ; return (ok, arg':args', res') } + +unify_fun_ty use_refinement arity ty +-- Common cases are all done by now +-- At this point we usually have an error, but ty could +-- be (a Int Bool), or (a Bool), which can match +-- So just use the unifier. But catch any error so we just +-- return the success/fail boolean + = do { arg <- newTyFlexiVarTy argTypeKind + ; res <- newTyFlexiVarTy openTypeKind + ; let fun_ty = mkFunTy arg res + ; (_, mb_unit) <- tryTc (uTys True ty ty True fun_ty fun_ty) + ; case mb_unit of { + Nothing -> return (False, [], ty) ; + Just _ -> + do { (ok, args', res') <- unify_fun_ty use_refinement (arity-1) res + ; return (ok, arg:args', res') + } } } \end{code} \begin{code} @@ -238,12 +292,18 @@ zapToTyConApp :: TyCon -- T :: k1 -> ... -> kn -> * -> Expected TcSigmaType -- Expected type (T a b c) -> TcM [TcType] -- Element types, a b c -- Insists that the Expected type is not a forall-type - + -- It's used for wired-in tycons, so we call checkWiredInTyCOn + -- Precondition: never called with FunTyCon zapToTyConApp tc (Check ty) - = unifyTyConApp tc ty -- NB: fails for a forall-type + = ASSERT( not (isFunTyCon tc) ) -- Never called with FunTyCon + do { checkWiredInTyCon tc ; unifyTyConApp tc ty } -- NB: fails for a forall-type + zapToTyConApp tc (Infer hole) - = do { (tc_app, elt_tys) <- newTyConApp tc + = do { (_, elt_tys, _) <- tcInstTyVars (tyConTyVars tc) + ; let tc_app = mkTyConApp tc elt_tys ; writeMutVar hole tc_app + ; traceTc (text "zap" <+> ppr tc) + ; checkWiredInTyCon tc ; return elt_tys } zapToListTy :: Expected TcType -> TcM TcType -- Special case for lists @@ -252,69 +312,79 @@ zapToListTy exp_ty = do { [elt_ty] <- zapToTyConApp listTyCon exp_ty ---------------------- unifyTyConApp :: TyCon -> TcType -> TcM [TcType] -unifyTyConApp tc ty = unify_tc_app True tc ty - -- Add a boolean flag to remember whether to use - -- the type refinement or not +unifyTyConApp tc ty + = ASSERT( not (isFunTyCon tc) ) -- Never called with FunTyCon + unify_tc_app (tyConArity tc) True tc ty + -- Add a boolean flag to remember whether + -- to use the type refinement or not unifyListTy :: TcType -> TcM TcType -- Special case for lists unifyListTy exp_ty = do { [elt_ty] <- unifyTyConApp listTyCon exp_ty ; return elt_ty } ---------- -unify_tc_app use_refinement tc (NoteTy _ ty) - = unify_tc_app use_refinement tc ty - -unify_tc_app use_refinement tc ty@(TyVarTy tyvar) - = do { details <- condLookupTcTyVar use_refinement tyvar +unify_tc_app n_args use_refinement tc (NoteTy _ ty) + = unify_tc_app n_args use_refinement tc ty + +unify_tc_app n_args use_refinement tc (TyConApp tycon arg_tys) + | tycon == tc + = ASSERT( n_args == length arg_tys ) -- ty::* + mapM (wobblify use_refinement) arg_tys + +unify_tc_app n_args use_refinement tc (AppTy fun_ty arg_ty) + = do { arg_ty' <- wobblify use_refinement arg_ty + ; arg_tys <- unify_tc_app (n_args - 1) use_refinement tc fun_ty + ; return (arg_tys ++ [arg_ty']) } + +unify_tc_app n_args use_refinement tc ty@(TyVarTy tyvar) + = do { traceTc (text "unify_tc_app: tyvar" <+> pprTcTyVar tyvar) + ; details <- condLookupTcTyVar use_refinement tyvar ; case details of - IndirectTv use' ty' -> unify_tc_app use' tc ty' - other -> unify_tc_app_help tc ty + IndirectTv use' ty' -> unify_tc_app n_args use' tc ty' + other -> unify_tc_app_help n_args tc ty } -unify_tc_app use_refinement tc ty - | Just (tycon, arg_tys) <- tcSplitTyConApp_maybe ty, - tycon == tc - = ASSERT( tyConArity tycon == length arg_tys ) -- ty::* - mapM (wobblify use_refinement) arg_tys - -unify_tc_app use_refinement tc ty = unify_tc_app_help tc ty +unify_tc_app n_args use_refinement tc ty = unify_tc_app_help n_args tc ty ----------- -unify_tc_app_help tc ty -- Revert to ordinary unification - = do { (tc_app, arg_tys) <- newTyConApp tc +unify_tc_app_help n_args tc ty -- Revert to ordinary unification + = do { (_, elt_tys, _) <- tcInstTyVars (take n_args (tyConTyVars tc)) + ; let tc_app = mkTyConApp tc elt_tys ; if not (isTauTy ty) then -- Can happen if we call zapToTyConApp tc (forall a. ty) unifyMisMatch ty tc_app else do { unifyTauTy ty tc_app - ; returnM arg_tys } } + ; returnM elt_tys } } ---------------------- -unifyAppTy :: TcType -- Expected type function: m - -> TcType -- Type to split: m a - -> TcM TcType -- Type arg: a -unifyAppTy tc ty = unify_app_ty True tc ty +unifyAppTy :: TcType -- Type to split: m a + -> TcM (TcType, TcType) -- (m,a) +-- Assumes (m:*->*) + +unifyAppTy ty = unify_app_ty True ty -unify_app_ty use tc (NoteTy _ ty) = unify_app_ty use tc ty +unify_app_ty use (NoteTy _ ty) = unify_app_ty use ty -unify_app_ty use tc ty@(TyVarTy tyvar) +unify_app_ty use ty@(TyVarTy tyvar) = do { details <- condLookupTcTyVar use tyvar ; case details of - IndirectTv use' ty' -> unify_app_ty use' tc ty' - other -> unify_app_ty_help tc ty + IndirectTv use' ty' -> unify_app_ty use' ty' + other -> unify_app_ty_help ty } -unify_app_ty use tc ty +unify_app_ty use ty | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty - = do { unifyTauTy tc fun_ty - ; wobblify use arg_ty } + = do { fun' <- wobblify use fun_ty + ; arg' <- wobblify use arg_ty + ; return (fun', arg') } - | otherwise = unify_app_ty_help tc ty + | otherwise = unify_app_ty_help ty -unify_app_ty_help tc ty -- Revert to ordinary unification - = do { arg_ty <- newTyFlexiVarTy (kindFunResult (typeKind tc)) - ; unifyTauTy (mkAppTy tc arg_ty) ty - ; return arg_ty } +unify_app_ty_help ty -- Revert to ordinary unification + = do { fun_ty <- newTyFlexiVarTy (mkArrowKind liftedTypeKind liftedTypeKind) + ; arg_ty <- newTyFlexiVarTy liftedTypeKind + ; unifyTauTy (mkAppTy fun_ty arg_ty) ty + ; return (fun_ty, arg_ty) } ---------------------- @@ -323,17 +393,16 @@ wobblify :: Bool -- True <=> don't wobblify -> TcM TcTauType -- Return a wobbly type. At the moment we do that by -- allocating a fresh meta type variable. -wobblify True ty = return ty +wobblify True ty = return ty -- Don't wobblify + +wobblify False ty@(TyVarTy tv) + | isMetaTyVar tv = return ty -- Already wobbly + wobblify False ty = do { uniq <- newUnique ; tv <- newMetaTyVar (mkSysTvName uniq FSLIT("w")) (typeKind ty) (Indirect ty) ; return (mkTyVarTy tv) } - ----------------------- -newTyConApp :: TyCon -> TcM (TcTauType, [TcTauType]) -newTyConApp tc = do { (tvs, args, _) <- tcInstTyVars (tyConTyVars tc) - ; return (mkTyConApp tc args, args) } \end{code} @@ -383,19 +452,33 @@ tcSubPat :: TcSigmaType -- Pattern type signature -> TcM () -- In patterns we insist on an exact match; hence no CoFn returned -- See Note [Pattern coercions] in TcPat +-- However, we can't call unify directly, because both types might be +-- polymorphic; hence the call to tcSub, followed by a check for +-- equal types. (We can't just check for the identity coercion, because +-- in the polymorphic case we might get back something eta-equivalent to +-- the identity coercion, but that's not easy to tell.) tcSubPat sig_ty (Infer hole) = do { sig_ty' <- zonkTcType sig_ty ; writeMutVar hole sig_ty' -- See notes with tcSubExp above ; return () } +-- This tcSub followed by tcEqType checks for identical types +-- It'd be done more neatly by augmenting the unifier to deal with +-- (identically shaped) for-all types. + tcSubPat sig_ty (Check exp_ty) = do { co_fn <- tcSub sig_ty exp_ty - - ; if isIdCoercion co_fn then + ; sig_ty' <- zonkTcType sig_ty + ; exp_ty' <- zonkTcType exp_ty + ; if tcEqType sig_ty' exp_ty' then return () - else - unifyMisMatch sig_ty exp_ty } + else do + { (env, msg) <- misMatchMsg sig_ty' exp_ty' + ; failWithTcM (env, msg $$ extra) } } + where + extra | isTauTy sig_ty = empty + | otherwise = ptext SLIT("Polymorphic types must match exactly in patterns") \end{code} @@ -498,11 +581,11 @@ tc_sub _ (FunTy exp_arg exp_res) _ (FunTy act_arg act_res) -- I'm not quite sure what to do about this! tc_sub exp_sty exp_ty@(FunTy exp_arg exp_res) _ act_ty - = do { ([act_arg], act_res) <- unifyFunTys 1 act_ty + = do { (act_arg, act_res) <- unify_fun act_ty ; tcSub_fun exp_arg exp_res act_arg act_res } tc_sub _ exp_ty act_sty act_ty@(FunTy act_arg act_res) - = do { ([exp_arg], exp_res) <- unifyFunTys 1 exp_ty + = do { (exp_arg, exp_res) <- unify_fun exp_ty ; tcSub_fun exp_arg exp_res act_arg act_res } ----------------------------------- @@ -511,6 +594,15 @@ tc_sub _ exp_ty act_sty act_ty@(FunTy act_arg act_res) tc_sub exp_sty expected_ty act_sty actual_ty = uTys True exp_sty expected_ty True act_sty actual_ty `thenM_` returnM idCoercion + +----------------------------------- +-- A helper to make a function type match +-- The error message isn't very good, but that's a problem with +-- all of this subsumption code +unify_fun ty + = do { (ok, args, res) <- unify_fun_ty True 1 ty + ; if ok then return (head args, res) + else failWithTc (ptext SLIT("Expecting a function type, but found") <+> quotes (ppr ty))} \end{code} \begin{code} @@ -556,12 +648,26 @@ tcGen :: TcSigmaType -- expected_ty tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall-type -- If not, the call is a no-op - = do { span <- getSrcSpanM - ; let rigid_info = GenSkol expected_ty span - ; (forall_tvs, theta, phi_ty) <- tcSkolType rigid_info expected_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) <- tcSkolType 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 - ; (result, lie) <- getLIE (thing_inside phi_ty) + ; (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 @@ -574,18 +680,9 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall -- Conclusion: include the free vars of the expected_ty in the -- list of "free vars" for the signature check. - ; dicts <- newDicts (SigOrigin rigid_info) theta + ; dicts <- newDicts (SigOrigin skol_info) theta ; inst_binds <- tcSimplifyCheck sig_msg forall_tvs dicts lie -#ifdef DEBUG - ; forall_tys <- zonkTcTyVars forall_tvs - ; 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]) -#endif - ; checkSigTyVarsWrt free_tvs forall_tvs ; traceTc (text "tcGen:done") @@ -594,7 +691,7 @@ tcGen expected_ty extra_tvs thing_inside -- We expect expected_ty to be a forall -- 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 forall_tvs (mkHsDictLam dict_ids (mkHsLet inst_binds (noLoc e))) + co_fn e = TyLam forall_tvs (mkHsDictLam dict_ids (mkHsDictLet inst_binds (noLoc e))) ; returnM (mkCoercion co_fn, result) } where free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs @@ -623,6 +720,12 @@ unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred ASSERT2( isTauTy ty2, ppr ty2 ) addErrCtxtM (unifyCtxt "type" ty1 ty2) $ uTys True ty1 ty1 True ty2 ty2 + +unifyTheta :: TcThetaType -> TcThetaType -> TcM () +unifyTheta theta1 theta2 + = do { checkTc (equalLength theta1 theta2) + (ptext SLIT("Contexts differ in length")) + ; unifyTauTyLists True (map mkPredTy theta1) True (map mkPredTy theta2) } \end{code} @unifyTauTyList@ unifies corresponding elements of two lists of @@ -700,12 +803,7 @@ uTys r1 _ (PredTy (ClassP c1 tys1)) r2 _ (PredTy (ClassP c2 tys2)) uTys r1 _ (FunTy fun1 arg1) r2 _ (FunTy fun2 arg2) = uTys r1 fun1 fun1 r2 fun2 fun2 `thenM_` uTys r1 arg1 arg1 r2 arg2 arg2 - -- NewType constructors must match -uTys r1 _ (NewTcApp tc1 tys1) r2 _ (NewTcApp tc2 tys2) - | tc1 == tc2 = unifyTauTyLists r1 tys1 r2 tys2 - -- See Note [TyCon app] - - -- Ordinary type constructors must match + -- Type constructors must match uTys r1 ps_ty1 (TyConApp con1 tys1) r2 ps_ty2 (TyConApp con2 tys2) | con1 == con2 = unifyTauTyLists r1 tys1 r2 tys2 -- See Note [TyCon app] @@ -823,31 +921,57 @@ uVar swapped r1 tv1 r2 ps_ty2 ty2 case details of IndirectTv r1' ty1 | swapped -> uTys r2 ps_ty2 ty2 r1' ty1 ty1 -- Swap back | otherwise -> uTys r1' ty1 ty1 r2 ps_ty2 ty2 -- Same order - FlexiTv -> uFlexiVar swapped tv1 r2 ps_ty2 ty2 - RigidTv -> uRigidVar swapped tv1 r2 ps_ty2 ty2 - - -- Expand synonyms; ignore FTVs -uFlexiVar :: Bool -> TcTyVar -> - Bool -> -- Allow refinements to ty2 - TcTauType -> TcTauType -> TcM () --- Invariant: tv1 is Flexi -uFlexiVar swapped tv1 r2 ps_ty2 (NoteTy n2 ty2) - = uFlexiVar swapped tv1 r2 ps_ty2 ty2 - -uFlexiVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2) + DoneTv details1 -> uDoneVar swapped tv1 details1 r2 ps_ty2 ty2 + +---------------- +uDoneVar :: Bool -- Args are swapped + -> TcTyVar -> TcTyVarDetails -- Tyvar 1 + -> Bool -- Allow refinements to ty2 + -> TcTauType -> TcTauType -- Type 2 + -> TcM () +-- Invariant: tyvar 1 is not unified with anything + +uDoneVar swapped tv1 details1 r2 ps_ty2 (NoteTy n2 ty2) + = -- Expand synonyms; ignore FTVs + uDoneVar swapped tv1 details1 r2 ps_ty2 ty2 + +uDoneVar swapped tv1 details1 r2 ps_ty2 ty2@(TyVarTy tv2) -- Same type variable => no-op | tv1 == tv2 = returnM () -- Distinct type variables | otherwise - = condLookupTcTyVar r2 tv2 `thenM` \ details -> - case details of - IndirectTv b ty2' -> uFlexiVar swapped tv1 b ty2' ty2' - FlexiTv | update_tv2 -> putMetaTyVar tv2 (TyVarTy tv1) - | otherwise -> updateFlexi swapped tv1 ty2 - RigidTv -> updateFlexi swapped tv1 ty2 - -- Note that updateFlexi does a sub-kind check + = do { lookup2 <- condLookupTcTyVar r2 tv2 + ; case lookup2 of + IndirectTv b ty2' -> uDoneVar swapped tv1 details1 b ty2' ty2' + DoneTv details2 -> uDoneVars swapped tv1 details1 tv2 details2 + } + +uDoneVar swapped tv1 details1 r2 ps_ty2 non_var_ty2 -- ty2 is not a type variable + = case details1 of + MetaTv ref1 -> do { -- 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 + ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2 + ; updateMeta swapped tv1 ref1 ty2 } + + skolem_details -> unifyMisMatch (TyVarTy tv1) ps_ty2 + + +---------------- +uDoneVars :: Bool -- Args are swapped + -> TcTyVar -> TcTyVarDetails -- Tyvar 1 + -> TcTyVar -> TcTyVarDetails -- Tyvar 2 + -> TcM () +-- Invarant: the type variables are distinct, +-- and are not already unified with anything + +uDoneVars swapped tv1 (MetaTv ref1) tv2 details2 + = case details2 of + MetaTv ref2 | update_tv2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) + other -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2) + -- Note that updateMeta does a sub-kind check -- We might unify (a b) with (c d) where b::*->* and d::*; this should fail where k1 = tyVarKind tv1 @@ -859,46 +983,27 @@ uFlexiVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2) -- so we can choose which to do. nicer_to_update_tv2 = isSystemName (varName tv2) - -- Try to update sys-y type variables in preference to sig-y ones - - -- First one is flexi, second one isn't a type variable -uFlexiVar swapped tv1 r2 ps_ty2 non_var_ty2 - = -- 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 - do { ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2 - ; updateFlexi swapped tv1 ty2 } - --- Ready to update tv1, which is flexi; occurs check is done -updateFlexi swapped tv1 ty2 - = do { checkKinds swapped tv1 ty2 - ; putMetaTyVar tv1 ty2 } - - -uRigidVar :: Bool -> TcTyVar - -> Bool -> -- Allow refinements to ty2 - TcTauType -> TcTauType -> TcM () --- Invariant: tv1 is Rigid -uRigidVar swapped tv1 r2 ps_ty2 (NoteTy n2 ty2) - = uRigidVar swapped tv1 r2 ps_ty2 ty2 - - -- The both-type-variable case -uRigidVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2) - -- Same type variable => no-op - | tv1 == tv2 - = returnM () + -- Try to update sys-y type variables in preference to ones + -- gotten (say) by instantiating a polymorphic function with + -- a user-written type sig + +uDoneVars swapped tv1 (SkolemTv _) tv2 details2 + = case details2 of + MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) + other -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2) - -- Distinct type variables - | otherwise - = condLookupTcTyVar r2 tv2 `thenM` \ details -> - case details of - IndirectTv b ty2' -> uRigidVar swapped tv1 b ty2' ty2' - FlexiTv -> updateFlexi swapped tv2 (TyVarTy tv1) - RigidTv -> unifyMisMatch (TyVarTy tv1) (TyVarTy tv2) +uDoneVars swapped tv1 (SigSkolTv _ ref1) tv2 details2 + = case details2 of + MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1) + SigSkolTv _ _ -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2) + other -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2) - -- Second one isn't a type variable -uRigidVar swapped tv1 r2 ps_ty2 non_var_ty2 - = unifyMisMatch (TyVarTy tv1) ps_ty2 +---------------- +updateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM () +-- Update tv1, which is flexi; occurs check is alrady done +updateMeta swapped tv1 ref1 ty2 + = do { checkKinds swapped tv1 ty2 + ; writeMutVar ref1 (Indirect ty2) } \end{code} \begin{code} @@ -915,7 +1020,6 @@ checkKinds swapped tv1 ty2 -- unlifted type: e.g. (id 3#) is illegal = addErrCtxtM (unifyKindCtxt swapped tv1 ty2) $ unifyKindMisMatch k1 k2 - where (k1,k2) | swapped = (tk2,tk1) | otherwise = (tk1,tk2) @@ -983,7 +1087,6 @@ okToUnifyWith tv ty ok (AppTy t1 t2) = ok t1 `and` ok t2 ok (FunTy t1 t2) = ok t1 `and` ok t2 ok (TyConApp _ ts) = oks ts - ok (NewTcApp _ ts) = oks ts ok (ForAllTy _ _) = Just NotMonoType ok (PredTy st) = ok_st st ok (NoteTy (FTVNote _) t) = ok t @@ -1168,12 +1271,15 @@ unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 infer pp2 = ppr ty2' <+> dcolon <+> ppr (typeKind ty2) unifyMisMatch ty1 ty2 + = do { (env, msg) <- misMatchMsg ty1 ty2 + ; failWithTcM (env, msg) } + +misMatchMsg ty1 ty2 = do { (env1, pp1, extra1) <- ppr_ty emptyTidyEnv ty1 ; (env2, pp2, extra2) <- ppr_ty env1 ty2 - ; let msg = sep [sep [ptext SLIT("Couldn't match") <+> pp1, nest 7 (ptext SLIT("against") <+> pp2)], - nest 2 extra1, nest 2 extra2] - in - failWithTcM (env2, msg) } + ; 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 @@ -1182,9 +1288,11 @@ ppr_ty env ty simple_result = (env1, quotes (ppr tidy_ty), empty) ; case tidy_ty of TyVarTy tv - | isSkolemTyVar tv -> return (env1, pp_rigid tv, - pprSkolemTyVar tv) + | isSkolemTyVar tv -> return (env2, pp_rigid tv', + pprTcTyVar tv') | otherwise -> return simple_result + where + (env2, tv') = tidySkolemTyVar env1 tv other -> return simple_result } where pp_rigid tv = ptext SLIT("the rigid variable") <+> quotes (ppr tv) @@ -1224,9 +1332,9 @@ 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) -> + = tryTc (unifyKind exp_kind act_kind) `thenM` \ (_errs, mb_r) -> case mb_r of { - Just _ -> returnM () ; -- Unification succeeded + Just r -> returnM () ; -- Unification succeeded Nothing -> -- So there's definitely an error @@ -1238,6 +1346,9 @@ checkExpectedKind ty act_kind exp_kind (act_as, _) = splitKindFunTys act_kind n_exp_as = length exp_as n_act_as = length act_as + + (env1, tidy_exp_kind) = tidyKind emptyTidyEnv 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") @@ -1253,11 +1364,14 @@ checkExpectedKind ty act_kind exp_kind <+> ptext SLIT("is lifted") | otherwise -- E.g. Monad [Int] - = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma, - ptext SLIT("but") <+> quotes (ppr ty) <+> - ptext SLIT("has kind") <+> quotes (pprKind act_kind)] + = 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 - failWithTc (ptext SLIT("Kind error:") <+> err) + failWithTcM (env2, err $$ more_info) } \end{code} @@ -1267,18 +1381,10 @@ checkExpectedKind ty act_kind exp_kind %* * %************************************************************************ -@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 @@ -1301,28 +1407,6 @@ 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 () checkSigTyVars sig_tvs = check_sig_tyvars emptyVarSet sig_tvs @@ -1337,82 +1421,60 @@ check_sig_tyvars -- tyvars should not mention any of these -- Guaranteed already zonked. -> [TcTyVar] -- Universally-quantified type variables in the signature - -- Not guaranteed zonked. + -- Guaranteed to be skolems -> TcM () - check_sig_tyvars extra_tvs [] = returnM () check_sig_tyvars extra_tvs sig_tvs - = do { gbl_tvs <- tcGetGlobalTyVars + = 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])) - -- Check that that the signature type vars are not free in the envt ; let env_tvs = gbl_tvs `unionVarSet` extra_tvs - ; checkM (not (mkVarSet sig_tvs `intersectsVarSet` env_tvs)) - (complain sig_tvs env_tvs) + ; ifM (any (`elemVarSet` env_tvs) sig_tvs) + (bleatEscapedTvs env_tvs sig_tvs sig_tvs) + } - ; ASSERT( all isSkolemTyVar sig_tvs ) - return () } +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 { (env3, msgs) <- foldlM check (env2, []) (tidy_tvs `zip` tidy_zonked_tvs) + ; failWithTcM (env3, main_msg $$ nest 2 (vcat msgs)) } where - complain sig_tvs globals - = -- "check" checks each sig tyvar in turn - foldlM check - (env, emptyVarEnv, []) - tidy_tvs `thenM` \ (env2, _, msgs) -> - - failWithTcM (env2, main_msg $$ nest 2 (vcat msgs)) - where - (env, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs - - main_msg = ptext SLIT("Inferred type is less polymorphic than expected") - - check (tidy_env, acc, msgs) tv - -- 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 lookupVarEnv acc tv of { - Just sig_tyvar' -> -- Error (b)! - returnM (tidy_env, acc, unify_msg tv 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) -> - -- This rigid type variable has escaped into the envt - -- We make it flexi so that subequent uses of these - -- variables don't give rise to a cascade of further errors - returnM (tidy_env1, acc, escape_msg tv globs : msgs) - - else -- All OK - returnM (tidy_env, extendVarEnv acc tv tv, msgs) - } -\end{code} + (env1, tidy_tvs) = tidyOpenTyVars emptyTidyEnv sig_tvs + (env2, tidy_zonked_tvs) = tidyOpenTyVars env1 zonked_tvs + main_msg = ptext SLIT("Inferred type is less polymorphic than expected") + + 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 globs - = mk_msg sig_tv <+> ptext SLIT("escapes") $$ - if notNull globs then - vcat [ptext SLIT("It 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. - -unify_msg tv thing = mk_msg tv <+> ptext SLIT("is unified with") <+> thing -mk_msg tv = ptext SLIT("Quantified type variable") <+> quotes (ppr tv) +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 + 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