[Git][ghc/ghc][wip/T21623] Improvements to comments, etc., from Richard
Richard Eisenberg (@rae)
gitlab at gitlab.haskell.org
Fri Sep 30 00:01:23 UTC 2022
Richard Eisenberg pushed to branch wip/T21623 at Glasgow Haskell Compiler / GHC
Commits:
6b10aad6 by Richard Eisenberg at 2022-09-29T19:47:07-04:00
Improvements to comments, etc., from Richard
- - - - -
8 changed files:
- compiler/GHC/Builtin/Types.hs
- compiler/GHC/Builtin/Types/Prim.hs
- compiler/GHC/Builtin/Uniques.hs
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Make.hs
- compiler/GHC/Core/Opt/Arity.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/Unify.hs
Changes:
=====================================
compiler/GHC/Builtin/Types.hs
=====================================
@@ -1437,7 +1437,7 @@ GHC.Core.TyCo.Rep.mkFunTy has assertions about the consistency of the argument
flag and arg/res types. But when constructing the kinds of tYPETyCon and
cONSTRAINTTyCon we don't want to make these checks because
TYPE :: RuntimeRep -> Type
-i.e. TYPE :: RuntimeRep- > TYPE LiftedRep
+i.e. TYPE :: RuntimeRep -> TYPE LiftedRep
so the check will loop infinitely. Hence the use of a naked FunTy
constructor in tTYPETyCon and cONSTRAINTTyCon.
@@ -1941,7 +1941,7 @@ type BoxingInfo b = (DataCon, Expr b, Type)
-- (K, K ty, boxed type)
-- e.g. (I#, I#, Int)
-- recall: data Int = I# Int#
- -- or (MkInt8Box, MkInt8Box @ty, Int8Box @ty)
+ -- or (MkInt8Box, MkInt8Box @ty, Int8Box ty)
-- recall: data Int8Box (a :: TYPE Int8Rep) = MkIntBox a
boxingDataCon_maybe :: HasDebugCallStack => Type -> Maybe (BoxingInfo b)
@@ -2003,7 +2003,7 @@ boxingDataConMap = foldl add emptyTypeMap boxingDataCons
add bdcm (kind, boxing_con) = extendTypeMap bdcm kind boxing_con
boxingDataCons :: [(Kind, DataCon)]
--- The TyCon is the RuntimeRep for which the DataCon is the right boxing
+-- The Kind is the kind of types for which the DataCon is the right boxing
boxingDataCons = zipWith mkBoxingDataCon
(map mkBoxingTyConUnique [1..])
[ (mkTYPEapp wordRepDataConTy, fsLit "WordBox", fsLit "MkWordBox")
=====================================
compiler/GHC/Builtin/Types/Prim.hs
=====================================
@@ -777,6 +777,12 @@ precisely, that TYPE and CONSTRAINT are not apart. This
non-apart-ness check is implemented in GHC.Core.Unify.unify_ty: look
for `maybeApart MARTypeVsConstraint`.
+We further extend this treatment to the different arrow types (see
+Note [Function type constructors and FunTy]): if we have
+FunCo (axC Int) <Int> :: (C Int => Int) ~ ((Int -> Int) -> Int), then
+we could extract an equality between (=>) and (->). We thus must ensure
+that (=>) and (->) (among the other arrow combinations) are not Apart.
+
Note that, as before, nothing prevents writing instances like:
instance C (Proxy @Type a) where ...
=====================================
compiler/GHC/Builtin/Uniques.hs
=====================================
@@ -300,7 +300,7 @@ Allocation of unique supply characters:
other a-z: lower case chars for unique supplies. Used so far:
a TypeChecking?
- b RuntimeRep
+ b Boxing tycons & datacons
c StgToCmm/Renamer
d desugarer
f AbsC flattener
@@ -314,6 +314,25 @@ Allocation of unique supply characters:
u Cmm pipeline
y GHCi bytecode generator
z anonymous sums
+
+All wired in tycons actually use *two* uniques:
+ * u: the TyCon itself
+ * u+1: the TyConRepName of the TyCon (for use with TypeRep)
+ The "+1" is implemented in tyConRepNameUnique.
+If this ever changes, make sure to also change the treatment for boxing tycons.
+
+All wired in datacons use *three* uniques:
+ * u: the DataCon itself
+ * u+1: its worker Id
+ * u+2: the TyConRepName of the promoted TyCon
+No wired-in datacons have wrappers.
+The "+1" is implemented in dataConWorkerUnique and the "+2" is in dataConTyRepNameUnique.
+If this ever changes, make sure to also change the treatment for boxing tycons.
+
+Because boxing tycons (see Note [Boxing constructors] in GHC.Builtin.Types)
+come with both a tycon and a datacon, each one takes up five slots, combining
+the two cases above. Getting from the tycon to the datacon (by adding 2)
+is implemented in boxingDataConUnique.
-}
mkAlphaTyVarUnique :: Int -> Unique
@@ -357,8 +376,7 @@ initExitJoinUnique = mkUnique 's' 0
--------------------------------------------------
-- Wired-in type constructor keys occupy *two* slots:
--- * u: the TyCon itself
--- * u+1: the TyConRepName of the TyCon
+-- See Note [Uniques for wired-in prelude things and known masks]
mkPreludeTyConUnique :: Int -> Unique
mkPreludeTyConUnique i = mkUnique '3' (2*i)
@@ -368,10 +386,7 @@ tyConRepNameUnique u = incrUnique u
--------------------------------------------------
-- Wired-in data constructor keys occupy *three* slots:
--- * u: the DataCon itself
--- * u+1: its worker Id
--- * u+2: the TyConRepName of the promoted TyCon
--- Prelude data constructors are too simple to need wrappers.
+-- See Note [Uniques for wired-in prelude things and known masks]
mkPreludeDataConUnique :: Int -> Unique
mkPreludeDataConUnique i = mkUnique '6' (3*i) -- Must be alphabetic
@@ -381,7 +396,9 @@ dataConWorkerUnique u = incrUnique u
dataConTyRepNameUnique u = stepUnique u 2
--------------------------------------------------
--- The data constructors of RuntimeRep occupy *six* slots:
+-- The data constructors of RuntimeRep occupy *five* slots:
+-- See Note [Uniques for wired-in prelude things and known masks]
+--
-- Example: WordRep
--
-- * u: the TyCon of the boxing data type WordBox
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -387,28 +387,8 @@ isReflMCo _ = False
Destructing coercions
%* *
%************************************************************************
-
-Note [Function coercions]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-** ToDo: needs updating **
-
-Remember that
- (->) :: forall {r1} {r2}. Multiplicity -> TYPE r1 -> TYPE r2 -> Type
- (=>) :: forall {r1} {r2}. CONSTRAINT r1 -> TYPE r2 -> Type
- (==>) :: forall {r1} {r2}. CONSTRAINT r1 -> CONSTRAINT r2 -> Consraint
-whose `RuntimeRep' arguments are intentionally marked inferred to
-avoid type application.
-
-Hence
- FunCo r VisArg mult co1 co2 :: (s1->t1) ~r (s2->t2)
-is short for
- TyConAppCo (->) mult co_rep1 co_rep2 co1 co2
-where co_rep1, co_rep2 are the coercions on the representations.
-
-and similarly for (=>) and (==>).
-}
-
-- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
-- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F at . Hence:
--
@@ -425,9 +405,9 @@ decomposeCo arity co rs
decomposeFunCo :: HasDebugCallStack
=> Coercion -- Input coercion
-> (CoercionN, Coercion, Coercion)
--- Expects co :: (s1 -> t1) ~ (s2 -> t2)
--- Returns (co1 :: s1~s2, co2 :: t1~t2)
--- See Note [Function coercions] for the "3" and "4"
+-- Expects co :: (s1 %m1-> t1) ~ (s2 %m2-> t2)
+-- Returns (cow :: m1 ~N m2, co1 :: s1~s2, co2 :: t1~t2)
+-- actually cow will be a Phantom coercion if the input is a Phantom coercion
decomposeFunCo (FunCo _ w co1 co2) = (w, co1, co2)
-- Short-circuits the calls to mkSelCo
@@ -770,11 +750,7 @@ mkNomReflCo = Refl
mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo r tc cos
| Just (_af, w, co1, co2) <- tyConAppFun_maybe (mkReflCo r) tc cos
- -- See Note [Function coercions]
- = -- (a :: TYPE ra) -> (b :: TYPE rb) ~ (c :: TYPE rc) -> (d :: TYPE rd)
- -- rep1 :: ra ~ rc rep2 :: rb ~ rd
- -- co1 :: a ~ c co2 :: b ~ d
- mkFunCo r w co1 co2
+ = mkFunCo r w co1 co2
-- Expand type synonyms
| ExpandsSyn tv_co_prs rhs_ty leftover_cos <- expandSynTyCon_maybe tc cos
@@ -1137,15 +1113,6 @@ getNthFun :: FunSel
-> a -- ^ argument
-> a -- ^ result
-> a -- ^ One of the above three
--- See Note [Function coercions]
--- If FunCo _ mult arg_co res_co :: (s1:TYPE sk1 :mult-> s2:TYPE sk2)
--- ~ (t1:TYPE tk1 :mult-> t2:TYPE tk2)
--- Then we want to behave as if co was
--- TyConAppCo mult argk_co resk_co arg_co res_co
--- where
--- argk_co :: sk1 ~ tk1 = mkSelCo 0 (mkKindCo arg_co)
--- resk_co :: sk2 ~ tk2 = mkSelCo 0 (mkKindCo res_co)
--- i.e. mkRuntimeRepCo
getNthFun SelMult mult _ _ = mult
getNthFun SelArg _ arg _ = arg
getNthFun SelRes _ _ res = res
@@ -1158,7 +1125,7 @@ mkLRCo lr co
= LRCo lr co
-- | Instantiates a 'Coercion'.
-mkInstCo :: Coercion -> Coercion -> Coercion
+mkInstCo :: Coercion -> CoercionN -> Coercion
mkInstCo (ForAllCo tcv _kind_co body_co) co
| Just (arg, _) <- isReflCo_maybe co
-- works for both tyvar and covar
@@ -1174,7 +1141,7 @@ mkGReflRightCo r ty co
-- instead of @isReflCo@
| otherwise = GRefl r ty (MCo co)
--- | Given @ty :: k1@, @co :: k1 ~ k2@,
+-- | Given @r@, @ty :: k1@, and @co :: k1 ~N k2@,
-- produces @co' :: (ty |> co) ~r ty@
mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion
mkGReflLeftCo r ty co
=====================================
compiler/GHC/Core/Make.hs
=====================================
@@ -417,7 +417,7 @@ mkCoreUbxSum arity alt tys exp
{- Note [Big tuples]
~~~~~~~~~~~~~~~~~~~~
"Big" tuples (`mkBigCoreTup` and friends) are more general than "small"
-ones (`mkCoreTup` and friend) in two ways.
+ones (`mkCoreTup` and friends) in two ways.
1. GHCs built-in tuples can only go up to 'mAX_TUPLE_SIZE' in arity, but
we might conceivably want to build such a massive tuple as part of the
@@ -501,8 +501,8 @@ wrapBox e
e_ty = exprType e
boxTy :: Type -> Type
--- ^ If (e :: ty) and (ty :: Type), wrapBox is a no-op
--- But if (ty :: ki), and ki is not Type, wrapBox returns the type
+-- ^ If (e :: ty) and (ty :: Type), boxTy is a no-op
+-- But if (ty :: ki), and ki is not Type, boxTy returns the type
-- of (K @ty e), where K is the boxing data constructor for ki
-- See Note [Boxing constructors] in GHC.Builtin.Types
boxTy ty
@@ -610,7 +610,7 @@ mkBigTupleSelectorSolo vars the_var scrut_var scrut
= mkBigTupleSelector vars the_var scrut_var scrut
-- | `mkSmallTupleSelector` is like 'mkBigTupleSelector', but for tuples that
--- are guaranteed never to be "big". Also does not unwrap Dict types.
+-- are guaranteed never to be "big". Also does not unwrap boxed types.
--
-- > mkSmallTupleSelector [x] x v e = [| e |]
-- > mkSmallTupleSelector [x,y,z] x v e = [| case e of v { (x,y,z) -> x } |]
=====================================
compiler/GHC/Core/Opt/Arity.hs
=====================================
@@ -2826,19 +2826,19 @@ pushCoTyArg co ty
= Nothing
where
Pair tyL tyR = coercionKind co
- -- co :: tyL ~ tyR
+ -- co :: tyL ~R tyR
-- tyL = forall (a1 :: k1). ty1
-- tyR = forall (a2 :: k2). ty2
co1 = mkSymCo (mkSelCo SelForAll co)
-- co1 :: k2 ~N k1
- -- Note that SelCo can extract a Nominal equality between the
+ -- Note that SelCo extracts a Nominal equality between the
-- kinds of the types related by a coercion between forall-types.
-- See the SelCo case in GHC.Core.Lint.
co2 = mkInstCo co (mkGReflLeftCo Nominal ty co1)
- -- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ]
- -- Arg of mkInstCo is always nominal, hence mkNomReflCo
+ -- co2 :: ty1[ (ty|>co1)/a1 ] ~R ty2[ ty/a2 ]
+ -- Arg of mkInstCo is always nominal, hence Nominal
-- | If @pushCoValArg co = Just (co_arg, co_res)@, then
--
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -965,7 +965,9 @@ data Coercion
-- ForAllCo :: _ -> N -> e -> e
| FunCo Role CoercionN Coercion Coercion -- See Note [FunCo]
- -- FunCo :: "e" -> N -> e -> e -> e
+ -- FunCo :: "e" -> N/P -> e -> e -> e
+ -- (if the role "e" is Phantom, the first coercion is, too)
+ -- the first coercion is for the multiplicity
-- These are special
| CoVarCo CoVar -- :: _ -> (N or R)
@@ -1193,17 +1195,13 @@ SelTyCon, SelForAll, and SelFun.
Note [FunCo]
~~~~~~~~~~~~
You might think that a FunCo (which connects two function types) should
-contain the FunTyFlag from the function types. But we are allowed to
-have an axiom (and hence a coercion) connecting Type and Constraint, thus
- co :: (t::Type) ~ (c::Constraint)
-c.f. GHC.Builtin.Types.Prim Note [Type and Constraint are not apart]
-Given such a coercion we can use FunCo to make
- FunCo co <Int> :: (t -> Int) ~ (c => Int)
-Note that the two arrows are different: those FunTys have different
-FunTyFlags! That's why:
-
-* FunCo does not store an FunTyFlag
-* We use mkFuntionType in the FunCo case of coercionLKind/coercoinRKind,
+contain the FunTyFlag from the function types. We don't need to store
+this, though: it's completely recoverable from the kinds of the arguments.
+We thus use mkFunctionType in the FunCo case of coercionLKind/coercionRKind,
+which sets the FunTyFlag correctly.
+
+If you are worried about coercions connecting, say, (=>) and (->), see
+Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim.
Note [Coercion axioms applied to coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -541,7 +541,7 @@ data MaybeApartReason
| MARInfinite -- ^ matching e.g. a ~? Maybe a
- | MARTypeVsConstraint -- ^ matching Type ~? Constraint
+ | MARTypeVsConstraint -- ^ matching Type ~? Constraint or the arrow types
-- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
instance Outputable MaybeApartReason where
@@ -1127,6 +1127,13 @@ unify_ty env ty1 ty2 _kco
, Just {} <- sORTKind_maybe ty2
= maybeApart MARTypeVsConstraint
+ -- The arrow types are not Apart
+ -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
+ -- NB: at this point we know that the two TyCons do not match
+ | FunTy {} <- ty1
+ , FunTy {} <- ty2
+ = maybeApart MARTypeVsConstraint
+
where
mb_tc_app1 = splitTyConApp_maybe ty1
mb_tc_app2 = splitTyConApp_maybe ty2
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6b10aad63a0d3506d195e4235a84d2f069b717e4
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/6b10aad63a0d3506d195e4235a84d2f069b717e4
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/20220929/b1d15e67/attachment-0001.html>
More information about the ghc-commits
mailing list