Commit effdd948 authored by Andrew Martin's avatar Andrew Martin Committed by Marge Bot

Implement the -XUnliftedNewtypes extension.

GHC Proposal: 0013-unlifted-newtypes.rst
Discussion: https://github.com/ghc-proposals/ghc-proposals/pull/98
Issues: #15219, #1311, #13595, #15883
Implementation Details:
  Note [Implementation of UnliftedNewtypes]
  Note [Unifying data family kinds]
  Note [Compulsory newtype unfolding]

This patch introduces the -XUnliftedNewtypes extension. When this
extension is enabled, GHC drops the restriction that the field in
a newtype must be of kind (TYPE 'LiftedRep). This allows types
like Int# and ByteArray# to be used in a newtype. Additionally,
coerce is made levity-polymorphic so that it can be used with
newtypes over unlifted types.

The bulk of the changes are in TcTyClsDecls.hs. With -XUnliftedNewtypes,
getInitialKind is more liberal, introducing a unification variable to
return the kind (TYPE r0) rather than just returning (TYPE 'LiftedRep).
When kind-checking a data constructor with kcConDecl, we attempt to
unify the kind of a newtype with the kind of its field's type. When
typechecking a data declaration with tcTyClDecl, we again perform a
unification. See the implementation note for more on this.
Co-authored-by: Richard Eisenberg's avatarRichard Eisenberg <rae@richarde.dev>
parent 3bc6df32
......@@ -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.
......
......@@ -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))]
{-
......
......@@ -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)
......@@ -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
]
......@@ -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]
~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -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
]
......
......@@ -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
......
......@@ -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]
......
......@@ -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}.
}
------------------------------------------------------------------------
......
......@@ -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
......
......@@ -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")
......
......@@ -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
{-
%************************************************************************
%* *
......
......@@ -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]
......
......@@ -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