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