Commit 81740ce8 authored by sheaf's avatar sheaf Committed by Marge Bot
Browse files

Introduce Concrete# for representation polymorphism checks

PHASE 1: we never rewrite Concrete# evidence.

This patch migrates all the representation polymorphism checks to
the typechecker, using a new constraint form

  Concrete# :: forall k. k -> TupleRep '[]

Whenever a type `ty` must be representation-polymorphic
(e.g. it is the type of an argument to a function), we emit a new
`Concrete# ty` Wanted constraint. If this constraint goes
unsolved, we report a representation-polymorphism error to the user.
The 'FRROrigin' datatype keeps track of the context of the
representation-polymorphism check, for more informative error messages.

This paves the way for further improvements, such as
allowing type families in RuntimeReps and improving the soundness
of typed Template Haskell. This is left as future work (PHASE 2).

fixes #17907 #20277 #20330 #20423 #20426

updates haddock submodule

-------------------------
Metric Decrease:
    T5642
-------------------------
parent 65bf3992
......@@ -1860,7 +1860,8 @@ statePrimTyConKey, stableNamePrimTyConKey, stableNameTyConKey,
typeConKey, threadIdPrimTyConKey, bcoPrimTyConKey, ptrTyConKey,
funPtrTyConKey, tVarPrimTyConKey, eqPrimTyConKey,
eqReprPrimTyConKey, eqPhantPrimTyConKey,
compactPrimTyConKey, stackSnapshotPrimTyConKey :: Unique
compactPrimTyConKey, stackSnapshotPrimTyConKey,
concretePrimTyConKey :: Unique
statePrimTyConKey = mkPreludeTyConUnique 50
stableNamePrimTyConKey = mkPreludeTyConUnique 51
stableNameTyConKey = mkPreludeTyConUnique 52
......@@ -1889,6 +1890,7 @@ funPtrTyConKey = mkPreludeTyConUnique 78
tVarPrimTyConKey = mkPreludeTyConUnique 79
compactPrimTyConKey = mkPreludeTyConUnique 80
stackSnapshotPrimTyConKey = mkPreludeTyConUnique 81
concretePrimTyConKey = mkPreludeTyConUnique 82
eitherTyConKey :: Unique
eitherTyConKey = mkPreludeTyConUnique 84
......@@ -2228,7 +2230,6 @@ integerIPDataConKey = mkPreludeDataConUnique 122
naturalNSDataConKey = mkPreludeDataConUnique 123
naturalNBDataConKey = mkPreludeDataConUnique 124
---------------- Template Haskell -------------------
-- GHC.Builtin.Names.TH: USES DataUniques 200-250
-----------------------------------------------------
......
......@@ -692,7 +692,7 @@ significantly simpler since otherwise we would need to define a calling
convention for curried applications that can accommodate representation
polymorphism.
To ensure saturation, CorePrep eta expands expand all primop applications as
To ensure saturation, CorePrep eta expands all primop applications as
described in Note [Eta expansion of hasNoBinding things in CorePrep] in
GHC.Core.Prep.
......
......@@ -102,6 +102,8 @@ module GHC.Builtin.Types.Prim(
eqPhantPrimTyCon, -- ty1 ~P# ty2 (at role Phantom)
equalityTyCon,
concretePrimTyCon,
-- * SIMD
#include "primop-vector-tys-exports.hs-incl"
) where
......@@ -164,6 +166,7 @@ unexposedPrimTyCons
= [ eqPrimTyCon
, eqReprPrimTyCon
, eqPhantPrimTyCon
, concretePrimTyCon
]
-- | Primitive 'TyCon's that are defined in, and exported from, GHC.Prim.
......@@ -227,7 +230,19 @@ mkBuiltInPrimTc fs unique tycon
BuiltInSyntax
charPrimTyConName, intPrimTyConName, int8PrimTyConName, int16PrimTyConName, int32PrimTyConName, int64PrimTyConName, wordPrimTyConName, word32PrimTyConName, word8PrimTyConName, word16PrimTyConName, word64PrimTyConName, addrPrimTyConName, floatPrimTyConName, doublePrimTyConName, statePrimTyConName, proxyPrimTyConName, realWorldTyConName, arrayPrimTyConName, arrayArrayPrimTyConName, smallArrayPrimTyConName, byteArrayPrimTyConName, mutableArrayPrimTyConName, mutableByteArrayPrimTyConName, mutableArrayArrayPrimTyConName, smallMutableArrayPrimTyConName, mutVarPrimTyConName, mVarPrimTyConName, ioPortPrimTyConName, tVarPrimTyConName, stablePtrPrimTyConName, stableNamePrimTyConName, compactPrimTyConName, bcoPrimTyConName, weakPrimTyConName, threadIdPrimTyConName, eqPrimTyConName, eqReprPrimTyConName, eqPhantPrimTyConName, stackSnapshotPrimTyConName :: Name
charPrimTyConName, intPrimTyConName, int8PrimTyConName, int16PrimTyConName, int32PrimTyConName, int64PrimTyConName,
wordPrimTyConName, word32PrimTyConName, word8PrimTyConName, word16PrimTyConName, word64PrimTyConName,
addrPrimTyConName, floatPrimTyConName, doublePrimTyConName,
statePrimTyConName, proxyPrimTyConName, realWorldTyConName,
arrayPrimTyConName, arrayArrayPrimTyConName, smallArrayPrimTyConName, byteArrayPrimTyConName,
mutableArrayPrimTyConName, mutableByteArrayPrimTyConName, mutableArrayArrayPrimTyConName,
smallMutableArrayPrimTyConName, mutVarPrimTyConName, mVarPrimTyConName,
ioPortPrimTyConName, tVarPrimTyConName, stablePtrPrimTyConName,
stableNamePrimTyConName, compactPrimTyConName, bcoPrimTyConName,
weakPrimTyConName, threadIdPrimTyConName,
eqPrimTyConName, eqReprPrimTyConName, eqPhantPrimTyConName,
stackSnapshotPrimTyConName,
concretePrimTyConName :: Name
charPrimTyConName = mkPrimTc (fsLit "Char#") charPrimTyConKey charPrimTyCon
intPrimTyConName = mkPrimTc (fsLit "Int#") intPrimTyConKey intPrimTyCon
int8PrimTyConName = mkPrimTc (fsLit "Int8#") int8PrimTyConKey int8PrimTyCon
......@@ -267,6 +282,7 @@ stackSnapshotPrimTyConName = mkPrimTc (fsLit "StackSnapshot#") stackSnapshotP
bcoPrimTyConName = mkPrimTc (fsLit "BCO") bcoPrimTyConKey bcoPrimTyCon
weakPrimTyConName = mkPrimTc (fsLit "Weak#") weakPrimTyConKey weakPrimTyCon
threadIdPrimTyConName = mkPrimTc (fsLit "ThreadId#") threadIdPrimTyConKey threadIdPrimTyCon
concretePrimTyConName = mkPrimTc (fsLit "Concrete#") concretePrimTyConKey concretePrimTyCon
{-
************************************************************************
......@@ -1026,6 +1042,25 @@ equalityTyCon Nominal = eqPrimTyCon
equalityTyCon Representational = eqReprPrimTyCon
equalityTyCon Phantom = eqPhantPrimTyCon
{- *********************************************************************
* *
The Concrete mechanism
* *
********************************************************************* -}
-- See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete.
-- type Concrete# :: forall k. k -> TYPE (TupleRep '[])
concretePrimTyCon :: TyCon
concretePrimTyCon =
mkPrimTyCon concretePrimTyConName binders res_kind roles
where
-- Kind :: forall k. k -> TYPE (TupleRep '[])
binders = mkTemplateTyConBinders [liftedTypeKind] (\[k] -> [k])
res_kind = unboxedTupleKind []
roles = [Nominal, Nominal]
{- *********************************************************************
* *
The primitive array types
......
......@@ -547,30 +547,34 @@ Note [Core case invariants]
See Note [Case expression invariants]
Note [Representation polymorphism invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The representation polymorphism invariants are described as follows,
according to the paper "Levity Polymorphism", PLDI '17.
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
GHC allows us to abstract over calling conventions using **representation polymorphism**.
For example, we have:
($) :: forall (r :: RuntimeRep) (a :: Type) (b :: TYPE r). a -> b -> b
* The type of a term-binder must not be representation-polymorphic,
unless it is a let(rec)-bound join point
(see Note [Invariants on join points])
In this example, the type `b` is representation-polymorphic: it has kind `TYPE r`,
where the type variable `r :: RuntimeRep` abstracts over the runtime representation
of values of type `b`.
* The type of the argument of an App must not be representation-polymorphic.
To ensure that programs containing representation-polymorphism remain compilable,
we enforce two invariants (the representation-polymorphism invariants),
as per "Levity Polymorphism" [PLDI'17]:
A type (t::TYPE r) is "representation-polymorphic" if 'r' has any free variables,
and "levity-polymorphic" if it is of the form (t::TYPE (BoxedRep v))
and 'v' has free variables (levity polymorphism is a special case of
representation polymorphism).
Note that the aforementioned "Levity Polymorphism" paper conflates both these
types of polymorphism; a more precise distinction was only made possible
with the introduction of BoxedRep.
I1. The type of a bound variable must have a fixed runtime representation
(except for join points: See Note [Invariants on join points])
I2. The type of a function argument must have a fixed runtime representation.
For example
\(r::RuntimeRep). \(a::TYPE r). \(x::a). e
is illegal because x's type has kind (TYPE r), which has 'r' free.
We thus wouldn't know how to compile this lambda abstraction.
See Note [Representation polymorphism checking] in GHC.HsToCore.Monad to see where these
invariants are established for user-written code.
In practice, we currently require something slightly stronger than a fixed runtime
representation: we check whether bound variables and function arguments have a
/fixed RuntimeRep/ in the sense of Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
See Note [Representation polymorphism checking] in GHC.Tc.Utils.Concrete
for an overview of how we enforce these invariants in the typechecker.
Note [Core let goal]
~~~~~~~~~~~~~~~~~~~~
......@@ -712,7 +716,7 @@ However, join points have simpler invariants in other ways
ok-for-speculation (i.e. drop the let/app invariant)
e.g. let j :: Int# = factorial x in ...
6. A join point can have a representation-polymorphic RHS
6. The RHS of join point is not required to have a fixed runtime representation,
e.g. let j :: r :: TYPE l = fail void# in ...
This happened in an intermediate program #13394
......
......@@ -480,17 +480,17 @@ lintCoreBindings dflags pass local_in_scope binds
, lf_check_inline_loop_breakers = check_lbs
, lf_check_static_ptrs = check_static_ptrs
, lf_check_linearity = check_linearity
, lf_check_levity_poly = check_levity }
, lf_check_fixed_rep = check_fixed_rep }
-- In the output of the desugarer, before optimisation,
-- we have eta-expanded data constructors with representation-polymorphic
-- bindings; so we switch off the lev-poly checks. The very simple
-- optimiser will beta-reduce them away.
-- bindings; so we switch off the representation-polymorphism checks.
-- The very simple optimiser will beta-reduce them away.
-- See Note [Checking representation-polymorphic data constructors]
-- in GHC.HsToCore.Expr.
check_levity = case pass of
CoreDesugar -> False
_ -> True
check_fixed_rep = case pass of
CoreDesugar -> False
_ -> True
-- See Note [Checking for global Ids]
check_globals = case pass of
......@@ -565,7 +565,7 @@ lintUnfolding is_compulsory dflags locn var_set expr
(_warns, errs) = initL dflags (defaultLintFlags dflags) vars $
if is_compulsory
-- See Note [Checking for representation polymorphism]
then noLPChecks linter
then noFixedRuntimeRepChecks linter
else linter
linter = addLoc (ImportedUnfolding locn) $
lintCoreExpr expr
......@@ -749,8 +749,8 @@ lintIdUnfolding bndr bndr_ty uf
| isStableUnfolding uf
, Just rhs <- maybeUnfoldingTemplate uf
= do { ty <- fst <$> (if isCompulsoryUnfolding uf
then noLPChecks $ lintRhs bndr rhs
-- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
then noFixedRuntimeRepChecks $ lintRhs bndr rhs
-- ^^^^^^^^^^^^^^^^^^^^^^^
-- See Note [Checking for representation polymorphism]
else lintRhs bndr rhs)
; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "unfolding") ty) }
......@@ -1191,11 +1191,11 @@ lintCoreArg (fun_ty, fun_ue) arg
-- See Note [Representation polymorphism invariants] in GHC.Core
; flags <- getLintFlags
; when (lf_check_levity_poly flags) $
-- Only do these checks if lf_check_levity_poly is on,
; when (lf_check_fixed_rep flags) $
-- Only do these checks if lf_check_fixed_rep is on,
-- because otherwise isUnliftedType panics
do { checkL (not (isTypeLevPoly arg_ty))
(text "Representation-polymorphic argument:"
do { checkL (typeHasFixedRuntimeRep arg_ty)
(text "Argument does not have a fixed runtime representation"
<+> ppr arg <+> dcolon
<+> parens (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty)))
......@@ -1550,9 +1550,9 @@ lintIdBndr top_lvl bind_site id thing_inside
(mkNonTopExternalNameMsg id)
-- See Note [Representation polymorphism invariants] in GHC.Core
; lintL (isJoinId id || not (lf_check_levity_poly flags)
|| not (isTypeLevPoly id_ty)) $
text "Representation-polymorphic binder:" <+> ppr id <+> dcolon <+>
; lintL (isJoinId id || not (lf_check_fixed_rep flags)
|| typeHasFixedRuntimeRep id_ty) $
text "Binder does not have a fixed runtime representation:" <+> ppr id <+> dcolon <+>
parens (ppr id_ty <+> dcolon <+> ppr (typeKind id_ty))
-- Check that a join-id is a not-top-level let-binding
......@@ -2121,17 +2121,17 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
| allow_ill_kinded_univ_co prov
= return () -- Skip kind checks
| otherwise
= do { checkWarnL (not lev_poly1)
(report "left-hand type is representation-polymorphic")
; checkWarnL (not lev_poly2)
(report "right-hand type is representation-polymorphic")
; when (not (lev_poly1 || lev_poly2)) $
= do { checkWarnL fixed_rep_1
(report "left-hand type does not have a fixed runtime representation")
; checkWarnL fixed_rep_2
(report "right-hand type does not have a fixed runtime representation")
; when (fixed_rep_1 && fixed_rep_2) $
do { checkWarnL (reps1 `equalLength` reps2)
(report "between values with different # of reps")
; zipWithM_ validateCoercion reps1 reps2 }}
where
lev_poly1 = isTypeLevPoly t1
lev_poly2 = isTypeLevPoly t2
fixed_rep_1 = typeHasFixedRuntimeRep t1
fixed_rep_2 = typeHasFixedRuntimeRep t2
-- don't look at these unless lev_poly1/2 are False
-- Otherwise, we get #13458
......@@ -2559,7 +2559,7 @@ data LintFlags
, lf_check_static_ptrs :: StaticPtrCheck -- ^ See Note [Checking StaticPtrs]
, lf_report_unsat_syns :: Bool -- ^ See Note [Linting type synonym applications]
, lf_check_linearity :: Bool -- ^ See Note [Linting linearity]
, lf_check_levity_poly :: Bool -- See Note [Checking for representation polymorphism]
, lf_check_fixed_rep :: Bool -- See Note [Checking for representation polymorphism]
}
-- See Note [Checking StaticPtrs]
......@@ -2578,7 +2578,7 @@ defaultLintFlags dflags = LF { lf_check_global_ids = False
, lf_check_static_ptrs = AllowAnywhere
, lf_check_linearity = gopt Opt_DoLinearCoreLinting dflags
, lf_report_unsat_syns = True
, lf_check_levity_poly = True
, lf_check_fixed_rep = True
}
newtype LintM a =
......@@ -2737,10 +2737,10 @@ setReportUnsat ru thing_inside
in unLintM thing_inside env' errs
-- See Note [Checking for representation polymorphism]
noLPChecks :: LintM a -> LintM a
noLPChecks thing_inside
noFixedRuntimeRepChecks :: LintM a -> LintM a
noFixedRuntimeRepChecks thing_inside
= LintM $ \env errs ->
let env' = env { le_flags = (le_flags env) { lf_check_levity_poly = False } }
let env' = env { le_flags = (le_flags env) { lf_check_fixed_rep = False } }
in unLintM thing_inside env' errs
getLintFlags :: LintM LintFlags
......
......@@ -1591,7 +1591,7 @@ mkEtaWW orig_oss ppr_orig_expr in_scope orig_ty
----------- Function types (t1 -> t2)
| Just (mult, arg_ty, res_ty) <- splitFunTy_maybe ty
, not (isTypeLevPoly arg_ty)
, typeHasFixedRuntimeRep arg_ty
-- See Note [Representation polymorphism invariants] in GHC.Core
-- See also test case typecheck/should_run/EtaExpandLevPoly
......@@ -1621,7 +1621,7 @@ mkEtaWW orig_oss ppr_orig_expr in_scope orig_ty
| otherwise -- We have an expression of arity > 0,
-- but its type isn't a function, or a binder
-- is representation-polymorphic
-- does not have a fixed runtime representation
= warnPprTrace True ((ppr orig_oss <+> ppr orig_ty) $$ ppr_orig_expr)
(getTCvInScope subst, EI [] MRefl)
-- This *can* legitimately happen:
......
......@@ -82,7 +82,6 @@ import GHC.Core.Opt.Monad ( FloatOutSwitches(..) )
import GHC.Core.Utils ( exprType, exprIsHNF
, exprOkForSpeculation
, exprIsTopLevelBindable
, isExprLevPoly
, collectMakeStaticArgs
, mkLamTypes
)
......@@ -91,7 +90,9 @@ import GHC.Core.FVs -- all of it
import GHC.Core.Subst
import GHC.Core.Make ( sortQuantVars )
import GHC.Core.Type ( Type, splitTyConApp_maybe, tyCoVarsOfType
, mightBeUnliftedType, closeOverKindsDSet )
, mightBeUnliftedType, closeOverKindsDSet
, typeHasFixedRuntimeRep
)
import GHC.Core.Multiplicity ( pattern Many )
import GHC.Core.DataCon ( dataConOrigResTy )
......@@ -668,8 +669,9 @@ lvlMFE env strict_ctxt ann_expr
-- Only floating to the top level is allowed.
|| hasFreeJoin env fvs -- If there is a free join, don't float
-- See Note [Free join points]
|| isExprLevPoly expr
-- We can't let-bind representation-polymorphic expressions
|| not (typeHasFixedRuntimeRep (exprType expr))
-- We can't let-bind an expression if we don't know
-- how it will be represented at runtime.
-- See Note [Representation polymorphism invariants] in GHC.Core
|| notWorthFloating expr abs_vars
|| not float_me
......
......@@ -434,9 +434,8 @@ simplNonRecX env bndr new_rhs
; completeNonRecX NotTopLevel env' (isStrictId bndr') bndr bndr' new_rhs }
-- NotTopLevel: simplNonRecX is only used for NotTopLevel things
--
-- isStrictId: use bndr' because in a representation-polymorphic
-- setting, the InId bndr might have a representation-polymorphic
-- type, which isStrictId doesn't expect
-- isStrictId: use bndr' because the InId bndr might not have
-- a fixed runtime representation, which isStrictId doesn't expect
-- c.f. Note [Dark corner with representation polymorphism]
--------------------------
......@@ -1543,7 +1542,7 @@ simplCast env body co0 cont0
addCoerce co cont@(ApplyToVal { sc_arg = arg, sc_env = arg_se
, sc_dup = dup, sc_cont = tail })
| Just (m_co1, m_co2) <- pushCoValArg co
, levity_ok m_co1
, fixed_rep m_co1
= {-#SCC "addCoerce-pushCoValArg" #-}
do { tail' <- addCoerceM m_co2 tail
; case m_co1 of {
......@@ -1571,10 +1570,11 @@ simplCast env body co0 cont0
-- See Note [Optimising reflexivity]
| otherwise = return (CastIt co cont)
levity_ok :: MCoercionR -> Bool
levity_ok MRefl = True
levity_ok (MCo co) = not $ isTypeLevPoly $ coercionRKind co
-- Without this check, we get a lev-poly arg
fixed_rep :: MCoercionR -> Bool
fixed_rep MRefl = True
fixed_rep (MCo co) = typeHasFixedRuntimeRep $ coercionRKind co
-- Without this check, we can get an argument which does not
-- have a fixed runtime representation.
-- See Note [Representation polymorphism invariants] in GHC.Core
-- test: typecheck/should_run/EtaExpandLevPoly
......@@ -1717,10 +1717,10 @@ simplRecE env pairs body cont
; return (floats1 `addFloats` floats2, expr') }
{- Note [Dark corner with representation polymorphism]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In `simplNonRecE`, the call to `isStrictId` will fail if the binder
has a representation-polymorphic type, of kind (TYPE r). So we are careful to
call `isStrictId` on the OutId, not the InId, in case we have
does not have a fixed runtime representation, e.g. if it is of kind (TYPE r).
So we are careful to call `isStrictId` on the OutId, not the InId, in case we have
((\(r::RuntimeRep) \(x::TYPE r). blah) Lifted arg)
That will lead to `simplNonRecE env (x::TYPE r) arg`, and we can't tell
if x is lifted or unlifted from that.
......@@ -1736,7 +1736,7 @@ GHCi or TH and operator sections will fall over if we don't take
care here.
Note [Avoiding exponential behaviour]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
One way in which we can get exponential behaviour is if we simplify a
big expression, and the re-simplify it -- and then this happens in a
deeply-nested way. So we must be jolly careful about re-simplifying
......
{-# LANGUAGE DerivingStrategies #-}
{-
Describes predicates as they are considered by the solver.
......@@ -16,6 +18,9 @@ module GHC.Core.Predicate (
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
-- Special predicates
SpecialPred(..), specialPredTyCon,
-- Class predicates
mkClassPred, isDictTy,
isClassPred, isEqPredClass, isCTupleClass,
......@@ -41,6 +46,7 @@ import GHC.Core.Coercion
import GHC.Core.Multiplicity ( scaledThing )
import GHC.Builtin.Names
import GHC.Builtin.Types.Prim ( concretePrimTyCon )
import GHC.Utils.Outputable
import GHC.Utils.Misc
......@@ -51,11 +57,31 @@ import GHC.Data.FastString( FastString )
-- | A predicate in the solver. The solver tries to prove Wanted predicates
-- from Given ones.
data Pred
-- | A typeclass predicate.
= ClassPred Class [Type]
-- | A type equality predicate.
| EqPred EqRel Type Type
-- | An irreducible predicate.
| IrredPred PredType
-- | A quantified predicate.
--
-- See Note [Quantified constraints] in GHC.Tc.Solver.Canonical
| ForAllPred [TyVar] [PredType] PredType
-- ForAllPred: see Note [Quantified constraints] in GHC.Tc.Solver.Canonical
-- | A special predicate, used internally in GHC.
--
-- The meaning of the type argument is dictated by the 'SpecialPred'
-- specified in the first agument; see the documentation of 'SpecialPred' for more info.
--
-- Example: @Concrete# rep@, used for representation-polymorphism checks
-- within GHC. See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete.
-- (This is the only example currently. More to come: see GHC ticket #20000.)
| SpecialPred SpecialPred Type
-- NB: There is no TuplePred case
-- Tuple predicates like (Eq a, Ord b) are just treated
-- as ClassPred, as if we had a tuple class with two superclasses
......@@ -67,6 +93,10 @@ classifyPredType ev_ty = case splitTyConApp_maybe ev_ty of
| tc `hasKey` eqReprPrimTyConKey -> EqPred ReprEq ty1 ty2
| tc `hasKey` eqPrimTyConKey -> EqPred NomEq ty1 ty2
Just (tc, [_ki, ty])
| tc `hasKey` concretePrimTyConKey
-> SpecialPred ConcretePrimPred ty
Just (tc, tys)
| Just clas <- tyConClass_maybe tc
-> ClassPred clas tys
......@@ -161,6 +191,35 @@ predTypeEqRel ty
| otherwise
= NomEq
-- --------------------- Special predicates ----------------------------------
-- | 'SpecialPred' describes all the special predicates
-- that are currently used in GHC.
--
-- These are different from the special typeclasses
-- (such as `KnownNat`, `Typeable`, `Coercible`, ...), as special predicates
-- can't be expressed as typeclasses, as they hold evidence of a different kind.
data SpecialPred
-- | A @Concrete#@ predicate, to check for representation polymorphism.
--
-- When the first argument to the 'SpecialPred' data constructor of 'Pred'
-- is 'ConcretePrimPred', the second argument is the type we are inspecting
-- to decide whether it is concrete. That is, it refers to the
-- second argument of the 'Concrete#' 'TyCon'. Recall that this 'TyCon' has kind
--
-- > forall k. k -> TupleRep '[]
--
-- See Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete for further details.
= ConcretePrimPred
deriving stock Eq
instance Outputable SpecialPred where
ppr ConcretePrimPred = text "Concrete#"
-- | Obtain the 'TyCon' associated with a special predicate.
specialPredTyCon :: SpecialPred -> TyCon
specialPredTyCon ConcretePrimPred = concretePrimTyCon
{-------------------------------------------
Predicates on PredType
--------------------------------------------}
......
......@@ -40,6 +40,7 @@ module GHC.Core.TyCon(
mkTupleTyCon,
mkSumTyCon,
mkDataTyConRhs,
mkLevPolyDataTyConRhs,
mkSynonymTyCon,
mkFamilyTyCon,
mkPromotedDataCon,
......@@ -73,7 +74,8 @@ module GHC.Core.TyCon(
isImplicitTyCon,
isTyConWithSrcDataCons,
isTcTyCon, setTcTyConKind,
isTcLevPoly,
tcHasFixedRuntimeRep,
isConcreteTyCon,
-- ** Extracting information out of TyCons
tyConName,
......@@ -1018,6 +1020,86 @@ So, when promoted to become a type constructor, the tyConBinders
will include CoVars. That is why we use [TyConTyCoBinder] for the
tyconBinders field. TyConTyCoBinder is a synonym for TyConBinder,
but with the clue that the binder can be a CoVar not just a TyVar.
Note [Representation-polymorphic TyCons]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
To check for representation-polymorphism directly in the typechecker,
e.g. when using GHC.Tc.Utils.TcMType.checkTypeHasFixedRuntimeRep,
we need to compute whether a type has a fixed RuntimeRep,
as per Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete.
It's useful to have a quick way to check whether a saturated application
of a type constructor has a fixed RuntimeRep. That is, we want
to know, given a TyCon 'T' of arity 'n', does
T a_1 ... a_n
always have a fixed RuntimeRep? That is, is it always the case
that this application has a kind of the form
T a_1 ... a_n :: TYPE rep
in which 'rep' is a concrete 'RuntimeRep'?
('Concrete' in the sense of Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete:
it contains no type-family applications or type variables.)
To answer this question, we have 'tcHasFixedRuntimeRep'.
If 'tcHasFixedRuntimeRep' returns 'True', it means we're sure that
every saturated application of `T` has a fixed RuntimeRep.
However, if it returns 'False', we don't know: perhaps some application might not
have a fixed RuntimeRep.
Examples:
- For type families, we won't know in general whether an application
will have a fixed RuntimeRep:
type F :: k -> k
type family F a where {..}
`tcHasFixedRuntimeRep F = False'
- For newtypes, we're usually OK:
newtype N a b c = MkN Int
No matter what arguments we apply `N` to, we always get something of
kind `Type`, which has a fixed RuntimeRep.
Thus `tcHasFixedRuntimeRep N = True`.
However, with `-XUnliftedNewtypes`, we can have representation-polymorphic
newtypes:
type UN :: TYPE rep -> TYPE rep
newtype UN a = MkUN a
`tcHasFixedRuntimeRep UN = False`
For example, `UN @Int8Rep Int8#` is represented by an 8-bit value,
while `UN @LiftedRep Int` is represented by a heap pointer.
To distinguish whether we are dealing with a representation-polymorphic newtype,
we keep track of which situation we are in using the 'nt_fixed_rep'
field of the 'NewTyCon' constructor of 'AlgTyConRhs', and read this field
to compute 'tcHasFixedRuntimeRep'.
- A similar story can be told for datatypes: we're usually OK,
except with `-XUnliftedDatatypes` which allows for levity polymorphism,
e.g.:
type UC :: TYPE (BoxedRep l) -> TYPE (BoxedRep l)
type UC a = MkUC a
`tcHasFixedRuntimeRep UC = False`
Here, we keep track of whether we are dealing with a levity-polymorphic
unlifted datatype using the 'data_fixed_lev' field of the 'DataTyCon'
constructor of 'AlgTyConRhs'.
N.B.: technically, the representation of a datatype is fixed,
as it is always a pointer. However, we currently require that we
know the specific `RuntimeRep`: knowing that it's `BoxedRep l`
for a type-variable `l` isn't enough. See #15532.
-}
-- | Represents right-hand-sides of 'TyCon's for algebraic types
......@@ -1040,8 +1122,21 @@ data AlgTyConRhs
-- tag (see the tag assignment in mkTyConTagMap)
data_cons_size :: Int,
-- ^ Cached value: length data_cons
is_enum :: Bool -- ^ Cached value: is this an enumeration type?
is_enum :: Bool, -- ^ Cached value: is this an enumeration type?
-- See Note [Enumeration types]
data_fixed_lev :: Bool
-- ^ 'True' if the data type constructor has
-- a known, fixed levity when fully applied
-- to its arguments, False otherwise.
--
-- This can only be 'False' with UnliftedDatatypes,