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