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