Simon Peyton Jones pushed to branch wip/T23162-part2 at Glasgow Haskell Compiler / GHC Commits: b9e6db41 by Simon Peyton Jones at 2025-12-09T13:00:00+00:00 Ad-hoc change for Givens; PM check only - - - - - 3 changed files: - compiler/GHC/Tc/Solver/FunDeps.hs - testsuite/tests/pmcheck/should_compile/T15753c.hs - testsuite/tests/typecheck/should_compile/T16188.hs Changes: ===================================== compiler/GHC/Tc/Solver/FunDeps.hs ===================================== @@ -484,13 +484,14 @@ tryEqFunDeps work_item@(EqCt { eq_lhs = work_lhs , TyFamLHS fam_tc work_args <- work_lhs -- We have F args ~N# rhs = do { eqs_for_me <- simpleStage $ getInertFamEqsFor fam_tc work_args work_rhs ; simpleStage $ traceTcS "tryEqFunDeps" (ppr work_item $$ ppr eqs_for_me) - ; tryFamEqFunDeps eqs_for_me fam_tc work_args work_item } + ; mode <- simpleStage getTcSMode + ; tryFamEqFunDeps mode eqs_for_me fam_tc work_args work_item } | otherwise = nopStage () -tryFamEqFunDeps :: [EqCt] -> TyCon -> [TcType] -> EqCt -> SolverStage () -tryFamEqFunDeps eqs_for_me fam_tc work_args +tryFamEqFunDeps :: TcSMode -> [EqCt] -> TyCon -> [TcType] -> EqCt -> SolverStage () +tryFamEqFunDeps mode eqs_for_me fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs = work_rhs }) | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc = if isGiven ev @@ -503,9 +504,9 @@ tryFamEqFunDeps eqs_for_me fam_tc work_args do { eqns <- mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs ; tryFDEqns fam_tc work_args work_item eqns } } --- | isGiven ev -- See (INJFAM:Given) --- = nopStage () --- Continue even for Givens in the hope of discovering insolubility + | isGiven ev -- See (INJFAM:Given) + , not (tcsmResumable mode) -- In the pattern-match checker, continue even for + = nopStage () -- Givens in the hope of discovering insolubility -- Only Wanted constraints below here ===================================== testsuite/tests/pmcheck/should_compile/T15753c.hs ===================================== @@ -41,6 +41,20 @@ g1 Refl su1 su2 | STrue <- sIsUnit su1 = case su2 of {} +{- [G] F u1 u2 ~ Char + [W] SBool (IsUnit u1) ~ SBool True +==> + [W] IsUnit u1 ~ True +==> fundep + 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 +-} + g2 :: F u1 u2 :~: Char -> SUnit u1 -> SUnit u2 -> Void ===================================== testsuite/tests/typecheck/should_compile/T16188.hs ===================================== @@ -46,3 +46,14 @@ blah :: forall (t :: Type) (re :: RegExp t). blah (SApp sre1 sre2) = case (sReNotEmpty sre1, sReNotEmpty sre2) of (STrue, STrue) -> () + +{- [W] ReNotEmpty alpha ~ True +--> fundeps + [W] alpha ~ App beta1 beta2 + [W] ReNotEmpty beta1 && ReNotEmpty beta2 ~ True +--> fundeps + alpha := App beta1 beta2 + [W] ReNotEmpty beta1 ~ True + [W] ReNotEmpty beta2 ~ True + +Unproducive loop! +-} View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b9e6db41d40b9f50a3406bc4b29f8d41... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/b9e6db41d40b9f50a3406bc4b29f8d41... You're receiving this email because of your account on gitlab.haskell.org.