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