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