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