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