GitLab

Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC

Commits:

ec1eeb9e

by Simon Peyton Jones at 2025-10-15T22:46:20+01:00

Do not treat CoercionHoles as free variables in coercions

2 changed files:

compiler/GHC/Core/TyCo/FVs.hs
compiler/GHC/Core/TyCo/Rep.hs

Changes:

compiler/GHC/Core/TyCo/FVs.hs

@@ -339,9 +339,8 @@ deepTcvFolder = TyCoFolder { tcf_view = noView  -- See Note [Free vars and synon
                                           acc `extendVarSet` v
      do_bndr is tcv _ = extendVarSet is tcv
 -    do_hole is hole  = do_tcv is (coHoleCoVar hole)
 -                       -- See Note [CoercionHoles and coercion free variables]
 -                       -- in GHC.Core.TyCo.Rep
 +    do_hole _ _  = mempty  -- See (CHFV1) in Note [CoercionHoles and coercion free variables]
 +                           -- in GHC.Core.TyCo.Rep
  {- *********************************************************************
  *                                                                      *
@@ -445,6 +444,8 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView
        -- the tyvar won't end up in the accumulator, so
        -- we'd look repeatedly.  Blargh.
 +    do_bndr is tcv _ = extendVarSet is tcv
++
      do_covar is v = Endo do_it
        where
          do_it acc | v `elemVarSet` is  = acc
@@ -452,10 +453,9 @@ deepCoVarFolder = TyCoFolder { tcf_view = noView
                    | otherwise          = appEndo (deep_cv_ty (varType v)) $
                                           acc `extendVarSet` v
 -    do_bndr is tcv _ = extendVarSet is tcv
 -    do_hole is hole  = do_covar is (coHoleCoVar hole)
 -                       -- See Note [CoercionHoles and coercion free variables]
 -                       -- in GHC.Core.TyCo.Rep
 +    do_hole _ _ = mempty
 +      -- See (CHFV1) in Note [CoercionHoles and coercion free variables]
 +      -- in GHC.Core.TyCo.Rep
  ------- Same again, but for DCoVarSet ----------
  --    But this time the free vars are shallow
@@ -661,9 +661,8 @@ tyCoFVsOfCo (FunCo { fco_mult = w, fco_arg = co1, fco_res = co2 }) fv_cand in_sc
    = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2 `unionFV` tyCoFVsOfCo w) fv_cand in_scope acc
  tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc
    = tyCoFVsOfCoVar v fv_cand in_scope acc
 -tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc
 -  = tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc
 -    -- See Note [CoercionHoles and coercion free variables]
 +tyCoFVsOfCo (HoleCo {}) fv_cand in_scope acc = emptyFV fv_cand in_scope acc
 +    -- Ignore holes: see (CHFV1) in 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

@@ -1803,17 +1803,23 @@ Other notes about HoleCo:
  Note [CoercionHoles and coercion free variables]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -Why does a CoercionHole contain a CoVar, as well as reference to
 -fill in?  Because we want to treat that CoVar as a free variable of
 -the coercion.  See #14584, and Note [What prevents a
 -constraint from floating] in GHC.Tc.Solver, item (4):
 +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):
          forall k. [W] co1 :: t1 ~# t2 |> co2
                    [W] co2 :: k ~# *
 -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.
 +   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 RewriterSets]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~