[Git][ghc/ghc][wip/T23109] Wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Fri May 19 16:10:39 UTC 2023
Simon Peyton Jones pushed to branch wip/T23109 at Glasgow Haskell Compiler / GHC
Commits:
76f92e51 by Simon Peyton Jones at 2023-05-19T17:12:19+01:00
Wibbles
- - - - -
5 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Opt/Arity.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Tc/TyCl/Instance.hs
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -45,7 +45,7 @@ module GHC.Core.Coercion (
mkPhantomCo,
mkHoleCo, mkUnivCo, mkSubCo,
mkAxiomInstCo, mkProofIrrelCo,
- downgradeRole, mkAxiomRuleCo,
+ downgradeRole, upgradeRole, mkAxiomRuleCo,
mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
mkKindCo,
castCoercionKind, castCoercionKind1, castCoercionKind2,
@@ -75,7 +75,7 @@ module GHC.Core.Coercion (
coToMCo, mkTransMCo, mkTransMCoL, mkTransMCoR, mkCastTyMCo, mkSymMCo,
mkHomoForAllMCo, mkFunResMCo, mkPiMCos,
- isReflMCo, checkReflexiveMCo,
+ isReflMCo, checkReflexiveMCo, isSubCo_maybe,
-- ** Coercion variables
mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
@@ -1305,6 +1305,10 @@ mkSubCo co@(FunCo { fco_role = Nominal, fco_arg = arg, fco_res = res })
mkSubCo co = assertPpr (coercionRole co == Nominal) (ppr co <+> ppr (coercionRole co)) $
SubCo co
+isSubCo_maybe :: Coercion -> Maybe Coercion
+isSubCo_maybe (SubCo co) = Just co
+isSubCo_maybe co = Nothing
+
-- | Changes a role, but only a downgrade. See Note [Role twiddling functions]
downgradeRole_maybe :: Role -- ^ desired role
-> Role -- ^ current role
@@ -1332,6 +1336,10 @@ downgradeRole r1 r2 co
Just co' -> co'
Nothing -> pprPanic "downgradeRole" (ppr co)
+upgradeRole :: Coercion -> Coercion
+upgradeRole (SubCo co) = co
+upgradeRole co = co
+
mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
mkAxiomRuleCo = AxiomRuleCo
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -2411,8 +2411,11 @@ lintCoercion the_co@(SelCo cs co)
; return (SelCo cs co') }
| otherwise
- -> failWithL (hang (text "Bad SelCo:")
- 2 (ppr the_co $$ ppr s $$ ppr t)) }
+ -> failWithL $ hang (text "Bad SelCo:") 2 $
+ vcat [ text "the_co:" <+> ppr the_co
+ , text "lhs type:" <+> ppr s
+ , text "rhs type:" <+> ppr t
+ , text "role:" <+> ppr co_role ] }
lintCoercion the_co@(LRCo lr co)
= do { co' <- lintCoercion co
=====================================
compiler/GHC/Core/Opt/Arity.hs
=====================================
@@ -52,7 +52,7 @@ import GHC.Core
import GHC.Core.FVs
import GHC.Core.Utils
import GHC.Core.DataCon
-import GHC.Core.TyCon ( tyConArity )
+import GHC.Core.TyCon ( TyCon, tyConArity, isInjectiveTyCon )
import GHC.Core.TyCon.RecWalk ( initRecTc, checkRecTc )
import GHC.Core.Predicate ( isDictTy, isEvVar, isCallStackPredTy )
import GHC.Core.Multiplicity
@@ -2952,39 +2952,17 @@ pushCoDataCon dc dc_args co
-- where S is a type function. In fact, exprIsConApp
-- will probably not be called in such circumstances,
-- but there's nothing wrong with it
-
- = let
- tc_arity = tyConArity to_tc
- dc_univ_tyvars = dataConUnivTyVars dc
- dc_ex_tcvars = dataConExTyCoVars dc
- arg_tys = dataConRepArgTys dc
-
- non_univ_args = dropList dc_univ_tyvars dc_args
- (ex_args, val_args) = splitAtList dc_ex_tcvars non_univ_args
-
- -- Make the "Psi" from the paper
- omegas = decomposeCo tc_arity co (tyConRolesRepresentational to_tc)
- (psi_subst, to_ex_arg_tys)
- = liftCoSubstWithEx Representational
- dc_univ_tyvars
- omegas
- dc_ex_tcvars
- (map exprToType ex_args)
-
- -- Cast the value arguments (which include dictionaries)
- new_val_args = zipWith cast_arg (map scaledThing arg_tys) val_args
- cast_arg arg_ty arg = mkCast arg (psi_subst arg_ty)
-
- to_ex_args = map Type to_ex_arg_tys
-
- dump_doc = vcat [ppr dc, ppr dc_univ_tyvars, ppr dc_ex_tcvars,
- ppr arg_tys, ppr dc_args,
- ppr ex_args, ppr val_args, ppr co, ppr from_ty, ppr to_ty, ppr to_tc
- , ppr $ mkTyConApp to_tc (map exprToType $ takeList dc_univ_tyvars dc_args) ]
- in
- assertPpr (eqType from_ty (mkTyConApp to_tc (map exprToType $ takeList dc_univ_tyvars dc_args))) dump_doc $
- assertPpr (equalLength val_args arg_tys) dump_doc $
- Just (dc, to_tc_arg_tys, to_ex_args ++ new_val_args)
+ = case isSubCo_maybe co of
+ Just co' -> Just (push_data_con to_tc to_tc_arg_tys dc dc_args co')
+ _ | isInjectiveTyCon to_tc Representational
+ -> Just (push_data_con to_tc to_tc_arg_tys dc dc_args co)
+ | otherwise
+ -> pprTrace "Yikes"
+ (vcat [ text "Scrut:" <+> ppr dc <+> ppr dc_args
+ , text "Co:" <+> ppr co
+ , text "of type:" <+> ppr (coercionType co)
+ , text "role:" <+> ppr (coercionRole co) ])
+ Nothing
| otherwise
= Nothing
@@ -2992,6 +2970,45 @@ pushCoDataCon dc dc_args co
where
Pair from_ty to_ty = coercionKind co
+push_data_con :: TyCon -> [Type] -> DataCon -> [CoreExpr] -> Coercion
+ -> (DataCon, [Type], [CoreExpr])
+push_data_con to_tc to_tc_arg_tys dc dc_args co
+ = assertPpr (eqType from_ty dc_app_ty) dump_doc $
+ assertPpr (equalLength val_args arg_tys) dump_doc $
+ assertPpr (isInjectiveTyCon to_tc (coercionRole co)) dump_doc $
+ (dc, to_tc_arg_tys, to_ex_args ++ new_val_args)
+ where
+ Pair from_ty to_ty = coercionKind co
+ tc_arity = tyConArity to_tc
+ dc_univ_tyvars = dataConUnivTyVars dc
+ dc_ex_tcvars = dataConExTyCoVars dc
+ arg_tys = dataConRepArgTys dc
+
+ dc_app_ty = mkTyConApp to_tc (map exprToType $ takeList dc_univ_tyvars dc_args)
+
+ non_univ_args = dropList dc_univ_tyvars dc_args
+ (ex_args, val_args) = splitAtList dc_ex_tcvars non_univ_args
+
+ -- Make the "Psi" from the paper
+ omegas = decomposeCo tc_arity co (tyConRolesRepresentational to_tc)
+ (psi_subst, to_ex_arg_tys)
+ = liftCoSubstWithEx Representational
+ dc_univ_tyvars
+ omegas
+ dc_ex_tcvars
+ (map exprToType ex_args)
+
+ -- Cast the value arguments (which include dictionaries)
+ new_val_args = zipWith cast_arg (map scaledThing arg_tys) val_args
+ cast_arg arg_ty arg = mkCast arg (psi_subst arg_ty)
+
+ to_ex_args = map Type to_ex_arg_tys
+
+ dump_doc = vcat [ppr dc, ppr dc_univ_tyvars, ppr dc_ex_tcvars,
+ ppr arg_tys, ppr dc_args,
+ ppr ex_args, ppr val_args, ppr co, ppr from_ty, ppr to_ty, ppr to_tc
+ , ppr $ mkTyConApp to_tc (map exprToType $ takeList dc_univ_tyvars dc_args) ]
+
collectBindersPushingCo :: CoreExpr -> ([Var], CoreExpr)
-- Collect lambda binders, pushing coercions inside if possible
-- E.g. (\x.e) |> g g :: <Int> -> blah
@@ -3047,7 +3064,33 @@ collectBindersPushingCo e
| otherwise = (reverse bs, mkCast (Lam b e) co)
-{-
+{- Note [pushCoDataCon for newtypes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ newtype N a = MkN (Maybe a)
+and the expression
+ MkN @Int e |> co
+where
+ d :: Maybe Int
+ co :: N Int ~R# N T is a coercion
+
+Then can we use pushCoDataCon to transform this to
+ MkInt @T (e |> Maybe co')
+where
+ (co' : Int ~R# T) = SelCo (SelTc 0 R) co
+
+Well, no. Look at Note [SelCo] in GHC.Core.TyCo.Rep, and especially
+Note [SelCo and newtypes]. We can't use SelCo on a representational
+coercion for a newtype -- it is not injective.
+
+But what if it happens that co = Sub co2 where
+ co2 : N Int ~N# N T
+Well, now we *can* use co2 to give
+ MkInt @T (e |> Maybe (Sub co'))
+where
+ (co' : Int ~N# T) = SelCo (SelTc 0 N) co2
+
+This is a rather common case.
Note [collectBindersPushingCo]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -938,7 +938,7 @@ instance Outputable Coercion where
ppr = pprCo
instance Outputable CoSel where
- ppr (SelTyCon n _r) = text "Tc" <> parens (int n)
+ ppr (SelTyCon n r) = text "Tc" <> parens (int n <> comma <> ppr r)
ppr SelForAll = text "All"
ppr (SelFun fs) = text "Fun" <> parens (ppr fs)
@@ -1045,19 +1045,21 @@ The Coercion form SelCo allows us to decompose a structural coercion, one
between ForallTys, or TyConApps, or FunTys.
There are three forms, split by the CoSel field inside the SelCo:
-SelTyCon, SelForAll, and SelFun.
+SelTyCon, SelForAll, and SelFun. The typing rules below are directly
+checked by the SelCo case of GHC.Core.Lint.lintCoercion.
* SelTyCon:
- co : (T s1..sn) ~r0 (T t1..tn)
- T is a data type, not a newtype, nor an arrow type
- r = tyConRole tc r0 i
+ co : (T s1..sn) ~r (T t1..tn)
+ T is not a saturated FunTyCon (use SelFun for that)
+ T is injective at role r
+ ri = tyConRole tc r i
i < n (i is zero-indexed)
----------------------------------
- SelCo (SelTyCon i r) : si ~r ti
+ SelCo (SelTyCon i ri) : si ~ri ti
- "Not a newtype": see Note [SelCo and newtypes]
- "Not an arrow type": see SelFun below
+ "Injective at role r": see Note [SelCo and newtypes]
+ "Not saturated FunTyCon": see SelFun below
See Note [SelCo Cached Roles]
@@ -1360,6 +1362,10 @@ SelCo, we'll get out a representational coercion. That is:
Yikes! Clearly, this is terrible. The solution is simple: forbid
SelCo to be used on newtypes if the internal coercion is representational.
+More specifically, we use isInjectiveTyCon to determine whether
+T is injective at role r:
+* Newtypes and datatypes are both injective at Nominal role, but
+* Newtypes are not injective at Representational role
See the SelCo equation for GHC.Core.Lint.lintCoercion.
This is not just some corner case discovered by a segfault somewhere;
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -54,9 +54,10 @@ import GHC.Tc.Utils.Unify
import GHC.Builtin.Names ( unsatisfiableIdName )
import GHC.Core ( Expr(..), mkApps, mkVarApps, mkLams )
import GHC.Core.Make ( nO_METHOD_BINDING_ERROR_ID )
-import GHC.Core.Unfold.Make ( mkInlineUnfoldingWithArity, mkDFunUnfolding )
+-- import GHC.Core.Unfold.Make ( mkInlineUnfoldingWithArity, mkDFunUnfolding )
+import GHC.Core.Unfold.Make (mkDFunUnfolding )
import GHC.Core.Type
-import GHC.Core.SimpleOpt
+-- import GHC.Core.SimpleOpt
import GHC.Core.Predicate( classMethodInstTy )
import GHC.Tc.Types.Evidence
import GHC.Core.TyCon
@@ -1314,7 +1315,7 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds })
inst_tv_tys = mkTyVarTys inst_tyvars
arg_wrapper = mkWpEvVarApps dfun_ev_vars <.> mkWpTyApps inst_tv_tys
- is_newtype = isNewTyCon class_tc
+-- is_newtype = isNewTyCon class_tc
dfun_id_w_prags = addDFunPrags dfun_id sc_meth_ids
dfun_spec_prags
-- | is_newtype = SpecPrags []
@@ -1361,8 +1362,8 @@ addDFunPrags dfun_id sc_meth_ids
= dfun_id `setIdUnfolding` mkDFunUnfolding dfun_bndrs dict_con dict_args
`setInlinePragma` dfunInlinePragma
where
- con_app = mkLams dfun_bndrs $
- mkApps (Var (dataConWrapId dict_con)) dict_args
+-- con_app = mkLams dfun_bndrs $
+-- mkApps (Var (dataConWrapId dict_con)) dict_args
-- This application will satisfy the Core invariants
-- from Note [Representation polymorphism invariants] in GHC.Core,
-- because typeclass method types are never unlifted.
@@ -1374,7 +1375,7 @@ addDFunPrags dfun_id sc_meth_ids
dfun_bndrs = dfun_tvs ++ ev_ids
clas_tc = classTyCon clas
dict_con = tyConSingleDataCon clas_tc
- is_newtype = isNewTyCon clas_tc
+-- is_newtype = isNewTyCon clas_tc
wrapId :: HsWrapper -> Id -> HsExpr GhcTc
wrapId wrapper id = mkHsWrap wrapper (HsVar noExtField (noLocA id))
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/76f92e51618db5fb3b09167fbd12957c7743ec2d
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/76f92e51618db5fb3b09167fbd12957c7743ec2d
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/20230519/15b0c8b5/attachment-0001.html>
More information about the ghc-commits
mailing list