diff options
Diffstat (limited to 'compiler/GHC/Tc/Utils')
| -rw-r--r-- | compiler/GHC/Tc/Utils/Instantiate.hs | 89 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcMType.hs | 9 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 19 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs | 444 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs-boot | 10 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Zonk.hs | 11 |
6 files changed, 298 insertions, 284 deletions
diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs index d93e8fc84f..0e928ed5fd 100644 --- a/compiler/GHC/Tc/Utils/Instantiate.hs +++ b/compiler/GHC/Tc/Utils/Instantiate.hs @@ -12,7 +12,7 @@ module GHC.Tc.Utils.Instantiate ( topSkolemise, - topInstantiate, topInstantiateInferred, + topInstantiate, instantiateSigma, instCall, instDFunType, instStupidTheta, instTyVarsWith, newWanted, newWanteds, @@ -72,6 +72,7 @@ import GHC.Types.Name import GHC.Types.Var import GHC.Core.DataCon import GHC.Types.Var.Env +import GHC.Types.Var.Set import GHC.Builtin.Names import GHC.Types.SrcLoc as SrcLoc import GHC.Driver.Session @@ -189,66 +190,44 @@ topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) -- and e :: ty -- then wrap e :: rho (that is, wrap :: ty "->" rho) -- NB: always returns a rho-type, with no top-level forall or (=>) -topInstantiate = top_instantiate True +topInstantiate orig ty + | (tvs, theta, body) <- tcSplitSigmaTy ty + , not (null tvs && null theta) + = do { (_, wrap1, body1) <- instantiateSigma orig tvs theta body --- | Instantiate all outer 'Inferred' binders --- and any context. Never looks through arrows or specified type variables. --- Used for visible type application. -topInstantiateInferred :: CtOrigin -> TcSigmaType - -> TcM (HsWrapper, TcSigmaType) --- if topInstantiate ty = (wrap, rho) --- and e :: ty --- then wrap e :: rho --- NB: may return a sigma-type -topInstantiateInferred = top_instantiate False - -top_instantiate :: Bool -- True <=> instantiate *all* variables - -- False <=> instantiate only the inferred ones - -> CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) -top_instantiate inst_all orig ty - | (binders, phi) <- tcSplitForAllVarBndrs ty - , (theta, rho) <- tcSplitPhiTy phi - , not (null binders && null theta) - = do { let (inst_bndrs, leave_bndrs) = span should_inst binders - (inst_theta, leave_theta) - | null leave_bndrs = (theta, []) - | otherwise = ([], theta) - in_scope = mkInScopeSet (tyCoVarsOfType ty) - empty_subst = mkEmptyTCvSubst in_scope - inst_tvs = binderVars inst_bndrs - ; (subst, inst_tvs') <- mapAccumLM newMetaTyVarX empty_subst inst_tvs - ; let inst_theta' = substTheta subst inst_theta - sigma' = substTy subst (mkForAllTys leave_bndrs $ - mkPhiTy leave_theta rho) - inst_tv_tys' = mkTyVarTys inst_tvs' - - ; wrap1 <- instCall orig inst_tv_tys' inst_theta' - ; traceTc "Instantiating" - (vcat [ text "all tyvars?" <+> ppr inst_all - , text "origin" <+> pprCtOrigin orig - , text "type" <+> debugPprType ty - , text "theta" <+> ppr theta - , text "leave_bndrs" <+> ppr leave_bndrs - , text "with" <+> vcat (map debugPprType inst_tv_tys') - , text "theta:" <+> ppr inst_theta' ]) - - ; (wrap2, rho2) <- - if null leave_bndrs -- NB: if inst_all is True then leave_bndrs = [] + -- Loop, to account for types like + -- forall a. Num a => forall b. Ord b => ... + ; (wrap2, rho) <- topInstantiate orig body1 - -- account for types like forall a. Num a => forall b. Ord b => ... - then top_instantiate inst_all orig sigma' + ; return (wrap2 <.> wrap1, rho) } - -- but don't loop if there were any un-inst'able tyvars - else return (idHsWrapper, sigma') + | otherwise = return (idHsWrapper, ty) - ; return (wrap2 <.> wrap1, rho2) } +instantiateSigma :: CtOrigin -> [TyVar] -> TcThetaType -> TcSigmaType + -> TcM ([TcTyVar], HsWrapper, TcSigmaType) +-- (instantiate orig tvs theta ty) +-- instantiates the the type variables tvs, emits the (instantiated) +-- constraints theta, and returns the (instantiated) type ty +instantiateSigma orig tvs theta body_ty + = do { (subst, inst_tvs) <- mapAccumLM newMetaTyVarX empty_subst tvs + ; let inst_theta = substTheta subst theta + inst_body = substTy subst body_ty + inst_tv_tys = mkTyVarTys inst_tvs + + ; wrap <- instCall orig inst_tv_tys inst_theta + ; traceTc "Instantiating" + (vcat [ text "origin" <+> pprCtOrigin orig + , text "tvs" <+> ppr tvs + , text "theta" <+> ppr theta + , text "type" <+> debugPprType body_ty + , text "with" <+> vcat (map debugPprType inst_tv_tys) + , text "theta:" <+> ppr inst_theta ]) - | otherwise = return (idHsWrapper, ty) + ; return (inst_tvs, wrap, inst_body) } where - - should_inst bndr - | inst_all = True - | otherwise = binderArgFlag bndr == Inferred + free_tvs = tyCoVarsOfType body_ty `unionVarSet` tyCoVarsOfTypes theta + in_scope = mkInScopeSet (free_tvs `delVarSetList` tvs) + empty_subst = mkEmptyTCvSubst in_scope instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM TCvSubst -- Use this when you want to instantiate (forall a b c. ty) with diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 0995eb51e9..62e39879d7 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -801,10 +801,11 @@ influences the way it is tidied; see TypeRep.tidyTyVarBndr. metaInfoToTyVarName :: MetaInfo -> FastString metaInfoToTyVarName meta_info = case meta_info of - TauTv -> fsLit "t" - FlatMetaTv -> fsLit "fmv" - FlatSkolTv -> fsLit "fsk" - TyVarTv -> fsLit "a" + TauTv -> fsLit "t" + FlatMetaTv -> fsLit "fmv" + FlatSkolTv -> fsLit "fsk" + TyVarTv -> fsLit "a" + RuntimeUnkTv -> fsLit "r" newAnonMetaTyVar :: MetaInfo -> Kind -> TcM TcTyVar newAnonMetaTyVar mi = newNamedAnonMetaTyVar (metaInfoToTyVarName mi) mi diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 21b6b962d9..6d5ef37442 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -57,7 +57,7 @@ module GHC.Tc.Utils.TcType ( -- These are important because they do not look through newtypes getTyVar, tcSplitForAllTy_maybe, - tcSplitForAllTys, + tcSplitForAllTys, tcSplitSomeForAllTys, tcSplitForAllTysReq, tcSplitForAllTysInvis, tcSplitPiTys, tcSplitPiTy_maybe, tcSplitForAllVarBndrs, tcSplitPhiTy, tcSplitPredFunTy_maybe, @@ -561,6 +561,9 @@ data MetaInfo -- It is filled in /only/ by unflattenGivens -- See Note [The flattening story] in GHC.Tc.Solver.Flatten + | RuntimeUnkTv -- A unification variable used in the GHCi debugger. + -- It /is/ allowed to unify with a polytype, unlike TauTv + instance Outputable MetaDetails where ppr Flexi = text "Flexi" ppr (Indirect ty) = text "Indirect" <+> ppr ty @@ -570,6 +573,7 @@ instance Outputable MetaInfo where ppr TyVarTv = text "tyv" ppr FlatMetaTv = text "fmv" ppr FlatSkolTv = text "fsk" + ppr RuntimeUnkTv = text "rutv" {- ********************************************************************* * * @@ -1222,6 +1226,19 @@ tcSplitForAllTys ty = ASSERT( all isTyVar (fst sty) ) sty where sty = splitForAllTys ty +-- | Like 'tcSplitForAllTys', but only splits a 'ForAllTy' if @argf_pred argf@ +-- is 'True', where @argf@ is the visibility of the @ForAllTy@'s binder and +-- @argf_pred@ is a predicate over visibilities provided as an argument to this +-- function. +tcSplitSomeForAllTys :: (ArgFlag -> Bool) -> Type -> ([TyVar], Type) +tcSplitSomeForAllTys argf_pred ty + = split ty ty [] + where + split _ (ForAllTy (Bndr tv argf) ty) tvs + | argf_pred argf = split ty ty (tv:tvs) + split orig_ty ty tvs | Just ty' <- coreView ty = split orig_ty ty' tvs + split orig_ty _ tvs = (reverse tvs, orig_ty) + -- | Like 'tcSplitForAllTys', but only splits 'ForAllTy's with 'Required' type -- variable binders. All split tyvars are annotated with '()'. tcSplitForAllTysReq :: Type -> ([TcReqTVBinder], Type) diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index 6a83348b2a..0c29a6557f 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -32,8 +32,8 @@ module GHC.Tc.Utils.Unify ( matchExpectedTyConApp, matchExpectedAppTy, matchExpectedFunTys, - matchActualFunTysRho, matchActualFunTySigma, matchExpectedFunKind, + matchActualFunTySigma, matchActualFunTysRho, metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..) @@ -69,13 +69,155 @@ import GHC.Driver.Session import GHC.Types.Basic import GHC.Data.Bag import GHC.Utils.Misc -import qualified GHC.LanguageExtensions as LangExt import GHC.Utils.Outputable as Outputable import GHC.Utils.Panic import Control.Monad import Control.Arrow ( second ) + +{- ********************************************************************* +* * + matchActualFunTys +* * +********************************************************************* -} + +-- | matchActualFunTySigma does looks for just one function arrow +-- returning an uninstantiated sigma-type +matchActualFunTySigma + :: SDoc -- See Note [Herald for matchExpectedFunTys] + -> Maybe SDoc -- The thing with type TcSigmaType + -> (Arity, [Scaled TcSigmaType]) -- Total number of value args in the call, and + -- types of values args to which function has + -- been applied already (reversed) + -- Both are used only for error messages) + -> TcRhoType -- Type to analyse: a TcRhoType + -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType) +-- The /argument/ is a RhoType +-- The /result/ is an (uninstantiated) SigmaType +-- +-- See Note [matchActualFunTy error handling] for the first three arguments + +-- If (wrap, arg_ty, res_ty) = matchActualFunTySigma ... fun_ty +-- then wrap :: fun_ty ~> (arg_ty -> res_ty) +-- and NB: res_ty is an (uninstantiated) SigmaType + +matchActualFunTySigma herald mb_thing err_info fun_ty + = ASSERT2( isRhoTy fun_ty, ppr fun_ty ) + go fun_ty + where + -- Does not allocate unnecessary meta variables: if the input already is + -- a function, we just take it apart. Not only is this efficient, + -- it's important for higher rank: the argument might be of form + -- (forall a. ty) -> other + -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd + -- hide the forall inside a meta-variable + go :: TcRhoType -- The type we're processing, perhaps after + -- expanding any type synonym + -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType) + go ty | Just ty' <- tcView ty = go ty' + + go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty }) + = ASSERT( af == VisArg ) + return (idHsWrapper, Scaled w arg_ty, res_ty) + + go ty@(TyVarTy tv) + | isMetaTyVar tv + = do { cts <- readMetaTyVar tv + ; case cts of + Indirect ty' -> go ty' + Flexi -> defer ty } + + -- In all other cases we bale out into ordinary unification + -- However unlike the meta-tyvar case, we are sure that the + -- number of arguments doesn't match arity of the original + -- type, so we can add a bit more context to the error message + -- (cf #7869). + -- + -- It is not always an error, because specialized type may have + -- different arity, for example: + -- + -- > f1 = f2 'a' + -- > f2 :: Monad m => m Bool + -- > f2 = undefined + -- + -- But in that case we add specialized type into error context + -- anyway, because it may be useful. See also #9605. + go ty = addErrCtxtM (mk_ctxt ty) (defer ty) + + ------------ + defer fun_ty + = do { arg_ty <- newOpenFlexiTyVarTy + ; res_ty <- newOpenFlexiTyVarTy + ; let unif_fun_ty = mkVisFunTyMany arg_ty res_ty + ; co <- unifyType mb_thing fun_ty unif_fun_ty + ; return (mkWpCastN co, unrestricted arg_ty, res_ty) } + + ------------ + mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) + mk_ctxt res_ty env = mkFunTysMsg env herald (reverse arg_tys_so_far) + res_ty n_val_args_in_call + (n_val_args_in_call, arg_tys_so_far) = err_info + +{- Note [matchActualFunTy error handling] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +matchActualFunTySigma is made much more complicated by the +desire to produce good error messages. Consider the application + f @Int x y +In GHC.Tc.Gen.Expr.tcArgs we deal with visible type arguments, +and then call matchActualFunTysPart for each individual value +argument. It, in turn, must instantiate any type/dictionary args, +before looking for an arrow type. + +But if it doesn't find an arrow type, it wants to generate a message +like "f is applied to two arguments but its type only has one". +To do that, it needs to konw about the args that tcArgs has already +munched up -- hence passing in n_val_args_in_call and arg_tys_so_far; +and hence also the accumulating so_far arg to 'go'. + +This allows us (in mk_ctxt) to construct f's /instantiated/ type, +with just the values-arg arrows, which is what we really want +in the error message. + +Ugh! +-} + +-- Like 'matchExpectedFunTys', but used when you have an "actual" type, +-- for example in function application +matchActualFunTysRho :: SDoc -- See Note [Herald for matchExpectedFunTys] + -> CtOrigin + -> Maybe SDoc -- the thing with type TcSigmaType + -> Arity + -> TcSigmaType + -> TcM (HsWrapper, [Scaled TcSigmaType], TcRhoType) +-- If matchActualFunTysRho n ty = (wrap, [t1,..,tn], res_ty) +-- then wrap : ty ~> (t1 -> ... -> tn -> res_ty) +-- and res_ty is a RhoType +-- NB: the returned type is top-instantiated; it's a RhoType +matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty + = go n_val_args_wanted [] fun_ty + where + go n so_far fun_ty + | not (isRhoTy fun_ty) + = do { (wrap1, rho) <- topInstantiate ct_orig fun_ty + ; (wrap2, arg_tys, res_ty) <- go n so_far rho + ; return (wrap2 <.> wrap1, arg_tys, res_ty) } + + go 0 _ fun_ty = return (idHsWrapper, [], fun_ty) + + go n so_far fun_ty + = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTySigma + herald mb_thing + (n_val_args_wanted, so_far) + fun_ty + ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1 + ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty doc + ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) } + where + doc = text "When inferring the argument type of a function with type" <+> + quotes (ppr fun_ty) + + {- ************************************************************************ * * @@ -226,167 +368,32 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside ------------ mk_ctxt :: [Scaled ExpSigmaType] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) mk_ctxt arg_tys res_ty env - = do { (env', ty) <- zonkTidyTcType env (mkVisFunTys arg_tys' res_ty) - ; return ( env', mk_fun_tys_msg herald ty arity) } + = mkFunTysMsg env herald arg_tys' res_ty arity where - arg_tys' = map (\(Scaled u v) -> Scaled u (checkingExpType "matchExpectedFunTys" v)) (reverse arg_tys) + arg_tys' = map (\(Scaled u v) -> Scaled u (checkingExpType "matchExpectedFunTys" v)) $ + reverse arg_tys -- this is safe b/c we're called from "go" --- Like 'matchExpectedFunTys', but used when you have an "actual" type, --- for example in function application -matchActualFunTysRho :: SDoc -- See Note [Herald for matchExpectedFunTys] - -> CtOrigin - -> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType - -> Arity - -> TcSigmaType - -> TcM (HsWrapper, [Scaled TcSigmaType], TcRhoType) --- If matchActualFunTysRho n ty = (wrap, [t1,..,tn], res_ty) --- then wrap : ty ~> (t1 -> ... -> tn -> res_ty) --- and res_ty is a RhoType --- NB: the returned type is top-instantiated; it's a RhoType -matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty - = go n_val_args_wanted [] fun_ty - where - go 0 _ fun_ty - = do { (wrap, rho) <- topInstantiate ct_orig fun_ty - ; return (wrap, [], rho) } - go n so_far fun_ty - = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTySigma - herald ct_orig mb_thing - (n_val_args_wanted, so_far) - fun_ty - ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1 - ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty doc - ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) } - where - doc = text "When inferring the argument type of a function with type" <+> - quotes (ppr fun_ty) - --- | matchActualFunTySigm does looks for just one function arrow --- returning an uninstantiated sigma-type -matchActualFunTySigma - :: SDoc -- See Note [Herald for matchExpectedFunTys] - -> CtOrigin - -> Maybe (HsExpr GhcRn) -- The thing with type TcSigmaType - -> (Arity, [Scaled TcSigmaType]) -- Total number of value args in the call, and - -- types of values args to which function has - -- been applied already (reversed) - -- Both are used only for error messages) - -> TcSigmaType -- Type to analyse - -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType) --- See Note [matchActualFunTys error handling] for all these arguments - --- If (wrap, arg_ty, res_ty) = matchActualFunTySigma ... fun_ty --- then wrap :: fun_ty ~> (arg_ty -> res_ty) --- and NB: res_ty is an (uninstantiated) SigmaType - -matchActualFunTySigma herald ct_orig mb_thing err_info fun_ty - = go fun_ty --- Does not allocate unnecessary meta variables: if the input already is --- a function, we just take it apart. Not only is this efficient, --- it's important for higher rank: the argument might be of form --- (forall a. ty) -> other --- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd --- hide the forall inside a meta-variable - --- (*) Sometimes it's necessary to call matchActualFunTys with only part --- (that is, to the right of some arrows) of the type of the function in --- question. (See GHC.Tc.Gen.Expr.tcArgs.) This argument is the reversed list of --- arguments already seen (that is, not part of the TcSigmaType passed --- in elsewhere). +mkFunTysMsg :: TidyEnv -> SDoc -> [Scaled TcType] -> TcType -> Arity + -> TcM (TidyEnv, MsgDoc) +mkFunTysMsg env herald arg_tys res_ty n_val_args_in_call + = do { (env', fun_rho) <- zonkTidyTcType env $ + mkVisFunTys arg_tys res_ty - where - go :: TcSigmaType -- The remainder of the type as we're processing - -> TcM (HsWrapper, Scaled TcSigmaType, TcSigmaType) - go ty | Just ty' <- tcView ty = go ty' + ; let (all_arg_tys, _) = splitFunTys fun_rho + n_fun_args = length all_arg_tys - go ty - | not (null tvs && null theta) - = do { (wrap1, rho) <- topInstantiate ct_orig ty - ; (wrap2, arg_ty, res_ty) <- go rho - ; return (wrap2 <.> wrap1, arg_ty, res_ty) } - where - (tvs, theta, _) = tcSplitSigmaTy ty - - go (FunTy { ft_af = af, ft_mult = w, ft_arg = arg_ty, ft_res = res_ty }) - = ASSERT( af == VisArg ) - return (idHsWrapper, Scaled w arg_ty, res_ty) + msg | n_val_args_in_call <= n_fun_args -- Enough args, in the end + = text "In the result of a function call" + | otherwise + = hang (full_herald <> comma) + 2 (sep [ text "but its type" <+> quotes (pprType fun_rho) + , if n_fun_args == 0 then text "has none" + else text "has only" <+> speakN n_fun_args]) - go ty@(TyVarTy tv) - | isMetaTyVar tv - = do { cts <- readMetaTyVar tv - ; case cts of - Indirect ty' -> go ty' - Flexi -> defer ty } - - -- In all other cases we bale out into ordinary unification - -- However unlike the meta-tyvar case, we are sure that the - -- number of arguments doesn't match arity of the original - -- type, so we can add a bit more context to the error message - -- (cf #7869). - -- - -- It is not always an error, because specialized type may have - -- different arity, for example: - -- - -- > f1 = f2 'a' - -- > f2 :: Monad m => m Bool - -- > f2 = undefined - -- - -- But in that case we add specialized type into error context - -- anyway, because it may be useful. See also #9605. - go ty = addErrCtxtM (mk_ctxt ty) (defer ty) - - ------------ - defer fun_ty - = do { arg_ty <- newOpenFlexiTyVarTy - ; res_ty <- newOpenFlexiTyVarTy - ; let unif_fun_ty = mkVisFunTyMany arg_ty res_ty - ; co <- unifyType mb_thing fun_ty unif_fun_ty - ; return (mkWpCastN co, unrestricted arg_ty, res_ty) } - - ------------ - mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) - mk_ctxt res_ty env - = do { (env', ty) <- zonkTidyTcType env $ - mkVisFunTys (reverse arg_tys_so_far) res_ty - ; return (env', mk_fun_tys_msg herald ty n_val_args_in_call) } - (n_val_args_in_call, arg_tys_so_far) = err_info - -mk_fun_tys_msg :: SDoc -> TcType -> Arity -> SDoc -mk_fun_tys_msg herald ty n_args_in_call - | n_args_in_call <= n_fun_args -- Enough args, in the end - = text "In the result of a function call" - | otherwise - = hang (herald <+> speakNOf n_args_in_call (text "value argument") <> comma) - 2 (sep [ text "but its type" <+> quotes (pprType ty) - , if n_fun_args == 0 then text "has none" - else text "has only" <+> speakN n_fun_args]) - where - (args, _) = tcSplitFunTys ty - n_fun_args = length args - -{- Note [matchActualFunTys error handling] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -matchActualFunTysPart is made much more complicated by the -desire to produce good error messages. Consider the application - f @Int x y -In GHC.Tc.Gen.Expr.tcArgs we deal with visible type arguments, -and then call matchActualFunTysPart for each individual value -argument. It, in turn, must instantiate any type/dictionary args, -before looking for an arrow type. - -But if it doesn't find an arrow type, it wants to generate a message -like "f is applied to two arguments but its type only has one". -To do that, it needs to konw about the args that tcArgs has already -munched up -- hence passing in n_val_args_in_call and arg_tys_so_far; -and hence also the accumulating so_far arg to 'go'. - -This allows us (in mk_ctxt) to construct f's /instantiated/ type, -with just the values-arg arrows, which is what we really want -in the error message. - -Ugh! --} + ; return (env', msg) } + where + full_herald = herald <+> speakNOf n_val_args_in_call (text "value argument") ---------------------- matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType) @@ -519,7 +526,7 @@ tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTc -> TcSigmaType -> ExpR tcWrapResultO orig rn_expr expr actual_ty res_ty = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty , text "Expected:" <+> ppr res_ty ]) - ; wrap <- tcSubTypeNC orig GenSigCtxt (Just rn_expr) actual_ty res_ty + ; wrap <- tcSubTypeNC orig GenSigCtxt (Just (ppr rn_expr)) actual_ty res_ty ; return (mkHsWrap wrap expr) } tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTc @@ -533,7 +540,7 @@ tcWrapResultMono rn_expr expr act_ty res_ty = ASSERT2( isRhoTy act_ty, ppr act_ty $$ ppr rn_expr ) do { co <- case res_ty of Infer inf_res -> fillInferResult act_ty inf_res - Check exp_ty -> unifyType (Just rn_expr) act_ty exp_ty + Check exp_ty -> unifyType (Just (ppr rn_expr)) act_ty exp_ty ; return (mkHsWrapCo co expr) } ------------------------ @@ -565,7 +572,7 @@ tcSubType orig ctxt ty_actual ty_expected tcSubTypeNC :: CtOrigin -- Used when instantiating -> UserTypeCtxt -- Used when skolemising - -> Maybe (HsExpr GhcRn) -- The expression that has type 'actual' (if known) + -> Maybe SDoc -- The expression that has type 'actual' (if known) -> TcSigmaType -- Actual type -> ExpRhoType -- Expected type -> TcM HsWrapper @@ -661,12 +668,7 @@ tc_sub_type unify inst_orig ctxt ty_actual ty_expected ; return (sk_wrap <.> inner_wrap) } where - possibly_poly ty - | isForAllTy ty = True - | Just (_, _, res) <- splitFunTy_maybe ty = possibly_poly res - | otherwise = False - -- NB *not* tcSplitFunTy, because here we want - -- to decompose type-class arguments too + possibly_poly ty = not (isRhoTy ty) definitely_poly ty | (tvs, theta, tau) <- tcSplitSigmaTy ty @@ -719,9 +721,6 @@ So roughly: then we can revert to simple equality. But we need to be careful. These examples are all fine: - * (Char -> forall a. a->a) <= (forall a. Char -> a -> a) - Polymorphism is buried in ty_actual - * (Char->Char) <= (forall a. Char -> Char) ty_expected isn't really polymorphic @@ -832,10 +831,11 @@ to checkConstraints. tcSkolemiseScoped is very similar, but differs in two ways: -* It deals specially with just the outer forall, bringing those - type variables into lexical scope. To my surprise, I found that - doing this regardless (in tcSkolemise) caused a non-trivial (1%-ish) - perf hit on the compiler. +* It deals specially with just the outer forall, bringing those type + variables into lexical scope. To my surprise, I found that doing + this unconditionally in tcSkolemise (i.e. doing it even if we don't + need to bring the variables into lexical scope, which is harmless) + caused a non-trivial (1%-ish) perf hit on the compiler. * It always calls checkConstraints, even if there are no skolem variables at all. Reason: there might be nested deferred errors @@ -848,6 +848,8 @@ tcSkolemise, tcSkolemiseScoped -> (TcType -> TcM result) -> TcM (HsWrapper, result) -- ^ The wrapper has type: spec_ty ~> expected_ty +-- See Note [Skolemisation] for the differences between +-- tcSkolemiseScoped and tcSkolemise tcSkolemiseScoped ctxt expected_ty thing_inside = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty @@ -1039,7 +1041,7 @@ take care: [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. #14185 is an example. - Building an implication keeps them separage. + Building an implication keeps them separate. -} {- @@ -1053,8 +1055,9 @@ The exported functions are all defined as versions of some non-exported generic functions. -} -unifyType :: Maybe (HsExpr GhcRn) -- ^ If present, has type 'ty1' - -> TcTauType -> TcTauType -> TcM TcCoercionN +unifyType :: Maybe SDoc -- ^ If present, the thing that has type ty1 + -> TcTauType -> TcTauType -- ty1, ty2 + -> TcM TcCoercionN -- :: ty1 ~# ty2 -- Actual and expected types -- Returns a coercion : ty1 ~ ty2 unifyType thing ty1 ty2 @@ -1077,13 +1080,13 @@ unifyTypeET ty1 ty2 , uo_visible = True } -unifyKind :: Maybe (HsType GhcRn) -> TcKind -> TcKind -> TcM CoercionN -unifyKind thing ty1 ty2 +unifyKind :: Maybe SDoc -> TcKind -> TcKind -> TcM CoercionN +unifyKind mb_thing ty1 ty2 = uType KindLevel origin ty1 ty2 where origin = TypeEqOrigin { uo_actual = ty1 , uo_expected = ty2 - , uo_thing = ppr <$> thing + , uo_thing = mb_thing , uo_visible = True } @@ -1186,10 +1189,12 @@ uType t_or_k origin orig_ty1 orig_ty2 | Just ty1' <- tcView ty1 = go ty1' ty2 | Just ty2' <- tcView ty2 = go ty1 ty2' - -- Functions (or predicate functions) just check the two parts - go (FunTy _ w1 fun1 arg1) (FunTy _ w2 fun2 arg2) - = do { co_l <- uType t_or_k origin fun1 fun2 - ; co_r <- uType t_or_k origin arg1 arg2 + -- Functions (t1 -> t2) just check the two parts + -- Do not attempt (c => t); just defer + go (FunTy { ft_af = VisArg, ft_mult = w1, ft_arg = arg1, ft_res = res1 }) + (FunTy { ft_af = VisArg, ft_mult = w2, ft_arg = arg2, ft_res = res2 }) + = do { co_l <- uType t_or_k origin arg1 arg2 + ; co_r <- uType t_or_k origin res1 res2 ; co_w <- uType t_or_k origin w1 w2 ; return $ mkFunCo Nominal co_w co_l co_r } @@ -1479,6 +1484,7 @@ swapOverTyVars is_given tv1 tv2 lhsPriority :: TcTyVar -> Int -- Higher => more important to be on the LHS +-- => more likely to be eliminated -- See Note [TyVar/TyVar orientation] lhsPriority tv = ASSERT2( isTyVar tv, ppr tv) @@ -1486,10 +1492,12 @@ lhsPriority tv RuntimeUnk -> 0 SkolemTv {} -> 0 MetaTv { mtv_info = info } -> case info of - FlatSkolTv -> 1 - TyVarTv -> 2 - TauTv -> 3 - FlatMetaTv -> 4 + FlatSkolTv -> 1 + TyVarTv -> 2 + TauTv -> 3 + FlatMetaTv -> 4 + RuntimeUnkTv -> 5 + {- Note [TyVar/TyVar orientation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Given (a ~ b), should we orient the CTyEqCan as (a~b) or (b~a)? @@ -1855,7 +1863,7 @@ matchExpectedFunKind hs_ty n k = go n k Indirect fun_kind -> go n fun_kind Flexi -> defer n k } - go n (FunTy _ w arg res) + go n (FunTy { ft_mult = w, ft_arg = arg, ft_res = res }) = do { co <- go (n-1) res ; return (mkTcFunCo Nominal (mkTcNomReflCo w) (mkTcNomReflCo arg) co) } @@ -1943,7 +1951,7 @@ occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult () -- a) the given variable occurs in the given type. -- b) there is a forall in the type (unless we have -XImpredicativeTypes) occCheckForErrors dflags tv ty - = case preCheck dflags True tv ty of + = case mtvu_check dflags True tv ty of MTVU_OK _ -> MTVU_OK () MTVU_Bad -> MTVU_Bad MTVU_HoleBlocker -> MTVU_HoleBlocker @@ -1957,13 +1965,20 @@ metaTyVarUpdateOK :: DynFlags -> TcType -- ty :: k2 -> MetaTyVarUpdateResult TcType -- possibly-expanded ty -- (metaTyVarUpdateOK tv ty) --- We are about to update the meta-tyvar tv with ty --- Check (a) that tv doesn't occur in ty (occurs check) +-- Checks that the equality tv~ty is OK to be used to rewrite +-- other equalities. Equivalently, checks the conditions for CTyEqCan +-- (a) that tv doesn't occur in ty (occurs check) -- (b) that ty does not have any foralls -- (in the impredicative case), or type functions -- (c) that ty does not have any blocking coercion holes -- See Note [Equalities with incompatible kinds] in "GHC.Tc.Solver.Canonical" -- +-- Used in two places: +-- - In the eager unifier: uUnfilledVar2 +-- - In the canonicaliser: GHC.Tc.Solver.Canonical.canEqTyVar2 +-- Note that in the latter case tv is not necessarily a meta-tyvar, +-- despite the name of this function. + -- We have two possible outcomes: -- (1) Return the type to update the type variable with, -- [we know the update is ok] @@ -1982,7 +1997,7 @@ metaTyVarUpdateOK :: DynFlags -- See Note [Refactoring hazard: checkTauTvUpdate] metaTyVarUpdateOK dflags tv ty - = case preCheck dflags False tv ty of + = case mtvu_check dflags False tv ty of -- False <=> type families not ok -- See Note [Prevent unification with type families] MTVU_OK _ -> MTVU_OK ty @@ -1992,11 +2007,11 @@ metaTyVarUpdateOK dflags tv ty Just expanded_ty -> MTVU_OK expanded_ty Nothing -> MTVU_Occurs -preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult () --- A quick check for --- (a) a forall type (unless -XImpredicativeTypes) --- (b) a predicate type (unless -XImpredicativeTypes) --- (c) a type family +mtvu_check :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult () +-- Checks the invariants for CTyEqCan. In particular: +-- (a) a forall type (forall a. blah) +-- (b) a predicate type (c => ty) +-- (c) a type family; see Note [Prevent unification with type families] -- (d) a blocking coercion hole -- (e) an occurrence of the type variable (occurs check) -- @@ -2004,15 +2019,20 @@ preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult () -- inside the kinds of variables it mentions. For (d) we look deeply -- in coercions, and for (e) we do look in the kinds of course. -preCheck dflags ty_fam_ok tv ty +mtvu_check dflags ty_fam_ok tv ty = fast_check ty where - details = tcTyVarDetails tv - impredicative_ok = canUnifyWithPolyType dflags details - ok :: MetaTyVarUpdateResult () ok = MTVU_OK () + -- The GHCi runtime debugger does its type-matching with + -- unification variables that can unify with a polytype + -- or a TyCon that would usually be disallowed by bad_tc + -- See Note [RuntimeUnkTv] in GHC.Runtime.Heap.Inspect + ghci_tv = case tcTyVarDetails tv of + MetaTv { mtv_info = RuntimeUnkTv } -> True + _ -> False + fast_check :: TcType -> MetaTyVarUpdateResult () fast_check (TyVarTy tv') | tv == tv' = MTVU_Occurs @@ -2021,19 +2041,19 @@ preCheck dflags ty_fam_ok tv ty -- in GHC.Core.Type fast_check (TyConApp tc tys) - | bad_tc tc = MTVU_Bad + | bad_tc tc, not ghci_tv = MTVU_Bad | otherwise = mapM fast_check tys >> ok fast_check (LitTy {}) = ok fast_check (FunTy{ft_af = af, ft_mult = w, ft_arg = a, ft_res = r}) | InvisArg <- af - , not impredicative_ok = MTVU_Bad + , not ghci_tv = MTVU_Bad | otherwise = fast_check w >> fast_check a >> fast_check r 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 (Bndr tv' _) ty) - | not impredicative_ok = MTVU_Bad - | tv == tv' = ok + | not ghci_tv = MTVU_Bad + | tv == tv' = ok | otherwise = do { fast_check_occ (tyVarKind tv') ; fast_check_occ ty } -- Under a forall we look only for occurrences of @@ -2056,14 +2076,6 @@ preCheck dflags ty_fam_ok tv ty bad_tc :: TyCon -> Bool bad_tc tc - | not (impredicative_ok || isTauTyCon tc) = True - | not (ty_fam_ok || isFamFreeTyCon tc) = True - | otherwise = False - -canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool -canUnifyWithPolyType dflags details - = case details of - MetaTv { mtv_info = TyVarTv } -> False - MetaTv { mtv_info = TauTv } -> xopt LangExt.ImpredicativeTypes dflags - _other -> True - -- We can have non-meta tyvars in given constraints + | not (isTauTyCon tc) = True + | not (ty_fam_ok || isFamFreeTyCon tc) = True + | otherwise = False diff --git a/compiler/GHC/Tc/Utils/Unify.hs-boot b/compiler/GHC/Tc/Utils/Unify.hs-boot index a54107fe07..7b4561420c 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs-boot +++ b/compiler/GHC/Tc/Utils/Unify.hs-boot @@ -5,14 +5,14 @@ import GHC.Tc.Utils.TcType ( TcTauType ) import GHC.Tc.Types ( TcM ) import GHC.Tc.Types.Evidence ( TcCoercion, HsWrapper ) import GHC.Tc.Types.Origin ( CtOrigin ) -import GHC.Hs.Expr ( HsExpr ) -import GHC.Hs.Type ( HsType, Mult ) -import GHC.Hs.Extension ( GhcRn ) +import GHC.Utils.Outputable( SDoc ) +import GHC.Hs.Type ( Mult ) + -- This boot file exists only to tie the knot between -- GHC.Tc.Utils.Unify and Inst -unifyType :: Maybe (HsExpr GhcRn) -> TcTauType -> TcTauType -> TcM TcCoercion -unifyKind :: Maybe (HsType GhcRn) -> TcTauType -> TcTauType -> TcM TcCoercion +unifyType :: Maybe SDoc -> TcTauType -> TcTauType -> TcM TcCoercion +unifyKind :: Maybe SDoc -> TcTauType -> TcTauType -> TcM TcCoercion tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs index 296dfa79a4..e00b5a09e3 100644 --- a/compiler/GHC/Tc/Utils/Zonk.hs +++ b/compiler/GHC/Tc/Utils/Zonk.hs @@ -723,6 +723,14 @@ zonkExpr env (HsVar x (L l id)) = ASSERT2( isNothing (isDataConId_maybe id), ppr id ) return (HsVar x (L l (zonkIdOcc env id))) +zonkExpr env (HsUnboundVar v occ) + = return (HsUnboundVar (zonkIdOcc env v) occ) + +zonkExpr env (HsRecFld _ (Ambiguous v occ)) + = return (HsRecFld noExtField (Ambiguous (zonkIdOcc env v) occ)) +zonkExpr env (HsRecFld _ (Unambiguous v occ)) + = return (HsRecFld noExtField (Unambiguous (zonkIdOcc env v) occ)) + zonkExpr _ e@(HsConLikeOut {}) = return e zonkExpr _ (HsIPVar x id) @@ -915,9 +923,6 @@ zonkExpr env (XExpr (WrapExpr (HsWrap co_fn expr))) zonkExpr env (XExpr (ExpansionExpr (HsExpanded a b))) = XExpr . ExpansionExpr . HsExpanded a <$> zonkExpr env b -zonkExpr _ e@(HsUnboundVar {}) - = return e - zonkExpr _ expr = pprPanic "zonkExpr" (ppr expr) ------------------------------------------------------------------------- |