[Git][ghc/ghc][wip/T23070-unify] Distinguish hetero-kind coercion holes from others
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri Apr 28 12:06:41 UTC 2023
Simon Peyton Jones pushed to branch wip/T23070-unify at Glasgow Haskell Compiler / GHC
Commits:
fd03125c by Simon Peyton Jones at 2023-04-28T13:06:59+01:00
Distinguish hetero-kind coercion holes from others
Fixes LopezJuan test. Hooray
- - - - -
8 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Tc/Plugin.hs
- compiler/GHC/Tc/Solver/Equality.hs
- compiler/GHC/Tc/Solver/Monad.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/Unify.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -2739,15 +2739,15 @@ has_co_hole_co :: Coercion -> Monoid.Any
folder = TyCoFolder { tcf_view = noView
, tcf_tyvar = const2 (Monoid.Any False)
, tcf_covar = const2 (Monoid.Any False)
- , tcf_hole = const2 (Monoid.Any True)
+ , tcf_hole = \_ hole -> Monoid.Any (isHeteroKindCoHole hole)
, tcf_tycobinder = const2
}
--- | Is there a coercion hole in this type?
+-- | Is there a hetero-kind coercion hole in this type?
hasCoercionHoleTy :: Type -> Bool
hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty
--- | Is there a coercion hole in this coercion?
+-- | Is there a hetero-kind coercion hole in this coercion?
hasCoercionHoleCo :: Coercion -> Bool
hasCoercionHoleCo = Monoid.getAny . has_co_hole_co
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -38,7 +38,7 @@ module GHC.Core.TyCo.Rep (
-- * Coercions
Coercion(..), CoSel(..), FunSel(..),
UnivCoProvenance(..),
- CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
+ CoercionHole(..), coHoleCoVar, setCoHoleCoVar, isHeteroKindCoHole,
CoercionN, CoercionR, CoercionP, KindCoercion,
MCoercion(..), MCoercionR, MCoercionN,
@@ -1454,12 +1454,19 @@ data CoercionHole
= CoercionHole { ch_co_var :: CoVar
-- See Note [CoercionHoles and coercion free variables]
- , ch_ref :: IORef (Maybe Coercion)
+ , ch_ref :: IORef (Maybe Coercion)
+
+ , ch_hetero_kind :: Bool
+ -- True <=> arises from a kind-level equality
+ -- ToDo: write a Note
}
coHoleCoVar :: CoercionHole -> CoVar
coHoleCoVar = ch_co_var
+isHeteroKindCoHole :: CoercionHole -> Bool
+isHeteroKindCoHole = ch_hetero_kind
+
setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole
setCoHoleCoVar h cv = h { ch_co_var = cv }
@@ -1470,7 +1477,8 @@ instance Data.Data CoercionHole where
dataTypeOf _ = mkNoRepType "CoercionHole"
instance Outputable CoercionHole where
- ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv)
+ ppr (CoercionHole { ch_co_var = cv, ch_hetero_kind = hk })
+ = braces (ppr cv <> ppWhen hk (text "[hk]"))
instance Uniquable CoercionHole where
getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv
=====================================
compiler/GHC/Tc/Plugin.hs
=====================================
@@ -184,7 +184,7 @@ newEvVar = unsafeTcPluginTcM . TcM.newEvVar
-- | Create a fresh coercion hole.
-- This should only be invoked within 'tcPluginSolve'.
newCoercionHole :: PredType -> TcPluginM CoercionHole
-newCoercionHole = unsafeTcPluginTcM . TcM.newCoercionHole
+newCoercionHole = unsafeTcPluginTcM . TcM.newVanillaCoercionHole
-- | Bind an evidence variable.
--
=====================================
compiler/GHC/Tc/Solver/Equality.hs
=====================================
@@ -1753,7 +1753,7 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs
| otherwise
-> tryIrredInstead reason ev eq_rel swapped lhs rhs ;
- PuOK rhs_redn _ ->
+ PuOK _ rhs_redn ->
-- Success: we can solve by unification
do { -- In the common case where rhs_redn is Refl, we don't need to rewrite
@@ -1839,7 +1839,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
-> tryIrredInstead reason ev eq_rel swapped lhs rhs
- PuOK rhs_redn _
+ PuOK _ rhs_redn
-> do { new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
(mkReflRedn (eqRelRole eq_rel) lhs_ty)
rhs_redn
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -1799,7 +1799,7 @@ emitNewWantedEq loc rewriters role ty1 ty2
newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType
-> TcS (CtEvidence, Coercion)
newWantedEq loc rewriters role ty1 ty2
- = do { hole <- wrapTcS $ TcM.newCoercionHole pty
+ = do { hole <- wrapTcS $ TcM.newCoercionHole loc pty
; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty)
; return ( CtWanted { ctev_pred = pty
, ctev_dest = HoleDest hole
@@ -2105,7 +2105,7 @@ checkTouchableTyVarEq
-> TcType -- The RHS
-> TcS (PuResult () Reduction)
-- Used for Nominal, Wanted equalities, with a touchable meta-tyvar on LHS
--- If checkTouchableTyVarEq tv ty = PuOK redn cts
+-- If checkTouchableTyVarEq tv ty = PuOK cts redn
-- then we can unify
-- tv := ty |> redn
-- with extra wanteds 'cts'
@@ -2122,7 +2122,7 @@ checkTouchableTyVarEq ev lhs_tv rhs
; traceTcS "checkTouchableTyVarEq }" (ppr lhs_tv $$ ppr check_result)
; case check_result of
PuFail reason -> return (PuFail reason)
- PuOK redn cts -> do { emitWork cts
+ PuOK cts redn -> do { emitWork cts
; return (pure redn) } }
where
@@ -2171,13 +2171,13 @@ checkTouchableTyVarEq ev lhs_tv rhs
_ -> TcM.newMetaTyVarTyAtLevel lhs_tv_lvl fam_app_kind
; let pty = mkPrimEqPredRole Nominal fam_app new_tv_ty
- ; hole <- TcM.newCoercionHole pty
+ ; hole <- TcM.newVanillaCoercionHole pty
; let new_ev = CtWanted { ctev_pred = pty
, ctev_dest = HoleDest hole
, ctev_loc = cb_loc
, ctev_rewriters = ctEvRewriters ev }
- ; return (PuOK (mkReduction (HoleCo hole) new_tv_ty)
- (singleCt (mkNonCanonical new_ev))) } }
+ ; return (PuOK (singleCt (mkNonCanonical new_ev))
+ (mkReduction (HoleCo hole) new_tv_ty)) } }
-- See Detail (7) of the Note
cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
@@ -2195,7 +2195,7 @@ checkTypeEq ev eq_rel lhs rhs
; traceTcS "checkTypeEq }" (ppr check_result)
; case check_result of
PuFail reason -> return (PuFail reason)
- PuOK redn prs -> do { new_givens <- mapBagM mk_new_given prs
+ PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs
; emitWork new_givens
; updInertTcS (addCycleBreakerBindings prs)
; return (pure redn) } }
@@ -2204,7 +2204,7 @@ checkTypeEq ev eq_rel lhs rhs
= do { check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs)
; case check_result of
PuFail reason -> return (PuFail reason)
- PuOK redn cts -> do { emitWork cts
+ PuOK cts redn -> do { emitWork cts
; return (pure redn) } }
where
check_given_rhs :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
@@ -2241,8 +2241,8 @@ checkTypeEq ev eq_rel lhs rhs
break_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction)
break_given fam_app
= do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app)
- ; return (PuOK (mkReflRedn Nominal (mkTyVarTy new_tv))
- (unitBag (new_tv, fam_app))) }
+ ; return (PuOK (unitBag (new_tv, fam_app))
+ (mkReflRedn Nominal (mkTyVarTy new_tv))) }
-- Why reflexive? See Detail (4) of the Note
---------------------------
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -2414,9 +2414,10 @@ data CtLoc
mkKindLoc :: TcType -> TcType -- original *types* being compared
-> CtLoc -> CtLoc
-mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc)
- (KindEqOrigin s1 s2 (ctLocOrigin loc)
- (ctLocTypeOrKind_maybe loc))
+mkKindLoc s1 s2 ctloc
+ | CtLoc { ctl_t_or_k = t_or_k, ctl_origin = origin } <- ctloc
+ = ctloc { ctl_origin = KindEqOrigin s1 s2 origin t_or_k
+ , ctl_t_or_k = Just KindLevel }
adjustCtLocTyConBinder :: TyConBinder -> CtLoc -> CtLoc
-- Adjust the CtLoc when decomposing a type constructor
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -44,7 +44,8 @@ module GHC.Tc.Utils.TcMType (
newTcEvBinds, newNoTcEvBinds, addTcEvBind,
emitNewExprHole,
- newCoercionHole, fillCoercionHole, isFilledCoercionHole,
+ newCoercionHole, newCoercionHoleO, newVanillaCoercionHole,
+ fillCoercionHole, isFilledCoercionHole,
unpackCoercionHole, unpackCoercionHole_maybe,
checkCoercionHole,
@@ -199,7 +200,7 @@ newEvVar ty = do { name <- newSysName (predTypeOccName ty)
newWantedWithLoc :: CtLoc -> PredType -> TcM CtEvidence
newWantedWithLoc loc pty
= do dst <- case classifyPredType pty of
- EqPred {} -> HoleDest <$> newCoercionHole pty
+ EqPred {} -> HoleDest <$> newCoercionHole loc pty
_ -> EvVarDest <$> newEvVar pty
return $ CtWanted { ctev_dest = dst
, ctev_pred = pty
@@ -224,9 +225,9 @@ newWanteds orig = mapM (newWanted orig Nothing)
----------------------------------------------
cloneWantedCtEv :: CtEvidence -> TcM CtEvidence
-cloneWantedCtEv ctev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ })
+cloneWantedCtEv ctev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _, ctev_loc = loc })
| isEqPrimPred pty
- = do { co_hole <- newCoercionHole pty
+ = do { co_hole <- newCoercionHole loc pty
; return (ctev { ctev_dest = HoleDest co_hole }) }
| otherwise
= pprPanic "cloneWantedCtEv" (ppr pty)
@@ -274,8 +275,8 @@ emitWantedEqs origin pairs
-- | Emits a new equality constraint
emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion
emitWantedEq origin t_or_k role ty1 ty2
- = do { hole <- newCoercionHole pty
- ; loc <- getCtLocM origin (Just t_or_k)
+ = do { hole <- newCoercionHoleO origin pty
+ ; loc <- getCtLocM origin (Just t_or_k)
; emitSimple $ mkNonCanonical $
CtWanted { ctev_pred = pty
, ctev_dest = HoleDest hole
@@ -354,12 +355,23 @@ newImplication
************************************************************************
-}
-newCoercionHole :: TcPredType -> TcM CoercionHole
-newCoercionHole pred_ty
+newVanillaCoercionHole :: TcPredType -> TcM CoercionHole
+newVanillaCoercionHole = new_coercion_hole False
+
+newCoercionHole :: CtLoc -> TcPredType -> TcM CoercionHole
+newCoercionHole loc = newCoercionHoleO (ctLocOrigin loc)
+
+newCoercionHoleO :: CtOrigin -> TcPredType -> TcM CoercionHole
+newCoercionHoleO (KindEqOrigin {}) = new_coercion_hole True
+newCoercionHoleO _ = new_coercion_hole False
+
+new_coercion_hole :: Bool -> TcPredType -> TcM CoercionHole
+new_coercion_hole hetero_kind pred_ty
= do { co_var <- newEvVar pred_ty
; traceTc "New coercion hole:" (ppr co_var <+> dcolon <+> ppr pred_ty)
; ref <- newMutVar Nothing
- ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } }
+ ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref
+ , ch_hetero_kind = hetero_kind } }
-- | Put a value in a coercion hole
fillCoercionHole :: CoercionHole -> Coercion -> TcM ()
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -1802,11 +1802,7 @@ mkKindEnv :: UnifyEnv -> TcType -> TcType -> UnifyEnv
-- Modify the UnifyEnv to be right for unifing
-- the kinds of these two types
mkKindEnv env@(UE { u_loc = ctloc }) ty1 ty2
- | CtLoc { ctl_t_or_k = t_or_k, ctl_origin = origin } <- ctloc
- , let kind_origin = KindEqOrigin ty1 ty2 origin t_or_k
- = env { u_role = Nominal
- , u_loc = ctloc { ctl_origin = kind_origin
- , ctl_t_or_k = Just KindLevel } }
+ = env { u_role = Nominal, u_loc = mkKindLoc ty1 ty2 ctloc }
uType, uType_defer
:: UnifyEnv
@@ -1820,7 +1816,7 @@ uType_defer (UE { u_loc = loc, u_defer = ref
, u_role = role, u_rewriters = rewriters })
ty1 ty2 -- ty1 is "actual", ty2 is "expected"
= do { let pred_ty = mkPrimEqPredRole role ty1 ty2
- ; hole <- newCoercionHole pred_ty
+ ; hole <- newCoercionHole loc pred_ty
; let ct = mkNonCanonical $
CtWanted { ctev_pred = pred_ty
, ctev_dest = HoleDest hole
@@ -2631,7 +2627,7 @@ uTypeCheckTouchableTyVarEq lhs_tv rhs
; traceTc "uTypeCheckTouchableTyVarEq }" (ppr check_result)
; case check_result of
PuFail reason -> return (PuFail reason)
- PuOK redn _ -> assertPpr (isReflCo (reductionCoercion redn))
+ PuOK _ redn -> assertPpr (isReflCo (reductionCoercion redn))
(ppr lhs_tv $$ ppr rhs $$ ppr redn) $
return (pure (reductionReducedType redn)) }
where
@@ -2779,22 +2775,22 @@ reductionCoercion is Refl. See `canEqCanLHSFinish_no_unification`.
-}
data PuResult a b = PuFail CheckTyEqResult
- | PuOK b (Bag a)
+ | PuOK (Bag a) b
instance Functor (PuResult a) where
fmap _ (PuFail prob) = PuFail prob
- fmap f (PuOK x cts) = PuOK (f x) cts
+ fmap f (PuOK cts x) = PuOK cts (f x)
instance Applicative (PuResult a) where
- pure x = PuOK x emptyBag
+ pure x = PuOK emptyBag x
PuFail p1 <*> PuFail p2 = PuFail (p1 S.<> p2)
PuFail p1 <*> PuOK {} = PuFail p1
PuOK {} <*> PuFail p2 = PuFail p2
- PuOK f c1 <*> PuOK x c2 = PuOK (f x) (c1 `unionBags` c2)
+ PuOK c1 f <*> PuOK c2 x = PuOK (c1 `unionBags` c2) (f x)
instance (Outputable a, Outputable b) => Outputable (PuResult a b) where
ppr (PuFail prob) = text "PuFail" <+> (ppr prob)
- ppr (PuOK x cts) = text "PuOK" <> braces
+ ppr (PuOK cts x) = text "PuOK" <> braces
(vcat [ text "redn:" <+> ppr x
, text "cts:" <+> ppr cts ])
@@ -2804,7 +2800,7 @@ pprPur (PuFail prob) = text "PuFail:" <> ppr prob
pprPur (PuOK {}) = text "PuOK"
okCheckRefl :: TcType -> TcM (PuResult a Reduction)
-okCheckRefl ty = return (PuOK (mkReflRedn Nominal ty) emptyBag)
+okCheckRefl ty = return (PuOK emptyBag (mkReflRedn Nominal ty))
failCheckWith :: CheckTyEqResult -> TcM (PuResult a b)
failCheckWith p = return (PuFail p)
@@ -2940,7 +2936,7 @@ checkTyEqRhs flags ty
checkCo :: TyEqFlags a -> Coercion -> TcM (PuResult a Coercion)
-- See Note [checkCo]
checkCo (TEF { tef_lhs = TyFamLHS {} }) co
- = return (PuOK co emptyBag)
+ = return (pure co)
checkCo (TEF { tef_lhs = TyVarLHS lhs_tv
, tef_unifying = unifying
@@ -2963,7 +2959,7 @@ checkCo (TEF { tef_lhs = TyVarLHS lhs_tv
= failCheckWith (cteProblem occ_prob)
| otherwise
- = return (PuOK co emptyBag)
+ = return (pure co)
{- Note [checkCo]
~~~~~~~~~~~~~~~~~
@@ -3147,7 +3143,7 @@ checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob
TEFA_Break breaker -- Recurse; and break if there is a problem
-> do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys
; case tys_res of
- PuOK redns cts -> return (PuOK (mkTyConAppRedn Nominal tc redns) cts)
+ PuOK cts redns -> return (PuOK cts (mkTyConAppRedn Nominal tc redns))
PuFail {} -> breaker fam_app }
where
arg_flags = famAppArgFlags flags
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/fd03125c10e2a7d938da69a7d509958db2dbbb2f
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/fd03125c10e2a7d938da69a7d509958db2dbbb2f
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230428/89b10e38/attachment-0001.html>
More information about the ghc-commits
mailing list