Merge branch 'master' of darcs.haskell.org:/home/darcs/ghc
[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 {-# OPTIONS -fno-warn-tabs #-}
10 -- The above warning supression flag is a temporary kludge.
11 -- While working on this module you are encouraged to remove it and
12 -- detab the module (please do the detabbing in a separate patch). See
13 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
14 -- for details
15
16 module TcTyClsDecls (
17         tcTyAndClassDecls, tcAddImplicits,
18
19         -- Functions used by TcInstDcls to check 
20         -- data/type family instance declarations
21         kcTyDefn, tcConDecls, dataDeclChecks, checkValidTyCon,
22         tcSynFamInstDecl, tcFamTyPats, 
23         tcAddFamInstCtxt, wrongKindOfFamily, badATErr, wrongATArgErr
24     ) where
25
26 #include "HsVersions.h"
27
28 import HsSyn
29 import HscTypes
30 import BuildTyCl
31 import TcUnify
32 import TcRnMonad
33 import TcEnv
34 import TcHsSyn
35 import TcBinds( tcRecSelBinds )
36 import TcTyDecls
37 import TcClassDcl
38 import TcHsType
39 import TcMType
40 import TcType
41 import TysWiredIn( unitTy )
42 import Type
43 import Kind
44 import Class
45 import TyCon
46 import DataCon
47 import Id
48 import MkCore           ( rEC_SEL_ERROR_ID )
49 import IdInfo
50 import Var
51 import VarSet
52 import Name
53 import NameSet
54 import NameEnv
55 import Outputable
56 import Maybes
57 import Unify
58 import Util
59 import SrcLoc
60 import ListSetOps
61 import Digraph
62 import DynFlags
63 import FastString
64 import Unique           ( mkBuiltinUnique )
65 import BasicTypes
66
67 import Bag
68 import Control.Monad
69 import Data.List
70 \end{code}
71
72
73 %************************************************************************
74 %*                                                                      *
75 \subsection{Type checking for type and class declarations}
76 %*                                                                      *
77 %************************************************************************
78
79 Note [Grouping of type and class declarations]
80 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
81 tcTyAndClassDecls is called on a list of `TyClGroup`s. Each group is a strongly
82 connected component of mutually dependent types and classes. We kind check and
83 type check each group separately to enhance kind polymorphism. Take the
84 following example:
85
86   type Id a = a
87   data X = X (Id Int)
88
89 If we were to kind check the two declarations together, we would give Id the
90 kind * -> *, since we apply it to an Int in the definition of X. But we can do
91 better than that, since Id really is kind polymorphic, and should get kind
92 forall (k::BOX). k -> k. Since it does not depend on anything else, it can be
93 kind-checked by itself, hence getting the most general kind. We then kind check
94 X, which works fine because we then know the polymorphic kind of Id, and simply
95 instantiate k to *.
96
97 \begin{code}
98
99 tcTyAndClassDecls :: ModDetails
100                   -> [TyClGroup Name]   -- Mutually-recursive groups in dependency order
101                   -> TcM TcGblEnv       -- Input env extended by types and classes
102                                         -- and their implicit Ids,DataCons
103 -- Fails if there are any errors
104 tcTyAndClassDecls boot_details tyclds_s
105   = checkNoErrs $       -- The code recovers internally, but if anything gave rise to
106                         -- an error we'd better stop now, to avoid a cascade
107     fold_env tyclds_s   -- Type check each group in dependency order folding the global env
108   where
109     fold_env :: [TyClGroup Name] -> TcM TcGblEnv
110     fold_env [] = getGblEnv
111     fold_env (tyclds:tyclds_s)
112       = do { tcg_env <- tcTyClGroup boot_details tyclds
113            ; setGblEnv tcg_env $ fold_env tyclds_s }
114              -- remaining groups are typecheck in the extended global env
115
116 tcTyClGroup :: ModDetails -> TyClGroup Name -> TcM TcGblEnv
117 -- Typecheck one strongly-connected component of type and class decls
118 tcTyClGroup boot_details tyclds
119   = do {    -- Step 1: kind-check this group and returns the final
120             -- (possibly-polymorphic) kind of each TyCon and Class
121             -- See Note [Kind checking for type and class decls]
122          names_w_poly_kinds <- kcTyClGroup tyclds
123        ; traceTc "tcTyAndCl generalized kinds" (ppr names_w_poly_kinds)
124
125             -- Step 2: type-check all groups together, returning 
126             -- the final TyCons and Classes
127        ; tyclss <- fixM $ \ rec_tyclss -> do
128            { let rec_flags = calcRecFlags boot_details rec_tyclss
129
130                  -- Populate environment with knot-tied ATyCon for TyCons
131                  -- NB: if the decls mention any ill-staged data cons
132                  -- (see Note [ARecDataCon: Recusion and promoting data constructors]
133                  -- we will have failed already in kcTyClGroup, so no worries here
134            ; tcExtendRecEnv (zipRecTyClss names_w_poly_kinds rec_tyclss) $
135
136                  -- Also extend the local type envt with bindings giving
137                  -- the (polymorphic) kind of each knot-tied TyCon or Class
138                  -- See Note [Type checking recursive type and class declarations]
139              tcExtendKindEnv names_w_poly_kinds              $
140
141                  -- Kind and type check declarations for this group
142              concatMapM (tcTyClDecl rec_flags) tyclds }
143
144            -- Step 3: Perform the validity chebck
145            -- We can do this now because we are done with the recursive knot
146            -- Do it before Step 4 (adding implicit things) because the latter
147            -- expects well-formed TyCons
148        ; tcExtendGlobalEnv tyclss $ do
149        { traceTc "Starting validity check" (ppr tyclss)
150        ; mapM_ (recoverM (return ()) . addLocM checkValidTyCl) 
151                (flattenTyClDecls tyclds)
152            -- We recover, which allows us to report multiple validity errors
153            -- even from successive groups.  But we stop after all groups are
154            -- processed if we find any errors.
155
156            -- Step 4: Add the implicit things;
157            -- we want them in the environment because
158            -- they may be mentioned in interface files
159        ; tcExtendGlobalValEnv (mkDefaultMethodIds tyclss) $
160          tcAddImplicits tyclss } }
161
162 tcAddImplicits :: [TyThing] -> TcM TcGblEnv
163 tcAddImplicits tyclss
164  = tcExtendGlobalEnvImplicit implicit_things $ 
165    tcRecSelBinds rec_sel_binds
166  where
167    implicit_things = concatMap implicitTyThings tyclss
168    rec_sel_binds   = mkRecSelBinds tyclss
169
170 zipRecTyClss :: [(Name, Kind)]
171              -> [TyThing]           -- Knot-tied
172              -> [(Name,TyThing)]
173 -- Build a name-TyThing mapping for the things bound by decls
174 -- being careful not to look at the [TyThing]
175 -- The TyThings in the result list must have a visible ATyCon,
176 -- because typechecking types (in, say, tcTyClDecl) looks at this outer constructor
177 zipRecTyClss kind_pairs rec_things
178   = [ (name, ATyCon (get name)) | (name, _kind) <- kind_pairs ]
179   where
180     rec_type_env :: TypeEnv
181     rec_type_env = mkTypeEnv rec_things
182
183     get name = case lookupTypeEnv rec_type_env name of
184                  Just (ATyCon tc) -> tc
185                  other            -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
186
187 flattenTyClDecls :: [LTyClDecl Name] -> [LTyClDecl Name]
188 -- Lift out the associated type declaraitons to top level
189 flattenTyClDecls [] = []
190 flattenTyClDecls (ld@(L _ d) : lds)
191   | isClassDecl d = ld : tcdATs d ++ flattenTyClDecls lds
192   | otherwise     = ld : flattenTyClDecls lds
193 \end{code}
194
195
196 %************************************************************************
197 %*                                                                      *
198                 Kind checking
199 %*                                                                      *
200 %************************************************************************
201
202 Note [Kind checking for type and class decls]
203 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
204 Kind checking is done thus:
205
206    1. Make up a kind variable for each parameter of the *data* type, 
207       and class, decls, and extend the kind environment (which is in
208       the TcLclEnv)
209
210    2. Dependency-analyse the type *synonyms* (which must be non-recursive),
211       and kind-check them in dependency order.  Extend the kind envt.
212
213    3. Kind check the data type and class decls
214
215 Synonyms are treated differently to data type and classes,
216 because a type synonym can be an unboxed type
217         type Foo = Int#
218 and a kind variable can't unify with UnboxedTypeKind
219 So we infer their kinds in dependency order
220
221 We need to kind check all types in the mutually recursive group
222 before we know the kind of the type variables.  For example:
223
224   class C a where
225      op :: D b => a -> b -> b
226
227   class D c where
228      bop :: (Monad c) => ...
229
230 Here, the kind of the locally-polymorphic type variable "b"
231 depends on *all the uses of class D*.  For example, the use of
232 Monad c in bop's type signature means that D must have kind Type->Type.
233
234 However type synonyms work differently.  They can have kinds which don't
235 just involve (->) and *:
236         type R = Int#           -- Kind #
237         type S a = Array# a     -- Kind * -> #
238         type T a b = (# a,b #)  -- Kind * -> * -> (# a,b #)
239 So we must infer their kinds from their right-hand sides *first* and then
240 use them, whereas for the mutually recursive data types D we bring into
241 scope kind bindings D -> k, where k is a kind variable, and do inference.
242
243 Type families
244 ~~~~~~~~~~~~~
245 This treatment of type synonyms only applies to Haskell 98-style synonyms.
246 General type functions can be recursive, and hence, appear in `alg_decls'.
247
248 The kind of a type family is solely determinded by its kind signature;
249 hence, only kind signatures participate in the construction of the initial
250 kind environment (as constructed by `getInitialKind').  In fact, we ignore
251 instances of families altogether in the following.  However, we need to
252 include the kinds of *associated* families into the construction of the
253 initial kind environment.  (This is handled by `allDecls').
254
255
256 \begin{code}
257 kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind)]
258 -- Kind check this group, kind generalize, and return the resulting local env
259 -- This bindds the TyCons and Classes of the group, but not the DataCons
260 -- See Note [Kind checking for type and class decls]
261 kcTyClGroup decls
262   = do  { mod <- getModule
263         ; traceTc "kcTyClGroup" (ptext (sLit "module") <+> ppr mod $$ vcat (map ppr decls))
264
265           -- Kind checking; 
266           --    1. Bind kind variables for non-synonyms
267           --    2. Kind-check synonyms, and bind kinds of those synonyms
268           --    3. Kind-check non-synonyms
269           --    4. Generalise the inferred kinds
270           -- See Note [Kind checking for type and class decls]
271
272           -- Step 1: Bind kind variables for non-synonyms
273         ; let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls
274         ; initial_kinds <- 
275                            getInitialKinds TopLevel non_syn_decls
276         ; traceTc "kcTyClGroup: initial kinds" (ppr initial_kinds)
277
278         -- Step 2: Set initial envt, kind-check the synonyms
279         ; lcl_env <- tcExtendTcTyThingEnv initial_kinds $ 
280                      kcSynDecls (calcSynCycles syn_decls)
281
282         -- Step 3: Set extended envt, kind-check the non-synonyms
283         ; setLclEnv lcl_env $
284           mapM_ kcLTyClDecl non_syn_decls
285
286              -- Step 4: generalisation
287              -- Kind checking done for this group
288              -- Now we have to kind generalize the flexis
289         ; res <- mapM (generalise (tcl_env lcl_env)) (flattenTyClDecls decls)
290
291         ; traceTc "kcTyClGroup result" (ppr res)
292         ; return res }
293
294   where
295     generalise :: TcTypeEnv -> LTyClDecl Name -> TcM (Name, Kind)
296     -- For polymorphic things this is a no-op
297     generalise kind_env (L _ decl)
298       = do { let name = tcdName decl
299                  tvs  = tcdTyVars decl
300            ; let kc_kind = case lookupNameEnv kind_env name of
301                                Just (AThing k) -> k
302                                _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
303            ; kvs <- kindGeneralize (tyVarsOfType kc_kind) (hsLTyVarNames tvs)
304            ; kc_kind' <- zonkTcKind kc_kind    -- Make sure kc_kind' has the final,
305                                                -- skolemised kind variables
306            ; traceTc "Generalise kind" (vcat [ ppr name, ppr kc_kind, ppr kvs, ppr kc_kind' ])
307            ; return (name, mkForAllTys kvs kc_kind') }
308
309 getInitialKinds :: TopLevelFlag -> [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
310 getInitialKinds top_lvl decls
311   = tcExtendTcTyThingEnv [ (tcdName d, APromotionErr (mk_promotion_err d))
312                          | L _ d <- flattenTyClDecls decls] $
313     concatMapM (addLocM (getInitialKind top_lvl)) decls
314   where
315     mk_promotion_err (ClassDecl {}) = ClassPE
316     mk_promotion_err _              = TyConPE
317
318 getInitialKind :: TopLevelFlag -> TyClDecl Name -> TcM [(Name, TcTyThing)]
319 -- Allocate a fresh kind variable for each TyCon and Class
320 -- For each tycon, return   (tc, AThing k)
321 --                 where k is the kind of tc, derived from the LHS
322 --                       of the definition (and probably including
323 --                       kind unification variables)
324 --      Example: data T a b = ...
325 --      return (T, kv1 -> kv2 -> kv3)
326 --
327 -- ALSO for each datacon, return (dc, ARecDataCon)
328 -- Note [ARecDataCon: Recusion and promoting data constructors]
329 -- 
330 -- No family instances are passed to getInitialKinds
331
332 getInitialKind top_lvl (TyFamily { tcdLName = L _ name, tcdTyVars = ktvs, tcdKindSig = ksig })
333   | isTopLevel top_lvl 
334   = kcHsTyVarBndrs True ktvs $ \ arg_kinds ->
335     do { res_k <- case ksig of 
336                     Just k  -> tcLHsKind k
337                     Nothing -> return liftedTypeKind
338        ; let body_kind = mkArrowKinds arg_kinds res_k
339              kvs       = varSetElems (tyVarsOfType body_kind)
340        ; return [ (name, AThing (mkForAllTys kvs body_kind)) ] }
341
342   | otherwise
343   = kcHsTyVarBndrs False ktvs $ \ arg_kinds ->
344     do { res_k <- case ksig of 
345                     Just k  -> tcLHsKind k
346                     Nothing -> newMetaKindVar
347        ; return [ (name, AThing (mkArrowKinds arg_kinds res_k)) ] }
348
349 getInitialKind _ (ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
350   = kcHsTyVarBndrs False ktvs $ \ arg_kinds ->
351     do { inner_prs <- getInitialKinds NotTopLevel ats
352        ; let main_pr = (name, AThing (mkArrowKinds arg_kinds constraintKind))
353        ; return (main_pr : inner_prs) }
354
355 getInitialKind top_lvl decl@(TyDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdTyDefn = defn })
356   | TyData { td_kindSig = Just ksig, td_cons = cons } <- defn
357   = ASSERT( isTopLevel top_lvl )
358     kcHsTyVarBndrs True ktvs $ \ arg_kinds -> 
359     do { res_k <- tcLHsKind ksig
360        ; let body_kind = mkArrowKinds arg_kinds res_k
361              kvs       = varSetElems (tyVarsOfType body_kind)
362              main_pr   = (name, AThing (mkForAllTys kvs body_kind))
363              inner_prs = [(unLoc (con_name con), APromotionErr RecDataConPE) | L _ con <- cons ]
364              -- See Note [ARecDataCon: Recusion and promoting data constructors]
365        ; return (main_pr : inner_prs) }
366  
367   | TyData { td_cons = cons } <- defn
368   = kcHsTyVarBndrs False ktvs $ \ arg_kinds -> 
369     do { let main_pr   = (name, AThing (mkArrowKinds arg_kinds liftedTypeKind))
370              inner_prs = [(unLoc (con_name con), APromotionErr RecDataConPE) | L _ con <- cons ]
371              -- See Note [ARecDataCon: Recusion and promoting data constructors]
372        ; return (main_pr : inner_prs) }
373
374   | otherwise = pprPanic "getInitialKind" (ppr decl)
375
376 getInitialKind _ (ForeignType { tcdLName = L _ name }) 
377   = return [(name, AThing liftedTypeKind)]
378
379
380 ----------------
381 kcSynDecls :: [SCC (LTyClDecl Name)] -> TcM TcLclEnv    -- Kind bindings
382 kcSynDecls [] = getLclEnv
383 kcSynDecls (group : groups)
384   = do  { nk <- kcSynDecl1 group
385         ; tcExtendKindEnv [nk] (kcSynDecls groups) }
386
387 kcSynDecl1 :: SCC (LTyClDecl Name)
388            -> TcM (Name,TcKind) -- Kind bindings
389 kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl
390 kcSynDecl1 (CyclicSCC decls)       = do { recSynErr decls; failM }
391                                      -- Fail here to avoid error cascade
392                                      -- of out-of-scope tycons
393
394 kcSynDecl :: TyClDecl Name -> TcM (Name, TcKind)
395 kcSynDecl decl@(TyDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
396                        , tcdTyDefn = TySynonym { td_synRhs = rhs } })
397   -- Returns a possibly-unzonked kind
398   = tcAddDeclCtxt decl $
399     kcHsTyVarBndrs False hs_tvs $ \ ks ->
400     do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs)
401                          <+> brackets (ppr ks))
402        ; (_, rhs_kind) <- tcLHsType rhs
403        ; traceTc "kcd2" (ppr name)
404        ; let tc_kind = mkArrowKinds ks rhs_kind
405        ; return (name, tc_kind) }
406 kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl)
407
408 ------------------------------------------------------------------------
409 kcLTyClDecl :: LTyClDecl Name -> TcM ()
410   -- See Note [Kind checking for type and class decls]
411 kcLTyClDecl (L loc decl)
412   = setSrcSpan loc $ tcAddDeclCtxt decl $ kcTyClDecl decl
413
414 kcTyClDecl :: TyClDecl Name -> TcM ()
415 -- This function is used solely for its side effect on kind variables
416
417 kcTyClDecl decl@(TyDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdTyDefn = defn })
418   | TyData { td_cons = cons, td_kindSig = Just _ } <- defn
419   = mapM_ (wrapLocM kcConDecl) cons  -- Ignore the td_ctxt; heavily deprecated and inconvenient
420
421   | TyData { td_ctxt = ctxt, td_cons = cons } <- defn
422   = kcTyClTyVars name hs_tvs $ \ _res_k -> 
423     do  { _ <- tcHsContext ctxt
424         ; mapM_ (wrapLocM kcConDecl) cons }
425
426   | otherwise = pprPanic "kcTyClDecl" (ppr decl)
427
428 kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
429                        , tcdCtxt = ctxt, tcdSigs = sigs, tcdATs = ats})
430   = kcTyClTyVars name hs_tvs $ \ _res_k -> 
431     do  { _ <- tcHsContext ctxt
432         ; mapM_ (wrapLocM kcTyClDecl) ats
433         ; mapM_ (wrapLocM kc_sig)     sigs }
434   where
435     kc_sig (TypeSig _ op_ty)    = discardResult (tcHsLiftedType op_ty)
436     kc_sig (GenericSig _ op_ty) = discardResult (tcHsLiftedType op_ty)
437     kc_sig _                    = return ()
438
439 kcTyClDecl (ForeignType {}) = return ()
440 kcTyClDecl (TyFamily {})    = return ()
441
442 -------------------
443 kcConDecl :: ConDecl Name -> TcM ()
444 kcConDecl (ConDecl { con_name = name, con_qvars = ex_tvs
445                    , con_cxt = ex_ctxt, con_details = details, con_res = res })
446   = addErrCtxt (dataConCtxt name) $
447     kcHsTyVarBndrs False ex_tvs $ \ _ -> 
448     do { _ <- tcHsContext ex_ctxt
449        ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
450        ; _ <- tcConRes res
451        ; return () }
452 \end{code}
453
454 Note [ARecDataCon: Recusion and promoting data constructors]
455 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
456 We don't want to allow promotion in a strongly connected component
457 when kind checking.
458
459 Consider:
460   data T f = K (f (K Any))
461
462 When kind checking the `data T' declaration the local env contains the
463 mappings:
464   T -> AThing <some initial kind>
465   K -> ARecDataCon
466
467 ANothing is only used for DataCons, and only used during type checking
468 in tcTyClGroup.
469
470
471 %************************************************************************
472 %*                                                                      *
473 \subsection{Type checking}
474 %*                                                                      *
475 %************************************************************************
476
477 Note [Type checking recursive type and class declarations]
478 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
479 At this point we have completed *kind-checking* of a mutually
480 recursive group of type/class decls (done in kcTyClGroup). However,
481 we discarded the kind-checked types (eg RHSs of data type decls); 
482 note that kcTyClDecl returns ().  There are two reasons:
483
484   * It's convenient, because we don't have to rebuild a
485     kinded HsDecl (a fairly elaborate type)
486
487   * It's necessary, because after kind-generalisation, the
488     TyCons/Classes may now be kind-polymorphic, and hence need
489     to be given kind arguments.  
490
491 Example:
492        data T f a = MkT (f a) (T f a)
493 During kind-checking, we give T the kind T :: k1 -> k2 -> *
494 and figure out constraints on k1, k2 etc. Then we generalise
495 to get   T :: forall k. (k->*) -> k -> *
496 So now the (T f a) in the RHS must be elaborated to (T k f a).
497     
498 However, during tcTyClDecl of T (above) we will be in a recursive
499 "knot". So we aren't allowed to look at the TyCon T itself; we are only
500 allowed to put it (lazily) in the returned structures.  But when
501 kind-checking the RHS of T's decl, we *do* need to know T's kind (so
502 that we can correctly elaboarate (T k f a).  How can we get T's kind
503 without looking at T?  Delicate answer: during tcTyClDecl, we extend
504
505   *Global* env with T -> ATyCon (the (not yet built) TyCon for T)
506   *Local*  env with T -> AThing (polymorphic kind of T)
507
508 Then:
509
510   * During TcHsType.kcTyVar we look in the *local* env, to get the
511     known kind for T.
512
513   * But in TcHsType.ds_type (and ds_var_app in particular) we look in
514     the *global* env to get the TyCon. But we must be careful not to
515     force the TyCon or we'll get a loop.
516
517 This fancy footwork (with two bindings for T) is only necesary for the
518 TyCons or Classes of this recursive group.  Earlier, finished groups,
519 live in the global env only.
520
521 \begin{code}
522 tcTyClDecl :: (Name -> RecFlag) -> LTyClDecl Name -> TcM [TyThing]
523 tcTyClDecl calc_isrec (L loc decl)
524   = setSrcSpan loc $ tcAddDeclCtxt decl $
525     traceTc "tcTyAndCl-x" (ppr decl) >>
526     tcTyClDecl1 NoParentTyCon calc_isrec decl
527
528   -- "type family" declarations
529 tcTyClDecl1 :: TyConParent -> (Name -> RecFlag) -> TyClDecl Name -> TcM [TyThing]
530 tcTyClDecl1 parent _calc_isrec
531             (TyFamily {tcdFlavour = TypeFamily, tcdLName = L _ tc_name, tcdTyVars = tvs})
532   = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
533   { traceTc "type family:" (ppr tc_name)
534   ; checkFamFlag tc_name
535   ; tycon <- buildSynTyCon tc_name tvs' SynFamilyTyCon kind parent
536   ; return [ATyCon tycon] }
537
538   -- "data family" declaration
539 tcTyClDecl1 parent _calc_isrec
540               (TyFamily {tcdFlavour = DataFamily, tcdLName = L _ tc_name, tcdTyVars = tvs})
541   = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
542   { traceTc "data family:" (ppr tc_name)
543   ; checkFamFlag tc_name
544   ; extra_tvs <- tcDataKindSig kind
545   ; let final_tvs = tvs' ++ extra_tvs    -- we may not need these
546         tycon = buildAlgTyCon tc_name final_tvs Nothing []
547                               DataFamilyTyCon Recursive True parent
548   ; return [ATyCon tycon] }
549
550   -- "type" synonym declaration
551 tcTyClDecl1 _parent calc_isrec
552             (TyDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdTyDefn = defn })
553
554   = ASSERT( isNoParent _parent )
555     tcTyClTyVars tc_name tvs $ \ tvs' kind -> 
556     tcTyDefn calc_isrec tc_name tvs' kind defn
557
558 tcTyClDecl1 _parent calc_isrec
559             (ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs
560             , tcdCtxt = ctxt, tcdMeths = meths
561             , tcdFDs = fundeps, tcdSigs = sigs
562             , tcdATs = ats, tcdATDefs = at_defs })
563   = ASSERT( isNoParent _parent )
564     do 
565   { (tvs', ctxt', fds', sig_stuff, gen_dm_env)
566        <- tcTyClTyVars class_name tvs $ \ tvs' kind -> do
567           { MASSERT( isConstraintKind kind )
568
569           ; ctxt' <- tcHsContext ctxt
570           ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'  
571                      -- Squeeze out any kind unification variables
572
573           ; fds'  <- mapM (addLocM tc_fundep) fundeps
574           ; (sig_stuff, gen_dm_env) <- tcClassSigs class_name sigs meths
575           ; return (tvs', ctxt', fds', sig_stuff, gen_dm_env) }
576
577   ; clas <- fixM $ \ clas -> do
578             { let       -- This little knot is just so we can get
579                         -- hold of the name of the class TyCon, which we
580                         -- need to look up its recursiveness
581                     tycon_name = tyConName (classTyCon clas)
582                     tc_isrec = calc_isrec tycon_name
583
584             ; at_stuff <- tcClassATs class_name (AssocFamilyTyCon clas) ats at_defs
585
586             ; buildClass False {- Must include unfoldings for selectors -}
587                          class_name tvs' ctxt' fds' at_stuff
588                          sig_stuff tc_isrec }
589
590   ; let gen_dm_ids = [ AnId (mkExportedLocalId gen_dm_name gen_dm_ty)
591                      | (sel_id, GenDefMeth gen_dm_name) <- classOpItems clas
592                      , let gen_dm_tau = expectJust "tcTyClDecl1" $
593                                         lookupNameEnv gen_dm_env (idName sel_id)
594                      , let gen_dm_ty = mkSigmaTy tvs' 
595                                                  [mkClassPred clas (mkTyVarTys tvs')] 
596                                                  gen_dm_tau
597                      ]
598         class_ats = map ATyCon (classATs clas)
599
600   ; return (ATyCon (classTyCon clas) : gen_dm_ids ++ class_ats )
601       -- NB: Order is important due to the call to `mkGlobalThings' when
602       --     tying the the type and class declaration type checking knot.
603   }
604   where
605     tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tcLookupTyVar tvs1 ;
606                                 ; tvs2' <- mapM tcLookupTyVar tvs2 ;
607                                 ; return (tvs1', tvs2') }
608
609 tcTyClDecl1 _ _
610   (ForeignType {tcdLName = L _ tc_name, tcdExtName = tc_ext_name})
611   = return [ATyCon (mkForeignTyCon tc_name tc_ext_name liftedTypeKind 0)]
612 \end{code}
613
614 \begin{code}
615 tcTyDefn :: (Name -> RecFlag) -> Name   
616          -> [TyVar] -> Kind
617          -> HsTyDefn Name -> TcM [TyThing]
618   -- NB: not used for newtype/data instances (whether associated or not)
619 tcTyDefn _calc_isrec tc_name tvs kind (TySynonym { td_synRhs = hs_ty })
620   = do { env <- getLclEnv
621        ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
622        ; rhs_ty <- tcCheckLHsType hs_ty kind
623        ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
624        ; tycon <- buildSynTyCon tc_name tvs (SynonymTyCon rhs_ty)
625                                 kind NoParentTyCon
626        ; return [ATyCon tycon] }
627
628 tcTyDefn calc_isrec tc_name tvs kind
629          (TyData { td_ND = new_or_data, td_cType = cType
630                  , td_ctxt = ctxt, td_kindSig = mb_ksig
631                  , td_cons = cons })
632   = do { extra_tvs <- tcDataKindSig kind
633        ; let is_rec     = calc_isrec tc_name
634              h98_syntax = consUseH98Syntax cons
635              final_tvs  = tvs ++ extra_tvs
636        ; stupid_theta <- tcHsContext ctxt
637        ; kind_signatures <- xoptM Opt_KindSignatures
638        ; existential_ok  <- xoptM Opt_ExistentialQuantification
639        ; gadt_ok         <- xoptM Opt_GADTs
640        ; is_boot         <- tcIsHsBoot  -- Are we compiling an hs-boot file?
641        ; let ex_ok = existential_ok || gadt_ok  -- Data cons can have existential context
642
643              -- Check that we don't use kind signatures without Glasgow extensions
644        ; 
645        ; case mb_ksig of
646            Nothing   -> return ()
647            Just hs_k -> do { checkTc (kind_signatures) (badSigTyDecl tc_name)
648                            ; tc_kind <- tcLHsKind hs_k
649                            ; _ <- unifyKind kind tc_kind
650                            ; return () }
651
652        ; dataDeclChecks tc_name new_or_data stupid_theta cons
653
654        ; tycon <- fixM $ \ tycon -> do
655              { let res_ty = mkTyConApp tycon (mkTyVarTys final_tvs)
656              ; data_cons <- tcConDecls new_or_data ex_ok tycon (final_tvs, res_ty) cons
657              ; tc_rhs <-
658                  if null cons && is_boot              -- In a hs-boot file, empty cons means
659                  then return totallyAbstractTyConRhs  -- "don't know"; hence totally Abstract
660                  else case new_or_data of
661                    DataType -> return (mkDataTyConRhs data_cons)
662                    NewType  -> ASSERT( not (null data_cons) )
663                                     mkNewTyConRhs tc_name tycon (head data_cons)
664              ; return (buildAlgTyCon tc_name final_tvs cType stupid_theta tc_rhs
665                                      is_rec (not h98_syntax) NoParentTyCon) }
666        ; return [ATyCon tycon] }
667 \end{code}
668
669 %************************************************************************
670 %*                                                                      *
671                Typechecking associated types (in class decls)
672                (including the associated-type defaults)
673 %*                                                                      *
674 %************************************************************************
675
676 Note [Associated type defaults]
677 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
678
679 The following is an example of associated type defaults:
680              class C a where
681                data D a 
682
683                type F a b :: *
684                type F a Z = [a]        -- Default
685                type F a (S n) = F a n  -- Default
686
687 Note that:
688   - We can have more than one default definition for a single associated type,
689     as long as they do not overlap (same rules as for instances)
690   - We can get default definitions only for type families, not data families
691
692 \begin{code}
693 tcClassATs :: Name             -- The class name (not knot-tied)
694            -> TyConParent      -- The class parent of this associated type
695            -> [LTyClDecl Name] -- Associated types. All FamTyCon
696            -> [LFamInstDecl Name] -- Associated type defaults. All SynTyCon
697            -> TcM [ClassATItem]
698 tcClassATs class_name parent ats at_defs
699   = do {  -- Complain about associated type defaults for non associated-types
700          sequence_ [ failWithTc (badATErr class_name n)
701                    | L _ n <- map (fid_tycon . unLoc) at_defs
702                    , not (n `elemNameSet` at_names) ]
703        ; mapM tc_at ats }
704   where
705     at_names = mkNameSet (map (tcdName . unLoc) ats)
706
707     at_defs_map :: NameEnv [LFamInstDecl Name]
708     -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'
709     at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv 
710                                               (famInstDeclName at_def) [at_def]) 
711                         emptyNameEnv at_defs
712
713     tc_at at = do { [ATyCon fam_tc] <- addLocM (tcTyClDecl1 parent
714                                                            (const Recursive)) at
715                   ; let at_defs = lookupNameEnv at_defs_map (tcdName (unLoc at))
716                                         `orElse` []
717                   ; atd <- mapM (tcDefaultAssocDecl fam_tc) at_defs
718                   ; return (fam_tc, atd) }
719
720 -------------------------
721 tcDefaultAssocDecl :: TyCon              -- ^ Family TyCon
722                    -> LFamInstDecl Name  -- ^ RHS
723                    -> TcM ATDefault      -- ^ Type checked RHS and free TyVars
724 tcDefaultAssocDecl fam_tc (L loc decl)
725   = setSrcSpan loc $
726     tcAddFamInstCtxt decl $
727     do { traceTc "tcDefaultAssocDecl" (ppr decl)
728        ; (at_tvs, at_tys, at_rhs) <- tcSynFamInstDecl fam_tc decl
729        ; return (ATD at_tvs at_tys at_rhs loc) }
730 -- We check for well-formedness and validity later, in checkValidClass
731
732 -------------------------
733 tcSynFamInstDecl :: TyCon -> FamInstDecl Name -> TcM ([TyVar], [Type], Type)
734 -- Placed here because type family instances appear as 
735 -- default decls in class declarations 
736 tcSynFamInstDecl fam_tc 
737     (FamInstDecl { fid_pats = pats, fid_defn = defn@(TySynonym { td_synRhs = hs_ty }) })
738   = do { checkTc (isSynTyCon fam_tc) (wrongKindOfFamily fam_tc)
739        ; tcFamTyPats fam_tc pats (kcTyDefn defn) $ \tvs' pats' res_kind -> 
740     do { rhs_ty <- tcCheckLHsType hs_ty res_kind
741        ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
742        ; traceTc "tcSynFamInstDecl" (ppr fam_tc <+> (ppr tvs' $$ ppr pats' $$ ppr rhs_ty))
743        ; return (tvs', pats', rhs_ty) } }
744
745 tcSynFamInstDecl _ decl = pprPanic "tcSynFamInstDecl" (ppr decl)
746
747 kcTyDefn :: HsTyDefn Name -> TcKind -> TcM ()
748 -- Used for 'data instance' and 'type instance' only
749 -- Ordinary 'data' and 'type' are handed by kcTyClDec and kcSynDecls resp
750 kcTyDefn (TyData { td_ctxt = ctxt, td_cons = cons, td_kindSig = mb_kind }) res_k
751   = do  { _ <- tcHsContext ctxt
752         ; mapM_ (wrapLocM kcConDecl) cons
753         ; kcResultKind mb_kind res_k }
754
755 kcTyDefn (TySynonym { td_synRhs = rhs_ty }) res_k
756   = discardResult (tcCheckLHsType rhs_ty res_k)
757
758 ------------------
759 kcResultKind :: Maybe (LHsKind Name) -> Kind -> TcM ()
760 kcResultKind Nothing res_k
761   = discardResult (unifyKind res_k liftedTypeKind)
762       --             type family F a 
763       -- defaults to type family F a :: *
764 kcResultKind (Just k ) res_k
765   = do { k' <- tcLHsKind k
766        ; discardResult (unifyKind k' res_k) }
767
768 -------------------------
769 -- Kind check type patterns and kind annotate the embedded type variables.
770 --     type instance F [a] = rhs
771 --
772 -- * Here we check that a type instance matches its kind signature, but we do
773 --   not check whether there is a pattern for each type index; the latter
774 --   check is only required for type synonym instances.
775
776 -----------------
777 tcFamTyPats :: TyCon
778             -> HsWithBndrs [LHsType Name] -- Patterns
779             -> (TcKind -> TcM ())       -- Kind checker for RHS
780                                         -- result is ignored
781             -> ([TKVar] -> [TcType] -> Kind -> TcM a)
782             -> TcM a
783 -- Check the type patterns of a type or data family instance
784 --     type instance F <pat1> <pat2> = <type>
785 -- The 'tyvars' are the free type variables of pats
786 -- 
787 -- NB: The family instance declaration may be an associated one,
788 -- nested inside an instance decl, thus
789 --        instance C [a] where
790 --          type F [a] = ...
791 -- In that case, the type variable 'a' will *already be in scope*
792 -- (and, if C is poly-kinded, so will its kind parameter).
793
794 tcFamTyPats fam_tc (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars }) 
795             kind_checker thing_inside
796   = do { -- A family instance must have exactly the same number of type
797          -- parameters as the family declaration.  You can't write
798          --     type family F a :: * -> *
799          --     type instance F Int y = y
800          -- because then the type (F Int) would be like (\y.y)
801        ; let (fam_kvs, fam_body) = splitForAllTys (tyConKind fam_tc)
802              fam_arity = tyConArity fam_tc - length fam_kvs
803        ; checkTc (length arg_pats == fam_arity) $
804                  wrongNumberOfParmsErr fam_arity
805
806          -- Instantiate with meta kind vars
807        ; fam_arg_kinds <- mapM (const newMetaKindVar) fam_kvs
808        ; loc <- getSrcSpanM
809        ; let (arg_kinds, res_kind) 
810                  = splitKindFunTysN fam_arity $
811                    substKiWith fam_kvs fam_arg_kinds fam_body
812              hs_tvs = HsQTvs { hsq_kvs = kvars
813                              , hsq_tvs = userHsTyVarBndrs loc tvars }
814
815          -- Kind-check and quantify
816          -- See Note [Quantifying over family patterns]
817        ; typats <- tcHsTyVarBndrs hs_tvs $ \ _ ->
818                    do { kind_checker res_kind
819                       ; tcHsArgTys (quotes (ppr fam_tc)) arg_pats arg_kinds }
820        ; let all_args = fam_arg_kinds ++ typats
821
822             -- Find free variables (after zonking)
823        ; tkvs <- zonkTyVarsAndFV (tyVarsOfTypes all_args)
824
825             -- Turn them into skolems, so that we don't subsequently 
826             -- replace a meta kind var with AnyK
827        ; qtkvs <- zonkQuantifiedTyVars (varSetElems tkvs)
828
829             -- Zonk the patterns etc into the Type world
830        ; (ze, qtkvs') <- zonkTyBndrsX emptyZonkEnv qtkvs
831        ; all_args'    <- zonkTcTypeToTypes ze all_args
832        ; res_kind'    <- zonkTcTypeToType  ze res_kind
833
834        ; traceTc "tcFamPats" (pprTvBndrs qtkvs' $$ ppr all_args' $$ ppr res_kind')
835        ; tcExtendTyVarEnv qtkvs' $
836          thing_inside qtkvs' all_args' res_kind' }
837 \end{code}
838
839 Note [Quantifying over family patterns]
840 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
841 We need to quantify over two different lots of kind variables:
842
843 First, the ones that come from the kinds of the tyvar args of 
844 tcTyVarBndrsKindGen, as usual
845   data family Dist a 
846
847   -- Proxy :: forall k. k -> *
848   data instance Dist (Proxy a) = DP
849   -- Generates  data DistProxy = DP
850   --            ax8 k (a::k) :: Dist * (Proxy k a) ~ DistProxy k a
851   -- The 'k' comes from the tcTyVarBndrsKindGen (a::k)
852
853 Second, the ones that come from the kind argument of the type family
854 which we pick up using the (tyVarsOfTypes typats) in the result of 
855 the thing_inside of tcHsTyvarBndrsGen.
856   -- Any :: forall k. k
857   data instance Dist Any = DA
858   -- Generates  data DistAny k = DA
859   --            ax7 k :: Dist k (Any k) ~ DistAny k 
860   -- The 'k' comes from kindGeneralizeKinds (Any k)
861
862 Note [Quantified kind variables of a family pattern]
863 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
864 Consider   type family KindFam (p :: k1) (q :: k1)
865            data T :: Maybe k1 -> k2 -> *
866            type instance KindFam (a :: Maybe k) b = T a b -> Int
867 The HsBSig for the family patterns will be ([k], [a])
868
869 Then in the family instance we want to
870   * Bring into scope [ "k" -> k:BOX, "a" -> a:k ]
871   * Kind-check the RHS
872   * Quantify the type instance over k and k', as well as a,b, thus
873        type instance [k, k', a:Maybe k, b:k'] 
874                      KindFam (Maybe k) k' a b = T k k' a b -> Int
875
876 Notice that in the third step we quantify over all the visibly-mentioned
877 type variables (a,b), but also over the implicitly mentioned kind varaibles
878 (k, k').  In this case one is bound explicitly but often there will be 
879 none. The role of the kind signature (a :: Maybe k) is to add a constraint
880 that 'a' must have that kind, and to bring 'k' into scope.
881
882 Note [Associated type instances]
883 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
884 We allow this:
885   class C a where
886     type T x a
887   instance C Int where
888     type T (S y) Int = y
889     type T Z     Int = Char
890
891 Note that 
892   a) The variable 'x' is not bound by the class decl
893   b) 'x' is instantiated to a non-type-variable in the instance
894   c) There are several type instance decls for T in the instance
895
896 All this is fine.  Of course, you can't give any *more* instances
897 for (T ty Int) elsewhere, becuase it's an *associated* type.
898
899 Note [Checking consistent instantiation]
900 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
901   class C a b where
902     type T a x b
903
904   instance C [p] Int
905     type T [p] y Int = (p,y,y)  -- Induces the family instance TyCon
906                                 --    type TR p y = (p,y,y)
907
908 So we 
909   * Form the mini-envt from the class type variables a,b
910     to the instance decl types [p],Int:   [a->[p], b->Int]
911
912   * Look at the tyvars a,x,b of the type family constructor T
913     (it shares tyvars with the class C)
914
915   * Apply the mini-evnt to them, and check that the result is
916     consistent with the instance types [p] y Int
917
918
919 %************************************************************************
920 %*                                                                      *
921                Data types
922 %*                                                                      *
923 %************************************************************************
924
925 \begin{code}
926 dataDeclChecks :: Name -> NewOrData -> ThetaType -> [LConDecl Name] -> TcM ()
927 dataDeclChecks tc_name new_or_data stupid_theta cons
928   = do {   -- Check that we don't use GADT syntax in H98 world
929          gadtSyntax_ok <- xoptM Opt_GADTSyntax
930        ; let h98_syntax = consUseH98Syntax cons
931        ; checkTc (gadtSyntax_ok || h98_syntax) (badGadtDecl tc_name)
932
933            -- Check that the stupid theta is empty for a GADT-style declaration
934        ; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
935
936          -- Check that a newtype has exactly one constructor
937          -- Do this before checking for empty data decls, so that
938          -- we don't suggest -XEmptyDataDecls for newtypes
939        ; checkTc (new_or_data == DataType || isSingleton cons) 
940                 (newtypeConError tc_name (length cons))
941
942                 -- Check that there's at least one condecl,
943          -- or else we're reading an hs-boot file, or -XEmptyDataDecls
944        ; empty_data_decls <- xoptM Opt_EmptyDataDecls
945        ; is_boot <- tcIsHsBoot  -- Are we compiling an hs-boot file?
946        ; checkTc (not (null cons) || empty_data_decls || is_boot)
947                  (emptyConDeclsErr tc_name) }
948     
949 -----------------------------------
950 tcConDecls :: NewOrData -> Bool -> TyCon -> ([TyVar], Type)
951            -> [LConDecl Name] -> TcM [DataCon]
952 tcConDecls new_or_data ex_ok rep_tycon res_tmpl cons
953   = mapM (addLocM (tcConDecl new_or_data ex_ok rep_tycon res_tmpl)) cons
954
955 tcConDecl :: NewOrData
956           -> Bool               -- True <=> -XExistentialQuantificaton or -XGADTs
957           -> TyCon              -- Representation tycon
958           -> ([TyVar], Type)    -- Return type template (with its template tyvars)
959           -> ConDecl Name 
960           -> TcM DataCon
961
962 tcConDecl new_or_data existential_ok rep_tycon res_tmpl         -- Data types
963           con@(ConDecl { con_name = name
964                        , con_qvars = hs_tvs, con_cxt = hs_ctxt
965                        , con_details = hs_details, con_res = hs_res_ty })
966   = addErrCtxt (dataConCtxt name) $
967     do { traceTc "tcConDecl 1" (ppr name)
968        ; (tvs, ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts) 
969            <- tcHsTyVarBndrs hs_tvs $ \ tvs ->
970               do { ctxt    <- tcHsContext hs_ctxt
971                  ; details <- tcConArgs new_or_data hs_details
972                  ; res_ty  <- tcConRes hs_res_ty
973                  ; let (is_infix, field_lbls, btys) = details
974                        (arg_tys, stricts)           = unzip btys
975                  ; return (tvs, ctxt, arg_tys, res_ty, is_infix, field_lbls, stricts) }
976
977        ; let pretend_res_ty = case res_ty of
978                                 ResTyH98     -> unitTy
979                                 ResTyGADT ty -> ty
980              pretend_con_ty = mkSigmaTy tvs ctxt (mkFunTys arg_tys pretend_res_ty)
981                 -- This pretend_con_ty stuff is just a convenient way to get the
982                 -- free kind variables of the type, for kindGeneralize to work on
983
984              -- Generalise the kind variables (returning quantifed TcKindVars)
985              -- and quanify the type variables (substiting their kinds)
986        ; kvs <- kindGeneralize (tyVarsOfType pretend_con_ty) (map getName tvs)
987        ; tvs <- zonkQuantifiedTyVars tvs
988
989              -- Zonk to Types
990        ; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv (kvs ++ tvs)
991        ; arg_tys <- zonkTcTypeToTypes ze arg_tys
992        ; ctxt    <- zonkTcTypeToTypes ze ctxt
993        ; res_ty  <- case res_ty of
994                       ResTyH98     -> return ResTyH98
995                       ResTyGADT ty -> ResTyGADT <$> zonkTcTypeToType ze ty
996
997        ; checkTc (existential_ok || conRepresentibleWithH98Syntax con)
998                  (badExistential name)
999
1000        ; let (univ_tvs, ex_tvs, eq_preds, res_ty')
1001                 = rejigConRes res_tmpl qtkvs res_ty
1002
1003        ; traceTc "tcConDecl 3" (ppr name)
1004        ; buildDataCon (unLoc name) is_infix
1005                       stricts field_lbls
1006                       univ_tvs ex_tvs eq_preds ctxt arg_tys
1007                       res_ty' rep_tycon
1008                 -- NB:  we put data_tc, the type constructor gotten from the
1009                 --      constructor type signature into the data constructor;
1010                 --      that way checkValidDataCon can complain if it's wrong.
1011        }
1012
1013 tcConArgs :: NewOrData -> HsConDeclDetails Name -> TcM (Bool, [Name], [(TcType, HsBang)])
1014 tcConArgs new_or_data (PrefixCon btys)     
1015   = do { btys' <- mapM (tcConArg new_or_data) btys
1016        ; return (False, [], btys') }
1017 tcConArgs new_or_data (InfixCon bty1 bty2) 
1018   = do { bty1' <- tcConArg new_or_data bty1
1019        ; bty2' <- tcConArg new_or_data bty2
1020        ; return (True, [], [bty1', bty2']) }
1021 tcConArgs new_or_data (RecCon fields)
1022   = do { btys' <- mapM (tcConArg new_or_data) btys
1023        ; return (False, field_names, btys') }
1024   where
1025     field_names = map (unLoc . cd_fld_name) fields
1026     btys        = map cd_fld_type fields
1027
1028 tcConArg :: NewOrData -> LHsType Name -> TcM (TcType, HsBang)
1029 tcConArg new_or_data bty
1030   = do  { traceTc "tcConArg 1" (ppr bty)
1031         ; arg_ty <- tcHsConArgType new_or_data bty
1032         ; traceTc "tcConArg 2" (ppr bty)
1033         ; strict_mark <- chooseBoxingStrategy arg_ty (getBangStrictness bty)
1034         ; return (arg_ty, strict_mark) }
1035
1036 tcConRes :: ResType (LHsType Name) -> TcM (ResType Type)
1037 tcConRes ResTyH98           = return ResTyH98
1038 tcConRes (ResTyGADT res_ty) = do { res_ty' <- tcHsLiftedType res_ty
1039                                  ; return (ResTyGADT res_ty') }
1040
1041 -- Example
1042 --   data instance T (b,c) where 
1043 --      TI :: forall e. e -> T (e,e)
1044 --
1045 -- The representation tycon looks like this:
1046 --   data :R7T b c where 
1047 --      TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
1048 -- In this case orig_res_ty = T (e,e)
1049
1050 rejigConRes :: ([TyVar], Type)  -- Template for result type; e.g.
1051                                 -- data instance T [a] b c = ...  
1052                                 --      gives template ([a,b,c], T [a] b c)
1053              -> [TyVar]         -- where MkT :: forall x y z. ...
1054              -> ResType Type
1055              -> ([TyVar],               -- Universal
1056                  [TyVar],               -- Existential (distinct OccNames from univs)
1057                  [(TyVar,Type)],        -- Equality predicates
1058                  Type)          -- Typechecked return type
1059         -- We don't check that the TyCon given in the ResTy is
1060         -- the same as the parent tycon, because we are in the middle
1061         -- of a recursive knot; so it's postponed until checkValidDataCon
1062
1063 rejigConRes (tmpl_tvs, res_ty) dc_tvs ResTyH98
1064   = (tmpl_tvs, dc_tvs, [], res_ty)
1065         -- In H98 syntax the dc_tvs are the existential ones
1066         --      data T a b c = forall d e. MkT ...
1067         -- The {a,b,c} are tc_tvs, and {d,e} are dc_tvs
1068
1069 rejigConRes (tmpl_tvs, res_tmpl) dc_tvs (ResTyGADT res_ty)
1070         -- E.g.  data T [a] b c where
1071         --         MkT :: forall x y z. T [(x,y)] z z
1072         -- Then we generate
1073         --      Univ tyvars     Eq-spec
1074         --          a              a~(x,y)
1075         --          b              b~z
1076         --          z              
1077         -- Existentials are the leftover type vars: [x,y]
1078         -- So we return ([a,b,z], [x,y], [a~(x,y),b~z], T [(x,y)] z z)
1079   = (univ_tvs, ex_tvs, eq_spec, res_ty)
1080   where
1081     Just subst = tcMatchTy (mkVarSet tmpl_tvs) res_tmpl res_ty
1082                 -- This 'Just' pattern is sure to match, because if not
1083                 -- checkValidDataCon will complain first. The 'subst'
1084                 -- should not be looked at until after checkValidDataCon
1085                 -- We can't check eagerly because we are in a "knot" in 
1086                 -- which 'tycon' is not yet fully defined
1087
1088                 -- /Lazily/ figure out the univ_tvs etc
1089                 -- Each univ_tv is either a dc_tv or a tmpl_tv
1090     (univ_tvs, eq_spec) = foldr choose ([], []) tmpl_tvs
1091     choose tmpl (univs, eqs)
1092       | Just ty <- lookupTyVar subst tmpl 
1093       = case tcGetTyVar_maybe ty of
1094           Just tv | not (tv `elem` univs)
1095             -> (tv:univs,   eqs)
1096           _other  -> (new_tmpl:univs, (new_tmpl,ty):eqs)
1097                      where  -- see Note [Substitution in template variables kinds]
1098                        new_tmpl = updateTyVarKind (substTy subst) tmpl
1099       | otherwise = pprPanic "tcResultType" (ppr res_ty)
1100     ex_tvs = dc_tvs `minusList` univ_tvs
1101
1102
1103 {-
1104 Note [Substitution in template variables kinds]
1105 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1106
1107 data List a = Nil | Cons a (List a)
1108 data SList s as where
1109   SNil :: SList s Nil
1110
1111 We call tcResultType with
1112   tmpl_tvs = [(k :: BOX), (s :: k -> *), (as :: List k)]
1113   res_tmpl = SList k s as
1114   res_ty = ResTyGADT (SList k1 (s1 :: k1 -> *) (Nil k1))
1115
1116 We get subst:
1117   k -> k1
1118   s -> s1
1119   as -> Nil k1
1120
1121 Now we want to find out the universal variables and the equivalences
1122 between some of them and types (GADT).
1123
1124 In this example, k and s are mapped to exactly variables which are not
1125 already present in the universal set, so we just add them without any
1126 coercion.
1127
1128 But 'as' is mapped to 'Nil k1', so we add 'as' to the universal set,
1129 and add the equivalence with 'Nil k1' in 'eqs'.
1130
1131 The problem is that with kind polymorphism, as's kind may now contain
1132 kind variables, and we have to apply the template substitution to it,
1133 which is why we create new_tmpl.
1134
1135 The template substitution only maps kind variables to kind variables,
1136 since GADTs are not kind indexed.
1137
1138 -}
1139
1140
1141 consUseH98Syntax :: [LConDecl a] -> Bool
1142 consUseH98Syntax (L _ (ConDecl { con_res = ResTyGADT _ }) : _) = False
1143 consUseH98Syntax _                                             = True
1144                  -- All constructors have same shape
1145
1146 conRepresentibleWithH98Syntax :: ConDecl Name -> Bool
1147 conRepresentibleWithH98Syntax
1148     (ConDecl {con_qvars = tvs, con_cxt = ctxt, con_res = ResTyH98 })
1149         = null (hsQTvBndrs tvs) && null (unLoc ctxt)
1150 conRepresentibleWithH98Syntax
1151     (ConDecl {con_qvars = tvs, con_cxt = ctxt, con_res = ResTyGADT (L _ t) })
1152         = null (unLoc ctxt) && f t (hsLTyVarNames tvs)
1153     where -- Each type variable should be used exactly once in the
1154           -- result type, and the result type must just be the type
1155           -- constructor applied to type variables
1156           f (HsAppTy (L _ t1) (L _ (HsTyVar v2))) vs
1157               = (v2 `elem` vs) && f t1 (delete v2 vs)
1158           f (HsTyVar _) [] = True
1159           f _ _ = False
1160
1161 -------------------
1162
1163 -- We attempt to unbox/unpack a strict field when either:
1164 --   (i)  The field is marked '!!', or
1165 --   (ii) The field is marked '!', and the -funbox-strict-fields flag is on.
1166 --
1167 -- We have turned off unboxing of newtypes because coercions make unboxing 
1168 -- and reboxing more complicated
1169 chooseBoxingStrategy :: TcType -> HsBang -> TcM HsBang
1170 chooseBoxingStrategy arg_ty bang
1171   = case bang of
1172         HsNoBang -> return HsNoBang
1173         HsStrict -> do { unbox_strict <- doptM Opt_UnboxStrictFields
1174                        ; if unbox_strict then return (can_unbox HsStrict arg_ty)
1175                                          else return HsStrict }
1176         HsNoUnpack -> return HsStrict
1177         HsUnpack -> do { omit_prags <- doptM Opt_OmitInterfacePragmas
1178                        ; let bang = can_unbox HsUnpackFailed arg_ty
1179                        ; if omit_prags && bang == HsUnpack
1180                             then return HsStrict
1181                             else return bang }
1182             -- Do not respect UNPACK pragmas if OmitInterfacePragmas is on
1183             -- See Trac #5252: unpacking means we must not conceal the
1184             --                 representation of the argument type
1185             -- However: even when OmitInterfacePragmas is on, we still want
1186             -- to know if we have HsUnpackFailed, because we omit a
1187             -- warning in that case (#3966)
1188         HsUnpackFailed -> pprPanic "chooseBoxingStrategy" (ppr arg_ty)
1189                           -- Source code never has shtes
1190   where
1191     can_unbox :: HsBang -> TcType -> HsBang
1192     -- Returns   HsUnpack  if we can unpack arg_ty
1193     --           fail_bang if we know what arg_ty is but we can't unpack it
1194     --           HsStrict  if it's abstract, so we don't know whether or not we can unbox it
1195     can_unbox fail_bang arg_ty 
1196        = case splitTyConApp_maybe arg_ty of
1197             Nothing -> fail_bang
1198
1199             Just (arg_tycon, tycon_args) 
1200               | isAbstractTyCon arg_tycon -> HsStrict   
1201                       -- See Note [Don't complain about UNPACK on abstract TyCons]
1202               | not (isRecursiveTyCon arg_tycon)        -- Note [Recusive unboxing]
1203               , isProductTyCon arg_tycon 
1204                     -- We can unbox if the type is a chain of newtypes 
1205                     -- with a product tycon at the end
1206               -> if isNewTyCon arg_tycon 
1207                  then can_unbox fail_bang (newTyConInstRhs arg_tycon tycon_args)
1208                  else HsUnpack
1209
1210               | otherwise -> fail_bang
1211 \end{code}
1212
1213 Note [Don't complain about UNPACK on abstract TyCons]
1214 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1215 We are going to complain about UnpackFailed, but if we say
1216    data T = MkT {-# UNPACK #-} !Wobble
1217 and Wobble is a newtype imported from a module that was compiled 
1218 without optimisation, we don't want to complain. Because it might
1219 be fine when optimsation is on.  I think this happens when Haddock
1220 is working over (say) GHC souce files.
1221
1222 Note [Recursive unboxing]
1223 ~~~~~~~~~~~~~~~~~~~~~~~~~
1224 Be careful not to try to unbox this!
1225         data T = MkT {-# UNPACK #-} !T Int
1226 Reason: consider
1227   data R = MkR {-# UNPACK #-} !S Int
1228   data S = MkS {-# UNPACK #-} !Int
1229 The representation arguments of MkR are the *representation* arguments
1230 of S (plus Int); the rep args of MkS are Int#.  This is obviously no
1231 good for T, because then we'd get an infinite number of arguments.
1232
1233 But it's the *argument* type that matters. This is fine:
1234         data S = MkS S !Int
1235 because Int is non-recursive.
1236
1237
1238 %************************************************************************
1239 %*                                                                      *
1240                 Validity checking
1241 %*                                                                      *
1242 %************************************************************************
1243
1244 Validity checking is done once the mutually-recursive knot has been
1245 tied, so we can look at things freely.
1246
1247 \begin{code}
1248 checkClassCycleErrs :: Class -> TcM ()
1249 checkClassCycleErrs cls
1250   = unless (null cls_cycles) $ mapM_ recClsErr cls_cycles
1251   where cls_cycles = calcClassCycles cls
1252
1253 checkValidTyCl :: TyClDecl Name -> TcM ()
1254 -- We do the validity check over declarations, rather than TyThings
1255 -- only so that we can add a nice context with tcAddDeclCtxt
1256 checkValidTyCl decl
1257   = tcAddDeclCtxt decl $
1258     do  { traceTc "Validity of 1" (ppr decl)
1259         ; env <- getGblEnv
1260         ; traceTc "Validity of 1a" (ppr (tcg_type_env env))
1261         ; thing <- tcLookupLocatedGlobal (tcdLName decl)
1262         ; traceTc "Validity of 2" (ppr decl)
1263         ; traceTc "Validity of" (ppr thing)
1264         ; case thing of
1265             ATyCon tc -> do
1266                 traceTc "  of kind" (ppr (tyConKind tc))
1267                 checkValidTyCon tc
1268             AnId _    -> return ()  -- Generic default methods are checked
1269                                     -- with their parent class
1270             _         -> panic "checkValidTyCl"
1271         ; traceTc "Done validity of" (ppr thing)        
1272         }
1273
1274 -------------------------
1275 -- For data types declared with record syntax, we require
1276 -- that each constructor that has a field 'f' 
1277 --      (a) has the same result type
1278 --      (b) has the same type for 'f'
1279 -- module alpha conversion of the quantified type variables
1280 -- of the constructor.
1281 --
1282 -- Note that we allow existentials to match becuase the
1283 -- fields can never meet. E.g
1284 --      data T where
1285 --        T1 { f1 :: b, f2 :: a, f3 ::Int } :: T
1286 --        T2 { f1 :: c, f2 :: c, f3 ::Int } :: T  
1287 -- Here we do not complain about f1,f2 because they are existential
1288
1289 checkValidTyCon :: TyCon -> TcM ()
1290 checkValidTyCon tc 
1291   | Just cl <- tyConClass_maybe tc
1292   = checkValidClass cl
1293
1294   | isSynTyCon tc 
1295   = case synTyConRhs tc of
1296       SynFamilyTyCon {} -> return ()
1297       SynonymTyCon ty   -> checkValidType syn_ctxt ty
1298
1299   | otherwise
1300   = do { -- Check the context on the data decl
1301        ; traceTc "cvtc1" (ppr tc)
1302        ; checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc)
1303         
1304         -- Check arg types of data constructors
1305        ; traceTc "cvtc2" (ppr tc)
1306        ; mapM_ (checkValidDataCon tc) data_cons
1307
1308         -- Check that fields with the same name share a type
1309        ; mapM_ check_fields groups }
1310
1311   where
1312     syn_ctxt  = TySynCtxt name
1313     name      = tyConName tc
1314     data_cons = tyConDataCons tc
1315
1316     groups = equivClasses cmp_fld (concatMap get_fields data_cons)
1317     cmp_fld (f1,_) (f2,_) = f1 `compare` f2
1318     get_fields con = dataConFieldLabels con `zip` repeat con
1319         -- dataConFieldLabels may return the empty list, which is fine
1320
1321     -- See Note [GADT record selectors] in MkId.lhs
1322     -- We must check (a) that the named field has the same 
1323     --                   type in each constructor
1324     --               (b) that those constructors have the same result type
1325     --
1326     -- However, the constructors may have differently named type variable
1327     -- and (worse) we don't know how the correspond to each other.  E.g.
1328     --     C1 :: forall a b. { f :: a, g :: b } -> T a b
1329     --     C2 :: forall d c. { f :: c, g :: c } -> T c d
1330     -- 
1331     -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
1332     -- result type against other candidates' types BOTH WAYS ROUND.
1333     -- If they magically agrees, take the substitution and
1334     -- apply them to the latter ones, and see if they match perfectly.
1335     check_fields ((label, con1) : other_fields)
1336         -- These fields all have the same name, but are from
1337         -- different constructors in the data type
1338         = recoverM (return ()) $ mapM_ checkOne other_fields
1339                 -- Check that all the fields in the group have the same type
1340                 -- NB: this check assumes that all the constructors of a given
1341                 -- data type use the same type variables
1342         where
1343         (tvs1, _, _, res1) = dataConSig con1
1344         ts1 = mkVarSet tvs1
1345         fty1 = dataConFieldType con1 label
1346
1347         checkOne (_, con2)    -- Do it bothways to ensure they are structurally identical
1348             = do { checkFieldCompat label con1 con2 ts1 res1 res2 fty1 fty2
1349                  ; checkFieldCompat label con2 con1 ts2 res2 res1 fty2 fty1 }
1350             where        
1351                 (tvs2, _, _, res2) = dataConSig con2
1352                 ts2 = mkVarSet tvs2
1353                 fty2 = dataConFieldType con2 label
1354     check_fields [] = panic "checkValidTyCon/check_fields []"
1355
1356 checkFieldCompat :: Name -> DataCon -> DataCon -> TyVarSet
1357                  -> Type -> Type -> Type -> Type -> TcM ()
1358 checkFieldCompat fld con1 con2 tvs1 res1 res2 fty1 fty2
1359   = do  { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
1360         ; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
1361   where
1362     mb_subst1 = tcMatchTy tvs1 res1 res2
1363     mb_subst2 = tcMatchTyX tvs1 (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
1364
1365 -------------------------------
1366 checkValidDataCon :: TyCon -> DataCon -> TcM ()
1367 checkValidDataCon tc con
1368   = setSrcSpan (srcLocSpan (getSrcLoc con))     $
1369     addErrCtxt (dataConCtxt con)                $ 
1370     do  { traceTc "Validity of data con" (ppr con)
1371         ; let tc_tvs = tyConTyVars tc
1372               res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
1373               actual_res_ty = dataConOrigResTy con
1374         ; traceTc "checkValidDataCon" (ppr con $$ ppr tc $$ ppr tc_tvs $$ ppr res_ty_tmpl)
1375         ; checkTc (isJust (tcMatchTy (mkVarSet tc_tvs)
1376                                 res_ty_tmpl
1377                                 actual_res_ty))
1378                   (badDataConTyCon con res_ty_tmpl actual_res_ty)
1379              -- IA0_TODO: we should also check that kind variables
1380              -- are only instantiated with kind variables
1381         ; checkValidMonoType (dataConOrigResTy con)
1382                 -- Disallow MkT :: T (forall a. a->a)
1383                 -- Reason: it's really the argument of an equality constraint
1384         ; checkValidType ctxt (dataConUserType con)
1385         ; when (isNewTyCon tc) (checkNewDataCon con)
1386
1387         ; mapM_ check_bang (dataConStrictMarks con `zip` [1..])
1388
1389         ; checkTc (not (any (isKindVar . fst) (dataConEqSpec con)))
1390                   (badGadtKindCon con)
1391
1392         ; traceTc "Done validity of data con" (ppr con <+> ppr (dataConRepType con))
1393     }
1394   where
1395     ctxt = ConArgCtxt (dataConName con) 
1396     check_bang (HsUnpackFailed, n) = addWarnTc (cant_unbox_msg n)
1397     check_bang _                   = return ()
1398
1399     cant_unbox_msg n = sep [ ptext (sLit "Ignoring unusable UNPACK pragma on the")
1400                            , speakNth n <+> ptext (sLit "argument of") <+> quotes (ppr con)]
1401
1402 -------------------------------
1403 checkNewDataCon :: DataCon -> TcM ()
1404 -- Checks for the data constructor of a newtype
1405 checkNewDataCon con
1406   = do  { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
1407                 -- One argument
1408         ; checkTc (null eq_spec) (newtypePredError con)
1409                 -- Return type is (T a b c)
1410         ; checkTc (null ex_tvs && null theta) (newtypeExError con)
1411                 -- No existentials
1412         ; checkTc (not (any isBanged (dataConStrictMarks con))) 
1413                   (newtypeStrictError con)
1414                 -- No strictness
1415     }
1416   where
1417     (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig con
1418
1419 -------------------------------
1420 checkValidClass :: Class -> TcM ()
1421 checkValidClass cls
1422   = do  { constrained_class_methods <- xoptM Opt_ConstrainedClassMethods
1423         ; multi_param_type_classes <- xoptM Opt_MultiParamTypeClasses
1424         ; fundep_classes <- xoptM Opt_FunctionalDependencies
1425
1426         -- Check that the class is unary, unless GlaExs
1427         ; checkTc (notNull tyvars) (nullaryClassErr cls)
1428         ; checkTc (multi_param_type_classes || unary) (classArityErr cls)
1429         ; checkTc (fundep_classes || null fundeps) (classFunDepsErr cls)
1430
1431         -- Check the super-classes
1432         ; checkValidTheta (ClassSCCtxt (className cls)) theta
1433
1434           -- Now check for cyclic superclasses
1435         ; checkClassCycleErrs cls
1436
1437         -- Check the class operations
1438         ; mapM_ (check_op constrained_class_methods) op_stuff
1439
1440         -- Check the associated type defaults are well-formed and instantiated
1441         -- See Note [Checking consistent instantiation]
1442         ; mapM_ check_at_defs at_stuff  }
1443   where
1444     (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
1445     unary = count isTypeVar tyvars == 1   -- Ignore kind variables
1446
1447     check_op constrained_class_methods (sel_id, dm) 
1448       = addErrCtxt (classOpCtxt sel_id tau) $ do
1449         { checkValidTheta ctxt (tail theta)
1450                 -- The 'tail' removes the initial (C a) from the
1451                 -- class itself, leaving just the method type
1452
1453         ; traceTc "class op type" (ppr op_ty <+> ppr tau)
1454         ; checkValidType ctxt tau
1455
1456                 -- Check that the type mentions at least one of
1457                 -- the class type variables...or at least one reachable
1458                 -- from one of the class variables.  Example: tc223
1459                 --   class Error e => Game b mv e | b -> mv e where
1460                 --      newBoard :: MonadState b m => m ()
1461                 -- Here, MonadState has a fundep m->b, so newBoard is fine
1462         ; let grown_tyvars = growThetaTyVars theta (mkVarSet tyvars)
1463         ; checkTc (tyVarsOfType tau `intersectsVarSet` grown_tyvars)
1464                   (noClassTyVarErr cls sel_id)
1465
1466         ; case dm of
1467             GenDefMeth dm_name -> do { dm_id <- tcLookupId dm_name
1468                                      ; checkValidType (FunSigCtxt op_name) (idType dm_id) }
1469             _                  -> return ()
1470         }
1471         where
1472           ctxt    = FunSigCtxt op_name
1473           op_name = idName sel_id
1474           op_ty   = idType sel_id
1475           (_,theta1,tau1) = tcSplitSigmaTy op_ty
1476           (_,theta2,tau2)  = tcSplitSigmaTy tau1
1477           (theta,tau) | constrained_class_methods = (theta1 ++ theta2, tau2)
1478                       | otherwise = (theta1, mkPhiTy (tail theta1) tau1)
1479                 -- Ugh!  The function might have a type like
1480                 --      op :: forall a. C a => forall b. (Eq b, Eq a) => tau2
1481                 -- With -XConstrainedClassMethods, we want to allow this, even though the inner 
1482                 -- forall has an (Eq a) constraint.  Whereas in general, each constraint 
1483                 -- in the context of a for-all must mention at least one quantified
1484                 -- type variable.  What a mess!
1485
1486     check_at_defs (fam_tc, defs)
1487       = do { mapM_ (\(ATD _tvs pats rhs _loc) -> checkValidFamInst pats rhs) defs
1488            ; tcAddDefaultAssocDeclCtxt (tyConName fam_tc) $ 
1489              mapM_ (check_loc_at_def fam_tc) defs }
1490
1491     -- Check that the index of the type instance is the same as on
1492     -- its parent class.  Eg
1493     --    class C a b where
1494     --       type F b x a ::*
1495     --    instnace C Int Bool where
1496     --       type F Bool Char Int = Int
1497     --       type F Bool Bool Int = Bool
1498     --  Here the first and third args should match
1499     --  the (C Int Bool)  header
1500     -- This is not to do with soundness; it's just checking that the
1501     -- type instance arg is the sam
1502     check_loc_at_def fam_tc (ATD _tvs pats _rhs loc)
1503       -- Set the location for each of the default declarations
1504       = setSrcSpan loc $ zipWithM_ check_arg (tyConTyVars fam_tc) pats
1505
1506     -- We only want to check this on the *class* TyVars,
1507     -- not the *family* TyVars (there may be more of these)
1508     -- Nor do we want to check kind vars, for which we don't enforce
1509     -- the "same name as parent" rule as we do for type variables
1510     -- c.f. Trac #7073
1511     check_arg fam_tc_tv at_ty
1512       = checkTc (   isKindVar fam_tc_tv
1513                  || not (fam_tc_tv `elem` tyvars)
1514                  || mkTyVarTy fam_tc_tv `eqType` at_ty) 
1515           (wrongATArgErr at_ty (mkTyVarTy fam_tc_tv))
1516
1517 checkFamFlag :: Name -> TcM ()
1518 -- Check that we don't use families without -XTypeFamilies
1519 -- The parser won't even parse them, but I suppose a GHC API
1520 -- client might have a go!
1521 checkFamFlag tc_name
1522   = do { idx_tys <- xoptM Opt_TypeFamilies
1523        ; checkTc idx_tys err_msg }
1524   where
1525     err_msg = hang (ptext (sLit "Illegal family declaraion for") <+> quotes (ppr tc_name))
1526                  2 (ptext (sLit "Use -XTypeFamilies to allow indexed type families"))
1527 \end{code}
1528
1529
1530 %************************************************************************
1531 %*                                                                      *
1532                 Building record selectors
1533 %*                                                                      *
1534 %************************************************************************
1535
1536 \begin{code}
1537 mkDefaultMethodIds :: [TyThing] -> [Id]
1538 -- See Note [Default method Ids and Template Haskell]
1539 mkDefaultMethodIds things
1540   = [ mkExportedLocalId dm_name (idType sel_id)
1541     | ATyCon tc <- things
1542     , Just cls <- [tyConClass_maybe tc]
1543     , (sel_id, DefMeth dm_name) <- classOpItems cls ]
1544 \end{code}
1545
1546 Note [Default method Ids and Template Haskell]
1547 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1548 Consider this (Trac #4169):
1549    class Numeric a where
1550      fromIntegerNum :: a
1551      fromIntegerNum = ...
1552
1553    ast :: Q [Dec]
1554    ast = [d| instance Numeric Int |]
1555
1556 When we typecheck 'ast' we have done the first pass over the class decl
1557 (in tcTyClDecls), but we have not yet typechecked the default-method
1558 declarations (becuase they can mention value declarations).  So we 
1559 must bring the default method Ids into scope first (so they can be seen
1560 when typechecking the [d| .. |] quote, and typecheck them later.
1561
1562 \begin{code}
1563 mkRecSelBinds :: [TyThing] -> HsValBinds Name
1564 -- NB We produce *un-typechecked* bindings, rather like 'deriving'
1565 --    This makes life easier, because the later type checking will add
1566 --    all necessary type abstractions and applications
1567 mkRecSelBinds tycons
1568   = ValBindsOut [(NonRecursive, b) | b <- binds] sigs
1569   where
1570     (sigs, binds) = unzip rec_sels
1571     rec_sels = map mkRecSelBind [ (tc,fld) 
1572                                 | ATyCon tc <- tycons
1573                                 , fld <- tyConFields tc ]
1574
1575 mkRecSelBind :: (TyCon, FieldLabel) -> (LSig Name, LHsBinds Name)
1576 mkRecSelBind (tycon, sel_name)
1577   = (L loc (IdSig sel_id), unitBag (L loc sel_bind))
1578   where
1579     loc    = getSrcSpan sel_name
1580     sel_id = Var.mkExportedLocalVar rec_details sel_name 
1581                                     sel_ty vanillaIdInfo
1582     rec_details = RecSelId { sel_tycon = tycon, sel_naughty = is_naughty }
1583
1584     -- Find a representative constructor, con1
1585     all_cons     = tyConDataCons tycon 
1586     cons_w_field = [ con | con <- all_cons
1587                    , sel_name `elem` dataConFieldLabels con ] 
1588     con1 = ASSERT( not (null cons_w_field) ) head cons_w_field
1589
1590     -- Selector type; Note [Polymorphic selectors]
1591     field_ty   = dataConFieldType con1 sel_name
1592     data_ty    = dataConOrigResTy con1
1593     data_tvs   = tyVarsOfType data_ty
1594     is_naughty = not (tyVarsOfType field_ty `subVarSet` data_tvs)  
1595     (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
1596     sel_ty | is_naughty = unitTy  -- See Note [Naughty record selectors]
1597            | otherwise  = mkForAllTys (varSetElemsKvsFirst $
1598                                        data_tvs `extendVarSetList` field_tvs) $
1599                           mkPhiTy (dataConStupidTheta con1) $   -- Urgh!
1600                           mkPhiTy field_theta               $   -- Urgh!
1601                           mkFunTy data_ty field_tau
1602
1603     -- Make the binding: sel (C2 { fld = x }) = x
1604     --                   sel (C7 { fld = x }) = x
1605     --    where cons_w_field = [C2,C7]
1606     sel_bind | is_naughty = mkTopFunBind sel_lname [mkSimpleMatch [] unit_rhs]
1607              | otherwise  = mkTopFunBind sel_lname (map mk_match cons_w_field ++ deflt)
1608     mk_match con = mkSimpleMatch [L loc (mk_sel_pat con)]
1609                                  (L loc (HsVar field_var))
1610     mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields)
1611     rec_fields = HsRecFields { rec_flds = [rec_field], rec_dotdot = Nothing }
1612     rec_field  = HsRecField { hsRecFieldId = sel_lname
1613                             , hsRecFieldArg = L loc (VarPat field_var)
1614                             , hsRecPun = False }
1615     sel_lname = L loc sel_name
1616     field_var = mkInternalName (mkBuiltinUnique 1) (getOccName sel_name) loc
1617
1618     -- Add catch-all default case unless the case is exhaustive
1619     -- We do this explicitly so that we get a nice error message that
1620     -- mentions this particular record selector
1621     deflt | not (any is_unused all_cons) = []
1622           | otherwise = [mkSimpleMatch [L loc (WildPat placeHolderType)] 
1623                             (mkHsApp (L loc (HsVar (getName rEC_SEL_ERROR_ID)))
1624                                      (L loc (HsLit msg_lit)))]
1625
1626         -- Do not add a default case unless there are unmatched
1627         -- constructors.  We must take account of GADTs, else we
1628         -- get overlap warning messages from the pattern-match checker
1629     is_unused con = not (con `elem` cons_w_field 
1630                          || dataConCannotMatch inst_tys con)
1631     inst_tys = tyConAppArgs data_ty
1632
1633     unit_rhs = mkLHsTupleExpr []
1634     msg_lit = HsStringPrim $ mkFastString $ 
1635               occNameString (getOccName sel_name)
1636
1637 ---------------
1638 tyConFields :: TyCon -> [FieldLabel]
1639 tyConFields tc 
1640   | isAlgTyCon tc = nub (concatMap dataConFieldLabels (tyConDataCons tc))
1641   | otherwise     = []
1642 \end{code}
1643
1644 Note [Polymorphic selectors]
1645 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1646 When a record has a polymorphic field, we pull the foralls out to the front.
1647    data T = MkT { f :: forall a. [a] -> a }
1648 Then f :: forall a. T -> [a] -> a
1649 NOT  f :: T -> forall a. [a] -> a
1650
1651 This is horrid.  It's only needed in deeply obscure cases, which I hate.
1652 The only case I know is test tc163, which is worth looking at.  It's far
1653 from clear that this test should succeed at all!
1654
1655 Note [Naughty record selectors]
1656 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1657 A "naughty" field is one for which we can't define a record 
1658 selector, because an existential type variable would escape.  For example:
1659         data T = forall a. MkT { x,y::a }
1660 We obviously can't define       
1661         x (MkT v _) = v
1662 Nevertheless we *do* put a RecSelId into the type environment
1663 so that if the user tries to use 'x' as a selector we can bleat
1664 helpfully, rather than saying unhelpfully that 'x' is not in scope.
1665 Hence the sel_naughty flag, to identify record selectors that don't really exist.
1666
1667 In general, a field is "naughty" if its type mentions a type variable that
1668 isn't in the result type of the constructor.  Note that this *allows*
1669 GADT record selectors (Note [GADT record selectors]) whose types may look 
1670 like     sel :: T [a] -> a
1671
1672 For naughty selectors we make a dummy binding 
1673    sel = ()
1674 for naughty selectors, so that the later type-check will add them to the
1675 environment, and they'll be exported.  The function is never called, because
1676 the tyepchecker spots the sel_naughty field.
1677
1678 Note [GADT record selectors]
1679 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1680 For GADTs, we require that all constructors with a common field 'f' have the same
1681 result type (modulo alpha conversion).  [Checked in TcTyClsDecls.checkValidTyCon]
1682 E.g. 
1683         data T where
1684           T1 { f :: Maybe a } :: T [a]
1685           T2 { f :: Maybe a, y :: b  } :: T [a]
1686           T3 :: T Int
1687
1688 and now the selector takes that result type as its argument:
1689    f :: forall a. T [a] -> Maybe a
1690
1691 Details: the "real" types of T1,T2 are:
1692    T1 :: forall r a.   (r~[a]) => a -> T r
1693    T2 :: forall r a b. (r~[a]) => a -> b -> T r
1694
1695 So the selector loooks like this:
1696    f :: forall a. T [a] -> Maybe a
1697    f (a:*) (t:T [a])
1698      = case t of
1699          T1 c   (g:[a]~[c]) (v:Maybe c)       -> v `cast` Maybe (right (sym g))
1700          T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
1701          T3 -> error "T3 does not have field f"
1702
1703 Note the forall'd tyvars of the selector are just the free tyvars
1704 of the result type; there may be other tyvars in the constructor's
1705 type (e.g. 'b' in T2).
1706
1707 Note the need for casts in the result!
1708
1709 Note [Selector running example]
1710 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1711 It's OK to combine GADTs and type families.  Here's a running example:
1712
1713         data instance T [a] where 
1714           T1 { fld :: b } :: T [Maybe b]
1715
1716 The representation type looks like this
1717         data :R7T a where
1718           T1 { fld :: b } :: :R7T (Maybe b)
1719
1720 and there's coercion from the family type to the representation type
1721         :CoR7T a :: T [a] ~ :R7T a
1722
1723 The selector we want for fld looks like this:
1724
1725         fld :: forall b. T [Maybe b] -> b
1726         fld = /\b. \(d::T [Maybe b]).
1727               case d `cast` :CoR7T (Maybe b) of 
1728                 T1 (x::b) -> x
1729
1730 The scrutinee of the case has type :R7T (Maybe b), which can be
1731 gotten by appying the eq_spec to the univ_tvs of the data con.
1732
1733 %************************************************************************
1734 %*                                                                      *
1735                 Error messages
1736 %*                                                                      *
1737 %************************************************************************
1738
1739 \begin{code}
1740 tcAddDefaultAssocDeclCtxt :: Name -> TcM a -> TcM a
1741 tcAddDefaultAssocDeclCtxt name thing_inside
1742   = addErrCtxt ctxt thing_inside
1743   where
1744      ctxt = hsep [ptext (sLit "In the type synonym instance default declaration for"),
1745                   quotes (ppr name)]
1746
1747 tcAddFamInstCtxt :: FamInstDecl Name -> TcM a -> TcM a
1748 tcAddFamInstCtxt (FamInstDecl { fid_tycon = tc, fid_defn = defn }) thing_inside
1749   = addErrCtxt ctxt thing_inside
1750   where
1751      ctxt = hsep [ptext (sLit "In the") <+> pprTyDefnFlavour defn 
1752                   <+> ptext (sLit "instance declaration for"),
1753                   quotes (ppr tc)]
1754
1755 resultTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc
1756 resultTypeMisMatch field_name con1 con2
1757   = vcat [sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2, 
1758                 ptext (sLit "have a common field") <+> quotes (ppr field_name) <> comma],
1759           nest 2 $ ptext (sLit "but have different result types")]
1760
1761 fieldTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc
1762 fieldTypeMisMatch field_name con1 con2
1763   = sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2, 
1764          ptext (sLit "give different types for field"), quotes (ppr field_name)]
1765
1766 dataConCtxt :: Outputable a => a -> SDoc
1767 dataConCtxt con = ptext (sLit "In the definition of data constructor") <+> quotes (ppr con)
1768
1769 classOpCtxt :: Var -> Type -> SDoc
1770 classOpCtxt sel_id tau = sep [ptext (sLit "When checking the class method:"),
1771                               nest 2 (ppr sel_id <+> dcolon <+> ppr tau)]
1772
1773 nullaryClassErr :: Class -> SDoc
1774 nullaryClassErr cls
1775   = ptext (sLit "No parameters for class")  <+> quotes (ppr cls)
1776
1777 classArityErr :: Class -> SDoc
1778 classArityErr cls
1779   = vcat [ptext (sLit "Too many parameters for class") <+> quotes (ppr cls),
1780           parens (ptext (sLit "Use -XMultiParamTypeClasses to allow multi-parameter classes"))]
1781
1782 classFunDepsErr :: Class -> SDoc
1783 classFunDepsErr cls
1784   = vcat [ptext (sLit "Fundeps in class") <+> quotes (ppr cls),
1785           parens (ptext (sLit "Use -XFunctionalDependencies to allow fundeps"))]
1786
1787 noClassTyVarErr :: Class -> Var -> SDoc
1788 noClassTyVarErr clas op
1789   = sep [ptext (sLit "The class method") <+> quotes (ppr op),
1790          ptext (sLit "mentions none of the type variables of the class") <+> 
1791                 ppr clas <+> hsep (map ppr (classTyVars clas))]
1792
1793 recSynErr :: [LTyClDecl Name] -> TcRn ()
1794 recSynErr syn_decls
1795   = setSrcSpan (getLoc (head sorted_decls)) $
1796     addErr (sep [ptext (sLit "Cycle in type synonym declarations:"),
1797                  nest 2 (vcat (map ppr_decl sorted_decls))])
1798   where
1799     sorted_decls = sortLocated syn_decls
1800     ppr_decl (L loc decl) = ppr loc <> colon <+> ppr decl
1801
1802 recClsErr :: [TyCon] -> TcRn ()
1803 recClsErr cycles
1804   = addErr (sep [ptext (sLit "Cycle in class declaration (via superclasses):"),
1805                  nest 2 (hsep (intersperse (text "->") (map ppr cycles)))])
1806
1807 badDataConTyCon :: DataCon -> Type -> Type -> SDoc
1808 badDataConTyCon data_con res_ty_tmpl actual_res_ty
1809   = hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con) <+>
1810                 ptext (sLit "returns type") <+> quotes (ppr actual_res_ty))
1811        2 (ptext (sLit "instead of an instance of its parent type") <+> quotes (ppr res_ty_tmpl))
1812
1813 badGadtKindCon :: DataCon -> SDoc
1814 badGadtKindCon data_con
1815   = hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con) 
1816           <+> ptext (sLit "cannot be GADT-like in its *kind* arguments"))
1817        2 (ppr data_con <+> dcolon <+> ppr (dataConUserType data_con))
1818
1819 badATErr :: Name -> Name -> SDoc
1820 badATErr clas op
1821   = hsep [ptext (sLit "Class"), quotes (ppr clas), 
1822           ptext (sLit "does not have an associated type"), quotes (ppr op)]
1823
1824 badGadtDecl :: Name -> SDoc
1825 badGadtDecl tc_name
1826   = vcat [ ptext (sLit "Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
1827          , nest 2 (parens $ ptext (sLit "Use -XGADTs to allow GADTs")) ]
1828
1829 badExistential :: Located Name -> SDoc
1830 badExistential con_name
1831   = hang (ptext (sLit "Data constructor") <+> quotes (ppr con_name) <+>
1832                 ptext (sLit "has existential type variables, a context, or a specialised result type"))
1833        2 (parens $ ptext (sLit "Use -XExistentialQuantification or -XGADTs to allow this"))
1834
1835 badStupidTheta :: Name -> SDoc
1836 badStupidTheta tc_name
1837   = ptext (sLit "A data type declared in GADT style cannot have a context:") <+> quotes (ppr tc_name)
1838
1839 newtypeConError :: Name -> Int -> SDoc
1840 newtypeConError tycon n
1841   = sep [ptext (sLit "A newtype must have exactly one constructor,"),
1842          nest 2 $ ptext (sLit "but") <+> quotes (ppr tycon) <+> ptext (sLit "has") <+> speakN n ]
1843
1844 newtypeExError :: DataCon -> SDoc
1845 newtypeExError con
1846   = sep [ptext (sLit "A newtype constructor cannot have an existential context,"),
1847          nest 2 $ ptext (sLit "but") <+> quotes (ppr con) <+> ptext (sLit "does")]
1848
1849 newtypeStrictError :: DataCon -> SDoc
1850 newtypeStrictError con
1851   = sep [ptext (sLit "A newtype constructor cannot have a strictness annotation,"),
1852          nest 2 $ ptext (sLit "but") <+> quotes (ppr con) <+> ptext (sLit "does")]
1853
1854 newtypePredError :: DataCon -> SDoc
1855 newtypePredError con
1856   = sep [ptext (sLit "A newtype constructor must have a return type of form T a1 ... an"),
1857          nest 2 $ ptext (sLit "but") <+> quotes (ppr con) <+> ptext (sLit "does not")]
1858
1859 newtypeFieldErr :: DataCon -> Int -> SDoc
1860 newtypeFieldErr con_name n_flds
1861   = sep [ptext (sLit "The constructor of a newtype must have exactly one field"), 
1862          nest 2 $ ptext (sLit "but") <+> quotes (ppr con_name) <+> ptext (sLit "has") <+> speakN n_flds]
1863
1864 badSigTyDecl :: Name -> SDoc
1865 badSigTyDecl tc_name
1866   = vcat [ ptext (sLit "Illegal kind signature") <+>
1867            quotes (ppr tc_name)
1868          , nest 2 (parens $ ptext (sLit "Use -XKindSignatures to allow kind signatures")) ]
1869
1870 emptyConDeclsErr :: Name -> SDoc
1871 emptyConDeclsErr tycon
1872   = sep [quotes (ppr tycon) <+> ptext (sLit "has no constructors"),
1873          nest 2 $ ptext (sLit "(-XEmptyDataDecls permits this)")]
1874
1875 wrongATArgErr :: Type -> Type -> SDoc
1876 wrongATArgErr ty instTy =
1877   sep [ ptext (sLit "Type indexes must match class instance head")
1878       , ptext (sLit "Found") <+> quotes (ppr ty)
1879         <+> ptext (sLit "but expected") <+> quotes (ppr instTy)
1880       ]
1881
1882 wrongNumberOfParmsErr :: Arity -> SDoc
1883 wrongNumberOfParmsErr exp_arity
1884   = ptext (sLit "Number of parameters must match family declaration; expected")
1885     <+> ppr exp_arity
1886
1887 wrongKindOfFamily :: TyCon -> SDoc
1888 wrongKindOfFamily family
1889   = ptext (sLit "Wrong category of family instance; declaration was for a")
1890     <+> kindOfFamily
1891   where
1892     kindOfFamily | isSynTyCon family = ptext (sLit "type synonym")
1893                  | isAlgTyCon family = ptext (sLit "data type")
1894                  | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
1895 \end{code}