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
3 changed files:
- compiler/GHC/Tc/Solver/FunDeps.hs
- testsuite/tests/pmcheck/should_compile/T15753c.hs
- testsuite/tests/typecheck/should_compile/T16188.hs
Changes:
| ... | ... | @@ -484,13 +484,14 @@ tryEqFunDeps work_item@(EqCt { eq_lhs = work_lhs |
| 484 | 484 | , TyFamLHS fam_tc work_args <- work_lhs -- We have F args ~N# rhs
|
| 485 | 485 | = do { eqs_for_me <- simpleStage $ getInertFamEqsFor fam_tc work_args work_rhs
|
| 486 | 486 | ; simpleStage $ traceTcS "tryEqFunDeps" (ppr work_item $$ ppr eqs_for_me)
|
| 487 | - ; tryFamEqFunDeps eqs_for_me fam_tc work_args work_item }
|
|
| 487 | + ; mode <- simpleStage getTcSMode
|
|
| 488 | + ; tryFamEqFunDeps mode eqs_for_me fam_tc work_args work_item }
|
|
| 488 | 489 | | otherwise
|
| 489 | 490 | = nopStage ()
|
| 490 | 491 | |
| 491 | 492 | |
| 492 | -tryFamEqFunDeps :: [EqCt] -> TyCon -> [TcType] -> EqCt -> SolverStage ()
|
|
| 493 | -tryFamEqFunDeps eqs_for_me fam_tc work_args
|
|
| 493 | +tryFamEqFunDeps :: TcSMode -> [EqCt] -> TyCon -> [TcType] -> EqCt -> SolverStage ()
|
|
| 494 | +tryFamEqFunDeps mode eqs_for_me fam_tc work_args
|
|
| 494 | 495 | work_item@(EqCt { eq_ev = ev, eq_rhs = work_rhs })
|
| 495 | 496 | | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
|
| 496 | 497 | = if isGiven ev
|
| ... | ... | @@ -503,9 +504,9 @@ tryFamEqFunDeps eqs_for_me fam_tc work_args |
| 503 | 504 | do { eqns <- mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs
|
| 504 | 505 | ; tryFDEqns fam_tc work_args work_item eqns } }
|
| 505 | 506 | |
| 506 | --- | isGiven ev -- See (INJFAM:Given)
|
|
| 507 | --- = nopStage ()
|
|
| 508 | --- Continue even for Givens in the hope of discovering insolubility
|
|
| 507 | + | isGiven ev -- See (INJFAM:Given)
|
|
| 508 | + , not (tcsmResumable mode) -- In the pattern-match checker, continue even for
|
|
| 509 | + = nopStage () -- Givens in the hope of discovering insolubility
|
|
| 509 | 510 | |
| 510 | 511 | -- Only Wanted constraints below here
|
| 511 | 512 |
| ... | ... | @@ -41,6 +41,20 @@ g1 Refl su1 su2 |
| 41 | 41 | | STrue <- sIsUnit su1
|
| 42 | 42 | = case su2 of {}
|
| 43 | 43 | |
| 44 | +{- [G] F u1 u2 ~ Char
|
|
| 45 | + [W] SBool (IsUnit u1) ~ SBool True
|
|
| 46 | +==>
|
|
| 47 | + [W] IsUnit u1 ~ True
|
|
| 48 | +==> fundep
|
|
| 49 | + u1 ~ ()
|
|
| 50 | + |
|
| 51 | + |
|
| 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
|
|
| 56 | +-}
|
|
| 57 | + |
|
| 44 | 58 | g2 :: F u1 u2 :~: Char
|
| 45 | 59 | -> SUnit u1 -> SUnit u2
|
| 46 | 60 | -> Void
|
| ... | ... | @@ -46,3 +46,14 @@ blah :: forall (t :: Type) (re :: RegExp t). |
| 46 | 46 | blah (SApp sre1 sre2)
|
| 47 | 47 | = case (sReNotEmpty sre1, sReNotEmpty sre2) of
|
| 48 | 48 | (STrue, STrue) -> ()
|
| 49 | + |
|
| 50 | +{- [W] ReNotEmpty alpha ~ True
|
|
| 51 | +--> fundeps
|
|
| 52 | + [W] alpha ~ App beta1 beta2
|
|
| 53 | + [W] ReNotEmpty beta1 && ReNotEmpty beta2 ~ True
|
|
| 54 | +--> fundeps + alpha := App beta1 beta2
|
|
| 55 | + [W] ReNotEmpty beta1 ~ True
|
|
| 56 | + [W] ReNotEmpty beta2 ~ True
|
|
| 57 | + |
|
| 58 | +Unproducive loop!
|
|
| 59 | +-} |