GitLab

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

Commits:

e50adf9c
by Simon Peyton Jones at 2025-10-17T08:19:14+01:00
```
Fix buglet in solving equalities from QCIs
```

f4875d90

by Simon Peyton Jones at 2025-10-17T08:19:42+01:00

Free vars of a type

...should include free vars of CoercionHoles

2 changed files:

compiler/GHC/Core/TyCo/FVs.hs
compiler/GHC/Tc/Solver/Equality.hs

Changes:

compiler/GHC/Core/TyCo/FVs.hs

@@ -338,9 +338,15 @@ deepTcvFolder = TyCoFolder { tcf_view = noView  -- See Note [Free vars and synon
                    | otherwise          = appEndo (deep_ty (varType v)) $
                                           acc `extendVarSet` v
 +    do_bndr :: TyCoVarSet -> TyVar -> ForAllTyFlag -> TyCoVarSet
      do_bndr is tcv _ = extendVarSet is tcv
 -    do_hole _ _  = mempty  -- See (CHFV1) in Note [CoercionHoles and coercion free variables]
 -                           -- in GHC.Core.TyCo.Rep
++
 +    do_hole :: VarSet -> CoercionHole -> Endo TyCoVarSet
 +    do_hole _ 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
  {- *********************************************************************
  *                                                                      *

compiler/GHC/Tc/Solver/Equality.hs

@@ -2935,8 +2935,7 @@ lookup_eq_in_qcis :: CtEvidence -> EqRel -> TcType -> TcType -> SolverStage ()
  --    [W] t1 ~# t2
  -- and a Given quantified contraint like (forall a b. blah => a ~ b)
  -- Why?  See Note [Looking up primitive equalities in quantified constraints]
 --- See also GHC.Tc.Solver.Dict
 --- Note [Equality superclasses in quantified constraints]
 +-- See also GHC.Tc.Solver.Dict Note [Equality superclasses in quantified constraints]
  lookup_eq_in_qcis (CtGiven {}) _ _ _
    = nopStage ()
@@ -2952,10 +2951,18 @@ lookup_eq_in_qcis ev@(CtWanted (WantedCt { ctev_dest = dest, ctev_loc = loc }))
    where
      hole = case dest of
               HoleDest hole -> hole   -- Equality constraints have HoleDest
 -             _ -> pprPanic "lookup_eq_in_qcis" (ppr dest)
 +             _ -> pprPanic "lookup_eq_in_qcis" (ppr dest)
      try :: SwapFlag -> SolverStage ()
 -    try swap -- First try looking for (lhs ~ rhs)
 +    -- E.g. We are trying to solve (say)
 +    --             [W] g : [Int] ~# b)
 +    --      from   [G] forall x. blah => b ~ [x]   -- A quantified constraint
 +    -- We can solve it like this
 +    --     d::b~[Int] := $df @Int blah        -- Apply the quantified constraint
 +    --     g'::b~#[Int] := sc_sel d           -- Binding, extract the coercion from d
 +    --     g(co-hole) := sym g'               -- Fill the original coercion hole
 +    -- Here g' is a fresh coercion variable.
 +    try swap
         | Just (cls, tys) <- unSwap swap (boxEqPred eq_rel) lhs rhs
         = Stage $
           do { let cls_pred = mkClassPred cls tys
@@ -2965,7 +2972,7 @@ lookup_eq_in_qcis ev@(CtWanted (WantedCt { ctev_dest = dest, ctev_loc = loc }))
                  OneInst {}
                    -> do { dict_ev <- newWantedEvVarNC loc emptyCoHoleSet cls_pred
                          ; chooseInstance dict_ev res
 -                        ; let co_var = coHoleCoVar hole
 +                        ; co_var <- newEvVar (unSwap swap (mkEqPred eq_rel) lhs rhs)
                          ; setEvBind (mkWantedEvBind co_var EvCanonical (mk_sc_sel cls tys dict_ev))
                          ; fillCoercionHole hole emptyCoHoleSet $
                            maybeSymCo swap (mkCoVarCo co_var)