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