diff options
Diffstat (limited to 'compiler/typecheck/TcUnify.hs')
| -rw-r--r-- | compiler/typecheck/TcUnify.hs | 893 |
1 files changed, 490 insertions, 403 deletions
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index 1cbf5741b2..05a30fdf35 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -13,10 +13,11 @@ module TcUnify ( tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET, tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_NC_O, tcSubTypeET, - checkConstraints, buildImplicationFor, + checkConstraints, checkTvConstraints, + buildImplicationFor, -- Various unifications - unifyType, unifyTheta, unifyKind, noThing, + unifyType, unifyKind, uType, promoteTcType, swapOverTyVars, canSolveByUnification, @@ -24,22 +25,20 @@ module TcUnify ( -- Holes tcInferInst, tcInferNoInst, matchExpectedListTy, - matchExpectedPArrTy, matchExpectedTyConApp, matchExpectedAppTy, matchExpectedFunTys, matchActualFunTys, matchActualFunTysPart, matchExpectedFunKind, - wrapFunResCoercion, - - occCheckExpand, metaTyVarUpdateOK, - occCheckForErrors, OccCheckResult(..) + metaTyVarUpdateOK, occCheckForErrors, OccCheckResult(..) ) where #include "HsVersions.h" +import GhcPrelude + import HsSyn import TyCoRep import TcMType @@ -48,7 +47,7 @@ import TcType import Type import Coercion import TcEvidence -import Name ( isSystemName ) +import Name( isSystemName ) import Inst import TyCon import TysWiredIn @@ -61,10 +60,8 @@ import DynFlags import BasicTypes import Bag import Util -import Pair( pFst ) import qualified GHC.LanguageExtensions as LangExt import Outputable -import FastString import Control.Monad import Control.Arrow ( second ) @@ -98,6 +95,23 @@ This is used to construct a message of form The function 'f' is applied to two arguments but its type `Int -> Int' has only one +When visible type applications (e.g., `f @Int 1 2`, as in #13902) enter the +picture, we have a choice in deciding whether to count the type applications as +proper arguments: + + The function 'f' is applied to one visible type argument + and two value arguments + but its type `forall a. a -> a` has only one visible type argument + and one value argument + +Or whether to include the type applications as part of the herald itself: + + The expression 'f @Int' is applied to two arguments + but its type `Int -> Int` has only one + +The latter is easier to implement and is arguably easier to understand, so we +choose to implement that option. + Note [matchExpectedFunTys] ~~~~~~~~~~~~~~~~~~~~~~~~~~ matchExpectedFunTys checks that a sigma has the form @@ -201,10 +215,9 @@ matchExpectedFunTys herald arity orig_ty thing_inside -- Like 'matchExpectedFunTys', but used when you have an "actual" type, -- for example in function application -matchActualFunTys :: Outputable a - => SDoc -- See Note [Herald for matchExpectedFunTys] +matchActualFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys] -> CtOrigin - -> Maybe a -- the thing with type TcSigmaType + -> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType -> Arity -> TcSigmaType -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) @@ -215,10 +228,9 @@ matchActualFunTys herald ct_orig mb_thing arity ty -- | Variant of 'matchActualFunTys' that works when supplied only part -- (that is, to the right of some arrows) of the full function type -matchActualFunTysPart :: Outputable a - => SDoc -- See Note [Herald for matchExpectedFunTys] +matchActualFunTysPart :: SDoc -- See Note [Herald for matchExpectedFunTys] -> CtOrigin - -> Maybe a -- the thing with type TcSigmaType + -> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType -> Arity -> TcSigmaType -> [TcSigmaType] -- reversed args. See (*) below. @@ -347,13 +359,6 @@ matchExpectedListTy exp_ty = do { (co, [elt_ty]) <- matchExpectedTyConApp listTyCon exp_ty ; return (co, elt_ty) } ----------------------- -matchExpectedPArrTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType) --- Special case for parrs -matchExpectedPArrTy exp_ty - = do { (co, [elt_ty]) <- matchExpectedTyConApp parrTyCon exp_ty - ; return (co, elt_ty) } - --------------------- matchExpectedTyConApp :: TyCon -- T :: forall kv1 ... kvm. k1 -> ... -> kn -> * -> TcRhoType -- orig_ty @@ -391,7 +396,7 @@ matchExpectedTyConApp tc orig_ty -- kind-compatible with T. For example, suppose we have -- matchExpectedTyConApp T (f Maybe) -- where data T a = MkT a - -- Then we don't want to instantate T's data constructors with + -- Then we don't want to instantiate T's data constructors with -- (a::*) ~ Maybe -- because that'll make types that are utterly ill-kinded. -- This happened in Trac #7368 @@ -400,7 +405,7 @@ matchExpectedTyConApp tc orig_ty ; traceTc "matchExpectedTyConApp" (ppr tc $$ ppr (tyConTyVars tc) $$ ppr arg_tvs) ; let args = mkTyVarTys arg_tvs tc_template = mkTyConApp tc args - ; co <- unifyType noThing tc_template orig_ty + ; co <- unifyType Nothing tc_template orig_ty ; return (co, args) } ---------------------- @@ -432,7 +437,7 @@ matchExpectedAppTy orig_ty defer = do { ty1 <- newFlexiTyVarTy kind1 ; ty2 <- newFlexiTyVarTy kind2 - ; co <- unifyType noThing (mkAppTy ty1 ty2) orig_ty + ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty ; return (co, (ty1, ty2)) } orig_kind = typeKind orig_ty @@ -531,9 +536,8 @@ skolemising the type. -- | Call this variant when you are in a higher-rank situation and -- you know the right-hand type is deeply skolemised. -tcSubTypeHR :: Outputable a - => CtOrigin -- ^ of the actual type - -> Maybe a -- ^ If present, it has type ty_actual +tcSubTypeHR :: CtOrigin -- ^ of the actual type + -> Maybe (HsExpr GhcRn) -- ^ If present, it has type ty_actual -> TcSigmaType -> ExpRhoType -> TcM HsWrapper tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt @@ -547,11 +551,18 @@ tcSubTypeET orig ctxt (Check ty_actual) ty_expected where eq_orig = TypeEqOrigin { uo_actual = ty_expected , uo_expected = ty_actual - , uo_thing = Nothing } + , uo_thing = Nothing + , uo_visible = True } tcSubTypeET _ _ (Infer inf_res) ty_expected = ASSERT2( not (ir_inst inf_res), ppr inf_res $$ ppr ty_expected ) - do { co <- fillInferResult ty_expected inf_res + -- An (Infer inf_res) ExpSigmaType passed into tcSubTypeET never + -- has the ir_inst field set. Reason: in patterns (which is what + -- tcSubTypeET is used for) do not aggressively instantiate + do { co <- fill_infer_result ty_expected inf_res + -- Since ir_inst is false, we can skip fillInferResult + -- and go straight to fill_infer_result + ; return (mkWpCastN (mkTcSymCo co)) } ------------------------ @@ -566,7 +577,7 @@ tcSubTypeO orig ctxt ty_actual ty_expected , pprUserTypeCtxt ctxt , ppr ty_actual , ppr ty_expected ]) - ; tcSubTypeDS_NC_O orig ctxt noThing ty_actual ty_expected } + ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected } addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a addSubTypeCtxt ty_actual ty_expected thing_inside @@ -605,7 +616,8 @@ tcSubType_NC ctxt ty_actual ty_expected where origin = TypeEqOrigin { uo_actual = ty_actual , uo_expected = ty_expected - , uo_thing = Nothing } + , uo_thing = Nothing + , uo_visible = True } tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper -- Just like tcSubType, but with the additional precondition that @@ -613,22 +625,22 @@ tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWr tcSubTypeDS orig ctxt ty_actual ty_expected = addSubTypeCtxt ty_actual ty_expected $ do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) - ; tcSubTypeDS_NC_O orig ctxt noThing ty_actual ty_expected } + ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected } -tcSubTypeDS_NC_O :: Outputable a - => CtOrigin -- origin used for instantiation only +tcSubTypeDS_NC_O :: CtOrigin -- origin used for instantiation only -> UserTypeCtxt - -> Maybe a + -> Maybe (HsExpr GhcRn) -> TcSigmaType -> ExpRhoType -> TcM HsWrapper -- Just like tcSubType, but with the additional precondition that -- ty_expected is deeply skolemised tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected = case ty_expected of - Infer inf_res -> fillInferResult_Inst inst_orig ty_actual inf_res + Infer inf_res -> fillInferResult inst_orig ty_actual inf_res Check ty -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty where eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty - , uo_thing = mkErrorThing <$> m_thing } + , uo_thing = ppr <$> m_thing + , uo_visible = True } --------------- tc_sub_tc_type :: CtOrigin -- used when calling uType @@ -643,7 +655,7 @@ tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected vcat [ text "ty_actual =" <+> ppr ty_actual , text "ty_expected =" <+> ppr ty_expected ] ; mkWpCastN <$> - uType eq_orig TypeLevel ty_actual ty_expected } + uType TypeLevel eq_orig ty_actual ty_expected } | otherwise -- This is the general case = do { traceTc "tc_sub_tc_type (general case)" $ @@ -738,7 +750,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected -- go ty_a (TyVarTy alpha) -- which, in the impredicative case unified alpha := ty_a -- where th_a is a polytype. Not only is this probably bogus (we - -- simply do not have decent story for imprdicative types), but it + -- simply do not have decent story for impredicative types), but it -- caused Trac #12616 because (also bizarrely) 'deriving' code had -- -XImpredicativeTypes on. I deleted the entire case. @@ -746,8 +758,9 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected | not (isPredTy act_arg) , not (isPredTy exp_arg) = -- See Note [Co/contra-variance of subsumption checking] - do { res_wrap <- tc_sub_type_ds eq_orig inst_orig ctxt act_res exp_res - ; arg_wrap <- tc_sub_tc_type eq_orig given_orig ctxt exp_arg act_arg + do { res_wrap <- tc_sub_type_ds eq_orig inst_orig ctxt act_res exp_res + ; arg_wrap <- tc_sub_tc_type eq_orig given_orig GenSigCtxt exp_arg act_arg + -- GenSigCtxt: See Note [Setting the argument context] ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res doc) } -- arg_wrap :: exp_arg ~> act_arg -- res_wrap :: act-res ~> exp_res @@ -789,45 +802,58 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected -> eq_orig { uo_actual = rho_a } _ -> eq_orig - ; cow <- uType eq_orig' TypeLevel rho_a ty_expected + ; cow <- uType TypeLevel eq_orig' rho_a ty_expected ; return (mkWpCastN cow <.> wrap) } -- use versions without synonyms expanded - unify = mkWpCastN <$> uType eq_orig TypeLevel ty_actual ty_expected + unify = mkWpCastN <$> uType TypeLevel eq_orig ty_actual ty_expected + +{- Note [Settting the argument context] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider we are doing the ambiguity check for the (bogus) + f :: (forall a b. C b => a -> a) -> Int + +We'll call + tcSubType ((forall a b. C b => a->a) -> Int ) + ((forall a b. C b => a->a) -> Int ) + +with a UserTypeCtxt of (FunSigCtxt "f"). Then we'll do the co/contra thing +on the argument type of the (->) -- and at that point we want to switch +to a UserTypeCtxt of GenSigCtxt. Why? + +* Error messages. If we stick with FunSigCtxt we get errors like + * Could not deduce: C b + from the context: C b0 + bound by the type signature for: + f :: forall a b. C b => a->a + But of course f does not have that type signature! + Example tests: T10508, T7220a, Simple14 + +* Implications. We may decide to build an implication for the whole + ambiguity check, but we don't need one for each level within it, + and TcUnify.alwaysBuildImplication checks the UserTypeCtxt. + See Note [When to build an implication] +-} ----------------- -- needs both un-type-checked (for origins) and type-checked (for wrapping) -- expressions tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType -> TcM (HsExpr GhcTcId) -tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) +tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr -- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more -- convenient. -tcWrapResultO :: CtOrigin -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType +tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType -> TcM (HsExpr GhcTcId) -tcWrapResultO orig expr actual_ty res_ty +tcWrapResultO orig rn_expr expr actual_ty res_ty = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty , text "Expected:" <+> ppr res_ty ]) ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt - (Just expr) actual_ty res_ty + (Just rn_expr) actual_ty res_ty ; return (mkHsWrap cow expr) } ------------------------------------ -wrapFunResCoercion - :: [TcType] -- Type of args - -> HsWrapper -- HsExpr a -> HsExpr b - -> TcM HsWrapper -- HsExpr (arg_tys -> a) -> HsExpr (arg_tys -> b) -wrapFunResCoercion arg_tys co_fn_res - | isIdHsWrapper co_fn_res - = return idHsWrapper - | null arg_tys - = return co_fn_res - | otherwise - = do { arg_ids <- newSysLocalIds (fsLit "sub") arg_tys - ; return (mkWpLams arg_ids <.> co_fn_res <.> mkWpEvVarApps arg_ids) } - {- ********************************************************************** %* * @@ -851,24 +877,24 @@ tcInfer instantiate tc_check ; res_ty <- readExpType res_ty ; return (result, res_ty) } -fillInferResult_Inst :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper --- If wrap = fillInferResult_Inst t1 t2 +fillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrapper +-- If wrap = fillInferResult t1 t2 -- => wrap :: t1 ~> t2 -- See Note [Deep instantiation of InferResult] -fillInferResult_Inst orig ty inf_res@(IR { ir_inst = instantiate_me }) +fillInferResult orig ty inf_res@(IR { ir_inst = instantiate_me }) | instantiate_me = do { (wrap, rho) <- deeplyInstantiate orig ty - ; co <- fillInferResult rho inf_res + ; co <- fill_infer_result rho inf_res ; return (mkWpCastN co <.> wrap) } | otherwise - = do { co <- fillInferResult ty inf_res + = do { co <- fill_infer_result ty inf_res ; return (mkWpCastN co) } -fillInferResult :: TcType -> InferResult -> TcM TcCoercionN --- If wrap = fillInferResult t1 t2 +fill_infer_result :: TcType -> InferResult -> TcM TcCoercionN +-- If wrap = fill_infer_result t1 t2 -- => wrap :: t1 ~> t2 -fillInferResult orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl +fill_infer_result orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl , ir_ref = ref }) = do { (ty_co, ty_to_fill_with) <- promoteTcType res_lvl orig_ty @@ -885,7 +911,7 @@ fillInferResult orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl = do { let ty_lvl = tcTypeLevel ty ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl), ppr u $$ ppr res_lvl $$ ppr ty_lvl $$ - ppr ty <+> ppr (typeKind ty) $$ ppr orig_ty ) + ppr ty <+> dcolon <+> ppr (typeKind ty) $$ ppr orig_ty ) ; cts <- readTcRef ref ; case cts of Just already_there -> pprPanic "writeExpType" @@ -909,7 +935,7 @@ has the ir_inst flag. f :: forall {a}. a -> forall b. Num b => b -> b -> b This is surely confusing for users. - And worse, the the monomorphism restriction won't properly. The MR is + And worse, the monomorphism restriction won't work properly. The MR is dealt with in simplifyInfer, and simplifyInfer has no way of instantiating. This could perhaps be worked around, but it may be hard to know even when instantiation should happen. @@ -958,7 +984,8 @@ promoteTcType dest_lvl ty ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr) ; let eq_orig = TypeEqOrigin { uo_actual = ty , uo_expected = prom_ty - , uo_thing = Nothing } + , uo_thing = Nothing + , uo_visible = False } ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty ; return (co, prom_ty) } @@ -969,9 +996,10 @@ promoteTcType dest_lvl ty ; let ty_kind = typeKind ty kind_orig = TypeEqOrigin { uo_actual = ty_kind , uo_expected = res_kind - , uo_thing = Nothing } - ; ki_co <- uType kind_orig KindLevel (typeKind ty) res_kind - ; let co = mkTcNomReflCo ty `mkTcCoherenceRightCo` ki_co + , uo_thing = Nothing + , uo_visible = False } + ; ki_co <- uType KindLevel kind_orig (typeKind ty) res_kind + ; let co = mkTcGReflRightCo Nominal ty ki_co ; return (co, ty `mkCastTy` ki_co) } {- Note [Promoting a type] @@ -1024,7 +1052,7 @@ to (forall a. a->a) -> alpha[l+1] and emit the constraint [W] alpha[l+1] ~ Int -Now the poromoted type can fill the ref cell, while the emitted +Now the promoted type can fill the ref cell, while the emitted equality can float or not, according to the usual rules. But that's not quite right! We are exposing the arrow! We could @@ -1037,7 +1065,7 @@ Here we abstract over the '->' inside the forall, in case that is subject to an equality constraint from a GADT match. Note that we kept the outer (->) because that's part of -the polymorphic "shape". And becauuse of impredicativity, +the polymorphic "shape". And because of impredicativity, GADT matches can't give equalities that affect polymorphic shape. @@ -1115,35 +1143,81 @@ checkConstraints :: SkolemInfo -> TcM (TcEvBinds, result) checkConstraints skol_info skol_tvs given thing_inside - = do { (implics, ev_binds, result) - <- buildImplication skol_info skol_tvs given thing_inside - ; emitImplications implics - ; return (ev_binds, result) } - -buildImplication :: SkolemInfo - -> [TcTyVar] -- Skolems - -> [EvVar] -- Given - -> TcM result - -> TcM (Bag Implication, TcEvBinds, result) -buildImplication skol_info skol_tvs given thing_inside - = do { tc_lvl <- getTcLevel - ; deferred_type_errors <- goptM Opt_DeferTypeErrors <||> - goptM Opt_DeferTypedHoles - ; if null skol_tvs && null given && (not deferred_type_errors || - not (isTopTcLevel tc_lvl)) - then do { res <- thing_inside - ; return (emptyBag, emptyTcEvBinds, res) } - -- Fast path. We check every function argument with - -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints. - -- But with the solver producing unlifted equalities, we need - -- to have an EvBindsVar for them when they might be deferred to - -- runtime. Otherwise, they end up as top-level unlifted bindings, - -- which are verboten. See also Note [Deferred errors for coercion holes] - -- in TcErrors. + = do { implication_needed <- implicationNeeded skol_info skol_tvs given + + ; if implication_needed + then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside + ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted + ; traceTc "checkConstraints" (ppr tclvl $$ ppr skol_tvs) + ; emitImplications implics + ; return (ev_binds, result) } + + else -- Fast path. We check every function argument with + -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints. + -- So this fast path is well-exercised + do { res <- thing_inside + ; return (emptyTcEvBinds, res) } } + +checkTvConstraints :: SkolemInfo + -> Maybe SDoc -- User-written telescope, if present + -> TcM ([TcTyVar], result) + -> TcM ([TcTyVar], result) + +checkTvConstraints skol_info m_telescope thing_inside + = do { (tclvl, wanted, (skol_tvs, result)) + <- pushLevelAndCaptureConstraints thing_inside + + ; if isEmptyWC wanted + then return () + else do { ev_binds <- newNoTcEvBinds + ; implic <- newImplication + ; emitImplication $ + implic { ic_tclvl = tclvl + , ic_skols = skol_tvs + , ic_no_eqs = True + , ic_telescope = m_telescope + , ic_wanted = wanted + , ic_binds = ev_binds + , ic_info = skol_info } } + ; return (skol_tvs, result) } + + +implicationNeeded :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM Bool +-- See Note [When to build an implication] +implicationNeeded skol_info skol_tvs given + | null skol_tvs + , null given + , not (alwaysBuildImplication skol_info) + = -- Empty skolems and givens + do { tc_lvl <- getTcLevel + ; if not (isTopTcLevel tc_lvl) -- No implication needed if we are + then return False -- already inside an implication else - do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside - ; (implics, ev_binds) <- buildImplicationFor tclvl skol_info skol_tvs given wanted - ; return (implics, ev_binds, result) }} + do { dflags <- getDynFlags -- If any deferral can happen, + -- we must build an implication + ; return (gopt Opt_DeferTypeErrors dflags || + gopt Opt_DeferTypedHoles dflags || + gopt Opt_DeferOutOfScopeVariables dflags) } } + + | otherwise -- Non-empty skolems or givens + = return True -- Definitely need an implication + +alwaysBuildImplication :: SkolemInfo -> Bool +-- See Note [When to build an implication] +alwaysBuildImplication _ = False + +{- Commmented out for now while I figure out about error messages. + See Trac #14185 + +alwaysBuildImplication (SigSkol ctxt _ _) + = case ctxt of + FunSigCtxt {} -> True -- RHS of a binding with a signature + _ -> False +alwaysBuildImplication (RuleSkol {}) = True +alwaysBuildImplication (InstSkol {}) = True +alwaysBuildImplication (FamInstSkol {}) = True +alwaysBuildImplication _ = False +-} buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar] -> [EvVar] -> WantedConstraints @@ -1157,21 +1231,52 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted = return (emptyBag, emptyTcEvBinds) | otherwise - = ASSERT2( all isSkolemTyVar skol_tvs, ppr skol_tvs ) + = ASSERT2( all (isSkolemTyVar <||> isTyVarTyVar) skol_tvs, ppr skol_tvs ) + -- Why allow TyVarTvs? Because implicitly declared kind variables in + -- non-CUSK type declarations are TyVarTvs, and we need to bring them + -- into scope as a skolem in an implication. This is OK, though, + -- because TyVarTvs will always remain tyvars, even after unification. do { ev_binds_var <- newTcEvBinds - ; env <- getLclEnv - ; let implic = Implic { ic_tclvl = tclvl - , ic_skols = skol_tvs - , ic_no_eqs = False - , ic_given = given - , ic_wanted = wanted - , ic_status = IC_Unsolved - , ic_binds = ev_binds_var - , ic_env = env - , ic_needed = emptyVarSet - , ic_info = skol_info } - - ; return (unitBag implic, TcEvBinds ev_binds_var) } + ; implic <- newImplication + ; let implic' = implic { ic_tclvl = tclvl + , ic_skols = skol_tvs + , ic_given = given + , ic_wanted = wanted + , ic_binds = ev_binds_var + , ic_info = skol_info } + + ; return (unitBag implic', TcEvBinds ev_binds_var) } + +{- Note [When to build an implication] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have some 'skolems' and some 'givens', and we are +considering whether to wrap the constraints in their scope into an +implication. We must /always/ so if either 'skolems' or 'givens' are +non-empty. But what if both are empty? You might think we could +always drop the implication. Other things being equal, the fewer +implications the better. Less clutter and overhead. But we must +take care: + +* If we have an unsolved [W] g :: a ~# b, and -fdefer-type-errors, + we'll make a /term-level/ evidence binding for 'g = error "blah"'. + We must have an EvBindsVar those bindings!, otherwise they end up as + top-level unlifted bindings, which are verboten. This only matters + at top level, so we check for that + See also Note [Deferred errors for coercion holes] in TcErrors. + cf Trac #14149 for an example of what goes wrong. + +* If you have + f :: Int; f = f_blah + g :: Bool; g = g_blah + If we don't build an implication for f or g (no tyvars, no givens), + the constraints for f_blah and g_blah are solved together. And that + can yield /very/ confusing error messages, because we can get + [W] C Int b1 -- from f_blah + [W] C Int b2 -- from g_blan + and fundpes can yield [D] b1 ~ b2, even though the two functions have + literally nothing to do with each other. Trac #14185 is an example. + Building an implication keeps them separage. +-} {- ************************************************************************ @@ -1184,41 +1289,25 @@ The exported functions are all defined as versions of some non-exported generic functions. -} -unifyType :: Outputable a => Maybe a -- ^ If present, has type 'ty1' +unifyType :: Maybe (HsExpr GhcRn) -- ^ If present, has type 'ty1' -> TcTauType -> TcTauType -> TcM TcCoercionN -- Actual and expected types -- Returns a coercion : ty1 ~ ty2 unifyType thing ty1 ty2 = traceTc "utype" (ppr ty1 $$ ppr ty2 $$ ppr thing) >> - uType origin TypeLevel ty1 ty2 + uType TypeLevel origin ty1 ty2 where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 - , uo_thing = mkErrorThing <$> thing } - --- | Use this instead of 'Nothing' when calling 'unifyType' without --- a good "thing" (where the "thing" has the "actual" type passed in) --- This has an 'Outputable' instance, avoiding amgiguity problems. -noThing :: Maybe (HsExpr GhcRn) -noThing = Nothing + , uo_thing = ppr <$> thing + , uo_visible = True } -- always called from a visible context -unifyKind :: Outputable a => Maybe a -> TcKind -> TcKind -> TcM CoercionN +unifyKind :: Maybe (HsType GhcRn) -> TcKind -> TcKind -> TcM CoercionN unifyKind thing ty1 ty2 = traceTc "ukind" (ppr ty1 $$ ppr ty2 $$ ppr thing) >> - uType origin KindLevel ty1 ty2 + uType KindLevel origin ty1 ty2 where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 - , uo_thing = mkErrorThing <$> thing } + , uo_thing = ppr <$> thing + , uo_visible = True } -- also always from a visible context --------------- -unifyPred :: PredType -> PredType -> TcM TcCoercionN --- Actual and expected types -unifyPred = unifyType noThing - ---------------- -unifyTheta :: TcThetaType -> TcThetaType -> TcM [TcCoercionN] --- Actual and expected types -unifyTheta theta1 theta2 - = do { checkTc (equalLength theta1 theta2) - (vcat [text "Contexts differ in length", - nest 2 $ parens $ text "Use RelaxedPolyRec to allow this"]) - ; zipWithM unifyPred theta1 theta2 } {- %************************************************************************ @@ -1231,16 +1320,16 @@ uType is the heart of the unifier. -} uType, uType_defer - :: CtOrigin - -> TypeOrKind + :: TypeOrKind + -> CtOrigin -> TcType -- ty1 is the *actual* type -> TcType -- ty2 is the *expected* type - -> TcM Coercion + -> TcM CoercionN -------------- -- It is always safe to defer unification to the main constraint solver -- See Note [Deferred unification] -uType_defer origin t_or_k ty1 ty2 +uType_defer t_or_k origin ty1 ty2 = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2 -- Error trace only @@ -1249,13 +1338,16 @@ uType_defer origin t_or_k ty1 ty2 ; whenDOptM Opt_D_dump_tc_trace $ do { ctxt <- getErrCtxt ; doc <- mkErrInfo emptyTidyEnv ctxt - ; traceTc "utype_defer" (vcat [ppr co, ppr ty1, - ppr ty2, pprCtOrigin origin, doc]) + ; traceTc "utype_defer" (vcat [ debugPprType ty1 + , debugPprType ty2 + , pprCtOrigin origin + , doc]) + ; traceTc "utype_defer2" (ppr co) } ; return co } -------------- -uType origin t_or_k orig_ty1 orig_ty2 +uType t_or_k origin orig_ty1 orig_ty2 = do { tclvl <- getTcLevel ; traceTc "u_tys" $ vcat [ text "tclvl" <+> ppr tclvl @@ -1267,10 +1359,21 @@ uType origin t_or_k orig_ty1 orig_ty2 else traceTc "u_tys yields coercion:" (ppr co) ; return co } where - go :: TcType -> TcType -> TcM Coercion + go :: TcType -> TcType -> TcM CoercionN -- The arguments to 'go' are always semantically identical -- to orig_ty{1,2} except for looking through type synonyms + -- Unwrap casts before looking for variables. This way, we can easily + -- recognize (t |> co) ~ (t |> co), which is nice. Previously, we + -- didn't do it this way, and then the unification above was deferred. + go (CastTy t1 co1) t2 + = do { co_tys <- uType t_or_k origin t1 t2 + ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) } + + go t1 (CastTy t2 co2) + = do { co_tys <- uType t_or_k origin t1 t2 + ; return (mkCoherenceRightCo Nominal t2 co2 co_tys) } + -- Variables; go for uVar -- Note that we pass in *original* (before synonym expansion), -- so that type variables tend to get filled in with @@ -1291,7 +1394,7 @@ uType origin t_or_k orig_ty1 orig_ty2 -- See Note [Expanding synonyms during unification] go ty1@(TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 - = return $ mkReflCo Nominal ty1 + = return $ mkNomReflCo ty1 -- See Note [Expanding synonyms during unification] -- @@ -1305,18 +1408,10 @@ uType origin t_or_k orig_ty1 orig_ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 | Just ty2' <- tcView ty2 = go ty1 ty2' - go (CastTy t1 co1) t2 - = do { co_tys <- go t1 t2 - ; return (mkCoherenceLeftCo co_tys co1) } - - go t1 (CastTy t2 co2) - = do { co_tys <- go t1 t2 - ; return (mkCoherenceRightCo co_tys co2) } - -- Functions (or predicate functions) just check the two parts go (FunTy fun1 arg1) (FunTy fun2 arg2) - = do { co_l <- uType origin t_or_k fun1 fun2 - ; co_r <- uType origin t_or_k arg1 arg2 + = do { co_l <- uType t_or_k origin fun1 fun2 + ; co_r <- uType t_or_k origin arg1 arg2 ; return $ mkFunCo Nominal co_l co_r } -- Always defer if a type synonym family (type function) @@ -1330,8 +1425,11 @@ uType origin t_or_k orig_ty1 orig_ty2 -- See Note [Mismatched type lists and application decomposition] | tc1 == tc2, equalLength tys1 tys2 = ASSERT2( isGenerativeTyCon tc1 Nominal, ppr tc1 ) - do { cos <- zipWithM (uType origin t_or_k) tys1 tys2 + do { cos <- zipWith3M (uType t_or_k) origins' tys1 tys2 ; return $ mkTyConAppCo Nominal tc1 cos } + where + origins' = map (\is_vis -> if is_vis then origin else toInvisibleOrigin origin) + (tcTyConVisibilities tc1) go (LitTy m) ty@(LitTy n) | m == n @@ -1341,24 +1439,24 @@ uType origin t_or_k orig_ty1 orig_ty2 -- Do not decompose FunTy against App; -- it's often a type error, so leave it for the constraint solver go (AppTy s1 t1) (AppTy s2 t2) - = go_app s1 t1 s2 t2 + = go_app (isNextArgVisible s1) s1 t1 s2 t2 go (AppTy s1 t1) (TyConApp tc2 ts2) | Just (ts2', t2') <- snocView ts2 = ASSERT( mightBeUnsaturatedTyCon tc2 ) - go_app s1 t1 (TyConApp tc2 ts2') t2' + go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2' go (TyConApp tc1 ts1) (AppTy s2 t2) | Just (ts1', t1') <- snocView ts1 = ASSERT( mightBeUnsaturatedTyCon tc1 ) - go_app (TyConApp tc1 ts1') t1' s2 t2 + go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2 go (CoercionTy co1) (CoercionTy co2) = do { let ty1 = coercionType co1 ty2 = coercionType co2 - ; kco <- uType (KindEqOrigin orig_ty1 (Just orig_ty2) origin + ; kco <- uType KindLevel + (KindEqOrigin orig_ty1 (Just orig_ty2) origin (Just t_or_k)) - KindLevel ty1 ty2 ; return $ mkProofIrrelCo Nominal kco co1 co2 } @@ -1369,12 +1467,15 @@ uType origin t_or_k orig_ty1 orig_ty2 ------------------ defer ty1 ty2 -- See Note [Check for equality before deferring] | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1) - | otherwise = uType_defer origin t_or_k ty1 ty2 + | otherwise = uType_defer t_or_k origin ty1 ty2 ------------------ - go_app s1 t1 s2 t2 - = do { co_s <- uType origin t_or_k s1 s2 - ; co_t <- uType origin t_or_k t1 t2 + go_app vis s1 t1 s2 t2 + = do { co_s <- uType t_or_k origin s1 s2 + ; let arg_origin + | vis = origin + | otherwise = toInvisibleOrigin origin + ; co_t <- uType t_or_k arg_origin t1 t2 ; return $ mkAppCo co_s co_t } {- Note [Check for equality before deferring] @@ -1421,6 +1522,9 @@ We expand synonyms during unification, but: more likely that the inferred types will mention type synonyms understandable to the user + * Similarly, we expand *after* the CastTy case, just in case the + CastTy wraps a variable. + * We expand *before* the TyConApp case. For example, if we have type Phantom a = Int and are unifying @@ -1528,84 +1632,141 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 go dflags cur_lvl | canSolveByUnification cur_lvl tv1 ty2 , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2 - = do { co_k <- uType kind_origin KindLevel (typeKind ty2') (tyVarKind tv1) - ; co <- updateMeta tv1 ty2' co_k - ; return (maybe_sym swapped co) } + = do { co_k <- uType KindLevel kind_origin (typeKind ty2') (tyVarKind tv1) + ; traceTc "uUnfilledVar2 ok" $ + vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) + , ppr ty2 <+> dcolon <+> ppr (typeKind ty2) + , ppr (isTcReflCo co_k), ppr co_k ] + + ; if isTcReflCo co_k -- only proceed if the kinds matched. + + then do { writeMetaTyVar tv1 ty2' + ; return (mkTcNomReflCo ty2') } + + else defer } -- This cannot be solved now. See TcCanonical + -- Note [Equalities with incompatible kinds] | otherwise - = unSwap swapped (uType_defer origin t_or_k) ty1 ty2 + = do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2) -- Occurs check or an untouchable: just defer -- NB: occurs check isn't necessarily fatal: -- eg tv1 occured in type family parameter + ; defer } ty1 = mkTyVarTy tv1 kind_origin = KindEqOrigin ty1 (Just ty2) origin (Just t_or_k) --- | apply sym iff swapped -maybe_sym :: SwapFlag -> Coercion -> Coercion -maybe_sym IsSwapped = mkSymCo -maybe_sym NotSwapped = id + defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2 swapOverTyVars :: TcTyVar -> TcTyVar -> Bool swapOverTyVars tv1 tv2 - | isFmvTyVar tv1 = False -- See Note [Fmv Orientation Invariant] - | isFmvTyVar tv2 = True - - | Just lvl1 <- metaTyVarTcLevel_maybe tv1 - -- If tv1 is touchable, swap only if tv2 is also - -- touchable and it's strictly better to update the latter - -- But see Note [Avoid unnecessary swaps] - = case metaTyVarTcLevel_maybe tv2 of - Nothing -> False - Just lvl2 | lvl2 `strictlyDeeperThan` lvl1 -> True - | lvl1 `strictlyDeeperThan` lvl2 -> False - | otherwise -> nicer_to_update tv2 - - -- So tv1 is not a meta tyvar - -- If only one is a meta tyvar, put it on the left - -- This is not because it'll be solved; but because - -- the floating step looks for meta tyvars on the left - | isMetaTyVar tv2 = True - - -- So neither is a meta tyvar (including FlatMetaTv) - - -- If only one is a flatten skolem, put it on the left - -- See Note [Eliminate flat-skols] - | not (isFlattenTyVar tv1), isFlattenTyVar tv2 = True + -- Level comparison: see Note [TyVar/TyVar orientation] + | lvl1 `strictlyDeeperThan` lvl2 = False + | lvl2 `strictlyDeeperThan` lvl1 = True - | otherwise = False + -- Priority: see Note [TyVar/TyVar orientation] + | pri1 > pri2 = False + | pri2 > pri1 = True - where - nicer_to_update tv2 - = (isSigTyVar tv1 && not (isSigTyVar tv2)) - || (isSystemName (Var.varName tv2) && not (isSystemName (Var.varName tv1))) + -- Names: see Note [TyVar/TyVar orientation] + | isSystemName tv2_name, not (isSystemName tv1_name) = True --- @trySpontaneousSolve wi@ solves equalities where one side is a --- touchable unification variable. --- Returns True <=> spontaneous solve happened -canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool -canSolveByUnification tclvl tv xi - | isTouchableMetaTyVar tclvl tv - = case metaTyVarInfo tv of - SigTv -> is_tyvar xi - _ -> True + | otherwise = False - | otherwise -- Untouchable - = False where - is_tyvar xi - = case tcGetTyVar_maybe xi of - Nothing -> False - Just tv -> case tcTyVarDetails tv of - MetaTv { mtv_info = info } - -> case info of - SigTv -> True - _ -> False - SkolemTv {} -> True - RuntimeUnk -> True - -{- Note [Fmv Orientation Invariant] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + lvl1 = tcTyVarLevel tv1 + lvl2 = tcTyVarLevel tv2 + pri1 = lhsPriority tv1 + pri2 = lhsPriority tv2 + tv1_name = Var.varName tv1 + tv2_name = Var.varName tv2 + + +lhsPriority :: TcTyVar -> Int +-- Higher => more important to be on the LHS +-- See Note [TyVar/TyVar orientation] +lhsPriority tv + = ASSERT2( isTyVar tv, ppr tv) + case tcTyVarDetails tv of + RuntimeUnk -> 0 + SkolemTv {} -> 0 + MetaTv { mtv_info = info } -> case info of + FlatSkolTv -> 1 + TyVarTv -> 2 + TauTv -> 3 + FlatMetaTv -> 4 +{- Note [TyVar/TyVar orientation] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Given (a ~ b), should we orient the CTyEqCan as (a~b) or (b~a)? +This is a surprisingly tricky question! + +First note: only swap if you have to! + See Note [Avoid unnecessary swaps] + +So we look for a positive reason to swap, using a three-step test: + +* Level comparison. If 'a' has deeper level than 'b', + put 'a' on the left. See Note [Deeper level on the left] + +* Priority. If the levels are the same, look at what kind of + type variable it is, using 'lhsPriority' + + - FlatMetaTv: Always put on the left. + See Note [Fmv Orientation Invariant] + NB: FlatMetaTvs always have the current level, never an + outer one. So nothing can be deeper than a FlatMetaTv + + + - TyVarTv/TauTv: if we have tyv_tv ~ tau_tv, put tau_tv + on the left because there are fewer + restrictions on updating TauTvs + + - TyVarTv/TauTv: put on the left either + a) Because it's touchable and can be unified, or + b) Even if it's not touchable, TcSimplify.floatEqualities + looks for meta tyvars on the left + + - FlatSkolTv: Put on the left in preference to a SkolemTv + See Note [Eliminate flat-skols] + +* Names. If the level and priority comparisons are all + equal, try to eliminate a TyVars with a System Name in + favour of ones with a Name derived from a user type signature + +* Age. At one point in the past we tried to break any remaining + ties by eliminating the younger type variable, based on their + Uniques. See Note [Eliminate younger unification variables] + (which also explains why we don't do this any more) + +Note [Deeper level on the left] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The most important thing is that we want to put tyvars with +the deepest level on the left. The reason to do so differs for +Wanteds and Givens, but either way, deepest wins! Simple. + +* Wanteds. Putting the deepest variable on the left maximise the + chances that it's a touchable meta-tyvar which can be solved. + +* Givens. Suppose we have something like + forall a[2]. b[1] ~ a[2] => beta[1] ~ a[2] + + If we orient the Given a[2] on the left, we'll rewrite the Wanted to + (beta[1] ~ b[1]), and that can float out of the implication. + Otherwise it can't. By putting the deepest variable on the left + we maximise our changes of eliminating skolem capture. + + See also TcSMonad Note [Let-bound skolems] for another reason + to orient with the deepest skolem on the left. + + IMPORTANT NOTE: this test does a level-number comparison on + skolems, so it's important that skolems have (accurate) level + numbers. + +See Trac #15009 for an further analysis of why "deepest on the left" +is a good plan. + +Note [Fmv Orientation Invariant] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ * We always orient a constraint fmv ~ alpha with fmv on the left, even if alpha is @@ -1638,14 +1799,88 @@ T10226, T10009.) [WD] F fmv ~ fmv, [WD] fmv ~ a And now we are stuck. -So instead the Fmv Orientation Invariant puts te fmv on the +So instead the Fmv Orientation Invariant puts the fmv on the left, giving [WD] fmv ~ alpha, [WD] F alpha ~ fmv, [WD] alpha ~ a Now we get alpha:=a, and everything works out -Note [Prevent unification with type families] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Eliminate flat-skols] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Suppose we have [G] Num (F [a]) +then we flatten to + [G] Num fsk + [G] F [a] ~ fsk +where fsk is a flatten-skolem (FlatSkolTv). Suppose we have + type instance F [a] = a +then we'll reduce the second constraint to + [G] a ~ fsk +and then replace all uses of 'a' with fsk. That's bad because +in error messages instead of saying 'a' we'll say (F [a]). In all +places, including those where the programmer wrote 'a' in the first +place. Very confusing! See Trac #7862. + +Solution: re-orient a~fsk to fsk~a, so that we preferentially eliminate +the fsk. + +Note [Avoid unnecessary swaps] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If we swap without actually improving matters, we can get an infinite loop. +Consider + work item: a ~ b + inert item: b ~ c +We canonicalise the work-item to (a ~ c). If we then swap it before +adding to the inert set, we'll add (c ~ a), and therefore kick out the +inert guy, so we get + new work item: b ~ c + inert item: c ~ a +And now the cycle just repeats + +Note [Eliminate younger unification variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Given a choice of unifying + alpha := beta or beta := alpha +we try, if possible, to eliminate the "younger" one, as determined +by `ltUnique`. Reason: the younger one is less likely to appear free in +an existing inert constraint, and hence we are less likely to be forced +into kicking out and rewriting inert constraints. + +This is a performance optimisation only. It turns out to fix +Trac #14723 all by itself, but clearly not reliably so! + +It's simple to implement (see nicer_to_update_tv2 in swapOverTyVars). +But, to my surprise, it didn't seem to make any significant difference +to the compiler's performance, so I didn't take it any further. Still +it seemed to too nice to discard altogether, so I'm leaving these +notes. SLPJ Jan 18. +-} + +-- @trySpontaneousSolve wi@ solves equalities where one side is a +-- touchable unification variable. +-- Returns True <=> spontaneous solve happened +canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool +canSolveByUnification tclvl tv xi + | isTouchableMetaTyVar tclvl tv + = case metaTyVarInfo tv of + TyVarTv -> is_tyvar xi + _ -> True + + | otherwise -- Untouchable + = False + where + is_tyvar xi + = case tcGetTyVar_maybe xi of + Nothing -> False + Just tv -> case tcTyVarDetails tv of + MetaTv { mtv_info = info } + -> case info of + TyVarTv -> True + _ -> False + SkolemTv {} -> True + RuntimeUnk -> True + +{- Note [Prevent unification with type families] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We prevent unification with type families because of an uneasy compromise. It's perfectly sound to unify with type families, and it even improves the error messages in the testsuite. It also modestly improves performance, at @@ -1768,38 +2003,26 @@ lookupTcTyVar tyvar where details = tcTyVarDetails tyvar --- | Fill in a meta-tyvar -updateMeta :: TcTyVar -- ^ tv to fill in, tv :: k1 - -> TcType -- ^ ty2 :: k2 - -> Coercion -- ^ kind_co :: k2 ~N k1 - -> TcM Coercion -- ^ :: tv ~N ty2 (= ty2 |> kind_co ~N ty2) -updateMeta tv1 ty2 kind_co - = do { let ty2' = ty2 `mkCastTy` kind_co - ty2_refl = mkNomReflCo ty2 - co = mkCoherenceLeftCo ty2_refl kind_co - ; writeMetaTyVar tv1 ty2' - ; return co } - {- Note [Unifying untouchables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We treat an untouchable type variable as if it was a skolem. That -ensures it won't unify with anything. It's a slight had, because +ensures it won't unify with anything. It's a slight hack, because we return a made-up TcTyVarDetails, but I think it works smoothly. -} -- | Breaks apart a function kind into its pieces. -matchExpectedFunKind :: Arity -- ^ # of args remaining, only for errors - -> TcType -- ^ type, only for errors +matchExpectedFunKind :: Outputable fun + => fun -- ^ type, only for errors -> TcKind -- ^ function kind -> TcM (Coercion, TcKind, TcKind) -- ^ co :: old_kind ~ arg -> res -matchExpectedFunKind num_args_remaining ty = go +matchExpectedFunKind hs_ty = go where go k | Just k' <- tcView k = go k' go k@(TyVarTy kvar) - | isTcTyVar kvar, isMetaTyVar kvar + | isMetaTyVar kvar = do { maybe_kind <- readMetaTyVar kvar ; case maybe_kind of Indirect fun_kind -> go fun_kind @@ -1812,12 +2035,12 @@ matchExpectedFunKind num_args_remaining ty = go = do { arg_kind <- newMetaKindVar ; res_kind <- newMetaKindVar ; let new_fun = mkFunTy arg_kind res_kind - thing = mkTypeErrorThingArgs ty num_args_remaining origin = TypeEqOrigin { uo_actual = k , uo_expected = new_fun - , uo_thing = Just thing + , uo_thing = Just (ppr hs_ty) + , uo_visible = True } - ; co <- uType origin KindLevel k new_fun + ; co <- uType KindLevel origin k new_fun ; return (co, arg_kind, res_kind) } @@ -1828,38 +2051,12 @@ matchExpectedFunKind num_args_remaining ty = go ********************************************************************* -} -{- Note [Occurs check expansion] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -(occurCheckExpand tv xi) expands synonyms in xi just enough to get rid -of occurrences of tv outside type function arguments, if that is -possible; otherwise, it returns Nothing. - -For example, suppose we have - type F a b = [a] -Then - occCheckExpand b (F Int b) = Just [Int] -but - occCheckExpand a (F a Int) = Nothing - -We don't promise to do the absolute minimum amount of expanding -necessary, but we try not to do expansions we don't need to. We -prefer doing inner expansions first. For example, - type F a b = (a, Int, a, [a]) - type G b = Char -We have - occCheckExpand b (F (G b)) = Just (F Char) -even though we could also expand F to get rid of b. - -The two variants of the function are to support TcUnify.checkTauTvUpdate, -which wants to prevent unification with type families. For more on this -point, see Note [Prevent unification with type families] in TcUnify. - -Note [Occurrence checking: look inside kinds] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Occurrence checking: look inside kinds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we are considering unifying (alpha :: *) ~ Int -> (beta :: alpha -> alpha) This may be an error (what is that alpha doing inside beta's kind?), -but we must not make the mistake of actuallyy unifying or we'll +but we must not make the mistake of actually unifying or we'll build an infinite data structure. So when looking for occurrences of alpha in the rhs, we must look in the kinds of type variables that occur there. @@ -1926,7 +2123,7 @@ occCheckForErrors dflags tv ty = case preCheck dflags True tv ty of OC_OK _ -> OC_OK () OC_Bad -> OC_Bad - OC_Occurs -> case occCheckExpand tv ty of + OC_Occurs -> case occCheckExpand [tv] ty of Nothing -> OC_Occurs Just _ -> OC_OK () @@ -1964,7 +2161,7 @@ metaTyVarUpdateOK dflags tv ty -- See Note [Prevent unification with type families] OC_OK _ -> Just ty OC_Bad -> Nothing -- forall or type function - OC_Occurs -> occCheckExpand tv ty + OC_Occurs -> occCheckExpand [tv] ty preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> OccCheckResult () -- A quick check for @@ -1999,7 +2196,7 @@ preCheck dflags ty_fam_ok tv ty fast_check (AppTy fun arg) = fast_check fun >> fast_check arg fast_check (CastTy ty co) = fast_check ty >> fast_check_co co fast_check (CoercionTy co) = fast_check_co co - fast_check (ForAllTy (TvBndr tv' _) ty) + fast_check (ForAllTy (Bndr tv' _) ty) | not impredicative_ok = OC_Bad | tv == tv' = ok | otherwise = do { fast_check_occ (tyVarKind tv') @@ -2025,120 +2222,10 @@ preCheck dflags ty_fam_ok tv ty | not (ty_fam_ok || isFamFreeTyCon tc) = True | otherwise = False -occCheckExpand :: TcTyVar -> TcType -> Maybe TcType --- See Note [Occurs check expansion] --- We may have needed to do some type synonym unfolding in order to --- get rid of the variable (or forall), so we also return the unfolded --- version of the type, which is guaranteed to be syntactically free --- of the given type variable. If the type is already syntactically --- free of the variable, then the same type is returned. -occCheckExpand tv ty - = go emptyVarEnv ty - where - go :: VarEnv TyVar -> Type -> Maybe Type - -- The VarEnv carries mappings necessary - -- because of kind expansion - go env (TyVarTy tv') - | tv == tv' = Nothing - | Just tv'' <- lookupVarEnv env tv' = return (mkTyVarTy tv'') - | otherwise = do { k' <- go env (tyVarKind tv') - ; return (mkTyVarTy $ - setTyVarKind tv' k') } - -- See Note [Occurrence checking: look inside kinds] - - go _ ty@(LitTy {}) = return ty - go env (AppTy ty1 ty2) = do { ty1' <- go env ty1 - ; ty2' <- go env ty2 - ; return (mkAppTy ty1' ty2') } - go env (FunTy ty1 ty2) = do { ty1' <- go env ty1 - ; ty2' <- go env ty2 - ; return (mkFunTy ty1' ty2') } - go env ty@(ForAllTy (TvBndr tv' vis) body_ty) - | tv == tv' = return ty - | otherwise = do { ki' <- go env (tyVarKind tv') - ; let tv'' = setTyVarKind tv' ki' - env' = extendVarEnv env tv' tv'' - ; body' <- go env' body_ty - ; return (ForAllTy (TvBndr tv'' vis) body') } - - -- For a type constructor application, first try expanding away the - -- offending variable from the arguments. If that doesn't work, next - -- see if the type constructor is a type synonym, and if so, expand - -- it and try again. - go env ty@(TyConApp tc tys) - = case mapM (go env) tys of - Just tys' -> return (mkTyConApp tc tys') - Nothing | Just ty' <- tcView ty -> go env ty' - | otherwise -> Nothing - -- Failing that, try to expand a synonym - - go env (CastTy ty co) = do { ty' <- go env ty - ; co' <- go_co env co - ; return (mkCastTy ty' co') } - go env (CoercionTy co) = do { co' <- go_co env co - ; return (mkCoercionTy co') } - - ------------------ - go_co env (Refl r ty) = do { ty' <- go env ty - ; return (mkReflCo r ty') } - -- Note: Coercions do not contain type synonyms - go_co env (TyConAppCo r tc args) = do { args' <- mapM (go_co env) args - ; return (mkTyConAppCo r tc args') } - go_co env (AppCo co arg) = do { co' <- go_co env co - ; arg' <- go_co env arg - ; return (mkAppCo co' arg') } - go_co env co@(ForAllCo tv' kind_co body_co) - | tv == tv' = return co - | otherwise = do { kind_co' <- go_co env kind_co - ; let tv'' = setTyVarKind tv' $ - pFst (coercionKind kind_co') - env' = extendVarEnv env tv' tv'' - ; body' <- go_co env' body_co - ; return (ForAllCo tv'' kind_co' body') } - go_co env (FunCo r co1 co2) = do { co1' <- go_co env co1 - ; co2' <- go_co env co2 - ; return (mkFunCo r co1' co2') } - go_co env (CoVarCo c) = do { k' <- go env (varType c) - ; return (mkCoVarCo (setVarType c k')) } - go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args - ; return (mkAxiomInstCo ax ind args') } - go_co env (UnivCo p r ty1 ty2) = do { p' <- go_prov env p - ; ty1' <- go env ty1 - ; ty2' <- go env ty2 - ; return (mkUnivCo p' r ty1' ty2') } - go_co env (SymCo co) = do { co' <- go_co env co - ; return (mkSymCo co') } - go_co env (TransCo co1 co2) = do { co1' <- go_co env co1 - ; co2' <- go_co env co2 - ; return (mkTransCo co1' co2') } - go_co env (NthCo n co) = do { co' <- go_co env co - ; return (mkNthCo n co') } - go_co env (LRCo lr co) = do { co' <- go_co env co - ; return (mkLRCo lr co') } - go_co env (InstCo co arg) = do { co' <- go_co env co - ; arg' <- go_co env arg - ; return (mkInstCo co' arg') } - go_co env (CoherenceCo co1 co2) = do { co1' <- go_co env co1 - ; co2' <- go_co env co2 - ; return (mkCoherenceCo co1' co2') } - go_co env (KindCo co) = do { co' <- go_co env co - ; return (mkKindCo co') } - go_co env (SubCo co) = do { co' <- go_co env co - ; return (mkSubCo co') } - go_co env (AxiomRuleCo ax cs) = do { cs' <- mapM (go_co env) cs - ; return (mkAxiomRuleCo ax cs') } - - ------------------ - go_prov _ UnsafeCoerceProv = return UnsafeCoerceProv - go_prov env (PhantomProv co) = PhantomProv <$> go_co env co - go_prov env (ProofIrrelProv co) = ProofIrrelProv <$> go_co env co - go_prov _ p@(PluginProv _) = return p - go_prov _ p@(HoleProv _) = return p - canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool canUnifyWithPolyType dflags details = case details of - MetaTv { mtv_info = SigTv } -> False - MetaTv { mtv_info = TauTv } -> xopt LangExt.ImpredicativeTypes dflags - _other -> True + MetaTv { mtv_info = TyVarTv } -> False + MetaTv { mtv_info = TauTv } -> xopt LangExt.ImpredicativeTypes dflags + _other -> True -- We can have non-meta tyvars in given constraints |