diff options
| author | sheaf <sam.derbyshire@gmail.com> | 2021-10-15 23:09:39 +0200 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2021-10-17 14:06:46 -0400 |
| commit | 81740ce83976e9d6b68594f8a4b489452cca56e5 (patch) | |
| tree | 7b41d1529975c2f78eaced81e26e4722d34c212f /compiler/GHC/Tc | |
| parent | 65bf3992aebb3c08f0c4e13a3fb89dd5620015a9 (diff) | |
| download | haskell-81740ce83976e9d6b68594f8a4b489452cca56e5.tar.gz | |
Introduce Concrete# for representation polymorphism checks
PHASE 1: we never rewrite Concrete# evidence.
This patch migrates all the representation polymorphism checks to
the typechecker, using a new constraint form
Concrete# :: forall k. k -> TupleRep '[]
Whenever a type `ty` must be representation-polymorphic
(e.g. it is the type of an argument to a function), we emit a new
`Concrete# ty` Wanted constraint. If this constraint goes
unsolved, we report a representation-polymorphism error to the user.
The 'FRROrigin' datatype keeps track of the context of the
representation-polymorphism check, for more informative error messages.
This paves the way for further improvements, such as
allowing type families in RuntimeReps and improving the soundness
of typed Template Haskell. This is left as future work (PHASE 2).
fixes #17907 #20277 #20330 #20423 #20426
updates haddock submodule
-------------------------
Metric Decrease:
T5642
-------------------------
Diffstat (limited to 'compiler/GHC/Tc')
32 files changed, 1816 insertions, 411 deletions
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 |