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 Working on pm-check [skip ci] - - - - - 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: ===================================== compiler/GHC/HsToCore/Monad.hs ===================================== @@ -115,6 +115,7 @@ import GHC.Tc.Utils.Env (lookupGlobal) import GHC.Utils.Error import GHC.Utils.Outputable import GHC.Utils.Panic +import GHC.Utils.Misc( HasDebugCallStack ) import qualified GHC.Data.Strict as Strict import Data.IORef @@ -346,7 +347,7 @@ initDsWithModGuts hsc_env (ModGuts { mg_module = this_mod, mg_binds = binds ; runDs hsc_env envs thing_inside } -initTcDsForSolver :: TcM a -> DsM a +initTcDsForSolver :: HasDebugCallStack => TcM a -> DsM a -- Spin up a TcM context so that we can run the constraint solver -- Returns any error messages generated by the constraint solver -- and (Just res) if no error happened; Nothing if an error happened ===================================== compiler/GHC/Tc/Solver.hs ===================================== @@ -728,7 +728,7 @@ tcCheckGivens :: InertSet -> Bag EvVar -> TcM (Maybe InertSet) -- -- See Note [Pattern match warnings with insoluble Givens] above. tcCheckGivens inerts given_ids = do - (sat, new_inerts) <- runTcSInerts inerts $ do + mb_res <- tryM $ runTcSInerts inerts $ do traceTcS "checkGivens {" (ppr inerts <+> ppr given_ids) lcl_env <- TcS.getLclEnv let given_loc = mkGivenLoc topTcLevel (getSkolemInfo unkSkol) (mkCtLocEnv lcl_env) @@ -739,7 +739,11 @@ tcCheckGivens inerts given_ids = do insols <- try_harder insols traceTcS "checkGivens }" (ppr insols) return (isEmptyBag insols) - return $ if sat then Just new_inerts else Nothing + case mb_res of + Left _ -> return (Just inerts) + Right (sat, new_inerts) + | sat -> return (Just new_inerts) + | otherwise -> return Nothing -- Definitely unsatisfiable where try_harder :: Cts -> TcS Cts -- Maybe we have to search up the superclass chain to find ===================================== compiler/GHC/Tc/Solver/InertSet.hs ===================================== @@ -1033,7 +1033,7 @@ Here are the KickOut Criteria: When adding [lhs_w -fw-> rhs_w] to a well-formed terminating substitution S, element [lhs_s -fs-> rhs_s] in S meets the KickOut Criteria if: - (KK0) fw >= fs AND any of (KK1), (KK2) or (KK3) hold + (KK0) fw >= fs AND any of (KK1), (KK2), (KK3) or (KK4) hold * (KK1: satisfy WF1) `lhs_w` is rewritable in `lhs_s`. @@ -1051,8 +1051,9 @@ Here are the KickOut Criteria: kick out if `rhs_s` is of form `(lhs_w t1 .. tn)` * (KK4: completeness) Kick out if - * lhs_s = F lhs_tys, and - * lhs_w is rewritable (anywhere) in rhs_s + * (KK4a) lhs_s = F lhs_tys, and + * (KK4b) lhs_w is rewritable (anywhere) in rhs_s + * (KK4c) F is closed or has injectivity annotions Rationale @@ -1068,10 +1069,10 @@ Rationale * (KK3) see Note [KK3: completeness of solving] * (KK4) is about completeness. If we have - Inert: F alpha ~ beta + Inert: F alpha ~ [beta] Work: beta ~ Int and F is closed or injective, then we want to kick out the inert item, in - case we get injectivity information from `F alpha ~ Int` that allows us to + case we get injectivity information from `F alpha ~ [Int]` that allows us to solve it. The above story is a bit vague wrt roles, but the code is not. ===================================== testsuite/tests/pmcheck/should_compile/T15753c.hs ===================================== @@ -41,6 +41,9 @@ g1 Refl su1 su2 | STrue <- sIsUnit su1 = case su2 of {} +-- g1a :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void +-- g1a r _ _ = case r of {} -- Why does this complain about missing Refl + {- [G] F u1 u2 ~ Char [W] SBool (IsUnit u1) ~ SBool True ==> @@ -49,10 +52,9 @@ g1 Refl su1 su2 u1 ~ () -[G] F u1 u2 ~ Char =>(fundep) [W] F u1a u2a ~ F u1 u2 - [W] If (IsUnit u1a) (Case u2b) Int ~ Char - =>(fundep) [W] IsUnit u1a ~ True - [W] Case u2b ~ Char <<-- insoluble +[G] F u1 u2 ~ Char =>(fundep) [W] If (IsUnit u1) (Case u2) Int ~ Char + =>(fundep) [W] IsUnit u1 ~ True + [W] Case u2 ~ Char <<-- insoluble: no relevant eqns -} g2 :: F u1 u2 :~: Char View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d5e390335cbf0c5da317b5749408c3bf... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/d5e390335cbf0c5da317b5749408c3bf... You're receiving this email because of your account on gitlab.haskell.org.