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