Simon Peyton Jones pushed to branch wip/T25440 at Glasgow Haskell Compiler / GHC Commits: 83430c77 by Simon Peyton Jones at 2025-04-22T10:12:08+01:00 Fix hetero kinded solving - - - - - 1 changed file: - compiler/GHC/Tc/Solver/Equality.hs Changes: ===================================== compiler/GHC/Tc/Solver/Equality.hs ===================================== @@ -1604,7 +1604,7 @@ canEqCanLHSHetero :: CtEvidence -- :: (xi1 :: ki1) ~ (xi2 :: ki2) -> TcType -> TcType -- xi2 -> TcKind -- ki2 -> TcS (StopOrContinue (Either IrredCt EqCt)) -canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 _ps_xi2 ki2 +canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 -- See Note [Equalities with incompatible kinds] -- See Note [Kind Equality Orientation] @@ -1613,60 +1613,63 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 _ps_xi2 ki2 -- NotSwapped: -- ev :: (lhs1:ki1) ~r# (xi2:ki2) -- kind_co :: k11 ~# ki2 -- Same orientation as ev --- type_ev :: lhs1 ~r# (xi2 |> sym kind_co) +-- new_ev :: lhs1 ~r# (xi2 |> sym kind_co) -- Swapped -- ev :: (xi2:ki2) ~r# (lhs1:ki1) -- kind_co :: ki2 ~# ki1 -- Same orientation as ev --- type_ev :: (xi2 |> kind_co) ~r# lhs1 +-- new_ev :: (xi2 |> kind_co) ~r# lhs1 +-- Note that we need the `sym` when we are /not/ swapped; hence `mk_sym_co` - = do { (kind_co, rewriters, unifs_happened) <- mk_kind_eq -- :: ki1 ~N ki2 - ; if unifs_happened - -- Unifications happened, so start again to do the zonking - -- Otherwise we might put something in the inert set that isn't inert - then startAgainWith (mkNonCanonical ev) - else - assertPpr (not (isEmptyRewriterSet rewriters)) (ppr ev) $ - -- The rewriter set won't be empty because the two kinds differ, and there - -- are no unifications, so we must have emitted one or more constraints - do { let lhs_redn = mkReflRedn role ps_xi1 - rhs_redn = mkGReflRightRedn role xi2 mb_sym_kind_co - mb_sym_kind_co = case swapped of - NotSwapped -> mkSymCo kind_co - IsSwapped -> kind_co - - ; traceTcS "Hetero equality gives rise to kind equality" - (ppr swapped $$ - ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ]) - ; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn - - -- The rewritten equality is non-canonical, so put it straight in the Irreds - ; finishCanWithIrred (NonCanonicalReason (cteProblem cteCoercionHole)) type_ev } } - --- ; let new_xi2 = mkCastTy ps_xi2 mb_sym_kind_co --- ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }} - - where - mk_kind_eq :: TcS (CoercionN, RewriterSet, Bool) - -- Returned kind_co has kind (k1 ~ k2) if NotSwapped, (k2 ~ k1) if Swapped - -- Returned Bool = True if unifications happened, so we should retry - mk_kind_eq = case ev of + = case ev of CtGiven (GivenCt { ctev_evar = evar, ctev_loc = loc }) -> do { let kind_co = mkKindCo (mkCoVarCo evar) pred_ty = unSwap swapped mkNomEqPred ki1 ki2 kind_loc = mkKindEqLoc xi1 xi2 loc ; kind_ev <- newGivenEvVar kind_loc (pred_ty, evCoercion kind_co) ; emitWorkNC [CtGiven kind_ev] - ; return (givenCtEvCoercion kind_ev, emptyRewriterSet, False) } + ; let kind_co = givenCtEvCoercion kind_ev + new_xi2 = mkCastTy ps_xi2 (mk_sym_co kind_co) + ; new_ev <- do_rewrite emptyRewriterSet kind_co + -- In the Given case, `new_ev` is canonical, so carry on + ; canEqCanLHSHomo new_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 } CtWanted {} - -> do { (kind_co, cts, unifs) <- wrapUnifierTcS ev Nominal $ \uenv -> - let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2) - in unSwap swapped (uType uenv') ki1 ki2 - ; return (kind_co, rewriterSetFromCts cts, not (null unifs)) } - + -> do { (kind_co, cts, unifs) <- wrapUnifierTcS ev Nominal $ \uenv -> + let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2) + in unSwap swapped (uType uenv') ki1 ki2 + ; if not (null unifs) + then -- Unifications happened, so start again to do the zonking + -- Otherwise we might put something in the inert set that isn't inert + startAgainWith (mkNonCanonical ev) + else + + assertPpr (not (isEmptyCts cts)) (ppr ev $$ ppr ki1 $$ ppr ki2) $ + -- The constraints won't be empty because the two kinds differ, and there + -- are no unifications, so we must have emitted one or more constraints + do { new_ev <- do_rewrite (rewriterSetFromCts cts) kind_co + -- The rewritten equality `new_ev` is non-canonical, + -- so put it straight in the Irreds + ; finishCanWithIrred (NonCanonicalReason (cteProblem cteCoercionHole)) new_ev } } + where xi1 = canEqLHSType lhs1 role = eqRelRole eq_rel + -- Apply mkSymCo when /not/ swapped + mk_sym_co co = case swapped of + NotSwapped -> mkSymCo co + IsSwapped -> co + + do_rewrite rewriters kind_co + = do { traceTcS "Hetero equality gives rise to kind equality" + (ppr swapped $$ + ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ]) + ; rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn } + where + -- kind_co :: ki1 ~N ki2 + lhs_redn = mkReflRedn role ps_xi1 + rhs_redn = mkGReflRightRedn role xi2 (mk_sym_co kind_co) + + canEqCanLHSHomo :: CtEvidence -- lhs ~ rhs -- or, if swapped: rhs ~ lhs -> EqRel -> SwapFlag View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/83430c7783133ae778d237975d4a8314... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/83430c7783133ae778d237975d4a8314... You're receiving this email because of your account on gitlab.haskell.org.