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