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