diff options
113 files changed, 1522 insertions, 202 deletions
diff --git a/compiler/basicTypes/Id.hs b/compiler/basicTypes/Id.hs index 621be76570..e2dfe925b1 100644 --- a/compiler/basicTypes/Id.hs +++ b/compiler/basicTypes/Id.hs @@ -567,7 +567,7 @@ lambdas if it is not applied to enough arguments; e.g. (#14561) The desugar has special magic to detect such cases: DsExpr.badUseOfLevPolyPrimop. And we want that magic to apply to levity-polymorphic compulsory-inline things. The easiest way to do this is for hasNoBinding to return True of all things -that have compulsory unfolding. A very Ids with a compulsory unfolding also +that have compulsory unfolding. Some Ids with a compulsory unfolding also have a binding, but it does not harm to say they don't here, and its a very simple way to fix #14561. diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs index f96b579ba9..741b48e58b 100644 --- a/compiler/basicTypes/MkId.hs +++ b/compiler/basicTypes/MkId.hs @@ -29,6 +29,7 @@ module MkId ( nullAddrId, seqId, lazyId, lazyIdKey, coercionTokenId, magicDictId, coerceId, proxyHashId, noinlineId, noinlineIdName, + coerceName, -- Re-export error Ids module PrelRules @@ -71,6 +72,7 @@ import DynFlags import Outputable import FastString import ListSetOps +import Var (VarBndr(Bndr)) import qualified GHC.LanguageExtensions as LangExt import Data.Maybe ( maybeToList ) @@ -338,6 +340,32 @@ effect whether a wrapper is present or not: We'd like 'map Age' to match the LHS. For this to happen, Age must be unfolded, otherwise we'll be stuck. This is tested in T16208. +It also allows for the posssibility of levity polymorphic newtypes +with wrappers (with -XUnliftedNewtypes): + + newtype N (a :: TYPE r) = MkN a + +With -XUnliftedNewtypes, this is allowed -- even though MkN is levity- +polymorphic. It's OK because MkN evaporates in the compiled code, becoming +just a cast. That is, it has a compulsory unfolding. As long as its +argument is not levity-polymorphic (which it can't be, according to +Note [Levity polymorphism invariants] in CoreSyn), and it's saturated, +no levity-polymorphic code ends up in the code generator. The saturation +condition is effectively checked by Note [Detecting forced eta expansion] +in DsExpr. + +However, if we make a *wrapper* for a newtype, we get into trouble. +The saturation condition is no longer checked (because hasNoBinding +returns False) and indeed we generate a forbidden levity-polymorphic +binding. + +The solution is simple, though: just make the newtype wrappers +as ephemeral as the newtype workers. In other words, give the wrappers +compulsory unfoldings and no bindings. The compulsory unfolding is given +in wrap_unf in mkDataConRep, and the lack of a binding happens in +TidyPgm.getTyConImplicitBinds, where we say that a newtype has no implicit +bindings. + ************************************************************************ * * \subsection{Dictionary selectors} @@ -595,6 +623,7 @@ But if we inline the wrapper, we get map (\a. case i of I# i# a -> Foo i# a) (f a) and now case-of-known-constructor eliminates the redundant allocation. + -} mkDataConRep :: DynFlags @@ -624,7 +653,7 @@ mkDataConRep dflags fam_envs wrap_name mb_bangs data_con -- We need to get the CAF info right here because TidyPgm -- does not tidy the IdInfo of implicit bindings (like the wrapper) -- so it not make sure that the CAF info is sane - `setNeverLevPoly` wrap_ty + `setLevityInfoWithType` wrap_ty wrap_sig = mkClosedStrictSig wrap_arg_dmds (dataConCPR data_con) @@ -1423,19 +1452,23 @@ coerceId = pcMiscPrelId coerceName ty info where info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma `setUnfoldingInfo` mkCompulsoryUnfolding rhs - `setNeverLevPoly` ty - eqRTy = mkTyConApp coercibleTyCon [ liftedTypeKind - , alphaTy, betaTy ] - eqRPrimTy = mkTyConApp eqReprPrimTyCon [ liftedTypeKind - , liftedTypeKind - , alphaTy, betaTy ] - ty = mkSpecForAllTys [alphaTyVar, betaTyVar] $ - mkInvisFunTy eqRTy $ - mkVisFunTy alphaTy betaTy - - [eqR,x,eq] = mkTemplateLocals [eqRTy, alphaTy, eqRPrimTy] - rhs = mkLams [alphaTyVar, betaTyVar, eqR, x] $ - mkWildCase (Var eqR) eqRTy betaTy $ + eqRTy = mkTyConApp coercibleTyCon [ tYPE r , a, b ] + eqRPrimTy = mkTyConApp eqReprPrimTyCon [ tYPE r, tYPE r, a, b ] + ty = mkForAllTys [ Bndr rv Inferred + , Bndr av Specified + , Bndr bv Specified + ] $ + mkInvisFunTy eqRTy $ + mkVisFunTy a b + + bndrs@[rv,av,bv] = mkTemplateKiTyVar runtimeRepTy + (\r -> [tYPE r, tYPE r]) + + [r, a, b] = mkTyVarTys bndrs + + [eqR,x,eq] = mkTemplateLocals [eqRTy, a, eqRPrimTy] + rhs = mkLams (bndrs ++ [eqR, x]) $ + mkWildCase (Var eqR) eqRTy b $ [(DataAlt coercibleDataCon, [eq], Cast (Var x) (mkCoVarCo eq))] {- diff --git a/compiler/codeGen/StgCmmForeign.hs b/compiler/codeGen/StgCmmForeign.hs index 7e26e7e118..172dcba219 100644 --- a/compiler/codeGen/StgCmmForeign.hs +++ b/compiler/codeGen/StgCmmForeign.hs @@ -619,6 +619,9 @@ typeToStgFArgType typ | tycon == mutableByteArrayPrimTyCon = StgByteArrayType | otherwise = StgPlainType where - -- should be a tycon app, since this is a foreign call + -- Should be a tycon app, since this is a foreign call. We look + -- through newtypes so the offset does not change if a user replaces + -- a type in a foreign function signature with a representationally + -- equivalent newtype. tycon = tyConAppTyCon (unwrapType typ) diff --git a/compiler/deSugar/DsExpr.hs b/compiler/deSugar/DsExpr.hs index 12b0c838a6..9516fbbe82 100644 --- a/compiler/deSugar/DsExpr.hs +++ b/compiler/deSugar/DsExpr.hs @@ -1091,7 +1091,7 @@ Note [Detecting forced eta expansion] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We cannot have levity polymorphic function arguments. See Note [Levity polymorphism invariants] in CoreSyn. But we *can* have -functions that take levity polymorphism arguments, as long as these +functions that take levity polymorphic arguments, as long as these functions are eta-reduced. (See #12708 for an example.) However, we absolutely cannot do this for functions that have no @@ -1162,7 +1162,11 @@ badUseOfLevPolyPrimop id ty levPolyPrimopErr :: Id -> Type -> [Type] -> DsM () levPolyPrimopErr primop ty bad_tys - = errDs $ vcat [ hang (text "Cannot use primitive with levity-polymorphic arguments:") - 2 (ppr primop <+> dcolon <+> pprWithTYPE ty) - , hang (text "Levity-polymorphic arguments:") - 2 (vcat (map (\t -> pprWithTYPE t <+> dcolon <+> pprWithTYPE (typeKind t)) bad_tys)) ] + = errDs $ vcat + [ hang (text "Cannot use function with levity-polymorphic arguments:") + 2 (ppr primop <+> dcolon <+> pprWithTYPE ty) + , hang (text "Levity-polymorphic arguments:") + 2 $ vcat $ map + (\t -> pprWithTYPE t <+> dcolon <+> pprWithTYPE (typeKind t)) + bad_tys + ] diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs index b186b36abb..130e39efab 100644 --- a/compiler/hsSyn/HsTypes.hs +++ b/compiler/hsSyn/HsTypes.hs @@ -62,6 +62,7 @@ module HsTypes ( mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy, ignoreParens, hsSigType, hsSigWcType, hsLTyVarBndrToType, hsLTyVarBndrsToTypes, + hsConDetailsArgs, -- Printing pprHsType, pprHsForAll, pprHsForAllExtra, pprHsExplicitForAll, @@ -912,6 +913,14 @@ instance (Outputable arg, Outputable rec) ppr (RecCon rec) = text "RecCon:" <+> ppr rec ppr (InfixCon l r) = text "InfixCon:" <+> ppr [l, r] +hsConDetailsArgs :: + HsConDetails (LHsType a) (Located [LConDeclField a]) + -> [LHsType a] +hsConDetailsArgs details = case details of + InfixCon a b -> [a,b] + PrefixCon xs -> xs + RecCon r -> map (cd_fld_type . unLoc) (unLoc r) + {- Note [ConDeclField passs] ~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index 1d026f6c99..805cdcef07 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -4527,6 +4527,7 @@ xFlagsDeps = [ flagSpec "UndecidableSuperClasses" LangExt.UndecidableSuperClasses, flagSpec "UnicodeSyntax" LangExt.UnicodeSyntax, flagSpec "UnliftedFFITypes" LangExt.UnliftedFFITypes, + flagSpec "UnliftedNewtypes" LangExt.UnliftedNewtypes, flagSpec "ViewPatterns" LangExt.ViewPatterns ] diff --git a/compiler/main/TidyPgm.hs b/compiler/main/TidyPgm.hs index 4f9c8c856f..66cef76861 100644 --- a/compiler/main/TidyPgm.hs +++ b/compiler/main/TidyPgm.hs @@ -566,7 +566,9 @@ See Note [Data constructor workers] in CorePrep. -} getTyConImplicitBinds :: TyCon -> [CoreBind] -getTyConImplicitBinds tc = map get_defn (mapMaybe dataConWrapId_maybe (tyConDataCons tc)) +getTyConImplicitBinds tc + | isNewTyCon tc = [] -- See Note [Compulsory newtype unfolding] in MkId + | otherwise = map get_defn (mapMaybe dataConWrapId_maybe (tyConDataCons tc)) getClassImplicitBinds :: Class -> [CoreBind] getClassImplicitBinds cls diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs index 3e0d87fd35..01c496a310 100644 --- a/compiler/prelude/TysPrim.hs +++ b/compiler/prelude/TysPrim.hs @@ -13,7 +13,7 @@ module TysPrim( mkPrimTyConName, -- For implicit parameters in TysWiredIn only mkTemplateKindVars, mkTemplateTyVars, mkTemplateTyVarsFrom, - mkTemplateKiTyVars, + mkTemplateKiTyVars, mkTemplateKiTyVar, mkTemplateTyConBinders, mkTemplateKindTyConBinders, mkTemplateAnonTyConBinders, @@ -251,14 +251,15 @@ alphaTyVars is a list of type variables for use in templates: ["a", "b", ..., "z", "t1", "t2", ... ] -} +mkTemplateKindVar :: Kind -> TyVar +mkTemplateKindVar = mkTyVar (mk_tv_name 0 "k") + mkTemplateKindVars :: [Kind] -> [TyVar] -- k0 with unique (mkAlphaTyVarUnique 0) -- k1 with unique (mkAlphaTyVarUnique 1) -- ... etc -mkTemplateKindVars [kind] - = [mkTyVar (mk_tv_name 0 "k") kind] - -- Special case for one kind: just "k" - +mkTemplateKindVars [kind] = [mkTemplateKindVar kind] + -- Special case for one kind: just "k" mkTemplateKindVars kinds = [ mkTyVar (mk_tv_name u ('k' : show u)) kind | (kind, u) <- kinds `zip` [0..] ] @@ -307,7 +308,7 @@ mkTemplateKiTyVars -> [TyVar] -- [kv1:k1, ..., kvn:kn, av1:ak1, ..., avm:akm] -- Example: if you want the tyvars for -- forall (r:RuntimeRep) (a:TYPE r) (b:*). blah --- call mkTemplateKiTyVars [RuntimeRep] (\[r]. [TYPE r, *) +-- call mkTemplateKiTyVars [RuntimeRep] (\[r] -> [TYPE r, *]) mkTemplateKiTyVars kind_var_kinds mk_arg_kinds = kv_bndrs ++ tv_bndrs where @@ -315,6 +316,21 @@ mkTemplateKiTyVars kind_var_kinds mk_arg_kinds anon_kinds = mk_arg_kinds (mkTyVarTys kv_bndrs) tv_bndrs = mkTemplateTyVarsFrom (length kv_bndrs) anon_kinds +mkTemplateKiTyVar + :: Kind -- [k1, .., kn] Kind of kind-forall'd var + -> (Kind -> [Kind]) -- Arg is kv1:k1 + -- Result is anon arg kinds [ak1, .., akm] + -> [TyVar] -- [kv1:k1, ..., kvn:kn, av1:ak1, ..., avm:akm] +-- Example: if you want the tyvars for +-- forall (r:RuntimeRep) (a:TYPE r) (b:*). blah +-- call mkTemplateKiTyVar RuntimeRep (\r -> [TYPE r, *]) +mkTemplateKiTyVar kind mk_arg_kinds + = kv_bndr : tv_bndrs + where + kv_bndr = mkTemplateKindVar kind + anon_kinds = mk_arg_kinds (mkTyVarTy kv_bndr) + tv_bndrs = mkTemplateTyVarsFrom 1 anon_kinds + mkTemplateKindTyConBinders :: [Kind] -> [TyConBinder] -- Makes named, Specified binders mkTemplateKindTyConBinders kinds = [mkNamedTyConBinder Specified tv | tv <- mkTemplateKindVars kinds] diff --git a/compiler/prelude/primops.txt.pp b/compiler/prelude/primops.txt.pp index ef8a459100..3bf0180c45 100644 --- a/compiler/prelude/primops.txt.pp +++ b/compiler/prelude/primops.txt.pp @@ -3439,6 +3439,11 @@ pseudoop "coerce" the newtype's concrete type to the abstract type. But it also works in more complicated settings, e.g. converting a list of newtypes to a list of concrete types. + + This function is runtime-representation polymorphic, but the + {\tt RuntimeRep} type argument is marked as {\tt Inferred}, meaning + that it is not available for visible type application. This means + the typechecker will accept {\tt coerce @Int @Age 42}. } ------------------------------------------------------------------------ diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs index 9e0d616ace..e3c9576e94 100644 --- a/compiler/rename/RnSource.hs +++ b/compiler/rename/RnSource.hs @@ -69,7 +69,7 @@ import Control.Arrow ( first ) import Data.List ( mapAccumL ) import qualified Data.List.NonEmpty as NE import Data.List.NonEmpty ( NonEmpty(..) ) -import Data.Maybe ( isNothing, fromMaybe ) +import Data.Maybe ( isNothing, isJust, fromMaybe ) import qualified Data.Set as Set ( difference, fromList, toList, null ) {- | @rnSourceDecl@ "renames" declarations. @@ -1539,18 +1539,22 @@ rnTyClDecl (SynDecl { tcdLName = tycon, tcdTyVars = tyvars, -- "data", "newtype" declarations -- both top level and (for an associated type) in an instance decl -rnTyClDecl (DataDecl { tcdLName = tycon, tcdTyVars = tyvars, - tcdFixity = fixity, tcdDataDefn = defn }) +rnTyClDecl (DataDecl _ _ _ _ (XHsDataDefn _)) = + panic "rnTyClDecl: DataDecl with XHsDataDefn" +rnTyClDecl (DataDecl + { tcdLName = tycon, tcdTyVars = tyvars, + tcdFixity = fixity, + tcdDataDefn = defn@HsDataDefn{ dd_ND = new_or_data + , dd_kindSig = kind_sig} }) = do { tycon' <- lookupLocatedTopBndrRn tycon ; let kvs = extractDataDefnKindVars defn doc = TyDataCtx tycon ; traceRn "rntycl-data" (ppr tycon <+> ppr kvs) ; bindHsQTyVars doc Nothing Nothing kvs tyvars $ \ tyvars' no_rhs_kvs -> do { (defn', fvs) <- rnDataDefn doc defn - -- See Note [Complete user-supplied kind signatures] in HsDecls - ; cusks_enabled <- xoptM LangExt.CUSKs - ; let cusk = cusks_enabled && hsTvbAllKinded tyvars' && no_rhs_kvs - rn_info = DataDeclRn { tcdDataCusk = cusk + ; cusk <- dataDeclHasCUSK + tyvars' new_or_data no_rhs_kvs (isJust kind_sig) + ; let rn_info = DataDeclRn { tcdDataCusk = cusk , tcdFVs = fvs } ; traceRn "rndata" (ppr tycon <+> ppr cusk <+> ppr no_rhs_kvs) ; return (DataDecl { tcdLName = tycon' @@ -1626,6 +1630,42 @@ rnTyClDecl (ClassDecl { tcdCtxt = context, tcdLName = lcls, rnTyClDecl (XTyClDecl _) = panic "rnTyClDecl" +-- Does the data type declaration include a CUSK? +dataDeclHasCUSK :: LHsQTyVars pass -> NewOrData -> Bool -> Bool -> RnM Bool +dataDeclHasCUSK tyvars new_or_data no_rhs_kvs has_kind_sig = do + { -- See Note [Unlifted Newtypes and CUSKs], and for a broader + -- picture, see Note [Implementation of UnliftedNewtypes]. + ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes + ; let non_cusk_newtype + | NewType <- new_or_data = + unlifted_newtypes && not has_kind_sig + | otherwise = False + -- See Note [CUSKs: complete user-supplied kind signatures] in HsDecls + ; cusks_enabled <- xoptM LangExt.CUSKs + ; return $ cusks_enabled && hsTvbAllKinded tyvars && + no_rhs_kvs && not non_cusk_newtype + } + +{- Note [Unlifted Newtypes and CUSKs] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When unlifted newtypes are enabled, a newtype must have a kind signature +in order to be considered have a CUSK. This is because the flow of +kind inference works differently. Consider: + + newtype Foo = FooC Int + +When UnliftedNewtypes is disabled, we decide that Foo has kind +`TYPE 'LiftedRep` without looking inside the data constructor. So, we +can say that Foo has a CUSK. However, when UnliftedNewtypes is enabled, +we fill in the kind of Foo as a metavar that gets solved by unification +with the kind of the field inside FooC (that is, Int, whose kind is +`TYPE 'LiftedRep`). But since we have to look inside the data constructors +to figure out the kind signature of Foo, it does not have a CUSK. + +See Note [Implementation of UnliftedNewtypes] for where this fits in to +the broader picture of UnliftedNewtypes. +-} + -- "type" and "type instance" declarations rnTySyn :: HsDocContext -> LHsType GhcPs -> RnM (LHsType GhcRn, FreeVars) rnTySyn doc rhs = rnLHsType doc rhs diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index 759830e97f..02b888703d 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -2015,11 +2015,11 @@ mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act level = m_level `orElse` TypeLevel occurs_check_error - | Just act_tv <- tcGetTyVar_maybe act - , act_tv `elemVarSet` tyCoVarsOfType exp + | Just tv <- tcGetTyVar_maybe ty1 + , tv `elemVarSet` tyCoVarsOfType ty2 = True - | Just exp_tv <- tcGetTyVar_maybe exp - , exp_tv `elemVarSet` tyCoVarsOfType act + | Just tv <- tcGetTyVar_maybe ty2 + , tv `elemVarSet` tyCoVarsOfType ty1 = True | otherwise = False @@ -2043,13 +2043,17 @@ mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act -> empty thing_msg = case maybe_thing of - Just thing -> \_ -> quotes thing <+> text "is" - Nothing -> \vowel -> text "got a" <> - if vowel then char 'n' else empty + Just thing -> \_ levity -> + quotes thing <+> text "is" <+> levity + Nothing -> \vowel levity -> + text "got a" <> + (if vowel then char 'n' else empty) <+> + levity <+> + text "type" msg2 = sep [ text "Expecting a lifted type, but" - , thing_msg True, text "unlifted" ] + , thing_msg True (text "unlifted") ] msg3 = sep [ text "Expecting an unlifted type, but" - , thing_msg False, text "lifted" ] + , thing_msg False (text "lifted") ] msg4 = maybe_num_args_msg $$ sep [ text "Expected a type, but" , maybe (text "found something with kind") diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs index eb65d1e093..d5c600dda8 100644 --- a/compiler/typecheck/TcEvidence.hs +++ b/compiler/typecheck/TcEvidence.hs @@ -30,6 +30,7 @@ module TcEvidence ( -- TcCoercion TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole, + TcMCoercion, Role(..), LeftOrRight(..), pickLR, mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcFunCo, @@ -42,7 +43,7 @@ module TcEvidence ( mkTcKindCo, tcCoercionKind, coVarsOfTcCo, mkTcCoVarCo, - isTcReflCo, isTcReflexiveCo, + isTcReflCo, isTcReflexiveCo, isTcGReflMCo, tcCoToMCo, tcCoercionRole, unwrapIP, wrapIP ) where @@ -98,6 +99,7 @@ type TcCoercion = Coercion type TcCoercionN = CoercionN -- A Nominal coercion ~N type TcCoercionR = CoercionR -- A Representational coercion ~R type TcCoercionP = CoercionP -- a phantom coercion +type TcMCoercion = MCoercion mkTcReflCo :: Role -> TcType -> TcCoercion mkTcSymCo :: TcCoercion -> TcCoercion @@ -133,6 +135,7 @@ tcCoercionKind :: TcCoercion -> Pair TcType tcCoercionRole :: TcCoercion -> Role coVarsOfTcCo :: TcCoercion -> TcTyCoVarSet isTcReflCo :: TcCoercion -> Bool +isTcGReflMCo :: TcMCoercion -> Bool -- | This version does a slow check, calculating the related types and seeing -- if they are equal. @@ -168,8 +171,12 @@ tcCoercionKind = coercionKind tcCoercionRole = coercionRole coVarsOfTcCo = coVarsOfCo isTcReflCo = isReflCo +isTcGReflMCo = isGReflMCo isTcReflexiveCo = isReflexiveCo +tcCoToMCo :: TcCoercion -> TcMCoercion +tcCoToMCo = coToMCo + {- %************************************************************************ %* * diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 5965170a55..f2a7950450 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -2122,8 +2122,6 @@ bindExplicitTKBndrs_Q_Skol, bindExplicitTKBndrs_Q_Tv bindExplicitTKBndrs_Q_Skol ctxt_kind = bindExplicitTKBndrsX (tcHsQTyVarBndr ctxt_kind newSkolemTyVar) bindExplicitTKBndrs_Q_Tv ctxt_kind = bindExplicitTKBndrsX (tcHsQTyVarBndr ctxt_kind newTyVarTyVar) --- | Used during the "kind-checking" pass in TcTyClsDecls only, --- and even then only for data-con declarations. bindExplicitTKBndrsX :: (HsTyVarBndr GhcRn -> TcM TcTyVar) -> [LHsTyVarBndr GhcRn] diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs index 9642756b99..25c598df6b 100644 --- a/compiler/typecheck/TcInstDcls.hs +++ b/compiler/typecheck/TcInstDcls.hs @@ -472,8 +472,7 @@ tcClsInstDecl (L loc (ClsInstDecl { cid_poly_ty = hs_ty, cid_binds = binds , cid_datafam_insts = adts })) = setSrcSpan loc $ addErrCtxt (instDeclCtxt1 hs_ty) $ - do { traceTc "tcLocalInstDecl" (ppr hs_ty) - ; dfun_ty <- tcHsClsInstType (InstDeclCtxt False) hs_ty + do { dfun_ty <- tcHsClsInstType (InstDeclCtxt False) hs_ty ; let (tyvars, theta, clas, inst_tys) = tcSplitDFunTy dfun_ty -- NB: tcHsClsInstType does checkValidInstance @@ -660,10 +659,10 @@ tcDataFamInstDecl mb_clsinfo ; gadt_syntax <- dataDeclChecks fam_name new_or_data hs_ctxt hs_cons -- Do /not/ check that the number of patterns = tyConArity fam_tc -- See [Arity of data families] in FamInstEnv - ; (qtvs, pats, res_kind, stupid_theta) <- tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksig hs_cons + new_or_data -- Eta-reduce the axiom if possible -- Quite tricky: see Note [Eta-reduction for data families] @@ -679,13 +678,26 @@ tcDataFamInstDecl mb_clsinfo -- first, so there is no reason to suppose that the eta_tvs -- (obtained from the pats) are at the end (#11148) - -- Eta-expand the representation tycon until it has reult kind * + -- Eta-expand the representation tycon until it has result + -- kind `TYPE r`, for some `r`. If UnliftedNewtypes is not enabled, we + -- go one step further and ensure that it has kind `TYPE 'LiftedRep`. + -- -- See also Note [Arity of data families] in FamInstEnv -- NB: we can do this after eta-reducing the axiom, because if -- we did it before the "extra" tvs from etaExpandAlgTyCon -- would always be eta-reduced ; (extra_tcbs, final_res_kind) <- etaExpandAlgTyCon full_tcbs res_kind - ; checkTc (tcIsLiftedTypeKind final_res_kind) (badKindSig True res_kind) + ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes + ; let allowUnlifted = unlifted_newtypes && new_or_data == NewType + -- With UnliftedNewtypes, we allow kinds other than Type, but they + -- must still be of the form `TYPE r` since we don't want to accept + -- Constraint or Nat. See Note [Implementation of UnliftedNewtypes]. + ; checkTc + (if allowUnlifted + then tcIsRuntimeTypeKind final_res_kind + else tcIsLiftedTypeKind final_res_kind + ) + (badKindSig True res_kind) ; let extra_pats = map (mkTyVarTy . binderVar) extra_tcbs all_pats = pats `chkAppend` extra_pats orig_res_ty = mkTyConApp fam_tc all_pats @@ -703,9 +715,10 @@ tcDataFamInstDecl mb_clsinfo ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) -> do { data_cons <- tcExtendTyVarEnv qtvs $ - -- For H98 decls, the tyvars scope - -- over the data constructors - tcConDecls rec_rep_tc ty_binders orig_res_ty hs_cons + -- For H98 decls, the tyvars scope + -- over the data constructors + tcConDecls rec_rep_tc new_or_data ty_binders final_res_kind + orig_res_ty hs_cons ; rep_tc_name <- newFamInstTyConName lfam_name pats ; axiom_name <- newFamInstAxiomName lfam_name [pats] @@ -722,7 +735,7 @@ tcDataFamInstDecl mb_clsinfo -- NB: Use the full ty_binders from the pats. See bullet toward -- the end of Note [Data type families] in TyCon rep_tc = mkAlgTyCon rep_tc_name - ty_binders liftedTypeKind + ty_binders final_res_kind (map (const Nominal) ty_binders) (fmap unLoc cType) stupid_theta tc_rhs parent @@ -782,12 +795,14 @@ tcDataFamInstDecl _ _ = panic "tcDataFamInstDecl" tcDataFamHeader :: AssocInstInfo -> TyCon -> [Name] -> Maybe [LHsTyVarBndr GhcRn] -> LexicalFixity -> LHsContext GhcRn -> HsTyPats GhcRn -> Maybe (LHsKind GhcRn) -> [LConDecl GhcRn] + -> NewOrData -> TcM ([TyVar], [Type], Kind, ThetaType) -- The "header" is the part other than the data constructors themselves -- e.g. data instance D [a] :: * -> * where ... -- Here the "header" is the bit before the "where" -tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksig hs_cons - = do { (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, res_kind))) +tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt + hs_pats m_ksig hs_cons new_or_data + = do { (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty))) <- pushTcLevelM_ $ solveEqualities $ bindImplicitTKBndrs_Q_Skol imp_vars $ @@ -799,17 +814,16 @@ tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksi -- with its parent class ; addConsistencyConstraints mb_clsinfo lhs_ty - -- Add constraints from the data constructors - ; mapM_ (wrapLocM_ kcConDecl) hs_cons - -- Add constraints from the result signature ; res_kind <- tc_kind_sig m_ksig + -- Add constraints from the data constructors + ; mapM_ (wrapLocM_ (kcConDecl new_or_data res_kind)) hs_cons ; lhs_ty <- checkExpectedKind_pp pp_lhs lhs_ty lhs_kind res_kind - ; return (stupid_theta, lhs_ty, res_kind) } + ; return (stupid_theta, lhs_ty) } -- See TcTyClsDecls Note [Generalising in tcFamTyPatsGuts] -- This code (and the stuff immediately above) is very similar - -- to that in tcFamTyInstEqnGuts. Maybe we should abstract the + -- to that in tcTyFamInstEqnGuts. Maybe we should abstract the -- common code; but for the moment I concluded that it's -- clearer to duplicate it. Still, if you fix a bug here, -- check there too! @@ -819,22 +833,33 @@ tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksi -- Zonk the patterns etc into the Type world ; (ze, qtvs) <- zonkTyBndrs qtvs - ; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty - ; res_kind <- zonkTcTypeToTypeX ze res_kind + -- See Note [Unifying data family kinds] about the discardCast + ; lhs_ty <- zonkTcTypeToTypeX ze (discardCast lhs_ty) ; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta -- Check that type patterns match the class instance head - ; let pats = unravelFamInstPats lhs_ty - ; return (qtvs, pats, res_kind, stupid_theta) } + -- The call to splitTyConApp_maybe here is just an inlining of + -- the body of unravelFamInstPats. + ; pats <- case splitTyConApp_maybe lhs_ty of + Just (_, pats) -> pure pats + Nothing -> pprPanic "tcDataFamHeader" (ppr lhs_ty) + ; return (qtvs, pats, typeKind lhs_ty, stupid_theta) } + -- See Note [Unifying data family kinds] about why we need typeKind here where fam_name = tyConName fam_tc data_ctxt = DataKindCtxt fam_name pp_lhs = pprHsFamInstLHS fam_name mb_bndrs hs_pats fixity hs_ctxt exp_bndrs = mb_bndrs `orElse` [] - -- See Note [Result kind signature for a data family instance] + -- See Note [Implementation of UnliftedNewtypes] in TcTyClsDecls, wrinkle (2). tc_kind_sig Nothing - = return liftedTypeKind + = do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes + ; if unlifted_newtypes && new_or_data == NewType + then newOpenTypeKind + else pure liftedTypeKind + } + + -- See Note [Result kind signature for a data family instance] tc_kind_sig (Just hs_kind) = do { sig_kind <- tcLHsKindSig data_ctxt hs_kind ; let (tvs, inner_kind) = tcSplitForAllTys sig_kind @@ -852,6 +877,36 @@ we actually have a place to put the regeneralised variables. Thus: skolemise away. cf. Inst.deeplySkolemise and TcUnify.tcSkolemise Examples in indexed-types/should_compile/T12369 +Note [Unifying data family kinds] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When we kind-check a newtype instance with -XUnliftedNewtypes, we must +unify the kind of the data family with any declared kind in the instance +declaration. For example: + + data Color = Red | Blue + type family Interpret (x :: Color) :: RuntimeRep where + Interpret 'Red = 'IntRep + Interpret 'Blue = 'WordRep + data family Foo (x :: Color) :: TYPE (Interpret x) + newtype instance Foo 'Red :: TYPE IntRep where + FooRedC :: Int# -> Foo 'Red + +We end up unifying `TYPE (Interpret 'Red)` (the kind of Foo, instantiated +with 'Red) and `TYPE IntRep` (the declared kind of the instance). This +unification succeeds, resulting in a coercion. The big question: what to +do with this coercion? Answer: nothing! A kind annotation on a newtype instance +is always redundant (except, perhaps, in that it helps guide unification). We +have a definitive kind for the data family from the data family declaration, +and so we learn nothing really new from the kind signature on an instance. +We still must perform this unification (done in the call to checkExpectedKind +toward the beginning of tcDataFamHeader), but the result is unhelpful. If there +is a cast, it will wrap the lhs_ty, and so we just drop it before splitting the +lhs_ty to reveal the underlying patterns. Because of the potential of dropping +a cast like this, we just use typeKind in the result instead of propagating res_kind +from above. + +This Note is wrinkle (3) in Note [Implementation of UnliftedNewtypes] in TcTyClsDecls. + Note [Eta-reduction for data families] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index fdb956aedd..31274fa05f 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -80,6 +80,7 @@ module TcMType ( zonkCt, zonkSkolemInfo, tcGetGlobalTyCoVars, + skolemiseUnboundMetaTyVar, ------------------------------ -- Levity polymorphism diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index a181377b62..d16be28773 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -30,9 +30,7 @@ import GhcPrelude import Bag import Class ( Class, classKey, classTyCon ) -import DynFlags ( WarningFlag ( Opt_WarnMonomorphism ) - , WarnReason ( Reason ) - , DynFlags( solverIterations ) ) +import DynFlags import HsExpr ( UnboundVar(..) ) import Id ( idType, mkLocalId ) import Inst @@ -229,12 +227,16 @@ simpl_top :: WantedConstraints -> TcS WantedConstraints simpl_top wanteds = do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds) -- This is where the main work happens - ; try_tyvar_defaulting wc_first_go } + ; dflags <- getDynFlags + ; try_tyvar_defaulting dflags wc_first_go } where - try_tyvar_defaulting :: WantedConstraints -> TcS WantedConstraints - try_tyvar_defaulting wc + try_tyvar_defaulting :: DynFlags -> WantedConstraints -> TcS WantedConstraints + try_tyvar_defaulting dflags wc | isEmptyWC wc = return wc + | insolubleWC wc + , gopt Opt_PrintExplicitRuntimeReps dflags -- See Note [Defaulting insolubles] + = try_class_defaulting wc | otherwise = do { free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc) ; let meta_tvs = filter (isTyVar <&&> isMetaTyVar) free_tvs @@ -252,7 +254,7 @@ simpl_top wanteds try_class_defaulting :: WantedConstraints -> TcS WantedConstraints try_class_defaulting wc - | isEmptyWC wc + | isEmptyWC wc || insolubleWC wc -- See Note [Defaulting insolubles] = return wc | otherwise -- See Note [When to do type-class defaulting] = do { something_happened <- applyDefaultingRules wc @@ -518,6 +520,50 @@ solveWantedsAndDrop, not simpl_top, so that we do no defaulting. This is ambiguous of course, but we don't want to default the (Num alpha) constraint to (Num Int)! Doing so gives a defaulting warning, but no error. + +Note [Defaulting insolubles] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If a set of wanteds is insoluble, we have no hope of accepting the +program. Yet we do not stop constraint solving, etc., because we may +simplify the wanteds to produce better error messages. So, once +we have an insoluble constraint, everything we do is just about producing +helpful error messages. + +Should we default in this case or not? Let's look at an example (tcfail004): + + (f,g) = (1,2,3) + +With defaulting, we get a conflict between (a0,b0) and (Integer,Integer,Integer). +Without defaulting, we get a conflict between (a0,b0) and (a1,b1,c1). I (Richard) +find the latter more helpful. Several other test cases (e.g. tcfail005) suggest +similarly. So: we should not do class defaulting with insolubles. + +On the other hand, RuntimeRep-defaulting is different. Witness tcfail078: + + f :: Integer i => i + f = 0 + +Without RuntimeRep-defaulting, we GHC suggests that Integer should have kind +TYPE r0 -> Constraint and then complains that r0 is actually untouchable +(presumably, because it can't be sure if `Integer i` entails an equality). +If we default, we are told of a clash between (* -> Constraint) and Constraint. +The latter seems far better, suggesting we *should* do RuntimeRep-defaulting +even on insolubles. + +But, evidently, not always. Witness UnliftedNewtypesInfinite: + + newtype Foo = FooC (# Int#, Foo #) + +This should fail with an occurs-check error on the kind of Foo (with -XUnliftedNewtypes). +If we default RuntimeRep-vars, we get + + Expecting a lifted type, but ‘(# Int#, Foo #)’ is unlifted + +which is just plain wrong. + +Conclusion: we should do RuntimeRep-defaulting on insolubles only when the user does not +want to hear about RuntimeRep stuff -- that is, when -fprint-explicit-runtime-reps +is not set. -} ------------------ diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index fc14b9605b..9d2aea8d15 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -37,6 +37,7 @@ import TcTyDecls import TcClassDcl import {-# SOURCE #-} TcInstDcls( tcInstDecls1 ) import TcDeriv (DerivInfo) +import TcUnify ( unifyKind ) import TcHsType import ClsInst( AssocInstInfo(..) ) import TcMType @@ -1030,9 +1031,15 @@ getInitialKind cusk , dd_ND = new_or_data } }) = do { let flav = newOrDataToFlavour new_or_data ; tc <- kcLHsQTyVars name flav cusk ktvs $ - case m_sig of - Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig - Nothing -> return liftedTypeKind + -- See Note [Implementation of UnliftedNewtypes] + do { unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes + ; case m_sig of + Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig + Nothing + | NewType <- new_or_data + , unlifted_newtypes -> newOpenTypeKind + | otherwise -> pure liftedTypeKind + } ; return [tc] } getInitialKind cusk (FamDecl { tcdFam = decl }) @@ -1127,8 +1134,13 @@ kcTyClDecl :: TyClDecl GhcRn -> TcM () kcTyClDecl (DataDecl { tcdLName = (dL->L _ name) , tcdDataDefn = defn }) | HsDataDefn { dd_cons = cons@((dL->L _ (ConDeclGADT {})) : _) - , dd_ctxt = (dL->L _ []) } <- defn - = mapM_ (wrapLocM_ kcConDecl) cons + , dd_ctxt = (dL->L _ []) + , dd_ND = new_or_data } <- defn + = do { tyCon <- kcLookupTcTyCon name + -- See Note [Implementation of UnliftedNewtypes] STEP 2 + ; (_, final_res_kind) <- etaExpandAlgTyCon (tyConBinders tyCon) (tyConResKind tyCon) + ; mapM_ (wrapLocM_ (kcConDecl new_or_data final_res_kind)) cons + } -- hs_tvs and dd_kindSig already dealt with in getInitialKind -- This must be a GADT-style decl, -- (see invariants of DataDefn declaration) @@ -1136,10 +1148,14 @@ kcTyClDecl (DataDecl { tcdLName = (dL->L _ name) -- ConDecls bind all their own variables -- (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it - | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn + | HsDataDefn { dd_ctxt = ctxt + , dd_cons = cons + , dd_ND = new_or_data } <- defn = bindTyClTyVars name $ \ _ _ -> - do { _ <- tcHsContext ctxt - ; mapM_ (wrapLocM_ kcConDecl) cons } + do { _ <- tcHsContext ctxt + ; tyCon <- kcLookupTcTyCon name + ; mapM_ (wrapLocM_ (kcConDecl new_or_data (tyConResKind tyCon))) cons + } kcTyClDecl (SynDecl { tcdLName = dL->L _ name, tcdRhs = rhs }) = bindTyClTyVars name $ \ _ res_kind -> @@ -1172,23 +1188,66 @@ kcTyClDecl (DataDecl _ _ _ _ (XHsDataDefn _)) = panic "kcTyClDecl" kcTyClDecl (XTyClDecl _) = panic "kcTyClDecl" ------------------- -kcConDecl :: ConDecl GhcRn -> TcM () -kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs - , con_mb_cxt = ex_ctxt, con_args = args }) + +-- | Unify the kind of the first type provided with the newtype's kind, if +-- -XUnliftedNewtypes is enabled and the NewOrData indicates Newtype. If there +-- is more than one type provided, do nothing: the newtype is in error, and this +-- will be caught in validity checking (which will give a better error than we can +-- here.) +unifyNewtypeKind :: DynFlags + -> NewOrData + -> [LHsType GhcRn] -- user-written argument types, should be just 1 + -> [TcType] -- type-checked argument types, should be just 1 + -> TcKind -- expected kind of newtype + -> TcM [TcType] -- casted argument types (should be just 1) + -- result = orig_arg |> kind_co + -- where kind_co :: orig_arg_ki ~N expected_ki +unifyNewtypeKind dflags NewType [hs_ty] [tc_ty] ki + | xopt LangExt.UnliftedNewtypes dflags + = do { traceTc "unifyNewtypeKind" (ppr hs_ty $$ ppr tc_ty $$ ppr ki) + ; co <- unifyKind (Just (unLoc hs_ty)) (typeKind tc_ty) ki + ; return [tc_ty `mkCastTy` co] } + -- See comments above: just do nothing here +unifyNewtypeKind _ _ _ arg_tys _ = return arg_tys + +-- Type check the types of the arguments to a data constructor. +-- This includes doing kind unification if the type is a newtype. +-- See Note [Implementation of UnliftedNewtypes] for why we need +-- the first two arguments. +kcConArgTys :: NewOrData -> Kind -> [LHsType GhcRn] -> TcM () +kcConArgTys new_or_data res_kind arg_tys = do + { arg_tc_tys <- mapM (tcHsOpenType . getBangType) arg_tys + -- See Note [Implementation of UnliftedNewtypes], STEP 2 + ; dflags <- getDynFlags + ; discardResult $ + unifyNewtypeKind dflags new_or_data arg_tys arg_tc_tys res_kind + } + +-- Kind check a data constructor. In additional to the data constructor, +-- we also need to know about whether or not its corresponding type was +-- declared with data or newtype, and we need to know the result kind of +-- this type. See Note [Implementation of UnliftedNewtypes] for why +-- we need the first two arguments. +kcConDecl :: + NewOrData -- Was the corresponding type declared with data or newtype? + -> Kind -- The result kind of the corresponding type constructor + -> ConDecl GhcRn -- The data constructor + -> TcM () +kcConDecl new_or_data res_kind (ConDeclH98 + { con_name = name, con_ex_tvs = ex_tvs + , con_mb_cxt = ex_ctxt, con_args = args }) = addErrCtxt (dataConCtxtName [name]) $ discardResult $ bindExplicitTKBndrs_Tv ex_tvs $ do { _ <- tcHsMbContext ex_ctxt - ; traceTc "kcConDecl {" (ppr name $$ ppr args) - ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args) - ; traceTc "kcConDecl }" (ppr name) + ; kcConArgTys new_or_data res_kind (hsConDeclArgTys args) + -- We don't need to check the telescope here, because that's + -- done in tcConDecl } - -- We don't need to check the telescope here, because that's - -- done in tcConDecl -kcConDecl (ConDeclGADT { con_names = names - , con_qvars = qtvs, con_mb_cxt = cxt - , con_args = args, con_res_ty = res_ty }) +kcConDecl new_or_data res_kind (ConDeclGADT + { con_names = names, con_qvars = qtvs, con_mb_cxt = cxt + , con_args = args, con_res_ty = res_ty }) | HsQTvs { hsq_ext = implicit_tkv_nms , hsq_explicit = explicit_tkv_nms } <- qtvs = -- Even though the data constructor's type is closed, we @@ -1204,11 +1263,11 @@ kcConDecl (ConDeclGADT { con_names = names bindExplicitTKBndrs_Tv explicit_tkv_nms $ -- Why "_Tv"? See Note [Kind-checking for GADTs] do { _ <- tcHsMbContext cxt - ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args) + ; kcConArgTys new_or_data res_kind (hsConDeclArgTys args) ; _ <- tcHsOpenType res_ty ; return () } -kcConDecl (XConDecl _) = panic "kcConDecl" -kcConDecl (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _) = panic "kcConDecl" +kcConDecl _ _ (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _) = panic "kcConDecl" +kcConDecl _ _ (XConDecl _) = panic "kcConDecl" {- Note [Recursion and promoting data constructors] @@ -1354,6 +1413,112 @@ For wired-in things we simply ignore the declaration and take the wired-in information. That avoids complications. e.g. the need to make the data constructor worker name for a constraint tuple match the wired-in one + +Note [Implementation of UnliftedNewtypes] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Expected behavior of UnliftedNewtypes: + +* Proposal: https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0013-unlifted-newtypes.rst +* Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/98 + +What follows is a high-level overview of the implementation of the +proposal. + +STEP 1: Getting the initial kind, as done by getInitialKind. We have +two sub-cases (assuming we have a newtype and -XUnliftedNewtypes is enabled): + +* With a CUSK: no change in kind-checking; the tycon is given the kind + the user writes, whatever it may be. + +* Without a CUSK: If there is no kind signature, the tycon is given + a kind `TYPE r`, for a fresh unification variable `r`. + +STEP 2: Kind-checking, as done by kcTyClDecl. This step is skipped for CUSKs. +The key function here is kcConDecl, which looks at an individual constructor +declaration. In the unlifted-newtypes case (i.e., -XUnliftedNewtypes and, +indeed, we are processing a newtype), we call unifyNewtypeKind, which is a +thin wrapper around unifyKind, unifying the kind of the one argument and the +result kind of the newtype tycon. + +Examples of newtypes affected by STEP 2, assuming -XUnliftedNewtypes is +enabled (we use r0 to denote a unification variable): + +newtype Foo rep = MkFoo (forall (a :: TYPE rep). a) ++ kcConDecl unifies (TYPE r0) with (TYPE rep), where (TYPE r0) + is the kind that getInitialKind invented for (Foo rep). + +data Color = Red | Blue +type family Interpret (x :: Color) :: RuntimeRep where + Interpret 'Red = 'IntRep + Interpret 'Blue = 'WordRep +data family Foo (x :: Color) :: TYPE (Interpret x) +newtype instance Foo 'Red = FooRedC Int# ++ kcConDecl unifies TYPE (Interpret 'Red) with TYPE 'IntRep + +Note that, in the GADT case, we might have a kind signature with arrows +(newtype XYZ a b :: Type -> Type where ...). We want only the final +component of the kind for checking in kcConDecl, so we call etaExpandAlgTyCon +in kcTyClDecl. + +STEP 3: Type-checking (desugaring), as done by tcTyClDecl. The key function +here is tcConDecl. Once again, we must call unifyNewtypeKind, for two reasons: + + A. It is possible that a GADT has a CUSK. (Note that this is *not* + possible for H98 types. Recall that CUSK types don't go through + kcTyClDecl, so we might not have done this kind check. + B. We need to produce the coercion to put on the argument type + if the kinds are different (for both H98 and GADT). + +Example of (B): + +type family F a where + F Int = LiftedRep + +newtype N :: TYPE (F Int) where + MkN :: Int -> N + +We really need to have the argument to MkN be (Int |> TYPE (sym axF)), where +axF :: F Int ~ LiftedRep. That way, the argument kind is the same as the +newtype kind, which is the principal correctness condition for newtypes. +This call to unifyNewtypeKind is what produces that coercion. + +Note that this is possible in the H98 case only for a data family, because +the H98 syntax doesn't permit a kind signature on the newtype itself. + + +1. In tcFamDecl1, we suppress a tcIsLiftedTypeKind check if + UnliftedNewtypes is on. This allows us to write things like: + data family Foo :: TYPE 'IntRep + +2. In a newtype instance (with -XUnliftedNewtypes), if the user does + not write a kind signature, we want to allow the possibility that + the kind is not Type, so we use newOpenTypeKind instead of liftedTypeKind. + This is done in tcDataFamHeader in TcInstDcls. Example: + + data family Bar (a :: RuntimeRep) :: TYPE a + newtype instance Bar 'IntRep = BarIntC Int# + newtype instance Bar 'WordRep :: TYPE 'WordRep where + BarWordC :: Word# -> Bar 'WordRep + + The data instance corresponding to IntRep does not specify a kind signature, + so tc_kind_sig just returns `TYPE r0` (where `r0` is a fresh metavariable). + The data instance corresponding to WordRep does have a kind signature, so + we use that kind signature. + +3. A data family and its newtype instance may be declared with slightly + different kinds. See Note [Unifying data family kinds] in TcInstDcls. + +There's also a change in the renamer: + +* In RnSource.rnTyClDecl, enabling UnliftedNewtypes changes what is means + for a newtype to have a CUSK. This is necessary since UnliftedNewtypes + means that, for newtypes without kind signatures, we must use the field + inside the data constructor to determine the result kind. + See Note [Unlifted Newtypes and CUSKs] for more detail. + +For completeness, it was also neccessary to make coerce work on +unlifted types, resolving #13595. + -} tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM TyCon @@ -1709,11 +1874,18 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info -- Type or a kind-variable -- For the latter, consider -- data family D a :: forall k. Type -> k + -- When UnliftedNewtypes is enabled, we loosen this restriction + -- on the return kind. See Note [Implementation of UnliftedNewtypes], wrinkle (1). ; let (_, final_res_kind) = splitPiTys res_kind - ; checkTc (tcIsLiftedTypeKind final_res_kind - || isJust (tcGetCastedTyVar_maybe final_res_kind)) - (badKindSig False res_kind) - + ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes + ; checkTc + ( (if unlifted_newtypes + then tcIsRuntimeTypeKind final_res_kind + else tcIsLiftedTypeKind final_res_kind + ) + || isJust (tcGetCastedTyVar_maybe final_res_kind) + ) + (badKindSig False res_kind) ; tc_rep_name <- newTyConRepName tc_name ; let tycon = mkFamilyTyCon tc_name binders res_kind @@ -1860,10 +2032,16 @@ tcDataDefn roles_info ; tcg_env <- getGblEnv ; (extra_bndrs, final_res_kind) <- etaExpandAlgTyCon tycon_binders res_kind - ; let hsc_src = tcg_src tcg_env - ; unless (mk_permissive_kind hsc_src cons) $ - checkTc (tcIsLiftedTypeKind final_res_kind) (badKindSig True res_kind) + ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes + ; let allowUnlifted = unlifted_newtypes && new_or_data == NewType + ; unless (mk_permissive_kind hsc_src cons || allowUnlifted) $ + checkTc + (if allowUnlifted + then tcIsRuntimeTypeKind final_res_kind + else tcIsLiftedTypeKind final_res_kind + ) + (badKindSig True res_kind) ; stupid_tc_theta <- pushTcLevelM_ $ solveEqualities $ tcHsContext ctxt ; stupid_theta <- zonkTcTypesToTypes stupid_tc_theta @@ -1877,8 +2055,13 @@ tcDataDefn roles_info { let final_bndrs = tycon_binders `chkAppend` extra_bndrs res_ty = mkTyConApp tycon (mkTyVarTys (binderVars final_bndrs)) roles = roles_info tc_name - - ; data_cons <- tcConDecls tycon final_bndrs res_ty cons + ; data_cons <- tcConDecls + tycon + new_or_data + final_bndrs + final_res_kind + res_ty + cons ; tc_rhs <- mk_tc_rhs hsc_src tycon data_cons ; tc_rep_nm <- newTyConRepName tc_name ; return (mkAlgTyCon tc_name @@ -1976,11 +2159,9 @@ tcTyFamInstEqn fam_tc mb_clsinfo vis_pats = numVisibleArgs hs_pats ; checkTc (vis_pats == vis_arity) $ wrongNumberOfParmsErr vis_arity - ; (qtvs, pats, rhs_ty) <- tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars (mb_expl_bndrs `orElse` []) hs_pats hs_rhs_ty - -- Don't print results they may be knot-tied -- (tcFamInstEqnGuts zonks to Type) ; return (mkCoAxBranch qtvs [] [] pats rhs_ty @@ -2015,7 +2196,7 @@ indexed-types/should_compile/T12369 for an example. So, the kind-checker must return the new skolems and args (that is, Type or (Type -> Type) for the equations above) and the instantiated kind. -Note [Generalising in tcFamTyPatsGuts] +Note [Generalising in tcTyFamInstEqnGuts] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we have something like type instance forall (a::k) b. F t1 t2 = rhs @@ -2073,7 +2254,7 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty ; rhs_ty <- tcCheckLHsType hs_rhs_ty rhs_kind ; return (lhs_ty, rhs_ty) } - -- See Note [Generalising in tcFamTyPatsGuts] + -- See Note [Generalising in tcTyFamInstEqnGuts] -- This code (and the stuff immediately above) is very similar -- to that in tcDataFamHeader. Maybe we should abstract the -- common code; but for the moment I concluded that it's @@ -2130,15 +2311,12 @@ unravelFamInstPats :: TcType -> [TcType] unravelFamInstPats fam_app = case splitTyConApp_maybe fam_app of Just (_, pats) -> pats - Nothing -> WARN( True, bad_lhs fam_app ) [] + Nothing -> panic "unravelFamInstPats: Ill-typed LHS of family instance" -- The Nothing case cannot happen for type families, because -- we don't call unravelFamInstPats until we've solved the - -- equalities. For data families I wasn't quite as convinced - -- so I've let it as a warning rather than a panic. - where - bad_lhs fam_app - = hang (text "Ill-typed LHS of family instance") - 2 (debugPprType fam_app) + -- equalities. For data families, it shouldn't happen either, + -- we need to fail hard and early if it does. See trac issue #15905 + -- for an example of this happening. addConsistencyConstraints :: AssocInstInfo -> TcType -> TcM () -- In the corresponding positions of the class and type-family, @@ -2295,25 +2473,26 @@ consUseGadtSyntax _ = False -- All constructors have same shape ----------------------------------- -tcConDecls :: KnotTied TyCon -> [KnotTied TyConBinder] -> KnotTied Type - -> [LConDecl GhcRn] -> TcM [DataCon] - -- Why both the tycon tyvars and binders? Because the tyvars - -- have all the names and the binders have the visibilities. -tcConDecls rep_tycon tmpl_bndrs res_tmpl +tcConDecls :: KnotTied TyCon -> NewOrData + -> [TyConBinder] -> TcKind -- binders and result kind of tycon + -> KnotTied Type -> [LConDecl GhcRn] -> TcM [DataCon] +tcConDecls rep_tycon new_or_data tmpl_bndrs res_kind res_tmpl = concatMapM $ addLocM $ - tcConDecl rep_tycon (mkTyConTagMap rep_tycon) tmpl_bndrs res_tmpl + tcConDecl rep_tycon (mkTyConTagMap rep_tycon) + tmpl_bndrs res_kind res_tmpl new_or_data -- It's important that we pay for tag allocation here, once per TyCon, -- See Note [Constructor tag allocation], fixes #14657 tcConDecl :: KnotTied TyCon -- Representation tycon. Knot-tied! -> NameEnv ConTag - -> [KnotTied TyConBinder] -> KnotTied Type - -- Return type template (with its template tyvars) - -- (tvs, T tys), where T is the family TyCon + -> [TyConBinder] -> TcKind -- tycon binders and result kind + -> KnotTied Type + -- Return type template (T tys), where T is the family TyCon + -> NewOrData -> ConDecl GhcRn -> TcM [DataCon] -tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl +tcConDecl rep_tycon tag_map tmpl_bndrs res_kind res_tmpl new_or_data (ConDeclH98 { con_name = name , con_ex_tvs = explicit_tkv_nms , con_mb_cxt = hs_ctxt @@ -2337,7 +2516,12 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl ; btys <- tcConArgs hs_args ; field_lbls <- lookupConstructorFields (unLoc name) ; let (arg_tys, stricts) = unzip btys - ; return (ctxt, arg_tys, field_lbls, stricts) + ; dflags <- getDynFlags + ; final_arg_tys <- + unifyNewtypeKind dflags new_or_data + (hsConDeclArgTys hs_args) + arg_tys res_kind + ; return (ctxt, final_arg_tys, field_lbls, stricts) } -- exp_tvs have explicit, user-written binding sites @@ -2393,7 +2577,9 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl ; mapM buildOneDataCon [name] } -tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl +tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data + -- NB: don't use res_kind here, as it's ill-scoped. Instead, we get + -- the res_kind by typechecking the result type. (ConDeclGADT { con_names = names , con_qvars = qtvs , con_mb_cxt = cxt, con_args = hs_args @@ -2412,13 +2598,19 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl bindExplicitTKBndrs_Skol explicit_tkv_nms $ do { ctxt <- tcHsMbContext cxt ; btys <- tcConArgs hs_args - ; res_ty <- tcHsLiftedType hs_res_ty - ; field_lbls <- lookupConstructorFields name ; let (arg_tys, stricts) = unzip btys - ; return (ctxt, arg_tys, res_ty, field_lbls, stricts) + ; res_ty <- tcHsOpenType hs_res_ty + -- See Note [Implementation of unlifted newtypes] + ; dflags <- getDynFlags + ; final_arg_tys <- + unifyNewtypeKind dflags new_or_data + (hsConDeclArgTys hs_args) + arg_tys (typeKind res_ty) + ; field_lbls <- lookupConstructorFields name + ; return (ctxt, final_arg_tys, res_ty, field_lbls, stricts) } ; imp_tvs <- zonkAndScopedSort imp_tvs - ; let user_tvs = imp_tvs ++ exp_tvs + ; let user_tvs = imp_tvs ++ exp_tvs ; tkvs <- kindGeneralize (mkSpecForAllTys user_tvs $ mkPhiTy ctxt $ @@ -2471,9 +2663,9 @@ tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl ; traceTc "tcConDecl 2" (ppr names) ; mapM buildOneDataCon names } -tcConDecl _ _ _ _ (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _) +tcConDecl _ _ _ _ _ _ (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _) = panic "tcConDecl" -tcConDecl _ _ _ _ (XConDecl _) = panic "tcConDecl" +tcConDecl _ _ _ _ _ _ (XConDecl _) = panic "tcConDecl" tcConIsInfixH98 :: Name -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn]) @@ -2580,11 +2772,10 @@ errors reported in one pass. See #7175, and #10836. rejigConRes :: [KnotTied TyConBinder] -> KnotTied Type -- Template for result type; e.g. -- data instance T [a] b c ... -- gives template ([a,b,c], T [a] b c) - -- Type must be of kind *! -> [TyVar] -- The constructor's inferred type variables -> [TyVar] -- The constructor's user-written, specified -- type variables - -> KnotTied Type -- res_ty type must be of kind * + -> KnotTied Type -- res_ty -> ([TyVar], -- Universal [TyVar], -- Existential (distinct OccNames from univs) [TyVar], -- The constructor's rejigged, user-written, @@ -2613,9 +2804,7 @@ rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty -- So we return ( [a,b,z], [x,y] -- , [], [x,y,z] -- , [a~(x,y),b~z], <arg-subst> ) - | Just subst <- ASSERT( isLiftedTypeKind (tcTypeKind res_ty) ) - ASSERT( isLiftedTypeKind (tcTypeKind res_tmpl) ) - tcMatchTy res_tmpl res_ty + | Just subst <- tcMatchTy res_tmpl res_ty = let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tmpl_tvs dc_tvs subst raw_ex_tvs = dc_tvs `minusList` univ_tvs (arg_subst, substed_ex_tvs) = substTyVarBndrs kind_subst raw_ex_tvs @@ -3153,8 +3342,13 @@ checkValidDataCon dflags existential_ok tc con -- Check all argument types for validity ; checkValidType ctxt (dataConUserType con) - ; mapM_ (checkForLevPoly empty) - (dataConOrigArgTys con) + + -- If we are dealing with a newtype, we allow levity polymorphism + -- regardless of whether or not UnliftedNewtypes is enabled. A + -- later check in checkNewDataCon handles this, producing a + -- better error message than checkForLevPoly would. + ; unless (isNewTyCon tc) + (mapM_ (checkForLevPoly empty) (dataConOrigArgTys con)) -- Extra checks for newtype data constructors ; when (isNewTyCon tc) (checkNewDataCon con) @@ -3237,8 +3431,13 @@ checkNewDataCon con = do { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys)) -- One argument - ; checkTc (not (isUnliftedType arg_ty1)) $ - text "A newtype cannot have an unlifted argument type" + ; unlifted_newtypes <- xoptM LangExt.UnliftedNewtypes + ; let allowedArgType = + unlifted_newtypes || isLiftedType_maybe arg_ty1 == Just True + ; checkTc allowedArgType $ vcat + [ text "A newtype cannot have an unlifted argument type" + , text "Perhaps you intended to use UnliftedNewtypes" + ] ; check_con (null eq_spec) $ text "A newtype constructor must have a return type of form T a1 ... an" diff --git a/compiler/typecheck/TcTypeable.hs b/compiler/typecheck/TcTypeable.hs index cf7700a98f..3488957366 100644 --- a/compiler/typecheck/TcTypeable.hs +++ b/compiler/typecheck/TcTypeable.hs @@ -17,7 +17,7 @@ import GhcPrelude import BasicTypes ( Boxity(..), neverInlinePragma, SourceText(..) ) import TcBinds( addTypecheckedBinds ) import IfaceEnv( newGlobalBinder ) -import TyCoRep( Type(..), TyLit(..) ) +import TyCoRep( Type(..), TyLit(..), isLiftedTypeKind ) import TcEnv import TcEvidence ( mkWpTyApps ) import TcRnMonad @@ -426,12 +426,14 @@ tyConIsTypeable tc = -- polytypes and types containing casts (which may be, for instance, a type -- family). typeIsTypeable :: Type -> Bool --- We handle types of the form (TYPE rep) specifically to avoid --- looping on (tyConIsTypeable RuntimeRep) +-- We handle types of the form (TYPE LiftedRep) specifically to avoid +-- looping on (tyConIsTypeable RuntimeRep). We used to consider (TYPE rr) +-- to be typeable without inspecting rr, but this exhibits bad behavior +-- when rr is a type family. typeIsTypeable ty | Just ty' <- coreView ty = typeIsTypeable ty' typeIsTypeable ty - | isJust (kindRep_maybe ty) = True + | isLiftedTypeKind ty = True typeIsTypeable (TyVarTy _) = True typeIsTypeable (AppTy a b) = typeIsTypeable a && typeIsTypeable b typeIsTypeable (FunTy _ a b) = typeIsTypeable a && typeIsTypeable b diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs index 8e4efbac50..81331e0b8e 100644 --- a/compiler/types/Coercion.hs +++ b/compiler/types/Coercion.hs @@ -62,7 +62,7 @@ module Coercion ( pickLR, isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe, - isReflCoVar_maybe, + isReflCoVar_maybe, isGReflMCo, coToMCo, -- ** Coercion variables mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique, @@ -592,6 +592,11 @@ isReflexiveCo_maybe co = Nothing where (Pair ty1 ty2, r) = coercionKindRole co +coToMCo :: Coercion -> MCoercion +coToMCo c = if isReflCo c + then MRefl + else MCo c + {- %************************************************************************ %* * diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index ff4501985e..f12a75f89a 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -59,6 +59,7 @@ module Type ( getRuntimeRep_maybe, kindRep_maybe, kindRep, mkCastTy, mkCoercionTy, splitCastTy_maybe, + discardCast, userTypeError_maybe, pprUserTypeErrorTy, @@ -137,6 +138,7 @@ module Type ( -- ** Finding the kind of a type typeKind, tcTypeKind, isTypeLevPoly, resultIsLevPoly, tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind, + tcIsRuntimeTypeKind, -- ** Common Kind liftedTypeKind, @@ -1277,6 +1279,21 @@ tyConBindersTyCoBinders = map to_tyb to_tyb (Bndr tv (NamedTCB vis)) = Named (Bndr tv vis) to_tyb (Bndr tv (AnonTCB af)) = Anon af (varType tv) +-- | Drop the cast on a type, if any. If there is no +-- cast, just return the original type. This is rarely what +-- you want. The CastTy data constructor (in TyCoRep) has the +-- invariant that another CastTy is not inside. See the +-- data constructor for a full description of this invariant. +-- Since CastTy cannot be nested, the result of discardCast +-- cannot be a CastTy. +discardCast :: Type -> Type +discardCast (CastTy ty _) = ASSERT(not (isCastTy ty)) ty + where + isCastTy CastTy{} = True + isCastTy _ = False +discardCast ty = ty + + {- -------------------------------------------------------------------- CoercionTy @@ -1827,6 +1844,17 @@ tcIsLiftedTypeKind ty | otherwise = False +-- | Is this kind equivalent to @TYPE r@ (for some unknown r)? +-- +-- This considers 'Constraint' to be distinct from @*@. +tcIsRuntimeTypeKind :: Kind -> Bool +tcIsRuntimeTypeKind ty + | Just (tc, _) <- tcSplitTyConApp_maybe ty -- Note: tcSplit here + , tc `hasKey` tYPETyConKey + = True + | otherwise + = False + tcReturnsConstraintKind :: Kind -> Bool -- True <=> the Kind ultimately returns a Constraint -- E.g. * -> Constraint diff --git a/docs/users_guide/8.10.1-notes.rst b/docs/users_guide/8.10.1-notes.rst index fde1451250..dfbb8f9224 100644 --- a/docs/users_guide/8.10.1-notes.rst +++ b/docs/users_guide/8.10.1-notes.rst @@ -10,6 +10,8 @@ following sections. Highlights ---------- +- The `UnliftedNewtypes` extension. + Full details ------------ @@ -83,6 +85,11 @@ Language type forall a (f :: forall k. k -> Type). T a f = f Int +- A new extension :extension:`UnliftedNewtypes` that relaxes restrictions + around what kinds of types can appear inside of the data constructor + for a `newtype`. This was proposed in + `GHC proposal #13 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0013-unlifted-newtypes.rst>`__. + Compiler ~~~~~~~~ diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index fdc3b2cafa..36e29c5253 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -178,6 +178,10 @@ There are some restrictions on the use of primitive types: newtype A = MkA Int# + However, this restriction can be relaxed by enabling + :extension:`-XUnliftedNewtypes`. The `section on unlifted newtypes + <#unlifted-newtypes>`__ details the behavior of such types. + - You cannot bind a variable with an unboxed type in a *top-level* binding. @@ -359,6 +363,77 @@ layout for a sum type works like this: as the ``Bool``-like ``(# (# #) | (# #) #)``, the unboxed sum layout only has an ``Int32`` tag field (i.e., the whole thing is represented by an integer). +.. _unlifted-newtypes: + +Unlifted Newtypes +----------------- + +.. extension:: UnliftedNewtypes + :shortdesc: Enable unlifted newtypes. + + :since: 8.10.1 + + Enable the use of newtypes over types with non-lifted runtime representations. + +``-XUnliftedNewtypes`` relaxes the restrictions around what types can appear inside +of a `newtype`. For example, the type :: + + newtype A = MkA Int# + +is accepted when this extension is enabled. This creates a type +``A :: TYPE 'IntRep`` and a data constructor ``MkA :: Int# -> A``. +Although the kind of ``A`` is inferred by GHC, there is nothing visually +distictive about this type that indicated that is it not of kind ``Type`` +like newtypes typically are. `GADTSyntax <#gadt-style>`__ can be used to +provide a kind signature for additional clarity :: + + newtype A :: TYPE 'IntRep where + MkA :: Int# -> A + +The ``Coercible`` machinery works with unlifted newtypes just like it does with +lifted types. In either of the equivalent formulations of ``A`` given above, +users would additionally have access to a coercion between ``A`` and ``Int#``. + +As a consequence of the +`levity-polymorphic binder restriction <#levity-polymorphic-restrictions>`__, +levity-polymorphic fields are disallowed in data constructors +of data types declared using ``data``. However, since ``newtype`` data +constructor application is implemented as a coercion instead of as function +application, this restriction does not apply to the field inside a ``newtype`` +data constructor. Thus, the type checker accepts :: + + newtype Identity# :: forall (r :: RuntimeRep). TYPE r -> TYPE r where + MkIdentity# :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Identity# a + +And with `UnboxedSums <#unboxed-sums>`__ enabled :: + + newtype Maybe# :: forall (r :: RuntimeRep). TYPE r -> TYPE (SumRep '[r, TupleRep '[]]) where + MkMaybe# :: forall (r :: RuntimeRep) (a :: TYPE r). (# a | (# #) #) -> Maybe# a + +This extension also relaxes some of the restrictions around data families. +It must be enabled in modules where either of the following occur: + +- A data family is declared with a kind other than ``Type``. Both ``Foo`` + and ``Bar``, defined below, fall into this category: + :: + class Foo a where + data FooKey a :: TYPE 'IntRep + class Bar (r :: RuntimeRep) where + data BarType r :: TYPE r + +- A ``newtype instance`` is written with a kind other than ``Type``. The + following instances of ``Foo`` and ``Bar`` as defined above fall into + this category. + :: + instance Foo Bool where + newtype FooKey Bool = FooKeyBoolC Int# + instance Bar 'WordRep where + newtype BarType 'WordRep = BarTypeWordRepC Word# + +This extension impacts the determination of whether or not a newtype has +a Complete User-Specified Kind Signature (CUSK). The exact impact is specified +`the section on CUSKs <#complete-kind-signatures>`__. + .. _syntax-extns: Syntactic extensions @@ -9097,6 +9172,20 @@ signature" for a type constructor? These are the forms: data T2 :: forall k. k -> Type -- CUSK: `k` is bound explicitly data T3 :: forall (k :: Type). k -> Type -- still a CUSK +- For a newtype, the rules are the same as they are for a data type + unless `UnliftedNewtypes <#unboxed-newtypes>`__ is enabled. + With `UnliftedNewtypes <#unboxed-newtypes>`__, the type constructor + only has a CUSK if a kind signature is present. As with a datatype + with a top-level ``::``, all kind variables must introduced after + the ``::`` must be explicitly quantified :: + + {-# LANGUAGE UnliftedNewtypes #-} + newtype N1 where -- No; missing kind signature + newtype N2 :: TYPE 'IntRep where -- Yes; kind signature present + newtype N3 (a :: Type) where -- No; missing kind signature + newtype N4 :: k -> Type where -- No; `k` is not explicitly quantified + newtype N5 :: forall (k :: Type). k -> Type where -- Yes; good signature + - For a class, every type variable must be annotated with a kind. - For a type synonym, every type variable and the result type must all @@ -9617,6 +9706,8 @@ thus say that ``->`` has type ``TYPE r1 -> TYPE r2 -> TYPE 'LiftedRep``. The result is always lifted because all functions are lifted in GHC. +.. _levity-polymorphic-restrictions: + No levity-polymorphic variables or arguments -------------------------------------------- diff --git a/libraries/base/Control/Category.hs b/libraries/base/Control/Category.hs index e8184956f2..96f0c33aed 100644 --- a/libraries/base/Control/Category.hs +++ b/libraries/base/Control/Category.hs @@ -23,7 +23,7 @@ module Control.Category where import qualified GHC.Base (id,(.)) import Data.Type.Coercion import Data.Type.Equality -import GHC.Prim (coerce) +import Data.Coerce (coerce) infixr 9 . infixr 1 >>>, <<< diff --git a/libraries/base/Data/Coerce.hs b/libraries/base/Data/Coerce.hs index 9bd7f9a41a..3785b8a104 100644 --- a/libraries/base/Data/Coerce.hs +++ b/libraries/base/Data/Coerce.hs @@ -1,5 +1,6 @@ {-# LANGUAGE Unsafe #-} {-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE MagicHash #-} ----------------------------------------------------------------------------- -- | @@ -21,9 +22,11 @@ module Data.Coerce ( -- * Safe coercions - coerce, Coercible, + coerce, Coercible ) where import GHC.Prim (coerce) import GHC.Types (Coercible) -import GHC.Base () -- for build ordering; see Notes in GHC.Base for more info +-- The import of GHC.Base is for build ordering; see Notes in GHC.Base for +-- more info. +import GHC.Base () diff --git a/libraries/base/Data/Type/Coercion.hs b/libraries/base/Data/Type/Coercion.hs index b757682a62..694bedec01 100644 --- a/libraries/base/Data/Type/Coercion.hs +++ b/libraries/base/Data/Type/Coercion.hs @@ -8,6 +8,7 @@ {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} +{-# LANGUAGE MagicHash #-} ----------------------------------------------------------------------------- -- | diff --git a/libraries/base/GHC/Base.hs b/libraries/base/GHC/Base.hs index 6fd2ff735b..2649146816 100644 --- a/libraries/base/GHC/Base.hs +++ b/libraries/base/GHC/Base.hs @@ -1156,7 +1156,6 @@ The rules for map work like this. {-# RULES "map/coerce" [1] map coerce = coerce #-} - ---------------------------------------------- -- append ---------------------------------------------- diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md index a9f6fcf272..3c12e7c511 100644 --- a/libraries/base/changelog.md +++ b/libraries/base/changelog.md @@ -9,6 +9,12 @@ to detect values `<= maxBound::Word` that were incorrectly encoded using the `NatJ#` constructor. + * The type of `coerce` has been generalized. It is now runtime-representation + polymorphic: + `forall {r :: RuntimeRep} (a :: TYPE r) (b :: TYPE r). Coercible a b => a -> b`. + The type argument `r` is marked as `Inferred` to prevent it from + interfering with visible type application. + ## 4.13.0.0 *TBA* * Bundled with GHC *TBA* diff --git a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs index ac47e165ff..ef1d5c9f9f 100644 --- a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs +++ b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs @@ -49,6 +49,7 @@ data Extension | AllowAmbiguousTypes | UnboxedTuples | UnboxedSums + | UnliftedNewtypes | BangPatterns | TypeFamilies | TypeFamilyDependencies diff --git a/libraries/ghc-prim/GHC/Types.hs b/libraries/ghc-prim/GHC/Types.hs index 9f2d3bc15b..7d4e62c381 100644 --- a/libraries/ghc-prim/GHC/Types.hs +++ b/libraries/ghc-prim/GHC/Types.hs @@ -282,7 +282,7 @@ class a ~ b -- by Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones and Stephanie Weirich. -- -- @since 4.7.0.0 -class Coercible a b +class Coercible (a :: k) (b :: k) -- See also Note [The equality types story] in TysPrim {- ********************************************************************* diff --git a/testsuite/tests/codeGen/should_fail/T13233.stderr b/testsuite/tests/codeGen/should_fail/T13233.stderr index c3683138f8..1531abed8e 100644 --- a/testsuite/tests/codeGen/should_fail/T13233.stderr +++ b/testsuite/tests/codeGen/should_fail/T13233.stderr @@ -1,23 +1,22 @@ T13233.hs:14:11: error: - Cannot use primitive with levity-polymorphic arguments: + Cannot use function with levity-polymorphic arguments: GHC.Prim.(#,#) :: a -> a -> (# a, a #) Levity-polymorphic arguments: a :: TYPE rep a :: TYPE rep T13233.hs:22:16: error: - Cannot use primitive with levity-polymorphic arguments: - GHC.Prim.(#,#) :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep) (a :: TYPE - rep1) (b :: TYPE - rep2). + Cannot use function with levity-polymorphic arguments: + GHC.Prim.(#,#) :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep) + (a :: TYPE rep1) (b :: TYPE rep2). a -> b -> (# a, b #) Levity-polymorphic arguments: a :: TYPE rep1 b :: TYPE rep2 T13233.hs:27:10: error: - Cannot use primitive with levity-polymorphic arguments: + Cannot use function with levity-polymorphic arguments: mkWeak# :: a -> b -> (State# RealWorld -> (# State# RealWorld, c #)) diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs index 09caa7f3c4..c432e4b90e 100644 --- a/testsuite/tests/driver/T4437.hs +++ b/testsuite/tests/driver/T4437.hs @@ -39,6 +39,7 @@ expectedGhcOnlyExtensions :: [String] expectedGhcOnlyExtensions = ["RelaxedLayout", "AlternativeLayoutRule", "AlternativeLayoutRuleTransitional", + "UnliftedNewtypes", "CUSKs", "ImportQualifiedPost"] diff --git a/testsuite/tests/driver/recomp006/recomp006.stderr b/testsuite/tests/driver/recomp006/recomp006.stderr index 25b48f375f..84549b6e62 100644 --- a/testsuite/tests/driver/recomp006/recomp006.stderr +++ b/testsuite/tests/driver/recomp006/recomp006.stderr @@ -1,7 +1,6 @@ A.hs:8:8: - Couldn't match expected type ‘Int’ - with actual type ‘(Integer, Integer)’ + Couldn't match expected type ‘Int’ with actual type ‘(a0, b0)’ In the expression: (2, 3) In the expression: (1, (2, 3)) In an equation for ‘f’: f = (1, (2, 3)) diff --git a/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.hs b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.hs new file mode 100644 index 0000000000..8e0aaeef50 --- /dev/null +++ b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.hs @@ -0,0 +1,47 @@ +{-# language ForeignFunctionInterface #-} +{-# language GADTSyntax #-} +{-# language KindSignatures #-} +{-# language MagicHash #-} +{-# language UnboxedTuples #-} +{-# language UnliftedFFITypes #-} +{-# language UnliftedNewtypes #-} + +{-# OPTIONS_GHC -O2 #-} + +import Data.Kind (Type) +import Data.Word +import GHC.Exts +import GHC.IO +import GHC.Word + +foreign import ccall unsafe "head_bytearray" + c_head_bytearray_a :: MutableByteArray# RealWorld -> IO Word8 +foreign import ccall unsafe "head_bytearray" + c_head_bytearray_b :: MyArray# -> IO Word8 + +newtype MyArray# :: TYPE 'UnliftedRep where + MyArray# :: MutableByteArray# RealWorld -> MyArray# + +data MutableByteArray :: Type where + MutableByteArray :: MutableByteArray# RealWorld -> MutableByteArray + +main :: IO () +main = do + ba@(MutableByteArray ba#) <- luckySingleton + print =<< readByteArray ba 0 + print =<< c_head_bytearray_a ba# + print =<< c_head_bytearray_b (MyArray# ba#) + +readByteArray :: MutableByteArray -> Int -> IO Word8 +readByteArray (MutableByteArray b#) (I# i#) = IO $ \s0 -> + case readWord8Array# b# i# s0 of + (# s1, w #) -> (# s1, W8# w #) + +-- Create a new mutable byte array of length 1 with the sole byte +-- set to the 105. +luckySingleton :: IO MutableByteArray +luckySingleton = IO $ \s0 -> case newByteArray# 1# s0 of + (# s1, marr# #) -> case writeWord8Array# marr# 0# 105## s1 of + s2 -> (# s2, MutableByteArray marr# #) + + diff --git a/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.stdout b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.stdout new file mode 100644 index 0000000000..b9c7be5412 --- /dev/null +++ b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset.stdout @@ -0,0 +1,3 @@ +105 +105 +105 diff --git a/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset_c.c b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset_c.c new file mode 100644 index 0000000000..38f1043105 --- /dev/null +++ b/testsuite/tests/ffi/should_run/UnliftedNewtypesByteArrayOffset_c.c @@ -0,0 +1,5 @@ +#include <stdint.h> + +uint8_t head_bytearray (uint8_t *arr) { + return arr[0]; +} diff --git a/testsuite/tests/ffi/should_run/all.T b/testsuite/tests/ffi/should_run/all.T index f692d2d04a..fa78c56b80 100644 --- a/testsuite/tests/ffi/should_run/all.T +++ b/testsuite/tests/ffi/should_run/all.T @@ -208,3 +208,5 @@ test('PrimFFIInt16', [omit_ways(['ghci'])], compile_and_run, ['PrimFFIInt16_c.c' test('PrimFFIWord16', [omit_ways(['ghci'])], compile_and_run, ['PrimFFIWord16_c.c']) test('T493', [omit_ways(['ghci'])], compile_and_run, ['T493_c.c']) + +test('UnliftedNewtypesByteArrayOffset', [omit_ways(['ghci'])], compile_and_run, ['UnliftedNewtypesByteArrayOffset_c.c']) diff --git a/testsuite/tests/module/mod130.stderr b/testsuite/tests/module/mod130.stderr index 26528b148a..9e41bcdc42 100644 --- a/testsuite/tests/module/mod130.stderr +++ b/testsuite/tests/module/mod130.stderr @@ -1,5 +1,5 @@ mod130.hs:7:5: error: - Variable not in scope: (<) :: Integer -> Int -> Int + Variable not in scope: (<) :: t0 -> Int -> Int Perhaps you want to remove ‘<’ from the explicit hiding list in the import of ‘Prelude’ (mod130.hs:4:1-33). diff --git a/testsuite/tests/module/mod147.stderr b/testsuite/tests/module/mod147.stderr index 39bf7d2dc7..0a4e3fd662 100644 --- a/testsuite/tests/module/mod147.stderr +++ b/testsuite/tests/module/mod147.stderr @@ -1,3 +1,2 @@ -mod147.hs:6:5: error: - Data constructor not in scope: D :: Integer -> t +mod147.hs:6:5: error: Data constructor not in scope: D :: t0 -> t diff --git a/testsuite/tests/polykinds/T14561.stderr b/testsuite/tests/polykinds/T14561.stderr index d39dec4d7b..05814f387c 100644 --- a/testsuite/tests/polykinds/T14561.stderr +++ b/testsuite/tests/polykinds/T14561.stderr @@ -1,5 +1,5 @@ T14561.hs:12:9: error: - Cannot use primitive with levity-polymorphic arguments: + Cannot use function with levity-polymorphic arguments: unsafeCoerce# :: a -> a Levity-polymorphic arguments: a :: TYPE r diff --git a/testsuite/tests/rename/should_fail/T15607.stderr b/testsuite/tests/rename/should_fail/T15607.stderr index 9bc84f42f7..4c1111eef9 100644 --- a/testsuite/tests/rename/should_fail/T15607.stderr +++ b/testsuite/tests/rename/should_fail/T15607.stderr @@ -1,5 +1,5 @@ T15607.hs:6:10: error: - • Variable not in scope: pure :: Integer -> t + • Variable not in scope: pure :: t0 -> t • Perhaps you want to remove ‘pure’ from the explicit hiding list in the import of ‘Prelude’ (T15607.hs:4:1-36). diff --git a/testsuite/tests/safeHaskell/ghci/p4.stderr b/testsuite/tests/safeHaskell/ghci/p4.stderr index a0dc5c319e..1d416eba39 100644 --- a/testsuite/tests/safeHaskell/ghci/p4.stderr +++ b/testsuite/tests/safeHaskell/ghci/p4.stderr @@ -4,6 +4,6 @@ No module named ‘System.IO.Unsafe’ is imported. <interactive>:6:9: error: - Variable not in scope: x :: IO Integer -> t + Variable not in scope: x :: IO b0 -> t <interactive>:7:1: error: Variable not in scope: y diff --git a/testsuite/tests/safeHaskell/ghci/p6.stderr b/testsuite/tests/safeHaskell/ghci/p6.stderr index 2e68cd9a60..6213243bb0 100644 --- a/testsuite/tests/safeHaskell/ghci/p6.stderr +++ b/testsuite/tests/safeHaskell/ghci/p6.stderr @@ -6,5 +6,5 @@ foreign import ccall safe "sin" c_sin :: Double -> Double <interactive>:12:1: error: - • Variable not in scope: c_sin :: Integer -> t + • Variable not in scope: c_sin :: t0 -> t • Perhaps you meant ‘c_sin'’ (line 7) diff --git a/testsuite/tests/typecheck/should_compile/UnlifNewUnify.hs b/testsuite/tests/typecheck/should_compile/UnlifNewUnify.hs new file mode 100644 index 0000000000..d32eed4ef1 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/UnlifNewUnify.hs @@ -0,0 +1,35 @@ +{-# Language CPP #-} +{-# Language QuantifiedConstraints #-} +{-# Language TypeApplications #-} +{-# Language PolyKinds #-} +{-# Language TypeOperators #-} +{-# Language DataKinds #-} +{-# Language TypeFamilies #-} +{-# Language TypeSynonymInstances #-} +{-# Language FlexibleInstances #-} +{-# Language GADTs #-} +{-# Language UndecidableInstances #-} +{-# Language MultiParamTypeClasses #-} +{-# Language FlexibleContexts #-} +{-# LANGUAGE UnliftedNewtypes #-} + +module Bug where +import Data.Coerce +import Data.Kind + +type Cat ob = ob -> ob -> Type + +type Obj = Type + +class + Ríki (obj :: Obj) where + type (-->) :: obj -> obj -> Type + + ið :: a --> (a::obj) + +data Op a = Op a + +type family UnOp op where UnOp ('Op obj) = obj + +newtype Y :: Cat (Op a) where + Y :: (UnOp b --> UnOp a) -> Y a b diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesDifficultUnification.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesDifficultUnification.hs new file mode 100644 index 0000000000..de831f9200 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesDifficultUnification.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UnliftedNewtypes #-} + +module UnliftedNewtypesDifficultUnification where + +import GHC.Exts +import Data.Kind + +data Color = Red | Blue + +type family Interpret (x :: Color) :: RuntimeRep where + Interpret 'Red = 'IntRep + Interpret 'Blue = 'WordRep + +data family Foo (x :: Color) :: TYPE (Interpret x) +newtype instance Foo 'Red = FooRedC Int# + +newtype Quux :: TYPE (Interpret Red) where + MkQ :: Int# -> Quux + +newtype instance Foo 'Blue :: TYPE WordRep where + MkFB :: Word# -> Foo 'Blue + +type family Lower (x :: Type) :: RuntimeRep where + Lower Int = IntRep + Lower Word = WordRep + +data family Bar (x :: Color) :: TYPE (Interpret x) + +newtype instance Bar 'Red :: TYPE (Lower Int) where + MkBR :: Int# -> Bar 'Red diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesForall.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesForall.hs new file mode 100644 index 0000000000..68221cb510 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesForall.hs @@ -0,0 +1,10 @@ +{-# Language RankNTypes #-} +{-# Language KindSignatures #-} +{-# Language PolyKinds #-} +{-# Language UnliftedNewtypes #-} + +module UnliftedNewtypesForall where + +import GHC.Exts + +newtype Foo rep = MkFoo (forall (a :: TYPE rep). a) diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesGnd.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesGnd.hs new file mode 100644 index 0000000000..d664801a08 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesGnd.hs @@ -0,0 +1,20 @@ +{-# language DataKinds #-} +{-# language DerivingStrategies #-} +{-# language GeneralizedNewtypeDeriving #-} +{-# language KindSignatures #-} +{-# language MagicHash #-} +{-# language PolyKinds #-} +{-# language UnliftedNewtypes #-} + +module UnliftedNewtypesGnd where + +import GHC.Exts (Int#,TYPE,RuntimeRep(IntRep),isTrue#,(==#)) + +class LevityEq (a :: TYPE 'IntRep) where + levityEq :: a -> a -> Bool + +instance LevityEq Int# where + levityEq x y = isTrue# (x ==# y) + +newtype Foo = Foo Int# + deriving newtype (LevityEq) diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesLPFamily.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesLPFamily.hs new file mode 100644 index 0000000000..1b8a18fc7c --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesLPFamily.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE ExplicitForAll, PolyKinds, TypeFamilies, GADTs, UnliftedNewtypes #-} + +module UnliftedNewtypesLPFamily where + +import GHC.Exts + +data family DF (a :: k) :: k + +newtype instance DF (a :: TYPE r) where + MkDF :: forall (r :: RuntimeRep) (a :: TYPE r). a -> DF a diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs new file mode 100644 index 0000000000..60f97bdd53 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnassociatedFamily.hs @@ -0,0 +1,26 @@ +{-# LANGUAGE UnliftedNewtypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UnboxedTuples #-} + +module UnliftedNewtypesUnassociatedFamily where + +import GHC.Int (Int(I#)) +import GHC.Word (Word(W#)) +import GHC.Exts (Int#,Word#) +import GHC.Exts (TYPE,RuntimeRep(LiftedRep,IntRep,WordRep,TupleRep)) + +data family DFT (r :: RuntimeRep) :: TYPE r +newtype instance DFT 'IntRep = MkDFT1 Int# +newtype instance DFT 'WordRep = MkDFT2 Word# +newtype instance DFT ('TupleRep '[ 'IntRep, 'WordRep]) + = MkDFT3 (# Int#, Word# #) +data instance DFT 'LiftedRep = MkDFT4 | MkDFT5 + +data family DF :: TYPE (r :: RuntimeRep) +newtype instance DF = MkDF1 Int# +newtype instance DF = MkDF2 Word# +newtype instance DF = MkDF3 (# Int#, Word# #) +data instance DF = MkDF4 | MkDF5 diff --git a/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs new file mode 100644 index 0000000000..9f5b984025 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/UnliftedNewtypesUnifySig.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UnboxedTuples #-} +{-# LANGUAGE UnliftedNewtypes #-} + +module UnliftedNewtypesUnassociatedFamily where + +import GHC.Int (Int(I#)) +import GHC.Exts (Int#,Word#,RuntimeRep(IntRep)) +import GHC.Exts (TYPE) + +type KindOf (a :: TYPE k) = k +data family D (a :: TYPE r) :: TYPE r +newtype instance D a = MkWordD Word# +newtype instance D a :: TYPE (KindOf a) where + MkIntD :: forall (a :: TYPE 'IntRep). Int# -> D a diff --git a/testsuite/tests/typecheck/should_compile/VtaCoerce.hs b/testsuite/tests/typecheck/should_compile/VtaCoerce.hs new file mode 100644 index 0000000000..ab8d7082f7 --- /dev/null +++ b/testsuite/tests/typecheck/should_compile/VtaCoerce.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE RankNTypes, TypeApplications #-} + +module VtaCoerce where + +import Data.Coerce (coerce) + +newtype Age = Age Int + +convert :: Int -> Age +convert = coerce @Int @Age diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T index 850b271140..d0f54c0eca 100644 --- a/testsuite/tests/typecheck/should_compile/all.T +++ b/testsuite/tests/typecheck/should_compile/all.T @@ -470,6 +470,7 @@ test('T10562', normal, compile, ['']) test('T10564', normal, compile, ['']) test('Vta1', normal, compile, ['']) test('Vta2', normal, compile, ['']) +test('VtaCoerce', normal, compile, ['']) test('PushHRIf', normal, compile, ['']) test('T10632', normal, compile, ['-Wredundant-constraints']) test('T10642', normal, compile, ['']) @@ -674,3 +675,10 @@ test('T16411', normal, compile, ['']) test('T16609', normal, compile, ['']) test('T505', normal, compile, ['']) test('T12928', normal, compile, ['']) +test('UnliftedNewtypesGnd', normal, compile, ['']) +test('UnliftedNewtypesUnassociatedFamily', normal, compile, ['']) +test('UnliftedNewtypesUnifySig', normal, compile, ['']) +test('UnliftedNewtypesForall', normal, compile, ['']) +test('UnlifNewUnify', normal, compile, ['']) +test('UnliftedNewtypesLPFamily', normal, compile, ['']) +test('UnliftedNewtypesDifficultUnification', normal, compile, ['']) diff --git a/testsuite/tests/typecheck/should_compile/tc211.stderr b/testsuite/tests/typecheck/should_compile/tc211.stderr index 3342cf72e3..ccc3da6fb0 100644 --- a/testsuite/tests/typecheck/should_compile/tc211.stderr +++ b/testsuite/tests/typecheck/should_compile/tc211.stderr @@ -1,7 +1,7 @@ tc211.hs:20:8: error: • Couldn't match expected type ‘forall a. a -> a’ - with actual type ‘a3 -> a3’ + with actual type ‘a9 -> a9’ • In the expression: (:) :: (forall a. a -> a) -> [forall a. a -> a] -> [forall a. a -> a] @@ -32,7 +32,7 @@ tc211.hs:25:20: error: tc211.hs:62:18: error: • Couldn't match expected type ‘forall a. a -> a’ - with actual type ‘a2 -> a2’ + with actual type ‘a6 -> a6’ • In the expression: Cons :: (forall a. a -> a) @@ -70,10 +70,10 @@ tc211.hs:68:8: error: (\ x -> x) Nil tc211.hs:76:9: error: - • Couldn't match type ‘forall a5. a5 -> a5’ with ‘a4 -> a4’ + • Couldn't match type ‘forall a11. a11 -> a11’ with ‘a10 -> a10’ Expected type: List (forall a. a -> a) - -> (forall a. a -> a) -> a4 -> a4 - Actual type: List (a4 -> a4) -> (a4 -> a4) -> a4 -> a4 + -> (forall a. a -> a) -> a10 -> a10 + Actual type: List (a10 -> a10) -> (a10 -> a10) -> a10 -> a10 • In the expression: foo2 :: List (forall a. a -> a) -> (forall a. a -> a) -> (forall a. a -> a) diff --git a/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr b/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr index 355bfe959c..1c108f719b 100644 --- a/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr +++ b/testsuite/tests/typecheck/should_compile/valid_hole_fits.stderr @@ -68,7 +68,8 @@ valid_hole_fits.hs:24:9: warning: [-Wtyped-holes (in -Wdefault)] (and originally defined at ValidHoleFits.hs:4:12-22)) valid_hole_fits.hs:27:5: warning: [-Wtyped-holes (in -Wdefault)] - • Found hole: _ :: Integer -> Maybe Integer + • Found hole: _ :: t0 -> Maybe Integer + Where: ‘t0’ is an ambiguous type variable • In the expression: _ In the expression: _ 2 In an equation for ‘k’: k = _ 2 diff --git a/testsuite/tests/typecheck/should_fail/T10971d.stderr b/testsuite/tests/typecheck/should_fail/T10971d.stderr index c5ad886683..5cf339bd8d 100644 --- a/testsuite/tests/typecheck/should_fail/T10971d.stderr +++ b/testsuite/tests/typecheck/should_fail/T10971d.stderr @@ -1,14 +1,12 @@ T10971d.hs:4:14: error: - • Couldn't match expected type ‘[a0]’ - with actual type ‘Maybe Integer’ + • Couldn't match expected type ‘[a0]’ with actual type ‘Maybe a2’ • In the first argument of ‘f’, namely ‘(Just 1)’ In the second argument of ‘($)’, namely ‘f (Just 1)’ In a stmt of a 'do' block: print $ f (Just 1) T10971d.hs:5:19: error: - • Couldn't match expected type ‘[Integer]’ - with actual type ‘Maybe Integer’ + • Couldn't match expected type ‘[b1]’ with actual type ‘Maybe a3’ • In the second argument of ‘g’, namely ‘(Just 5)’ In the second argument of ‘($)’, namely ‘g (+ 1) (Just 5)’ In a stmt of a 'do' block: print $ g (+ 1) (Just 5) diff --git a/testsuite/tests/typecheck/should_fail/T12729.stderr b/testsuite/tests/typecheck/should_fail/T12729.stderr index 39dac1116f..fafa6316c3 100644 --- a/testsuite/tests/typecheck/should_fail/T12729.stderr +++ b/testsuite/tests/typecheck/should_fail/T12729.stderr @@ -1,10 +1,12 @@ T12729.hs:8:4: error: • A newtype cannot have an unlifted argument type + Perhaps you intended to use UnliftedNewtypes • In the definition of data constructor ‘MkA’ In the newtype declaration for ‘A’ T12729.hs:10:13: error: • A newtype cannot have an unlifted argument type + Perhaps you intended to use UnliftedNewtypes • In the definition of data constructor ‘MkB’ In the newtype declaration for ‘B’ diff --git a/testsuite/tests/typecheck/should_fail/T13902.stderr b/testsuite/tests/typecheck/should_fail/T13902.stderr index c3d07edfd1..2794ae25ec 100644 --- a/testsuite/tests/typecheck/should_fail/T13902.stderr +++ b/testsuite/tests/typecheck/should_fail/T13902.stderr @@ -1,7 +1,6 @@ T13902.hs:8:5: error: - • Couldn't match expected type ‘Integer -> Int’ - with actual type ‘Int’ + • Couldn't match expected type ‘t0 -> Int’ with actual type ‘Int’ • The expression ‘f @Int’ is applied to two arguments, but its type ‘Int -> Int’ has only one In the expression: f @Int 42 5 diff --git a/testsuite/tests/typecheck/should_fail/T15883.hs b/testsuite/tests/typecheck/should_fail/T15883.hs new file mode 100644 index 0000000000..29ccbc835a --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15883.hs @@ -0,0 +1,9 @@ +{-# Language KindSignatures #-} +{-# Language PolyKinds #-} +{-# Language RankNTypes #-} + +module T15883 where + +import GHC.Exts + +newtype Foo rep = MkFoo (forall (a :: TYPE rep). a) diff --git a/testsuite/tests/typecheck/should_fail/T15883.stderr b/testsuite/tests/typecheck/should_fail/T15883.stderr new file mode 100644 index 0000000000..4bfbc615e6 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15883.stderr @@ -0,0 +1,5 @@ +T15883.hs:9:19: + A newtype cannot have an unlifted argument type + Perhaps you intended to use UnliftedNewtypes + In the definition of data constructor ‘MkFoo’ + In the newtype declaration for ‘Foo’ diff --git a/testsuite/tests/typecheck/should_fail/T15883b.hs b/testsuite/tests/typecheck/should_fail/T15883b.hs new file mode 100644 index 0000000000..82613943a7 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15883b.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UnliftedNewtypes #-} + +module T15883b where + +import GHC.Exts + +newtype Foo rep = MkFoo (forall (a :: TYPE rep). a) +deriving stock instance Eq (Foo LiftedRep) diff --git a/testsuite/tests/typecheck/should_fail/T15883b.stderr b/testsuite/tests/typecheck/should_fail/T15883b.stderr new file mode 100644 index 0000000000..a89403d4af --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15883b.stderr @@ -0,0 +1,5 @@ +T15883b.hs:14:1: + Can't make a derived instance of + ‘Eq (Foo 'LiftedRep)’ with the stock strategy: + Don't know how to derive ‘Eq’ for type ‘forall a. a’ + In the stand-alone deriving instance for ‘Eq (Foo LiftedRep)’ diff --git a/testsuite/tests/typecheck/should_fail/T15883c.hs b/testsuite/tests/typecheck/should_fail/T15883c.hs new file mode 100644 index 0000000000..bd031540c2 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15883c.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UnliftedNewtypes #-} + +module T15883c where + +import GHC.Exts + +newtype Foo rep = MkFoo (forall (a :: TYPE rep). a) +deriving stock instance Ord (Foo LiftedRep) diff --git a/testsuite/tests/typecheck/should_fail/T15883c.stderr b/testsuite/tests/typecheck/should_fail/T15883c.stderr new file mode 100644 index 0000000000..5444f5d6c8 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15883c.stderr @@ -0,0 +1,5 @@ +T15883c.hs:14:1: + Can't make a derived instance of + ‘Ord (Foo 'LiftedRep)’ with the stock strategy: + Don't know how to derive ‘Ord’ for type ‘forall a. a’ + In the stand-alone deriving instance for ‘Ord (Foo LiftedRep)’ diff --git a/testsuite/tests/typecheck/should_fail/T15883d.hs b/testsuite/tests/typecheck/should_fail/T15883d.hs new file mode 100644 index 0000000000..fd86c5cab3 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15883d.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UnliftedNewtypes #-} + +module T15883d where + +import GHC.Exts + +newtype Foo rep = MkFoo (forall (a :: TYPE rep). a) +deriving stock instance Show (Foo LiftedRep) + diff --git a/testsuite/tests/typecheck/should_fail/T15883d.stderr b/testsuite/tests/typecheck/should_fail/T15883d.stderr new file mode 100644 index 0000000000..b080ff6544 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15883d.stderr @@ -0,0 +1,5 @@ +T15883d.hs:14:1: + Can't make a derived instance of + ‘Show (Foo 'LiftedRep)’ with the stock strategy: + Don't know how to derive ‘Show’ for type ‘forall a. a’ + In the stand-alone deriving instance for ‘Show (Foo LiftedRep)’ diff --git a/testsuite/tests/typecheck/should_fail/T15883e.hs b/testsuite/tests/typecheck/should_fail/T15883e.hs new file mode 100644 index 0000000000..bb1dcacf92 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15883e.hs @@ -0,0 +1,18 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UnliftedNewtypes #-} + +module T15883e where + +import GHC.Exts +import Data.Data (Data) + +newtype Foo rep = MkFoo (forall (a :: TYPE rep). a) +deriving stock instance Data (Foo LiftedRep) + + diff --git a/testsuite/tests/typecheck/should_fail/T15883e.stderr b/testsuite/tests/typecheck/should_fail/T15883e.stderr new file mode 100644 index 0000000000..05e07f0307 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/T15883e.stderr @@ -0,0 +1,5 @@ +T15883e.hs:16:1: + Can't make a derived instance of + ‘Data (Foo 'LiftedRep)’ with the stock strategy: + Don't know how to derive ‘Data’ for type ‘forall a. a’ + In the stand-alone deriving instance for ‘Data (Foo LiftedRep)’ diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr index d22d13f92b..ec991bc39f 100644 --- a/testsuite/tests/typecheck/should_fail/T8603.stderr +++ b/testsuite/tests/typecheck/should_fail/T8603.stderr @@ -1,7 +1,7 @@ T8603.hs:33:17: error: • Couldn't match type ‘RV a1’ with ‘StateT s RV a0’ - Expected type: [Integer] -> StateT s RV a0 + Expected type: [a2] -> StateT s RV a0 Actual type: t0 ((->) [a1]) (RV a1) • The function ‘lift’ is applied to two arguments, but its type ‘([a1] -> RV a1) -> t0 ((->) [a1]) (RV a1)’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.hs new file mode 100644 index 0000000000..f5fd1092ca --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE UnliftedNewtypes #-} + +module Goof where + +import GHC.Exts (coerce) +import GHC.Types (RuntimeRep,TYPE,Coercible) + +goof :: forall (rep :: RuntimeRep) (x :: TYPE rep) (y :: TYPE rep). + Coercible x y => x -> y +goof = coerce diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.stderr new file mode 100644 index 0000000000..638dc80ff8 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesCoerceFail.stderr @@ -0,0 +1,5 @@ +UnliftedNewtypesCoerceFail.hs:15:8: + Cannot use function with levity-polymorphic arguments: + coerce :: x -> y + Levity-polymorphic arguments: x :: TYPE rep + diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.hs new file mode 100644 index 0000000000..530b1f5241 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE UnliftedNewtypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE MagicHash #-} + +module UnliftedNewtypesConstraintFamily where + +import Data.Kind (Type,Constraint) + +data family D (a :: Type) :: Constraint diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.stderr new file mode 100644 index 0000000000..9c6816b3c1 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesConstraintFamily.stderr @@ -0,0 +1,5 @@ +UnliftedNewtypesConstraintFamily.hs:11:1: + Kind signature on data type declaration has non-* + and non-variable return kind + Constraint + In the data family declaration for ‘D’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.hs new file mode 100644 index 0000000000..f37549ed76 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.hs @@ -0,0 +1,6 @@ +{-# LANGUAGE UnliftedNewtypes #-} + +main :: IO () +main = return () + +newtype Baz = Baz (Show Int) diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.stderr new file mode 100644 index 0000000000..58b7d65d31 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFail.stderr @@ -0,0 +1,5 @@ +UnliftedNewtypesFail.hs:6:20: + Expected a type, but ‘Show Int’ has kind ‘Constraint’ + In the type ‘(Show Int)’ + In the definition of data constructor ‘Baz’ + In the newtype declaration for ‘Baz’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.hs new file mode 100644 index 0000000000..0306a11c9f --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UnliftedNewtypes #-} + +module UnliftedNewtypesFamilyKindFail1 where + +import Data.Kind (Type) + +data family DF (a :: Type) :: 5 diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr new file mode 100644 index 0000000000..13c9836c43 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail1.stderr @@ -0,0 +1,4 @@ +UnliftedNewtypesFamilyKindFail1.hs:11:31: + Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’ + In the kind ‘5’ + In the data family declaration for ‘DF’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.hs new file mode 100644 index 0000000000..a2baf8ca5c --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE UnliftedNewtypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE MagicHash #-} + +module UnliftedNewtypesFamilyKindFail2 where + +import Data.Kind (Type) + +data family F k :: k +newtype instance F 5 = MkF (F 5) diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr new file mode 100644 index 0000000000..57c4a3c2e9 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesFamilyKindFail2.stderr @@ -0,0 +1,11 @@ +UnliftedNewtypesFamilyKindFail2.hs:12:20: + Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’ + In the first argument of ‘F’, namely ‘5’ + In the newtype instance declaration for ‘F’ + +UnliftedNewtypesFamilyKindFail2.hs:12:31: + Expected a type, but ‘5’ has kind ‘GHC.Types.Nat’ + In the first argument of ‘F’, namely ‘5’ + In the type ‘(F 5)’ + In the definition of data constructor ‘MkF’ + diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.hs new file mode 100644 index 0000000000..644943e398 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.hs @@ -0,0 +1,9 @@ +{-# language MagicHash #-} +{-# language UnboxedTuples #-} +{-# language UnliftedNewtypes #-} + +module UnliftedNewtypesInfinite where + +import GHC.Exts (Int#) + +newtype Foo = FooC (# Int#, Foo #) diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr new file mode 100644 index 0000000000..65db9f5a84 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInfinite.stderr @@ -0,0 +1,6 @@ + +UnliftedNewtypesInfinite.hs:9:15: error: + • Occurs check: cannot construct the infinite kind: + t0 ~ 'GHC.Types.TupleRep '[ 'GHC.Types.IntRep, t0] + • In the definition of data constructor ‘FooC’ + In the newtype declaration for ‘Foo’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.hs new file mode 100644 index 0000000000..8f1f9b4c65 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UnliftedNewtypes #-} +{-# LANGUAGE TypeFamilies #-} +module UnliftedNewtypesInstanceFail where + +import GHC.Exts + +class Foo a where + data Bar a :: TYPE 'IntRep + +instance Foo Bool where + newtype Bar Bool :: TYPE 'WordRep where + BarBoolC :: Word# -> Bar Bool diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr new file mode 100644 index 0000000000..3fb2814dab --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesInstanceFail.stderr @@ -0,0 +1,5 @@ +UnliftedNewtypesInstanceFail.hs:13:3: + Expected kind ‘TYPE 'WordRep’, + but ‘Bar Bool’ has kind ‘TYPE 'IntRep’ + In the newtype instance declaration for ‘Bar’ + In the instance declaration for ‘Foo Bool’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.hs new file mode 100644 index 0000000000..f5d134e3b1 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.hs @@ -0,0 +1,16 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE UnliftedNewtypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeInType #-} + +module UnliftedNewtypesLevityBinder where + +import GHC.Types (RuntimeRep,TYPE,Coercible) + +newtype Ident :: forall (r :: RuntimeRep). TYPE r -> TYPE r where + IdentC :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Ident a + +bad :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Ident a +bad = IdentC diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr new file mode 100644 index 0000000000..90cf5b23aa --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesLevityBinder.stderr @@ -0,0 +1,4 @@ +UnliftedNewtypesLevityBinder.hs:16:7: + Cannot use function with levity-polymorphic arguments: + UnliftedNewtypesLevityBinder.IdentC :: a -> Ident a + Levity-polymorphic arguments: a :: TYPE r diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.hs new file mode 100644 index 0000000000..6c085267db --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.hs @@ -0,0 +1,12 @@ +{-# language MagicHash #-} +{-# language GADTSyntax #-} +{-# language KindSignatures #-} +{-# language UnliftedNewtypes #-} + +module UnliftedNewtypesMismatchedKind where + +import Data.Kind (Type) +import GHC.Exts + +newtype T :: Type where + MkT :: Int# -> T diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.stderr new file mode 100644 index 0000000000..1d3cb50f90 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKind.stderr @@ -0,0 +1,4 @@ +UnliftedNewtypesMismatchedKind.hs:12:3: + Expecting a lifted type, but ‘Int#’ is unlifted + In the definition of data constructor ‘MkT’ + In the newtype declaration for ‘T’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.hs new file mode 100644 index 0000000000..255643a69d --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.hs @@ -0,0 +1,11 @@ +{-# language GADTSyntax #-} +{-# language KindSignatures #-} +{-# language MagicHash #-} +{-# language UnliftedNewtypes #-} + +module UnliftedNewtypesMismatchedKindRecord where + +import GHC.Exts + +newtype Foo :: TYPE 'IntRep where + FooC :: { getFoo :: Word# } -> Foo diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.stderr new file mode 100644 index 0000000000..2530a438ab --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMismatchedKindRecord.stderr @@ -0,0 +1,5 @@ +UnliftedNewtypesMismatchedKindRecord.hs:11:3: + Expected kind ‘TYPE 'IntRep’, + but ‘Word#’ has kind ‘TYPE 'WordRep’ + In the definition of data constructor ‘FooC’ + In the newtype declaration for ‘Foo’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.hs new file mode 100644 index 0000000000..81a2041d2b --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UnliftedNewtypes #-} + +-- In tcConDecl, there is a place where a panic can happen if +-- a newtype has multiple fields. This test is here to make +-- sure that the appropriate validity checks happen before +-- we get to the panic. See Note [Kind-checking the field type]. + +module UnliftedNewtypesMultiFieldGadt where + +import GHC.Exts +import Data.Kind + +newtype Foo :: TYPE 'IntRep where + FooC :: Bool -> Char -> Foo diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.stderr new file mode 100644 index 0000000000..70493e0d96 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesMultiFieldGadt.stderr @@ -0,0 +1,5 @@ +UnliftedNewtypesMultiFieldGadt.hs:19:3: + The constructor of a newtype must have exactly one field + but ‘FooC’ has two + In the definition of data constructor ‘FooC’ + In the newtype declaration for ‘Foo’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.hs new file mode 100644 index 0000000000..6c6aadccc8 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.hs @@ -0,0 +1,9 @@ +{-# LANGUAGE MagicHash #-} + +module UnliftedNewtypesNotEnabled + ( Baz(..) + ) where + +import GHC.Exts (Int#) + +newtype Baz = Baz Int# diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.stderr new file mode 100644 index 0000000000..37496c4edd --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesNotEnabled.stderr @@ -0,0 +1,5 @@ +UnliftedNewtypesNotEnabled.hs:9:15: + A newtype cannot have an unlifted argument type + Perhaps you intended to use UnliftedNewtypes + In the definition of data constructor ‘Baz’ + In the newtype declaration for ‘Baz’ diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.hs b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.hs new file mode 100644 index 0000000000..6c1959e035 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE UnliftedNewtypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE MagicHash #-} + +module UnliftedNewtypesOverlap where + +import GHC.Exts (TYPE) + +data family DF :: TYPE r +data instance DF = MkDF4 | MkDF5 +newtype instance DF = MkDF6 Int diff --git a/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.stderr b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.stderr new file mode 100644 index 0000000000..808e8c0f60 --- /dev/null +++ b/testsuite/tests/typecheck/should_fail/UnliftedNewtypesOverlap.stderr @@ -0,0 +1,4 @@ +UnliftedNewtypesOverlap.hs:12:15: + Conflicting family instance declarations: + DF -- Defined at UnliftedNewtypesOverlap.hs:12:15 + DF -- Defined at UnliftedNewtypesOverlap.hs:13:18 diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T index 5be507edbf..7ee15ebc4c 100644 --- a/testsuite/tests/typecheck/should_fail/all.T +++ b/testsuite/tests/typecheck/should_fail/all.T @@ -518,3 +518,21 @@ test('T16456', normal, compile_fail, ['-fprint-explicit-foralls']) test('T16627', normal, compile_fail, ['']) test('T502', normal, compile_fail, ['']) test('T16517', normal, compile_fail, ['']) +test('T15883', normal, compile_fail, ['']) +test('T15883b', normal, compile_fail, ['']) +test('T15883c', normal, compile_fail, ['']) +test('T15883d', normal, compile_fail, ['']) +test('T15883e', normal, compile_fail, ['']) +test('UnliftedNewtypesFail', normal, compile_fail, ['']) +test('UnliftedNewtypesNotEnabled', normal, compile_fail, ['']) +test('UnliftedNewtypesCoerceFail', normal, compile_fail, ['']) +test('UnliftedNewtypesInstanceFail', normal, compile_fail, ['']) +test('UnliftedNewtypesInfinite', normal, compile_fail, ['-fprint-explicit-runtime-reps']) +test('UnliftedNewtypesLevityBinder', normal, compile_fail, ['']) +test('UnliftedNewtypesOverlap', normal, compile_fail, ['']) +test('UnliftedNewtypesFamilyKindFail1', normal, compile_fail, ['']) +test('UnliftedNewtypesFamilyKindFail2', normal, compile_fail, ['']) +test('UnliftedNewtypesConstraintFamily', normal, compile_fail, ['']) +test('UnliftedNewtypesMismatchedKind', normal, compile_fail, ['']) +test('UnliftedNewtypesMismatchedKindRecord', normal, compile_fail, ['']) +test('UnliftedNewtypesMultiFieldGadt', normal, compile_fail, ['']) diff --git a/testsuite/tests/typecheck/should_fail/mc24.stderr b/testsuite/tests/typecheck/should_fail/mc24.stderr index 7f016283b1..06a9c51690 100644 --- a/testsuite/tests/typecheck/should_fail/mc24.stderr +++ b/testsuite/tests/typecheck/should_fail/mc24.stderr @@ -1,8 +1,8 @@ mc24.hs:10:31: error: - • Couldn't match type ‘[a0]’ with ‘[a] -> m [a]’ - Expected type: (a -> Integer) -> [a] -> m [a] - Actual type: [a0] -> [a0] + • Couldn't match type ‘[a1]’ with ‘[a] -> m [a]’ + Expected type: (a -> a0) -> [a] -> m [a] + Actual type: [a1] -> [a1] • Possible cause: ‘take’ is applied to too many arguments In the expression: take 2 In a stmt of a monad comprehension: then group by x using take 2 diff --git a/testsuite/tests/typecheck/should_fail/tcfail004.stderr b/testsuite/tests/typecheck/should_fail/tcfail004.stderr index 7bf64d841a..9d6657e651 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail004.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail004.stderr @@ -1,7 +1,7 @@ tcfail004.hs:3:9: error: • Couldn't match expected type ‘(a, b)’ - with actual type ‘(Integer, Integer, Integer)’ + with actual type ‘(a0, b0, c0)’ • In the expression: (1, 2, 3) In a pattern binding: (f, g) = (1, 2, 3) • Relevant bindings include diff --git a/testsuite/tests/typecheck/should_fail/tcfail005.stderr b/testsuite/tests/typecheck/should_fail/tcfail005.stderr index 56db4cf58b..d206505cdc 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail005.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail005.stderr @@ -1,7 +1,6 @@ tcfail005.hs:3:9: error: - • Couldn't match expected type ‘[a]’ - with actual type ‘(Integer, Char)’ + • Couldn't match expected type ‘[a]’ with actual type ‘(a0, Char)’ • In the expression: (1, 'a') In a pattern binding: (h : i) = (1, 'a') • Relevant bindings include diff --git a/testsuite/tests/typecheck/should_fail/tcfail079.stderr b/testsuite/tests/typecheck/should_fail/tcfail079.stderr index 78d14f9c35..769b8335ed 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail079.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail079.stderr @@ -1,5 +1,5 @@ - tcfail079.hs:9:19: error: • A newtype cannot have an unlifted argument type + Perhaps you intended to use UnliftedNewtypes • In the definition of data constructor ‘Unboxed’ In the newtype declaration for ‘Unboxed’ diff --git a/testsuite/tests/typecheck/should_fail/tcfail140.stderr b/testsuite/tests/typecheck/should_fail/tcfail140.stderr index 85217315ca..924e14081b 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail140.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail140.stderr @@ -1,7 +1,6 @@ tcfail140.hs:10:7: error: - • Couldn't match expected type ‘Integer -> t’ - with actual type ‘Int’ + • Couldn't match expected type ‘t0 -> t’ with actual type ‘Int’ • The function ‘f’ is applied to two arguments, but its type ‘Int -> Int’ has only one In the expression: f 3 9 @@ -9,8 +8,7 @@ tcfail140.hs:10:7: error: • Relevant bindings include bar :: t (bound at tcfail140.hs:10:1) tcfail140.hs:12:10: error: - • Couldn't match expected type ‘Integer -> t’ - with actual type ‘Int’ + • Couldn't match expected type ‘t1 -> t’ with actual type ‘Int’ • The operator ‘f’ takes two arguments, but its type ‘Int -> Int’ has only one In the expression: 3 `f` 4 diff --git a/testsuite/tests/typecheck/should_fail/tcfail159.stderr b/testsuite/tests/typecheck/should_fail/tcfail159.stderr index 412ba47d3f..706b3afa32 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail159.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail159.stderr @@ -1,6 +1,6 @@ tcfail159.hs:9:11: error: - • Expecting a lifted type, but got an unlifted + • Expecting a lifted type, but got an unlifted type • In the pattern: ~(# p, q #) In a case alternative: ~(# p, q #) -> p In the expression: case h x of { ~(# p, q #) -> p } diff --git a/testsuite/tests/typecheck/should_fail/tcfail189.stderr b/testsuite/tests/typecheck/should_fail/tcfail189.stderr index f23243bdd0..f33d1e37f6 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail189.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail189.stderr @@ -1,8 +1,8 @@ tcfail189.hs:10:31: error: - • Couldn't match type ‘[a0]’ with ‘[a] -> [[a]]’ - Expected type: (a -> Integer) -> [a] -> [[a]] - Actual type: [a0] -> [a0] + • Couldn't match type ‘[a1]’ with ‘[a] -> [[a]]’ + Expected type: (a -> a0) -> [a] -> [[a]] + Actual type: [a1] -> [a1] • Possible cause: ‘take’ is applied to too many arguments In the expression: take 2 In a stmt of a list comprehension: then group by x using take 2 diff --git a/testsuite/tests/typecheck/should_fail/tcfail206.stderr b/testsuite/tests/typecheck/should_fail/tcfail206.stderr index 51fbbb3825..7c97fc02af 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail206.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail206.stderr @@ -7,9 +7,9 @@ tcfail206.hs:5:5: error: In an equation for ‘a’: a = (, True) tcfail206.hs:8:5: error: - • Couldn't match type ‘(Integer, Int)’ with ‘Bool -> (Int, Bool)’ + • Couldn't match type ‘(t1, Int)’ with ‘Bool -> (Int, Bool)’ Expected type: Int -> Bool -> (Int, Bool) - Actual type: Int -> (Integer, Int) + Actual type: Int -> (t1, Int) • In the expression: (1,) In an equation for ‘b’: b = (1,) @@ -34,10 +34,10 @@ tcfail206.hs:14:5: error: In an equation for ‘d’: d = (# , True #) tcfail206.hs:17:5: error: - • Couldn't match type ‘(# Integer, Int #)’ + • Couldn't match type ‘(# t0, Int #)’ with ‘Bool -> (# Int, Bool #)’ Expected type: Int -> Bool -> (# Int, Bool #) - Actual type: Int -> (# Integer, Int #) + Actual type: Int -> (# t0, Int #) • In the expression: (# 1, #) In an equation for ‘e’: e = (# 1, #) diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.hs new file mode 100644 index 0000000000..53905a302a --- /dev/null +++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.hs @@ -0,0 +1,22 @@ +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UnliftedNewtypes #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE UnboxedTuples #-} +{-# LANGUAGE UnboxedSums #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeFamilies #-} + +import GHC.Int (Int(I#)) +import GHC.Word (Word(W#)) +import GHC.Exts (Int#,Word#,(+#)) +import GHC.Types +import Data.Coerce (coerce) + +main :: IO () +main = do + print (I# (coerce (Foo 5#))) + +newtype Foo = Foo Int# diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.stdout new file mode 100644 index 0000000000..7ed6ff82de --- /dev/null +++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesCoerceRun.stdout @@ -0,0 +1 @@ +5 diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.hs new file mode 100644 index 0000000000..a6331b8329 --- /dev/null +++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.hs @@ -0,0 +1,32 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UnliftedNewtypes #-} + +import GHC.Int (Int(I#)) +import GHC.Word (Word(W#)) +import GHC.Exts (Int#,Word#) +import Data.Proxy (Proxy(..)) +import GHC.Exts (TYPE,RuntimeRep(..)) + +main :: IO () +main = case method (Proxy :: Proxy 'IntRep) of + BarIntC y -> case method (Proxy :: Proxy 'WordRep) of + BarWordC z -> do + print (I# y) + print (W# z) + +class Foo (a :: RuntimeRep) where + data Bar a :: TYPE a + method :: Proxy a -> Bar a + +instance Foo 'IntRep where + newtype instance Bar 'IntRep = BarIntC Int# + method _ = BarIntC 5# + +instance Foo 'WordRep where + newtype instance Bar 'WordRep :: TYPE 'WordRep where + BarWordC :: Word# -> Bar 'WordRep + method _ = BarWordC 7## diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.stdout new file mode 100644 index 0000000000..b3172d1242 --- /dev/null +++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesDependentFamilyRun.stdout @@ -0,0 +1,2 @@ +5 +7 diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.hs new file mode 100644 index 0000000000..b0fdc88dbb --- /dev/null +++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UnliftedNewtypes #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} + +import GHC.Int (Int(I#)) +import GHC.Word (Word(W#)) +import GHC.Exts (Int#,Word#) +import GHC.Types + +main :: IO () +main = do + print (method 5 (BarIntC 6#)) + print (method 13 (BarWordC 9#)) + +class Foo a where + data Bar a :: TYPE 'IntRep + method :: a -> Bar a -> a + +instance Foo Int where + newtype Bar Int = BarIntC Int# + method x (BarIntC y) = x + I# y + +instance Foo Word where + newtype Bar Word = BarWordC Int# + method x (BarWordC y) = x - fromIntegral (I# y) diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.stdout new file mode 100644 index 0000000000..dfa5ffdccf --- /dev/null +++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesFamilyRun.stdout @@ -0,0 +1,2 @@ +11 +4 diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.hs new file mode 100644 index 0000000000..f81367268b --- /dev/null +++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.hs @@ -0,0 +1,41 @@ +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UnliftedNewtypes #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE UnboxedTuples #-} +{-# LANGUAGE UnboxedSums #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeFamilies #-} + +import GHC.Int (Int(I#)) +import GHC.Word (Word(W#)) +import GHC.Exts (Int#,Word#,(+#)) +import GHC.Types + +main :: IO () +main = case (IdentityC 5#) of + IdentityC x -> case ex of + IdentityC y -> do + print (I# x) + print y + print (maybeInt# 12 increment# (Maybe# (# 42# | #))) + print (maybeInt# 27 increment# (Maybe# (# | (# #) #))) + +newtype Identity :: forall (r :: RuntimeRep). TYPE r -> TYPE r where + IdentityC :: forall (r :: RuntimeRep) (a :: TYPE r). a -> Identity a + +newtype Maybe# :: forall (r :: RuntimeRep). + TYPE r -> TYPE (SumRep '[r, TupleRep '[]]) where + Maybe# :: forall (r :: RuntimeRep) (a :: TYPE r). (# a | (# #) #) -> Maybe# a + +maybeInt# :: a -> (Int# -> a) -> Maybe# Int# -> a +maybeInt# def _ (Maybe# (# | (# #) #)) = def +maybeInt# _ f (Maybe# (# i | #)) = f i + +increment# :: Int# -> Int +increment# i = I# (i +# 1#) + +ex :: Identity Bool +ex = IdentityC True diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.stdout new file mode 100644 index 0000000000..e5835b0b94 --- /dev/null +++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesIdentityRun.stdout @@ -0,0 +1,4 @@ +5 +True +43 +27 diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.hs b/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.hs new file mode 100644 index 0000000000..b6c07396bf --- /dev/null +++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.hs @@ -0,0 +1,46 @@ +{-# LANGUAGE GADTSyntax #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE UnliftedNewtypes #-} +{-# LANGUAGE RankNTypes #-} + +import GHC.Int (Int(I#)) +import GHC.Word (Word(W#)) +import GHC.Exts (Int#,Word#) +import GHC.Types + +main :: IO () +main = do + let a = idIntRep (FooC 6#) + b = idWordRep (BarC 7##) + c = idWordRep (PatC 3##) + d = idIntRep (DarthC 5#) + print (I# (getFoo a)) + print (W# (case b of BarC w -> w)) + print (W# (case c of PatC w -> w)) + print (I# (case d of DarthC w -> w)) + print (A1 13#) + print (A2 15##) + +newtype Darth = DarthC Int# + +newtype Foo = FooC { getFoo :: Int# } + +newtype Bar :: TYPE 'WordRep where + BarC :: Word# -> Bar + +newtype Pat where + PatC :: Word# -> Pat + +data A1 :: Type where + A1 :: Int# -> A1 + deriving (Show) + +data A2 = A2 Word# + deriving (Show) + +idIntRep :: forall (a :: TYPE 'IntRep). a -> a +idIntRep x = x + +idWordRep :: forall (a :: TYPE 'WordRep). a -> a +idWordRep x = x diff --git a/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.stdout b/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.stdout new file mode 100644 index 0000000000..df8e8ed83d --- /dev/null +++ b/testsuite/tests/typecheck/should_run/UnliftedNewtypesRun.stdout @@ -0,0 +1,6 @@ +6 +7 +3 +5 +A1 13# +A2 15## diff --git a/testsuite/tests/typecheck/should_run/all.T b/testsuite/tests/typecheck/should_run/all.T index 598d467b7e..05fddcb0b0 100755 --- a/testsuite/tests/typecheck/should_run/all.T +++ b/testsuite/tests/typecheck/should_run/all.T @@ -135,3 +135,8 @@ test('T14218', normal, compile_and_run, ['']) test('T14236', normal, compile_and_run, ['']) test('T14925', normal, compile_and_run, ['']) test('T14341', normal, compile_and_run, ['']) +test('UnliftedNewtypesRun', normal, compile_and_run, ['']) +test('UnliftedNewtypesFamilyRun', normal, compile_and_run, ['']) +test('UnliftedNewtypesDependentFamilyRun', normal, compile_and_run, ['']) +test('UnliftedNewtypesIdentityRun', normal, compile_and_run, ['']) +test('UnliftedNewtypesCoerceRun', normal, compile_and_run, ['']) |