Simon Peyton Jones pushed to branch wip/T26115 at Glasgow Haskell Compiler / GHC
Commits:
-
5c2484eb
by Simon Peyton Jones at 2025-06-22T23:56:27+01:00
5 changed files:
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Solver/Solve.hs
- compiler/GHC/Tc/Types/Constraint.hs
Changes:
| ... | ... | @@ -1137,7 +1137,10 @@ matchLocalInst body_pred loc |
| 1137 | 1137 | match_local_inst inerts (qci@(QCI { qci_tvs = qtvs
|
| 1138 | 1138 | , qci_body = qbody
|
| 1139 | 1139 | , qci_ev = qev })
|
| 1140 | - :qcis)
|
|
| 1140 | + : qcis)
|
|
| 1141 | + | isWanted qev -- Skip Wanteds
|
|
| 1142 | + = match_local_inst inerts qcis
|
|
| 1143 | + |
|
| 1141 | 1144 | | let in_scope = mkInScopeSet (qtv_set `unionVarSet` body_pred_tv_set)
|
| 1142 | 1145 | , Just tv_subst <- ruleMatchTyKiX qtv_set (mkRnEnv2 in_scope)
|
| 1143 | 1146 | emptyTvSubstEnv qbody body_pred
|
| ... | ... | @@ -1875,8 +1875,9 @@ noGivenNewtypeReprEqs tc (IS { inert_cans = inerts }) |
| 1875 | 1875 | | otherwise
|
| 1876 | 1876 | = False
|
| 1877 | 1877 | |
| 1878 | - might_help_qc (QCI { qci_body = pred })
|
|
| 1879 | - | ClassPred cls [_, t1, t2] <- classifyPredType pred
|
|
| 1878 | + might_help_qc (QCI { qci_ev = ev, qci_body = pred })
|
|
| 1879 | + | isGiven ev
|
|
| 1880 | + , ClassPred cls [_, t1, t2] <- classifyPredType pred
|
|
| 1880 | 1881 | , cls `hasKey` coercibleTyConKey
|
| 1881 | 1882 | = headed_by_tc t1 t2
|
| 1882 | 1883 | | otherwise
|
| ... | ... | @@ -2380,9 +2380,6 @@ unifyForAllBody :: CtEvidence -> Role -> (UnifyEnv -> TcM a) |
| 2380 | 2380 | -- See See (SF5) in Note [Solving forall equalities] in GHC.Tc.Solver.Equality
|
| 2381 | 2381 | unifyForAllBody ev role unify_body
|
| 2382 | 2382 | = do { (res, cts, unified) <- wrapUnifierX ev role unify_body
|
| 2383 | - -- Ignore the rewriters. They are used in wrapUnifierTcS only
|
|
| 2384 | - -- as an optimistion to prioritise the work list; but they are
|
|
| 2385 | - -- /also/ stored in each individual constraint we return.
|
|
| 2386 | 2383 | |
| 2387 | 2384 | -- Kick out any inert constraint that we have unified
|
| 2388 | 2385 | ; _ <- kickOutAfterUnification unified
|
| ... | ... | @@ -280,7 +280,7 @@ solveNestedImplications implics |
| 280 | 280 | ; return unsolved_implics }
|
| 281 | 281 | |
| 282 | 282 | solveImplication :: Implication -- Wanted
|
| 283 | - -> TcS Implication -- Simplified implication (empty or singleton)
|
|
| 283 | + -> TcS Implication -- Simplified implication
|
|
| 284 | 284 | -- Precondition: The TcS monad contains an empty worklist and given-only inerts
|
| 285 | 285 | -- which after trying to solve this implication we must restore to their original value
|
| 286 | 286 | solveImplication imp@(Implic { ic_tclvl = tclvl
|
| ... | ... | @@ -1318,11 +1318,11 @@ try_inert_qcs (QCI { qci_ev = ev_w }) inerts = |
| 1318 | 1318 | -- See Note [Solving a Wanted forall-constraint]
|
| 1319 | 1319 | solveWantedForAll_norm :: WantedCtEvidence -> [TcTyVar] -> TcThetaType -> PredType
|
| 1320 | 1320 | -> SolverStage Void
|
| 1321 | -solveWantedForAll_norm wtd@(WantedCt { ctev_dest = dest, ctev_loc = loc
|
|
| 1321 | +solveWantedForAll_norm wtd@(WantedCt { ctev_dest = dest, ctev_loc = ct_loc
|
|
| 1322 | 1322 | , ctev_rewriters = rewriters })
|
| 1323 | 1323 | tvs theta body_pred
|
| 1324 | 1324 | = Stage $
|
| 1325 | - TcS.setSrcSpan (getCtLocEnvLoc $ ctLocEnv loc) $
|
|
| 1325 | + TcS.setSrcSpan (getCtLocEnvLoc loc_env) $
|
|
| 1326 | 1326 | -- This setSrcSpan is important: the emitImplicationTcS uses that
|
| 1327 | 1327 | -- TcLclEnv for the implication, and that in turn sets the location
|
| 1328 | 1328 | -- for the Givens when solving the constraint (#21006)
|
| ... | ... | @@ -1339,24 +1339,38 @@ solveWantedForAll_norm wtd@(WantedCt { ctev_dest = dest, ctev_loc = loc |
| 1339 | 1339 | ; given_ev_vars <- mapM newEvVar inst_theta
|
| 1340 | 1340 | ; (lvl, (w_id, wanteds))
|
| 1341 | 1341 | <- pushLevelNoWorkList (ppr skol_info) $
|
| 1342 | - do { let loc' = setCtLocOrigin loc (ScOrigin is_qc NakedSc)
|
|
| 1342 | + do { let ct_loc' = setCtLocOrigin ct_loc (ScOrigin is_qc NakedSc)
|
|
| 1343 | 1343 | -- Set the thing to prove to have a ScOrigin, so we are
|
| 1344 | 1344 | -- careful about its termination checks.
|
| 1345 | 1345 | -- See (QC-INV) in Note [Solving a Wanted forall-constraint]
|
| 1346 | - ; wanted_ev <- newWantedNC loc' rewriters inst_pred
|
|
| 1346 | + ; wanted_ev <- newWantedNC ct_loc' rewriters inst_pred
|
|
| 1347 | 1347 | -- NB: inst_pred can be an equality
|
| 1348 | 1348 | ; return ( wantedCtEvEvId wanted_ev
|
| 1349 | 1349 | , unitBag (mkNonCanonical $ CtWanted wanted_ev)) }
|
| 1350 | 1350 | |
| 1351 | 1351 | ; traceTcS "solveForAll" (ppr given_ev_vars $$ ppr wanteds $$ ppr w_id)
|
| 1352 | - ; ev_binds <- emitImplicationTcS lvl skol_info_anon skol_tvs given_ev_vars wanteds
|
|
| 1352 | + ; ev_binds_var <- newTcEvBinds
|
|
| 1353 | + ; solved <- trySolveImplication $
|
|
| 1354 | + implicationPrototype loc_env
|
|
| 1355 | + { ic_tclvl = lvl
|
|
| 1356 | + , ic_binds = ev_binds_var
|
|
| 1357 | + , ic_info = skol_info_anon
|
|
| 1358 | + , ic_warn_inacessible = False
|
|
| 1359 | + , ic_skols = skol_tvs
|
|
| 1360 | + , ic_given = given_ev_vars
|
|
| 1361 | + , ic_wanted = emptyWC { wc_simple = wanteds } }
|
|
| 1362 | + ; if not solved
|
|
| 1363 | + then updInertIrreds (
|
|
| 1364 | + else
|
|
| 1365 | + do { ev_binds <- emitImplicationTcS lvl skol_info_anon skol_tvs given_ev_vars wanteds
|
|
| 1353 | 1366 | |
| 1354 | 1367 | ; setWantedEvTerm dest EvCanonical $
|
| 1355 | 1368 | EvFun { et_tvs = skol_tvs, et_given = given_ev_vars
|
| 1356 | 1369 | , et_binds = ev_binds, et_body = w_id }
|
| 1357 | 1370 | ; stopWith (CtWanted wtd) "Wanted forall-constraint (implication)" }
|
| 1358 | 1371 | where
|
| 1359 | - is_qc = IsQC (ctLocOrigin loc)
|
|
| 1372 | + loc_env = ctLocEnv loc
|
|
| 1373 | + is_qc = IsQC (ctLocOrigin ct_loc)
|
|
| 1360 | 1374 | |
| 1361 | 1375 | empty_subst = mkEmptySubst $ mkInScopeSet $
|
| 1362 | 1376 | tyCoVarsOfTypes (body_pred:theta) `delVarSetList` tvs
|
| ... | ... | @@ -990,8 +990,9 @@ pendingScDict_maybe _ = Nothing |
| 990 | 990 | |
| 991 | 991 | pendingScInst_maybe :: QCInst -> Maybe QCInst
|
| 992 | 992 | -- Same as isPendingScDict, but for QCInsts
|
| 993 | -pendingScInst_maybe qci@(QCI { qci_pend_sc = f })
|
|
| 994 | - | pendingFuel f = Just (qci { qci_pend_sc = doNotExpand })
|
|
| 993 | +pendingScInst_maybe qci@(QCI { qci_flav = flav, qci_pend_sc = f })
|
|
| 994 | + | Given <- flav -- Do not expand Wanted QCIs
|
|
| 995 | + , pendingFuel f = Just (qci { qci_pend_sc = doNotExpand })
|
|
| 995 | 996 | | otherwise = Nothing
|
| 996 | 997 | |
| 997 | 998 | superClassesMightHelp :: WantedConstraints -> Bool
|