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