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