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