diff options
Diffstat (limited to 'compiler')
69 files changed, 2399 insertions, 1237 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) diff --git a/compiler/Language/Haskell/Syntax/Expr.hs b/compiler/Language/Haskell/Syntax/Expr.hs index 2215ed1210..e8538dfa43 100644 --- a/compiler/Language/Haskell/Syntax/Expr.hs +++ b/compiler/Language/Haskell/Syntax/Expr.hs @@ -973,10 +973,17 @@ data HsCmd id -- in Language.Haskell.Syntax.Extension --- | Haskell Array Application Type -data HsArrAppType = HsHigherOrderApp | HsFirstOrderApp - deriving Data - +-- | Haskell arrow application type. +data HsArrAppType + -- | First order arrow application '-<' + = HsHigherOrderApp + -- | Higher order arrow application '-<<' + | HsFirstOrderApp + deriving Data + +pprHsArrType :: HsArrAppType -> SDoc +pprHsArrType HsHigherOrderApp = text "higher order arrow application" +pprHsArrType HsFirstOrderApp = text "first order arrow application" {- | Top-level command, introducing a new arrow. This may occur inside a proc (where the stack is empty) or as an diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in index 668642af80..e32e8572ec 100644 --- a/compiler/ghc.cabal.in +++ b/compiler/ghc.cabal.in @@ -667,6 +667,7 @@ Library GHC.Tc.Types.Origin GHC.Tc.Types.Rank GHC.Tc.Utils.Backpack + GHC.Tc.Utils.Concrete GHC.Tc.Utils.Env GHC.Tc.Utils.Instantiate GHC.Tc.Utils.Monad |