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