Move exprIsConApp_maybe to CoreSubst so we can use it in VSO. Fix VSO bug with unlift...
[ghc.git] / compiler / typecheck / TcTyClsDecls.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The AQUA Project, Glasgow University, 1996-1998
4 %
5
6 TcTyClsDecls: Typecheck type and class declarations
7
8 \begin{code}
9 module TcTyClsDecls (
10         tcTyAndClassDecls, kcDataDecl, tcConDecls, mkRecSelBinds,
11         checkValidTyCon, dataDeclChecks
12     ) where
13
14 #include "HsVersions.h"
15
16 import HsSyn
17 import HscTypes
18 import BuildTyCl
19 import TcUnify
20 import TcRnMonad
21 import TcEnv
22 import TcTyDecls
23 import TcClassDcl
24 import TcHsType
25 import TcMType
26 import TcType
27 import TysWiredIn       ( unitTy )
28 import Type
29 import Class
30 import TyCon
31 import DataCon
32 import Id
33 import MkCore           ( rEC_SEL_ERROR_ID )
34 import IdInfo
35 import Var
36 import VarSet
37 import Name
38 import NameEnv
39 import Outputable
40 import Maybes
41 import Unify
42 import Util
43 import SrcLoc
44 import ListSetOps
45 import Digraph
46 import DynFlags
47 import FastString
48 import Unique           ( mkBuiltinUnique )
49 import BasicTypes
50
51 import Bag
52 import Control.Monad
53 import Data.List
54 \end{code}
55
56
57 %************************************************************************
58 %*                                                                      *
59 \subsection{Type checking for type and class declarations}
60 %*                                                                      *
61 %************************************************************************
62
63 \begin{code}
64
65 tcTyAndClassDecls :: ModDetails 
66                    -> [[LTyClDecl Name]]     -- Mutually-recursive groups in dependency order
67                    -> TcM (TcGblEnv,         -- Input env extended by types and classes 
68                                              -- and their implicit Ids,DataCons
69                            HsValBinds Name)  -- Renamed bindings for record selectors
70 -- Fails if there are any errors
71
72 tcTyAndClassDecls boot_details decls_s
73   = checkNoErrs $       -- The code recovers internally, but if anything gave rise to
74                         -- an error we'd better stop now, to avoid a cascade
75     do { let tyclds_s = map (filterOut (isFamInstDecl . unLoc)) decls_s
76                   -- Remove family instance decls altogether
77                   -- They are dealt with by TcInstDcls
78               
79        ; tyclss <- fixM $ \ rec_tyclss ->
80               tcExtendRecEnv (zipRecTyClss tyclds_s rec_tyclss) $
81                 -- We must populate the environment with the loop-tied
82                 -- T's right away (even before kind checking), because 
83                 -- the kind checker may "fault in" some type constructors 
84                 -- that recursively mention T
85
86               do {    -- Kind-check in dependency order
87                       -- See Note [Kind checking for type and class decls]
88                    kc_decls <- kcTyClDecls tyclds_s
89
90                       -- And now build the TyCons/Classes
91                 ; let rec_flags = calcRecFlags boot_details rec_tyclss
92                 ; concatMapM (tcTyClDecl rec_flags) kc_decls }
93
94        ; traceTc "tcTyAndCl" (ppr tyclss)
95
96        ; tcExtendGlobalEnv tyclss $ do
97        {  -- Perform the validity check
98           -- We can do this now because we are done with the recursive knot
99           traceTc "ready for validity check" empty
100         ; mapM_ (addLocM checkValidTyCl) (concat tyclds_s)
101         ; traceTc "done" empty
102
103         -- Add the implicit things;
104         -- we want them in the environment because
105         -- they may be mentioned in interface files
106         -- NB: All associated types and their implicit things will be added a
107         --     second time here.  This doesn't matter as the definitions are
108         --     the same.
109         ; let { implicit_things = concatMap implicitTyThings tyclss
110               ; rec_sel_binds   = mkRecSelBinds [tc | ATyCon tc <- tyclss]
111               ; dm_ids          = mkDefaultMethodIds tyclss }
112
113         ; env <- tcExtendGlobalEnv implicit_things $
114                  tcExtendGlobalValEnv dm_ids $
115                  getGblEnv
116         ; return (env, rec_sel_binds) } }
117                     
118 zipRecTyClss :: [[LTyClDecl Name]]
119              -> [TyThing]           -- Knot-tied
120              -> [(Name,TyThing)]
121 -- Build a name-TyThing mapping for the things bound by decls
122 -- being careful not to look at the [TyThing]
123 -- The TyThings in the result list must have a visible ATyCon,
124 -- because typechecking types (in, say, tcTyClDecl) looks at this outer constructor
125 zipRecTyClss decls_s rec_things
126   = [ get decl | decls <- decls_s, L _ decl <- flattenATs decls ]
127   where
128     rec_type_env :: TypeEnv
129     rec_type_env = mkTypeEnv rec_things
130
131     get :: TyClDecl Name -> (Name, TyThing)
132     get decl = (name, ATyCon tc)
133       where
134         name = tcdName decl
135         Just (ATyCon tc) = lookupTypeEnv rec_type_env name
136 \end{code}
137
138
139 %************************************************************************
140 %*                                                                      *
141                 Kind checking
142 %*                                                                      *
143 %************************************************************************
144
145 Note [Kind checking for type and class decls]
146 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
147 Kind checking is done thus:
148
149    1. Make up a kind variable for each parameter of the *data* type, 
150       and class, decls, and extend the kind environment (which is in
151       the TcLclEnv)
152
153    2. Dependency-analyse the type *synonyms* (which must be non-recursive),
154       and kind-check them in dependency order.  Extend the kind envt.
155
156    3. Kind check the data type and class decls
157
158 Synonyms are treated differently to data type and classes,
159 because a type synonym can be an unboxed type
160         type Foo = Int#
161 and a kind variable can't unify with UnboxedTypeKind
162 So we infer their kinds in dependency order
163
164 We need to kind check all types in the mutually recursive group
165 before we know the kind of the type variables.  For example:
166
167 class C a where
168    op :: D b => a -> b -> b
169
170 class D c where
171    bop :: (Monad c) => ...
172
173 Here, the kind of the locally-polymorphic type variable "b"
174 depends on *all the uses of class D*.  For example, the use of
175 Monad c in bop's type signature means that D must have kind Type->Type.
176
177 However type synonyms work differently.  They can have kinds which don't
178 just involve (->) and *:
179         type R = Int#           -- Kind #
180         type S a = Array# a     -- Kind * -> #
181         type T a b = (# a,b #)  -- Kind * -> * -> (# a,b #)
182 So we must infer their kinds from their right-hand sides *first* and then
183 use them, whereas for the mutually recursive data types D we bring into
184 scope kind bindings D -> k, where k is a kind variable, and do inference.
185
186 Type families
187 ~~~~~~~~~~~~~
188 This treatment of type synonyms only applies to Haskell 98-style synonyms.
189 General type functions can be recursive, and hence, appear in `alg_decls'.
190
191 The kind of a type family is solely determinded by its kind signature;
192 hence, only kind signatures participate in the construction of the initial
193 kind environment (as constructed by `getInitialKind').  In fact, we ignore
194 instances of families altogether in the following.  However, we need to
195 include the kinds of associated families into the construction of the
196 initial kind environment.  (This is handled by `allDecls').
197
198
199 \begin{code}
200 kcTyClDecls :: [[LTyClDecl Name]] -> TcM [LTyClDecl Name]
201 kcTyClDecls []                = return []
202 kcTyClDecls (decls : decls_s) = do { (tcl_env, kc_decls1) <- kcTyClDecls1 decls
203                                    ; kc_decls2 <- setLclEnv tcl_env (kcTyClDecls decls_s)
204                                    ; return (kc_decls1 ++ kc_decls2) }
205
206 kcTyClDecls1 :: [LTyClDecl Name] -> TcM (TcLclEnv, [LTyClDecl Name])
207 kcTyClDecls1 decls
208   = do  {       -- Omit instances of type families; they are handled together
209                 -- with the *heads* of class instances
210         ; let (syn_decls, alg_decls) = partition (isSynDecl . unLoc) decls
211               alg_at_decls           = flattenATs alg_decls
212
213         ; mod <- getModule
214         ; traceTc "tcTyAndCl" (ptext (sLit "module") <+> ppr mod $$ vcat (map ppr decls))
215
216           -- Kind checking; see Note [Kind checking for type and class decls]
217         ; alg_kinds <- mapM getInitialKind alg_at_decls
218         ; tcExtendKindEnv alg_kinds $  do
219
220         { (kc_syn_decls, tcl_env) <- kcSynDecls (calcSynCycles syn_decls)
221
222           -- Now check for cyclic classes
223         ; checkClassCycleErrs syn_decls alg_decls
224
225         ; setLclEnv tcl_env $  do
226         { kc_alg_decls <- mapM (wrapLocM kcTyClDecl) alg_decls
227                 
228              -- Kind checking done for this group, so zonk the kind variables
229              -- See Note [Kind checking for type and class decls]
230         ; mapM_ (zonkTcKindToKind . snd) alg_kinds
231
232         ; return (tcl_env, kc_syn_decls ++ kc_alg_decls) } } }
233
234 flattenATs :: [LTyClDecl Name] -> [LTyClDecl Name]
235 flattenATs decls = concatMap flatten decls
236   where
237     flatten decl@(L _ (ClassDecl {tcdATs = ats})) = decl : ats
238     flatten decl                                  = [decl]
239
240 getInitialKind :: LTyClDecl Name -> TcM (Name, TcKind)
241 -- Only for data type, class, and indexed type declarations
242 -- Get as much info as possible from the data, class, or indexed type decl,
243 -- so as to maximise usefulness of error messages
244 getInitialKind (L _ decl)
245   = do  { arg_kinds <- mapM (mk_arg_kind . unLoc) (tyClDeclTyVars decl)
246         ; res_kind  <- mk_res_kind decl
247         ; return (tcdName decl, mkArrowKinds arg_kinds res_kind) }
248   where
249     mk_arg_kind (UserTyVar _ _)      = newKindVar
250     mk_arg_kind (KindedTyVar _ kind) = return kind
251
252     mk_res_kind (TyFamily { tcdKind    = Just kind }) = return kind
253     mk_res_kind (TyData   { tcdKindSig = Just kind }) = return kind
254         -- On GADT-style declarations we allow a kind signature
255         --      data T :: *->* where { ... }
256     mk_res_kind (ClassDecl {}) = return constraintKind
257     mk_res_kind _              = return liftedTypeKind
258
259
260 ----------------
261 kcSynDecls :: [SCC (LTyClDecl Name)] 
262            -> TcM ([LTyClDecl Name],    -- Kind-annotated decls
263                    TcLclEnv)    -- Kind bindings
264 kcSynDecls []
265   = do { tcl_env <- getLclEnv; return ([], tcl_env) }
266 kcSynDecls (group : groups)
267   = do  { (decl,  nk)      <- kcSynDecl group
268         ; (decls, tcl_env) <- tcExtendKindEnv [nk] (kcSynDecls groups)
269         ; return (decl:decls, tcl_env) }
270                         
271 ----------------
272 kcSynDecl :: SCC (LTyClDecl Name) 
273            -> TcM (LTyClDecl Name,      -- Kind-annotated decls
274                    (Name,TcKind))       -- Kind bindings
275 kcSynDecl (AcyclicSCC (L loc decl))
276   = tcAddDeclCtxt decl  $
277     kcHsTyVars (tcdTyVars decl) (\ k_tvs ->
278     do { traceTc "kcd1" (ppr (unLoc (tcdLName decl)) <+> brackets (ppr (tcdTyVars decl)) 
279                         <+> brackets (ppr k_tvs))
280        ; (k_rhs, rhs_kind) <- kcLHsType (tcdSynRhs decl)
281        ; traceTc "kcd2" (ppr (unLoc (tcdLName decl)))
282        ; let tc_kind = foldr (mkArrowKind . hsTyVarKind . unLoc) rhs_kind k_tvs
283        ; return (L loc (decl { tcdTyVars = k_tvs, tcdSynRhs = k_rhs }),
284                  (unLoc (tcdLName decl), tc_kind)) })
285
286 kcSynDecl (CyclicSCC decls)
287   = do { recSynErr decls; failM }       -- Fail here to avoid error cascade
288                                         -- of out-of-scope tycons
289
290 ------------------------------------------------------------------------
291 kcTyClDecl :: TyClDecl Name -> TcM (TyClDecl Name)
292         -- Not used for type synonyms (see kcSynDecl)
293
294 kcTyClDecl decl@(TyData {})
295   = ASSERT( not . isFamInstDecl $ decl )   -- must not be a family instance
296     kcTyClDeclBody decl $
297       kcDataDecl decl
298
299 kcTyClDecl decl@(TyFamily {})
300   = kcFamilyDecl [] decl      -- the empty list signals a toplevel decl      
301
302 kcTyClDecl decl@(ClassDecl {tcdCtxt = ctxt, tcdSigs = sigs, tcdATs = ats})
303   = kcTyClDeclBody decl $ \ tvs' ->
304     do  { ctxt' <- kcHsContext ctxt     
305         ; ats'  <- mapM (wrapLocM (kcFamilyDecl tvs')) ats
306         ; sigs' <- mapM (wrapLocM kc_sig) sigs
307         ; return (decl {tcdTyVars = tvs', tcdCtxt = ctxt', tcdSigs = sigs',
308                         tcdATs = ats'}) }
309   where
310     kc_sig (TypeSig nm op_ty) = do { op_ty' <- kcHsLiftedSigType op_ty
311                                    ; return (TypeSig nm op_ty') }
312     kc_sig (GenericSig nm op_ty) = do { op_ty' <- kcHsLiftedSigType op_ty
313                                       ; return (GenericSig nm op_ty') }
314     kc_sig other_sig          = return other_sig
315
316 kcTyClDecl decl@(ForeignType {})
317   = return decl
318
319 kcTyClDecl (TySynonym {}) = panic "kcTyClDecl TySynonym"
320
321 kcTyClDeclBody :: TyClDecl Name
322                -> ([LHsTyVarBndr Name] -> TcM a)
323                -> TcM a
324 -- getInitialKind has made a suitably-shaped kind for the type or class
325 -- Unpack it, and attribute those kinds to the type variables
326 -- Extend the env with bindings for the tyvars, taken from
327 -- the kind of the tycon/class.  Give it to the thing inside, and 
328 -- check the result kind matches
329 kcTyClDeclBody decl thing_inside
330   = tcAddDeclCtxt decl          $
331     do  { tc_ty_thing <- tcLookupLocated (tcdLName decl)
332         ; let tc_kind    = case tc_ty_thing of
333                              AThing k -> k
334                              _ -> pprPanic "kcTyClDeclBody" (ppr tc_ty_thing)
335               (kinds, _) = splitKindFunTys tc_kind
336               hs_tvs     = tcdTyVars decl
337               kinded_tvs = ASSERT( length kinds >= length hs_tvs )
338                            zipWith add_kind hs_tvs kinds
339         ; tcExtendKindEnvTvs kinded_tvs thing_inside }
340   where
341     add_kind (L loc (UserTyVar n _))   k = L loc (UserTyVar n k)
342     add_kind (L loc (KindedTyVar n _)) k = L loc (KindedTyVar n k)
343
344 -- Kind check a data declaration, assuming that we already extended the
345 -- kind environment with the type variables of the left-hand side (these
346 -- kinded type variables are also passed as the second parameter).
347 --
348 kcDataDecl :: TyClDecl Name -> [LHsTyVarBndr Name] -> TcM (TyClDecl Name)
349 kcDataDecl decl@(TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdCons = cons})
350            tvs
351   = do  { ctxt' <- kcHsContext ctxt     
352         ; cons' <- mapM (wrapLocM kc_con_decl) cons
353         ; return (decl {tcdTyVars = tvs, tcdCtxt = ctxt', tcdCons = cons'}) }
354   where
355     -- doc comments are typechecked to Nothing here
356     kc_con_decl con_decl@(ConDecl { con_name = name, con_qvars = ex_tvs
357                                   , con_cxt = ex_ctxt, con_details = details, con_res = res })
358       = addErrCtxt (dataConCtxt name)   $ 
359         kcHsTyVars ex_tvs $ \ex_tvs' -> do
360         do { ex_ctxt' <- kcHsContext ex_ctxt
361            ; details' <- kc_con_details details 
362            ; res'     <- case res of
363                 ResTyH98 -> return ResTyH98
364                 ResTyGADT ty -> do { ty' <- kcHsSigType ty; return (ResTyGADT ty') }
365            ; return (con_decl { con_qvars = ex_tvs', con_cxt = ex_ctxt'
366                               , con_details = details', con_res = res' }) }
367
368     kc_con_details (PrefixCon btys) 
369         = do { btys' <- mapM kc_larg_ty btys 
370              ; return (PrefixCon btys') }
371     kc_con_details (InfixCon bty1 bty2) 
372         = do { bty1' <- kc_larg_ty bty1
373              ; bty2' <- kc_larg_ty bty2
374              ; return (InfixCon bty1' bty2') }
375     kc_con_details (RecCon fields) 
376         = do { fields' <- mapM kc_field fields
377              ; return (RecCon fields') }
378
379     kc_field (ConDeclField fld bty d) = do { bty' <- kc_larg_ty bty
380                                            ; return (ConDeclField fld bty' d) }
381
382     kc_larg_ty bty = case new_or_data of
383                         DataType -> kcHsSigType bty
384                         NewType  -> kcHsLiftedSigType bty
385         -- Can't allow an unlifted type for newtypes, because we're effectively
386         -- going to remove the constructor while coercing it to a lifted type.
387         -- And newtypes can't be bang'd
388 kcDataDecl d _ = pprPanic "kcDataDecl" (ppr d)
389
390 -- Kind check a family declaration or type family default declaration.
391 --
392 kcFamilyDecl :: [LHsTyVarBndr Name]  -- tyvars of enclosing class decl if any
393              -> TyClDecl Name -> TcM (TyClDecl Name)
394 kcFamilyDecl classTvs decl@(TyFamily {tcdKind = kind})
395   = kcTyClDeclBody decl $ \tvs' ->
396     do { mapM_ unifyClassParmKinds tvs'
397        ; return (decl {tcdTyVars = tvs', 
398                        tcdKind = kind `mplus` Just liftedTypeKind})
399                        -- default result kind is '*'
400        }
401   where
402     unifyClassParmKinds (L _ tv) 
403       | (n,k) <- hsTyVarNameKind tv
404       , Just classParmKind <- lookup n classTyKinds 
405       = unifyKind k classParmKind
406       | otherwise = return ()
407     classTyKinds = [hsTyVarNameKind tv | L _ tv <- classTvs]
408
409 kcFamilyDecl _ (TySynonym {})              -- type family defaults
410   = panic "TcTyClsDecls.kcFamilyDecl: not implemented yet"
411 kcFamilyDecl _ d = pprPanic "kcFamilyDecl" (ppr d)
412 \end{code}
413
414
415 %************************************************************************
416 %*                                                                      *
417 \subsection{Type checking}
418 %*                                                                      *
419 %************************************************************************
420
421 \begin{code}
422 tcTyClDecl :: (Name -> RecFlag) -> LTyClDecl Name -> TcM [TyThing]
423
424 tcTyClDecl calc_isrec (L loc decl)
425   = setSrcSpan loc $ tcAddDeclCtxt decl $
426     traceTc "tcTyAndCl-x" (ppr decl) >>
427     tcTyClDecl1 NoParentTyCon calc_isrec decl
428
429   -- "type family" declarations
430 tcTyClDecl1 :: TyConParent -> (Name -> RecFlag) -> TyClDecl Name -> TcM [TyThing]
431 tcTyClDecl1 parent _calc_isrec 
432   (TyFamily {tcdFlavour = TypeFamily, 
433              tcdLName = L _ tc_name, tcdTyVars = tvs,
434              tcdKind = Just kind}) -- NB: kind at latest added during kind checking
435   = tcTyVarBndrs tvs  $ \ tvs' -> do 
436   { traceTc "type family:" (ppr tc_name) 
437   ; checkFamFlag tc_name
438   ; tycon <- buildSynTyCon tc_name tvs' SynFamilyTyCon kind parent Nothing
439   ; return [ATyCon tycon]
440   }
441
442   -- "data family" declaration
443 tcTyClDecl1 parent _calc_isrec 
444   (TyFamily {tcdFlavour = DataFamily, 
445              tcdLName = L _ tc_name, tcdTyVars = tvs, tcdKind = mb_kind})
446   = tcTyVarBndrs tvs  $ \ tvs' -> do 
447   { traceTc "data family:" (ppr tc_name) 
448   ; checkFamFlag tc_name
449   ; extra_tvs <- tcDataKindSig mb_kind
450   ; let final_tvs = tvs' ++ extra_tvs    -- we may not need these
451   ; tycon <- buildAlgTyCon tc_name final_tvs [] 
452                DataFamilyTyCon Recursive True 
453                parent Nothing
454   ; return [ATyCon tycon]
455   }
456
457   -- "type" synonym declaration
458 tcTyClDecl1 _parent _calc_isrec
459   (TySynonym {tcdLName = L _ tc_name, tcdTyVars = tvs, tcdSynRhs = rhs_ty})
460   = ASSERT( isNoParent _parent )
461     tcTyVarBndrs tvs            $ \ tvs' -> do 
462     { traceTc "tcd1" (ppr tc_name) 
463     ; rhs_ty' <- tcHsKindedType rhs_ty
464     ; tycon <- buildSynTyCon tc_name tvs' (SynonymTyCon rhs_ty') 
465                              (typeKind rhs_ty') NoParentTyCon  Nothing
466     ; return [ATyCon tycon] }
467
468   -- "newtype" and "data"
469   -- NB: not used for newtype/data instances (whether associated or not)
470 tcTyClDecl1 _parent calc_isrec
471   (TyData {tcdND = new_or_data, tcdCtxt = ctxt, tcdTyVars = tvs,
472            tcdLName = L _ tc_name, tcdKindSig = mb_ksig, tcdCons = cons})
473   = ASSERT( isNoParent _parent )
474     tcTyVarBndrs tvs    $ \ tvs' -> do 
475   { extra_tvs <- tcDataKindSig mb_ksig
476   ; let final_tvs = tvs' ++ extra_tvs
477   ; stupid_theta <- tcHsKindedContext ctxt
478   ; kind_signatures <- xoptM Opt_KindSignatures
479   ; existential_ok <- xoptM Opt_ExistentialQuantification
480   ; gadt_ok      <- xoptM Opt_GADTs
481   ; is_boot      <- tcIsHsBoot  -- Are we compiling an hs-boot file?
482   ; let ex_ok = existential_ok || gadt_ok       -- Data cons can have existential context
483
484         -- Check that we don't use kind signatures without Glasgow extensions
485   ; checkTc (kind_signatures || isNothing mb_ksig) (badSigTyDecl tc_name)
486
487   ; dataDeclChecks tc_name new_or_data stupid_theta cons
488
489   ; tycon <- fixM (\ tycon -> do 
490         { let res_ty = mkTyConApp tycon (mkTyVarTys final_tvs)
491         ; data_cons <- tcConDecls ex_ok tycon (final_tvs, res_ty) cons
492         ; tc_rhs <-
493             if null cons && is_boot           -- In a hs-boot file, empty cons means
494             then return totallyAbstractTyConRhs  -- "don't know"; hence totally Abstract
495             else case new_or_data of
496                    DataType -> return (mkDataTyConRhs data_cons)
497                    NewType  -> ASSERT( not (null data_cons) )
498                                mkNewTyConRhs tc_name tycon (head data_cons)
499         ; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs is_rec
500             (not h98_syntax) NoParentTyCon Nothing
501         })
502   ; return [ATyCon tycon]
503   }
504   where
505     is_rec   = calc_isrec tc_name
506     h98_syntax = consUseH98Syntax cons
507
508 tcTyClDecl1 _parent calc_isrec 
509   (ClassDecl {tcdLName = L _ class_tycon_name, tcdTyVars = tvs, 
510               tcdCtxt = ctxt, tcdMeths = meths,
511               tcdFDs = fundeps, tcdSigs = sigs, tcdATs = ats} )
512   = ASSERT( isNoParent _parent )
513     tcTyVarBndrs tvs            $ \ tvs' -> do 
514   { ctxt' <- tcHsKindedContext ctxt
515   ; fds' <- mapM (addLocM tc_fundep) fundeps
516   ; (sig_stuff, gen_dm_env) <- tcClassSigs class_tycon_name sigs meths
517   ; clas <- fixM $ \ clas -> do
518             { let tc_isrec = calc_isrec class_tycon_name
519             ; atss' <- mapM (addLocM $ tcTyClDecl1 (AssocFamilyTyCon clas) (const Recursive)) ats
520             -- NB: 'ats' only contains "type family" and "data family"
521             --     declarations as well as type family defaults
522             ; buildClass False {- Must include unfoldings for selectors -}
523                          class_tycon_name tvs' ctxt' fds' (concat atss')
524                          sig_stuff tc_isrec }
525
526   ; let gen_dm_ids = [ AnId (mkExportedLocalId gen_dm_name gen_dm_ty)
527                      | (sel_id, GenDefMeth gen_dm_name) <- classOpItems clas
528                      , let gen_dm_tau = expectJust "tcTyClDecl1" $
529                                         lookupNameEnv gen_dm_env (idName sel_id)
530                      , let gen_dm_ty = mkSigmaTy tvs' 
531                                                  [mkClassPred clas (mkTyVarTys tvs')] 
532                                                  gen_dm_tau
533                      ]
534         class_ats = map ATyCon (classATs clas)
535
536   ; return (ATyCon (classTyCon clas) : gen_dm_ids ++ class_ats )
537       -- NB: Order is important due to the call to `mkGlobalThings' when
538       --     tying the the type and class declaration type checking knot.
539   }
540   where
541     tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tcLookupTyVar tvs1 ;
542                                 ; tvs2' <- mapM tcLookupTyVar tvs2 ;
543                                 ; return (tvs1', tvs2') }
544
545 tcTyClDecl1 _ _
546   (ForeignType {tcdLName = L _ tc_name, tcdExtName = tc_ext_name})
547   = return [ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0)]
548
549 tcTyClDecl1 _ _ d = pprPanic "tcTyClDecl1" (ppr d)
550
551 dataDeclChecks :: Name -> NewOrData -> ThetaType -> [LConDecl Name] -> TcM ()
552 dataDeclChecks tc_name new_or_data stupid_theta cons
553   = do {   -- Check that we don't use GADT syntax in H98 world
554          gadtSyntax_ok <- xoptM Opt_GADTSyntax
555        ; let h98_syntax = consUseH98Syntax cons
556        ; checkTc (gadtSyntax_ok || h98_syntax) (badGadtDecl tc_name)
557
558            -- Check that the stupid theta is empty for a GADT-style declaration
559        ; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
560
561         -- Check that a newtype has exactly one constructor
562         -- Do this before checking for empty data decls, so that
563         -- we don't suggest -XEmptyDataDecls for newtypes
564       ; checkTc (new_or_data == DataType || isSingleton cons) 
565                 (newtypeConError tc_name (length cons))
566
567         -- Check that there's at least one condecl,
568         -- or else we're reading an hs-boot file, or -XEmptyDataDecls
569       ; empty_data_decls <- xoptM Opt_EmptyDataDecls
570       ; is_boot <- tcIsHsBoot   -- Are we compiling an hs-boot file?
571       ; checkTc (not (null cons) || empty_data_decls || is_boot)
572                 (emptyConDeclsErr tc_name) }
573     
574 -----------------------------------
575 tcConDecls :: Bool -> TyCon -> ([TyVar], Type)
576            -> [LConDecl Name] -> TcM [DataCon]
577 tcConDecls ex_ok rep_tycon res_tmpl cons
578   = mapM (addLocM (tcConDecl ex_ok rep_tycon res_tmpl)) cons
579
580 tcConDecl :: Bool               -- True <=> -XExistentialQuantificaton or -XGADTs
581           -> TyCon              -- Representation tycon
582           -> ([TyVar], Type)    -- Return type template (with its template tyvars)
583           -> ConDecl Name 
584           -> TcM DataCon
585
586 tcConDecl existential_ok rep_tycon res_tmpl     -- Data types
587           con@(ConDecl {con_name = name, con_qvars = tvs, con_cxt = ctxt
588                    , con_details = details, con_res = res_ty })
589   = addErrCtxt (dataConCtxt name)       $ 
590     tcTyVarBndrs tvs                    $ \ tvs' -> do 
591     { ctxt' <- tcHsKindedContext ctxt
592     ; checkTc (existential_ok || conRepresentibleWithH98Syntax con)
593               (badExistential name)
594     ; (univ_tvs, ex_tvs, eq_preds, res_ty') <- tcResultType res_tmpl tvs' res_ty
595     ; let 
596         tc_datacon is_infix field_lbls btys
597           = do { (arg_tys, stricts) <- mapAndUnzipM tcConArg btys
598                ; buildDataCon (unLoc name) is_infix
599                     stricts field_lbls
600                     univ_tvs ex_tvs eq_preds ctxt' arg_tys
601                     res_ty' rep_tycon }
602                 -- NB:  we put data_tc, the type constructor gotten from the
603                 --      constructor type signature into the data constructor;
604                 --      that way checkValidDataCon can complain if it's wrong.
605
606     ; case details of
607         PrefixCon btys     -> tc_datacon False [] btys
608         InfixCon bty1 bty2 -> tc_datacon True  [] [bty1,bty2]
609         RecCon fields      -> tc_datacon False field_names btys
610                            where
611                               field_names = map (unLoc . cd_fld_name) fields
612                               btys        = map cd_fld_type fields
613     }
614
615 -- Example
616 --   data instance T (b,c) where 
617 --      TI :: forall e. e -> T (e,e)
618 --
619 -- The representation tycon looks like this:
620 --   data :R7T b c where 
621 --      TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
622 -- In this case orig_res_ty = T (e,e)
623
624 tcResultType :: ([TyVar], Type) -- Template for result type; e.g.
625                                 -- data instance T [a] b c = ...  
626                                 --      gives template ([a,b,c], T [a] b c)
627              -> [TyVar]         -- where MkT :: forall x y z. ...
628              -> ResType Name
629              -> TcM ([TyVar],           -- Universal
630                      [TyVar],           -- Existential (distinct OccNames from univs)
631                      [(TyVar,Type)],    -- Equality predicates
632                      Type)              -- Typechecked return type
633         -- We don't check that the TyCon given in the ResTy is
634         -- the same as the parent tycon, becuase we are in the middle
635         -- of a recursive knot; so it's postponed until checkValidDataCon
636
637 tcResultType (tmpl_tvs, res_ty) dc_tvs ResTyH98
638   = return (tmpl_tvs, dc_tvs, [], res_ty)
639         -- In H98 syntax the dc_tvs are the existential ones
640         --      data T a b c = forall d e. MkT ...
641         -- The {a,b,c} are tc_tvs, and {d,e} are dc_tvs
642
643 tcResultType (tmpl_tvs, res_tmpl) dc_tvs (ResTyGADT res_ty)
644         -- E.g.  data T [a] b c where
645         --         MkT :: forall x y z. T [(x,y)] z z
646         -- Then we generate
647         --      Univ tyvars     Eq-spec
648         --          a              a~(x,y)
649         --          b              b~z
650         --          z              
651         -- Existentials are the leftover type vars: [x,y]
652         -- So we return ([a,b,z], [x,y], [a~(x,y),b~z], T [(x,y)] z z)
653   = do  { res_ty' <- tcHsKindedType res_ty
654         ; let Just subst = tcMatchTy (mkVarSet tmpl_tvs) res_tmpl res_ty'
655
656                 -- /Lazily/ figure out the univ_tvs etc
657                 -- Each univ_tv is either a dc_tv or a tmpl_tv
658               (univ_tvs, eq_spec) = foldr choose ([], []) tidy_tmpl_tvs
659               choose tmpl (univs, eqs)
660                 | Just ty <- lookupTyVar subst tmpl 
661                 = case tcGetTyVar_maybe ty of
662                     Just tv | not (tv `elem` univs)
663                             -> (tv:univs,   eqs)
664                     _other  -> (tmpl:univs, (tmpl,ty):eqs)
665                 | otherwise = pprPanic "tcResultType" (ppr res_ty)
666               ex_tvs = dc_tvs `minusList` univ_tvs
667
668         ; return (univ_tvs, ex_tvs, eq_spec, res_ty') }
669   where
670         -- NB: tmpl_tvs and dc_tvs are distinct, but
671         -- we want them to be *visibly* distinct, both for
672         -- interface files and general confusion.  So rename
673         -- the tc_tvs, since they are not used yet (no 
674         -- consequential renaming needed)
675     (_, tidy_tmpl_tvs) = mapAccumL tidy_one init_occ_env tmpl_tvs
676     init_occ_env       = initTidyOccEnv (map getOccName dc_tvs)
677     tidy_one env tv    = (env', setTyVarName tv (tidyNameOcc name occ'))
678               where
679                  name = tyVarName tv
680                  (env', occ') = tidyOccName env (getOccName name) 
681
682 consUseH98Syntax :: [LConDecl a] -> Bool
683 consUseH98Syntax (L _ (ConDecl { con_res = ResTyGADT _ }) : _) = False
684 consUseH98Syntax _                                             = True
685                  -- All constructors have same shape
686
687 conRepresentibleWithH98Syntax :: ConDecl Name -> Bool
688 conRepresentibleWithH98Syntax
689     (ConDecl {con_qvars = tvs, con_cxt = ctxt, con_res = ResTyH98 })
690         = null tvs && null (unLoc ctxt)
691 conRepresentibleWithH98Syntax
692     (ConDecl {con_qvars = tvs, con_cxt = ctxt, con_res = ResTyGADT (L _ t) })
693         = null (unLoc ctxt) && f t (map (hsTyVarName . unLoc) tvs)
694     where -- Each type variable should be used exactly once in the
695           -- result type, and the result type must just be the type
696           -- constructor applied to type variables
697           f (HsAppTy (L _ t1) (L _ (HsTyVar v2))) vs
698               = (v2 `elem` vs) && f t1 (delete v2 vs)
699           f (HsTyVar _) [] = True
700           f _ _ = False
701
702 -------------------
703 tcConArg :: LHsType Name -> TcM (TcType, HsBang)
704 tcConArg bty
705   = do  { arg_ty <- tcHsBangType bty
706         ; strict_mark <- chooseBoxingStrategy arg_ty (getBangStrictness bty)
707         ; return (arg_ty, strict_mark) }
708
709 -- We attempt to unbox/unpack a strict field when either:
710 --   (i)  The field is marked '!!', or
711 --   (ii) The field is marked '!', and the -funbox-strict-fields flag is on.
712 --
713 -- We have turned off unboxing of newtypes because coercions make unboxing 
714 -- and reboxing more complicated
715 chooseBoxingStrategy :: TcType -> HsBang -> TcM HsBang
716 chooseBoxingStrategy arg_ty bang
717   = case bang of
718         HsNoBang -> return HsNoBang
719         HsStrict -> do { unbox_strict <- doptM Opt_UnboxStrictFields
720                        ; if unbox_strict then return (can_unbox HsStrict arg_ty)
721                                          else return HsStrict }
722         HsUnpack -> do { omit_prags <- doptM Opt_OmitInterfacePragmas
723             -- Do not respect UNPACK pragmas if OmitInterfacePragmas is on
724             -- See Trac #5252: unpacking means we must not conceal the
725             --                 representation of the argument type
726                        ; if omit_prags then return HsStrict
727                                        else return (can_unbox HsUnpackFailed arg_ty) }
728         HsUnpackFailed -> pprPanic "chooseBoxingStrategy" (ppr arg_ty)
729                           -- Source code never has shtes
730   where
731     can_unbox :: HsBang -> TcType -> HsBang
732     -- Returns   HsUnpack  if we can unpack arg_ty
733     --           fail_bang if we know what arg_ty is but we can't unpack it
734     --           HsStrict  if it's abstract, so we don't know whether or not we can unbox it
735     can_unbox fail_bang arg_ty 
736        = case splitTyConApp_maybe arg_ty of
737             Nothing -> fail_bang
738
739             Just (arg_tycon, tycon_args) 
740               | isAbstractTyCon arg_tycon -> HsStrict   
741                       -- See Note [Don't complain about UNPACK on abstract TyCons]
742               | not (isRecursiveTyCon arg_tycon)        -- Note [Recusive unboxing]
743               , isProductTyCon arg_tycon 
744                     -- We can unbox if the type is a chain of newtypes 
745                     -- with a product tycon at the end
746               -> if isNewTyCon arg_tycon 
747                  then can_unbox fail_bang (newTyConInstRhs arg_tycon tycon_args)
748                  else HsUnpack
749
750               | otherwise -> fail_bang
751 \end{code}
752
753 Note [Don't complain about UNPACK on abstract TyCons]
754 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
755 We are going to complain about UnpackFailed, but if we say
756    data T = MkT {-# UNPACK #-} !Wobble
757 and Wobble is a newtype imported from a module that was compiled 
758 without optimisation, we don't want to complain. Because it might
759 be fine when optimsation is on.  I think this happens when Haddock
760 is working over (say) GHC souce files.
761
762 Note [Recursive unboxing]
763 ~~~~~~~~~~~~~~~~~~~~~~~~~
764 Be careful not to try to unbox this!
765         data T = MkT {-# UNPACK #-} !T Int
766 Reason: consider
767   data R = MkR {-# UNPACK #-} !S Int
768   data S = MkS {-# UNPACK #-} !Int
769 The representation arguments of MkR are the *representation* arguments
770 of S (plus Int); the rep args of MkS are Int#.  This is obviously no
771 good for T, because then we'd get an infinite number of arguments.
772
773 But it's the *argument* type that matters. This is fine:
774         data S = MkS S !Int
775 because Int is non-recursive.
776
777
778 %************************************************************************
779 %*                                                                      *
780                 Validity checking
781 %*                                                                      *
782 %************************************************************************
783
784 Validity checking is done once the mutually-recursive knot has been
785 tied, so we can look at things freely.
786
787 \begin{code}
788 checkClassCycleErrs :: [LTyClDecl Name] -> [LTyClDecl Name] -> TcM ()
789 checkClassCycleErrs syn_decls alg_decls
790   | null cls_cycles
791   = return ()
792   | otherwise
793   = do { mapM_ recClsErr cls_cycles
794        ; failM }       -- Give up now, because later checkValidTyCl
795                        -- will loop if the synonym is recursive
796   where
797     cls_cycles = calcClassCycles syn_decls alg_decls
798
799 checkValidTyCl :: TyClDecl Name -> TcM ()
800 -- We do the validity check over declarations, rather than TyThings
801 -- only so that we can add a nice context with tcAddDeclCtxt
802 checkValidTyCl decl
803   = tcAddDeclCtxt decl $
804     do  { thing <- tcLookupLocatedGlobal (tcdLName decl)
805         ; traceTc "Validity of" (ppr thing)     
806         ; case thing of
807             ATyCon tc -> do
808                 checkValidTyCon tc
809                 case decl of
810                   ClassDecl { tcdATs = ats } -> mapM_ (addLocM checkValidTyCl) ats
811                   _                          -> return ()
812             AnId _    -> return ()  -- Generic default methods are checked
813                                     -- with their parent class
814             _         -> panic "checkValidTyCl"
815         ; traceTc "Done validity of" (ppr thing)        
816         }
817
818 -------------------------
819 -- For data types declared with record syntax, we require
820 -- that each constructor that has a field 'f' 
821 --      (a) has the same result type
822 --      (b) has the same type for 'f'
823 -- module alpha conversion of the quantified type variables
824 -- of the constructor.
825 --
826 -- Note that we allow existentials to match becuase the
827 -- fields can never meet. E.g
828 --      data T where
829 --        T1 { f1 :: b, f2 :: a, f3 ::Int } :: T
830 --        T2 { f1 :: c, f2 :: c, f3 ::Int } :: T  
831 -- Here we do not complain about f1,f2 because they are existential
832
833 checkValidTyCon :: TyCon -> TcM ()
834 checkValidTyCon tc 
835   | Just cl <- tyConClass_maybe tc
836   = checkValidClass cl
837
838   | isSynTyCon tc 
839   = case synTyConRhs tc of
840       SynFamilyTyCon {} -> return ()
841       SynonymTyCon ty   -> checkValidType syn_ctxt ty
842   | otherwise
843   = do  -- Check the context on the data decl
844     checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc)
845         
846         -- Check arg types of data constructors
847     mapM_ (checkValidDataCon tc) data_cons
848
849         -- Check that fields with the same name share a type
850     mapM_ check_fields groups
851
852   where
853     syn_ctxt  = TySynCtxt name
854     name      = tyConName tc
855     data_cons = tyConDataCons tc
856
857     groups = equivClasses cmp_fld (concatMap get_fields data_cons)
858     cmp_fld (f1,_) (f2,_) = f1 `compare` f2
859     get_fields con = dataConFieldLabels con `zip` repeat con
860         -- dataConFieldLabels may return the empty list, which is fine
861
862     -- See Note [GADT record selectors] in MkId.lhs
863     -- We must check (a) that the named field has the same 
864     --                   type in each constructor
865     --               (b) that those constructors have the same result type
866     --
867     -- However, the constructors may have differently named type variable
868     -- and (worse) we don't know how the correspond to each other.  E.g.
869     --     C1 :: forall a b. { f :: a, g :: b } -> T a b
870     --     C2 :: forall d c. { f :: c, g :: c } -> T c d
871     -- 
872     -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
873     -- result type against other candidates' types BOTH WAYS ROUND.
874     -- If they magically agrees, take the substitution and
875     -- apply them to the latter ones, and see if they match perfectly.
876     check_fields ((label, con1) : other_fields)
877         -- These fields all have the same name, but are from
878         -- different constructors in the data type
879         = recoverM (return ()) $ mapM_ checkOne other_fields
880                 -- Check that all the fields in the group have the same type
881                 -- NB: this check assumes that all the constructors of a given
882                 -- data type use the same type variables
883         where
884         (tvs1, _, _, res1) = dataConSig con1
885         ts1 = mkVarSet tvs1
886         fty1 = dataConFieldType con1 label
887
888         checkOne (_, con2)    -- Do it bothways to ensure they are structurally identical
889             = do { checkFieldCompat label con1 con2 ts1 res1 res2 fty1 fty2
890                  ; checkFieldCompat label con2 con1 ts2 res2 res1 fty2 fty1 }
891             where        
892                 (tvs2, _, _, res2) = dataConSig con2
893                 ts2 = mkVarSet tvs2
894                 fty2 = dataConFieldType con2 label
895     check_fields [] = panic "checkValidTyCon/check_fields []"
896
897 checkFieldCompat :: Name -> DataCon -> DataCon -> TyVarSet
898                  -> Type -> Type -> Type -> Type -> TcM ()
899 checkFieldCompat fld con1 con2 tvs1 res1 res2 fty1 fty2
900   = do  { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
901         ; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
902   where
903     mb_subst1 = tcMatchTy tvs1 res1 res2
904     mb_subst2 = tcMatchTyX tvs1 (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
905
906 -------------------------------
907 checkValidDataCon :: TyCon -> DataCon -> TcM ()
908 checkValidDataCon tc con
909   = setSrcSpan (srcLocSpan (getSrcLoc con))     $
910     addErrCtxt (dataConCtxt con)                $ 
911     do  { traceTc "Validity of data con" (ppr con)
912         ; let tc_tvs = tyConTyVars tc
913               res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
914               actual_res_ty = dataConOrigResTy con
915         ; checkTc (isJust (tcMatchTy (mkVarSet tc_tvs)
916                                 res_ty_tmpl
917                                 actual_res_ty))
918                   (badDataConTyCon con res_ty_tmpl actual_res_ty)
919         ; checkValidMonoType (dataConOrigResTy con)
920                 -- Disallow MkT :: T (forall a. a->a)
921                 -- Reason: it's really the argument of an equality constraint
922         ; checkValidType ctxt (dataConUserType con)
923         ; when (isNewTyCon tc) (checkNewDataCon con)
924         ; mapM_ check_bang (dataConStrictMarks con `zip` [1..])
925     }
926   where
927     ctxt = ConArgCtxt (dataConName con) 
928     check_bang (HsUnpackFailed, n) = addWarnTc (cant_unbox_msg n)
929     check_bang _                   = return ()
930
931     cant_unbox_msg n = sep [ ptext (sLit "Ignoring unusable UNPACK pragma on the")
932                            , speakNth n <+> ptext (sLit "argument of") <+> quotes (ppr con)]
933
934 -------------------------------
935 checkNewDataCon :: DataCon -> TcM ()
936 -- Checks for the data constructor of a newtype
937 checkNewDataCon con
938   = do  { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
939                 -- One argument
940         ; checkTc (null eq_spec) (newtypePredError con)
941                 -- Return type is (T a b c)
942         ; checkTc (null ex_tvs && null theta) (newtypeExError con)
943                 -- No existentials
944         ; checkTc (not (any isBanged (dataConStrictMarks con))) 
945                   (newtypeStrictError con)
946                 -- No strictness
947     }
948   where
949     (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig con
950
951 -------------------------------
952 checkValidClass :: Class -> TcM ()
953 checkValidClass cls
954   = do  { constrained_class_methods <- xoptM Opt_ConstrainedClassMethods
955         ; multi_param_type_classes <- xoptM Opt_MultiParamTypeClasses
956         ; fundep_classes <- xoptM Opt_FunctionalDependencies
957
958         -- Check that the class is unary, unless GlaExs
959         ; checkTc (notNull tyvars) (nullaryClassErr cls)
960         ; checkTc (multi_param_type_classes || unary) (classArityErr cls)
961         ; checkTc (fundep_classes || null fundeps) (classFunDepsErr cls)
962
963         -- Check the super-classes
964         ; checkValidTheta (ClassSCCtxt (className cls)) theta
965
966         -- Check the class operations
967         ; mapM_ (check_op constrained_class_methods) op_stuff
968
969         -- Check that if the class has generic methods, then the
970         -- class has only one parameter.  We can't do generic
971         -- multi-parameter type classes!
972         ; checkTc (unary || no_generics) (genericMultiParamErr cls)
973         }
974   where
975     (tyvars, fundeps, theta, _, _, op_stuff) = classExtraBigSig cls
976     unary       = isSingleton tyvars
977     no_generics = null [() | (_, (GenDefMeth _)) <- op_stuff]
978
979     check_op constrained_class_methods (sel_id, dm) 
980       = addErrCtxt (classOpCtxt sel_id tau) $ do
981         { checkValidTheta SigmaCtxt (tail theta)
982                 -- The 'tail' removes the initial (C a) from the
983                 -- class itself, leaving just the method type
984
985         ; traceTc "class op type" (ppr op_ty <+> ppr tau)
986         ; checkValidType (FunSigCtxt op_name) tau
987
988                 -- Check that the type mentions at least one of
989                 -- the class type variables...or at least one reachable
990                 -- from one of the class variables.  Example: tc223
991                 --   class Error e => Game b mv e | b -> mv e where
992                 --      newBoard :: MonadState b m => m ()
993                 -- Here, MonadState has a fundep m->b, so newBoard is fine
994         ; let grown_tyvars = growThetaTyVars theta (mkVarSet tyvars)
995         ; checkTc (tyVarsOfType tau `intersectsVarSet` grown_tyvars)
996                   (noClassTyVarErr cls sel_id)
997
998         ; case dm of
999             GenDefMeth dm_name -> do { dm_id <- tcLookupId dm_name
1000                                      ; checkValidType (FunSigCtxt op_name) (idType dm_id) }
1001             _                  -> return ()
1002         }
1003         where
1004           op_name = idName sel_id
1005           op_ty   = idType sel_id
1006           (_,theta1,tau1) = tcSplitSigmaTy op_ty
1007           (_,theta2,tau2)  = tcSplitSigmaTy tau1
1008           (theta,tau) | constrained_class_methods = (theta1 ++ theta2, tau2)
1009                       | otherwise = (theta1, mkPhiTy (tail theta1) tau1)
1010                 -- Ugh!  The function might have a type like
1011                 --      op :: forall a. C a => forall b. (Eq b, Eq a) => tau2
1012                 -- With -XConstrainedClassMethods, we want to allow this, even though the inner 
1013                 -- forall has an (Eq a) constraint.  Whereas in general, each constraint 
1014                 -- in the context of a for-all must mention at least one quantified
1015                 -- type variable.  What a mess!
1016
1017 checkFamFlag :: Name -> TcM ()
1018 -- Check that we don't use families without -XTypeFamilies
1019 -- The parser won't even parse them, but I suppose a GHC API
1020 -- client might have a go!
1021 checkFamFlag tc_name
1022   = do { idx_tys <- xoptM Opt_TypeFamilies
1023        ; checkTc idx_tys err_msg }
1024   where
1025     err_msg = hang (ptext (sLit "Illegal family declaraion for") <+> quotes (ppr tc_name))
1026                  2 (ptext (sLit "Use -XTypeFamilies to allow indexed type families"))
1027 \end{code}
1028
1029
1030 %************************************************************************
1031 %*                                                                      *
1032                 Building record selectors
1033 %*                                                                      *
1034 %************************************************************************
1035
1036 \begin{code}
1037 mkDefaultMethodIds :: [TyThing] -> [Id]
1038 -- See Note [Default method Ids and Template Haskell]
1039 mkDefaultMethodIds things
1040   = [ mkExportedLocalId dm_name (idType sel_id)
1041     | ATyCon tc <- things
1042     , Just cls <- [tyConClass_maybe tc]
1043     , (sel_id, DefMeth dm_name) <- classOpItems cls ]
1044 \end{code}
1045
1046 Note [Default method Ids and Template Haskell]
1047 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1048 Consider this (Trac #4169):
1049    class Numeric a where
1050      fromIntegerNum :: a
1051      fromIntegerNum = ...
1052
1053    ast :: Q [Dec]
1054    ast = [d| instance Numeric Int |]
1055
1056 When we typecheck 'ast' we have done the first pass over the class decl
1057 (in tcTyClDecls), but we have not yet typechecked the default-method
1058 declarations (becuase they can mention value declarations).  So we 
1059 must bring the default method Ids into scope first (so they can be seen
1060 when typechecking the [d| .. |] quote, and typecheck them later.
1061
1062 \begin{code}
1063 mkRecSelBinds :: [TyCon] -> HsValBinds Name
1064 -- NB We produce *un-typechecked* bindings, rather like 'deriving'
1065 --    This makes life easier, because the later type checking will add
1066 --    all necessary type abstractions and applications
1067 mkRecSelBinds tycons
1068   = ValBindsOut [(NonRecursive, b) | b <- binds] sigs
1069   where
1070     (sigs, binds) = unzip rec_sels
1071     rec_sels = map mkRecSelBind [ (tc,fld) 
1072                                 | tc <- tycons
1073                                 , fld <- tyConFields tc ]
1074
1075 mkRecSelBind :: (TyCon, FieldLabel) -> (LSig Name, LHsBinds Name)
1076 mkRecSelBind (tycon, sel_name)
1077   = (L loc (IdSig sel_id), unitBag (L loc sel_bind))
1078   where
1079     loc         = getSrcSpan tycon    
1080     sel_id      = Var.mkLocalVar rec_details sel_name sel_ty vanillaIdInfo
1081     rec_details = RecSelId { sel_tycon = tycon, sel_naughty = is_naughty }
1082
1083     -- Find a representative constructor, con1
1084     all_cons     = tyConDataCons tycon 
1085     cons_w_field = [ con | con <- all_cons
1086                    , sel_name `elem` dataConFieldLabels con ] 
1087     con1 = ASSERT( not (null cons_w_field) ) head cons_w_field
1088
1089     -- Selector type; Note [Polymorphic selectors]
1090     field_ty   = dataConFieldType con1 sel_name
1091     data_ty    = dataConOrigResTy con1
1092     data_tvs   = tyVarsOfType data_ty
1093     is_naughty = not (tyVarsOfType field_ty `subVarSet` data_tvs)  
1094     (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
1095     sel_ty | is_naughty = unitTy  -- See Note [Naughty record selectors]
1096            | otherwise  = mkForAllTys (varSetElems data_tvs ++ field_tvs) $ 
1097                           mkPhiTy (dataConStupidTheta con1) $   -- Urgh!
1098                           mkPhiTy field_theta               $   -- Urgh!
1099                           mkFunTy data_ty field_tau
1100
1101     -- Make the binding: sel (C2 { fld = x }) = x
1102     --                   sel (C7 { fld = x }) = x
1103     --    where cons_w_field = [C2,C7]
1104     sel_bind | is_naughty = mkTopFunBind sel_lname [mkSimpleMatch [] unit_rhs]
1105              | otherwise  = mkTopFunBind sel_lname (map mk_match cons_w_field ++ deflt)
1106     mk_match con = mkSimpleMatch [L loc (mk_sel_pat con)] 
1107                                  (L loc (HsVar field_var))
1108     mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields)
1109     rec_fields = HsRecFields { rec_flds = [rec_field], rec_dotdot = Nothing }
1110     rec_field  = HsRecField { hsRecFieldId = sel_lname
1111                             , hsRecFieldArg = nlVarPat field_var
1112                             , hsRecPun = False }
1113     sel_lname = L loc sel_name
1114     field_var = mkInternalName (mkBuiltinUnique 1) (getOccName sel_name) loc
1115
1116     -- Add catch-all default case unless the case is exhaustive
1117     -- We do this explicitly so that we get a nice error message that
1118     -- mentions this particular record selector
1119     deflt | not (any is_unused all_cons) = []
1120           | otherwise = [mkSimpleMatch [nlWildPat] 
1121                             (nlHsApp (nlHsVar (getName rEC_SEL_ERROR_ID))
1122                                      (nlHsLit msg_lit))]
1123
1124         -- Do not add a default case unless there are unmatched
1125         -- constructors.  We must take account of GADTs, else we
1126         -- get overlap warning messages from the pattern-match checker
1127     is_unused con = not (con `elem` cons_w_field 
1128                          || dataConCannotMatch inst_tys con)
1129     inst_tys = tyConAppArgs data_ty
1130
1131     unit_rhs = mkLHsTupleExpr []
1132     msg_lit = HsStringPrim $ mkFastString $ 
1133               occNameString (getOccName sel_name)
1134
1135 ---------------
1136 tyConFields :: TyCon -> [FieldLabel]
1137 tyConFields tc 
1138   | isAlgTyCon tc = nub (concatMap dataConFieldLabels (tyConDataCons tc))
1139   | otherwise     = []
1140 \end{code}
1141
1142 Note [Polymorphic selectors]
1143 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1144 When a record has a polymorphic field, we pull the foralls out to the front.
1145    data T = MkT { f :: forall a. [a] -> a }
1146 Then f :: forall a. T -> [a] -> a
1147 NOT  f :: T -> forall a. [a] -> a
1148
1149 This is horrid.  It's only needed in deeply obscure cases, which I hate.
1150 The only case I know is test tc163, which is worth looking at.  It's far
1151 from clear that this test should succeed at all!
1152
1153 Note [Naughty record selectors]
1154 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1155 A "naughty" field is one for which we can't define a record 
1156 selector, because an existential type variable would escape.  For example:
1157         data T = forall a. MkT { x,y::a }
1158 We obviously can't define       
1159         x (MkT v _) = v
1160 Nevertheless we *do* put a RecSelId into the type environment
1161 so that if the user tries to use 'x' as a selector we can bleat
1162 helpfully, rather than saying unhelpfully that 'x' is not in scope.
1163 Hence the sel_naughty flag, to identify record selectors that don't really exist.
1164
1165 In general, a field is "naughty" if its type mentions a type variable that
1166 isn't in the result type of the constructor.  Note that this *allows*
1167 GADT record selectors (Note [GADT record selectors]) whose types may look 
1168 like     sel :: T [a] -> a
1169
1170 For naughty selectors we make a dummy binding 
1171    sel = ()
1172 for naughty selectors, so that the later type-check will add them to the
1173 environment, and they'll be exported.  The function is never called, because
1174 the tyepchecker spots the sel_naughty field.
1175
1176 Note [GADT record selectors]
1177 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1178 For GADTs, we require that all constructors with a common field 'f' have the same
1179 result type (modulo alpha conversion).  [Checked in TcTyClsDecls.checkValidTyCon]
1180 E.g. 
1181         data T where
1182           T1 { f :: Maybe a } :: T [a]
1183           T2 { f :: Maybe a, y :: b  } :: T [a]
1184           T3 :: T Int
1185
1186 and now the selector takes that result type as its argument:
1187    f :: forall a. T [a] -> Maybe a
1188
1189 Details: the "real" types of T1,T2 are:
1190    T1 :: forall r a.   (r~[a]) => a -> T r
1191    T2 :: forall r a b. (r~[a]) => a -> b -> T r
1192
1193 So the selector loooks like this:
1194    f :: forall a. T [a] -> Maybe a
1195    f (a:*) (t:T [a])
1196      = case t of
1197          T1 c   (g:[a]~[c]) (v:Maybe c)       -> v `cast` Maybe (right (sym g))
1198          T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
1199          T3 -> error "T3 does not have field f"
1200
1201 Note the forall'd tyvars of the selector are just the free tyvars
1202 of the result type; there may be other tyvars in the constructor's
1203 type (e.g. 'b' in T2).
1204
1205 Note the need for casts in the result!
1206
1207 Note [Selector running example]
1208 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1209 It's OK to combine GADTs and type families.  Here's a running example:
1210
1211         data instance T [a] where 
1212           T1 { fld :: b } :: T [Maybe b]
1213
1214 The representation type looks like this
1215         data :R7T a where
1216           T1 { fld :: b } :: :R7T (Maybe b)
1217
1218 and there's coercion from the family type to the representation type
1219         :CoR7T a :: T [a] ~ :R7T a
1220
1221 The selector we want for fld looks like this:
1222
1223         fld :: forall b. T [Maybe b] -> b
1224         fld = /\b. \(d::T [Maybe b]).
1225               case d `cast` :CoR7T (Maybe b) of 
1226                 T1 (x::b) -> x
1227
1228 The scrutinee of the case has type :R7T (Maybe b), which can be
1229 gotten by appying the eq_spec to the univ_tvs of the data con.
1230
1231 %************************************************************************
1232 %*                                                                      *
1233                 Error messages
1234 %*                                                                      *
1235 %************************************************************************
1236
1237 \begin{code}
1238 resultTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc
1239 resultTypeMisMatch field_name con1 con2
1240   = vcat [sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2, 
1241                 ptext (sLit "have a common field") <+> quotes (ppr field_name) <> comma],
1242           nest 2 $ ptext (sLit "but have different result types")]
1243
1244 fieldTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc
1245 fieldTypeMisMatch field_name con1 con2
1246   = sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2, 
1247          ptext (sLit "give different types for field"), quotes (ppr field_name)]
1248
1249 dataConCtxt :: Outputable a => a -> SDoc
1250 dataConCtxt con = ptext (sLit "In the definition of data constructor") <+> quotes (ppr con)
1251
1252 classOpCtxt :: Var -> Type -> SDoc
1253 classOpCtxt sel_id tau = sep [ptext (sLit "When checking the class method:"),
1254                               nest 2 (ppr sel_id <+> dcolon <+> ppr tau)]
1255
1256 nullaryClassErr :: Class -> SDoc
1257 nullaryClassErr cls
1258   = ptext (sLit "No parameters for class")  <+> quotes (ppr cls)
1259
1260 classArityErr :: Class -> SDoc
1261 classArityErr cls
1262   = vcat [ptext (sLit "Too many parameters for class") <+> quotes (ppr cls),
1263           parens (ptext (sLit "Use -XMultiParamTypeClasses to allow multi-parameter classes"))]
1264
1265 classFunDepsErr :: Class -> SDoc
1266 classFunDepsErr cls
1267   = vcat [ptext (sLit "Fundeps in class") <+> quotes (ppr cls),
1268           parens (ptext (sLit "Use -XFunctionalDependencies to allow fundeps"))]
1269
1270 noClassTyVarErr :: Class -> Var -> SDoc
1271 noClassTyVarErr clas op
1272   = sep [ptext (sLit "The class method") <+> quotes (ppr op),
1273          ptext (sLit "mentions none of the type variables of the class") <+> 
1274                 ppr clas <+> hsep (map ppr (classTyVars clas))]
1275
1276 genericMultiParamErr :: Class -> SDoc
1277 genericMultiParamErr clas
1278   = ptext (sLit "The multi-parameter class") <+> quotes (ppr clas) <+> 
1279     ptext (sLit "cannot have generic methods")
1280
1281 recSynErr :: [LTyClDecl Name] -> TcRn ()
1282 recSynErr syn_decls
1283   = setSrcSpan (getLoc (head sorted_decls)) $
1284     addErr (sep [ptext (sLit "Cycle in type synonym declarations:"),
1285                  nest 2 (vcat (map ppr_decl sorted_decls))])
1286   where
1287     sorted_decls = sortLocated syn_decls
1288     ppr_decl (L loc decl) = ppr loc <> colon <+> ppr decl
1289
1290 recClsErr :: [Located (TyClDecl Name)] -> TcRn ()
1291 recClsErr cls_decls
1292   = setSrcSpan (getLoc (head sorted_decls)) $
1293     addErr (sep [ptext (sLit "Cycle in class declarations (via superclasses):"),
1294                 nest 2 (vcat (map ppr_decl sorted_decls))])
1295   where
1296     sorted_decls = sortLocated cls_decls
1297     ppr_decl (L loc decl) = ppr loc <> colon <+> ppr (decl { tcdSigs = [] })
1298
1299 sortLocated :: [Located a] -> [Located a]
1300 sortLocated things = sortLe le things
1301   where
1302     le (L l1 _) (L l2 _) = l1 <= l2
1303
1304 badDataConTyCon :: DataCon -> Type -> Type -> SDoc
1305 badDataConTyCon data_con res_ty_tmpl actual_res_ty
1306   = hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con) <+>
1307                 ptext (sLit "returns type") <+> quotes (ppr actual_res_ty))
1308        2 (ptext (sLit "instead of an instance of its parent type") <+> quotes (ppr res_ty_tmpl))
1309
1310 badGadtDecl :: Name -> SDoc
1311 badGadtDecl tc_name
1312   = vcat [ ptext (sLit "Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
1313          , nest 2 (parens $ ptext (sLit "Use -XGADTs to allow GADTs")) ]
1314
1315 badExistential :: Located Name -> SDoc
1316 badExistential con_name
1317   = hang (ptext (sLit "Data constructor") <+> quotes (ppr con_name) <+>
1318                 ptext (sLit "has existential type variables, a context, or a specialised result type"))
1319        2 (parens $ ptext (sLit "Use -XExistentialQuantification or -XGADTs to allow this"))
1320
1321 badStupidTheta :: Name -> SDoc
1322 badStupidTheta tc_name
1323   = ptext (sLit "A data type declared in GADT style cannot have a context:") <+> quotes (ppr tc_name)
1324
1325 newtypeConError :: Name -> Int -> SDoc
1326 newtypeConError tycon n
1327   = sep [ptext (sLit "A newtype must have exactly one constructor,"),
1328          nest 2 $ ptext (sLit "but") <+> quotes (ppr tycon) <+> ptext (sLit "has") <+> speakN n ]
1329
1330 newtypeExError :: DataCon -> SDoc
1331 newtypeExError con
1332   = sep [ptext (sLit "A newtype constructor cannot have an existential context,"),
1333          nest 2 $ ptext (sLit "but") <+> quotes (ppr con) <+> ptext (sLit "does")]
1334
1335 newtypeStrictError :: DataCon -> SDoc
1336 newtypeStrictError con
1337   = sep [ptext (sLit "A newtype constructor cannot have a strictness annotation,"),
1338          nest 2 $ ptext (sLit "but") <+> quotes (ppr con) <+> ptext (sLit "does")]
1339
1340 newtypePredError :: DataCon -> SDoc
1341 newtypePredError con
1342   = sep [ptext (sLit "A newtype constructor must have a return type of form T a1 ... an"),
1343          nest 2 $ ptext (sLit "but") <+> quotes (ppr con) <+> ptext (sLit "does not")]
1344
1345 newtypeFieldErr :: DataCon -> Int -> SDoc
1346 newtypeFieldErr con_name n_flds
1347   = sep [ptext (sLit "The constructor of a newtype must have exactly one field"), 
1348          nest 2 $ ptext (sLit "but") <+> quotes (ppr con_name) <+> ptext (sLit "has") <+> speakN n_flds]
1349
1350 badSigTyDecl :: Name -> SDoc
1351 badSigTyDecl tc_name
1352   = vcat [ ptext (sLit "Illegal kind signature") <+>
1353            quotes (ppr tc_name)
1354          , nest 2 (parens $ ptext (sLit "Use -XKindSignatures to allow kind signatures")) ]
1355
1356 emptyConDeclsErr :: Name -> SDoc
1357 emptyConDeclsErr tycon
1358   = sep [quotes (ppr tycon) <+> ptext (sLit "has no constructors"),
1359          nest 2 $ ptext (sLit "(-XEmptyDataDecls permits this)")]
1360 \end{code}