Major patch to add -fwarn-redundant-constraints
[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 #-}
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, tcAddDataFamInstCtxt,
19 wrongKindOfFamily, dataConCtxt, badDataConTyCon
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 TcSimplify( growThetaTyVars )
32 import TcBinds( tcRecSelBinds )
33 import TcTyDecls
34 import TcClassDcl
35 import TcHsType
36 import TcMType
37 import TcType
38 import TysWiredIn( unitTy )
39 import FamInst
40 import FamInstEnv( isDominatedBy, mkCoAxBranch, mkBranchedCoAxiom )
41 import Coercion( pprCoAxBranch, ltRole )
42 import Type
43 import TypeRep -- for checkValidRoles
44 import Kind
45 import Class
46 import CoAxiom
47 import TyCon
48 import DataCon
49 import Id
50 import MkCore ( rEC_SEL_ERROR_ID )
51 import IdInfo
52 import Var
53 import VarEnv
54 import VarSet
55 import Module
56 import Name
57 import NameSet
58 import NameEnv
59 import Outputable
60 import Maybes
61 import Unify
62 import Util
63 import SrcLoc
64 import ListSetOps
65 import Digraph
66 import DynFlags
67 import FastString
68 import Unique ( mkBuiltinUnique )
69 import BasicTypes
70
71 import Bag
72 import Control.Monad
73 import Data.List
74
75 {-
76 ************************************************************************
77 * *
78 \subsection{Type checking for type and class declarations}
79 * *
80 ************************************************************************
81
82 Note [Grouping of type and class declarations]
83 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
84 tcTyAndClassDecls is called on a list of `TyClGroup`s. Each group is a strongly
85 connected component of mutually dependent types and classes. We kind check and
86 type check each group separately to enhance kind polymorphism. Take the
87 following example:
88
89 type Id a = a
90 data X = X (Id Int)
91
92 If we were to kind check the two declarations together, we would give Id the
93 kind * -> *, since we apply it to an Int in the definition of X. But we can do
94 better than that, since Id really is kind polymorphic, and should get kind
95 forall (k::BOX). k -> k. Since it does not depend on anything else, it can be
96 kind-checked by itself, hence getting the most general kind. We then kind check
97 X, which works fine because we then know the polymorphic kind of Id, and simply
98 instantiate k to *.
99
100 Note [Check role annotations in a second pass]
101 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
102 Role inference potentially depends on the types of all of the datacons declared
103 in a mutually recursive group. The validity of a role annotation, in turn,
104 depends on the result of role inference. Because the types of datacons might
105 be ill-formed (see #7175 and Note [Checking GADT return types]) we must check
106 *all* the tycons in a group for validity before checking *any* of the roles.
107 Thus, we take two passes over the resulting tycons, first checking for general
108 validity and then checking for valid role annotations.
109 -}
110
111 tcTyAndClassDecls :: ModDetails
112 -> [TyClGroup Name] -- Mutually-recursive groups in dependency order
113 -> TcM TcGblEnv -- Input env extended by types and classes
114 -- and their implicit Ids,DataCons
115 -- Fails if there are any errors
116 tcTyAndClassDecls boot_details tyclds_s
117 = checkNoErrs $ -- The code recovers internally, but if anything gave rise to
118 -- an error we'd better stop now, to avoid a cascade
119 fold_env tyclds_s -- Type check each group in dependency order folding the global env
120 where
121 fold_env :: [TyClGroup Name] -> TcM TcGblEnv
122 fold_env [] = getGblEnv
123 fold_env (tyclds:tyclds_s)
124 = do { tcg_env <- tcTyClGroup boot_details tyclds
125 ; setGblEnv tcg_env $ fold_env tyclds_s }
126 -- remaining groups are typecheck in the extended global env
127
128 tcTyClGroup :: ModDetails -> TyClGroup Name -> TcM TcGblEnv
129 -- Typecheck one strongly-connected component of type and class decls
130 tcTyClGroup boot_details tyclds
131 = do { -- Step 1: kind-check this group and returns the final
132 -- (possibly-polymorphic) kind of each TyCon and Class
133 -- See Note [Kind checking for type and class decls]
134 names_w_poly_kinds <- kcTyClGroup tyclds
135 ; traceTc "tcTyAndCl generalized kinds" (ppr names_w_poly_kinds)
136
137 -- Step 2: type-check all groups together, returning
138 -- the final TyCons and Classes
139 ; let role_annots = extractRoleAnnots tyclds
140 decls = group_tyclds tyclds
141 ; tyclss <- fixM $ \ rec_tyclss -> do
142 { is_boot <- tcIsHsBootOrSig
143 ; let rec_flags = calcRecFlags boot_details is_boot
144 role_annots rec_tyclss
145
146 -- Populate environment with knot-tied ATyCon for TyCons
147 -- NB: if the decls mention any ill-staged data cons
148 -- (see Note [Recusion and promoting data constructors]
149 -- we will have failed already in kcTyClGroup, so no worries here
150 ; tcExtendRecEnv (zipRecTyClss names_w_poly_kinds rec_tyclss) $
151
152 -- Also extend the local type envt with bindings giving
153 -- the (polymorphic) kind of each knot-tied TyCon or Class
154 -- See Note [Type checking recursive type and class declarations]
155 tcExtendKindEnv names_w_poly_kinds $
156
157 -- Kind and type check declarations for this group
158 concatMapM (tcTyClDecl rec_flags) decls }
159
160 -- Step 3: Perform the validity check
161 -- We can do this now because we are done with the recursive knot
162 -- Do it before Step 4 (adding implicit things) because the latter
163 -- expects well-formed TyCons
164 ; tcExtendGlobalEnv tyclss $ do
165 { traceTc "Starting validity check" (ppr tyclss)
166 ; checkNoErrs $
167 mapM_ (recoverM (return ()) . checkValidTyCl) tyclss
168 -- We recover, which allows us to report multiple validity errors
169 -- the checkNoErrs is necessary to fix #7175.
170 ; mapM_ (recoverM (return ()) . checkValidRoleAnnots role_annots) tyclss
171 -- See Note [Check role annotations in a second pass]
172
173 -- Step 4: Add the implicit things;
174 -- we want them in the environment because
175 -- they may be mentioned in interface files
176 ; tcExtendGlobalValEnv (mkDefaultMethodIds tyclss) $
177 tcAddImplicits tyclss } }
178
179 tcAddImplicits :: [TyThing] -> TcM TcGblEnv
180 tcAddImplicits tyclss
181 = tcExtendGlobalEnvImplicit implicit_things $
182 tcRecSelBinds rec_sel_binds
183 where
184 implicit_things = concatMap implicitTyThings tyclss
185 rec_sel_binds = mkRecSelBinds tyclss
186
187 zipRecTyClss :: [(Name, Kind)]
188 -> [TyThing] -- Knot-tied
189 -> [(Name,TyThing)]
190 -- Build a name-TyThing mapping for the things bound by decls
191 -- being careful not to look at the [TyThing]
192 -- The TyThings in the result list must have a visible ATyCon,
193 -- because typechecking types (in, say, tcTyClDecl) looks at this outer constructor
194 zipRecTyClss kind_pairs rec_things
195 = [ (name, ATyCon (get name)) | (name, _kind) <- kind_pairs ]
196 where
197 rec_type_env :: TypeEnv
198 rec_type_env = mkTypeEnv rec_things
199
200 get name = case lookupTypeEnv rec_type_env name of
201 Just (ATyCon tc) -> tc
202 other -> pprPanic "zipRecTyClss" (ppr name <+> ppr other)
203
204 {-
205 ************************************************************************
206 * *
207 Kind checking
208 * *
209 ************************************************************************
210
211 Note [Kind checking for type and class decls]
212 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
213 Kind checking is done thus:
214
215 1. Make up a kind variable for each parameter of the *data* type, class,
216 and closed type family decls, and extend the kind environment (which is
217 in the TcLclEnv)
218
219 2. Dependency-analyse the type *synonyms* (which must be non-recursive),
220 and kind-check them in dependency order. Extend the kind envt.
221
222 3. Kind check the data type and class decls
223
224 Synonyms are treated differently to data type and classes,
225 because a type synonym can be an unboxed type
226 type Foo = Int#
227 and a kind variable can't unify with UnboxedTypeKind
228 So we infer their kinds in dependency order
229
230 We need to kind check all types in the mutually recursive group
231 before we know the kind of the type variables. For example:
232
233 class C a where
234 op :: D b => a -> b -> b
235
236 class D c where
237 bop :: (Monad c) => ...
238
239 Here, the kind of the locally-polymorphic type variable "b"
240 depends on *all the uses of class D*. For example, the use of
241 Monad c in bop's type signature means that D must have kind Type->Type.
242
243 However type synonyms work differently. They can have kinds which don't
244 just involve (->) and *:
245 type R = Int# -- Kind #
246 type S a = Array# a -- Kind * -> #
247 type T a b = (# a,b #) -- Kind * -> * -> (# a,b #)
248 So we must infer their kinds from their right-hand sides *first* and then
249 use them, whereas for the mutually recursive data types D we bring into
250 scope kind bindings D -> k, where k is a kind variable, and do inference.
251
252 Open type families
253 ~~~~~~~~~~~~~~~~~~
254 This treatment of type synonyms only applies to Haskell 98-style synonyms.
255 General type functions can be recursive, and hence, appear in `alg_decls'.
256
257 The kind of an open type family is solely determinded by its kind signature;
258 hence, only kind signatures participate in the construction of the initial
259 kind environment (as constructed by `getInitialKind'). In fact, we ignore
260 instances of families altogether in the following. However, we need to include
261 the kinds of *associated* families into the construction of the initial kind
262 environment. (This is handled by `allDecls').
263 -}
264
265 kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind)]
266 -- Kind check this group, kind generalize, and return the resulting local env
267 -- This bindds the TyCons and Classes of the group, but not the DataCons
268 -- See Note [Kind checking for type and class decls]
269 kcTyClGroup (TyClGroup { group_tyclds = decls })
270 = do { mod <- getModule
271 ; traceTc "kcTyClGroup" (ptext (sLit "module") <+> ppr mod $$ vcat (map ppr decls))
272
273 -- Kind checking;
274 -- 1. Bind kind variables for non-synonyms
275 -- 2. Kind-check synonyms, and bind kinds of those synonyms
276 -- 3. Kind-check non-synonyms
277 -- 4. Generalise the inferred kinds
278 -- See Note [Kind checking for type and class decls]
279
280 -- Step 1: Bind kind variables for non-synonyms
281 ; let (syn_decls, non_syn_decls) = partition (isSynDecl . unLoc) decls
282 ; initial_kinds <- getInitialKinds non_syn_decls
283 ; traceTc "kcTyClGroup: initial kinds" (ppr initial_kinds)
284
285 -- Step 2: Set initial envt, kind-check the synonyms
286 ; lcl_env <- tcExtendKindEnv2 initial_kinds $
287 kcSynDecls (calcSynCycles syn_decls)
288
289 -- Step 3: Set extended envt, kind-check the non-synonyms
290 ; setLclEnv lcl_env $
291 mapM_ kcLTyClDecl non_syn_decls
292
293 -- Step 4: generalisation
294 -- Kind checking done for this group
295 -- Now we have to kind generalize the flexis
296 ; res <- concatMapM (generaliseTCD (tcl_env lcl_env)) decls
297
298 ; traceTc "kcTyClGroup result" (ppr res)
299 ; return res }
300
301 where
302 generalise :: TcTypeEnv -> Name -> TcM (Name, Kind)
303 -- For polymorphic things this is a no-op
304 generalise kind_env name
305 = do { let kc_kind = case lookupNameEnv kind_env name of
306 Just (AThing k) -> k
307 _ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
308 ; kvs <- kindGeneralize (tyVarsOfType kc_kind)
309 ; kc_kind' <- zonkTcKind kc_kind -- Make sure kc_kind' has the final,
310 -- skolemised kind variables
311 ; traceTc "Generalise kind" (vcat [ ppr name, ppr kc_kind, ppr kvs, ppr kc_kind' ])
312 ; return (name, mkForAllTys kvs kc_kind') }
313
314 generaliseTCD :: TcTypeEnv -> LTyClDecl Name -> TcM [(Name, Kind)]
315 generaliseTCD kind_env (L _ decl)
316 | ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
317 = do { first <- generalise kind_env name
318 ; rest <- mapM ((generaliseFamDecl kind_env) . unLoc) ats
319 ; return (first : rest) }
320
321 | FamDecl { tcdFam = fam } <- decl
322 = do { res <- generaliseFamDecl kind_env fam
323 ; return [res] }
324
325 | otherwise
326 = do { res <- generalise kind_env (tcdName decl)
327 ; return [res] }
328
329 generaliseFamDecl :: TcTypeEnv -> FamilyDecl Name -> TcM (Name, Kind)
330 generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
331 = generalise kind_env name
332
333 mk_thing_env :: [LTyClDecl Name] -> [(Name, TcTyThing)]
334 mk_thing_env [] = []
335 mk_thing_env (decl : decls)
336 | L _ (ClassDecl { tcdLName = L _ nm, tcdATs = ats }) <- decl
337 = (nm, APromotionErr ClassPE) :
338 (map (, APromotionErr TyConPE) $ map (unLoc . fdLName . unLoc) ats) ++
339 (mk_thing_env decls)
340
341 | otherwise
342 = (tcdName (unLoc decl), APromotionErr TyConPE) :
343 (mk_thing_env decls)
344
345 getInitialKinds :: [LTyClDecl Name] -> TcM [(Name, TcTyThing)]
346 getInitialKinds decls
347 = tcExtendKindEnv2 (mk_thing_env decls) $
348 do { pairss <- mapM (addLocM getInitialKind) decls
349 ; return (concat pairss) }
350
351 getInitialKind :: TyClDecl Name -> TcM [(Name, TcTyThing)]
352 -- Allocate a fresh kind variable for each TyCon and Class
353 -- For each tycon, return (tc, AThing k)
354 -- where k is the kind of tc, derived from the LHS
355 -- of the definition (and probably including
356 -- kind unification variables)
357 -- Example: data T a b = ...
358 -- return (T, kv1 -> kv2 -> kv3)
359 --
360 -- This pass deals with (ie incorporates into the kind it produces)
361 -- * The kind signatures on type-variable binders
362 -- * The result kinds signature on a TyClDecl
363 --
364 -- ALSO for each datacon, return (dc, APromotionErr RecDataConPE)
365 -- Note [ARecDataCon: Recursion and promoting data constructors]
366 --
367 -- No family instances are passed to getInitialKinds
368
369 getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs = ats })
370 = do { (cl_kind, inner_prs) <-
371 kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $
372 do { inner_prs <- getFamDeclInitialKinds ats
373 ; return (constraintKind, inner_prs) }
374 ; let main_pr = (name, AThing cl_kind)
375 ; return (main_pr : inner_prs) }
376
377 getInitialKind decl@(DataDecl { tcdLName = L _ name
378 , tcdTyVars = ktvs
379 , tcdDataDefn = HsDataDefn { dd_kindSig = m_sig
380 , dd_cons = cons' } })
381 = let cons = cons' -- AZ list monad coming
382 in
383 do { (decl_kind, _) <-
384 kcHsTyVarBndrs (hsDeclHasCusk decl) ktvs $
385 do { res_k <- case m_sig of
386 Just ksig -> tcLHsKind ksig
387 Nothing -> return liftedTypeKind
388 ; return (res_k, ()) }
389 ; let main_pr = (name, AThing decl_kind)
390 inner_prs = [ (unLoc con, APromotionErr RecDataConPE)
391 | L _ con' <- cons, con <- con_names con' ]
392 ; return (main_pr : inner_prs) }
393
394 getInitialKind (FamDecl { tcdFam = decl })
395 = getFamDeclInitialKind decl
396
397 getInitialKind decl@(SynDecl {})
398 = pprPanic "getInitialKind" (ppr decl)
399
400 ---------------------------------
401 getFamDeclInitialKinds :: [LFamilyDecl Name] -> TcM [(Name, TcTyThing)]
402 getFamDeclInitialKinds decls
403 = tcExtendKindEnv2 [ (n, APromotionErr TyConPE)
404 | L _ (FamilyDecl { fdLName = L _ n }) <- decls] $
405 concatMapM (addLocM getFamDeclInitialKind) decls
406
407 getFamDeclInitialKind :: FamilyDecl Name
408 -> TcM [(Name, TcTyThing)]
409 getFamDeclInitialKind decl@(FamilyDecl { fdLName = L _ name
410 , fdTyVars = ktvs
411 , fdKindSig = ksig })
412 = do { (fam_kind, _) <-
413 kcHsTyVarBndrs (famDeclHasCusk decl) ktvs $
414 do { res_k <- case ksig of
415 Just k -> tcLHsKind k
416 Nothing
417 | famDeclHasCusk decl -> return liftedTypeKind
418 | otherwise -> newMetaKindVar
419 ; return (res_k, ()) }
420 ; return [ (name, AThing fam_kind) ] }
421
422 ----------------
423 kcSynDecls :: [SCC (LTyClDecl Name)]
424 -> TcM TcLclEnv -- Kind bindings
425 kcSynDecls [] = getLclEnv
426 kcSynDecls (group : groups)
427 = do { (n,k) <- kcSynDecl1 group
428 ; lcl_env <- tcExtendKindEnv [(n,k)] (kcSynDecls groups)
429 ; return lcl_env }
430
431 kcSynDecl1 :: SCC (LTyClDecl Name)
432 -> TcM (Name,TcKind) -- Kind bindings
433 kcSynDecl1 (AcyclicSCC (L _ decl)) = kcSynDecl decl
434 kcSynDecl1 (CyclicSCC decls) = do { recSynErr decls; failM }
435 -- Fail here to avoid error cascade
436 -- of out-of-scope tycons
437
438 kcSynDecl :: TyClDecl Name -> TcM (Name, TcKind)
439 kcSynDecl decl@(SynDecl { tcdTyVars = hs_tvs, tcdLName = L _ name
440 , tcdRhs = rhs })
441 -- Returns a possibly-unzonked kind
442 = tcAddDeclCtxt decl $
443 do { (syn_kind, _) <-
444 kcHsTyVarBndrs (hsDeclHasCusk decl) hs_tvs $
445 do { traceTc "kcd1" (ppr name <+> brackets (ppr hs_tvs))
446 ; (_, rhs_kind) <- tcLHsType rhs
447 ; traceTc "kcd2" (ppr name)
448 ; return (rhs_kind, ()) }
449 ; return (name, syn_kind) }
450 kcSynDecl decl = pprPanic "kcSynDecl" (ppr decl)
451
452 ------------------------------------------------------------------------
453 kcLTyClDecl :: LTyClDecl Name -> TcM ()
454 -- See Note [Kind checking for type and class decls]
455 kcLTyClDecl (L loc decl)
456 = setSrcSpan loc $ tcAddDeclCtxt decl $ kcTyClDecl decl
457
458 kcTyClDecl :: TyClDecl Name -> TcM ()
459 -- This function is used solely for its side effect on kind variables
460 -- NB kind signatures on the type variables and
461 -- result kind signature have aready been dealt with
462 -- by getInitialKind, so we can ignore them here.
463
464 kcTyClDecl (DataDecl { tcdLName = L _ name, tcdTyVars = hs_tvs, tcdDataDefn = defn })
465 | HsDataDefn { dd_cons = cons, dd_kindSig = Just _ } <- defn
466 = mapM_ (wrapLocM kcConDecl) cons
467 -- hs_tvs and dd_kindSig already dealt with in getInitialKind
468 -- If dd_kindSig is Just, this must be a GADT-style decl,
469 -- (see invariants of DataDefn declaration)
470 -- so (a) we don't need to bring the hs_tvs into scope, because the
471 -- ConDecls bind all their own variables
472 -- (b) dd_ctxt is not allowed for GADT-style decls, so we can ignore it
473
474 | HsDataDefn { dd_ctxt = ctxt, dd_cons = cons } <- defn
475 = kcTyClTyVars name hs_tvs $
476 do { _ <- tcHsContext ctxt
477 ; mapM_ (wrapLocM kcConDecl) cons }
478
479 kcTyClDecl decl@(SynDecl {}) = pprPanic "kcTyClDecl" (ppr decl)
480
481 kcTyClDecl (ClassDecl { tcdLName = L _ name, tcdTyVars = hs_tvs
482 , tcdCtxt = ctxt, tcdSigs = sigs })
483 = kcTyClTyVars name hs_tvs $
484 do { _ <- tcHsContext ctxt
485 ; mapM_ (wrapLocM kc_sig) sigs }
486 where
487 kc_sig (TypeSig _ op_ty _) = discardResult (tcHsLiftedType op_ty)
488 kc_sig (GenericSig _ op_ty) = discardResult (tcHsLiftedType op_ty)
489 kc_sig _ = return ()
490
491 -- closed type families look at their equations, but other families don't
492 -- do anything here
493 kcTyClDecl (FamDecl (FamilyDecl { fdLName = L _ fam_tc_name
494 , fdTyVars = hs_tvs
495 , fdInfo = ClosedTypeFamily eqns }))
496 = do { tc_kind <- kcLookupKind fam_tc_name
497 ; let fam_tc_shape = ( fam_tc_name, length (hsQTvBndrs hs_tvs), tc_kind)
498 ; mapM_ (kcTyFamInstEqn fam_tc_shape) eqns }
499 kcTyClDecl (FamDecl {}) = return ()
500
501 -------------------
502 kcConDecl :: ConDecl Name -> TcM ()
503 kcConDecl (ConDecl { con_names = names, con_qvars = ex_tvs
504 , con_cxt = ex_ctxt, con_details = details
505 , con_res = res })
506 = addErrCtxt (dataConCtxtName names) $
507 -- the 'False' says that the existentials don't have a CUSK, as the
508 -- concept doesn't really apply here. We just need to bring the variables
509 -- into scope!
510 do { _ <- kcHsTyVarBndrs False ex_tvs $
511 do { _ <- tcHsContext ex_ctxt
512 ; mapM_ (tcHsOpenType . getBangType) (hsConDeclArgTys details)
513 ; _ <- tcConRes res
514 ; return (panic "kcConDecl", ()) }
515 ; return () }
516
517 {-
518 Note [Recursion and promoting data constructors]
519 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
520 We don't want to allow promotion in a strongly connected component
521 when kind checking.
522
523 Consider:
524 data T f = K (f (K Any))
525
526 When kind checking the `data T' declaration the local env contains the
527 mappings:
528 T -> AThing <some initial kind>
529 K -> ARecDataCon
530
531 ANothing is only used for DataCons, and only used during type checking
532 in tcTyClGroup.
533
534
535 ************************************************************************
536 * *
537 \subsection{Type checking}
538 * *
539 ************************************************************************
540
541 Note [Type checking recursive type and class declarations]
542 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
543 At this point we have completed *kind-checking* of a mutually
544 recursive group of type/class decls (done in kcTyClGroup). However,
545 we discarded the kind-checked types (eg RHSs of data type decls);
546 note that kcTyClDecl returns (). There are two reasons:
547
548 * It's convenient, because we don't have to rebuild a
549 kinded HsDecl (a fairly elaborate type)
550
551 * It's necessary, because after kind-generalisation, the
552 TyCons/Classes may now be kind-polymorphic, and hence need
553 to be given kind arguments.
554
555 Example:
556 data T f a = MkT (f a) (T f a)
557 During kind-checking, we give T the kind T :: k1 -> k2 -> *
558 and figure out constraints on k1, k2 etc. Then we generalise
559 to get T :: forall k. (k->*) -> k -> *
560 So now the (T f a) in the RHS must be elaborated to (T k f a).
561
562 However, during tcTyClDecl of T (above) we will be in a recursive
563 "knot". So we aren't allowed to look at the TyCon T itself; we are only
564 allowed to put it (lazily) in the returned structures. But when
565 kind-checking the RHS of T's decl, we *do* need to know T's kind (so
566 that we can correctly elaboarate (T k f a). How can we get T's kind
567 without looking at T? Delicate answer: during tcTyClDecl, we extend
568
569 *Global* env with T -> ATyCon (the (not yet built) TyCon for T)
570 *Local* env with T -> AThing (polymorphic kind of T)
571
572 Then:
573
574 * During TcHsType.kcTyVar we look in the *local* env, to get the
575 known kind for T.
576
577 * But in TcHsType.ds_type (and ds_var_app in particular) we look in
578 the *global* env to get the TyCon. But we must be careful not to
579 force the TyCon or we'll get a loop.
580
581 This fancy footwork (with two bindings for T) is only necesary for the
582 TyCons or Classes of this recursive group. Earlier, finished groups,
583 live in the global env only.
584 -}
585
586 tcTyClDecl :: RecTyInfo -> LTyClDecl Name -> TcM [TyThing]
587 tcTyClDecl rec_info (L loc decl)
588 = setSrcSpan loc $ tcAddDeclCtxt decl $
589 traceTc "tcTyAndCl-x" (ppr decl) >>
590 tcTyClDecl1 NoParentTyCon rec_info decl
591
592 -- "type family" declarations
593 tcTyClDecl1 :: TyConParent -> RecTyInfo -> TyClDecl Name -> TcM [TyThing]
594 tcTyClDecl1 parent _rec_info (FamDecl { tcdFam = fd })
595 = tcFamDecl1 parent fd
596
597 -- "type" synonym declaration
598 tcTyClDecl1 _parent rec_info
599 (SynDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdRhs = rhs })
600 = ASSERT( isNoParent _parent )
601 tcTyClTyVars tc_name tvs $ \ tvs' kind ->
602 tcTySynRhs rec_info tc_name tvs' kind rhs
603
604 -- "data/newtype" declaration
605 tcTyClDecl1 _parent rec_info
606 (DataDecl { tcdLName = L _ tc_name, tcdTyVars = tvs, tcdDataDefn = defn })
607 = ASSERT( isNoParent _parent )
608 tcTyClTyVars tc_name tvs $ \ tvs' kind ->
609 tcDataDefn rec_info tc_name tvs' kind defn
610
611 tcTyClDecl1 _parent rec_info
612 (ClassDecl { tcdLName = L _ class_name, tcdTyVars = tvs
613 , tcdCtxt = ctxt, tcdMeths = meths
614 , tcdFDs = fundeps, tcdSigs = sigs
615 , tcdATs = ats, tcdATDefs = at_defs })
616 = ASSERT( isNoParent _parent )
617 do { (clas, tvs', gen_dm_env) <- fixM $ \ ~(clas,_,_) ->
618 tcTyClTyVars class_name tvs $ \ tvs' kind ->
619 do { MASSERT( isConstraintKind kind )
620 -- This little knot is just so we can get
621 -- hold of the name of the class TyCon, which we
622 -- need to look up its recursiveness
623 ; let tycon_name = tyConName (classTyCon clas)
624 tc_isrec = rti_is_rec rec_info tycon_name
625 roles = rti_roles rec_info tycon_name
626
627 ; ctxt' <- tcHsContext ctxt
628 ; ctxt' <- zonkTcTypeToTypes emptyZonkEnv ctxt'
629 -- Squeeze out any kind unification variables
630 ; fds' <- mapM (addLocM tc_fundep) fundeps
631 ; (sig_stuff, gen_dm_env) <- tcClassSigs class_name sigs meths
632 ; at_stuff <- tcClassATs class_name (AssocFamilyTyCon clas) ats at_defs
633 ; mindef <- tcClassMinimalDef class_name sigs sig_stuff
634 ; clas <- buildClass
635 class_name tvs' roles ctxt' fds' at_stuff
636 sig_stuff mindef tc_isrec
637 ; traceTc "tcClassDecl" (ppr fundeps $$ ppr tvs' $$ ppr fds')
638 ; return (clas, tvs', gen_dm_env) }
639
640 ; let { gen_dm_ids = [ AnId (mkExportedLocalId VanillaId gen_dm_name gen_dm_ty)
641 | (sel_id, GenDefMeth gen_dm_name) <- classOpItems clas
642 , let gen_dm_tau = expectJust "tcTyClDecl1" $
643 lookupNameEnv gen_dm_env (idName sel_id)
644 , let gen_dm_ty = mkSigmaTy tvs'
645 [mkClassPred clas (mkTyVarTys tvs')]
646 gen_dm_tau
647 ]
648 ; class_ats = map ATyCon (classATs clas) }
649
650 ; return (ATyCon (classTyCon clas) : gen_dm_ids ++ class_ats ) }
651 -- NB: Order is important due to the call to `mkGlobalThings' when
652 -- tying the the type and class declaration type checking knot.
653 where
654 tc_fundep (tvs1, tvs2) = do { tvs1' <- mapM tc_fd_tyvar tvs1 ;
655 ; tvs2' <- mapM tc_fd_tyvar tvs2 ;
656 ; return (tvs1', tvs2') }
657 tc_fd_tyvar name -- Scoped kind variables are bound to unification variables
658 -- which are now fixed, so we can zonk
659 = do { tv <- tcLookupTyVar name
660 ; ty <- zonkTyVarOcc emptyZonkEnv tv
661 -- Squeeze out any kind unification variables
662 ; case getTyVar_maybe ty of
663 Just tv' -> return tv'
664 Nothing -> pprPanic "tc_fd_tyvar" (ppr name $$ ppr tv $$ ppr ty) }
665
666 tcFamDecl1 :: TyConParent -> FamilyDecl Name -> TcM [TyThing]
667 tcFamDecl1 parent
668 (FamilyDecl {fdInfo = OpenTypeFamily, fdLName = L _ tc_name, fdTyVars = tvs})
669 = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
670 { traceTc "open type family:" (ppr tc_name)
671 ; checkFamFlag tc_name
672 ; tycon <- buildFamilyTyCon tc_name tvs' OpenSynFamilyTyCon kind parent
673 ; return [ATyCon tycon] }
674
675 tcFamDecl1 parent
676 (FamilyDecl { fdInfo = ClosedTypeFamily eqns
677 , fdLName = lname@(L _ tc_name), fdTyVars = tvs })
678 -- Closed type families are a little tricky, because they contain the definition
679 -- of both the type family and the equations for a CoAxiom.
680 -- Note: eqns might be empty, in a hs-boot file!
681 = do { traceTc "closed type family:" (ppr tc_name)
682 -- the variables in the header have no scope:
683 ; (tvs', kind) <- tcTyClTyVars tc_name tvs $ \ tvs' kind ->
684 return (tvs', kind)
685
686 ; checkFamFlag tc_name -- make sure we have -XTypeFamilies
687
688 -- Process the equations, creating CoAxBranches
689 ; tc_kind <- kcLookupKind tc_name
690 ; let fam_tc_shape = (tc_name, length (hsQTvBndrs tvs), tc_kind)
691
692 ; branches <- mapM (tcTyFamInstEqn fam_tc_shape) eqns
693
694 -- we need the tycon that we will be creating, but it's in scope.
695 -- just look it up.
696 ; fam_tc <- tcLookupLocatedTyCon lname
697
698 -- create a CoAxiom, with the correct src location. It is Vitally
699 -- Important that we do not pass the branches into
700 -- newFamInstAxiomName. They have types that have been zonked inside
701 -- the knot and we will die if we look at them. This is OK here
702 -- because there will only be one axiom, so we don't need to
703 -- differentiate names.
704 -- See [Zonking inside the knot] in TcHsType
705 ; loc <- getSrcSpanM
706 ; co_ax_name <- newFamInstAxiomName loc tc_name []
707
708 -- mkBranchedCoAxiom will fail on an empty list of branches, but
709 -- we'll never look at co_ax in this case
710 ; let co_ax = mkBranchedCoAxiom co_ax_name fam_tc branches
711
712 -- now, finally, build the TyCon
713 ; let syn_rhs = if null eqns
714 then AbstractClosedSynFamilyTyCon
715 else ClosedSynFamilyTyCon co_ax
716 ; tycon <- buildFamilyTyCon tc_name tvs' syn_rhs kind parent
717
718 ; let result = if null eqns
719 then [ATyCon tycon]
720 else [ATyCon tycon, ACoAxiom co_ax]
721 ; return result }
722 -- We check for instance validity later, when doing validity checking for
723 -- the tycon
724
725 tcFamDecl1 parent
726 (FamilyDecl {fdInfo = DataFamily, fdLName = L _ tc_name, fdTyVars = tvs})
727 = tcTyClTyVars tc_name tvs $ \ tvs' kind -> do
728 { traceTc "data family:" (ppr tc_name)
729 ; checkFamFlag tc_name
730 ; extra_tvs <- tcDataKindSig kind
731 ; let final_tvs = tvs' ++ extra_tvs -- we may not need these
732 roles = map (const Nominal) final_tvs
733 tycon = buildAlgTyCon tc_name final_tvs roles Nothing []
734 DataFamilyTyCon Recursive
735 False -- Not promotable to the kind level
736 True -- GADT syntax
737 parent
738 ; return [ATyCon tycon] }
739
740 tcTySynRhs :: RecTyInfo
741 -> Name
742 -> [TyVar] -> Kind
743 -> LHsType Name -> TcM [TyThing]
744 tcTySynRhs rec_info tc_name tvs kind hs_ty
745 = do { env <- getLclEnv
746 ; traceTc "tc-syn" (ppr tc_name $$ ppr (tcl_env env))
747 ; rhs_ty <- tcCheckLHsType hs_ty kind
748 ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
749 ; let roles = rti_roles rec_info tc_name
750 ; tycon <- buildSynonymTyCon tc_name tvs roles rhs_ty kind
751 ; return [ATyCon tycon] }
752
753 tcDataDefn :: RecTyInfo -> Name
754 -> [TyVar] -> Kind
755 -> HsDataDefn Name -> TcM [TyThing]
756 -- NB: not used for newtype/data instances (whether associated or not)
757 tcDataDefn rec_info tc_name tvs kind
758 (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
759 , dd_ctxt = ctxt, dd_kindSig = mb_ksig
760 , dd_cons = cons' })
761 = let cons = cons' -- AZ List monad coming
762 in do { extra_tvs <- tcDataKindSig kind
763 ; let final_tvs = tvs ++ extra_tvs
764 roles = rti_roles rec_info tc_name
765 ; stupid_tc_theta <- tcHsContext ctxt
766 ; stupid_theta <- zonkTcTypeToTypes emptyZonkEnv stupid_tc_theta
767 ; kind_signatures <- xoptM Opt_KindSignatures
768 ; is_boot <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
769
770 -- Check that we don't use kind signatures without Glasgow extensions
771 ; case mb_ksig of
772 Nothing -> return ()
773 Just hs_k -> do { checkTc (kind_signatures) (badSigTyDecl tc_name)
774 ; tc_kind <- tcLHsKind hs_k
775 ; checkKind kind tc_kind
776 ; return () }
777
778 ; gadt_syntax <- dataDeclChecks tc_name new_or_data stupid_theta cons
779
780 ; tycon <- fixM $ \ tycon -> do
781 { let res_ty = mkTyConApp tycon (mkTyVarTys final_tvs)
782 ; data_cons <- tcConDecls new_or_data tycon (final_tvs, res_ty) cons
783 ; tc_rhs <-
784 if null cons && is_boot -- In a hs-boot file, empty cons means
785 then return totallyAbstractTyConRhs -- "don't know"; hence totally Abstract
786 else case new_or_data of
787 DataType -> return (mkDataTyConRhs data_cons)
788 NewType -> ASSERT( not (null data_cons) )
789 mkNewTyConRhs tc_name tycon (head data_cons)
790 ; return (buildAlgTyCon tc_name final_tvs roles (fmap unLoc cType)
791 stupid_theta tc_rhs
792 (rti_is_rec rec_info tc_name)
793 (rti_promotable rec_info)
794 gadt_syntax NoParentTyCon) }
795 ; return [ATyCon tycon] }
796
797 {-
798 ************************************************************************
799 * *
800 Typechecking associated types (in class decls)
801 (including the associated-type defaults)
802 * *
803 ************************************************************************
804
805 Note [Associated type defaults]
806 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
807
808 The following is an example of associated type defaults:
809 class C a where
810 data D a
811
812 type F a b :: *
813 type F a Z = [a] -- Default
814 type F a (S n) = F a n -- Default
815
816 Note that:
817 - We can have more than one default definition for a single associated type,
818 as long as they do not overlap (same rules as for instances)
819 - We can get default definitions only for type families, not data families
820 -}
821
822 tcClassATs :: Name -- The class name (not knot-tied)
823 -> TyConParent -- The class parent of this associated type
824 -> [LFamilyDecl Name] -- Associated types.
825 -> [LTyFamDefltEqn Name] -- Associated type defaults.
826 -> TcM [ClassATItem]
827 tcClassATs class_name parent ats at_defs
828 = do { -- Complain about associated type defaults for non associated-types
829 sequence_ [ failWithTc (badATErr class_name n)
830 | n <- map at_def_tycon at_defs
831 , not (n `elemNameSet` at_names) ]
832 ; mapM tc_at ats }
833 where
834 at_def_tycon :: LTyFamDefltEqn Name -> Name
835 at_def_tycon (L _ eqn) = unLoc (tfe_tycon eqn)
836
837 at_fam_name :: LFamilyDecl Name -> Name
838 at_fam_name (L _ decl) = unLoc (fdLName decl)
839
840 at_names = mkNameSet (map at_fam_name ats)
841
842 at_defs_map :: NameEnv [LTyFamDefltEqn Name]
843 -- Maps an AT in 'ats' to a list of all its default defs in 'at_defs'
844 at_defs_map = foldr (\at_def nenv -> extendNameEnv_C (++) nenv
845 (at_def_tycon at_def) [at_def])
846 emptyNameEnv at_defs
847
848 tc_at at = do { [ATyCon fam_tc] <- addLocM (tcFamDecl1 parent) at
849 ; let at_defs = lookupNameEnv at_defs_map (at_fam_name at)
850 `orElse` []
851 ; atd <- tcDefaultAssocDecl fam_tc at_defs
852 ; return (ATI fam_tc atd) }
853
854 -------------------------
855 tcDefaultAssocDecl :: TyCon -- ^ Family TyCon
856 -> [LTyFamDefltEqn Name] -- ^ Defaults
857 -> TcM (Maybe Type) -- ^ Type checked RHS
858 tcDefaultAssocDecl _ []
859 = return Nothing -- No default declaration
860
861 tcDefaultAssocDecl _ (d1:_:_)
862 = failWithTc (ptext (sLit "More than one default declaration for")
863 <+> ppr (tfe_tycon (unLoc d1)))
864
865 tcDefaultAssocDecl fam_tc [L loc (TyFamEqn { tfe_tycon = L _ tc_name
866 , tfe_pats = hs_tvs
867 , tfe_rhs = rhs })]
868 = setSrcSpan loc $
869 tcAddFamInstCtxt (ptext (sLit "default type instance")) tc_name $
870 tcTyClTyVars tc_name hs_tvs $ \ tvs rhs_kind ->
871 do { traceTc "tcDefaultAssocDecl" (ppr tc_name)
872 ; checkTc (isTypeFamilyTyCon fam_tc) (wrongKindOfFamily fam_tc)
873 ; let (fam_name, fam_pat_arity, _) = famTyConShape fam_tc
874 ; ASSERT( fam_name == tc_name )
875 checkTc (length (hsQTvBndrs hs_tvs) == fam_pat_arity)
876 (wrongNumberOfParmsErr fam_pat_arity)
877 ; rhs_ty <- tcCheckLHsType rhs rhs_kind
878 ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
879 ; let fam_tc_tvs = tyConTyVars fam_tc
880 subst = zipTopTvSubst tvs (mkTyVarTys fam_tc_tvs)
881 ; return ( ASSERT( equalLength fam_tc_tvs tvs )
882 Just (substTy subst rhs_ty) ) }
883 -- We check for well-formedness and validity later, in checkValidClass
884
885 -------------------------
886 kcTyFamInstEqn :: FamTyConShape -> LTyFamInstEqn Name -> TcM ()
887 kcTyFamInstEqn fam_tc_shape
888 (L loc (TyFamEqn { tfe_pats = pats, tfe_rhs = hs_ty }))
889 = setSrcSpan loc $
890 discardResult $
891 tc_fam_ty_pats fam_tc_shape pats (discardResult . (tcCheckLHsType hs_ty))
892
893 tcTyFamInstEqn :: FamTyConShape -> LTyFamInstEqn Name -> TcM CoAxBranch
894 -- Needs to be here, not in TcInstDcls, because closed families
895 -- (typechecked here) have TyFamInstEqns
896 tcTyFamInstEqn fam_tc_shape@(fam_tc_name,_,_)
897 (L loc (TyFamEqn { tfe_tycon = L _ eqn_tc_name
898 , tfe_pats = pats
899 , tfe_rhs = hs_ty }))
900 = setSrcSpan loc $
901 tcFamTyPats fam_tc_shape pats (discardResult . (tcCheckLHsType hs_ty)) $
902 \tvs' pats' res_kind ->
903 do { checkTc (fam_tc_name == eqn_tc_name)
904 (wrongTyFamName fam_tc_name eqn_tc_name)
905 ; rhs_ty <- tcCheckLHsType hs_ty res_kind
906 ; rhs_ty <- zonkTcTypeToType emptyZonkEnv rhs_ty
907 ; traceTc "tcTyFamInstEqn" (ppr fam_tc_name <+> ppr tvs')
908 -- don't print out the pats here, as they might be zonked inside the knot
909 ; return (mkCoAxBranch tvs' pats' rhs_ty loc) }
910
911 kcDataDefn :: HsDataDefn Name -> TcKind -> TcM ()
912 -- Used for 'data instance' only
913 -- Ordinary 'data' is handled by kcTyClDec
914 kcDataDefn (HsDataDefn { dd_ctxt = ctxt, dd_cons = cons, dd_kindSig = mb_kind }) res_k
915 = do { _ <- tcHsContext ctxt
916 ; checkNoErrs $ mapM_ (wrapLocM kcConDecl) cons
917 -- See Note [Failing early in kcDataDefn]
918 ; kcResultKind mb_kind res_k }
919
920 ------------------
921 kcResultKind :: Maybe (LHsKind Name) -> Kind -> TcM ()
922 kcResultKind Nothing res_k
923 = checkKind res_k liftedTypeKind
924 -- type family F a
925 -- defaults to type family F a :: *
926 kcResultKind (Just k) res_k
927 = do { k' <- tcLHsKind k
928 ; checkKind k' res_k }
929
930 {-
931 Kind check type patterns and kind annotate the embedded type variables.
932 type instance F [a] = rhs
933
934 * Here we check that a type instance matches its kind signature, but we do
935 not check whether there is a pattern for each type index; the latter
936 check is only required for type synonym instances.
937
938 Note [tc_fam_ty_pats vs tcFamTyPats]
939 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
940 tc_fam_ty_pats does the type checking of the patterns, but it doesn't
941 zonk or generate any desugaring. It is used when kind-checking closed
942 type families.
943
944 tcFamTyPats type checks the patterns, zonks, and then calls thing_inside
945 to generate a desugaring. It is used during type-checking (not kind-checking).
946
947 Note [Type-checking type patterns]
948 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
949 When typechecking the patterns of a family instance declaration, we can't
950 rely on using the family TyCon, because this is sometimes called
951 from within a type-checking knot. (Specifically for closed type families.)
952 The type FamTyConShape gives just enough information to do the job.
953
954 The "arity" field of FamTyConShape is the *visible* arity of the family
955 type constructor, i.e. what the users sees and writes, not including kind
956 arguments.
957
958 See also Note [tc_fam_ty_pats vs tcFamTyPats]
959
960 Note [Failing early in kcDataDefn]
961 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
962 We need to use checkNoErrs when calling kcConDecl. This is because kcConDecl
963 calls tcConDecl, which checks that the return type of a GADT-like constructor
964 is actually an instance of the type head. Without the checkNoErrs, potentially
965 two bad things could happen:
966
967 1) Duplicate error messages, because tcConDecl will be called again during
968 *type* checking (as opposed to kind checking)
969 2) If we just keep blindly forging forward after both kind checking and type
970 checking, we can get a panic in rejigConRes. See Trac #8368.
971 -}
972
973 -----------------
974 type FamTyConShape = (Name, Arity, Kind) -- See Note [Type-checking type patterns]
975
976 famTyConShape :: TyCon -> FamTyConShape
977 famTyConShape fam_tc
978 = ( tyConName fam_tc
979 , length (filterOut isKindVar (tyConTyVars fam_tc))
980 , tyConKind fam_tc )
981
982 tc_fam_ty_pats :: FamTyConShape
983 -> HsWithBndrs Name [LHsType Name] -- Patterns
984 -> (TcKind -> TcM ()) -- Kind checker for RHS
985 -- result is ignored
986 -> TcM ([Kind], [Type], Kind)
987 -- Check the type patterns of a type or data family instance
988 -- type instance F <pat1> <pat2> = <type>
989 -- The 'tyvars' are the free type variables of pats
990 --
991 -- NB: The family instance declaration may be an associated one,
992 -- nested inside an instance decl, thus
993 -- instance C [a] where
994 -- type F [a] = ...
995 -- In that case, the type variable 'a' will *already be in scope*
996 -- (and, if C is poly-kinded, so will its kind parameter).
997
998 tc_fam_ty_pats (name, arity, kind)
999 (HsWB { hswb_cts = arg_pats, hswb_kvs = kvars, hswb_tvs = tvars })
1000 kind_checker
1001 = do { let (fam_kvs, fam_body) = splitForAllTys kind
1002
1003 -- We wish to check that the pattern has the right number of arguments
1004 -- in checkValidFamPats (in TcValidity), so we can do the check *after*
1005 -- we're done with the knot. But, the splitKindFunTysN below will panic
1006 -- if there are *too many* patterns. So, we do a preliminary check here.
1007 -- Note that we don't have enough information at hand to do a full check,
1008 -- as that requires the full declared arity of the family, which isn't
1009 -- nearby.
1010 ; checkTc (length arg_pats == arity) $
1011 wrongNumberOfParmsErr arity
1012
1013 -- Instantiate with meta kind vars
1014 ; fam_arg_kinds <- mapM (const newMetaKindVar) fam_kvs
1015 ; loc <- getSrcSpanM
1016 ; let (arg_kinds, res_kind)
1017 = splitKindFunTysN (length arg_pats) $
1018 substKiWith fam_kvs fam_arg_kinds fam_body
1019 hs_tvs = HsQTvs { hsq_kvs = kvars
1020 , hsq_tvs = userHsTyVarBndrs loc tvars }
1021
1022 -- Kind-check and quantify
1023 -- See Note [Quantifying over family patterns]
1024 ; typats <- tcHsTyVarBndrs hs_tvs $ \ _ ->
1025 do { kind_checker res_kind
1026 ; tcHsArgTys (quotes (ppr name)) arg_pats arg_kinds }
1027
1028 ; return (fam_arg_kinds, typats, res_kind) }
1029
1030 -- See Note [tc_fam_ty_pats vs tcFamTyPats]
1031 tcFamTyPats :: FamTyConShape
1032 -> HsWithBndrs Name [LHsType Name] -- patterns
1033 -> (TcKind -> TcM ()) -- kind-checker for RHS
1034 -> ([TKVar] -- Kind and type variables
1035 -> [TcType] -- Kind and type arguments
1036 -> Kind -> TcM a)
1037 -> TcM a
1038 tcFamTyPats fam_shape@(name,_,_) pats kind_checker thing_inside
1039 = do { (fam_arg_kinds, typats, res_kind)
1040 <- tc_fam_ty_pats fam_shape pats kind_checker
1041 ; let all_args = fam_arg_kinds ++ typats
1042
1043 -- Find free variables (after zonking) and turn
1044 -- them into skolems, so that we don't subsequently
1045 -- replace a meta kind var with AnyK
1046 -- Very like kindGeneralize
1047 ; qtkvs <- quantifyTyVars emptyVarSet (tyVarsOfTypes all_args)
1048
1049 -- Zonk the patterns etc into the Type world
1050 ; (ze, qtkvs') <- zonkTyBndrsX emptyZonkEnv qtkvs
1051 ; all_args' <- zonkTcTypeToTypes ze all_args
1052 ; res_kind' <- zonkTcTypeToType ze res_kind
1053
1054 ; traceTc "tcFamTyPats" (ppr name)
1055 -- don't print out too much, as we might be in the knot
1056 ; tcExtendTyVarEnv qtkvs' $
1057 thing_inside qtkvs' all_args' res_kind' }
1058
1059 {-
1060 Note [Quantifying over family patterns]
1061 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1062 We need to quantify over two different lots of kind variables:
1063
1064 First, the ones that come from the kinds of the tyvar args of
1065 tcTyVarBndrsKindGen, as usual
1066 data family Dist a
1067
1068 -- Proxy :: forall k. k -> *
1069 data instance Dist (Proxy a) = DP
1070 -- Generates data DistProxy = DP
1071 -- ax8 k (a::k) :: Dist * (Proxy k a) ~ DistProxy k a
1072 -- The 'k' comes from the tcTyVarBndrsKindGen (a::k)
1073
1074 Second, the ones that come from the kind argument of the type family
1075 which we pick up using the (tyVarsOfTypes typats) in the result of
1076 the thing_inside of tcHsTyvarBndrsGen.
1077 -- Any :: forall k. k
1078 data instance Dist Any = DA
1079 -- Generates data DistAny k = DA
1080 -- ax7 k :: Dist k (Any k) ~ DistAny k
1081 -- The 'k' comes from kindGeneralizeKinds (Any k)
1082
1083 Note [Quantified kind variables of a family pattern]
1084 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1085 Consider type family KindFam (p :: k1) (q :: k1)
1086 data T :: Maybe k1 -> k2 -> *
1087 type instance KindFam (a :: Maybe k) b = T a b -> Int
1088 The HsBSig for the family patterns will be ([k], [a])
1089
1090 Then in the family instance we want to
1091 * Bring into scope [ "k" -> k:BOX, "a" -> a:k ]
1092 * Kind-check the RHS
1093 * Quantify the type instance over k and k', as well as a,b, thus
1094 type instance [k, k', a:Maybe k, b:k']
1095 KindFam (Maybe k) k' a b = T k k' a b -> Int
1096
1097 Notice that in the third step we quantify over all the visibly-mentioned
1098 type variables (a,b), but also over the implicitly mentioned kind variables
1099 (k, k'). In this case one is bound explicitly but often there will be
1100 none. The role of the kind signature (a :: Maybe k) is to add a constraint
1101 that 'a' must have that kind, and to bring 'k' into scope.
1102
1103
1104 ************************************************************************
1105 * *
1106 Data types
1107 * *
1108 ************************************************************************
1109 -}
1110
1111 dataDeclChecks :: Name -> NewOrData -> ThetaType -> [LConDecl Name] -> TcM Bool
1112 dataDeclChecks tc_name new_or_data stupid_theta cons
1113 = do { -- Check that we don't use GADT syntax in H98 world
1114 gadtSyntax_ok <- xoptM Opt_GADTSyntax
1115 ; let gadt_syntax = consUseGadtSyntax cons
1116 ; checkTc (gadtSyntax_ok || not gadt_syntax) (badGadtDecl tc_name)
1117
1118 -- Check that the stupid theta is empty for a GADT-style declaration
1119 ; checkTc (null stupid_theta || not gadt_syntax) (badStupidTheta tc_name)
1120
1121 -- Check that a newtype has exactly one constructor
1122 -- Do this before checking for empty data decls, so that
1123 -- we don't suggest -XEmptyDataDecls for newtypes
1124 ; checkTc (new_or_data == DataType || isSingleton cons)
1125 (newtypeConError tc_name (length cons))
1126
1127 -- Check that there's at least one condecl,
1128 -- or else we're reading an hs-boot file, or -XEmptyDataDecls
1129 ; empty_data_decls <- xoptM Opt_EmptyDataDecls
1130 ; is_boot <- tcIsHsBootOrSig -- Are we compiling an hs-boot file?
1131 ; checkTc (not (null cons) || empty_data_decls || is_boot)
1132 (emptyConDeclsErr tc_name)
1133 ; return gadt_syntax }
1134
1135
1136 -----------------------------------
1137 consUseGadtSyntax :: [LConDecl a] -> Bool
1138 consUseGadtSyntax (L _ (ConDecl { con_res = ResTyGADT _ }) : _) = True
1139 consUseGadtSyntax _ = False
1140 -- All constructors have same shape
1141
1142 -----------------------------------
1143 tcConDecls :: NewOrData -> TyCon -> ([TyVar], Type)
1144 -> [LConDecl Name] -> TcM [DataCon]
1145 tcConDecls new_or_data rep_tycon (tmpl_tvs, res_tmpl) cons
1146 = concatMapM (addLocM $ tcConDecl new_or_data rep_tycon tmpl_tvs res_tmpl)
1147 cons
1148
1149 tcConDecl :: NewOrData
1150 -> TyCon -- Representation tycon
1151 -> [TyVar] -> Type -- Return type template (with its template tyvars)
1152 -- (tvs, T tys), where T is the family TyCon
1153 -> ConDecl Name
1154 -> TcM [DataCon]
1155
1156 tcConDecl new_or_data rep_tycon tmpl_tvs res_tmpl -- Data types
1157 (ConDecl { con_names = names
1158 , con_qvars = hs_tvs, con_cxt = hs_ctxt
1159 , con_details = hs_details, con_res = hs_res_ty })
1160 = addErrCtxt (dataConCtxtName names) $
1161 do { traceTc "tcConDecl 1" (ppr names)
1162 ; (ctxt, arg_tys, res_ty, field_lbls, stricts)
1163 <- tcHsTyVarBndrs hs_tvs $ \ _ ->
1164 do { ctxt <- tcHsContext hs_ctxt
1165 ; details <- tcConArgs new_or_data hs_details
1166 ; res_ty <- tcConRes hs_res_ty
1167 ; let (field_lbls, btys) = details
1168 (arg_tys, stricts) = unzip btys
1169 ; return (ctxt, arg_tys, res_ty, field_lbls, stricts)
1170 }
1171
1172 -- Generalise the kind variables (returning quantified TcKindVars)
1173 -- and quantify the type variables (substituting their kinds)
1174 -- REMEMBER: 'tkvs' are:
1175 -- ResTyH98: the *existential* type variables only
1176 -- ResTyGADT: *all* the quantified type variables
1177 -- c.f. the comment on con_qvars in HsDecls
1178 ; tkvs <- case res_ty of
1179 ResTyH98 -> quantifyTyVars (mkVarSet tmpl_tvs) (tyVarsOfTypes (ctxt++arg_tys))
1180 ResTyGADT res_ty -> quantifyTyVars emptyVarSet (tyVarsOfTypes (res_ty:ctxt++arg_tys))
1181
1182 -- Zonk to Types
1183 ; (ze, qtkvs) <- zonkTyBndrsX emptyZonkEnv tkvs
1184 ; arg_tys <- zonkTcTypeToTypes ze arg_tys
1185 ; ctxt <- zonkTcTypeToTypes ze ctxt
1186 ; res_ty <- case res_ty of
1187 ResTyH98 -> return ResTyH98
1188 ResTyGADT ty -> ResTyGADT <$> zonkTcTypeToType ze ty
1189
1190 ; let (univ_tvs, ex_tvs, eq_preds, res_ty') = rejigConRes tmpl_tvs res_tmpl qtkvs res_ty
1191
1192 ; fam_envs <- tcGetFamInstEnvs
1193 ; let
1194 buildOneDataCon (L _ name) = do
1195 { is_infix <- tcConIsInfix name hs_details res_ty
1196 ; buildDataCon fam_envs name is_infix
1197 stricts field_lbls
1198 univ_tvs ex_tvs eq_preds ctxt arg_tys
1199 res_ty' rep_tycon
1200 -- NB: we put data_tc, the type constructor gotten from the
1201 -- constructor type signature into the data constructor;
1202 -- that way checkValidDataCon can complain if it's wrong.
1203 }
1204 ; mapM buildOneDataCon names
1205 }
1206
1207
1208 tcConIsInfix :: Name
1209 -> HsConDetails (LHsType Name) [LConDeclField Name]
1210 -> ResType Type
1211 -> TcM Bool
1212 tcConIsInfix _ details ResTyH98
1213 = case details of
1214 InfixCon {} -> return True
1215 _ -> return False
1216 tcConIsInfix con details (ResTyGADT _)
1217 = case details of
1218 InfixCon {} -> return True
1219 RecCon {} -> return False
1220 PrefixCon arg_tys -- See Note [Infix GADT cons]
1221 | isSymOcc (getOccName con)
1222 , [_ty1,_ty2] <- arg_tys
1223 -> do { fix_env <- getFixityEnv
1224 ; return (con `elemNameEnv` fix_env) }
1225 | otherwise -> return False
1226
1227
1228
1229 tcConArgs :: NewOrData -> HsConDeclDetails Name
1230 -> TcM ([Name], [(TcType, HsBang)])
1231 tcConArgs new_or_data (PrefixCon btys)
1232 = do { btys' <- mapM (tcConArg new_or_data) btys
1233 ; return ([], btys') }
1234 tcConArgs new_or_data (InfixCon bty1 bty2)
1235 = do { bty1' <- tcConArg new_or_data bty1
1236 ; bty2' <- tcConArg new_or_data bty2
1237 ; return ([], [bty1', bty2']) }
1238 tcConArgs new_or_data (RecCon fields)
1239 = do { btys' <- mapM (tcConArg new_or_data) btys
1240 ; return (field_names, btys') }
1241 where
1242 -- We need a one-to-one mapping from field_names to btys
1243 combined = map (\(L _ f) -> (cd_fld_names f,cd_fld_type f)) fields
1244 explode (ns,ty) = zip (map unLoc ns) (repeat ty)
1245 exploded = concatMap explode combined
1246 (field_names,btys) = unzip exploded
1247
1248 tcConArg :: NewOrData -> LHsType Name -> TcM (TcType, HsBang)
1249 tcConArg new_or_data bty
1250 = do { traceTc "tcConArg 1" (ppr bty)
1251 ; arg_ty <- tcHsConArgType new_or_data bty
1252 ; traceTc "tcConArg 2" (ppr bty)
1253 ; return (arg_ty, getBangStrictness bty) }
1254
1255 tcConRes :: ResType (LHsType Name) -> TcM (ResType Type)
1256 tcConRes ResTyH98 = return ResTyH98
1257 tcConRes (ResTyGADT res_ty) = do { res_ty' <- tcHsLiftedType res_ty
1258 ; return (ResTyGADT res_ty') }
1259
1260 {-
1261 Note [Infix GADT constructors]
1262 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1263 We do not currently have syntax to declare an infix constructor in GADT syntax,
1264 but it makes a (small) difference to the Show instance. So as a slightly
1265 ad-hoc solution, we regard a GADT data constructor as infix if
1266 a) it is an operator symbol
1267 b) it has two arguments
1268 c) there is a fixity declaration for it
1269 For example:
1270 infix 6 (:--:)
1271 data T a where
1272 (:--:) :: t1 -> t2 -> T Int
1273
1274
1275 Note [Checking GADT return types]
1276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1277 There is a delicacy around checking the return types of a datacon. The
1278 central problem is dealing with a declaration like
1279
1280 data T a where
1281 MkT :: a -> Q a
1282
1283 Note that the return type of MkT is totally bogus. When creating the T
1284 tycon, we also need to create the MkT datacon, which must have a "rejigged"
1285 return type. That is, the MkT datacon's type must be transformed to have
1286 a uniform return type with explicit coercions for GADT-like type parameters.
1287 This rejigging is what rejigConRes does. The problem is, though, that checking
1288 that the return type is appropriate is much easier when done over *Type*,
1289 not *HsType*.
1290
1291 So, we want to make rejigConRes lazy and then check the validity of the return
1292 type in checkValidDataCon. But, if the return type is bogus, rejigConRes can't
1293 work -- it will have a failed pattern match. Luckily, if we run
1294 checkValidDataCon before ever looking at the rejigged return type
1295 (checkValidDataCon checks the dataConUserType, which is not rejigged!), we
1296 catch the error before forcing the rejigged type and panicking.
1297 -}
1298
1299 -- Example
1300 -- data instance T (b,c) where
1301 -- TI :: forall e. e -> T (e,e)
1302 --
1303 -- The representation tycon looks like this:
1304 -- data :R7T b c where
1305 -- TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
1306 -- In this case orig_res_ty = T (e,e)
1307
1308 rejigConRes :: [TyVar] -> Type -- Template for result type; e.g.
1309 -- data instance T [a] b c = ...
1310 -- gives template ([a,b,c], T [a] b c)
1311 -> [TyVar] -- where MkT :: forall x y z. ...
1312 -> ResType Type
1313 -> ([TyVar], -- Universal
1314 [TyVar], -- Existential (distinct OccNames from univs)
1315 [(TyVar,Type)], -- Equality predicates
1316 Type) -- Typechecked return type
1317 -- We don't check that the TyCon given in the ResTy is
1318 -- the same as the parent tycon, because checkValidDataCon will do it
1319
1320 rejigConRes tmpl_tvs res_ty dc_tvs ResTyH98
1321 = (tmpl_tvs, dc_tvs, [], res_ty)
1322 -- In H98 syntax the dc_tvs are the existential ones
1323 -- data T a b c = forall d e. MkT ...
1324 -- The {a,b,c} are tc_tvs, and {d,e} are dc_tvs
1325
1326 rejigConRes tmpl_tvs res_tmpl dc_tvs (ResTyGADT res_ty)
1327 -- E.g. data T [a] b c where
1328 -- MkT :: forall x y z. T [(x,y)] z z
1329 -- Then we generate
1330 -- Univ tyvars Eq-spec
1331 -- a a~(x,y)
1332 -- b b~z
1333 -- z
1334 -- Existentials are the leftover type vars: [x,y]
1335 -- So we return ([a,b,z], [x,y], [a~(x,y),b~z], T [(x,y)] z z)
1336 = (univ_tvs, ex_tvs, eq_spec, res_ty)
1337 where
1338 Just subst = tcMatchTy (mkVarSet tmpl_tvs) res_tmpl res_ty
1339 -- This 'Just' pattern is sure to match, because if not
1340 -- checkValidDataCon will complain first.
1341 -- See Note [Checking GADT return types]
1342
1343 -- /Lazily/ figure out the univ_tvs etc
1344 -- Each univ_tv is either a dc_tv or a tmpl_tv
1345 (univ_tvs, eq_spec) = foldr choose ([], []) tmpl_tvs
1346 choose tmpl (univs, eqs)
1347 | Just ty <- lookupTyVar subst tmpl
1348 = case tcGetTyVar_maybe ty of
1349 Just tv | not (tv `elem` univs)
1350 -> (tv:univs, eqs)
1351 _other -> (new_tmpl:univs, (new_tmpl,ty):eqs)
1352 where -- see Note [Substitution in template variables kinds]
1353 new_tmpl = updateTyVarKind (substTy subst) tmpl
1354 | otherwise = pprPanic "tcResultType" (ppr res_ty)
1355 ex_tvs = dc_tvs `minusList` univ_tvs
1356
1357 {-
1358 Note [Substitution in template variables kinds]
1359 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1360
1361 data List a = Nil | Cons a (List a)
1362 data SList s as where
1363 SNil :: SList s Nil
1364
1365 We call tcResultType with
1366 tmpl_tvs = [(k :: BOX), (s :: k -> *), (as :: List k)]
1367 res_tmpl = SList k s as
1368 res_ty = ResTyGADT (SList k1 (s1 :: k1 -> *) (Nil k1))
1369
1370 We get subst:
1371 k -> k1
1372 s -> s1
1373 as -> Nil k1
1374
1375 Now we want to find out the universal variables and the equivalences
1376 between some of them and types (GADT).
1377
1378 In this example, k and s are mapped to exactly variables which are not
1379 already present in the universal set, so we just add them without any
1380 coercion.
1381
1382 But 'as' is mapped to 'Nil k1', so we add 'as' to the universal set,
1383 and add the equivalence with 'Nil k1' in 'eqs'.
1384
1385 The problem is that with kind polymorphism, as's kind may now contain
1386 kind variables, and we have to apply the template substitution to it,
1387 which is why we create new_tmpl.
1388
1389 The template substitution only maps kind variables to kind variables,
1390 since GADTs are not kind indexed.
1391
1392 ************************************************************************
1393 * *
1394 Validity checking
1395 * *
1396 ************************************************************************
1397
1398 Validity checking is done once the mutually-recursive knot has been
1399 tied, so we can look at things freely.
1400 -}
1401
1402 checkClassCycleErrs :: Class -> TcM ()
1403 checkClassCycleErrs cls = mapM_ recClsErr (calcClassCycles cls)
1404
1405 checkValidTyCl :: TyThing -> TcM ()
1406 checkValidTyCl thing
1407 = setSrcSpan (getSrcSpan thing) $
1408 addTyThingCtxt thing $
1409 case thing of
1410 ATyCon tc -> checkValidTyCon tc
1411 AnId _ -> return () -- Generic default methods are checked
1412 -- with their parent class
1413 ACoAxiom _ -> return () -- Axioms checked with their parent
1414 -- closed family tycon
1415 _ -> pprTrace "checkValidTyCl" (ppr thing) $ return ()
1416
1417 -------------------------
1418 -- For data types declared with record syntax, we require
1419 -- that each constructor that has a field 'f'
1420 -- (a) has the same result type
1421 -- (b) has the same type for 'f'
1422 -- module alpha conversion of the quantified type variables
1423 -- of the constructor.
1424 --
1425 -- Note that we allow existentials to match because the
1426 -- fields can never meet. E.g
1427 -- data T where
1428 -- T1 { f1 :: b, f2 :: a, f3 ::Int } :: T
1429 -- T2 { f1 :: c, f2 :: c, f3 ::Int } :: T
1430 -- Here we do not complain about f1,f2 because they are existential
1431
1432 checkValidTyCon :: TyCon -> TcM ()
1433 checkValidTyCon tc
1434 | Just cl <- tyConClass_maybe tc
1435 = checkValidClass cl
1436
1437 | Just syn_rhs <- synTyConRhs_maybe tc
1438 = checkValidType syn_ctxt syn_rhs
1439
1440 | Just fam_flav <- famTyConFlav_maybe tc
1441 = case fam_flav of
1442 { ClosedSynFamilyTyCon ax -> checkValidClosedCoAxiom ax
1443 ; AbstractClosedSynFamilyTyCon ->
1444 do { hsBoot <- tcIsHsBootOrSig
1445 ; checkTc hsBoot $
1446 ptext (sLit "You may omit the equations in a closed type family") $$
1447 ptext (sLit "only in a .hs-boot file") }
1448 ; OpenSynFamilyTyCon -> return ()
1449 ; BuiltInSynFamTyCon _ -> return () }
1450
1451 | otherwise
1452 = do { -- Check the context on the data decl
1453 traceTc "cvtc1" (ppr tc)
1454 ; checkValidTheta (DataTyCtxt name) (tyConStupidTheta tc)
1455
1456 ; traceTc "cvtc2" (ppr tc)
1457
1458 ; dflags <- getDynFlags
1459 ; existential_ok <- xoptM Opt_ExistentialQuantification
1460 ; gadt_ok <- xoptM Opt_GADTs
1461 ; let ex_ok = existential_ok || gadt_ok -- Data cons can have existential context
1462 ; mapM_ (checkValidDataCon dflags ex_ok tc) data_cons
1463
1464 -- Check that fields with the same name share a type
1465 ; mapM_ check_fields groups }
1466
1467 where
1468 syn_ctxt = TySynCtxt name
1469 name = tyConName tc
1470 data_cons = tyConDataCons tc
1471
1472 groups = equivClasses cmp_fld (concatMap get_fields data_cons)
1473 cmp_fld (f1,_) (f2,_) = f1 `compare` f2
1474 get_fields con = dataConFieldLabels con `zip` repeat con
1475 -- dataConFieldLabels may return the empty list, which is fine
1476
1477 -- See Note [GADT record selectors] in MkId.lhs
1478 -- We must check (a) that the named field has the same
1479 -- type in each constructor
1480 -- (b) that those constructors have the same result type
1481 --
1482 -- However, the constructors may have differently named type variable
1483 -- and (worse) we don't know how the correspond to each other. E.g.
1484 -- C1 :: forall a b. { f :: a, g :: b } -> T a b
1485 -- C2 :: forall d c. { f :: c, g :: c } -> T c d
1486 --
1487 -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
1488 -- result type against other candidates' types BOTH WAYS ROUND.
1489 -- If they magically agrees, take the substitution and
1490 -- apply them to the latter ones, and see if they match perfectly.
1491 check_fields ((label, con1) : other_fields)
1492 -- These fields all have the same name, but are from
1493 -- different constructors in the data type
1494 = recoverM (return ()) $ mapM_ checkOne other_fields
1495 -- Check that all the fields in the group have the same type
1496 -- NB: this check assumes that all the constructors of a given
1497 -- data type use the same type variables
1498 where
1499 (tvs1, _, _, res1) = dataConSig con1
1500 ts1 = mkVarSet tvs1
1501 fty1 = dataConFieldType con1 label
1502
1503 checkOne (_, con2) -- Do it bothways to ensure they are structurally identical
1504 = do { checkFieldCompat label con1 con2 ts1 res1 res2 fty1 fty2
1505 ; checkFieldCompat label con2 con1 ts2 res2 res1 fty2 fty1 }
1506 where
1507 (tvs2, _, _, res2) = dataConSig con2
1508 ts2 = mkVarSet tvs2
1509 fty2 = dataConFieldType con2 label
1510 check_fields [] = panic "checkValidTyCon/check_fields []"
1511
1512 checkValidClosedCoAxiom :: CoAxiom Branched -> TcM ()
1513 checkValidClosedCoAxiom (CoAxiom { co_ax_branches = branches, co_ax_tc = tc })
1514 = tcAddClosedTypeFamilyDeclCtxt tc $
1515 do { brListFoldlM_ check_accessibility [] branches
1516 ; void $ brListMapM (checkValidTyFamInst Nothing tc) branches }
1517 where
1518 check_accessibility :: [CoAxBranch] -- prev branches (in reverse order)
1519 -> CoAxBranch -- cur branch
1520 -> TcM [CoAxBranch] -- cur : prev
1521 -- Check whether the branch is dominated by earlier
1522 -- ones and hence is inaccessible
1523 check_accessibility prev_branches cur_branch
1524 = do { when (cur_branch `isDominatedBy` prev_branches) $
1525 addWarnAt (coAxBranchSpan cur_branch) $
1526 inaccessibleCoAxBranch tc cur_branch
1527 ; return (cur_branch : prev_branches) }
1528
1529 checkFieldCompat :: Name -> DataCon -> DataCon -> TyVarSet
1530 -> Type -> Type -> Type -> Type -> TcM ()
1531 checkFieldCompat fld con1 con2 tvs1 res1 res2 fty1 fty2
1532 = do { checkTc (isJust mb_subst1) (resultTypeMisMatch fld con1 con2)
1533 ; checkTc (isJust mb_subst2) (fieldTypeMisMatch fld con1 con2) }
1534 where
1535 mb_subst1 = tcMatchTy tvs1 res1 res2
1536 mb_subst2 = tcMatchTyX tvs1 (expectJust "checkFieldCompat" mb_subst1) fty1 fty2
1537
1538 -------------------------------
1539 checkValidDataCon :: DynFlags -> Bool -> TyCon -> DataCon -> TcM ()
1540 checkValidDataCon dflags existential_ok tc con
1541 = setSrcSpan (srcLocSpan (getSrcLoc con)) $
1542 addErrCtxt (dataConCtxt con) $
1543 do { -- Check that the return type of the data constructor
1544 -- matches the type constructor; eg reject this:
1545 -- data T a where { MkT :: Bogus a }
1546 -- c.f. Note [Check role annotations in a second pass]
1547 -- and Note [Checking GADT return types]
1548 let tc_tvs = tyConTyVars tc
1549 res_ty_tmpl = mkFamilyTyConApp tc (mkTyVarTys tc_tvs)
1550 orig_res_ty = dataConOrigResTy con
1551 ; traceTc "checkValidDataCon" (vcat
1552 [ ppr con, ppr tc, ppr tc_tvs
1553 , ppr res_ty_tmpl <+> dcolon <+> ppr (typeKind res_ty_tmpl)
1554 , ppr orig_res_ty <+> dcolon <+> ppr (typeKind orig_res_ty)])
1555
1556 ; checkTc (isJust (tcMatchTy (mkVarSet tc_tvs)
1557 res_ty_tmpl
1558 orig_res_ty))
1559 (badDataConTyCon con res_ty_tmpl orig_res_ty)
1560
1561 -- Check that the result type is a *monotype*
1562 -- e.g. reject this: MkT :: T (forall a. a->a)
1563 -- Reason: it's really the argument of an equality constraint
1564 ; checkValidMonoType orig_res_ty
1565
1566 -- Check all argument types for validity
1567 ; checkValidType ctxt (dataConUserType con)
1568
1569 -- Extra checks for newtype data constructors
1570 ; when (isNewTyCon tc) (checkNewDataCon con)
1571
1572 -- Check that UNPACK pragmas and bangs work out
1573 -- E.g. reject data T = MkT {-# UNPACK #-} Int -- No "!"
1574 -- data T = MkT {-# UNPACK #-} !a -- Can't unpack
1575 ; mapM_ check_bang (zip3 (dataConStrictMarks con) (dataConRepBangs con) [1..])
1576
1577 -- Check that existentials are allowed if they are used
1578 ; checkTc (existential_ok || isVanillaDataCon con)
1579 (badExistential con)
1580
1581 -- Check that we aren't doing GADT type refinement on kind variables
1582 -- e.g reject data T (a::k) where
1583 -- T1 :: T Int
1584 -- T2 :: T Maybe
1585 ; checkTc (not (any (isKindVar . fst) (dataConEqSpec con)))
1586 (badGadtKindCon con)
1587
1588 ; traceTc "Done validity of data con" (ppr con <+> ppr (dataConRepType con))
1589 }
1590 where
1591 ctxt = ConArgCtxt (dataConName con)
1592 check_bang (HsUserBang (Just want_unpack) has_bang, rep_bang, n)
1593 | want_unpack, not has_bang
1594 = addWarnTc (bad_bang n (ptext (sLit "UNPACK pragma lacks '!'")))
1595 | want_unpack
1596 , case rep_bang of { HsUnpack {} -> False; _ -> True }
1597 , not (gopt Opt_OmitInterfacePragmas dflags)
1598 -- If not optimising, se don't unpack, so don't complain!
1599 -- See MkId.dataConArgRep, the (HsBang True) case
1600 = addWarnTc (bad_bang n (ptext (sLit "Ignoring unusable UNPACK pragma")))
1601
1602 check_bang _
1603 = return ()
1604
1605 bad_bang n herald
1606 = hang herald 2 (ptext (sLit "on the") <+> speakNth n
1607 <+> ptext (sLit "argument of") <+> quotes (ppr con))
1608 -------------------------------
1609 checkNewDataCon :: DataCon -> TcM ()
1610 -- Further checks for the data constructor of a newtype
1611 checkNewDataCon con
1612 = do { checkTc (isSingleton arg_tys) (newtypeFieldErr con (length arg_tys))
1613 -- One argument
1614
1615 ; check_con (null eq_spec) $
1616 ptext (sLit "A newtype constructor must have a return type of form T a1 ... an")
1617 -- Return type is (T a b c)
1618
1619 ; check_con (null theta) $
1620 ptext (sLit "A newtype constructor cannot have a context in its type")
1621
1622 ; check_con (null ex_tvs) $
1623 ptext (sLit "A newtype constructor cannot have existential type variables")
1624 -- No existentials
1625
1626 ; checkTc (not (any isBanged (dataConStrictMarks con)))
1627 (newtypeStrictError con)
1628 -- No strictness
1629 }
1630 where
1631 (_univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig con
1632 check_con what msg
1633 = checkTc what (msg $$ ppr con <+> dcolon <+> ppr (dataConUserType con))
1634
1635 -------------------------------
1636 checkValidClass :: Class -> TcM ()
1637 checkValidClass cls
1638 = do { constrained_class_methods <- xoptM Opt_ConstrainedClassMethods
1639 ; multi_param_type_classes <- xoptM Opt_MultiParamTypeClasses
1640 ; nullary_type_classes <- xoptM Opt_NullaryTypeClasses
1641 ; fundep_classes <- xoptM Opt_FunctionalDependencies
1642
1643 -- Check that the class is unary, unless multiparameter type classes
1644 -- are enabled; also recognize deprecated nullary type classes
1645 -- extension (subsumed by multiparameter type classes, Trac #8993)
1646 ; checkTc (multi_param_type_classes || arity == 1 ||
1647 (nullary_type_classes && arity == 0))
1648 (classArityErr arity cls)
1649 ; checkTc (fundep_classes || null fundeps) (classFunDepsErr cls)
1650
1651 -- Check the super-classes
1652 ; checkValidTheta (ClassSCCtxt (className cls)) theta
1653
1654 -- Now check for cyclic superclasses
1655 -- If there are superclass cycles, checkClassCycleErrs bails.
1656 ; checkClassCycleErrs cls
1657
1658 -- Check the class operations.
1659 -- But only if there have been no earlier errors
1660 -- See Note [Abort when superclass cycle is detected]
1661 ; whenNoErrs $
1662 mapM_ (check_op constrained_class_methods) op_stuff
1663
1664 -- Check the associated type defaults are well-formed and instantiated
1665 ; mapM_ check_at_defs at_stuff }
1666 where
1667 (tyvars, fundeps, theta, _, at_stuff, op_stuff) = classExtraBigSig cls
1668 arity = count isTypeVar tyvars -- Ignore kind variables
1669
1670 check_op constrained_class_methods (sel_id, dm)
1671 = addErrCtxt (classOpCtxt sel_id tau) $ do
1672 { checkValidTheta ctxt (tail theta)
1673 -- The 'tail' removes the initial (C a) from the
1674 -- class itself, leaving just the method type
1675
1676 ; traceTc "class op type" (ppr op_ty <+> ppr tau)
1677 ; checkValidType ctxt tau
1678
1679 -- Check that the type mentions at least one of
1680 -- the class type variables...or at least one reachable
1681 -- from one of the class variables. Example: tc223
1682 -- class Error e => Game b mv e | b -> mv e where
1683 -- newBoard :: MonadState b m => m ()
1684 -- Here, MonadState has a fundep m->b, so newBoard is fine
1685 -- The check is disabled for nullary type classes,
1686 -- since there is no possible ambiguity
1687 ; let grown_tyvars = growThetaTyVars theta (mkVarSet tyvars)
1688 ; checkTc (arity == 0 || tyVarsOfType tau `intersectsVarSet` grown_tyvars)
1689 (noClassTyVarErr cls (ptext (sLit "class method") <+> quotes (ppr sel_id)))
1690
1691 ; case dm of
1692 GenDefMeth dm_name -> do { dm_id <- tcLookupId dm_name
1693 ; checkValidType ctxt (idType dm_id) }
1694 _ -> return ()
1695 }
1696 where
1697 ctxt = FunSigCtxt op_name True -- Report redundant class constraints
1698 op_name = idName sel_id
1699 op_ty = idType sel_id
1700 (_,theta1,tau1) = tcSplitSigmaTy op_ty
1701 (_,theta2,tau2) = tcSplitSigmaTy tau1
1702 (theta,tau) | constrained_class_methods = (theta1 ++ theta2, tau2)
1703 | otherwise = (theta1, mkPhiTy (tail theta1) tau1)
1704 -- Ugh! The function might have a type like
1705 -- op :: forall a. C a => forall b. (Eq b, Eq a) => tau2
1706 -- With -XConstrainedClassMethods, we want to allow this, even though the inner
1707 -- forall has an (Eq a) constraint. Whereas in general, each constraint
1708 -- in the context of a for-all must mention at least one quantified
1709 -- type variable. What a mess!
1710
1711 check_at_defs (ATI fam_tc _)
1712 = do { traceTc "check-at" (ppr fam_tc $$ ppr (tyConTyVars fam_tc) $$ ppr tyvars)
1713 ; checkTc (any (`elem` tyvars) (tyConTyVars fam_tc))
1714 (noClassTyVarErr cls (ptext (sLit "associated type") <+> quotes (ppr fam_tc))) }
1715
1716 checkFamFlag :: Name -> TcM ()
1717 -- Check that we don't use families without -XTypeFamilies
1718 -- The parser won't even parse them, but I suppose a GHC API
1719 -- client might have a go!
1720 checkFamFlag tc_name
1721 = do { idx_tys <- xoptM Opt_TypeFamilies
1722 ; checkTc idx_tys err_msg }
1723 where
1724 err_msg = hang (ptext (sLit "Illegal family declaration for") <+> quotes (ppr tc_name))
1725 2 (ptext (sLit "Use TypeFamilies to allow indexed type families"))
1726
1727 {-
1728 Note [Abort when superclass cycle is detected]
1729 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1730 We must avoid doing the ambiguity check for the methods (in
1731 checkValidClass.check_op) when there are already errors accumulated.
1732 This is because one of the errors may be a superclass cycle, and
1733 superclass cycles cause canonicalization to loop. Here is a
1734 representative example:
1735
1736 class D a => C a where
1737 meth :: D a => ()
1738 class C a => D a
1739
1740 This fixes Trac #9415, #9739
1741
1742 ************************************************************************
1743 * *
1744 Checking role validity
1745 * *
1746 ************************************************************************
1747 -}
1748
1749 checkValidRoleAnnots :: RoleAnnots -> TyThing -> TcM ()
1750 checkValidRoleAnnots role_annots thing
1751 = case thing of
1752 { ATyCon tc
1753 | isTypeSynonymTyCon tc -> check_no_roles
1754 | isFamilyTyCon tc -> check_no_roles
1755 | isAlgTyCon tc -> check_roles
1756 where
1757 name = tyConName tc
1758
1759 -- Role annotations are given only on *type* variables, but a tycon stores
1760 -- roles for all variables. So, we drop the kind roles (which are all
1761 -- Nominal, anyway).
1762 tyvars = tyConTyVars tc
1763 roles = tyConRoles tc
1764 (kind_vars, type_vars) = span isKindVar tyvars
1765 type_roles = dropList kind_vars roles
1766 role_annot_decl_maybe = lookupRoleAnnots role_annots name
1767
1768 check_roles
1769 = whenIsJust role_annot_decl_maybe $
1770 \decl@(L loc (RoleAnnotDecl _ the_role_annots)) ->
1771 addRoleAnnotCtxt name $
1772 setSrcSpan loc $ do
1773 { role_annots_ok <- xoptM Opt_RoleAnnotations
1774 ; checkTc role_annots_ok $ needXRoleAnnotations tc
1775 ; checkTc (type_vars `equalLength` the_role_annots)
1776 (wrongNumberOfRoles type_vars decl)
1777 ; _ <- zipWith3M checkRoleAnnot type_vars the_role_annots type_roles
1778 -- Representational or phantom roles for class parameters
1779 -- quickly lead to incoherence. So, we require
1780 -- IncoherentInstances to have them. See #8773.
1781 ; incoherent_roles_ok <- xoptM Opt_IncoherentInstances
1782 ; checkTc ( incoherent_roles_ok
1783 || (not $ isClassTyCon tc)
1784 || (all (== Nominal) type_roles))
1785 incoherentRoles
1786
1787 ; lint <- goptM Opt_DoCoreLinting
1788 ; when lint $ checkValidRoles tc }
1789
1790 check_no_roles
1791 = whenIsJust role_annot_decl_maybe illegalRoleAnnotDecl
1792 ; _ -> return () }
1793
1794 checkRoleAnnot :: TyVar -> Located (Maybe Role) -> Role -> TcM ()
1795 checkRoleAnnot _ (L _ Nothing) _ = return ()
1796 checkRoleAnnot tv (L _ (Just r1)) r2
1797 = when (r1 /= r2) $
1798 addErrTc $ badRoleAnnot (tyVarName tv) r1 r2
1799
1800 -- This is a double-check on the role inference algorithm. It is only run when
1801 -- -dcore-lint is enabled. See Note [Role inference] in TcTyDecls
1802 checkValidRoles :: TyCon -> TcM ()
1803 -- If you edit this function, you may need to update the GHC formalism
1804 -- See Note [GHC Formalism] in CoreLint
1805 checkValidRoles tc
1806 | isAlgTyCon tc
1807 -- tyConDataCons returns an empty list for data families
1808 = mapM_ check_dc_roles (tyConDataCons tc)
1809 | Just rhs <- synTyConRhs_maybe tc
1810 = check_ty_roles (zipVarEnv (tyConTyVars tc) (tyConRoles tc)) Representational rhs
1811 | otherwise
1812 = return ()
1813 where
1814 check_dc_roles datacon
1815 = do { traceTc "check_dc_roles" (ppr datacon <+> ppr (tyConRoles tc))
1816 ; mapM_ (check_ty_roles role_env Representational) $
1817 eqSpecPreds eq_spec ++ theta ++ arg_tys }
1818 -- See Note [Role-checking data constructor arguments] in TcTyDecls
1819 where
1820 (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig datacon
1821 univ_roles = zipVarEnv univ_tvs (tyConRoles tc)
1822 -- zipVarEnv uses zipEqual, but we don't want that for ex_tvs
1823 ex_roles = mkVarEnv (zip ex_tvs (repeat Nominal))
1824 role_env = univ_roles `plusVarEnv` ex_roles
1825
1826 check_ty_roles env role (TyVarTy tv)
1827 = case lookupVarEnv env tv of
1828 Just role' -> unless (role' `ltRole` role || role' == role) $
1829 report_error $ ptext (sLit "type variable") <+> quotes (ppr tv) <+>
1830 ptext (sLit "cannot have role") <+> ppr role <+>
1831 ptext (sLit "because it was assigned role") <+> ppr role'
1832 Nothing -> report_error $ ptext (sLit "type variable") <+> quotes (ppr tv) <+>
1833 ptext (sLit "missing in environment")
1834
1835 check_ty_roles env Representational (TyConApp tc tys)
1836 = let roles' = tyConRoles tc in
1837 zipWithM_ (maybe_check_ty_roles env) roles' tys
1838
1839 check_ty_roles env Nominal (TyConApp _ tys)
1840 = mapM_ (check_ty_roles env Nominal) tys
1841
1842 check_ty_roles _ Phantom ty@(TyConApp {})
1843 = pprPanic "check_ty_roles" (ppr ty)
1844
1845 check_ty_roles env role (AppTy ty1 ty2)
1846 = check_ty_roles env role ty1
1847 >> check_ty_roles env Nominal ty2
1848
1849 check_ty_roles env role (FunTy ty1 ty2)
1850 = check_ty_roles env role ty1
1851 >> check_ty_roles env role ty2
1852
1853 check_ty_roles env role (ForAllTy tv ty)
1854 = check_ty_roles (extendVarEnv env tv Nominal) role ty
1855
1856 check_ty_roles _ _ (LitTy {}) = return ()
1857
1858 maybe_check_ty_roles env role ty
1859 = when (role == Nominal || role == Representational) $
1860 check_ty_roles env role ty
1861
1862 report_error doc
1863 = addErrTc $ vcat [ptext (sLit "Internal error in role inference:"),
1864 doc,
1865 ptext (sLit "Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug")]
1866
1867 {-
1868 ************************************************************************
1869 * *
1870 Building record selectors
1871 * *
1872 ************************************************************************
1873 -}
1874
1875 mkDefaultMethodIds :: [TyThing] -> [Id]
1876 -- See Note [Default method Ids and Template Haskell]
1877 mkDefaultMethodIds things
1878 = [ mkExportedLocalId VanillaId dm_name (idType sel_id)
1879 | ATyCon tc <- things
1880 , Just cls <- [tyConClass_maybe tc]
1881 , (sel_id, DefMeth dm_name) <- classOpItems cls ]
1882
1883 {-
1884 Note [Default method Ids and Template Haskell]
1885 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1886 Consider this (Trac #4169):
1887 class Numeric a where
1888 fromIntegerNum :: a
1889 fromIntegerNum = ...
1890
1891 ast :: Q [Dec]
1892 ast = [d| instance Numeric Int |]
1893
1894 When we typecheck 'ast' we have done the first pass over the class decl
1895 (in tcTyClDecls), but we have not yet typechecked the default-method
1896 declarations (because they can mention value declarations). So we
1897 must bring the default method Ids into scope first (so they can be seen
1898 when typechecking the [d| .. |] quote, and typecheck them later.
1899 -}
1900
1901 mkRecSelBinds :: [TyThing] -> HsValBinds Name
1902 -- NB We produce *un-typechecked* bindings, rather like 'deriving'
1903 -- This makes life easier, because the later type checking will add
1904 -- all necessary type abstractions and applications
1905 mkRecSelBinds tycons
1906 = ValBindsOut [(NonRecursive, b) | b <- binds] sigs
1907 where
1908 (sigs, binds) = unzip rec_sels
1909 rec_sels = map mkRecSelBind [ (tc,fld)
1910 | ATyCon tc <- tycons
1911 , fld <- tyConFields tc ]
1912
1913 mkRecSelBind :: (TyCon, FieldLabel) -> (LSig Name, LHsBinds Name)
1914 mkRecSelBind (tycon, sel_name)
1915 = (L loc (IdSig sel_id), unitBag (L loc sel_bind))
1916 where
1917 loc = getSrcSpan sel_name
1918 sel_id = mkExportedLocalId rec_details sel_name sel_ty
1919 rec_details = RecSelId { sel_tycon = tycon, sel_naughty = is_naughty }
1920
1921 -- Find a representative constructor, con1
1922 all_cons = tyConDataCons tycon
1923 cons_w_field = [ con | con <- all_cons
1924 , sel_name `elem` dataConFieldLabels con ]
1925 con1 = ASSERT( not (null cons_w_field) ) head cons_w_field
1926
1927 -- Selector type; Note [Polymorphic selectors]
1928 field_ty = dataConFieldType con1 sel_name
1929 data_ty = dataConOrigResTy con1
1930 data_tvs = tyVarsOfType data_ty
1931 is_naughty = not (tyVarsOfType field_ty `subVarSet` data_tvs)
1932 (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty
1933 sel_ty | is_naughty = unitTy -- See Note [Naughty record selectors]
1934 | otherwise = mkForAllTys (varSetElemsKvsFirst $
1935 data_tvs `extendVarSetList` field_tvs) $
1936 mkPhiTy (dataConStupidTheta con1) $ -- Urgh!
1937 mkPhiTy field_theta $ -- Urgh!
1938 mkFunTy data_ty field_tau
1939
1940 -- Make the binding: sel (C2 { fld = x }) = x
1941 -- sel (C7 { fld = x }) = x
1942 -- where cons_w_field = [C2,C7]
1943 sel_bind = mkTopFunBind Generated sel_lname alts
1944 where
1945 alts | is_naughty = [mkSimpleMatch [] unit_rhs]
1946 | otherwise = map mk_match cons_w_field ++ deflt
1947 mk_match con = mkSimpleMatch [L loc (mk_sel_pat con)]
1948 (L loc (HsVar field_var))
1949 mk_sel_pat con = ConPatIn (L loc (getName con)) (RecCon rec_fields)
1950 rec_fields = HsRecFields { rec_flds = [rec_field], rec_dotdot = Nothing }
1951 rec_field = noLoc (HsRecField { hsRecFieldId = sel_lname
1952 , hsRecFieldArg = L loc (VarPat field_var)
1953 , hsRecPun = False })
1954 sel_lname = L loc sel_name
1955 field_var = mkInternalName (mkBuiltinUnique 1) (getOccName sel_name) loc
1956
1957 -- Add catch-all default case unless the case is exhaustive
1958 -- We do this explicitly so that we get a nice error message that
1959 -- mentions this particular record selector
1960 deflt | all dealt_with all_cons = []
1961 | otherwise = [mkSimpleMatch [L loc (WildPat placeHolderType)]
1962 (mkHsApp (L loc (HsVar (getName rEC_SEL_ERROR_ID)))
1963 (L loc (HsLit msg_lit)))]
1964
1965 -- Do not add a default case unless there are unmatched
1966 -- constructors. We must take account of GADTs, else we
1967 -- get overlap warning messages from the pattern-match checker
1968 -- NB: we need to pass type args for the *representation* TyCon
1969 -- to dataConCannotMatch, hence the calculation of inst_tys
1970 -- This matters in data families
1971 -- data instance T Int a where
1972 -- A :: { fld :: Int } -> T Int Bool
1973 -- B :: { fld :: Int } -> T Int Char
1974 dealt_with con = con `elem` cons_w_field || dataConCannotMatch inst_tys con
1975 inst_tys = substTyVars (mkTopTvSubst (dataConEqSpec con1)) (dataConUnivTyVars con1)
1976
1977 unit_rhs = mkLHsTupleExpr []
1978 msg_lit = HsStringPrim "" $ unsafeMkByteString $
1979 occNameString (getOccName sel_name)
1980
1981 ---------------
1982 tyConFields :: TyCon -> [FieldLabel]
1983 tyConFields tc
1984 | isAlgTyCon tc = nub (concatMap dataConFieldLabels (tyConDataCons tc))
1985 | otherwise = []
1986
1987 {-
1988 Note [Polymorphic selectors]
1989 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1990 When a record has a polymorphic field, we pull the foralls out to the front.
1991 data T = MkT { f :: forall a. [a] -> a }
1992 Then f :: forall a. T -> [a] -> a
1993 NOT f :: T -> forall a. [a] -> a
1994
1995 This is horrid. It's only needed in deeply obscure cases, which I hate.
1996 The only case I know is test tc163, which is worth looking at. It's far
1997 from clear that this test should succeed at all!
1998
1999 Note [Naughty record selectors]
2000 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2001 A "naughty" field is one for which we can't define a record
2002 selector, because an existential type variable would escape. For example:
2003 data T = forall a. MkT { x,y::a }
2004 We obviously can't define
2005 x (MkT v _) = v
2006 Nevertheless we *do* put a RecSelId into the type environment
2007 so that if the user tries to use 'x' as a selector we can bleat
2008 helpfully, rather than saying unhelpfully that 'x' is not in scope.
2009 Hence the sel_naughty flag, to identify record selectors that don't really exist.
2010
2011 In general, a field is "naughty" if its type mentions a type variable that
2012 isn't in the result type of the constructor. Note that this *allows*
2013 GADT record selectors (Note [GADT record selectors]) whose types may look
2014 like sel :: T [a] -> a
2015
2016 For naughty selectors we make a dummy binding
2017 sel = ()
2018 for naughty selectors, so that the later type-check will add them to the
2019 environment, and they'll be exported. The function is never called, because
2020 the tyepchecker spots the sel_naughty field.
2021
2022 Note [GADT record selectors]
2023 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2024 For GADTs, we require that all constructors with a common field 'f' have the same
2025 result type (modulo alpha conversion). [Checked in TcTyClsDecls.checkValidTyCon]
2026 E.g.
2027 data T where
2028 T1 { f :: Maybe a } :: T [a]
2029 T2 { f :: Maybe a, y :: b } :: T [a]
2030 T3 :: T Int
2031
2032 and now the selector takes that result type as its argument:
2033 f :: forall a. T [a] -> Maybe a
2034
2035 Details: the "real" types of T1,T2 are:
2036 T1 :: forall r a. (r~[a]) => a -> T r
2037 T2 :: forall r a b. (r~[a]) => a -> b -> T r
2038
2039 So the selector loooks like this:
2040 f :: forall a. T [a] -> Maybe a
2041 f (a:*) (t:T [a])
2042 = case t of
2043 T1 c (g:[a]~[c]) (v:Maybe c) -> v `cast` Maybe (right (sym g))
2044 T2 c d (g:[a]~[c]) (v:Maybe c) (w:d) -> v `cast` Maybe (right (sym g))
2045 T3 -> error "T3 does not have field f"
2046
2047 Note the forall'd tyvars of the selector are just the free tyvars
2048 of the result type; there may be other tyvars in the constructor's
2049 type (e.g. 'b' in T2).
2050
2051 Note the need for casts in the result!
2052
2053 Note [Selector running example]
2054 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2055 It's OK to combine GADTs and type families. Here's a running example:
2056
2057 data instance T [a] where
2058 T1 { fld :: b } :: T [Maybe b]
2059
2060 The representation type looks like this
2061 data :R7T a where
2062 T1 { fld :: b } :: :R7T (Maybe b)
2063
2064 and there's coercion from the family type to the representation type
2065 :CoR7T a :: T [a] ~ :R7T a
2066
2067 The selector we want for fld looks like this:
2068
2069 fld :: forall b. T [Maybe b] -> b
2070 fld = /\b. \(d::T [Maybe b]).
2071 case d `cast` :CoR7T (Maybe b) of
2072 T1 (x::b) -> x
2073
2074 The scrutinee of the case has type :R7T (Maybe b), which can be
2075 gotten by appying the eq_spec to the univ_tvs of the data con.
2076
2077 ************************************************************************
2078 * *
2079 Error messages
2080 * *
2081 ************************************************************************
2082 -}
2083
2084 tcAddTyFamInstCtxt :: TyFamInstDecl Name -> TcM a -> TcM a
2085 tcAddTyFamInstCtxt decl
2086 = tcAddFamInstCtxt (ptext (sLit "type instance")) (tyFamInstDeclName decl)
2087
2088 tcAddDataFamInstCtxt :: DataFamInstDecl Name -> TcM a -> TcM a
2089 tcAddDataFamInstCtxt decl
2090 = tcAddFamInstCtxt (pprDataFamInstFlavour decl <+> ptext (sLit "instance"))
2091 (unLoc (dfid_tycon decl))
2092
2093 tcAddFamInstCtxt :: SDoc -> Name -> TcM a -> TcM a
2094 tcAddFamInstCtxt flavour tycon thing_inside
2095 = addErrCtxt ctxt thing_inside
2096 where
2097 ctxt = hsep [ptext (sLit "In the") <+> flavour
2098 <+> ptext (sLit "declaration for"),
2099 quotes (ppr tycon)]
2100
2101 tcAddClosedTypeFamilyDeclCtxt :: TyCon -> TcM a -> TcM a
2102 tcAddClosedTypeFamilyDeclCtxt tc
2103 = addErrCtxt ctxt
2104 where
2105 ctxt = ptext (sLit "In the equations for closed type family") <+>
2106 quotes (ppr tc)
2107
2108 resultTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc
2109 resultTypeMisMatch field_name con1 con2
2110 = vcat [sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2,
2111 ptext (sLit "have a common field") <+> quotes (ppr field_name) <> comma],
2112 nest 2 $ ptext (sLit "but have different result types")]
2113
2114 fieldTypeMisMatch :: Name -> DataCon -> DataCon -> SDoc
2115 fieldTypeMisMatch field_name con1 con2
2116 = sep [ptext (sLit "Constructors") <+> ppr con1 <+> ptext (sLit "and") <+> ppr con2,
2117 ptext (sLit "give different types for field"), quotes (ppr field_name)]
2118
2119 dataConCtxtName :: [Located Name] -> SDoc
2120 dataConCtxtName [con]
2121 = ptext (sLit "In the definition of data constructor") <+> quotes (ppr con)
2122 dataConCtxtName con
2123 = ptext (sLit "In the definition of data constructors") <+> interpp'SP con
2124
2125 dataConCtxt :: Outputable a => a -> SDoc
2126 dataConCtxt con = ptext (sLit "In the definition of data constructor") <+> quotes (ppr con)
2127
2128 classOpCtxt :: Var -> Type -> SDoc
2129 classOpCtxt sel_id tau = sep [ptext (sLit "When checking the class method:"),
2130 nest 2 (pprPrefixOcc sel_id <+> dcolon <+> ppr tau)]
2131
2132 classArityErr :: Int -> Class -> SDoc
2133 classArityErr n cls
2134 | n == 0 = mkErr "No" "no-parameter"
2135 | otherwise = mkErr "Too many" "multi-parameter"
2136 where
2137 mkErr howMany allowWhat =
2138 vcat [ptext (sLit $ howMany ++ " parameters for class") <+> quotes (ppr cls),
2139 parens (ptext (sLit $ "Use MultiParamTypeClasses to allow "
2140 ++ allowWhat ++ " classes"))]
2141
2142 classFunDepsErr :: Class -> SDoc
2143 classFunDepsErr cls
2144 = vcat [ptext (sLit "Fundeps in class") <+> quotes (ppr cls),
2145 parens (ptext (sLit "Use FunctionalDependencies to allow fundeps"))]
2146
2147 noClassTyVarErr :: Class -> SDoc -> SDoc
2148 noClassTyVarErr clas what
2149 = sep [ptext (sLit "The") <+> what,
2150 ptext (sLit "mentions none of the type or kind variables of the class") <+>
2151 quotes (ppr clas <+> hsep (map ppr (classTyVars clas)))]
2152
2153 recSynErr :: [LTyClDecl Name] -> TcRn ()
2154 recSynErr syn_decls
2155 = setSrcSpan (getLoc (head sorted_decls)) $
2156 addErr (sep [ptext (sLit "Cycle in type synonym declarations:"),
2157 nest 2 (vcat (map ppr_decl sorted_decls))])
2158 where
2159 sorted_decls = sortLocated syn_decls
2160 ppr_decl (L loc decl) = ppr loc <> colon <+> ppr decl
2161
2162 recClsErr :: [TyCon] -> TcRn ()
2163 recClsErr cycles
2164 = addErr (sep [ptext (sLit "Cycle in class declaration (via superclasses):"),
2165 nest 2 (hsep (intersperse (text "->") (map ppr cycles)))])
2166
2167 badDataConTyCon :: DataCon -> Type -> Type -> SDoc
2168 badDataConTyCon data_con res_ty_tmpl actual_res_ty
2169 = hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con) <+>
2170 ptext (sLit "returns type") <+> quotes (ppr actual_res_ty))
2171 2 (ptext (sLit "instead of an instance of its parent type") <+> quotes (ppr res_ty_tmpl))
2172
2173 badGadtKindCon :: DataCon -> SDoc
2174 badGadtKindCon data_con
2175 = hang (ptext (sLit "Data constructor") <+> quotes (ppr data_con)
2176 <+> ptext (sLit "cannot be GADT-like in its *kind* arguments"))
2177 2 (ppr data_con <+> dcolon <+> ppr (dataConUserType data_con))
2178
2179 badGadtDecl :: Name -> SDoc
2180 badGadtDecl tc_name
2181 = vcat [ ptext (sLit "Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
2182 , nest 2 (parens $ ptext (sLit "Use GADTs to allow GADTs")) ]
2183
2184 badExistential :: DataCon -> SDoc
2185 badExistential con
2186 = hang (ptext (sLit "Data constructor") <+> quotes (ppr con) <+>
2187 ptext (sLit "has existential type variables, a context, or a specialised result type"))
2188 2 (vcat [ ppr con <+> dcolon <+> ppr (dataConUserType con)
2189 , parens $ ptext (sLit "Use ExistentialQuantification or GADTs to allow this") ])
2190
2191 badStupidTheta :: Name -> SDoc
2192 badStupidTheta tc_name
2193 = ptext (sLit "A data type declared in GADT style cannot have a context:") <+> quotes (ppr tc_name)
2194
2195 newtypeConError :: Name -> Int -> SDoc
2196 newtypeConError tycon n
2197 = sep [ptext (sLit "A newtype must have exactly one constructor,"),
2198 nest 2 $ ptext (sLit "but") <+> quotes (ppr tycon) <+> ptext (sLit "has") <+> speakN n ]
2199
2200 newtypeStrictError :: DataCon -> SDoc
2201 newtypeStrictError con
2202 = sep [ptext (sLit "A newtype constructor cannot have a strictness annotation,"),
2203 nest 2 $ ptext (sLit "but") <+> quotes (ppr con) <+> ptext (sLit "does")]
2204
2205 newtypeFieldErr :: DataCon -> Int -> SDoc
2206 newtypeFieldErr con_name n_flds
2207 = sep [ptext (sLit "The constructor of a newtype must have exactly one field"),
2208 nest 2 $ ptext (sLit "but") <+> quotes (ppr con_name) <+> ptext (sLit "has") <+> speakN n_flds]
2209
2210 badSigTyDecl :: Name -> SDoc
2211 badSigTyDecl tc_name
2212 = vcat [ ptext (sLit "Illegal kind signature") <+>
2213 quotes (ppr tc_name)
2214 , nest 2 (parens $ ptext (sLit "Use KindSignatures to allow kind signatures")) ]
2215
2216 emptyConDeclsErr :: Name -> SDoc
2217 emptyConDeclsErr tycon
2218 = sep [quotes (ppr tycon) <+> ptext (sLit "has no constructors"),
2219 nest 2 $ ptext (sLit "(EmptyDataDecls permits this)")]
2220
2221 wrongKindOfFamily :: TyCon -> SDoc
2222 wrongKindOfFamily family
2223 = ptext (sLit "Wrong category of family instance; declaration was for a")
2224 <+> kindOfFamily
2225 where
2226 kindOfFamily | isTypeFamilyTyCon family = text "type family"
2227 | isDataFamilyTyCon family = text "data family"
2228 | otherwise = pprPanic "wrongKindOfFamily" (ppr family)
2229
2230 wrongNumberOfParmsErr :: Arity -> SDoc
2231 wrongNumberOfParmsErr max_args
2232 = ptext (sLit "Number of parameters must match family declaration; expected")
2233 <+> ppr max_args
2234
2235 wrongTyFamName :: Name -> Name -> SDoc
2236 wrongTyFamName fam_tc_name eqn_tc_name
2237 = hang (ptext (sLit "Mismatched type name in type family instance."))
2238 2 (vcat [ ptext (sLit "Expected:") <+> ppr fam_tc_name
2239 , ptext (sLit " Actual:") <+> ppr eqn_tc_name ])
2240
2241 inaccessibleCoAxBranch :: TyCon -> CoAxBranch -> SDoc
2242 inaccessibleCoAxBranch tc fi
2243 = ptext (sLit "Overlapped type family instance equation:") $$
2244 (pprCoAxBranch tc fi)
2245
2246 badRoleAnnot :: Name -> Role -> Role -> SDoc
2247 badRoleAnnot var annot inferred
2248 = hang (ptext (sLit "Role mismatch on variable") <+> ppr var <> colon)
2249 2 (sep [ ptext (sLit "Annotation says"), ppr annot
2250 , ptext (sLit "but role"), ppr inferred
2251 , ptext (sLit "is required") ])
2252
2253 wrongNumberOfRoles :: [a] -> LRoleAnnotDecl Name -> SDoc
2254 wrongNumberOfRoles tyvars d@(L _ (RoleAnnotDecl _ annots))
2255 = hang (ptext (sLit "Wrong number of roles listed in role annotation;") $$
2256 ptext (sLit "Expected") <+> (ppr $ length tyvars) <> comma <+>
2257 ptext (sLit "got") <+> (ppr $ length annots) <> colon)
2258 2 (ppr d)
2259
2260 illegalRoleAnnotDecl :: LRoleAnnotDecl Name -> TcM ()
2261 illegalRoleAnnotDecl (L loc (RoleAnnotDecl tycon _))
2262 = setErrCtxt [] $
2263 setSrcSpan loc $
2264 addErrTc (ptext (sLit "Illegal role annotation for") <+> ppr tycon <> char ';' $$
2265 ptext (sLit "they are allowed only for datatypes and classes."))
2266
2267 needXRoleAnnotations :: TyCon -> SDoc
2268 needXRoleAnnotations tc
2269 = ptext (sLit "Illegal role annotation for") <+> ppr tc <> char ';' $$
2270 ptext (sLit "did you intend to use RoleAnnotations?")
2271
2272 incoherentRoles :: SDoc
2273 incoherentRoles = (text "Roles other than" <+> quotes (text "nominal") <+>
2274 text "for class parameters can lead to incoherence.") $$
2275 (text "Use IncoherentInstances to allow this; bad role found")
2276
2277 addTyThingCtxt :: TyThing -> TcM a -> TcM a
2278 addTyThingCtxt thing
2279 = addErrCtxt ctxt
2280 where
2281 name = getName thing
2282 flav = case thing of
2283 ATyCon tc
2284 | isClassTyCon tc -> ptext (sLit "class")
2285 | isTypeFamilyTyCon tc -> ptext (sLit "type family")
2286 | isDataFamilyTyCon tc -> ptext (sLit "data family")
2287 | isTypeSynonymTyCon tc -> ptext (sLit "type")
2288 | isNewTyCon tc -> ptext (sLit "newtype")
2289 | isDataTyCon tc -> ptext (sLit "data")
2290
2291 _ -> pprTrace "addTyThingCtxt strange" (ppr thing)
2292 Outputable.empty
2293
2294 ctxt = hsep [ ptext (sLit "In the"), flav
2295 , ptext (sLit "declaration for"), quotes (ppr name) ]
2296
2297 addRoleAnnotCtxt :: Name -> TcM a -> TcM a
2298 addRoleAnnotCtxt name
2299 = addErrCtxt $
2300 text "while checking a role annotation for" <+> quotes (ppr name)