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 Wibble CoercionHole free vars - - - - - 3030178d by Simon Peyton Jones at 2025-10-21T23:07:22+01:00 Wibble improve forall - - - - - 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: ===================================== compiler/GHC/Core/TyCo/FVs.hs ===================================== @@ -238,6 +238,16 @@ ill-scoped; an alternative we have not explored. But see `occCheckExpand` in this module for a function that does, selectively, expand synonyms to reduce free-var occurences. + +Note [CoercionHoles and coercion free variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Generally, we do not treat a CoercionHole as a free variable of a coercion; +see `tyCoVarsOfType` and friends. + +But there is an exception. When finding the free /coercion/ variables of a type, +in `coVarsOfType`, we /do/ treat a CoercionHole as a free variable. Why? +The sole reason is in Note [Emitting the residual implication in simplifyInfer] +in GHC.Tc.Solver. Yuk. This is not pretty. -} {- ********************************************************************* @@ -352,8 +362,7 @@ deepTcvFolder = TyCoFolder { tcf_view = noView -- See Note [Free vars and synon do_hole _is hole = deep_ty (varType (coHoleCoVar hole)) -- We don't collect the CoercionHole itself, but we /do/ -- need to collect the free variables of its /kind/ - -- See (CHFV1) in Note [CoercionHoles and coercion free variables] - -- in GHC.Core.TyCo.Rep + -- See Note [CoercionHoles and coercion free variables] {- ********************************************************************* * * @@ -423,7 +432,12 @@ shallowTcvFolder = TyCoFolder { tcf_view = noView -- See Note [Free vars and sy Here we are only interested in the free /coercion/ variables. We can achieve this through a slightly different TyCo folder. -Notice that we look deeply, into kinds. +Notice that + +* We look deeply, into kinds. + +* We /include/ CoercionHoles. Why? Specifically because of #14584, + Note [Emitting the residual implication in simplifyInfer] in GHC.Tc.Solver See #14880. -} @@ -466,9 +480,9 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView | otherwise = appEndoOS (deep_cv_ty (varType v)) $ acc `extendVarSet` v - do_hole _ _ = mempty - -- See (CHFV1) in Note [CoercionHoles and coercion free variables] - -- in GHC.Core.TyCo.Rep + do_hole is hole = do_covar is (coHoleCoVar hole) + -- We /do/ treat a CoercionHole as a free variable + -- See Note [CoercionHoles and coercion free variables] ------- Same again, but for DCoVarSet ---------- -- 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 tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc = tyCoFVsOfCoVar v fv_cand in_scope acc tyCoFVsOfCo (HoleCo {}) fv_cand in_scope acc = emptyFV fv_cand in_scope acc - -- Ignore holes: see (CHFV1) in Note [CoercionHoles and coercion free variables] + -- Ignore holes: Note [CoercionHoles and coercion free variables] tyCoFVsOfCo (AxiomCo _ cs) fv_cand in_scope acc = tyCoFVsOfCos cs fv_cand in_scope acc tyCoFVsOfCo (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = deps}) fv_cand in_scope acc = (tyCoFVsOfCos deps `unionFV` tyCoFVsOfType t1 ===================================== compiler/GHC/Core/TyCo/Rep.hs ===================================== @@ -1687,7 +1687,7 @@ holes `HoleCo`, which get filled in later. -- | A coercion to be filled in by the type-checker. See Note [Coercion holes] data CoercionHole = CoercionHole { ch_co_var :: CoVar - -- See Note [CoercionHoles and coercion free variables] + -- See Note [Coercion holes] wrinkle (COH2) , ch_ref :: IORef (Maybe (Coercion, CoHoleSet)) -- The CoHoleSet is (possibly a superset of) @@ -1789,38 +1789,24 @@ the evidence for unboxed equalities: Other notes about HoleCo: - * INVARIANT: CoercionHole and HoleCo are used only during type checking, +(COH1) INVARIANT: CoercionHole and HoleCo are used only during type checking, and should never appear in Core. Just like unification variables; a Type can contain a TcTyVar, but only during type checking. If, one day, we use type-level information to separate out forms that can appear during type-checking vs forms that can appear in core proper, holes in Core will be ruled out. - * See Note [CoercionHoles and coercion free variables] - - * Coercion holes can be compared for equality like other coercions: - by looking at the types coerced. - - -Note [CoercionHoles and coercion free variables] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Why does a CoercionHole contain a CoVar, as well as reference to fill in? +(COH2) Why does a CoercionHole contain a CoVar, as well as reference to fill in? * It really helps for debug pretty-printing. * It carries a type which makes `coercionKind` and `coercionRole` work * It has a Unique, which gives the hole an identity; see calls to `ctEvEvId` -(CHFV1) We do not treat a CoercionHole as a free variable of a coercion. - In the past we did: See #14584, and Note [What prevents a constraint from floating] - in GHC.Tc.Solver, item (4): +(COH3) See Note [CoercionHoles and coercion free variables] in GHC.Core.TyCo.FVs - forall k. [W] co1 :: t1 ~# t2 |> co2 - [W] co2 :: k ~# * +(COH4) Coercion holes can be compared for equality like other coercions: + by looking at the types coerced. - Here co2 is a CoercionHole. But we /must/ know that it is free in - co1, because that's all that stops it floating outside the - implication. - But nowadays this is all irrelevant because we don't float constraints. Note [CoercionHoles and CoHoleSets] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -543,6 +543,7 @@ can_eq_nc_forall ev eq_rel s1 s2 -- Generate and solve the constraints that live in the body of the implication -- See (SF5) and (SF6) in Note [Solving forall equalities] + ; nested_ev_binds_var <- newNoTcEvBinds ; (unifs, (all_co, solved)) <- reportFineGrainUnifications $ do { -- Generate constraints @@ -553,13 +554,8 @@ can_eq_nc_forall ev eq_rel s1 s2 ; traceTcS "Trying to solve the implication" (ppr s1 $$ ppr s2 $$ ppr wanteds) - -- Solve the `wanteds` in a nested context - -- Use the /same/ TcEvBinds var as the context; we do not expect any dict binds - -- but we do want to record any used Given coercions (in `evb_tcvs`) so that - -- they are kept alive by `neededEvVars`. Admittedly they are free in `all_co`, - -- but only if we zonk it, which `neededEvVars` does not do (see test T7196). - ; ev_binds_var <- getTcEvBindsVar - ; residual_wanted <- nestImplicTcS skol_info_anon ev_binds_var tclvl $ + -- Solve the `wanteds` in a nested context. + ; residual_wanted <- nestImplicTcS skol_info_anon nested_ev_binds_var tclvl $ solveSimpleWanteds wanteds ; return (all_co, isSolvedWC residual_wanted) } @@ -568,7 +564,13 @@ can_eq_nc_forall ev eq_rel s1 s2 ; kickOutAfterUnification unifs ; if solved - then do { setWantedEq orig_dest emptyCoHoleSet all_co + then do { -- Record any used used Given coercions (in `evb_tcvs`) so that + -- they are kept alive by `neededEvVars`. Admittedly they are free in `all_co`, + -- but only if we zonk it, which `neededEvVars` does not do (see test T7196). + ev_binds_var <- getTcEvBindsVar + ; updTcEvBinds ev_binds_var nested_ev_binds_var + + ; setWantedEq orig_dest emptyCoHoleSet all_co -- emptyCoHoleSet: fully solved, so all_co has no holes ; stopWith ev "Polytype equality: solved" } ===================================== compiler/GHC/Tc/Solver/Monad.hs ===================================== @@ -20,7 +20,7 @@ module GHC.Tc.Solver.Monad ( failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS, runTcSEqualities, nestTcS, nestImplicTcS, tryShortCutTcS, nestFunDepsTcS, - setEvBindsTcS, setTcLevelTcS, + setEvBindsTcS, setTcLevelTcS, updTcEvBinds, selectNextWorkItem, getWorkList, @@ -1434,6 +1434,10 @@ setTcEvBindsMap :: EvBindsVar -> EvBindMap -> TcS () setTcEvBindsMap ev_binds_var binds = wrapTcS $ TcM.setTcEvBindsMap ev_binds_var binds +updTcEvBinds :: EvBindsVar -> EvBindsVar -> TcS () +updTcEvBinds evb nested_evb + = wrapTcS $ TcM.updTcEvBinds evb nested_evb + getDefaultInfo :: TcS (DefaultEnv, Bool) getDefaultInfo = wrapTcS TcM.tcGetDefaultTys View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/8a9962249f6f9c0f7e18d88971afdee... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/8a9962249f6f9c0f7e18d88971afdee... You're receiving this email because of your account on gitlab.haskell.org.