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