diff options
| author | Simon Peyton Jones <simonpj@microsoft.com> | 2020-12-08 13:50:42 +0000 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-12-20 20:46:31 -0500 |
| commit | 995a8f9d2bd0e98480a8c60498fdfff1fb8de009 (patch) | |
| tree | 61242096fd19d009128a59fd22a09d66a656fa0d | |
| parent | 35fa0786b6ded2420f0a07446c8e45bff9bb01e0 (diff) | |
| download | haskell-995a8f9d2bd0e98480a8c60498fdfff1fb8de009.tar.gz | |
Kill floatEqualities completely
This patch delivers on #17656, by entirel killing off the complex
floatEqualities mechanism. Previously, floatEqualities would float an
equality out of an implication, so that it could be solved at an outer
level. But now we simply do unification in-place, without floating the
constraint, relying on level numbers to determine untouchability.
There are a number of important new Notes:
* GHC.Tc.Utils.Unify Note [Unification preconditions]
describes the preconditions for unification, including both
skolem-escape and touchability.
* GHC.Tc.Solver.Interact Note [Solve by unification]
describes what we do when we do unify
* GHC.Tc.Solver.Monad Note [The Unification Level Flag]
describes how we control solver iteration under this new scheme
* GHC.Tc.Solver.Monad Note [Tracking Given equalities]
describes how we track when we have Given equalities
* GHC.Tc.Types.Constraint Note [HasGivenEqs]
is a new explanation of the ic_given_eqs field of an implication
A big raft of subtle Notes in Solver, concerning floatEqualities,
disappears.
Main code changes:
* GHC.Tc.Solver.floatEqualities disappears entirely
* GHC.Tc.Solver.Monad: new fields in InertCans, inert_given_eq_lvl
and inert_given_eq, updated by updateGivenEqs
See Note [Tracking Given equalities].
* In exchange for updateGivenEqa, GHC.Tc.Solver.Monad.getHasGivenEqs
is much simpler and more efficient
* I found I could kill of metaTyVarUpdateOK entirely
One test case T14683 showed a 5.1% decrease in compile-time
allocation; and T5631 was down 2.2%. Other changes were small.
Metric Decrease:
T14683
T5631
20 files changed, 998 insertions, 987 deletions
diff --git a/compiler/GHC/Runtime/Heap/Inspect.hs b/compiler/GHC/Runtime/Heap/Inspect.hs index d5758cdfbd..bf6c24d722 100644 --- a/compiler/GHC/Runtime/Heap/Inspect.hs +++ b/compiler/GHC/Runtime/Heap/Inspect.hs @@ -577,7 +577,7 @@ newOpenVar = liftTcM (do { kind <- newOpenTypeKind ~~~~~~~~~~~~~~~~~~~~~~ In the GHCi debugger we use unification variables whose MetaInfo is RuntimeUnkTv. The special property of a RuntimeUnkTv is that it can -unify with a polytype (see GHC.Tc.Utils.Unify.metaTyVarUpdateOK). +unify with a polytype (see GHC.Tc.Utils.Unify.checkTypeEq). If we don't do this `:print <term>` will fail if the type of <term> has nested `forall`s or `=>`s. diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index 71b919b4fd..e7d7ff6c2b 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -21,7 +21,7 @@ import GHC.Tc.Utils.Monad import GHC.Tc.Types.Constraint import GHC.Core.Predicate import GHC.Tc.Utils.TcMType -import GHC.Tc.Utils.Unify( occCheckForErrors, MetaTyVarUpdateResult(..) ) +import GHC.Tc.Utils.Unify( occCheckForErrors, CheckTyEqResult(..) ) import GHC.Tc.Utils.Env( tcInitTidyEnv ) import GHC.Tc.Utils.TcType import GHC.Tc.Types.Origin @@ -1482,7 +1482,7 @@ mkTyVarEqErr' dflags ctxt report ct tv1 ty2 , report ] - | MTVU_Occurs <- occ_check_expand + | CTE_Occurs <- occ_check_expand -- We report an "occurs check" even for a ~ F t a, where F is a type -- function; it's not insoluble (because in principle F could reduce) -- but we have certainly been unable to solve it @@ -1503,7 +1503,7 @@ mkTyVarEqErr' dflags ctxt report ct tv1 ty2 ; mkErrorMsgFromCt ctxt ct $ mconcat [headline_msg, extra2, extra3, report] } - | MTVU_Bad <- occ_check_expand + | CTE_Bad <- occ_check_expand = do { let msg = vcat [ text "Cannot instantiate unification variable" <+> quotes (ppr tv1) , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2) ] diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs index 5f17621b62..83f8cc567d 100644 --- a/compiler/GHC/Tc/Gen/App.hs +++ b/compiler/GHC/Tc/Gen/App.hs @@ -955,7 +955,7 @@ That is the entire point of qlUnify! Wrinkles: * We must not make an occurs-check; we use occCheckExpand for that. -* metaTyVarUpdateOK also checks for various other things, including +* checkTypeEq also checks for various other things, including - foralls, and predicate types (which we want to allow here) - type families (relates to a very specific and exotic performance question, that is unlikely to bite here) diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index 5f92272242..ecd4e82304 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -312,7 +312,7 @@ Note [Promotion in signatures] If an unsolved metavariable in a signature is not generalized (because we're not generalizing the construct -- e.g., pattern sig -- or because the metavars are constrained -- see kindGeneralizeSome) -we need to promote to maintain (WantedTvInv) of Note [TcLevel and untouchable type variables] +we need to promote to maintain (WantedTvInv) of Note [TcLevel invariants] in GHC.Tc.Utils.TcType. Note that promotion is identical in effect to generalizing and the reinstantiating with a fresh metavariable at the current level. So in some sense, we generalize *all* variables, but then re-instantiate @@ -330,7 +330,7 @@ the pattern signature (which is not kind-generalized). When we are checking the *body* of foo, though, we need to unify the type of x with the argument type of bar. At this point, the ambient TcLevel is 1, and spotting a matavariable with level 2 would violate the (WantedTvInv) invariant of -Note [TcLevel and untouchable type variables]. So, instead of kind-generalizing, +Note [TcLevel invariants]. So, instead of kind-generalizing, we promote the metavariable to level 1. This is all done in kindGeneralizeNone. -} diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index 8b21b72768..a31b15b285 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -264,7 +264,7 @@ floatKindEqualities wc = float_wc emptyVarSet wc = Nothing -- A short cut /plus/ we must keep track of IC_BadTelescope | otherwise = do { (simples, holes) <- float_wc new_trapping_tvs wanted - ; when (not (isEmptyBag simples) && given_eqs /= NoGivenEqs) $ + ; when (not (isEmptyBag simples) && given_eqs == MaybeGivenEqs) $ Nothing -- If there are some constraints to float out, but we can't -- because we don't float out past local equalities @@ -1282,7 +1282,8 @@ decideMonoTyVars infer_mode name_taus psigs candidates mr_msg ; traceTc "decideMonoTyVars" $ vcat - [ text "mono_tvs0 =" <+> ppr mono_tvs0 + [ text "infer_mode =" <+> ppr infer_mode + , text "mono_tvs0 =" <+> ppr mono_tvs0 , text "no_quant =" <+> ppr no_quant , text "maybe_quant =" <+> ppr maybe_quant , text "eq_constraints =" <+> ppr eq_constraints @@ -1325,7 +1326,7 @@ defaultTyVarsAndSimplify :: TcLevel -- and re-simplify in case the defaulting allows further simplification defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates = do { -- Promote any tyvars that we cannot generalise - -- See Note [Promote momomorphic tyvars] + -- See Note [Promote monomorphic tyvars] ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs) ; any_promoted <- promoteTyVarSet mono_tvs @@ -1405,7 +1406,10 @@ decideQuantifiedTyVars name_taus psigs candidates dvs_plus = dv { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs } ; traceTc "decideQuantifiedTyVars" (vcat - [ text "candidates =" <+> ppr candidates + [ text "tau_tys =" <+> ppr tau_tys + , text "candidates =" <+> ppr candidates + , text "cand_kvs =" <+> ppr cand_kvs + , text "cand_tvs =" <+> ppr cand_tvs , text "tau_tys =" <+> ppr tau_tys , text "seed_tys =" <+> ppr seed_tys , text "seed_tcvs =" <+> ppr (tyCoVarsOfTypes seed_tys) @@ -1434,7 +1438,7 @@ growThetaTyVars theta tcvs pred_tcvs = tyCoVarsOfType pred -{- Note [Promote momomorphic tyvars] +{- Note [Promote monomorphic tyvars] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Promote any type variables that are free in the environment. Eg f :: forall qtvs. bound_theta => zonked_tau @@ -1448,7 +1452,7 @@ we don't quantify over beta (since it is fixed by envt) so we must promote it! The inferred type is just f :: beta -> beta -NB: promoteTyVar ignores coercion variables +NB: promoteTyVarSet ignores coercion variables Note [Quantification and partial signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1660,22 +1664,14 @@ solveWantedsAndDrop wanted solveWanteds :: WantedConstraints -> TcS WantedConstraints -- so that the inert set doesn't mindlessly propagate. -- NB: wc_simples may be wanted /or/ derived now -solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics, wc_holes = holes }) +solveWanteds wc@(WC { wc_holes = holes }) = do { cur_lvl <- TcS.getTcLevel ; traceTcS "solveWanteds {" $ vcat [ text "Level =" <+> ppr cur_lvl , ppr wc ] - ; wc1 <- solveSimpleWanteds simples - -- Any insoluble constraints are in 'simples' and so get rewritten - -- See Note [Rewrite insolubles] in GHC.Tc.Solver.Monad - - ; (floated_eqs, implics2) <- solveNestedImplications $ - implics `unionBags` wc_impl wc1 - - ; dflags <- getDynFlags - ; solved_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs - (wc1 { wc_impl = implics2 }) + ; dflags <- getDynFlags + ; solved_wc <- simplify_loop 0 (solverIterations dflags) True wc ; holes' <- simplifyHoles holes ; let final_wc = solved_wc { wc_holes = holes' } @@ -1688,9 +1684,44 @@ solveWanteds wc@(WC { wc_simple = simples, wc_impl = implics, wc_holes = holes } ; return final_wc } -simpl_loop :: Int -> IntWithInf -> Cts - -> WantedConstraints -> TcS WantedConstraints -simpl_loop n limit floated_eqs wc@(WC { wc_simple = simples }) +simplify_loop :: Int -> IntWithInf -> Bool + -> WantedConstraints -> TcS WantedConstraints +-- Do a round of solving, and call maybe_simplify_again to iterate +-- The 'definitely_redo_implications' flags is False if the only reason we +-- are iterating is that we have added some new Derived superclasses (from Wanteds) +-- hoping for fundeps to help us; see Note [Superclass iteration] +-- +-- Does not affect wc_holes at all; reason: wc_holes never affects anything +-- else, so we do them once, at the end in solveWanteds +simplify_loop n limit definitely_redo_implications + wc@(WC { wc_simple = simples, wc_impl = implics }) + = do { csTraceTcS $ + text "simplify_loop iteration=" <> int n + <+> (parens $ hsep [ text "definitely_redo =" <+> ppr definitely_redo_implications <> comma + , int (lengthBag simples) <+> text "simples to solve" ]) + ; traceTcS "simplify_loop: wc =" (ppr wc) + + ; (unifs1, wc1) <- reportUnifications $ -- See Note [Superclass iteration] + solveSimpleWanteds simples + -- Any insoluble constraints are in 'simples' and so get rewritten + -- See Note [Rewrite insolubles] in GHC.Tc.Solver.Monad + + ; wc2 <- if not definitely_redo_implications -- See Note [Superclass iteration] + && unifs1 == 0 -- for this conditional + && isEmptyBag (wc_impl wc1) + then return (wc { wc_simple = wc_simple wc1 }) -- Short cut + else do { implics2 <- solveNestedImplications $ + implics `unionBags` (wc_impl wc1) + ; return (wc { wc_simple = wc_simple wc1 + , wc_impl = implics2 }) } + + ; unif_happened <- resetUnificationFlag + -- Note [The Unification Level Flag] in GHC.Tc.Solver.Monad + ; maybe_simplify_again (n+1) limit unif_happened wc2 } + +maybe_simplify_again :: Int -> IntWithInf -> Bool + -> WantedConstraints -> TcS WantedConstraints +maybe_simplify_again n limit unif_happened wc@(WC { wc_simple = simples }) | n `intGtLimit` limit = do { -- Add an error (not a warning) if we blow the limit, -- Typically if we blow the limit we are going to report some other error @@ -1699,17 +1730,12 @@ simpl_loop n limit floated_eqs wc@(WC { wc_simple = simples }) addErrTcS (hang (text "solveWanteds: too many iterations" <+> parens (text "limit =" <+> ppr limit)) 2 (vcat [ text "Unsolved:" <+> ppr wc - , ppUnless (isEmptyBag floated_eqs) $ - text "Floated equalities:" <+> ppr floated_eqs , text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit" ])) ; return wc } - | not (isEmptyBag floated_eqs) - = simplify_again n limit True (wc { wc_simple = floated_eqs `unionBags` simples }) - -- Put floated_eqs first so they get solved first - -- NB: the floated_eqs may include /derived/ equalities - -- arising from fundeps inside an implication + | unif_happened + = simplify_loop n limit True wc | superClassesMightHelp wc = -- We still have unsolved goals, and apparently no way to solve them, @@ -1722,82 +1748,65 @@ simpl_loop n limit floated_eqs wc@(WC { wc_simple = simples }) do { new_given <- makeSuperClasses pending_given ; new_wanted <- makeSuperClasses pending_wanted ; solveSimpleGivens new_given -- Add the new Givens to the inert set - ; simplify_again n limit (null pending_given) + ; simplify_loop n limit (not (null pending_given)) $ wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } } + -- (not (null pending_given)): see Note [Superclass iteration] | otherwise = return wc -simplify_again :: Int -> IntWithInf -> Bool - -> WantedConstraints -> TcS WantedConstraints --- We have definitely decided to have another go at solving --- the wanted constraints (we have tried at least once already -simplify_again n limit no_new_given_scs - wc@(WC { wc_simple = simples, wc_impl = implics }) - = do { csTraceTcS $ - text "simpl_loop iteration=" <> int n - <+> (parens $ hsep [ text "no new given superclasses =" <+> ppr no_new_given_scs <> comma - , int (lengthBag simples) <+> text "simples to solve" ]) - ; traceTcS "simpl_loop: wc =" (ppr wc) - - ; (unifs1, wc1) <- reportUnifications $ - solveSimpleWanteds $ - simples - - -- See Note [Cutting off simpl_loop] - -- We have already tried to solve the nested implications once - -- Try again only if we have unified some meta-variables - -- (which is a bit like adding more givens), or we have some - -- new Given superclasses - ; let new_implics = wc_impl wc1 - ; if unifs1 == 0 && - no_new_given_scs && - isEmptyBag new_implics - - then -- Do not even try to solve the implications - simpl_loop (n+1) limit emptyBag (wc1 { wc_impl = implics }) - - else -- Try to solve the implications - do { (floated_eqs2, implics2) <- solveNestedImplications $ - implics `unionBags` new_implics - ; simpl_loop (n+1) limit floated_eqs2 (wc1 { wc_impl = implics2 }) - } } +{- Note [Superclass iteration] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this implication constraint + forall a. + [W] d: C Int beta + forall b. blah +where + class D a b | a -> b + class D a b => C a b +We will expand d's superclasses, giving [D] D Int beta, in the hope of geting +fundeps to unify beta. Doing so is usually fruitless (no useful fundeps), +and if so it seems a pity to waste time iterating the implications (forall b. blah) +(If we add new Given superclasses it's a different matter: it's really worth looking +at the implications.) + +Hence the definitely_redo_implications flag to simplify_loop. It's usually +True, but False in the case where the only reason to iterate is new Derived +superclasses. In that case we check whether the new Deriveds actually led to +any new unifications, and iterate the implications only if so. +-} solveNestedImplications :: Bag Implication - -> TcS (Cts, Bag Implication) + -> TcS (Bag Implication) -- Precondition: the TcS inerts may contain unsolved simples which have -- to be converted to givens before we go inside a nested implication. solveNestedImplications implics | isEmptyBag implics - = return (emptyBag, emptyBag) + = return (emptyBag) | otherwise = do { traceTcS "solveNestedImplications starting {" empty - ; (floated_eqs_s, unsolved_implics) <- mapAndUnzipBagM solveImplication implics - ; let floated_eqs = concatBag floated_eqs_s + ; unsolved_implics <- mapBagM solveImplication implics -- ... and we are back in the original TcS inerts -- Notice that the original includes the _insoluble_simples so it was safe to ignore -- them in the beginning of this function. ; traceTcS "solveNestedImplications end }" $ - vcat [ text "all floated_eqs =" <+> ppr floated_eqs - , text "unsolved_implics =" <+> ppr unsolved_implics ] + vcat [ text "unsolved_implics =" <+> ppr unsolved_implics ] - ; return (floated_eqs, catBagMaybes unsolved_implics) } + ; return (catBagMaybes unsolved_implics) } solveImplication :: Implication -- Wanted - -> TcS (Cts, -- All wanted or derived floated equalities: var = type - Maybe Implication) -- Simplified implication (empty or singleton) + -> TcS (Maybe Implication) -- Simplified implication (empty or singleton) -- Precondition: The TcS monad contains an empty worklist and given-only inerts -- which after trying to solve this implication we must restore to their original value solveImplication imp@(Implic { ic_tclvl = tclvl , ic_binds = ev_binds_var - , ic_skols = skols , ic_given = given_ids , ic_wanted = wanteds , ic_info = info , ic_status = status }) | isSolvedStatus status - = return (emptyCts, Just imp) -- Do nothing + = return (Just imp) -- Do nothing | otherwise -- Even for IC_Insoluble it is worth doing more work -- The insoluble stuff might be in one sub-implication @@ -1819,7 +1828,7 @@ solveImplication imp@(Implic { ic_tclvl = tclvl ; residual_wanted <- solveWanteds wanteds -- solveWanteds, *not* solveWantedsAndDrop, because -- we want to retain derived equalities so we can float - -- them out in floatEqualities + -- them out in floatEqualities. ; (has_eqs, given_insols) <- getHasGivenEqs tclvl -- Call getHasGivenEqs /after/ solveWanteds, because @@ -1828,10 +1837,6 @@ solveImplication imp@(Implic { ic_tclvl = tclvl ; return (has_eqs, given_insols, residual_wanted) } - ; (floated_eqs, residual_wanted) - <- floatEqualities skols given_ids ev_binds_var - has_given_eqs residual_wanted - ; traceTcS "solveImplication 2" (ppr given_insols $$ ppr residual_wanted) ; let final_wanted = residual_wanted `addInsols` given_insols @@ -1845,15 +1850,14 @@ solveImplication imp@(Implic { ic_tclvl = tclvl ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var ; traceTcS "solveImplication end }" $ vcat [ text "has_given_eqs =" <+> ppr has_given_eqs - , text "floated_eqs =" <+> ppr floated_eqs , text "res_implic =" <+> ppr res_implic , text "implication evbinds =" <+> ppr (evBindMapBinds evbinds) , text "implication tvcs =" <+> ppr tcvs ] - ; return (floated_eqs, res_implic) } + ; return res_implic } -- TcLevels must be strictly increasing (see (ImplicInv) in - -- Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType), + -- Note [TcLevel invariants] in GHC.Tc.Utils.TcType), -- and in fact I think they should always increase one level at a time. -- Though sensible, this check causes lots of testsuite failures. It is @@ -2237,49 +2241,8 @@ Consider (see #9939) We report (Eq a) as redundant, whereas actually (Ord a) is. But it's really not easy to detect that! - -Note [Cutting off simpl_loop] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -It is very important not to iterate in simpl_loop unless there is a chance -of progress. #8474 is a classic example: - - * There's a deeply-nested chain of implication constraints. - ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int - - * From the innermost one we get a [D] alpha ~ Int, - but alpha is untouchable until we get out to the outermost one - - * We float [D] alpha~Int out (it is in floated_eqs), but since alpha - is untouchable, the solveInteract in simpl_loop makes no progress - - * So there is no point in attempting to re-solve - ?yn:betan => [W] ?x:Int - via solveNestedImplications, because we'll just get the - same [D] again - - * If we *do* re-solve, we'll get an infinite loop. It is cut off by - the fixed bound of 10, but solving the next takes 10*10*...*10 (ie - exponentially many) iterations! - -Conclusion: we should call solveNestedImplications only if we did -some unification in solveSimpleWanteds; because that's the only way -we'll get more Givens (a unification is like adding a Given) to -allow the implication to make progress. -} -promoteTyVarTcS :: TcTyVar -> TcS () --- When we float a constraint out of an implication we must restore --- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType --- See Note [Promoting unification variables] --- We don't just call promoteTyVar because we want to use unifyTyVar, --- not writeMetaTyVar -promoteTyVarTcS tv - = do { tclvl <- TcS.getTcLevel - ; when (isFloatedTouchableMetaTyVar tclvl tv) $ - do { cloned_tv <- TcS.cloneMetaTyVar tv - ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl - ; unifyTyVar tv (mkTyVarTy rhs_tv) } } - -- | Like 'defaultTyVar', but in the TcS monad. defaultTyVarTcS :: TcTyVar -> TcS Bool defaultTyVarTcS the_tv @@ -2314,7 +2277,7 @@ approximateWC float_past_equalities wc concatMapBag (float_implic trapping_tvs) implics float_implic :: TcTyCoVarSet -> Implication -> Cts float_implic trapping_tvs imp - | float_past_equalities || ic_given_eqs imp == NoGivenEqs + | float_past_equalities || ic_given_eqs imp /= MaybeGivenEqs = float_wc new_trapping_tvs (ic_wanted imp) | otherwise -- Take care with equalities = emptyCts -- See (1) under Note [ApproximateWC] @@ -2414,7 +2377,7 @@ approximateWC to produce a list of candidate constraints. Then we MUST a) Promote any meta-tyvars that have been floated out by approximateWC, to restore invariant (WantedInv) described in - Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType. + Note [TcLevel invariants] in GHC.Tc.Utils.TcType. b) Default the kind of any meta-tyvars that are not mentioned in in the environment. @@ -2430,8 +2393,7 @@ Note [Promoting unification variables] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When we float an equality out of an implication we must "promote" free unification variables of the equality, in order to maintain Invariant -(WantedInv) from Note [TcLevel and untouchable type variables] in -TcType. for the leftover implication. +(WantedInv) from Note [TcLevel invariants] in GHC.Tc.Types.TcType. This is absolutely necessary. Consider the following example. We start with two implications and a class with a functional dependency. @@ -2468,276 +2430,6 @@ beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs: in (g1 '3', g2 undefined) - -********************************************************************************* -* * -* Floating equalities * -* * -********************************************************************************* - -Note [Float Equalities out of Implications] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -For ordinary pattern matches (including existentials) we float -equalities out of implications, for instance: - data T where - MkT :: Eq a => a -> T - f x y = case x of MkT _ -> (y::Int) -We get the implication constraint (x::T) (y::alpha): - forall a. [untouchable=alpha] Eq a => alpha ~ Int -We want to float out the equality into a scope where alpha is no -longer untouchable, to solve the implication! - -But we cannot float equalities out of implications whose givens may -yield or contain equalities: - - data T a where - T1 :: T Int - T2 :: T Bool - T3 :: T a - - h :: T a -> a -> Int - - f x y = case x of - T1 -> y::Int - T2 -> y::Bool - T3 -> h x y - -We generate constraint, for (x::T alpha) and (y :: beta): - [untouchables = beta] (alpha ~ Int => beta ~ Int) -- From 1st branch - [untouchables = beta] (alpha ~ Bool => beta ~ Bool) -- From 2nd branch - (alpha ~ beta) -- From 3rd branch - -If we float the equality (beta ~ Int) outside of the first implication and -the equality (beta ~ Bool) out of the second we get an insoluble constraint. -But if we just leave them inside the implications, we unify alpha := beta and -solve everything. - -Principle: - We do not want to float equalities out which may - need the given *evidence* to become soluble. - -Consequence: classes with functional dependencies don't matter (since there is -no evidence for a fundep equality), but equality superclasses do matter (since -they carry evidence). --} - -floatEqualities :: [TcTyVar] -> [EvId] -> EvBindsVar -> HasGivenEqs - -> WantedConstraints - -> TcS (Cts, WantedConstraints) --- Main idea: see Note [Float Equalities out of Implications] --- --- Precondition: the wc_simple of the incoming WantedConstraints are --- fully zonked, so that we can see their free variables --- --- Postcondition: The returned floated constraints (Cts) are only --- Wanted or Derived --- --- Also performs some unifications (via promoteTyVar), adding to --- monadically-carried ty_binds. These will be used when processing --- floated_eqs later --- --- Subtleties: Note [Float equalities from under a skolem binding] --- Note [Skolem escape] --- Note [What prevents a constraint from floating] -floatEqualities skols given_ids ev_binds_var has_given_eqs - wanteds@(WC { wc_simple = simples }) - | MaybeGivenEqs <- has_given_eqs -- There are some given equalities, so don't float - = return (emptyBag, wanteds) -- Note [Float Equalities out of Implications] - - | otherwise - = do { -- First zonk: the inert set (from whence they came) is not - -- necessarily fully zonked; equalities are not kicked out - -- if a unification cannot make progress. See Note - -- [inert_eqs: the inert equalities] in GHC.Tc.Solver.Monad, which - -- describes how the inert set might not actually be inert. - simples <- TcS.zonkSimples simples - ; binds <- TcS.getTcEvBindsMap ev_binds_var - - -- Now we can pick the ones to float - -- The constraints are de-canonicalised - ; let (candidate_eqs, no_float_cts) = partitionBag is_float_eq_candidate simples - - seed_skols = mkVarSet skols `unionVarSet` - mkVarSet given_ids `unionVarSet` - foldr add_non_flt_ct emptyVarSet no_float_cts `unionVarSet` - evBindMapToVarSet binds - -- seed_skols: See Note [What prevents a constraint from floating] (1,2,3) - -- Include the EvIds of any non-floating constraints - - extended_skols = transCloVarSet (add_captured_ev_ids candidate_eqs) seed_skols - -- extended_skols contains the EvIds of all the trapped constraints - -- See Note [What prevents a constraint from floating] (3) - - (flt_eqs, no_flt_eqs) = partitionBag (is_floatable extended_skols) - candidate_eqs - - remaining_simples = no_float_cts `andCts` no_flt_eqs - - -- Promote any unification variables mentioned in the floated equalities - -- See Note [Promoting unification variables] - ; mapM_ promoteTyVarTcS (tyCoVarsOfCtsList flt_eqs) - - ; traceTcS "floatEqualities" (vcat [ text "Skols =" <+> ppr skols - , text "Extended skols =" <+> ppr extended_skols - , text "Simples =" <+> ppr simples - , text "Candidate eqs =" <+> ppr candidate_eqs - , text "Floated eqs =" <+> ppr flt_eqs]) - ; return ( flt_eqs, wanteds { wc_simple = remaining_simples } ) } - - where - add_non_flt_ct :: Ct -> VarSet -> VarSet - add_non_flt_ct ct acc | isDerivedCt ct = acc - | otherwise = extendVarSet acc (ctEvId ct) - - is_floatable :: VarSet -> Ct -> Bool - is_floatable skols ct - | isDerivedCt ct = tyCoVarsOfCt ct `disjointVarSet` skols - | otherwise = not (ctEvId ct `elemVarSet` skols) - - add_captured_ev_ids :: Cts -> VarSet -> VarSet - add_captured_ev_ids cts skols = foldr extra_skol emptyVarSet cts - where - extra_skol ct acc - | isDerivedCt ct = acc - | tyCoVarsOfCt ct `intersectsVarSet` skols = extendVarSet acc (ctEvId ct) - | otherwise = acc - - -- Identify which equalities are candidates for floating - -- Float out alpha ~ ty which might be unified outside - -- See Note [Which equalities to float] - is_float_eq_candidate ct - | pred <- ctPred ct - , EqPred NomEq ty1 ty2 <- classifyPredType pred - , case ct of - CIrredCan {} -> False -- See Note [Do not float blocked constraints] - _ -> True -- See #18855 - = float_eq ty1 ty2 || float_eq ty2 ty1 - | otherwise - = False - - float_eq ty1 ty2 - = case getTyVar_maybe ty1 of - Just tv1 -> isMetaTyVar tv1 - && (not (isTyVarTyVar tv1) || isTyVarTy ty2) - Nothing -> False - -{- Note [Do not float blocked constraints] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -As #18855 showed, we must not float an equality that is blocked. -Consider - forall a[4]. [W] co1: alpha[4] ~ Maybe (a[4] |> bco) - [W] co2: alpha[4] ~ Maybe (beta[4] |> bco]) - [W] bco: kappa[2] ~ Type - -Now co1, co2 are blocked by bco. We will eventually float out bco -and solve it at level 2. But the danger is that we will *also* -float out co2, and that is bad bad bad. Because we'll promote alpha -and beta to level 2, and then fail to unify the promoted beta -with the skolem a[4]. - -Solution: don't float out blocked equalities. Remember: we only want -to float out if we can solve; see Note [Which equalities to float]. - -(Future plan: kill floating altogether.) - -Note [Float equalities from under a skolem binding] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Which of the simple equalities can we float out? Obviously, only -ones that don't mention the skolem-bound variables. But that is -over-eager. Consider - [2] forall a. F a beta[1] ~ gamma[2], G beta[1] gamma[2] ~ Int -The second constraint doesn't mention 'a'. But if we float it, -we'll promote gamma[2] to gamma'[1]. Now suppose that we learn that -beta := Bool, and F a Bool = a, and G Bool _ = Int. Then we'll -we left with the constraint - [2] forall a. a ~ gamma'[1] -which is insoluble because gamma became untouchable. - -Solution: float only constraints that stand a jolly good chance of -being soluble simply by being floated, namely ones of form - a ~ ty -where 'a' is a currently-untouchable unification variable, but may -become touchable by being floated (perhaps by more than one level). - -We had a very complicated rule previously, but this is nice and -simple. (To see the notes, look at this Note in a version of -GHC.Tc.Solver prior to Oct 2014). - -Note [Which equalities to float] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Which equalities should we float? We want to float ones where there -is a decent chance that floating outwards will allow unification to -happen. In particular, float out equalities that are: - -* Of form (alpha ~# ty) or (ty ~# alpha), where - * alpha is a meta-tyvar. - * And 'alpha' is not a TyVarTv with 'ty' being a non-tyvar. In that - case, floating out won't help either, and it may affect grouping - of error messages. - - NB: generally we won't see (ty ~ alpha), with alpha on the right because - of Note [Unification variables on the left] in GHC.Tc.Utils.Unify, - but if we have (F tys ~ alpha) and alpha is untouchable, then it will - appear on the right. Example T4494. - -* Nominal. No point in floating (alpha ~R# ty), because we do not - unify representational equalities even if alpha is touchable. - See Note [Do not unify representational equalities] in GHC.Tc.Solver.Interact. - -Note [Skolem escape] -~~~~~~~~~~~~~~~~~~~~ -You might worry about skolem escape with all this floating. -For example, consider - [2] forall a. (a ~ F beta[2] delta, - Maybe beta[2] ~ gamma[1]) - -The (Maybe beta ~ gamma) doesn't mention 'a', so we float it, and -solve with gamma := beta. But what if later delta:=Int, and - F b Int = b. -Then we'd get a ~ beta[2], and solve to get beta:=a, and now the -skolem has escaped! - -But it's ok: when we float (Maybe beta[2] ~ gamma[1]), we promote beta[2] -to beta[1], and that means the (a ~ beta[1]) will be stuck, as it should be. - -Note [What prevents a constraint from floating] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -What /prevents/ a constraint from floating? If it mentions one of the -"bound variables of the implication". What are they? - -The "bound variables of the implication" are - - 1. The skolem type variables `ic_skols` - - 2. The "given" evidence variables `ic_given`. Example: - forall a. (co :: t1 ~# t2) => [W] co2 : (a ~# b |> co) - Here 'co' is bound - - 3. The binders of all evidence bindings in `ic_binds`. Example - forall a. (d :: t1 ~ t2) - EvBinds { (co :: t1 ~# t2) = superclass-sel d } - => [W] co2 : (a ~# b |> co) - Here `co` is gotten by superclass selection from `d`, and the - wanted constraint co2 must not float. - - 4. And the evidence variable of any equality constraint (incl - Wanted ones) whose type mentions a bound variable. Example: - forall k. [W] co1 :: t1 ~# t2 |> co2 - [W] co2 :: k ~# * - Here, since `k` is bound, so is `co2` and hence so is `co1`. - -Here (1,2,3) are handled by the "seed_skols" calculation, and -(4) is done by the transCloVarSet call. - -The possible dependence on givens, and evidence bindings, is more -subtle than we'd realised at first. See #14584. - -How can (4) arise? Suppose we have (k :: *), (a :: k), and ([G} k ~ *). -Then form an equality like (a ~ Int) we might end up with - [W] co1 :: k ~ * - [W] co2 :: (a |> co1) ~ Int - - ********************************************************************************* * * * Defaulting and disambiguation * diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index ce8bf24632..7586bd5ed5 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -4,9 +4,9 @@ module GHC.Tc.Solver.Canonical( canonicalize, - unifyDerived, + unifyDerived, unifyTest, UnifyTestResult(..), makeSuperClasses, - StopOrContinue(..), stopWith, continueWith, + StopOrContinue(..), stopWith, continueWith, andWhenContinue, solveCallStack -- For GHC.Tc.Solver ) where @@ -51,7 +51,8 @@ import GHC.Data.Bag import GHC.Utils.Monad import Control.Monad import Data.Maybe ( isJust, isNothing ) -import Data.List ( zip4 ) +import Data.List ( zip4, partition ) +import GHC.Types.Unique.Set( nonDetEltsUniqSet ) import GHC.Types.Basic import Data.Bifunctor ( bimap ) @@ -2246,10 +2247,10 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco -- If we have F a ~ F (F a), we want to swap. swap_for_occurs - | MTVU_OK () <- checkTyFamEq dflags fun_tc2 fun_args2 - (mkTyConApp fun_tc1 fun_args1) - , MTVU_Occurs <- checkTyFamEq dflags fun_tc1 fun_args1 - (mkTyConApp fun_tc2 fun_args2) + | CTE_OK <- checkTyFamEq dflags fun_tc2 fun_args2 + (mkTyConApp fun_tc1 fun_args1) + , CTE_Occurs <- checkTyFamEq dflags fun_tc1 fun_args1 + (mkTyConApp fun_tc2 fun_args2) = True | otherwise @@ -2274,8 +2275,8 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco -- This function handles the case where one side is a tyvar and the other is -- a type family application. Which to put on the left? --- If we can unify the variable, put it on the left, as this may be our only --- shot to unify. +-- If the tyvar is a touchable meta-tyvar, put it on the left, as this may +-- be our only shot to unify. -- Otherwise, put the function on the left, because it's generally better to -- rewrite away function calls. This makes types smaller. And it seems necessary: -- [W] F alpha ~ alpha @@ -2283,22 +2284,20 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco -- [W] G alpha beta ~ Int ( where we have type instance G a a = a ) -- If we end up with a stuck alpha ~ F alpha, we won't be able to solve this. -- Test case: indexed-types/should_compile/CEqCanOccursCheck --- It would probably work to always put the variable on the left, but we think --- it would be less efficient. canEqTyVarFunEq :: CtEvidence -- :: lhs ~ (rhs |> mco) -- or (rhs |> mco) ~ lhs if swapped -> EqRel -> SwapFlag - -> TyVar -> TcType -- lhs, pretty lhs - -> TyCon -> [Xi] -> TcType -- rhs fun, rhs args, pretty rhs + -> TyVar -> TcType -- lhs (or if swapped rhs), pretty lhs + -> TyCon -> [Xi] -> TcType -- rhs (or if swapped lhs) fun and args, pretty rhs -> MCoercion -- :: kind(rhs) ~N kind(lhs) -> TcS (StopOrContinue Ct) canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco - = do { tclvl <- getTcLevel - ; dflags <- getDynFlags - ; if | isTouchableMetaTyVar tclvl tv1 - , MTVU_OK _ <- checkTyVarEq dflags YesTypeFamilies tv1 (ps_xi2 `mkCastTyMCo` mco) - -> canEqCanLHSFinish ev eq_rel swapped (TyVarLHS tv1) - (ps_xi2 `mkCastTyMCo` mco) + = do { can_unify <- unifyTest ev tv1 rhs + ; dflags <- getDynFlags + ; if | case can_unify of { NoUnify -> False; _ -> True } + , CTE_OK <- checkTyVarEq dflags YesTypeFamilies tv1 rhs + -> canEqCanLHSFinish ev eq_rel swapped (TyVarLHS tv1) rhs + | otherwise -> do { new_ev <- rewriteCastedEquality ev eq_rel swapped (mkTyVarTy tv1) (mkTyConApp fun_tc2 fun_args2) @@ -2308,6 +2307,82 @@ canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco (ps_xi1 `mkCastTyMCo` sym_mco) } } where sym_mco = mkTcSymMCo mco + rhs = ps_xi2 `mkCastTyMCo` mco + +data UnifyTestResult + -- See Note [Solve by unification] in GHC.Tc.Solver.Interact + -- which points out that having UnifySameLevel is just an optimisation; + -- we could manage with UnifyOuterLevel alone (suitably renamed) + = UnifySameLevel + | UnifyOuterLevel [TcTyVar] -- Promote these + TcLevel -- ..to this level + | NoUnify + +instance Outputable UnifyTestResult where + ppr UnifySameLevel = text "UnifySameLevel" + ppr (UnifyOuterLevel tvs lvl) = text "UnifyOuterLevel" <> parens (ppr lvl <+> ppr tvs) + ppr NoUnify = text "NoUnify" + +unifyTest :: CtEvidence -> TcTyVar -> TcType -> TcS UnifyTestResult +-- This is the key test for untouchability: +-- See Note [Unification preconditions] in GHC.Tc.Utils.Unify +-- and Note [Solve by unification] in GHC.Tc.Solver.Interact +unifyTest ev tv1 rhs + | not (isGiven ev) -- See Note [Do not unify Givens] + , MetaTv { mtv_tclvl = tv_lvl, mtv_info = info } <- tcTyVarDetails tv1 + , canSolveByUnification info rhs + = do { ambient_lvl <- getTcLevel + ; given_eq_lvl <- getInnermostGivenEqLevel + + ; if | tv_lvl `sameDepthAs` ambient_lvl + -> return UnifySameLevel + + | tv_lvl `deeperThanOrSame` given_eq_lvl -- No intervening given equalities + , all (does_not_escape tv_lvl) free_skols -- No skolem escapes + -> return (UnifyOuterLevel free_metas tv_lvl) + + | otherwise + -> return NoUnify } + | otherwise + = return NoUnify + where + (free_metas, free_skols) = partition isPromotableMetaTyVar $ + nonDetEltsUniqSet $ + tyCoVarsOfType rhs + + does_not_escape tv_lvl fv + | isTyVar fv = tv_lvl `deeperThanOrSame` tcTyVarLevel fv + | otherwise = True + -- Coercion variables are not an escape risk + -- If an implication binds a coercion variable, it'll have equalities, + -- so the "intervening given equalities" test above will catch it + -- Coercion holes get filled with coercions, so again no problem. + +{- Note [Do not unify Givens] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider this GADT match + data T a where + T1 :: T Int + ... + + f x = case x of + T1 -> True + ... + +So we get f :: T alpha[1] -> beta[1] + x :: T alpha[1] +and from the T1 branch we get the implication + forall[2] (alpha[1] ~ Int) => beta[1] ~ Bool + +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.) + +Simple solution: never unify in Givens! +-} -- The RHS here is either not CanEqLHS, or it's one that we -- want to rewrite the LHS to (as per e.g. swapOverTyVars) @@ -2427,11 +2502,11 @@ canEqOK :: DynFlags -> EqRel -> CanEqLHS -> Xi -> CanEqOK canEqOK dflags eq_rel lhs rhs = ASSERT( good_rhs ) case checkTypeEq dflags YesTypeFamilies lhs rhs of - MTVU_OK () -> CanEqOK - MTVU_Bad -> CanEqNotOK OtherCIS + CTE_OK -> CanEqOK + CTE_Bad -> CanEqNotOK OtherCIS -- Violation of TyEq:F - MTVU_HoleBlocker -> CanEqNotOK (BlockedCIS holes) + CTE_HoleBlocker -> CanEqNotOK (BlockedCIS holes) where holes = coercionHolesOfType rhs -- This is the case detailed in -- Note [Equalities with incompatible kinds] @@ -2440,7 +2515,7 @@ canEqOK dflags eq_rel lhs rhs -- These are both a violation of TyEq:OC, but we -- want to differentiate for better production of -- error messages - MTVU_Occurs | TyVarLHS tv <- lhs + CTE_Occurs | TyVarLHS tv <- lhs , isInsolubleOccursCheck eq_rel tv rhs -> CanEqNotOK InsolubleCIS -- If we have a ~ [a], it is not canonical, and in particular -- we don't want to rewrite existing inerts with it, otherwise diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index dc20b90260..e8ab8ad82a 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE CPP #-} +{-# LANGUAGE CPP, MultiWayIf #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} @@ -14,7 +14,6 @@ import GHC.Prelude import GHC.Types.Basic ( SwapFlag(..), infinity, IntWithInf, intGtLimit ) import GHC.Tc.Solver.Canonical -import GHC.Tc.Utils.Unify( canSolveByUnification ) import GHC.Types.Var.Set import GHC.Core.Type as Type import GHC.Core.InstEnv ( DFunInstType ) @@ -39,6 +38,7 @@ import GHC.Tc.Types import GHC.Tc.Types.Constraint import GHC.Core.Predicate import GHC.Tc.Types.Origin +import GHC.Tc.Utils.TcMType( promoteMetaTyVarTo ) import GHC.Tc.Solver.Monad import GHC.Data.Bag import GHC.Utils.Monad ( concatMapM, foldlM ) @@ -106,8 +106,6 @@ solveSimpleGivens givens go new_givens } solveSimpleWanteds :: Cts -> TcS WantedConstraints --- NB: 'simples' may contain /derived/ equalities, floated --- out from a nested implication. So don't discard deriveds! -- The result is not necessarily zonked solveSimpleWanteds simples = do { traceTcS "solveSimpleWanteds {" (ppr simples) @@ -430,12 +428,11 @@ interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct) interactWithInertsStage wi = do { inerts <- getTcSInerts - ; lvl <- getTcLevel ; let ics = inert_cans inerts ; case wi of - CEqCan {} -> interactEq lvl ics wi - CIrredCan {} -> interactIrred ics wi - CDictCan {} -> interactDict ics wi + CEqCan {} -> interactEq ics wi + CIrredCan {} -> interactIrred ics wi + CDictCan {} -> interactDict ics wi _ -> pprPanic "interactWithInerts" (ppr wi) } -- CNonCanonical have been canonicalised @@ -734,25 +731,26 @@ Example of (b): assume a top-level class and instance declaration: Assume we have started with an implication: - forall c. Eq c => { wc_simple = D [c] c [W] } + forall c. Eq c => { wc_simple = [W] D [c] c } -which we have simplified to: +which we have simplified to, with a Derived constraing coming from +D's functional dependency: - forall c. Eq c => { wc_simple = D [c] c [W] - (c ~ [c]) [D] } + forall c. Eq c => { wc_simple = [W] D [c] c [W] + [D] (c ~ [c]) } -For some reason, e.g. because we floated an equality somewhere else, -we might try to re-solve this implication. If we do not do a -dropDerivedWC, then we will end up trying to solve the following -constraints the second time: +When iterating the solver, we might try to re-solve this +implication. If we do not do a dropDerivedWC, then we will end up +trying to solve the following constraints the second time: - (D [c] c) [W] - (c ~ [c]) [D] + [W] (D [c] c) + [D] (c ~ [c]) which will result in two Deriveds to end up in the insoluble set: - wc_simple = D [c] c [W] - (c ~ [c]) [D], (c ~ [c]) [D] + wc_simple = [W] D [c] c + [D] (c ~ [c]) + [D] (c ~ [c]) -} {- @@ -1439,8 +1437,8 @@ inertsCanDischarge inerts lhs rhs fr | otherwise = False -- Work item is fully discharged -interactEq :: TcLevel -> InertCans -> Ct -> TcS (StopOrContinue Ct) -interactEq tclvl inerts workItem@(CEqCan { cc_lhs = lhs +interactEq :: InertCans -> Ct -> TcS (StopOrContinue Ct) +interactEq inerts workItem@(CEqCan { cc_lhs = lhs , cc_rhs = rhs , cc_ev = ev , cc_eq_rel = eq_rel }) @@ -1465,24 +1463,43 @@ interactEq tclvl inerts workItem@(CEqCan { cc_lhs = lhs = do { traceTcS "Not unifying representational equality" (ppr workItem) ; continueWith workItem } - -- try improvement, if possible - | TyFamLHS fam_tc fam_args <- lhs - , isImprovable ev - = do { improveLocalFunEqs ev inerts fam_tc fam_args rhs - ; continueWith workItem } - - | TyVarLHS tv <- lhs - , canSolveByUnification tclvl tv rhs - = do { solveByUnification ev tv rhs - ; n_kicked <- kickOutAfterUnification tv - ; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) } - | otherwise - = continueWith workItem - -interactEq _ _ wi = pprPanic "interactEq" (ppr wi) - -solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS () + = case lhs of + TyVarLHS tv -> tryToSolveByUnification workItem ev tv rhs + + TyFamLHS tc args -> do { when (isImprovable ev) $ + -- Try improvement, if possible + improveLocalFunEqs ev inerts tc args rhs + ; continueWith workItem } + +interactEq _ wi = pprPanic "interactEq" (ppr wi) + +---------------------- +-- We have a meta-tyvar on the left, and metaTyVarUpateOK has said "yes" +-- So try to solve by unifying. +-- Three reasons why not: +-- Skolem escape +-- Given equalities (GADTs) +-- Unifying a TyVarTv with a non-tyvar type +tryToSolveByUnification :: Ct -> CtEvidence + -> TcTyVar -- LHS tyvar + -> TcType -- RHS + -> TcS (StopOrContinue Ct) +tryToSolveByUnification work_item ev tv rhs + = do { can_unify <- unifyTest ev tv rhs + ; traceTcS "tryToSolveByUnification" (vcat [ ppr tv <+> char '~' <+> ppr rhs + , ppr can_unify ]) + + ; case can_unify of + NoUnify -> continueWith work_item + -- For the latter two cases see Note [Solve by unification] + UnifySameLevel -> solveByUnification ev tv rhs + UnifyOuterLevel free_metas tv_lvl + -> do { wrapTcS $ mapM_ (promoteMetaTyVarTo tv_lvl) free_metas + ; setUnificationFlag tv_lvl + ; solveByUnification ev tv rhs } } + +solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS (StopOrContinue Ct) -- Solve with the identity coercion -- Precondition: kind(xi) equals kind(tv) -- Precondition: CtEvidence is Wanted or Derived @@ -1504,9 +1521,10 @@ solveByUnification wd tv xi text "Coercion:" <+> pprEq tv_ty xi, text "Left Kind is:" <+> ppr (tcTypeKind tv_ty), text "Right Kind is:" <+> ppr (tcTypeKind xi) ] - ; unifyTyVar tv xi - ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) } + ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) + ; n_kicked <- kickOutAfterUnification tv + ; return (Stop wd (text "Solved by unification" <+> pprKicked n_kicked)) } {- Note [Avoid double unifications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1542,6 +1560,34 @@ and we want to get alpha := N b. See also #15144, which was caused by unifying a representational equality. +Note [Solve by unification] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If we solve + alpha[n] ~ ty +by unification, there are two cases to consider + +* UnifySameLevel: if the ambient level is 'n', then + we can simply update alpha := ty, and do nothing else + +* UnifyOuterLevel free_metas n: if the ambient level is greater than + 'n' (the level of alpha), in addition to setting alpha := ty we must + do two other things: + + 1. Promote all the free meta-vars of 'ty' to level n. After all, + alpha[n] is at level n, and so if we set, say, + alpha[n] := Maybe beta[m], + we must ensure that when unifying beta we do skolem-escape checks + etc relevent to level n. Simple way to do that: promote beta to + level n. + + 2. Set the Unification Level Flag to record that a level-n unification has + taken place. See Note [The Unification Level Flag] in GHC.Tc.Solver.Monad + +NB: UnifySameLevel is just an optimisation for UnifyOuterLevel. Promotion +would be a no-op, and setting the unification flag unnecessarily would just +make the solver iterate more often. (We don't need to iterate when unifying +at the ambient level becuase of the kick-out mechanism.) + ************************************************************************ * * diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 76d9316bf6..2560a8e185 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -17,7 +17,7 @@ module GHC.Tc.Solver.Monad ( -- The TcS monad TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds, runTcSInerts, - failTcS, warnTcS, addErrTcS, + failTcS, warnTcS, addErrTcS, wrapTcS, runTcSEqualities, nestTcS, nestImplicTcS, setEvBindsTcS, emitImplicationTcS, emitTvImplicationTcS, @@ -31,6 +31,7 @@ module GHC.Tc.Solver.Monad ( panicTcS, traceTcS, traceFireTcS, bumpStepCountTcS, csTraceTcS, wrapErrTcS, wrapWarnTcS, + resetUnificationFlag, setUnificationFlag, -- Evidence creation and transformation MaybeNew(..), freshGoals, isFresh, getEvExpr, @@ -60,7 +61,7 @@ module GHC.Tc.Solver.Monad ( updInertTcS, updInertCans, updInertDicts, updInertIrreds, getHasGivenEqs, setInertCans, getInertEqs, getInertCans, getInertGivens, - getInertInsols, + getInertInsols, getInnermostGivenEqLevel, getTcSInerts, setTcSInerts, matchableGivens, prohibitedSuperClassSolve, mightMatchLater, getUnsolvedInerts, @@ -186,7 +187,6 @@ import Control.Monad import GHC.Utils.Monad import Data.IORef import Data.List ( partition, mapAccumL ) -import qualified Data.Semigroup as S import Data.List.NonEmpty ( NonEmpty(..), cons, toList, nonEmpty ) import qualified Data.List.NonEmpty as NE import Control.Arrow ( first ) @@ -418,12 +418,14 @@ instance Outputable InertSet where emptyInertCans :: InertCans emptyInertCans - = IC { inert_eqs = emptyDVarEnv - , inert_dicts = emptyDicts - , inert_safehask = emptyDicts - , inert_funeqs = emptyFunEqs - , inert_insts = [] - , inert_irreds = emptyCts } + = IC { inert_eqs = emptyDVarEnv + , inert_given_eq_lvl = topTcLevel + , inert_given_eqs = False + , inert_dicts = emptyDicts + , inert_safehask = emptyDicts + , inert_funeqs = emptyFunEqs + , inert_insts = [] + , inert_irreds = emptyCts } emptyInert :: InertSet emptyInert @@ -697,6 +699,19 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more -- Irreducible predicates that cannot be made canonical, -- and which don't interact with others (e.g. (c a)) -- and insoluble predicates (e.g. Int ~ Bool, or a ~ [a]) + + , inert_given_eq_lvl :: TcLevel + -- The TcLevel of the innermost implication that has a Given + -- equality of the sort that make a unification variable untouchable + -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify). + -- See Note [Tracking Given equalities] below + + , inert_given_eqs :: Bool + -- True <=> The inert Givens *at this level* (tcl_tclvl) + -- could includes at least one equality /other than/ a + -- let-bound skolem equality. + -- Reason: report these givens when reporting a failed equality + -- See Note [Tracking Given equalities] } type InertEqs = DTyVarEnv EqualCtList @@ -730,7 +745,126 @@ listToEqualCtList :: [Ct] -> Maybe EqualCtList -- non-empty listToEqualCtList cts = EqualCtList <$> nonEmpty cts -{- Note [Detailed InertCans Invariants] +{- Note [Tracking Given equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +For reasons described in (UNTOUCHABLE) in GHC.Tc.Utils.Unify +Note [Unification preconditions], we can't unify + alpha[2] ~ Int +under a level-4 implication if there are any Given equalities +bound by the implications at level 3 of 4. To that end, the +InertCans tracks + + inert_given_eq_lvl :: TcLevel + -- The TcLevel of the innermost implication that has a Given + -- equality of the sort that make a unification variable untouchable + -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify). + +We update inert_given_eq_lvl whenever we add a Given to the +inert set, in updateGivenEqs. + +Then a unification variable alpha[n] is untouchable iff + n < inert_given_eq_lvl +that is, if the unification variable was born outside an +enclosing Given equality. + +Exactly which constraints should trigger (UNTOUCHABLE), and hence +should update inert_given_eq_lvl? + +* We do /not/ need to worry about let-bound skolems, such ast + forall[2] a. a ~ [b] => blah + See Note [Let-bound skolems] + +* Consider an implication + forall[2]. beta[1] => alpha[1] ~ Int + where beta is a unification variable that has already been unified + to () in an outer scope. Then alpha[1] is perfectly touchable and + we can unify alpha := Int. So when deciding whether the givens contain + an equality, we should canonicalise first, rather than just looking at + the /original/ givens (#8644). + + * However, we must take account of *potential* equalities. Consider the + same example again, but this time we have /not/ yet unified beta: + forall[2] beta[1] => ...blah... + + Because beta might turn into an equality, updateGivenEqs conservatively + treats it as a potential equality, and updates inert_give_eq_lvl + + * What about something like forall[2] a b. a ~ F b => [W] alpha[1] ~ X y z? + + That Given cannot affect the Wanted, because the Given is entirely + *local*: it mentions only skolems bound in the very same + implication. Such equalities need not make alpha untouchable. (Test + case typecheck/should_compile/LocalGivenEqs has a real-life + motivating example, with some detailed commentary.) + Hence the 'mentionsOuterVar' test in updateGivenEqs. + + However, solely to support better error messages + (see Note [HasGivenEqs] in GHC.Tc.Types.Constraint) we also track + these "local" equalities in the boolean inert_given_eqs field. + This field is used only to set the ic_given_eqs field to LocalGivenEqs; + see the function getHasGivenEqs. + + Here is a simpler case that triggers this behaviour: + + data T where + MkT :: F a ~ G b => a -> b -> T + + f (MkT _ _) = True + + Because of this behaviour around local equality givens, we can infer the + type of f. This is typecheck/should_compile/LocalGivenEqs2. + + * We need not look at the equality relation involved (nominal vs + representational), because representational equalities can still + imply nominal ones. For example, if (G a ~R G b) and G's argument's + role is nominal, then we can deduce a ~N b. + +Note [Let-bound skolems] +~~~~~~~~~~~~~~~~~~~~~~~~ +If * the inert set contains a canonical Given CEqCan (a ~ ty) +and * 'a' is a skolem bound in this very implication, + +then: +a) The Given is pretty much a let-binding, like + f :: (a ~ b->c) => a -> a + Here the equality constraint is like saying + let a = b->c in ... + It is not adding any new, local equality information, + and hence can be ignored by has_given_eqs + +b) 'a' will have been completely substituted out in the inert set, + so we can safely discard it. + +For an example, see #9211. + +See also GHC.Tc.Utils.Unify Note [Deeper level on the left] for how we ensure +that the right variable is on the left of the equality when both are +tyvars. + +You might wonder whether the skolem really needs to be bound "in the +very same implication" as the equuality constraint. +Consider this (c.f. #15009): + + data S a where + MkS :: (a ~ Int) => S a + + g :: forall a. S a -> a -> blah + g x y = let h = \z. ( z :: Int + , case x of + MkS -> [y,z]) + in ... + +From the type signature for `g`, we get `y::a` . Then when we +encounter the `\z`, we'll assign `z :: alpha[1]`, say. Next, from the +body of the lambda we'll get + + [W] alpha[1] ~ Int -- From z::Int + [W] forall[2]. (a ~ Int) => [W] alpha[1] ~ a -- From [y,z] + +Now, unify alpha := a. Now we are stuck with an unsolved alpha~Int! +So we must treat alpha as untouchable under the forall[2] implication. + +Note [Detailed InertCans Invariants] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The InertCans represents a collection of constraints with the following properties: @@ -1027,6 +1161,8 @@ instance Outputable InertCans where ppr (IC { inert_eqs = eqs , inert_funeqs = funeqs, inert_dicts = dicts , inert_safehask = safehask, inert_irreds = irreds + , inert_given_eq_lvl = ge_lvl + , inert_given_eqs = given_eqs , inert_insts = insts }) = braces $ vcat @@ -1043,6 +1179,8 @@ instance Outputable InertCans where text "Irreds =" <+> pprCts irreds , ppUnless (null insts) $ text "Given instances =" <+> vcat (map ppr insts) + , text "Innermost given equalities =" <+> ppr ge_lvl + , text "Given eqs at this level =" <+> ppr given_eqs ] where folder (EqualCtList eqs) rest = nonEmptyToBag eqs `andCts` rest @@ -1456,20 +1594,32 @@ findEq icans (TyFamLHS fun_tc fun_args) addInertForAll :: QCInst -> TcS () -- Add a local Given instance, typically arising from a type signature addInertForAll new_qci - = do { ics <- getInertCans - ; insts' <- add_qci (inert_insts ics) - ; setInertCans (ics { inert_insts = insts' }) } + = do { ics <- getInertCans + ; ics1 <- add_qci ics + + -- Update given equalities. C.f updateGivenEqs + ; tclvl <- getTcLevel + ; let pred = qci_pred new_qci + not_equality = isClassPred pred && not (isEqPred pred) + -- True <=> definitely not an equality + -- A qci_pred like (f a) might be an equality + + ics2 | not_equality = ics1 + | otherwise = ics1 { inert_given_eq_lvl = tclvl + , inert_given_eqs = True } + + ; setInertCans ics2 } where - add_qci :: [QCInst] -> TcS [QCInst] + add_qci :: InertCans -> TcS InertCans -- See Note [Do not add duplicate quantified instances] - add_qci qcis + add_qci ics@(IC { inert_insts = qcis }) | any same_qci qcis = do { traceTcS "skipping duplicate quantified instance" (ppr new_qci) - ; return qcis } + ; return ics } | otherwise = do { traceTcS "adding new inert quantified instance" (ppr new_qci) - ; return (new_qci : qcis) } + ; return (ics { inert_insts = new_qci : qcis }) } same_qci old_qci = tcEqType (ctEvPred (qci_ev old_qci)) (ctEvPred (qci_ev new_qci)) @@ -1523,7 +1673,8 @@ addInertCan ct ; ics <- getInertCans ; ct <- maybeEmitShadow ics ct ; ics <- maybeKickOut ics ct - ; setInertCans (add_item ics ct) + ; tclvl <- getTcLevel + ; setInertCans (add_item tclvl ics ct) ; traceTcS "addInertCan }" $ empty } @@ -1536,23 +1687,54 @@ maybeKickOut ics ct | otherwise = return ics -add_item :: InertCans -> Ct -> InertCans -add_item ics item@(CEqCan { cc_lhs = TyFamLHS tc tys }) - = ics { inert_funeqs = addCanFunEq (inert_funeqs ics) tc tys item } - -add_item ics item@(CEqCan { cc_lhs = TyVarLHS tv }) - = ics { inert_eqs = addTyEq (inert_eqs ics) tv item } - -add_item ics@(IC { inert_irreds = irreds }) item@(CIrredCan {}) - = ics { inert_irreds = irreds `Bag.snocBag` item } - -add_item ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) +add_item :: TcLevel -> InertCans -> Ct -> InertCans +add_item tc_lvl + ics@(IC { inert_funeqs = funeqs, inert_eqs = eqs }) + item@(CEqCan { cc_lhs = lhs }) + = updateGivenEqs tc_lvl item $ + case lhs of + TyFamLHS tc tys -> ics { inert_funeqs = addCanFunEq funeqs tc tys item } + TyVarLHS tv -> ics { inert_eqs = addTyEq eqs tv item } + +add_item tc_lvl ics@(IC { inert_irreds = irreds }) item@(CIrredCan {}) + = updateGivenEqs tc_lvl item $ -- An Irred might turn out to be an + -- equality, so we play safe + ics { inert_irreds = irreds `Bag.snocBag` item } + +add_item _ ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) = ics { inert_dicts = addDict (inert_dicts ics) cls tys item } -add_item _ item +add_item _ _ item = pprPanic "upd_inert set: can't happen! Inserting " $ ppr item -- Can't be CNonCanonical because they only land in inert_irreds +updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans +-- Set the inert_given_eq_level to the current level (tclvl) +-- if the constraint is a given equality that should prevent +-- filling in an outer unification variable. +-- See See Note [Tracking Given equalities] +updateGivenEqs tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl }) + | not (isGivenCt ct) = inerts + | not_equality ct = inerts -- See Note [Let-bound skolems] + | otherwise = inerts { inert_given_eq_lvl = ge_lvl' + , inert_given_eqs = True } + where + ge_lvl' | mentionsOuterVar tclvl (ctEvidence ct) + -- Includes things like (c a), which *might* be an equality + = tclvl + | otherwise + = ge_lvl + + not_equality :: Ct -> Bool + -- True <=> definitely not an equality of any kind + -- except for a let-bound skolem, which doesn't count + -- See Note [Let-bound skolems] + -- NB: no need to spot the boxed CDictCan (a ~ b) because its + -- superclass (a ~# b) will be a CEqCan + not_equality (CEqCan { cc_lhs = TyVarLHS tv }) = not (isOuterTyVar tclvl tv) + not_equality (CDictCan {}) = True + not_equality _ = False + ----------------------------------------- kickOutRewritable :: CtFlavourRole -- Flavour/role of the equality that -- is being added to the inert set @@ -1596,7 +1778,6 @@ kick_out_rewritable :: CtFlavourRole -- Flavour/role of the equality that kick_out_rewritable new_fr new_lhs ics@(IC { inert_eqs = tv_eqs , inert_dicts = dictmap - , inert_safehask = safehask , inert_funeqs = funeqmap , inert_irreds = irreds , inert_insts = old_insts }) @@ -1610,12 +1791,12 @@ kick_out_rewritable new_fr new_lhs | otherwise = (kicked_out, inert_cans_in) where - inert_cans_in = IC { inert_eqs = tv_eqs_in - , inert_dicts = dicts_in - , inert_safehask = safehask -- ?? - , inert_funeqs = feqs_in - , inert_irreds = irs_in - , inert_insts = insts_in } + -- inert_safehask stays unchanged; is that right? + inert_cans_in = ics { inert_eqs = tv_eqs_in + , inert_dicts = dicts_in + , inert_funeqs = feqs_in + , inert_irreds = irs_in + , inert_insts = insts_in } kicked_out :: WorkList -- NB: use extendWorkList to ensure that kicked-out equalities get priority @@ -1968,6 +2149,10 @@ updInertIrreds upd_fn getInertEqs :: TcS (DTyVarEnv EqualCtList) getInertEqs = do { inert <- getInertCans; return (inert_eqs inert) } +getInnermostGivenEqLevel :: TcS TcLevel +getInnermostGivenEqLevel = do { inert <- getInertCans + ; return (inert_given_eq_lvl inert) } + getInertInsols :: TcS Cts -- Returns insoluble equality constraints -- specifically including Givens @@ -2077,63 +2262,46 @@ getUnsolvedInerts getHasGivenEqs :: TcLevel -- TcLevel of this implication -> TcS ( HasGivenEqs -- are there Given equalities? , Cts ) -- Insoluble equalities arising from givens --- See Note [When does an implication have given equalities?] +-- See Note [Tracking Given equalities] getHasGivenEqs tclvl - = do { inerts@(IC { inert_eqs = ieqs, inert_funeqs = funeqs, inert_irreds = irreds }) + = do { inerts@(IC { inert_irreds = irreds + , inert_given_eqs = given_eqs + , inert_given_eq_lvl = ge_lvl }) <- getInertCans - ; let has_given_eqs = foldMap check_local_given_ct irreds - S.<> foldMap (lift_equal_ct_list check_local_given_tv_eq) ieqs - S.<> foldMapFunEqs (lift_equal_ct_list check_local_given_ct) funeqs - insols = filterBag insolubleEqCt irreds + ; let insols = filterBag insolubleEqCt irreds -- Specifically includes ones that originated in some -- outer context but were refined to an insoluble by -- a local equality; so do /not/ add ct_given_here. + -- See Note [HasGivenEqs] in GHC.Tc.Types.Constraint, and + -- Note [Tracking Given equalities] in this module + has_ge | ge_lvl == tclvl = MaybeGivenEqs + | given_eqs = LocalGivenEqs + | otherwise = NoGivenEqs + ; traceTcS "getHasGivenEqs" $ - vcat [ text "has_given_eqs:" <+> ppr has_given_eqs + vcat [ text "given_eqs:" <+> ppr given_eqs + , text "ge_lvl:" <+> ppr ge_lvl + , text "ambient level:" <+> ppr tclvl , text "Inerts:" <+> ppr inerts , text "Insols:" <+> ppr insols] - ; return (has_given_eqs, insols) } - where - check_local_given_ct :: Ct -> HasGivenEqs - check_local_given_ct ct - | given_here ev = if mentions_outer_var ev then MaybeGivenEqs else LocalGivenEqs - | otherwise = NoGivenEqs - where - ev = ctEvidence ct - - lift_equal_ct_list :: (Ct -> HasGivenEqs) -> EqualCtList -> HasGivenEqs - -- returns NoGivenEqs for non-singleton lists, as Given lists are always - -- singletons - lift_equal_ct_list check (EqualCtList (ct :| [])) = check ct - lift_equal_ct_list _ _ = NoGivenEqs - - check_local_given_tv_eq :: Ct -> HasGivenEqs - check_local_given_tv_eq (CEqCan { cc_lhs = TyVarLHS tv, cc_ev = ev}) - | given_here ev - = if is_outer_var tv then MaybeGivenEqs else NoGivenEqs - -- See Note [Let-bound skolems] - | otherwise - = NoGivenEqs - check_local_given_tv_eq other_ct = check_local_given_ct other_ct - - given_here :: CtEvidence -> Bool - -- True for a Given bound by the current implication, - -- i.e. the current level - given_here ev = isGiven ev - && tclvl == ctLocLevel (ctEvLoc ev) - - mentions_outer_var :: CtEvidence -> Bool - mentions_outer_var = anyFreeVarsOfType is_outer_var . ctEvPred - - is_outer_var :: TyCoVar -> Bool - is_outer_var tv - -- NB: 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 = isTouchableMetaTyVar tclvl tv || - tclvl `strictlyDeeperThan` tcTyVarLevel tv - | otherwise = False + ; return (has_ge, insols) } + +mentionsOuterVar :: TcLevel -> CtEvidence -> Bool +mentionsOuterVar tclvl ev + = anyFreeVarsOfType (isOuterTyVar tclvl) $ + ctEvPred ev + +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. + | otherwise = False -- Coercion variables; doesn't much matter -- | Returns Given constraints that might, -- potentially, match the given pred. This is used when checking to see if a @@ -2267,112 +2435,6 @@ Examples: This treatment fixes #18910 and is tested in typecheck/should_compile/InstanceGivenOverlap{,2} -Note [When does an implication have given equalities?] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider an implication - beta => alpha ~ Int -where beta is a unification variable that has already been unified -to () in an outer scope. Then we can float the (alpha ~ Int) out -just fine. So when deciding whether the givens contain an equality, -we should canonicalise first, rather than just looking at the original -givens (#8644). - -So we simply look at the inert, canonical Givens and see if there are -any equalities among them, the calculation of has_given_eqs. There -are some wrinkles: - - * We must know which ones are bound in *this* implication and which - are bound further out. We can find that out from the TcLevel - of the Given, which is itself recorded in the tcl_tclvl field - of the TcLclEnv stored in the Given (ev_given_here). - - What about interactions between inner and outer givens? - - Outer given is rewritten by an inner given, then there must - have been an inner given equality, hence the “given-eq” flag - will be true anyway. - - - Inner given rewritten by outer, retains its level (ie. The inner one) - - * We must take account of *potential* equalities, like the one above: - beta => ...blah... - If we still don't know what beta is, we conservatively treat it as potentially - becoming an equality. Hence including 'irreds' in the calculation or has_given_eqs. - Note that we can't really know what's in an irred, so any irred is considered - a potential equality. - - * What about something like forall a b. a ~ F b => [W] c ~ X y z? That Given - cannot affect the Wanted, because the Given is entirely *local*: it mentions - only skolems bound in the very same implication. Such equalities need not - prevent floating. (Test case typecheck/should_compile/LocalGivenEqs has a - real-life motivating example, with some detailed commentary.) These - equalities are noted with LocalGivenEqs: they do not prevent floating, but - they also are allowed to show up in error messages. See - Note [Suppress redundant givens during error reporting] in GHC.Tc.Errors. - The difference between what stops floating and what is suppressed from - error messages is why we need three options for HasGivenEqs. - - There is also a simpler case that triggers this behaviour: - - data T where - MkT :: F a ~ G b => a -> b -> T - - f (MkT _ _) = True - - Because of this behaviour around local equality givens, we can infer the - type of f. This is typecheck/should_compile/LocalGivenEqs2. - - * See Note [Let-bound skolems] for another wrinkle - - * We need not look at the equality relation involved (nominal vs representational), - because representational equalities can still imply nominal ones. For example, - if (G a ~R G b) and G's argument's role is nominal, then we can deduce a ~N b. - -Note [Let-bound skolems] -~~~~~~~~~~~~~~~~~~~~~~~~ -If * the inert set contains a canonical Given CEqCan (a ~ ty) -and * 'a' is a skolem bound in this very implication, - -then: -a) The Given is pretty much a let-binding, like - f :: (a ~ b->c) => a -> a - Here the equality constraint is like saying - let a = b->c in ... - It is not adding any new, local equality information, - and hence can be ignored by has_given_eqs - -b) 'a' will have been completely substituted out in the inert set, - so we can safely discard it. - -For an example, see #9211. - -See also GHC.Tc.Utils.Unify Note [Deeper level on the left] for how we ensure -that the right variable is on the left of the equality when both are -tyvars. - -You might wonder whether the skokem really needs to be bound "in the -very same implication" as the equuality constraint. -(c.f. #15009) Consider this: - - data S a where - MkS :: (a ~ Int) => S a - - g :: forall a. S a -> a -> blah - g x y = let h = \z. ( z :: Int - , case x of - MkS -> [y,z]) - in ... - -From the type signature for `g`, we get `y::a` . Then when we -encounter the `\z`, we'll assign `z :: alpha[1]`, say. Next, from the -body of the lambda we'll get - - [W] alpha[1] ~ Int -- From z::Int - [W] forall[2]. (a ~ Int) => [W] alpha[1] ~ a -- From [y,z] - -Now, suppose we decide to float `alpha ~ a` out of the implication -and then unify `alpha := a`. Now we are stuck! But if treat -`alpha ~ Int` first, and unify `alpha := Int`, all is fine. -But we absolutely cannot float that equality or we will get stuck. -} removeInertCts :: [Ct] -> InertCans -> InertCans @@ -2552,9 +2614,6 @@ tcAppMapToBag m = foldTcAppMap consBag m emptyBag foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b foldTcAppMap k m z = foldDTyConEnv (foldTM k) z m -foldMapTcAppMap :: Monoid m => (a -> m) -> TcAppMap a -> m -foldMapTcAppMap f = foldMap (foldMap f) - {- ********************************************************************* * * @@ -2688,9 +2747,6 @@ findFunEqsByTyCon m tc foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b foldFunEqs = foldTcAppMap -foldMapFunEqs :: Monoid m => (a -> m) -> FunEqMap a -> m -foldMapFunEqs = foldMapTcAppMap - insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a insertFunEq m tc tys val = insertTcApp m tc tys val @@ -2723,6 +2779,12 @@ data TcSEnv -- The number of unification variables we have filled -- The important thing is whether it is non-zero + tcs_unif_lvl :: IORef (Maybe TcLevel), + -- The Unification Level Flag + -- Outermost level at which we have unified a meta tyvar + -- Starts at Nothing, then (Just i), then (Just j) where j<i + -- See Note [The Unification Level Flag] + tcs_count :: IORef Int, -- Global step count tcs_inerts :: IORef InertSet, -- Current inert set @@ -2877,8 +2939,10 @@ runTcSWithEvBinds' restore_cycles ev_binds_var tcs ; step_count <- TcM.newTcRef 0 ; inert_var <- TcM.newTcRef emptyInert ; wl_var <- TcM.newTcRef emptyWorkList + ; unif_lvl_var <- TcM.newTcRef Nothing ; let env = TcSEnv { tcs_ev_binds = ev_binds_var , tcs_unified = unified_var + , tcs_unif_lvl = unif_lvl_var , tcs_count = step_count , tcs_inerts = inert_var , tcs_worklist = wl_var } @@ -2941,15 +3005,19 @@ nestImplicTcS ref inner_tclvl (TcS thing_inside) = TcS $ \ TcSEnv { tcs_unified = unified_var , tcs_inerts = old_inert_var , tcs_count = count + , tcs_unif_lvl = unif_lvl } -> do { inerts <- TcM.readTcRef old_inert_var - ; let nest_inert = inerts { inert_cycle_breakers = [] } - -- all other InertSet fields are inherited + ; let nest_inert = inerts { inert_cycle_breakers = [] + , inert_cans = (inert_cans inerts) + { inert_given_eqs = False } } + -- All other InertSet fields are inherited ; new_inert_var <- TcM.newTcRef nest_inert ; new_wl_var <- TcM.newTcRef emptyWorkList - ; let nest_env = TcSEnv { tcs_ev_binds = ref + ; let nest_env = TcSEnv { tcs_count = count -- Inherited + , tcs_unif_lvl = unif_lvl -- Inherited + , tcs_ev_binds = ref , tcs_unified = unified_var - , tcs_count = count , tcs_inerts = new_inert_var , tcs_worklist = new_wl_var } ; res <- TcM.setTcLevel inner_tclvl $ @@ -3262,6 +3330,97 @@ pprKicked n = parens (int n <+> text "kicked out") {- ********************************************************************* * * +* The Unification Level Flag * +* * +********************************************************************* -} + +{- Note [The Unification Level Flag] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider a deep tree of implication constraints + forall[1] a. -- Outer-implic + C alpha[1] -- Simple + forall[2] c. ....(C alpha[1]).... -- Implic-1 + forall[2] b. ....(alpha[1] ~ Int).... -- Implic-2 + +The (C alpha) is insoluble until we know alpha. We solve alpha +by unifying alpha:=Int somewhere deep inside Implic-2. But then we +must try to solve the Outer-implic all over again. This time we can +solve (C alpha) both in Outer-implic, and nested inside Implic-1. + +When should we iterate solving a level-n implication? +Answer: if any unification of a tyvar at level n takes place + in the ic_implics of that implication. + +* What if a unification takes place at level n-1? Then don't iterate + level n, because we'll iterate level n-1, and that will in turn iterate + level n. + +* What if a unification takes place at level n, in the ic_simples of + level n? No need to track this, because the kick-out mechanism deals + with it. (We can't drop kick-out in favour of iteration, becuase kick-out + works for skolem-equalities, not just unifications.) + +So the monad-global Unification Level Flag, kept in tcs_unif_lvl keeps +track of + - Whether any unifications at all have taken place (Nothing => no unifications) + - If so, what is the outermost level that has seen a unification (Just lvl) + +The iteration done in the simplify_loop/maybe_simplify_again loop in GHC.Tc.Solver. + +It helpful not to iterate unless there is a chance of progress. #8474 is +an example: + + * There's a deeply-nested chain of implication constraints. + ?x:alpha => ?y1:beta1 => ... ?yn:betan => [W] ?x:Int + + * From the innermost one we get a [D] alpha[1] ~ Int, + so we can unify. + + * It's better not to iterate the inner implications, but go all the + way out to level 1 before iterating -- because iterating level 1 + will iterate the inner levels anyway. + +(In the olden days when we "floated" thse Derived constraints, this was +much, much more important -- we got exponential behaviour, as each iteration +produced the same Derived constraint.) +-} + + +resetUnificationFlag :: TcS Bool +-- We are at ambient level i +-- If the unification flag = Just i, reset it to Nothing and return True +-- Otherwise leave it unchanged and return False +resetUnificationFlag + = TcS $ \env -> + do { let ref = tcs_unif_lvl env + ; ambient_lvl <- TcM.getTcLevel + ; mb_lvl <- TcM.readTcRef ref + ; TcM.traceTc "resetUnificationFlag" $ + vcat [ text "ambient:" <+> ppr ambient_lvl + , text "unif_lvl:" <+> ppr mb_lvl ] + ; case mb_lvl of + Nothing -> return False + Just unif_lvl | ambient_lvl `strictlyDeeperThan` unif_lvl + -> return False + | otherwise + -> do { TcM.writeTcRef ref Nothing + ; return True } } + +setUnificationFlag :: TcLevel -> TcS () +-- (setUnificationFlag i) sets the unification level to (Just i) +-- unless it already is (Just j) where j <= i +setUnificationFlag lvl + = TcS $ \env -> + do { let ref = tcs_unif_lvl env + ; mb_lvl <- TcM.readTcRef ref + ; case mb_lvl of + Just unif_lvl | lvl `deeperThanOrSame` unif_lvl + -> return () + _ -> TcM.writeTcRef ref (Just lvl) } + + +{- ********************************************************************* +* * * Instantiation etc. * * ********************************************************************* -} diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index 3950f1db77..6f58b6bf35 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -1095,7 +1095,7 @@ Yuk! data Implication = Implic { -- Invariants for a tree of implications: - -- see TcType Note [TcLevel and untouchable type variables] + -- see TcType Note [TcLevel invariants] ic_tclvl :: TcLevel, -- TcLevel of unification variables -- allocated /inside/ this implication @@ -1172,44 +1172,57 @@ data ImplicStatus | IC_Unsolved -- Neither of the above; might go either way --- | Does this implication have Given equalities? --- See Note [When does an implication have given equalities?] in GHC.Tc.Solver.Monad, --- which also explains why we need three options here. Also, see --- Note [Suppress redundant givens during error reporting] in GHC.Tc.Errors --- --- Stops floating | Suppresses Givens in errors --- ----------------------------------------------- --- NoGivenEqs NO | YES --- LocalGivenEqs NO | NO --- MaybeGivenEqs YES | NO --- --- Examples: --- --- NoGivenEqs: Eq a => ... --- (Show a, Num a) => ... --- forall a. a ~ Either Int Bool => ... --- See Note [Let-bound skolems] in GHC.Tc.Solver.Monad for --- that last one --- --- LocalGivenEqs: forall a b. F a ~ G b => ... --- forall a. F a ~ Int => ... --- --- MaybeGivenEqs: (a ~ b) => ... --- forall a. F a ~ b => ... --- --- The check is conservative. A MaybeGivenEqs might not have any equalities. --- A LocalGivenEqs might local equalities, but it definitely does not have non-local --- equalities. A NoGivenEqs definitely does not have equalities (except let-bound --- skolems). -data HasGivenEqs - = NoGivenEqs -- definitely no given equalities, - -- except by Note [Let-bound skolems] in GHC.Tc.Solver.Monad - | LocalGivenEqs -- might have Given equalities that affect only local skolems - -- e.g. forall a b. (a ~ F b) => ...; definitely no others - | MaybeGivenEqs -- might have any kind of Given equalities; no floating out - -- is possible. +data HasGivenEqs -- See Note [HasGivenEqs] + = NoGivenEqs -- Definitely no given equalities, + -- except by Note [Let-bound skolems] in GHC.Tc.Solver.Monad + | LocalGivenEqs -- Might have Given equalities, but only ones that affect only + -- local skolems e.g. forall a b. (a ~ F b) => ... + | MaybeGivenEqs -- Might have any kind of Given equalities; no floating out + -- is possible. deriving Eq +{- Note [HasGivenEqs] +~~~~~~~~~~~~~~~~~~~~~ +The GivenEqs data type describes the Given constraints of an implication constraint: + +* NoGivenEqs: definitely no Given equalities, except perhaps let-bound skolems + which don't count: see Note [Let-bound skolems] in GHC.Tc.Solver.Monad + Examples: forall a. Eq a => ... + forall a. (Show a, Num a) => ... + forall a. a ~ Either Int Bool => ... -- Let-bound skolem + +* LocalGivenEqs: definitely no Given equalities that would affect principal + types. But may have equalities that affect only skolems of this implication + (and hence do not affect princial types) + Examples: forall a. F a ~ Int => ... + forall a b. F a ~ G b => ... + +* MaybeGivenEqs: may have Given equalities that would affect principal + types + Examples: forall. (a ~ b) => ... + forall a. F a ~ b => ... + forall a. c a => ... -- The 'c' might be instantiated to (b ~) + forall a. C a b => .... + where class x~y => C a b + so there is an equality in the superclass of a Given + +The HasGivenEqs classifications affect two things: + +* Suppressing redundant givens during error reporting; see GHC.Tc.Errors + Note [Suppress redundant givens during error reporting] + +* Floating in approximateWC. + +Specifically, here's how it goes: + + Stops floating | Suppresses Givens in errors + in approximateWC | + ----------------------------------------------- + NoGivenEqs NO | YES + LocalGivenEqs NO | NO + MaybeGivenEqs YES | NO +-} + instance Outputable Implication where ppr (Implic { ic_tclvl = tclvl, ic_skols = skols , ic_given = given, ic_given_eqs = given_eqs diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs index 1b13d82869..9c0971aa42 100644 --- a/compiler/GHC/Tc/Utils/Env.hs +++ b/compiler/GHC/Tc/Utils/Env.hs @@ -692,8 +692,11 @@ tcCheckUsage name id_mult thing_inside -- -- It works nicely in practice. (promote_mult, _, _, _) = mapTyCo mapper - mapper = TyCoMapper { tcm_tyvar = \ () tv -> do { _ <- promoteTyVar tv - ; zonkTcTyVar tv } + mapper = TyCoMapper { tcm_tyvar = \ () tv -> if isMetaTyVar tv + then do { tclvl <- getTcLevel + ; _ <- promoteMetaTyVarTo tclvl tv + ; zonkTcTyVar tv } + else return (mkTyVarTy tv) , tcm_covar = \ () cv -> return (mkCoVarCo cv) , tcm_hole = \ () h -> return (mkHoleCo h) , tcm_tycobinder = \ () tcv _flag -> return ((), tcv) diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs index 5cb8ed8d88..240a836d72 100644 --- a/compiler/GHC/Tc/Utils/Monad.hs +++ b/compiler/GHC/Tc/Utils/Monad.hs @@ -1865,7 +1865,7 @@ It's distressingly delicate though: class constraints mentioned above. But we may /also/ end up taking constraints built at some inner level, and emitting them at some outer level, and then breaking the TcLevel invariants - See Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType + See Note [TcLevel invariants] in GHC.Tc.Utils.TcType So dropMisleading has a horridly ad-hoc structure. It keeps only /insoluble/ flat constraints (which are unlikely to very visibly trip diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 9ced918756..075c14a987 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -80,7 +80,7 @@ module GHC.Tc.Utils.TcMType ( --------------------------------- -- Promotion, defaulting, skolemisation - defaultTyVar, promoteTyVar, promoteTyVarSet, + defaultTyVar, promoteMetaTyVarTo, promoteTyVarSet, quantifyTyVars, isQuantifiableTv, skolemiseUnboundMetaTyVar, zonkAndSkolemise, skolemiseQuantifiedTyVar, @@ -964,12 +964,18 @@ writeMetaTyVarRef tyvar ref ty ; writeTcRef ref (Indirect ty) } -- Everything from here on only happens if DEBUG is on + -- Need to zonk 'ty' because we may only recently have promoted + -- its free meta-tyvars (see Solver.Interact.tryToSolveByUnification) | otherwise = do { meta_details <- readMutVar ref; -- Zonk kinds to allow the error check to work ; zonked_tv_kind <- zonkTcType tv_kind - ; zonked_ty_kind <- zonkTcType ty_kind - ; let kind_check_ok = tcIsConstraintKind zonked_tv_kind + ; zonked_ty <- zonkTcType ty + ; let zonked_ty_kind = tcTypeKind zonked_ty + zonked_ty_lvl = tcTypeLevel zonked_ty + level_check_ok = not (zonked_ty_lvl `strictlyDeeperThan` tv_lvl) + level_check_msg = ppr zonked_ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty + kind_check_ok = tcIsConstraintKind zonked_tv_kind || tcEqKind zonked_ty_kind zonked_tv_kind -- Hack alert! tcIsConstraintKind: see GHC.Tc.Gen.HsType -- Note [Extra-constraint holes in partial type signatures] @@ -994,13 +1000,9 @@ writeMetaTyVarRef tyvar ref ty ; writeMutVar ref (Indirect ty) } where tv_kind = tyVarKind tyvar - ty_kind = tcTypeKind ty tv_lvl = tcTyVarLevel tyvar - ty_lvl = tcTypeLevel ty - level_check_ok = not (ty_lvl `strictlyDeeperThan` tv_lvl) - level_check_msg = ppr ty_lvl $$ ppr tv_lvl $$ ppr tyvar $$ ppr ty double_upd_msg details = hang (text "Double update of meta tyvar") 2 (ppr tyvar $$ ppr details) @@ -1572,8 +1574,8 @@ than the ambient level (see Note [Use level numbers of quantification]). Note [Use level numbers for quantification] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The level numbers assigned to metavariables are very useful. Not only -do they track touchability (Note [TcLevel and untouchable type variables] -in GHC.Tc.Utils.TcType), but they also allow us to determine which variables to +do they track touchability (Note [TcLevel invariants] in GHC.Tc.Utils.TcType), +but they also allow us to determine which variables to generalise. The rule is this: When generalising, quantify only metavariables with a TcLevel greater @@ -2007,29 +2009,31 @@ a \/\a in the final result but all the occurrences of a will be zonked to () * * ********************************************************************* -} -promoteTyVar :: TcTyVar -> TcM Bool +promoteMetaTyVarTo :: TcLevel -> TcTyVar -> TcM Bool -- When we float a constraint out of an implication we must restore --- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType +-- invariant (WantedInv) in Note [TcLevel invariants] in GHC.Tc.Utils.TcType -- Return True <=> we did some promotion -- Also returns either the original tyvar (no promotion) or the new one -- See Note [Promoting unification variables] -promoteTyVar tv - = do { tclvl <- getTcLevel - ; if (isFloatedTouchableMetaTyVar tclvl tv) - then do { cloned_tv <- cloneMetaTyVar tv - ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl - ; writeMetaTyVar tv (mkTyVarTy rhs_tv) - ; traceTc "promoteTyVar" (ppr tv <+> text "-->" <+> ppr rhs_tv) - ; return True } - else do { traceTc "promoteTyVar: no" (ppr tv) - ; return False } } +promoteMetaTyVarTo tclvl tv + | ASSERT2( isMetaTyVar tv, ppr tv ) + tcTyVarLevel tv `strictlyDeeperThan` tclvl + = do { cloned_tv <- cloneMetaTyVar tv + ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl + ; writeMetaTyVar tv (mkTyVarTy rhs_tv) + ; traceTc "promoteTyVar" (ppr tv <+> text "-->" <+> ppr rhs_tv) + ; return True } + | otherwise + = return False -- Returns whether or not *any* tyvar is defaulted promoteTyVarSet :: TcTyVarSet -> TcM Bool promoteTyVarSet tvs - = do { bools <- mapM promoteTyVar (nonDetEltsUniqSet tvs) + = do { tclvl <- getTcLevel + ; bools <- mapM (promoteMetaTyVarTo tclvl) $ + filter isPromotableMetaTyVar $ + nonDetEltsUniqSet tvs -- Non-determinism is OK because order of promotion doesn't matter - ; return (or bools) } diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 6e4eea8f19..942bdd979a 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -33,7 +33,7 @@ module GHC.Tc.Utils.TcType ( -- TcLevel TcLevel(..), topTcLevel, pushTcLevel, isTopTcLevel, - strictlyDeeperThan, sameDepthAs, + strictlyDeeperThan, deeperThanOrSame, sameDepthAs, tcTypeLevel, tcTyVarLevel, maxTcLevel, promoteSkolem, promoteSkolemX, promoteSkolemsX, -------------------------------- @@ -45,8 +45,7 @@ module GHC.Tc.Utils.TcType ( isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo, isFlexi, isIndirect, isRuntimeUnkSkol, metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe, - isTouchableMetaTyVar, - isFloatedTouchableMetaTyVar, + isTouchableMetaTyVar, isPromotableMetaTyVar, findDupTyVarTvs, mkTyVarNamePairs, -------------------------------- @@ -516,7 +515,7 @@ data TcTyVarDetails | MetaTv { mtv_info :: MetaInfo , mtv_ref :: IORef MetaDetails - , mtv_tclvl :: TcLevel } -- See Note [TcLevel and untouchable type variables] + , mtv_tclvl :: TcLevel } -- See Note [TcLevel invariants] vanillaSkolemTv, superSkolemTv :: TcTyVarDetails -- See Note [Binding when looking up instances] in GHC.Core.InstEnv @@ -574,13 +573,14 @@ instance Outputable MetaInfo where ********************************************************************* -} newtype TcLevel = TcLevel Int deriving( Eq, Ord ) - -- See Note [TcLevel and untouchable type variables] for what this Int is + -- See Note [TcLevel invariants] for what this Int is -- See also Note [TcLevel assignment] {- -Note [TcLevel and untouchable type variables] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [TcLevel invariants] +~~~~~~~~~~~~~~~~~~~~~~~~~ * Each unification variable (MetaTv) + and skolem (SkolemTv) and each Implication has a level number (of type TcLevel) @@ -602,9 +602,8 @@ Note [TcLevel and untouchable type variables] LESS THAN OR EQUAL TO the ic_tclvl of I See Note [WantedInv] -* A unification variable is *touchable* if its level number - is EQUAL TO that of its immediate parent implication, - and it is a TauTv or TyVarTv (but /not/ CycleBreakerTv) +The level of a MetaTyVar also governs its untouchability. See +Note [Unification preconditions] in GHC.Tc.Utils.Unify. Note [WantedInv] ~~~~~~~~~~~~~~~~ @@ -679,13 +678,17 @@ strictlyDeeperThan :: TcLevel -> TcLevel -> Bool strictlyDeeperThan (TcLevel tv_tclvl) (TcLevel ctxt_tclvl) = tv_tclvl > ctxt_tclvl +deeperThanOrSame :: TcLevel -> TcLevel -> Bool +deeperThanOrSame (TcLevel tv_tclvl) (TcLevel ctxt_tclvl) + = tv_tclvl >= ctxt_tclvl + sameDepthAs :: TcLevel -> TcLevel -> Bool sameDepthAs (TcLevel ctxt_tclvl) (TcLevel tv_tclvl) = ctxt_tclvl == tv_tclvl -- NB: invariant ctxt_tclvl >= tv_tclvl -- So <= would be equivalent checkTcLevelInvariant :: TcLevel -> TcLevel -> Bool --- Checks (WantedInv) from Note [TcLevel and untouchable type variables] +-- Checks (WantedInv) from Note [TcLevel invariants] checkTcLevelInvariant (TcLevel ctxt_tclvl) (TcLevel tv_tclvl) = ctxt_tclvl >= tv_tclvl @@ -998,6 +1001,16 @@ tcIsTcTyVar :: TcTyVar -> Bool -- See Note [TcTyVars and TyVars in the typechecker] tcIsTcTyVar tv = isTyVar tv +isPromotableMetaTyVar :: TcTyVar -> Bool +-- True is this is a meta-tyvar that can be +-- promoted to an outer level +isPromotableMetaTyVar tv + | isTyVar tv -- See Note [Coercion variables in free variable lists] + , MetaTv { mtv_info = info } <- tcTyVarDetails tv + = isTouchableInfo info -- Can't promote cycle breakers + | otherwise + = False + isTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool isTouchableMetaTyVar ctxt_tclvl tv | isTyVar tv -- See Note [Coercion variables in free variable lists] @@ -1009,15 +1022,6 @@ isTouchableMetaTyVar ctxt_tclvl tv | otherwise = False -isFloatedTouchableMetaTyVar :: TcLevel -> TcTyVar -> Bool -isFloatedTouchableMetaTyVar ctxt_tclvl tv - | isTyVar tv -- See Note [Coercion variables in free variable lists] - , MetaTv { mtv_tclvl = tv_tclvl, mtv_info = info } <- tcTyVarDetails tv - , isTouchableInfo info - = tv_tclvl `strictlyDeeperThan` ctxt_tclvl - - | otherwise = False - isImmutableTyVar :: TyVar -> Bool isImmutableTyVar tv = isSkolemTyVar tv diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index f0cf431ff5..892ab050d5 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -37,7 +37,7 @@ module GHC.Tc.Utils.Unify ( matchExpectedFunKind, matchActualFunTySigma, matchActualFunTysRho, - metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..), + occCheckForErrors, CheckTyEqResult(..), checkTyVarEq, checkTyFamEq, checkTypeEq, AreTypeFamiliesOK(..) ) where @@ -78,6 +78,7 @@ import GHC.Utils.Panic import GHC.Exts ( inline ) import Control.Monad import Control.Arrow ( second ) +import qualified Data.Semigroup as S {- ********************************************************************* @@ -1170,17 +1171,17 @@ uType t_or_k origin orig_ty1 orig_ty2 -- so that type variables tend to get filled in with -- the most informative version of the type go (TyVarTy tv1) ty2 - = do { lookup_res <- lookupTcTyVar tv1 + = do { lookup_res <- isFilledMetaTyVar_maybe tv1 ; case lookup_res of - Filled ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1) - ; go ty1 ty2 } - Unfilled _ -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 } + Just ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1) + ; go ty1 ty2 } + Nothing -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 } go ty1 (TyVarTy tv2) - = do { lookup_res <- lookupTcTyVar tv2 + = do { lookup_res <- isFilledMetaTyVar_maybe tv2 ; case lookup_res of - Filled ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2) - ; go ty1 ty2 } - Unfilled _ -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 } + Just ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2) + ; go ty1 ty2 } + Nothing -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 } -- See Note [Expanding synonyms during unification] go ty1@(TyConApp tc1 []) (TyConApp tc2 []) @@ -1434,10 +1435,12 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 ; go dflags cur_lvl } where go dflags cur_lvl - | canSolveByUnification cur_lvl tv1 ty2 + | isTouchableMetaTyVar cur_lvl tv1 + -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles + , canSolveByUnification (metaTyVarInfo tv1) ty2 + , CTE_OK <- checkTyVarEq dflags NoTypeFamilies tv1 ty2 -- See Note [Prevent unification with type families] about the NoTypeFamilies: - , MTVU_OK ty2' <- metaTyVarUpdateOK dflags NoTypeFamilies tv1 ty2 - = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2') (tyVarKind tv1) + = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2) (tyVarKind tv1) ; traceTc "uUnfilledVar2 ok" $ vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) , ppr ty2 <+> dcolon <+> ppr (tcTypeKind ty2) @@ -1447,8 +1450,8 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 -- Only proceed if the kinds match -- NB: tv1 should still be unfilled, despite the kind unification -- because tv1 is not free in ty2 (or, hence, in its kind) - then do { writeMetaTyVar tv1 ty2' - ; return (mkTcNomReflCo ty2') } + then do { writeMetaTyVar tv1 ty2 + ; return (mkTcNomReflCo ty2) } else defer } -- This cannot be solved now. See GHC.Tc.Solver.Canonical -- Note [Equalities with incompatible kinds] @@ -1465,6 +1468,22 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2 +canSolveByUnification :: MetaInfo -> TcType -> Bool +-- See Note [Unification preconditions, (TYVAR-TV)] +canSolveByUnification info xi + = case info of + CycleBreakerTv -> False + TyVarTv -> case tcGetTyVar_maybe xi of + Nothing -> False + Just tv -> case tcTyVarDetails tv of + MetaTv { mtv_info = info } + -> case info of + TyVarTv -> True + _ -> False + SkolemTv {} -> True + RuntimeUnk -> True + _ -> True + swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool swapOverTyVars is_given tv1 tv2 -- See Note [Unification variables on the left] @@ -1508,8 +1527,94 @@ lhsPriority tv TauTv -> 2 RuntimeUnkTv -> 3 -{- Note [TyVar/TyVar orientation] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Unification preconditions] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Question: given a homogeneous equality (alpha ~# ty), when is it OK to +unify alpha := ty? + +This note only applied to /homogeneous/ equalities, in which both +sides have the same kind. + +There are three reasons not to unify: + +1. (SKOL-ESC) Skolem-escape + Consider the constraint + forall[2] a[2]. alpha[1] ~ Maybe a[2] + If we unify alpha := Maybe a, the skolem 'a' may escape its scope. + The level alpha[1] says that alpha may be used outside this constraint, + where 'a' is not in scope at all. So we must not unify. + + Bottom line: when looking at a constraint alpha[n] := ty, do not unify + if any free variable of 'ty' has level deeper (greater) than n + +2. (UNTOUCHABLE) Untouchable unification variables + Consider the constraint + forall[2] a[2]. b[1] ~ Int => alpha[1] ~ Int + There is no (SKOL-ESC) problem with unifying alpha := Int, but it might + not be the principal solution. Perhaps the "right" solution is alpha := b. + We simply can't tell. See "OutsideIn(X): modular type inference with local + assumptions", section 2.2. We say that alpha[1] is "untouchable" inside + this implication. + + Bottom line: at amibient level 'l', when looking at a constraint + alpha[n] ~ ty, do not unify alpha := ty if there are any given equalities + between levels 'n' and 'l'. + + Exactly what is a "given equality" for the purpose of (UNTOUCHABLE)? + Answer: see Note [Tracking Given equalities] in GHC.Tc.Solver.Monad + +3. (TYVAR-TV) Unifying TyVarTvs and CycleBreakerTvs + This precondition looks at the MetaInfo of the unification variable: + + * TyVarTv: When considering alpha{tyv} ~ ty, if alpha{tyv} is a + TyVarTv it can only unify with a type variable, not with a + structured type. So if 'ty' is a structured type, such as (Maybe x), + don't unify. + + * CycleBreakerTv: never unified, except by restoreTyVarCycles. + + +Needless to say, all three have wrinkles: + +* (SKOL-ESC) Promotion. Given alpha[n] ~ ty, what if beta[k] is free + in 'ty', where beta is a unification variable, and k>n? 'beta' + stands for a monotype, and since it is part of a level-n type + (equal to alpha[n]), we must /promote/ beta to level n. Just make + up a fresh gamma[n], and unify beta[k] := gamma[n]. + +* (TYVAR-TV) Unification variables. Suppose alpha[tyv,n] is a level-n + TyVarTv (see Note [Signature skolems] in GHC.Tc.Types.TcType)? Now + consider alpha[tyv,n] ~ Bool. We don't want to unify because that + would break the TyVarTv invariant. + + What about alpha[tyv,n] ~ beta[tau,n], where beta is an ordinary + TauTv? Again, don't unify, because beta might later be unified + with, say Bool. (If levels permit, we reverse the orientation here; + see Note [TyVar/TyVar orientation].) + +* (UNTOUCHABLE) Untouchability. When considering (alpha[n] ~ ty), how + do we know whether there are any given equalities between level n + and the ambient level? We answer in two ways: + + * In the eager unifier, we only unify if l=n. If not, alpha may be + untouchable, and defer to the constraint solver. This check is + made in GHC.Tc.Utils.uUnifilledVar2, in the guard + isTouchableMetaTyVar. + + * In the constraint solver, we track where Given equalities occur + and use that to guard unification in GHC.Tc.Solver.Canonical.unifyTest + More details in Note [Tracking Given equalities] in GHC.Tc.Solver.Monad + + Historical note: in the olden days (pre 2021) the constraint solver + also used to unify only if l=n. Equalities were "floated" out of the + implication in a separate step, so that they would become touchable. + But the float/don't-float question turned out to be very delicate, + as you can see if you look at the long series of Notes associated with + GHC.Tc.Solver.floatEqualities, around Nov 2020. It's much easier + to unify in-place, with no floating. + +Note [TyVar/TyVar orientation] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Given (a ~ b), should we orient the CEqCan as (a~b) or (b~a)? This is a surprisingly tricky question! This is invariant (TyEq:TV). @@ -1617,8 +1722,8 @@ inert guy, so we get inert item: c ~ a And now the cycle just repeats -Note [Eliminate younger unification variables] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Historical Note [Eliminate younger unification variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Given a choice of unifying alpha := beta or beta := alpha we try, if possible, to eliminate the "younger" one, as determined @@ -1632,36 +1737,11 @@ This is a performance optimisation only. It turns out to fix It's simple to implement (see nicer_to_update_tv2 in swapOverTyVars). But, to my surprise, it didn't seem to make any significant difference to the compiler's performance, so I didn't take it any further. Still -it seemed to too nice to discard altogether, so I'm leaving these +it seemed too nice to discard altogether, so I'm leaving these notes. SLPJ Jan 18. --} --- @trySpontaneousSolve wi@ solves equalities where one side is a --- touchable unification variable. --- Returns True <=> spontaneous solve happened -canSolveByUnification :: TcLevel -> TcTyVar -> TcType -> Bool -canSolveByUnification tclvl tv xi - | isTouchableMetaTyVar tclvl tv - = case metaTyVarInfo tv of - TyVarTv -> is_tyvar xi - _ -> True - - | otherwise -- Untouchable - = False - where - is_tyvar xi - = case tcGetTyVar_maybe xi of - Nothing -> False - Just tv -> case tcTyVarDetails tv of - MetaTv { mtv_info = info } - -> case info of - TyVarTv -> True - _ -> False - SkolemTv {} -> True - RuntimeUnk -> True - -{- Note [Prevent unification with type families] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Prevent unification with type families] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We prevent unification with type families because of an uneasy compromise. It's perfectly sound to unify with type families, and it even improves the error messages in the testsuite. It also modestly improves performance, at @@ -1765,35 +1845,6 @@ type-checking (with wrappers, etc.). Types get desugared very differently, causing this wibble in behavior seen here. -} -data LookupTyVarResult -- The result of a lookupTcTyVar call - = Unfilled TcTyVarDetails -- SkolemTv or virgin MetaTv - | Filled TcType - -lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult -lookupTcTyVar tyvar - | MetaTv { mtv_ref = ref } <- details - = do { meta_details <- readMutVar ref - ; case meta_details of - Indirect ty -> return (Filled ty) - Flexi -> do { is_touchable <- isTouchableTcM tyvar - -- Note [Unifying untouchables] - ; if is_touchable then - return (Unfilled details) - else - return (Unfilled vanillaSkolemTv) } } - | otherwise - = return (Unfilled details) - where - details = tcTyVarDetails tyvar - -{- -Note [Unifying untouchables] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We treat an untouchable type variable as if it was a skolem. That -ensures it won't unify with anything. It's a slight hack, because -we return a made-up TcTyVarDetails, but I think it works smoothly. --} - -- | Breaks apart a function kind into its pieces. matchExpectedFunKind :: Outputable fun @@ -1872,44 +1923,38 @@ with (forall k. k->*) -} -data MetaTyVarUpdateResult a - = MTVU_OK a - | MTVU_Bad -- Forall, predicate, or type family - | MTVU_HoleBlocker -- Blocking coercion hole +data CheckTyEqResult + = CTE_OK + | CTE_Bad -- Forall, predicate, or type family + | CTE_HoleBlocker -- Blocking coercion hole -- See Note [Equalities with incompatible kinds] in "GHC.Tc.Solver.Canonical" - | MTVU_Occurs - deriving (Functor) - -instance Applicative MetaTyVarUpdateResult where - pure = MTVU_OK - (<*>) = ap - -instance Monad MetaTyVarUpdateResult where - MTVU_OK x >>= k = k x - MTVU_Bad >>= _ = MTVU_Bad - MTVU_HoleBlocker >>= _ = MTVU_HoleBlocker - MTVU_Occurs >>= _ = MTVU_Occurs - -instance Outputable a => Outputable (MetaTyVarUpdateResult a) where - ppr (MTVU_OK a) = text "MTVU_OK" <+> ppr a - ppr MTVU_Bad = text "MTVU_Bad" - ppr MTVU_HoleBlocker = text "MTVU_HoleBlocker" - ppr MTVU_Occurs = text "MTVU_Occurs" - -occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult () --- Just for error-message generation; so we return MetaTyVarUpdateResult + | CTE_Occurs + +instance S.Semigroup CheckTyEqResult where + CTE_OK <> x = x + x <> _ = x + +instance Monoid CheckTyEqResult where + mempty = CTE_OK + +instance Outputable CheckTyEqResult where + ppr CTE_OK = text "CTE_OK" + ppr CTE_Bad = text "CTE_Bad" + ppr CTE_HoleBlocker = text "CTE_HoleBlocker" + ppr CTE_Occurs = text "CTE_Occurs" + +occCheckForErrors :: DynFlags -> TcTyVar -> Type -> CheckTyEqResult +-- Just for error-message generation; so we return CheckTyEqResult -- so the caller can report the right kind of error -- Check whether -- 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 checkTyVarEq dflags YesTypeFamilies tv ty of - MTVU_OK _ -> MTVU_OK () - MTVU_Bad -> MTVU_Bad - MTVU_HoleBlocker -> MTVU_HoleBlocker - MTVU_Occurs -> case occCheckExpand [tv] ty of - Nothing -> MTVU_Occurs - Just _ -> MTVU_OK () + CTE_Occurs -> case occCheckExpand [tv] ty of + Nothing -> CTE_Occurs + Just _ -> CTE_OK + other -> other ---------------- data AreTypeFamiliesOK = YesTypeFamilies @@ -1920,52 +1965,7 @@ instance Outputable AreTypeFamiliesOK where ppr YesTypeFamilies = text "YesTypeFamilies" ppr NoTypeFamilies = text "NoTypeFamilies" -metaTyVarUpdateOK :: DynFlags - -> AreTypeFamiliesOK -- allow type families in RHS? - -> TcTyVar -- tv :: k1 - -> TcType -- ty :: k2 - -> MetaTyVarUpdateResult TcType -- possibly-expanded ty --- (metaTyVarUpdateOK tv ty) --- Checks that the equality tv~ty is OK to be used to rewrite --- other equalities. Equivalently, checks the conditions for CEqCan --- (a) that tv doesn't occur in ty (occurs check) --- (b) that ty does not have any foralls or (perhaps) 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] --- (2) Return Nothing, --- [the update might be dodgy] --- --- Note that "Nothing" does not mean "definite error". For example --- type family F a --- type instance F Int = Int --- consider --- a ~ F a --- This is perfectly reasonable, if we later get a ~ Int. For now, though, --- we return Nothing, leaving it to the later constraint simplifier to --- sort matters out. --- --- See Note [Refactoring hazard: metaTyVarUpdateOK] - -metaTyVarUpdateOK dflags ty_fam_ok tv ty - = case checkTyVarEq dflags ty_fam_ok tv ty of - MTVU_OK _ -> MTVU_OK ty - MTVU_Bad -> MTVU_Bad -- forall, predicate, type function - MTVU_HoleBlocker -> MTVU_HoleBlocker -- coercion hole - MTVU_Occurs -> case occCheckExpand [tv] ty of - Just expanded_ty -> MTVU_OK expanded_ty - Nothing -> MTVU_Occurs - -checkTyVarEq :: DynFlags -> AreTypeFamiliesOK -> TcTyVar -> TcType -> MetaTyVarUpdateResult () +checkTyVarEq :: DynFlags -> AreTypeFamiliesOK -> TcTyVar -> TcType -> CheckTyEqResult checkTyVarEq dflags ty_fam_ok tv ty = inline checkTypeEq dflags ty_fam_ok (TyVarLHS tv) ty -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away @@ -1974,13 +1974,13 @@ checkTyFamEq :: DynFlags -> TyCon -- type function -> [TcType] -- args, exactly saturated -> TcType -- RHS - -> MetaTyVarUpdateResult () + -> CheckTyEqResult checkTyFamEq dflags fun_tc fun_args ty = inline checkTypeEq dflags YesTypeFamilies (TyFamLHS fun_tc fun_args) ty -- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away checkTypeEq :: DynFlags -> AreTypeFamiliesOK -> CanEqLHS -> TcType - -> MetaTyVarUpdateResult () + -> CheckTyEqResult -- Checks the invariants for CEqCan. In particular: -- (a) a forall type (forall a. blah) -- (b) a predicate type (c => ty) @@ -1988,6 +1988,14 @@ checkTypeEq :: DynFlags -> AreTypeFamiliesOK -> CanEqLHS -> TcType -- (d) a blocking coercion hole -- (e) an occurrence of the LHS (occurs check) -- +-- Note that an occurs-check does not mean "definite error". For example +-- type family F a +-- type instance F Int = Int +-- consider +-- b0 ~ F b0 +-- This is perfectly reasonable, if we later get b0 ~ Int. But we +-- certainly can't unify b0 := F b0 +-- -- For (a), (b), and (c) we check only the top level of the type, NOT -- inside the kinds of variables it mentions. For (d) we look deeply -- in coercions when the LHS is a tyvar (but skip coercions for type family @@ -1995,14 +2003,11 @@ checkTypeEq :: DynFlags -> AreTypeFamiliesOK -> CanEqLHS -> TcType -- -- checkTypeEq is called from -- * checkTyFamEq, checkTyVarEq (which inline it to specialise away the --- case-analysis on 'lhs' +-- case-analysis on 'lhs') -- * checkEqCanLHSFinish, which does not know the form of 'lhs' checkTypeEq dflags ty_fam_ok lhs ty = go ty where - 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 @@ -2015,71 +2020,70 @@ checkTypeEq dflags ty_fam_ok lhs ty | otherwise = False - go :: TcType -> MetaTyVarUpdateResult () + go :: TcType -> CheckTyEqResult go (TyVarTy tv') = go_tv tv' go (TyConApp tc tys) = go_tc tc tys - go (LitTy {}) = ok + go (LitTy {}) = CTE_OK go (FunTy{ft_af = af, ft_mult = w, ft_arg = a, ft_res = r}) | InvisArg <- af - , not ghci_tv = MTVU_Bad - | otherwise = go w >> go a >> go r - go (AppTy fun arg) = go fun >> go arg - go (CastTy ty co) = go ty >> go_co co + , not ghci_tv = CTE_Bad + | otherwise = go w S.<> go a S.<> go r + go (AppTy fun arg) = go fun S.<> go arg + go (CastTy ty co) = go ty S.<> go_co co go (CoercionTy co) = go_co co go (ForAllTy (Bndr tv' _) ty) - | not ghci_tv = MTVU_Bad + | not ghci_tv = CTE_Bad | otherwise = case lhs of - TyVarLHS tv | tv == tv' -> ok - | otherwise -> do { go_occ tv (tyVarKind tv') - ; go ty } + TyVarLHS tv | tv == tv' -> CTE_OK + | otherwise -> go_occ tv (tyVarKind tv') S.<> go ty _ -> go ty - go_tv :: TcTyVar -> MetaTyVarUpdateResult () + go_tv :: TcTyVar -> CheckTyEqResult -- this slightly peculiar way of defining this means -- we don't have to evaluate this `case` at every variable -- occurrence go_tv = case lhs of TyVarLHS tv -> \ tv' -> if tv == tv' - then MTVU_Occurs + then CTE_Occurs else go_occ tv (tyVarKind tv') - TyFamLHS {} -> \ _tv' -> ok + TyFamLHS {} -> \ _tv' -> CTE_OK -- See Note [Occurrence checking: look inside kinds] in GHC.Core.Type -- For kinds, we only do an occurs check; we do not worry -- about type families or foralls -- See Note [Checking for foralls] - go_occ tv k | tv `elemVarSet` tyCoVarsOfType k = MTVU_Occurs - | otherwise = ok + go_occ tv k | tv `elemVarSet` tyCoVarsOfType k = CTE_Occurs + | otherwise = CTE_OK - go_tc :: TyCon -> [TcType] -> MetaTyVarUpdateResult () + go_tc :: TyCon -> [TcType] -> CheckTyEqResult -- this slightly peculiar way of defining this means -- we don't have to evaluate this `case` at every tyconapp go_tc = case lhs of TyVarLHS {} -> \ tc tys -> - if | good_tc tc -> mapM go tys >> ok - | otherwise -> MTVU_Bad + if | good_tc tc -> mconcat (map go tys) + | otherwise -> CTE_Bad TyFamLHS fam_tc fam_args -> \ tc tys -> - if | tcEqTyConApps fam_tc fam_args tc tys -> MTVU_Occurs - | good_tc tc -> mapM go tys >> ok - | otherwise -> MTVU_Bad + if | tcEqTyConApps fam_tc fam_args tc tys -> CTE_Occurs + | good_tc tc -> mconcat (map go tys) + | otherwise -> CTE_Bad -- no bother about impredicativity in coercions, as they're -- inferred go_co co | not (gopt Opt_DeferTypeErrors dflags) , hasCoercionHoleCo co - = MTVU_HoleBlocker -- Wrinkle (2) in GHC.Tc.Solver.Canonical + = CTE_HoleBlocker -- Wrinkle (2) in GHC.Tc.Solver.Canonical -- See GHC.Tc.Solver.Canonical Note [Equalities with incompatible kinds] -- Wrinkle (2) about this case in general, Wrinkle (4b) about the check for -- deferred type errors. | TyVarLHS tv <- lhs , tv `elemVarSet` tyCoVarsOfCo co - = MTVU_Occurs + = CTE_Occurs -- Don't check coercions for type families; see commentary at top of function | otherwise - = ok + = CTE_OK good_tc :: TyCon -> Bool good_tc diff --git a/testsuite/tests/ghci.debugger/scripts/break012.stdout b/testsuite/tests/ghci.debugger/scripts/break012.stdout index 2e86b42713..5d478ae04e 100644 --- a/testsuite/tests/ghci.debugger/scripts/break012.stdout +++ b/testsuite/tests/ghci.debugger/scripts/break012.stdout @@ -1,14 +1,14 @@ Stopped in Main.g, break012.hs:5:10-18 -_result :: (p, a1 -> a1, (), a -> a -> a) = _ -a :: p = _ -b :: a2 -> a2 = _ +_result :: (a1, a2 -> a2, (), a -> a -> a) = _ +a :: a1 = _ +b :: a3 -> a3 = _ c :: () = _ d :: a -> a -> a = _ -a :: p -b :: a2 -> a2 +a :: a1 +b :: a3 -> a3 c :: () d :: a -> a -> a -a = (_t1::p) -b = (_t2::a2 -> a2) +a = (_t1::a1) +b = (_t2::a3 -> a3) c = (_t3::()) d = (_t4::a -> a -> a) diff --git a/testsuite/tests/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr index 1a7162d612..f3b6343893 100644 --- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr +++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr @@ -14,35 +14,18 @@ T10403.hs:15:12: warning: [-Wpartial-type-signatures (in -Wdefault)] • In the type signature: h1 :: _ => _ T10403.hs:19:7: warning: [-Wpartial-type-signatures (in -Wdefault)] - • Found type wildcard ‘_’ standing for ‘(a -> a1) -> f0 a -> H f0’ - Where: ‘f0’ is an ambiguous type variable + • Found type wildcard ‘_’ + standing for ‘(a -> a1) -> B t0 a -> H (B t0)’ + Where: ‘t0’ is an ambiguous type variable ‘a1’, ‘a’ are rigid type variables bound by - the inferred type of h2 :: (a -> a1) -> f0 a -> H f0 + the inferred type of h2 :: (a -> a1) -> B t0 a -> H (B t0) at T10403.hs:22:1-41 • In the type signature: h2 :: _ -T10403.hs:22:15: warning: [-Wdeferred-type-errors (in -Wdefault)] - • Ambiguous type variable ‘f0’ arising from a use of ‘fmap’ - prevents the constraint ‘(Functor f0)’ from being solved. - Relevant bindings include - b :: f0 a (bound at T10403.hs:22:6) - h2 :: (a -> a1) -> f0 a -> H f0 (bound at T10403.hs:22:1) - Probable fix: use a type annotation to specify what ‘f0’ should be. - These potential instances exist: - instance Functor IO -- Defined in ‘GHC.Base’ - instance Functor (B t) -- Defined at T10403.hs:10:10 - instance Functor I -- Defined at T10403.hs:6:10 - ...plus five others - ...plus two instances involving out-of-scope types - (use -fprint-potential-instances to see them all) - • In the second argument of ‘(.)’, namely ‘fmap (const ())’ - In the expression: (H . fmap (const ())) (fmap f b) - In an equation for ‘h2’: h2 f b = (H . fmap (const ())) (fmap f b) - T10403.hs:28:8: warning: [-Wdeferred-type-errors (in -Wdefault)] - • Couldn't match type ‘f0’ with ‘B t’ + • Couldn't match type ‘t0’ with ‘t’ Expected: H (B t) - Actual: H f0 + Actual: H (B t0) because type variable ‘t’ would escape its scope This (rigid, skolem) type variable is bound by the type signature for: diff --git a/testsuite/tests/partial-sigs/should_compile/T14715.stderr b/testsuite/tests/partial-sigs/should_compile/T14715.stderr index e352f0d644..4d3a668241 100644 --- a/testsuite/tests/partial-sigs/should_compile/T14715.stderr +++ b/testsuite/tests/partial-sigs/should_compile/T14715.stderr @@ -1,12 +1,11 @@ T14715.hs:13:53: warning: [-Wpartial-type-signatures (in -Wdefault)] - • Found extra-constraints wildcard standing for - ‘Reduce (LiftOf zq) zq’ - Where: ‘zq’ is a rigid type variable bound by + • 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 (LiftOf zq) zq) => + bench_mulPublic :: (z ~ LiftOf zq, Reduce z zq) => Cyc zp -> Cyc z -> IO (zp, zq) - at T14715.hs:13:32-33 + at T14715.hs:13:27-33 • In the type signature: - bench_mulPublic :: forall z zp zq. - (z ~ LiftOf zq, _) => Cyc zp -> Cyc z -> IO (zp, zq) + bench_mulPublic :: forall z zp zq. (z ~ LiftOf zq, _) => + Cyc zp -> Cyc z -> IO (zp, zq) diff --git a/testsuite/tests/partial-sigs/should_fail/ScopedNamedWildcardsBad.stderr b/testsuite/tests/partial-sigs/should_fail/ScopedNamedWildcardsBad.stderr index 713bdc65c3..ee618dff56 100644 --- a/testsuite/tests/partial-sigs/should_fail/ScopedNamedWildcardsBad.stderr +++ b/testsuite/tests/partial-sigs/should_fail/ScopedNamedWildcardsBad.stderr @@ -1,6 +1,11 @@ -ScopedNamedWildcardsBad.hs:8:21: error: +ScopedNamedWildcardsBad.hs:11:15: error: • Couldn't match expected type ‘Bool’ with actual type ‘Char’ - • In the first argument of ‘not’, namely ‘x’ - In the expression: not x - In an equation for ‘v’: v = not x + • In the first argument of ‘g’, namely ‘'x'’ + In the expression: g 'x' + In the expression: + let + v = not x + g :: _a -> _a + g x = x + in (g 'x') diff --git a/testsuite/tests/typecheck/should_fail/ExpandSynsFail2.stderr b/testsuite/tests/typecheck/should_fail/ExpandSynsFail2.stderr index 24aca978e3..5aae6fea45 100644 --- a/testsuite/tests/typecheck/should_fail/ExpandSynsFail2.stderr +++ b/testsuite/tests/typecheck/should_fail/ExpandSynsFail2.stderr @@ -1,6 +1,6 @@ ExpandSynsFail2.hs:19:37: error: - • Couldn't match type ‘Int’ with ‘Bool’ + • Couldn't match type ‘Bool’ with ‘Int’ Expected: ST s Foo Actual: MyBarST s Type synonyms expanded: diff --git a/testsuite/tests/typecheck/should_fail/T7453.stderr b/testsuite/tests/typecheck/should_fail/T7453.stderr index 224f5b90fe..53cbe52420 100644 --- a/testsuite/tests/typecheck/should_fail/T7453.stderr +++ b/testsuite/tests/typecheck/should_fail/T7453.stderr @@ -1,6 +1,8 @@ -T7453.hs:10:30: error: - • Couldn't match expected type ‘t’ with actual type ‘p’ +T7453.hs:9:15: error: + • Couldn't match type ‘t’ with ‘p’ + Expected: Id t + Actual: Id p ‘t’ is a rigid type variable bound by the type signature for: z :: forall t. Id t @@ -8,17 +10,29 @@ T7453.hs:10:30: error: ‘p’ is a rigid type variable bound by the inferred type of cast1 :: p -> a at T7453.hs:(7,1)-(10,30) - • In the first argument of ‘Id’, namely ‘v’ - In the expression: Id v - In an equation for ‘aux’: aux = Id v + • In the expression: aux + In an equation for ‘z’: + z = aux + where + aux = Id v + In an equation for ‘cast1’: + cast1 v + = runId z + where + z :: Id t + z = aux + where + aux = Id v • Relevant bindings include - aux :: Id t (bound at T7453.hs:10:21) + aux :: Id p (bound at T7453.hs:10:21) z :: Id t (bound at T7453.hs:9:11) v :: p (bound at T7453.hs:7:7) cast1 :: p -> a (bound at T7453.hs:7:1) -T7453.hs:16:33: error: - • Couldn't match expected type ‘t1’ with actual type ‘p’ +T7453.hs:15:15: error: + • Couldn't match type ‘t1’ with ‘p’ + Expected: () -> t1 + Actual: () -> p ‘t1’ is a rigid type variable bound by the type signature for: z :: forall t1. () -> t1 @@ -26,11 +40,21 @@ T7453.hs:16:33: error: ‘p’ is a rigid type variable bound by the inferred type of cast2 :: p -> t at T7453.hs:(13,1)-(16,33) - • In the first argument of ‘const’, namely ‘v’ - In the expression: const v - In an equation for ‘aux’: aux = const v + • In the expression: aux + In an equation for ‘z’: + z = aux + where + aux = const v + In an equation for ‘cast2’: + cast2 v + = z () + where + z :: () -> t + z = aux + where + aux = const v • Relevant bindings include - aux :: b -> t1 (bound at T7453.hs:16:21) + aux :: forall {b}. b -> p (bound at T7453.hs:16:21) z :: () -> t1 (bound at T7453.hs:15:11) v :: p (bound at T7453.hs:13:7) cast2 :: p -> t (bound at T7453.hs:13:1) |