Embrace -XTypeInType, add -XStarIsType
[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, MultiWayIf #-}
10 {-# LANGUAGE TypeFamilies #-}
11
12 module TcTyClsDecls (
13 tcTyAndClassDecls, tcAddImplicits,
14
15 -- Functions used by TcInstDcls to check
16 -- data/type family instance declarations
17 kcDataDefn, tcConDecls, dataDeclChecks, checkValidTyCon,
18 tcFamTyPats, tcTyFamInstEqn,
19 tcAddTyFamInstCtxt, tcMkDataFamInstCtxt, tcAddDataFamInstCtxt,
20 wrongKindOfFamily, dataConCtxt
21 ) where
22
23 #include "HsVersions.h"
24
25 import GhcPrelude
26
27 import HsSyn
28 import HscTypes
29 import BuildTyCl
30 import TcRnMonad
31 import TcEnv
32 import TcValidity
33 import TcHsSyn
34 import TcTyDecls
35 import TcClassDcl
36 import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
37 import TcDeriv (DerivInfo)
38 import TcEvidence ( tcCoercionKind, isEmptyTcEvBinds )
39 import TcUnify ( checkConstraints )
40 import TcHsType
41 import TcMType
42 import TysWiredIn ( unitTy )
43 import TcType
44 import RnEnv( lookupConstructorFields )
45 import FamInst
46 import FamInstEnv
47 import Coercion
48 import Type
49 import TyCoRep -- for checkValidRoles
50 import Kind
51 import Class
52 import CoAxiom
53 import TyCon
54 import DataCon
55 import Id
56 import Var
57 import VarEnv
58 import VarSet
59 import Module
60 import Name
61 import NameSet
62 import NameEnv
63 import Outputable
64 import Maybes
65 import Unify
66 import Util
67 import Pair
68 import SrcLoc
69 import ListSetOps
70 import DynFlags
71 import Unique
72 import BasicTypes
73 import qualified GHC.LanguageExtensions as LangExt
74
75 import Control.Monad
76 import Data.List
77 import Data.List.NonEmpty ( NonEmpty(..) )
78
79 {-
80 ************************************************************************
81 * *
82 \subsection{Type checking for type and class declarations}
83 * *
84 ************************************************************************
85
86 Note [Grouping of type and class declarations]
87 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
88 tcTyAndClassDecls is called on a list of `TyClGroup`s. Each group is a strongly
89 connected component of mutually dependent types and classes. We kind check and
90 type check each group separately to enhance kind polymorphism. Take the
91 following example:
92
93 type Id a = a
94 data X = X (Id Int)
95
96 If we were to kind check the two declarations together, we would give Id the
97 kind * -> *, since we apply it to an Int in the definition of X. But we can do
98 better than that, since Id really is kind polymorphic, and should get kind
99 forall (k::*). k -> k. Since it does not depend on anything else, it can be
100 kind-checked by itself, hence getting the most general kind. We then kind check
101 X, which works fine because we then know the polymorphic kind of Id, and simply
102 instantiate k to *.
103
104 Note [Check role annotations in a second pass]
105 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
106 Role inference potentially depends on the types of all of the datacons declared
107 in a mutually recursive group. The validity of a role annotation, in turn,
108 depends on the result of role inference. Because the types of datacons might
109 be ill-formed (see #7175 and Note [Checking GADT return types]) we must check
110 *all* the tycons in a group for validity before checking *any* of the roles.
111 Thus, we take two passes over the resulting tycons, first checking for general
112 validity and then checking for valid role annotations.
113 -}
114
115 tcTyAndClassDecls :: [TyClGroup GhcRn] -- Mutually-recursive groups in
116 -- dependency order
117 -> TcM ( TcGblEnv -- Input env extended by types and
118 -- classes
119 -- and their implicit Ids,DataCons
120 , [InstInfo GhcRn] -- Source-code instance decls info
121 , [DerivInfo] -- data family deriving info
122 )
123 -- Fails if there are any errors
124 tcTyAndClassDecls tyclds_s
125 -- The code recovers internally, but if anything gave rise to
126 -- an error we'd better stop now, to avoid a cascade
127 -- Type check each group in dependency order folding the global env
128 = checkNoErrs $ fold_env [] [] tyclds_s
129 where
130 fold_env :: [InstInfo GhcRn]
131 -> [DerivInfo]
132 -> [TyClGroup GhcRn]
133 -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
134 fold_env inst_info deriv_info []
135 = do { gbl_env <- getGblEnv
136 ; return (gbl_env, inst_info, deriv_info) }
137 fold_env inst_info deriv_info (tyclds:tyclds_s)
138 = do { (tcg_env, inst_info', deriv_info') <- tcTyClGroup tyclds
139 ; setGblEnv tcg_env $
140 -- remaining groups are typechecked in the extended global env.
141 fold_env (inst_info' ++ inst_info)
142 (deriv_info' ++ deriv_info)
143 tyclds_s }
144
145 tcTyClGroup :: TyClGroup GhcRn
146 -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo])
147 -- Typecheck one strongly-connected component of type, class, and instance decls
148 -- See Note [TyClGroups and dependency analysis] in HsDecls
149 tcTyClGroup (TyClGroup { group_tyclds = tyclds
150 , group_roles = roles
151 , group_instds = instds })
152 = do { let role_annots = mkRoleAnnotEnv roles
153
154 -- Step 1: Typecheck the type/class declarations
155 ; traceTc "---- tcTyClGroup ---- {" empty
156 ; traceTc "Decls for" (ppr (map (tcdName . unLoc) tyclds))
157 ; tyclss <- tcTyClDecls tyclds role_annots
158
159 -- Step 1.5: Make sure we don't have any type synonym cycles
160 ; traceTc "Starting synonym cycle check" (ppr tyclss)
161 ; this_uid <- fmap thisPackage getDynFlags
162 ; checkSynCycles this_uid tyclss tyclds
163 ; traceTc "Done synonym cycle check" (ppr tyclss)
164
165 -- Step 2: Perform the validity check on those types/classes
166 -- We can do this now because we are done with the recursive knot
167 -- Do it before Step 3 (adding implicit things) because the latter
168 -- expects well-formed TyCons
169 ; traceTc "Starting validity check" (ppr tyclss)
170 ; tyclss <- mapM checkValidTyCl tyclss
171 ; traceTc "Done validity check" (ppr tyclss)
172 ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
173 -- See Note [Check role annotations in a second pass]
174
175 ; traceTc "---- end tcTyClGroup ---- }" empty
176
177 -- Step 3: Add the implicit things;
178 -- we want them in the environment because
179 -- they may be mentioned in interface files
180 ; tcExtendTyConEnv tyclss $
181 do { gbl_env <- tcAddImplicits tyclss
182 ; setGblEnv gbl_env $
183 do {
184 -- Step 4: check instance declarations
185 ; (gbl_env, inst_info, datafam_deriv_info) <- tcInstDecls1 instds
186
187 ; return (gbl_env, inst_info, datafam_deriv_info) } } }
188 tcTyClGroup (XTyClGroup _) = panic "tcTyClGroup"
189
190 tcTyClDecls :: [LTyClDecl GhcRn] -> RoleAnnotEnv -> TcM [TyCon]
191 tcTyClDecls tyclds role_annots
192 = tcExtendKindEnv promotion_err_env $ --- See Note [Type environment evolution]
193 do { -- Step 1: kind-check this group and returns the final
194 -- (possibly-polymorphic) kind of each TyCon and Class
195 -- See Note [Kind checking for type and class decls]
196 tc_tycons <- kcTyClGroup tyclds
197 ; traceTc "tcTyAndCl generalized kinds" (vcat (map ppr_tc_tycon tc_tycons))
198
199 -- Step 2: type-check all groups together, returning
200 -- the final TyCons and Classes
201 --
202 -- NB: We have to be careful here to NOT eagerly unfold
203 -- type synonyms, as we have not tested for type synonym
204 -- loops yet and could fall into a black hole.
205 ; fixM $ \ ~rec_tyclss -> do
206 { tcg_env <- getGblEnv
207 ; let roles = inferRoles (tcg_src tcg_env) role_annots rec_tyclss
208
209 -- Populate environment with knot-tied ATyCon for TyCons
210 -- NB: if the decls mention any ill-staged data cons
211 -- (see Note [Recursion and promoting data constructors])
212 -- we will have failed already in kcTyClGroup, so no worries here
213 ; tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $
214
215 -- Also extend the local type envt with bindings giving
216 -- the (polymorphic) kind of each knot-tied TyCon or Class
217 -- See Note [Type checking recursive type and class declarations]
218 -- and Note [Type environment evolution]
219 tcExtendKindEnvWithTyCons tc_tycons $
220
221 -- Kind and type check declarations for this group
222 mapM (tcTyClDecl roles) tyclds
223 } }
224 where
225 promotion_err_env = mkPromotionErrorEnv tyclds
226 ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
227 , ppr (tyConBinders tc) <> comma
228 , ppr (tyConResKind tc) ])
229
230 zipRecTyClss :: [TcTyCon]
231 -> [TyCon] -- Knot-tied
232 -> [(Name,TyThing)]
233 -- Build a name-TyThing mapping for the TyCons bound by decls
234 -- being careful not to look at the knot-tied [TyThing]
235 -- The TyThings in the result list must have a visible ATyCon,
236 -- because typechecking types (in, say, tcTyClDecl) looks at
237 -- this outer constructor
238 zipRecTyClss tc_tycons rec_tycons
239 = [ (name, ATyCon (get name)) | tc_tycon <- tc_tycons, let name = getName tc_tycon ]
240 where
241 rec_tc_env :: NameEnv TyCon
242 rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
243
244 add_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
245 add_tc tc env = foldr add_one_tc env (tc : tyConATs tc)
246
247 add_one_tc :: TyCon -> NameEnv TyCon -> NameEnv TyCon
248 add_one_tc tc env = extendNameEnv env (tyConName tc) tc
249
250 get name = case lookupNameEnv rec_tc_env name of
251 Just tc -> tc
252 other -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
253
254 {-
255 ************************************************************************
256 * *
257 Kind checking
258 * *
259 ************************************************************************
260
261 Note [Kind checking for type and class decls]
262 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
263 Kind checking is done thus:
264
265 1. Make up a kind variable for each parameter of the declarations,
266 and extend the kind environment (which is in the TcLclEnv)
267
268 2. Kind check the declarations
269
270 We need to kind check all types in the mutually recursive group
271 before we know the kind of the type variables. For example:
272
273 class C a where
274 op :: D b => a -> b -> b
275
276 class D c where
277 bop :: (Monad c) => ...
278
279 Here, the kind of the locally-polymorphic type variable "b"
280 depends on *all the uses of class D*. For example, the use of
281 Monad c in bop's type signature means that D must have kind Type->Type.
282
283 Note: we don't treat type synonyms specially (we used to, in the past);
284 in particular, even if we have a type synonym cycle, we still kind check
285 it normally, and test for cycles later (checkSynCycles). The reason
286 we can get away with this is because we have more systematic TYPE r
287 inference, which means that we can do unification between kinds that
288 aren't lifted (this historically was not true.)
289
290 The downside of not directly reading off the kinds off the RHS of
291 type synonyms in topological order is that we don't transparently
292 support making synonyms of types with higher-rank kinds. But
293 you can always specify a CUSK directly to make this work out.
294 See tc269 for an example.
295
296 Note [Skip decls with CUSKs in kcLTyClDecl]
297 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
298 Consider
299
300 data T (a :: *) = MkT (S a) -- Has CUSK
301 data S a = MkS (T Int) (S a) -- No CUSK
302
303 Via getInitialKinds we get
304 T :: * -> *
305 S :: kappa -> *
306
307 Then we call kcTyClDecl on each decl in the group, to constrain the
308 kind unification variables. BUT we /skip/ the RHS of any decl with
309 a CUSK. Here we skip the RHS of T, so we eventually get
310 S :: forall k. k -> *
311
312 This gets us more polymorphism than we would otherwise get, similar
313 (but implemented strangely differently from) the treatment of type
314 signatures in value declarations.
315
316 Open type families
317 ~~~~~~~~~~~~~~~~~~
318 This treatment of type synonyms only applies to Haskell 98-style synonyms.
319 General type functions can be recursive, and hence, appear in `alg_decls'.
320
321 The kind of an open type family is solely determinded by its kind signature;
322 hence, only kind signatures participate in the construction of the initial
323 kind environment (as constructed by `getInitialKind'). In fact, we ignore
324 instances of families altogether in the following. However, we need to include
325 the kinds of *associated* families into the construction of the initial kind
326 environment. (This is handled by `allDecls').
327
328 See also Note [Kind checking recursive type and class declarations]
329
330 Note [How TcTyCons work]
331 ~~~~~~~~~~~~~~~~~~~~~~~~
332 TcTyCons are used for two distinct purposes
333
334 1. When recovering from a type error in a type declaration,
335 we want to put the erroneous TyCon in the environment in a
336 way that won't lead to more errors. We use a TcTyCon for this;
337 see makeRecoveryTyCon.
338
339 2. When checking a type/class declaration (in module TcTyClsDecls), we come
340 upon knowledge of the eventual tycon in bits and pieces.
341
342 S1) First, we use getInitialKinds to look over the user-provided
343 kind signature of a tycon (including, for example, the number
344 of parameters written to the tycon) to get an initial shape of
345 the tycon's kind. We record that shape in a TcTyCon.
346
347 S2) Then, using these initial kinds, we kind-check the body of the
348 tycon (class methods, data constructors, etc.), filling in the
349 metavariables in the tycon's initial kind.
350
351 S3) We then generalize to get the tycon's final, fixed
352 kind. Finally, once this has happened for all tycons in a
353 mutually recursive group, we can desugar the lot.
354
355 For convenience, we store partially-known tycons in TcTyCons, which
356 might store meta-variables. These TcTyCons are stored in the local
357 environment in TcTyClsDecls, until the real full TyCons can be created
358 during desugaring. A desugared program should never have a TcTyCon.
359
360 A challenging piece in all of this is that we end up taking three separate
361 passes over every declaration:
362 - one in getInitialKind (this pass look only at the head, not the body)
363 - one in kcTyClDecls (to kind-check the body)
364 - a final one in tcTyClDecls (to desugar)
365 In the latter two passes, we need to connect the user-written type
366 variables in an LHsQTyVars with the variables in the tycon's
367 inferred kind. Because the tycon might not have a CUSK, this
368 matching up is, in general, quite hard to do. (Look through the
369 git history between Dec 2015 and Apr 2016 for
370 TcHsType.splitTelescopeTvs!) Instead of trying, we just store the
371 list of type variables to bring into scope, in the
372 tyConScopedTyVars field of the TcTyCon. These tyvars are brought
373 into scope in kcTyClTyVars and tcTyClTyVars, both in TcHsType.
374
375 In a TcTyCon, everything is zonked after the kind-checking pass (S2).
376
377 Note [Check telescope again during generalisation]
378 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
379 The telescope check before kind generalisation is useful to catch something
380 like this:
381
382 data T a k = MkT (Proxy (a :: k))
383
384 Clearly, the k has to come first. Checking for this problem must come before
385 kind generalisation, as described in Note [Bad telescopes] in
386 TcValidity.
387
388 However, we have to check again *after* kind generalisation, to catch something
389 like this:
390
391 data SameKind :: k -> k -> Type -- to force unification
392 data S a (b :: a) (d :: SameKind c b)
393
394 Note that c has no explicit binding site. As such, it's quantified by kind
395 generalisation. (Note that kcHsTyVarBndrs does not return such variables
396 as binders in its returned TcTyCon.) The user-written part of this telescope
397 is well-ordered; no earlier variables depend on later ones. However, after
398 kind generalisation, we put c up front, like so:
399
400 data S {c :: a} a (b :: a) (d :: SameKind c b)
401
402 We now have a problem. We could detect this problem just by looking at the
403 free vars of the kinds of the generalised variables (the kvs), but we get
404 such a nice error message out of checkValidTelescope that it seems like the
405 right thing to do.
406
407 Note [Type environment evolution]
408 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
409 As we typecheck a group of declarations the type environment evolves.
410 Consider for example:
411 data B (a :: Type) = MkB (Proxy 'MkB)
412
413 We do the following steps:
414
415 1. Start of tcTyClDecls: use mkPromotionErrorEnv to initialise the
416 type env with promotion errors
417 B :-> TyConPE
418 MkB :-> DataConPE
419
420 2. kcTyCLGruup
421 - Do getInitialKinds, which will signal a promotion
422 error if B is used in any of the kinds needed to initialse
423 B's kind (e.g. (a :: Type)) here
424
425 - Extend the type env with these intial kinds (monomorphic for
426 decls that lack a CUSK)
427 B :-> TcTyCon <initial kind>
428 (thereby overriding the B :-> TyConPE binding)
429 and do kcLTyClDecl on each decl to get equality constraints on
430 all those inital kinds
431
432 - Generalise the inital kind, making a poly-kinded TcTyCon
433
434 3. Back in tcTyDecls, extend the envt with bindings of the poly-kinded
435 TcTyCons, again overriding the promotion-error bindings.
436
437 But note that the data constructor promotion errors are still in place
438 so that (in our example) a use of MkB will sitll be signalled as
439 an error.
440
441 4. Typecheck the decls.
442
443 5. In tcTyClGroup, extend the envt with bindings for TyCon and DataCons
444
445
446 Note [Missed opportunity to retain higher-rank kinds]
447 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
448 In 'kcTyClGroup', there is a missed opportunity to make kind
449 inference work in a few more cases. The idea is analogous
450 to Note [Single function non-recursive binding special-case]:
451
452 * If we have an SCC with a single decl, which is non-recursive,
453 instead of creating a unification variable representing the
454 kind of the decl and unifying it with the rhs, we can just
455 read the type directly of the rhs.
456
457 * Furthermore, we can update our SCC analysis to ignore
458 dependencies on declarations which have CUSKs: we don't
459 have to kind-check these all at once, since we can use
460 the CUSK to initialize the kind environment.
461
462 Unfortunately this requires reworking a bit of the code in
463 'kcLTyClDecl' so I've decided to punt unless someone shouts about it.
464 -}
465
466 kcTyClGroup :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
467
468 -- Kind check this group, kind generalize, and return the resulting local env
469 -- This binds the TyCons and Classes of the group, but not the DataCons
470 -- See Note [Kind checking for type and class decls]
471 -- Third return value is Nothing if the tycon be unsaturated; otherwise,
472 -- the arity
473 kcTyClGroup decls
474 = do { mod <- getModule
475 ; traceTc "---- kcTyClGroup ---- {" (text "module" <+> ppr mod $$ vcat (map ppr decls))
476
477 -- Kind checking;
478 -- 1. Bind kind variables for decls
479 -- 2. Kind-check decls
480 -- 3. Generalise the inferred kinds
481 -- See Note [Kind checking for type and class decls]
482
483 -- Step 1: Bind kind variables for all decls
484 ; initial_tcs <- getInitialKinds decls
485 ; traceTc "kcTyClGroup: initial kinds" $
486 ppr_tc_kinds initial_tcs
487
488 -- Step 2: Set extended envt, kind-check the decls
489 -- NB: the environment extension overrides the tycon
490 -- promotion-errors bindings
491 -- See Note [Type environment evolution]
492
493 ; solveEqualities $
494 tcExtendKindEnvWithTyCons initial_tcs $
495 mapM_ kcLTyClDecl decls
496
497 -- Step 3: generalisation
498 -- Kind checking done for this group
499 -- Now we have to kind generalize the flexis
500 ; poly_tcs <- mapAndReportM generalise initial_tcs
501
502 ; traceTc "---- kcTyClGroup end ---- }" (ppr_tc_kinds poly_tcs)
503 ; return poly_tcs }
504
505 where
506 ppr_tc_kinds tcs = vcat (map pp_tc tcs)
507 pp_tc tc = ppr (tyConName tc) <+> dcolon <+> ppr (tyConKind tc)
508
509 generalise :: TcTyCon -> TcM TcTyCon
510 -- For polymorphic things this is a no-op
511 generalise tc
512 = setSrcSpan (getSrcSpan tc) $
513 addTyConCtxt tc $
514 do { let name = tyConName tc
515 ; tc_binders <- mapM zonkTcTyVarBinder (tyConBinders tc)
516 ; tc_res_kind <- zonkTcType (tyConResKind tc)
517 ; let scoped_tvs = tcTyConScopedTyVars tc
518 user_tyvars = tcTyConUserTyVars tc
519
520 -- See Note [checkValidDependency]
521 ; checkValidDependency tc_binders tc_res_kind
522
523 -- See Note [Bad telescopes] in TcValidity
524 ; checkValidTelescope tc_binders user_tyvars empty
525 ; kvs <- kindGeneralize (mkTyConKind tc_binders tc_res_kind)
526
527 ; let all_binders = mkNamedTyConBinders Inferred kvs ++ tc_binders
528
529 ; (env, all_binders') <- zonkTyVarBindersX emptyZonkEnv all_binders
530 ; tc_res_kind' <- zonkTcTypeToType env tc_res_kind
531 ; scoped_tvs' <- zonkSigTyVarPairs scoped_tvs
532
533 -- See Note [Check telescope again during generalisation]
534 ; let extra = text "NB: Implicitly declared variables come before others."
535 ; checkValidTelescope all_binders user_tyvars extra
536
537 -- Make sure tc_kind' has the final, zonked kind variables
538 ; traceTc "Generalise kind" $
539 vcat [ ppr name, ppr tc_binders, ppr (mkTyConKind tc_binders tc_res_kind)
540 , ppr kvs, ppr all_binders, ppr tc_res_kind
541 , ppr all_binders', ppr tc_res_kind'
542 , ppr scoped_tvs ]
543
544 ; return (mkTcTyCon name user_tyvars all_binders' tc_res_kind'
545 scoped_tvs'
546 (tyConFlavour tc)) }
547
548
549 --------------
550 tcExtendKindEnvWithTyCons :: [TcTyCon] -> TcM a -> TcM a
551 tcExtendKindEnvWithTyCons tcs
552 = tcExtendKindEnvList [ (tyConName tc, ATcTyCon tc) | tc <- tcs ]
553
554 --------------
555 mkPromotionErrorEnv :: [LTyClDecl GhcRn] -> TcTypeEnv
556 -- Maps each tycon/datacon to a suitable promotion error
557 -- tc :-> APromotionErr TyConPE
558 -- dc :-> APromotionErr RecDataConPE
559 -- See Note [Recursion and promoting data constructors]
560
561 mkPromotionErrorEnv decls
562 = foldr (plusNameEnv . mk_prom_err_env . unLoc)
563 emptyNameEnv decls
564
565 mk_prom_err_env :: TyClDecl GhcRn -> TcTypeEnv
566 mk_prom_err_env (ClassDecl { tcdLName = L _ nm, tcdATs = ats })
567 = unitNameEnv nm (APromotionErr ClassPE)
568 `plusNameEnv`
569 mkNameEnv [ (name, APromotionErr TyConPE)
570 | L _ (FamilyDecl { fdLName = L _ name }) <- ats ]
571
572 mk_prom_err_env (DataDecl { tcdLName = L _ name
573 , tcdDataDefn = HsDataDefn { dd_cons = cons } })
574 = unitNameEnv name (APromotionErr TyConPE)
575 `plusNameEnv`
576 mkNameEnv [ (con, APromotionErr RecDataConPE)
577 | L _ con' <- cons, L _ con <- getConNames con' ]
578
579 mk_prom_err_env decl
580 = unitNameEnv (tcdName decl) (APromotionErr TyConPE)
581 -- Works for family declarations too
582
583 --------------
584 getInitialKinds :: [LTyClDecl GhcRn] -> TcM [TcTyCon]
585 -- Returns a TcTyCon for each TyCon bound by the decls,
586 -- each with its initial kind
587
588 getInitialKinds decls = concatMapM (addLocM getInitialKind) decls
589
590 getInitialKind :: TyClDecl GhcRn -> TcM [TcTyCon]
591 -- Allocate a fresh kind variable for each TyCon and Class
592 -- For each tycon, return a TcTyCon with kind k
593 -- where k is the kind of tc, derived from the LHS
594 -- of the definition (and probably including
595 -- kind unification variables)
596 -- Example: data T a b = ...
597 -- return (T, kv1 -> kv2 -> kv3)
598 --
599 -- This pass deals with (ie incorporates into the kind it produces)
600 -- * The kind signatures on type-variable binders
601 -- * The result kinds signature on a TyClDecl
602 --
603 -- No family instances are passed to getInitialKinds
604
605 getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
606 = do { let cusk = hsDeclHasCusk decl
607 ; (tycon, inner_tcs) <-
608 kcLHsQTyVars name ClassFlavour cusk ktvs $
609 do { inner_tcs <- getFamDeclInitialKinds (Just cusk) ats
610 ; return (constraintKind, inner_tcs) }
611 ; return (tycon : inner_tcs) }
612
613 getInitialKind decl@(DataDecl { tcdLName = L _ name
614 , tcdTyVars = ktvs
615 , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
616 , dd_ND = new_or_data } })
617 = do { (tycon, _) <-
618 kcLHsQTyVars name (newOrDataToFlavour new_or_data) (hsDeclHasCusk decl) ktvs $
619 do { res_k <- case m_sig of
620 Just ksig -> tcLHsKindSig (DataKindCtxt name) ksig
621 Nothing -> return liftedTypeKind
622 ; return (res_k, ()) }
623 ; return [tycon] }
624
625 getInitialKind (FamDecl { tcdFam = decl })
626 = do { tc <- getFamDeclInitialKind Nothing decl
627 ; return [tc] }
628
629 getInitialKind decl@(SynDecl { tcdLName = L _ name
630 , tcdTyVars = ktvs
631 , tcdRhs = rhs })
632 = do { (tycon, _) <- kcLHsQTyVars name TypeSynonymFlavour
633 (hsDeclHasCusk decl) ktvs $
634 do { res_k <- case kind_annotation rhs of
635 Nothing -> newMetaKindVar
636 Just ksig -> tcLHsKindSig (TySynKindCtxt name) ksig
637 ; return (res_k, ()) }
638 ; return [tycon] }
639 where
640 -- Keep this synchronized with 'hsDeclHasCusk'.
641 kind_annotation (L _ ty) = case ty of
642 HsParTy _ lty -> kind_annotation lty
643 HsKindSig _ _ k -> Just k
644 _ -> Nothing
645
646 getInitialKind (DataDecl _ (L _ _) _ _ (XHsDataDefn _)) = panic "getInitialKind"
647 getInitialKind (XTyClDecl _) = panic "getInitialKind"
648
649 ---------------------------------
650 getFamDeclInitialKinds :: Maybe Bool -- if assoc., CUSKness of assoc. class
651 -> [LFamilyDecl GhcRn]
652 -> TcM [TcTyCon]
653 getFamDeclInitialKinds mb_cusk decls
654 = mapM (addLocM (getFamDeclInitialKind mb_cusk)) decls
655
656 getFamDeclInitialKind :: Maybe Bool -- if assoc., CUSKness of assoc. class
657 -> FamilyDecl GhcRn
658 -> TcM TcTyCon
659 getFamDeclInitialKind mb_cusk decl@(FamilyDecl { fdLName = L _ name
660 , fdTyVars = ktvs
661 , fdResultSig = L _ resultSig
662 , fdInfo = info })
663 = do { (tycon, _) <-
664 kcLHsQTyVars name flav cusk ktvs $
665 do { res_k <- case resultSig of
666 KindSig _ ki -> tcLHsKindSig ctxt ki
667 TyVarSig _ (L _ (KindedTyVar _ _ ki)) -> tcLHsKindSig ctxt ki
668 _ -- open type families have * return kind by default
669 | tcFlavourIsOpen flav -> return liftedTypeKind
670 -- closed type families have their return kind inferred
671 -- by default
672 | otherwise -> newMetaKindVar
673 ; return (res_k, ()) }
674 ; return tycon }
675 where
676 cusk = famDeclHasCusk mb_cusk decl
677 flav = case info of
678 DataFamily -> DataFamilyFlavour (isJust mb_cusk)
679 OpenTypeFamily -> OpenTypeFamilyFlavour (isJust mb_cusk)
680 ClosedTypeFamily _ -> ClosedTypeFamilyFlavour
681 ctxt = TyFamResKindCtxt name
682 getFamDeclInitialKind _ (XFamilyDecl _) = panic "getFamDeclInitialKind"
683
684 ------------------------------------------------------------------------
685 kcLTyClDecl :: LTyClDecl GhcRn -> TcM ()
686 -- See Note [Kind checking for type and class decls]
687 kcLTyClDecl (L loc decl)
688 | hsDeclHasCusk decl -- See Note [Skip decls with CUSKs in kcLTyClDecl]
689 = traceTc "kcTyClDecl skipped due to cusk" (ppr tc_name)
690
691 | otherwise
692 = setSrcSpan loc $
693 tcAddDeclCtxt decl $
694 do { traceTc "kcTyClDecl {" (ppr tc_name)
695 ; kcTyClDecl decl
696 ; traceTc "kcTyClDecl done }" (ppr tc_name) }
697 where
698 tc_name = tyClDeclLName decl
699
700 kcTyClDecl :: TyClDecl GhcRn -> TcM ()
701 -- This function is used solely for its side effect on kind variables
702 -- NB kind signatures on the type variables and
703 -- result kind signature have already been dealt with
704 -- by getInitialKind, so we can ignore them here.
705
706 kcTyClDecl (DataDecl { tcdLName = L _ name, tcdDataDefn = defn })
707 | HsDataDefn { dd_cons = cons@(L _ (ConDeclGADT {}) : _), dd_ctxt = L _ [] } <- defn
708 = mapM_ (wrapLocM kcConDecl) cons
709 -- hs_tvs and dd_kindSig already dealt with in getInitialKind
710 -- This must be a GADT-style decl,
711 -- (see invariants of DataDefn declaration)
712 -- so (a) we don't need to bring the hs_tvs into scope, because the
713 -- ConDecls bind all their own variables
714 -- (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it
715
716 | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
717 = kcTyClTyVars name $
718 do { _ <- tcHsContext ctxt
719 ; mapM_ (wrapLocM kcConDecl) cons }
720
721 kcTyClDecl (SynDecl { tcdLName = L _ name, tcdRhs = lrhs })
722 = kcTyClTyVars name $
723 do { syn_tc <- kcLookupTcTyCon name
724 -- NB: check against the result kind that we allocated
725 -- in getInitialKinds.
726 ; discardResult $ tcCheckLHsType lrhs (tyConResKind syn_tc) }
727
728 kcTyClDecl (ClassDecl { tcdLName = L _ name
729 , tcdCtxt = ctxt, tcdSigs = sigs })
730 = kcTyClTyVars name $
731 do { _ <- tcHsContext ctxt
732 ; mapM_ (wrapLocM kc_sig) sigs }
733 where
734 kc_sig (ClassOpSig _ _ nms op_ty)
735 = kcHsSigType (TyConSkol ClassFlavour name) nms op_ty
736 kc_sig _ = return ()
737
738 kcTyClDecl (FamDecl _ (FamilyDecl { fdLName = L _ fam_tc_name
739 , fdInfo = fd_info }))
740 -- closed type families look at their equations, but other families don't
741 -- do anything here
742 = case fd_info of
743 ClosedTypeFamily (Just eqns) ->
744 do { fam_tc <- kcLookupTcTyCon fam_tc_name
745 ; mapM_ (kcTyFamInstEqn fam_tc) eqns }
746 _ -> return ()
747 kcTyClDecl (FamDecl _ (XFamilyDecl _)) = panic "kcTyClDecl"
748 kcTyClDecl (DataDecl _ (L _ _) _ _ (XHsDataDefn _)) = panic "kcTyClDecl"
749 kcTyClDecl (XTyClDecl _) = panic "kcTyClDecl"
750
751 -------------------
752 kcConDecl :: ConDecl GhcRn -> TcM ()
753 kcConDecl (ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs
754 , con_mb_cxt = ex_ctxt, con_args = args })
755 = addErrCtxt (dataConCtxtName [name]) $
756 -- See Note [Use SigTvs in kind-checking pass]
757 kcExplicitTKBndrs ex_tvs $
758 do { _ <- tcHsMbContext ex_ctxt
759 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args) }
760 -- We don't need to check the telescope here, because that's
761 -- done in tcConDecl
762
763 kcConDecl (ConDeclGADT { con_names = names
764 , con_qvars = qtvs, con_mb_cxt = cxt
765 , con_args = args, con_res_ty = res_ty })
766 | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = implicit_tkv_nms }
767 , hsq_explicit = explicit_tkv_nms } <- qtvs
768 = -- Even though the data constructor's type is closed, we
769 -- must still kind-check the type, because that may influence
770 -- the inferred kind of the /type/ constructor. Example:
771 -- data T f a where
772 -- MkT :: f a -> T f a
773 -- If we don't look at MkT we won't get the correct kind
774 -- for the type constructor T
775 addErrCtxt (dataConCtxtName names) $
776 discardResult $
777 kcImplicitTKBndrs implicit_tkv_nms $
778 kcExplicitTKBndrs explicit_tkv_nms $
779 do { _ <- tcHsMbContext cxt
780 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys args)
781 ; _ <- tcHsOpenType res_ty
782 ; return () }
783 kcConDecl (XConDecl _) = panic "kcConDecl"
784 kcConDecl (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _) = panic "kcConDecl"
785
786 {-
787 Note [Recursion and promoting data constructors]
788 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
789 We don't want to allow promotion in a strongly connected component
790 when kind checking.
791
792 Consider:
793 data T f = K (f (K Any))
794
795 When kind checking the `data T' declaration the local env contains the
796 mappings:
797 T -> ATcTyCon <some initial kind>
798 K -> APromotionErr
799
800 APromotionErr is only used for DataCons, and only used during type checking
801 in tcTyClGroup.
802
803 Note [Use SigTvs in kind-checking pass]
804 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
805 Consider
806
807 data Proxy a where
808 MkProxy1 :: forall k (b :: k). Proxy b
809 MkProxy2 :: forall j (c :: j). Proxy c
810
811 It seems reasonable that this should be accepted. But something very strange
812 is going on here: when we're kind-checking this declaration, we need to unify
813 the kind of `a` with k and j -- even though k and j's scopes are local to the type of
814 MkProxy{1,2}. The best approach we've come up with is to use SigTvs during
815 the kind-checking pass. First off, note that it's OK if the kind-checking pass
816 is too permissive: we'll snag the problems in the type-checking pass later.
817 (This extra permissiveness might happen with something like
818
819 data SameKind :: k -> k -> Type
820 data Bad a where
821 MkBad :: forall k1 k2 (a :: k1) (b :: k2). Bad (SameKind a b)
822
823 which would be accepted if k1 and k2 were SigTvs. This is correctly rejected
824 in the second pass, though. Test case: polykinds/SigTvKinds3)
825 Recall that the kind-checking pass exists solely to collect constraints
826 on the kinds and to power unification.
827
828 To achieve the use of SigTvs, we must be careful to use specialized functions
829 that produce SigTvs, not ordinary skolems. This is why we need
830 kcExplicitTKBndrs and kcImplicitTKBndrs in TcHsType, separate from their
831 tc... variants.
832
833 The drawback of this approach is sometimes it will accept a definition that
834 a (hypothetical) declarative specification would likely reject. As a general
835 rule, we don't want to allow polymorphic recursion without a CUSK. Indeed,
836 the whole point of CUSKs is to allow polymorphic recursion. Yet, the SigTvs
837 approach allows a limited form of polymorphic recursion *without* a CUSK.
838
839 To wit:
840 data T a = forall k (b :: k). MkT (T b) Int
841 (test case: dependent/should_compile/T14066a)
842
843 Note that this is polymorphically recursive, with the recursive occurrence
844 of T used at a kind other than a's kind. The approach outlined here accepts
845 this definition, because this kind is still a kind variable (and so the
846 SigTvs unify). Stepping back, I (Richard) have a hard time envisioning a
847 way to describe exactly what declarations will be accepted and which will
848 be rejected (without a CUSK). However, the accepted definitions are indeed
849 well-kinded and any rejected definitions would be accepted with a CUSK,
850 and so this wrinkle need not cause anyone to lose sleep.
851
852 ************************************************************************
853 * *
854 \subsection{Type checking}
855 * *
856 ************************************************************************
857
858 Note [Type checking recursive type and class declarations]
859 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
860 At this point we have completed *kind-checking* of a mutually
861 recursive group of type/class decls (done in kcTyClGroup). However,
862 we discarded the kind-checked types (eg RHSs of data type decls);
863 note that kcTyClDecl returns (). There are two reasons:
864
865 * It's convenient, because we don't have to rebuild a
866 kinded HsDecl (a fairly elaborate type)
867
868 * It's necessary, because after kind-generalisation, the
869 TyCons/Classes may now be kind-polymorphic, and hence need
870 to be given kind arguments.
871
872 Example:
873 data T f a = MkT (f a) (T f a)
874 During kind-checking, we give T the kind T :: k1 -> k2 -> *
875 and figure out constraints on k1, k2 etc. Then we generalise
876 to get T :: forall k. (k->*) -> k -> *
877 So now the (T f a) in the RHS must be elaborated to (T k f a).
878
879 However, during tcTyClDecl of T (above) we will be in a recursive
880 "knot". So we aren't allowed to look at the TyCon T itself; we are only
881 allowed to put it (lazily) in the returned structures. But when
882 kind-checking the RHS of T's decl, we *do* need to know T's kind (so
883 that we can correctly elaboarate (T k f a). How can we get T's kind
884 without looking at T? Delicate answer: during tcTyClDecl, we extend
885
886 *Global* env with T -> ATyCon (the (not yet built) final TyCon for T)
887 *Local* env with T -> ATcTyCon (TcTyCon with the polymorphic kind of T)
888
889 Then:
890
891 * During TcHsType.kcTyVar we look in the *local* env, to get the
892 known kind for T.
893
894 * But in TcHsType.ds_type (and ds_var_app in particular) we look in
895 the *global* env to get the TyCon. But we must be careful not to
896 force the TyCon or we'll get a loop.
897
898 This fancy footwork (with two bindings for T) is only necessary for the
899 TyCons or Classes of this recursive group. Earlier, finished groups,
900 live in the global env only.
901
902 See also Note [Kind checking recursive type and class declarations]
903
904 Note [Kind checking recursive type and class declarations]
905 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
906 Before we can type-check the decls, we must kind check them. This
907 is done by establishing an "initial kind", which is a rather uninformed
908 guess at a tycon's kind (by counting arguments, mainly) and then
909 using this initial kind for recursive occurrences.
910
911 The initial kind is stored in exactly the same way during kind-checking
912 as it is during type-checking (Note [Type checking recursive type and class
913 declarations]): in the *local* environment, with ATcTyCon. But we still
914 must store *something* in the *global* environment. Even though we
915 discard the result of kind-checking, we sometimes need to produce error
916 messages. These error messages will want to refer to the tycons being
917 checked, except that they don't exist yet, and it would be Terribly
918 Annoying to get the error messages to refer back to HsSyn. So we
919 create a TcTyCon and put it in the global env. This tycon can
920 print out its name and knows its kind,
921 but any other action taken on it will panic. Note
922 that TcTyCons are *not* knot-tied, unlike the rather valid but
923 knot-tied ones that occur during type-checking.
924
925 Note [Declarations for wired-in things]
926 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
927 For wired-in things we simply ignore the declaration
928 and take the wired-in information. That avoids complications.
929 e.g. the need to make the data constructor worker name for
930 a constraint tuple match the wired-in one
931 -}
932
933 tcTyClDecl :: RolesInfo -> LTyClDecl GhcRn -> TcM TyCon
934 tcTyClDecl roles_info (L loc decl)
935 | Just thing <- wiredInNameTyThing_maybe (tcdName decl)
936 = case thing of -- See Note [Declarations for wired-in things]
937 ATyCon tc -> return tc
938 _ -> pprPanic "tcTyClDecl" (ppr thing)
939
940 | otherwise
941 = setSrcSpan loc $ tcAddDeclCtxt decl $
942 do { traceTc "---- tcTyClDecl ---- {" (ppr decl)
943 ; tc <- tcTyClDecl1 Nothing roles_info decl
944 ; traceTc "---- tcTyClDecl end ---- }" (ppr tc)
945 ; return tc }
946
947 -- "type family" declarations
948 tcTyClDecl1 :: Maybe Class -> RolesInfo -> TyClDecl GhcRn -> TcM TyCon
949 tcTyClDecl1 parent _roles_info (FamDecl { tcdFam = fd })
950 = tcFamDecl1 parent fd
951
952 -- "type" synonym declaration
953 tcTyClDecl1 _parent roles_info
954 (SynDecl { tcdLName = L _ tc_name, tcdRhs = rhs })
955 = ASSERT( isNothing _parent )
956 tcTyClTyVars tc_name $ \ binders res_kind ->
957 tcTySynRhs roles_info tc_name binders res_kind rhs
958
959 -- "data/newtype" declaration
960 tcTyClDecl1 _parent roles_info
961 (DataDecl { tcdLName = L _ tc_name
962 , tcdDataDefn = defn })
963 = ASSERT( isNothing _parent )
964 tcTyClTyVars tc_name $ \ tycon_binders res_kind ->
965 tcDataDefn roles_info tc_name tycon_binders res_kind defn
966
967 tcTyClDecl1 _parent roles_info
968 (ClassDecl { tcdLName = L _ class_name
969 , tcdCtxt = ctxt, tcdMeths = meths
970 , tcdFDs = fundeps, tcdSigs = sigs
971 , tcdATs = ats, tcdATDefs = at_defs })
972 = ASSERT( isNothing _parent )
973 do { clas <- fixM $ \ clas ->
974 -- We need the knot because 'clas' is passed into tcClassATs
975 tcTyClTyVars class_name $ \ binders res_kind ->
976 do { MASSERT( isConstraintKind res_kind )
977 ; traceTc "tcClassDecl 1" (ppr class_name $$ ppr binders)
978 ; let tycon_name = class_name -- We use the same name
979 roles = roles_info tycon_name -- for TyCon and Class
980
981 ; ctxt' <- solveEqualities $ tcHsContext ctxt
982 ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
983 -- Squeeze out any kind unification variables
984 ; fds' <- mapM (addLocM tc_fundep) fundeps
985 ; sig_stuff <- tcClassSigs class_name sigs meths
986 ; at_stuff <- tcClassATs class_name clas ats at_defs
987 ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
988 -- TODO: Allow us to distinguish between abstract class,
989 -- and concrete class with no methods (maybe by
990 -- specifying a trailing where or not
991 ; is_boot <- tcIsHsBootOrSig
992 ; let body | is_boot, null ctxt', null at_stuff, null sig_stuff
993 = Nothing
994 | otherwise
995 = Just (ctxt', at_stuff, sig_stuff, mindef)
996 ; clas <- buildClass class_name binders roles fds' body
997 ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$
998 ppr fds')
999 ; return clas }
1000
1001 ; return (classTyCon clas) }
1002 where
1003 tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM (tcLookupTyVar . unLoc) tvs1 ;
1004 ; tvs2' <- mapM (tcLookupTyVar . unLoc) tvs2 ;
1005 ; return (tvs1', tvs2') }
1006
1007 tcTyClDecl1 _ _ (XTyClDecl _) = panic "tcTyClDecl1"
1008
1009 tcFamDecl1 :: Maybe Class -> FamilyDecl GhcRn -> TcM TyCon
1010 tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_name)
1011 , fdResultSig = L _ sig, fdTyVars = user_tyvars
1012 , fdInjectivityAnn = inj })
1013 | DataFamily <- fam_info
1014 = tcTyClTyVars tc_name $ \ binders res_kind -> do
1015 { traceTc "data family:" (ppr tc_name)
1016 ; checkFamFlag tc_name
1017
1018 -- Check the kind signature, if any.
1019 -- Data families might have a variable return kind.
1020 -- See See Note [Arity of data families] in FamInstEnv.
1021 ; (extra_binders, final_res_kind) <- tcDataKindSig binders res_kind
1022 ; checkTc (tcIsLiftedTypeKind final_res_kind
1023 || isJust (tcGetCastedTyVar_maybe final_res_kind))
1024 (badKindSig False res_kind)
1025
1026 ; tc_rep_name <- newTyConRepName tc_name
1027 ; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
1028 final_res_kind
1029 (resultVariableName sig)
1030 (DataFamilyTyCon tc_rep_name)
1031 parent NotInjective
1032 ; return tycon }
1033
1034 | OpenTypeFamily <- fam_info
1035 = tcTyClTyVars tc_name $ \ binders res_kind -> do
1036 { traceTc "open type family:" (ppr tc_name)
1037 ; checkFamFlag tc_name
1038 ; inj' <- tcInjectivity binders inj
1039 ; let tycon = mkFamilyTyCon tc_name binders res_kind
1040 (resultVariableName sig) OpenSynFamilyTyCon
1041 parent inj'
1042 ; return tycon }
1043
1044 | ClosedTypeFamily mb_eqns <- fam_info
1045 = -- Closed type families are a little tricky, because they contain the definition
1046 -- of both the type family and the equations for a CoAxiom.
1047 do { traceTc "Closed type family:" (ppr tc_name)
1048 -- the variables in the header scope only over the injectivity
1049 -- declaration but this is not involved here
1050 ; (inj', binders, res_kind)
1051 <- tcTyClTyVars tc_name
1052 $ \ binders res_kind ->
1053 do { inj' <- tcInjectivity binders inj
1054 ; return (inj', binders, res_kind) }
1055
1056 ; checkFamFlag tc_name -- make sure we have -XTypeFamilies
1057
1058 -- If Nothing, this is an abstract family in a hs-boot file;
1059 -- but eqns might be empty in the Just case as well
1060 ; case mb_eqns of
1061 Nothing ->
1062 return $ mkFamilyTyCon tc_name binders res_kind
1063 (resultVariableName sig)
1064 AbstractClosedSynFamilyTyCon parent
1065 inj'
1066 Just eqns -> do {
1067
1068 -- Process the equations, creating CoAxBranches
1069 ; let tc_fam_tc = mkTcTyCon tc_name (ppr user_tyvars) binders res_kind
1070 [] ClosedTypeFamilyFlavour
1071
1072 ; branches <- mapAndReportM (tcTyFamInstEqn tc_fam_tc Nothing) eqns
1073 -- Do not attempt to drop equations dominated by earlier
1074 -- ones here; in the case of mutual recursion with a data
1075 -- type, we get a knot-tying failure. Instead we check
1076 -- for this afterwards, in TcValidity.checkValidCoAxiom
1077 -- Example: tc265
1078
1079 -- Create a CoAxiom, with the correct src location. It is Vitally
1080 -- Important that we do not pass the branches into
1081 -- newFamInstAxiomName. They have types that have been zonked inside
1082 -- the knot and we will die if we look at them. This is OK here
1083 -- because there will only be one axiom, so we don't need to
1084 -- differentiate names.
1085 -- See [Zonking inside the knot] in TcHsType
1086 ; co_ax_name <- newFamInstAxiomName tc_lname []
1087
1088 ; let mb_co_ax
1089 | null eqns = Nothing -- mkBranchedCoAxiom fails on empty list
1090 | otherwise = Just (mkBranchedCoAxiom co_ax_name fam_tc branches)
1091
1092 fam_tc = mkFamilyTyCon tc_name binders res_kind (resultVariableName sig)
1093 (ClosedSynFamilyTyCon mb_co_ax) parent inj'
1094
1095 -- We check for instance validity later, when doing validity
1096 -- checking for the tycon. Exception: checking equations
1097 -- overlap done by dropDominatedAxioms
1098 ; return fam_tc } }
1099
1100 | otherwise = panic "tcFamInst1" -- Silence pattern-exhaustiveness checker
1101 tcFamDecl1 _ (XFamilyDecl _) = panic "tcFamDecl1"
1102
1103 -- | Maybe return a list of Bools that say whether a type family was declared
1104 -- injective in the corresponding type arguments. Length of the list is equal to
1105 -- the number of arguments (including implicit kind/coercion arguments).
1106 -- True on position
1107 -- N means that a function is injective in its Nth argument. False means it is
1108 -- not.
1109 tcInjectivity :: [TyConBinder] -> Maybe (LInjectivityAnn GhcRn)
1110 -> TcM Injectivity
1111 tcInjectivity _ Nothing
1112 = return NotInjective
1113
1114 -- User provided an injectivity annotation, so for each tyvar argument we
1115 -- check whether a type family was declared injective in that argument. We
1116 -- return a list of Bools, where True means that corresponding type variable
1117 -- was mentioned in lInjNames (type family is injective in that argument) and
1118 -- False means that it was not mentioned in lInjNames (type family is not
1119 -- injective in that type variable). We also extend injectivity information to
1120 -- kind variables, so if a user declares:
1121 --
1122 -- type family F (a :: k1) (b :: k2) = (r :: k3) | r -> a
1123 --
1124 -- then we mark both `a` and `k1` as injective.
1125 -- NB: the return kind is considered to be *input* argument to a type family.
1126 -- Since injectivity allows to infer input arguments from the result in theory
1127 -- we should always mark the result kind variable (`k3` in this example) as
1128 -- injective. The reason is that result type has always an assigned kind and
1129 -- therefore we can always infer the result kind if we know the result type.
1130 -- But this does not seem to be useful in any way so we don't do it. (Another
1131 -- reason is that the implementation would not be straightforward.)
1132 tcInjectivity tcbs (Just (L loc (InjectivityAnn _ lInjNames)))
1133 = setSrcSpan loc $
1134 do { let tvs = binderVars tcbs
1135 ; dflags <- getDynFlags
1136 ; checkTc (xopt LangExt.TypeFamilyDependencies dflags)
1137 (text "Illegal injectivity annotation" $$
1138 text "Use TypeFamilyDependencies to allow this")
1139 ; inj_tvs <- mapM (tcLookupTyVar . unLoc) lInjNames
1140 ; inj_tvs <- mapM zonkTcTyVarToTyVar inj_tvs -- zonk the kinds
1141 ; let inj_ktvs = filterVarSet isTyVar $ -- no injective coercion vars
1142 closeOverKinds (mkVarSet inj_tvs)
1143 ; let inj_bools = map (`elemVarSet` inj_ktvs) tvs
1144 ; traceTc "tcInjectivity" (vcat [ ppr tvs, ppr lInjNames, ppr inj_tvs
1145 , ppr inj_ktvs, ppr inj_bools ])
1146 ; return $ Injective inj_bools }
1147
1148 tcTySynRhs :: RolesInfo
1149 -> Name
1150 -> [TyConBinder] -> Kind
1151 -> LHsType GhcRn -> TcM TyCon
1152 tcTySynRhs roles_info tc_name binders res_kind hs_ty
1153 = do { env <- getLclEnv
1154 ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
1155 ; rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
1156 ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
1157 ; let roles = roles_info tc_name
1158 tycon = buildSynTyCon tc_name binders res_kind roles rhs_ty
1159 ; return tycon }
1160
1161 tcDataDefn :: RolesInfo -> Name
1162 -> [TyConBinder] -> Kind
1163 -> HsDataDefn GhcRn -> TcM TyCon
1164 -- NB: not used for newtype/data instances (whether associated or not)
1165 tcDataDefn roles_info
1166 tc_name tycon_binders res_kind
1167 (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
1168 , dd_ctxt = ctxt, dd_kindSig = mb_ksig
1169 , dd_cons = cons })
1170 = do { tcg_env <- getGblEnv
1171 ; let hsc_src = tcg_src tcg_env
1172 ; (extra_bndrs, final_res_kind) <- tcDataKindSig tycon_binders res_kind
1173 ; unless (mk_permissive_kind hsc_src cons) $
1174 checkTc (tcIsLiftedTypeKind final_res_kind) (badKindSig True res_kind)
1175
1176 ; let final_bndrs = tycon_binders `chkAppend` extra_bndrs
1177 roles = roles_info tc_name
1178
1179 ; stupid_tc_theta <- solveEqualities $ tcHsContext ctxt
1180 ; stupid_theta <- zonkTcTypeToTypes emptyZonkEnv
1181 stupid_tc_theta
1182 ; kind_signatures <- xoptM LangExt.KindSignatures
1183
1184 -- Check that we don't use kind signatures without Glasgow extensions
1185 ; when (isJust mb_ksig) $
1186 checkTc (kind_signatures) (badSigTyDecl tc_name)
1187
1188 ; gadt_syntax <- dataDeclChecks tc_name new_or_data stupid_theta cons
1189
1190 ; tycon <- fixM $ \ tycon -> do
1191 { let res_ty = mkTyConApp tycon (mkTyVarTys (binderVars final_bndrs))
1192 ; data_cons <- tcConDecls tycon (final_bndrs, res_ty) cons
1193 ; tc_rhs <- mk_tc_rhs hsc_src tycon data_cons
1194 ; tc_rep_nm <- newTyConRepName tc_name
1195 ; return (mkAlgTyCon tc_name
1196 final_bndrs
1197 final_res_kind
1198 roles
1199 (fmap unLoc cType)
1200 stupid_theta tc_rhs
1201 (VanillaAlgTyCon tc_rep_nm)
1202 gadt_syntax) }
1203 ; traceTc "tcDataDefn" (ppr tc_name $$ ppr tycon_binders $$ ppr extra_bndrs)
1204 ; return tycon }
1205 where
1206 -- Abstract data types in hsig files can have arbitrary kinds,
1207 -- because they may be implemented by type synonyms
1208 -- (which themselves can have arbitrary kinds, not just *)
1209 mk_permissive_kind HsigFile [] = True
1210 mk_permissive_kind _ _ = False
1211
1212 -- In hs-boot, a 'data' declaration with no constructors
1213 -- indicates a nominally distinct abstract data type.
1214 mk_tc_rhs HsBootFile _ []
1215 = return AbstractTyCon
1216
1217 mk_tc_rhs HsigFile _ [] -- ditto
1218 = return AbstractTyCon
1219
1220 mk_tc_rhs _ tycon data_cons
1221 = case new_or_data of
1222 DataType -> return (mkDataTyConRhs data_cons)
1223 NewType -> ASSERT( not (null data_cons) )
1224 mkNewTyConRhs tc_name tycon (head data_cons)
1225 tcDataDefn _ _ _ _ (XHsDataDefn _) = panic "tcDataDefn"
1226
1227 {-
1228 ************************************************************************
1229 * *
1230 Typechecking associated types (in class decls)
1231 (including the associated-type defaults)
1232 * *
1233 ************************************************************************
1234
1235 Note [Associated type defaults]
1236 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1237
1238 The following is an example of associated type defaults:
1239 class C a where
1240 data D a
1241
1242 type F a b :: *
1243 type F a b = [a] -- Default
1244
1245 Note that we can get default definitions only for type families, not data
1246 families.
1247 -}
1248
1249 tcClassATs :: Name -- The class name (not knot-tied)
1250 -> Class -- The class parent of this associated type
1251 -> [LFamilyDecl GhcRn] -- Associated types.
1252 -> [LTyFamDefltEqn GhcRn] -- Associated type defaults.
1253 -> TcM [ClassATItem]
1254 tcClassATs class_name cls ats at_defs
1255 = do { -- Complain about associated type defaults for non associated-types
1256 sequence_ [ failWithTc (badATErr class_name n)
1257 | n <- map at_def_tycon at_defs
1258 , not (n `elemNameSet` at_names) ]
1259 ; mapM tc_at ats }
1260 where
1261 at_def_tycon :: LTyFamDefltEqn GhcRn -> Name
1262 at_def_tycon (L _ eqn) = unLoc (feqn_tycon eqn)
1263
1264 at_fam_name :: LFamilyDecl GhcRn -> Name
1265 at_fam_name (L _ decl) = unLoc (fdLName decl)
1266
1267 at_names = mkNameSet (map at_fam_name ats)
1268
1269 at_defs_map :: NameEnv [LTyFamDefltEqn GhcRn]
1270 -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'
1271 at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv
1272 (at_def_tycon at_def) [at_def])
1273 emptyNameEnv at_defs
1274
1275 tc_at at = do { fam_tc <- addLocM (tcFamDecl1 (Just cls)) at
1276 ; let at_defs = lookupNameEnv at_defs_map (at_fam_name at)
1277 `orElse` []
1278 ; atd <- tcDefaultAssocDecl fam_tc at_defs
1279 ; return (ATI fam_tc atd) }
1280
1281 -------------------------
1282 tcDefaultAssocDecl :: TyCon -- ^ Family TyCon (not knot-tied)
1283 -> [LTyFamDefltEqn GhcRn] -- ^ Defaults
1284 -> TcM (Maybe (Type, SrcSpan)) -- ^ Type checked RHS
1285 tcDefaultAssocDecl _ []
1286 = return Nothing -- No default declaration
1287
1288 tcDefaultAssocDecl _ (d1:_:_)
1289 = failWithTc (text "More than one default declaration for"
1290 <+> ppr (feqn_tycon (unLoc d1)))
1291
1292 tcDefaultAssocDecl fam_tc [L loc (FamEqn { feqn_tycon = L _ tc_name
1293 , feqn_pats = hs_tvs
1294 , feqn_rhs = rhs })]
1295 | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = imp_vars}
1296 , hsq_explicit = exp_vars } <- hs_tvs
1297 = -- See Note [Type-checking default assoc decls]
1298 setSrcSpan loc $
1299 tcAddFamInstCtxt (text "default type instance") tc_name $
1300 do { traceTc "tcDefaultAssocDecl" (ppr tc_name)
1301 ; let fam_tc_name = tyConName fam_tc
1302 fam_arity = length (tyConVisibleTyVars fam_tc)
1303
1304 -- Kind of family check
1305 ; ASSERT( fam_tc_name == tc_name )
1306 checkTc (isTypeFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
1307
1308 -- Arity check
1309 ; checkTc (exp_vars `lengthIs` fam_arity)
1310 (wrongNumberOfParmsErr fam_arity)
1311
1312 -- Typecheck RHS
1313 ; let all_vars = imp_vars ++ map hsLTyVarName exp_vars
1314 pats = map hsLTyVarBndrToType exp_vars
1315
1316 -- NB: Use tcFamTyPats, not tcTyClTyVars. The latter expects to get
1317 -- the LHsQTyVars used for declaring a tycon, but the names here
1318 -- are different.
1319
1320 -- You might think we should pass in some ClsInstInfo, as we're looking
1321 -- at an associated type. But this would be wrong, because an associated
1322 -- type default LHS can mention *different* type variables than the
1323 -- enclosing class. So it's treated more as a freestanding beast.
1324 ; (pats', rhs_ty)
1325 <- tcFamTyPats fam_tc Nothing all_vars pats
1326 (kcTyFamEqnRhs Nothing rhs) $
1327 \tvs pats rhs_kind ->
1328 do { rhs_ty <- solveEqualities $
1329 tcCheckLHsType rhs rhs_kind
1330
1331 -- Zonk the patterns etc into the Type world
1332 ; (ze, _) <- zonkTyBndrsX emptyZonkEnv tvs
1333 ; pats' <- zonkTcTypeToTypes ze pats
1334 ; rhs_ty' <- zonkTcTypeToType ze rhs_ty
1335 ; return (pats', rhs_ty') }
1336
1337 -- See Note [Type-checking default assoc decls]
1338 ; case tcMatchTys pats' (mkTyVarTys (tyConTyVars fam_tc)) of
1339 Just subst -> return (Just (substTyUnchecked subst rhs_ty, loc) )
1340 Nothing -> failWithTc (defaultAssocKindErr fam_tc)
1341 -- We check for well-formedness and validity later,
1342 -- in checkValidClass
1343 }
1344 tcDefaultAssocDecl _ [L _ (XFamEqn _)] = panic "tcDefaultAssocDecl"
1345 tcDefaultAssocDecl _ [L _ (FamEqn _ (L _ _) (XLHsQTyVars _) _ _)]
1346 = panic "tcDefaultAssocDecl"
1347
1348 {- Note [Type-checking default assoc decls]
1349 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1350 Consider this default declaration for an associated type
1351
1352 class C a where
1353 type F (a :: k) b :: *
1354 type F x y = Proxy x -> y
1355
1356 Note that the class variable 'a' doesn't scope over the default assoc
1357 decl (rather oddly I think), and (less oddly) neither does the second
1358 argument 'b' of the associated type 'F', or the kind variable 'k'.
1359 Instead, the default decl is treated more like a top-level type
1360 instance.
1361
1362 However we store the default rhs (Proxy x -> y) in F's TyCon, using
1363 F's own type variables, so we need to convert it to (Proxy a -> b).
1364 We do this by calling tcMatchTys to match them up. This also ensures
1365 that x's kind matches a's and similarly for y and b. The error
1366 message isn't great, mind you. (Trac #11361 was caused by not doing a
1367 proper tcMatchTys here.) -}
1368
1369 -------------------------
1370 kcTyFamInstEqn :: TcTyCon -> LTyFamInstEqn GhcRn -> TcM ()
1371 kcTyFamInstEqn tc_fam_tc
1372 (L loc (HsIB { hsib_ext = HsIBRn { hsib_vars = tv_names }
1373 , hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name
1374 , feqn_pats = pats
1375 , feqn_rhs = hs_ty }}))
1376 = setSrcSpan loc $
1377 do { traceTc "kcTyFamInstEqn" (vcat
1378 [ text "tc_name =" <+> ppr eqn_tc_name
1379 , text "fam_tc =" <+> ppr tc_fam_tc <+> dcolon <+> ppr (tyConKind tc_fam_tc)
1380 , text "hsib_vars =" <+> ppr tv_names
1381 , text "feqn_pats =" <+> ppr pats ])
1382 ; checkTc (fam_name == eqn_tc_name)
1383 (wrongTyFamName fam_name eqn_tc_name)
1384 -- this check reports an arity error instead of a kind error; easier for user
1385 ; checkTc (pats `lengthIs` vis_arity) $
1386 wrongNumberOfParmsErr vis_arity
1387 ; kcFamTyPats tc_fam_tc tv_names pats $ \ rhs_kind ->
1388 discardResult $ kcTyFamEqnRhs Nothing hs_ty rhs_kind }
1389 where
1390 fam_name = tyConName tc_fam_tc
1391 vis_arity = length (tyConVisibleTyVars tc_fam_tc)
1392 kcTyFamInstEqn _ (L _ (XHsImplicitBndrs _)) = panic "kcTyFamInstEqn"
1393 kcTyFamInstEqn _ (L _ (HsIB _ (XFamEqn _))) = panic "kcTyFamInstEqn"
1394
1395 -- Infer the kind of the type on the RHS of a type family eqn. Then use
1396 -- this kind to check the kind of the LHS of the equation. This is useful
1397 -- as the callback to tcFamTyPats.
1398 kcTyFamEqnRhs :: Maybe ClsInstInfo
1399 -> LHsType GhcRn -- ^ Eqn RHS
1400 -> TcKind -- ^ Inferred kind of left-hand side
1401 -> TcM ([TcType], TcKind) -- ^ New pats, inst'ed kind of left-hand side
1402 kcTyFamEqnRhs mb_clsinfo rhs_hs_ty lhs_ki
1403 = do { -- It's still possible the lhs_ki has some foralls. Instantiate these away.
1404 (new_pats, insted_lhs_ki)
1405 <- instantiateTyUntilN mb_kind_env 0 lhs_ki
1406
1407 ; traceTc "kcTyFamEqnRhs" (vcat
1408 [ text "rhs_hs_ty =" <+> ppr rhs_hs_ty
1409 , text "lhs_ki =" <+> ppr lhs_ki
1410 , text "insted_lhs_ki =" <+> ppr insted_lhs_ki
1411 , text "new_pats =" <+> ppr new_pats
1412 ])
1413
1414 ; _ <- tcCheckLHsType rhs_hs_ty insted_lhs_ki
1415
1416 ; return (new_pats, insted_lhs_ki) }
1417 where
1418 mb_kind_env = thdOf3 <$> mb_clsinfo
1419
1420 tcTyFamInstEqn :: TcTyCon -> Maybe ClsInstInfo -> LTyFamInstEqn GhcRn
1421 -> TcM CoAxBranch
1422 -- Needs to be here, not in TcInstDcls, because closed families
1423 -- (typechecked here) have TyFamInstEqns
1424 tcTyFamInstEqn fam_tc mb_clsinfo
1425 (L loc (HsIB { hsib_ext = HsIBRn { hsib_vars = tv_names }
1426 , hsib_body = FamEqn { feqn_tycon = L _ eqn_tc_name
1427 , feqn_pats = pats
1428 , feqn_rhs = hs_ty }}))
1429 = ASSERT( getName fam_tc == eqn_tc_name )
1430 setSrcSpan loc $
1431 tcFamTyPats fam_tc mb_clsinfo tv_names pats
1432 (kcTyFamEqnRhs mb_clsinfo hs_ty) $
1433 \tvs pats res_kind ->
1434 do { rhs_ty <- solveEqualities $ tcCheckLHsType hs_ty res_kind
1435
1436 ; (ze, tvs') <- zonkTyBndrsX emptyZonkEnv tvs
1437 ; pats' <- zonkTcTypeToTypes ze pats
1438 ; rhs_ty' <- zonkTcTypeToType ze rhs_ty
1439 ; traceTc "tcTyFamInstEqn" (ppr fam_tc <+> pprTyVars tvs')
1440 -- don't print out the pats here, as they might be zonked inside the knot
1441 ; return (mkCoAxBranch tvs' [] pats' rhs_ty'
1442 (map (const Nominal) tvs')
1443 loc) }
1444 tcTyFamInstEqn _ _ (L _ (XHsImplicitBndrs _)) = panic "tcTyFamInstEqn"
1445 tcTyFamInstEqn _ _ (L _ (HsIB _ (XFamEqn _))) = panic "tcTyFamInstEqn"
1446
1447 kcDataDefn :: Maybe (VarEnv Kind) -- ^ Possibly, instantiations for vars
1448 -- (associated types only)
1449 -> DataFamInstDecl GhcRn
1450 -> TcKind -- ^ the kind of the tycon applied to pats
1451 -> TcM ([TcType], TcKind)
1452 -- ^ the kind signature might force instantiation
1453 -- of the tycon; this returns any extra args and the inst'ed kind
1454 -- See Note [Instantiating a family tycon]
1455 -- Used for 'data instance' only
1456 -- Ordinary 'data' is handled by kcTyClDec
1457 kcDataDefn mb_kind_env
1458 (DataFamInstDecl { dfid_eqn = HsIB { hsib_body =
1459 FamEqn { feqn_tycon = fam_name
1460 , feqn_pats = pats
1461 , feqn_fixity = fixity
1462 , feqn_rhs = HsDataDefn { dd_ctxt = ctxt
1463 , dd_cons = cons
1464 , dd_kindSig = mb_kind } }}})
1465 res_k
1466 = do { _ <- tcHsContext ctxt
1467 ; checkNoErrs $ mapM_ (wrapLocM kcConDecl) cons
1468 -- See Note [Failing early in kcDataDefn]
1469 ; exp_res_kind <- case mb_kind of
1470 Nothing -> return liftedTypeKind
1471 Just k -> tcLHsKindSig (DataKindCtxt (unLoc fam_name)) k
1472
1473 -- The expected type might have a forall at the type. Normally, we
1474 -- can't skolemise in kinds because we don't have type-level lambda.
1475 -- But here, we're at the top-level of an instance declaration, so
1476 -- we actually have a place to put the regeneralised variables.
1477 -- Thus: skolemise away. cf. Inst.deeplySkolemise and TcUnify.tcSkolemise
1478 -- Examples in indexed-types/should_compile/T12369
1479 ; let (tvs_to_skolemise, inner_res_kind) = tcSplitForAllTys exp_res_kind
1480
1481 ; (skol_subst, tvs') <- tcInstSkolTyVars tvs_to_skolemise
1482 -- we don't need to do anything substantive with the tvs' because the
1483 -- quantifyTyVars in tcFamTyPats will catch them.
1484
1485 ; let inner_res_kind' = substTyAddInScope skol_subst inner_res_kind
1486 tv_prs = zip (map tyVarName tvs_to_skolemise) tvs'
1487 skol_info = SigSkol InstDeclCtxt exp_res_kind tv_prs
1488
1489 ; (ev_binds, (_, new_args, co))
1490 <- solveEqualities $
1491 checkConstraints skol_info tvs' [] $
1492 checkExpectedKindX mb_kind_env pp_fam_app
1493 bogus_ty res_k inner_res_kind'
1494
1495 ; let Pair lhs_ki rhs_ki = tcCoercionKind co
1496
1497 ; when debugIsOn $
1498 do { (_, ev_binds) <- zonkTcEvBinds emptyZonkEnv ev_binds
1499 ; MASSERT( isEmptyTcEvBinds ev_binds )
1500 ; lhs_ki <- zonkTcType lhs_ki
1501 ; rhs_ki <- zonkTcType rhs_ki
1502 ; MASSERT( lhs_ki `tcEqType` rhs_ki ) }
1503
1504 ; return (new_args, lhs_ki) }
1505 where
1506 bogus_ty = pprPanic "kcDataDefn" (ppr fam_name <+> ppr pats)
1507 pp_fam_app = pprFamInstLHS fam_name pats fixity (unLoc ctxt) mb_kind
1508 kcDataDefn _ (DataFamInstDecl (XHsImplicitBndrs _)) _
1509 = panic "kcDataDefn"
1510 kcDataDefn _ (DataFamInstDecl (HsIB _ (FamEqn _ _ _ _ (XHsDataDefn _)))) _
1511 = panic "kcDataDefn"
1512 kcDataDefn _ (DataFamInstDecl (HsIB _ (XFamEqn _))) _
1513 = panic "kcDataDefn"
1514
1515 {-
1516 Kind check type patterns and kind annotate the embedded type variables.
1517 type instance F [a] = rhs
1518
1519 * Here we check that a type instance matches its kind signature, but we do
1520 not check whether there is a pattern for each type index; the latter
1521 check is only required for type synonym instances.
1522
1523 Note [Instantiating a family tycon]
1524 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1525 It's possible that kind-checking the result of a family tycon applied to
1526 its patterns will instantiate the tycon further. For example, we might
1527 have
1528
1529 type family F :: k where
1530 F = Int
1531 F = Maybe
1532
1533 After checking (F :: forall k. k) (with no visible patterns), we still need
1534 to instantiate the k. With data family instances, this problem can be even
1535 more intricate, due to Note [Arity of data families] in FamInstEnv. See
1536 indexed-types/should_compile/T12369 for an example.
1537
1538 So, the kind-checker must return both the new args (that is, Type
1539 (Type -> Type) for the equations above) and the instantiated kind.
1540
1541 Because we don't need this information in the kind-checking phase of
1542 checking closed type families, we don't require these extra pieces of
1543 information in tc_fam_ty_pats.
1544
1545 Note [Failing early in kcDataDefn]
1546 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1547 We need to use checkNoErrs when calling kcConDecl. This is because kcConDecl
1548 calls tcConDecl, which checks that the return type of a GADT-like constructor
1549 is actually an instance of the type head. Without the checkNoErrs, potentially
1550 two bad things could happen:
1551
1552 1) Duplicate error messages, because tcConDecl will be called again during
1553 *type* checking (as opposed to kind checking)
1554 2) If we just keep blindly forging forward after both kind checking and type
1555 checking, we can get a panic in rejigConRes. See Trac #8368.
1556 -}
1557
1558 -----------------
1559 kcFamTyPats :: TcTyCon
1560 -> [Name]
1561 -> HsTyPats GhcRn
1562 -> (TcKind -> TcM ())
1563 -> TcM ()
1564 kcFamTyPats tc_fam_tc tv_names arg_pats kind_checker
1565 = discardResult $
1566 kcImplicitTKBndrs tv_names $
1567 do { let loc = nameSrcSpan name
1568 lhs_fun = L loc (HsTyVar noExt NotPromoted (L loc name))
1569 -- lhs_fun is for error messages only
1570 no_fun = pprPanic "kcFamTyPats" (ppr name)
1571 fun_kind = tyConKind tc_fam_tc
1572
1573 ; (_, _, res_kind_out) <- tcInferApps typeLevelMode Nothing lhs_fun no_fun
1574 fun_kind arg_pats
1575 ; kind_checker res_kind_out }
1576 where
1577 name = tyConName tc_fam_tc
1578
1579 tcFamTyPats :: TyCon
1580 -> Maybe ClsInstInfo
1581 -> [Name] -- Implicitly bound kind/type variable names
1582 -> HsTyPats GhcRn -- Type patterns
1583 -> (TcKind -> TcM ([TcType], TcKind))
1584 -- kind-checker for RHS
1585 -- See Note [Instantiating a family tycon]
1586 -> ( [TcTyVar] -- Kind and type variables
1587 -> [TcType] -- Kind and type arguments
1588 -> TcKind
1589 -> TcM a) -- NB: You can use solveEqualities here.
1590 -> TcM a
1591 -- Check the type patterns of a type or data family instance
1592 -- type instance F <pat1> <pat2> = <type>
1593 -- The 'tyvars' are the free type variables of pats
1594 --
1595 -- NB: The family instance declaration may be an associated one,
1596 -- nested inside an instance decl, thus
1597 -- instance C [a] where
1598 -- type F [a] = ...
1599 -- In that case, the type variable 'a' will *already be in scope*
1600 -- (and, if C is poly-kinded, so will its kind parameter).
1601 tcFamTyPats fam_tc mb_clsinfo
1602 tv_names arg_pats kind_checker thing_inside
1603 = do { -- First, check the arity.
1604 -- If we wait until validity checking, we'll get kind
1605 -- errors below when an arity error will be much easier to
1606 -- understand.
1607 let should_check_arity
1608 | DataFamilyFlavour _ <- flav = False
1609 -- why not check data families? See [Arity of data families] in FamInstEnv
1610 | otherwise = True
1611
1612 ; when should_check_arity $
1613 checkTc (arg_pats `lengthIs` vis_arity) $
1614 wrongNumberOfParmsErr vis_arity
1615 -- report only explicit arguments
1616
1617 ; (fam_used_tvs, (typats, (more_typats, res_kind)))
1618 <- solveEqualities $ -- See Note [Constraints in patterns]
1619 tcImplicitTKBndrs FamInstSkol tv_names $
1620 do { let loc = nameSrcSpan fam_name
1621 lhs_fun = L loc (HsTyVar noExt NotPromoted
1622 (L loc fam_name))
1623 fun_ty = mkTyConApp fam_tc []
1624 fun_kind = tyConKind fam_tc
1625 mb_kind_env = thdOf3 <$> mb_clsinfo
1626
1627 ; (_, args, res_kind_out)
1628 <- tcInferApps typeLevelMode mb_kind_env
1629 lhs_fun fun_ty fun_kind arg_pats
1630
1631 ; stuff <- kind_checker res_kind_out
1632 ; return (args, stuff) }
1633
1634 {- TODO (RAE): This should be cleverer. Consider this:
1635
1636 type family F a
1637
1638 data G a where
1639 MkG :: F a ~ Bool => G a
1640
1641 type family Foo (x :: G a) :: F a
1642 type instance Foo MkG = False
1643
1644 This should probably be accepted. Yet the solveEqualities
1645 will fail, unable to solve (F a ~ Bool)
1646 We want to quantify over that proof.
1647 But see Note [Constraints in patterns]
1648 below, which is missing this piece. -}
1649
1650
1651 -- Find free variables (after zonking) and turn
1652 -- them into skolems, so that we don't subsequently
1653 -- replace a meta kind var with (Any *)
1654 -- Very like kindGeneralize
1655 ; let all_pats = typats `chkAppend` more_typats
1656 ; vars <- zonkTcTypesAndSplitDepVars all_pats
1657 ; qtkvs <- quantifyTyVars emptyVarSet vars
1658
1659 ; when debugIsOn $
1660 do { all_pats <- mapM zonkTcTypeInKnot all_pats
1661 ; MASSERT2( isEmptyVarSet $ coVarsOfTypes all_pats, ppr all_pats ) }
1662 -- This should be the case, because otherwise the solveEqualities
1663 -- above would fail. TODO (RAE): Update once the solveEqualities
1664 -- bit is cleverer.
1665
1666 ; traceTc "tcFamTyPats" (ppr (getName fam_tc)
1667 $$ ppr all_pats $$ ppr qtkvs)
1668 -- Don't print out too much, as we might be in the knot
1669
1670 -- See Note [Free-floating kind vars] in TcHsType
1671 ; let all_mentioned_tvs = mkVarSet qtkvs
1672 -- qtkvs has all the tyvars bound by LHS
1673 -- type patterns
1674 unmentioned_tvs = filterOut (`elemVarSet` all_mentioned_tvs)
1675 fam_used_tvs
1676 -- If there are tyvars left over, we can
1677 -- assume they're free-floating, since they
1678 -- aren't bound by a type pattern
1679 ; checkNoErrs $ reportFloatingKvs fam_name flav
1680 qtkvs unmentioned_tvs
1681
1682 ; scopeTyVars FamInstSkol qtkvs $
1683 -- Extend envt with TcTyVars not TyVars, because the
1684 -- kind checking etc done by thing_inside does not expect
1685 -- to encounter TyVars; it expects TcTyVars
1686 thing_inside qtkvs all_pats res_kind }
1687 where
1688 fam_name = tyConName fam_tc
1689 flav = tyConFlavour fam_tc
1690 vis_arity = length (tyConVisibleTyVars fam_tc)
1691
1692
1693 {-
1694 Note [Constraints in patterns]
1695 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1696 NB: This isn't the whole story. See comment in tcFamTyPats.
1697
1698 At first glance, it seems there is a complicated story to tell in tcFamTyPats
1699 around constraint solving. After all, type family patterns can now do
1700 GADT pattern-matching, which is jolly complicated. But, there's a key fact
1701 which makes this all simple: everything is at top level! There cannot
1702 be untouchable type variables. There can't be weird interaction between
1703 case branches. There can't be global skolems.
1704
1705 This means that the semantics of type-level GADT matching is a little
1706 different than term level. If we have
1707
1708 data G a where
1709 MkGBool :: G Bool
1710
1711 And then
1712
1713 type family F (a :: G k) :: k
1714 type instance F MkGBool = True
1715
1716 we get
1717
1718 axF : F Bool (MkGBool <Bool>) ~ True
1719
1720 Simple! No casting on the RHS, because we can affect the kind parameter
1721 to F.
1722
1723 If we ever introduce local type families, this all gets a lot more
1724 complicated, and will end up looking awfully like term-level GADT
1725 pattern-matching.
1726
1727
1728 ** The new story **
1729
1730 Here is really what we want:
1731
1732 The matcher really can't deal with covars in arbitrary spots in coercions.
1733 But it can deal with covars that are arguments to GADT data constructors.
1734 So we somehow want to allow covars only in precisely those spots, then use
1735 them as givens when checking the RHS. TODO (RAE): Implement plan.
1736
1737
1738 Note [Quantifying over family patterns]
1739 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1740 We need to quantify over two different lots of kind variables:
1741
1742 First, the ones that come from the kinds of the tyvar args of
1743 tcTyVarBndrsKindGen, as usual
1744 data family Dist a
1745
1746 -- Proxy :: forall k. k -> *
1747 data instance Dist (Proxy a) = DP
1748 -- Generates data DistProxy = DP
1749 -- ax8 k (a::k) :: Dist * (Proxy k a) ~ DistProxy k a
1750 -- The 'k' comes from the tcTyVarBndrsKindGen (a::k)
1751
1752 Second, the ones that come from the kind argument of the type family
1753 which we pick up using the (tyCoVarsOfTypes typats) in the result of
1754 the thing_inside of tcHsTyvarBndrsGen.
1755 -- Any :: forall k. k
1756 data instance Dist Any = DA
1757 -- Generates data DistAny k = DA
1758 -- ax7 k :: Dist k (Any k) ~ DistAny k
1759 -- The 'k' comes from kindGeneralizeKinds (Any k)
1760
1761 Note [Quantified kind variables of a family pattern]
1762 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1763 Consider type family KindFam (p :: k1) (q :: k1)
1764 data T :: Maybe k1 -> k2 -> *
1765 type instance KindFam (a :: Maybe k) b = T a b -> Int
1766 The HsBSig for the family patterns will be ([k], [a])
1767
1768 Then in the family instance we want to
1769 * Bring into scope [ "k" -> k:*, "a" -> a:k ]
1770 * Kind-check the RHS
1771 * Quantify the type instance over k and k', as well as a,b, thus
1772 type instance [k, k', a:Maybe k, b:k']
1773 KindFam (Maybe k) k' a b = T k k' a b -> Int
1774
1775 Notice that in the third step we quantify over all the visibly-mentioned
1776 type variables (a,b), but also over the implicitly mentioned kind variables
1777 (k, k'). In this case one is bound explicitly but often there will be
1778 none. The role of the kind signature (a :: Maybe k) is to add a constraint
1779 that 'a' must have that kind, and to bring 'k' into scope.
1780
1781
1782
1783 ************************************************************************
1784 * *
1785 Data types
1786 * *
1787 ************************************************************************
1788 -}
1789
1790 dataDeclChecks :: Name -> NewOrData -> ThetaType -> [LConDecl GhcRn] -> TcM Bool
1791 dataDeclChecks tc_name new_or_data stupid_theta cons
1792 = do { -- Check that we don't use GADT syntax in H98 world
1793 gadtSyntax_ok <- xoptM LangExt.GADTSyntax
1794 ; let gadt_syntax = consUseGadtSyntax cons
1795 ; checkTc (gadtSyntax_ok || not gadt_syntax) (badGadtDecl tc_name)
1796
1797 -- Check that the stupid theta is empty for a GADT-style declaration
1798 ; checkTc (null stupid_theta || not gadt_syntax) (badStupidTheta tc_name)
1799
1800 -- Check that a newtype has exactly one constructor
1801 -- Do this before checking for empty data decls, so that
1802 -- we don't suggest -XEmptyDataDecls for newtypes
1803 ; checkTc (new_or_data == DataType || isSingleton cons)
1804 (newtypeConError tc_name (length cons))
1805
1806 -- Check that there's at least one condecl,
1807 -- or else we're reading an hs-boot file, or -XEmptyDataDecls
1808 ; empty_data_decls <- xoptM LangExt.EmptyDataDecls
1809 ; is_boot <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
1810 ; checkTc (not (null cons) || empty_data_decls || is_boot)
1811 (emptyConDeclsErr tc_name)
1812 ; return gadt_syntax }
1813
1814
1815 -----------------------------------
1816 consUseGadtSyntax :: [LConDecl a] -> Bool
1817 consUseGadtSyntax (L _ (ConDeclGADT { }) : _) = True
1818 consUseGadtSyntax _ = False
1819 -- All constructors have same shape
1820
1821 -----------------------------------
1822 tcConDecls :: TyCon -> ([TyConBinder], Type)
1823 -> [LConDecl GhcRn] -> TcM [DataCon]
1824 -- Why both the tycon tyvars and binders? Because the tyvars
1825 -- have all the names and the binders have the visibilities.
1826 tcConDecls rep_tycon (tmpl_bndrs, res_tmpl)
1827 = concatMapM $ addLocM $
1828 tcConDecl rep_tycon (mkTyConTagMap rep_tycon) tmpl_bndrs res_tmpl
1829 -- It's important that we pay for tag allocation here, once per TyCon,
1830 -- See Note [Constructor tag allocation], fixes #14657
1831
1832 tcConDecl :: TyCon -- Representation tycon. Knot-tied!
1833 -> NameEnv ConTag
1834 -> [TyConBinder] -> Type
1835 -- Return type template (with its template tyvars)
1836 -- (tvs, T tys), where T is the family TyCon
1837 -> ConDecl GhcRn
1838 -> TcM [DataCon]
1839
1840 tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
1841 (ConDeclH98 { con_name = name
1842 , con_ex_tvs = explicit_tkv_nms
1843 , con_mb_cxt = hs_ctxt
1844 , con_args = hs_args })
1845 = addErrCtxt (dataConCtxtName [name]) $
1846 do { -- Get hold of the existential type variables
1847 -- e.g. data T a = forall k (b::k) f. MkT a (f b)
1848 -- Here tmpl_bndrs = {a}
1849 -- hs_qvars = HsQTvs { hsq_implicit = {k}
1850 -- , hsq_explicit = {f,b} }
1851
1852 ; traceTc "tcConDecl 1" (vcat [ ppr name, ppr explicit_tkv_nms ])
1853
1854 ; (exp_tvs, (ctxt, arg_tys, field_lbls, stricts))
1855 <- solveEqualities $
1856 tcExplicitTKBndrs skol_info explicit_tkv_nms $
1857 do { ctxt <- tcHsMbContext hs_ctxt
1858 ; btys <- tcConArgs hs_args
1859 ; field_lbls <- lookupConstructorFields (unLoc name)
1860 ; let (arg_tys, stricts) = unzip btys
1861 ; return (ctxt, arg_tys, field_lbls, stricts)
1862 }
1863
1864 -- exp_tvs have explicit, user-written binding sites
1865 -- the kvs below are those kind variables entirely unmentioned by the user
1866 -- and discovered only by generalization
1867
1868 ; kvs <- quantifyConDecl (mkVarSet (binderVars tmpl_bndrs))
1869 (mkSpecForAllTys exp_tvs $
1870 mkFunTys ctxt $
1871 mkFunTys arg_tys $
1872 unitTy)
1873 -- That type is a lie, of course. (It shouldn't end in ()!)
1874 -- And we could construct a proper result type from the info
1875 -- at hand. But the result would mention only the tmpl_tvs,
1876 -- and so it just creates more work to do it right. Really,
1877 -- we're doing this to get the right behavior around removing
1878 -- any vars bound in exp_binders.
1879
1880 -- Zonk to Types
1881 ; (ze, qkvs) <- zonkTyBndrsX emptyZonkEnv kvs
1882 ; (ze, user_qtvs) <- zonkTyBndrsX ze exp_tvs
1883 ; arg_tys <- zonkTcTypeToTypes ze arg_tys
1884 ; ctxt <- zonkTcTypeToTypes ze ctxt
1885
1886 ; fam_envs <- tcGetFamInstEnvs
1887
1888 -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
1889 ; traceTc "tcConDecl 2" (ppr name $$ ppr field_lbls)
1890 ; let
1891 univ_tvbs = tyConTyVarBinders tmpl_bndrs
1892 univ_tvs = binderVars univ_tvbs
1893 ex_tvbs = mkTyVarBinders Inferred qkvs ++
1894 mkTyVarBinders Specified user_qtvs
1895 ex_tvs = qkvs ++ user_qtvs
1896 -- For H98 datatypes, the user-written tyvar binders are precisely
1897 -- the universals followed by the existentials.
1898 -- See Note [DataCon user type variable binders] in DataCon.
1899 user_tvbs = univ_tvbs ++ ex_tvbs
1900 buildOneDataCon (L _ name) = do
1901 { is_infix <- tcConIsInfixH98 name hs_args
1902 ; rep_nm <- newTyConRepName name
1903
1904 ; buildDataCon fam_envs name is_infix rep_nm
1905 stricts Nothing field_lbls
1906 univ_tvs ex_tvs user_tvbs
1907 [{- no eq_preds -}] ctxt arg_tys
1908 res_tmpl rep_tycon tag_map
1909 -- NB: we put data_tc, the type constructor gotten from the
1910 -- constructor type signature into the data constructor;
1911 -- that way checkValidDataCon can complain if it's wrong.
1912 }
1913 ; traceTc "tcConDecl 2" (ppr name)
1914 ; mapM buildOneDataCon [name]
1915 }
1916 where
1917 skol_info = SigTypeSkol (ConArgCtxt (unLoc name))
1918
1919 tcConDecl rep_tycon tag_map tmpl_bndrs res_tmpl
1920 (ConDeclGADT { con_names = names
1921 , con_qvars = qtvs
1922 , con_mb_cxt = cxt, con_args = hs_args
1923 , con_res_ty = res_ty })
1924 | HsQTvs { hsq_ext = HsQTvsRn { hsq_implicit = implicit_tkv_nms }
1925 , hsq_explicit = explicit_tkv_nms } <- qtvs
1926 = addErrCtxt (dataConCtxtName names) $
1927 do { traceTc "tcConDecl 1" (ppr names)
1928 ; let (L _ name : _) = names
1929 skol_info = DataConSkol name
1930
1931 ; (imp_tvs, (exp_tvs, (ctxt, arg_tys, res_ty, field_lbls, stricts)))
1932 <- solveEqualities $
1933 tcImplicitTKBndrs skol_info implicit_tkv_nms $
1934 tcExplicitTKBndrs skol_info explicit_tkv_nms $
1935 do { ctxt <- tcHsMbContext cxt
1936 ; btys <- tcConArgs hs_args
1937 ; res_ty' <- tcHsLiftedType res_ty
1938 ; field_lbls <- lookupConstructorFields name
1939 ; let (arg_tys, stricts) = unzip btys
1940 ; return (ctxt, arg_tys, res_ty', field_lbls, stricts)
1941 }
1942 ; let user_tvs = imp_tvs ++ exp_tvs
1943
1944 ; tkvs <- quantifyConDecl emptyVarSet (mkSpecForAllTys user_tvs $
1945 mkFunTys ctxt $
1946 mkFunTys arg_tys $
1947 res_ty)
1948
1949 -- Zonk to Types
1950 ; (ze, tkvs) <- zonkTyBndrsX emptyZonkEnv tkvs
1951 ; (ze, user_tvs) <- zonkTyBndrsX ze user_tvs
1952 ; arg_tys <- zonkTcTypeToTypes ze arg_tys
1953 ; ctxt <- zonkTcTypeToTypes ze ctxt
1954 ; res_ty <- zonkTcTypeToType ze res_ty
1955
1956 ; let (univ_tvs, ex_tvs, tkvs', user_tvs', eq_preds, arg_subst)
1957 = rejigConRes tmpl_bndrs res_tmpl tkvs user_tvs res_ty
1958 -- NB: this is a /lazy/ binding, so we pass six thunks to
1959 -- buildDataCon without yet forcing the guards in rejigConRes
1960 -- See Note [Checking GADT return types]
1961
1962 -- Compute the user-written tyvar binders. These have the same
1963 -- tyvars as univ_tvs/ex_tvs, but perhaps in a different order.
1964 -- See Note [DataCon user type variable binders] in DataCon.
1965 tkv_bndrs = mkTyVarBinders Inferred tkvs'
1966 user_tv_bndrs = mkTyVarBinders Specified user_tvs'
1967 all_user_bndrs = tkv_bndrs ++ user_tv_bndrs
1968
1969 ctxt' = substTys arg_subst ctxt
1970 arg_tys' = substTys arg_subst arg_tys
1971 res_ty' = substTy arg_subst res_ty
1972
1973
1974 ; fam_envs <- tcGetFamInstEnvs
1975
1976 -- Can't print univ_tvs, arg_tys etc, because we are inside the knot here
1977 ; traceTc "tcConDecl 2" (ppr names $$ ppr field_lbls)
1978 ; let
1979 buildOneDataCon (L _ name) = do
1980 { is_infix <- tcConIsInfixGADT name hs_args
1981 ; rep_nm <- newTyConRepName name
1982
1983 ; buildDataCon fam_envs name is_infix
1984 rep_nm
1985 stricts Nothing field_lbls
1986 univ_tvs ex_tvs all_user_bndrs eq_preds
1987 ctxt' arg_tys' res_ty' rep_tycon tag_map
1988 -- NB: we put data_tc, the type constructor gotten from the
1989 -- constructor type signature into the data constructor;
1990 -- that way checkValidDataCon can complain if it's wrong.
1991 }
1992 ; traceTc "tcConDecl 2" (ppr names)
1993 ; mapM buildOneDataCon names
1994 }
1995 tcConDecl _ _ _ _ (ConDeclGADT _ _ _ (XLHsQTyVars _) _ _ _ _)
1996 = panic "tcConDecl"
1997 tcConDecl _ _ _ _ (XConDecl _) = panic "tcConDecl"
1998
1999 -- | Produce the telescope of kind variables that this datacon is
2000 -- implicitly quantified over. Incoming type need not be zonked.
2001 quantifyConDecl :: TcTyCoVarSet -- outer tvs, not to be quantified over; zonked
2002 -> TcType -> TcM [TcTyVar]
2003 quantifyConDecl gbl_tvs ty
2004 = do { ty <- zonkTcTypeInKnot ty
2005 ; let fvs = candidateQTyVarsOfType ty
2006 ; quantifyTyVars gbl_tvs fvs }
2007
2008 tcConIsInfixH98 :: Name
2009 -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn])
2010 -> TcM Bool
2011 tcConIsInfixH98 _ details
2012 = case details of
2013 InfixCon {} -> return True
2014 _ -> return False
2015
2016 tcConIsInfixGADT :: Name
2017 -> HsConDetails (LHsType GhcRn) (Located [LConDeclField GhcRn])
2018 -> TcM Bool
2019 tcConIsInfixGADT con details
2020 = case details of
2021 InfixCon {} -> return True
2022 RecCon {} -> return False
2023 PrefixCon arg_tys -- See Note [Infix GADT constructors]
2024 | isSymOcc (getOccName con)
2025 , [_ty1,_ty2] <- arg_tys
2026 -> do { fix_env <- getFixityEnv
2027 ; return (con `elemNameEnv` fix_env) }
2028 | otherwise -> return False
2029
2030 tcConArgs :: HsConDeclDetails GhcRn
2031 -> TcM [(TcType, HsSrcBang)]
2032 tcConArgs (PrefixCon btys)
2033 = mapM tcConArg btys
2034 tcConArgs (InfixCon bty1 bty2)
2035 = do { bty1' <- tcConArg bty1
2036 ; bty2' <- tcConArg bty2
2037 ; return [bty1', bty2'] }
2038 tcConArgs (RecCon fields)
2039 = mapM tcConArg btys
2040 where
2041 -- We need a one-to-one mapping from field_names to btys
2042 combined = map (\(L _ f) -> (cd_fld_names f,cd_fld_type f)) (unLoc fields)
2043 explode (ns,ty) = zip ns (repeat ty)
2044 exploded = concatMap explode combined
2045 (_,btys) = unzip exploded
2046
2047
2048 tcConArg :: LHsType GhcRn -> TcM (TcType, HsSrcBang)
2049 tcConArg bty
2050 = do { traceTc "tcConArg 1" (ppr bty)
2051 ; arg_ty <- tcHsOpenType (getBangType bty)
2052 -- Newtypes can't have unboxed types, but we check
2053 -- that in checkValidDataCon; this tcConArg stuff
2054 -- doesn't happen for GADT-style declarations
2055 ; traceTc "tcConArg 2" (ppr bty)
2056 ; return (arg_ty, getBangStrictness bty) }
2057
2058 {-
2059 Note [Infix GADT constructors]
2060 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2061 We do not currently have syntax to declare an infix constructor in GADT syntax,
2062 but it makes a (small) difference to the Show instance. So as a slightly
2063 ad-hoc solution, we regard a GADT data constructor as infix if
2064 a) it is an operator symbol
2065 b) it has two arguments
2066 c) there is a fixity declaration for it
2067 For example:
2068 infix 6 (:--:)
2069 data T a where
2070 (:--:) :: t1 -> t2 -> T Int
2071
2072
2073 Note [Checking GADT return types]
2074 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2075 There is a delicacy around checking the return types of a datacon. The
2076 central problem is dealing with a declaration like
2077
2078 data T a where
2079 MkT :: T a -> Q a
2080
2081 Note that the return type of MkT is totally bogus. When creating the T
2082 tycon, we also need to create the MkT datacon, which must have a "rejigged"
2083 return type. That is, the MkT datacon's type must be transformed to have
2084 a uniform return type with explicit coercions for GADT-like type parameters.
2085 This rejigging is what rejigConRes does. The problem is, though, that checking
2086 that the return type is appropriate is much easier when done over *Type*,
2087 not *HsType*, and doing a call to tcMatchTy will loop because T isn't fully
2088 defined yet.
2089
2090 So, we want to make rejigConRes lazy and then check the validity of
2091 the return type in checkValidDataCon. To do this we /always/ return a
2092 6-tuple from rejigConRes (so that we can compute the return type from it, which
2093 checkValidDataCon needs), but the first three fields may be bogus if
2094 the return type isn't valid (the last equation for rejigConRes).
2095
2096 This is better than an earlier solution which reduced the number of
2097 errors reported in one pass. See Trac #7175, and #10836.
2098 -}
2099
2100 -- Example
2101 -- data instance T (b,c) where
2102 -- TI :: forall e. e -> T (e,e)
2103 --
2104 -- The representation tycon looks like this:
2105 -- data :R7T b c where
2106 -- TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
2107 -- In this case orig_res_ty = T (e,e)
2108
2109 rejigConRes :: [TyConBinder] -> Type -- Template for result type; e.g.
2110 -- data instance T [a] b c ...
2111 -- gives template ([a,b,c], T [a] b c)
2112 -- Type must be of kind *!
2113 -> [TyVar] -- The constructor's user-written, inferred
2114 -- type variables
2115 -> [TyVar] -- The constructor's user-written, specified
2116 -- type variables
2117 -> Type -- res_ty type must be of kind *
2118 -> ([TyVar], -- Universal
2119 [TyVar], -- Existential (distinct OccNames from univs)
2120 [TyVar], -- The constructor's rejigged, user-written,
2121 -- inferred type variables
2122 [TyVar], -- The constructor's rejigged, user-written,
2123 -- specified type variables
2124 [EqSpec], -- Equality predicates
2125 TCvSubst) -- Substitution to apply to argument types
2126 -- We don't check that the TyCon given in the ResTy is
2127 -- the same as the parent tycon, because checkValidDataCon will do it
2128
2129 rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty
2130 -- E.g. data T [a] b c where
2131 -- MkT :: forall x y z. T [(x,y)] z z
2132 -- The {a,b,c} are the tmpl_tvs, and the {x,y,z} are the dc_tvs
2133 -- (NB: unlike the H98 case, the dc_tvs are not all existential)
2134 -- Then we generate
2135 -- Univ tyvars Eq-spec
2136 -- a a~(x,y)
2137 -- b b~z
2138 -- z
2139 -- Existentials are the leftover type vars: [x,y]
2140 -- The user-written type variables are what is listed in the forall:
2141 -- [x, y, z] (all specified). We must rejig these as well.
2142 -- See Note [DataCon user type variable binders] in DataCon.
2143 -- So we return ( [a,b,z], [x,y]
2144 -- , [], [x,y,z]
2145 -- , [a~(x,y),b~z], <arg-subst> )
2146 | Just subst <- ASSERT( isLiftedTypeKind (typeKind res_ty) )
2147 ASSERT( isLiftedTypeKind (typeKind res_tmpl) )
2148 tcMatchTy res_tmpl res_ty
2149 = let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tmpl_tvs dc_tvs subst
2150 raw_ex_tvs = dc_tvs `minusList` univ_tvs
2151 (arg_subst, substed_ex_tvs)
2152 = mapAccumL substTyVarBndr kind_subst raw_ex_tvs
2153
2154 -- After rejigging the existential tyvars, the resulting substitution
2155 -- gives us exactly what we need to rejig the user-written tyvars,
2156 -- since the dcUserTyVarBinders invariant guarantees that the
2157 -- substitution has *all* the tyvars in its domain.
2158 -- See Note [DataCon user type variable binders] in DataCon.
2159 subst_user_tvs = map (getTyVar "rejigConRes" . substTyVar arg_subst)
2160 substed_inferred_tvs = subst_user_tvs dc_inferred_tvs
2161 substed_specified_tvs = subst_user_tvs dc_specified_tvs
2162
2163 substed_eqs = map (substEqSpec arg_subst) raw_eqs
2164 in
2165 (univ_tvs, substed_ex_tvs, substed_inferred_tvs, substed_specified_tvs,
2166 substed_eqs, arg_subst)
2167
2168 | otherwise
2169 -- If the return type of the data constructor doesn't match the parent
2170 -- type constructor, or the arity is wrong, the tcMatchTy will fail
2171 -- e.g data T a b where
2172 -- T1 :: Maybe a -- Wrong tycon
2173 -- T2 :: T [a] -- Wrong arity
2174 -- We are detect that later, in checkValidDataCon, but meanwhile
2175 -- we must do *something*, not just crash. So we do something simple
2176 -- albeit bogus, relying on checkValidDataCon to check the
2177 -- bad-result-type error before seeing that the other fields look odd
2178 -- See Note [Checking GADT return types]
2179 = (tmpl_tvs, dc_tvs `minusList` tmpl_tvs, dc_inferred_tvs, dc_specified_tvs,
2180 [], emptyTCvSubst)
2181 where
2182 dc_tvs = dc_inferred_tvs ++ dc_specified_tvs
2183 tmpl_tvs = binderVars tmpl_bndrs
2184
2185 {- Note [mkGADTVars]
2186 ~~~~~~~~~~~~~~~~~~~~
2187 Running example:
2188
2189 data T (k1 :: *) (k2 :: *) (a :: k2) (b :: k2) where
2190 MkT :: forall (x1 : *) (y :: x1) (z :: *).
2191 T x1 * (Proxy (y :: x1), z) z
2192
2193 We need the rejigged type to be
2194
2195 MkT :: forall (x1 :: *) (k2 :: *) (a :: k2) (b :: k2).
2196 forall (y :: x1) (z :: *).
2197 (k2 ~ *, a ~ (Proxy x1 y, z), b ~ z)
2198 => T x1 k2 a b
2199
2200 You might naively expect that z should become a universal tyvar,
2201 not an existential. (After all, x1 becomes a universal tyvar.)
2202 But z has kind * while b has kind k2, so the return type
2203 T x1 k2 a z
2204 is ill-kinded. Another way to say it is this: the universal
2205 tyvars must have exactly the same kinds as the tyConTyVars.
2206
2207 So we need an existential tyvar and a heterogeneous equality
2208 constraint. (The b ~ z is a bit redundant with the k2 ~ * that
2209 comes before in that b ~ z implies k2 ~ *. I'm sure we could do
2210 some analysis that could eliminate k2 ~ *. But we don't do this
2211 yet.)
2212
2213 The data con signature has already been fully kind-checked.
2214 The return type
2215
2216 T x1 * (Proxy (y :: x1), z) z
2217 becomes
2218 qtkvs = [x1 :: *, y :: x1, z :: *]
2219 res_tmpl = T x1 * (Proxy x1 y, z) z
2220
2221 We start off by matching (T k1 k2 a b) with (T x1 * (Proxy x1 y, z) z). We
2222 know this match will succeed because of the validity check (actually done
2223 later, but laziness saves us -- see Note [Checking GADT return types]).
2224 Thus, we get
2225
2226 subst := { k1 |-> x1, k2 |-> *, a |-> (Proxy x1 y, z), b |-> z }
2227
2228 Now, we need to figure out what the GADT equalities should be. In this case,
2229 we *don't* want (k1 ~ x1) to be a GADT equality: it should just be a
2230 renaming. The others should be GADT equalities. We also need to make
2231 sure that the universally-quantified variables of the datacon match up
2232 with the tyvars of the tycon, as required for Core context well-formedness.
2233 (This last bit is why we have to rejig at all!)
2234
2235 `choose` walks down the tycon tyvars, figuring out what to do with each one.
2236 It carries two substitutions:
2237 - t_sub's domain is *template* or *tycon* tyvars, mapping them to variables
2238 mentioned in the datacon signature.
2239 - r_sub's domain is *result* tyvars, names written by the programmer in
2240 the datacon signature. The final rejigged type will use these names, but
2241 the subst is still needed because sometimes the printed name of these variables
2242 is different. (See choose_tv_name, below.)
2243
2244 Before explaining the details of `choose`, let's just look at its operation
2245 on our example:
2246
2247 choose [] [] {} {} [k1, k2, a, b]
2248 --> -- first branch of `case` statement
2249 choose
2250 univs: [x1 :: *]
2251 eq_spec: []
2252 t_sub: {k1 |-> x1}
2253 r_sub: {x1 |-> x1}
2254 t_tvs: [k2, a, b]
2255 --> -- second branch of `case` statement
2256 choose
2257 univs: [k2 :: *, x1 :: *]
2258 eq_spec: [k2 ~ *]
2259 t_sub: {k1 |-> x1, k2 |-> k2}
2260 r_sub: {x1 |-> x1}
2261 t_tvs: [a, b]
2262 --> -- second branch of `case` statement
2263 choose
2264 univs: [a :: k2, k2 :: *, x1 :: *]
2265 eq_spec: [ a ~ (Proxy x1 y, z)
2266 , k2 ~ * ]
2267 t_sub: {k1 |-> x1, k2 |-> k2, a |-> a}
2268 r_sub: {x1 |-> x1}
2269 t_tvs: [b]
2270 --> -- second branch of `case` statement
2271 choose
2272 univs: [b :: k2, a :: k2, k2 :: *, x1 :: *]
2273 eq_spec: [ b ~ z
2274 , a ~ (Proxy x1 y, z)
2275 , k2 ~ * ]
2276 t_sub: {k1 |-> x1, k2 |-> k2, a |-> a, b |-> z}
2277 r_sub: {x1 |-> x1}
2278 t_tvs: []
2279 --> -- end of recursion
2280 ( [x1 :: *, k2 :: *, a :: k2, b :: k2]
2281 , [k2 ~ *, a ~ (Proxy x1 y, z), b ~ z]
2282 , {x1 |-> x1} )
2283
2284 `choose` looks up each tycon tyvar in the matching (it *must* be matched!).
2285
2286 * If it finds a bare result tyvar (the first branch of the `case`
2287 statement), it checks to make sure that the result tyvar isn't yet
2288 in the list of univ_tvs. If it is in that list, then we have a
2289 repeated variable in the return type, and we in fact need a GADT
2290 equality.
2291
2292 * It then checks to make sure that the kind of the result tyvar
2293 matches the kind of the template tyvar. This check is what forces
2294 `z` to be existential, as it should be, explained above.
2295
2296 * Assuming no repeated variables or kind-changing, we wish to use the
2297 variable name given in the datacon signature (that is, `x1` not
2298 `k1`), not the tycon signature (which may have been made up by
2299 GHC). So, we add a mapping from the tycon tyvar to the result tyvar
2300 to t_sub.
2301
2302 * If we discover that a mapping in `subst` gives us a non-tyvar (the
2303 second branch of the `case` statement), then we have a GADT equality
2304 to create. We create a fresh equality, but we don't extend any
2305 substitutions. The template variable substitution is meant for use
2306 in universal tyvar kinds, and these shouldn't be affected by any
2307 GADT equalities.
2308
2309 This whole algorithm is quite delicate, indeed. I (Richard E.) see two ways
2310 of simplifying it:
2311
2312 1) The first branch of the `case` statement is really an optimization, used
2313 in order to get fewer GADT equalities. It might be possible to make a GADT
2314 equality for *every* univ. tyvar, even if the equality is trivial, and then
2315 either deal with the bigger type or somehow reduce it later.
2316
2317 2) This algorithm strives to use the names for type variables as specified
2318 by the user in the datacon signature. If we always used the tycon tyvar
2319 names, for example, this would be simplified. This change would almost
2320 certainly degrade error messages a bit, though.
2321 -}
2322
2323 -- ^ From information about a source datacon definition, extract out
2324 -- what the universal variables and the GADT equalities should be.
2325 -- See Note [mkGADTVars].
2326 mkGADTVars :: [TyVar] -- ^ The tycon vars
2327 -> [TyVar] -- ^ The datacon vars
2328 -> TCvSubst -- ^ The matching between the template result type
2329 -- and the actual result type
2330 -> ( [TyVar]
2331 , [EqSpec]
2332 , TCvSubst ) -- ^ The univ. variables, the GADT equalities,
2333 -- and a subst to apply to the GADT equalities
2334 -- and existentials.
2335 mkGADTVars tmpl_tvs dc_tvs subst
2336 = choose [] [] empty_subst empty_subst tmpl_tvs
2337 where
2338 in_scope = mkInScopeSet (mkVarSet tmpl_tvs `unionVarSet` mkVarSet dc_tvs)
2339 `unionInScope` getTCvInScope subst
2340 empty_subst = mkEmptyTCvSubst in_scope
2341
2342 choose :: [TyVar] -- accumulator of univ tvs, reversed
2343 -> [EqSpec] -- accumulator of GADT equalities, reversed
2344 -> TCvSubst -- template substitution
2345 -> TCvSubst -- res. substitution
2346 -> [TyVar] -- template tvs (the univ tvs passed in)
2347 -> ( [TyVar] -- the univ_tvs
2348 , [EqSpec] -- GADT equalities
2349 , TCvSubst ) -- a substitution to fix kinds in ex_tvs
2350
2351 choose univs eqs _t_sub r_sub []
2352 = (reverse univs, reverse eqs, r_sub)
2353 choose univs eqs t_sub r_sub (t_tv:t_tvs)
2354 | Just r_ty <- lookupTyVar subst t_tv
2355 = case getTyVar_maybe r_ty of
2356 Just r_tv
2357 | not (r_tv `elem` univs)
2358 , tyVarKind r_tv `eqType` (substTy t_sub (tyVarKind t_tv))
2359 -> -- simple, well-kinded variable substitution.
2360 choose (r_tv:univs) eqs
2361 (extendTvSubst t_sub t_tv r_ty')
2362 (extendTvSubst r_sub r_tv r_ty')
2363 t_tvs
2364 where
2365 r_tv1 = setTyVarName r_tv (choose_tv_name r_tv t_tv)
2366 r_ty' = mkTyVarTy r_tv1
2367
2368 -- Not a simple substitution: make an equality predicate
2369 _ -> choose (t_tv':univs) (mkEqSpec t_tv' r_ty : eqs)
2370 (extendTvSubst t_sub t_tv (mkTyVarTy t_tv'))
2371 -- We've updated the kind of t_tv,
2372 -- so add it to t_sub (Trac #14162)
2373 r_sub t_tvs
2374 where
2375 t_tv' = updateTyVarKind (substTy t_sub) t_tv
2376
2377 | otherwise
2378 = pprPanic "mkGADTVars" (ppr tmpl_tvs $$ ppr subst)
2379
2380 -- choose an appropriate name for a univ tyvar.
2381 -- This *must* preserve the Unique of the result tv, so that we
2382 -- can detect repeated variables. It prefers user-specified names
2383 -- over system names. A result variable with a system name can
2384 -- happen with GHC-generated implicit kind variables.
2385 choose_tv_name :: TyVar -> TyVar -> Name
2386 choose_tv_name r_tv t_tv
2387 | isSystemName r_tv_name
2388 = setNameUnique t_tv_name (getUnique r_tv_name)
2389
2390 | otherwise
2391 = r_tv_name
2392
2393 where
2394 r_tv_name = getName r_tv
2395 t_tv_name = getName t_tv
2396
2397 {-
2398 Note [Substitution in template variables kinds]
2399 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2400
2401 data G (a :: Maybe k) where
2402 MkG :: G Nothing
2403
2404 With explicit kind variables
2405
2406 data G k (a :: Maybe k) where
2407 MkG :: G k1 (Nothing k1)
2408
2409 Note how k1 is distinct from k. So, when we match the template
2410 `G k a` against `G k1 (Nothing k1)`, we get a subst
2411 [ k |-> k1, a |-> Nothing k1 ]. Even though this subst has two
2412 mappings, we surely don't want to add (k, k1) to the list of
2413 GADT equalities -- that would be overly complex and would create
2414 more untouchable variables than we need. So, when figuring out
2415 which tyvars are GADT-like and which aren't (the fundamental
2416 job of `choose`), we want to treat `k` as *not* GADT-like.
2417 Instead, we wish to substitute in `a`'s kind, to get (a :: Maybe k1)
2418 instead of (a :: Maybe k). This is the reason for dealing
2419 with a substitution in here.
2420
2421 However, we do not *always* want to substitute. Consider
2422
2423 data H (a :: k) where
2424 MkH :: H Int
2425
2426 With explicit kind variables:
2427
2428 data H k (a :: k) where
2429 MkH :: H * Int
2430
2431 Here, we have a kind-indexed GADT. The subst in question is
2432 [ k |-> *, a |-> Int ]. Now, we *don't* want to substitute in `a`'s
2433 kind, because that would give a constructor with the type
2434
2435 MkH :: forall (k :: *) (a :: *). (k ~ *) -> (a ~ Int) -> H k a
2436
2437 The problem here is that a's kind is wrong -- it needs to be k, not *!
2438 So, if the matching for a variable is anything but another bare variable,
2439 we drop the mapping from the substitution before proceeding. This
2440 was not an issue before kind-indexed GADTs because this case could
2441 never happen.
2442
2443 ************************************************************************
2444 * *
2445 Validity checking
2446 * *
2447 ************************************************************************
2448
2449 Validity checking is done once the mutually-recursive knot has been
2450 tied, so we can look at things freely.
2451 -}
2452
2453 checkValidTyCl :: TyCon -> TcM TyCon
2454 checkValidTyCl tc
2455 = setSrcSpan (getSrcSpan tc) $
2456 addTyConCtxt tc $
2457 recoverM recovery_code
2458 (do { traceTc "Starting validity for tycon" (ppr tc)
2459 ; checkValidTyCon tc
2460 ; traceTc "Done validity for tycon" (ppr tc)
2461 ; return tc })
2462 where
2463 recovery_code -- See Note [Recover from validity error]
2464 = do { traceTc "Aborted validity for tycon" (ppr tc)
2465 ; return fake_tc }
2466 fake_tc | not (isClassTyCon tc)
2467 = makeRecoveryTyCon tc
2468 | otherwise
2469 = tc
2470
2471 {- Note [Recover from validity error]
2472 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2473 We recover from a validity error in a type or class, which allows us
2474 to report multiple validity errors. In the failure case we return a
2475 TyCon of the right kind, but with no interesting behaviour
2476 (makeRecoveryTyCon). Why? Suppose we have
2477 type T a = Fun
2478 where Fun is a type family of arity 1. The RHS is invalid, but we
2479 want to go on checking validity of subsequent type declarations.
2480 So we replace T with an abstract TyCon which will do no harm.
2481 See indexed-types/should_fail/BadSock and Trac #10896
2482
2483 Painfully, though, we *don't* want to do this for classes.
2484 Consider tcfail041:
2485 class (?x::Int) => C a where ...
2486 instance C Int
2487 The class is invalid because of the superclass constraint. But
2488 we still want it to look like a /class/, else the instance bleats
2489 that the instance is mal-formed because it hasn't got a class in
2490 the head.
2491 -}
2492
2493 -------------------------
2494 -- For data types declared with record syntax, we require
2495 -- that each constructor that has a field 'f'
2496 -- (a) has the same result type
2497 -- (b) has the same type for 'f'
2498 -- module alpha conversion of the quantified type variables
2499 -- of the constructor.
2500 --
2501 -- Note that we allow existentials to match because the
2502 -- fields can never meet. E.g
2503 -- data T where
2504 -- T1 { f1 :: b, f2 :: a, f3 ::Int } :: T
2505 -- T2 { f1 :: c, f2 :: c, f3 ::Int } :: T
2506 -- Here we do not complain about f1,f2 because they are existential
2507
2508 checkValidTyCon :: TyCon -> TcM ()
2509 checkValidTyCon tc
2510 | isPrimTyCon tc -- Happens when Haddock'ing GHC.Prim
2511 = return ()
2512
2513 | otherwise
2514 = do { traceTc "checkValidTyCon" (ppr tc $$ ppr (tyConClass_maybe tc))
2515 ; if | Just cl <- tyConClass_maybe tc
2516 -> checkValidClass cl
2517
2518 | Just syn_rhs <- synTyConRhs_maybe tc
2519 -> do { checkValidType syn_ctxt syn_rhs
2520 ; checkTySynRhs syn_ctxt syn_rhs }
2521
2522 | Just fam_flav <- famTyConFlav_maybe tc
2523 -> case fam_flav of
2524 { ClosedSynFamilyTyCon (Just ax)
2525 -> tcAddClosedTypeFamilyDeclCtxt tc $
2526 checkValidCoAxiom ax
2527 ; ClosedSynFamilyTyCon Nothing -> return ()
2528 ; AbstractClosedSynFamilyTyCon ->
2529 do { hsBoot <- tcIsHsBootOrSig
2530 ; checkTc hsBoot $
2531 text "You may define an abstract closed type family" $$
2532 text "only in a .hs-boot file" }
2533 ; DataFamilyTyCon {} -> return ()
2534 ; OpenSynFamilyTyCon -> return ()
2535 ; BuiltInSynFamTyCon _ -> return () }
2536
2537 | otherwise -> do
2538 { -- Check the context on the data decl
2539 traceTc "cvtc1" (ppr tc)
2540 ; checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc)
2541
2542 ; traceTc "cvtc2" (ppr tc)
2543
2544 ; dflags <- getDynFlags
2545 ; existential_ok <- xoptM LangExt.ExistentialQuantification
2546 ; gadt_ok <- xoptM LangExt.GADTs
2547 ; let ex_ok = existential_ok || gadt_ok
2548 -- Data cons can have existential context
2549 ; mapM_ (checkValidDataCon dflags ex_ok tc) data_cons
2550 ; mapM_ (checkPartialRecordField data_cons) (tyConFieldLabels tc)
2551
2552 -- Check that fields with the same name share a type
2553 ; mapM_ check_fields groups }}
2554 where
2555 syn_ctxt = TySynCtxt name
2556 name = tyConName tc
2557 data_cons = tyConDataCons tc
2558
2559 groups = equivClasses cmp_fld (concatMap get_fields data_cons)
2560 cmp_fld (f1,_) (f2,_) = flLabel f1 `compare` flLabel f2
2561 get_fields con = dataConFieldLabels con `zip` repeat con
2562 -- dataConFieldLabels may return the empty list, which is fine
2563
2564 -- See Note [GADT record selectors] in TcTyDecls
2565 -- We must check (a) that the named field has the same
2566 -- type in each constructor
2567 -- (b) that those constructors have the same result type
2568 --
2569 -- However, the constructors may have differently named type variable
2570 -- and (worse) we don't know how the correspond to each other. E.g.
2571 -- C1 :: forall a b. { f :: a, g :: b } -> T a b
2572 -- C2 :: forall d c. { f :: c, g :: c } -> T c d
2573 --
2574 -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
2575 -- result type against other candidates' types BOTH WAYS ROUND.
2576 -- If they magically agrees, take the substitution and
2577 -- apply them to the latter ones, and see if they match perfectly.
2578 check_fields ((label, con1) :| other_fields)
2579 -- These fields all have the same name, but are from
2580 -- different constructors in the data type
2581 = recoverM (return ()) $ mapM_ checkOne other_fields
2582 -- Check that all the fields in the group have the same type
2583 -- NB: this check assumes that all the constructors of a given
2584 -- data type use the same type variables
2585 where
2586 (_, _, _, res1) = dataConSig con1
2587 fty1 = dataConFieldType con1 lbl
2588 lbl = flLabel label
2589
2590 checkOne (_, con2) -- Do it both ways to ensure they are structurally identical
2591 = do { checkFieldCompat lbl con1 con2 res1 res2 fty1 fty2
2592 ; checkFieldCompat lbl con2 con1 res2 res1 fty2 fty1 }
2593 where
2594 (_, _, _, res2) = dataConSig con2
2595 fty2 = dataConFieldType con2 lbl
2596
2597 checkPartialRecordField :: [DataCon] -> FieldLabel -> TcM ()
2598 -- Checks the partial record field selector, and warns.
2599 -- See Note [Checking partial record field]
2600 checkPartialRecordField all_cons fld
2601 = setSrcSpan loc $
2602 warnIfFlag Opt_WarnPartialFields
2603 (not is_exhaustive && not (startsWithUnderscore occ_name))
2604 (sep [text "Use of partial record field selector" <> colon,
2605 nest 2 $ quotes (ppr occ_name)])
2606 where
2607 sel_name = flSelector fld
2608 loc = getSrcSpan sel_name
2609 occ_name = getOccName sel_name
2610
2611 (cons_with_field, cons_without_field) = partition has_field all_cons
2612 has_field con = fld `elem` (dataConFieldLabels con)
2613 is_exhaustive = all (dataConCannotMatch inst_tys) cons_without_field
2614
2615 con1 = ASSERT( not (null cons_with_field) ) head cons_with_field
2616 (univ_tvs, _, eq_spec, _, _, _) = dataConFullSig con1
2617 eq_subst = mkTvSubstPrs (map eqSpecPair eq_spec)
2618 inst_tys = substTyVars eq_subst univ_tvs
2619
2620 checkFieldCompat :: FieldLabelString -> DataCon -> DataCon
2621 -> Type -> Type -> Type -> Type -> TcM ()
2622 checkFieldCompat fld con1 con2 res1 res2 fty1 fty2
2623 = do { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
2624 ; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
2625 where
2626 mb_subst1 = tcMatchTy res1 res2
2627 mb_subst2 = tcMatchTyX (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
2628
2629 -------------------------------
2630 checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM ()
2631 checkValidDataCon dflags existential_ok tc con
2632 = setSrcSpan (getSrcSpan con) $
2633 addErrCtxt (dataConCtxt con) $
2634 do { -- Check that the return type of the data constructor
2635 -- matches the type constructor; eg reject this:
2636 -- data T a where { MkT :: Bogus a }
2637 -- It's important to do this first:
2638 -- see Note [Checking GADT return types]
2639 -- and c.f. Note [Check role annotations in a second pass]
2640 let tc_tvs = tyConTyVars tc
2641 res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
2642 orig_res_ty = dataConOrigResTy con
2643 ; traceTc "checkValidDataCon" (vcat
2644 [ ppr con, ppr tc, ppr tc_tvs
2645 , ppr res_ty_tmpl <+> dcolon <+> ppr (typeKind res_ty_tmpl)
2646 , ppr orig_res_ty <+> dcolon <+> ppr (typeKind orig_res_ty)])
2647
2648
2649 ; checkTc (isJust (tcMatchTy res_ty_tmpl
2650 orig_res_ty))
2651 (badDataConTyCon con res_ty_tmpl orig_res_ty)
2652 -- Note that checkTc aborts if it finds an error. This is
2653 -- critical to avoid panicking when we call dataConUserType
2654 -- on an un-rejiggable datacon!
2655
2656 ; traceTc "checkValidDataCon 2" (ppr (dataConUserType con))
2657
2658 -- Check that the result type is a *monotype*
2659 -- e.g. reject this: MkT :: T (forall a. a->a)
2660 -- Reason: it's really the argument of an equality constraint
2661 ; checkValidMonoType orig_res_ty
2662
2663 -- Check all argument types for validity
2664 ; checkValidType ctxt (dataConUserType con)
2665 ; mapM_ (checkForLevPoly empty)
2666 (dataConOrigArgTys con)
2667
2668 -- Extra checks for newtype data constructors
2669 ; when (isNewTyCon tc) (checkNewDataCon con)
2670
2671 -- Check that existentials are allowed if they are used
2672 ; checkTc (existential_ok || isVanillaDataCon con)
2673 (badExistential con)
2674
2675 -- Check that UNPACK pragmas and bangs work out
2676 -- E.g. reject data T = MkT {-# UNPACK #-} Int -- No "!"
2677 -- data T = MkT {-# UNPACK #-} !a -- Can't unpack
2678 ; zipWith3M_ check_bang (dataConSrcBangs con) (dataConImplBangs con) [1..]
2679
2680 ; traceTc "Done validity of data con" $
2681 vcat [ ppr con
2682 , text "Datacon user type:" <+> ppr (dataConUserType con)
2683 , text "Datacon rep type:" <+> ppr (dataConRepType con)
2684 , text "Rep typcon binders:" <+> ppr (tyConBinders (dataConTyCon con))
2685 , case tyConFamInst_maybe (dataConTyCon con) of
2686 Nothing -> text "not family"
2687 Just (f, _) -> ppr (tyConBinders f) ]
2688 }
2689 where
2690 ctxt = ConArgCtxt (dataConName con)
2691
2692 check_bang :: HsSrcBang -> HsImplBang -> Int -> TcM ()
2693 check_bang (HsSrcBang _ _ SrcLazy) _ n
2694 | not (xopt LangExt.StrictData dflags)
2695 = addErrTc
2696 (bad_bang n (text "Lazy annotation (~) without StrictData"))
2697 check_bang (HsSrcBang _ want_unpack strict_mark) rep_bang n
2698 | isSrcUnpacked want_unpack, not is_strict
2699 = addWarnTc NoReason (bad_bang n (text "UNPACK pragma lacks '!'"))
2700 | isSrcUnpacked want_unpack
2701 , case rep_bang of { HsUnpack {} -> False; _ -> True }
2702 -- If not optimising, we don't unpack (rep_bang is never
2703 -- HsUnpack), so don't complain! This happens, e.g., in Haddock.
2704 -- See dataConSrcToImplBang.
2705 , not (gopt Opt_OmitInterfacePragmas dflags)
2706 -- When typechecking an indefinite package in Backpack, we
2707 -- may attempt to UNPACK an abstract type. The test here will
2708 -- conclude that this is unusable, but it might become usable
2709 -- when we actually fill in the abstract type. As such, don't
2710 -- warn in this case (it gives users the wrong idea about whether
2711 -- or not UNPACK on abstract types is supported; it is!)
2712 , unitIdIsDefinite (thisPackage dflags)
2713 = addWarnTc NoReason (bad_bang n (text "Ignoring unusable UNPACK pragma"))
2714 where
2715 is_strict = case strict_mark of
2716 NoSrcStrict -> xopt LangExt.StrictData dflags
2717 bang -> isSrcStrict bang
2718
2719 check_bang _ _ _
2720 = return ()
2721
2722 bad_bang n herald
2723 = hang herald 2 (text "on the" <+> speakNth n
2724 <+> text "argument of" <+> quotes (ppr con))
2725 -------------------------------
2726 checkNewDataCon :: DataCon -> TcM ()
2727 -- Further checks for the data constructor of a newtype
2728 checkNewDataCon con
2729 = do { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
2730 -- One argument
2731
2732 ; checkTc (not (isUnliftedType arg_ty1)) $
2733 text "A newtype cannot have an unlifted argument type"
2734
2735 ; check_con (null eq_spec) $
2736 text "A newtype constructor must have a return type of form T a1 ... an"
2737 -- Return type is (T a b c)
2738
2739 ; check_con (null theta) $
2740 text "A newtype constructor cannot have a context in its type"
2741
2742 ; check_con (null ex_tvs) $
2743 text "A newtype constructor cannot have existential type variables"
2744 -- No existentials
2745
2746 ; checkTc (all ok_bang (dataConSrcBangs con))
2747 (newtypeStrictError con)
2748 -- No strictness annotations
2749 }
2750 where
2751 (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
2752 = dataConFullSig con
2753 check_con what msg
2754 = checkTc what (msg $$ ppr con <+> dcolon <+> ppr (dataConUserType con))
2755
2756 (arg_ty1 : _) = arg_tys
2757
2758 ok_bang (HsSrcBang _ _ SrcStrict) = False
2759 ok_bang (HsSrcBang _ _ SrcLazy) = False
2760 ok_bang _ = True
2761
2762 -------------------------------
2763 checkValidClass :: Class -> TcM ()
2764 checkValidClass cls
2765 = do { constrained_class_methods <- xoptM LangExt.ConstrainedClassMethods
2766 ; multi_param_type_classes <- xoptM LangExt.MultiParamTypeClasses
2767 ; nullary_type_classes <- xoptM LangExt.NullaryTypeClasses
2768 ; fundep_classes <- xoptM LangExt.FunctionalDependencies
2769 ; undecidable_super_classes <- xoptM LangExt.UndecidableSuperClasses
2770
2771 -- Check that the class is unary, unless multiparameter type classes
2772 -- are enabled; also recognize deprecated nullary type classes
2773 -- extension (subsumed by multiparameter type classes, Trac #8993)
2774 ; checkTc (multi_param_type_classes || cls_arity == 1 ||
2775 (nullary_type_classes && cls_arity == 0))
2776 (classArityErr cls_arity cls)
2777 ; checkTc (fundep_classes || null fundeps) (classFunDepsErr cls)
2778
2779 -- Check the super-classes
2780 ; checkValidTheta (ClassSCCtxt (className cls)) theta
2781
2782 -- Now check for cyclic superclasses
2783 -- If there are superclass cycles, checkClassCycleErrs bails.
2784 ; unless undecidable_super_classes $
2785 case checkClassCycles cls of
2786 Just err -> setSrcSpan (getSrcSpan cls) $
2787 addErrTc err
2788 Nothing -> return ()
2789
2790 -- Check the class operations.
2791 -- But only if there have been no earlier errors
2792 -- See Note [Abort when superclass cycle is detected]
2793 ; whenNoErrs $
2794 mapM_ (check_op constrained_class_methods) op_stuff
2795
2796 -- Check the associated type defaults are well-formed and instantiated
2797 ; mapM_ check_at at_stuff }
2798 where
2799 (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
2800 cls_arity = length (tyConVisibleTyVars (classTyCon cls))
2801 -- Ignore invisible variables
2802 cls_tv_set = mkVarSet tyvars
2803 mini_env = zipVarEnv tyvars (mkTyVarTys tyvars)
2804 mb_cls = Just (cls, tyvars, mini_env)
2805
2806 check_op constrained_class_methods (sel_id, dm)
2807 = setSrcSpan (getSrcSpan sel_id) $
2808 addErrCtxt (classOpCtxt sel_id op_ty) $ do
2809 { traceTc "class op type" (ppr op_ty)
2810 ; checkValidType ctxt op_ty
2811 -- This implements the ambiguity check, among other things
2812 -- Example: tc223
2813 -- class Error e => Game b mv e | b -> mv e where
2814 -- newBoard :: MonadState b m => m ()
2815 -- Here, MonadState has a fundep m->b, so newBoard is fine
2816
2817 -- a method cannot be levity polymorphic, as we have to store the
2818 -- method in a dictionary
2819 -- example of what this prevents:
2820 -- class BoundedX (a :: TYPE r) where minBound :: a
2821 -- See Note [Levity polymorphism checking] in DsMonad
2822 ; checkForLevPoly empty tau1
2823
2824 ; unless constrained_class_methods $
2825 mapM_ check_constraint (tail (cls_pred:op_theta))
2826
2827 ; check_dm ctxt sel_id cls_pred tau2 dm
2828 }
2829 where
2830 ctxt = FunSigCtxt op_name True -- Report redundant class constraints
2831 op_name = idName sel_id
2832 op_ty = idType sel_id
2833 (_,cls_pred,tau1) = tcSplitMethodTy op_ty
2834 -- See Note [Splitting nested sigma types in class type signatures]
2835 (_,op_theta,tau2) = tcSplitNestedSigmaTys tau1
2836
2837 check_constraint :: TcPredType -> TcM ()
2838 check_constraint pred -- See Note [Class method constraints]
2839 = when (not (isEmptyVarSet pred_tvs) &&
2840 pred_tvs `subVarSet` cls_tv_set)
2841 (addErrTc (badMethPred sel_id pred))
2842 where
2843 pred_tvs = tyCoVarsOfType pred
2844
2845 check_at (ATI fam_tc m_dflt_rhs)
2846 = do { checkTc (cls_arity == 0 || any (`elemVarSet` cls_tv_set) fam_tvs)
2847 (noClassTyVarErr cls fam_tc)
2848 -- Check that the associated type mentions at least
2849 -- one of the class type variables
2850 -- The check is disabled for nullary type classes,
2851 -- since there is no possible ambiguity (Trac #10020)
2852
2853 -- Check that any default declarations for associated types are valid
2854 ; whenIsJust m_dflt_rhs $ \ (rhs, loc) ->
2855 checkValidTyFamEqn mb_cls fam_tc
2856 fam_tvs [] (mkTyVarTys fam_tvs) rhs pp_lhs loc }
2857 where
2858 fam_tvs = tyConTyVars fam_tc
2859 pp_lhs = ppr (mkTyConApp fam_tc (mkTyVarTys fam_tvs))
2860
2861 check_dm :: UserTypeCtxt -> Id -> PredType -> Type -> DefMethInfo -> TcM ()
2862 -- Check validity of the /top-level/ generic-default type
2863 -- E.g for class C a where
2864 -- default op :: forall b. (a~b) => blah
2865 -- we do not want to do an ambiguity check on a type with
2866 -- a free TyVar 'a' (Trac #11608). See TcType
2867 -- Note [TyVars and TcTyVars during type checking] in TcType
2868 -- Hence the mkDefaultMethodType to close the type.
2869 check_dm ctxt sel_id vanilla_cls_pred vanilla_tau
2870 (Just (dm_name, dm_spec@(GenericDM dm_ty)))
2871 = setSrcSpan (getSrcSpan dm_name) $ do
2872 -- We have carefully set the SrcSpan on the generic
2873 -- default-method Name to be that of the generic
2874 -- default type signature
2875
2876 -- First, we check that that the method's default type signature
2877 -- aligns with the non-default type signature.
2878 -- See Note [Default method type signatures must align]
2879 let cls_pred = mkClassPred cls $ mkTyVarTys $ classTyVars cls
2880 -- Note that the second field of this tuple contains the context
2881 -- of the default type signature, making it apparent that we
2882 -- ignore method contexts completely when validity-checking
2883 -- default type signatures. See the end of
2884 -- Note [Default method type signatures must align]
2885 -- to learn why this is OK.
2886 --
2887 -- See also
2888 -- Note [Splitting nested sigma types in class type signatures]
2889 -- for an explanation of why we don't use tcSplitSigmaTy here.
2890 (_, _, dm_tau) = tcSplitNestedSigmaTys dm_ty
2891
2892 -- Given this class definition:
2893 --
2894 -- class C a b where
2895 -- op :: forall p q. (Ord a, D p q)
2896 -- => a -> b -> p -> (a, b)
2897 -- default op :: forall r s. E r
2898 -- => a -> b -> s -> (a, b)
2899 --
2900 -- We want to match up two types of the form:
2901 --
2902 -- Vanilla type sig: C aa bb => aa -> bb -> p -> (aa, bb)
2903 -- Default type sig: C a b => a -> b -> s -> (a, b)
2904 --
2905 -- Notice that the two type signatures can be quantified over
2906 -- different class type variables! Therefore, it's important that
2907 -- we include the class predicate parts to match up a with aa and
2908 -- b with bb.
2909 vanilla_phi_ty = mkPhiTy [vanilla_cls_pred] vanilla_tau
2910 dm_phi_ty = mkPhiTy [cls_pred] dm_tau
2911
2912 traceTc "check_dm" $ vcat
2913 [ text "vanilla_phi_ty" <+> ppr vanilla_phi_ty
2914 , text "dm_phi_ty" <+> ppr dm_phi_ty ]
2915
2916 -- Actually checking that the types align is done with a call to
2917 -- tcMatchTys. We need to get a match in both directions to rule
2918 -- out degenerate cases like these:
2919 --
2920 -- class Foo a where
2921 -- foo1 :: a -> b
2922 -- default foo1 :: a -> Int
2923 --
2924 -- foo2 :: a -> Int
2925 -- default foo2 :: a -> b
2926 unless (isJust $ tcMatchTys [dm_phi_ty, vanilla_phi_ty]
2927 [vanilla_phi_ty, dm_phi_ty]) $ addErrTc $
2928 hang (text "The default type signature for"
2929 <+> ppr sel_id <> colon)
2930 2 (ppr dm_ty)
2931 $$ (text "does not match its corresponding"
2932 <+> text "non-default type signature")
2933
2934 -- Now do an ambiguity check on the default type signature.
2935 checkValidType ctxt (mkDefaultMethodType cls sel_id dm_spec)
2936 check_dm _ _ _ _ _ = return ()
2937
2938 checkFamFlag :: Name -> TcM ()
2939 -- Check that we don't use families without -XTypeFamilies
2940 -- The parser won't even parse them, but I suppose a GHC API
2941 -- client might have a go!
2942 checkFamFlag tc_name
2943 = do { idx_tys <- xoptM LangExt.TypeFamilies
2944 ; checkTc idx_tys err_msg }
2945 where
2946 err_msg = hang (text "Illegal family declaration for" <+> quotes (ppr tc_name))
2947 2 (text "Enable TypeFamilies to allow indexed type families")
2948
2949 {- Note [Class method constraints]
2950 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2951 Haskell 2010 is supposed to reject
2952 class C a where
2953 op :: Eq a => a -> a
2954 where the method type constrains only the class variable(s). (The extension
2955 -XConstrainedClassMethods switches off this check.) But regardless
2956 we should not reject
2957 class C a where
2958 op :: (?x::Int) => a -> a
2959 as pointed out in Trac #11793. So the test here rejects the program if
2960 * -XConstrainedClassMethods is off
2961 * the tyvars of the constraint are non-empty
2962 * all the tyvars are class tyvars, none are locally quantified
2963
2964 Note [Abort when superclass cycle is detected]
2965 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2966 We must avoid doing the ambiguity check for the methods (in
2967 checkValidClass.check_op) when there are already errors accumulated.
2968 This is because one of the errors may be a superclass cycle, and
2969 superclass cycles cause canonicalization to loop. Here is a
2970 representative example:
2971
2972 class D a => C a where
2973 meth :: D a => ()
2974 class C a => D a
2975
2976 This fixes Trac #9415, #9739
2977
2978 Note [Default method type signatures must align]
2979 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2980 GHC enforces the invariant that a class method's default type signature
2981 must "align" with that of the method's non-default type signature, as per
2982 GHC Trac #12918. For instance, if you have:
2983
2984 class Foo a where
2985 bar :: forall b. Context => a -> b
2986
2987 Then a default type signature for bar must be alpha equivalent to
2988 (forall b. a -> b). That is, the types must be the same modulo differences in
2989 contexts. So the following would be acceptable default type signatures:
2990
2991 default bar :: forall b. Context1 => a -> b
2992 default bar :: forall x. Context2 => a -> x
2993
2994 But the following are NOT acceptable default type signatures:
2995
2996 default bar :: forall b. b -> a
2997 default bar :: forall x. x
2998 default bar :: a -> Int
2999
3000 Note that a is bound by the class declaration for Foo itself, so it is
3001 not allowed to differ in the default type signature.
3002
3003 The default type signature (default bar :: a -> Int) deserves special mention,
3004 since (a -> Int) is a straightforward instantiation of (forall b. a -> b). To
3005 write this, you need to declare the default type signature like so:
3006
3007 default bar :: forall b. (b ~ Int). a -> b
3008
3009 As noted in #12918, there are several reasons to do this:
3010
3011 1. It would make no sense to have a type that was flat-out incompatible with
3012 the non-default type signature. For instance, if you had:
3013
3014 class Foo a where
3015 bar :: a -> Int
3016 default bar :: a -> Bool
3017
3018 Then that would always fail in an instance declaration. So this check
3019 nips such cases in the bud before they have the chance to produce
3020 confusing error messages.
3021
3022 2. Internally, GHC uses TypeApplications to instantiate the default method in
3023 an instance. See Note [Default methods in instances] in TcInstDcls.
3024 Thus, GHC needs to know exactly what the universally quantified type
3025 variables are, and when instantiated that way, the default method's type
3026 must match the expected type.
3027
3028 3. Aesthetically, by only allowing the default type signature to differ in its
3029 context, we are making it more explicit the ways in which the default type
3030 signature is less polymorphic than the non-default type signature.
3031
3032 You might be wondering: why are the contexts allowed to be different, but not
3033 the rest of the type signature? That's because default implementations often
3034 rely on assumptions that the more general, non-default type signatures do not.
3035 For instance, in the Enum class declaration:
3036
3037 class Enum a where
3038 enum :: [a]
3039 default enum :: (Generic a, GEnum (Rep a)) => [a]
3040 enum = map to genum
3041
3042 class GEnum f where
3043 genum :: [f a]
3044
3045 The default implementation for enum only works for types that are instances of
3046 Generic, and for which their generic Rep type is an instance of GEnum. But
3047 clearly enum doesn't _have_ to use this implementation, so naturally, the
3048 context for enum is allowed to be different to accomodate this. As a result,
3049 when we validity-check default type signatures, we ignore contexts completely.
3050
3051 Note that when checking whether two type signatures match, we must take care to
3052 split as many foralls as it takes to retrieve the tau types we which to check.
3053 See Note [Splitting nested sigma types in class type signatures].
3054
3055 Note [Splitting nested sigma types in class type signatures]
3056 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3057 Consider this type synonym and class definition:
3058
3059 type Traversal s t a b = forall f. Applicative f => (a -> f b) -> s -> f t
3060
3061 class Each s t a b where
3062 each :: Traversal s t a b
3063 default each :: (Traversable g, s ~ g a, t ~ g b) => Traversal s t a b
3064
3065 It might seem obvious that the tau types in both type signatures for `each`
3066 are the same, but actually getting GHC to conclude this is surprisingly tricky.
3067 That is because in general, the form of a class method's non-default type
3068 signature is:
3069
3070 forall a. C a => forall d. D d => E a b
3071
3072 And the general form of a default type signature is:
3073
3074 forall f. F f => E a f -- The variable `a` comes from the class
3075
3076 So it you want to get the tau types in each type signature, you might find it
3077 reasonable to call tcSplitSigmaTy twice on the non-default type signature, and
3078 call it once on the default type signature. For most classes and methods, this
3079 will work, but Each is a bit of an exceptional case. The way `each` is written,
3080 it doesn't quantify any additional type variables besides those of the Each
3081 class itself, so the non-default type signature for `each` is actually this:
3082
3083 forall s t a b. Each s t a b => Traversal s t a b
3084
3085 Notice that there _appears_ to only be one forall. But there's actually another
3086 forall lurking in the Traversal type synonym, so if you call tcSplitSigmaTy
3087 twice, you'll also go under the forall in Traversal! That is, you'll end up
3088 with:
3089
3090 (a -> f b) -> s -> f t
3091
3092 A problem arises because you only call tcSplitSigmaTy once on the default type
3093 signature for `each`, which gives you
3094
3095 Traversal s t a b
3096
3097 Or, equivalently:
3098
3099 forall f. Applicative f => (a -> f b) -> s -> f t
3100
3101 This is _not_ the same thing as (a -> f b) -> s -> f t! So now tcMatchTy will
3102 say that the tau types for `each` are not equal.
3103
3104 A solution to this problem is to use tcSplitNestedSigmaTys instead of
3105 tcSplitSigmaTy. tcSplitNestedSigmaTys will always split any foralls that it
3106 sees until it can't go any further, so if you called it on the default type
3107 signature for `each`, it would return (a -> f b) -> s -> f t like we desired.
3108
3109 Note [Checking partial record field]
3110 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
3111 This check checks the partial record field selector, and warns (Trac #7169).
3112
3113 For example:
3114
3115 data T a = A { m1 :: a, m2 :: a } | B { m1 :: a }
3116
3117 The function 'm2' is partial record field, and will fail when it is applied to
3118 'B'. The warning identifies such partial fields. The check is performed at the
3119 declaration of T, not at the call-sites of m2.
3120
3121 The warning can be suppressed by prefixing the field-name with an underscore.
3122 For example:
3123
3124 data T a = A { m1 :: a, _m2 :: a } | B { m1 :: a }
3125
3126 Note [checkValidDependency]
3127 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
3128 Consider
3129
3130 data Proxy k (a :: k)
3131 data Proxy2 k a = P (Proxy k a)
3132
3133 (This is test dependent/should_fail/InferDependency.) While it seems GHC can
3134 figure out the dependency between the arguments to Proxy2, this case errors.
3135 The problem is that when we build the initial kind (getInitialKind) for
3136 a tycon, we need to decide whether an argument is dependent or not. At first,
3137 I thought we could just assume that *all* arguments are dependent, and then
3138 patch it up later. However, this causes problems in error messages (where
3139 tycon's have mysterious kinds "forall (a :: k) -> blah") and in unification
3140 (where we try to unify kappa ~ forall (a :: k) -> blah, failing because the
3141 RHS is not a tau-type). Perhaps a cleverer algorithm could sort this out
3142 (say, by storing the dependency flag in a mutable cell and by avoiding
3143 these fancy kinds in error messages depending on the extension in effect)
3144 but it doesn't seem worth it.
3145
3146 So: we choose the dependency for each argument variable once and for all
3147 in getInitialKind. This means that any dependency must be lexically manifest.
3148
3149 checkValidDependency checks to make sure that no lexically non-dependent
3150 argument actually appears in a kind. Note the example above, where the k
3151 in Proxy2 is a dependent argument, but this fact is not lexically
3152 manifest. checkValidDependency will reject. This function must be called
3153 *before* kind generalization, because kind generalization works with
3154 the result of mkTyConKind, which will think that Proxy2's kind is
3155 Type -> k -> Type, where k is unbound. (It won't use a forall for a
3156 "non-dependent" argument k.)
3157 -}
3158
3159 -- | See Note [checkValidDependency]
3160 checkValidDependency :: [TyConBinder] -- zonked
3161 -> TcKind -- zonked (result kind)
3162 -> TcM ()
3163 checkValidDependency binders res_kind
3164 = go (tyCoVarsOfType res_kind) (reverse binders)
3165 where
3166 go :: TyCoVarSet -- fvs from scope
3167 -> [TyConBinder] -- binders, in reverse order
3168 -> TcM ()
3169 go _ [] = return () -- all set
3170 go fvs (tcb : tcbs)
3171 | not (isNamedTyConBinder tcb) && tcb_var `elemVarSet` fvs
3172 = do { setSrcSpan (getSrcSpan tcb_var) $
3173 addErrTc (vcat [ text "Type constructor argument" <+> quotes (ppr tcb_var) <+>
3174 text "is used dependently."
3175 , text "Any dependent arguments must be obviously so, not inferred"
3176 , text "by the type-checker."
3177 , hang (text "Inferred argument kinds:")
3178 2 (vcat (map pp_binder binders))
3179 , text "Suggestion: use" <+> quotes (ppr tcb_var) <+>
3180 text "in a kind to make the dependency clearer." ])
3181 ; go new_fvs tcbs }
3182
3183 | otherwise
3184 = go new_fvs tcbs
3185 where
3186 new_fvs = fvs `delVarSet` tcb_var
3187 `unionVarSet` tyCoVarsOfType tcb_kind
3188
3189 tcb_var = binderVar tcb
3190 tcb_kind = tyVarKind tcb_var
3191
3192 pp_binder binder = ppr (binderVar binder) <+> dcolon <+> ppr (binderKind binder)
3193
3194 {-
3195 ************************************************************************
3196 * *
3197 Checking role validity
3198 * *
3199 ************************************************************************
3200 -}
3201
3202 checkValidRoleAnnots :: RoleAnnotEnv -> TyCon -> TcM ()
3203 checkValidRoleAnnots role_annots tc
3204 | isTypeSynonymTyCon tc = check_no_roles
3205 | isFamilyTyCon tc = check_no_roles
3206 | isAlgTyCon tc = check_roles
3207 | otherwise = return ()
3208 where
3209 -- Role annotations are given only on *explicit* variables,
3210 -- but a tycon stores roles for all variables.
3211 -- So, we drop the implicit roles (which are all Nominal, anyway).
3212 name = tyConName tc
3213 tyvars = tyConTyVars tc
3214 roles = tyConRoles tc
3215 (vis_roles, vis_vars) = unzip $ snd $
3216 partitionInvisibles tc (mkTyVarTy . snd) $
3217 zip roles tyvars
3218 role_annot_decl_maybe = lookupRoleAnnot role_annots name
3219
3220 check_roles
3221 = whenIsJust role_annot_decl_maybe $
3222 \decl@(L loc (RoleAnnotDecl _ _ the_role_annots)) ->
3223 addRoleAnnotCtxt name $
3224 setSrcSpan loc $ do
3225 { role_annots_ok <- xoptM LangExt.RoleAnnotations
3226 ; checkTc role_annots_ok $ needXRoleAnnotations tc
3227 ; checkTc (vis_vars `equalLength` the_role_annots)
3228 (wrongNumberOfRoles vis_vars decl)
3229 ; _ <- zipWith3M checkRoleAnnot vis_vars the_role_annots vis_roles
3230 -- Representational or phantom roles for class parameters
3231 -- quickly lead to incoherence. So, we require
3232 -- IncoherentInstances to have them. See #8773, #14292
3233 ; incoherent_roles_ok <- xoptM LangExt.IncoherentInstances
3234 ; checkTc ( incoherent_roles_ok
3235 || (not $ isClassTyCon tc)
3236 || (all (== Nominal) vis_roles))
3237 incoherentRoles
3238
3239 ; lint <- goptM Opt_DoCoreLinting
3240 ; when lint $ checkValidRoles tc }
3241
3242 check_no_roles
3243 = whenIsJust role_annot_decl_maybe illegalRoleAnnotDecl
3244
3245 checkRoleAnnot :: TyVar -> Located (Maybe Role) -> Role -> TcM ()
3246 checkRoleAnnot _ (L _ Nothing) _ = return ()
3247 checkRoleAnnot tv (L _ (Just r1)) r2
3248 = when (r1 /= r2) $
3249 addErrTc $ badRoleAnnot (tyVarName tv) r1 r2
3250
3251 -- This is a double-check on the role inference algorithm. It is only run when
3252 -- -dcore-lint is enabled. See Note [Role inference] in TcTyDecls
3253 checkValidRoles :: TyCon -> TcM ()
3254 -- If you edit this function, you may need to update the GHC formalism
3255 -- See Note [GHC Formalism] in CoreLint
3256 checkValidRoles tc
3257 | isAlgTyCon tc
3258 -- tyConDataCons returns an empty list for data families
3259 = mapM_ check_dc_roles (tyConDataCons tc)
3260 | Just rhs <- synTyConRhs_maybe tc
3261 = check_ty_roles (zipVarEnv (tyConTyVars tc) (tyConRoles tc)) Representational rhs
3262 | otherwise
3263 = return ()
3264 where
3265 check_dc_roles datacon
3266 = do { traceTc "check_dc_roles" (ppr datacon <+> ppr (tyConRoles tc))
3267 ; mapM_ (check_ty_roles role_env Representational) $
3268 eqSpecPreds eq_spec ++ theta ++ arg_tys }
3269 -- See Note [Role-checking data constructor arguments] in TcTyDecls
3270 where
3271 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty)
3272 = dataConFullSig datacon
3273 univ_roles = zipVarEnv univ_tvs (tyConRoles tc)
3274 -- zipVarEnv uses zipEqual, but we don't want that for ex_tvs
3275 ex_roles = mkVarEnv (map (, Nominal) ex_tvs)
3276 role_env = univ_roles `plusVarEnv` ex_roles
3277
3278 check_ty_roles env role ty
3279 | Just ty' <- coreView ty -- #14101
3280 = check_ty_roles env role ty'
3281
3282 check_ty_roles env role (TyVarTy tv)
3283 = case lookupVarEnv env tv of
3284 Just role' -> unless (role' `ltRole` role || role' == role) $
3285 report_error $ text "type variable" <+> quotes (ppr tv) <+>
3286 text "cannot have role" <+> ppr role <+>
3287 text "because it was assigned role" <+> ppr role'
3288 Nothing -> report_error $ text "type variable" <+> quotes (ppr tv) <+>
3289 text "missing in environment"
3290
3291 check_ty_roles env Representational (TyConApp tc tys)
3292 = let roles' = tyConRoles tc in
3293 zipWithM_ (maybe_check_ty_roles env) roles' tys
3294
3295 check_ty_roles env Nominal (TyConApp _ tys)
3296 = mapM_ (check_ty_roles env Nominal) tys
3297
3298 check_ty_roles _ Phantom ty@(TyConApp {})
3299 = pprPanic "check_ty_roles" (ppr ty)
3300
3301 check_ty_roles env role (AppTy ty1 ty2)
3302 = check_ty_roles env role ty1
3303 >> check_ty_roles env Nominal ty2
3304
3305 check_ty_roles env role (FunTy ty1 ty2)
3306 = check_ty_roles env role ty1
3307 >> check_ty_roles env role ty2
3308
3309 check_ty_roles env role (ForAllTy (TvBndr tv _) ty)
3310 = check_ty_roles env Nominal (tyVarKind tv)
3311 >> check_ty_roles (extendVarEnv env tv Nominal) role ty
3312
3313 check_ty_roles _ _ (LitTy {}) = return ()
3314
3315 check_ty_roles env role (CastTy t _)
3316 = check_ty_roles env role t
3317
3318 check_ty_roles _ role (CoercionTy co)
3319 = unless (role == Phantom) $
3320 report_error $ text "coercion" <+> ppr co <+> text "has bad role" <+> ppr role
3321
3322 maybe_check_ty_roles env role ty
3323 = when (role == Nominal || role == Representational) $
3324 check_ty_roles env role ty
3325
3326 report_error doc
3327 = addErrTc $ vcat [text "Internal error in role inference:",
3328 doc,
3329 text "Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug"]
3330
3331 {-
3332 ************************************************************************
3333 * *
3334 Error messages
3335 * *
3336 ************************************************************************
3337 -}
3338
3339 tcAddTyFamInstCtxt :: TyFamInstDecl GhcRn -> TcM a -> TcM a
3340 tcAddTyFamInstCtxt decl
3341 = tcAddFamInstCtxt (text "type instance") (tyFamInstDeclName decl)
3342
3343 tcMkDataFamInstCtxt :: DataFamInstDecl GhcRn -> SDoc
3344 tcMkDataFamInstCtxt decl@(DataFamInstDecl { dfid_eqn =
3345 HsIB { hsib_body = eqn }})
3346 = tcMkFamInstCtxt (pprDataFamInstFlavour decl <+> text "instance")
3347 (unLoc (feqn_tycon eqn))
3348 tcMkDataFamInstCtxt (DataFamInstDecl (XHsImplicitBndrs _))
3349 = panic "tcMkDataFamInstCtxt"
3350
3351 tcAddDataFamInstCtxt :: DataFamInstDecl GhcRn -> TcM a -> TcM a
3352 tcAddDataFamInstCtxt decl
3353 = addErrCtxt (tcMkDataFamInstCtxt decl)
3354
3355 tcMkFamInstCtxt :: SDoc -> Name -> SDoc
3356 tcMkFamInstCtxt flavour tycon
3357 = hsep [ text "In the" <+> flavour <+> text "declaration for"
3358 , quotes (ppr tycon) ]
3359
3360 tcAddFamInstCtxt :: SDoc -> Name -> TcM a -> TcM a
3361 tcAddFamInstCtxt flavour tycon thing_inside
3362 = addErrCtxt (tcMkFamInstCtxt flavour tycon) thing_inside
3363
3364 tcAddClosedTypeFamilyDeclCtxt :: TyCon -> TcM a -> TcM a
3365 tcAddClosedTypeFamilyDeclCtxt tc
3366 = addErrCtxt ctxt
3367 where
3368 ctxt = text "In the equations for closed type family" <+>
3369 quotes (ppr tc)
3370
3371 resultTypeMisMatch :: FieldLabelString -> DataCon -> DataCon -> SDoc
3372 resultTypeMisMatch field_name con1 con2
3373 = vcat [sep [text "Constructors" <+> ppr con1 <+> text "and" <+> ppr con2,
3374 text "have a common field" <+> quotes (ppr field_name) <> comma],
3375 nest 2 $ text "but have different result types"]
3376
3377 fieldTypeMisMatch :: FieldLabelString -> DataCon -> DataCon -> SDoc
3378 fieldTypeMisMatch field_name con1 con2
3379 = sep [text "Constructors" <+> ppr con1 <+> text "and" <+> ppr con2,
3380 text "give different types for field", quotes (ppr field_name)]
3381
3382 dataConCtxtName :: [Located Name] -> SDoc
3383 dataConCtxtName [con]
3384 = text "In the definition of data constructor" <+> quotes (ppr con)
3385 dataConCtxtName con
3386 = text "In the definition of data constructors" <+> interpp'SP con
3387
3388 dataConCtxt :: Outputable a => a -> SDoc
3389 dataConCtxt con = text "In the definition of data constructor" <+> quotes (ppr con)
3390
3391 classOpCtxt :: Var -> Type -> SDoc
3392 classOpCtxt sel_id tau = sep [text "When checking the class method:",
3393 nest 2 (pprPrefixOcc sel_id <+> dcolon <+> ppr tau)]
3394
3395 classArityErr :: Int -> Class -> SDoc
3396 classArityErr n cls
3397 | n == 0 = mkErr "No" "no-parameter"
3398 | otherwise = mkErr "Too many" "multi-parameter"
3399 where
3400 mkErr howMany allowWhat =
3401 vcat [text (howMany ++ " parameters for class") <+> quotes (ppr cls),
3402 parens (text ("Enable MultiParamTypeClasses to allow "
3403 ++ allowWhat ++ " classes"))]
3404
3405 classFunDepsErr :: Class -> SDoc
3406 classFunDepsErr cls
3407 = vcat [text "Fundeps in class" <+> quotes (ppr cls),
3408 parens (text "Enable FunctionalDependencies to allow fundeps")]
3409
3410 badMethPred :: Id -> TcPredType -> SDoc
3411 badMethPred sel_id pred
3412 = vcat [ hang (text "Constraint" <+> quotes (ppr pred)
3413 <+> text "in the type of" <+> quotes (ppr sel_id))
3414 2 (text "constrains only the class type variables")
3415 , text "Enable ConstrainedClassMethods to allow it" ]
3416
3417 noClassTyVarErr :: Class -> TyCon -> SDoc
3418 noClassTyVarErr clas fam_tc
3419 = sep [ text "The associated type" <+> quotes (ppr fam_tc)
3420 , text "mentions none of the type or kind variables of the class" <+>
3421 quotes (ppr clas <+> hsep (map ppr (classTyVars clas)))]
3422
3423 badDataConTyCon :: DataCon -> Type -> Type -> SDoc
3424 badDataConTyCon data_con res_ty_tmpl actual_res_ty
3425 | tcIsForAllTy actual_res_ty
3426 = nested_foralls_contexts_suggestion
3427 | isJust (tcSplitPredFunTy_maybe actual_res_ty)
3428 = nested_foralls_contexts_suggestion
3429 | otherwise
3430 = hang (text "Data constructor" <+> quotes (ppr data_con) <+>
3431 text "returns type" <+> quotes (ppr actual_res_ty))
3432 2 (text "instead of an instance of its parent type" <+> quotes (ppr res_ty_tmpl))
3433 where
3434 -- This suggestion is useful for suggesting how to correct code like what
3435 -- was reported in Trac #12087:
3436 --
3437 -- data F a where
3438 -- MkF :: Ord a => Eq a => a -> F a
3439 --
3440 -- Although nested foralls or contexts are allowed in function type
3441 -- signatures, it is much more difficult to engineer GADT constructor type
3442 -- signatures to allow something similar, so we error in the latter case.
3443 -- Nevertheless, we can at least suggest how a user might reshuffle their
3444 -- exotic GADT constructor type signature so that GHC will accept.
3445 nested_foralls_contexts_suggestion =
3446 text "GADT constructor type signature cannot contain nested"
3447 <+> quotes forAllLit <> text "s or contexts"
3448 $+$ hang (text "Suggestion: instead use this type signature:")
3449 2 (ppr (dataConName data_con) <+> dcolon <+> ppr suggested_ty)
3450
3451 -- To construct a type that GHC would accept (suggested_ty), we:
3452 --
3453 -- 1) Find the existentially quantified type variables and the class
3454 -- predicates from the datacon. (NB: We don't need the universally
3455 -- quantified type variables, since rejigConRes won't substitute them in
3456 -- the result type if it fails, as in this scenario.)
3457 -- 2) Split apart the return type (which is headed by a forall or a
3458 -- context) using tcSplitNestedSigmaTys, collecting the type variables
3459 -- and class predicates we find, as well as the rho type lurking
3460 -- underneath the nested foralls and contexts.
3461 -- 3) Smash together the type variables and class predicates from 1) and
3462 -- 2), and prepend them to the rho type from 2).
3463 actual_ex_tvs = dataConExTyVars data_con
3464 actual_theta = dataConTheta data_con
3465 (actual_res_tvs, actual_res_theta, actual_res_rho)
3466 = tcSplitNestedSigmaTys actual_res_ty
3467 suggested_ty = mkSpecForAllTys (actual_ex_tvs ++ actual_res_tvs) $
3468 mkFunTys (actual_theta ++ actual_res_theta)
3469 actual_res_rho
3470
3471 badGadtDecl :: Name -> SDoc
3472 badGadtDecl tc_name
3473 = vcat [ text "Illegal generalised algebraic data declaration for" <+> quotes (ppr tc_name)
3474 , nest 2 (parens $ text "Enable the GADTs extension to allow this") ]
3475
3476 badExistential :: DataCon -> SDoc
3477 badExistential con
3478 = hang (text "Data constructor" <+> quotes (ppr con) <+>
3479 text "has existential type variables, a context, or a specialised result type")
3480 2 (vcat [ ppr con <+> dcolon <+> ppr (dataConUserType con)
3481 , parens $ text "Enable ExistentialQuantification or GADTs to allow this" ])
3482
3483 badStupidTheta :: Name -> SDoc
3484 badStupidTheta tc_name
3485 = text "A data type declared in GADT style cannot have a context:" <+> quotes (ppr tc_name)
3486
3487 newtypeConError :: Name -> Int -> SDoc
3488 newtypeConError tycon n
3489 = sep [text "A newtype must have exactly one constructor,",
3490 nest 2 $ text "but" <+> quotes (ppr tycon) <+> text "has" <+> speakN n ]
3491
3492 newtypeStrictError :: DataCon -> SDoc
3493 newtypeStrictError con
3494 = sep [text "A newtype constructor cannot have a strictness annotation,",
3495 nest 2 $ text "but" <+> quotes (ppr con) <+> text "does"]
3496
3497 newtypeFieldErr :: DataCon -> Int -> SDoc
3498 newtypeFieldErr con_name n_flds
3499 = sep [text "The constructor of a newtype must have exactly one field",
3500 nest 2 $ text "but" <+> quotes (ppr con_name) <+> text "has" <+> speakN n_flds]
3501
3502 badSigTyDecl :: Name -> SDoc
3503 badSigTyDecl tc_name
3504 = vcat [ text "Illegal kind signature" <+>
3505 quotes (ppr tc_name)
3506 , nest 2 (parens $ text "Use KindSignatures to allow kind signatures") ]
3507
3508 emptyConDeclsErr :: Name -> SDoc
3509 emptyConDeclsErr tycon
3510 = sep [quotes (ppr tycon) <+> text "has no constructors",
3511 nest 2 $ text "(EmptyDataDecls permits this)"]
3512
3513 wrongKindOfFamily :: TyCon -> SDoc
3514 wrongKindOfFamily family
3515 = text "Wrong category of family instance; declaration was for a"
3516 <+> kindOfFamily
3517 where
3518 kindOfFamily | isTypeFamilyTyCon family = text "type family"
3519 | isDataFamilyTyCon family = text "data family"
3520 | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
3521
3522 wrongNumberOfParmsErr :: Arity -> SDoc
3523 wrongNumberOfParmsErr max_args
3524 = text "Number of parameters must match family declaration; expected"
3525 <+> ppr max_args
3526
3527 defaultAssocKindErr :: TyCon -> SDoc
3528 defaultAssocKindErr fam_tc
3529 = text "Kind mis-match on LHS of default declaration for"
3530 <+> quotes (ppr fam_tc)
3531
3532 wrongTyFamName :: Name -> Name -> SDoc
3533 wrongTyFamName fam_tc_name eqn_tc_name
3534 = hang (text "Mismatched type name in type family instance.")
3535 2 (vcat [ text "Expected:" <+> ppr fam_tc_name
3536 , text " Actual:" <+> ppr eqn_tc_name ])
3537
3538 badRoleAnnot :: Name -> Role -> Role -> SDoc
3539 badRoleAnnot var annot inferred
3540 = hang (text "Role mismatch on variable" <+> ppr var <> colon)
3541 2 (sep [ text "Annotation says", ppr annot
3542 , text "but role", ppr inferred
3543 , text "is required" ])
3544
3545 wrongNumberOfRoles :: [a] -> LRoleAnnotDecl GhcRn -> SDoc
3546 wrongNumberOfRoles tyvars d@(L _ (RoleAnnotDecl _ _ annots))
3547 = hang (text "Wrong number of roles listed in role annotation;" $$
3548 text "Expected" <+> (ppr $ length tyvars) <> comma <+>
3549 text "got" <+> (ppr $ length annots) <> colon)
3550 2 (ppr d)
3551 wrongNumberOfRoles _ (L _ (XRoleAnnotDecl _)) = panic "wrongNumberOfRoles"
3552
3553 illegalRoleAnnotDecl :: LRoleAnnotDecl GhcRn -> TcM ()
3554 illegalRoleAnnotDecl (L loc (RoleAnnotDecl _ tycon _))
3555 = setErrCtxt [] $
3556 setSrcSpan loc $
3557 addErrTc (text "Illegal role annotation for" <+> ppr tycon <> char ';' $$
3558 text "they are allowed only for datatypes and classes.")
3559 illegalRoleAnnotDecl (L _ (XRoleAnnotDecl _)) = panic "illegalRoleAnnotDecl"
3560
3561 needXRoleAnnotations :: TyCon -> SDoc
3562 needXRoleAnnotations tc
3563 = text "Illegal role annotation for" <+> ppr tc <> char ';' $$
3564 text "did you intend to use RoleAnnotations?"
3565
3566 incoherentRoles :: SDoc
3567 incoherentRoles = (text "Roles other than" <+> quotes (text "nominal") <+>
3568 text "for class parameters can lead to incoherence.") $$
3569 (text "Use IncoherentInstances to allow this; bad role found")
3570
3571 addTyConCtxt :: TyCon -> TcM a -> TcM a
3572 addTyConCtxt tc
3573 = addErrCtxt ctxt
3574 where
3575 name = getName tc
3576 flav = ppr (tyConFlavour tc)
3577 ctxt = hsep [ text "In the", flav
3578 , text "declaration for", quotes (ppr name) ]
3579
3580 addRoleAnnotCtxt :: Name -> TcM a -> TcM a
3581 addRoleAnnotCtxt name
3582 = addErrCtxt $
3583 text "while checking a role annotation for" <+> quotes (ppr name)