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