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