[Git][ghc/ghc][wip/jsem] 2 commits: matchLocalInst: do domination analysis
Matthew Pickering (@mpickering)
gitlab at gitlab.haskell.org
Thu Oct 20 11:42:01 UTC 2022
Matthew Pickering pushed to branch wip/jsem at Glasgow Haskell Compiler / GHC
Commits:
c5da6e3e by sheaf at 2022-10-20T12:32:55+01:00
matchLocalInst: do domination analysis
When multiple Given quantified constraints match a Wanted, and there is
a quantified constraint that dominates all others, we now pick it
to solve the Wanted.
See Note [Use only the best matching quantified constraint].
For example:
[G] d1: forall a b. ( Eq a, Num b, C a b ) => D a b
[G] d2: forall a . C a Int => D a Int
[W] {w}: D a Int
When solving the Wanted, we find that both Givens match, but we pick
the second, because it has a weaker precondition, C a Int, compared
to (Eq a, Num Int, C a Int). We thus say that d2 dominates d1;
see Note [When does a quantified instance dominate another?].
This domination test is done purely in terms of superclass expansion,
in the function GHC.Tc.Solver.Interact.impliedBySCs. We don't attempt
to do a full round of constraint solving; this simple check suffices
for now.
Fixes #22216 and #22223
- - - - -
267f54e7 by Matthew Pickering at 2022-10-20T12:41:42+01:00
latest changes
- - - - -
16 changed files:
- compiler/GHC/Driver/MakeSem.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Origin.hs
- compiler/GHC/Utils/Misc.hs
- docs/users_guide/9.6.1-notes.rst
- hadrian/src/Rules/Compile.hs
- libraries/Cabal
- + testsuite/tests/quantified-constraints/T22216a.hs
- + testsuite/tests/quantified-constraints/T22216b.hs
- + testsuite/tests/quantified-constraints/T22216c.hs
- + testsuite/tests/quantified-constraints/T22216d.hs
- + testsuite/tests/quantified-constraints/T22216e.hs
- + testsuite/tests/quantified-constraints/T22223.hs
- testsuite/tests/quantified-constraints/all.T
Changes:
=====================================
compiler/GHC/Driver/MakeSem.hs
=====================================
@@ -1,6 +1,7 @@
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TupleSections #-}
-- | Implementation of a jobserver using system semaphores.
--
@@ -28,6 +29,7 @@ import GHC.Utils.Logger
import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Trace
+import GHC.Utils.Json
import Control.Monad
import qualified Control.Monad.Catch as MC
@@ -36,6 +38,7 @@ import Control.Concurrent.STM
import Data.Foldable
import Data.Functor
import GHC.Stack
+import Debug.Trace
---------------------------------------
-- Semaphore jobserver
@@ -180,7 +183,7 @@ guardRelease ( Jobs { tokensFree, tokensOwned, jobsWaiting } )
-- Blocks, waiting on the jobserver to supply a free token.
acquireJob :: Logger -> TVar JobResources -> IO ()
acquireJob logger jobs_tvar = do
- (job_tmvar, jobs0) <- atomically $ modifyJobResources jobs_tvar \ jobs -> do
+ (job_tmvar, jobs0) <- tracedAtomically "acquire" $ modifyJobResources jobs_tvar \ jobs -> do
job_tmvar <- newEmptyTMVar
return ((job_tmvar, jobs), addJob job_tmvar jobs)
logDumpMsg logger "acquireJob {" $ ppr jobs0
@@ -191,16 +194,11 @@ acquireJob logger jobs_tvar = do
-- releasing its corresponding token.
releaseJob :: Logger -> TVar JobResources -> IO ()
releaseJob logger jobs_tvar = do
- (jobs0, jobs1) <- atomically do
- jobs0 <- modifyJobResources jobs_tvar \ jobs -> do
+ tracedAtomically "release" do
+ modifyJobResources jobs_tvar \ jobs -> do
massertPpr (tokensFree jobs < tokensOwned jobs)
(text "releaseJob: more free jobs than owned jobs!")
- return (jobs, addFreeToken jobs)
- jobs1 <- readTVar jobs_tvar
- pure (jobs0,jobs1)
- logDumpMsg logger "releaseJob" $
- vcat [ text "jobs0:" <+> ppr jobs0
- , text "jobs1:" <+> ppr jobs1 ]
+ return ((), addFreeToken jobs)
-- | Release all tokens owned from the semaphore (to clean up
@@ -247,7 +245,7 @@ dispatchTokens jobs@( Jobs { tokensFree = toks_free, jobsWaiting = wait } )
-- of the 'TVar' remains in normal form.
modifyJobResources :: HasCallStack => TVar JobResources
-> (JobResources -> STM (a, JobResources))
- -> STM a
+ -> STM (a, Maybe JobResources)
modifyJobResources jobs_tvar action = do
old_jobs <- readTVar jobs_tvar
(a, jobs) <- action old_jobs
@@ -256,13 +254,32 @@ modifyJobResources jobs_tvar action = do
-- there must be no pending jobs.
massertPpr (null (jobsWaiting jobs) || tokensFree jobs >= tokensFree old_jobs) $
vcat [ text "modiyJobResources: pending jobs but fewer free tokens" ]
- pprTraceM "modify" (ppr old_jobs $$ ppr jobs $$ callStackDoc)
+ dispatched_jobs <- dispatchTokens jobs
+ writeTVar jobs_tvar dispatched_jobs
+ return (a, Just dispatched_jobs)
- jobs <- dispatchTokens jobs
- pprTraceM "dispatch_modify" (ppr jobs)
- writeTVar jobs_tvar jobs
+
+tracedAtomically_ :: String -> STM (Maybe JobResources) -> IO ()
+tracedAtomically_ s act = tracedAtomically s (((),) <$> act)
+
+tracedAtomically :: String -> STM (a, Maybe JobResources) -> IO a
+tracedAtomically origin act = do
+ (a, mjr) <- atomically act
+ forM_ mjr $ \jr -> do
+ -- MP: Could also trace to a logger here as well with suitable verbosity
+ -- Use the "jsem:" prefix to identify where the write traces are
+ traceEventIO ("jsem:" ++ renderJobResources origin jr)
return a
+renderJobResources :: String -> JobResources -> String
+renderJobResources origin (Jobs own free pending) = showSDocUnsafe $ renderJSON $
+ JSObject [ ("name", JSString origin)
+ , ("owned", JSInt own)
+ , ("free", JSInt free)
+ , ("pending", JSInt (length pending) )
+ ]
+
+
-- | Spawn a new thread that waits on the semaphore in order to acquire
-- an additional token.
acquireThread :: Jobserver -> IO JobserverAction
@@ -270,19 +287,19 @@ acquireThread (Jobserver { jSemaphore = sem, jobs = jobs_tvar }) = do
threadFinished_tmvar <- newEmptyTMVarIO
tid <- forkIO $ MC.mask_ $ do
wait_res <- MC.try (waitOnSemaphore sem)
- atomically do
- r <- case wait_res of
+ tracedAtomically_ "acquire_thread" do
+ (r, jb) <- case wait_res of
Left (e :: MC.SomeException) -> do
- pprTraceM "exc_bad_bad" (text $ show e)
- return $ Just e
+ return $ (Just e, Nothing)
Right success -> do
if success
then do
- modifyJobResources jobs_tvar \ jobs -> return ((), addToken jobs)
- return Nothing
+ modifyJobResources jobs_tvar \ jobs -> return (Nothing, addToken jobs)
else
- return Nothing
+ return (Nothing, Nothing)
putTMVar threadFinished_tmvar r
+ return jb
+ labelThread tid "acquire_thread"
return $ Acquiring { activeThread = tid
, threadFinished = threadFinished_tmvar }
@@ -292,8 +309,10 @@ releaseThread :: Jobserver -> IO JobserverAction
releaseThread (Jobserver { jSemaphore = sem, jobs = jobs_tvar }) = do
threadFinished_tmvar <- newEmptyTMVarIO
MC.mask_ do
+ -- Pre-release the resource so that another thread doesn't take control of it
+ -- just as we release the lock on the semaphore.
still_ok_to_release
- <- atomically $ modifyJobResources jobs_tvar \ jobs ->
+ <- tracedAtomically "pre_release" $ modifyJobResources jobs_tvar \ jobs ->
if guardRelease jobs
-- TODO: should this also debounce?
then return (True , removeOwnedToken $ removeFreeToken jobs)
@@ -304,20 +323,16 @@ releaseThread (Jobserver { jSemaphore = sem, jobs = jobs_tvar }) = do
tid <- forkIO $ do
x <- MC.try $ void $ do
releaseSemaphore sem 1
- atomically do
- r <- case x of
+ tracedAtomically_ "post-release" $ do
+ (r, jobs) <- case x of
Left (e :: MC.SomeException) -> do
- pprTraceM "exc" (text $ show e)
modifyJobResources jobs_tvar \ jobs ->
- return ((), addToken jobs)
- return (Just e)
+ return (Just e, addToken jobs)
Right () -> do
--- modifyJobResources jobs_tvar \ jobs ->
--- return ((), jobs)
- -- NB: we already decremented the number of free tokens above,
- -- so don't do that a second time.
- return Nothing
+ return (Nothing, Nothing)
putTMVar threadFinished_tmvar r
+ return jobs
+ labelThread tid "release_thread"
return $ Releasing { activeThread = tid
, threadFinished = threadFinished_tmvar }
@@ -477,6 +492,7 @@ makeJobserver logger sem_name = do
| otherwise
-> Just e
Right () -> Nothing
+ labelThread loop_tid "job_server"
let
acquireSem = acquireJob logger jobs_tvar
releaseSem = releaseJob logger jobs_tvar
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -1558,23 +1558,28 @@ matchableGivens loc_w pred_w inerts@(IS { inert_cans = inert_cans })
matchable_given :: Ct -> Bool
matchable_given ct
| CtGiven { ctev_loc = loc_g, ctev_pred = pred_g } <- ctEvidence ct
- = mightEqualLater inerts pred_g loc_g pred_w loc_w
+ = isJust $ mightEqualLater inerts pred_g loc_g pred_w loc_w
| otherwise
= False
-mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
+mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Maybe Subst
-- See Note [What might equal later?]
-- Used to implement logic in Note [Instance and Given overlap] in GHC.Tc.Solver.Interact
mightEqualLater inert_set given_pred given_loc wanted_pred wanted_loc
| prohibitedSuperClassSolve given_loc wanted_loc
- = False
+ = Nothing
| otherwise
= case tcUnifyTysFG bind_fun [flattened_given] [flattened_wanted] of
- SurelyApart -> False -- types that are surely apart do not equal later
- MaybeApart MARInfinite _ -> False -- see Example 7 in the Note.
- _ -> True
+ Unifiable subst
+ -> Just subst
+ MaybeApart reason subst
+ | MARInfinite <- reason -- see Example 7 in the Note.
+ -> Nothing
+ | otherwise
+ -> Just subst
+ SurelyApart -> Nothing
where
in_scope = mkInScopeSet $ tyCoVarsOfTypes [given_pred, wanted_pred]
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -50,6 +50,7 @@ import GHC.Types.Var.Env
import qualified Data.Semigroup as S
import Control.Monad
+import Data.Maybe ( listToMaybe, mapMaybe )
import GHC.Data.Pair (Pair(..))
import GHC.Types.Unique( hasKey )
import GHC.Driver.Session
@@ -2470,109 +2471,236 @@ matchLocalInst :: TcPredType -> CtLoc -> TcS ClsInstResult
matchLocalInst pred loc
= do { inerts@(IS { inert_cans = ics }) <- getTcSInerts
; case match_local_inst inerts (inert_insts ics) of
- ([], Nothing) -> do { traceTcS "No local instance for" (ppr pred)
- ; return NoInstance }
-
- -- See Note [Use only the best local instance] about
- -- superclass depths
- (matches, unifs)
- | [(dfun_ev, inst_tys)] <- best_matches
- , maybe True (> min_sc_depth) unifs
- -> do { let dfun_id = ctEvEvId dfun_ev
- ; (tys, theta) <- instDFunType dfun_id inst_tys
- ; let result = OneInst { cir_new_theta = theta
- , cir_mk_ev = evDFunApp dfun_id tys
- , cir_what = LocalInstance }
- ; traceTcS "Best local inst found:" (ppr result)
- ; traceTcS "All local insts:" (ppr matches)
- ; return result }
-
- | otherwise
- -> do { traceTcS "Multiple local instances for" (ppr pred)
- ; return NotSure }
-
- where
- extract_depth = sc_depth . ctEvLoc . fst
- min_sc_depth = minimum (map extract_depth matches)
- best_matches = filter ((== min_sc_depth) . extract_depth) matches }
+ { ([], []) -> do { traceTcS "No local instance for" (ppr pred)
+ ; return NoInstance }
+ ; (matches, unifs) ->
+ do { matches <- mapM mk_instDFun matches
+ ; unifs <- mapM mk_instDFun unifs
+ -- See Note [Use only the best matching quantified constraint]
+ ; case dominatingMatch matches of
+ { Just (dfun_id, tys, theta)
+ | all ((theta `impliedBySCs`) . thdOf3) unifs
+ ->
+ do { let result = OneInst { cir_new_theta = theta
+ , cir_mk_ev = evDFunApp dfun_id tys
+ , cir_what = LocalInstance }
+ ; traceTcS "Best local instance found:" $
+ vcat [ text "pred:" <+> ppr pred
+ , text "result:" <+> ppr result
+ , text "matches:" <+> ppr matches
+ , text "unifs:" <+> ppr unifs ]
+ ; return result }
+
+ ; mb_best ->
+ do { traceTcS "Multiple local instances; not committing to any"
+ $ vcat [ text "pred:" <+> ppr pred
+ , text "matches:" <+> ppr matches
+ , text "unifs:" <+> ppr unifs
+ , text "best_match:" <+> ppr mb_best ]
+ ; return NotSure }}}}}
where
pred_tv_set = tyCoVarsOfType pred
- sc_depth :: CtLoc -> Int
- sc_depth ctloc = case ctLocOrigin ctloc of
- InstSCOrigin depth _ -> depth
- OtherSCOrigin depth _ -> depth
- _ -> 0
+ mk_instDFun :: (CtEvidence, [DFunInstType]) -> TcS InstDFun
+ mk_instDFun (ev, tys) =
+ let dfun_id = ctEvEvId ev
+ in do { (tys, theta) <- instDFunType (ctEvEvId ev) tys
+ ; return (dfun_id, tys, theta) }
- -- See Note [Use only the best local instance] about superclass depths
+ -- Compute matching and unifying local instances
match_local_inst :: InertSet
-> [QCInst]
-> ( [(CtEvidence, [DFunInstType])]
- , Maybe Int ) -- Nothing ==> no unifying local insts
- -- Just n ==> unifying local insts, with
- -- minimum superclass depth
- -- of n
+ , [(CtEvidence, [DFunInstType])] )
match_local_inst _inerts []
- = ([], Nothing)
- match_local_inst inerts (qci@(QCI { qci_tvs = qtvs, qci_pred = qpred
- , qci_ev = qev })
- : qcis)
+ = ([], [])
+ match_local_inst inerts (qci@(QCI { qci_tvs = qtvs
+ , qci_pred = qpred
+ , qci_ev = qev })
+ :qcis)
| let in_scope = mkInScopeSet (qtv_set `unionVarSet` pred_tv_set)
, Just tv_subst <- ruleMatchTyKiX qtv_set (mkRnEnv2 in_scope)
emptyTvSubstEnv qpred pred
, let match = (qev, map (lookupVarEnv tv_subst) qtvs)
- = (match:matches, unif)
+ = (match:matches, unifs)
| otherwise
= assertPpr (disjointVarSet qtv_set (tyCoVarsOfType pred))
(ppr qci $$ ppr pred)
-- ASSERT: unification relies on the
-- quantified variables being fresh
- (matches, unif `combine` this_unif)
+ (matches, this_unif `combine` unifs)
where
qloc = ctEvLoc qev
qtv_set = mkVarSet qtvs
+ (matches, unifs) = match_local_inst inerts qcis
this_unif
- | mightEqualLater inerts qpred qloc pred loc = Just (sc_depth qloc)
- | otherwise = Nothing
- (matches, unif) = match_local_inst inerts qcis
+ | Just subst <- mightEqualLater inerts qpred qloc pred loc
+ = Just (qev, map (lookupTyVar subst) qtvs)
+ | otherwise
+ = Nothing
- combine Nothing Nothing = Nothing
- combine (Just n) Nothing = Just n
- combine Nothing (Just n) = Just n
- combine (Just n1) (Just n2) = Just (n1 `min` n2)
+ combine Nothing us = us
+ combine (Just u) us = u : us
-{- Note [Use only the best local instance]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+-- | Instance dictionary function and type.
+type InstDFun = (DFunId, [TcType], TcThetaType)
+
+-- | Try to find a local quantified instance that dominates all others,
+-- i.e. which has a weaker instance context than all the others.
+--
+-- See Note [Use only the best matching quantified constraint].
+dominatingMatch :: [InstDFun] -> Maybe InstDFun
+dominatingMatch matches =
+ listToMaybe $ mapMaybe (uncurry go) (holes matches)
+ -- listToMaybe: arbitrarily pick any one context that is weaker than
+ -- all others, e.g. so that we can handle [Eq a, Num a] vs [Num a, Eq a]
+ -- (see test case T22223).
+
+ where
+ go :: InstDFun -> [InstDFun] -> Maybe InstDFun
+ go this [] = Just this
+ go this@(_,_,this_theta) ((_,_,other_theta):others)
+ | this_theta `impliedBySCs` other_theta
+ = go this others
+ | otherwise
+ = Nothing
+
+-- | Whether a collection of constraints is implied by another collection,
+-- according to a simple superclass check.
+--
+-- See Note [When does a quantified instance dominate another?].
+impliedBySCs :: TcThetaType -> TcThetaType -> Bool
+impliedBySCs c1 c2 = all in_c2 c1
+ where
+ in_c2 :: TcPredType -> Bool
+ in_c2 pred = any (pred `eqType`) c2_expanded
+
+ c2_expanded :: [TcPredType] -- Includes all superclasses
+ c2_expanded = [ q | p <- c2, q <- p : transSuperClasses p ]
+
+
+{- Note [When does a quantified instance dominate another?]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When matching local quantified instances, it's useful to be able to pick
+the one with the weakest precondition, e.g. if one has both
+
+ [G] d1: forall a b. ( Eq a, Num b, C a b ) => D a b
+ [G] d2: forall a . C a Int => D a Int
+ [W] {w}: D a Int
+
+Then it makes sense to use d2 to solve w, as doing so we end up with a strictly
+weaker proof obligation of `C a Int`, compared to `(Eq a, Num Int, C a Int)`
+were we to use d1.
+
+In theory, to compute whether one context implies another, we would need to
+recursively invoke the constraint solver. This is expensive, so we instead do
+a simple check using superclasses, implemented in impliedBySCs.
+
+Examples:
+
+ - [Eq a] is implied by [Ord a]
+ - [Ord a] is not implied by [Eq a],
+ - any context is implied by itself,
+ - the empty context is implied by any context.
+
+Note [Use only the best matching quantified constraint]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (#20582) the ambiguity check for
(forall a. Ord (m a), forall a. Semigroup a => Eq (m a)) => m Int
Because of eager expansion of given superclasses, we get
- [G] forall a. Ord (m a)
- [G] forall a. Eq (m a)
- [G] forall a. Semigroup a => Eq (m a)
+ [G] d1: forall a. Ord (m a)
+ [G] d2: forall a. Eq (m a)
+ [G] d3: forall a. Semigroup a => Eq (m a)
- [W] forall a. Ord (m a)
- [W] forall a. Semigroup a => Eq (m a)
+ [W] {w1}: forall a. Ord (m a)
+ [W] {w2}: forall a. Semigroup a => Eq (m a)
The first wanted is solved straightforwardly. But the second wanted
-matches *two* local instances. Our general rule around multiple local
+matches *two* local instances: d2 and d3. Our general rule around multiple local
instances is that we refuse to commit to any of them. However, that
means that our type fails the ambiguity check. That's bad: the type
is perfectly fine. (This actually came up in the wild, in the streamly
library.)
-The solution is to prefer local instances with fewer superclass selections.
-So, matchLocalInst is careful to whittle down the matches only to the
-ones with the shallowest superclass depth, and also to worry about unifying
-local instances that are at that depth (or less).
+The solution is to prefer local instances which are easier to prove, meaning
+that they have a weaker precondition. In this case, the empty context
+of d2 is a weaker constraint than the "Semigroup a" context of d3, so we prefer
+using it when proving w2. This allows us to pass the ambiguity check here.
+
+Our criterion for solving a Wanted by matching local quantified instances is
+thus as follows:
+
+ - There is a matching local quantified instance that dominates all others
+ matches, in the sense of [When does a quantified instance dominate another?].
+ Any such match do, we pick it arbitrarily (the T22223 example below says why).
+ - This local quantified instance also dominates all the unifiers, as we
+ wouldn't want to commit to a single match when we might have multiple,
+ genuinely different matches after further unification takes place.
+
+Some other examples:
+
+
+ #15244:
+
+ f :: (C g, D g) => ....
+ class S g => C g where ...
+ class S g => D g where ...
+ class (forall a. Eq a => Eq (g a)) => S g where ...
+
+ Here, in f's RHS, there are two identical quantified constraints
+ available, one via the superclasses of C and one via the superclasses
+ of D. Given that each implies the other, we pick one arbitrarily.
+
+
+ #22216:
+
+ class Eq a
+ class Eq a => Ord a
+ class (forall b. Eq b => Eq (f b)) => Eq1 f
+ class (Eq1 f, forall b. Ord b => Ord (f b)) => Ord1 f
+
+ Suppose we have
+
+ [G] d1: Ord1 f
+ [G] d2: Eq a
+ [W] {w}: Eq (f a)
+
+ Superclass expansion of d1 gives us:
+
+ [G] d3 : Eq1 f
+ [G] d4 : forall b. Ord b => Ord (f b)
+
+ expanding d4 and d5 gives us, respectively:
+
+ [G] d5 : forall b. Eq b => Eq (f b)
+ [G] d6 : forall b. Ord b => Eq (f b)
+
+ Now we have two matching local instances that we could use when solving the
+ Wanted. However, it's obviously silly to use d6, given that d5 provides us with
+ as much information, with a strictly weaker precondition. So we pick d5 to solve
+ w. If we chose d6, we would get [W] Ord a, which in this case we can't solve.
+
+
+ #22223:
-By preferring these shallower local instances, we can use the last given
-listed above and pass the ambiguity check.
+ [G] forall a b. (Eq a, Ord b) => C a b
+ [G] forall a b. (Ord b, Eq a) => C a b
+ [W] C x y
-The instance-depth mechanism uses the same superclass depth
-information as described in Note [Replacement vs keeping], 2a.
+ Here we should be free to pick either quantified constraint, as they are
+ equivalent up to re-ordering of the constraints in the context.
+ See also Note [Do not add duplicate quantified instances]
+ in GHC.Tc.Solver.Monad.
-Test case: typecheck/should_compile/T20582.
+Test cases:
+ typecheck/should_compile/T20582
+ quantified-constraints/T15244
+ quantified-constraints/T22216{a,b,c,d,e}
+ quantified-constraints/T22223
+Historical note: a previous solution was to instead pick the local instance
+with the least superclass depth (see Note [Replacement vs keeping]),
+but that doesn't work for the example from #22216.
-}
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -220,21 +220,17 @@ addInertForAll new_qci
{- Note [Do not add duplicate quantified instances]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this (#15244):
+As an optimisation, we avoid adding duplicate quantified instances to the
+inert set; we use a simple duplicate check using tcEqType for simplicity,
+even though it doesn't account for superficial differences, e.g. it will count
+the following two constraints as different (#22223):
- f :: (C g, D g) => ....
- class S g => C g where ...
- class S g => D g where ...
- class (forall a. Eq a => Eq (g a)) => S g where ...
+ - forall a b. C a b
+ - forall b a. C a b
-Then in f's RHS there are two identical quantified constraints
-available, one via the superclasses of C and one via the superclasses
-of D. The two are identical, and it seems wrong to reject the program
-because of that. But without doing duplicate-elimination we will have
-two matching QCInsts when we try to solve constraints arising from f's
-RHS.
-
-The simplest thing is simply to eliminate duplicates, which we do here.
+The main logic that allows us to pick local instances, even in the presence of
+duplicates, is explained in Note [Use only the best matching quantified constraint]
+in GHC.Tc.Solver.Interact.
-}
{- *********************************************************************
=====================================
compiler/GHC/Tc/Types/Origin.hs
=====================================
@@ -464,8 +464,7 @@ data CtOrigin
-- have 'InstSCOrigin' origin.
| InstSCOrigin ScDepth -- ^ The number of superclass selections necessary to
-- get this constraint; see Note [Replacement vs keeping]
- -- and Note [Use only the best local instance], both in
- -- GHC.Tc.Solver.Interact
+ -- in GHC.Tc.Solver.Interact
TypeSize -- ^ If @(C ty1 .. tyn)@ is the largest class from
-- which we made a superclass selection in the chain,
-- then @TypeSize = sizeTypes [ty1, .., tyn]@
@@ -478,12 +477,13 @@ data CtOrigin
-- f = e
-- When typechecking body of 'f', the superclasses of the Given (Foo a)
-- will have 'OtherSCOrigin'.
- -- Needed for Note [Replacement vs keeping] and
- -- Note [Use only the best local instance], both in GHC.Tc.Solver.Interact.
+ --
+ -- Needed for Note [Replacement vs keeping] in GHC.Tc.Solver.Interact.
| OtherSCOrigin ScDepth -- ^ The number of superclass selections necessary to
-- get this constraint
- SkolemInfoAnon -- ^ Where the sub-class constraint arose from
- -- (used only for printing)
+ SkolemInfoAnon
+ -- ^ Where the sub-class constraint arose from
+ -- (used only for printing)
-- All the others are for *wanted* constraints
=====================================
compiler/GHC/Utils/Misc.hs
=====================================
@@ -43,6 +43,8 @@ module GHC.Utils.Misc (
chunkList,
+ holes,
+
changeLast,
mapLastM,
@@ -506,6 +508,13 @@ chunkList :: Int -> [a] -> [[a]]
chunkList _ [] = []
chunkList n xs = as : chunkList n bs where (as,bs) = splitAt n xs
+-- | Compute all the ways of removing a single element from a list.
+--
+-- > holes [1,2,3] = [(1, [2,3]), (2, [1,3]), (3, [1,2])]
+holes :: [a] -> [(a, [a])]
+holes [] = []
+holes (x:xs) = (x, xs) : mapSnd (x:) (holes xs)
+
-- | Replace the last element of a list with another element.
changeLast :: [a] -> a -> [a]
changeLast [] _ = panic "changeLast"
=====================================
docs/users_guide/9.6.1-notes.rst
=====================================
@@ -68,6 +68,16 @@ Language
:extension:`TypeData`. This extension permits ``type data`` declarations
as a more fine-grained alternative to :extension:`DataKinds`.
+- GHC now does a better job of solving constraints in the presence of multiple
+ matching quantified constraints. For example, if we want to solve
+ ``C a b Int`` and we have matching quantified constraints: ::
+
+ forall x y z. (Ord x, Enum y, Num z) => C x y z
+ forall u v. (Enum v, Eq u) => C u v Int
+
+ Then GHC will use the second quantified constraint to solve ``C a b Int``,
+ as it has a strictly weaker precondition.
+
Compiler
~~~~~~~~
=====================================
hadrian/src/Rules/Compile.hs
=====================================
@@ -208,7 +208,7 @@ compileHsObjectAndHi rs objpath = do
let ctx = objectContext b
-- Ideally we want to use --make to build with stage0 but we need to use -jsem
-- to recover build-time performance so we only do it for stage1 at the moment.
- if stage < Stage3
+ if isStage0 stage
then compileWithOneShot ctx
else compileWithMake ctx
=====================================
libraries/Cabal
=====================================
@@ -1 +1 @@
-Subproject commit 410f871df899e5af0847089354e0031fe051551d
+Subproject commit b01efbe2b9119c0d5b257afd2eb264dd476868c2
=====================================
testsuite/tests/quantified-constraints/T22216a.hs
=====================================
@@ -0,0 +1,14 @@
+{-# LANGUAGE QuantifiedConstraints, UndecidableInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module T22216a where
+
+class Eq a
+class Eq a => Ord a
+
+class (forall b. Eq b => Eq (f b)) => Eq1 f
+class (Eq1 f, forall b. Ord b => Ord (f b)) => Ord1 f
+
+foo :: (Ord a, Ord1 f) => (Eq (f a) => r) -> r
+foo r = r
=====================================
testsuite/tests/quantified-constraints/T22216b.hs
=====================================
@@ -0,0 +1,11 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE StandaloneDeriving #-}
+
+module T22216b where
+
+import Data.Functor.Classes
+
+newtype T f a = MkT (f a)
+ deriving ( Eq, Ord, Eq1
+ , Ord1
+ )
=====================================
testsuite/tests/quantified-constraints/T22216c.hs
=====================================
@@ -0,0 +1,23 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T22216c where
+
+import Prelude (Bool, Ordering)
+
+class Eq a where
+class Eq a => Ord a where
+class (forall a. Eq a => Eq (f a)) => Eq1 f where
+
+class (Eq1 f, forall a. Ord a => Ord (f a)) => Ord1 f where
+ liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering
+
+instance Eq (T f a)
+instance Ord (T f a)
+instance Eq1 (T f)
+
+newtype T f a = MkT (f a)
+ deriving Ord1
=====================================
testsuite/tests/quantified-constraints/T22216d.hs
=====================================
@@ -0,0 +1,33 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module T22216d where
+
+class (forall a. Eq a => Eq (f a)) => Eq1 f where
+ liftEq :: (a -> b -> Bool) -> f a -> f b -> Bool
+
+eq1 :: (Eq1 f, Eq a) => f a -> f a -> Bool
+eq1 = liftEq (==)
+
+class (Eq1 f, forall a. Ord a => Ord (f a)) => Ord1 f where
+ liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering
+
+compare1 :: (Ord1 f, Ord a) => f a -> f a -> Ordering
+compare1 = liftCompare compare
+
+data Cofree f a = a :< f (Cofree f a)
+
+instance (Eq1 f, Eq a) => Eq (Cofree f a) where
+ (==) = eq1
+
+instance (Eq1 f) => Eq1 (Cofree f) where
+ liftEq eq = go
+ where
+ go (a :< as) (b :< bs) = eq a b && liftEq go as bs
+
+instance (Ord1 f, Ord a) => Ord (Cofree f a) where
+ compare = compare1
+
+instance (Ord1 f) => Ord1 (Cofree f) where
+ liftCompare cmp = go
+ where
+ go (a :< as) (b :< bs) = cmp a b `mappend` liftCompare go as bs
=====================================
testsuite/tests/quantified-constraints/T22216e.hs
=====================================
@@ -0,0 +1,19 @@
+{-# LANGUAGE QuantifiedConstraints, UndecidableInstances #-}
+{-# LANGUAGE RankNTypes #-}
+
+module T22216e where
+
+import Data.Kind
+
+type C :: Type -> Type -> Constraint
+type D :: Type -> Type -> Constraint
+
+class C a b
+instance C () Int
+class D a b
+
+foo :: ( forall a b. ( Eq a, Num b, C a b ) => D a b
+ , forall a . C a Int => D a Int
+ )
+ => ( D () Int => r ) -> r
+foo r = r
=====================================
testsuite/tests/quantified-constraints/T22223.hs
=====================================
@@ -0,0 +1,24 @@
+{-# LANGUAGE AllowAmbiguousTypes, RankNTypes, QuantifiedConstraints #-}
+
+module T22223 where
+
+import Data.Kind
+
+type C :: Type -> Type -> Constraint
+class C a b
+
+-- Change the order of quantification
+foo :: ( forall a b. (Eq a, Ord b) => C a b
+ , forall b a. (Eq a, Ord b) => C a b
+ , Eq x
+ , Ord y )
+ => ( C x y => r ) -> r
+foo r = r
+
+-- Permute the constraints in the context
+bar :: ( forall a b. (Eq a, Ord b) => C a b
+ , forall a b. (Ord b, Eq a) => C a b
+ , Eq x
+ , Ord y )
+ => ( C x y => r ) -> r
+bar r = r
=====================================
testsuite/tests/quantified-constraints/all.T
=====================================
@@ -34,3 +34,9 @@ test('T19921', normal, compile_fail, [''])
test('T16474', normal, compile_fail, [''])
test('T21006', normal, compile_fail, [''])
test('T21037', normal, compile, [''])
+test('T22216a', normal, compile, [''])
+test('T22216b', normal, compile, [''])
+test('T22216c', normal, compile, [''])
+test('T22216d', normal, compile, [''])
+test('T22216e', normal, compile, [''])
+test('T22223', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/15dffa987cc50df6d15b66b25b7a658b4b0d1e32...267f54e7f23c671daf0c4dbe15249ac3d986edfd
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/15dffa987cc50df6d15b66b25b7a658b4b0d1e32...267f54e7f23c671daf0c4dbe15249ac3d986edfd
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20221020/cfe1f842/attachment-0001.html>
More information about the ghc-commits
mailing list