Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC
Commits:
-
4fc4a4f2
by Simon Peyton Jones at 2025-10-21T23:07:07+01:00
-
3030178d
by Simon Peyton Jones at 2025-10-21T23:07:22+01:00
4 changed files:
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
Changes:
| ... | ... | @@ -238,6 +238,16 @@ ill-scoped; an alternative we have not explored. |
| 238 | 238 | |
| 239 | 239 | But see `occCheckExpand` in this module for a function that does, selectively,
|
| 240 | 240 | expand synonyms to reduce free-var occurences.
|
| 241 | + |
|
| 242 | +Note [CoercionHoles and coercion free variables]
|
|
| 243 | +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
| 244 | +Generally, we do not treat a CoercionHole as a free variable of a coercion;
|
|
| 245 | +see `tyCoVarsOfType` and friends.
|
|
| 246 | + |
|
| 247 | +But there is an exception. When finding the free /coercion/ variables of a type,
|
|
| 248 | +in `coVarsOfType`, we /do/ treat a CoercionHole as a free variable. Why?
|
|
| 249 | +The sole reason is in Note [Emitting the residual implication in simplifyInfer]
|
|
| 250 | +in GHC.Tc.Solver. Yuk. This is not pretty.
|
|
| 241 | 251 | -}
|
| 242 | 252 | |
| 243 | 253 | {- *********************************************************************
|
| ... | ... | @@ -352,8 +362,7 @@ deepTcvFolder = TyCoFolder { tcf_view = noView -- See Note [Free vars and synon |
| 352 | 362 | do_hole _is hole = deep_ty (varType (coHoleCoVar hole))
|
| 353 | 363 | -- We don't collect the CoercionHole itself, but we /do/
|
| 354 | 364 | -- need to collect the free variables of its /kind/
|
| 355 | - -- See (CHFV1) in Note [CoercionHoles and coercion free variables]
|
|
| 356 | - -- in GHC.Core.TyCo.Rep
|
|
| 365 | + -- See Note [CoercionHoles and coercion free variables]
|
|
| 357 | 366 | |
| 358 | 367 | {- *********************************************************************
|
| 359 | 368 | * *
|
| ... | ... | @@ -423,7 +432,12 @@ shallowTcvFolder = TyCoFolder { tcf_view = noView -- See Note [Free vars and sy |
| 423 | 432 | Here we are only interested in the free /coercion/ variables.
|
| 424 | 433 | We can achieve this through a slightly different TyCo folder.
|
| 425 | 434 | |
| 426 | -Notice that we look deeply, into kinds.
|
|
| 435 | +Notice that
|
|
| 436 | + |
|
| 437 | +* We look deeply, into kinds.
|
|
| 438 | + |
|
| 439 | +* We /include/ CoercionHoles. Why? Specifically because of #14584,
|
|
| 440 | + Note [Emitting the residual implication in simplifyInfer] in GHC.Tc.Solver
|
|
| 427 | 441 | |
| 428 | 442 | See #14880.
|
| 429 | 443 | -}
|
| ... | ... | @@ -466,9 +480,9 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView |
| 466 | 480 | | otherwise = appEndoOS (deep_cv_ty (varType v)) $
|
| 467 | 481 | acc `extendVarSet` v
|
| 468 | 482 | |
| 469 | - do_hole _ _ = mempty
|
|
| 470 | - -- See (CHFV1) in Note [CoercionHoles and coercion free variables]
|
|
| 471 | - -- in GHC.Core.TyCo.Rep
|
|
| 483 | + do_hole is hole = do_covar is (coHoleCoVar hole)
|
|
| 484 | + -- We /do/ treat a CoercionHole as a free variable
|
|
| 485 | + -- See Note [CoercionHoles and coercion free variables]
|
|
| 472 | 486 | |
| 473 | 487 | ------- Same again, but for DCoVarSet ----------
|
| 474 | 488 | -- But this time the free vars are shallow
|
| ... | ... | @@ -675,7 +689,7 @@ tyCoFVsOfCo (FunCo { fco_mult = w, fco_arg = co1, fco_res = co2 }) fv_cand in_sc |
| 675 | 689 | tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc
|
| 676 | 690 | = tyCoFVsOfCoVar v fv_cand in_scope acc
|
| 677 | 691 | tyCoFVsOfCo (HoleCo {}) fv_cand in_scope acc = emptyFV fv_cand in_scope acc
|
| 678 | - -- Ignore holes: see (CHFV1) in Note [CoercionHoles and coercion free variables]
|
|
| 692 | + -- Ignore holes: Note [CoercionHoles and coercion free variables]
|
|
| 679 | 693 | tyCoFVsOfCo (AxiomCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc
|
| 680 | 694 | tyCoFVsOfCo (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = deps}) fv_cand in_scope acc
|
| 681 | 695 | = (tyCoFVsOfCos deps `unionFV` tyCoFVsOfType t1
|
| ... | ... | @@ -1687,7 +1687,7 @@ holes `HoleCo`, which get filled in later. |
| 1687 | 1687 | -- | A coercion to be filled in by the type-checker. See Note [Coercion holes]
|
| 1688 | 1688 | data CoercionHole
|
| 1689 | 1689 | = CoercionHole { ch_co_var :: CoVar
|
| 1690 | - -- See Note [CoercionHoles and coercion free variables]
|
|
| 1690 | + -- See Note [Coercion holes] wrinkle (COH2)
|
|
| 1691 | 1691 | |
| 1692 | 1692 | , ch_ref :: IORef (Maybe (Coercion, CoHoleSet))
|
| 1693 | 1693 | -- The CoHoleSet is (possibly a superset of)
|
| ... | ... | @@ -1789,38 +1789,24 @@ the evidence for unboxed equalities: |
| 1789 | 1789 | |
| 1790 | 1790 | Other notes about HoleCo:
|
| 1791 | 1791 | |
| 1792 | - * INVARIANT: CoercionHole and HoleCo are used only during type checking,
|
|
| 1792 | +(COH1) INVARIANT: CoercionHole and HoleCo are used only during type checking,
|
|
| 1793 | 1793 | and should never appear in Core. Just like unification variables; a Type
|
| 1794 | 1794 | can contain a TcTyVar, but only during type checking. If, one day, we
|
| 1795 | 1795 | use type-level information to separate out forms that can appear during
|
| 1796 | 1796 | type-checking vs forms that can appear in core proper, holes in Core will
|
| 1797 | 1797 | be ruled out.
|
| 1798 | 1798 | |
| 1799 | - * See Note [CoercionHoles and coercion free variables]
|
|
| 1800 | - |
|
| 1801 | - * Coercion holes can be compared for equality like other coercions:
|
|
| 1802 | - by looking at the types coerced.
|
|
| 1803 | - |
|
| 1804 | - |
|
| 1805 | -Note [CoercionHoles and coercion free variables]
|
|
| 1806 | -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
| 1807 | -Why does a CoercionHole contain a CoVar, as well as reference to fill in?
|
|
| 1799 | +(COH2) Why does a CoercionHole contain a CoVar, as well as reference to fill in?
|
|
| 1808 | 1800 | * It really helps for debug pretty-printing.
|
| 1809 | 1801 | * It carries a type which makes `coercionKind` and `coercionRole` work
|
| 1810 | 1802 | * It has a Unique, which gives the hole an identity; see calls to `ctEvEvId`
|
| 1811 | 1803 | |
| 1812 | -(CHFV1) We do not treat a CoercionHole as a free variable of a coercion.
|
|
| 1813 | - In the past we did: See #14584, and Note [What prevents a constraint from floating]
|
|
| 1814 | - in GHC.Tc.Solver, item (4):
|
|
| 1804 | +(COH3) See Note [CoercionHoles and coercion free variables] in GHC.Core.TyCo.FVs
|
|
| 1815 | 1805 | |
| 1816 | - forall k. [W] co1 :: t1 ~# t2 |> co2
|
|
| 1817 | - [W] co2 :: k ~# *
|
|
| 1806 | +(COH4) Coercion holes can be compared for equality like other coercions:
|
|
| 1807 | + by looking at the types coerced.
|
|
| 1818 | 1808 | |
| 1819 | - Here co2 is a CoercionHole. But we /must/ know that it is free in
|
|
| 1820 | - co1, because that's all that stops it floating outside the
|
|
| 1821 | - implication.
|
|
| 1822 | 1809 | |
| 1823 | - But nowadays this is all irrelevant because we don't float constraints.
|
|
| 1824 | 1810 | |
| 1825 | 1811 | Note [CoercionHoles and CoHoleSets]
|
| 1826 | 1812 | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
|
| ... | ... | @@ -543,6 +543,7 @@ can_eq_nc_forall ev eq_rel s1 s2 |
| 543 | 543 | |
| 544 | 544 | -- Generate and solve the constraints that live in the body of the implication
|
| 545 | 545 | -- See (SF5) and (SF6) in Note [Solving forall equalities]
|
| 546 | + ; nested_ev_binds_var <- newNoTcEvBinds
|
|
| 546 | 547 | ; (unifs, (all_co, solved))
|
| 547 | 548 | <- reportFineGrainUnifications $
|
| 548 | 549 | do { -- Generate constraints
|
| ... | ... | @@ -553,13 +554,8 @@ can_eq_nc_forall ev eq_rel s1 s2 |
| 553 | 554 | |
| 554 | 555 | ; traceTcS "Trying to solve the implication" (ppr s1 $$ ppr s2 $$ ppr wanteds)
|
| 555 | 556 | |
| 556 | - -- Solve the `wanteds` in a nested context
|
|
| 557 | - -- Use the /same/ TcEvBinds var as the context; we do not expect any dict binds
|
|
| 558 | - -- but we do want to record any used Given coercions (in `evb_tcvs`) so that
|
|
| 559 | - -- they are kept alive by `neededEvVars`. Admittedly they are free in `all_co`,
|
|
| 560 | - -- but only if we zonk it, which `neededEvVars` does not do (see test T7196).
|
|
| 561 | - ; ev_binds_var <- getTcEvBindsVar
|
|
| 562 | - ; residual_wanted <- nestImplicTcS skol_info_anon ev_binds_var tclvl $
|
|
| 557 | + -- Solve the `wanteds` in a nested context.
|
|
| 558 | + ; residual_wanted <- nestImplicTcS skol_info_anon nested_ev_binds_var tclvl $
|
|
| 563 | 559 | solveSimpleWanteds wanteds
|
| 564 | 560 | |
| 565 | 561 | ; return (all_co, isSolvedWC residual_wanted) }
|
| ... | ... | @@ -568,7 +564,13 @@ can_eq_nc_forall ev eq_rel s1 s2 |
| 568 | 564 | ; kickOutAfterUnification unifs
|
| 569 | 565 | |
| 570 | 566 | ; if solved
|
| 571 | - then do { setWantedEq orig_dest emptyCoHoleSet all_co
|
|
| 567 | + then do { -- Record any used used Given coercions (in `evb_tcvs`) so that
|
|
| 568 | + -- they are kept alive by `neededEvVars`. Admittedly they are free in `all_co`,
|
|
| 569 | + -- but only if we zonk it, which `neededEvVars` does not do (see test T7196).
|
|
| 570 | + ev_binds_var <- getTcEvBindsVar
|
|
| 571 | + ; updTcEvBinds ev_binds_var nested_ev_binds_var
|
|
| 572 | + |
|
| 573 | + ; setWantedEq orig_dest emptyCoHoleSet all_co
|
|
| 572 | 574 | -- emptyCoHoleSet: fully solved, so all_co has no holes
|
| 573 | 575 | ; stopWith ev "Polytype equality: solved" }
|
| 574 | 576 |
| ... | ... | @@ -20,7 +20,7 @@ module GHC.Tc.Solver.Monad ( |
| 20 | 20 | failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS,
|
| 21 | 21 | runTcSEqualities,
|
| 22 | 22 | nestTcS, nestImplicTcS, tryShortCutTcS, nestFunDepsTcS,
|
| 23 | - setEvBindsTcS, setTcLevelTcS,
|
|
| 23 | + setEvBindsTcS, setTcLevelTcS, updTcEvBinds,
|
|
| 24 | 24 | |
| 25 | 25 | selectNextWorkItem,
|
| 26 | 26 | getWorkList,
|
| ... | ... | @@ -1434,6 +1434,10 @@ setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS () |
| 1434 | 1434 | setTcEvBindsMap ev_binds_var binds
|
| 1435 | 1435 | = wrapTcS $ TcM.setTcEvBindsMap ev_binds_var binds
|
| 1436 | 1436 | |
| 1437 | +updTcEvBinds :: EvBindsVar -> EvBindsVar -> TcS ()
|
|
| 1438 | +updTcEvBinds evb nested_evb
|
|
| 1439 | + = wrapTcS $ TcM.updTcEvBinds evb nested_evb
|
|
| 1440 | + |
|
| 1437 | 1441 | getDefaultInfo :: TcS (DefaultEnv, Bool)
|
| 1438 | 1442 | getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
|
| 1439 | 1443 |