diff options
| author | sheaf <sam.derbyshire@gmail.com> | 2021-10-15 23:09:39 +0200 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2021-10-17 14:06:46 -0400 |
| commit | 81740ce83976e9d6b68594f8a4b489452cca56e5 (patch) | |
| tree | 7b41d1529975c2f78eaced81e26e4722d34c212f /compiler/GHC | |
| parent | 65bf3992aebb3c08f0c4e13a3fb89dd5620015a9 (diff) | |
| download | haskell-81740ce83976e9d6b68594f8a4b489452cca56e5.tar.gz | |
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
-------------------------
Diffstat (limited to 'compiler/GHC')
67 files changed, 2387 insertions, 1233 deletions
diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs index 22b2cf6b9c..5f02b8e42b 100644 --- a/compiler/GHC/Builtin/Names.hs +++ b/compiler/GHC/Builtin/Names.hs @@ -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 ----------------------------------------------------- diff --git a/compiler/GHC/Builtin/PrimOps.hs b/compiler/GHC/Builtin/PrimOps.hs index 9bfed53382..40f5e65605 100644 --- a/compiler/GHC/Builtin/PrimOps.hs +++ b/compiler/GHC/Builtin/PrimOps.hs @@ -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. diff --git a/compiler/GHC/Builtin/Types/Prim.hs b/compiler/GHC/Builtin/Types/Prim.hs index 9ba6d87927..32ceb36a2d 100644 --- a/compiler/GHC/Builtin/Types/Prim.hs +++ b/compiler/GHC/Builtin/Types/Prim.hs @@ -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 {- ************************************************************************ @@ -1028,6 +1044,25 @@ 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 * * ********************************************************************* -} diff --git a/compiler/GHC/Core.hs b/compiler/GHC/Core.hs index fb93fc093f..9a52e96eae 100644 --- a/compiler/GHC/Core.hs +++ b/compiler/GHC/Core.hs @@ -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 diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs index 8854086d53..9c89044c81 100644 --- a/compiler/GHC/Core/Lint.hs +++ b/compiler/GHC/Core/Lint.hs @@ -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 diff --git a/compiler/GHC/Core/Opt/Arity.hs b/compiler/GHC/Core/Opt/Arity.hs index f25d04e0ed..c0a5f79b11 100644 --- a/compiler/GHC/Core/Opt/Arity.hs +++ b/compiler/GHC/Core/Opt/Arity.hs @@ -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: diff --git a/compiler/GHC/Core/Opt/SetLevels.hs b/compiler/GHC/Core/Opt/SetLevels.hs index b012c37e4e..084e8430e6 100644 --- a/compiler/GHC/Core/Opt/SetLevels.hs +++ b/compiler/GHC/Core/Opt/SetLevels.hs @@ -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 diff --git a/compiler/GHC/Core/Opt/Simplify.hs b/compiler/GHC/Core/Opt/Simplify.hs index 53d95a2c8b..407f84a6c5 100644 --- a/compiler/GHC/Core/Opt/Simplify.hs +++ b/compiler/GHC/Core/Opt/Simplify.hs @@ -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 diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs index 9601a92138..bf6d10f0f7 100644 --- a/compiler/GHC/Core/Predicate.hs +++ b/compiler/GHC/Core/Predicate.hs @@ -1,3 +1,5 @@ +{-# 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 --------------------------------------------} diff --git a/compiler/GHC/Core/TyCon.hs b/compiler/GHC/Core/TyCon.hs index 9001c3bc43..8a4da0f541 100644 --- a/compiler/GHC/Core/TyCon.hs +++ b/compiler/GHC/Core/TyCon.hs @@ -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, + -- e.g. + -- + -- > data A :: TYPE (BoxedRep l) where { MkA :: Int -> A } + -- + -- This boolean is cached to make it cheaper to check + -- for levity and representation-polymorphism in + -- tcHasFixedRuntimeRep. } | TupleTyCon { -- A boxed, unboxed, or constraint tuple @@ -1085,29 +1180,37 @@ data AlgTyConRhs -- See Note [Newtype eta] -- Watch out! If any newtypes become transparent -- again check #1072. - nt_lev_poly :: Bool - -- 'True' if the newtype can be - -- representation-polymorphic when fully applied to its - -- arguments, 'False' otherwise. - -- This can only ever be 'True' with UnliftedNewtypes. + nt_fixed_rep :: Bool + -- ^ 'True' if the newtype has a know, fixed representation + -- when fully applied to its arguments, 'False' otherwise. + -- This can only ever be 'False' with UnliftedNewtypes. + -- + -- Example: -- - -- Invariant: nt_lev_poly nt = isTypeLevPoly (nt_rhs nt) + -- > newtype N (a :: TYPE r) = MkN a -- - -- This is cached to make it cheaper to check if a - -- variable binding is representation-polymorphic, - -- as used by isTcLevPoly. + -- Invariant: nt_fixed_rep nt = tcHasFixedRuntimeRep (nt_rhs nt) + -- + -- This boolean is cached to make it cheaper to check if a + -- variable binding is representation-polymorphic + -- in tcHasFixedRuntimeRep. } mkSumTyConRhs :: [DataCon] -> AlgTyConRhs mkSumTyConRhs data_cons = SumTyCon data_cons (length data_cons) -mkDataTyConRhs :: [DataCon] -> AlgTyConRhs -mkDataTyConRhs cons +-- | Create an 'AlgTyConRhs' from the data constructors, +-- for a potentially levity-polymorphic datatype (with `UnliftedDatatypes`). +mkLevPolyDataTyConRhs :: Bool -- ^ whether the 'DataCon' has a fixed levity + -> [DataCon] + -> AlgTyConRhs +mkLevPolyDataTyConRhs fixed_lev cons = DataTyCon { data_cons = cons, data_cons_size = length cons, - is_enum = not (null cons) && all is_enum_con cons + is_enum = not (null cons) && all is_enum_con cons, -- See Note [Enumeration types] in GHC.Core.TyCon + data_fixed_lev = fixed_lev } where is_enum_con con @@ -1115,6 +1218,12 @@ mkDataTyConRhs cons <- dataConFullSig con = null ex_tvs && null eq_spec && null theta && null arg_tys +-- | Create an 'AlgTyConRhs' from the data constructors. +-- +-- Use 'mkLevPolyDataConRhs' if the datatype can be levity-polymorphic. +mkDataTyConRhs :: [DataCon] -> AlgTyConRhs +mkDataTyConRhs = mkLevPolyDataTyConRhs False + -- | Some promoted datacons signify extra info relevant to GHC. For example, -- the @IntRep@ constructor of @RuntimeRep@ corresponds to the 'IntRep' -- constructor of 'PrimRep'. This data structure allows us to store this @@ -1862,7 +1971,8 @@ noTcTyConScopedTyVars = [] -- | Create an unlifted primitive 'TyCon', such as @Int#@. mkPrimTyCon :: Name -> [TyConBinder] - -> Kind -- ^ /result/ kind, never representation-polymorphic + -> Kind -- ^ /result/ kind + -- Must answer 'True' to 'isFixedRuntimeRepKind' (no representation polymorphism). -> [Role] -> TyCon mkPrimTyCon name binders res_kind roles = mkPrimTyCon' name binders res_kind roles True (mkPrelTyConRepName name) @@ -1885,9 +1995,10 @@ mkLiftedPrimTyCon name binders res_kind roles where rep_nm = mkPrelTyConRepName name mkPrimTyCon' :: Name -> [TyConBinder] - -> Kind -- ^ /result/ kind, never representation-polymorphic + -> Kind -- ^ /result/ kind + -- Must answer 'True' to 'isFixedRuntimeRepKind' (i.e., no representation polymorphism). -- (If you need a representation-polymorphic PrimTyCon, - -- change isTcLevPoly.) + -- change tcHasFixedRuntimeRep.) -> [Role] -> Bool -> TyConRepName -> TyCon mkPrimTyCon' name binders res_kind roles is_unlifted rep_nm @@ -1981,7 +2092,7 @@ isFunTyCon _ = False -- | Test if the 'TyCon' is algebraic but abstract (invisible data constructors) isAbstractTyCon :: TyCon -> Bool -isAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon }) = True +isAbstractTyCon (AlgTyCon { algTcRhs = AbstractTyCon {} }) = True isAbstractTyCon _ = False -- | Does this 'TyCon' represent something that cannot be defined in Haskell? @@ -2360,25 +2471,61 @@ setTcTyConKind tc@(TcTyCon {}) kind = let tc' = tc { tyConKind = kind in tc' setTcTyConKind tc _ = pprPanic "setTcTyConKind" (ppr tc) --- | Could this TyCon ever be representation-polymorphic when fully applied? --- True is safe. False means we're sure. Does only a quick check --- based on the TyCon's category. --- Precondition: The fully-applied TyCon has kind (TYPE blah) -isTcLevPoly :: TyCon -> Bool -isTcLevPoly FunTyCon{} = False -isTcLevPoly (AlgTyCon { algTcParent = parent, algTcRhs = rhs }) +-- | Does this 'TyCon' have a fixed RuntimeRep when fully applied, +-- as per Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete? +-- +-- False is safe. True means we're sure. +-- Does only a quick check, based on the TyCon's category. +-- +-- See Note [Representation-polymorphic TyCons] +tcHasFixedRuntimeRep :: TyCon -> Bool +tcHasFixedRuntimeRep FunTyCon{} = True +tcHasFixedRuntimeRep (AlgTyCon { algTcParent = parent, algTcRhs = rhs }) | UnboxedAlgTyCon _ <- parent - = True - | NewTyCon { nt_lev_poly = lev_poly } <- rhs - = lev_poly -- Newtypes can be representation-polymorphic - -- with UnliftedNewtypes (#17360) - | otherwise = False -isTcLevPoly SynonymTyCon{} = True -isTcLevPoly FamilyTyCon{} = True -isTcLevPoly PrimTyCon{} = False -isTcLevPoly TcTyCon{} = False -isTcLevPoly tc@PromotedDataCon{} = pprPanic "isTcLevPoly datacon" (ppr tc) + | NewTyCon { nt_fixed_rep = fixed_rep } <- rhs + = fixed_rep -- A newtype might not have a fixed runtime representation + -- with UnliftedNewtypes (#17360) + | DataTyCon { data_fixed_lev = fixed_lev } <- rhs + = fixed_lev -- A datatype might not have a fixed levity with UnliftedDatatypes (#20423). + -- NB: the current representation-polymorphism checks require that + -- the representation be fully-known, including levity variables. + -- This might be relaxed in the future (#15532). + | AbstractTyCon {} <- rhs + = False -- An abstract TyCon might not have a fixed runtime representation. + -- Note that this is an entirely different matter from the concreteness + -- of the 'TyCon', in the sense of 'isConcreteTyCon'. + | otherwise + = True +tcHasFixedRuntimeRep SynonymTyCon{} = False +tcHasFixedRuntimeRep FamilyTyCon{} = False +tcHasFixedRuntimeRep PrimTyCon{} = True +tcHasFixedRuntimeRep TcTyCon{} = False +tcHasFixedRuntimeRep tc@PromotedDataCon{} = pprPanic "tcHasFixedRuntimeRep datacon" (ppr tc) + +-- | Is this 'TyCon' concrete (i.e. not a synonym/type family)? +-- +-- Used for representation polymorphism checks. +isConcreteTyCon :: TyCon -> Bool +isConcreteTyCon = isConcreteTyConFlavour . tyConFlavour + +-- | Is this 'TyConFlavour' concrete (i.e. not a synonym/type family)? +-- +-- Used for representation polymorphism checks. +isConcreteTyConFlavour :: TyConFlavour -> Bool +isConcreteTyConFlavour = \case + ClassFlavour -> True + TupleFlavour {} -> True + SumFlavour -> True + DataTypeFlavour -> True + NewtypeFlavour -> True + AbstractTypeFlavour -> True -- See (3) in Note [Solving Concrete# constraints] in GHC.Tc.Utils.Concrete + DataFamilyFlavour {} -> False -- See + OpenTypeFamilyFlavour {} -> False + ClosedTypeFamilyFlavour -> False + TypeSynonymFlavour -> False + BuiltInTypeFlavour -> True + PromotedDataConFlavour -> True {- ----------------------------------------------- @@ -2758,7 +2905,7 @@ tcFlavourMustBeSaturated NewtypeFlavour = False tcFlavourMustBeSaturated DataFamilyFlavour{} = False tcFlavourMustBeSaturated TupleFlavour{} = False tcFlavourMustBeSaturated SumFlavour = False -tcFlavourMustBeSaturated AbstractTypeFlavour = False +tcFlavourMustBeSaturated AbstractTypeFlavour {} = False tcFlavourMustBeSaturated BuiltInTypeFlavour = False tcFlavourMustBeSaturated PromotedDataConFlavour = False tcFlavourMustBeSaturated TypeSynonymFlavour = True @@ -2775,7 +2922,7 @@ tcFlavourIsOpen DataTypeFlavour = False tcFlavourIsOpen NewtypeFlavour = False tcFlavourIsOpen TupleFlavour{} = False tcFlavourIsOpen SumFlavour = False -tcFlavourIsOpen AbstractTypeFlavour = False +tcFlavourIsOpen AbstractTypeFlavour {} = False tcFlavourIsOpen BuiltInTypeFlavour = False tcFlavourIsOpen PromotedDataConFlavour = False tcFlavourIsOpen TypeSynonymFlavour = False diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index b2d12c7f35..16688cf287 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -145,7 +145,7 @@ module GHC.Core.Type ( Kind, -- ** Finding the kind of a type - typeKind, tcTypeKind, isTypeLevPoly, resultIsLevPoly, + typeKind, tcTypeKind, typeHasFixedRuntimeRep, resultHasFixedRuntimeRep, tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind, tcIsBoxedTypeKind, tcIsRuntimeTypeKind, @@ -233,7 +233,7 @@ module GHC.Core.Type ( -- * Kinds isConstraintKindCon, classifiesTypeWithValues, - isKindLevPoly + isConcrete, isFixedRuntimeRepKind, ) where import GHC.Prelude @@ -2971,31 +2971,32 @@ typeLiteralKind (NumTyLit {}) = naturalTy typeLiteralKind (StrTyLit {}) = typeSymbolKind typeLiteralKind (CharTyLit {}) = charTy --- | Returns True if a type is representation-polymorphic. Should be the same --- as (isKindLevPoly . typeKind) but much faster. --- Precondition: The type has kind (TYPE blah) -isTypeLevPoly :: Type -> Bool -isTypeLevPoly = go +-- | Returns True if a type has a fixed runtime rep, +-- as per Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete. +-- +-- This function is equivalent to @('isFixedRuntimeRepKind' . 'typeKind')@, +-- but much faster. +-- +-- __Precondition:__ The type has kind @('TYPE' blah)@ +typeHasFixedRuntimeRep :: Type -> Bool +typeHasFixedRuntimeRep = go where - go ty@(TyVarTy {}) = check_kind ty - go ty@(AppTy {}) = check_kind ty - go ty@(TyConApp tc _) | not (isTcLevPoly tc) = False - | otherwise = check_kind ty - go (ForAllTy _ ty) = go ty - go (FunTy {}) = False - go (LitTy {}) = False - go ty@(CastTy {}) = check_kind ty - go ty@(CoercionTy {}) = pprPanic "isTypeLevPoly co" (ppr ty) - - check_kind = isKindLevPoly . typeKind - --- | Looking past all pi-types, is the end result potentially --- representation-polymorphic? --- Example: True for (forall r (a :: TYPE r). String -> a) --- Example: False for (forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). a -> b -> Type) -resultIsLevPoly :: Type -> Bool -resultIsLevPoly = isTypeLevPoly . snd . splitPiTys - + go (TyConApp tc _) + | tcHasFixedRuntimeRep tc = True + go (FunTy {}) = True + go (LitTy {}) = True + go (ForAllTy _ ty) = go ty + go ty = isFixedRuntimeRepKind (typeKind ty) + +-- | Looking past all pi-types, does the end result have a +-- fixed runtime rep, as per Note [Fixed RuntimeRep] in GHC.Tc.Utils.Concrete? +-- +-- Examples: +-- +-- * False for @(forall r (a :: TYPE r). String -> a)@ +-- * True for @(forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). a -> b -> Type)@ +resultHasFixedRuntimeRep :: Type -> Bool +resultHasFixedRuntimeRep = typeHasFixedRuntimeRep . snd . splitPiTys {- ********************************************************************** * * @@ -3334,26 +3335,37 @@ distinct uniques, they are treated as equal at all times except during type inference. -} --- | Tests whether the given kind (which should look like @TYPE x@) --- is something other than a constructor tree (that is, constructors at every node). --- E.g. True of TYPE k, TYPE (F Int) --- False of TYPE 'LiftedRep -isKindLevPoly :: Kind -> Bool -isKindLevPoly k = assertPpr (isLiftedTypeKind k || _is_type) (ppr k) $ - -- the isLiftedTypeKind check is necessary b/c of Constraint - go k +-- | Tests whether the given kind is a constructor tree +-- (that is, constructors at every node). +-- +-- E.g. @False@ for @TYPE k@, @TYPE (F Int)@ +-- @True@ for @TYPE 'LiftedRep@ +-- +-- __Precondition:__ The type has kind @('TYPE' blah)@. +isFixedRuntimeRepKind :: HasDebugCallStack => Kind -> Bool +isFixedRuntimeRepKind k + = assertPpr (isLiftedTypeKind k || _is_type) (ppr k) $ + -- the isLiftedTypeKind check is necessary b/c of Constraint + isConcrete k + where + _is_type = classifiesTypeWithValues k + +-- | Tests whether the given type is a constructor tree, +-- consisting only of concrete type constructors and applications. +isConcrete :: Type -> Bool +isConcrete = go where go ty | Just ty' <- coreView ty = go ty' - go TyVarTy{} = True - go AppTy{} = True -- it can't be a TyConApp - go (TyConApp tc tys) = isFamilyTyCon tc || any go tys - go ForAllTy{} = True - go (FunTy _ w t1 t2) = go w || go t1 || go t2 - go LitTy{} = False - go CastTy{} = True - go CoercionTy{} = True - - _is_type = classifiesTypeWithValues k + go TyVarTy{} = False + go AppTy{} = False -- it can't be a TyConApp + go (TyConApp tc tys) + | isConcreteTyCon tc = all go tys + | otherwise = False + go ForAllTy{} = False + go (FunTy _ w t1 t2) = go w && go t1 && go t2 + go LitTy{} = True + go CastTy{} = False + go CoercionTy{} = False ----------------------------------------- -- | Does this classify a type allowed to have values? Responds True to things diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs index 03d3fca294..6b7eb3bf11 100644 --- a/compiler/GHC/Core/Utils.hs +++ b/compiler/GHC/Core/Utils.hs @@ -23,7 +23,6 @@ module GHC.Core.Utils ( -- * Properties of expressions exprType, coreAltType, coreAltsType, mkLamType, mkLamTypes, mkFunctionType, - isExprLevPoly, exprIsDupable, exprIsTrivial, getIdFromTrivialExpr, exprIsDeadEnd, getIdFromTrivialExpr_maybe, exprIsCheap, exprIsExpandable, exprIsCheapX, CheapAppFun, @@ -191,46 +190,6 @@ mkFunctionType mult arg_ty res_ty mkLamTypes vs ty = foldr mkLamType ty vs --- | Is this expression representation-polymorphic? This should be the --- same as saying (isKindLevPoly . typeKind . exprType) but --- much faster. -isExprLevPoly :: CoreExpr -> Bool -isExprLevPoly = go - where - go (Var _) = False -- no representation-poly binders - go (Lit _) = False -- no representation-poly literals - go e@(App f _) | not (go_app f) = False - | otherwise = check_type e - go (Lam _ _) = False - go (Let _ e) = go e - go e@(Case {}) = check_type e -- checking type is fast - go e@(Cast {}) = check_type e - go (Tick _ e) = go e - go e@(Type {}) = pprPanic "isExprLevPoly ty" (ppr e) - go (Coercion {}) = False -- this case can happen in GHC.Core.Opt.SetLevels - - check_type = isTypeLevPoly . exprType -- slow approach - - -- if the function is a variable (common case), check its - -- levityInfo. This might mean we don't need to look up and compute - -- on the type. Spec of these functions: return False if there is - -- no possibility, ever, of this expression becoming - -- representation-polymorphic, no matter what it's applied to; - -- return True otherwise. - -- Returning True is always safe. See also Note [Levity info] in - -- IdInfo - go_app (Var id) = not (isNeverLevPolyId id) - go_app (Lit _) = False - go_app (App f _) = go_app f - go_app (Lam _ e) = go_app e - go_app (Let _ e) = go_app e - go_app (Case _ _ ty _) = resultIsLevPoly ty - go_app (Cast _ co) = resultIsLevPoly (coercionRKind co) - go_app (Tick _ e) = go_app e - go_app e@(Type {}) = pprPanic "isExprLevPoly app ty" (ppr e) - go_app e@(Coercion {}) = pprPanic "isExprLevPoly app co" (ppr e) - - {- Note [Type bindings] ~~~~~~~~~~~~~~~~~~~~ @@ -2002,8 +1961,8 @@ exprIsTopLevelBindable :: CoreExpr -> Type -> Bool -- see Note [Core top-level string literals] in "GHC.Core" exprIsTopLevelBindable expr ty = not (mightBeUnliftedType ty) - -- Note that 'expr' may be representation-polymorphic here, consequently - -- we must use 'mightBeUnliftedType' rather than 'isUnliftedType', + -- Note that 'expr' may not have a fixed runtime representation here, + -- consequently we must use 'mightBeUnliftedType' rather than 'isUnliftedType', -- as the latter would panic. || exprIsTickedString expr diff --git a/compiler/GHC/CoreToIface.hs b/compiler/GHC/CoreToIface.hs index 2356f6c7f5..2a4e6c9f33 100644 --- a/compiler/GHC/CoreToIface.hs +++ b/compiler/GHC/CoreToIface.hs @@ -491,8 +491,8 @@ toIfaceIdInfo id_info inline_hsinfo | isDefaultInlinePragma inline_prag = Nothing | otherwise = Just (HsInline inline_prag) - ------------ Levity polymorphism ---------- - levity_hsinfo | isNeverLevPolyIdInfo id_info = Just HsLevity + ------------ Representation polymorphism ---------- + levity_hsinfo | isNeverRepPolyIdInfo id_info = Just HsLevity | otherwise = Nothing toIfaceJoinInfo :: Maybe JoinArity -> IfaceJoinInfo diff --git a/compiler/GHC/Data/List/SetOps.hs b/compiler/GHC/Data/List/SetOps.hs index fac12fadd8..9a5d138863 100644 --- a/compiler/GHC/Data/List/SetOps.hs +++ b/compiler/GHC/Data/List/SetOps.hs @@ -18,7 +18,7 @@ module GHC.Data.List.SetOps ( Assoc, assoc, assocMaybe, assocUsing, assocDefault, assocDefaultUsing, -- Duplicate handling - hasNoDups, removeDups, findDupsEq, + hasNoDups, removeDups, nubOrdBy, findDupsEq, equivClasses, -- Indexing @@ -160,6 +160,11 @@ equivClasses cmp items = NE.groupBy eq (L.sortBy cmp items) where eq a b = case cmp a b of { EQ -> True; _ -> False } +-- | Remove the duplicates from a list using the provided +-- comparison function. +-- +-- Returns the list without duplicates, and accumulates +-- all the duplicates in the second component of its result. removeDups :: (a -> a -> Ordering) -- Comparison function -> [a] -> ([a], -- List with no duplicates @@ -176,6 +181,11 @@ removeDups cmp xs collect_dups dups_so_far (x :| []) = (dups_so_far, x) collect_dups dups_so_far dups@(x :| _) = (dups:dups_so_far, x) +-- | Remove the duplicates from a list using the provided +-- comparison function. +nubOrdBy :: (a -> a -> Ordering) -> [a] -> [a] +nubOrdBy cmp xs = fst (removeDups cmp xs) + findDupsEq :: (a->a->Bool) -> [a] -> [NonEmpty a] findDupsEq _ [] = [] findDupsEq eq (x:xs) | L.null eq_xs = findDupsEq eq xs diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs index d6785c2a96..4e2dfc9316 100644 --- a/compiler/GHC/Hs/Expr.hs +++ b/compiler/GHC/Hs/Expr.hs @@ -178,10 +178,6 @@ data RecordUpdTc = RecordUpdTc } -- | HsWrap appears only in typechecker output --- Invariant: The contained Expr is *NOT* itself an HsWrap. --- See Note [Detecting forced eta expansion] in "GHC.HsToCore.Expr". --- This invariant is maintained by 'GHC.Hs.Utils.mkHsWrap'. --- hs_syn is something like HsExpr or HsCmd data HsWrap hs_syn = HsWrap HsWrapper -- the wrapper (hs_syn GhcTc) -- the thing that is wrapped diff --git a/compiler/GHC/Hs/Syn/Type.hs b/compiler/GHC/Hs/Syn/Type.hs index f586d8176b..f260a4c19b 100644 --- a/compiler/GHC/Hs/Syn/Type.hs +++ b/compiler/GHC/Hs/Syn/Type.hs @@ -181,7 +181,7 @@ hsWrapperType wrap ty = prTypeType $ go wrap (ty,[]) where go WpHole = id go (w1 `WpCompose` w2) = go w1 . go w2 - go (WpFun _ w2 (Scaled m exp_arg) _) = liftPRType $ \t -> + go (WpFun _ w2 (Scaled m exp_arg)) = liftPRType $ \t -> let act_res = funResultTy t exp_res = hsWrapperType w2 act_res in mkFunctionType m exp_arg exp_res diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs index e5e3b35b94..eb410a3c6a 100644 --- a/compiler/GHC/Hs/Utils.hs +++ b/compiler/GHC/Hs/Utils.hs @@ -785,13 +785,9 @@ mkClassOpSigs sigs mkLHsWrap :: HsWrapper -> LHsExpr GhcTc -> LHsExpr GhcTc mkLHsWrap co_fn (L loc e) = L loc (mkHsWrap co_fn e) --- | Avoid @'HsWrap' co1 ('HsWrap' co2 _)@ and @'HsWrap' co1 ('HsPar' _ _)@ --- See Note [Detecting forced eta expansion] in "GHC.HsToCore.Expr" mkHsWrap :: HsWrapper -> HsExpr GhcTc -> HsExpr GhcTc -mkHsWrap co_fn e | isIdHsWrapper co_fn = e -mkHsWrap co_fn (XExpr (WrapExpr (HsWrap co_fn' e))) = mkHsWrap (co_fn <.> co_fn') e -mkHsWrap co_fn (HsPar x lpar (L l e) rpar) = HsPar x lpar (L l (mkHsWrap co_fn e)) rpar -mkHsWrap co_fn e = XExpr (WrapExpr $ HsWrap co_fn e) +mkHsWrap co_fn e | isIdHsWrapper co_fn = e +mkHsWrap co_fn e = XExpr (WrapExpr $ HsWrap co_fn e) mkHsWrapCo :: TcCoercionN -- A Nominal coercion a ~N b -> HsExpr GhcTc -> HsExpr GhcTc diff --git a/compiler/GHC/HsToCore.hs b/compiler/GHC/HsToCore.hs index 2824b1fafe..bc87d42a75 100644 --- a/compiler/GHC/HsToCore.hs +++ b/compiler/GHC/HsToCore.hs @@ -648,7 +648,7 @@ or (Core) (x |> (GRefl :: a ~# (a |> TYPE co1)) ; co2) It looks like we can write this in Haskell directly, but we can't: -the reprsentation polymorphism checks defeat us. Note that `x` is a +the representation polymorphism checks defeat us. Note that `x` is a representation-polymorphic variable. So we must wire it in with a compulsory unfolding, like other representation-polymorphic primops. @@ -755,10 +755,13 @@ mkUnsafeCoercePrimPair _old_id old_expr info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma `setUnfoldingInfo` mkCompulsoryUnfolding' rhs + `setArityInfo` arity ty = mkSpecForAllTys [ runtimeRep1TyVar, runtimeRep2TyVar , openAlphaTyVar, openBetaTyVar ] $ mkVisFunTyMany openAlphaTy openBetaTy + arity = 1 + id = mkExportedVanillaId unsafeCoercePrimName ty `setIdInfo` info ; return (id, old_expr) } diff --git a/compiler/GHC/HsToCore/Arrows.hs b/compiler/GHC/HsToCore/Arrows.hs index 2338e2a451..9833a27f86 100644 --- a/compiler/GHC/HsToCore/Arrows.hs +++ b/compiler/GHC/HsToCore/Arrows.hs @@ -27,13 +27,11 @@ import GHC.Hs.Syn.Type -- So WATCH OUT; check each use of split*Ty functions. -- Sigh. This is a pain. -import {-# SOURCE #-} GHC.HsToCore.Expr ( dsExpr, dsLExpr, dsLExprNoLP, dsLocalBinds, +import {-# SOURCE #-} GHC.HsToCore.Expr ( dsExpr, dsLExpr, dsLocalBinds, dsSyntaxExpr ) import GHC.Tc.Utils.TcType -import GHC.Core.Type( splitPiTy ) import GHC.Core.Multiplicity -import GHC.Tc.Errors.Types ( LevityCheckProvenance(..) ) import GHC.Tc.Types.Evidence import GHC.Core import GHC.Core.FVs @@ -75,25 +73,6 @@ mkCmdEnv tc_meths the_choice_id = assocMaybe prs choiceAName the_loop_id = assocMaybe prs loopAName - -- used as an argument in, e.g., do_premap - ; check_lev_poly 3 the_arr_id - - -- used as an argument in, e.g., dsCmdStmt/BodyStmt - ; check_lev_poly 5 the_compose_id - - -- used as an argument in, e.g., dsCmdStmt/BodyStmt - ; check_lev_poly 4 the_first_id - - -- the result of the_app_id is used as an argument in, e.g., - -- dsCmd/HsCmdArrApp/HsHigherOrderApp - ; check_lev_poly 2 the_app_id - - -- used as an argument in, e.g., HsCmdIf - ; check_lev_poly 5 the_choice_id - - -- used as an argument in, e.g., RecStmt - ; check_lev_poly 4 the_loop_id - ; return (meth_binds, DsCmdEnv { arr_id = Var (unmaybe the_arr_id arrAName), compose_id = Var (unmaybe the_compose_id composeAName), @@ -112,20 +91,6 @@ mkCmdEnv tc_meths unmaybe Nothing name = pprPanic "mkCmdEnv" (text "Not found:" <+> ppr name) unmaybe (Just id) _ = id - -- returns the result type of a pi-type (that is, a forall or a function) - -- Note that this result type may be ill-scoped. - res_type :: Type -> Type - res_type ty = res_ty - where - (_, res_ty) = splitPiTy ty - - check_lev_poly :: Int -- arity - -> Maybe Id -> DsM () - check_lev_poly _ Nothing = return () - check_lev_poly arity (Just id) - = dsNoLevPoly (nTimes arity res_type (idType id)) (LevityCheckMkCmdEnv id) - - -- arr :: forall b c. (b -> c) -> a b c do_arr :: DsCmdEnv -> Type -> Type -> CoreExpr -> CoreExpr do_arr ids b_ty c_ty f = mkApps (arr_id ids) [Type b_ty, Type c_ty, f] @@ -367,7 +332,7 @@ dsCmd ids local_vars stack_ty res_ty let (a_arg_ty, _res_ty') = tcSplitAppTy arrow_ty (_a_ty, arg_ty) = tcSplitAppTy a_arg_ty - core_arrow <- dsLExprNoLP arrow + core_arrow <- dsLExpr arrow core_arg <- dsLExpr arg stack_id <- newSysLocalDs Many stack_ty core_make_arg <- matchEnvStack env_ids stack_id core_arg @@ -423,7 +388,7 @@ dsCmd ids local_vars stack_ty res_ty (HsCmdApp _ cmd arg) env_ids = do (core_cmd, free_vars, env_ids') <- dsfixCmd ids local_vars stack_ty' res_ty cmd stack_id <- newSysLocalDs Many stack_ty - arg_id <- newSysLocalDsNoLP Many arg_ty + arg_id <- newSysLocalDs Many arg_ty -- push the argument expression onto the stack let stack' = mkCorePairExpr (Var arg_id) (Var stack_id) @@ -628,11 +593,7 @@ dsCmd ids local_vars stack_ty res_ty (HsCmdLet _ lbinds@binds body) env_ids = do -- -- ---> premap (\ (env,stk) -> env) c -dsCmd ids local_vars stack_ty res_ty do_block@(HsCmdDo stmts_ty - (L loc stmts)) - env_ids = do - putSrcSpanDsA loc $ - dsNoLevPoly stmts_ty (LevityCheckDoCmd do_block) +dsCmd ids local_vars stack_ty res_ty (HsCmdDo _ (L _ stmts)) env_ids = do (core_stmts, env_ids') <- dsCmdDo ids local_vars res_ty stmts env_ids let env_ty = mkBigCoreVarTupTy env_ids core_fst <- mkFstExpr env_ty stack_ty @@ -702,8 +663,7 @@ dsfixCmd DIdSet, -- subset of local vars that occur free [Id]) -- the same local vars as a list, fed back dsfixCmd ids local_vars stk_ty cmd_ty cmd - = do { putSrcSpanDs (getLocA cmd) $ dsNoLevPoly cmd_ty (LevityCheckDesugaringCmd cmd) - ; trimInput (dsLCmd ids local_vars stk_ty cmd_ty cmd) } + = trimInput (dsLCmd ids local_vars stk_ty cmd_ty cmd) -- Feed back the list of local variables actually used a command, -- for use as the input tuple of the generated arrow. @@ -744,7 +704,7 @@ dsCmdLam ids local_vars stack_ty res_ty pats body env_ids = do (pat_tys, stack_ty') = splitTypeAt (length pats) stack_ty (core_body, free_vars, env_ids') <- dsfixCmd ids local_vars' stack_ty' res_ty body - param_ids <- mapM (newSysLocalDsNoLP Many) pat_tys + param_ids <- mapM (newSysLocalDs Many) pat_tys stack_id' <- newSysLocalDs Many stack_ty' -- the expression is built from the inside out, so the actions @@ -790,8 +750,7 @@ dsCmdDo _ _ _ [] _ = panic "dsCmdDo" -- -- ---> premap (\ (xs) -> ((xs), ())) c -dsCmdDo ids local_vars res_ty [L loc (LastStmt _ body _ _)] env_ids = do - putSrcSpanDsA loc $ dsNoLevPoly res_ty (LevityCheckInCmd body) +dsCmdDo ids local_vars res_ty [L _ (LastStmt _ body _ _)] env_ids = do (core_body, env_ids') <- dsLCmd ids local_vars unitTy res_ty body env_ids let env_ty = mkBigCoreVarTupTy env_ids env_var <- newSysLocalDs Many env_ty @@ -859,7 +818,6 @@ dsCmdStmt ids local_vars out_ids (BodyStmt c_ty cmd _ _) env_ids = do out_ty = mkBigCoreVarTupTy out_ids before_c_ty = mkCorePairTy in_ty1 out_ty after_c_ty = mkCorePairTy c_ty out_ty - dsNoLevPoly c_ty LevityCheckCmdStmt snd_fn <- mkSndExpr c_ty out_ty return (do_premap ids in_ty before_c_ty out_ty core_mux $ do_compose ids before_c_ty after_c_ty out_ty diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs index 602de4070a..596e4333b1 100644 --- a/compiler/GHC/HsToCore/Binds.hs +++ b/compiler/GHC/HsToCore/Binds.hs @@ -1118,16 +1118,13 @@ dsHsWrapper (WpCompose c1 c2) = do { w1 <- dsHsWrapper c1 ; return (w1 . w2) } -- See comments on WpFun in GHC.Tc.Types.Evidence for an explanation of what -- the specification of this clause is -dsHsWrapper (WpFun c1 c2 (Scaled w t1) doc) - = do { x <- newSysLocalDsNoLP w t1 +dsHsWrapper (WpFun c1 c2 (Scaled w t1)) + = do { x <- newSysLocalDs w t1 ; w1 <- dsHsWrapper c1 ; w2 <- dsHsWrapper c2 ; let app f a = mkCoreAppDs (text "dsHsWrapper") f a arg = w1 (Var x) - ; (_, ok) <- askNoErrsDs $ dsNoLevPolyExpr arg (LevityCheckWpFun doc) - ; if ok - then return (\e -> (Lam x (w2 (app e arg)))) - else return id } -- this return is irrelevant + ; return (\e -> (Lam x (w2 (app e arg)))) } dsHsWrapper (WpCast co) = assert (coercionRole co == Representational) $ return $ \e -> mkCastDs e co dsHsWrapper (WpEvApp tm) = do { core_tm <- dsEvTerm tm diff --git a/compiler/GHC/HsToCore/Errors/Ppr.hs b/compiler/GHC/HsToCore/Errors/Ppr.hs index 3109370543..a1aa921b2e 100644 --- a/compiler/GHC/HsToCore/Errors/Ppr.hs +++ b/compiler/GHC/HsToCore/Errors/Ppr.hs @@ -5,14 +5,11 @@ module GHC.HsToCore.Errors.Ppr where import GHC.Builtin.Names (withDictName) import GHC.Core.Predicate (isEvVar) -import GHC.Core.TyCo.Ppr (pprWithTYPE) import GHC.Core.Type -import GHC.Core.Utils (exprType) import GHC.Driver.Flags import GHC.Hs import GHC.HsToCore.Errors.Types import GHC.Prelude -import GHC.Tc.Errors.Ppr (formatLevPolyErr, pprLevityPolyInType) import GHC.Types.Basic (pprRuleName) import GHC.Types.Error import GHC.Types.Id (idType) @@ -197,21 +194,6 @@ instance Diagnostic DsMessage where -> mkSimpleDecorated $ hang (text "Recursive bindings for unlifted types aren't allowed:") 2 (vcat (map ppr binds)) - DsCannotUseFunWithPolyArgs orig_hs_expr ty bad_tys - -> mkSimpleDecorated $ - vcat [ hang (text "Cannot use function with representation-polymorphic arguments:") - 2 (hang (ppr orig_hs_expr) 2 (dcolon <+> pprWithTYPE ty)) - , ppUnlessOption sdocPrintTypecheckerElaboration $ vcat - [ text "(Note that representation-polymorphic primops," - , text "such as 'coerce' and unboxed tuples, are eta-expanded" - , text "internally because they must occur fully saturated." - , text "Use -fprint-typechecker-elaboration to display the full expression.)" - ] - , hang (text "Representation-polymorphic arguments:") - 2 $ vcat $ map - (\t -> pprWithTYPE t <+> dcolon <+> pprWithTYPE (typeKind t)) - bad_tys - ] DsRuleMightInlineFirst rule_name lhs_id _ -> mkSimpleDecorated $ vcat [ hang (text "Rule" <+> pprRuleName rule_name @@ -227,17 +209,6 @@ instance Diagnostic DsMessage where <+> text "for"<+> quotes (ppr lhs_id) <+> text "might fire first") ] - DsLevityPolyInExpr e prov - -> let extra = case prov of - LevityCheckHsExpr hsExpr -> ppr hsExpr - LevityCheckWpFun doc -> doc - LevityCheckInSyntaxExpr (DsArgNum n) expr - -> text "In the" <+> speakNth n <+> text "argument of" <+> quotes (ppr expr) - - in mkSimpleDecorated $ - formatLevPolyErr (exprType e) $$ (text "In the type of expression:" <+> extra) - DsLevityPolyInType ty prov - -> mkSimpleDecorated $ pprLevityPolyInType ty prov diagnosticReason = \case DsUnknownMessage m -> diagnosticReason m @@ -268,11 +239,8 @@ instance Diagnostic DsMessage where DsWrongDoBind{} -> WarningWithFlag Opt_WarnWrongDoBind DsUnusedDoBind{} -> WarningWithFlag Opt_WarnUnusedDoBind DsRecBindsNotAllowedForUnliftedTys{} -> ErrorWithoutFlag - DsCannotUseFunWithPolyArgs{} -> ErrorWithoutFlag DsRuleMightInlineFirst{} -> WarningWithFlag Opt_WarnInlineRuleShadowing DsAnotherRuleMightFireFirst{} -> WarningWithFlag Opt_WarnInlineRuleShadowing - DsLevityPolyInExpr{} -> ErrorWithoutFlag - DsLevityPolyInType{} -> ErrorWithoutFlag diagnosticHints = \case DsUnknownMessage m -> diagnosticHints m @@ -309,11 +277,8 @@ instance Diagnostic DsMessage where DsUnusedDoBind rhs _ -> [SuggestBindToWildcard rhs] DsRecBindsNotAllowedForUnliftedTys{} -> noHints DsInvalidInstantiationDictAtType{} -> noHints - DsCannotUseFunWithPolyArgs{} -> noHints DsRuleMightInlineFirst _ lhs_id rule_act -> [SuggestAddInlineOrNoInlinePragma lhs_id rule_act] DsAnotherRuleMightFireFirst _ bad_rule _ -> [SuggestAddPhaseToCompetingRule bad_rule] - DsLevityPolyInExpr{} -> noHints - DsLevityPolyInType{} -> noHints {- Note [Suggest NegativeLiterals] diff --git a/compiler/GHC/HsToCore/Errors/Types.hs b/compiler/GHC/HsToCore/Errors/Types.hs index 1747ae7914..55164e741b 100644 --- a/compiler/GHC/HsToCore/Errors/Types.hs +++ b/compiler/GHC/HsToCore/Errors/Types.hs @@ -12,13 +12,11 @@ import GHC.Core.Type import GHC.Driver.Session import GHC.Hs import GHC.HsToCore.Pmc.Solver.Types -import GHC.Tc.Errors.Types (LevityCheckProvenance) import GHC.Types.Basic (Activation) import GHC.Types.Error import GHC.Types.ForeignCall import GHC.Types.Id import GHC.Types.Name (Name) -import GHC.Utils.Outputable import qualified GHC.LanguageExtensions as LangExt newtype MinBound = MinBound Integer @@ -144,31 +142,15 @@ data DsMessage | DsRecBindsNotAllowedForUnliftedTys ![LHsBindLR GhcTc GhcTc] - -- NOTE(adn) The first argument is an opaque 'expr' with an - -- 'Outputable' constraint because this messages is emitted from - -- 'GHC.HsToCore.Expr.checkLevPolyArgs' which gets passed a polymorphic - -- 'Outputable' type. - | forall expr. Outputable expr => DsCannotUseFunWithPolyArgs !expr !Type ![Type] - | DsRuleMightInlineFirst !RuleName !Var !Activation | DsAnotherRuleMightFireFirst !RuleName !RuleName -- the \"bad\" rule !Var - | DsLevityPolyInExpr !CoreExpr !LevityExprProvenance - - | DsLevityPolyInType !Type !LevityCheckProvenance - -- The positional number of the argument for an expression (first, second, third, etc) newtype DsArgNum = DsArgNum Int --- | Where the levity checking for the expression originated -data LevityExprProvenance - = LevityCheckHsExpr !(HsExpr GhcTc) - | LevityCheckWpFun !SDoc -- FIXME(adn) Alas 'WpFun' gives us an SDoc here. - | LevityCheckInSyntaxExpr !DsArgNum !(HsExpr GhcTc) - -- | Why TemplateHaskell rejected the splice. Used in the 'DsNotYetHandledByTH' -- constructor of a 'DsMessage'. data ThRejectionReason diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs index c22bb5a135..a8f14ffdd0 100644 --- a/compiler/GHC/HsToCore/Expr.hs +++ b/compiler/GHC/HsToCore/Expr.hs @@ -13,7 +13,7 @@ Desugaring expressions. -} module GHC.HsToCore.Expr - ( dsExpr, dsLExpr, dsLExprNoLP, dsLocalBinds + ( dsExpr, dsLExpr, dsLocalBinds , dsValBinds, dsLit, dsSyntaxExpr ) where @@ -30,7 +30,6 @@ import GHC.HsToCore.Arrows import GHC.HsToCore.Monad import GHC.HsToCore.Pmc ( addTyCs, pmcGRHSs ) import GHC.HsToCore.Errors.Types -import GHC.Hs.Syn.Type ( hsExprType, hsWrapperType ) import GHC.Types.SourceText import GHC.Types.Name import GHC.Types.Name.Env @@ -241,18 +240,6 @@ dsLExpr :: LHsExpr GhcTc -> DsM CoreExpr dsLExpr (L loc e) = putSrcSpanDsA loc $ dsExpr e --- | Variant of 'dsLExpr' that ensures that the result is not --- representation- polymorphic. This should be used when the resulting --- expression will be an argument to some other function. --- See Note [Representation polymorphism checking] in "GHC.HsToCore.Monad" --- See Note [Representation polymorphism invariants] in "GHC.Core" -dsLExprNoLP :: LHsExpr GhcTc -> DsM CoreExpr -dsLExprNoLP (L loc e) - = putSrcSpanDsA loc $ - do { e' <- dsExpr e - ; dsNoLevPolyExpr e' (LevityCheckHsExpr e) - ; return e' } - dsExpr :: HsExpr GhcTc -> DsM CoreExpr dsExpr (HsVar _ (L _ id)) = dsHsVar id dsExpr (HsRecSel _ (FieldOcc id _)) = dsHsVar id @@ -279,7 +266,7 @@ dsExpr e@(XExpr ext_expr_tc) = case ext_expr_tc of ExpansionExpr (HsExpanded _ b) -> dsExpr b WrapExpr {} -> dsHsWrapped e - ConLikeTc {} -> dsHsWrapped e + ConLikeTc con tvs tys -> dsConLike con tvs tys -- Hpc Support HsTick tickish e -> do e' <- dsLExpr e @@ -320,10 +307,8 @@ dsExpr (HsLamCase _ matches) dsExpr e@(HsApp _ fun arg) = do { fun' <- dsLExpr fun - -- See Note [Desugaring representation-polymorphic applications] - -- in GHC.HsToCore.Utils - ; dsWhenNoErrs (hsExprType e) (dsLExprNoLP arg) - (\arg' -> mkCoreAppDs (text "HsApp" <+> ppr e) fun' arg') } + ; arg' <- dsLExpr arg + ; return $ mkCoreAppDs (text "HsApp" <+> ppr e) fun' arg' } dsExpr e@(HsAppType {}) = dsHsWrapped e @@ -345,32 +330,25 @@ That 'g' in the 'in' part is an evidence variable, and when converting to core it must become a CO. -} -dsExpr e@(ExplicitTuple _ tup_args boxity) +dsExpr (ExplicitTuple _ tup_args boxity) = do { let go (lam_vars, args) (Missing (Scaled mult ty)) -- For every missing expression, we need -- another lambda in the desugaring. - = do { lam_var <- newSysLocalDsNoLP mult ty + = do { lam_var <- newSysLocalDs mult ty ; return (lam_var : lam_vars, Var lam_var : args) } go (lam_vars, args) (Present _ expr) -- Expressions that are present don't generate -- lambdas, just arguments. - = do { core_expr <- dsLExprNoLP expr + = do { core_expr <- dsLExpr expr ; return (lam_vars, core_expr : args) } - -- See Note [Desugaring representation-polymorphic applications] - -- in GHC.HsToCore.Utils - ; dsWhenNoErrs (hsExprType e) (foldM go ([], []) (reverse tup_args)) + ; (lam_vars, args) <- foldM go ([], []) (reverse tup_args) -- The reverse is because foldM goes left-to-right - (\(lam_vars, args) -> - mkCoreLams lam_vars $ - mkCoreTupBoxity boxity args) } + ; return $ mkCoreLams lam_vars (mkCoreTupBoxity boxity args) } -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make -dsExpr e@(ExplicitSum types alt arity expr) - -- See Note [Desugaring representation-polymorphic applications] - -- in GHC.HsToCore.Utils - = dsWhenNoErrs (hsExprType e) (dsLExprNoLP expr) - (mkCoreUbxSum arity alt types) +dsExpr (ExplicitSum types alt arity expr) + = mkCoreUbxSum arity alt types <$> dsLExpr expr dsExpr (HsPragE _ prag expr) = ds_prag_expr prag expr @@ -441,7 +419,7 @@ See Note [Grand plan for static forms] in GHC.Iface.Tidy.StaticPtrTable for an o -} dsExpr (HsStatic _ expr@(L loc _)) = do - expr_ds <- dsLExprNoLP expr + expr_ds <- dsLExpr expr let ty = exprType expr_ds makeStaticId <- dsLookupGlobalId makeStaticName @@ -495,8 +473,8 @@ dsExpr (RecordCon { rcon_con = L _ con_like mk_arg (arg_ty, fl) = case findField (rec_flds rbinds) (flSelector fl) of - (rhs:rhss) -> assert (null rhss ) - dsLExprNoLP rhs + (rhs:rhss) -> assert (null rhss) + dsLExpr rhs [] -> mkErrorAppDs rEC_CON_ERROR_ID arg_ty (ppr (flLabel fl)) unlabelled_bottom arg_ty = mkErrorAppDs rEC_CON_ERROR_ID arg_ty Outputable.empty @@ -808,23 +786,7 @@ dsSyntaxExpr (SyntaxExprTc { syn_expr = expr ; core_arg_wraps <- mapM dsHsWrapper arg_wraps ; core_res_wrap <- dsHsWrapper res_wrap ; let wrapped_args = zipWithEqual "dsSyntaxExpr" ($) core_arg_wraps arg_exprs - -- We need to compute the type of the desugared expression without - -- actually performing the desugaring, which could be problematic - -- in the presence of representation polymorphism. - -- See Note [Desugaring representation-polymorphic applications] - -- in GHC.HsToCore.Utils - expr_type = hsWrapperType res_wrap - (applyTypeToArgs (ppr fun) (exprType fun) wrapped_args) - ; dsWhenNoErrs expr_type - (zipWithM_ dsNoLevPolyExpr wrapped_args [ mk_msg n | n <- [1..] ]) - (\_ -> core_res_wrap (mkCoreApps fun wrapped_args)) } - -- Use mkCoreApps instead of mkApps: - -- unboxed types are possible with RebindableSyntax (#19883) - -- This won't be evaluated if there are any - -- representation-polymorphic arguments. - - where - mk_msg n = LevityCheckInSyntaxExpr (DsArgNum n) expr + ; return $ core_res_wrap (mkCoreApps fun wrapped_args) } dsSyntaxExpr NoSyntaxExprTc _ = panic "dsSyntaxExpr" findField :: [LHsRecField GhcTc arg] -> Name -> [arg] @@ -897,7 +859,7 @@ dsExplicitList :: Type -> [LHsExpr GhcTc] -- See Note [Desugaring explicit lists] dsExplicitList elt_ty xs = do { dflags <- getDynFlags - ; xs' <- mapM dsLExprNoLP xs + ; xs' <- mapM dsLExpr xs ; if xs' `lengthExceeds` maxBuildLength -- Don't generate builds if the list is very long. || null xs' @@ -913,25 +875,25 @@ dsExplicitList elt_ty xs dsArithSeq :: PostTcExpr -> (ArithSeqInfo GhcTc) -> DsM CoreExpr dsArithSeq expr (From from) - = App <$> dsExpr expr <*> dsLExprNoLP from + = App <$> dsExpr expr <*> dsLExpr from dsArithSeq expr (FromTo from to) = do fam_envs <- dsGetFamInstEnvs dflags <- getDynFlags warnAboutEmptyEnumerations fam_envs dflags from Nothing to expr' <- dsExpr expr - from' <- dsLExprNoLP from - to' <- dsLExprNoLP to + from' <- dsLExpr from + to' <- dsLExpr to return $ mkApps expr' [from', to'] dsArithSeq expr (FromThen from thn) - = mkApps <$> dsExpr expr <*> mapM dsLExprNoLP [from, thn] + = mkApps <$> dsExpr expr <*> mapM dsLExpr [from, thn] dsArithSeq expr (FromThenTo from thn to) = do fam_envs <- dsGetFamInstEnvs dflags <- getDynFlags warnAboutEmptyEnumerations fam_envs dflags from (Just thn) to expr' <- dsExpr expr - from' <- dsLExprNoLP from - thn' <- dsLExprNoLP thn - to' <- dsLExprNoLP to + from' <- dsLExpr from + thn' <- dsLExpr thn + to' <- dsLExpr to return $ mkApps expr' [from', thn', to'] {- @@ -1057,8 +1019,7 @@ dsHsVar :: Id -> DsM CoreExpr -- NB: withDict is always instantiated by a wrapper, so we need -- only check for it in dsHsUnwrapped dsHsVar var - = do { checkLevPolyFunction var var (idType var) - ; return (varToCoreExpr var) } -- See Note [Desugaring vars] + = return (varToCoreExpr var) -- See Note [Desugaring vars] dsHsConLike :: ConLike -> DsM CoreExpr dsHsConLike (RealDataCon dc) @@ -1131,112 +1092,13 @@ warnDiscardedDoBindings rhs rhs_ty {- ************************************************************************ * * - Representation polymorphism checks + dsHsWrapped and ds_withDict * * ************************************************************************ - -Note [Checking for representation-polymorphic functions] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We cannot have representation-polymorphic function arguments. See -Note [Representation polymorphism invariants] in GHC.Core. That is -checked by dsLExprNoLP. - -But what about - const True (unsafeCoerce# :: forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). a -> b) - -Since `unsafeCoerce#` has no binding, it has a compulsory unfolding. -But that compulsory unfolding is a representation-polymorphic lambda, which -is no good. So we want to reject this. On the other hand - const True (unsafeCoerce# @LiftedRep @UnliftedRep) -is absolutely fine. - -We have to collect all the type-instantiation and *then* check. That -is what dsHsWrapped does. Because we might have an HsVar without a -wrapper, we check in dsHsVar as well. typecheck/should_fail/T17021 -triggers this case. - -Note that if `f :: forall r (a :: TYPE r). blah`, then - const True f -is absolutely fine. Here `f` is a function, represented by a -pointer, and we can pass it to `const` (or anything else). (See -#12708 for an example.) It's only the Id.hasNoBinding functions -that are a problem. See checkLevPolyFunction. - -Interestingly, this approach does not look to see whether the Id in -question will be eta expanded. The logic is this: - * Either the Id in question is saturated or not. - * If it is, then it surely can't have representation-polymorphic arguments. - If its wrapped type contains representation-polymorphic arguments, reject. - * If it's not, then it can't be eta expanded with representation-polymorphic - argument. If its wrapped type contains representation-polymorphic arguments, - reject. -So, either way, we're good to reject. - -Note [Nasty wrinkle in representation-polymorphic function check] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A nasty wrinkle came up in T13244 - type family Rep x - type instance Rep Int = IntRep - - type Unboxed x :: TYPE (Rep x) - type instance Unboxed Int = Int# - - box :: Unboxed Int -> Int - box = I# - -Here the function I# is wrapped in a /cast/, thus - box = I# |> (co :: (Int# -> Int) ~ (Unboxed Int -> Int)) -If we look only at final type of the expression, - namely: Unboxed Int -> Int, -the kind of the argument type is TYPE (Rep Int), and that needs -type-family reduction to determine the runtime representation. - -So we split the wrapper into the instantiating part (which is what -we really want) and everything else; see splitWrapper. This is -very disgusting. - -But it also improves the error message in an example like T13233_elab: - obscure :: (forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep) - (a :: TYPE rep1) (b :: TYPE rep2). - a -> b -> (# a, b #)) -> () - obscure _ = () - - quux = obscure (#,#) - -Around the (#,#) we'll get some type /abstractions/ wrapping some type -/instantiations/. In the representation polymorphism error message, -we really only want to report the instantiations. -Hence passing (mkHsWrap w_inner e) to checkLevPolyArgs. - - -Note [Checking representation-polymorphic data constructors] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Similarly, generated by a newtype data constructor, we might get this: - (/\(r :: RuntimeRep) (a :: TYPE r) \(x::a). K r a x) @LiftedRep Int 4 - -which we want to accept. See Note [Typechecking data constructors] in -GHC.Tc.Gen.Head. - -Because we want to accept this, we switch off Lint's -representation polymorphism checks when Lint checks the output of the -desugarer; see the lf_check_levity_poly flag in -GHC.Core.Lint.lintCoreBindings. - -We can get this situation both for representation-polymorphic -newtype constructors (T18481), and for representation-polymorphic -algebraic data types, e.g (T18481a) - type T :: TYPE (BoxedRep r) -> TYPE (BoxedRep r) - data T a = MkT Int - - f :: T Bool - f = MkT @Lifted @Bool 42 -} ------------------------------ dsHsWrapped :: HsExpr GhcTc -> DsM CoreExpr --- Looks for a function 'f' wrapped in type applications (HsAppType) --- or wrappers (HsWrap), and checks that any hasNoBinding function --- is not representation-polymorphic, *after* instantiation with those wrappers dsHsWrapped orig_hs_expr = go idHsWrapper orig_hs_expr where @@ -1247,31 +1109,18 @@ dsHsWrapped orig_hs_expr go wrap (HsAppType ty (L _ hs_e) _) = go (wrap <.> WpTyApp ty) hs_e - go wrap e@(XExpr (ConLikeTc con tvs tys)) - = do { let (w_outer, w_inner) = splitWrapper wrap - ; w_outer' <- dsHsWrapper w_outer - ; w_inner' <- dsHsWrapper w_inner - ; ds_con <- dsConLike con tvs tys - ; let inst_e = w_inner' ds_con - inst_ty = exprType inst_e - ; checkLevPolyArgs (mkHsWrap w_inner e) inst_ty - ; return (w_outer' inst_e) } - - go wrap e@(HsVar _ (L _ var)) + go wrap (HsVar _ (L _ var)) | var `hasKey` withDictKey = do { wrap' <- dsHsWrapper wrap ; ds_withDict (exprType (wrap' (varToCoreExpr var))) } | otherwise - = do { let (w_outer, w_inner) = splitWrapper wrap - ; w_outer' <- dsHsWrapper w_outer - ; w_inner' <- dsHsWrapper w_inner - ; let inst_e = w_inner' (varToCoreExpr var) - inst_ty = exprType inst_e - ; checkLevPolyFunction (mkHsWrap w_inner e) var inst_ty + = do { wrap' <- dsHsWrapper wrap + ; let expr = wrap' (varToCoreExpr var) + ty = exprType expr ; dflags <- getDynFlags - ; warnAboutIdentities dflags var inst_ty - ; return (w_outer' inst_e) } + ; warnAboutIdentities dflags var ty + ; return expr } go wrap hs_e = do { wrap' <- dsHsWrapper wrap @@ -1279,32 +1128,6 @@ dsHsWrapped orig_hs_expr do { e <- dsExpr hs_e ; return (wrap' e) } } -splitWrapper :: HsWrapper -> (HsWrapper, HsWrapper) --- Split a wrapper w into (outer_wrap <.> inner_wrap), where --- inner_wrap does instantiation (type and evidence application) --- and outer_wrap is everything else, such as a final cast --- See Note [Nasty wrinkle in representation-polymorphic function check] -splitWrapper wrap - = go WpHole wrap - where - go :: HsWrapper -> HsWrapper -> (HsWrapper, HsWrapper) - -- If (go w1 w2) = (w3,w4) then - -- - w1 <.> w2 = w3 <.> w4 - -- - w4 does instantiation only ("instantiator" below) - -- 'go' mainly dispatches on w2, using w1 as a work-list - -- onto which it pushes stuff in w2 to come back to later - go WpHole WpHole = (WpHole,WpHole) - go w WpHole = splitWrapper w - go w1 (w2 `WpCompose` w3) = go (w1 <.> w2) w3 - - go w1 w2 | instantiator w2 = liftSnd (<.> w2) (splitWrapper w1) - | otherwise = (w1 <.> w2, WpHole) - - instantiator (WpTyApp {}) = True - instantiator (WpEvApp {}) = True - instantiator _ = False - - -- See Note [withDict] ds_withDict :: Type -> DsM CoreExpr ds_withDict wrapped_ty @@ -1456,30 +1279,3 @@ Some further observations about `withDict`: error, which is trickier to do with the way that GHC.Core.Opt.ConstantFold is set up. -} - --- | Takes a (pretty-printed) expression, a function, and its --- instantiated type. If the function is a hasNoBinding op, and the --- type has representation-polymorphic arguments, issue an error. --- Note [Checking for representation-polymorphic functions] -checkLevPolyFunction :: Outputable e => e -> Id -> Type -> DsM () -checkLevPolyFunction orig_hs_expr var ty - | hasNoBinding var - = checkLevPolyArgs orig_hs_expr ty - | otherwise - = return () - -checkLevPolyArgs :: Outputable e => e -> Type -> DsM () --- Check that there are no representation-polymorphic arguments in --- the supplied type --- E.g. Given (forall a. t1 -> t2 -> blah), ensure that t1,t2 --- are not representation-polymorhic --- --- Pass orig_hs_expr, so that the user can see entire thing --- Note [Checking for representation-polymorphic functions] -checkLevPolyArgs orig_hs_expr ty - | let (binders, _) = splitPiTys ty - arg_tys = mapMaybe binderRelevantType_maybe binders - bad_tys = filter isTypeLevPoly arg_tys - , not (null bad_tys) - = diagnosticDs $ DsCannotUseFunWithPolyArgs orig_hs_expr ty bad_tys - | otherwise = return () diff --git a/compiler/GHC/HsToCore/Expr.hs-boot b/compiler/GHC/HsToCore/Expr.hs-boot index ce438dceb9..720f8fa8fc 100644 --- a/compiler/GHC/HsToCore/Expr.hs-boot +++ b/compiler/GHC/HsToCore/Expr.hs-boot @@ -5,6 +5,6 @@ import GHC.Core ( CoreExpr ) import GHC.Hs.Extension ( GhcTc) dsExpr :: HsExpr GhcTc -> DsM CoreExpr -dsLExpr, dsLExprNoLP :: LHsExpr GhcTc -> DsM CoreExpr +dsLExpr :: LHsExpr GhcTc -> DsM CoreExpr dsSyntaxExpr :: SyntaxExpr GhcTc -> [CoreExpr] -> DsM CoreExpr dsLocalBinds :: HsLocalBinds GhcTc -> CoreExpr -> DsM CoreExpr diff --git a/compiler/GHC/HsToCore/ListComp.hs b/compiler/GHC/HsToCore/ListComp.hs index 3f649903a1..12a40e6c90 100644 --- a/compiler/GHC/HsToCore/ListComp.hs +++ b/compiler/GHC/HsToCore/ListComp.hs @@ -13,10 +13,9 @@ module GHC.HsToCore.ListComp ( dsListComp, dsMonadComp ) where import GHC.Prelude -import {-# SOURCE #-} GHC.HsToCore.Expr ( dsExpr, dsLExpr, dsLExprNoLP, dsLocalBinds, dsSyntaxExpr ) +import {-# SOURCE #-} GHC.HsToCore.Expr ( dsExpr, dsLExpr, dsLocalBinds, dsSyntaxExpr ) import GHC.Hs -import GHC.Tc.Errors.Types ( LevityCheckProvenance(..) ) import GHC.Hs.Syn.Type import GHC.Core import GHC.Core.Make @@ -139,8 +138,6 @@ dsTransStmt (TransStmt { trS_form = form, trS_stmts = stmts, trS_bndrs = binderM , Var unzip_fn' , inner_list_expr' ] - dsNoLevPoly (tcFunResultTyN (length usingArgs') (exprType usingExpr')) (LevityCheckInFunUse using) - -- Build a pattern that ensures the consumer binds into the NEW binders, -- which hold lists rather than single values let pat = mkBigLHsVarPatTupId to_bndrs -- NB: no '! @@ -240,7 +237,7 @@ deListComp (stmt@(TransStmt {}) : quals) list = do deBindComp pat inner_list_expr quals list deListComp (BindStmt _ pat list1 : quals) core_list2 = do -- rule A' above - core_list1 <- dsLExprNoLP list1 + core_list1 <- dsLExpr list1 deBindComp pat core_list1 quals core_list2 deListComp (ParStmt _ stmtss_w_bndrs _ _ : quals) list @@ -328,7 +325,7 @@ dfListComp _ _ [] = panic "dfListComp" dfListComp c_id n_id (LastStmt _ body _ _ : quals) = assert (null quals) $ - do { core_body <- dsLExprNoLP body + do { core_body <- dsLExpr body ; return (mkApps (Var c_id) [core_body, Var n_id]) } -- Non-last: must be a guard @@ -549,7 +546,7 @@ dsMcStmt (TransStmt { trS_stmts = stmts, trS_bndrs = bndrs ; let tup_n_ty' = mkBigCoreVarTupTy to_bndrs ; body <- dsMcStmts stmts_rest - ; n_tup_var' <- newSysLocalDsNoLP Many n_tup_ty' + ; n_tup_var' <- newSysLocalDs Many n_tup_ty' ; tup_n_var' <- newSysLocalDs Many tup_n_ty' ; tup_n_expr' <- mkMcUnzipM form fmap_op n_tup_var' from_bndr_tys ; us <- newUniqueSupply diff --git a/compiler/GHC/HsToCore/Match.hs b/compiler/GHC/HsToCore/Match.hs index 67a478907c..a4cdb78f6d 100644 --- a/compiler/GHC/HsToCore/Match.hs +++ b/compiler/GHC/HsToCore/Match.hs @@ -750,7 +750,7 @@ matchWrapper ctxt mb_scr (MG { mg_alts = L _ matches ; locn <- getSrcSpanDs ; new_vars <- case matches of - [] -> newSysLocalsDsNoLP arg_tys + [] -> newSysLocalsDs arg_tys (m:_) -> selectMatchVars (zipWithEqual "matchWrapper" (\a b -> (scaledMult a, unLoc b)) @@ -1117,7 +1117,7 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2 -- equating different ways of writing a coercion) wrap WpHole WpHole = True wrap (WpCompose w1 w2) (WpCompose w1' w2') = wrap w1 w1' && wrap w2 w2' - wrap (WpFun w1 w2 _ _) (WpFun w1' w2' _ _) = wrap w1 w1' && wrap w2 w2' + wrap (WpFun w1 w2 _) (WpFun w1' w2' _) = wrap w1 w1' && wrap w2 w2' wrap (WpCast co) (WpCast co') = co `eqCoercion` co' wrap (WpEvApp et1) (WpEvApp et2) = et1 `ev_term` et2 wrap (WpTyApp t) (WpTyApp t') = eqType t t' diff --git a/compiler/GHC/HsToCore/Match/Constructor.hs b/compiler/GHC/HsToCore/Match/Constructor.hs index 303ca416d2..1e56808278 100644 --- a/compiler/GHC/HsToCore/Match/Constructor.hs +++ b/compiler/GHC/HsToCore/Match/Constructor.hs @@ -245,10 +245,11 @@ same_fields flds1 flds2 ----------------- selectConMatchVars :: [Scaled Type] -> ConArgPats -> DsM [Id] -selectConMatchVars arg_tys con = case con of - (RecCon {}) -> newSysLocalsDsNoLP arg_tys - (PrefixCon _ ps) -> selectMatchVars (zipMults arg_tys ps) - (InfixCon p1 p2) -> selectMatchVars (zipMults arg_tys [p1, p2]) +selectConMatchVars arg_tys con + = case con of + RecCon {} -> newSysLocalsDs arg_tys + PrefixCon _ ps -> selectMatchVars (zipMults arg_tys ps) + InfixCon p1 p2 -> selectMatchVars (zipMults arg_tys [p1, p2]) where zipMults = zipWithEqual "selectConMatchVar" (\a b -> (scaledMult a, unLoc b)) diff --git a/compiler/GHC/HsToCore/Monad.hs b/compiler/GHC/HsToCore/Monad.hs index 84a9e9a9e5..9211b52fd7 100644 --- a/compiler/GHC/HsToCore/Monad.hs +++ b/compiler/GHC/HsToCore/Monad.hs @@ -19,8 +19,8 @@ module GHC.HsToCore.Monad ( foldlM, foldrM, whenGOptM, unsetGOptM, unsetWOptM, xoptM, Applicative(..),(<$>), - duplicateLocalDs, newSysLocalDsNoLP, newSysLocalDs, - newSysLocalsDsNoLP, newSysLocalsDs, newUniqueId, + duplicateLocalDs, newSysLocalDs, + newSysLocalsDs, newUniqueId, newFailLocalDs, newPredVarDs, getSrcSpanDs, putSrcSpanDs, putSrcSpanDsA, mkPrintUnqualifiedDs, @@ -42,15 +42,11 @@ module GHC.HsToCore.Monad ( -- Warnings and errors DsWarning, diagnosticDs, errDsCoreExpr, failWithDs, failDs, discardWarningsDs, - askNoErrsDs, -- Data types DsMatchContext(..), EquationInfo(..), MatchResult (..), runMatchResult, DsWrapper, idDsWrapper, - -- Representation polymorphism - dsNoLevPoly, dsNoLevPolyExpr, - -- Trace injection pprRuntimeTrace ) where @@ -71,7 +67,7 @@ import GHC.HsToCore.Pmc.Solver.Types (Nablas, initNablas) import GHC.Core.FamInstEnv import GHC.Core import GHC.Core.Make ( unitExpr ) -import GHC.Core.Utils ( exprType, isExprLevPoly ) +import GHC.Core.Utils ( exprType ) import GHC.Core.DataCon import GHC.Core.ConLike import GHC.Core.TyCon @@ -80,9 +76,7 @@ import GHC.Core.Multiplicity import GHC.IfaceToCore -import GHC.Tc.Errors.Types ( LevityCheckProvenance(..) ) import GHC.Tc.Utils.Monad -import GHC.Tc.Utils.TcMType ( checkForLevPolyX ) import GHC.Builtin.Names @@ -371,56 +365,11 @@ grab one or more names. @newLocalDs@ isn't exported---exported functions are defined with it. The difference in name-strings makes it easier to read debugging output. -Note [Representation polymorphism checking] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -According to the "Levity Polymorphism" paper (PLDI '17), -representation polymorphism is forbidden in precisely two places: -in the type of a bound term-level argument, and in the type of an argument -to a function. -Note that the paper doesn't distinguish levity polymorphism, such as - \(v::Levity). \(a::TYPE (BoxedRep v)). \(x::a). expr -from the more general representation polymorphism, as the BoxedRep -constructor of RuntimeRep didn't exist at the time. - -The paper explains the restrictions more fully, but briefly: -expressions in these contexts need to be stored in registers, and it's -hard (read: impossible) to store something that's representation-polymorphic. - -We cannot check for bad representation polymorphism conveniently -in the type checker, because we can't tell, a priori, which -representation metavariables will be solved. -At one point, I (Richard) thought we could check in the zonker, but it's hard -to know where precisely are the abstracted variables and the arguments. So -we check in the desugarer, the only place where we can see the Core code and -still report respectable syntax to the user. This covers the vast majority -of cases; see calls to GHC.HsToCore.Monad.dsNoLevPoly and friends. - -Representation polymorphism is also prohibited in the types of binders, and the -desugarer checks for this in GHC-generated Ids. (The zonker handles -the user-writted ids in zonkIdBndr.) This is done in newSysLocalDsNoLP. -The newSysLocalDs variant is used in the vast majority of cases where -the binder is obviously not representation-polymorphic, omitting the check. -It would be nice to ASSERT that there is no representation polymorphism here, -but we can't, because of the fixM in GHC.HsToCore.Arrows. It's all OK, though: -Core Lint will catch an error here. - -However, the desugarer is the wrong place for certain checks. In particular, -the desugarer can't report a sensible error message if an HsWrapper is malformed. -After all, GHC itself produced the HsWrapper. So we store some message text -in the appropriate HsWrappers (e.g. WpFun) that we can print out in the -desugarer. - -There are a few more checks in places where Core is generated outside the -desugarer. For example, in datatype and class declarations, where -representation polymorphism is checked for during validity checking. -It would be nice to have one central place for all this, but that doesn't -seem possible while still reporting nice error messages. - -} -- Make a new Id with the same print name, but different type, and new unique newUniqueId :: Id -> Mult -> Type -> DsM Id -newUniqueId id = mk_local (occNameFS (nameOccName (idName id))) +newUniqueId id = mkSysLocalOrCoVarM (occNameFS (nameOccName (idName id))) duplicateLocalDs :: Id -> DsM Id duplicateLocalDs old_local @@ -431,27 +380,13 @@ newPredVarDs :: PredType -> DsM Var newPredVarDs = mkSysLocalOrCoVarM (fsLit "ds") Many -- like newSysLocalDs, but we allow covars -newSysLocalDsNoLP, newSysLocalDs, newFailLocalDs :: Mult -> Type -> DsM Id -newSysLocalDsNoLP = mk_local (fsLit "ds") - --- this variant should be used when the caller can be sure that the variable type --- is not representation-polymorphic. It is necessary when the type --- is knot-tied because of the fixM used in GHC.HsToCore.Arrows. --- See Note [Representation polymorphism checking] +newSysLocalDs, newFailLocalDs :: Mult -> Type -> DsM Id newSysLocalDs = mkSysLocalM (fsLit "ds") newFailLocalDs = mkSysLocalM (fsLit "fail") - -- the fail variable is used only in a situation where we can tell that - -- representation polymorphism is impossible. -newSysLocalsDsNoLP, newSysLocalsDs :: [Scaled Type] -> DsM [Id] -newSysLocalsDsNoLP = mapM (\(Scaled w t) -> newSysLocalDsNoLP w t) +newSysLocalsDs :: [Scaled Type] -> DsM [Id] newSysLocalsDs = mapM (\(Scaled w t) -> newSysLocalDs w t) -mk_local :: FastString -> Mult -> Type -> DsM Id -mk_local fs w ty = do { dsNoLevPoly ty LevityCheckInVarType -- could improve the msg with another - -- parameter indicating context - ; mkSysLocalOrCoVarM fs w ty } - {- We can also reach out and either set/grab location information from the @SrcSpan@ being carried around. @@ -508,36 +443,6 @@ failWithDs msg failDs :: DsM a failDs = failM --- (askNoErrsDs m) runs m --- If m fails, --- then (askNoErrsDs m) fails --- If m succeeds with result r, --- then (askNoErrsDs m) succeeds with result (r, b), --- where b is True iff m generated no errors --- Regardless of success or failure, --- propagate any errors/warnings generated by m --- --- c.f. GHC.Tc.Utils.Monad.askNoErrs -askNoErrsDs :: DsM a -> DsM (a, Bool) -askNoErrsDs thing_inside - = do { errs_var <- newMutVar emptyMessages - ; env <- getGblEnv - ; mb_res <- tryM $ -- Be careful to catch exceptions - -- so that we propagate errors correctly - -- (#13642) - setGblEnv (env { ds_msgs = errs_var }) $ - thing_inside - - -- Propagate errors - ; msgs <- readMutVar errs_var - ; updMutVar (ds_msgs env) (unionMessages msgs) - - -- And return - ; case mb_res of - Left _ -> failM - Right res -> do { let errs_found = errorsFound msgs - ; return (res, not errs_found) } } - mkPrintUnqualifiedDs :: DsM PrintUnqualified mkPrintUnqualifiedDs = ds_unqual <$> getGblEnv @@ -603,20 +508,6 @@ discardWarningsDs thing_inside ; return result } --- | Fail with an error message if the type is representation-polymorphic. -dsNoLevPoly :: Type -> LevityCheckProvenance -> DsM () --- See Note [Representation polymorphism checking] -dsNoLevPoly ty provenance = - checkForLevPolyX (\ty -> diagnosticDs . DsLevityPolyInType ty) provenance ty - --- | Check an expression for representation polymorphism, failing if it is --- representation-polymorphic. -dsNoLevPolyExpr :: CoreExpr -> LevityExprProvenance -> DsM () --- See Note [Representation polymorphism checking] -dsNoLevPolyExpr e provenance - | isExprLevPoly e = diagnosticDs (DsLevityPolyInExpr e provenance) - | otherwise = return () - -- | Inject a trace message into the compiled program. Whereas -- pprTrace prints out information *while compiling*, pprRuntimeTrace -- captures that information and causes it to be printed *at runtime* diff --git a/compiler/GHC/HsToCore/Utils.hs b/compiler/GHC/HsToCore/Utils.hs index 8572a23c39..2ea1bb3cbe 100644 --- a/compiler/GHC/HsToCore/Utils.hs +++ b/compiler/GHC/HsToCore/Utils.hs @@ -30,7 +30,7 @@ module GHC.HsToCore.Utils ( wrapBind, wrapBinds, mkErrorAppDs, mkCoreAppDs, mkCoreAppsDs, mkCastDs, - mkFailExpr, dsWhenNoErrs, + mkFailExpr, seqVar, @@ -132,10 +132,10 @@ selectMatchVars ps = mapM (uncurry selectMatchVar) ps selectMatchVar :: Mult -> Pat GhcTc -> DsM Id -- Postcondition: the returned Id has an Internal Name -selectMatchVar w (BangPat _ pat) = selectMatchVar w (unLoc pat) -selectMatchVar w (LazyPat _ pat) = selectMatchVar w (unLoc pat) +selectMatchVar w (BangPat _ pat) = selectMatchVar w (unLoc pat) +selectMatchVar w (LazyPat _ pat) = selectMatchVar w (unLoc pat) selectMatchVar w (ParPat _ _ pat _) = selectMatchVar w (unLoc pat) -selectMatchVar _w (VarPat _ var) = return (localiseId (unLoc var)) +selectMatchVar _w (VarPat _ var) = return (localiseId (unLoc var)) -- Note [Localise pattern binders] -- -- Remark: when the pattern is a variable (or @@ -144,7 +144,7 @@ selectMatchVar _w (VarPat _ var) = return (localiseId (unLoc var)) -- itself. It's easier to pull it from the -- variable, so we ignore the multiplicity. selectMatchVar _w (AsPat _ var _) = assert (isManyDataConTy _w ) (return (unLoc var)) -selectMatchVar w other_pat = newSysLocalDsNoLP w (hsPatType other_pat) +selectMatchVar w other_pat = newSysLocalDs w (hsPatType other_pat) {- Note [Localise pattern binders] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -739,7 +739,7 @@ mkSelectorBinds ticks pat val_expr | is_flat_prod_lpat pat' -- Special case (B) = do { let pat_ty = hsLPatType pat' - ; val_var <- newSysLocalDsNoLP Many pat_ty + ; val_var <- newSysLocalDs Many pat_ty ; let mk_bind tick bndr_var -- (mk_bind sv bv) generates bv = case sv of { pat -> bv } @@ -982,69 +982,6 @@ mk_fail_msg dflags ctx pat = showPpr dflags $ text "Pattern match failure in" <+> pprHsDoFlavour ctx <+> text "at" <+> ppr (getLocA pat) -{- Note [Desugaring representation-polymorphic applications] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -To desugar a function application - -> HsApp _ f e :: HsExpr GhcTc - -into Core, we need to know whether the argument e is lifted or unlifted, -in order to respect the let/app invariant. - (See Note [Core let/app invariant] in GHC.Core) - -This causes a problem when e is representation-polymorphic, as we aren't able -to determine whether to build a Core application - -> f_desugared e_desugared - -or a strict binding: - -> case e_desugared of { x -> f_desugared x } - -See GHC.Core.Make.mkValApp, which will call isUnliftedType, which panics -on a representation-polymorphic type. - -These representation-polymorphic applications are disallowed in source Haskell, -but we might want to continue desugaring as much as possible instead of -aborting as soon as we see such a problematic function application. - -When desugaring an expression which might have problems (such as disallowed -representation polymorphism as above), we check for errors first, and then: - - - if no problems were detected, desugar normally, - - if errors were found, we want to avoid desugaring, so we instead return - a runtime error Core expression which has the right type. - -This is what the function dsWhenNoErrs achieves: - -> dsWhenNoErrs result_ty thing_inside mk_expr - -We run thing_inside to check for errors. If there are no errors, we apply -mk_expr to desugar; otherwise, we construct a runtime error at type result_ty. - -Note that result_ty is only used when there is an error, and isn't inspected -otherwise; this means it's OK to pass something that can be a bit expensive -to compute. - -See #12709 for an example of why this machinery is necessary. -See also #14765 and #18149 for why it is important to return an expression -that has the proper type in case of an error. --} - --- | Runs the thing_inside. If there are no errors, use the provided --- function to construct a Core expression, and return it. --- Otherwise, return a runtime error, of the given type. --- This is useful for doing a bunch of representation polymorphism checks --- and then avoiding making a Core App. --- See Note [Desugaring representation-polymorphic applications] -dsWhenNoErrs :: Type -> DsM a -> (a -> CoreExpr) -> DsM CoreExpr -dsWhenNoErrs result_ty thing_inside mk_expr - = do { (result, no_errs) <- askNoErrsDs thing_inside - ; if no_errs - then return $ mk_expr result - else mkErrorAppDs rUNTIME_ERROR_ID result_ty - (text "dsWhenNoErrs found errors") } - {- ********************************************************************* * * Ticks diff --git a/compiler/GHC/Iface/Ext/Ast.hs b/compiler/GHC/Iface/Ext/Ast.hs index 58047e531f..fbeaa8ca3a 100644 --- a/compiler/GHC/Iface/Ext/Ast.hs +++ b/compiler/GHC/Iface/Ext/Ast.hs @@ -680,7 +680,7 @@ instance ToHie (LocatedA HsWrapper) where (WpLet bs) -> toHie $ EvBindContext (mkScopeA osp) (getRealSpanA osp) (L osp bs) (WpCompose a b) -> concatM $ [toHie (L osp a), toHie (L osp b)] - (WpFun a b _ _) -> concatM $ + (WpFun a b _) -> concatM $ [toHie (L osp a), toHie (L osp b)] (WpEvLam a) -> toHie $ C (EvidenceVarBind EvWrapperBind (mkScopeA osp) (getRealSpanA osp)) diff --git a/compiler/GHC/Iface/Syntax.hs b/compiler/GHC/Iface/Syntax.hs index b2aaad5e23..39f0bd5336 100644 --- a/compiler/GHC/Iface/Syntax.hs +++ b/compiler/GHC/Iface/Syntax.hs @@ -230,7 +230,7 @@ data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars :: [IfaceTvBndr] -- See Note [Storing compatibility] in GHC.Core.Coercion.Axiom data IfaceConDecls - = IfAbstractTyCon -- c.f TyCon.AbstractTyCon + = IfAbstractTyCon -- c.f TyCon.AbstractTyCon | IfDataTyCon [IfaceConDecl] -- Data type decls | IfNewTyCon IfaceConDecl -- Newtype decls @@ -375,7 +375,7 @@ data IfaceUnfolding -- We only serialise the IdDetails of top-level Ids, and even then -- we only need a very limited selection. Notably, none of the --- implicit ones are needed here, because they are not put it +-- implicit ones are needed here, because they are not put in -- interface files data IfaceIdDetails @@ -452,9 +452,9 @@ See [https://gitlab.haskell.org/ghc/ghc/wikis/commentary/compiler/recompilation- -} visibleIfConDecls :: IfaceConDecls -> [IfaceConDecl] -visibleIfConDecls IfAbstractTyCon = [] -visibleIfConDecls (IfDataTyCon cs) = cs -visibleIfConDecls (IfNewTyCon c) = [c] +visibleIfConDecls (IfAbstractTyCon {}) = [] +visibleIfConDecls (IfDataTyCon cs) = cs +visibleIfConDecls (IfNewTyCon c) = [c] ifaceDeclImplicitBndrs :: IfaceDecl -> [OccName] -- *Excludes* the 'main' name, but *includes* the implicitly-bound names @@ -471,9 +471,9 @@ ifaceDeclImplicitBndrs :: IfaceDecl -> [OccName] ifaceDeclImplicitBndrs (IfaceData {ifName = tc_name, ifCons = cons }) = case cons of - IfAbstractTyCon -> [] - IfNewTyCon cd -> mkNewTyCoOcc (occName tc_name) : ifaceConDeclImplicitBndrs cd - IfDataTyCon cds -> concatMap ifaceConDeclImplicitBndrs cds + IfAbstractTyCon {} -> [] + IfNewTyCon cd -> mkNewTyCoOcc (occName tc_name) : ifaceConDeclImplicitBndrs cd + IfDataTyCon cds -> concatMap ifaceConDeclImplicitBndrs cds ifaceDeclImplicitBndrs (IfaceClass { ifBody = IfAbstractClass }) = [] diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs index 686a519a0c..0250078b62 100644 --- a/compiler/GHC/IfaceToCore.hs +++ b/compiler/GHC/IfaceToCore.hs @@ -238,7 +238,7 @@ typecheckIface iface -- | Returns true if an 'IfaceDecl' is for @data T@ (an abstract data type) isAbstractIfaceDecl :: IfaceDecl -> Bool -isAbstractIfaceDecl IfaceData{ ifCons = IfAbstractTyCon } = True +isAbstractIfaceDecl IfaceData{ ifCons = IfAbstractTyCon {} } = True isAbstractIfaceDecl IfaceClass{ ifBody = IfAbstractClass } = True isAbstractIfaceDecl IfaceFamily{ ifFamFlav = IfaceAbstractClosedSynFamilyTyCon } = True isAbstractIfaceDecl _ = False @@ -1035,11 +1035,17 @@ tc_ax_branch prev_branches tcIfaceDataCons :: Name -> TyCon -> [TyConBinder] -> IfaceConDecls -> IfL AlgTyConRhs tcIfaceDataCons tycon_name tycon tc_tybinders if_cons = case if_cons of - IfAbstractTyCon -> return AbstractTyCon - IfDataTyCon cons -> do { data_cons <- mapM tc_con_decl cons - ; return (mkDataTyConRhs data_cons) } - IfNewTyCon con -> do { data_con <- tc_con_decl con - ; mkNewTyConRhs tycon_name tycon data_con } + IfAbstractTyCon + -> return AbstractTyCon + IfDataTyCon cons + -> do { data_cons <- mapM tc_con_decl cons + ; return $ + mkLevPolyDataTyConRhs + (isFixedRuntimeRepKind $ tyConResKind tycon) + data_cons } + IfNewTyCon con + -> do { data_con <- tc_con_decl con + ; mkNewTyConRhs tycon_name tycon data_con } where univ_tvs :: [TyVar] univ_tvs = binderVars tc_tybinders @@ -1661,7 +1667,7 @@ tcIdInfo ignore_prags toplvl name ty info = do tcPrag info (HsDmdSig str) = return (info `setDmdSigInfo` str) tcPrag info (HsCprSig cpr) = return (info `setCprSigInfo` cpr) tcPrag info (HsInline prag) = return (info `setInlinePragInfo` prag) - tcPrag info HsLevity = return (info `setNeverLevPoly` ty) + tcPrag info HsLevity = return (info `setNeverRepPoly` ty) tcPrag info (HsLFInfo lf_info) = do lf_info <- tcLFInfo lf_info return (info `setLFInfo` lf_info) @@ -1909,13 +1915,15 @@ tcIfaceCoAxiom name = do { thing <- tcIfaceImplicit name tcIfaceCoAxiomRule :: IfLclName -> IfL CoAxiomRule --- Unlike CoAxioms, which arise form user 'type instance' declarations, --- there are a fixed set of CoAxiomRules, --- currently enumerated in typeNatCoAxiomRules +-- Unlike CoAxioms, which arise from user 'type instance' declarations, +-- there are a fixed set of CoAxiomRules: +-- - axioms for type-level literals (Nat and Symbol), +-- enumerated in typeNatCoAxiomRules tcIfaceCoAxiomRule n - = case lookupUFM typeNatCoAxiomRules n of - Just ax -> return ax - _ -> pprPanic "tcIfaceCoAxiomRule" (ppr n) + | Just ax <- lookupUFM typeNatCoAxiomRules n + = return ax + | otherwise + = pprPanic "tcIfaceCoAxiomRule" (ppr n) tcIfaceDataCon :: Name -> IfL DataCon tcIfaceDataCon name = do { thing <- tcIfaceGlobal name diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index f474c3383d..ff6525f24d 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -57,7 +57,8 @@ import GHC.Core.Predicate import GHC.Core.Type import GHC.Core.Coercion import GHC.Core.TyCo.Rep -import GHC.Core.TyCo.Ppr ( pprTyVars, pprWithExplicitKindsWhen, pprSourceTyCon, pprWithTYPE ) +import GHC.Core.TyCo.Ppr ( pprTyVars, pprWithExplicitKindsWhen, pprSourceTyCon + , pprWithTYPE ) import GHC.Core.Unify ( tcMatchTys ) import GHC.Core.InstEnv import GHC.Core.TyCon @@ -75,12 +76,14 @@ import GHC.Utils.FV ( fvVarList, unionFV ) import GHC.Data.Bag import GHC.Data.FastString import GHC.Utils.Trace (pprTraceUserWarning) -import GHC.Data.List.SetOps ( equivClasses ) +import GHC.Data.List.SetOps ( equivClasses, nubOrdBy ) import GHC.Data.Maybe import qualified GHC.Data.Strict as Strict import Control.Monad ( unless, when, foldM, forM_ ) import Data.Foldable ( toList ) +import Data.Functor ( (<&>) ) +import Data.Function ( on ) import Data.List ( partition, mapAccumL, sortBy, unfoldr ) -- import Data.Semigroup ( Semigroup ) import qualified Data.Semigroup as Semigroup @@ -564,7 +567,10 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics -- says to suppress ; let ctxt2 = ctxt { cec_suppress = cec_suppress ctxt || cec_suppress ctxt1 } ; (_, leftovers) <- tryReporters ctxt2 report2 cts1 - ; massertPpr (null leftovers) (ppr leftovers) + ; massertPpr (null leftovers) + (text "The following unsolved Wanted constraints \ + \have not been reported to the user:" + $$ ppr leftovers) -- All the Derived ones have been filtered out of simples -- by the constraint solver. This is ok; we don't want @@ -606,6 +612,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics -- report2: we suppress these if there are insolubles elsewhere in the tree report2 = [ ("Implicit params", is_ip, False, mkGroupReporter mkIPErr) , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr) + , ("FixedRuntimeRep", is_FRR, False, mkGroupReporter mkFRRErr) , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ] -- also checks to make sure the constraint isn't HoleBlockerReason @@ -615,7 +622,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics unblocked checker ct pred = checker ct pred -- rigid_nom_eq, rigid_nom_tv_eq, - is_dict, is_equality, is_ip, is_irred :: Ct -> Pred -> Bool + is_dict, is_equality, is_ip, is_FRR, is_irred :: Ct -> Pred -> Bool is_given_eq ct pred | EqPred {} <- pred = arisesFromGivens ct @@ -652,6 +659,12 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics is_ip _ (ClassPred cls _) = isIPClass cls is_ip _ _ = False + is_FRR ct (SpecialPred ConcretePrimPred _) + | FixedRuntimeRepOrigin {} <- ctOrigin ct + = True + is_FRR _ _ + = False + is_irred _ (IrredPred {}) = True is_irred _ _ = False @@ -928,9 +941,10 @@ suppressGroup mk_err ctxt cts -- See Note [No deferring for multiplicity errors] nonDeferrableOrigin :: CtOrigin -> Bool -nonDeferrableOrigin NonLinearPatternOrigin = True -nonDeferrableOrigin (UsageEnvironmentOf _) = True -nonDeferrableOrigin _ = False +nonDeferrableOrigin NonLinearPatternOrigin = True +nonDeferrableOrigin (UsageEnvironmentOf {}) = True +nonDeferrableOrigin (FixedRuntimeRepOrigin {}) = True +nonDeferrableOrigin _ = False maybeReportError :: ReportErrCtxt -> Ct -> Report -> TcM () maybeReportError ctxt ct report @@ -1428,6 +1442,53 @@ mkIPErr ctxt cts where (ct1:_) = cts +---------------- + +-- | Create a user-facing error message for unsolved @'Concrete#' ki@ +-- Wanted constraints arising from representation-polymorphism checks. +-- +-- See Note [Reporting representation-polymorphism errors] in GHC.Tc.Types.Origin. +mkFRRErr :: ReportErrCtxt -> [Ct] -> TcM Report +mkFRRErr ctxt cts + = do { -- Zonking/tidying. + ; origs <- + -- Zonk/tidy the 'CtOrigin's. + zonkTidyOrigins (cec_tidy ctxt) (map ctOrigin cts) + <&> + -- Then remove duplicates: only retain one 'CtOrigin' per representation-polymorphic type. + (nubOrdBy (nonDetCmpType `on` frr_type) . snd) + + -- Obtain all the errors we want to report (constraints with FixedRuntimeRep origin), + -- with the corresponding types: + -- ty1 :: TYPE rep1, ty2 :: TYPE rep2, ... + ; let tys = map frr_type origs + kis = map typeKind tys + + -- Assemble the error message: pair up each origin with the corresponding type, e.g. + -- • FixedRuntimeRep origin msg 1 ... + -- a :: TYPE r1 + -- • FixedRuntimeRep origin msg 2 ... + -- b :: TYPE r2 + + combine_origin_ty_ki :: CtOrigin -> Type -> Kind -> SDoc + combine_origin_ty_ki orig ty ki = + -- Add bullet points if there is more than one error. + (if length tys > 1 then (bullet <+>) else id) $ + vcat [pprArising orig <> colon + ,nest 2 $ ppr ty <+> dcolon <+> pprWithTYPE ki] + + msg :: SDoc + msg = vcat $ zipWith3 combine_origin_ty_ki origs tys kis + + ; return $ important msg } + where + + frr_type :: CtOrigin -> Type + frr_type (FixedRuntimeRepOrigin ty _) = ty + frr_type orig + = pprPanic "mkFRRErr: not a FixedRuntimeRep origin" + (text "origin =" <+> ppr orig) + {- Note [Constraints include ...] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2396,7 +2457,7 @@ Warn of loopy local equalities that were dropped. ************************************************************************ -} -mkDictErr :: ReportErrCtxt -> [Ct] -> TcM Report +mkDictErr :: HasDebugCallStack => ReportErrCtxt -> [Ct] -> TcM Report mkDictErr ctxt cts = assert (not (null cts)) $ do { inst_envs <- tcGetInstEnvs @@ -2430,7 +2491,7 @@ mkDictErr ctxt cts -- but we really only want to report the latter elim_superclasses cts = mkMinimalBySCs ctPred cts -mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult) +mk_dict_err :: HasCallStack => ReportErrCtxt -> (Ct, ClsInstLookupResult) -> TcM SDoc -- Report an overlap error if this class constraint results -- from an overlap (returning Left clas), otherwise return (Right pred) @@ -3035,7 +3096,7 @@ relevantBindings want_filtering ctxt ct -- enclosing *type* equality, because that's more useful for the programmer ; let extra_tvs = case tidy_orig of KindEqOrigin t1 t2 _ _ -> tyCoVarsOfTypes [t1,t2] - _ -> emptyVarSet + _ -> emptyVarSet ct_fvs = tyCoVarsOfCt ct `unionVarSet` extra_tvs -- Put a zonked, tidied CtOrigin into the Ct diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs index 1fa94e496a..e282d8fe8d 100644 --- a/compiler/GHC/Tc/Errors/Ppr.hs +++ b/compiler/GHC/Tc/Errors/Ppr.hs @@ -2,10 +2,8 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} -- instance Diagnostic TcRnMessage {-# LANGUAGE RecordWildCards #-} -module GHC.Tc.Errors.Ppr ( - formatLevPolyErr - , pprLevityPolyInType - ) where +module GHC.Tc.Errors.Ppr ( pprTypeDoesNotHaveFixedRuntimeRep ) + where import GHC.Prelude @@ -19,7 +17,7 @@ import GHC.Core.DataCon (DataCon) import GHC.Core.FamInstEnv (famInstAxiom) import GHC.Core.InstEnv import GHC.Core.TyCon (isNewTyCon) -import GHC.Core.TyCo.Ppr (pprKind, pprParendType, pprType, pprWithTYPE, +import GHC.Core.TyCo.Ppr (pprKind, pprParendType, pprType, pprWithExplicitKindsWhen, pprTheta, pprClassPred, pprTypeApp, pprSourceTyCon) import GHC.Core.Type @@ -49,8 +47,8 @@ instance Diagnostic TcRnMessage where diagnosticMessage = \case TcRnUnknownMessage m -> diagnosticMessage m - TcLevityPolyInType ty prov (ErrInfo extra supplementary) - -> mkDecorated [pprLevityPolyInType ty prov, extra, supplementary] + TcRnTypeDoesNotHaveFixedRuntimeRep ty prov (ErrInfo extra supplementary) + -> mkDecorated [pprTypeDoesNotHaveFixedRuntimeRep ty prov, extra, supplementary] TcRnMessageWithInfo unit_state msg_with_info -> case msg_with_info of TcRnMessageDetailed err_info msg @@ -508,10 +506,22 @@ instance Diagnostic TcRnMessage where -> mkSimpleDecorated $ text "Proc patterns cannot use existential or GADT data constructors" + TcRnSpecialClassInst cls because_safeHaskell + -> mkSimpleDecorated $ + text "Class" <+> quotes (ppr $ className cls) + <+> text "does not support user-specified instances" + <> safeHaskell_msg + where + safeHaskell_msg + | because_safeHaskell + = text " when Safe Haskell is enabled." + | otherwise + = dot + diagnosticReason = \case TcRnUnknownMessage m -> diagnosticReason m - TcLevityPolyInType{} + TcRnTypeDoesNotHaveFixedRuntimeRep{} -> ErrorWithoutFlag TcRnMessageWithInfo _ msg_with_info -> case msg_with_info of @@ -721,11 +731,13 @@ instance Diagnostic TcRnMessage where -> ErrorWithoutFlag TcRnArrowProcGADTPattern -> ErrorWithoutFlag + TcRnSpecialClassInst {} + -> ErrorWithoutFlag diagnosticHints = \case TcRnUnknownMessage m -> diagnosticHints m - TcLevityPolyInType{} + TcRnTypeDoesNotHaveFixedRuntimeRep{} -> noHints TcRnMessageWithInfo _ msg_with_info -> case msg_with_info of @@ -929,6 +941,8 @@ instance Diagnostic TcRnMessage where -> noHints TcRnArrowProcGADTPattern -> noHints + TcRnSpecialClassInst {} + -> noHints deriveInstanceErrReasonHints :: Class -> UsingGeneralizedNewtypeDeriving @@ -1034,47 +1048,20 @@ dodgy_msg_insert tc = IEThingAll noAnn ii ii :: LIEWrappedName (IdP (GhcPass p)) ii = noLocA (IEName $ noLocA tc) -formatLevPolyErr :: Type -- representation-polymorphic type - -> SDoc -formatLevPolyErr ty - = hang (text "A representation-polymorphic type is not allowed here:") - 2 (vcat [ text "Type:" <+> pprWithTYPE tidy_ty - , text "Kind:" <+> pprWithTYPE tidy_ki ]) +pprTypeDoesNotHaveFixedRuntimeRep :: Type -> FixedRuntimeRepProvenance -> SDoc +pprTypeDoesNotHaveFixedRuntimeRep ty prov = + let what = pprFixedRuntimeRepProvenance prov + in text "The" <+> what <+> text "does not have a fixed runtime representation:" + $$ format_frr_err ty + +format_frr_err :: Type -- ^ the type which doesn't have a fixed runtime representation + -> SDoc +format_frr_err ty + = (bullet <+> ppr tidy_ty <+> dcolon <+> ppr tidy_ki) where (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty tidy_ki = tidyType tidy_env (tcTypeKind ty) -pprLevityPolyInType :: Type -> LevityCheckProvenance -> SDoc -pprLevityPolyInType ty prov = - let extra = case prov of - LevityCheckInBinder v - -> text "In the type of binder" <+> quotes (ppr v) - LevityCheckInVarType - -> text "When trying to create a variable of type:" <+> ppr ty - LevityCheckInWildcardPattern - -> text "In a wildcard pattern" - LevityCheckInUnboxedTuplePattern p - -> text "In the type of an element of an unboxed tuple pattern:" $$ ppr p - LevityCheckPatSynSig - -> empty - LevityCheckCmdStmt - -> empty -- I (Richard E, Dec '16) have no idea what to say here - LevityCheckMkCmdEnv id_var - -> text "In the result of the function" <+> quotes (ppr id_var) - LevityCheckDoCmd do_block - -> text "In the do-command:" <+> ppr do_block - LevityCheckDesugaringCmd cmd - -> text "When desugaring the command:" <+> ppr cmd - LevityCheckInCmd body - -> text "In the command:" <+> ppr body - LevityCheckInFunUse using - -> text "In the result of a" <+> quotes (text "using") <+> text "function:" <+> ppr using - LevityCheckInValidDataCon - -> empty - LevityCheckInValidClass - -> empty - in formatLevPolyErr ty $$ extra - pprField :: (FieldLabelString, TcType) -> SDoc pprField (f,ty) = ppr f <+> dcolon <+> ppr ty diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs index db0a6b0c33..10cc3524df 100644 --- a/compiler/GHC/Tc/Errors/Types.hs +++ b/compiler/GHC/Tc/Errors/Types.hs @@ -4,7 +4,8 @@ module GHC.Tc.Errors.Types ( TcRnMessage(..) , TcRnMessageDetailed(..) , ErrInfo(..) - , LevityCheckProvenance(..) + , FixedRuntimeRepProvenance(..) + , pprFixedRuntimeRepProvenance , ShadowedNameProvenance(..) , RecordFieldPart(..) , InjectivityErrReason(..) @@ -56,7 +57,7 @@ import GHC.Core.DataCon (DataCon) import GHC.Core.FamInstEnv (FamInst) import GHC.Core.InstEnv (ClsInst) import GHC.Core.TyCon (TyCon, TyConFlavour) -import GHC.Core.Type (Kind, Type, Var, ThetaType, PredType) +import GHC.Core.Type (Kind, Type, ThetaType, PredType) import GHC.Unit.State (UnitState) import GHC.Unit.Module.Name (ModuleName) import GHC.Types.Basic @@ -137,12 +138,21 @@ data TcRnMessage where -> !TcRnMessageDetailed -> TcRnMessage - {-| A levity polymorphism check happening during TcRn. + {-| A type which was expected to have a fixed runtime representation + does not have a fixed runtime representation. + + Example: + + data D (a :: TYPE r) = MkD a + + Test cases: T11724, T18534, + RepPolyPatSynArg, RepPolyPatSynUnliftedNewtype, + RepPolyPatSynRes, T20423 -} - TcLevityPolyInType :: !Type - -> !LevityCheckProvenance - -> !ErrInfo -- Extra info accumulated in the TcM monad - -> TcRnMessage + TcRnTypeDoesNotHaveFixedRuntimeRep :: !Type + -> !FixedRuntimeRepProvenance + -> !ErrInfo -- Extra info accumulated in the TcM monad + -> TcRnMessage {-| TcRnImplicitLift is a warning (controlled with -Wimplicit-lift) that occurs when a Template Haskell quote implicitly uses 'lift'. @@ -1249,6 +1259,21 @@ data TcRnMessage where rename/should_fail/RnStaticPointersFail03 -} TcRnStaticFormNotClosed :: Name -> NotClosedReason -> TcRnMessage + {-| TcRnSpecialClassInst is an error that occurs when a user + attempts to define an instance for a built-in typeclass such as + 'Coercible', 'Typeable', or 'KnownNat', outside of a signature file. + + Test cases: deriving/should_fail/T9687 + deriving/should_fail/T14916 + polykinds/T8132 + typecheck/should_fail/TcCoercibleFail2 + typecheck/should_fail/T12837 + typecheck/should_fail/T14390 + + -} + TcRnSpecialClassInst :: !Class + -> !Bool -- ^ Whether the error is due to Safe Haskell being enabled + -> TcRnMessage {-| TcRnUselessTypeable is a warning (controlled by -Wderiving-typeable) that occurs when trying to derive an instance of the 'Typeable' class. Deriving @@ -1400,21 +1425,32 @@ data ShadowedNameProvenance | ShadowedNameProvenanceGlobal [GlobalRdrElt] -- ^ The shadowed name is global, typically imported from elsewhere. --- | Where the levity checking for the input type originated -data LevityCheckProvenance - = LevityCheckInVarType - | LevityCheckInBinder !Var - | LevityCheckInWildcardPattern - | LevityCheckInUnboxedTuplePattern !(Pat GhcTc) - | LevityCheckPatSynSig - | LevityCheckCmdStmt - | LevityCheckMkCmdEnv !Var - | LevityCheckDoCmd !(HsCmd GhcTc) - | LevityCheckDesugaringCmd !(LHsCmd GhcTc) - | LevityCheckInCmd !(LHsCmd GhcTc) - | LevityCheckInFunUse !(LHsExpr GhcTc) - | LevityCheckInValidDataCon - | LevityCheckInValidClass +-- | In what context did we require a type to have a fixed runtime representation? +-- +-- Used by 'GHC.Tc.Utils.TcMType.checkTypeHasFixedRuntimeRep' for throwing +-- representation polymorphism errors when validity checking. +-- +-- See Note [Representation polymorphism checking] in GHC.Tc.Utils.Concrete +data FixedRuntimeRepProvenance + -- | Data constructor fields must have a fixed runtime representation. + -- + -- Tests: T11734, T18534. + = FixedRuntimeRepDataConField + + -- | Pattern synonym signature arguments must have a fixed runtime representation. + -- + -- Test: RepPolyPatSynArg. + | FixedRuntimeRepPatSynSigArg + + -- | Pattern synonym signature scrutinee must have a fixed runtime representation. + -- + -- Test: RepPolyPatSynRes. + | FixedRuntimeRepPatSynSigRes + +pprFixedRuntimeRepProvenance :: FixedRuntimeRepProvenance -> SDoc +pprFixedRuntimeRepProvenance FixedRuntimeRepDataConField = text "data constructor field" +pprFixedRuntimeRepProvenance FixedRuntimeRepPatSynSigArg = text "pattern synonym argument" +pprFixedRuntimeRepProvenance FixedRuntimeRepPatSynSigRes = text "pattern synonym scrutinee" -- | Why the particular injectivity error arose together with more information, -- if any. diff --git a/compiler/GHC/Tc/Gen/App.hs b/compiler/GHC/Tc/Gen/App.hs index cc0814cced..22454d1acc 100644 --- a/compiler/GHC/Tc/Gen/App.hs +++ b/compiler/GHC/Tc/Gen/App.hs @@ -2,6 +2,7 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow] @@ -21,13 +22,21 @@ module GHC.Tc.Gen.App import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr ) -import GHC.Builtin.Types (multiplicityTy) +import GHC.Types.Basic ( Arity ) +import GHC.Types.Id ( idArity, idName, hasNoBinding ) +import GHC.Types.Name ( isWiredInName ) +import GHC.Types.Var +import GHC.Builtin.Types ( multiplicityTy ) +import GHC.Core.ConLike ( ConLike(..) ) +import GHC.Core.DataCon ( dataConRepArity + , isNewDataCon, isUnboxedSumDataCon, isUnboxedTupleDataCon ) import GHC.Tc.Gen.Head import GHC.Hs import GHC.Tc.Errors.Types import GHC.Tc.Utils.Monad import GHC.Tc.Utils.Unify import GHC.Tc.Utils.Instantiate +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep ) import GHC.Tc.Instance.Family ( tcGetFamInstEnvs, tcLookupDataFamInst_maybe ) import GHC.Tc.Gen.HsType import GHC.Tc.Utils.TcMType @@ -317,6 +326,22 @@ tcApp rn_expr exp_res_ty ; do_ql <- wantQuickLook rn_fun ; (delta, inst_args, app_res_rho) <- tcInstFun do_ql True fun fun_sigma rn_args + -- Check for representation polymorphism in the case that + -- the head of the application is a primop or data constructor + -- which has argument types that are representation-polymorphic. + -- This amounts to checking that the leftover argument types, + -- up until the arity, are not representation-polymorphic, + -- so that we can perform eta-expansion later without introducing + -- representation-polymorphic binders. + -- + -- See Note [Checking for representation-polymorphic built-ins] + ; traceTc "tcApp FRR" $ + vcat + [ text "tc_fun =" <+> ppr tc_fun + , text "inst_args =" <+> ppr inst_args + , text "app_res_rho =" <+> ppr app_res_rho ] + ; hasFixedRuntimeRep_remainingValArgs inst_args app_res_rho tc_fun + -- Quick look at result ; app_res_rho <- if do_ql then quickLookResultType delta app_res_rho exp_res_ty @@ -353,14 +378,221 @@ tcApp rn_expr exp_res_ty -- Typecheck the value arguments ; tc_args <- tcValArgs do_ql inst_args - -- Reconstruct, with special case for tagToEnum# - ; tc_expr <- if isTagToEnum rn_fun - then tcTagToEnum tc_fun fun_ctxt tc_args app_res_rho - else return (rebuildHsApps tc_fun fun_ctxt tc_args) + -- Reconstruct, with a special cases for tagToEnum#. + ; tc_expr <- + if isTagToEnum rn_fun + then tcTagToEnum tc_fun fun_ctxt tc_args app_res_rho + else do return (rebuildHsApps tc_fun fun_ctxt tc_args) -- Wrap the result ; return (mkHsWrapCo res_co tc_expr) } +{- +Note [Checking for representation-polymorphic built-ins] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We cannot have representation-polymorphic or levity-polymorphic +function arguments. See Note [Representation polymorphism invariants] +in GHC.Core. That is checked by the calls to `hasFixedRuntimeRep ` in +`tcEValArg`. + +But some /built-in/ functions are representation-polymorphic. Users +can't define such Ids; they are all GHC built-ins or data +constructors. Specifically they are: + +1. A few wired-in Ids like unsafeCoerce#, with compulsory unfoldings. +2. Primops, such as raise# +3. Newtype constructors with `UnliftedNewtypes` that have + a representation-polymorphic argument. +4. Representation-polymorphic data constructors: unboxed tuples + and unboxed sums. + +For (1) consider + badId :: forall r (a :: TYPE r). a -> a + badId = unsafeCoerce# @r @r @a @a + +The wired-in function + unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) + (a :: TYPE r1) (b :: TYPE r2). + a -> b +has a convenient but representation-polymorphic type. It has no +binding; instead it has a compulsory unfolding, after which we +would have + badId = /\r /\(a :: TYPE r). \(x::a). ...body of unsafeCorece#... +And this is no good because of that rep-poly \(x::a). So we want +to reject this. + +On the other hand + goodId :: forall (a :: Type). a -> a + goodId = unsafeCoerce# @LiftedRep @LiftedRep @a @a + +is absolutely fine, because after we inline the unfolding, the \(x::a) +is representation-monomorphic. + +Test cases: T14561, RepPolyWrappedVar2. + +For primops (2) the situation is similar; they are eta-expanded in +CorePrep to be saturated, and that eta-expansion must not add a +representation-polymorphic lambda. + +Test cases: T14561b, RepPolyWrappedVar, UnliftedNewtypesCoerceFail. + +For (3), consider a representation-polymorphic newtype with +UnliftedNewtypes: + + type Id :: forall r. TYPE r -> TYPE r + newtype Id a where { MkId :: a } + + bad :: forall r (a :: TYPE r). a -> Id a + bad = MkId @r @a -- Want to reject + + good :: forall (a :: Type). a -> Id a + good = MkId @LiftedRep @a -- Want to accept + +Test cases: T18481, UnliftedNewtypesLevityBinder + +So these three cases need special treatment. We add a special case +in tcApp to check whether an application of an Id has any remaining +representation-polymorphic arguments, after instantiation and application +of previous arguments. This is achieved by the hasFixedRuntimeRep_remainingValArgs +function, which computes the types of the remaining value arguments, and checks +that each of these have a fixed runtime representation using hasFixedRuntimeRep. + +Wrinkles + +* Because of Note [Typechecking data constructors] in GHC.Tc.Gen.Head, + we desugar a representation-polymorphic data constructor application + like this: + (/\(r :: RuntimeRep) (a :: TYPE r) \(x::a). K r a x) @LiftedRep Int 4 + That is, a rep-poly lambda applied to arguments that instantiate it in + a rep-mono way. It's a bit like a compulsory unfolding that has been + inlined, but not yet beta-reduced. + + Because we want to accept this, we switch off Lint's representation + polymorphism checks when Lint checks the output of the desugarer; + see the lf_check_fixed_repy flag in GHC.Core.Lint.lintCoreBindings. + +* Arity. We don't want to check for arguments past the + arity of the function. For example + + raise# :: forall {r :: RuntimeRep} (a :: Type) (b :: TYPE r). a -> b + + has arity 1, so an instantiation such as: + + foo :: forall w r (z :: TYPE r). w -> z -> z + foo = raise# @w @(z -> z) + + is unproblematic. This means we must take care not to perform a + representation-polymorphism check on `z`. + + To achieve this, we consult the arity of the 'Id' which is the head + of the application (or just use 1 for a newtype constructor), + and keep track of how many value-level arguments we have seen, + to ensure we stop checking once we reach the arity. + This is slightly complicated by the need to include both visible + and invisible arguments, as the arity counts both: + see GHC.Tc.Gen.Head.countVisAndInvisValArgs. + + Test cases: T20330{a,b} + +-} + +-- | Check for representation-polymorphism in the remaining argument types +-- of a variable or data constructor, after it has been instantiated and applied to some arguments. +-- +-- See Note [Checking for representation-polymorphic built-ins] +hasFixedRuntimeRep_remainingValArgs :: [HsExprArg 'TcpInst] -> TcRhoType -> HsExpr GhcTc -> TcM () +hasFixedRuntimeRep_remainingValArgs applied_args app_res_rho = \case + + HsVar _ (L _ fun_id) + + -- (1): unsafeCoerce# + -- 'unsafeCoerce#' is peculiar: it is patched in manually as per + -- Note [Wiring in unsafeCoerce#] in GHC.HsToCore. + -- Unfortunately, even though its arity is set to 1 in GHC.HsToCore.mkUnsafeCoercePrimPair, + -- at this stage, if we query idArity, we get 0. This is because + -- we end up looking at the non-patched version of unsafeCoerce# + -- defined in Unsafe.Coerce, and that one indeed has arity 0. + -- + -- We thus manually specify the correct arity of 1 here. + | idName fun_id == unsafeCoercePrimName + -> check_thing fun_id 1 (FRRNoBindingResArg fun_id) + + -- (2): primops and other wired-in representation-polymorphic functions, + -- such as 'rightSection', 'oneShot', etc; see bindings with Compulsory unfoldings + -- in GHC.Types.Id.Make + | isWiredInName (idName fun_id) && hasNoBinding fun_id + -> check_thing fun_id (idArity fun_id) (FRRNoBindingResArg fun_id) + -- NB: idArity consults the IdInfo of the Id. This can be a problem + -- in the presence of hs-boot files, as we might not have finished + -- typechecking; inspecting the IdInfo at this point can cause + -- strange Core Lint errors (see #20447). + -- We avoid this entirely by only checking wired-in names, + -- as those are the only ones this check is applicable to anyway. + + + XExpr (ConLikeTc (RealDataCon con) _ _) + -- (3): Representation-polymorphic newtype constructors. + | isNewDataCon con + -- (4): Unboxed tuples and unboxed sums + || isUnboxedTupleDataCon con + || isUnboxedSumDataCon con + -> check_thing con (dataConRepArity con) (FRRDataConArg con) + + _ -> return () + + where + nb_applied_vis_val_args :: Int + nb_applied_vis_val_args = count isHsValArg applied_args + + nb_applied_val_args :: Int + nb_applied_val_args = countVisAndInvisValArgs applied_args + + arg_tys :: [TyCoBinder] + arg_tys = fst $ splitPiTys app_res_rho + -- We do not need to zonk app_res_rho first, because the number of arrows + -- in the (possibly instantiated) inferred type of the function will + -- be at least the arity of the function. + + check_thing :: Outputable thing => thing -> Arity -> (Int -> FRROrigin) -> TcM () + check_thing thing arity mk_frr_orig = do + traceTc "tcApp remainingValArgs check_thing" (debug_msg thing arity) + go (nb_applied_vis_val_args + 1) (nb_applied_val_args + 1) arg_tys + where + go :: Int -- ^ visible value argument index + -- (only used to report the argument position in error messages) + -> Int -- ^ value argument index + -- used to count up to the arity to ensure we don't check too many argument types + -> [TyCoBinder] + -> TcM () + go _ i_val _ + | i_val > arity + = return () + go _ _ [] + -- Should never happen: it would mean that the arity is higher + -- than the number of arguments apparent from the type + = pprPanic "hasFixedRuntimeRep_remainingValArgs" (debug_msg thing arity) + go i_visval !i_val (Anon af (Scaled _ arg_ty) : tys) + = case af of + InvisArg -> + go i_visval (i_val + 1) tys + VisArg -> do + _concrete_ev <- hasFixedRuntimeRep (mk_frr_orig i_visval) arg_ty + go (i_visval + 1) (i_val + 1) tys + go i_visval i_val (_: tys) + = go i_visval i_val tys + + -- A message containing all the relevant info, in case this functions + -- needs to be debugged again at some point. + debug_msg :: Outputable thing => thing -> Arity -> SDoc + debug_msg thing arity = + vcat + [ text "thing =" <+> ppr thing + , text "arity =" <+> ppr arity + , text "applied_args =" <+> ppr applied_args + , text "nb_applied_vis_val_args =" <+> ppr nb_applied_vis_val_args + , text "nb_applied_val_args =" <+> ppr nb_applied_val_args + , text "arg_tys =" <+> ppr arg_tys ] + -------------------- wantQuickLook :: HsExpr GhcRn -> TcM Bool -- GHC switches on impredicativity all the time for ($) @@ -438,9 +670,10 @@ tcEValArg :: AppCtxt -> EValArg 'TcpInst -> TcSigmaType -> TcM (LHsExpr GhcTc) tcEValArg ctxt (ValArg larg@(L arg_loc arg)) exp_arg_sigma = addArgCtxt ctxt larg $ do { arg' <- tcPolyExpr arg (mkCheckExpType exp_arg_sigma) + ; _concrete_ev <- hasFixedRuntimeRep (FRRApp arg) exp_arg_sigma ; return (L arg_loc arg') } -tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc _) +tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc arg) , va_fun = (inner_fun, fun_ctxt) , va_args = inner_args , va_ty = app_res_rho }) exp_arg_sigma @@ -448,6 +681,7 @@ tcEValArg ctxt (ValArgQL { va_expr = larg@(L arg_loc _) do { traceTc "tcEValArgQL {" (vcat [ ppr inner_fun <+> ppr inner_args ]) ; tc_args <- tcValArgs True inner_args ; co <- unifyType Nothing app_res_rho exp_arg_sigma + ; _concrete_ev <- hasFixedRuntimeRep (FRRApp arg) exp_arg_sigma ; traceTc "tcEValArg }" empty ; return (L arg_loc $ mkHsWrapCo co $ rebuildHsApps inner_fun fun_ctxt tc_args) } diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs index 0d0e482b35..45e8f08a5e 100644 --- a/compiler/GHC/Tc/Gen/Arrow.hs +++ b/compiler/GHC/Tc/Gen/Arrow.hs @@ -22,6 +22,7 @@ import GHC.Hs.Syn.Type import GHC.Tc.Errors.Types import GHC.Tc.Gen.Match import GHC.Tc.Gen.Head( tcCheckId ) +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep ) import GHC.Tc.Utils.TcType import GHC.Tc.Utils.TcMType import GHC.Tc.Gen.Bind @@ -91,13 +92,14 @@ tcProc :: LPat GhcRn -> LHsCmdTop GhcRn -- proc pat -> expr -> ExpRhoType -- Expected type of whole proc expression -> TcM (LPat GhcTc, LHsCmdTop GhcTc, TcCoercion) -tcProc pat cmd@(L _ (HsCmdTop names _)) exp_ty +tcProc pat cmd@(L loc (HsCmdTop names _)) exp_ty = do { exp_ty <- expTypeToType exp_ty -- no higher-rank stuff with arrows ; (co, (exp_ty1, res_ty)) <- matchExpectedAppTy exp_ty ; (co1, (arr_ty, arg_ty)) <- matchExpectedAppTy exp_ty1 -- start with the names as they are used to desugar the proc itself -- See #17423 - ; names' <- mapM (tcSyntaxName ProcOrigin arr_ty) names + ; names' <- setSrcSpan loc $ + mapM (tcSyntaxName ProcOrigin arr_ty) names ; let cmd_env = CmdEnv { cmd_arr = arr_ty } ; (pat', cmd') <- newArrowScope $ tcCheckPat (ArrowMatchCtxt ProcExpr) pat (unrestricted arg_ty) @@ -141,9 +143,10 @@ tcCmdTop env names (L loc (HsCmdTop _names cmd)) cmd_ty@(cmd_stk, res_ty) ---------------------------------------- tcCmd :: CmdEnv -> LHsCmd GhcRn -> CmdType -> TcM (LHsCmd GhcTc) -- The main recursive function -tcCmd env (L loc cmd) res_ty +tcCmd env (L loc cmd) cmd_ty@(_, res_ty) = setSrcSpan (locA loc) $ do - { cmd' <- tc_cmd env cmd res_ty + { cmd' <- tc_cmd env cmd cmd_ty + ; _concrete_ev <- hasFixedRuntimeRep (FRRArrow $ ArrowCmdResTy cmd) res_ty ; return (L loc cmd') } tc_cmd :: CmdEnv -> HsCmd GhcRn -> CmdType -> TcM (HsCmd GhcTc) @@ -219,6 +222,10 @@ tc_cmd env cmd@(HsCmdArrApp _ fun arg ho_app lr) (_, res_ty) ; arg' <- tcCheckMonoExpr arg arg_ty + ; _concrete_ev <- hasFixedRuntimeRep + (FRRArrow $ ArrowCmdArrApp (unLoc fun) (unLoc arg) ho_app) + fun_ty + ; return (HsCmdArrApp fun_ty fun' arg' ho_app lr) } where -- Before type-checking f, use the environment of the enclosing @@ -243,6 +250,9 @@ tc_cmd env cmd@(HsCmdApp x fun arg) (cmd_stk, res_ty) do { arg_ty <- newOpenFlexiTyVarTy ; fun' <- tcCmd env fun (mkPairTy arg_ty cmd_stk, res_ty) ; arg' <- tcCheckMonoExpr arg arg_ty + ; _concrete_ev <- hasFixedRuntimeRep + (FRRArrow $ ArrowCmdApp (unLoc fun) (unLoc arg)) + arg_ty ; return (HsCmdApp x fun' arg') } ------------------------------------------- @@ -271,6 +281,15 @@ tc_cmd env , m_pats = pats' , m_grhss = grhss' }) arg_tys = map (unrestricted . hsLPatType) pats' + + ; _concrete_evs <- + zipWithM + (\ (Scaled _ arg_ty) i -> + hasFixedRuntimeRep (FRRArrow $ ArrowCmdLam i) arg_ty) + arg_tys + [1..] + + ; let cmd' = HsCmdLam x (MG { mg_alts = L l [match'] , mg_ext = MatchGroupTc arg_tys res_ty , mg_origin = origin }) @@ -326,11 +345,12 @@ tc_cmd env cmd@(HsCmdArrForm x expr f fixity cmd_args) (cmd_stk, res_ty) where tc_cmd_arg :: LHsCmdTop GhcRn -> TcM (LHsCmdTop GhcTc, TcType) - tc_cmd_arg cmd@(L _ (HsCmdTop names _)) + tc_cmd_arg cmd@(L loc (HsCmdTop names _)) = do { arr_ty <- newFlexiTyVarTy arrowTyConKind ; stk_ty <- newFlexiTyVarTy liftedTypeKind ; res_ty <- newFlexiTyVarTy liftedTypeKind - ; names' <- mapM (tcSyntaxName ProcOrigin arr_ty) names + ; names' <- setSrcSpan loc $ + mapM (tcSyntaxName ArrowCmdOrigin arr_ty) names ; let env' = env { cmd_arr = arr_ty } ; cmd' <- tcCmdTop env' names' cmd (stk_ty, res_ty) ; return (cmd', mkCmdArrTy env' (mkPairTy alphaTy stk_ty) res_ty) } diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs index e540e3db91..93fa9a7e2c 100644 --- a/compiler/GHC/Tc/Gen/Bind.hs +++ b/compiler/GHC/Tc/Gen/Bind.hs @@ -34,6 +34,7 @@ import GHC.Data.FastString import GHC.Hs import GHC.Tc.Errors.Types import GHC.Tc.Gen.Sig +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep ) import GHC.Tc.Utils.Monad import GHC.Tc.Types.Origin import GHC.Tc.Utils.Env @@ -519,6 +520,11 @@ tcPolyBinds sig_fn prag_fn rec_group rec_tc closed bind_list InferGen mn -> tcPolyInfer rec_tc prag_fn sig_fn mn bind_list CheckGen lbind sig -> tcPolyCheck prag_fn sig lbind + ; _concrete_evs <- + mapM (\ poly_id -> + hasFixedRuntimeRep (FRRBinder $ idName poly_id) (idType poly_id)) + poly_ids + ; traceTc "} End of bindings for" (vcat [ ppr binder_names, ppr rec_group , vcat [ppr id <+> ppr (idType id) | id <- poly_ids] ]) @@ -1181,7 +1187,7 @@ tcMonoBinds :: RecFlag -- Whether the binding is recursive for typechecking pur -> [LHsBind GhcRn] -> TcM (LHsBinds GhcTc, [MonoBindInfo]) --- SPECIAL CASE 1: see Note [Inference for non-recursive function bindings] +-- SPECIAL CASE 1: see Note [Special case for non-recursive function bindings] tcMonoBinds is_rec sig_fn no_gen [ L b_loc (FunBind { fun_id = L nm_loc name , fun_matches = matches })] @@ -1210,7 +1216,7 @@ tcMonoBinds is_rec sig_fn no_gen , mbi_sig = Nothing , mbi_mono_id = mono_id }]) } --- SPECIAL CASE 2: see Note [Inference for non-recursive pattern bindings] +-- SPECIAL CASE 2: see Note [Special case for non-recursive pattern bindings] tcMonoBinds is_rec sig_fn no_gen [L b_loc (PatBind { pat_lhs = pat, pat_rhs = grhss })] | NonRecursive <- is_rec -- ...binder isn't mentioned in RHS @@ -1470,6 +1476,7 @@ tcRhs (TcPatBind infos pat' grhss pat_ty) do { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty) ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $ tcGRHSsPat grhss (mkCheckExpType pat_ty) + ; return ( PatBind { pat_lhs = pat', pat_rhs = grhss' , pat_ext = pat_ty , pat_ticks = ([],[]) } )} diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs index 899a69353e..077414b96a 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs +++ b/compiler/GHC/Tc/Gen/Expr.hs @@ -40,6 +40,7 @@ import GHC.Types.Error import GHC.Core.Multiplicity import GHC.Core.UsageEnv import GHC.Tc.Errors.Types +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep, mkWpFun ) import GHC.Tc.Utils.Instantiate import GHC.Tc.Gen.App import GHC.Tc.Gen.Head @@ -344,7 +345,16 @@ tcExpr (ExplicitSum _ alt arity expr) res_ty ; (coi, arg_tys) <- matchExpectedTyConApp sum_tc res_ty ; -- Drop levity vars, we don't care about them here let arg_tys' = drop arity arg_tys - ; expr' <- tcCheckPolyExpr expr (arg_tys' `getNth` (alt - 1)) + arg_ty = arg_tys' `getNth` (alt - 1) + ; expr' <- tcCheckPolyExpr expr arg_ty + -- Check the whole res_ty, not just the arg_ty, to avoid #20277. + -- Example: + -- a :: TYPE rep (representation-polymorphic) + -- (# 17# | #) :: (# Int# | a #) + -- This should cause an error, even though (17# :: Int#) + -- is not representation-polymorphic: we don't know how + -- wide the concrete representation of the sum type will be. + ; _concrete_ev <- hasFixedRuntimeRep FRRUnboxedSum res_ty ; return $ mkHsWrapCo coi (ExplicitSum arg_tys' alt arity expr' ) } @@ -938,12 +948,17 @@ tcTupArgs :: [HsTupArg GhcRn] -> [TcSigmaType] -> TcM [HsTupArg GhcTc] tcTupArgs args tys = do massert (equalLength args tys) checkTupSize (length args) - mapM go (args `zip` tys) + zipWith3M go [1,2..] args tys where - go (Missing {}, arg_ty) = do { mult <- newFlexiTyVarTy multiplicityTy - ; return (Missing (Scaled mult arg_ty)) } - go (Present x expr, arg_ty) = do { expr' <- tcCheckPolyExpr expr arg_ty - ; return (Present x expr') } + go :: Int -> HsTupArg GhcRn -> TcType -> TcM (HsTupArg GhcTc) + go i (Missing {}) arg_ty + = do { mult <- newFlexiTyVarTy multiplicityTy + ; _concrete_ev <- hasFixedRuntimeRep (FRRTupleSection i) arg_ty + ; return (Missing (Scaled mult arg_ty)) } + go i (Present x expr) arg_ty + = do { expr' <- tcCheckPolyExpr expr arg_ty + ; _concrete_ev <- hasFixedRuntimeRep (FRRTupleArg i) arg_ty + ; return (Present x expr') } --------------------------- -- See TcType.SyntaxOpType also for commentary @@ -1003,8 +1018,8 @@ tcSynArgE :: CtOrigin -- ^ returns a wrapper :: (type of right shape) "->" (type passed in) tcSynArgE orig sigma_ty syn_ty thing_inside = do { (skol_wrap, (result, ty_wrapper)) - <- tcSkolemise GenSigCtxt sigma_ty $ \ rho_ty -> - go rho_ty syn_ty + <- tcSkolemise GenSigCtxt sigma_ty + (\ rho_ty -> go rho_ty syn_ty) ; return (result, skol_wrap <.> ty_wrapper) } where go rho_ty SynAny @@ -1046,13 +1061,11 @@ tcSynArgE orig sigma_ty syn_ty thing_inside do { result <- thing_inside (arg_results ++ res_results) ([arg_mult] ++ arg_res_mults ++ res_res_mults) ; return (result, arg_tc_ty, res_tc_ty, arg_mult) }} - ; return ( result - , match_wrapper <.> - mkWpFun (arg_wrapper2 <.> arg_wrapper1) res_wrapper - (Scaled op_mult arg_ty) res_ty doc ) } + ; fun_wrap <- mkWpFun (arg_wrapper2 <.> arg_wrapper1) res_wrapper + (Scaled op_mult arg_ty) res_ty (WpFunSyntaxOp orig) + ; return (result, match_wrapper <.> fun_wrap) } where herald = text "This rebindable syntax expects a function with" - doc = text "When checking a rebindable syntax operator arising from" <+> ppr orig go rho_ty (SynType the_ty) = do { wrap <- tcSubTypePat orig GenSigCtxt the_ty rho_ty @@ -1374,6 +1387,9 @@ tcRecordField con_like flds_w_tys (L loc (FieldOcc sel_name lbl)) rhs | Just field_ty <- assocMaybe flds_w_tys sel_name = addErrCtxt (fieldCtxt field_lbl) $ do { rhs' <- tcCheckPolyExprNC rhs field_ty + ; _concrete_ev <- + hasFixedRuntimeRep (FRRRecordUpdate (unLoc lbl) (unLoc rhs)) + field_ty ; let field_id = mkUserLocal (nameOccName sel_name) (nameUnique sel_name) Many field_ty loc diff --git a/compiler/GHC/Tc/Gen/Head.hs b/compiler/GHC/Tc/Gen/Head.hs index 78f9b0265a..bfaba5efcc 100644 --- a/compiler/GHC/Tc/Gen/Head.hs +++ b/compiler/GHC/Tc/Gen/Head.hs @@ -22,6 +22,7 @@ module GHC.Tc.Gen.Head , splitHsApps, rebuildHsApps , addArgWrap, isHsValArg , countLeadingValArgs, isVisibleArg, pprHsExprArgTc + , countVisAndInvisValArgs, countHsWrapperInvisArgs , tcInferAppHead, tcInferAppHead_maybe , tcInferId, tcCheckId @@ -75,6 +76,7 @@ import GHC.Types.SrcLoc import GHC.Utils.Misc import GHC.Data.Maybe import GHC.Utils.Outputable as Outputable +import GHC.Utils.Panic import GHC.Utils.Panic.Plain import Control.Monad @@ -323,6 +325,36 @@ isVisibleArg (EValArg {}) = True isVisibleArg (ETypeArg {}) = True isVisibleArg _ = False +-- | Count visible and invisible value arguments in a list +-- of 'HsExprArg' arguments. +countVisAndInvisValArgs :: [HsExprArg id] -> Arity +countVisAndInvisValArgs [] = 0 +countVisAndInvisValArgs (EValArg {} : args) = 1 + countVisAndInvisValArgs args +countVisAndInvisValArgs (EWrap wrap : args) = + case wrap of { EHsWrap hsWrap -> countHsWrapperInvisArgs hsWrap + countVisAndInvisValArgs args + ; EPar {} -> countVisAndInvisValArgs args + ; EExpand {} -> countVisAndInvisValArgs args } +countVisAndInvisValArgs (EPrag {} : args) = countVisAndInvisValArgs args +countVisAndInvisValArgs (ETypeArg {}: args) = countVisAndInvisValArgs args + +-- | Counts the number of invisible term-level arguments applied by an 'HsWrapper'. +-- Precondition: this wrapper contains no abstractions. +countHsWrapperInvisArgs :: HsWrapper -> Arity +countHsWrapperInvisArgs = go + where + go WpHole = 0 + go (WpCompose wrap1 wrap2) = go wrap1 + go wrap2 + go fun@(WpFun {}) = nope fun + go (WpCast {}) = 0 + go evLam@(WpEvLam {}) = nope evLam + go (WpEvApp _) = 1 + go tyLam@(WpTyLam {}) = nope tyLam + go (WpTyApp _) = 0 + go (WpLet _) = 0 + go (WpMultCoercion {}) = 0 + + nope x = pprPanic "countHsWrapperInvisApps" (ppr x) + instance OutputableBndrId (XPass p) => Outputable (HsExprArg p) where ppr (EValArg { eva_arg = arg }) = text "EValArg" <+> ppr arg ppr (EPrag _ p) = text "EPrag" <+> ppr p diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs index c8eb8fd233..ab767b877c 100644 --- a/compiler/GHC/Tc/Gen/Match.hs +++ b/compiler/GHC/Tc/Gen/Match.hs @@ -49,6 +49,7 @@ import GHC.Tc.Gen.Head( tcCheckId ) import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.TcType import GHC.Tc.Gen.Bind +import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep ) import GHC.Tc.Utils.Unify import GHC.Tc.Types.Origin import GHC.Tc.Types.Evidence @@ -226,6 +227,10 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches = do { tcEmitBindingUsage bottomUE ; pat_tys <- mapM scaledExpTypeToType pat_tys ; rhs_ty <- expTypeToType rhs_ty + ; _concrete_evs <- zipWithM + (\ i (Scaled _ pat_ty) -> + hasFixedRuntimeRep (FRRMatch (mc_what ctxt) i) pat_ty) + [1..] pat_tys ; return (MG { mg_alts = L l [] , mg_ext = MatchGroupTc pat_tys rhs_ty , mg_origin = origin }) } @@ -236,6 +241,10 @@ tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches ; tcEmitBindingUsage $ supUEs usages ; pat_tys <- mapM readScaledExpType pat_tys ; rhs_ty <- readExpType rhs_ty + ; _concrete_evs <- zipWithM + (\ i (Scaled _ pat_ty) -> + hasFixedRuntimeRep (FRRMatch (mc_what ctxt) i) pat_ty) + [1..] pat_tys ; return (MG { mg_alts = L l matches' , mg_ext = MatchGroupTc pat_tys rhs_ty , mg_origin = origin }) } @@ -431,6 +440,7 @@ tcGuardStmt ctxt (BindStmt _ pat rhs) res_ty thing_inside -- two multiplicity to still be the same. (rhs', rhs_ty) <- tcScalingUsage Many $ tcInferRhoNC rhs -- Stmt has a context already + ; _concrete_ev <- hasFixedRuntimeRep FRRBindStmtGuard rhs_ty ; (pat', thing) <- tcCheckPat_O (StmtCtxt ctxt) (lexprCtOrigin rhs) pat (unrestricted rhs_ty) $ thing_inside res_ty @@ -583,14 +593,16 @@ tcMcStmt _ (LastStmt x body noret return_op) res_ty thing_inside tcMcStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside -- (>>=) :: rhs_ty -> (pat_ty -> new_res_ty) -> res_ty - = do { ((rhs', pat_mult, pat', thing, new_res_ty), bind_op') + = do { ((rhs_ty, rhs', pat_mult, pat', thing, new_res_ty), bind_op') <- tcSyntaxOp MCompOrigin (xbsrn_bindOp xbsrn) [SynRho, SynFun SynAny SynRho] res_ty $ \ [rhs_ty, pat_ty, new_res_ty] [rhs_mult, fun_mult, pat_mult] -> do { rhs' <- tcScalingUsage rhs_mult $ tcCheckMonoExprNC rhs rhs_ty ; (pat', thing) <- tcScalingUsage fun_mult $ tcCheckPat (StmtCtxt ctxt) pat (Scaled pat_mult pat_ty) $ thing_inside (mkCheckExpType new_res_ty) - ; return (rhs', pat_mult, pat', thing, new_res_ty) } + ; return (rhs_ty, rhs', pat_mult, pat', thing, new_res_ty) } + + ; _concrete_ev <- hasFixedRuntimeRep (FRRBindStmt MonadComprehension) rhs_ty -- If (but only if) the pattern can fail, typecheck the 'fail' operator ; fail_op' <- fmap join . forM (xbsrn_failOp xbsrn) $ \fail -> @@ -613,17 +625,23 @@ tcMcStmt _ (BodyStmt _ rhs then_op guard_op) res_ty thing_inside -- guard_op :: test_ty -> rhs_ty -- then_op :: rhs_ty -> new_res_ty -> res_ty -- Where test_ty is, for example, Bool - ; ((thing, rhs', rhs_ty, guard_op'), then_op') + ; ((thing, rhs', rhs_ty, new_res_ty, test_ty, guard_op'), then_op') <- tcSyntaxOp MCompOrigin then_op [SynRho, SynRho] res_ty $ \ [rhs_ty, new_res_ty] [rhs_mult, fun_mult] -> - do { (rhs', guard_op') + do { ((rhs', test_ty), guard_op') <- tcScalingUsage rhs_mult $ tcSyntaxOp MCompOrigin guard_op [SynAny] (mkCheckExpType rhs_ty) $ - \ [test_ty] [test_mult] -> - tcScalingUsage test_mult $ tcCheckMonoExpr rhs test_ty + \ [test_ty] [test_mult] -> do + rhs' <- tcScalingUsage test_mult $ tcCheckMonoExpr rhs test_ty + return $ (rhs', test_ty) ; thing <- tcScalingUsage fun_mult $ thing_inside (mkCheckExpType new_res_ty) - ; return (thing, rhs', rhs_ty, guard_op') } + ; return (thing, rhs', rhs_ty, new_res_ty, test_ty, guard_op') } + + ; _evTerm1 <- hasFixedRuntimeRep FRRBodyStmtGuard test_ty + ; _evTerm2 <- hasFixedRuntimeRep (FRRBodyStmt MonadComprehension 1) rhs_ty + ; _evTerm3 <- hasFixedRuntimeRep (FRRBodyStmt MonadComprehension 2) new_res_ty + ; return (BodyStmt rhs_ty rhs' then_op' guard_op', thing) } -- Grouping statements @@ -850,13 +868,15 @@ tcDoStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside -- This level of generality is needed for using do-notation -- in full generality; see #1537 - ((rhs', pat_mult, pat', new_res_ty, thing), bind_op') + ((rhs_ty, rhs', pat_mult, pat', new_res_ty, thing), bind_op') <- tcSyntaxOp DoOrigin (xbsrn_bindOp xbsrn) [SynRho, SynFun SynAny SynRho] res_ty $ \ [rhs_ty, pat_ty, new_res_ty] [rhs_mult,fun_mult,pat_mult] -> do { rhs' <-tcScalingUsage rhs_mult $ tcCheckMonoExprNC rhs rhs_ty ; (pat', thing) <- tcScalingUsage fun_mult $ tcCheckPat (StmtCtxt ctxt) pat (Scaled pat_mult pat_ty) $ thing_inside (mkCheckExpType new_res_ty) - ; return (rhs', pat_mult, pat', new_res_ty, thing) } + ; return (rhs_ty, rhs', pat_mult, pat', new_res_ty, thing) } + + ; _concrete_ev <- hasFixedRuntimeRep (FRRBindStmt DoNotation) rhs_ty -- If (but only if) the pattern can fail, typecheck the 'fail' operator ; fail_op' <- fmap join . forM (xbsrn_failOp xbsrn) $ \fail -> @@ -884,12 +904,14 @@ tcDoStmt ctxt (ApplicativeStmt _ pairs mb_join) res_ty thing_inside tcDoStmt _ (BodyStmt _ rhs then_op _) res_ty thing_inside = do { -- Deal with rebindable syntax; -- (>>) :: rhs_ty -> new_res_ty -> res_ty - ; ((rhs', rhs_ty, thing), then_op') + ; ((rhs', rhs_ty, new_res_ty, thing), then_op') <- tcSyntaxOp DoOrigin then_op [SynRho, SynRho] res_ty $ \ [rhs_ty, new_res_ty] [rhs_mult,fun_mult] -> do { rhs' <- tcScalingUsage rhs_mult $ tcCheckMonoExprNC rhs rhs_ty ; thing <- tcScalingUsage fun_mult $ thing_inside (mkCheckExpType new_res_ty) - ; return (rhs', rhs_ty, thing) } + ; return (rhs', rhs_ty, new_res_ty, thing) } + ; _evTerm1 <- hasFixedRuntimeRep (FRRBodyStmt DoNotation 1) rhs_ty + ; _evTerm2 <- hasFixedRuntimeRep (FRRBodyStmt DoNotation 2) new_res_ty ; return (BodyStmt rhs_ty rhs' then_op' noSyntaxExpr, thing) } tcDoStmt ctxt (RecStmt { recS_stmts = L l stmts, recS_later_ids = later_names diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs index 78a4e22901..332ea601b1 100644 --- a/compiler/GHC/Tc/Gen/Pat.hs +++ b/compiler/GHC/Tc/Gen/Pat.hs @@ -36,6 +36,7 @@ import GHC.Rename.Utils import GHC.Tc.Errors.Types import GHC.Tc.Utils.Zonk import GHC.Tc.Gen.Sig( TcPragEnv, lookupPragEnv, addInlinePrags ) +import GHC.Tc.Utils.Concrete ( mkWpFun ) import GHC.Tc.Utils.Monad import GHC.Tc.Utils.Instantiate import GHC.Types.Error @@ -445,12 +446,12 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of ; let Scaled w h_pat_ty = pat_ty ; pat_ty <- readExpType h_pat_ty - ; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper - (Scaled w pat_ty) inf_res_sigma doc - -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->" - -- (pat_ty -> inf_res_sigma) + ; expr_wrap2' <- mkWpFun expr_wrap2 idHsWrapper + (Scaled w pat_ty) inf_res_sigma (WpFunViewPat $ unLoc expr) + -- expr_wrap2' :: (inf_arg_ty -> inf_res_sigma) "->" + -- (pat_ty -> inf_res_sigma) + ; let expr_wrap = expr_wrap2' <.> expr_wrap1 <.> mult_wrap - doc = text "When checking the view pattern function:" <+> (ppr expr) ; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) } @@ -656,6 +657,7 @@ AST is used for the subtraction operation. ; return (lit2', wrap, bndr_id) } ; pat_ty <- readExpType pat_exp_ty + -- The Report says that n+k patterns must be in Integral -- but it's silly to insist on this in the RebindableSyntax case ; unlessM (xoptM LangExt.RebindableSyntax) $ diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs index 73dedfbaf5..46b1e16313 100644 --- a/compiler/GHC/Tc/Gen/Rule.hs +++ b/compiler/GHC/Tc/Gen/Rule.hs @@ -477,12 +477,17 @@ getRuleQuantCts wc new_skol_tvs = skol_tvs `extendVarSetList` ic_skols imp rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool - rule_quant_ct skol_tvs ct - | EqPred _ t1 t2 <- classifyPredType (ctPred ct) - , not (ok_eq t1 t2) - = False -- Note [RULE quantification over equalities] - | otherwise - = tyCoVarsOfCt ct `disjointVarSet` skol_tvs + rule_quant_ct skol_tvs ct = case classifyPredType (ctPred ct) of + EqPred _ t1 t2 + | not (ok_eq t1 t2) + -> False -- Note [RULE quantification over equalities] + SpecialPred {} + -- RULES must never quantify over special predicates, as that + -- would leak internal GHC implementation details to the user. + -- + -- Tests (for Concrete# predicates): RepPolyRule{1,2,3}. + -> False + _ -> tyCoVarsOfCt ct `disjointVarSet` skol_tvs ok_eq t1 t2 | t1 `tcEqType` t2 = False diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs index 67715e9b5b..bec5af03b0 100644 --- a/compiler/GHC/Tc/Gen/Sig.hs +++ b/compiler/GHC/Tc/Gen/Sig.hs @@ -32,15 +32,15 @@ import GHC.Driver.Backend import GHC.Hs -import GHC.Tc.Errors.Types ( TcRnMessage(..), LevityCheckProvenance(..) ) +import GHC.Tc.Errors.Types ( FixedRuntimeRepProvenance(..), TcRnMessage(..) ) import GHC.Tc.Gen.HsType import GHC.Tc.Types import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities ) import GHC.Tc.Utils.Monad +import GHC.Tc.Utils.TcMType ( checkTypeHasFixedRuntimeRep ) import GHC.Tc.Utils.Zonk import GHC.Tc.Types.Origin import GHC.Tc.Utils.TcType -import GHC.Tc.Utils.TcMType import GHC.Tc.Validity ( checkValidType ) import GHC.Tc.Utils.Unify( tcSkolemise, unifyType ) import GHC.Tc.Utils.Instantiate( topInstantiate, tcInstTypeBndrs ) @@ -452,10 +452,15 @@ tcPatSynSig name sig_ty@(L _ (HsSig{sig_bndrs = hs_outer_bndrs, sig_body = hs_ty ; checkValidType ctxt $ build_patsyn_type implicit_bndrs univ_bndrs req ex_bndrs prov body_ty - -- arguments become the types of binders. We thus cannot allow - -- representation polymorphism here - ; let (arg_tys, _) = tcSplitFunTys body_ty - ; mapM_ (checkForLevPoly LevityCheckPatSynSig . scaledThing) arg_tys + -- Neither argument types nor the return type may be representation polymorphic. + -- This is because, when creating a matcher: + -- - the argument types become the the binder types (see test RepPolyPatySynArg), + -- - the return type becomes the scrutinee type (see test RepPolyPatSynRes). + ; let (arg_tys, res_ty) = tcSplitFunTys body_ty + ; mapM_ + (\(Scaled _ arg_ty) -> checkTypeHasFixedRuntimeRep FixedRuntimeRepPatSynSigArg arg_ty) + arg_tys + ; checkTypeHasFixedRuntimeRep FixedRuntimeRepPatSynSigRes res_ty ; traceTc "tcTySig }" $ vcat [ text "kvs" <+> ppr_tvs (binderVars kv_bndrs) diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs index 757226ed28..8063ce7720 100644 --- a/compiler/GHC/Tc/Instance/Class.hs +++ b/compiler/GHC/Tc/Instance/Class.hs @@ -1,18 +1,18 @@ - {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} module GHC.Tc.Instance.Class ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..), safeOverlap, instanceReturnsDictCon, - AssocInstInfo(..), isNotAssociated + AssocInstInfo(..), isNotAssociated, ) where import GHC.Prelude import GHC.Driver.Session +import GHC.Core.TyCo.Rep import GHC.Tc.Utils.Env import GHC.Tc.Utils.Monad @@ -25,7 +25,7 @@ import GHC.Tc.Instance.Family( tcGetFamInstEnvs, tcInstNewTyCon_maybe, tcLookupD import GHC.Rename.Env( addUsedGRE ) import GHC.Builtin.Types -import GHC.Builtin.Types.Prim( eqPrimTyCon, eqReprPrimTyCon ) +import GHC.Builtin.Types.Prim import GHC.Builtin.Names import GHC.Types.Name.Reader( lookupGRE_FieldLabel, greMangledName ) @@ -37,7 +37,7 @@ import GHC.Types.Id import GHC.Core.Predicate import GHC.Core.InstEnv import GHC.Core.Type -import GHC.Core.Make ( mkCharExpr, mkStringExprFS, mkNaturalExpr ) +import GHC.Core.Make ( mkCharExpr, mkNaturalExpr, mkStringExprFS ) import GHC.Core.DataCon import GHC.Core.TyCon import GHC.Core.Class @@ -609,7 +609,6 @@ matchCoercible args@[k, t1, t2] args' = [k, k, t1, t2] matchCoercible args = pprPanic "matchLiftedCoercible" (ppr args) - {- ******************************************************************** * * Class lookup for overloaded record fields diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs index 0cf68fcb35..8739c33ec5 100644 --- a/compiler/GHC/Tc/Module.hs +++ b/compiler/GHC/Tc/Module.hs @@ -1308,7 +1308,7 @@ checkBootTyCon is_boot tc1 tc2 Nothing -> Just roles_msg -} - eqAlgRhs _ AbstractTyCon _rhs2 + eqAlgRhs _ (AbstractTyCon {}) _rhs2 = checkSuccess -- rhs2 is guaranteed to be injective, since it's an AlgTyCon eqAlgRhs _ tc1@DataTyCon{} tc2@DataTyCon{} = checkListBy eqCon (data_cons tc1) (data_cons tc2) (text "constructors") diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index cdb86b92e2..eb205e71cb 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -15,6 +15,7 @@ import GHC.Prelude import GHC.Tc.Types.Constraint import GHC.Core.Predicate import GHC.Tc.Types.Origin +import GHC.Tc.Utils.Concrete ( newConcretePrimWanted ) import GHC.Tc.Utils.Unify import GHC.Tc.Utils.TcType import GHC.Core.Type @@ -41,6 +42,7 @@ import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Panic.Plain import GHC.Builtin.Types ( anyTypeOfKind ) +import GHC.Builtin.Types.Prim ( concretePrimTyCon ) import GHC.Types.Name.Set import GHC.Types.Name.Reader import GHC.Hs.Type( HsIPName(..) ) @@ -97,6 +99,9 @@ canonicalize (CNonCanonical { cc_ev = ev }) canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc })) = canForAll ev pend_sc +canonicalize (CSpecialCan { cc_ev = ev, cc_special_pred = special_pred, cc_xi = xi }) + = canSpecial ev special_pred xi + canonicalize (CIrredCan { cc_ev = ev }) = canNC ev -- Instead of rewriting the evidence before classifying, it's possible we @@ -131,6 +136,8 @@ canNC ev = canIrred ev ForAllPred tvs th p -> do traceTcS "canEvNC:forall" (ppr pred) canForAllNC ev tvs th p + SpecialPred tc ty -> do traceTcS "canEvNC:special" (ppr pred) + canSpecial ev tc ty where pred = ctEvPred ev @@ -208,7 +215,7 @@ canClass :: CtEvidence -- Precondition: EvVar is class evidence canClass ev cls tys pend_sc fds - = -- all classes do *nominal* matching + = -- all classes do *nominal* matching assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $ do { redns@(Reductions _ xis) <- rewriteArgsNom ev cls_tc tys ; let redn@(Reduction _ xi) = mkClassPredRedn cls redns @@ -718,12 +725,19 @@ canIrred ev -- that the IrredPred branch stops work ; case classifyPredType (ctEvPred new_ev) of ClassPred cls tys -> canClassNC new_ev cls tys - EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2 + EqPred eq_rel ty1 ty2 -> -- IrredPreds have kind Constraint, so + -- cannot become EqPreds + pprPanic "canIrred: EqPred" + (ppr ev $$ ppr eq_rel $$ ppr ty1 $$ ppr ty2) ForAllPred tvs th p -> -- this is highly suspect; Quick Look -- should never leave a meta-var filled -- in with a polytype. This is #18987. do traceTcS "canEvNC:forall" (ppr pred) canForAllNC ev tvs th p + SpecialPred tc tys -> -- IrredPreds have kind Constraint, so cannot + -- become SpecialPreds + pprPanic "canIrred: SpecialPred" + (ppr ev $$ ppr tc $$ ppr tys) IrredPred {} -> continueWith $ mkIrredCt IrredShapeReason new_ev } } @@ -897,6 +911,133 @@ we'll find a match in the InstEnv. ************************************************************************ * * +* Special predicates +* * +********************************************************************* -} + +-- | Canonicalise a 'SpecialPred' constraint. +canSpecial :: CtEvidence -> SpecialPred -> TcType -> TcS (StopOrContinue Ct) +canSpecial ev special_pred ty + = do { -- Special constraints should never appear in Givens. + ; massertPpr (not $ isGivenOrigin $ ctEvOrigin ev) + (text "canSpecial: Given Special constraint" $$ ppr ev) + ; case special_pred of + { ConcretePrimPred -> canConcretePrim ev ty } } + +{- Note [Canonical Concrete# constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +A 'Concrete#' constraint can be decomposed precisely when +it is an application, possibly nullary, of a concrete 'TyCon'. + +A canonical 'Concrete#' constraint is one that cannot be decomposed. + +To illustrate, when we come across a constraint of the form `Concrete# (f a_1 ... a_n)`, +to canonicalise it, we decompose it into the collection of constraints +`Concrete# a_1`, ..., `Concrete# a_n`, whenever `f` is a concrete type constructor +(that is, it is not a type variable, nor a type-family, nor an abstract 'TyCon' +as declared in a Backpack signature file). + +Writing NC for a non-canonical constraint and C for a canonical one, +here are some examples: + + (1) + NC: Concrete# IntRep + ==> nullary decomposition, by observing that `IntRep = TyConApp intRepTyCon []` + + (2) + NC: Concrete# (TYPE (TupleRep '[Rep, rr])) -- where 'Rep' is an abstract type and 'rr' is a type variable + ==> decompose once, noting that 'TYPE' is a concrete 'TyCon' + NC: Concrete# (TupleRep '[Rep, rr]) + ==> decompose again in the same way but with 'TupleRep' + NC: Concrete# ((:) @RuntimeRep Rep ((:) @RuntimeRep rr [])) + ==> handle (:) and its type-level argument 'RuntimeRep' (which is concrete) + C: Concrete# Rep, NC: Concrete# ((:) @RuntimeRep rr [])) + ==> the second constraint can be decomposed again; 'RuntimeRep' and '[]' are concrete, so we get + C: Concrete# Rep, C: Concrete# rr + +-} + +-- | Canonicalise a 'Concrete#' constraint. +-- +-- See Note [Canonical Concrete# constraints] for details. +canConcretePrim :: CtEvidence -> TcType -> TcS (StopOrContinue Ct) +canConcretePrim ev ty + = do { + -- As per Note [The Concrete mechanism] in GHC.Tc.Instance.Class, + -- in PHASE 1, we don't allow a 'Concrete#' constraint to be rewritten. + -- We still need to zonk, otherwise we can end up stuck with a constraint + -- such as `Concrete# rep` for a unification variable `rep`, + -- which we can't make progress on. + ; ty <- zonkTcType ty + ; traceTcS "canConcretePrim" $ + vcat [text "ev =" <+> ppr ev, text "ty =" <+> ppr ty] + + ; decomposeConcretePrim ev ty } + +-- | Try to decompose a 'Concrete#' constraint: +-- +-- - calls 'canDecomposableConcretePrim' if the constraint can be decomposed; +-- - calls 'canNonDecomposableConcretePrim' otherwise. +decomposeConcretePrim :: CtEvidence -> Type -> TcS (StopOrContinue Ct) +decomposeConcretePrim ev ty + -- Handle applications of concrete 'TyCon's. + -- See examples (1,2) in Note [Canonical Concrete# constraints]. + | (f,args) <- tcSplitAppTys ty + , Just f_tc <- tyConAppTyCon_maybe f + , isConcreteTyCon f_tc + = canDecomposableConcretePrim ev f_tc args + + -- Couldn't decompose the constraint: keep it as-is. + | otherwise + = canNonDecomposableConcretePrim ev ty + +-- | Decompose a constraint of the form @'Concrete#' (f t_1 ... t_n)@, +-- for a concrete `TyCon' `f`. +-- +-- This function will emit new Wanted @Concrete# t_i@ constraints, one for +-- each of the arguments of `f`. +-- +-- See Note [Canonical Concrete# constraints]. +canDecomposableConcretePrim :: CtEvidence + -> TyCon + -> [TcType] + -> TcS (StopOrContinue Ct) +canDecomposableConcretePrim ev f_tc args + = do { traceTcS "canDecomposableConcretePrim" $ + vcat [text "args =" <+> ppr args, text "ev =" <+> ppr ev] + ; arg_cos <- mapM (emit_new_concretePrim_wanted (ctEvLoc ev)) args + ; case ev of + CtWanted { ctev_dest = dest } + -> setWantedEvTerm dest (evCoercion $ mkTyConAppCo Nominal f_tc arg_cos) + _ -> pprPanic "canDecomposableConcretePrim: non-Wanted" $ + vcat [ text "ev =" <+> ppr ev + , text "args =" <+> ppr args ] + ; stopWith ev "Decomposed Concrete#" } + +-- | Canonicalise a non-decomposable 'Concrete#' constraint. +canNonDecomposableConcretePrim :: CtEvidence -> TcType -> TcS (StopOrContinue Ct) +canNonDecomposableConcretePrim ev ty + = do { -- Update the evidence to account for the zonk to `ty`. + let ki = typeKind ty + new_ev = ev { ctev_pred = mkTyConApp concretePrimTyCon [ki, ty] } + new_ct = + CSpecialCan { cc_ev = new_ev + , cc_special_pred = ConcretePrimPred + , cc_xi = ty } + ; traceTcS "canNonDecomposableConcretePrim" $ + vcat [ text "ty =" <+> ppr ty, text "new_ev =" <+> ppr new_ev ] + ; continueWith new_ct } + +-- | Create a new 'Concrete#' Wanted constraint and immediately add it +-- to the work list. +emit_new_concretePrim_wanted :: CtLoc -> Type -> TcS Coercion +emit_new_concretePrim_wanted loc ty + = do { (hole, wanted) <- wrapTcS $ newConcretePrimWanted loc ty + ; emitWorkNC [wanted] + ; return $ mkHoleCo hole } + +{- ********************************************************************** +* * * Equalities * * ************************************************************************ diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs index 5f41ca4ffd..f5e6fda5c3 100644 --- a/compiler/GHC/Tc/Solver/InertSet.hs +++ b/compiler/GHC/Tc/Solver/InertSet.hs @@ -41,6 +41,7 @@ import GHC.Tc.Utils.TcType import GHC.Types.Var import GHC.Types.Var.Env +import GHC.Core.Class (Class(..)) import GHC.Core.Reduction import GHC.Core.Predicate import GHC.Core.TyCo.FVs @@ -1235,7 +1236,10 @@ addInertItem tc_lvl ics@(IC { inert_irreds = irreds }) item@(CIrredCan {}) ics { inert_irreds = irreds `snocBag` item } addInertItem _ ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) - = ics { inert_dicts = addDictCt (inert_dicts ics) cls tys item } + = ics { inert_dicts = addDictCt (inert_dicts ics) (classTyCon cls) tys item } + +addInertItem _ ics@( IC { inert_irreds = irreds }) item@(CSpecialCan {}) + = ics { inert_irreds = irreds `snocBag` item } addInertItem _ _ item = pprPanic "upd_inert set: can't happen! Inserting " $ diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index e583861196..ff3b3e7fcd 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -1,5 +1,4 @@ - {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} @@ -431,9 +430,10 @@ interactWithInertsStage wi = do { inerts <- getTcSInerts ; let ics = inert_cans inerts ; case wi of - CEqCan {} -> interactEq ics wi - CIrredCan {} -> interactIrred ics wi - CDictCan {} -> interactDict ics wi + CEqCan {} -> interactEq ics wi + CIrredCan {} -> interactIrred ics wi + CDictCan {} -> interactDict ics wi + CSpecialCan {} -> continueWith wi -- cannot have Special Givens, so nothing to interact with _ -> pprPanic "interactWithInerts" (ppr wi) } -- CNonCanonical have been canonicalised @@ -1905,13 +1905,23 @@ topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct) topReactionsStage work_item = do { traceTcS "doTopReact" (ppr work_item) ; case work_item of - CDictCan {} -> do { inerts <- getTcSInerts - ; doTopReactDict inerts work_item } - CEqCan {} -> doTopReactEq work_item - CIrredCan {} -> doTopReactOther work_item - _ -> -- Any other work item does not react with any top-level equations - continueWith work_item } + CDictCan {} -> + do { inerts <- getTcSInerts + ; doTopReactDict inerts work_item } + + CEqCan {} -> + doTopReactEq work_item + + CSpecialCan {} -> + -- No top-level interactions for special constraints. + continueWith work_item + + CIrredCan {} -> + doTopReactOther work_item + + -- Any other work item does not react with any top-level equations + _ -> continueWith work_item } -------------------- doTopReactOther :: Ct -> TcS (StopOrContinue Ct) @@ -1939,6 +1949,12 @@ doTopReactOther work_item loc = ctEvLoc ev pred = ctEvPred ev +{-******************************************************************** +* * + Top-level reaction for equality constraints (CEqCan) +* * +********************************************************************-} + doTopReactEqPred :: Ct -> EqRel -> TcType -> TcType -> TcS (StopOrContinue Ct) doTopReactEqPred work_item eq_rel t1 t2 -- See Note [Looking up primitive equalities in quantified constraints] diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index 7baf9ea186..7efc6c9ab9 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -159,6 +159,7 @@ import GHC.Types.Var.Set import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Logger +import GHC.Utils.Misc (HasDebugCallStack) import GHC.Data.Bag as Bag import GHC.Types.Unique.Supply import GHC.Tc.Types @@ -729,7 +730,7 @@ kickOutAfterFillingCoercionHole hole filled_co -------------- addInertSafehask :: InertCans -> Ct -> InertCans addInertSafehask ics item@(CDictCan { cc_class = cls, cc_tyargs = tys }) - = ics { inert_safehask = addDictCt (inert_dicts ics) cls tys item } + = ics { inert_safehask = addDictCt (inert_dicts ics) (classTyCon cls) tys item } addInertSafehask _ item = pprPanic "addInertSafehask: can't happen! Inserting " $ ppr item @@ -767,7 +768,6 @@ setSolvedDicts solved_dicts = updInertTcS $ \ ics -> ics { inert_solved_dicts = solved_dicts } - {- ********************************************************************* * * Other inert-set operations @@ -878,7 +878,7 @@ get_sc_pending this_lvl ic@(IC { inert_dicts = dicts, inert_insts = insts }) add :: Ct -> DictMap Ct -> DictMap Ct add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) dicts - = addDictCt dicts cls tys ct + = addDictCt dicts (classTyCon cls) tys ct add ct _ = pprPanic "getPendingScDicts" (ppr ct) get_pending_inst :: [Ct] -> QCInst -> ([Ct], QCInst) @@ -901,21 +901,21 @@ getUnsolvedInerts :: TcS ( Bag Implication -- (because they come from the inert set) -- the unsolved implics may not be getUnsolvedInerts - = do { IC { inert_eqs = tv_eqs - , inert_funeqs = fun_eqs - , inert_irreds = irreds - , inert_blocked = blocked - , inert_dicts = idicts + = do { IC { inert_eqs = tv_eqs + , inert_funeqs = fun_eqs + , inert_irreds = irreds + , inert_blocked = blocked + , inert_dicts = idicts } <- getInertCans - ; let unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs emptyCts - unsolved_fun_eqs = foldFunEqs add_if_unsolveds fun_eqs emptyCts - unsolved_irreds = Bag.filterBag is_unsolved irreds - unsolved_blocked = blocked -- all blocked equalities are W/D - unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts - unsolved_others = unionManyBags [ unsolved_irreds - , unsolved_dicts - , unsolved_blocked ] + ; let unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs emptyCts + unsolved_fun_eqs = foldFunEqs add_if_unsolveds fun_eqs emptyCts + unsolved_irreds = Bag.filterBag is_unsolved irreds + unsolved_blocked = blocked -- all blocked equalities are W/D + unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts + unsolved_others = unionManyBags [ unsolved_irreds + , unsolved_dicts + , unsolved_blocked ] ; implics <- getWorkListImplics @@ -1077,6 +1077,8 @@ removeInertCt is ct = CQuantCan {} -> panic "removeInertCt: CQuantCan" CIrredCan {} -> panic "removeInertCt: CIrredEvCan" CNonCanonical {} -> panic "removeInertCt: CNonCanonical" + CSpecialCan _ special_pred _ -> + pprPanic "removeInertCt" (ppr "CSpecialCan" <+> parens (ppr special_pred)) -- | Looks up a family application in the inerts. lookupFamAppInert :: TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole)) @@ -2025,7 +2027,7 @@ useVars co_vars ; TcM.writeTcRef ref tcvs' } } -- | Equalities only -setWantedEq :: TcEvDest -> Coercion -> TcS () +setWantedEq :: HasDebugCallStack => TcEvDest -> Coercion -> TcS () setWantedEq (HoleDest hole) co = do { useVars (coVarsOfCo co) ; fillCoercionHole hole co } diff --git a/compiler/GHC/Tc/Solver/Types.hs b/compiler/GHC/Tc/Solver/Types.hs index 1636bbede4..1b367e450e 100644 --- a/compiler/GHC/Tc/Solver/Types.hs +++ b/compiler/GHC/Tc/Solver/Types.hs @@ -15,7 +15,9 @@ module GHC.Tc.Solver.Types ( FunEqMap, emptyFunEqs, foldFunEqs, findFunEq, insertFunEq, findFunEqsByTyCon, - TcAppMap, isEmptyTcAppMap, insertTcApp, alterTcApp, filterTcAppMap, + TcAppMap, emptyTcAppMap, isEmptyTcAppMap, + insertTcApp, alterTcApp, filterTcAppMap, + tcAppMapToBag, foldTcAppMap, EqualCtList, pattern EqualCtList, equalCtListToList, filterEqualCtList, unitEqualCtList, @@ -155,10 +157,10 @@ delDict m cls tys = delTcApp m (classTyCon cls) tys addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a addDict m cls tys item = insertTcApp m (classTyCon cls) tys item -addDictCt :: DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct +addDictCt :: DictMap Ct -> TyCon -> [Type] -> Ct -> DictMap Ct -- Like addDict, but combines [W] and [D] to [WD] -- See Note [KeepBoth] in GHC.Tc.Solver.Interact -addDictCt m cls tys new_ct = alterTcApp m (classTyCon cls) tys xt_ct +addDictCt m tc tys new_ct = alterTcApp m tc tys xt_ct where new_ct_ev = ctEvidence new_ct diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs index 968baad524..713d3f173b 100644 --- a/compiler/GHC/Tc/TyCl.hs +++ b/compiler/GHC/Tc/TyCl.hs @@ -33,7 +33,7 @@ import GHC.Driver.Session import GHC.Hs -import GHC.Tc.Errors.Types ( TcRnMessage(..), LevityCheckProvenance(..) ) +import GHC.Tc.Errors.Types ( TcRnMessage(..), FixedRuntimeRepProvenance(..) ) import GHC.Tc.TyCl.Build import GHC.Tc.Solver( pushLevelAndSolveEqualities, pushLevelAndSolveEqualitiesX , reportUnsolvedEqualities ) @@ -2955,21 +2955,21 @@ tcDataDefn err_ctxt roles_info tc_name mk_permissive_kind HsigFile [] = True mk_permissive_kind _ _ = False - -- In hs-boot, a 'data' declaration with no constructors + -- In an hs-boot or a signature file, + -- a 'data' declaration with no constructors -- indicates a nominally distinct abstract data type. - mk_tc_rhs HsBootFile _ [] - = return AbstractTyCon - - mk_tc_rhs HsigFile _ [] -- ditto + mk_tc_rhs (isHsBootOrSig -> True) _ [] = return AbstractTyCon mk_tc_rhs _ tycon data_cons = case new_or_data of - DataType -> return (mkDataTyConRhs data_cons) + DataType -> return $ + mkLevPolyDataTyConRhs + (isFixedRuntimeRepKind (tyConResKind tycon)) + data_cons NewType -> assert (not (null data_cons)) $ mkNewTyConRhs tc_name tycon (head data_cons) - ------------------------- kcTyFamInstEqn :: TcTyCon -> LTyFamInstEqn GhcRn -> TcM () -- Used for the equations of a closed type family only @@ -4372,10 +4372,11 @@ checkValidDataCon dflags existential_ok tc con -- If we are dealing with a newtype, we allow representation -- polymorphism regardless of whether or not UnliftedNewtypes -- is enabled. A later check in checkNewDataCon handles this, - -- producing a better error message than checkForLevPoly would. + -- producing a better error message than checkTypeHasFixedRuntimeRep would. ; unless (isNewTyCon tc) $ checkNoErrs $ - mapM_ (checkForLevPoly LevityCheckInValidDataCon) (map scaledThing $ dataConOrigArgTys con) + mapM_ (checkTypeHasFixedRuntimeRep FixedRuntimeRepDataConField) + (map scaledThing $ dataConOrigArgTys con) -- the checkNoErrs is to prevent a panic in isVanillaDataCon -- (called a a few lines down), which can fall over if there is a -- bang on a representation-polymorphic argument. This is #18534, @@ -4587,12 +4588,11 @@ checkValidClass cls -- newBoard :: MonadState b m => m () -- Here, MonadState has a fundep m->b, so newBoard is fine - -- a method cannot be representation-polymorphic, as we have to - -- store the method in a dictionary - -- example of what this prevents: - -- class BoundedX (a :: TYPE r) where minBound :: a - -- See Note [Representation polymorphism checking] in GHC.HsToCore.Monad - ; checkForLevPoly LevityCheckInValidClass tau1 + -- NB: we don't check that the class method is not representation-polymorphic here, + -- as GHC.TcGen.TyCl.tcClassSigType already includes a subtype check that guarantees + -- typeclass methods always have kind 'Type'. + -- + -- Test case: rep-poly/RepPolyClassMethod. ; unless constrained_class_methods $ mapM_ check_constraint (tail (cls_pred:op_theta)) diff --git a/compiler/GHC/Tc/TyCl/Build.hs b/compiler/GHC/Tc/TyCl/Build.hs index 2d0309db54..7206fe70bd 100644 --- a/compiler/GHC/Tc/TyCl/Build.hs +++ b/compiler/GHC/Tc/TyCl/Build.hs @@ -52,11 +52,11 @@ mkNewTyConRhs tycon_name tycon con = do { co_tycon_name <- newImplicitBinder tycon_name mkNewTyCoOcc ; let nt_ax = mkNewTypeCoAxiom co_tycon_name tycon etad_tvs etad_roles etad_rhs ; traceIf (text "mkNewTyConRhs" <+> ppr nt_ax) - ; return (NewTyCon { data_con = con, - nt_rhs = rhs_ty, - nt_etad_rhs = (etad_tvs, etad_rhs), - nt_co = nt_ax, - nt_lev_poly = isKindLevPoly res_kind } ) } + ; return (NewTyCon { data_con = con, + nt_rhs = rhs_ty, + nt_etad_rhs = (etad_tvs, etad_rhs), + nt_co = nt_ax, + nt_fixed_rep = isFixedRuntimeRepKind res_kind } ) } -- Coreview looks through newtypes with a Nothing -- for nt_co, or uses explicit coercions otherwise where @@ -292,7 +292,8 @@ buildClass tycon_name binders roles fds Nothing ; tc_rep_name <- newTyConRepName tycon_name ; let univ_tvs = binderVars binders tycon = mkClassTyCon tycon_name binders roles - AbstractTyCon rec_clas tc_rep_name + AbstractTyCon + rec_clas tc_rep_name result = mkAbstractClass tycon_name univ_tvs fds tycon ; traceIf (text "buildClass" <+> ppr tycon) ; return result } diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index 386c657aba..23c9fd8fff 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -750,7 +750,10 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env ; rep_tc_name <- newFamInstTyConName lfam_name pats ; axiom_name <- newFamInstAxiomName lfam_name [pats] ; tc_rhs <- case new_or_data of - DataType -> return (mkDataTyConRhs data_cons) + DataType -> return $ + mkLevPolyDataTyConRhs + (isFixedRuntimeRepKind final_res_kind) + data_cons NewType -> assert (not (null data_cons)) $ mkNewTyConRhs rep_tc_name rec_rep_tc (head data_cons) @@ -1333,8 +1336,9 @@ addDFunPrags dfun_id sc_meth_ids where con_app = mkLams dfun_bndrs $ mkApps (Var (dataConWrapId dict_con)) dict_args - -- mkApps is OK because of the checkForLevPoly call in checkValidClass - -- See Note [Representation polymorphism checking] in GHC.HsToCore.Monad + -- This application will satisfy the Core invariants + -- from Note [Representation polymorphism invariants] in GHC.Core, + -- because typeclass method types are never unlifted. dict_args = map Type inst_tys ++ [mkVarApps (Var id) dfun_bndrs | id <- sc_meth_ids] diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index 7c7b2df772..398234fa5d 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -239,6 +239,19 @@ data Ct -- look like this, with the payload in an -- auxiliary type + -- | A special canonical constraint. + -- + -- When the 'SpecialPred' is 'ConcretePrimPred': + -- + -- - `cc_ev` is Wanted, + -- - `cc_xi = ty`, where `ty` cannot be decomposed any further. + -- See Note [Canonical Concrete# constraints] in GHC.Tc.Solver.Canonical. + | CSpecialCan { + cc_ev :: CtEvidence, + cc_special_pred :: SpecialPred, + cc_xi :: Xi + } + ------------ -- | A 'CanEqLHS' is a type that can appear on the left of a canonical -- equality: a type variable or exactly-saturated type family application. @@ -612,6 +625,8 @@ instance Outputable Ct where CQuantCan (QCI { qci_pend_sc = pend_sc }) | pend_sc -> text "CQuantCan(psc)" | otherwise -> text "CQuantCan" + CSpecialCan { cc_special_pred = special_pred } -> + text "CSpecialCan" <> parens (ppr special_pred) ----------------------------------- -- | Is a type a canonical LHS? That is, is it a tyvar or an exactly-saturated diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs index e260976c38..cad95a5242 100644 --- a/compiler/GHC/Tc/Types/Evidence.hs +++ b/compiler/GHC/Tc/Types/Evidence.hs @@ -9,7 +9,7 @@ module GHC.Tc.Types.Evidence ( HsWrapper(..), (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, collectHsWrapBinders, - mkWpFun, idHsWrapper, isIdHsWrapper, + idHsWrapper, isIdHsWrapper, pprHsWrapper, hsWrapDictBinders, -- * Evidence bindings @@ -225,7 +225,7 @@ data HsWrapper -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. []) -- But ([] a) `WpCompose` ([] b) = ([] b a) - | WpFun HsWrapper HsWrapper (Scaled TcType) SDoc + | WpFun HsWrapper HsWrapper (Scaled TcType) -- (WpFun wrap1 wrap2 (w, t1))[e] = \(x:_w t1). wrap2[ e wrap1[x] ] -- So note that if wrap1 :: exp_arg <= act_arg -- wrap2 :: act_res <= exp_res @@ -233,9 +233,8 @@ data HsWrapper -- This isn't the same as for mkFunCo, but it has to be this way -- because we can't use 'sym' to flip around these HsWrappers -- The TcType is the "from" type of the first wrapper - -- The SDoc explains the circumstances under which we have created this - -- WpFun, in case we run afoul of representation polymorphism restrictions in - -- the desugarer. See Note [Representation polymorphism checking] in GHC.HsToCore.Monad + -- + -- Use 'mkWpFun' to construct such a wrapper. | WpCast TcCoercionR -- A cast: [] `cast` co -- Guaranteed not the identity coercion @@ -256,45 +255,7 @@ data HsWrapper | WpMultCoercion Coercion -- Require that a Coercion be reflexive; otherwise, -- error in the desugarer. See GHC.Tc.Utils.Unify -- Note [Wrapper returned from tcSubMult] - --- Cannot derive Data instance because SDoc is not Data (it stores a function). --- So we do it manually: -instance Data.Data HsWrapper where - gfoldl _ z WpHole = z WpHole - gfoldl k z (WpCompose a1 a2) = z WpCompose `k` a1 `k` a2 - gfoldl k z (WpFun a1 a2 a3 _) = z wpFunEmpty `k` a1 `k` a2 `k` a3 - gfoldl k z (WpCast a1) = z WpCast `k` a1 - gfoldl k z (WpEvLam a1) = z WpEvLam `k` a1 - gfoldl k z (WpEvApp a1) = z WpEvApp `k` a1 - gfoldl k z (WpTyLam a1) = z WpTyLam `k` a1 - gfoldl k z (WpTyApp a1) = z WpTyApp `k` a1 - gfoldl k z (WpLet a1) = z WpLet `k` a1 - gfoldl k z (WpMultCoercion a1) = z WpMultCoercion `k` a1 - - gunfold k z c = case Data.constrIndex c of - 1 -> z WpHole - 2 -> k (k (z WpCompose)) - 3 -> k (k (k (z wpFunEmpty))) - 4 -> k (z WpCast) - 5 -> k (z WpEvLam) - 6 -> k (z WpEvApp) - 7 -> k (z WpTyLam) - 8 -> k (z WpTyApp) - 9 -> k (z WpLet) - _ -> k (z WpMultCoercion) - - toConstr WpHole = wpHole_constr - toConstr (WpCompose _ _) = wpCompose_constr - toConstr (WpFun _ _ _ _) = wpFun_constr - toConstr (WpCast _) = wpCast_constr - toConstr (WpEvLam _) = wpEvLam_constr - toConstr (WpEvApp _) = wpEvApp_constr - toConstr (WpTyLam _) = wpTyLam_constr - toConstr (WpTyApp _) = wpTyApp_constr - toConstr (WpLet _) = wpLet_constr - toConstr (WpMultCoercion _) = wpMultCoercion_constr - - dataTypeOf _ = hsWrapper_dataType + deriving Data.Data -- | The Semigroup instance is a bit fishy, since @WpCompose@, as a data -- constructor, is "syntactic" and not associative. Concretely, if @a@, @b@, @@ -315,50 +276,11 @@ instance S.Semigroup HsWrapper where instance Monoid HsWrapper where mempty = WpHole -hsWrapper_dataType :: Data.DataType -hsWrapper_dataType - = Data.mkDataType "HsWrapper" - [ wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr - , wpEvLam_constr, wpEvApp_constr, wpTyLam_constr, wpTyApp_constr - , wpLet_constr, wpMultCoercion_constr ] - -wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr, wpEvLam_constr, - wpEvApp_constr, wpTyLam_constr, wpTyApp_constr, wpLet_constr, - wpMultCoercion_constr :: Data.Constr -wpHole_constr = mkHsWrapperConstr "WpHole" -wpCompose_constr = mkHsWrapperConstr "WpCompose" -wpFun_constr = mkHsWrapperConstr "WpFun" -wpCast_constr = mkHsWrapperConstr "WpCast" -wpEvLam_constr = mkHsWrapperConstr "WpEvLam" -wpEvApp_constr = mkHsWrapperConstr "WpEvApp" -wpTyLam_constr = mkHsWrapperConstr "WpTyLam" -wpTyApp_constr = mkHsWrapperConstr "WpTyApp" -wpLet_constr = mkHsWrapperConstr "WpLet" -wpMultCoercion_constr = mkHsWrapperConstr "WpMultCoercion" - -mkHsWrapperConstr :: String -> Data.Constr -mkHsWrapperConstr name = Data.mkConstr hsWrapper_dataType name [] Data.Prefix - -wpFunEmpty :: HsWrapper -> HsWrapper -> Scaled TcType -> HsWrapper -wpFunEmpty c1 c2 t1 = WpFun c1 c2 t1 empty - (<.>) :: HsWrapper -> HsWrapper -> HsWrapper WpHole <.> c = c c <.> WpHole = c c1 <.> c2 = c1 `WpCompose` c2 -mkWpFun :: HsWrapper -> HsWrapper - -> (Scaled TcType) -- the "from" type of the first wrapper - -> TcType -- either type of the second wrapper (used only when the - -- second wrapper is the identity) - -> SDoc -- what caused you to want a WpFun? Something like "When converting ..." - -> HsWrapper -mkWpFun WpHole WpHole _ _ _ = WpHole -mkWpFun WpHole (WpCast co2) (Scaled w t1) _ _ = WpCast (mkTcFunCo Representational (multToCo w) (mkTcRepReflCo t1) co2) -mkWpFun (WpCast co1) WpHole (Scaled w _) t2 _ = WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) (mkTcRepReflCo t2)) -mkWpFun (WpCast co1) (WpCast co2) (Scaled w _) _ _ = WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) co2) -mkWpFun co1 co2 t1 _ d = WpFun co1 co2 t1 d - mkWpCastR :: TcCoercionR -> HsWrapper mkWpCastR co | isTcReflCo co = WpHole @@ -420,7 +342,7 @@ hsWrapDictBinders wrap = go wrap where go (WpEvLam dict_id) = unitBag dict_id go (w1 `WpCompose` w2) = go w1 `unionBags` go w2 - go (WpFun _ w _ _) = go w + go (WpFun _ w _) = go w go WpHole = emptyBag go (WpCast {}) = emptyBag go (WpEvApp {}) = emptyBag @@ -1033,8 +955,8 @@ pprHsWrapper wrap pp_thing_inside -- False <=> appears as body of let or lambda help it WpHole = it help it (WpCompose f1 f2) = help (help it f2) f1 - help it (WpFun f1 f2 (Scaled w t1) _) = add_parens $ text "\\(x" <> dcolon <> brackets (ppr w) <> ppr t1 <> text ")." <+> - help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False + help it (WpFun f1 f2 (Scaled w t1)) = add_parens $ text "\\(x" <> dcolon <> brackets (ppr w) <> ppr t1 <> text ")." <+> + help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False help it (WpCast co) = add_parens $ sep [it False, nest 2 (text "|>" <+> pprParendCo co)] help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)] diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs index 3d55427ae6..25c96b6437 100644 --- a/compiler/GHC/Tc/Types/Origin.hs +++ b/compiler/GHC/Tc/Types/Origin.hs @@ -21,7 +21,15 @@ module GHC.Tc.Types.Origin ( pprCtOrigin, isGivenOrigin, -- CtOrigin and CallStack - isPushCallStackOrigin, callStackOriginFS + isPushCallStackOrigin, callStackOriginFS, + -- FixedRuntimeRep origin + FRROrigin(..), pprFRROrigin, + StmtOrigin(..), + + -- Arrow command origin + FRRArrowOrigin(..), pprFRRArrowOrigin, + -- HsWrapper WpFun origin + WpFunOrigin(..), pprWpFunOrigin, ) where @@ -226,8 +234,6 @@ data SkolemInfo -- The pattern MkT x will allocate an existential type -- variable for 'a'. - | ArrowSkol -- An arrow form (see GHC.Tc.Gen.Arrow) - | IPSkol [HsIPName] -- Binding site of an implicit parameter | RuleSkol RuleName -- The LHS of a RULE @@ -272,7 +278,6 @@ pprSkolInfo (InstSC n) = text "the instance declaration" <> whenPprDebug pprSkolInfo FamInstSkol = text "a family instance declaration" pprSkolInfo BracketSkol = text "a Template Haskell bracket" pprSkolInfo (RuleSkol name) = text "the RULE" <+> pprRuleName name -pprSkolInfo ArrowSkol = text "an arrow form" pprSkolInfo (PatSkol cl mc) = sep [ pprPatSkolInfo cl , text "in" <+> pprMatchContext mc ] pprSkolInfo (InferSkol ids) = hang (text "the inferred type" <> plural ids <+> text "of") @@ -437,6 +442,7 @@ data CtOrigin | MCompPatOrigin (LPat GhcRn) -- Arising from a failable pattern in a -- monad comprehension | ProcOrigin -- Arising from a proc expression + | ArrowCmdOrigin -- Arising from an arrow command | AnnOrigin -- An annotation | FunDepOrigin1 -- A functional dependency from combining @@ -460,15 +466,25 @@ data CtOrigin -- the user should never see this one, -- unless ImpredicativeTypes is on, where all -- bets are off - | InstProvidedOrigin Module ClsInst - -- Skolem variable arose when we were testing if an instance - -- is solvable or not. + + -- | Testing whether the constraint associated with an instance declaration + -- in a signature file is satisfied upon instantiation. + -- + -- Test cases: backpack/should_fail/bkpfail{11,43}.bkp + | InstProvidedOrigin + Module -- ^ Module in which the instance was declared + ClsInst -- ^ The declared typeclass instance + | NonLinearPatternOrigin | UsageEnvironmentOf Name | CycleBreakerOrigin CtOrigin -- origin of the original constraint -- See Detail (7) of Note [Type variable cycles] in GHC.Tc.Solver.Canonical + | FixedRuntimeRepOrigin + !Type -- ^ The type being checked for representation polymorphism. + -- We record it here for access in 'GHC.Tc.Errors.mkFRRErr'. + !FRROrigin -- An origin is visible if the place where the constraint arises is manifest -- in user code. Currently, all origins are visible except for invisible @@ -637,6 +653,12 @@ pprCtOrigin (InstProvidedOrigin mod cls_inst) pprCtOrigin (CycleBreakerOrigin orig) = pprCtOrigin orig +pprCtOrigin (FixedRuntimeRepOrigin _ frrOrig) + -- We ignore the type argument, as we would prefer + -- to report all types that don't have a fixed runtime representation at once, + -- in 'GHC.Tc.Errors.mkFRRErr'. + = pprFRROrigin frrOrig + pprCtOrigin simple_origin = ctoHerald <+> pprCtO simple_origin @@ -668,6 +690,7 @@ pprCtO DefaultOrigin = text "a 'default' declaration" pprCtO DoOrigin = text "a do statement" pprCtO MCompOrigin = text "a statement in a monad comprehension" pprCtO ProcOrigin = text "a proc expression" +pprCtO ArrowCmdOrigin = text "an arrow command" pprCtO AnnOrigin = text "an annotation" pprCtO (ExprHoleOrigin occ) = text "a use of" <+> quotes (ppr occ) pprCtO (TypeHoleOrigin occ) = text "a use of wildcard" <+> quotes (ppr occ) @@ -696,6 +719,7 @@ pprCtO (Shouldn'tHappenOrigin note) = text note pprCtO (ProvCtxtOrigin {}) = text "a provided constraint" pprCtO (InstProvidedOrigin {}) = text "a provided constraint" pprCtO (CycleBreakerOrigin orig) = pprCtO orig +pprCtO (FixedRuntimeRepOrigin {}) = text "a representation polymorphism check" {- ********************************************************************* * * @@ -717,3 +741,317 @@ callStackOriginFS :: CtOrigin -> FastString -- This is the string that appears in the CallStack callStackOriginFS (OccurrenceOf fun) = occNameFS (getOccName fun) callStackOriginFS orig = mkFastString (showSDocUnsafe (pprCtO orig)) + +{- +************************************************************************ +* * + Checking for representation polymorphism +* * +************************************************************************ + +Note [Reporting representation-polymorphism errors] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When we emit a 'Concrete#' Wanted constraint using GHC.Tc.Utils.Concrete.hasFixedRuntimeRep, +we provide a 'CtOrigin' using the 'FixedRuntimeRepOrigin' constructor of, +which keeps track of two things: + - the type which we want to ensure has a fixed runtime representation, + - the 'FRROrigin' explaining the nature of the check, e.g. a pattern, + a function application, a record update, ... + +If the constraint goes unsolved, we report it as follows: + - we detect that the unsolved Wanted is a Concrete# constraint in + GHC.Tc.Errors.reportWanteds using is_FRR, + - we assemble an error message in GHC.Tc.Errors.mkFRRErr. + +For example, if we try to write the program + + foo :: forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). a -> b -> () + foo x y = () + +we will get two unsolved Concrete# wanted constraints, namely +'Concrete# r1' and 'Concrete# r2', and their 'CtOrigin's will be: + + FixedRuntimeRepOrigin a (FRRVarPattern x) + FixedRuntimeRepOrigin b (FRRVarPattern y) + +These constraints will be processed in tandem by mkFRRErr, +producing an error message of the form: + + Representation-polymorphic types are not allowed here. + * The variable 'x' bound by the pattern + does not have a fixed runtime representation: + a :: TYPE r1 + * The variable 'y' bound by the pattern + does not have a fixed runtime representation: + b :: TYPE r2 +-} + +-- | Where are we checking that a type has a fixed runtime representation? +-- Equivalently: what is the origin of an emitted 'Concrete#' constraint? +data FRROrigin + + -- | Function arguments must have a fixed runtime representation. + -- + -- Test case: RepPolyApp. + = FRRApp !(HsExpr GhcRn) + + -- | Record fields in record updates must have a fixed runtime representation. + -- + -- Test case: RepPolyRecordUpdate. + | FRRRecordUpdate !RdrName !(HsExpr GhcRn) + + -- | Variable binders must have a fixed runtime representation. + -- + -- Test cases: LevPolyLet, RepPolyPatBind. + | FRRBinder !Name + + -- | The type of a pattern in a match group must have a fixed runtime representation. + -- + -- This rules out: + -- - individual patterns which don't have a fixed runtime representation, + -- - a representation-polymorphic empty case statement, + -- - representation-polymorphic GADT pattern matches + -- in which individual pattern types have a fixed runtime representation. + -- + -- Test cases: RepPolyRecordPattern, RepPolyUnboxedPatterns, + -- RepPolyBinder, RepPolyWildcardPattern, RepPolyMatch, + -- RepPolyNPlusK, RepPolyPatBind, T20426. + | FRRMatch !(HsMatchContext GhcTc) !Int + + -- | An instantiation of a newtype/data constructor in which + -- one of the remaining arguments types does not have a fixed runtime representation. + -- + -- Test case: UnliftedNewtypesLevityBinder. + | FRRDataConArg !DataCon !Int + + -- | An instantiation of an 'Id' with no binding (e.g. `coerce`, `unsafeCoerce#`) + -- in which one of the remaining arguments types does not have a fixed runtime representation. + -- + -- Test cases: RepPolyWrappedVar, T14561, UnliftedNewtypesCoerceFail. + | FRRNoBindingResArg !Id !Int + + -- | Arguments to unboxed tuples must have fixed runtime representations. + -- + -- Test case: RepPolyTuple. + | FRRTupleArg !Int + + -- | Tuple sections must have a fixed runtime representation. + -- + -- Test case: RepPolyTupleSection. + | FRRTupleSection !Int + + -- | Unboxed sums must have a fixed runtime representation. + -- + -- Test cases: RepPolySum. + | FRRUnboxedSum + + -- | The body of a @do@ expression or a monad comprehension must + -- have a fixed runtime representation. + -- + -- Test cases: RepPolyDoBody{1,2}, RepPolyMcBody. + | FRRBodyStmt !StmtOrigin !Int + + -- | Arguments to a guard in a monad comprehesion must have + -- a fixed runtime representation. + -- + -- Test case: RepPolyMcGuard. + | FRRBodyStmtGuard + + -- | Arguments to `(>>=)` arising from a @do@ expression + -- or a monad comprehension must have a fixed runtime representation. + -- + -- Test cases: RepPolyDoBind, RepPolyMcBind. + | FRRBindStmt !StmtOrigin + + -- | A value bound by a pattern guard must have a fixed runtime representation. + -- + -- Test cases: none. + | FRRBindStmtGuard + + -- | A representation-polymorphism check arising from arrow notation. + -- + -- See 'FRRArrowOrigin' for more details. + | FRRArrow !FRRArrowOrigin + + -- | A representation-polymorphic check arising from an 'HsWrapper'. + -- + -- See 'WpFunOrigin' for more details. + | FRRWpFun !WpFunOrigin + +-- | Print the context for a @FixedRuntimeRep@ representation-polymorphism check. +-- +-- Note that this function does not include the specific 'RuntimeRep' +-- which is not fixed. That information is added by 'GHC.Tc.Errors.mkFRRErr'. +pprFRROrigin :: FRROrigin -> SDoc +pprFRROrigin (FRRApp arg) + = sep [ text "The function argument" + , nest 2 $ quotes (ppr arg) + , text "does not have a fixed runtime representation"] +pprFRROrigin (FRRRecordUpdate lbl _arg) + = hsep [ text "The record update at field" + , quotes (ppr lbl) + , text "does not have a fixed runtime representation"] +pprFRROrigin (FRRBinder binder) + = hsep [ text "The binder" + , quotes (ppr binder) + , text "does not have a fixed runtime representation"] +pprFRROrigin (FRRMatch matchCtxt i) + = vcat [ text "The type of the" <+> speakNth i <+> text "pattern in the" <+> pprMatchContextNoun matchCtxt + , text "does not have a fixed runtime representation"] +pprFRROrigin (FRRDataConArg con i) + = sep [ text "The" <+> what + , text "does not have a fixed runtime representation"] + where + what :: SDoc + what + | isNewDataCon con + = text "newtype constructor argument" + | otherwise + = text "data constructor argument in" <+> speakNth i <+> text "position" +pprFRROrigin (FRRNoBindingResArg fn i) + = vcat [ text "Unsaturated use of a representation-polymorphic primitive function." + , text "The" <+> speakNth i <+> text "argument of" <+> quotes (ppr $ getName fn) + , text "does not have a fixed runtime representation" ] +pprFRROrigin (FRRTupleArg i) + = hsep [ text "The tuple argument in" <+> speakNth i <+> text "position" + , text "does not have a fixed runtime representation"] +pprFRROrigin (FRRTupleSection i) + = hsep [ text "The tuple section does not have a fixed runtime representation" + , text "in the" <+> speakNth i <+> text "position" ] +pprFRROrigin FRRUnboxedSum + = hsep [ text "The unboxed sum result type" + , text "does not have a fixed runtime representation"] +pprFRROrigin (FRRBodyStmt stmtOrig i) + = vcat [ text "The" <+> speakNth i <+> text "argument to (>>)" <> comma + , text "arising from the" <+> ppr stmtOrig <> comma + , text "does not have a fixed runtime representation" ] +pprFRROrigin FRRBodyStmtGuard + = vcat [ text "The argument to" <+> quotes (text "guard") <> comma + , text "arising from the" <+> ppr MonadComprehension <> comma + , text "does not have a fixed runtime representation" ] +pprFRROrigin (FRRBindStmt stmtOrig) + = vcat [ text "The first argument to (>>=)" <> comma + , text "arising from the" <+> ppr stmtOrig <> comma + , text "does not have a fixed runtime representation" ] +pprFRROrigin FRRBindStmtGuard + = hsep [ text "The return type of the bind statement" + , text "does not have a fixed runtime representation" ] +pprFRROrigin (FRRArrow arrowOrig) + = pprFRRArrowOrigin arrowOrig +pprFRROrigin (FRRWpFun wpFunOrig) + = pprWpFunOrigin wpFunOrig + +instance Outputable FRROrigin where + ppr = pprFRROrigin + +-- | Are we in a @do@ expression or a monad comprehension? +-- +-- This datatype is only used to report this context to the user in error messages. +data StmtOrigin + = MonadComprehension + | DoNotation + +instance Outputable StmtOrigin where + ppr MonadComprehension = text "monad comprehension" + ppr DoNotation = quotes ( text "do" ) <+> text "statement" + +{- ********************************************************************* +* * + FixedRuntimeRep: arrows +* * +********************************************************************* -} + +-- | While typechecking arrow notation, in which context +-- did a representation polymorphism check arise? +-- +-- See 'FRROrigin' for more general origins of representation polymorphism checks. +data FRRArrowOrigin + + -- | The result of an arrow command does not have a fixed runtime representation. + -- + -- Test case: RepPolyArrowCmd. + = ArrowCmdResTy !(HsCmd GhcRn) + + -- | The argument to an arrow in an arrow command application does not have + -- a fixed runtime representation. + -- + -- Test cases: none. + | ArrowCmdApp !(HsCmd GhcRn) !(HsExpr GhcRn) + + -- | A function in an arrow application does not have + -- a fixed runtime representation. + -- + -- Test cases: none. + | ArrowCmdArrApp !(HsExpr GhcRn) !(HsExpr GhcRn) !HsArrAppType + + -- | A pattern in an arrow command abstraction does not have + -- a fixed runtime representation. + -- + -- Test cases: none. + | ArrowCmdLam !Int + + -- | The overall type of an arrow proc expression does not have + -- a fixed runtime representation. + -- + -- Test case: RepPolyArrowFun. + | ArrowFun !(HsExpr GhcRn) + +pprFRRArrowOrigin :: FRRArrowOrigin -> SDoc +pprFRRArrowOrigin (ArrowCmdResTy cmd) + = vcat [ hang (text "The arrow command") 2 (quotes (ppr cmd)) + , text "does not have a fixed runtime representation" ] +pprFRRArrowOrigin (ArrowCmdApp fun arg) + = vcat [ text "In the arrow command application of" + , nest 2 (quotes (ppr fun)) + , text "to" + , nest 2 (quotes (ppr arg)) <> comma + , text "the argument does not have a fixed runtime representation" ] +pprFRRArrowOrigin (ArrowCmdArrApp fun arg ho_app) + = vcat [ text "In the" <+> pprHsArrType ho_app <+> text "of" + , nest 2 (quotes (ppr fun)) + , text "to" + , nest 2 (quotes (ppr arg)) <> comma + , text "the function does not have a fixed runtime representation" ] +pprFRRArrowOrigin (ArrowCmdLam i) + = vcat [ text "The" <+> speakNth i <+> text "pattern of the arrow command abstraction" + , text "does not have a fixed runtime representation" ] +pprFRRArrowOrigin (ArrowFun fun) + = vcat [ text "The return type of the arrow function" + , nest 2 (quotes (ppr fun)) + , text "does not have a fixed runtime representation" ] + +instance Outputable FRRArrowOrigin where + ppr = pprFRRArrowOrigin + +{- ********************************************************************* +* * + FixedRuntimeRep: HsWrapper WpFun origin +* * +********************************************************************* -} + +-- | While typechecking a 'WpFun' 'HsWrapper', in which context +-- did a representation polymorphism check arise? +-- +-- See 'FRROrigin' for more general origins of representation polymorphism checks. +data WpFunOrigin + = WpFunSyntaxOp !CtOrigin + | WpFunViewPat !(HsExpr GhcRn) + | WpFunFunTy !Type + | WpFunFunExpTy !ExpType + +pprWpFunOrigin :: WpFunOrigin -> SDoc +pprWpFunOrigin (WpFunSyntaxOp orig) + = vcat [ text "When checking a rebindable syntax operator arising from" + , nest 2 (ppr orig) ] +pprWpFunOrigin (WpFunViewPat expr) + = vcat [ text "When checking the view pattern function:" + , nest 2 (ppr expr) ] +pprWpFunOrigin (WpFunFunTy fun_ty) + = vcat [ text "When inferring the argument type of a function with type" + , nest 2 (ppr fun_ty) ] +pprWpFunOrigin (WpFunFunExpTy fun_ty) + = vcat [ text "When inferring the argument type of a function with expected type" + , nest 2 (ppr fun_ty) ] + +instance Outputable WpFunOrigin where + ppr = pprWpFunOrigin diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs new file mode 100644 index 0000000000..0b20a1af9d --- /dev/null +++ b/compiler/GHC/Tc/Utils/Concrete.hs @@ -0,0 +1,521 @@ +{-# LANGUAGE MultiWayIf #-} + +module GHC.Tc.Utils.Concrete + ( -- * Creating/emitting 'Concrete#' constraints + hasFixedRuntimeRep + , newConcretePrimWanted + -- * HsWrapper: checking for representation-polymorphism + , mkWpFun + ) + where + +import GHC.Prelude + +import GHC.Core.Coercion +import GHC.Core.TyCo.Rep + +import GHC.Tc.Utils.Monad +import GHC.Tc.Utils.TcType ( TcType, mkTyConApp ) +import GHC.Tc.Utils.TcMType ( newCoercionHole, newFlexiTyVarTy ) +import GHC.Tc.Types.Constraint +import GHC.Tc.Types.Evidence +import GHC.Tc.Types.Origin ( CtOrigin(..), FRROrigin(..), WpFunOrigin(..) ) + +import GHC.Builtin.Types ( unliftedTypeKindTyCon, liftedTypeKindTyCon ) +import GHC.Builtin.Types.Prim ( concretePrimTyCon ) + +import GHC.Types.Basic ( TypeOrKind(KindLevel) ) + +import GHC.Core.Type ( isConcrete, typeKind ) + +{- Note [Concrete overview] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Special predicates of the form `Concrete# ty` are used +to check, in the typechecker, that certain types have a fixed runtime representation. +We give here an overview of the various moving parts, to serve +as a central point of reference for this topic. + + * Representation polymorphism + Note [Representation polymorphism invariants] in GHC.Core + Note [Representation polymorphism checking] + + The first note explains why we require that certain types have + a fixed runtime representation. + + The second note details why we sometimes need a constraint to + perform such checks in the typechecker: we might not know immediately + whether a type has a fixed runtime representation. For example, we might + need further unification to take place before being able to decide. + So, instead of checking immediately, we emit a constraint. + + * What does it mean for a type to be concrete? + Note [Concrete types] + Note [The Concrete mechanism] + + The predicate 'Concrete# ty' is satisfied when we can produce + a coercion + + co :: ty ~ concrete_ty + + where 'concrete_ty' consists only of concrete types (no type variables, + no type families). + + The first note explains more precisely what it means for a type to be concrete. + The second note explains how this relates to the `Concrete#` predicate, + and explains that the implementation is happening in two phases (PHASE 1 and PHASE 2). + In PHASE 1 (the current implementation) we only allow trivial evidence + of the form `co = Refl`. + + * Fixed runtime representation vs fixed RuntimeRep + Note [Fixed RuntimeRep] + + We currently enforce the representation-polymorphism invariants by checking + that binders and function arguments have a "fixed RuntimeRep". + That is, `ty :: ki` has a "fixed RuntimeRep" if we can solve `Concrete# ki`. + + This is slightly less general than we might like, as this rules out + types with kind `TYPE (BoxedRep l)`: we know that this will be represented + by a pointer, which should be enough to go on in many situations. + + * When do we emit 'Concrete#' constraints? + Note [hasFixedRuntimeRep] + + We introduce 'Concrete#' constraints to satisfy the representation-polymorphism + invariants outlined in Note [Representation polymorphism invariants] in GHC.Core, + which mostly amounts to the following two cases: + + - checking that a binder has a fixed runtime representation, + - checking that a function argument has a fixed runtime representation. + + The note explains precisely how we emit these 'Concrete#' constraints. + + * How do we solve Concrete# constraints? + Note [Solving Concrete# constraints] in GHC.Tc.Instance.Class + + Concrete# constraints are solved through two mechanisms, + which are both explained further in the note: + + - by decomposing them, e.g. `Concrete# (TYPE r)` is turned + into `Concrete# r` (canonicalisation of `Concrete#` constraints), + - by using 'Concrete' instances (top-level interactions). + The note explains that the evidence we get from using such 'Concrete' + instances can only ever be Refl, even in PHASE 2. + + * Reporting unsolved Concrete# constraints + Note [Reporting representation-polymorphism errors] in GHC.Tc.Types.Origin + + When we emit a 'Concrete#' constraint, we also provide a 'FRROrigin' + which gives context about the check being done. This origin gets reported + to the user if we end up with an unsolved Wanted 'Concrete#' constraint. + +Note [Representation polymorphism checking] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +According to the "Levity Polymorphism" paper (PLDI '17), +there are two places in which we must know that a type has a +fixed runtime representation, as explained in + Note [Representation polymorphism invariants] in GHC.Core: + + I1. the type of a bound term-level variable, + I2. the type of an argument to a function. + +The paper explains the restrictions more fully, but briefly: +expressions in these contexts need to be stored in registers, and it's +hard (read: impossible) to store something that does not have a +fixed runtime representation. + +In practice, we enforce these types to have a /fixed RuntimeRep/, which is slightly +stronger, as explained in Note [Fixed RuntimeRep]. + +There are two different ways we check whether a given type +has a fixed runtime representation, both in the typechecker: + + 1. When typechecking type declarations (e.g. datatypes, typeclass, pattern synonyms), + under the GHC.Tc.TyCl module hierarchy. + In these situations, we can immediately reject bad representation polymorphism. + + For instance, the following datatype declaration + + data Foo (r :: RuntimeRep) (a :: TYPE r) = Foo a + + is rejected in GHC.Tc.TyCl.checkValidDataCon upon seeing that the type 'a' + is representation-polymorphic. + + Such checks are done using `GHC.Tc.Utils.TcMType.checkTypeHasFixedRuntimeRep`, + with `GHC.Tc.Errors.Types.FixedRuntimeRepProvenance` describing the different + contexts in which bad representation polymorphism can occur while validity checking. + + 2. When typechecking value-level declarations (functions, expressions, patterns, ...), + under the GHC.Tc.Gen module hierarchy. + In these situations, the typechecker might need to do some work to figure out + whether a type has a fixed runtime representation or not. For instance, + GHC might introduce a metavariable (rr :: RuntimeRep), which is only later + (through constraint solving) discovered to be equal to FloatRep. + + This is handled by the Concrete mechanism outlined in + Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete. + See Note [Concrete overview] in GHC.Tc.Utils.Concrete for an overview + of the various moving parts. + + The idea is that, to guarantee that a type (rr :: RuntimeRep) is + representation-monomorphic, we emit a 'Concrete# rr' Wanted constraint. + If GHC can solve this constraint, it means 'rr' is monomorphic, and we + are OK to proceed. Otherwise, we report this unsolved Wanted in the form + of a representation-polymorphism error. The different contexts in which + such constraints arise are enumerated in 'FRROrigin'. + +Note [Concrete types] +~~~~~~~~~~~~~~~~~~~~~ +Definition: a type is /concrete/ + iff it consists of a tree of concrete type constructors + See GHC.Core.Type.isConcrete + +Definition: a /concrete type constructor/ is defined by + - a promoted data constructor + - a class, data type or newtype + - a primitive type like Array# or Int# + - an abstract type as defined in a Backpack signature file + (see Note [Synonyms implement abstract data] in GHC.Tc.Module) + In particular, type and data families are not concrete. + See GHC.Core.TyCon.isConcreteTyCon. + +Examples of concrete types: + Lifted, BoxedRep Lifted, TYPE (BoxedRep Lifted) are all concrete +Examples of non-concrete types + F Int, TYPE (F Int), TYPE r, a Int + NB: (F Int) is not concrete because F is a type function + +Note [The Concrete mechanism] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +As explained in (2) in Note [Representation polymorphism checking], +to check (ty :: ki) has a fixed runtime representation, +we emit a `Concrete# ki` constraint, where + + Concrete# :: forall k. k -> TupleRep '[] + +Such constraints get solved by decomposition, as per + Note [Canonical Concrete# constraints] in GHC.Tc.Solver.Canonical. +When unsolved Wanted `Concrete#` constraints remain after typechecking, +we report them as representation-polymorphism errors, using `GHC.Tc.Types.Origin.FRROrigin` +to inform the user of the context in which a fixed-runtime-rep check arose. + +-------------- +-- EVIDENCE -- +-------------- + +The evidence for a 'Concrete# ty' constraint is a nominal coercion + + co :: ty ~# concrete_ty + +where 'concrete_ty' consists only of (non-synonym) type constructors and applications +(after expanding any vanilla type synonyms). + + OK: + + TYPE FloatRep + TYPE (BoxedRep Lifted) + Type + TYPE (TupleRep '[ FloatRep, SumRep '[ IntRep, IntRep ] ]) + + Not OK: + + Type variables: + + ty + TYPE r + TYPE (BoxedRep l) + + Type family applications: + + TYPE (Id FloatRep) + +This is so that we can compute the 'PrimRep's needed to represent the type +using 'runtimeRepPrimRep', which expects to be able to read off the 'RuntimeRep', +as per Note [Getting from RuntimeRep to PrimRep] in GHC.Types.RepType. + +Note that the evidence for a `Concrete#` constraint isn't a typeclass dictionary: +like with `(~#)`, the evidence is an (unlifted) nominal coercion, which justifies defining + + Concrete# :: forall k. k -> TYPE (TupleRep '[]) + +We still need a constraint that users can write in their own programs, +so much like `(~#)` and `(~)` we also define: + + Concrete :: forall k. k -> Constraint + +The need for user-facing 'Concrete' constraints is detailed in + Note [Concrete and Concrete#] in GHC.Builtin.Types. + +------------------------- +-- PHASE 1 and PHASE 2 -- +------------------------- + +The Concrete mechanism is being implemented in two separate phases. + +In PHASE 1 (currently implemented), we never allow a 'Concrete#' constraint +to be rewritten (see e.g. GHC.Tc.Solver.Canonical.canConcretePrim). +The only allowable evidence term is Refl, which forbids any program +that requires type family evaluation in order to determine that a 'RuntimeRep' is fixed. +N.B.: we do not currently check that this invariant is upheld: as we are discarding the +evidence in PHASE 1, we no longer have access to the coercion after constraint solving +(which is the point at which we would want to check that the filled in evidence is Refl). + +In PHASE 2 (future work), we lift this restriction. To illustrate what this entails, +recall that the code generator needs to be able to compute 'PrimRep's, so that it +can put function arguments in the correct registers, etc. +As a result, we must insert additional casts in Core to ensure that no type family +reduction is needed to be able to compute 'PrimRep's. For example, the Core + + f = /\ ( a :: F Int ). \ ( x :: a ). some_expression + +is problematic when 'F' is a type family: we don't know what runtime representation to use +for 'x', so we can't compile this function (we can't evaluate type family applications +after we are done with typechecking). Instead, we ensure the 'RuntimeRep' is always +explicitly visible: + + f = /\ ( a :: F Int ). \ ( x :: ( a |> kco ) ). some_expression + +where 'kco' is the evidence for `Concrete# (F Int)`, for example if `F Int = TYPE Int#` +this would be: + + kco :: F Int ~# TYPE Int# + +As `( a |> kco ) :: TYPE Int#`, the code generator knows to use a machine-sized +integer register for `x`, and all is good again. + +Example test cases that require PHASE 2: T13105, T17021, T20363b. + +Note [Fixed RuntimeRep] +~~~~~~~~~~~~~~~~~~~~~~~ +Definition: + a type `ty :: ki` has a /fixed RuntimeRep/ + iff we can solve `Concrete# ki` + +In PHASE 1 (see Note [The Concrete mechanism]), this is equivalent to: + + a type `ty :: ki` has a /fixed RuntimeRep/ + iff `ki` is a concrete type (in the sense of Note [Concrete types]). + +This definition is crafted to be useful to satisfy the invariants of +Core; see Note [Representation polymorphism invariants] in GHC.Core. + +Notice that "fixed RuntimeRep" means (for now anyway) that + * we know the runtime representation, and + * we know the levity. + +For example (ty :: TYPE (BoxedRep l)), where `l` is a levity variable +is /not/ "fixed RuntimeRep", even though it is always represented by +a heap pointer, because we don't know the levity. In due course we +will want to make finer distinctions, as explained in the paper +Kinds are Calling Conventions [ICFP'20], but this suffices for now. + +Note [hasFixedRuntimeRep] +~~~~~~~~~~~~~~~~~~~~~~~~~ +The 'hasFixedRuntimeRep' function is responsible for taking a type 'ty' +and emitting a 'Concrete#' constraint to ensure that 'ty' has a fixed `RuntimeRep`, +as outlined in Note [The Concrete mechanism]. + +To do so, we compute the kind 'ki' of 'ty' and emit a 'Concrete# ki' constraint, +which will only be solved if we can prove that 'ty' indeed has a fixed RuntimeRep. + + [Wrinkle: Typed Template Haskell] + We don't perform any checks when type-checking a typed Template Haskell quote: + we want to allow representation polymorphic quotes, as long as they are + monomorphised at splice site. + + Example: + + Module1 + + repPolyId :: forall r (a :: TYPE r). CodeQ (a -> a) + repPolyId = [|| \ x -> x ||] + + Module2 + + import Module1 + + id1 :: Int -> Int + id1 = $$repPolyId + + id2 :: Int# -> Int# + id2 = $$repPolyId + + We implement this skip by inspecting the TH stage in `hasFixedRuntimeRep`. + + A better solution would be to use 'CodeC' constraints, as in the paper + "Staging With Class", POPL 2022 + by Ningning Xie, Matthew Pickering, Andres Löh, Nicolas Wu, Jeremy Yallop, Meng Wang + but for the moment, as we will typecheck again when splicing, + this shouldn't cause any problems in practice. See ticket #18170. + + Test case: rep-poly/T18170a. + +Note [Solving Concrete# constraints] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +The representation polymorphism checks emit 'Concrete# ty' constraints, +as explained in Note [hasFixedRuntimeRep] in GHC.Tc.Utils.Concrete. + +The main mechanism through which a `Concrete# ty` constraint is solved +is to directly inspect 'ty' to check that it is a concrete type +such as 'TYPE IntRep' or `TYPE (TupleRep '[ TupleRep '[], FloatRep ])`, +and not, e.g., a skolem type variable. + +There are, however, some interactions to take into account: + + 1. Decomposition. + + The solving of `Concrete#` constraints works recursively. + For example, to solve a Wanted `Concrete# (TYPE r)` constraint, + we decompose it, emitting a new `Concrete# @RuntimeRep r` Wanted constraint, + and use it to solve the original `Concrete# (TYPE r)` constraint. + This happens in the canonicaliser -- see GHC.Tc.Solver.Canonical.canDecomposableConcretePrim. + + Note that Decomposition fully solves `Concrete# ty` whenever `ty` is a + concrete type. For example: + + Concrete# (TYPE (BoxedRep Lifted)) + ==> (decompose) + Concrete# (BoxedRep Lifted) + ==> (decompose) + Concrete# Lifted + ==> (decompose) + <nothing, since Lifted is nullary> + + 2. Rewriting. + + In PHASE 1 (as per Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete), + we don't have to worry about a 'Concrete#' constraint being rewritten. + We only need to zonk: if e.g. a metavariable, `alpha`, gets unified with `IntRep`, + we should be able to solve `Concrete# alpha`. + + In PHASE 2, we will need to proceed as in GHC.Tc.Solver.Canonical.canClass: + if we have a constraint `Concrete# (F ty1)` and a coercion witnessing the reduction of + `F`, say `co :: F ty1 ~# ty2`, then we will solve `Concrete# (F ty1)` in terms of `Concrete# ty2`, + by rewriting the evidence for `Concrete# ty2` using `co` (see GHC.Tc.Solver.Canonical.rewriteEvidence). + + 3. Backpack + + Abstract 'TyCon's in Backpack signature files are always considered to be concrete. + This is because of the strong restrictions around how abstract types are allowed + to be implemented, as laid out in Note [Synonyms implement abstract data] in GHC.Tc.Module. + In particular, no variables or type family applications are allowed. + + Examples: backpack/should_run/T13955.bkp, rep-poly/RepPolyBackpack2. +-} + +-- | A coercion hole used to store evidence for `Concrete#` constraints. +-- +-- See Note [The Concrete mechanism]. +type ConcreteHole = CoercionHole + +-- | Evidence for a `Concrete#` constraint: +-- essentially a 'ConcreteHole' (a coercion hole) that will be filled later, +-- except: +-- +-- - we might already have the evidence now; no point in creating a coercion hole +-- in that case; +-- - we sometimes skip the check entirely, e.g. in Typed Template Haskell +-- (see [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep]). +data ConcreteEvidence + = ConcreteReflEvidence + -- ^ We have evidence right now: don't bother creating a 'ConcreteHole'. + | ConcreteTypedTHNoEvidence + -- ^ We don't emit 'Concrete#' constraints in Typed Template Haskell. + -- See [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep]. + | ConcreteHoleEvidence ConcreteHole + -- ^ The general form of evidence: a 'ConcreteHole' that should be + -- filled in later by the constraint solver, as per + -- Note [Solving Concrete# constraints]. + +-- | Check that the kind of the provided type is of the form +-- @TYPE rep@ for a __fixed__ 'RuntimeRep' @rep@. +-- +-- If this isn't immediately obvious, for instance if the 'RuntimeRep' +-- is hidden under a type-family application such as +-- +-- > ty :: TYPE (F x) +-- +-- this function will emit a new Wanted 'Concrete#' constraint. +hasFixedRuntimeRep :: FRROrigin -> Type -> TcM ConcreteEvidence +hasFixedRuntimeRep frrOrig ty + + -- Shortcut: check for 'Type' and 'UnliftedType' type synonyms. + | TyConApp tc [] <- ki + , tc == liftedTypeKindTyCon || tc == unliftedTypeKindTyCon + = return ConcreteReflEvidence + + | otherwise + = do { th_stage <- getStage + ; if + -- We have evidence for 'Concrete# ty' right now: + -- no need to emit a constraint/create an evidence hole. + | isConcrete ki + -> return ConcreteReflEvidence + + -- See [Wrinkle: Typed Template Haskell] in Note [hasFixedRuntimeRep]. + | Brack _ (TcPending {}) <- th_stage + -> return ConcreteTypedTHNoEvidence + + -- Create a new Wanted 'Concrete#' constraint and emit it. + | otherwise + -> do { loc <- getCtLocM (FixedRuntimeRepOrigin ty frrOrig) (Just KindLevel) + ; (hole, ct_ev) <- newConcretePrimWanted loc ki + ; emitSimple $ mkNonCanonical ct_ev + ; return $ ConcreteHoleEvidence hole } } + where + ki :: Kind + ki = typeKind ty + +-- | Create a new (initially unfilled) coercion hole, +-- to hold evidence for a @'Concrete#' (ty :: ki)@ constraint. +newConcreteHole :: Kind -- ^ Kind of the thing we want to ensure is concrete (e.g. 'runtimeRepTy') + -> Type -- ^ Thing we want to ensure is concrete (e.g. some 'RuntimeRep') + -> TcM ConcreteHole +newConcreteHole ki ty + = do { concrete_ty <- newFlexiTyVarTy ki + ; let co_ty = mkHeteroPrimEqPred ki ki ty concrete_ty + ; newCoercionHole co_ty } + +-- | Create a new 'Concrete#' constraint. +newConcretePrimWanted :: CtLoc -> Type -> TcM (ConcreteHole, CtEvidence) +newConcretePrimWanted loc ty + = do { let + ki :: Kind + ki = typeKind ty + ; hole <- newConcreteHole ki ty + ; let + wantedCtEv :: CtEvidence + wantedCtEv = + CtWanted + { ctev_dest = HoleDest hole + , ctev_pred = mkTyConApp concretePrimTyCon [ki, ty] + , ctev_nosh = WOnly -- WOnly, because Derived Concrete# constraints + -- aren't useful: solving a Concrete# constraint + -- can't cause any unification to take place. + , ctev_loc = loc + } + ; return (hole, wantedCtEv) } + +{-*********************************************************************** +* * + HsWrapper +* * +***********************************************************************-} + +-- | Smart constructor to create a 'WpFun' 'HsWrapper'. +-- +-- Might emit a 'Concrete#' constraint, to check for +-- representation polymorphism. This is necessary, as 'WpFun' will desugar to +-- a lambda abstraction, whose binder must have a fixed runtime representation. +mkWpFun :: HsWrapper -> HsWrapper + -> Scaled TcType -- ^ the "from" type of the first wrapper + -> TcType -- ^ either type of the second wrapper (used only when the + -- second wrapper is the identity) + -> WpFunOrigin -- ^ what caused you to want a WpFun? + -> TcM HsWrapper +mkWpFun WpHole WpHole _ _ _ = return $ WpHole +mkWpFun WpHole (WpCast co2) (Scaled w t1) _ _ = return $ WpCast (mkTcFunCo Representational (multToCo w) (mkTcRepReflCo t1) co2) +mkWpFun (WpCast co1) WpHole (Scaled w _) t2 _ = return $ WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) (mkTcRepReflCo t2)) +mkWpFun (WpCast co1) (WpCast co2) (Scaled w _) _ _ = return $ WpCast (mkTcFunCo Representational (multToCo w) (mkTcSymCo co1) co2) +mkWpFun co1 co2 t1 _ wpFunOrig + = do { _concrete_ev <- hasFixedRuntimeRep (FRRWpFun wpFunOrig) (scaledThing t1) + ; return $ WpFun co1 co2 t1 } diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs index 6977dcf105..dace3d08f6 100644 --- a/compiler/GHC/Tc/Utils/Instantiate.hs +++ b/compiler/GHC/Tc/Utils/Instantiate.hs @@ -69,12 +69,13 @@ import GHC.Tc.Types.Origin import GHC.Tc.Utils.Env import GHC.Tc.Types.Evidence import GHC.Tc.Instance.FunDeps +import GHC.Tc.Utils.Concrete import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.TcType import GHC.Tc.Errors.Types import GHC.Types.Id.Make( mkDictFunId ) -import GHC.Types.Basic ( TypeOrKind(..) ) +import GHC.Types.Basic ( TypeOrKind(..), Arity ) import GHC.Types.Error import GHC.Types.SourceText import GHC.Types.SrcLoc as SrcLoc @@ -95,7 +96,7 @@ import GHC.Unit.External import Data.List ( mapAccumL ) import qualified Data.List.NonEmpty as NE -import Control.Monad( unless ) +import Control.Monad( when, unless, void ) import Data.Function ( on ) {- @@ -740,10 +741,10 @@ just use the expression inline. -} tcSyntaxName :: CtOrigin - -> TcType -- ^ Type to instantiate it at - -> (Name, HsExpr GhcRn) -- ^ (Standard name, user name) + -> TcType -- ^ Type to instantiate it at + -> (Name, HsExpr GhcRn) -- ^ (Standard name, user name) -> TcM (Name, HsExpr GhcTc) - -- ^ (Standard name, suitable expression) + -- ^ (Standard name, suitable expression) -- USED ONLY FOR CmdTop (sigh) *** -- See Note [CmdSyntaxTable] in "GHC.Hs.Expr" @@ -755,31 +756,65 @@ tcSyntaxName orig ty (std_nm, HsVar _ (L _ user_nm)) tcSyntaxName orig ty (std_nm, user_nm_expr) = do std_id <- tcLookupId std_nm let - -- C.f. newMethodAtLoc ([tv], _, tau) = tcSplitSigmaTy (idType std_id) sigma1 = substTyWith [tv] [ty] tau -- Actually, the "tau-type" might be a sigma-type in the -- case of locally-polymorphic methods. - addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do + span <- getSrcSpanM + addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1 span) $ do -- Check that the user-supplied thing has the -- same type as the standard one. -- Tiresome jiggling because tcCheckSigma takes a located expression - span <- getSrcSpanM expr <- tcCheckPolyExpr (L (noAnnSrcSpan span) user_nm_expr) sigma1 + hasFixedRuntimeRepRes std_nm user_nm_expr sigma1 return (std_nm, unLoc expr) -syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> TidyEnv +syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> SrcSpan -> TidyEnv -> TcRn (TidyEnv, SDoc) -syntaxNameCtxt name orig ty tidy_env - = do { inst_loc <- getCtLocM orig (Just TypeLevel) - ; let msg = vcat [ text "When checking that" <+> quotes (ppr name) +syntaxNameCtxt name orig ty loc tidy_env = return (tidy_env, msg) + where + msg = vcat [ text "When checking that" <+> quotes (ppr name) <+> text "(needed by a syntactic construct)" - , nest 2 (text "has the required type:" - <+> ppr (tidyType tidy_env ty)) - , nest 2 (pprCtLoc inst_loc) ] - ; return (tidy_env, msg) } + , nest 2 (text "has the required type:" + <+> ppr (tidyType tidy_env ty)) + , nest 2 (sep [ppr orig, text "at" <+> ppr loc])] + +{- +************************************************************************ +* * + FixedRuntimeRep +* * +************************************************************************ +-} + +-- | Check that the result type of an expression has a fixed runtime representation. +-- +-- Used only for arrow operations such as 'arr', 'first', etc. +hasFixedRuntimeRepRes :: Name -> HsExpr GhcRn -> TcSigmaType -> TcM () +hasFixedRuntimeRepRes std_nm user_expr ty = mapM_ do_check mb_arity + where + do_check :: Arity -> TcM () + do_check arity = + let res_ty = nTimes arity (snd . splitPiTy) ty + in void $ hasFixedRuntimeRep (FRRArrow $ ArrowFun user_expr) res_ty + mb_arity :: Maybe Arity + mb_arity -- arity of the arrow operation, counting type-level arguments + | std_nm == arrAName -- result used as an argument in, e.g., do_premap + = Just 3 + | std_nm == composeAName -- result used as an argument in, e.g., dsCmdStmt/BodyStmt + = Just 5 + | std_nm == firstAName -- result used as an argument in, e.g., dsCmdStmt/BodyStmt + = Just 4 + | std_nm == appAName -- result used as an argument in, e.g., dsCmd/HsCmdArrApp/HsHigherOrderApp + = Just 2 + | std_nm == choiceAName -- result used as an argument in, e.g., HsCmdIf + = Just 5 + | std_nm == loopAName -- result used as an argument in, e.g., HsCmdIf + = Just 4 + | otherwise + = Nothing {- ************************************************************************ @@ -827,7 +862,8 @@ newClsInst overlap_mode dfun_name tvs theta clas tys ; oflag <- getOverlapFlag overlap_mode ; let inst = mkLocalInstance dfun oflag tvs' clas tys' - ; warnIf (isOrphan (is_orphan inst)) (TcRnOrphanInstance inst) + ; when (isOrphan (is_orphan inst)) $ + addDiagnostic (TcRnOrphanInstance inst) ; return inst } tcExtendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 1a008bbff0..7be996a789 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -66,7 +66,7 @@ module GHC.Tc.Utils.TcMType ( -------------------------------- -- Zonking and tidying - zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, + zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, zonkTidyOrigins, tidyEvVar, tidyCt, tidyHole, tidySkolemInfo, zonkTcTyVar, zonkTcTyVars, zonkTcTyVarToTyVar, zonkInvisTVBinder, @@ -93,7 +93,7 @@ module GHC.Tc.Utils.TcMType ( ------------------------------ -- Representation polymorphism - ensureNotLevPoly, checkForLevPoly, checkForLevPolyX, + checkTypeHasFixedRuntimeRep, ) where import GHC.Prelude @@ -116,6 +116,7 @@ import GHC.Core.TyCon import GHC.Core.Coercion import GHC.Core.Class import GHC.Core.Predicate +import GHC.Core.InstEnv (ClsInst(is_tys)) import GHC.Types.Var import GHC.Types.Id as Id @@ -203,7 +204,7 @@ newWanteds orig = mapM (newWanted orig Nothing) cloneWanted :: Ct -> TcM Ct cloneWanted ct - | ev@(CtWanted { ctev_pred = pty }) <- ctEvidence ct + | ev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ }) <- ctEvidence ct = do { co_hole <- newCoercionHole pty ; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) } | otherwise @@ -307,6 +308,9 @@ predTypeOccName ty = case classifyPredType ty of EqPred {} -> mkVarOccFS (fsLit "co") IrredPred {} -> mkVarOccFS (fsLit "irred") ForAllPred {} -> mkVarOccFS (fsLit "df") + SpecialPred special_pred _ -> + case special_pred of + ConcretePrimPred -> mkVarOccFS (fsLit "concr") -- | Create a new 'Implication' with as many sensible defaults for its fields -- as possible. Note that the 'ic_tclvl', 'ic_binds', and 'ic_info' fields do @@ -2550,8 +2554,20 @@ zonkTidyOrigin env (FunDepOrigin2 p1 o1 p2 l2) ; (env2, p2') <- zonkTidyTcType env1 p2 ; (env3, o1') <- zonkTidyOrigin env2 o1 ; return (env3, FunDepOrigin2 p1' o1' p2' l2) } +zonkTidyOrigin env (CycleBreakerOrigin orig) + = do { (env1, orig') <- zonkTidyOrigin env orig + ; return (env1, CycleBreakerOrigin orig') } +zonkTidyOrigin env (InstProvidedOrigin mod cls_inst) + = do { (env1, is_tys') <- mapAccumLM zonkTidyTcType env (is_tys cls_inst) + ; return (env1, InstProvidedOrigin mod (cls_inst {is_tys = is_tys'})) } +zonkTidyOrigin env (FixedRuntimeRepOrigin ty frr_orig) + = do { (env1, ty') <- zonkTidyTcType env ty + ; return (env1, FixedRuntimeRepOrigin ty' frr_orig)} zonkTidyOrigin env orig = return (env, orig) +zonkTidyOrigins :: TidyEnv -> [CtOrigin] -> TcM (TidyEnv, [CtOrigin]) +zonkTidyOrigins = mapAccumLM zonkTidyOrigin + ---------------- tidyCt :: TidyEnv -> Ct -> Ct -- Used only in error reporting @@ -2614,43 +2630,22 @@ tidySigSkol env cx ty tv_prs %* * Representation polymorphism checks * * -************************************************************************* - -See Note [Representation polymorphism checking] in GHC.HsToCore.Monad - --} +***********************************************************************-} --- | According to the rules around representation polymorphism --- (see https://gitlab.haskell.org/ghc/ghc/wikis/no-sub-kinds), no binder --- can have a representation-polymorphic type. This check ensures --- that we respect this rule. It is a bit regrettable that this error --- occurs in zonking, after which we should have reported all errors. --- But it's hard to see where else to do it, because this can be discovered --- only after all solving is done. And, perhaps most importantly, this --- isn't really a compositional property of a type system, so it's --- not a terrible surprise that the check has to go in an awkward spot. -ensureNotLevPoly :: Type -- its zonked type - -> LevityCheckProvenance -- where this happened - -> TcM () -ensureNotLevPoly ty provenance - = whenNoErrs $ -- sometimes we end up zonking bogus definitions of type - -- forall a. a. See, for example, test ghci/scripts/T9140 - checkForLevPoly provenance ty - - -- See Note [Representation polymorphism checking] in GHC.HsToCore.Monad -checkForLevPoly :: LevityCheckProvenance -> Type -> TcM () -checkForLevPoly = checkForLevPolyX (\ty -> addDetailedDiagnostic . TcLevityPolyInType ty) - -checkForLevPolyX :: Monad m - => (Type -> LevityCheckProvenance -> m ()) -- how to report an error - -> LevityCheckProvenance - -> Type - -> m () -checkForLevPolyX add_err provenance ty - | isTypeLevPoly ty - = add_err ty provenance - | otherwise - = return () +-- | Check that the specified type has a fixed runtime representation. +-- +-- If it isn't, throw a representation-polymorphism error appropriate +-- for the context (as specified by the 'FixedRuntimeRepProvenance'). +-- +-- Unlike the other representation polymorphism checks, which emit +-- 'Concrete#' constraints, this function does not emit any constraints, +-- as it has enough information to immediately make a decision. +-- +-- See (1) in Note [Representation polymorphism checking] in GHC.Tc.Utils.Concrete +checkTypeHasFixedRuntimeRep :: FixedRuntimeRepProvenance -> Type -> TcM () +checkTypeHasFixedRuntimeRep prov ty = + unless (typeHasFixedRuntimeRep ty) + (addDetailedDiagnostic $ TcRnTypeDoesNotHaveFixedRuntimeRep ty prov) {- %************************************************************************ diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 5313ef39d4..b79a4152e1 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -146,7 +146,7 @@ module GHC.Tc.Utils.TcType ( isClassPred, isEqPrimPred, isIPLikePred, isEqPred, isEqPredClass, mkClassPred, tcSplitDFunTy, tcSplitDFunHead, tcSplitMethodTy, - isRuntimeRepVar, isKindLevPoly, + isRuntimeRepVar, isFixedRuntimeRepKind, isVisibleBinder, isInvisibleBinder, -- Type substitutions @@ -1935,6 +1935,7 @@ isImprovementPred ty ClassPred cls _ -> classHasFds cls IrredPred {} -> True -- Might have equalities after reduction? ForAllPred {} -> False + SpecialPred {} -> False {- Note [Expanding superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index dc1fd382d2..a0b8106a8d 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -43,18 +43,23 @@ import GHC.Prelude import GHC.Hs import GHC.Core.TyCo.Rep import GHC.Core.TyCo.Ppr( debugPprType ) -import GHC.Tc.Utils.TcMType +import GHC.Tc.Utils.Concrete ( mkWpFun ) +import GHC.Tc.Utils.Env +import GHC.Tc.Utils.Instantiate import GHC.Tc.Utils.Monad +import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.TcType -import GHC.Tc.Utils.Env + + import GHC.Core.Type import GHC.Core.Coercion import GHC.Core.Multiplicity + import GHC.Tc.Types.Evidence import GHC.Tc.Types.Constraint import GHC.Tc.Types.Origin import GHC.Types.Name( isSystemName ) -import GHC.Tc.Utils.Instantiate + import GHC.Core.TyCon import GHC.Builtin.Types import GHC.Types.Var as Var @@ -210,12 +215,8 @@ matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty (n_val_args_wanted, so_far) fun_ty ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1 - ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty doc + ; wrap_fun2 <- mkWpFun idHsWrapper wrap_res arg_ty1 res_ty (WpFunFunTy fun_ty) ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) } - where - doc = text "When inferring the argument type of a function with type" <+> - quotes (ppr fun_ty) - {- ************************************************************************ @@ -320,11 +321,8 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside = assert (af == VisArg) $ do { (wrap_res, result) <- go ((Scaled mult $ mkCheckExpType arg_ty) : acc_arg_tys) (n-1) res_ty - ; let fun_wrap = mkWpFun idHsWrapper wrap_res (Scaled mult arg_ty) res_ty doc + ; fun_wrap <- mkWpFun idHsWrapper wrap_res (Scaled mult arg_ty) res_ty (WpFunFunExpTy orig_ty) ; return ( fun_wrap, result ) } - where - doc = text "When inferring the argument type of a function with type" <+> - quotes (ppr orig_ty) go acc_arg_tys n ty@(TyVarTy tv) | isMetaTyVar tv @@ -779,7 +777,7 @@ There is no notion of multiplicity coercion in Core, therefore the wrapper returned by tcSubMult (and derived functions such as tcCheckUsage and checkManyPattern) is quite unlike any other wrapper: it checks whether the coercion produced by the constraint solver is trivial, producing a type error -is it is not. This is implemented via the WpMultCoercion wrapper, as desugared +if it is not. This is implemented via the WpMultCoercion wrapper, as desugared by GHC.HsToCore.Binds.dsHsWrapper, which does the reflexivity check. This wrapper needs to be placed in the term; otherwise, checking of the @@ -788,11 +786,14 @@ anywhere, since it doesn't affect the desugared code. Why do we check this in the desugarer? It's a convenient place, since it's right after all the constraints are solved. We need the constraints to be -solved to check whether they are trivial or not. Plus there is precedent for -type errors during desuraging (such as the representation polymorphism -restriction). An alternative would be to have a kind of constraint which can -only produce trivial evidence, then this check would happen in the constraint -solver (#18756). +solved to check whether they are trivial or not. + +An alternative would be to have a kind of constraint which can +only produce trivial evidence. This would allow such checks to happen +in the constraint solver (#18756). +This would be similar to the existing setup for Concrete, see + Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete + (PHASE 1 in particular). -} tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs index 963fe9f9b1..3ac4b13582 100644 --- a/compiler/GHC/Tc/Utils/Zonk.hs +++ b/compiler/GHC/Tc/Utils/Zonk.hs @@ -49,7 +49,6 @@ import GHC.Builtin.Names import GHC.Hs -import GHC.Tc.Errors.Types ( LevityCheckProvenance(..) ) import {-# SOURCE #-} GHC.Tc.Gen.Splice (runTopSplice) import GHC.Tc.Utils.Monad import GHC.Tc.TyCl.Build ( TcMethInfo, MethInfo ) @@ -387,8 +386,6 @@ zonkIdOccs env ids = map (zonkIdOcc env) ids zonkIdBndr :: ZonkEnv -> TcId -> TcM Id zonkIdBndr env v = do Scaled w' ty' <- zonkScaledTcTypeToTypeX env (idScaledType v) - ensureNotLevPoly ty' (LevityCheckInBinder v) - return (modifyIdInfo (`setLevityInfoWithType` ty') (setIdMult (setIdType v ty') w')) zonkIdBndrs :: ZonkEnv -> [TcId] -> TcM [Id] @@ -1065,10 +1062,10 @@ zonkCoFn env WpHole = return (env, WpHole) zonkCoFn env (WpCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1 ; (env2, c2') <- zonkCoFn env1 c2 ; return (env2, WpCompose c1' c2') } -zonkCoFn env (WpFun c1 c2 t1 d) = do { (env1, c1') <- zonkCoFn env c1 - ; (env2, c2') <- zonkCoFn env1 c2 - ; t1' <- zonkScaledTcTypeToTypeX env2 t1 - ; return (env2, WpFun c1' c2' t1' d) } +zonkCoFn env (WpFun c1 c2 t1) = do { (env1, c1') <- zonkCoFn env c1 + ; (env2, c2') <- zonkCoFn env1 c2 + ; t1' <- zonkScaledTcTypeToTypeX env2 t1 + ; return (env2, WpFun c1' c2' t1') } zonkCoFn env (WpCast co) = do { co' <- zonkCoToCo env co ; return (env, WpCast co') } zonkCoFn env (WpEvLam ev) = do { (env', ev') <- zonkEvBndrX env ev @@ -1348,7 +1345,6 @@ zonk_pat env (ParPat x lpar p rpar) zonk_pat env (WildPat ty) = do { ty' <- zonkTcTypeToTypeX env ty - ; ensureNotLevPoly ty' LevityCheckInWildcardPattern ; return (env, WildPat ty') } zonk_pat env (VarPat x (L l v)) @@ -1389,8 +1385,7 @@ zonk_pat env (SumPat tys pat alt arity ) ; (env', pat') <- zonkPat env pat ; return (env', SumPat tys' pat' alt arity) } -zonk_pat env p@(ConPat { pat_con = L _ con - , pat_args = args +zonk_pat env p@(ConPat { pat_args = args , pat_con_ext = p'@(ConPatTc { cpt_tvs = tyvars , cpt_dicts = evs @@ -1401,16 +1396,6 @@ zonk_pat env p@(ConPat { pat_con = L _ con }) = assert (all isImmutableTyVar tyvars) $ do { new_tys <- mapM (zonkTcTypeToTypeX env) tys - - -- an unboxed tuple pattern (but only an unboxed tuple pattern) - -- might have representation-polymorphic arguments. - -- Check for this badness. - ; case con of - RealDataCon dc - | isUnboxedTupleTyCon (dataConTyCon dc) - -> mapM_ (checkForLevPoly (LevityCheckInUnboxedTuplePattern p)) (dropRuntimeRepArgs new_tys) - _ -> return () - ; (env0, new_tyvars) <- zonkTyBndrsX env tyvars -- Must zonk the existential variables, because their -- /kind/ need potential zonking. diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs index 9e0f070056..de007d0fac 100644 --- a/compiler/GHC/Tc/Validity.hs +++ b/compiler/GHC/Tc/Validity.hs @@ -1,4 +1,5 @@ +{-# LANGUAGE DerivingStrategies #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} @@ -32,7 +33,7 @@ import GHC.Core.TyCo.FVs import GHC.Core.TyCo.Rep import GHC.Core.TyCo.Ppr import GHC.Tc.Utils.TcType hiding ( sizeType, sizeTypes ) -import GHC.Builtin.Types ( heqTyConName, eqTyConName, coercibleTyConName, manyDataConTy ) +import GHC.Builtin.Types import GHC.Builtin.Names import GHC.Core.Type import GHC.Core.Unify ( tcMatchTyX_BM, BindFlag(..) ) @@ -692,8 +693,10 @@ check_type ve (AppTy ty1 ty2) check_type ve ty@(TyConApp tc tys) | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc = check_syn_tc_app ve ty tc tys - | isUnboxedTupleTyCon tc = check_ubx_tuple ve ty tys - | otherwise = mapM_ (check_arg_type False ve) tys + | isUnboxedTupleTyCon tc + = check_ubx_tuple ve ty tys + | otherwise + = mapM_ (check_arg_type False ve) tys check_type _ (LitTy {}) = return () @@ -1384,11 +1387,12 @@ checkValidInstHead ctxt clas cls_args Note [Instances of built-in classes in signature files] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -User defined instances for KnownNat, KnownSymbol and Typeable are -disallowed -- they are generated when needed by GHC itself on-the-fly. +User defined instances for KnownNat, KnownSymbol, KnownChar, +and Typeable are disallowed + -- they are generated when needed by GHC itself, on-the-fly. However, if they occur in a Backpack signature file, they have an -entirely different meaning. Suppose in M.hsig we see +entirely different meaning. To illustrate, suppose in M.hsig we see signature M where data T :: Nat @@ -1407,6 +1411,7 @@ in hsig files, where `is_sig` is True. check_special_inst_head :: DynFlags -> Bool -> Bool -> UserTypeCtxt -> Class -> [Type] -> TcM () -- Wow! There are a surprising number of ad-hoc special cases here. +-- TODO: common up the logic for special typeclasses (see GHC ticket #20441). check_special_inst_head dflags is_boot is_sig ctxt clas cls_args -- If not in an hs-boot file, abstract classes cannot have instances @@ -1421,15 +1426,15 @@ check_special_inst_head dflags is_boot is_sig ctxt clas cls_args , not is_sig -- Note [Instances of built-in classes in signature files] , hand_written_bindings - = failWithTc rejected_class_msg + = failWithTc $ TcRnSpecialClassInst clas False - -- Handwritten instances of KnownNat/KnownSymbol class - -- are always forbidden (#12837) + -- Handwritten instances of KnownNat/KnownSymbol + -- are forbidden outside of signature files (#12837) | clas_nm `elem` [ knownNatClassName, knownSymbolClassName ] , not is_sig -- Note [Instances of built-in classes in signature files] , hand_written_bindings - = failWithTc rejected_class_msg + = failWithTc $ TcRnSpecialClassInst clas False -- For the most part we don't allow -- instances for (~), (~~), or Coercible; @@ -1437,12 +1442,12 @@ check_special_inst_head dflags is_boot is_sig ctxt clas cls_args -- f :: (forall a b. Coercible a b => Coercible (m a) (m b)) => ...m... | clas_nm `elem` [ heqTyConName, eqTyConName, coercibleTyConName ] , not quantified_constraint - = failWithTc rejected_class_msg + = failWithTc $ TcRnSpecialClassInst clas False -- Check for hand-written Generic instances (disallowed in Safe Haskell) | clas_nm `elem` genericClassNames , hand_written_bindings - = do { failIfTc (safeLanguageOn dflags) gen_inst_err + = do { failIfTc (safeLanguageOn dflags) (TcRnSpecialClassInst clas True) ; when (safeInferOn dflags) (recordUnsafeInfer emptyMessages) } | clas_nm == hasFieldClassName @@ -1501,18 +1506,6 @@ check_special_inst_head dflags is_boot is_sig ctxt clas cls_args text "Only one type can be given in an instance head." $$ text "Use MultiParamTypeClasses if you want to allow more, or zero." - rejected_class_msg :: TcRnMessage - rejected_class_msg = TcRnUnknownMessage $ mkPlainError noHints $ rejected_class_doc - - rejected_class_doc :: SDoc - rejected_class_doc = - text "Class" <+> quotes (ppr clas_nm) - <+> text "does not support user-specified instances" - - gen_inst_err :: TcRnMessage - gen_inst_err = TcRnUnknownMessage $ mkPlainError noHints $ - rejected_class_doc $$ nest 2 (text "(in Safe Haskell)") - mb_ty_args_msg | not (xopt LangExt.TypeSynonymInstances dflags) , not (all tcInstHeadTyNotSynonym ty_args) @@ -1819,8 +1812,9 @@ checkInstTermination theta head_pred check :: VarSet -> PredType -> TcM () check foralld_tvs pred = case classifyPredType pred of - EqPred {} -> return () -- See #4200. - IrredPred {} -> check2 foralld_tvs pred (sizeType pred) + EqPred {} -> return () -- See #4200. + SpecialPred {} -> return () + IrredPred {} -> check2 foralld_tvs pred (sizeType pred) ClassPred cls tys | isTerminatingClass cls -> return () @@ -2834,6 +2828,7 @@ sizePred ty = goClass ty -- The filtering looks bogus -- See Note [Invisible arguments and termination] go (EqPred {}) = 0 + go (SpecialPred {}) = 0 go (IrredPred ty) = sizeType ty go (ForAllPred _ _ pred) = goClass pred diff --git a/compiler/GHC/Types/Id.hs b/compiler/GHC/Types/Id.hs index 6183e51ead..df34dd12fd 100644 --- a/compiler/GHC/Types/Id.hs +++ b/compiler/GHC/Types/Id.hs @@ -99,7 +99,7 @@ module GHC.Types.Id ( idCafInfo, idLFInfo_maybe, idOneShotInfo, idStateHackOneShotInfo, idOccInfo, - isNeverLevPolyId, + isNeverRepPolyId, -- ** Writing 'IdInfo' fields setIdUnfolding, setCaseBndrEvald, @@ -567,7 +567,6 @@ hasNoBinding id = case Var.idDetails id of FCallId _ -> True DataConWorkId dc -> isUnboxedTupleDataCon dc || isUnboxedSumDataCon dc _ -> isCompulsoryUnfolding (idUnfolding id) - -- See Note [Representation-polymorphic Ids] isImplicitId :: Id -> Bool -- ^ 'isImplicitId' tells whether an 'Id's info is implied by other @@ -589,26 +588,6 @@ isImplicitId id idIsFrom :: Module -> Id -> Bool idIsFrom mod id = nameIsLocalOrFrom mod (idName id) -{- Note [Representation-polymorphic Ids] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Some representation-polymorphic Ids must be applied and inlined, not left -un-saturated. Example: - unsafeCoerceId :: forall r1 r2 (a::TYPE r1) (b::TYPE r2). a -> b - -This has a compulsory unfolding because we can't lambda-bind those -arguments. But the compulsory unfolding may leave representation-polymorphic -lambdas if it is not applied to enough arguments; e.g. (#14561) - bad :: forall (a :: TYPE r). a -> a - bad = unsafeCoerce# - -The desugar has special magic to detect such cases: GHC.HsToCore.Expr.badUseOfLevPolyPrimop. -And we want that magic to apply to representation-polymorphic compulsory-inline things. -The easiest way to do this is for hasNoBinding to return True of all things -that have compulsory unfolding. Some Ids with a compulsory unfolding also -have a binding, but it does not harm to say they don't here, and its a very -simple way to fix #14561. --} - isDeadBinder :: Id -> Bool isDeadBinder bndr | isId bndr = isDeadOcc (idOccInfo bndr) | otherwise = False -- TyVars count as not dead @@ -1011,5 +990,5 @@ transferPolyIdInfo old_id abstract_wrt new_id `setDmdSigInfo` new_strictness `setCprSigInfo` old_cpr -isNeverLevPolyId :: Id -> Bool -isNeverLevPolyId = isNeverLevPolyIdInfo . idInfo +isNeverRepPolyId :: Id -> Bool +isNeverRepPolyId = isNeverRepPolyIdInfo . idInfo diff --git a/compiler/GHC/Types/Id/Info.hs b/compiler/GHC/Types/Id/Info.hs index 35d2f61734..ec5607d40f 100644 --- a/compiler/GHC/Types/Id/Info.hs +++ b/compiler/GHC/Types/Id/Info.hs @@ -83,8 +83,8 @@ module GHC.Types.Id.Info ( TickBoxOp(..), TickBoxId, -- ** Levity info - LevityInfo, levityInfo, setNeverLevPoly, setLevityInfoWithType, - isNeverLevPolyIdInfo + LevityInfo, levityInfo, setNeverRepPoly, setLevityInfoWithType, + isNeverRepPolyIdInfo ) where import GHC.Prelude @@ -124,7 +124,7 @@ infixl 1 `setRuleInfo`, `setDmdSigInfo`, `setCprSigInfo`, `setDemandInfo`, - `setNeverLevPoly`, + `setNeverRepPoly`, `setLevityInfoWithType` {- @@ -736,12 +736,16 @@ Note [Levity info] ~~~~~~~~~~~~~~~~~~ Ids store whether or not they can be representation-polymorphic at any amount -of saturation. This is helpful in optimizing the representation polymorphism -check done in the desugarer, where we can usually learn that something is not -representation-polymorphic without actually figuring out its type. -See isExprLevPoly in GHC.Core.Utils for where this info is used. -Storing this is required to prevent perf/compiler/T5631 from blowing up. - +of saturation. This is helpful in optimizing representation polymorphism checks, +allowing us to learn that something is not representation-polymorphic without +actually figuring out its type. +See exprHasFixedRuntimeRep in GHC.Core.Utils for where this info is used. + +Historical note: this was very important when representation polymorphism +was checked in the desugarer (it was needed to prevent T5631 from blowing up). +It's less important now that the checks happen in the typechecker, but remains useful. +Refer to Note [The Concrete mechanism] in GHC.Tc.Utils.Concrete for details +about the new approach being used. -} -- See Note [Levity info] @@ -756,19 +760,19 @@ instance Outputable LevityInfo where -- | Marks an IdInfo describing an Id that is never representation-polymorphic -- (even when applied). The Type is only there for checking that it's really -- never representation-polymorphic. -setNeverLevPoly :: HasDebugCallStack => IdInfo -> Type -> IdInfo -setNeverLevPoly info ty - = assertPpr (not (resultIsLevPoly ty)) (ppr ty) $ +setNeverRepPoly :: HasDebugCallStack => IdInfo -> Type -> IdInfo +setNeverRepPoly info ty + = assertPpr (resultHasFixedRuntimeRep ty) (ppr ty) $ info { bitfield = bitfieldSetLevityInfo NeverLevityPolymorphic (bitfield info) } setLevityInfoWithType :: IdInfo -> Type -> IdInfo setLevityInfoWithType info ty - | not (resultIsLevPoly ty) + | resultHasFixedRuntimeRep ty = info { bitfield = bitfieldSetLevityInfo NeverLevityPolymorphic (bitfield info) } | otherwise = info -isNeverLevPolyIdInfo :: IdInfo -> Bool -isNeverLevPolyIdInfo info +isNeverRepPolyIdInfo :: IdInfo -> Bool +isNeverRepPolyIdInfo info | NeverLevityPolymorphic <- levityInfo info = True | otherwise = False diff --git a/compiler/GHC/Types/Id/Make.hs b/compiler/GHC/Types/Id/Make.hs index 7239998b5d..e52c12ce71 100644 --- a/compiler/GHC/Types/Id/Make.hs +++ b/compiler/GHC/Types/Id/Make.hs @@ -373,13 +373,13 @@ just a cast. That is, it has a compulsory unfolding. As long as its argument is not representation-polymorphic (which it can't be, according to Note [Representation polymorphism invariants] in GHC.Core), and it's saturated, no representation-polymorphic code ends up in the code generator. -The saturation condition is effectively checked by -Note [Detecting forced eta expansion] in GHC.HsToCore.Expr. +The saturation condition is effectively checked in +GHC.Tc.Gen.App.hasFixedRuntimeRep_remainingValArgs. However, if we make a *wrapper* for a newtype, we get into trouble. -The saturation condition is no longer checked (because hasNoBinding -returns False) and indeed we generate a forbidden representation-polymorphic -binding. +In that case, we generate a forbidden representation-polymorphic +binding, and we must then ensure that it is always instantiated +at a representation-monomorphic type. The solution is simple, though: just make the newtype wrappers as ephemeral as the newtype workers. In other words, give the wrappers @@ -586,7 +586,7 @@ mkDataConWorkId wkr_name data_con -- even if arity = 0 `setLevityInfoWithType` wkr_ty -- NB: unboxed tuples have workers, so we can't use - -- setNeverLevPoly + -- setNeverRepPoly wkr_inline_prag = defaultInlinePragma { inl_rule = ConLike } wkr_arity = dataConRepArity data_con @@ -1300,7 +1300,7 @@ mkPrimOpId prim_op -- PrimOps don't ever construct a product, but we want to preserve bottoms cpr | isDeadEndDiv (snd (splitDmdSig strict_sig)) = botCpr - | otherwise = topCpr + | otherwise = topCpr info = noCafIdInfo `setRuleInfo` mkRuleInfo (maybeToList $ primOpRules name prim_op) @@ -1429,7 +1429,7 @@ proxyHashId :: Id proxyHashId = pcMiscPrelId proxyName ty (noCafIdInfo `setUnfoldingInfo` evaldUnfolding -- Note [evaldUnfoldings] - `setNeverLevPoly` ty) + `setNeverRepPoly` ty) where -- proxy# :: forall {k} (a:k). Proxy# k a -- @@ -1449,7 +1449,7 @@ nullAddrId = pcMiscPrelId nullAddrName addrPrimTy info where info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma `setUnfoldingInfo` mkCompulsoryUnfolding defaultSimpleOpts (Lit nullAddrLit) - `setNeverLevPoly` addrPrimTy + `setNeverRepPoly` addrPrimTy ------------------------------------------------ seqId :: Id -- See Note [seqId magic] @@ -1457,6 +1457,7 @@ seqId = pcMiscPrelId seqName ty info where info = noCafIdInfo `setInlinePragInfo` inline_prag `setUnfoldingInfo` mkCompulsoryUnfolding defaultSimpleOpts rhs + `setArityInfo` arity inline_prag = alwaysInlinePragma `setInlinePragmaActivation` ActiveAfter @@ -1476,17 +1477,19 @@ seqId = pcMiscPrelId seqName ty info rhs = mkLams ([runtimeRep2TyVar, alphaTyVar, openBetaTyVar, x, y]) $ Case (Var x) x openBetaTy [Alt DEFAULT [] (Var y)] + arity = 2 + ------------------------------------------------ lazyId :: Id -- See Note [lazyId magic] lazyId = pcMiscPrelId lazyIdName ty info where - info = noCafIdInfo `setNeverLevPoly` ty + info = noCafIdInfo `setNeverRepPoly` ty ty = mkSpecForAllTys [alphaTyVar] (mkVisFunTyMany alphaTy alphaTy) noinlineId :: Id -- See Note [noinlineId magic] noinlineId = pcMiscPrelId noinlineIdName ty info where - info = noCafIdInfo `setNeverLevPoly` ty + info = noCafIdInfo `setNeverRepPoly` ty ty = mkSpecForAllTys [alphaTyVar] (mkVisFunTyMany alphaTy alphaTy) oneShotId :: Id -- See Note [The oneShot function] @@ -1494,6 +1497,7 @@ oneShotId = pcMiscPrelId oneShotName ty info where info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma `setUnfoldingInfo` mkCompulsoryUnfolding defaultSimpleOpts rhs + `setArityInfo` arity ty = mkInfForAllTys [ runtimeRep1TyVar, runtimeRep2TyVar ] $ mkSpecForAllTys [ openAlphaTyVar, openBetaTyVar ] $ mkVisFunTyMany fun_ty fun_ty @@ -1504,6 +1508,7 @@ oneShotId = pcMiscPrelId oneShotName ty info , openAlphaTyVar, openBetaTyVar , body, x'] $ Var body `App` Var x' + arity = 2 ---------------------------------------------------------------------- {- Note [Wired-in Ids for rebindable syntax] @@ -1533,6 +1538,7 @@ leftSectionId = pcMiscPrelId leftSectionName ty info where info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma `setUnfoldingInfo` mkCompulsoryUnfolding defaultSimpleOpts rhs + `setArityInfo` arity ty = mkInfForAllTys [runtimeRep1TyVar,runtimeRep2TyVar, multiplicityTyVar1] $ mkSpecForAllTys [openAlphaTyVar, openBetaTyVar] $ exprType body @@ -1544,6 +1550,7 @@ leftSectionId = pcMiscPrelId leftSectionName ty info rhs = mkLams [ runtimeRep1TyVar, runtimeRep2TyVar, multiplicityTyVar1 , openAlphaTyVar, openBetaTyVar ] body body = mkLams [f,xmult] $ App (Var f) (Var xmult) + arity = 2 -- See Note [Left and right sections] in GHC.Rename.Expr -- See Note [Wired-in Ids for rebindable syntax] @@ -1556,6 +1563,7 @@ rightSectionId = pcMiscPrelId rightSectionName ty info where info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma `setUnfoldingInfo` mkCompulsoryUnfolding defaultSimpleOpts rhs + `setArityInfo` arity ty = mkInfForAllTys [runtimeRep1TyVar,runtimeRep2TyVar,runtimeRep3TyVar , multiplicityTyVar1, multiplicityTyVar2 ] $ mkSpecForAllTys [openAlphaTyVar, openBetaTyVar, openGammaTyVar ] $ @@ -1572,6 +1580,7 @@ rightSectionId = pcMiscPrelId rightSectionName ty info , multiplicityTyVar1, multiplicityTyVar2 , openAlphaTyVar, openBetaTyVar, openGammaTyVar ] body body = mkLams [f,ymult,xmult] $ mkVarApps (Var f) [xmult,ymult] + arity = 3 -------------------------------------------------------------------------------- @@ -1580,6 +1589,7 @@ coerceId = pcMiscPrelId coerceName ty info where info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma `setUnfoldingInfo` mkCompulsoryUnfolding defaultSimpleOpts rhs + `setArityInfo` 2 eqRTy = mkTyConApp coercibleTyCon [ tYPE r , a, b ] eqRPrimTy = mkTyConApp eqReprPrimTyCon [ tYPE r, tYPE r, a, b ] ty = mkInvisForAllTys [ Bndr rv InferredSpec @@ -1792,7 +1802,7 @@ realWorldPrimId :: Id -- :: State# RealWorld realWorldPrimId = pcMiscPrelId realWorldName realWorldStatePrimTy (noCafIdInfo `setUnfoldingInfo` evaldUnfolding -- Note [evaldUnfoldings] `setOneShotInfo` stateHackOneShot - `setNeverLevPoly` realWorldStatePrimTy) + `setNeverRepPoly` realWorldStatePrimTy) voidPrimId :: Id -- Global constant :: Void# -- The type Void# is now the same as (# #) (ticket #18441), @@ -1802,7 +1812,7 @@ voidPrimId :: Id -- Global constant :: Void# -- a top-level unlifted value. voidPrimId = pcMiscPrelId voidPrimIdName unboxedUnitTy (noCafIdInfo `setUnfoldingInfo` mkCompulsoryUnfolding defaultSimpleOpts rhs - `setNeverLevPoly` unboxedUnitTy) + `setNeverRepPoly` unboxedUnitTy) where rhs = Var (dataConWorkId unboxedUnitDataCon) |