X-Git-Url: http://git.megacz.com/?p=ghc-hetmet.git;a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcUnify.lhs;h=572ad4437cfd2489ad95f2a6f266c1b2fe54db80;hp=ade2db0d4935692b3334cb8f2a492a2ee553d77a;hb=HEAD;hpb=b10d7d079ec9c3fc22d4700fe484dd297bddb805 diff --git a/compiler/typecheck/TcUnify.lhs b/compiler/typecheck/TcUnify.lhs index ade2db0..572ad44 100644 --- a/compiler/typecheck/TcUnify.lhs +++ b/compiler/typecheck/TcUnify.lhs @@ -20,15 +20,15 @@ module TcUnify ( matchExpectedListTy, matchExpectedPArrTy, matchExpectedTyConApp, matchExpectedAppTy, matchExpectedFunTys, matchExpectedFunKind, - wrapFunResCoercion + wrapFunResCoercion, failWithMisMatch ) where #include "HsVersions.h" import HsSyn import TypeRep - -import TcErrors ( typeExtraInfoMsg, unifyCtxt ) +import CoreUtils( mkPiTypes ) +import TcErrors ( unifyCtxt ) import TcMType import TcIface import TcRnMonad @@ -44,8 +44,6 @@ import VarEnv import Name import ErrUtils import BasicTypes -import Bag - import Maybes ( allMaybes ) import Util import Outputable @@ -104,7 +102,7 @@ expected type, becuase it expects that to have been done already matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys] -> Arity -> TcRhoType - -> TcM (CoercionI, [TcSigmaType], TcRhoType) + -> TcM (Coercion, [TcSigmaType], TcRhoType) -- If matchExpectFunTys n ty = (co, [t1,..,tn], ty_r) -- then co : ty ~ (t1 -> ... -> tn -> ty_r) @@ -123,7 +121,7 @@ matchExpectedFunTys herald arity orig_ty -- then co : ty ~ t1 -> .. -> tn -> ty_r go n_req ty - | n_req == 0 = return (IdCo ty, [], ty) + | n_req == 0 = return (mkReflCo ty, [], ty) go n_req ty | Just ty' <- tcView ty = go n_req ty' @@ -131,7 +129,7 @@ matchExpectedFunTys herald arity orig_ty go n_req (FunTy arg_ty res_ty) | not (isPredTy arg_ty) = do { (coi, tys, ty_r) <- go (n_req-1) res_ty - ; return (mkFunTyCoI (IdCo arg_ty) coi, arg_ty:tys, ty_r) } + ; return (mkFunCo (mkReflCo arg_ty) coi, arg_ty:tys, ty_r) } go _ (TyConApp tc _) -- A common case | not (isSynFamilyTyCon tc) @@ -174,14 +172,14 @@ matchExpectedFunTys herald arity orig_ty \begin{code} ---------------------- -matchExpectedListTy :: TcRhoType -> TcM (CoercionI, TcRhoType) +matchExpectedListTy :: TcRhoType -> TcM (Coercion, TcRhoType) -- Special case for lists matchExpectedListTy exp_ty = do { (coi, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty ; return (coi, elt_ty) } ---------------------- -matchExpectedPArrTy :: TcRhoType -> TcM (CoercionI, TcRhoType) +matchExpectedPArrTy :: TcRhoType -> TcM (Coercion, TcRhoType) -- Special case for parrs matchExpectedPArrTy exp_ty = do { (coi, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty @@ -190,7 +188,7 @@ matchExpectedPArrTy exp_ty ---------------------- matchExpectedTyConApp :: TyCon -- T :: k1 -> ... -> kn -> * -> TcRhoType -- orig_ty - -> TcM (CoercionI, -- T a b c ~ orig_ty + -> TcM (Coercion, -- T a b c ~ orig_ty [TcSigmaType]) -- Element types, a b c -- It's used for wired-in tycons, so we call checkWiredInTyCon @@ -201,7 +199,7 @@ matchExpectedTyConApp tc orig_ty = do { checkWiredInTyCon tc ; go (tyConArity tc) orig_ty [] } where - go :: Int -> TcRhoType -> [TcSigmaType] -> TcM (CoercionI, [TcSigmaType]) + go :: Int -> TcRhoType -> [TcSigmaType] -> TcM (Coercion, [TcSigmaType]) -- If go n ty tys = (co, [t1..tn] ++ tys) -- then co : T t1..tn ~ ty @@ -218,12 +216,12 @@ matchExpectedTyConApp tc orig_ty go n_req ty@(TyConApp tycon args) tys | tc == tycon = ASSERT( n_req == length args) -- ty::* - return (IdCo ty, args ++ tys) + return (mkReflCo ty, args ++ tys) go n_req (AppTy fun arg) tys | n_req > 0 = do { (coi, args) <- go (n_req - 1) fun (arg : tys) - ; return (mkAppTyCoI coi (IdCo arg), args) } + ; return (mkAppCo coi (mkReflCo arg), args) } go n_req ty tys = defer n_req ty tys @@ -237,7 +235,7 @@ matchExpectedTyConApp tc orig_ty ---------------------- matchExpectedAppTy :: TcRhoType -- orig_ty - -> TcM (CoercionI, -- m a ~ orig_ty + -> TcM (Coercion, -- m a ~ orig_ty (TcSigmaType, TcSigmaType)) -- Returns m, a -- If the incoming type is a mutable type variable of kind k, then -- matchExpectedAppTy returns a new type variable (m: * -> k); note the *. @@ -249,7 +247,7 @@ matchExpectedAppTy orig_ty | Just ty' <- tcView ty = go ty' | Just (fun_ty, arg_ty) <- tcSplitAppTy_maybe ty - = return (IdCo orig_ty, (fun_ty, arg_ty)) + = return (mkReflCo orig_ty, (fun_ty, arg_ty)) go (TyVarTy tv) | ASSERT( isTcTyVar tv) isMetaTyVar tv @@ -284,7 +282,6 @@ matchExpectedAppTy orig_ty %************************************************************************ All the tcSub calls have the form - tcSub actual_ty expected_ty which checks actual_ty <= expected_ty @@ -298,24 +295,24 @@ which takes an HsExpr of type actual_ty into one of type expected_ty. \begin{code} -tcSubType :: CtOrigin -> SkolemInfo -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +tcSubType :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper -- Check that ty_actual is more polymorphic than ty_expected -- Both arguments might be polytypes, so we must instantiate and skolemise -- Returns a wrapper of shape ty_actual ~ ty_expected -tcSubType origin skol_info ty_actual ty_expected +tcSubType origin ctxt ty_actual ty_expected | isSigmaTy ty_actual = do { (sk_wrap, inst_wrap) - <- tcGen skol_info ty_expected $ \ _ sk_rho -> do + <- tcGen ctxt ty_expected $ \ _ sk_rho -> do { (in_wrap, in_rho) <- deeplyInstantiate origin ty_actual ; coi <- unifyType in_rho sk_rho - ; return (coiToHsWrapper coi <.> in_wrap) } + ; return (coToHsWrapper coi <.> in_wrap) } ; return (sk_wrap <.> inst_wrap) } | otherwise -- Urgh! It seems deeply weird to have equality -- when actual is not a polytype, and it makes a big -- difference e.g. tcfail104 = do { coi <- unifyType ty_actual ty_expected - ; return (coiToHsWrapper coi) } + ; return (coToHsWrapper coi) } tcInfer :: (TcType -> TcM a) -> TcM (a, TcType) tcInfer tc_infer = do { ty <- newFlexiTyVarTy openTypeKind @@ -327,7 +324,7 @@ tcWrapResult :: HsExpr TcId -> TcRhoType -> TcRhoType -> TcM (HsExpr TcId) tcWrapResult expr actual_ty res_ty = do { coi <- unifyType actual_ty res_ty -- Both types are deeply skolemised - ; return (mkHsWrapCoI coi expr) } + ; return (mkHsWrapCo coi expr) } ----------------------------------- wrapFunResCoercion @@ -353,16 +350,16 @@ wrapFunResCoercion arg_tys co_fn_res %************************************************************************ \begin{code} -tcGen :: SkolemInfo -> TcType +tcGen :: UserTypeCtxt -> TcType -> ([TcTyVar] -> TcRhoType -> TcM result) -> TcM (HsWrapper, result) -- The expression has type: spec_ty -> expected_ty -tcGen skol_info expected_ty thing_inside +tcGen ctxt expected_ty thing_inside -- We expect expected_ty to be a forall-type -- If not, the call is a no-op = do { traceTc "tcGen" empty - ; (wrap, tvs', given, rho') <- deeplySkolemise skol_info expected_ty + ; (wrap, tvs', given, rho') <- deeplySkolemise expected_ty ; when debugIsOn $ traceTc "tcGen" $ vcat [ @@ -379,9 +376,13 @@ tcGen skol_info expected_ty thing_inside -- So now s' isn't unconstrained because it's linked to a. -- -- However [Oct 10] now that the untouchables are a range of - -- TcTyVars, all tihs is handled automatically with no need for + -- TcTyVars, all this is handled automatically with no need for -- extra faffing around + -- Use the *instantiated* type in the SkolemInfo + -- so that the names of displayed type variables line up + ; let skol_info = SigSkol ctxt (mkPiTypes given rho') + ; (ev_binds, result) <- checkConstraints skol_info tvs' given $ thing_inside tvs' rho' @@ -402,14 +403,11 @@ checkConstraints skol_info skol_tvs given thing_inside -- tcPolyExpr, which uses tcGen and hence checkConstraints. | otherwise - = do { (ev_binds, wanted, result) <- newImplication skol_info - skol_tvs given thing_inside - ; emitConstraints wanted - ; return (ev_binds, result) } + = newImplication skol_info skol_tvs given thing_inside newImplication :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM result - -> TcM (TcEvBinds, WantedConstraints, result) + -> TcM (TcEvBinds, result) newImplication skol_info skol_tvs given thing_inside = ASSERT2( all isTcTyVar skol_tvs, ppr skol_tvs ) ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs ) @@ -417,28 +415,28 @@ newImplication skol_info skol_tvs given thing_inside captureUntouchables $ thing_inside - ; if isEmptyBag wanted && not (hasEqualities given) + ; if isEmptyWC wanted && not (hasEqualities given) -- Optimisation : if there are no wanteds, and the givens -- are sufficiently simple, don't generate an implication -- at all. Reason for the hasEqualities test: -- we don't want to lose the "inaccessible alternative" -- error check then - return (emptyTcEvBinds, emptyWanteds, result) + return (emptyTcEvBinds, result) else do { ev_binds_var <- newTcEvBinds ; lcl_env <- getLclTypeEnv ; loc <- getCtLoc skol_info - ; let implic = Implic { ic_untch = untch - , ic_env = lcl_env - , ic_skols = mkVarSet skol_tvs - , ic_scoped = panic "emitImplication" - , ic_given = given - , ic_wanted = wanted - , ic_binds = ev_binds_var - , ic_loc = loc } - - ; return (TcEvBinds ev_binds_var, unitBag (WcImplic implic), result) } } + ; emitImplication $ Implic { ic_untch = untch + , ic_env = lcl_env + , ic_skols = mkVarSet skol_tvs + , ic_given = given + , ic_wanted = wanted + , ic_insol = insolubleWC wanted + , ic_binds = ev_binds_var + , ic_loc = loc } + + ; return (TcEvBinds ev_binds_var, result) } } \end{code} %************************************************************************ @@ -452,18 +450,18 @@ non-exported generic functions. \begin{code} --------------- -unifyType :: TcTauType -> TcTauType -> TcM CoercionI +unifyType :: TcTauType -> TcTauType -> TcM Coercion -- Actual and expected types -- Returns a coercion : ty1 ~ ty2 unifyType ty1 ty2 = uType [] ty1 ty2 --------------- -unifyPred :: PredType -> PredType -> TcM CoercionI +unifyPred :: PredType -> PredType -> TcM Coercion -- Actual and expected types unifyPred p1 p2 = uPred [UnifyOrigin (mkPredTy p1) (mkPredTy p2)] p1 p2 --------------- -unifyTheta :: TcThetaType -> TcThetaType -> TcM [CoercionI] +unifyTheta :: TcThetaType -> TcThetaType -> TcM [Coercion] -- Actual and expected types unifyTheta theta1 theta2 = do { checkTc (equalLength theta1 theta2) @@ -514,18 +512,23 @@ uType, uType_np, uType_defer :: [EqOrigin] -> TcType -- ty1 is the *actual* type -> TcType -- ty2 is the *expected* type - -> TcM CoercionI + -> TcM Coercion -------------- -- It is always safe to defer unification to the main constraint solver -- See Note [Deferred unification] uType_defer (item : origin) ty1 ty2 - = do { co_var <- newWantedCoVar ty1 ty2 - ; traceTc "utype_defer" (vcat [ppr co_var, ppr ty1, ppr ty2, ppr origin]) + = wrapEqCtxt origin $ + do { co_var <- newCoVar ty1 ty2 ; loc <- getCtLoc (TypeEqOrigin item) - ; wrapEqCtxt origin $ - emitConstraint (WcEvVar (WantedEvVar co_var loc)) - ; return $ ACo $ mkTyVarTy co_var } + ; emitFlat (mkEvVarX co_var loc) + + -- Error trace only + ; ctxt <- getErrCtxt + ; doc <- mkErrInfo emptyTidyEnv ctxt + ; traceTc "utype_defer" (vcat [ppr co_var, ppr ty1, ppr ty2, ppr origin, doc]) + + ; return $ mkCoVarCo co_var } uType_defer [] _ _ = panic "uType_defer" @@ -540,16 +543,16 @@ uType_np origin orig_ty1 orig_ty2 = do { traceTc "u_tys " $ vcat [ sep [ ppr orig_ty1, text "~", ppr orig_ty2] , ppr origin] - ; coi <- go origin orig_ty1 orig_ty2 - ; case coi of - ACo co -> traceTc "u_tys yields coercion:" (ppr co) - IdCo _ -> traceTc "u_tys yields no coercion" empty + ; coi <- go orig_ty1 orig_ty2 + ; if isReflCo coi + then traceTc "u_tys yields no coercion" empty + else traceTc "u_tys yields coercion:" (ppr coi) ; return coi } where bale_out :: [EqOrigin] -> TcM a bale_out origin = failWithMisMatch origin - go :: [EqOrigin] -> TcType -> TcType -> TcM CoercionI + go :: TcType -> TcType -> TcM Coercion -- The arguments to 'go' are always semantically identical -- to orig_ty{1,2} except for looking through type synonyms @@ -557,107 +560,108 @@ uType_np origin orig_ty1 orig_ty2 -- Note that we pass in *original* (before synonym expansion), -- so that type variables tend to get filled in with -- the most informative version of the type - go origin (TyVarTy tyvar1) ty2 = uVar origin NotSwapped tyvar1 ty2 - go origin ty1 (TyVarTy tyvar2) = uVar origin IsSwapped tyvar2 ty1 + go (TyVarTy tyvar1) ty2 = uVar origin NotSwapped tyvar1 ty2 + go ty1 (TyVarTy tyvar2) = uVar origin IsSwapped tyvar2 ty1 -- Expand synonyms: -- see Note [Unification and synonyms] -- Do this after the variable case so that we tend to unify - -- variables with un-expended type synonym - go origin ty1 ty2 - | Just ty1' <- tcView ty1 = uType origin ty1' ty2 - | Just ty2' <- tcView ty2 = uType origin ty1 ty2' - + -- variables with un-expanded type synonym + -- + -- Also NB that we recurse to 'go' so that we don't push a + -- new item on the origin stack. As a result if we have + -- type Foo = Int + -- and we try to unify Foo ~ Bool + -- we'll end up saying "can't match Foo with Bool" + -- rather than "can't match "Int with Bool". See Trac #4535. + go ty1 ty2 + | Just ty1' <- tcView ty1 = go ty1' ty2 + | Just ty2' <- tcView ty2 = go ty1 ty2' + -- Predicates - go origin (PredTy p1) (PredTy p2) = uPred origin p1 p2 - - -- Coercion functions: (t1a ~ t1b) => t1c ~ (t2a ~ t2b) => t2c - go origin ty1 ty2 - | Just (t1a,t1b,t1c) <- splitCoPredTy_maybe ty1, - Just (t2a,t2b,t2c) <- splitCoPredTy_maybe ty2 - = do { co1 <- uType origin t1a t2a - ; co2 <- uType origin t1b t2b - ; co3 <- uType origin t1c t2c - ; return $ mkCoPredCoI co1 co2 co3 } + go (PredTy p1) (PredTy p2) = uPred origin p1 p2 -- Functions (or predicate functions) just check the two parts - go origin (FunTy fun1 arg1) (FunTy fun2 arg2) + go (FunTy fun1 arg1) (FunTy fun2 arg2) = do { coi_l <- uType origin fun1 fun2 ; coi_r <- uType origin arg1 arg2 - ; return $ mkFunTyCoI coi_l coi_r } + ; return $ mkFunCo coi_l coi_r } -- Always defer if a type synonym family (type function) -- is involved. (Data families behave rigidly.) - go origin ty1@(TyConApp tc1 _) ty2 + go ty1@(TyConApp tc1 _) ty2 | isSynFamilyTyCon tc1 = uType_defer origin ty1 ty2 - go origin ty1 ty2@(TyConApp tc2 _) + go ty1 ty2@(TyConApp tc2 _) | isSynFamilyTyCon tc2 = uType_defer origin ty1 ty2 - go origin (TyConApp tc1 tys1) (TyConApp tc2 tys2) + go (TyConApp tc1 tys1) (TyConApp tc2 tys2) | tc1 == tc2 -- See Note [TyCon app] = do { cois <- uList origin uType tys1 tys2 - ; return $ mkTyConAppCoI tc1 cois } + ; return $ mkTyConAppCo tc1 cois } -- See Note [Care with type applications] - go origin (AppTy s1 t1) ty2 + go (AppTy s1 t1) ty2 | Just (s2,t2) <- tcSplitAppTy_maybe ty2 = do { coi_s <- uType_np origin s1 s2 -- See Note [Unifying AppTy] ; coi_t <- uType origin t1 t2 - ; return $ mkAppTyCoI coi_s coi_t } + ; return $ mkAppCo coi_s coi_t } - go origin ty1 (AppTy s2 t2) + go ty1 (AppTy s2 t2) | Just (s1,t1) <- tcSplitAppTy_maybe ty1 = do { coi_s <- uType_np origin s1 s2 ; coi_t <- uType origin t1 t2 - ; return $ mkAppTyCoI coi_s coi_t } + ; return $ mkAppCo coi_s coi_t } - go _ ty1 ty2 + go ty1 ty2 | tcIsForAllTy ty1 || tcIsForAllTy ty2 = unifySigmaTy origin ty1 ty2 -- Anything else fails - go origin _ _ = bale_out origin + go _ _ = bale_out origin -unifySigmaTy :: [EqOrigin] -> TcType -> TcType -> TcM CoercionI +unifySigmaTy :: [EqOrigin] -> TcType -> TcType -> TcM Coercion unifySigmaTy origin ty1 ty2 = do { let (tvs1, body1) = tcSplitForAllTys ty1 (tvs2, body2) = tcSplitForAllTys ty2 ; unless (equalLength tvs1 tvs2) (failWithMisMatch origin) - ; skol_tvs <- tcInstSkolTyVars UnkSkol tvs1 -- Not a helpful SkolemInfo + ; skol_tvs <- tcInstSkolTyVars tvs1 -- Get location from monad, not from tvs1 ; let tys = mkTyVarTys skol_tvs in_scope = mkInScopeSet (mkVarSet skol_tvs) - phi1 = substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1 - phi2 = substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2 --- untch = tyVarsOfType ty1 `unionVarSet` tyVarsOfType ty2 + phi1 = Type.substTy (mkTvSubst in_scope (zipTyEnv tvs1 tys)) body1 + phi2 = Type.substTy (mkTvSubst in_scope (zipTyEnv tvs2 tys)) body2 ; ((coi, _untch), lie) <- captureConstraints $ captureUntouchables $ uType origin phi1 phi2 -- Check for escape; e.g. (forall a. a->b) ~ (forall a. a->a) - ; let bad_lie = filterBag is_bad lie - is_bad w = any (`elemVarSet` tyVarsOfWanted w) skol_tvs - ; when (not (isEmptyBag bad_lie)) + -- VERY UNSATISFACTORY; the constraint might be fine, but + -- we fail eagerly because we don't have any place to put + -- the bindings from an implication constraint + -- This only works because most constraints get solved on the fly + -- See Note [Avoid deferring] + ; when (any (`elemVarSet` tyVarsOfWC lie) skol_tvs) (failWithMisMatch origin) -- ToDo: give details from bad_lie ; emitConstraints lie - ; return (foldr mkForAllTyCoI coi skol_tvs) } + ; return (foldr mkForAllCo coi skol_tvs) } ---------- -uPred :: [EqOrigin] -> PredType -> PredType -> TcM CoercionI +uPred :: [EqOrigin] -> PredType -> PredType -> TcM Coercion uPred origin (IParam n1 t1) (IParam n2 t2) | n1 == n2 = do { coi <- uType origin t1 t2 - ; return $ mkIParamPredCoI n1 coi } + ; return $ mkPredCo $ IParam n1 coi } uPred origin (ClassP c1 tys1) (ClassP c2 tys2) | c1 == c2 = do { cois <- uList origin uType tys1 tys2 -- Guaranteed equal lengths because the kinds check - ; return $ mkClassPPredCoI c1 cois } + ; return $ mkPredCo $ ClassP c1 cois } + uPred origin (EqPred ty1a ty1b) (EqPred ty2a ty2b) - = do { coia <- uType origin ty1a ty2a - ; coib <- uType origin ty1b ty2b - ; return $ mkEqPredCoI coia coib } + = do { coa <- uType origin ty1a ty2a + ; cob <- uType origin ty1b ty2b + ; return $ mkPredCo $ EqPred coa cob } uPred origin _ _ = failWithMisMatch origin @@ -801,7 +805,7 @@ of the substitution; rather, notice that @uVar@ (defined below) nips back into @uTys@ if it turns out that the variable is already bound. \begin{code} -uVar :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTauType -> TcM CoercionI +uVar :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTauType -> TcM Coercion uVar origin swapped tv1 ty2 = do { traceTc "uVar" (vcat [ ppr origin , ppr swapped @@ -819,13 +823,13 @@ uUnfilledVar :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTyVarDetails -- Tyvar 1 -> TcTauType -- Type 2 - -> TcM CoercionI + -> TcM Coercion -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar -- It might be a skolem, or untouchable, or meta uUnfilledVar origin swapped tv1 details1 (TyVarTy tv2) | tv1 == tv2 -- Same type variable => no-op - = return (IdCo (mkTyVarTy tv1)) + = return (mkReflCo (mkTyVarTy tv1)) | otherwise -- Distinct type variables = do { lookup2 <- lookupTcTyVar tv2 @@ -843,9 +847,13 @@ uUnfilledVar origin swapped tv1 details1 non_var_ty2 -- ty2 is not a type varia Just ty2' -> updateMeta tv1 ref1 ty2' } - _other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts + _other -> do { traceTc "Skolem defer" (ppr tv1); defer } -- Skolems of all sorts where - defer = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2 + defer | Just ty2' <- tcView non_var_ty2 -- Note [Avoid deferring] + -- non_var_ty2 isn't expanded yet + = uUnfilledVar origin swapped tv1 details1 ty2' + | otherwise + = unSwap swapped (uType_defer origin) (mkTyVarTy tv1) non_var_ty2 -- Occurs check or an untouchable: just defer -- NB: occurs check isn't necessarily fatal: -- eg tv1 occured in type family parameter @@ -855,7 +863,7 @@ uUnfilledVars :: [EqOrigin] -> SwapFlag -> TcTyVar -> TcTyVarDetails -- Tyvar 1 -> TcTyVar -> TcTyVarDetails -- Tyvar 2 - -> TcM CoercionI + -> TcM Coercion -- Invarant: The type variables are distinct, -- Neither is filled in yet @@ -880,8 +888,8 @@ uUnfilledVars origin swapped tv1 details1 tv2 details2 ty1 = mkTyVarTy tv1 ty2 = mkTyVarTy tv2 - nicer_to_update_tv1 _ (SigTv _) = True - nicer_to_update_tv1 (SigTv _) _ = False + nicer_to_update_tv1 _ SigTv = True + nicer_to_update_tv1 SigTv _ = False nicer_to_update_tv1 _ _ = isSystemName (Var.varName tv1) -- Try not to update SigTvs; and try to update sys-y type -- variables in preference to ones gotten (say) by @@ -944,14 +952,26 @@ checkTauTvUpdate tv ty = Just (EqPred ty1' ty2') -- Fall-through ok_pred _pty = Nothing - \end{code} +Note [Avoid deferring] +~~~~~~~~~~~~~~~~~~~~~~ +We try to avoid creating deferred constraints for two reasons. + * First, efficiency. + * Second, currently we can only defer some constraints + under a forall. See unifySigmaTy. +So expanding synonyms here is a good thing to do. Example (Trac #4917) + a ~ Const a b +where type Const a b = a. We can solve this immediately, even when +'a' is a skolem, just by expanding the synonym; and we should do so + in case this unification happens inside unifySigmaTy (sigh). + Note [Type synonyms and the occur check] -~~~~~~~~~~~~~~~~~~~~ -Generally speaking we need to update a variable with type synonyms not expanded, which -improves later error messages, except for when looking inside a type synonym may help resolve -a spurious occurs check error. Consider: +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Generally speaking we try to update a variable with type synonyms not +expanded, which improves later error messages, unless looking +inside a type synonym may help resolve a spurious occurs check +error. Consider: type A a = () f :: (A a -> a -> ()) -> () @@ -1013,7 +1033,7 @@ lookupTcTyVar tyvar Indirect ty -> return (Filled ty) Flexi -> do { is_untch <- isUntouchable tyvar ; let -- Note [Unifying untouchables] - ret_details | is_untch = SkolemTv UnkSkol + ret_details | is_untch = vanillaSkolemTv | otherwise = details ; return (Unfilled ret_details) } } | otherwise @@ -1022,10 +1042,10 @@ lookupTcTyVar tyvar details = ASSERT2( isTcTyVar tyvar, ppr tyvar ) tcTyVarDetails tyvar -updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM CoercionI +updateMeta :: TcTyVar -> TcRef MetaDetails -> TcType -> TcM Coercion updateMeta tv1 ref1 ty2 = do { writeMetaTyVarRef tv1 ref1 ty2 - ; return (IdCo ty2) } + ; return (mkReflCo ty2) } \end{code} Note [Unifying untouchables] @@ -1069,18 +1089,14 @@ failWithMisMatch (item:origin) ; env0 <- tcInitTidyEnv ; let (env1, pp_exp) = tidyOpenType env0 ty_exp (env2, pp_act) = tidyOpenType env1 ty_act - ; failWithTcM (misMatchMsg env2 pp_act pp_exp) } + ; failWithTcM (env2, misMatchMsg pp_act pp_exp) } failWithMisMatch [] = panic "failWithMisMatch" -misMatchMsg :: TidyEnv -> TcType -> TcType -> (TidyEnv, SDoc) -misMatchMsg env ty_act ty_exp - = (env2, sep [sep [ ptext (sLit "Couldn't match expected type") <+> quotes (ppr ty_exp) - , nest 12 $ ptext (sLit "with actual type") <+> quotes (ppr ty_act)] - , nest 2 (extra1 $$ extra2) ]) - where - (env1, extra1) = typeExtraInfoMsg env ty_exp - (env2, extra2) = typeExtraInfoMsg env1 ty_act +misMatchMsg :: TcType -> TcType -> SDoc +misMatchMsg ty_act ty_exp + = sep [ ptext (sLit "Couldn't match expected type") <+> quotes (ppr ty_exp) + , nest 12 $ ptext (sLit "with actual type") <+> quotes (ppr ty_act)] \end{code}