diff options
Diffstat (limited to 'compiler/GHC')
-rw-r--r-- | compiler/GHC/Core/Opt/Specialise.hs | 42 | ||||
-rw-r--r-- | compiler/GHC/Core/Predicate.hs | 151 | ||||
-rw-r--r-- | compiler/GHC/Tc/Instance/Class.hs | 7 | ||||
-rw-r--r-- | compiler/GHC/Tc/Module.hs | 13 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver.hs | 2 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Canonical.hs | 4 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Interact.hs | 9 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 3 | ||||
-rw-r--r-- | compiler/GHC/Tc/TyCl/Instance.hs | 3 | ||||
-rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 6 |
10 files changed, 159 insertions, 81 deletions
diff --git a/compiler/GHC/Core/Opt/Specialise.hs b/compiler/GHC/Core/Opt/Specialise.hs index f489ac2eff..8e9e35d208 100644 --- a/compiler/GHC/Core/Opt/Specialise.hs +++ b/compiler/GHC/Core/Opt/Specialise.hs @@ -2514,9 +2514,12 @@ mkCallUDs' env f args -- we decide on a case by case basis if we want to specialise -- on this argument; if so, SpecDict, if not UnspecArg mk_spec_arg arg (Anon InvisArg pred) - | type_determines_value (scaledThing pred) - , interestingDict env arg -- Note [Interesting dictionary arguments] + | not (isIPLikePred (scaledThing pred)) + -- See Note [Type determines value] + , interestingDict env arg + -- See Note [Interesting dictionary arguments] = SpecDict arg + | otherwise = UnspecArg mk_spec_arg _ (Anon VisArg _) @@ -2529,41 +2532,18 @@ mkCallUDs' env f args -- in specImports -- Use 'realIdUnfolding' to ignore the loop-breaker flag! - type_determines_value pred -- See Note [Type determines value] - = case classifyPredType pred of - ClassPred cls _ -> not (isIPClass cls) -- Superclasses can't be IPs - EqPred {} -> True - IrredPred {} -> True -- Things like (D []) where D is a - -- Constraint-ranged family; #7785 - ForAllPred {} -> True - -{- -Note [Type determines value] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Only specialise on non-IP *class* params, because these are the ones -whose *type* determines their *value*. In particular, with implicit -params, the type args *don't* say what the value of the implicit param -is! See #7101. +{- Note [Type determines value] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Only specialise on non-impicit-parameter predicates, because these +are the ones whose *type* determines their *value*. In particular, +with implicit params, the type args *don't* say what the value of the +implicit param is! See #7101. So we treat implicit params just like ordinary arguments for the purposes of specialisation. Note that we still want to specialise functions with implicit params if they have *other* dicts which are class params; see #17930. -One apparent additional complexity involves type families. For -example, consider - type family D (v::*->*) :: Constraint - type instance D [] = () - f :: D v => v Char -> Int -If we see a call (f "foo"), we'll pass a "dictionary" - () |> (g :: () ~ D []) -and it's good to specialise f at this dictionary. - -So the question is: can an implicit parameter "hide inside" a -type-family constraint like (D a). Well, no. We don't allow - type instance D Maybe = ?x:Int -Hence the IrredPred case in type_determines_value. See #7785. - Note [Interesting dictionary arguments] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs index eb31c1be06..89dc9a9e71 100644 --- a/compiler/GHC/Core/Predicate.hs +++ b/compiler/GHC/Core/Predicate.hs @@ -20,9 +20,10 @@ module GHC.Core.Predicate ( mkClassPred, isDictTy, isClassPred, isEqPredClass, isCTupleClass, getClassPredTys, getClassPredTys_maybe, + classMethodTy, classMethodInstTy, -- Implicit parameters - isIPPred, isIPPred_maybe, isIPTyCon, isIPClass, hasIPPred, + isIPLikePred, hasIPSuperClasses, isIPTyCon, isIPClass, -- Evidence variables DictId, isEvVar, isDictId @@ -39,12 +40,10 @@ import GHC.Core.Multiplicity ( scaledThing ) import GHC.Builtin.Names -import GHC.Data.FastString import GHC.Utils.Outputable import GHC.Utils.Misc import GHC.Utils.Panic -import Control.Monad ( guard ) -- | A predicate in the solver. The solver tries to prove Wanted predicates -- from Given ones. @@ -95,6 +94,26 @@ getClassPredTys_maybe ty = case splitTyConApp_maybe ty of Just (tc, tys) | Just clas <- tyConClass_maybe tc -> Just (clas, tys) _ -> Nothing +classMethodTy :: Id -> Type +-- Takes a class selector op :: forall a. C a => meth_ty +-- and returns the type of its method, meth_ty +-- The selector can be a superclass selector, in which case +-- you get back a superclass +classMethodTy sel_id + = funResultTy $ -- meth_ty + dropForAlls $ -- C a => meth_ty + varType sel_id -- forall a. C n => meth_ty + +classMethodInstTy :: Id -> [Type] -> Type +-- Takes a class selector op :: forall a b. C a b => meth_ty +-- and the types [ty1, ty2] at which it is instantiated, +-- returns the instantiated type of its method, meth_ty[t1/a,t2/b] +-- The selector can be a superclass selector, in which case +-- you get back a superclass +classMethodInstTy sel_id arg_tys + = funResultTy $ + piResultTys (varType sel_id) arg_tys + -- --------------------- Equality predicates --------------------------------- -- | A choice of equality relation. This is separate from the type 'Role' @@ -170,7 +189,7 @@ isEqPredClass :: Class -> Bool isEqPredClass cls = cls `hasKey` eqTyConKey || cls `hasKey` heqTyConKey -isClassPred, isEqPred, isEqPrimPred, isIPPred :: PredType -> Bool +isClassPred, isEqPred, isEqPrimPred :: PredType -> Bool isClassPred ty = case tyConAppTyCon_maybe ty of Just tyCon | isClassTyCon tyCon -> True _ -> False @@ -186,9 +205,15 @@ isEqPred ty -- True of (a ~ b) and (a ~~ b) isEqPrimPred ty = isCoVarType ty -- True of (a ~# b) (a ~R# b) -isIPPred ty = case tyConAppTyCon_maybe ty of - Just tc -> isIPTyCon tc - _ -> False +isCTupleClass :: Class -> Bool +isCTupleClass cls = isTupleTyCon (classTyCon cls) + + +{- ********************************************************************* +* * + Implicit parameters +* * +********************************************************************* -} isIPTyCon :: TyCon -> Bool isIPTyCon tc = tc `hasKey` ipClassKey @@ -197,31 +222,103 @@ isIPTyCon tc = tc `hasKey` ipClassKey isIPClass :: Class -> Bool isIPClass cls = cls `hasKey` ipClassKey -isCTupleClass :: Class -> Bool -isCTupleClass cls = isTupleTyCon (classTyCon cls) +isIPLikePred :: Type -> Bool +-- See Note [Local implicit parameters] +isIPLikePred = is_ip_like_pred initIPRecTc -isIPPred_maybe :: Type -> Maybe (FastString, Type) -isIPPred_maybe ty = - do (tc,[t1,t2]) <- splitTyConApp_maybe ty - guard (isIPTyCon tc) - x <- isStrLitTy t1 - return (x,t2) - -hasIPPred :: PredType -> Bool -hasIPPred pred - = case classifyPredType pred of - ClassPred cls tys - | isIPClass cls -> True - | isCTupleClass cls -> any hasIPPred tys - _other -> False -{- -************************************************************************ +is_ip_like_pred :: RecTcChecker -> Type -> Bool +is_ip_like_pred rec_clss ty + | Just (tc, tys) <- splitTyConApp_maybe ty + , Just rec_clss' <- if isTupleTyCon tc -- Tuples never cause recursion + then Just rec_clss + else checkRecTc rec_clss tc + , Just cls <- tyConClass_maybe tc + = isIPClass cls || has_ip_super_classes rec_clss' cls tys + + | otherwise + = False -- Includes things like (D []) where D is + -- a Constraint-ranged family; #7785 + +hasIPSuperClasses :: Class -> [Type] -> Bool +-- See Note [Local implicit parameters] +hasIPSuperClasses = has_ip_super_classes initIPRecTc + +has_ip_super_classes :: RecTcChecker -> Class -> [Type] -> Bool +has_ip_super_classes rec_clss cls tys + = any ip_ish (classSCSelIds cls) + where + -- Check that the type of a superclass determines its value + -- sc_sel_id :: forall a b. C a b -> <superclass type> + ip_ish sc_sel_id = is_ip_like_pred rec_clss $ + classMethodInstTy sc_sel_id tys + +initIPRecTc :: RecTcChecker +initIPRecTc = setRecTcMaxBound 1 initRecTc + +{- Note [Local implicit parameters] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The function isIPLikePred tells if this predicate, or any of its +superclasses, is an implicit parameter. + +Why are implicit parameters special? Unlike normal classes, we can +have local instances for implicit parameters, in the form of + let ?x = True in ... +So in various places we must be careful not to assume that any value +of the right type will do; we must carefully look for the innermost binding. +So isIPLikePred checks whether this is an implicit parameter, or has +a superclass that is an implicit parameter. + +Several wrinkles + +* We must be careful with superclasses, as #18649 showed. Haskell + doesn't allow an implicit parameter as a superclass + class (?x::a) => C a where ... + but with a constraint tuple we might have + (% Eq a, ?x::Int %) + and /its/ superclasses, namely (Eq a) and (?x::Int), /do/ include an + implicit parameter. + + With ConstraintKinds this can apply to /any/ class, e.g. + class sc => C sc where ... + Then (C (?x::Int)) has (?x::Int) as a superclass. So we must + instantiate and check each superclass, one by one, in + hasIPSuperClasses. + +* With -XRecursiveSuperClasses, the superclass hunt can go on forever, + so we need a RecTcChecker to cut it off. + +* Another apparent additional complexity involves type families. For + example, consider + type family D (v::*->*) :: Constraint + type instance D [] = () + f :: D v => v Char -> Int + If we see a call (f "foo"), we'll pass a "dictionary" + () |> (g :: () ~ D []) + and it's good to specialise f at this dictionary. + +So the question is: can an implicit parameter "hide inside" a +type-family constraint like (D a). Well, no. We don't allow + type instance D Maybe = ?x:Int +Hence the umbrella 'otherwise' case in is_ip_like_pred. See #7785. + +Small worries (Sept 20): +* I don't see what stops us having that 'type instance'. Indeed I + think nothing does. +* I'm a little concerned about type variables; such a variable might + be instantiated to an implicit parameter. I don't think this + matters in the cases for which isIPLikePred is used, and it's pretty + obscure anyway. +* The superclass hunt stops when it encounters the same class again, + but in principle we could have the same class, differently instantiated, + and the second time it could have an implicit parameter +I'm going to treat these as problems for another day. They are all exotic. -} + +{- ********************************************************************* * * Evidence variables * * -************************************************************************ --} +********************************************************************* -} isEvVar :: Var -> Bool isEvVar var = isEvVarType (varType var) diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs index 278b63f03c..b66ad2d447 100644 --- a/compiler/GHC/Tc/Instance/Class.hs +++ b/compiler/GHC/Tc/Instance/Class.hs @@ -388,10 +388,9 @@ makeLitDict clas ty et | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty] -- co_dict :: KnownNat n ~ SNat n , [ meth ] <- classMethods clas - , Just tcRep <- tyConAppTyCon_maybe -- SNat - $ funResultTy -- SNat n - $ dropForAlls -- KnownNat n => SNat n - $ idType meth -- forall n. KnownNat n => SNat n + , Just tcRep <- tyConAppTyCon_maybe (classMethodTy meth) + -- If the method type is forall n. KnownNat n => SNat n + -- then tcRep is SNat , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty] -- SNat n ~ Integer , let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep)) diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs index 311f87458f..20538dd230 100644 --- a/compiler/GHC/Tc/Module.hs +++ b/compiler/GHC/Tc/Module.hs @@ -65,9 +65,10 @@ import GHC.Builtin.Types ( unitTy, mkListTy ) import GHC.Driver.Plugins import GHC.Driver.Session import GHC.Hs -import GHC.Iface.Syntax ( ShowSub(..), showToHeader ) -import GHC.Iface.Type ( ShowForAllFlag(..) ) -import GHC.Core.PatSyn( pprPatSynType ) +import GHC.Iface.Syntax ( ShowSub(..), showToHeader ) +import GHC.Iface.Type ( ShowForAllFlag(..) ) +import GHC.Core.PatSyn ( pprPatSynType ) +import GHC.Core.Predicate ( classMethodTy ) import GHC.Builtin.Names import GHC.Builtin.Utils import GHC.Types.Name.Reader @@ -1014,10 +1015,8 @@ checkBootTyCon is_boot tc1 tc2 name2 = idName id2 pname1 = quotes (ppr name1) pname2 = quotes (ppr name2) - (_, rho_ty1) = splitForAllTys (idType id1) - op_ty1 = funResultTy rho_ty1 - (_, rho_ty2) = splitForAllTys (idType id2) - op_ty2 = funResultTy rho_ty2 + op_ty1 = classMethodTy id1 + op_ty2 = classMethodTy id2 eqAT (ATI tc1 def_ats1) (ATI tc2 def_ats2) = checkBootTyCon is_boot tc1 tc2 `andThenCheck` diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index f08622d8f1..ad0ea2ed3c 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -1374,7 +1374,7 @@ growThetaTyVars theta tcvs | otherwise = transCloVarSet mk_next seed_tcvs where seed_tcvs = tcvs `unionVarSet` tyCoVarsOfTypes ips - (ips, non_ips) = partition isIPPred theta + (ips, non_ips) = partition isIPLikePred theta -- See Note [Inheriting implicit parameters] in GHC.Tc.Utils.TcType mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index ce663d9764..557e56f48f 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -29,7 +29,7 @@ import GHC.Core.Multiplicity import GHC.Core.TyCo.Rep -- cleverly decomposes types, good for completeness checking import GHC.Core.Coercion import GHC.Core -import GHC.Types.Id( idType, mkTemplateLocals ) +import GHC.Types.Id( mkTemplateLocals ) import GHC.Core.FamInstEnv ( FamInstEnvs ) import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe ) import GHC.Types.Var @@ -542,7 +542,7 @@ mk_strict_superclasses rec_clss (CtGiven { ctev_evar = evar, ctev_loc = loc }) mk_given_desc sel_id sc_pred ; mk_superclasses rec_clss given_ev tvs theta sc_pred } where - sc_pred = funResultTy (piResultTys (idType sel_id) tys) + sc_pred = classMethodInstTy sel_id tys -- See Note [Nested quantified constraint superclasses] mk_given_desc :: Id -> PredType -> (PredType, EvTerm) diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index adc28d994a..bbdfb56b71 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -566,10 +566,10 @@ solveOneFromTheOther ev_i ev_w ev_id_w = ctEvEvId ev_w different_level_strategy -- Both Given - | isIPPred pred = if lvl_w > lvl_i then KeepWork else KeepInert - | otherwise = if lvl_w > lvl_i then KeepInert else KeepWork + | isIPLikePred pred = if lvl_w > lvl_i then KeepWork else KeepInert + | otherwise = if lvl_w > lvl_i then KeepInert else KeepWork -- See Note [Replacement vs keeping] (the different-level bullet) - -- For the isIPPred case see Note [Shadowing of Implicit Parameters] + -- For the isIPLikePred case see Note [Shadowing of Implicit Parameters] same_level_strategy binds -- Both Given | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i @@ -1071,6 +1071,8 @@ shortCutSolver dflags ev_w ev_i -- programs should typecheck regardless of whether we take this step or -- not. See Note [Shortcut solving] + && not (isIPLikePred (ctEvPred ev_w)) -- Not for implicit parameters (#18627) + && not (xopt LangExt.IncoherentInstances dflags) -- If IncoherentInstances is on then we cannot rely on coherence of proofs -- in order to justify this optimization: The proof provided by the @@ -1079,6 +1081,7 @@ shortCutSolver dflags ev_w ev_i && gopt Opt_SolveConstantDicts dflags -- Enabled by the -fsolve-constant-dicts flag + = do { ev_binds_var <- getTcEvBindsVar ; ev_binds <- ASSERT2( not (isCoEvBindsVar ev_binds_var ), ppr ev_w ) getTcEvBindsMap ev_binds_var diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 7facc96055..aaa1a8428a 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -2527,8 +2527,7 @@ emptyDictMap = emptyTcAppMap findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a findDict m loc cls tys - | isCTupleClass cls - , any hasIPPred tys -- See Note [Tuples hiding implicit parameters] + | hasIPSuperClasses cls tys -- See Note [Tuples hiding implicit parameters] = Nothing | Just {} <- isCallStackPred cls tys diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index 42ec78276e..36d25d0eaf 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -54,6 +54,7 @@ import GHC.Core.Make ( nO_METHOD_BINDING_ERROR_ID ) import GHC.Core.Unfold.Make ( mkInlineUnfoldingWithArity, mkDFunUnfolding ) import GHC.Core.Type import GHC.Core.SimpleOpt +import GHC.Core.Predicate( classMethodInstTy ) import GHC.Tc.Types.Evidence import GHC.Core.TyCon import GHC.Core.Coercion.Axiom @@ -1634,7 +1635,7 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys nO_METHOD_BINDING_ERROR_ID error_msg dflags = L inst_loc (HsLit noExtField (HsStringPrim NoSourceText (unsafeMkByteString (error_string dflags)))) - meth_tau = funResultTy (piResultTys (idType sel_id) inst_tys) + meth_tau = classMethodInstTy sel_id inst_tys error_string dflags = showSDoc dflags (hcat [ppr inst_loc, vbar, ppr sel_id ]) lam_wrapper = mkWpTyLams tyvars <.> mkWpLams dfun_ev_vars diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 357858cf9a..21b6b962d9 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -79,7 +79,7 @@ module GHC.Tc.Utils.TcType ( isFloatingTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy, isIntegerTy, isNaturalTy, isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred, - hasIPPred, isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, + isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy, isPredTy, isTyVarClassPred, isTyVarHead, isInsolubleOccursCheck, checkValidClsArgs, hasTyVarHead, isRigidTy, isAlmostFunctionFree, @@ -141,7 +141,7 @@ module GHC.Tc.Utils.TcType ( mkTyConTy, mkTyVarTy, mkTyVarTys, mkTyCoVarTy, mkTyCoVarTys, - isClassPred, isEqPrimPred, isIPPred, isEqPred, isEqPredClass, + isClassPred, isEqPrimPred, isIPLikePred, isEqPred, isEqPredClass, mkClassPred, tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy, isRuntimeRepVar, isKindLevPoly, @@ -1747,7 +1747,7 @@ pickCapturedPreds pickCapturedPreds qtvs theta = filter captured theta where - captured pred = isIPPred pred || (tyCoVarsOfType pred `intersectsVarSet` qtvs) + captured pred = isIPLikePred pred || (tyCoVarsOfType pred `intersectsVarSet` qtvs) -- Superclasses |