From eff86e8a5bddf61824fcd0147a70890b692efdcb Mon Sep 17 00:00:00 2001 From: Richard Eisenberg Date: Mon, 21 Mar 2022 22:14:15 +0000 Subject: Add Red Herring to Note [What might equal later?] Close #21208. --- compiler/GHC/Tc/Solver/InertSet.hs | 129 +++++++++++++++++++++ compiler/GHC/Tc/Solver/Interact.hs | 2 +- compiler/GHC/Tc/Solver/Monad.hs | 86 -------------- testsuite/tests/typecheck/should_compile/T21208.hs | 18 +++ testsuite/tests/typecheck/should_compile/all.T | 1 + 5 files changed, 149 insertions(+), 87 deletions(-) create mode 100644 testsuite/tests/typecheck/should_compile/T21208.hs diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs index b2416e9915..cc2afc1b0e 100644 --- a/compiler/GHC/Tc/Solver/InertSet.hs +++ b/compiler/GHC/Tc/Solver/InertSet.hs @@ -1643,6 +1643,135 @@ prohibitedSuperClassSolve from_loc solve_loc | otherwise = False +{- Note [What might equal later?] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We must determine whether a Given might later equal a Wanted. We +definitely need to account for the possibility that any metavariable +might be arbitrarily instantiated. Yet we do *not* want +to allow skolems in to be instantiated, as we've already rewritten +with respect to any Givens. (We're solving a Wanted here, and so +all Givens have already been processed.) + +This is best understood by example. + +1. C alpha ~? C Int + + That given certainly might match later. + +2. C a ~? C Int + + No. No new givens are going to arise that will get the `a` to rewrite + to Int. + +3. C alpha[tv] ~? C Int + + That alpha[tv] is a TyVarTv, unifiable only with other type variables. + It cannot equal later. + +4. C (F alpha) ~? C Int + + Sure -- that can equal later, if we learn something useful about alpha. + +5. C (F alpha[tv]) ~? C Int + + This, too, might equal later. Perhaps we have [G] F b ~ Int elsewhere. + Or maybe we have C (F alpha[tv] beta[tv]), these unify with each other, + and F x x = Int. Remember: returning True doesn't commit ourselves to + anything. + +6. C (F a) ~? C a + + No, this won't match later. If we could rewrite (F a) or a, we would + have by now. But see also Red Herring below. + +7. C (Maybe alpha) ~? C alpha + + We say this cannot equal later, because it would require + alpha := Maybe (Maybe (Maybe ...)). While such a type can be contrived, + we choose not to worry about it. See Note [Infinitary substitution in lookup] + in GHC.Core.InstEnv. Getting this wrong let to #19107, tested in + typecheck/should_compile/T19107. + +8. C cbv ~? C Int + where cbv = F a + + The cbv is a cycle-breaker var which stands for F a. See + Note [Type variable cycles] in GHC.Tc.Solver.Canonical. + This is just like case 6, and we say "no". Saying "no" here is + essential in getting the parser to type-check, with its use of DisambECP. + +9. C cbv ~? C Int + where cbv = F alpha + + Here, we might indeed equal later. Distinguishing between + this case and Example 8 is why we need the InertSet in mightEqualLater. + +10. C (F alpha, Int) ~? C (Bool, F alpha) + + This cannot equal later, because F a would have to equal both Bool and + Int. + +To deal with type family applications, we use the Core flattener. See +Note [Flattening type-family applications when matching instances] in GHC.Core.Unify. +The Core flattener replaces all type family applications with +fresh variables. The next question: should we allow these fresh +variables in the domain of a unifying substitution? + +A type family application that mentions only skolems (example 6) is settled: +any skolems would have been rewritten w.r.t. Givens by now. These type family +applications match only themselves. A type family application that mentions +metavariables, on the other hand, can match anything. So, if the original type +family application contains a metavariable, we use BindMe to tell the unifier +to allow it in the substitution. On the other hand, a type family application +with only skolems is considered rigid. + +This treatment fixes #18910 and is tested in +typecheck/should_compile/InstanceGivenOverlap{,2} + +Red Herring +~~~~~~~~~~~ +In #21208, we have this scenario: + +instance forall b. C b +[G] C a[sk] +[W] C (F a[sk]) + +What should we do with that wanted? According to the logic above, the Given +cannot match later (this is example 6), and so we use the global instance. +But wait, you say: What if we learn later (say by a future type instance F a = a) +that F a unifies with a? That looks like the Given might really match later! + +This mechanism described in this Note is *not* about this kind of situation, however. +It is all asking whether a Given might match the Wanted *in this run of the solver*. +It is *not* about whether a variable might be instantiated so that the Given matches, +or whether a type instance introduced in a downstream module might make the Given match. +The reason we care about what might match later is only about avoiding order-dependence. +That is, we don't want to commit to a course of action that depends on seeing constraints +in a certain order. But an instantiation of a variable and a later type instance +don't introduce order dependency in this way, and so mightMatchLater is right to ignore +these possibilities. + +Here is an example, with no type families, that is perhaps clearer: + +instance forall b. C (Maybe b) +[G] C (Maybe Int) +[W] C (Maybe a) + +What to do? We *might* say that the Given could match later and should thus block +us from using the global instance. But we don't do this. Instead, we rely on class +coherence to say that choosing the global instance is just fine, even if later we +call a function with (a := Int). After all, in this run of the solver, [G] C (Maybe Int) +will definitely never match [W] C (Maybe a). (Recall that we process Givens before +Wanteds, so there is no [G] a ~ Int hanging about unseen.) + +Interestingly, in the first case (from #21208), the behavior changed between +GHC 8.10.7 and GHC 9.2, with the latter behaving correctly and the former +reporting overlapping instances. + +Test case: typecheck/should_compile/T21208. + +-} + {- ********************************************************************* * * Cycle breakers diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index 75a117798e..5c4b18621f 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -2352,7 +2352,7 @@ Other notes: - natural numbers - Typeable -* See also Note [What might equal later?] in GHC.Tc.Solver.Monad. +* See also Note [What might equal later?] in GHC.Tc.Solver.InertSet. * The given-overlap problem is arguably not easy to appear in practice due to our aggressive prioritization of equality solving over other diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index c253770616..a039630887 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -631,92 +631,6 @@ getHasGivenEqs tclvl insoluble_given_equality ct = insolubleEqCt ct && isGivenCt ct -{- Note [What might equal later?] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We must determine whether a Given might later equal a Wanted. We -definitely need to account for the possibility that any metavariable -might be arbitrarily instantiated. Yet we do *not* want -to allow skolems in to be instantiated, as we've already rewritten -with respect to any Givens. (We're solving a Wanted here, and so -all Givens have already been processed.) - -This is best understood by example. - -1. C alpha ~? C Int - - That given certainly might match later. - -2. C a ~? C Int - - No. No new givens are going to arise that will get the `a` to rewrite - to Int. - -3. C alpha[tv] ~? C Int - - That alpha[tv] is a TyVarTv, unifiable only with other type variables. - It cannot equal later. - -4. C (F alpha) ~? C Int - - Sure -- that can equal later, if we learn something useful about alpha. - -5. C (F alpha[tv]) ~? C Int - - This, too, might equal later. Perhaps we have [G] F b ~ Int elsewhere. - Or maybe we have C (F alpha[tv] beta[tv]), these unify with each other, - and F x x = Int. Remember: returning True doesn't commit ourselves to - anything. - -6. C (F a) ~? C a - - No, this won't match later. If we could rewrite (F a) or a, we would - have by now. - -7. C (Maybe alpha) ~? C alpha - - We say this cannot equal later, because it would require - alpha := Maybe (Maybe (Maybe ...)). While such a type can be contrived, - we choose not to worry about it. See Note [Infinitary substitution in lookup] - in GHC.Core.InstEnv. Getting this wrong let to #19107, tested in - typecheck/should_compile/T19107. - -8. C cbv ~? C Int - where cbv = F a - - The cbv is a cycle-breaker var which stands for F a. See - Note [Type variable cycles] in GHC.Tc.Solver.Canonical. - This is just like case 6, and we say "no". Saying "no" here is - essential in getting the parser to type-check, with its use of DisambECP. - -9. C cbv ~? C Int - where cbv = F alpha - - Here, we might indeed equal later. Distinguishing between - this case and Example 8 is why we need the InertSet in mightEqualLater. - -10. C (F alpha, Int) ~? C (Bool, F alpha) - - This cannot equal later, because F a would have to equal both Bool and - Int. - -To deal with type family applications, we use the Core flattener. See -Note [Flattening type-family applications when matching instances] in GHC.Core.Unify. -The Core flattener replaces all type family applications with -fresh variables. The next question: should we allow these fresh -variables in the domain of a unifying substitution? - -A type family application that mentions only skolems (example 6) is settled: -any skolems would have been rewritten w.r.t. Givens by now. These type family -applications match only themselves. A type family application that mentions -metavariables, on the other hand, can match anything. So, if the original type -family application contains a metavariable, we use BindMe to tell the unifier -to allow it in the substitution. On the other hand, a type family application -with only skolems is considered rigid. - -This treatment fixes #18910 and is tested in -typecheck/should_compile/InstanceGivenOverlap{,2} --} - removeInertCts :: [Ct] -> InertCans -> InertCans -- ^ Remove inert constraints from the 'InertCans', for use when a -- typechecker plugin wishes to discard a given. diff --git a/testsuite/tests/typecheck/should_compile/T21208.hs b/testsuite/tests/typecheck/should_compile/T21208.hs new file mode 100644 index 0000000000..fc90f99693 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/T21208.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleInstances #-} + +module T21208 where + +type family F a + +inject :: a -> F a +inject = undefined + +class C a where + meth :: a -> () + +instance C a where + meth _ = () + +g :: C a => a -> () +g x = meth (inject x) diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 24574892e7..64828410f9 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -560,6 +560,7 @@ test('T11525', normal, multi_compile, [None, [('T11525_Plugin.hs', '-package ghc'), ('T11525.hs', '')], '-dynamic' if have_dynamic() else '']) test('T12923_1', normal, compile, ['']) +test('T21208', normal, compile, ['']) test('T12923_2', normal, compile, ['']) test('T12923_3', normal, compile, ['']) test('T13381', normal, compile_fail, ['']) -- cgit v1.2.1