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