[Git][ghc/ghc][wip/T21623] More wibbles
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Sat Sep 17 23:50:54 UTC 2022
Simon Peyton Jones pushed to branch wip/T21623 at Glasgow Haskell Compiler / GHC
Commits:
883cb479 by Simon Peyton Jones at 2022-09-18T00:47:11+01:00
More wibbles
Reaedy for RAE review
- - - - -
12 changed files:
- compiler/GHC/Builtin/Types.hs
- compiler/GHC/Builtin/Types/Prim.hs
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/DataCon.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Make.hs
- compiler/GHC/Core/RoughMap.hs
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Tc/Utils/Instantiate.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Types/Id/Make.hs
Changes:
=====================================
compiler/GHC/Builtin/Types.hs
=====================================
@@ -1901,8 +1901,8 @@ doubleDataCon = pcDataCon doubleDataConName [] [doublePrimTy] doubleTyCon
* *
********************************************************************* -}
-{- Note [Boxing constructors}
-
+{- Note [Boxing constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In ghc-prim:GHC.Types we have a family of data types, one for each RuntimeRep
that "box" unlifted values into a (boxed, lifted) value of kind Type. For example
@@ -1913,6 +1913,9 @@ that "box" unlifted values into a (boxed, lifted) value of kind Type. For exampl
Then we can package an `Int#` into an `IntBox` with `MkIntBox`. We can also
package up a (lifted) Constraint as a value of kind Type.
+There are a fixed number of RuntimeReps, so we only need a fixed number
+of boxing types. (For TupleRep we need to box recursively; not yet done.)
+
This is used:
* In desugaring, when we need to package up a bunch of values into a tuple,
=====================================
compiler/GHC/Builtin/Types/Prim.hs
=====================================
@@ -742,13 +742,19 @@ So for example:
a ~ b :: CONSTRAINT (BoxedRep Lifted)
a ~# b :: CONSTRAINT (TupleRep [])
-Note that:
+Constraints are mostly lifted, but unlifted ones are useful too.
+Specifically (a ~# b) :: CONSTRAINT (TupleRep [])
-* Type and Constraint are considered distinct throughout GHC. But they
- are not /apart/: see Note [Type and Constraint are not apart]
+Wrinkles
-* Constraints are mostly lifted, but unlifted ones are useful too.
- Specifically (a ~# b) :: CONSTRAINT (TupleRep [])
+(W1) Type and Constraint are considered distinct throughout GHC. But they
+ are not /apart/: see Note [Type and Constraint are not apart]
+
+(W2) We need two absent-error Ids, aBSENT_ERROR_ID for types of kind Type, and
+ aBSENT_CONSTRAINT_ERROR_ID for vaues of kind Constraint. Ditto noInlineId
+ vs noInlieConstraintId in GHC.Types.Id.Make; see Note [inlineId magic].
+
+(W3) We need a TypeOrConstraint flag in LitRubbish.
Note [Type and Constraint are not apart]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -782,6 +788,13 @@ irretrievably overlap with:
instance C (Proxy @Constraint a) where ...
+Wrinkles
+
+(W1) In GHC.Core.RoughMap.roughMapTyConName we are careful to map
+ TYPE and CONSTRAINT to the same rough-map key.
+ **ToDo**: explain why
+
+
Note [RuntimeRep polymorphism]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Generally speaking, you can't be polymorphic in `RuntimeRep`. E.g
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -704,7 +704,6 @@ of Coercion, and they perform very basic optimizations.
Note [Role twiddling functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
There are a plethora of functions for twiddling roles:
mkSubCo: Requires a nominal input coercion and always produces a
=====================================
compiler/GHC/Core/DataCon.hs
=====================================
@@ -430,16 +430,16 @@ data DataCon
-- Existentially-quantified type and coercion vars [x,y]
-- For an example involving coercion variables,
- -- Why tycovars? See Note [Existential coercion variables]
+ -- Why TyCoVars? See Note [Existential coercion variables]
dcExTyCoVars :: [TyCoVar],
-- INVARIANT: the UnivTyVars and ExTyCoVars all have distinct OccNames
-- Reason: less confusing, and easier to generate Iface syntax
-- The type/coercion vars in the order the user wrote them [c,y,x,b]
- -- INVARIANT: the set of tyvars in dcUserTyVarBinders is exactly the set
- -- of tyvars (*not* covars) of dcExTyCoVars unioned with the
- -- set of dcUnivTyVars whose tyvars do not appear in dcEqSpec
+ -- INVARIANT(dataConTyVars: the set of tyvars in dcUserTyVarBinders is
+ -- exactly the set of tyvars (*not* covars) of dcExTyCoVars unioned
+ -- with the set of dcUnivTyVars whose tyvars do not appear in dcEqSpec
-- See Note [DataCon user type variable binders]
dcUserTyVarBinders :: [InvisTVBinder],
@@ -672,9 +672,9 @@ the result, and get this type for the "true underlying" worker data con:
(We don't need to make up a fresh tyvar for the second arg; 'd' will do.)
-End of Reasons
+--- End of Reasons ---
-Invariant: the set of tyvars in dcUserTyVarBinders
+INVARIANT(dataConTyVars): the set of tyvars in dcUserTyVarBinders
consists precisely of:
* The set of tyvars in dcUnivTyVars whose type variables do not appear in
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -1599,19 +1599,25 @@ lintBinder site var linterF
lintTyBndr :: TyVar -> (LintedTyCoVar -> LintM a) -> LintM a
lintTyBndr = lintTyCoBndr -- We could specialise it, I guess
--- lintCoBndr :: CoVar -> (LintedTyCoVar -> LintM a) -> LintM a
--- lintCoBndr = lintTyCoBndr -- We could specialise it, I guess
-
lintTyCoBndr :: TyCoVar -> (LintedTyCoVar -> LintM a) -> LintM a
lintTyCoBndr tcv thing_inside
= do { subst <- getSubst
- ; kind' <- lintType (varType tcv)
+ ; tcv_type' <- lintType (varType tcv)
; let tcv' = uniqAway (getSubstInScope subst) $
- setVarType tcv kind'
+ setVarType tcv tcv_type'
subst' = extendTCvSubstWithClone subst tcv tcv'
- ; when (isCoVar tcv) $
- lintL (isCoVarType kind')
- (text "CoVar with non-coercion type:" <+> pprTyVar tcv)
+
+ -- See (FORALL1) and (FORALL2) in GHC.Core.Type
+ ; if (isTyVar tcv)
+ then -- Check that in (forall (a:ki). blah) we have ki:Type
+ lintL (tcIsLiftedTypeKind (typeKind tcv_type')) $
+ hang (text "TyCoVar whose kind does not have kind Type")
+ 2 (ppr tcv' <+> dcolon <+> ppr (typeKind tcv_type'))
+ else -- Check that in (forall (cv::ty). blah),
+ -- then ty looks like (t1 ~# t2)
+ lintL (isCoVarType tcv_type') $
+ text "CoVar with non-coercion type:" <+> pprTyVar tcv
+
; updateSubst subst' (thing_inside tcv') }
lintIdBndrs :: forall a. TopLevelFlag -> [Id] -> ([LintedId] -> LintM a) -> LintM a
@@ -1693,7 +1699,7 @@ lintValueType ty
= addLoc (InType ty) $
do { ty' <- lintType ty
; let sk = typeKind ty'
- ; lintL (classifiesTypeWithValues sk) $
+ ; lintL (isTYPEorCONSTRAINT sk) $
hang (text "Ill-kinded type:" <+> ppr ty)
2 (text "has kind:" <+> ppr sk)
; return ty' }
@@ -1854,7 +1860,7 @@ lintTySynFamApp report_unsat ty tc tys
-- Confirms that a type is really TYPE r or Constraint
checkValueType :: LintedType -> SDoc -> LintM ()
checkValueType ty doc
- = lintL (classifiesTypeWithValues kind)
+ = lintL (isTYPEorCONSTRAINT kind)
(text "Non-Type-like kind when Type-like expected:" <+> ppr kind $$
text "when checking" <+> doc)
where
@@ -1866,8 +1872,8 @@ lintArrow :: SDoc -> LintedType -> LintedType -> LintedType -> LintM ()
-- See Note [GHC Formalism]
lintArrow what t1 t2 tw -- Eg lintArrow "type or kind `blah'" k1 k2 kw
-- or lintArrow "coercion `blah'" k1 k2 kw
- = do { unless (classifiesTypeWithValues k1) (report (text "argument") k1)
- ; unless (classifiesTypeWithValues k2) (report (text "result") k2)
+ = do { unless (isTYPEorCONSTRAINT k1) (report (text "argument") k1)
+ ; unless (isTYPEorCONSTRAINT k2) (report (text "result") k2)
; unless (isMultiplicityTy kw) (report (text "multiplicity") kw) }
where
k1 = typeKind t1
@@ -2206,8 +2212,8 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
k2 = typeKind ty2'
; prov' <- lint_prov k1 k2 prov
- ; when (r /= Phantom && classifiesTypeWithValues k1
- && classifiesTypeWithValues k2)
+ ; when (r /= Phantom && isTYPEorCONSTRAINT k1
+ && isTYPEorCONSTRAINT k2)
(checkTypes ty1 ty2)
; return (UnivCo prov' r ty1' ty2') }
=====================================
compiler/GHC/Core/Make.hs
=====================================
@@ -331,33 +331,7 @@ mkStringExprFSWith ids str
************************************************************************
-}
-{- Note [Big tuples]
-~~~~~~~~~~~~~~~~~~~~
-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
-output of a desugaring stage (notably that for list comprehensions).
-
-We call tuples above this size "big tuples", and emulate them by
-creating and pattern matching on >nested< tuples that are expressible
-by GHC.
-
-Nesting policy: it's better to have a 2-tuple of 10-tuples (3 objects)
-than a 10-tuple of 2-tuples (11 objects), so we want the leaves of any
-construction to be big.
-
-If you just use the 'mkBigCoreTup', 'mkBigCoreVarTupTy', 'mkBigTupleSelector'
-and 'mkBigTupleCase' functions to do all your work with tuples you should be
-fine, and not have to worry about the arity limitation at all.
-
-
-`mkBigCoreVarTup` builds a tuple; the inverse to `mkBigTupleSelector`.
-
-* If it has only one element, it is the identity function.
-
-* If there are more elements than a big tuple can have, it nests
- the tuples. See Note [Big tuples]
-
-Note [Flattening one-tuples]
+{- Note [Flattening one-tuples]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This family of functions creates a tuple of variables/expressions/types.
mkCoreTup [e1,e2,e3] = (e1,e2,e3)
@@ -387,6 +361,7 @@ This arose from discussions in #16881.
One-tuples that arise internally depend on the circumstance; often flattening
is a good idea. Decisions are made on a case-by-case basis.
+'mkCoreTupSolo` and `mkBigCoreVarTupSolo` build tuples without flattening.
-}
-- | Build the type of a small tuple that holds the specified variables
@@ -435,6 +410,39 @@ mkCoreUbxSum arity alt tys exp
++ map Type tys
++ [exp])
+{- Note [Big tuples]
+~~~~~~~~~~~~~~~~~~~~
+"Big" tuples (`mkBigCoreTup` and friends) are more general than "small"
+ones (`mkCoreTup` and friend) 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
+ output of a desugaring stage (notably that for list comprehensions).
+
+ `mkBigCoreTup` encodes such big tuples by creating and pattern
+ matching on /nested/ small tuples that are directly expressible by
+ GHC.
+
+ Nesting policy: it's better to have a 2-tuple of 10-tuples (3 objects)
+ than a 10-tuple of 2-tuples (11 objects), so we want the leaves of any
+ construction to be big.
+
+2. When desugaring arrows we gather up a tuple of free variables, which
+ may include dictionries (of kind Constraint) and unboxed values.
+
+ These can't live in a tuple. `mkBigCoreTup` encodes such tuples by
+ boxing up the offending arguments: see Note [Boxing constructors]
+ in GHC.Builtin.Types.
+
+If you just use the 'mkBigCoreTup', 'mkBigCoreVarTupTy', 'mkBigTupleSelector'
+and 'mkBigTupleCase' functions to do all your work with tuples you should be
+fine, and not have to worry about the arity limitation, or kind limitation at
+all.
+
+The "big" tuple operations flatten 1-tuples just like "small" tuples.
+But see Note [Don't flatten tuples from HsSyn]
+-}
+
mkBigCoreVarTupSolo :: [Id] -> CoreExpr
-- Same as mkBigCoreVarTup, but
-- - one-tuples are not flattened
=====================================
compiler/GHC/Core/RoughMap.hs
=====================================
@@ -286,7 +286,7 @@ roughMatchTyConName tc
= tYPETyConName -- TYPE and CONSTRAINT are not apart, so they must use
-- the same rough-map key. We arbitrarily use TYPE.
-- See Note [Type and Constraint are not apart]
- -- in GHC.Builtin.Types.Prim
+ -- wrinkle (W1) in GHC.Builtin.Types.Prim
| otherwise
= assertPpr (isGenerativeTyCon tc Nominal) (ppr tc) tc_name
where
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -1401,8 +1401,8 @@ All data constructors can be promoted to become a type constructor,
via the PromotedDataCon alternative in GHC.Core.TyCon.
* The TyCon promoted from a DataCon has the *same* Name and Unique as
- the DataCon. Eg. If the data constructor Data.Maybe.Just(unique 78,
- say) is promoted to a TyCon whose name is Data.Maybe.Just(unique 78)
+ the DataCon. Eg. If the data constructor Data.Maybe.Just(unique 78)
+ is promoted to a TyCon whose name is Data.Maybe.Just(unique 78)
* We promote the *user* type of the DataCon. Eg
data T = MkT {-# UNPACK #-} !(Bool, Bool)
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -231,7 +231,7 @@ module GHC.Core.Type (
tidyForAllTyBinder, tidyForAllTyBinders,
-- * Kinds
- classifiesTypeWithValues,
+ isTYPEorCONSTRAINT,
isConcrete, isFixedRuntimeRepKind,
) where
@@ -2519,10 +2519,12 @@ Note [Kinding rules for types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Here are the kinding rules for types
- t1 : TYPE rep1
- t2 : TYPE rep2
+ torc1 is TYPE or CONSTRAINT
+ torc2 is TYPE or CONSTRAINT
+ t1 : torc1 rep1
+ t2 : torc2 rep2
(FUN) ----------------
- t1 -> t2 : Type
+ t1 -> t2 : torc2 LiftedRep
ty : TYPE rep
`a` is not free in rep
@@ -2544,18 +2546,32 @@ Here are the kinding rules for types
(PRED2) ---------------------
t1 => t2 : Constraint
- ty : TYPE rep
+ torc is TYPE or CONSTRAINT
+ ty : body_torc rep
+ ki : Type
+ `a` is a type variable
`a` is not free in rep
(FORALL1) -----------------------
- forall a. ty : TYPE rep
+ forall (a::ki). ty : torc rep
- ty : Constraint
+ torc is TYPE or CONSTRAINT
+ ty : body_torc rep
+ `c` is not free in rep
+ `c` is free in ty -- Surprise 1!
(FORALL2) -------------------------
- forall a. ty : Constraint
+ forall (cv::k1 ~#{N,R} k2). ty : body_torc LiftedRep
+ -- Surprise 2!
Note that:
-* The only way we distinguish '->' from '=>' is by the fact
- that the argument is a PredTy. Both are FunTys
+* (FORALL1) rejects (forall (a::Maybe). blah)
+
+* (FORALL2) Surprise 1:
+ See GHC.Core.TyCo.Rep Note [Unused coercion variable in ForAllTy]
+
+* (FORALL2) Surprise 2: coercion abstractions are not erased, so
+ this must be LiftedRep, just liike (FUN). (FORALL2) is just a
+ dependent form of (FUN).
+
Note [Phantom type variables in kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2578,6 +2594,7 @@ occCheckExpand to expand any type synonyms in the kind of 'ty'
to eliminate 'a'. See kinding rule (FORALL) in
Note [Kinding rules for types]
+
See also
* GHC.Core.Type.occCheckExpand
* GHC.Core.Utils.coreAltsType
@@ -2613,16 +2630,21 @@ typeKind ty@(ForAllTy {})
-- We must make sure tv does not occur in kind
-- As it is already out of scope!
-- See Note [Phantom type variables in kinds]
- Just k' -> k'
Nothing -> pprPanic "typeKind"
(ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind)
+
+ Just k' | all isTyVar tvs -> k' -- Rule (FORALL1)
+ | otherwise -> lifted_kind_from_body -- Rule (FORALL2)
where
(tvs, body) = splitForAllTyVars ty
body_kind = typeKind body
----------------------------------------------
--- Utilities to be used in GHC.Core.Unify,
--- which uses "tc" functions
+ lifted_kind_from_body -- Implements (FORALL2)
+ = case sORTKind_maybe body_kind of
+ Just (ConstraintLike, _) -> constraintKind
+ Just (TypeLike, _) -> liftedTypeKind
+ Nothing -> pprPanic "typeKind" (ppr body_kind)
+
---------------------------------------------
sORTKind_maybe :: Kind -> Maybe (TypeOrConstraint, Type)
@@ -2651,7 +2673,7 @@ typeTypeOrConstraint ty
isPredTy :: HasDebugCallStack => Type -> Bool
-- Precondition: expects a type that classifies values
-- See Note [Types for coercions, predicates, and evidence] in GHC.Core.TyCo.Rep
--- Returns True for types of kind Constraint, False for ones of kind Type
+-- Returns True for types of kind (CONSTRAINT _), False for ones of kind (TYPE _)
isPredTy ty = case typeTypeOrConstraint ty of
TypeLike -> False
ConstraintLike -> True
@@ -2659,9 +2681,9 @@ isPredTy ty = case typeTypeOrConstraint ty of
-----------------------------------------
-- | Does this classify a type allowed to have values? Responds True to things
-- like *, TYPE Lifted, TYPE IntRep, TYPE v, Constraint.
-classifiesTypeWithValues :: Kind -> Bool
+isTYPEorCONSTRAINT :: Kind -> Bool
-- ^ True of a kind `TYPE _` or `CONSTRAINT _`
-classifiesTypeWithValues k = isJust (sORTKind_maybe k)
+isTYPEorCONSTRAINT k = isJust (sORTKind_maybe k)
isConstraintLikeKind :: Kind -> Bool
-- True of (CONSTRAINT _)
@@ -2679,20 +2701,14 @@ isConstraintKind kind
tcIsLiftedTypeKind :: Kind -> Bool
-- ^ Is this kind equivalent to 'Type' i.e. TYPE LiftedRep?
---
--- This considers 'Constraint' to be distinct from 'Type'. For a version that
--- treats them as the same type, see 'isLiftedTypeKind'.
tcIsLiftedTypeKind kind
| Just (TypeLike, rep) <- sORTKind_maybe kind
= isLiftedRuntimeRep rep
| otherwise
= False
--- | Is this kind equivalent to @TYPE (BoxedRep l)@ for some @l :: Levity@?
---
--- This considers 'Constraint' to be distinct from 'Type'. For a version that
--- treats them as the same type, see 'isLiftedTypeKind'.
tcIsBoxedTypeKind :: Kind -> Bool
+-- ^ Is this kind equivalent to @TYPE (BoxedRep l)@ for some @l :: Levity@?
tcIsBoxedTypeKind kind
| Just (TypeLike, rep) <- sORTKind_maybe kind
= isBoxedRuntimeRep rep
@@ -2760,7 +2776,7 @@ argsHaveFixedRuntimeRep ty
-- __Precondition:__ The type has kind `TYPE blah` or `CONSTRAINT blah`
isFixedRuntimeRepKind :: HasDebugCallStack => Kind -> Bool
isFixedRuntimeRepKind k
- = assertPpr (classifiesTypeWithValues k) (ppr k) $
+ = assertPpr (isTYPEorCONSTRAINT k) (ppr k) $
-- the isLiftedTypeKind check is necessary b/c of Constraint
isConcrete k
=====================================
compiler/GHC/Tc/Utils/Instantiate.hs
=====================================
@@ -369,6 +369,7 @@ instStupidTheta orig theta
-- | Given ty::forall k1 k2. k, instantiate all the invisible forall-binders
-- returning ty @kk1 @kk2 :: k[kk1/k1, kk2/k1]
+-- Called only to instantiate kinds, in user-written type signatures
tcInstInvisibleTyBinders :: TcType -> TcKind -> TcM (TcType, TcKind)
tcInstInvisibleTyBinders ty kind
= do { (extra_args, kind') <- tcInstInvisibleTyBindersN n_invis kind
@@ -377,6 +378,7 @@ tcInstInvisibleTyBinders ty kind
n_invis = invisibleTyBndrCount kind
tcInstInvisibleTyBindersN :: Int -> TcKind -> TcM ([TcType], TcKind)
+-- Called only to instantiate kinds, in user-written type signatures
tcInstInvisibleTyBindersN 0 kind
= return ([], kind)
tcInstInvisibleTyBindersN n ty
@@ -394,20 +396,22 @@ tcInstInvisibleTyBindersN n ty
| otherwise
= return ([], substTy subst kind)
--- | Used only in *types*
tcInstInvisibleTyBinder :: Subst -> PiTyVarBinder -> TcM (Subst, TcType)
+-- Called only to instantiate kinds, in user-written type signatures
+
tcInstInvisibleTyBinder subst (Named (Bndr tv _))
= do { (subst', tv') <- newMetaTyVarX subst tv
; return (subst', mkTyVarTy tv') }
tcInstInvisibleTyBinder subst (Anon ty af)
| Just (mk, k1, k2) <- get_eq_tys_maybe (substTy subst (scaledThing ty))
- -- Equality is the *only* constraint currently handled in types.
+ -- For kinds like (k1 ~ k2) => blah, we want to emit a unification
+ -- constraint for (k1 ~# k2) and return the argument (Eq# k1 k2)
-- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
+ -- Equality is the *only* constraint currently handled in types.
= assert (isInvisibleAnonArg af) $
do { co <- unifyKind Nothing k1 k2
- ; arg' <- mk co
- ; return (subst, arg') }
+ ; return (subst, mk co) }
| otherwise -- This should never happen
-- See GHC.Core.TyCo.Rep Note [Constraints in kinds]
@@ -415,8 +419,8 @@ tcInstInvisibleTyBinder subst (Anon ty af)
-------------------------------
get_eq_tys_maybe :: Type
- -> Maybe ( Coercion -> TcM Type
- -- given a coercion proving t1 ~# t2, produce the
+ -> Maybe ( Coercion -> Type
+ -- Given a coercion proving t1 ~# t2, produce the
-- right instantiation for the PiTyVarBinder at hand
, Type -- t1
, Type -- t2
@@ -426,30 +430,27 @@ get_eq_tys_maybe ty
-- Lifted heterogeneous equality (~~)
| Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
, tc `hasKey` heqTyConKey
- = Just (\co -> mkHEqBoxTy co k1 k2, k1, k2)
+ = Just (mkHEqBoxTy k1 k2, k1, k2)
-- Lifted homogeneous equality (~)
| Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
, tc `hasKey` eqTyConKey
- = Just (\co -> mkEqBoxTy co k1 k2, k1, k2)
+ = Just (mkEqBoxTy k1 k2, k1, k2)
| otherwise
= Nothing
-- | This takes @a ~# b@ and returns @a ~~ b at .
-mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
--- monadic just for convenience with mkEqBoxTy
-mkHEqBoxTy co ty1 ty2
- = return $
- mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
+mkHEqBoxTy :: Type -> Type -> TcCoercion -> Type
+mkHEqBoxTy ty1 ty2 co
+ = mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
where k1 = typeKind ty1
k2 = typeKind ty2
-- | This takes @a ~# b@ and returns @a ~ b at .
-mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
-mkEqBoxTy co ty1 ty2
- = return $
- mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
+mkEqBoxTy :: Type -> Type -> TcCoercion -> Type
+mkEqBoxTy ty1 ty2 co
+ = mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
where k = typeKind ty1
{- *********************************************************************
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -128,7 +128,7 @@ module GHC.Tc.Utils.TcType (
--------------------------------
-- Reexported from Kind
Kind, liftedTypeKind, constraintKind,
- isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues,
+ isLiftedTypeKind, isUnliftedTypeKind, isTYPEorCONSTRAINT,
--------------------------------
-- Reexported from Type
=====================================
compiler/GHC/Types/Id/Make.hs
=====================================
@@ -1744,24 +1744,24 @@ But actually we give 'noinline' a wired-in name for three distinct reasons:
noinline (f x y) ==> noinline f x y
This is done in GHC.HsToCore.Utils.mkCoreAppDs.
This is only needed for noinlineId, not noInlineConstraintId (wrinkle
- (a) below), because the latter never shows up in user code.
+ (W1) below), because the latter never shows up in user code.
Wrinkles
-a) Sometimes case (2) above needs to apply `noinline` to a type of kind
- Constraint; e.g.
+(W1) Sometimes case (2) above needs to apply `noinline` to a type of kind
+ Constraint; e.g.
noinline @(Eq Int) $dfEqInt
- We don't have type-or-kind polymorphism, so we simply have two `inline`
- Ids, namely `noinlineId` and `noinlineConstraintId`.
-
-b) Note that noinline as currently implemented can hide some simplifications
- since it hides strictness from the demand analyser. Specifically, the
- demand analyser will treat 'noinline f x' as lazy in 'x', even if the
- demand signature of 'f' specifies that it is strict in its argument. We
- considered fixing this this by adding a special case to the demand
- analyser to address #16588. However, the special case seemed like a large
- and expensive hammer to address a rare case and consequently we rather
- opted to use a more minimal solution.
+ We don't have type-or-kind polymorphism, so we simply have two `inline`
+ Ids, namely `noinlineId` and `noinlineConstraintId`.
+
+(W2) Note that noinline as currently implemented can hide some simplifications
+ since it hides strictness from the demand analyser. Specifically, the
+ demand analyser will treat 'noinline f x' as lazy in 'x', even if the
+ demand signature of 'f' specifies that it is strict in its argument. We
+ considered fixing this this by adding a special case to the demand
+ analyser to address #16588. However, the special case seemed like a large
+ and expensive hammer to address a rare case and consequently we rather
+ opted to use a more minimal solution.
Note [nospecId magic]
~~~~~~~~~~~~~~~~~~~~~
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/883cb4793c9f65f82dec512a28639dacec77dc39
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/883cb4793c9f65f82dec512a28639dacec77dc39
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/20220917/56ff7216/attachment-0001.html>
More information about the ghc-commits
mailing list