diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2020-12-17 16:53:02 +0000 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2021-01-02 07:34:01 -0500 |
commit | 5650c79e0087fb37311fbe81a2ce6f63b36b91d3 (patch) | |
tree | 6bdc3d6cf1f815a778b539228ac21cb6c4bf66e1 | |
parent | 87bc458de497cdc407c5c32572103a452ee36e4d (diff) | |
download | haskell-5650c79e0087fb37311fbe81a2ce6f63b36b91d3.tar.gz |
Establish invariant (GivenInv)
This patch establishes invariant (GivenInv) from GHC.Tc.Utils.TcType
Note [TcLevel invariants]. (GivenInv) says that unification variables
from level 'n' should not appear in the Givens for level 'n'. See
Note [GivenInv] in teh same module.
This invariant was already very nearly true, but a dark corner of
partial type signatures made it false. The patch re-jigs partial type
signatures a bit to avoid the problem, and documents the invariant
much more thorughly
Fixes #18646 along the way: see Note [Extra-constraints wildcards]
in GHC.Tc.Gen.Bind
I also simplified the interface to tcSimplifyInfer slightly, so that
it /emits/ the residual constraint, rather than /returning/ it.
-rw-r--r-- | compiler/GHC/Tc/Gen/Bind.hs | 47 | ||||
-rw-r--r-- | compiler/GHC/Tc/Gen/Head.hs | 3 | ||||
-rw-r--r-- | compiler/GHC/Tc/Module.hs | 5 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver.hs | 152 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Canonical.hs | 5 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 29 | ||||
-rw-r--r-- | compiler/GHC/Tc/TyCl/PatSyn.hs | 5 | ||||
-rw-r--r-- | compiler/GHC/Tc/Types/Origin.hs | 2 | ||||
-rw-r--r-- | compiler/GHC/Tc/Utils/TcType.hs | 102 | ||||
-rw-r--r-- | testsuite/tests/partial-sigs/should_compile/T14658.hs | 10 | ||||
-rw-r--r-- | testsuite/tests/partial-sigs/should_compile/T14658.stderr | 9 | ||||
-rw-r--r-- | testsuite/tests/partial-sigs/should_compile/T14715.stderr | 2 | ||||
-rw-r--r-- | testsuite/tests/partial-sigs/should_compile/T18646.hs | 16 | ||||
-rw-r--r-- | testsuite/tests/partial-sigs/should_compile/T18646.stderr | 22 | ||||
-rw-r--r-- | testsuite/tests/partial-sigs/should_compile/all.T | 2 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.hs | 15 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.stderr | 15 | ||||
-rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 2 |
18 files changed, 297 insertions, 146 deletions
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs index 178390192f..4528bb5f1b 100644 --- a/compiler/GHC/Tc/Gen/Bind.hs +++ b/compiler/GHC/Tc/Gen/Bind.hs @@ -47,8 +47,8 @@ import GHC.Core.FamInstEnv( normaliseType ) import GHC.Tc.Instance.Family( tcGetFamInstEnvs ) import GHC.Tc.Utils.TcType import GHC.Core.Type (mkStrLitTy, tidyOpenType, mkCastTy) +import GHC.Builtin.Types ( mkBoxedTupleTy ) import GHC.Builtin.Types.Prim -import GHC.Builtin.Types( mkBoxedTupleTy ) import GHC.Types.SourceText import GHC.Types.Id import GHC.Types.Var as Var @@ -729,9 +729,8 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list ; mapM_ (checkOverloadedSig mono) sigs ; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted) - ; (qtvs, givens, ev_binds, residual, insoluble) + ; (qtvs, givens, ev_binds, insoluble) <- simplifyInfer tclvl infer_mode sigs name_taus wanted - ; emitConstraints residual ; let inferred_theta = map evVarPred givens ; exports <- checkNoErrs $ @@ -946,29 +945,30 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs -- so that the Hole constraint we have already emitted -- (in tcHsPartialSigType) can report what filled it in. -- NB: my_theta already includes all the annotated constraints - ; let inferred_diff = [ pred - | pred <- my_theta - , all (not . (`eqType` pred)) annotated_theta ] - ; ctuple <- mk_ctuple inferred_diff + ; diff_theta <- findInferredDiff annotated_theta my_theta ; case tcGetCastedTyVar_maybe wc_var_ty of -- We know that wc_co must have type kind(wc_var) ~ Constraint, as it - -- comes from the checkExpectedKind in GHC.Tc.Gen.HsType.tcAnonWildCardOcc. So, to - -- make the kinds work out, we reverse the cast here. - Just (wc_var, wc_co) -> writeMetaTyVar wc_var (ctuple `mkCastTy` mkTcSymCo wc_co) + -- comes from the checkExpectedKind in GHC.Tc.Gen.HsType.tcAnonWildCardOcc. + -- So, to make the kinds work out, we reverse the cast here. + Just (wc_var, wc_co) -> writeMetaTyVar wc_var (mk_ctuple diff_theta + `mkCastTy` mkTcSymCo wc_co) Nothing -> pprPanic "chooseInferredQuantifiers 1" (ppr wc_var_ty) ; traceTc "completeTheta" $ vcat [ ppr sig - , ppr annotated_theta, ppr inferred_theta - , ppr inferred_diff ] - ; return (free_tvs, my_theta) } - - mk_ctuple preds = return (mkBoxedTupleTy preds) + , text "annotated_theta:" <+> ppr annotated_theta + , text "inferred_theta:" <+> ppr inferred_theta + , text "my_theta:" <+> ppr my_theta + , text "diff_theta:" <+> ppr diff_theta ] + ; return (free_tvs, annotated_theta ++ diff_theta) } + -- Return (annotated_theta ++ diff_theta) + -- See Note [Extra-constraints wildcards] + + mk_ctuple preds = mkBoxedTupleTy preds -- Hack alert! See GHC.Tc.Gen.HsType: -- Note [Extra-constraint holes in partial type signatures] - mk_impedance_match_msg :: MonoBindInfo -> TcType -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc) @@ -1086,6 +1086,21 @@ So we make a test, one per partial signature, to check that the explicitly-quantified type variables have not been unified together. #14449 showed this up. +Note [Extra-constraints wildcards] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this from #18646 + class Foo x where + foo :: x + + bar :: (Foo (), _) => f () + bar = pure foo + +We get [W] Foo (), [W] Applicative f. When we do pickCapturedPreds in +choose_psig_context, we'll discard Foo ()! Usually would not quantify over +such (closed) predicates. So my_theta will be (Applicative f). But we really +do want to quantify over (Foo ()) -- it was speicfied by the programmer. +Solution: always return annotated_theta (user-specified) plus the extra piece +diff_theta. Note [Validity of inferred types] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs index e5806637b0..84e391ee50 100644 --- a/compiler/GHC/Tc/Gen/Head.hs +++ b/compiler/GHC/Tc/Gen/Head.hs @@ -659,9 +659,8 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc }) = ApplyMR | otherwise = NoRestrictions - ; (qtvs, givens, ev_binds, residual, _) + ; (qtvs, givens, ev_binds, _) <- simplifyInfer tclvl infer_mode [sig_inst] [(name, tau)] wanted - ; emitConstraints residual ; tau <- zonkTcType tau ; let inferred_theta = map evVarPred givens diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs index 8f3cec19d0..174055bd01 100644 --- a/compiler/GHC/Tc/Module.hs +++ b/compiler/GHC/Tc/Module.hs @@ -2526,8 +2526,9 @@ tcRnExpr hsc_env mode rdr_expr -- Generalise uniq <- newUnique ; let { fresh_it = itName uniq (getLoc rdr_expr) } ; - (qtvs, dicts, _, residual, _) - <- simplifyInfer tclvl infer_mode + ((qtvs, dicts, _, _), residual) + <- captureConstraints $ + simplifyInfer tclvl infer_mode [] {- No sig vars -} [(fresh_it, res_ty)] lie ; diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index a31b15b285..991708111d 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -1,7 +1,7 @@ {-# LANGUAGE CPP #-} module GHC.Tc.Solver( - simplifyInfer, InferMode(..), + InferMode(..), simplifyInfer, findInferredDiff, growThetaTyVars, simplifyAmbiguityCheck, simplifyDefault, @@ -32,10 +32,10 @@ import GHC.Prelude import GHC.Data.Bag import GHC.Core.Class ( Class, classKey, classTyCon ) import GHC.Driver.Session -import GHC.Types.Id ( idType ) import GHC.Tc.Utils.Instantiate import GHC.Data.List.SetOps import GHC.Types.Name +import GHC.Types.Id( idType ) import GHC.Utils.Outputable import GHC.Builtin.Utils import GHC.Builtin.Names @@ -897,7 +897,6 @@ simplifyInfer :: TcLevel -- Used when generating the constraints -> TcM ([TcTyVar], -- Quantify over these type variables [EvVar], -- ... and these constraints (fully zonked) TcEvBinds, -- ... binding these evidence variables - WantedConstraints, -- Redidual as-yet-unsolved constraints Bool) -- True <=> the residual constraints are insoluble simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds @@ -912,7 +911,7 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds ; dep_vars <- candidateQTyVarsOfTypes (psig_tv_tys ++ psig_theta ++ map snd name_taus) ; qtkvs <- quantifyTyVars dep_vars ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs) - ; return (qtkvs, [], emptyTcEvBinds, emptyWC, False) } + ; return (qtkvs, [], emptyTcEvBinds, False) } | otherwise = do { traceTc "simplifyInfer {" $ vcat @@ -933,18 +932,13 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds -- bindings, so we can't just revert to the input -- constraint. - ; tc_env <- TcM.getEnv - ; ev_binds_var <- TcM.newTcEvBinds - ; psig_theta_vars <- mapM TcM.newEvVar psig_theta + ; ev_binds_var <- TcM.newTcEvBinds + ; psig_evs <- newWanteds AnnOrigin psig_theta ; wanted_transformed_incl_derivs <- setTcLevel rhs_tclvl $ runTcSWithEvBinds ev_binds_var $ - do { let loc = mkGivenLoc rhs_tclvl UnkSkol $ - env_lcl tc_env - psig_givens = mkGivens loc psig_theta_vars - ; _ <- solveSimpleGivens psig_givens - -- See Note [Add signature contexts as givens] - ; solveWanteds wanteds } + solveWanteds (mkSimpleWC psig_evs `andWC` wanteds) + -- psig_evs : see Note [Add signature contexts as givens] -- Find quant_pred_candidates, the predicates that -- we'll consider quantifying over @@ -972,20 +966,10 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds quant_pred_candidates ; bound_theta_vars <- mapM TcM.newEvVar bound_theta - -- We must produce bindings for the psig_theta_vars, because we may have - -- used them in evidence bindings constructed by solveWanteds earlier - -- Easiest way to do this is to emit them as new Wanteds (#14643) - ; ct_loc <- getCtLocM AnnOrigin Nothing - ; let psig_wanted = [ CtWanted { ctev_pred = idType psig_theta_var - , ctev_dest = EvVarDest psig_theta_var - , ctev_nosh = WDeriv - , ctev_loc = ct_loc } - | psig_theta_var <- psig_theta_vars ] - - -- Now construct the residual constraint - ; residual_wanted <- mkResidualConstraints rhs_tclvl ev_binds_var + -- Now emit the residual constraint + ; emitResidualConstraints rhs_tclvl ev_binds_var name_taus co_vars qtvs bound_theta_vars - (wanted_transformed `andWC` mkSimpleWC psig_wanted) + wanted_transformed -- All done! ; traceTc "} simplifyInfer/produced residual implication for quantification" $ @@ -995,30 +979,31 @@ simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds , text "qtvs =" <+> ppr qtvs , text "definite_error =" <+> ppr definite_error ] - ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var - , residual_wanted, definite_error ) } + ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var, definite_error ) } -- NB: bound_theta_vars must be fully zonked where partial_sigs = filter isPartialSig sigs -------------------- -mkResidualConstraints :: TcLevel -> EvBindsVar - -> [(Name, TcTauType)] - -> VarSet -> [TcTyVar] -> [EvVar] - -> WantedConstraints -> TcM WantedConstraints +emitResidualConstraints :: TcLevel -> EvBindsVar + -> [(Name, TcTauType)] + -> VarSet -> [TcTyVar] -> [EvVar] + -> WantedConstraints -> TcM () -- Emit the remaining constraints from the RHS. --- See Note [Emitting the residual implication in simplifyInfer] -mkResidualConstraints rhs_tclvl ev_binds_var +emitResidualConstraints rhs_tclvl ev_binds_var name_taus co_vars qtvs full_theta_vars wanteds | isEmptyWC wanteds - = return wanteds + = return () | otherwise = do { wanted_simple <- TcM.zonkSimples (wc_simple wanteds) ; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars + -- Reason for the partition: + -- see Note [Emitting the residual implication in simplifyInfer] - ; _ <- TcM.promoteTyVarSet (tyCoVarsOfCts outer_simple) +-- Already done by defaultTyVarsAndSimplify +-- ; _ <- TcM.promoteTyVarSet (tyCoVarsOfCts outer_simple) ; let inner_wanted = wanteds { wc_simple = inner_simple } ; implics <- if isEmptyWC inner_wanted @@ -1033,21 +1018,50 @@ mkResidualConstraints rhs_tclvl ev_binds_var , ic_given_eqs = MaybeGivenEqs , ic_info = skol_info } - ; return (emptyWC { wc_simple = outer_simple - , wc_impl = implics })} + ; emitConstraints (emptyWC { wc_simple = outer_simple + , wc_impl = implics }) } where full_theta = map idType full_theta_vars - skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty) - | (name, ty) <- name_taus ] - -- Don't add the quantified variables here, because - -- they are also bound in ic_skols and we want them - -- to be tidied uniformly + skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty) + | (name, ty) <- name_taus ] + -- We don't add the quantified variables here, because they are + -- also bound in ic_skols and we want them to be tidied + -- uniformly. -------------------- ctsPreds :: Cts -> [PredType] ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts , let ev = ctEvidence ct ] +findInferredDiff :: TcThetaType -> TcThetaType -> TcM TcThetaType +findInferredDiff annotated_theta inferred_theta + = pushTcLevelM_ $ + do { lcl_env <- TcM.getLclEnv + ; given_ids <- mapM TcM.newEvVar annotated_theta + ; wanteds <- newWanteds AnnOrigin inferred_theta + ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env + given_cts = mkGivens given_loc given_ids + + ; residual <- runTcSDeriveds $ + do { _ <- solveSimpleGivens given_cts + ; solveSimpleWanteds (listToBag (map mkNonCanonical wanteds)) } + -- NB: There are no meta tyvars fromn this level annotated_theta + -- because we have either promoted them or unified them + -- See `Note [Quantification and partial signatures]` Wrinkle 2 + + ; return (map (box_pred . ctPred) $ + bagToList $ + wc_simple residual) } + where + box_pred :: PredType -> PredType + box_pred pred = case classifyPredType pred of + EqPred rel ty1 ty2 + | Just (cls,tys) <- boxEqPred rel ty1 ty2 + -> mkClassPred cls tys + | otherwise + -> pprPanic "findInferredDiff" (ppr pred) + _other -> pred + {- Note [Emitting the residual implication in simplifyInfer] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider @@ -1074,31 +1088,30 @@ constraints out. (NB: this set of CoVars should be closed-over-kinds.) All rather subtle; see #14584. -Note [Add signature contexts as givens] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Add signature contexts as wanteds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this (#11016): f2 :: (?x :: Int) => _ f2 = ?x + or this - f3 :: a ~ Bool => (a, _) - f3 = (True, False) -or theis - f4 :: (Ord a, _) => a -> Bool - f4 x = x==x + class C a b | a -> b + g :: C p q => p -> q + f3 :: C Int b => _ + f3 = g (3::Int) We'll use plan InferGen because there are holes in the type. But: * For f2 we want to have the (?x :: Int) constraint floating around so that the functional dependencies kick in. Otherwise the occurrence of ?x on the RHS produces constraint (?x :: alpha), and we won't unify alpha:=Int. - * For f3 we want the (a ~ Bool) available to solve the wanted (a ~ Bool) - in the RHS - * For f4 we want to use the (Ord a) in the signature to solve the Eq a - constraint. -Solution: in simplifyInfer, just before simplifying the constraints -gathered from the RHS, add Given constraints for the context of any -type signatures. + * For f3 want the (C Int b) constraint from the partial signature + to meet the (C Int beta) constraint we get from the call to g; again, + fundeps + +Solution: in simplifyInfer, we add the constraints from the signature +as extra Wanteds ************************************************************************ * * @@ -1181,12 +1194,15 @@ decideQuantification infer_mode rhs_tclvl name_taus psigs candidates ; psig_theta <- TcM.zonkTcTypes (concatMap sig_inst_theta psigs) ; let quantifiable_candidates = pickQuantifiablePreds (mkVarSet qtvs) candidates - -- NB: do /not/ run pickQuantifiablePreds over psig_theta, - -- because we always want to quantify over psig_theta, and not - -- drop any of them; e.g. CallStack constraints. c.f #14658 theta = mkMinimalBySCs id $ -- See Note [Minimize by Superclasses] - (psig_theta ++ quantifiable_candidates) + psig_theta ++ quantifiable_candidates + -- NB: add psig_theta back in here, even though it's already + -- part of candidates, because we always want to quantify over + -- psig_theta, and pickQuantifiableCandidates might have + -- dropped some e.g. CallStack constraints. c.f #14658 + -- equalities (a ~ Bool) + -- Remember, this is the theta for the residual constraint ; traceTc "decideQuantification" (vcat [ text "infer_mode:" <+> ppr infer_mode @@ -2123,13 +2139,13 @@ the example for why (partial-sigs/should_compile/T12844): type family Head (xs :: [k]) where Head (x ': xs) = x GHC correctly infers that the extra-constraints wildcard on `bar` -should be (Head rngs ~ '(r, r'), Foo rngs). It then adds this constraint -as a Given on the implication constraint for `bar`. (This implication is -created by mkResidualConstraints in simplifyInfer.) The Hole for -the _ is stored within the implication's WantedConstraints. -When simplifyHoles is called, that constraint is already assumed as -a Given. Simplifying with respect to it turns it into -('(r, r') ~ '(r, r'), Foo rngs), which is disastrous. +should be (Head rngs ~ '(r, r'), Foo rngs). It then adds this +constraint as a Given on the implication constraint for `bar`. (This +implication is emitted by emitResidualConstraints.) The Hole for the _ +is stored within the implication's WantedConstraints. When +simplifyHoles is called, that constraint is already assumed as a +Given. Simplifying with respect to it turns it into ('(r, r') ~ '(r, +r'), Foo rngs), which is disastrous. Furthermore, there is no need to simplify here: extra-constraints wildcards are filled in with the output of the solver, in chooseInferredQuantifiers diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 1a5aacdbe1..4df06c2fca 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -2378,8 +2378,9 @@ Now, clearly we don't want to unify alpha:=Int! Yet at the moment we process [G] alpha[1] ~ Int, we don't have any given-equalities in the inert set, and hence there are no given equalities to make alpha untouchable. -(NB: if it were alpha[2] ~ Int, this argument wouldn't hold. But that -almost never happens, and will never happen at all if we cure #18929.) +NB: if it were alpha[2] ~ Int, this argument wouldn't hold. But that +never happens: invariant (GivenInv) in Note [TcLevel invariants] +in GHC.Tc.Utils.TcType. Simple solution: never unify in Givens! -} diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 2560a8e185..3f7be9a822 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -2032,6 +2032,18 @@ new equality, to maintain the inert-set invariants. inert_solved_funeqs optimistically. But when we lookup we have to take the substitution into account +NB: we could in principle avoid kick-out: + a) When unifying a meta-tyvar from an outer level, because + then the entire implication will be iterated; see + Note [The Unification Level Flag] + + b) For Givens, after a unification. By (GivenInv) in GHC.Tc.Utils.TcType + Note [TcLevel invariants], a Given can't include a meta-tyvar from + its own level, so it falls under (a). Of course, we must still + kick out Givens when adding a new non-unificaiton Given. + +But kicking out more vigorously may lead to earlier unification and fewer +iterations, so we don't take advantage of these possibilities. Note [Rewrite insolubles] ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2296,11 +2308,13 @@ isOuterTyVar :: TcLevel -> TyCoVar -> Bool -- True of a type variable that comes from a -- shallower level than the ambient level (tclvl) isOuterTyVar tclvl tv - | isTyVar tv = tclvl `strictlyDeeperThan` tcTyVarLevel tv - || isPromotableMetaTyVar tv - -- isPromotable: a meta-tv alpha[3] may end up unifying with skolem b[2], - -- so treat it as an "outer" var, even at level 3. - -- This will become redundant after fixing #18929. + | isTyVar tv = ASSERT2( not (isTouchableMetaTyVar tclvl tv), ppr tv <+> ppr tclvl ) + tclvl `strictlyDeeperThan` tcTyVarLevel tv + -- ASSERT: we are dealing with Givens here, and invariant (GivenInv) from + -- Note Note [TcLevel invariants] in GHC.Tc.Utils.TcType ensures that there can't + -- be a touchable meta tyvar. If this wasn't true, you might worry that, + -- at level 3, a meta-tv alpha[3] gets unified with skolem b[2], and thereby + -- becomes "outer" even though its level numbers says it isn't. | otherwise = False -- Coercion variables; doesn't much matter -- | Returns Given constraints that might, @@ -2424,8 +2438,8 @@ Examples: [G] C (F alpha) [W] C a This also might match later. Again, we will need to flatten to - find this out. (Surprised about a metavariable in a Given? See - #18929.) + find this out. (Surprised about a metavariable in a Given? That + can easily happen -- See Note [GivenInv] in GHC.Tc.Utils.TcType.) [G] C (F a) [W] C a @@ -2434,7 +2448,6 @@ Examples: This treatment fixes #18910 and is tested in typecheck/should_compile/InstanceGivenOverlap{,2} - -} removeInertCts :: [Ct] -> InertCans -> InertCans diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs index 0a0b3f3bad..880787447e 100644 --- a/compiler/GHC/Tc/TyCl/PatSyn.hs +++ b/compiler/GHC/Tc/TyCl/PatSyn.hs @@ -166,8 +166,9 @@ tcInferPatSynDecl (PSB { psb_id = lname@(L _ name), psb_args = details -- ex_tvs in its kind k. -- See Note [Type variables whose kind is captured] - ; (univ_tvs, req_dicts, ev_binds, residual, _) - <- simplifyInfer tclvl NoRestrictions [] named_taus wanted + ; ((univ_tvs, req_dicts, ev_binds, _), residual) + <- captureConstraints $ + simplifyInfer tclvl NoRestrictions [] named_taus wanted ; top_ev_binds <- checkNoErrs (simplifyTop residual) ; addTopEvBinds top_ev_binds $ diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs index 0ce4b238d4..91fac134bc 100644 --- a/compiler/GHC/Tc/Types/Origin.hs +++ b/compiler/GHC/Tc/Types/Origin.hs @@ -257,7 +257,7 @@ pprSkolInfo (PatSkol cl mc) = sep [ pprPatSkolInfo cl , text "in" <+> pprMatchContext mc ] pprSkolInfo (InferSkol ids) = hang (text "the inferred type" <> plural ids <+> text "of") 2 (vcat [ ppr name <+> dcolon <+> ppr ty - | (name,ty) <- ids ]) + | (name,ty) <- ids ]) pprSkolInfo (UnifyForAllSkol ty) = text "the type" <+> ppr ty pprSkolInfo (TyConSkol flav name) = text "the" <+> ppr flav <+> text "declaration for" <+> quotes (ppr name) pprSkolInfo (DataConSkol name)= text "the data constructor" <+> quotes (ppr name) diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 942bdd979a..9ec129ef4a 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -596,6 +596,7 @@ Note [TcLevel invariants] (GivenInv) The level number of a unification variable appearing in the 'ic_given' of an implication I should be STRICTLY LESS THAN the ic_tclvl of I + See Note [GivenInv] (WantedInv) The level number of a unification variable appearing in the 'ic_wanted' of an implication I should be @@ -605,6 +606,47 @@ Note [TcLevel invariants] The level of a MetaTyVar also governs its untouchability. See Note [Unification preconditions] in GHC.Tc.Utils.Unify. +Note [TcLevel assignment] +~~~~~~~~~~~~~~~~~~~~~~~~~ +We arrange the TcLevels like this + + 0 Top level + 1 First-level implication constraints + 2 Second-level implication constraints + ...etc... + +Note [GivenInv] +~~~~~~~~~~~~~~~ +Invariant (GivenInv) is not essential, but it is easy to guarantee, and +it is a useful extra piece of structure. It ensures that the Givens of +an implication don't change because of unifications /at the same level/ +caused by Wanteds. (Wanteds can also cause unifications at an outer +level, but that will iterate the entire implication; see GHC.Tc.Solver.Monad +Note [The Unification Level Flag].) + +Givens can certainly contain meta-tyvars from /outer/ levels. E.g. + data T a where + MkT :: Eq a => a -> MkT a + + f x = case x of MkT y -> y && True + +Then we'll infer (x :: T alpha[1]). The Givens from the implication +arising from the pattern match will look like this: + + forall[2] . Eq alpha[1] => (alpha[1] ~ Bool) + +But if we unify alpha (which in this case we will), we'll iterate +the entire implication via Note [The Unification Level Flag] in +GHC.Tc.Solver.Monad. That isn't true of unifications at the /ambient/ +level. + +It would be entirely possible to weaken (GivenInv), to LESS THAN OR +EQUAL TO, but we'd need to think carefully about + - kick-out for Givens + - GHC.Tc.Solver.Monad.isOuterTyVar +But in fact (GivenInv) is automatically true, so we're adhering to +it for now. See #18929. + Note [WantedInv] ~~~~~~~~~~~~~~~~ Why is WantedInv important? Consider this implication, where @@ -615,48 +657,6 @@ the constraint (C alpha[3]) disobeys WantedInv: We can unify alpha:=b in the inner implication, because 'alpha' is touchable; but then 'b' has excaped its scope into the outer implication. - -Note [Skolem escape prevention] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We only unify touchable unification variables. Because of -(WantedInv), there can be no occurrences of the variable further out, -so the unification can't cause the skolems to escape. Example: - data T = forall a. MkT a (a->Int) - f x (MkT v f) = length [v,x] -We decide (x::alpha), and generate an implication like - [1]forall a. (a ~ alpha[0]) -But we must not unify alpha:=a, because the skolem would escape. - -For the cases where we DO want to unify, we rely on floating the -equality. Example (with same T) - g x (MkT v f) = x && True -We decide (x::alpha), and generate an implication like - [1]forall a. (Bool ~ alpha[0]) -We do NOT unify directly, bur rather float out (if the constraint -does not mention 'a') to get - (Bool ~ alpha[0]) /\ [1]forall a.() -and NOW we can unify alpha. - -The same idea of only unifying touchables solves another problem. -Suppose we had - (F Int ~ uf[0]) /\ [1](forall a. C a => F Int ~ beta[1]) -In this example, beta is touchable inside the implication. The -first solveSimpleWanteds step leaves 'uf' un-unified. Then we move inside -the implication where a new constraint - uf ~ beta -emerges. If we (wrongly) spontaneously solved it to get uf := beta, -the whole implication disappears but when we pop out again we are left with -(F Int ~ uf) which will be unified by our final zonking stage and -uf will get unified *once more* to (F Int). - -Note [TcLevel assignment] -~~~~~~~~~~~~~~~~~~~~~~~~~ -We arrange the TcLevels like this - - 0 Top level - 1 First-level implication constraints - 2 Second-level implication constraints - ...etc... -} maxTcLevel :: TcLevel -> TcLevel -> TcLevel @@ -1859,7 +1859,7 @@ mkMinimalBySCs :: forall a. (a -> PredType) -> [a] -> [a] mkMinimalBySCs get_pred xs = go preds_with_scs [] where preds_with_scs :: [PredWithSCs a] - preds_with_scs = [ (pred, pred : transSuperClasses pred, x) + preds_with_scs = [ (pred, implicants pred, x) | x <- xs , let pred = get_pred x ] @@ -1877,6 +1877,8 @@ mkMinimalBySCs get_pred xs = go preds_with_scs [] -- Note [Remove redundant provided dicts] = go work_list min_preds | p `in_cloud` work_list || p `in_cloud` min_preds + -- Why look at work-list too? Suppose work_item is Eq a, + -- and work-list contains Ord a = go work_list min_preds | otherwise = go work_list (work_item : min_preds) @@ -1884,6 +1886,20 @@ mkMinimalBySCs get_pred xs = go preds_with_scs [] in_cloud :: PredType -> [PredWithSCs a] -> Bool in_cloud p ps = or [ p `tcEqType` p' | (_, scs, _) <- ps, p' <- scs ] + implicants pred + = pred : eq_extras pred ++ transSuperClasses pred + + -- Combine (a ~ b) and (b ~ a); no need to have both in one context + -- These can arise when dealing with partial type signatures (e.g. T14715) + eq_extras pred + = case classifyPredType pred of + EqPred r t1 t2 -> [mkPrimEqPredRole (eqRelRole r) t2 t1] + ClassPred cls [k1,k2,t1,t2] + | cls `hasKey` heqTyConKey -> [mkClassPred cls [k2, k1, t2, t1]] + ClassPred cls [k,t1,t2] + | cls `hasKey` eqTyConKey -> [mkClassPred cls [k, t2, t1]] + _ -> [] + transSuperClasses :: PredType -> [PredType] -- (transSuperClasses p) returns (p's superclasses) not including p -- Stop if you encounter the same class again diff --git a/testsuite/tests/partial-sigs/should_compile/T14658.hs b/testsuite/tests/partial-sigs/should_compile/T14658.hs new file mode 100644 index 0000000000..7c985cb180 --- /dev/null +++ b/testsuite/tests/partial-sigs/should_compile/T14658.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE PartialTypeSignatures, ImplicitParams #-} + +module T14658 where + +import GHC.Stack + +-- Test ensures that the final 'f' has a CallStack constraint +-- as specified in the partial type signature +foo :: (?loc :: CallStack, _) => a -> a -> Bool +foo x y = x==y diff --git a/testsuite/tests/partial-sigs/should_compile/T14658.stderr b/testsuite/tests/partial-sigs/should_compile/T14658.stderr new file mode 100644 index 0000000000..7c76ea24e2 --- /dev/null +++ b/testsuite/tests/partial-sigs/should_compile/T14658.stderr @@ -0,0 +1,9 @@ + +T14658.hs:9:28: warning: [-Wpartial-type-signatures (in -Wdefault)] + • Found extra-constraints wildcard standing for ‘Eq a’ + Where: ‘a’ is a rigid type variable bound by + the inferred type of + foo :: (?loc::CallStack, Eq a) => a -> a -> Bool + at T14658.hs:9:1-47 + • In the type signature: + foo :: (?loc :: CallStack, _) => a -> a -> Bool diff --git a/testsuite/tests/partial-sigs/should_compile/T14715.stderr b/testsuite/tests/partial-sigs/should_compile/T14715.stderr index 4d3a668241..286ca25671 100644 --- a/testsuite/tests/partial-sigs/should_compile/T14715.stderr +++ b/testsuite/tests/partial-sigs/should_compile/T14715.stderr @@ -3,7 +3,7 @@ T14715.hs:13:53: warning: [-Wpartial-type-signatures (in -Wdefault)] • Found extra-constraints wildcard standing for ‘Reduce z zq’ Where: ‘z’, ‘zq’ are rigid type variables bound by the inferred type of - bench_mulPublic :: (z ~ LiftOf zq, Reduce z zq) => + bench_mulPublic :: (LiftOf zq ~ z, Reduce z zq) => Cyc zp -> Cyc z -> IO (zp, zq) at T14715.hs:13:27-33 • In the type signature: diff --git a/testsuite/tests/partial-sigs/should_compile/T18646.hs b/testsuite/tests/partial-sigs/should_compile/T18646.hs new file mode 100644 index 0000000000..6cad019853 --- /dev/null +++ b/testsuite/tests/partial-sigs/should_compile/T18646.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE PartialTypeSignatures #-} + +module Foo where + +class Foo x where + foo :: x + +bar :: (Foo (), _) => f () +bar = pure foo + +marie :: (Foo x, _) => f x +marie = pure foo + +anne :: _ => f x +anne = pure foo diff --git a/testsuite/tests/partial-sigs/should_compile/T18646.stderr b/testsuite/tests/partial-sigs/should_compile/T18646.stderr new file mode 100644 index 0000000000..ab5bd90aa5 --- /dev/null +++ b/testsuite/tests/partial-sigs/should_compile/T18646.stderr @@ -0,0 +1,22 @@ + +T18646.hs:9:17: warning: [-Wpartial-type-signatures (in -Wdefault)] + • Found extra-constraints wildcard standing for ‘Applicative f’ + Where: ‘f’ is a rigid type variable bound by + the inferred type of bar :: (Foo (), Applicative f) => f () + at T18646.hs:9:1-26 + • In the type signature: bar :: (Foo (), _) => f () + +T18646.hs:12:18: warning: [-Wpartial-type-signatures (in -Wdefault)] + • Found extra-constraints wildcard standing for ‘Applicative f’ + Where: ‘f’ is a rigid type variable bound by + the inferred type of marie :: (Foo x, Applicative f) => f x + at T18646.hs:12:1-26 + • In the type signature: marie :: (Foo x, _) => f x + +T18646.hs:15:9: warning: [-Wpartial-type-signatures (in -Wdefault)] + • Found extra-constraints wildcard standing for + ‘(Applicative f, Foo x)’ + Where: ‘f’, ‘x’ are rigid type variables bound by + the inferred type of anne :: (Applicative f, Foo x) => f x + at T18646.hs:15:1-16 + • In the type signature: anne :: _ => f x diff --git a/testsuite/tests/partial-sigs/should_compile/all.T b/testsuite/tests/partial-sigs/should_compile/all.T index 8bb939addd..00d051447f 100644 --- a/testsuite/tests/partial-sigs/should_compile/all.T +++ b/testsuite/tests/partial-sigs/should_compile/all.T @@ -97,3 +97,5 @@ test('T16728a', normal, compile, ['']) test('T16728b', normal, compile, ['']) test('T18008', normal, compile, ['']) test('T16762d', normal, compile, ['']) +test('T14658', normal, compile, ['']) +test('T18646', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.hs b/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.hs index 67c475ee23..6b9f019b3c 100644 --- a/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.hs +++ b/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.hs @@ -31,9 +31,23 @@ instance k ~ Bool => HasBoolKind (t :: k) it'sABoolLater :: forall t. HasBoolKind t => Int it'sABoolLater = undefined +-- This test 'g' used to pass, prior to my fix of #18929 +-- But it is /extremely/ delicate, relying on inhibiting constraint +-- solving because of overlapping Givens (couldMatchLater) +-- We are content for it to fail now; see #18929 +-- If it starts to pass in some later universe, that's fine too g :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _ g _ x = it'sABoolNow @t + wob x +{- Notes about 'g' + [G] Q (F (Tagged @Bool t a)) + [W] Q [beta] ==> Q [a] ==>{instance} P a + [W] R beta [a] ==>{instance} beta ~ a +-} + +{- Commenting out these because they all fail + in the same way as 'g' + g2 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _ g2 _ x = wob x + it'sABoolNow @t @@ -42,3 +56,4 @@ g3 _ x = it'sABoolLater @t + wob x g4 :: forall t a. Q (F (Tagged t a)) => Proxy t -> [a] -> _ g4 _ x = wob x + it'sABoolLater @t +-} diff --git a/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.stderr b/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.stderr new file mode 100644 index 0000000000..4f125f6715 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/InstanceGivenOverlap2.stderr @@ -0,0 +1,15 @@ + +InstanceGivenOverlap2.hs:40:1: error: + • Could not deduce (P a) + from the context: Q (F (Tagged t a)) + bound by the inferred type for ‘g’: + forall (t :: Bool) a. Q (F (Tagged t a)) => Proxy t -> [a] -> Int + at InstanceGivenOverlap2.hs:40:1-31 + • When checking that the inferred type + g :: forall {t :: Bool} {a}. + (Q (F (Tagged t a)), P a) => + Proxy t -> [a] -> Int + is as general as its (partial) signature + g :: forall (t :: Bool) a. + Q (F (Tagged t a)) => + Proxy t -> [a] -> Int diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 588c5fc2e4..da663d484b 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -735,7 +735,7 @@ test('T17812', normal, compile, ['']) test('T17186', normal, compile, ['']) test('CbvOverlap', normal, compile, ['']) test('InstanceGivenOverlap', normal, compile, ['']) -test('InstanceGivenOverlap2', normal, compile, ['']) +test('InstanceGivenOverlap2', normal, compile_fail, ['']) test('T19044', normal, compile, ['']) test('T19052', normal, compile, ['']) test('LocalGivenEqs', normal, compile, ['']) |