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