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