Simon Peyton Jones pushed to branch wip/T23162-part2 at Glasgow Haskell Compiler / GHC
Commits:
-
d5e39033
by Simon Peyton Jones at 2025-12-09T15:06:27+00:00
4 changed files:
- compiler/GHC/HsToCore/Monad.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- testsuite/tests/pmcheck/should_compile/T15753c.hs
Changes:
| ... | ... | @@ -115,6 +115,7 @@ import GHC.Tc.Utils.Env (lookupGlobal) |
| 115 | 115 | import GHC.Utils.Error
|
| 116 | 116 | import GHC.Utils.Outputable
|
| 117 | 117 | import GHC.Utils.Panic
|
| 118 | +import GHC.Utils.Misc( HasDebugCallStack )
|
|
| 118 | 119 | import qualified GHC.Data.Strict as Strict
|
| 119 | 120 | |
| 120 | 121 | import Data.IORef
|
| ... | ... | @@ -346,7 +347,7 @@ initDsWithModGuts hsc_env (ModGuts { mg_module = this_mod, mg_binds = binds |
| 346 | 347 | ; runDs hsc_env envs thing_inside
|
| 347 | 348 | }
|
| 348 | 349 | |
| 349 | -initTcDsForSolver :: TcM a -> DsM a
|
|
| 350 | +initTcDsForSolver :: HasDebugCallStack => TcM a -> DsM a
|
|
| 350 | 351 | -- Spin up a TcM context so that we can run the constraint solver
|
| 351 | 352 | -- Returns any error messages generated by the constraint solver
|
| 352 | 353 | -- and (Just res) if no error happened; Nothing if an error happened
|
| ... | ... | @@ -728,7 +728,7 @@ tcCheckGivens :: InertSet -> Bag EvVar -> TcM (Maybe InertSet) |
| 728 | 728 | --
|
| 729 | 729 | -- See Note [Pattern match warnings with insoluble Givens] above.
|
| 730 | 730 | tcCheckGivens inerts given_ids = do
|
| 731 | - (sat, new_inerts) <- runTcSInerts inerts $ do
|
|
| 731 | + mb_res <- tryM $ runTcSInerts inerts $ do
|
|
| 732 | 732 | traceTcS "checkGivens {" (ppr inerts <+> ppr given_ids)
|
| 733 | 733 | lcl_env <- TcS.getLclEnv
|
| 734 | 734 | let given_loc = mkGivenLoc topTcLevel (getSkolemInfo unkSkol) (mkCtLocEnv lcl_env)
|
| ... | ... | @@ -739,7 +739,11 @@ tcCheckGivens inerts given_ids = do |
| 739 | 739 | insols <- try_harder insols
|
| 740 | 740 | traceTcS "checkGivens }" (ppr insols)
|
| 741 | 741 | return (isEmptyBag insols)
|
| 742 | - return $ if sat then Just new_inerts else Nothing
|
|
| 742 | + case mb_res of
|
|
| 743 | + Left _ -> return (Just inerts)
|
|
| 744 | + Right (sat, new_inerts)
|
|
| 745 | + | sat -> return (Just new_inerts)
|
|
| 746 | + | otherwise -> return Nothing -- Definitely unsatisfiable
|
|
| 743 | 747 | where
|
| 744 | 748 | try_harder :: Cts -> TcS Cts
|
| 745 | 749 | -- Maybe we have to search up the superclass chain to find
|
| ... | ... | @@ -1033,7 +1033,7 @@ Here are the KickOut Criteria: |
| 1033 | 1033 | When adding [lhs_w -fw-> rhs_w] to a well-formed terminating substitution S,
|
| 1034 | 1034 | element [lhs_s -fs-> rhs_s] in S meets the KickOut Criteria if:
|
| 1035 | 1035 | |
| 1036 | - (KK0) fw >= fs AND any of (KK1), (KK2) or (KK3) hold
|
|
| 1036 | + (KK0) fw >= fs AND any of (KK1), (KK2), (KK3) or (KK4) hold
|
|
| 1037 | 1037 | |
| 1038 | 1038 | * (KK1: satisfy WF1) `lhs_w` is rewritable in `lhs_s`.
|
| 1039 | 1039 | |
| ... | ... | @@ -1051,8 +1051,9 @@ Here are the KickOut Criteria: |
| 1051 | 1051 | kick out if `rhs_s` is of form `(lhs_w t1 .. tn)`
|
| 1052 | 1052 | |
| 1053 | 1053 | * (KK4: completeness) Kick out if
|
| 1054 | - * lhs_s = F lhs_tys, and
|
|
| 1055 | - * lhs_w is rewritable (anywhere) in rhs_s
|
|
| 1054 | + * (KK4a) lhs_s = F lhs_tys, and
|
|
| 1055 | + * (KK4b) lhs_w is rewritable (anywhere) in rhs_s
|
|
| 1056 | + * (KK4c) F is closed or has injectivity annotions
|
|
| 1056 | 1057 | |
| 1057 | 1058 | Rationale
|
| 1058 | 1059 | |
| ... | ... | @@ -1068,10 +1069,10 @@ Rationale |
| 1068 | 1069 | * (KK3) see Note [KK3: completeness of solving]
|
| 1069 | 1070 | |
| 1070 | 1071 | * (KK4) is about completeness. If we have
|
| 1071 | - Inert: F alpha ~ beta
|
|
| 1072 | + Inert: F alpha ~ [beta]
|
|
| 1072 | 1073 | Work: beta ~ Int
|
| 1073 | 1074 | and F is closed or injective, then we want to kick out the inert item, in
|
| 1074 | - case we get injectivity information from `F alpha ~ Int` that allows us to
|
|
| 1075 | + case we get injectivity information from `F alpha ~ [Int]` that allows us to
|
|
| 1075 | 1076 | solve it.
|
| 1076 | 1077 | |
| 1077 | 1078 | The above story is a bit vague wrt roles, but the code is not.
|
| ... | ... | @@ -41,6 +41,9 @@ g1 Refl su1 su2 |
| 41 | 41 | | STrue <- sIsUnit su1
|
| 42 | 42 | = case su2 of {}
|
| 43 | 43 | |
| 44 | +-- g1a :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void
|
|
| 45 | +-- g1a r _ _ = case r of {} -- Why does this complain about missing Refl
|
|
| 46 | + |
|
| 44 | 47 | {- [G] F u1 u2 ~ Char
|
| 45 | 48 | [W] SBool (IsUnit u1) ~ SBool True
|
| 46 | 49 | ==>
|
| ... | ... | @@ -49,10 +52,9 @@ g1 Refl su1 su2 |
| 49 | 52 | u1 ~ ()
|
| 50 | 53 | |
| 51 | 54 | |
| 52 | -[G] F u1 u2 ~ Char =>(fundep) [W] F u1a u2a ~ F u1 u2
|
|
| 53 | - [W] If (IsUnit u1a) (Case u2b) Int ~ Char
|
|
| 54 | - =>(fundep) [W] IsUnit u1a ~ True
|
|
| 55 | - [W] Case u2b ~ Char <<-- insoluble
|
|
| 55 | +[G] F u1 u2 ~ Char =>(fundep) [W] If (IsUnit u1) (Case u2) Int ~ Char
|
|
| 56 | + =>(fundep) [W] IsUnit u1 ~ True
|
|
| 57 | + [W] Case u2 ~ Char <<-- insoluble: no relevant eqns
|
|
| 56 | 58 | -}
|
| 57 | 59 | |
| 58 | 60 | g2 :: F u1 u2 :~: Char
|