diff options
Diffstat (limited to 'compiler/GHC/Tc/Utils/TcType.hs')
| -rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 184 |
1 files changed, 24 insertions, 160 deletions
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index ae35cea3a2..807ad0ab56 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -92,11 +92,12 @@ module GHC.Tc.Utils.TcType ( orphNamesOfType, orphNamesOfCo, orphNamesOfTypes, orphNamesOfCoCon, getDFunTyKey, evVarPred, + ambigTkvsOfTy, --------------------------------- -- Predicate types mkMinimalBySCs, transSuperClasses, - pickQuantifiablePreds, pickCapturedPreds, + pickCapturedPreds, immSuperClasses, boxEqPred, isImprovementPred, @@ -105,7 +106,7 @@ module GHC.Tc.Utils.TcType ( -- * Finding "exact" (non-dead) type variables exactTyCoVarsOfType, exactTyCoVarsOfTypes, - anyRewritableTyVar, anyRewritableTyFamApp, anyRewritableCanEqLHS, + anyRewritableTyVar, anyRewritableTyFamApp, --------------------------------- -- Foreign import and export @@ -231,6 +232,7 @@ import qualified GHC.LanguageExtensions as LangExt import Data.IORef import Data.List.NonEmpty( NonEmpty(..) ) +import Data.List ( partition ) import {-# SOURCE #-} GHC.Tc.Types.Origin ( unkSkol, SkolemInfo ) @@ -847,15 +849,14 @@ isTyFamFree :: Type -> Bool -- ^ Check that a type does not contain any type family applications. isTyFamFree = null . tcTyFamInsts -any_rewritable :: Bool -- Ignore casts and coercions - -> EqRel -- Ambient role +any_rewritable :: EqRel -- Ambient role -> (EqRel -> TcTyVar -> Bool) -- check tyvar -> (EqRel -> TyCon -> [TcType] -> Bool) -- check type family -> (TyCon -> Bool) -- expand type synonym? -> TcType -> Bool -- Checks every tyvar and tyconapp (not including FunTys) within a type, -- ORing the results of the predicates above together --- Do not look inside casts and coercions if 'ignore_cos' is True +-- Do not look inside casts and coercions -- See Note [anyRewritableTyVar must be role-aware] -- -- This looks like it should use foldTyCo, but that function is @@ -864,7 +865,7 @@ any_rewritable :: Bool -- Ignore casts and coercions -- -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function. {-# INLINE any_rewritable #-} -- this allows specialization of predicates -any_rewritable ignore_cos role tv_pred tc_pred should_expand +any_rewritable role tv_pred tc_pred should_expand = go role emptyVarSet where go_tv rl bvs tv | tv `elemVarSet` bvs = False @@ -890,8 +891,8 @@ any_rewritable ignore_cos role tv_pred tc_pred should_expand where arg_rep = getRuntimeRep arg -- forgetting these causes #17024 res_rep = getRuntimeRep res go rl bvs (ForAllTy tv ty) = go rl (bvs `extendVarSet` binderVar tv) ty - go rl bvs (CastTy ty co) = go rl bvs ty || go_co rl bvs co - go rl bvs (CoercionTy co) = go_co rl bvs co -- ToDo: check + go rl bvs (CastTy ty _) = go rl bvs ty + go _ _ (CoercionTy _) = False go_tc NomEq bvs _ tys = any (go NomEq bvs) tys go_tc ReprEq bvs tc tys = any (go_arg bvs) @@ -901,19 +902,12 @@ any_rewritable ignore_cos role tv_pred tc_pred should_expand go_arg bvs (Representational, ty) = go ReprEq bvs ty go_arg _ (Phantom, _) = False -- We never rewrite with phantoms - go_co rl bvs co - | ignore_cos = False - | otherwise = anyVarSet (go_tv rl bvs) (tyCoVarsOfCo co) - -- We don't have an equivalent of anyRewritableTyVar for coercions - -- (at least not yet) so take the free vars and test them - -anyRewritableTyVar :: Bool -- Ignore casts and coercions - -> EqRel -- Ambient role +anyRewritableTyVar :: EqRel -- Ambient role -> (EqRel -> TcTyVar -> Bool) -- check tyvar -> TcType -> Bool -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function. -anyRewritableTyVar ignore_cos role pred - = any_rewritable ignore_cos role pred +anyRewritableTyVar role pred + = any_rewritable role pred (\ _ _ _ -> False) -- no special check for tyconapps -- (this False is ORed with other results, so it -- really means "do nothing special"; the arguments @@ -930,18 +924,7 @@ anyRewritableTyFamApp :: EqRel -- Ambient role -- always ignores casts & coercions -- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function. anyRewritableTyFamApp role check_tyconapp - = any_rewritable True role (\ _ _ -> False) check_tyconapp (not . isFamFreeTyCon) - --- This version is used by shouldSplitWD. It *does* look in casts --- and coercions, and it always expands type synonyms whose RHSs mention --- type families. --- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function. -anyRewritableCanEqLHS :: EqRel -- Ambient role - -> (EqRel -> TcTyVar -> Bool) -- check tyvar - -> (EqRel -> TyCon -> [TcType] -> Bool) -- check type family - -> TcType -> Bool -anyRewritableCanEqLHS role check_tyvar check_tyconapp - = any_rewritable False role check_tyvar check_tyconapp (not . isFamFreeTyCon) + = any_rewritable role (\ _ _ -> False) check_tyconapp (not . isFamFreeTyCon) {- Note [anyRewritableTyVar must be role-aware] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1170,6 +1153,16 @@ findDupTyVarTvs prs eq_snd (_,tv1) (_,tv2) = tv1 == tv2 mk_result_prs ((n1,_) :| xs) = map (\(n2,_) -> (n1,n2)) xs +-- | Returns the (kind, type) variables in a type that are +-- as-yet-unknown: metavariables and RuntimeUnks +ambigTkvsOfTy :: TcType -> ([Var],[Var]) +ambigTkvsOfTy ty + = partition (`elemVarSet` dep_tkv_set) ambig_tkvs + where + tkvs = tyCoVarsOfTypeList ty + ambig_tkvs = filter isAmbiguousTyVar tkvs + dep_tkv_set = tyCoVarsOfTypes (map tyVarKind tkvs) + {- ************************************************************************ * * @@ -1774,71 +1767,7 @@ evVarPred var = varType var -- partial signatures, (isEvVarType kappa) will return False. But -- nothing is wrong. So I just removed the ASSERT. ------------------- --- | When inferring types, should we quantify over a given predicate? --- Generally true of classes; generally false of equality constraints. --- Equality constraints that mention quantified type variables and --- implicit variables complicate the story. See Notes --- [Inheriting implicit parameters] and [Quantifying over equality constraints] -pickQuantifiablePreds - :: TyVarSet -- Quantifying over these - -> TcThetaType -- Proposed constraints to quantify - -> TcThetaType -- A subset that we can actually quantify --- This function decides whether a particular constraint should be --- quantified over, given the type variables that are being quantified -pickQuantifiablePreds qtvs theta - = let flex_ctxt = True in -- Quantify over non-tyvar constraints, even without - -- -XFlexibleContexts: see #10608, #10351 - -- flex_ctxt <- xoptM Opt_FlexibleContexts - mapMaybe (pick_me flex_ctxt) theta - where - pick_me flex_ctxt pred - = case classifyPredType pred of - - ClassPred cls tys - | Just {} <- isCallStackPred cls tys - -- NEVER infer a CallStack constraint. Otherwise we let - -- the constraints bubble up to be solved from the outer - -- context, or be defaulted when we reach the top-level. - -- See Note [Overview of implicit CallStacks] - -> Nothing - - | isIPClass cls - -> Just pred -- See Note [Inheriting implicit parameters] - - | pick_cls_pred flex_ctxt cls tys - -> Just pred - - EqPred eq_rel ty1 ty2 - | quantify_equality eq_rel ty1 ty2 - , Just (cls, tys) <- boxEqPred eq_rel ty1 ty2 - -- boxEqPred: See Note [Lift equality constraints when quantifying] - , pick_cls_pred flex_ctxt cls tys - -> Just (mkClassPred cls tys) - - IrredPred ty - | tyCoVarsOfType ty `intersectsVarSet` qtvs - -> Just pred - - _ -> Nothing - - - pick_cls_pred flex_ctxt cls tys - = tyCoVarsOfTypes tys `intersectsVarSet` qtvs - && (checkValidClsArgs flex_ctxt cls tys) - -- Only quantify over predicates that checkValidType - -- will pass! See #10351. - - -- See Note [Quantifying over equality constraints] - quantify_equality NomEq ty1 ty2 = quant_fun ty1 || quant_fun ty2 - quantify_equality ReprEq _ _ = True - - quant_fun ty - = case tcSplitTyConApp_maybe ty of - Just (tc, tys) | isTypeFamilyTyCon tc - -> tyCoVarsOfTypes tys `intersectsVarSet` qtvs - _ -> False - +--------------------------- boxEqPred :: EqRel -> Type -> Type -> Maybe (Class, [Type]) -- Given (t1 ~# t2) or (t1 ~R# t2) return the boxed version -- (t1 ~ t2) or (t1 `Coercible` t2) @@ -2013,71 +1942,6 @@ Notice that See also GHC.Tc.TyCl.Utils.checkClassCycles. -Note [Lift equality constraints when quantifying] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We can't quantify over a constraint (t1 ~# t2) because that isn't a -predicate type; see Note [Types for coercions, predicates, and evidence] -in GHC.Core.TyCo.Rep. - -So we have to 'lift' it to (t1 ~ t2). Similarly (~R#) must be lifted -to Coercible. - -This tiresome lifting is the reason that pick_me (in -pickQuantifiablePreds) returns a Maybe rather than a Bool. - -Note [Quantifying over equality constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Should we quantify over an equality constraint (s ~ t)? In general, we don't. -Doing so may simply postpone a type error from the function definition site to -its call site. (At worst, imagine (Int ~ Bool)). - -However, consider this - forall a. (F [a] ~ Int) => blah -Should we quantify over the (F [a] ~ Int)? Perhaps yes, because at the call -site we will know 'a', and perhaps we have instance F [Bool] = Int. -So we *do* quantify over a type-family equality where the arguments mention -the quantified variables. - -Note [Inheriting implicit parameters] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider this: - - f x = (x::Int) + ?y - -where f is *not* a top-level binding. -From the RHS of f we'll get the constraint (?y::Int). -There are two types we might infer for f: - - f :: Int -> Int - -(so we get ?y from the context of f's definition), or - - f :: (?y::Int) => Int -> Int - -At first you might think the first was better, because then -?y behaves like a free variable of the definition, rather than -having to be passed at each call site. But of course, the WHOLE -IDEA is that ?y should be passed at each call site (that's what -dynamic binding means) so we'd better infer the second. - -BOTTOM LINE: when *inferring types* you must quantify over implicit -parameters, *even if* they don't mention the bound type variables. -Reason: because implicit parameters, uniquely, have local instance -declarations. See pickQuantifiablePreds. - -Note [Quantifying over equality constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Should we quantify over an equality constraint (s ~ t)? In general, we don't. -Doing so may simply postpone a type error from the function definition site to -its call site. (At worst, imagine (Int ~ Bool)). - -However, consider this - forall a. (F [a] ~ Int) => blah -Should we quantify over the (F [a] ~ Int). Perhaps yes, because at the call -site we will know 'a', and perhaps we have instance F [Bool] = Int. -So we *do* quantify over a type-family equality where the arguments mention -the quantified variables. - ************************************************************************ * * Classifying types |