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