K -> ARecDataCon
ANothing is only used for DataCons, and only used during type checking
in tcTyClGroup.
%************************************************************************
%* *
\subsection{Type checking}
%* *
%************************************************************************
Note [Type checking recursive type and class declarations]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At this point we have completed *kind-checking* of a mutually
recursive group of type/class decls (done in kcTyClGroup). However,
we discarded the kind-checked types (eg RHSs of data type decls);
note that kcTyClDecl returns (). There are two reasons:
* It's convenient, because we don't have to rebuild a
kinded HsDecl (a fairly elaborate type)
* It's necessary, because after kind-generalisation, the
TyCons/Classes may now be kind-polymorphic, and hence need
to be given kind arguments.
Example:
data T f a = MkT (f a) (T f a)
During kind-checking, we give T the kind T :: k1 -> k2 -> *
and figure out constraints on k1, k2 etc. Then we generalise
to get T :: forall k. (k->*) -> k -> *
So now the (T f a) in the RHS must be elaborated to (T k f a).
However, during tcTyClDecl of T (above) we will be in a recursive
"knot". So we aren't allowed to look at the TyCon T itself; we are only
allowed to put it (lazily) in the returned structures. But when
kind-checking the RHS of T's decl, we *do* need to know T's kind (so
that we can correctly elaboarate (T k f a). How can we get T's kind
without looking at T? Delicate answer: during tcTyClDecl, we extend
*Global* env with T -> ATyCon (the (not yet built) TyCon for T)
*Local* env with T -> AThing (polymorphic kind of T)
Then:
* During TcHsType.kcTyVar we look in the *local* env, to get the
known kind for T.
* But in TcHsType.ds_type (and ds_var_app in particular) we look in
the *global* env to get the TyCon. But we must be careful not to
force the TyCon or we'll get a loop.
This fancy footwork (with two bindings for T) is only necesary for the
TyCons or Classes of this recursive group. Earlier, finished groups,
live in the global env only.
\begin{code}
tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM [TyThing]
tcTyClDecl rec_info (L loc decl)
= setSrcSpan loc $ tcAddDeclCtxt decl $
traceTc "tcTyAndCl-x" (ppr decl) >>
tcTyClDecl1 NoParentTyCon rec_info decl
tcTyClDecl1 :: TyConParent -> RecTyInfo -> TyClDecl Name -> TcM [TyThing]
tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd })
= tcFamDecl1 parent fd
tcTyClDecl1 _parent rec_info
(SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs })
= ASSERT( isNoParent _parent )
tcTyClTyVars tc_name tvs $ \ tvs' kind ->
tcTySynRhs rec_info tc_name tvs' kind rhs
tcTyClDecl1 _parent rec_info
(DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn })
= ASSERT( isNoParent _parent )
tcTyClTyVars tc_name tvs $ \ tvs' kind ->
tcDataDefn rec_info tc_name tvs' kind defn
tcTyClDecl1 _parent rec_info
(ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs
, tcdCtxt = ctxt, tcdMeths = meths
, tcdFDs = fundeps, tcdSigs = sigs
, tcdATs = ats, tcdATDefs = at_defs })
= ASSERT( isNoParent _parent )
do { (clas, tvs', gen_dm_env) <- fixM $ \ ~(clas,_,_) ->
tcTyClTyVars class_name tvs $ \ tvs' kind ->
do { MASSERT( isConstraintKind kind )
; let tycon_name = tyConName (classTyCon clas)
tc_isrec = rti_is_rec rec_info tycon_name
roles = rti_roles rec_info tycon_name
; ctxt' <- tcHsContext ctxt
; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
; fds' <- mapM (addLocM tc_fundep) fundeps
; (sig_stuff, gen_dm_env) <- tcClassSigs class_name sigs meths
; at_stuff <- tcClassATs class_name (AssocFamilyTyCon clas) ats at_defs
; mindef <- tcClassMinimalDef class_name sigs sig_stuff
; clas <- buildClass False
class_name tvs' roles ctxt' fds' at_stuff
sig_stuff mindef tc_isrec
; traceTc "tcClassDecl" (ppr fundeps $$ ppr tvs' $$ ppr fds')
; return (clas, tvs', gen_dm_env) }
; let { gen_dm_ids = [ AnId (mkExportedLocalId gen_dm_name gen_dm_ty)
| (sel_id, GenDefMeth gen_dm_name) <- classOpItems clas
, let gen_dm_tau = expectJust "tcTyClDecl1" $
lookupNameEnv gen_dm_env (idName sel_id)
, let gen_dm_ty = mkSigmaTy tvs'
[mkClassPred clas (mkTyVarTys tvs')]
gen_dm_tau
]
; class_ats = map ATyCon (classATs clas) }
; return (ATyCon (classTyCon clas) : gen_dm_ids ++ class_ats ) }
where
tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tc_fd_tyvar tvs1 ;
; tvs2' <- mapM tc_fd_tyvar tvs2 ;
; return (tvs1', tvs2') }
tc_fd_tyvar name
= do { tv <- tcLookupTyVar name
; ty <- zonkTyVarOcc emptyZonkEnv tv
; case getTyVar_maybe ty of
Just tv' -> return tv'
Nothing -> pprPanic "tc_fd_tyvar" (ppr name $$ ppr tv $$ ppr ty) }
tcTyClDecl1 _ _
(ForeignType {tcdLName = L _ tc_name, tcdExtName = tc_ext_name})
= return [ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind)]
\end{code}
\begin{code}
tcFamDecl1 :: TyConParent -> FamilyDecl Name -> TcM [TyThing]
tcFamDecl1 parent
(FamilyDecl {fdInfo = OpenTypeFamily, fdLName = L _ tc_name, fdTyVars = tvs})
= tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
{ traceTc "open type family:" (ppr tc_name)
; checkFamFlag tc_name
; let roles = map (const Nominal) tvs'
; tycon <- buildSynTyCon tc_name tvs' roles OpenSynFamilyTyCon kind parent
; return [ATyCon tycon] }
tcFamDecl1 parent
(FamilyDecl { fdInfo = ClosedTypeFamily eqns
, fdLName = lname@(L _ tc_name), fdTyVars = tvs })
= do { traceTc "closed type family:" (ppr tc_name)
; (tvs', kind) <- tcTyClTyVars tc_name tvs $ \ tvs' kind ->
return (tvs', kind)
; checkFamFlag tc_name
; let names = map (tfie_tycon . unLoc) eqns
; tcSynFamInstNames lname names
; tycon_kind <- kcLookupKind tc_name
; branches <- mapM (tcTyFamInstEqn tc_name tycon_kind) eqns
; fam_tc <- tcLookupLocatedTyCon lname
; loc <- getSrcSpanM
; co_ax_name <- newFamInstAxiomName loc tc_name []
; let co_ax = mkBranchedCoAxiom co_ax_name fam_tc branches
; let syn_rhs = if null eqns
then AbstractClosedSynFamilyTyCon
else ClosedSynFamilyTyCon co_ax
roles = map (const Nominal) tvs'
; tycon <- buildSynTyCon tc_name tvs' roles syn_rhs kind parent
; let result = if null eqns
then [ATyCon tycon]
else [ATyCon tycon, ACoAxiom co_ax]
; return result }
tcFamDecl1 parent
(FamilyDecl {fdInfo = DataFamily, fdLName = L _ tc_name, fdTyVars = tvs})
= tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
{ traceTc "data family:" (ppr tc_name)
; checkFamFlag tc_name
; extra_tvs <- tcDataKindSig kind
; let final_tvs = tvs' ++ extra_tvs
roles = map (const Nominal) final_tvs
tycon = buildAlgTyCon tc_name final_tvs roles Nothing []
DataFamilyTyCon Recursive
False
True
parent
; return [ATyCon tycon] }
tcTySynRhs :: RecTyInfo
-> Name
-> [TyVar] -> Kind
-> LHsType Name -> TcM [TyThing]
tcTySynRhs rec_info tc_name tvs kind hs_ty
= do { env <- getLclEnv
; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
; rhs_ty <- tcCheckLHsType hs_ty kind
; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
; let roles = rti_roles rec_info tc_name
; tycon <- buildSynTyCon tc_name tvs roles (SynonymTyCon rhs_ty)
kind NoParentTyCon
; return [ATyCon tycon] }
tcDataDefn :: RecTyInfo -> Name
-> [TyVar] -> Kind
-> HsDataDefn Name -> TcM [TyThing]
tcDataDefn rec_info tc_name tvs kind
(HsDataDefn { dd_ND = new_or_data, dd_cType = cType
, dd_ctxt = ctxt, dd_kindSig = mb_ksig
, dd_cons = cons })
= do { extra_tvs <- tcDataKindSig kind
; let final_tvs = tvs ++ extra_tvs
roles = rti_roles rec_info tc_name
; stupid_theta <- tcHsContext ctxt
; kind_signatures <- xoptM Opt_KindSignatures
; is_boot <- tcIsHsBoot
; case mb_ksig of
Nothing -> return ()
Just hs_k -> do { checkTc (kind_signatures) (badSigTyDecl tc_name)
; tc_kind <- tcLHsKind hs_k
; checkKind kind tc_kind
; return () }
; h98_syntax <- dataDeclChecks tc_name new_or_data stupid_theta cons
; tycon <- fixM $ \ tycon -> do
{ let res_ty = mkTyConApp tycon (mkTyVarTys final_tvs)
; data_cons <- tcConDecls new_or_data tycon (final_tvs, res_ty) cons
; tc_rhs <-
if null cons && is_boot
then return totallyAbstractTyConRhs
else case new_or_data of
DataType -> return (mkDataTyConRhs data_cons)
NewType -> ASSERT( not (null data_cons) )
mkNewTyConRhs tc_name tycon (head data_cons)
; return (buildAlgTyCon tc_name final_tvs roles cType stupid_theta tc_rhs
(rti_is_rec rec_info tc_name)
(rti_promotable rec_info)
(not h98_syntax) NoParentTyCon) }
; return [ATyCon tycon] }
\end{code}
%************************************************************************
%* *
Typechecking associated types (in class decls)
(including the associated-type defaults)
%* *
%************************************************************************
Note [Associated type defaults]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The following is an example of associated type defaults:
class C a where
data D a
type F a b :: *
type F a Z = [a] -- Default
type F a (S n) = F a n -- Default
Note that:
- We can have more than one default definition for a single associated type,
as long as they do not overlap (same rules as for instances)
- We can get default definitions only for type families, not data families
\begin{code}
tcClassATs :: Name
-> TyConParent
-> [LFamilyDecl Name]
-> [LTyFamInstDecl Name]
-> TcM [ClassATItem]
tcClassATs class_name parent ats at_defs
= do {
sequence_ [ failWithTc (badATErr class_name n)
| n <- map (tyFamInstDeclName . unLoc) at_defs
, not (n `elemNameSet` at_names) ]
; mapM tc_at ats }
where
at_names = mkNameSet (map (unLoc . fdLName . unLoc) ats)
at_defs_map :: NameEnv [LTyFamInstDecl Name]
at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv
(tyFamInstDeclName (unLoc at_def)) [at_def])
emptyNameEnv at_defs
tc_at at = do { [ATyCon fam_tc] <- addLocM (tcFamDecl1 parent) at
; let at_defs = lookupNameEnv at_defs_map (unLoc $ fdLName $ unLoc at)
`orElse` []
; atd <- mapM (tcDefaultAssocDecl fam_tc) at_defs
; return (fam_tc, atd) }
tcDefaultAssocDecl :: TyCon
-> LTyFamInstDecl Name
-> TcM CoAxBranch
tcDefaultAssocDecl fam_tc (L loc decl)
= setSrcSpan loc $
tcAddTyFamInstCtxt decl $
do { traceTc "tcDefaultAssocDecl" (ppr decl)
; tcSynFamInstDecl fam_tc decl }
tcSynFamInstDecl :: TyCon -> TyFamInstDecl Name -> TcM CoAxBranch
tcSynFamInstDecl fam_tc (TyFamInstDecl { tfid_eqn = eqn })
= do { checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
; tcTyFamInstEqn (tyConName fam_tc) (tyConKind fam_tc) eqn }
tcSynFamInstNames :: Located Name -> [Located Name] -> TcM ()
tcSynFamInstNames (L _ first) names
= do { let badNames = filter ((/= first) . unLoc) names
; mapM_ (failLocated (wrongNamesInInstGroup first)) badNames }
where
failLocated :: (Name -> SDoc) -> Located Name -> TcM ()
failLocated msg_fun (L loc name)
= setSrcSpan loc $
failWithTc (msg_fun name)
kcTyFamInstEqn :: Name -> Kind -> LTyFamInstEqn Name -> TcM ()
kcTyFamInstEqn fam_tc_name kind
(L loc (TyFamInstEqn { tfie_pats = pats, tfie_rhs = hs_ty }))
= setSrcSpan loc $
discardResult $
tc_fam_ty_pats fam_tc_name kind pats (discardResult . (tcCheckLHsType hs_ty))
tcTyFamInstEqn :: Name -> Kind -> LTyFamInstEqn Name -> TcM CoAxBranch
tcTyFamInstEqn fam_tc_name kind
(L loc (TyFamInstEqn { tfie_pats = pats, tfie_rhs = hs_ty }))
= setSrcSpan loc $
tcFamTyPats fam_tc_name kind pats (discardResult . (tcCheckLHsType hs_ty)) $
\tvs' pats' res_kind ->
do { rhs_ty <- tcCheckLHsType hs_ty res_kind
; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
; traceTc "tcTyFamInstEqn" (ppr fam_tc_name <+> ppr tvs')
; return (mkCoAxBranch tvs' pats' rhs_ty loc) }
kcDataDefn :: HsDataDefn Name -> TcKind -> TcM ()
kcDataDefn (HsDataDefn { dd_ctxt = ctxt, dd_cons = cons, dd_kindSig = mb_kind }) res_k
= do { _ <- tcHsContext ctxt
; checkNoErrs $ mapM_ (wrapLocM kcConDecl) cons
; kcResultKind mb_kind res_k }
kcResultKind :: Maybe (LHsKind Name) -> Kind -> TcM ()
kcResultKind Nothing res_k
= checkKind res_k liftedTypeKind
kcResultKind (Just k) res_k
= do { k' <- tcLHsKind k
; checkKind k' res_k }
\end{code}
Kind check type patterns and kind annotate the embedded type variables.
type instance F [a] = rhs
* Here we check that a type instance matches its kind signature, but we do
not check whether there is a pattern for each type index; the latter
check is only required for type synonym instances.
Note [tc_fam_ty_pats vs tcFamTyPats]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
tc_fam_ty_pats does the type checking of the patterns, but it doesn't
zonk or generate any desugaring. It is used when kind-checking closed
type families.
tcFamTyPats type checks the patterns, zonks, and then calls thing_inside
to generate a desugaring. It is used during type-checking (not kind-checking).
Note [Failing early in kcDataDefn]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We need to use checkNoErrs when calling kcConDecl. This is because kcConDecl
calls tcConDecl, which checks that the return type of a GADT-like constructor
is actually an instance of the type head. Without the checkNoErrs, potentially
two bad things could happen:
1) Duplicate error messages, because tcConDecl will be called again during
*type* checking (as opposed to kind checking)
2) If we just keep blindly forging forward after both kind checking and type
checking, we can get a panic in rejigConRes. See Trac #8368.
\begin{code}
tc_fam_ty_pats :: Name
-> Kind
-> HsWithBndrs [LHsType Name]
-> (TcKind -> TcM ())
-> TcM ([Kind], [Type], Kind)
tc_fam_ty_pats fam_tc_name kind
(HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars })
kind_checker
= do { let (fam_kvs, fam_body) = splitForAllTys kind
; let max_args = length (fst $ splitKindFunTys fam_body)
; checkTc (length arg_pats <= max_args) $
wrongNumberOfParmsErrTooMany max_args
; fam_arg_kinds <- mapM (const newMetaKindVar) fam_kvs
; loc <- getSrcSpanM
; let (arg_kinds, res_kind)
= splitKindFunTysN (length arg_pats) $
substKiWith fam_kvs fam_arg_kinds fam_body
hs_tvs = HsQTvs { hsq_kvs = kvars
, hsq_tvs = userHsTyVarBndrs loc tvars }
; typats <- tcHsTyVarBndrs hs_tvs $ \ _ ->
do { kind_checker res_kind
; tcHsArgTys (quotes (ppr fam_tc_name)) arg_pats arg_kinds }
; return (fam_arg_kinds, typats, res_kind) }
tcFamTyPats :: Name
-> Kind
-> HsWithBndrs [LHsType Name]
-> (TcKind -> TcM ())
-> ([TKVar] -> [TcType] -> Kind -> TcM a)
-> TcM a
tcFamTyPats fam_tc_name kind pats kind_checker thing_inside
= do { (fam_arg_kinds, typats, res_kind)
<- tc_fam_ty_pats fam_tc_name kind pats kind_checker
; let all_args = fam_arg_kinds ++ typats
; qtkvs <- quantifyTyVars emptyVarSet (tyVarsOfTypes all_args)
; (ze, qtkvs') <- zonkTyBndrsX emptyZonkEnv qtkvs
; all_args' <- zonkTcTypeToTypes ze all_args
; res_kind' <- zonkTcTypeToType ze res_kind
; traceTc "tcFamTyPats" (ppr fam_tc_name)
; tcExtendTyVarEnv qtkvs' $
thing_inside qtkvs' all_args' res_kind' }
\end{code}
Note [Quantifying over family patterns]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We need to quantify over two different lots of kind variables:
First, the ones that come from the kinds of the tyvar args of
tcTyVarBndrsKindGen, as usual
data family Dist a
-- Proxy :: forall k. k -> *
data instance Dist (Proxy a) = DP
-- Generates data DistProxy = DP
-- ax8 k (a::k) :: Dist * (Proxy k a) ~ DistProxy k a
-- The 'k' comes from the tcTyVarBndrsKindGen (a::k)
Second, the ones that come from the kind argument of the type family
which we pick up using the (tyVarsOfTypes typats) in the result of
the thing_inside of tcHsTyvarBndrsGen.
-- Any :: forall k. k
data instance Dist Any = DA
-- Generates data DistAny k = DA
-- ax7 k :: Dist k (Any k) ~ DistAny k
-- The 'k' comes from kindGeneralizeKinds (Any k)
Note [Quantified kind variables of a family pattern]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider type family KindFam (p :: k1) (q :: k1)
data T :: Maybe k1 -> k2 -> *
type instance KindFam (a :: Maybe k) b = T a b -> Int
The HsBSig for the family patterns will be ([k], [a])
Then in the family instance we want to
* Bring into scope [ "k" -> k:BOX, "a" -> a:k ]
* Kind-check the RHS
* Quantify the type instance over k and k', as well as a,b, thus
type instance [k, k', a:Maybe k, b:k']
KindFam (Maybe k) k' a b = T k k' a b -> Int
Notice that in the third step we quantify over all the visibly-mentioned
type variables (a,b), but also over the implicitly mentioned kind varaibles
(k, k'). In this case one is bound explicitly but often there will be
none. The role of the kind signature (a :: Maybe k) is to add a constraint
that 'a' must have that kind, and to bring 'k' into scope.
%************************************************************************
%* *
Data types
%* *
%************************************************************************
\begin{code}
dataDeclChecks :: Name -> NewOrData -> ThetaType -> [LConDecl Name] -> TcM Bool
dataDeclChecks tc_name new_or_data stupid_theta cons
= do {
gadtSyntax_ok <- xoptM Opt_GADTSyntax
; let h98_syntax = consUseH98Syntax cons
; checkTc (gadtSyntax_ok || h98_syntax) (badGadtDecl tc_name)
; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
; checkTc (new_or_data == DataType || isSingleton cons)
(newtypeConError tc_name (length cons))
; empty_data_decls <- xoptM Opt_EmptyDataDecls
; is_boot <- tcIsHsBoot
; checkTc (not (null cons) || empty_data_decls || is_boot)
(emptyConDeclsErr tc_name)
; return h98_syntax }
consUseH98Syntax :: [LConDecl a] -> Bool
consUseH98Syntax (L _ (ConDecl { con_res = ResTyGADT _ }) : _) = False
consUseH98Syntax _ = True
tcConDecls :: NewOrData -> TyCon -> ([TyVar], Type)
-> [LConDecl Name] -> TcM [DataCon]
tcConDecls new_or_data rep_tycon (tmpl_tvs, res_tmpl) cons
= mapM (addLocM $ tcConDecl new_or_data rep_tycon tmpl_tvs res_tmpl) cons
tcConDecl :: NewOrData
-> TyCon
-> [TyVar] -> Type
-> ConDecl Name
-> TcM DataCon
tcConDecl new_or_data rep_tycon tmpl_tvs res_tmpl
(ConDecl { con_name = name
, con_qvars = hs_tvs, con_cxt = hs_ctxt
, con_details = hs_details, con_res = hs_res_ty })
= addErrCtxt (dataConCtxt name) $
do { traceTc "tcConDecl 1" (ppr name)
; (ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts)
<- tcHsTyVarBndrs hs_tvs $ \ _ ->
do { ctxt <- tcHsContext hs_ctxt
; details <- tcConArgs new_or_data hs_details
; res_ty <- tcConRes hs_res_ty
; let (is_infix, field_lbls, btys) = details
(arg_tys, stricts) = unzip btys
; return (ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts) }
; tkvs <- case res_ty of
ResTyH98 -> quantifyTyVars (mkVarSet tmpl_tvs) (tyVarsOfTypes (ctxt++arg_tys))
ResTyGADT res_ty -> quantifyTyVars emptyVarSet (tyVarsOfTypes (res_ty:ctxt++arg_tys))
; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv tkvs
; arg_tys <- zonkTcTypeToTypes ze arg_tys
; ctxt <- zonkTcTypeToTypes ze ctxt
; res_ty <- case res_ty of
ResTyH98 -> return ResTyH98
ResTyGADT ty -> ResTyGADT <$> zonkTcTypeToType ze ty
; let (univ_tvs, ex_tvs, eq_preds, res_ty') = rejigConRes tmpl_tvs res_tmpl qtkvs res_ty
; fam_envs <- tcGetFamInstEnvs
; buildDataCon fam_envs (unLoc name) is_infix
stricts field_lbls
univ_tvs ex_tvs eq_preds ctxt arg_tys
res_ty' rep_tycon
}
tcConArgs :: NewOrData -> HsConDeclDetails Name -> TcM (Bool, [Name], [(TcType, HsBang)])
tcConArgs new_or_data (PrefixCon btys)
= do { btys' <- mapM (tcConArg new_or_data) btys
; return (False, [], btys') }
tcConArgs new_or_data (InfixCon bty1 bty2)
= do { bty1' <- tcConArg new_or_data bty1
; bty2' <- tcConArg new_or_data bty2
; return (True, [], [bty1', bty2']) }
tcConArgs new_or_data (RecCon fields)
= do { btys' <- mapM (tcConArg new_or_data) btys
; return (False, field_names, btys') }
where
field_names = map (unLoc . cd_fld_name) fields
btys = map cd_fld_type fields
tcConArg :: NewOrData -> LHsType Name -> TcM (TcType, HsBang)
tcConArg new_or_data bty
= do { traceTc "tcConArg 1" (ppr bty)
; arg_ty <- tcHsConArgType new_or_data bty
; traceTc "tcConArg 2" (ppr bty)
; return (arg_ty, getBangStrictness bty) }
tcConRes :: ResType (LHsType Name) -> TcM (ResType Type)
tcConRes ResTyH98 = return ResTyH98
tcConRes (ResTyGADT res_ty) = do { res_ty' <- tcHsLiftedType res_ty
; return (ResTyGADT res_ty') }
\end{code}
Note [Checking GADT return types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There is a delicacy around checking the return types of a datacon. The
central problem is dealing with a declaration like
data T a where
MkT :: a -> Q a
Note that the return type of MkT is totally bogus. When creating the T
tycon, we also need to create the MkT datacon, which must have a "rejigged"
return type. That is, the MkT datacon's type must be transformed to have
a uniform return type with explicit coercions for GADT-like type parameters.
This rejigging is what rejigConRes does. The problem is, though, that checking
that the return type is appropriate is much easier when done over *Type*,
not *HsType*.
So, we want to make rejigConRes lazy and then check the validity of the return
type in checkValidDataCon. But, if the return type is bogus, rejigConRes can't
work -- it will have a failed pattern match. Luckily, if we run
checkValidDataCon before ever looking at the rejigged return type
(checkValidDataCon checks the dataConUserType, which is not rejigged!), we
catch the error before forcing the rejigged type and panicking.
\begin{code}
rejigConRes :: [TyVar] -> Type
-> [TyVar]
-> ResType Type
-> ([TyVar],
[TyVar],
[(TyVar,Type)],
Type)
rejigConRes tmpl_tvs res_ty dc_tvs ResTyH98
= (tmpl_tvs, dc_tvs, [], res_ty)
rejigConRes tmpl_tvs res_tmpl dc_tvs (ResTyGADT res_ty)
= (univ_tvs, ex_tvs, eq_spec, res_ty)
where
Just subst = tcMatchTy (mkVarSet tmpl_tvs) res_tmpl res_ty
(univ_tvs, eq_spec) = foldr choose ([], []) tmpl_tvs
choose tmpl (univs, eqs)
| Just ty <- lookupTyVar subst tmpl
= case tcGetTyVar_maybe ty of
Just tv | not (tv `elem` univs)
-> (tv:univs, eqs)
_other -> (new_tmpl:univs, (new_tmpl,ty):eqs)
where
new_tmpl = updateTyVarKind (substTy subst) tmpl
| otherwise = pprPanic "tcResultType" (ppr res_ty)
ex_tvs = dc_tvs `minusList` univ_tvs
\end{code}
Note [Substitution in template variables kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
data List a = Nil | Cons a (List a)
data SList s as where
SNil :: SList s Nil
We call tcResultType with
tmpl_tvs = [(k :: BOX), (s :: k -> *), (as :: List k)]
res_tmpl = SList k s as
res_ty = ResTyGADT (SList k1 (s1 :: k1 -> *) (Nil k1))
We get subst:
k -> k1
s -> s1
as -> Nil k1
Now we want to find out the universal variables and the equivalences
between some of them and types (GADT).
In this example, k and s are mapped to exactly variables which are not
already present in the universal set, so we just add them without any
coercion.
But 'as' is mapped to 'Nil k1', so we add 'as' to the universal set,
and add the equivalence with 'Nil k1' in 'eqs'.
The problem is that with kind polymorphism, as's kind may now contain
kind variables, and we have to apply the template substitution to it,
which is why we create new_tmpl.
The template substitution only maps kind variables to kind variables,
since GADTs are not kind indexed.
%************************************************************************
%* *
Validity checking
%* *
%************************************************************************
Validity checking is done once the mutually-recursive knot has been
tied, so we can look at things freely.
\begin{code}
checkClassCycleErrs :: Class -> TcM ()
checkClassCycleErrs cls
= unless (null cls_cycles) $ mapM_ recClsErr cls_cycles
where cls_cycles = calcClassCycles cls
checkValidTyCl :: TyThing -> TcM ()
checkValidTyCl thing
= setSrcSpan (getSrcSpan thing) $
addTyThingCtxt thing $
case thing of
ATyCon tc -> checkValidTyCon tc
AnId _ -> return ()
ACoAxiom _ -> return ()
_ -> pprTrace "checkValidTyCl" (ppr thing) $ return ()
checkValidTyCon :: TyCon -> TcM ()
checkValidTyCon tc
| Just cl <- tyConClass_maybe tc
= checkValidClass cl
| Just syn_rhs <- synTyConRhs_maybe tc
= case syn_rhs of
{ ClosedSynFamilyTyCon ax -> checkValidClosedCoAxiom ax
; AbstractClosedSynFamilyTyCon ->
do { hsBoot <- tcIsHsBoot
; checkTc hsBoot $
ptext (sLit "You may omit the equations in a closed type family") $$
ptext (sLit "only in a .hs-boot file") }
; OpenSynFamilyTyCon -> return ()
; SynonymTyCon ty -> checkValidType syn_ctxt ty
; BuiltInSynFamTyCon _ -> return () }
| otherwise
= do {
traceTc "cvtc1" (ppr tc)
; checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc)
; traceTc "cvtc2" (ppr tc)
; dflags <- getDynFlags
; existential_ok <- xoptM Opt_ExistentialQuantification
; gadt_ok <- xoptM Opt_GADTs
; let ex_ok = existential_ok || gadt_ok
; mapM_ (checkValidDataCon dflags ex_ok tc) data_cons
; mapM_ check_fields groups }
where
syn_ctxt = TySynCtxt name
name = tyConName tc
data_cons = tyConDataCons tc
groups = equivClasses cmp_fld (concatMap get_fields data_cons)
cmp_fld (f1,_) (f2,_) = f1 `compare` f2
get_fields con = dataConFieldLabels con `zip` repeat con
check_fields ((label, con1) : other_fields)
= recoverM (return ()) $ mapM_ checkOne other_fields
where
(tvs1, _, _, res1) = dataConSig con1
ts1 = mkVarSet tvs1
fty1 = dataConFieldType con1 label
checkOne (_, con2)
= do { checkFieldCompat label con1 con2 ts1 res1 res2 fty1 fty2
; checkFieldCompat label con2 con1 ts2 res2 res1 fty2 fty1 }
where
(tvs2, _, _, res2) = dataConSig con2
ts2 = mkVarSet tvs2
fty2 = dataConFieldType con2 label
check_fields [] = panic "checkValidTyCon/check_fields []"
checkValidClosedCoAxiom :: CoAxiom Branched -> TcM ()
checkValidClosedCoAxiom (CoAxiom { co_ax_branches = branches, co_ax_tc = tc })
= tcAddClosedTypeFamilyDeclCtxt tc $
do { brListFoldlM_ check_accessibility [] branches
; void $ brListMapM (checkValidTyFamInst Nothing tc) branches }
where
check_accessibility :: [CoAxBranch]
-> CoAxBranch
-> TcM [CoAxBranch]
check_accessibility prev_branches cur_branch
= do { when (cur_branch `isDominatedBy` prev_branches) $
setSrcSpan (coAxBranchSpan cur_branch) $
addErrTc $ inaccessibleCoAxBranch tc cur_branch
; return (cur_branch : prev_branches) }
checkFieldCompat :: Name -> DataCon -> DataCon -> TyVarSet
-> Type -> Type -> Type -> Type -> TcM ()
checkFieldCompat fld con1 con2 tvs1 res1 res2 fty1 fty2
= do { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
where
mb_subst1 = tcMatchTy tvs1 res1 res2
mb_subst2 = tcMatchTyX tvs1 (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM ()
checkValidDataCon dflags existential_ok tc con
= setSrcSpan (srcLocSpan (getSrcLoc con)) $
addErrCtxt (dataConCtxt con) $
do { traceTc "checkValidDataCon" (ppr con $$ ppr tc)
; let tc_tvs = tyConTyVars tc
res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
orig_res_ty = dataConOrigResTy con
; checkTc (isJust (tcMatchTy (mkVarSet tc_tvs)
res_ty_tmpl
orig_res_ty))
(badDataConTyCon con res_ty_tmpl orig_res_ty)
; checkValidMonoType orig_res_ty
; checkValidType ctxt (dataConUserType con)
; when (isNewTyCon tc) (checkNewDataCon con)
; mapM_ check_bang (zip3 (dataConStrictMarks con) (dataConRepBangs con) [1..])
; checkTc (existential_ok || isVanillaDataCon con)
(badExistential con)
; checkTc (not (any (isKindVar . fst) (dataConEqSpec con)))
(badGadtKindCon con)
; traceTc "Done validity of data con" (ppr con <+> ppr (dataConRepType con))
}
where
ctxt = ConArgCtxt (dataConName con)
check_bang (HsUserBang (Just want_unpack) has_bang, rep_bang, n)
| want_unpack, not has_bang
= addWarnTc (bad_bang n (ptext (sLit "UNPACK pragma lacks '!'")))
| want_unpack
, case rep_bang of { HsUnpack {} -> False; _ -> True }
, not (gopt Opt_OmitInterfacePragmas dflags)
= addWarnTc (bad_bang n (ptext (sLit "Ignoring unusable UNPACK pragma")))
check_bang _
= return ()
bad_bang n herald
= hang herald 2 (ptext (sLit "on the") <+> speakNth n
<+> ptext (sLit "argument of") <+> quotes (ppr con))
checkNewDataCon :: DataCon -> TcM ()
checkNewDataCon con
= do { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
; check_con (null eq_spec) $
ptext (sLit "A newtype constructor must have a return type of form T a1 ... an")
; check_con (null theta) $
ptext (sLit "A newtype constructor cannot have a context in its type")
; check_con (null ex_tvs) $
ptext (sLit "A newtype constructor cannot have existential type variables")
; checkTc (not (any isBanged (dataConStrictMarks con)))
(newtypeStrictError con)
}
where
(_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig con
check_con what msg
= checkTc what (msg $$ ppr con <+> dcolon <+> ppr (dataConUserType con))
checkValidClass :: Class -> TcM ()
checkValidClass cls
= do { constrained_class_methods <- xoptM Opt_ConstrainedClassMethods
; multi_param_type_classes <- xoptM Opt_MultiParamTypeClasses
; nullary_type_classes <- xoptM Opt_NullaryTypeClasses
; fundep_classes <- xoptM Opt_FunctionalDependencies
; checkTc (nullary_type_classes || notNull tyvars) (nullaryClassErr cls)
; checkTc (multi_param_type_classes || arity <= 1) (classArityErr cls)
; checkTc (fundep_classes || null fundeps) (classFunDepsErr cls)
; checkValidTheta (ClassSCCtxt (className cls)) theta
; checkClassCycleErrs cls
; mapM_ (check_op constrained_class_methods) op_stuff
; mapM_ check_at_defs at_stuff }
where
(tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
arity = count isTypeVar tyvars
check_op constrained_class_methods (sel_id, dm)
= addErrCtxt (classOpCtxt sel_id tau) $ do
{ checkValidTheta ctxt (tail theta)
; traceTc "class op type" (ppr op_ty <+> ppr tau)
; checkValidType ctxt tau
; let grown_tyvars = growThetaTyVars theta (mkVarSet tyvars)
; checkTc (arity == 0 || tyVarsOfType tau `intersectsVarSet` grown_tyvars)
(noClassTyVarErr cls sel_id)
; case dm of
GenDefMeth dm_name -> do { dm_id <- tcLookupId dm_name
; checkValidType (FunSigCtxt op_name) (idType dm_id) }
_ -> return ()
}
where
ctxt = FunSigCtxt op_name
op_name = idName sel_id
op_ty = idType sel_id
(_,theta1,tau1) = tcSplitSigmaTy op_ty
(_,theta2,tau2) = tcSplitSigmaTy tau1
(theta,tau) | constrained_class_methods = (theta1 ++ theta2, tau2)
| otherwise = (theta1, mkPhiTy (tail theta1) tau1)
check_at_defs (fam_tc, defs)
= tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $
mapM_ (checkValidTyFamInst mb_clsinfo fam_tc) defs
mb_clsinfo = Just (cls, mkVarEnv [ (tv, mkTyVarTy tv) | tv <- tyvars ])
checkFamFlag :: Name -> TcM ()
checkFamFlag tc_name
= do { idx_tys <- xoptM Opt_TypeFamilies
; checkTc idx_tys err_msg }
where
err_msg = hang (ptext (sLit "Illegal family declaraion for") <+> quotes (ppr tc_name))
2 (ptext (sLit "Use TypeFamilies to allow indexed type families"))
\end{code}
%************************************************************************
%* *
Checking role validity
%* *
%************************************************************************
\begin{code}
checkValidRoleAnnots :: RoleAnnots -> TyThing -> TcM ()
checkValidRoleAnnots role_annots thing
= case thing of
{ ATyCon tc
| isSynTyCon tc -> check_no_roles
| isFamilyTyCon tc -> check_no_roles
| isAlgTyCon tc -> check_roles
where
name = tyConName tc
tyvars = tyConTyVars tc
roles = tyConRoles tc
(kind_vars, type_vars) = span isKindVar tyvars
type_roles = dropList kind_vars roles
role_annot_decl_maybe = lookupRoleAnnots role_annots name
check_roles
= whenIsJust role_annot_decl_maybe $
\decl@(L loc (RoleAnnotDecl _ the_role_annots)) ->
addRoleAnnotCtxt name $
setSrcSpan loc $ do
{ role_annots_ok <- xoptM Opt_RoleAnnotations
; checkTc role_annots_ok $ needXRoleAnnotations tc
; checkTc (type_vars `equalLength` the_role_annots)
(wrongNumberOfRoles type_vars decl)
; _ <- zipWith3M checkRoleAnnot type_vars the_role_annots type_roles
; lint <- goptM Opt_DoCoreLinting
; when lint $ checkValidRoles tc }
check_no_roles
= whenIsJust role_annot_decl_maybe illegalRoleAnnotDecl
; _ -> return () }
checkRoleAnnot :: TyVar -> Located (Maybe Role) -> Role -> TcM ()
checkRoleAnnot _ (L _ Nothing) _ = return ()
checkRoleAnnot tv (L _ (Just r1)) r2
= when (r1 /= r2) $
addErrTc $ badRoleAnnot (tyVarName tv) r1 r2
checkValidRoles :: TyCon -> TcM ()
checkValidRoles tc
| isAlgTyCon tc
= mapM_ check_dc_roles (tyConDataCons tc)
| Just (SynonymTyCon rhs) <- synTyConRhs_maybe tc
= check_ty_roles (zipVarEnv (tyConTyVars tc) (tyConRoles tc)) Representational rhs
| otherwise
= return ()
where
check_dc_roles datacon
= do { traceTc "check_dc_roles" (ppr datacon <+> ppr (tyConRoles tc))
; mapM_ (check_ty_roles role_env Representational) $
eqSpecPreds eq_spec ++ theta ++ arg_tys }
where
(univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig datacon
univ_roles = zipVarEnv univ_tvs (tyConRoles tc)
ex_roles = mkVarEnv (zip ex_tvs (repeat Nominal))
role_env = univ_roles `plusVarEnv` ex_roles
check_ty_roles env role (TyVarTy tv)
= case lookupVarEnv env tv of
Just role' -> unless (role' `ltRole` role || role' == role) $
report_error $ ptext (sLit "type variable") <+> quotes (ppr tv) <+>
ptext (sLit "cannot have role") <+> ppr role <+>
ptext (sLit "because it was assigned role") <+> ppr role'
Nothing -> report_error $ ptext (sLit "type variable") <+> quotes (ppr tv) <+>
ptext (sLit "missing in environment")
check_ty_roles env Representational (TyConApp tc tys)
= let roles' = tyConRoles tc in
zipWithM_ (maybe_check_ty_roles env) roles' tys
check_ty_roles env Nominal (TyConApp _ tys)
= mapM_ (check_ty_roles env Nominal) tys
check_ty_roles _ Phantom ty@(TyConApp {})
= pprPanic "check_ty_roles" (ppr ty)
check_ty_roles env role (AppTy ty1 ty2)
= check_ty_roles env role ty1
>> check_ty_roles env Nominal ty2
check_ty_roles env role (FunTy ty1 ty2)
= check_ty_roles env role ty1
>> check_ty_roles env role ty2
check_ty_roles env role (ForAllTy tv ty)
= check_ty_roles (extendVarEnv env tv Nominal) role ty
check_ty_roles _ _ (LitTy {}) = return ()
maybe_check_ty_roles env role ty
= when (role == Nominal || role == Representational) $
check_ty_roles env role ty
report_error doc
= addErrTc $ vcat [ptext (sLit "Internal error in role inference:"),
doc,
ptext (sLit "Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug")]
\end{code}
%************************************************************************
%* *
Building record selectors
%* *
%************************************************************************
\begin{code}
mkDefaultMethodIds :: [TyThing] -> [Id]
mkDefaultMethodIds things
= [ mkExportedLocalId dm_name (idType sel_id)
| ATyCon tc <- things
, Just cls <- [tyConClass_maybe tc]
, (sel_id, DefMeth dm_name) <- classOpItems cls ]
\end{code}
Note [Default method Ids and Template Haskell]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this (Trac #4169):
class Numeric a where
fromIntegerNum :: a
fromIntegerNum = ...
ast :: Q [Dec]
ast = [d| instance Numeric Int |]
When we typecheck 'ast' we have done the first pass over the class decl
(in tcTyClDecls), but we have not yet typechecked the default-method
declarations (because they can mention value declarations). So we
must bring the default method Ids into scope first (so they can be seen
when typechecking the [d| .. |] quote, and typecheck them later.
\begin{code}
mkRecSelBinds :: [TyThing] -> HsValBinds Name
mkRecSelBinds tycons
= ValBindsOut [(NonRecursive, b) | b <- binds] sigs
where
(sigs, binds) = unzip rec_sels
rec_sels = map mkRecSelBind [ (tc,fld)
| ATyCon tc <- tycons
, fld <- tyConFields tc ]
mkRecSelBind :: (TyCon, FieldLabel) -> (LSig Name, LHsBinds Name)
mkRecSelBind (tycon, sel_name)
= (L loc (IdSig sel_id), unitBag (Generated, L loc sel_bind))
where
loc = getSrcSpan sel_name
sel_id = Var.mkExportedLocalVar rec_details sel_name
sel_ty vanillaIdInfo
rec_details = RecSelId { sel_tycon = tycon, sel_naughty = is_naughty }
all_cons = tyConDataCons tycon
cons_w_field = [ con | con <- all_cons
, sel_name `elem` dataConFieldLabels con ]
con1 = ASSERT( not (null cons_w_field) ) head cons_w_field
field_ty = dataConFieldType con1 sel_name
data_ty = dataConOrigResTy con1
data_tvs = tyVarsOfType data_ty
is_naughty = not (tyVarsOfType field_ty `subVarSet` data_tvs)
(field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
sel_ty | is_naughty = unitTy
| otherwise = mkForAllTys (varSetElemsKvsFirst $
data_tvs `extendVarSetList` field_tvs) $
mkPhiTy (dataConStupidTheta con1) $
mkPhiTy field_theta $
mkFunTy data_ty field_tau
sel_bind | is_naughty = mkTopFunBind sel_lname [mkSimpleMatch [] unit_rhs]
| otherwise = mkTopFunBind sel_lname (map mk_match cons_w_field ++ deflt)
mk_match con = mkSimpleMatch [L loc (mk_sel_pat con)]
(L loc (HsVar field_var))
mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields)
rec_fields = HsRecFields { rec_flds = [rec_field], rec_dotdot = Nothing }
rec_field = HsRecField { hsRecFieldId = sel_lname
, hsRecFieldArg = L loc (VarPat field_var)
, hsRecPun = False }
sel_lname = L loc sel_name
field_var = mkInternalName (mkBuiltinUnique 1) (getOccName sel_name) loc
deflt | all dealt_with all_cons = []
| otherwise = [mkSimpleMatch [L loc (WildPat placeHolderType)]
(mkHsApp (L loc (HsVar (getName rEC_SEL_ERROR_ID)))
(L loc (HsLit msg_lit)))]
dealt_with con = con `elem` cons_w_field || dataConCannotMatch inst_tys con
inst_tys = substTyVars (mkTopTvSubst (dataConEqSpec con1)) (dataConUnivTyVars con1)
unit_rhs = mkLHsTupleExpr []
msg_lit = HsStringPrim $ unsafeMkByteString $
occNameString (getOccName sel_name)
tyConFields :: TyCon -> [FieldLabel]
tyConFields tc
| isAlgTyCon tc = nub (concatMap dataConFieldLabels (tyConDataCons tc))
| otherwise = []
\end{code}
Note [Polymorphic selectors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When a record has a polymorphic field, we pull the foralls out to the front.
data T = MkT { f :: forall a. [a] -> a }
Then f :: forall a. T -> [a] -> a
NOT f :: T -> forall a. [a] -> a
This is horrid. It's only needed in deeply obscure cases, which I hate.
The only case I know is test tc163, which is worth looking at. It's far
from clear that this test should succeed at all!
Note [Naughty record selectors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A "naughty" field is one for which we can't define a record
selector, because an existential type variable would escape. For example:
data T = forall a. MkT { x,y::a }
We obviously can't define
x (MkT v _) = v
Nevertheless we *do* put a RecSelId into the type environment
so that if the user tries to use 'x' as a selector we can bleat
helpfully, rather than saying unhelpfully that 'x' is not in scope.
Hence the sel_naughty flag, to identify record selectors that don't really exist.
In general, a field is "naughty" if its type mentions a type variable that
isn't in the result type of the constructor. Note that this *allows*
GADT record selectors (Note [GADT record selectors]) whose types may look
like sel :: T [a] -> a
For naughty selectors we make a dummy binding
sel = ()
for naughty selectors, so that the later type-check will add them to the
environment, and they'll be exported. The function is never called, because
the tyepchecker spots the sel_naughty field.
Note [GADT record selectors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For GADTs, we require that all constructors with a common field 'f' have the same
result type (modulo alpha conversion). [Checked in TcTyClsDecls.checkValidTyCon]
E.g.
data T where
T1 { f :: Maybe a } :: T [a]
T2 { f :: Maybe a, y :: b } :: T [a]
T3 :: T Int
and now the selector takes that result type as its argument:
f :: forall a. T [a] -> Maybe a
Details: the "real" types of T1,T2 are:
T1 :: forall r a. (r~[a]) => a -> T r
T2 :: forall r a b. (r~[a]) => a -> b -> T r
So the selector loooks like this:
f :: forall a. T [a] -> Maybe a
f (a:*) (t:T [a])
= case t of
T1 c (g:[a]~[c]) (v:Maybe c) -> v `cast` Maybe (right (sym g))
T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
T3 -> error "T3 does not have field f"
Note the forall'd tyvars of the selector are just the free tyvars
of the result type; there may be other tyvars in the constructor's
type (e.g. 'b' in T2).
Note the need for casts in the result!
Note [Selector running example]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's OK to combine GADTs and type families. Here's a running example:
data instance T [a] where
T1 { fld :: b } :: T [Maybe b]
The representation type looks like this
data :R7T a where
T1 { fld :: b } :: :R7T (Maybe b)
and there's coercion from the family type to the representation type
:CoR7T a :: T [a] ~ :R7T a
The selector we want for fld looks like this:
fld :: forall b. T [Maybe b] -> b
fld = /\b. \(d::T [Maybe b]).
case d `cast` :CoR7T (Maybe b) of
T1 (x::b) -> x
The scrutinee of the case has type :R7T (Maybe b), which can be
gotten by appying the eq_spec to the univ_tvs of the data con.
%************************************************************************
%* *
Error messages
%* *
%************************************************************************
\begin{code}
tcAddDefaultAssocDeclCtxt :: Name -> TcM a -> TcM a
tcAddDefaultAssocDeclCtxt name thing_inside
= addErrCtxt ctxt thing_inside
where
ctxt = hsep [ptext (sLit "In the type synonym instance default declaration for"),
quotes (ppr name)]
tcAddTyFamInstCtxt :: TyFamInstDecl Name -> TcM a -> TcM a
tcAddTyFamInstCtxt decl
= tcAddFamInstCtxt (ptext (sLit "type instance")) (tyFamInstDeclName decl)
tcAddDataFamInstCtxt :: DataFamInstDecl Name -> TcM a -> TcM a
tcAddDataFamInstCtxt decl
= tcAddFamInstCtxt (pprDataFamInstFlavour decl <+> ptext (sLit "instance"))
(unLoc (dfid_tycon decl))
tcAddFamInstCtxt :: SDoc -> Name -> TcM a -> TcM a
tcAddFamInstCtxt flavour tycon thing_inside
= addErrCtxt ctxt thing_inside
where
ctxt = hsep [ptext (sLit "In the") <+> flavour
<+> ptext (sLit "declaration for"),
quotes (ppr tycon)]
tcAddClosedTypeFamilyDeclCtxt :: TyCon -> TcM a -> TcM a
tcAddClosedTypeFamilyDeclCtxt tc
= addErrCtxt ctxt
where
ctxt = ptext (sLit "In the equations for closed type family") <+>
quotes (ppr tc)
resultTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc
resultTypeMisMatch field_name con1 con2
= vcat [sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2,
ptext (sLit "have a common field") <+> quotes (ppr field_name) <> comma],
nest 2 $ ptext (sLit "but have different result types")]
fieldTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc
fieldTypeMisMatch field_name con1 con2
= sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2,
ptext (sLit "give different types for field"), quotes (ppr field_name)]
dataConCtxt :: Outputable a => a -> SDoc
dataConCtxt con = ptext (sLit "In the definition of data constructor") <+> quotes (ppr con)
classOpCtxt :: Var -> Type -> SDoc
classOpCtxt sel_id tau = sep [ptext (sLit "When checking the class method:"),
nest 2 (pprPrefixOcc sel_id <+> dcolon <+> ppr tau)]
nullaryClassErr :: Class -> SDoc
nullaryClassErr cls
= vcat [ptext (sLit "No parameters for class") <+> quotes (ppr cls),
parens (ptext (sLit "Use NullaryTypeClasses to allow no-parameter classes"))]
classArityErr :: Class -> SDoc
classArityErr cls
= vcat [ptext (sLit "Too many parameters for class") <+> quotes (ppr cls),
parens (ptext (sLit "Use MultiParamTypeClasses to allow multi-parameter classes"))]
classFunDepsErr :: Class -> SDoc
classFunDepsErr cls
= vcat [ptext (sLit "Fundeps in class") <+> quotes (ppr cls),
parens (ptext (sLit "Use FunctionalDependencies to allow fundeps"))]
noClassTyVarErr :: Class -> Var -> SDoc
noClassTyVarErr clas op
= sep [ptext (sLit "The class method") <+> quotes (ppr op),
ptext (sLit "mentions none of the type variables of the class") <+>
ppr clas <+> hsep (map ppr (classTyVars clas))]
recSynErr :: [LTyClDecl Name] -> TcRn ()
recSynErr syn_decls
= setSrcSpan (getLoc (head sorted_decls)) $
addErr (sep [ptext (sLit "Cycle in type synonym declarations:"),
nest 2 (vcat (map ppr_decl sorted_decls))])
where
sorted_decls = sortLocated syn_decls
ppr_decl (L loc decl) = ppr loc <> colon <+> ppr decl
recClsErr :: [TyCon] -> TcRn ()
recClsErr cycles
= addErr (sep [ptext (sLit "Cycle in class declaration (via superclasses):"),
nest 2 (hsep (intersperse (text "->") (map ppr cycles)))])
badDataConTyCon :: DataCon -> Type -> Type -> SDoc
badDataConTyCon data_con res_ty_tmpl actual_res_ty
= hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con) <+>
ptext (sLit "returns type") <+> quotes (ppr actual_res_ty))
2 (ptext (sLit "instead of an instance of its parent type") <+> quotes (ppr res_ty_tmpl))
badGadtKindCon :: DataCon -> SDoc
badGadtKindCon data_con
= hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con)
<+> ptext (sLit "cannot be GADT-like in its *kind* arguments"))
2 (ppr data_con <+> dcolon <+> ppr (dataConUserType data_con))
badGadtDecl :: Name -> SDoc
badGadtDecl tc_name
= vcat [ ptext (sLit "Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
, nest 2 (parens $ ptext (sLit "Use GADTs to allow GADTs")) ]
badExistential :: DataCon -> SDoc
badExistential con
= hang (ptext (sLit "Data constructor") <+> quotes (ppr con) <+>
ptext (sLit "has existential type variables, a context, or a specialised result type"))
2 (vcat [ ppr con <+> dcolon <+> ppr (dataConUserType con)
, parens $ ptext (sLit "Use ExistentialQuantification or GADTs to allow this") ])
badStupidTheta :: Name -> SDoc
badStupidTheta tc_name
= ptext (sLit "A data type declared in GADT style cannot have a context:") <+> quotes (ppr tc_name)
newtypeConError :: Name -> Int -> SDoc
newtypeConError tycon n
= sep [ptext (sLit "A newtype must have exactly one constructor,"),
nest 2 $ ptext (sLit "but") <+> quotes (ppr tycon) <+> ptext (sLit "has") <+> speakN n ]
newtypeStrictError :: DataCon -> SDoc
newtypeStrictError con
= sep [ptext (sLit "A newtype constructor cannot have a strictness annotation,"),
nest 2 $ ptext (sLit "but") <+> quotes (ppr con) <+> ptext (sLit "does")]
newtypeFieldErr :: DataCon -> Int -> SDoc
newtypeFieldErr con_name n_flds
= sep [ptext (sLit "The constructor of a newtype must have exactly one field"),
nest 2 $ ptext (sLit "but") <+> quotes (ppr con_name) <+> ptext (sLit "has") <+> speakN n_flds]
badSigTyDecl :: Name -> SDoc
badSigTyDecl tc_name
= vcat [ ptext (sLit "Illegal kind signature") <+>
quotes (ppr tc_name)
, nest 2 (parens $ ptext (sLit "Use KindSignatures to allow kind signatures")) ]
emptyConDeclsErr :: Name -> SDoc
emptyConDeclsErr tycon
= sep [quotes (ppr tycon) <+> ptext (sLit "has no constructors"),
nest 2 $ ptext (sLit "(EmptyDataDecls permits this)")]
wrongKindOfFamily :: TyCon -> SDoc
wrongKindOfFamily family
= ptext (sLit "Wrong category of family instance; declaration was for a")
<+> kindOfFamily
where
kindOfFamily | isSynTyCon family = ptext (sLit "type synonym")
| isAlgTyCon family = ptext (sLit "data type")
| otherwise = pprPanic "wrongKindOfFamily" (ppr family)
wrongNumberOfParmsErrTooMany :: Arity -> SDoc
wrongNumberOfParmsErrTooMany max_args
= ptext (sLit "Number of parameters must match family declaration; expected no more than")
<+> ppr max_args
wrongNamesInInstGroup :: Name -> Name -> SDoc
wrongNamesInInstGroup first cur
= ptext (sLit "Mismatched type names in closed type family declaration.") $$
ptext (sLit "First name was") <+>
(ppr first) <> (ptext (sLit "; this one is")) <+> (ppr cur)
inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
inaccessibleCoAxBranch tc fi
= ptext (sLit "Inaccessible family instance equation:") $$
(pprCoAxBranch tc fi)
badRoleAnnot :: Name -> Role -> Role -> SDoc
badRoleAnnot var annot inferred
= hang (ptext (sLit "Role mismatch on variable") <+> ppr var <> colon)
2 (sep [ ptext (sLit "Annotation says"), ppr annot
, ptext (sLit "but role"), ppr inferred
, ptext (sLit "is required") ])
wrongNumberOfRoles :: [a] -> LRoleAnnotDecl Name -> SDoc
wrongNumberOfRoles tyvars d@(L _ (RoleAnnotDecl _ annots))
= hang (ptext (sLit "Wrong number of roles listed in role annotation;") $$
ptext (sLit "Expected") <+> (ppr $ length tyvars) <> comma <+>
ptext (sLit "got") <+> (ppr $ length annots) <> colon)
2 (ppr d)
illegalRoleAnnotDecl :: LRoleAnnotDecl Name -> TcM ()
illegalRoleAnnotDecl (L loc (RoleAnnotDecl tycon _))
= setErrCtxt [] $
setSrcSpan loc $
addErrTc (ptext (sLit "Illegal role annotation for") <+> ppr tycon <> char ';' $$
ptext (sLit "they are allowed only for datatypes and classes."))
needXRoleAnnotations :: TyCon -> SDoc
needXRoleAnnotations tc
= ptext (sLit "Illegal role annotation for") <+> ppr tc <> char ';' $$
ptext (sLit "did you intend to use RoleAnnotations?")
addTyThingCtxt :: TyThing -> TcM a -> TcM a
addTyThingCtxt thing
= addErrCtxt ctxt
where
name = getName thing
flav = case thing of
ATyCon tc
| isClassTyCon tc -> ptext (sLit "class")
| isSynFamilyTyCon tc -> ptext (sLit "type family")
| isDataFamilyTyCon tc -> ptext (sLit "data family")
| isSynTyCon tc -> ptext (sLit "type")
| isNewTyCon tc -> ptext (sLit "newtype")
| isDataTyCon tc -> ptext (sLit "data")
_ -> pprTrace "addTyThingCtxt strange" (ppr thing)
empty
ctxt = hsep [ ptext (sLit "In the"), flav
, ptext (sLit "declaration for"), quotes (ppr name) ]
addRoleAnnotCtxt :: Name -> TcM a -> TcM a
addRoleAnnotCtxt name
= addErrCtxt $
text "while checking a role annotation for" <+> quotes (ppr name)
\end{code}