2 % (c) The AQUA Project, Glasgow University, 1996-1998
4 \section[TcTyClsDecls]{Typecheck type and class declarations}
11 #include "HsVersions.h"
13 import HsSyn ( TyClDecl(..), HsConDetails(..), HsTyVarBndr(..),
14 ConDecl(..), Sig(..), NewOrData(..), ResType(..),
15 tyClDeclTyVars, isSynDecl, isClassDecl, hsConArgs,
16 LTyClDecl, tcdName, hsTyVarName, LHsTyVarBndr
18 import HsTypes ( HsBang(..), getBangStrictness )
19 import BasicTypes ( RecFlag(..), StrictnessMark(..) )
20 import HscTypes ( implicitTyThings, ModDetails )
21 import BuildTyCl ( buildClass, buildAlgTyCon, buildSynTyCon, buildDataCon,
22 mkDataTyConRhs, mkNewTyConRhs )
24 import TcEnv ( TyThing(..),
25 tcLookupLocated, tcLookupLocatedGlobal,
26 tcExtendGlobalEnv, tcExtendKindEnv, tcExtendKindEnvTvs,
27 tcExtendRecEnv, tcLookupTyVar, InstInfo )
28 import TcTyDecls ( calcRecFlags, calcClassCycles, calcSynCycles )
29 import TcClassDcl ( tcClassSigs, tcAddDeclCtxt )
30 import TcHsType ( kcHsTyVars, kcHsLiftedSigType, kcHsType,
31 kcHsContext, tcTyVarBndrs, tcHsKindedType, tcHsKindedContext,
32 kcHsSigType, tcHsBangType, tcLHsConResTy, tcDataKindSig )
33 import TcMType ( newKindVar, checkValidTheta, checkValidType,
35 UserTypeCtxt(..), SourceTyCtxt(..) )
36 import TcType ( TcKind, TcType, Type, tyVarsOfType, mkPhiTy,
37 mkArrowKind, liftedTypeKind, mkTyVarTys,
38 tcSplitSigmaTy, tcEqTypes, tcGetTyVar_maybe )
39 import Type ( PredType(..), splitTyConApp_maybe, mkTyVarTy,
41 -- pprParendType, pprThetaArrow
43 import Generics ( validGenericMethodType, canDoGenerics )
44 import Class ( Class, className, classTyCon, DefMeth(..), classBigSig, classTyVars )
45 import TyCon ( TyCon, AlgTyConRhs( AbstractTyCon ),
46 tyConDataCons, mkForeignTyCon, isProductTyCon, isRecursiveTyCon,
47 tyConStupidTheta, synTyConRhs, isSynTyCon, tyConName,
49 import DataCon ( DataCon, dataConUserType, dataConName,
50 dataConFieldLabels, dataConTyCon, dataConAllTyVars,
51 dataConFieldType, dataConResTys )
52 import Var ( TyVar, idType, idName )
53 import VarSet ( elemVarSet, mkVarSet )
54 import Name ( Name, getSrcLoc )
56 import Maybe ( isJust )
57 import Maybes ( expectJust )
58 import Unify ( tcMatchTys, tcMatchTyX )
59 import Util ( zipLazy, isSingleton, notNull, sortLe )
60 import List ( partition )
61 import SrcLoc ( Located(..), unLoc, getLoc, srcLocSpan )
62 import ListSetOps ( equivClasses, minusList )
63 import List ( delete )
64 import Digraph ( SCC(..) )
65 import DynFlags ( DynFlag( Opt_GlasgowExts, Opt_Generics,
66 Opt_UnboxStrictFields ) )
70 %************************************************************************
72 \subsection{Type checking for type and class declarations}
74 %************************************************************************
78 Consider a mutually-recursive group, binding
79 a type constructor T and a class C.
81 Step 1: getInitialKind
82 Construct a KindEnv by binding T and C to a kind variable
85 In that environment, do a kind check
87 Step 3: Zonk the kinds
89 Step 4: buildTyConOrClass
90 Construct an environment binding T to a TyCon and C to a Class.
91 a) Their kinds comes from zonking the relevant kind variable
92 b) Their arity (for synonyms) comes direct from the decl
93 c) The funcional dependencies come from the decl
94 d) The rest comes a knot-tied binding of T and C, returned from Step 4
95 e) The variances of the tycons in the group is calculated from
99 In this environment, walk over the decls, constructing the TyCons and Classes.
100 This uses in a strict way items (a)-(c) above, which is why they must
101 be constructed in Step 4. Feed the results back to Step 4.
102 For this step, pass the is-recursive flag as the wimp-out flag
106 Step 6: Extend environment
107 We extend the type environment with bindings not only for the TyCons and Classes,
108 but also for their "implicit Ids" like data constructors and class selectors
110 Step 7: checkValidTyCl
111 For a recursive group only, check all the decls again, just
112 to check all the side conditions on validity. We could not
113 do this before because we were in a mutually recursive knot.
115 Identification of recursive TyCons
116 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
117 The knot-tying parameters: @rec_details_list@ is an alist mapping @Name@s to
120 Identifying a TyCon as recursive serves two purposes
122 1. Avoid infinite types. Non-recursive newtypes are treated as
123 "transparent", like type synonyms, after the type checker. If we did
124 this for all newtypes, we'd get infinite types. So we figure out for
125 each newtype whether it is "recursive", and add a coercion if so. In
126 effect, we are trying to "cut the loops" by identifying a loop-breaker.
128 2. Avoid infinite unboxing. This is nothing to do with newtypes.
132 Well, this function diverges, but we don't want the strictness analyser
133 to diverge. But the strictness analyser will diverge because it looks
134 deeper and deeper into the structure of T. (I believe there are
135 examples where the function does something sane, and the strictness
136 analyser still diverges, but I can't see one now.)
138 Now, concerning (1), the FC2 branch currently adds a coercion for ALL
139 newtypes. I did this as an experiment, to try to expose cases in which
140 the coercions got in the way of optimisations. If it turns out that we
141 can indeed always use a coercion, then we don't risk recursive types,
142 and don't need to figure out what the loop breakers are.
144 For newtype *families* though, we will always have a coercion, so they
145 are always loop breakers! So you can easily adjust the current
146 algorithm by simply treating all newtype families as loop breakers (and
147 indeed type families). I think.
150 tcTyAndClassDecls :: ModDetails -> [LTyClDecl Name]
151 -> TcM TcGblEnv -- Input env extended by types and classes
152 -- and their implicit Ids,DataCons
153 tcTyAndClassDecls boot_details decls
154 = do { -- First check for cyclic type synonysm or classes
155 -- See notes with checkCycleErrs
158 ; traceTc (text "tcTyAndCl" <+> ppr mod)
159 ; (syn_tycons, alg_tyclss) <- fixM (\ ~(rec_syn_tycons, rec_alg_tyclss) ->
160 do { let { -- Calculate variances and rec-flag
161 ; (syn_decls, alg_decls) = partition (isSynDecl . unLoc)
163 -- Extend the global env with the knot-tied results
164 -- for data types and classes
166 -- We must populate the environment with the loop-tied T's right
167 -- away, because the kind checker may "fault in" some type
168 -- constructors that recursively mention T
169 ; let { gbl_things = mkGlobalThings alg_decls rec_alg_tyclss }
170 ; tcExtendRecEnv gbl_things $ do
172 -- Kind-check the declarations
173 { (kc_syn_decls, kc_alg_decls) <- kcTyClDecls syn_decls alg_decls
175 ; let { calc_rec = calcRecFlags boot_details rec_alg_tyclss
176 ; tc_decl = addLocM (tcTyClDecl calc_rec) }
177 -- Type-check the type synonyms, and extend the envt
178 ; syn_tycons <- tcSynDecls kc_syn_decls
179 ; tcExtendGlobalEnv syn_tycons $ do
181 -- Type-check the data types and classes
182 { alg_tyclss <- mappM tc_decl kc_alg_decls
183 ; return (syn_tycons, alg_tyclss)
185 -- Finished with knot-tying now
186 -- Extend the environment with the finished things
187 ; tcExtendGlobalEnv (syn_tycons ++ alg_tyclss) $ do
189 -- Perform the validity check
190 { traceTc (text "ready for validity check")
191 ; mappM_ (addLocM checkValidTyCl) decls
192 ; traceTc (text "done")
194 -- Add the implicit things;
195 -- we want them in the environment because
196 -- they may be mentioned in interface files
197 ; let { implicit_things = concatMap implicitTyThings alg_tyclss }
198 ; traceTc ((text "Adding" <+> ppr alg_tyclss) $$ (text "and" <+> ppr implicit_things))
199 ; tcExtendGlobalEnv implicit_things getGblEnv
202 mkGlobalThings :: [LTyClDecl Name] -- The decls
203 -> [TyThing] -- Knot-tied, in 1-1 correspondence with the decls
205 -- Driven by the Decls, and treating the TyThings lazily
206 -- make a TypeEnv for the new things
207 mkGlobalThings decls things
208 = map mk_thing (decls `zipLazy` things)
210 mk_thing (L _ (ClassDecl {tcdLName = L _ name}), ~(AClass cl))
212 mk_thing (L _ decl, ~(ATyCon tc))
213 = (tcdName decl, ATyCon tc)
217 %************************************************************************
221 %************************************************************************
223 We need to kind check all types in the mutually recursive group
224 before we know the kind of the type variables. For example:
227 op :: D b => a -> b -> b
230 bop :: (Monad c) => ...
232 Here, the kind of the locally-polymorphic type variable "b"
233 depends on *all the uses of class D*. For example, the use of
234 Monad c in bop's type signature means that D must have kind Type->Type.
236 However type synonyms work differently. They can have kinds which don't
237 just involve (->) and *:
238 type R = Int# -- Kind #
239 type S a = Array# a -- Kind * -> #
240 type T a b = (# a,b #) -- Kind * -> * -> (# a,b #)
241 So we must infer their kinds from their right-hand sides *first* and then
242 use them, whereas for the mutually recursive data types D we bring into
243 scope kind bindings D -> k, where k is a kind variable, and do inference.
246 kcTyClDecls syn_decls alg_decls
247 = do { -- First extend the kind env with each data
248 -- type and class, mapping them to a type variable
249 alg_kinds <- mappM getInitialKind alg_decls
250 ; tcExtendKindEnv alg_kinds $ do
252 -- Now kind-check the type synonyms, in dependency order
253 -- We do these differently to data type and classes,
254 -- because a type synonym can be an unboxed type
256 -- and a kind variable can't unify with UnboxedTypeKind
257 -- So we infer their kinds in dependency order
258 { (kc_syn_decls, syn_kinds) <- kcSynDecls (calcSynCycles syn_decls)
259 ; tcExtendKindEnv syn_kinds $ do
261 -- Now kind-check the data type and class declarations,
262 -- returning kind-annotated decls
263 { kc_alg_decls <- mappM (wrapLocM kcTyClDecl) alg_decls
265 ; return (kc_syn_decls, kc_alg_decls) }}}
267 ------------------------------------------------------------------------
268 getInitialKind :: LTyClDecl Name -> TcM (Name, TcKind)
269 -- Only for data type and class declarations
270 -- Get as much info as possible from the data or class decl,
271 -- so as to maximise usefulness of error messages
272 getInitialKind (L _ decl)
273 = do { arg_kinds <- mapM (mk_arg_kind . unLoc) (tyClDeclTyVars decl)
274 ; res_kind <- mk_res_kind decl
275 ; return (tcdName decl, mkArrowKinds arg_kinds res_kind) }
277 mk_arg_kind (UserTyVar _) = newKindVar
278 mk_arg_kind (KindedTyVar _ kind) = return kind
280 mk_res_kind (TyData { tcdKindSig = Just kind }) = return kind
281 -- On GADT-style declarations we allow a kind signature
282 -- data T :: *->* where { ... }
283 mk_res_kind other = return liftedTypeKind
287 kcSynDecls :: [SCC (LTyClDecl Name)]
288 -> TcM ([LTyClDecl Name], -- Kind-annotated decls
289 [(Name,TcKind)]) -- Kind bindings
292 kcSynDecls (group : groups)
293 = do { (decl, nk) <- kcSynDecl group
294 ; (decls, nks) <- tcExtendKindEnv [nk] (kcSynDecls groups)
295 ; return (decl:decls, nk:nks) }
298 kcSynDecl :: SCC (LTyClDecl Name)
299 -> TcM (LTyClDecl Name, -- Kind-annotated decls
300 (Name,TcKind)) -- Kind bindings
301 kcSynDecl (AcyclicSCC ldecl@(L loc decl))
302 = tcAddDeclCtxt decl $
303 kcHsTyVars (tcdTyVars decl) (\ k_tvs ->
304 do { traceTc (text "kcd1" <+> ppr (unLoc (tcdLName decl)) <+> brackets (ppr (tcdTyVars decl))
305 <+> brackets (ppr k_tvs))
306 ; (k_rhs, rhs_kind) <- kcHsType (tcdSynRhs decl)
307 ; traceTc (text "kcd2" <+> ppr (unLoc (tcdLName decl)))
308 ; let tc_kind = foldr (mkArrowKind . kindedTyVarKind) rhs_kind k_tvs
309 ; return (L loc (decl { tcdTyVars = k_tvs, tcdSynRhs = k_rhs }),
310 (unLoc (tcdLName decl), tc_kind)) })
312 kcSynDecl (CyclicSCC decls)
313 = do { recSynErr decls; failM } -- Fail here to avoid error cascade
314 -- of out-of-scope tycons
316 kindedTyVarKind (L _ (KindedTyVar _ k)) = k
318 ------------------------------------------------------------------------
319 kcTyClDecl :: TyClDecl Name -> TcM (TyClDecl Name)
320 -- Not used for type synonyms (see kcSynDecl)
322 kcTyClDecl decl@(TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdCons = cons})
323 = kcTyClDeclBody decl $ \ tvs' ->
324 do { ctxt' <- kcHsContext ctxt
325 ; cons' <- mappM (wrapLocM kc_con_decl) cons
326 ; return (decl {tcdTyVars = tvs', tcdCtxt = ctxt', tcdCons = cons'}) }
328 kc_con_decl (ConDecl name expl ex_tvs ex_ctxt details res) = do
329 kcHsTyVars ex_tvs $ \ex_tvs' -> do
330 ex_ctxt' <- kcHsContext ex_ctxt
331 details' <- kc_con_details details
333 ResTyH98 -> return ResTyH98
334 ResTyGADT ty -> do { ty' <- kcHsSigType ty; return (ResTyGADT ty') }
335 return (ConDecl name expl ex_tvs' ex_ctxt' details' res')
337 kc_con_details (PrefixCon btys)
338 = do { btys' <- mappM kc_larg_ty btys ; return (PrefixCon btys') }
339 kc_con_details (InfixCon bty1 bty2)
340 = do { bty1' <- kc_larg_ty bty1; bty2' <- kc_larg_ty bty2; return (InfixCon bty1' bty2') }
341 kc_con_details (RecCon fields)
342 = do { fields' <- mappM kc_field fields; return (RecCon fields') }
344 kc_field (fld, bty) = do { bty' <- kc_larg_ty bty ; return (fld, bty') }
346 kc_larg_ty bty = case new_or_data of
347 DataType -> kcHsSigType bty
348 NewType -> kcHsLiftedSigType bty
349 -- Can't allow an unlifted type for newtypes, because we're effectively
350 -- going to remove the constructor while coercing it to a lifted type.
351 -- And newtypes can't be bang'd
354 kcTyClDecl decl@(ClassDecl {tcdCtxt = ctxt, tcdSigs = sigs})
355 = kcTyClDeclBody decl $ \ tvs' ->
356 do { is_boot <- tcIsHsBoot
357 ; ctxt' <- kcHsContext ctxt
358 ; sigs' <- mappM (wrapLocM kc_sig) sigs
359 ; return (decl {tcdTyVars = tvs', tcdCtxt = ctxt', tcdSigs = sigs'}) }
361 kc_sig (TypeSig nm op_ty) = do { op_ty' <- kcHsLiftedSigType op_ty
362 ; return (TypeSig nm op_ty') }
363 kc_sig other_sig = return other_sig
365 kcTyClDecl decl@(ForeignType {})
368 kcTyClDeclBody :: TyClDecl Name
369 -> ([LHsTyVarBndr Name] -> TcM a)
371 -- getInitialKind has made a suitably-shaped kind for the type or class
372 -- Unpack it, and attribute those kinds to the type variables
373 -- Extend the env with bindings for the tyvars, taken from
374 -- the kind of the tycon/class. Give it to the thing inside, and
375 -- check the result kind matches
376 kcTyClDeclBody decl thing_inside
377 = tcAddDeclCtxt decl $
378 do { tc_ty_thing <- tcLookupLocated (tcdLName decl)
379 ; let tc_kind = case tc_ty_thing of { AThing k -> k }
380 (kinds, _) = splitKindFunTys tc_kind
381 hs_tvs = tcdTyVars decl
382 kinded_tvs = ASSERT( length kinds >= length hs_tvs )
383 [ L loc (KindedTyVar (hsTyVarName tv) k)
384 | (L loc tv, k) <- zip hs_tvs kinds]
385 ; tcExtendKindEnvTvs kinded_tvs (thing_inside kinded_tvs) }
389 %************************************************************************
391 \subsection{Type checking}
393 %************************************************************************
396 tcSynDecls :: [LTyClDecl Name] -> TcM [TyThing]
397 tcSynDecls [] = return []
398 tcSynDecls (decl : decls)
399 = do { syn_tc <- addLocM tcSynDecl decl
400 ; syn_tcs <- tcExtendGlobalEnv [syn_tc] (tcSynDecls decls)
401 ; return (syn_tc : syn_tcs) }
404 (TySynonym {tcdLName = L _ tc_name, tcdTyVars = tvs, tcdSynRhs = rhs_ty})
405 = tcTyVarBndrs tvs $ \ tvs' -> do
406 { traceTc (text "tcd1" <+> ppr tc_name)
407 ; rhs_ty' <- tcHsKindedType rhs_ty
408 ; return (ATyCon (buildSynTyCon tc_name tvs' rhs_ty')) }
411 tcTyClDecl :: (Name -> RecFlag) -> TyClDecl Name -> TcM TyThing
413 tcTyClDecl calc_isrec decl
414 = tcAddDeclCtxt decl (tcTyClDecl1 calc_isrec decl)
416 tcTyClDecl1 calc_isrec
417 (TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdTyVars = tvs,
418 tcdLName = L _ tc_name, tcdKindSig = mb_ksig, tcdCons = cons})
419 = tcTyVarBndrs tvs $ \ tvs' -> do
420 { extra_tvs <- tcDataKindSig mb_ksig
421 ; let final_tvs = tvs' ++ extra_tvs
422 ; stupid_theta <- tcHsKindedContext ctxt
423 ; want_generic <- doptM Opt_Generics
424 ; unbox_strict <- doptM Opt_UnboxStrictFields
425 ; gla_exts <- doptM Opt_GlasgowExts
426 ; is_boot <- tcIsHsBoot -- Are we compiling an hs-boot file?
428 -- Check that we don't use GADT syntax in H98 world
429 ; checkTc (gla_exts || h98_syntax) (badGadtDecl tc_name)
431 -- Check that the stupid theta is empty for a GADT-style declaration
432 ; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
434 -- Check that there's at least one condecl,
435 -- or else we're reading an hs-boot file, or -fglasgow-exts
436 ; checkTc (not (null cons) || gla_exts || is_boot)
437 (emptyConDeclsErr tc_name)
439 -- Check that a newtype has exactly one constructor
440 ; checkTc (new_or_data == DataType || isSingleton cons)
441 (newtypeConError tc_name (length cons))
443 ; tycon <- fixM (\ tycon -> do
444 { data_cons <- mappM (addLocM (tcConDecl unbox_strict new_or_data
448 if null cons && is_boot -- In a hs-boot file, empty cons means
449 then return AbstractTyCon -- "don't know"; hence Abstract
450 else case new_or_data of
451 DataType -> return (mkDataTyConRhs data_cons)
453 ASSERT( isSingleton data_cons )
454 mkNewTyConRhs tc_name tycon (head data_cons)
455 ; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs is_rec
456 (want_generic && canDoGenerics data_cons) h98_syntax
458 ; return (ATyCon tycon)
461 is_rec = calc_isrec tc_name
462 h98_syntax = case cons of -- All constructors have same shape
463 L _ (ConDecl { con_res = ResTyGADT _ }) : _ -> False
466 tcTyClDecl1 calc_isrec
467 (ClassDecl {tcdLName = L _ class_name, tcdTyVars = tvs,
468 tcdCtxt = ctxt, tcdMeths = meths,
469 tcdFDs = fundeps, tcdSigs = sigs, tcdATs = ats} )
470 = tcTyVarBndrs tvs $ \ tvs' -> do
471 { ctxt' <- tcHsKindedContext ctxt
472 ; fds' <- mappM (addLocM tc_fundep) fundeps
473 -- !!!TODO: process `ats`; what do we want to store in the `Class'? -=chak
474 ; sig_stuff <- tcClassSigs class_name sigs meths
475 ; clas <- fixM (\ clas ->
476 let -- This little knot is just so we can get
477 -- hold of the name of the class TyCon, which we
478 -- need to look up its recursiveness and variance
479 tycon_name = tyConName (classTyCon clas)
480 tc_isrec = calc_isrec tycon_name
482 buildClass class_name tvs' ctxt' fds'
484 ; return (AClass clas) }
486 tc_fundep (tvs1, tvs2) = do { tvs1' <- mappM tcLookupTyVar tvs1 ;
487 ; tvs2' <- mappM tcLookupTyVar tvs2 ;
488 ; return (tvs1', tvs2') }
491 tcTyClDecl1 calc_isrec
492 (ForeignType {tcdLName = L _ tc_name, tcdExtName = tc_ext_name})
493 = returnM (ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0))
495 -----------------------------------
496 tcConDecl :: Bool -- True <=> -funbox-strict_fields
497 -> NewOrData -> TyCon -> [TyVar]
498 -> ConDecl Name -> TcM DataCon
500 tcConDecl unbox_strict NewType tycon tc_tvs -- Newtypes
501 (ConDecl name _ ex_tvs ex_ctxt details ResTyH98)
502 = do { let tc_datacon field_lbls arg_ty
503 = do { arg_ty' <- tcHsKindedType arg_ty -- No bang on newtype
504 ; buildDataCon (unLoc name) False {- Prefix -}
506 (map unLoc field_lbls)
507 tc_tvs [] -- No existentials
508 [] [] -- No equalities, predicates
512 -- Check that a newtype has no existential stuff
513 ; checkTc (null ex_tvs && null (unLoc ex_ctxt)) (newtypeExError name)
516 PrefixCon [arg_ty] -> tc_datacon [] arg_ty
517 RecCon [(field_lbl, arg_ty)] -> tc_datacon [field_lbl] arg_ty
518 other -> failWithTc (newtypeFieldErr name (length (hsConArgs details)))
519 -- Check that the constructor has exactly one field
522 tcConDecl unbox_strict DataType tycon tc_tvs -- Data types
523 (ConDecl name _ tvs ctxt details res_ty)
524 = tcTyVarBndrs tvs $ \ tvs' -> do
525 { ctxt' <- tcHsKindedContext ctxt
526 ; (univ_tvs, ex_tvs, eq_preds, data_tc) <- tcResultType tycon tc_tvs tvs' res_ty
528 tc_datacon is_infix field_lbls btys
529 = do { let bangs = map getBangStrictness btys
530 ; arg_tys <- mappM tcHsBangType btys
531 ; buildDataCon (unLoc name) is_infix
532 (argStrictness unbox_strict tycon bangs arg_tys)
533 (map unLoc field_lbls)
534 univ_tvs ex_tvs eq_preds ctxt' arg_tys
536 -- NB: we put data_tc, the type constructor gotten from the constructor
537 -- type signature into the data constructor; that way
538 -- checkValidDataCon can complain if it's wrong.
541 PrefixCon btys -> tc_datacon False [] btys
542 InfixCon bty1 bty2 -> tc_datacon True [] [bty1,bty2]
543 RecCon fields -> tc_datacon False field_names btys
545 (field_names, btys) = unzip fields
549 tcResultType :: TyCon
550 -> [TyVar] -- data T a b c = ...
551 -> [TyVar] -- where MkT :: forall a b c. ...
553 -> TcM ([TyVar], -- Universal
554 [TyVar], -- Existential
555 [(TyVar,Type)], -- Equality predicates
556 TyCon) -- TyCon given in the ResTy
557 -- We don't check that the TyCon given in the ResTy is
558 -- the same as the parent tycon, becuase we are in the middle
559 -- of a recursive knot; so it's postponed until checkValidDataCon
561 tcResultType decl_tycon tc_tvs dc_tvs ResTyH98
562 = return (tc_tvs, dc_tvs, [], decl_tycon)
563 -- In H98 syntax the dc_tvs are the existential ones
564 -- data T a b c = forall d e. MkT ...
565 -- The {a,b,c} are tc_tvs, and {d,e} are dc_tvs
567 tcResultType _ tc_tvs dc_tvs (ResTyGADT res_ty)
568 -- E.g. data T a b c where
569 -- MkT :: forall x y z. T (x,y) z z
571 -- ([a,z,c], [x,y], [a:=:(x,y), c:=:z], T)
573 = do { (dc_tycon, res_tys) <- tcLHsConResTy res_ty
574 -- NB: tc_tvs and dc_tvs are distinct
575 ; let univ_tvs = choose_univs [] tc_tvs res_tys
576 -- Each univ_tv is either a dc_tv or a tc_tv
577 ex_tvs = dc_tvs `minusList` univ_tvs
578 eq_spec = [ (tv, ty) | (tv,ty) <- univ_tvs `zip` res_tys,
580 ; return (univ_tvs, ex_tvs, eq_spec, dc_tycon) }
582 -- choose_univs uses the res_ty itself if it's a type variable
583 -- and hasn't already been used; otherwise it uses one of the tc_tvs
584 choose_univs used tc_tvs []
585 = ASSERT( null tc_tvs ) []
586 choose_univs used (tc_tv:tc_tvs) (res_ty:res_tys)
587 | Just tv <- tcGetTyVar_maybe res_ty, not (tv `elem` used)
588 = tv : choose_univs (tv:used) tc_tvs res_tys
590 = tc_tv : choose_univs used tc_tvs res_tys
593 argStrictness :: Bool -- True <=> -funbox-strict_fields
595 -> [TcType] -> [StrictnessMark]
596 argStrictness unbox_strict tycon bangs arg_tys
597 = ASSERT( length bangs == length arg_tys )
598 zipWith (chooseBoxingStrategy unbox_strict tycon) arg_tys bangs
600 -- We attempt to unbox/unpack a strict field when either:
601 -- (i) The field is marked '!!', or
602 -- (ii) The field is marked '!', and the -funbox-strict-fields flag is on.
604 -- We have turned off unboxing of newtypes because coercions make unboxing
605 -- and reboxing more complicated
606 chooseBoxingStrategy :: Bool -> TyCon -> TcType -> HsBang -> StrictnessMark
607 chooseBoxingStrategy unbox_strict_fields tycon arg_ty bang
609 HsNoBang -> NotMarkedStrict
610 HsStrict | unbox_strict_fields
611 && can_unbox arg_ty -> MarkedUnboxed
612 HsUnbox | can_unbox arg_ty -> MarkedUnboxed
613 other -> MarkedStrict
615 -- we can unbox if the type is a chain of newtypes with a product tycon
617 can_unbox arg_ty = case splitTyConApp_maybe arg_ty of
619 Just (arg_tycon, tycon_args) ->
620 not (isRecursiveTyCon tycon) &&
621 isProductTyCon arg_tycon &&
622 (if isNewTyCon arg_tycon then
623 can_unbox (newTyConInstRhs arg_tycon tycon_args)
627 %************************************************************************
629 \subsection{Dependency analysis}
631 %************************************************************************
633 Validity checking is done once the mutually-recursive knot has been
634 tied, so we can look at things freely.
637 checkCycleErrs :: [LTyClDecl Name] -> TcM ()
638 checkCycleErrs tyclss
642 = do { mappM_ recClsErr cls_cycles
643 ; failM } -- Give up now, because later checkValidTyCl
644 -- will loop if the synonym is recursive
646 cls_cycles = calcClassCycles tyclss
648 checkValidTyCl :: TyClDecl Name -> TcM ()
649 -- We do the validity check over declarations, rather than TyThings
650 -- only so that we can add a nice context with tcAddDeclCtxt
652 = tcAddDeclCtxt decl $
653 do { thing <- tcLookupLocatedGlobal (tcdLName decl)
654 ; traceTc (text "Validity of" <+> ppr thing)
656 ATyCon tc -> checkValidTyCon tc
657 AClass cl -> checkValidClass cl
658 ; traceTc (text "Done validity of" <+> ppr thing)
661 -------------------------
662 -- For data types declared with record syntax, we require
663 -- that each constructor that has a field 'f'
664 -- (a) has the same result type
665 -- (b) has the same type for 'f'
666 -- module alpha conversion of the quantified type variables
667 -- of the constructor.
669 checkValidTyCon :: TyCon -> TcM ()
672 = checkValidType syn_ctxt syn_rhs
674 = -- Check the context on the data decl
675 checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc) `thenM_`
677 -- Check arg types of data constructors
678 mappM_ (checkValidDataCon tc) data_cons `thenM_`
680 -- Check that fields with the same name share a type
681 mappM_ check_fields groups
684 syn_ctxt = TySynCtxt name
686 syn_rhs = synTyConRhs tc
687 data_cons = tyConDataCons tc
689 groups = equivClasses cmp_fld (concatMap get_fields data_cons)
690 cmp_fld (f1,_) (f2,_) = f1 `compare` f2
691 get_fields con = dataConFieldLabels con `zip` repeat con
692 -- dataConFieldLabels may return the empty list, which is fine
694 -- See Note [GADT record selectors] in MkId.lhs
695 -- We must check (a) that the named field has the same
696 -- type in each constructor
697 -- (b) that those constructors have the same result type
699 -- However, the constructors may have differently named type variable
700 -- and (worse) we don't know how the correspond to each other. E.g.
701 -- C1 :: forall a b. { f :: a, g :: b } -> T a b
702 -- C2 :: forall d c. { f :: c, g :: c } -> T c d
704 -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
705 -- result type against other candidates' types BOTH WAYS ROUND.
706 -- If they magically agrees, take the substitution and
707 -- apply them to the latter ones, and see if they match perfectly.
708 check_fields fields@((label, con1) : other_fields)
709 -- These fields all have the same name, but are from
710 -- different constructors in the data type
711 = recoverM (return ()) $ mapM_ checkOne other_fields
712 -- Check that all the fields in the group have the same type
713 -- NB: this check assumes that all the constructors of a given
714 -- data type use the same type variables
716 tvs1 = mkVarSet (dataConAllTyVars con1)
717 res1 = dataConResTys con1
718 fty1 = dataConFieldType con1 label
720 checkOne (_, con2) -- Do it bothways to ensure they are structurally identical
721 = do { checkFieldCompat label con1 con2 tvs1 res1 res2 fty1 fty2
722 ; checkFieldCompat label con2 con1 tvs2 res2 res1 fty2 fty1 }
724 tvs2 = mkVarSet (dataConAllTyVars con2)
725 res2 = dataConResTys con2
726 fty2 = dataConFieldType con2 label
728 checkFieldCompat fld con1 con2 tvs1 res1 res2 fty1 fty2
729 = do { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
730 ; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
732 mb_subst1 = tcMatchTys tvs1 res1 res2
733 mb_subst2 = tcMatchTyX tvs1 (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
735 -------------------------------
736 checkValidDataCon :: TyCon -> DataCon -> TcM ()
737 checkValidDataCon tc con
738 = setSrcSpan (srcLocSpan (getSrcLoc con)) $
739 addErrCtxt (dataConCtxt con) $
740 do { checkTc (dataConTyCon con == tc) (badDataConTyCon con)
741 ; checkValidType ctxt (dataConUserType con) }
743 ctxt = ConArgCtxt (dataConName con)
745 -------------------------------
746 checkValidClass :: Class -> TcM ()
748 = do { -- CHECK ARITY 1 FOR HASKELL 1.4
749 gla_exts <- doptM Opt_GlasgowExts
751 -- Check that the class is unary, unless GlaExs
752 ; checkTc (notNull tyvars) (nullaryClassErr cls)
753 ; checkTc (gla_exts || unary) (classArityErr cls)
755 -- Check the super-classes
756 ; checkValidTheta (ClassSCCtxt (className cls)) theta
758 -- Check the class operations
759 ; mappM_ (check_op gla_exts) op_stuff
761 -- Check that if the class has generic methods, then the
762 -- class has only one parameter. We can't do generic
763 -- multi-parameter type classes!
764 ; checkTc (unary || no_generics) (genericMultiParamErr cls)
766 -- Check that the class has no associated types, unless GlaExs
767 ; checkTc (gla_exts || no_ats) (badATDecl cls)
770 (tyvars, theta, _, op_stuff) = classBigSig cls
771 unary = isSingleton tyvars
772 no_generics = null [() | (_, GenDefMeth) <- op_stuff]
773 no_ats = True -- !!!TODO: determine whether the class has ATs -=chak
775 check_op gla_exts (sel_id, dm)
776 = addErrCtxt (classOpCtxt sel_id tau) $ do
777 { checkValidTheta SigmaCtxt (tail theta)
778 -- The 'tail' removes the initial (C a) from the
779 -- class itself, leaving just the method type
781 ; checkValidType (FunSigCtxt op_name) tau
783 -- Check that the type mentions at least one of
784 -- the class type variables
785 ; checkTc (any (`elemVarSet` tyVarsOfType tau) tyvars)
786 (noClassTyVarErr cls sel_id)
788 -- Check that for a generic method, the type of
789 -- the method is sufficiently simple
790 ; checkTc (dm /= GenDefMeth || validGenericMethodType tau)
791 (badGenericMethodType op_name op_ty)
794 op_name = idName sel_id
795 op_ty = idType sel_id
796 (_,theta1,tau1) = tcSplitSigmaTy op_ty
797 (_,theta2,tau2) = tcSplitSigmaTy tau1
798 (theta,tau) | gla_exts = (theta1 ++ theta2, tau2)
799 | otherwise = (theta1, mkPhiTy (tail theta1) tau1)
800 -- Ugh! The function might have a type like
801 -- op :: forall a. C a => forall b. (Eq b, Eq a) => tau2
802 -- With -fglasgow-exts, we want to allow this, even though the inner
803 -- forall has an (Eq a) constraint. Whereas in general, each constraint
804 -- in the context of a for-all must mention at least one quantified
805 -- type variable. What a mess!
808 ---------------------------------------------------------------------
809 resultTypeMisMatch field_name con1 con2
810 = vcat [sep [ptext SLIT("Constructors") <+> ppr con1 <+> ptext SLIT("and") <+> ppr con2,
811 ptext SLIT("have a common field") <+> quotes (ppr field_name) <> comma],
812 nest 2 $ ptext SLIT("but have different result types")]
813 fieldTypeMisMatch field_name con1 con2
814 = sep [ptext SLIT("Constructors") <+> ppr con1 <+> ptext SLIT("and") <+> ppr con2,
815 ptext SLIT("give different types for field"), quotes (ppr field_name)]
817 dataConCtxt con = ptext SLIT("In the definition of data constructor") <+> quotes (ppr con)
819 classOpCtxt sel_id tau = sep [ptext SLIT("When checking the class method:"),
820 nest 2 (ppr sel_id <+> dcolon <+> ppr tau)]
823 = ptext SLIT("No parameters for class") <+> quotes (ppr cls)
826 = vcat [ptext SLIT("Too many parameters for class") <+> quotes (ppr cls),
827 parens (ptext SLIT("Use -fglasgow-exts to allow multi-parameter classes"))]
829 noClassTyVarErr clas op
830 = sep [ptext SLIT("The class method") <+> quotes (ppr op),
831 ptext SLIT("mentions none of the type variables of the class") <+>
832 ppr clas <+> hsep (map ppr (classTyVars clas))]
834 genericMultiParamErr clas
835 = ptext SLIT("The multi-parameter class") <+> quotes (ppr clas) <+>
836 ptext SLIT("cannot have generic methods")
838 badGenericMethodType op op_ty
839 = hang (ptext SLIT("Generic method type is too complex"))
840 4 (vcat [ppr op <+> dcolon <+> ppr op_ty,
841 ptext SLIT("You can only use type variables, arrows, lists, and tuples")])
844 = setSrcSpan (getLoc (head sorted_decls)) $
845 addErr (sep [ptext SLIT("Cycle in type synonym declarations:"),
846 nest 2 (vcat (map ppr_decl sorted_decls))])
848 sorted_decls = sortLocated syn_decls
849 ppr_decl (L loc decl) = ppr loc <> colon <+> ppr decl
852 = setSrcSpan (getLoc (head sorted_decls)) $
853 addErr (sep [ptext SLIT("Cycle in class declarations (via superclasses):"),
854 nest 2 (vcat (map ppr_decl sorted_decls))])
856 sorted_decls = sortLocated cls_decls
857 ppr_decl (L loc decl) = ppr loc <> colon <+> ppr (decl { tcdSigs = [] })
859 sortLocated :: [Located a] -> [Located a]
860 sortLocated things = sortLe le things
862 le (L l1 _) (L l2 _) = l1 <= l2
864 badDataConTyCon data_con
865 = hang (ptext SLIT("Data constructor") <+> quotes (ppr data_con) <+>
866 ptext SLIT("returns type") <+> quotes (ppr (dataConTyCon data_con)))
867 2 (ptext SLIT("instead of its parent type"))
870 = vcat [ ptext SLIT("Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
871 , nest 2 (parens $ ptext SLIT("Use -fglasgow-exts to allow GADTs")) ]
873 badStupidTheta tc_name
874 = ptext SLIT("A data type declared in GADT style cannot have a context:") <+> quotes (ppr tc_name)
876 newtypeConError tycon n
877 = sep [ptext SLIT("A newtype must have exactly one constructor,"),
878 nest 2 $ ptext SLIT("but") <+> quotes (ppr tycon) <+> ptext SLIT("has") <+> speakN n ]
881 = sep [ptext SLIT("A newtype constructor cannot have an existential context,"),
882 nest 2 $ ptext SLIT("but") <+> quotes (ppr con) <+> ptext SLIT("does")]
884 newtypeFieldErr con_name n_flds
885 = sep [ptext SLIT("The constructor of a newtype must have exactly one field"),
886 nest 2 $ ptext SLIT("but") <+> quotes (ppr con_name) <+> ptext SLIT("has") <+> speakN n_flds]
889 = vcat [ ptext SLIT("Illegal associated type declaration in") <+> quotes (ppr cl_name)
890 , nest 2 (parens $ ptext SLIT("Use -fglasgow-exts to allow ATs")) ]
892 emptyConDeclsErr tycon
893 = sep [quotes (ppr tycon) <+> ptext SLIT("has no constructors"),
894 nest 2 $ ptext SLIT("(-fglasgow-exts permits this)")]