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) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/058b40f2f7d5c04256e81d4a6fdd5a9... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/058b40f2f7d5c04256e81d4a6fdd5a9... You're receiving this email because of your account on gitlab.haskell.org.