2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
5 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
9 -- The above warning supression flag is a temporary kludge.
10 -- While working on this module you are encouraged to remove it and fix
11 -- any warnings in the module. See
12 -- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
16 tcHsSigType, tcHsDeriv,
17 tcHsInstHead, tcHsQuantifiedType,
21 kcHsTyVars, kcHsSigType, kcHsLiftedSigType,
22 kcCheckHsType, kcHsContext, kcHsType,
24 -- Typechecking kinded types
25 tcHsKindedContext, tcHsKindedType, tcHsBangType,
26 tcTyVarBndrs, dsHsType, tcLHsConResTy,
29 -- Pattern type signatures
30 tcHsPatSigType, tcPatSig
33 #include "HsVersions.h"
43 import {- Kind parts of -} Type
62 ----------------------------
64 ----------------------------
66 Generally speaking we now type-check types in three phases
68 1. kcHsType: kind check the HsType
69 *includes* performing any TH type splices;
70 so it returns a translated, and kind-annotated, type
72 2. dsHsType: convert from HsType to Type:
74 expand type synonyms [mkGenTyApps]
75 hoist the foralls [tcHsType]
77 3. checkValidType: check the validity of the resulting type
79 Often these steps are done one after the other (tcHsSigType).
80 But in mutually recursive groups of type and class decls we do
81 1 kind-check the whole group
82 2 build TyCons/Classes in a knot-tied way
83 3 check the validity of types in the now-unknotted TyCons/Classes
85 For example, when we find
86 (forall a m. m a -> m a)
87 we bind a,m to kind varibles and kind-check (m a -> m a). This makes
88 a get kind *, and m get kind *->*. Now we typecheck (m a -> m a) in
89 an environment that binds a and m suitably.
91 The kind checker passed to tcHsTyVars needs to look at enough to
92 establish the kind of the tyvar:
93 * For a group of type and class decls, it's just the group, not
94 the rest of the program
95 * For a tyvar bound in a pattern type signature, its the types
96 mentioned in the other type signatures in that bunch of patterns
97 * For a tyvar bound in a RULE, it's the type signatures on other
98 universally quantified variables in the rule
100 Note that this may occasionally give surprising results. For example:
102 data T a b = MkT (a b)
104 Here we deduce a::*->*, b::*
105 But equally valid would be a::(*->*)-> *, b::*->*
110 Some of the validity check could in principle be done by the kind checker,
113 - During desugaring, we normalise by expanding type synonyms. Only
114 after this step can we check things like type-synonym saturation
115 e.g. type T k = k Int
117 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
118 and then S is saturated. This is a GHC extension.
120 - Similarly, also a GHC extension, we look through synonyms before complaining
121 about the form of a class or instance declaration
123 - Ambiguity checks involve functional dependencies, and it's easier to wait
124 until knots have been resolved before poking into them
126 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
127 finished building the loop. So to keep things simple, we postpone most validity
128 checking until step (3).
132 During step (1) we might fault in a TyCon defined in another module, and it might
133 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
134 knot around type declarations with ARecThing, so that the fault-in code can get
135 the TyCon being defined.
138 %************************************************************************
140 \subsection{Checking types}
142 %************************************************************************
145 tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
146 -- Do kind checking, and hoist for-alls to the top
147 -- NB: it's important that the foralls that come from the top-level
148 -- HsForAllTy in hs_ty occur *first* in the returned type.
149 -- See Note [Scoped] with TcSigInfo
150 tcHsSigType ctxt hs_ty
151 = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
152 do { kinded_ty <- kcTypeType hs_ty
153 ; ty <- tcHsKindedType kinded_ty
154 ; checkValidType ctxt ty
157 tcHsInstHead :: LHsType Name -> TcM ([TyVar], ThetaType, Type)
158 -- Typecheck an instance head. We can't use
159 -- tcHsSigType, because it's not a valid user type.
161 = do { kinded_ty <- kcHsSigType hs_ty
162 ; poly_ty <- tcHsKindedType kinded_ty
163 ; return (tcSplitSigmaTy poly_ty) }
165 tcHsQuantifiedType :: [LHsTyVarBndr Name] -> LHsType Name -> TcM ([TyVar], Type)
166 -- Behave very like type-checking (HsForAllTy sig_tvs hs_ty),
167 -- except that we want to keep the tvs separate
168 tcHsQuantifiedType tv_names hs_ty
169 = kcHsTyVars tv_names $ \ tv_names' ->
170 do { kc_ty <- kcHsSigType hs_ty
171 ; tcTyVarBndrs tv_names' $ \ tvs ->
172 do { ty <- dsHsType kc_ty
173 ; return (tvs, ty) } }
175 -- Used for the deriving(...) items
176 tcHsDeriv :: LHsType Name -> TcM ([TyVar], Class, [Type])
177 tcHsDeriv = addLocM (tc_hs_deriv [])
179 tc_hs_deriv tv_names (HsPredTy (HsClassP cls_name hs_tys))
180 = kcHsTyVars tv_names $ \ tv_names' ->
181 do { cls_kind <- kcClass cls_name
182 ; (tys, res_kind) <- kcApps cls_kind (ppr cls_name) hs_tys
183 ; tcTyVarBndrs tv_names' $ \ tyvars ->
184 do { arg_tys <- dsHsTypes tys
185 ; cls <- tcLookupClass cls_name
186 ; return (tyvars, cls, arg_tys) }}
188 tc_hs_deriv tv_names1 (HsForAllTy _ tv_names2 (L _ []) (L _ ty))
189 = -- Funny newtype deriving form
191 -- where C has arity 2. Hence can't use regular functions
192 tc_hs_deriv (tv_names1 ++ tv_names2) ty
195 = failWithTc (ptext (sLit "Illegal deriving item") <+> ppr other)
198 These functions are used during knot-tying in
199 type and class declarations, when we have to
200 separate kind-checking, desugaring, and validity checking
203 kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
204 -- Used for type signatures
205 kcHsSigType ty = kcTypeType ty
206 kcHsLiftedSigType ty = kcLiftedType ty
208 tcHsKindedType :: LHsType Name -> TcM Type
209 -- Don't do kind checking, nor validity checking.
210 -- This is used in type and class decls, where kinding is
211 -- done in advance, and validity checking is done later
212 -- [Validity checking done later because of knot-tying issues.]
213 tcHsKindedType hs_ty = dsHsType hs_ty
215 tcHsBangType :: LHsType Name -> TcM Type
216 -- Permit a bang, but discard it
217 tcHsBangType (L span (HsBangTy b ty)) = tcHsKindedType ty
218 tcHsBangType ty = tcHsKindedType ty
220 tcHsKindedContext :: LHsContext Name -> TcM ThetaType
221 -- Used when we are expecting a ClassContext (i.e. no implicit params)
222 -- Does not do validity checking, like tcHsKindedType
223 tcHsKindedContext hs_theta = addLocM (mapM dsHsLPred) hs_theta
227 %************************************************************************
229 The main kind checker: kcHsType
231 %************************************************************************
233 First a couple of simple wrappers for kcHsType
236 ---------------------------
237 kcLiftedType :: LHsType Name -> TcM (LHsType Name)
238 -- The type ty must be a *lifted* *type*
239 kcLiftedType ty = kcCheckHsType ty liftedTypeKind
241 ---------------------------
242 kcTypeType :: LHsType Name -> TcM (LHsType Name)
243 -- The type ty must be a *type*, but it can be lifted or
244 -- unlifted or an unboxed tuple.
245 kcTypeType ty = kcCheckHsType ty openTypeKind
247 ---------------------------
248 kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
249 -- Check that the type has the specified kind
250 -- Be sure to use checkExpectedKind, rather than simply unifying
251 -- with OpenTypeKind, because it gives better error messages
252 kcCheckHsType (L span ty) exp_kind
254 do { (ty', act_kind) <- add_ctxt ty (kc_hs_type ty)
255 -- Add the context round the inner check only
256 -- because checkExpectedKind already mentions
257 -- 'ty' by name in any error message
259 ; checkExpectedKind (strip ty) act_kind exp_kind
260 ; return (L span ty') }
262 -- Wrap a context around only if we want to show that contexts.
263 add_ctxt (HsPredTy p) thing = thing
264 -- Omit invisble ones and ones user's won't grok (HsPred p).
265 add_ctxt (HsForAllTy _ _ (L _ []) _) thing = thing
266 -- Omit wrapping if the theta-part is empty
267 -- Reason: the recursive call to kcLiftedType, in the ForAllTy
268 -- case of kc_hs_type, will do the wrapping instead
269 -- and we don't want to duplicate
270 add_ctxt other_ty thing = addErrCtxt (typeCtxt other_ty) thing
272 -- We infer the kind of the type, and then complain if it's
273 -- not right. But we don't want to complain about
274 -- (ty) or !(ty) or forall a. ty
275 -- when the real difficulty is with the 'ty' part.
276 strip (HsParTy (L _ ty)) = strip ty
277 strip (HsBangTy _ (L _ ty)) = strip ty
278 strip (HsForAllTy _ _ _ (L _ ty)) = strip ty
282 Here comes the main function
285 kcHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
286 kcHsType ty = wrapLocFstM kc_hs_type ty
287 -- kcHsType *returns* the kind of the type, rather than taking an expected
288 -- kind as argument as tcExpr does.
290 -- (a) the kind of (->) is
291 -- forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
292 -- so we'd need to generate huge numbers of bx variables.
293 -- (b) kinds are so simple that the error messages are fine
295 -- The translated type has explicitly-kinded type-variable binders
297 kc_hs_type (HsParTy ty) = do
298 (ty', kind) <- kcHsType ty
299 return (HsParTy ty', kind)
301 kc_hs_type (HsTyVar name) = do
303 return (HsTyVar name, kind)
305 kc_hs_type (HsListTy ty) = do
306 ty' <- kcLiftedType ty
307 return (HsListTy ty', liftedTypeKind)
309 kc_hs_type (HsPArrTy ty) = do
310 ty' <- kcLiftedType ty
311 return (HsPArrTy ty', liftedTypeKind)
313 kc_hs_type (HsNumTy n)
314 = return (HsNumTy n, liftedTypeKind)
316 kc_hs_type (HsKindSig ty k) = do
317 ty' <- kcCheckHsType ty k
318 return (HsKindSig ty' k, k)
320 kc_hs_type (HsTupleTy Boxed tys) = do
321 tys' <- mapM kcLiftedType tys
322 return (HsTupleTy Boxed tys', liftedTypeKind)
324 kc_hs_type (HsTupleTy Unboxed tys) = do
325 tys' <- mapM kcTypeType tys
326 return (HsTupleTy Unboxed tys', ubxTupleKind)
328 kc_hs_type (HsFunTy ty1 ty2) = do
329 ty1' <- kcCheckHsType ty1 argTypeKind
330 ty2' <- kcTypeType ty2
331 return (HsFunTy ty1' ty2', liftedTypeKind)
333 kc_hs_type ty@(HsOpTy ty1 op ty2) = do
334 op_kind <- addLocM kcTyVar op
335 ([ty1',ty2'], res_kind) <- kcApps op_kind (ppr op) [ty1,ty2]
336 return (HsOpTy ty1' op ty2', res_kind)
338 kc_hs_type ty@(HsAppTy ty1 ty2) = do
339 (fun_ty', fun_kind) <- kcHsType fun_ty
340 ((arg_ty':arg_tys'), res_kind) <- kcApps fun_kind (ppr fun_ty) arg_tys
341 return (foldl mk_app (HsAppTy fun_ty' arg_ty') arg_tys', res_kind)
343 (fun_ty, arg_tys) = split ty1 [ty2]
344 split (L _ (HsAppTy f a)) as = split f (a:as)
346 mk_app fun arg = HsAppTy (noLoc fun) arg -- Add noLocs for inner nodes of
347 -- the application; they are
350 kc_hs_type ty@(HsPredTy (HsEqualP _ _))
353 kc_hs_type (HsPredTy pred) = do
354 pred' <- kcHsPred pred
355 return (HsPredTy pred', liftedTypeKind)
357 kc_hs_type (HsForAllTy exp tv_names context ty)
358 = kcHsTyVars tv_names $ \ tv_names' ->
359 do { ctxt' <- kcHsContext context
360 ; ty' <- kcLiftedType ty
361 -- The body of a forall is usually a type, but in principle
362 -- there's no reason to prohibit *unlifted* types.
363 -- In fact, GHC can itself construct a function with an
364 -- unboxed tuple inside a for-all (via CPR analyis; see
365 -- typecheck/should_compile/tc170)
367 -- Still, that's only for internal interfaces, which aren't
368 -- kind-checked, so we only allow liftedTypeKind here
370 ; return (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind) }
372 kc_hs_type (HsBangTy b ty) = do
373 (ty', kind) <- kcHsType ty
374 return (HsBangTy b ty', kind)
376 kc_hs_type ty@(HsSpliceTy _)
377 = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
379 -- remove the doc nodes here, no need to worry about the location since
380 -- its the same for a doc node and it's child type node
381 kc_hs_type (HsDocTy ty _)
382 = kc_hs_type (unLoc ty)
384 ---------------------------
385 kcApps :: TcKind -- Function kind
387 -> [LHsType Name] -- Arg types
388 -> TcM ([LHsType Name], TcKind) -- Kind-checked args
389 kcApps fun_kind ppr_fun args = do
390 (arg_kinds, res_kind) <- split_fk fun_kind (length args)
391 args' <- zipWithM kc_arg args arg_kinds
392 return (args', res_kind)
394 split_fk fk 0 = return ([], fk)
395 split_fk fk n = do mb_fk <- unifyFunKind fk
397 Nothing -> failWithTc too_many_args
398 Just (ak,fk') -> do (aks, rk) <- split_fk fk' (n-1)
401 kc_arg arg arg_kind = kcCheckHsType arg arg_kind
403 too_many_args = ptext (sLit "Kind error:") <+> quotes ppr_fun <+>
404 ptext (sLit "is applied to too many type arguments")
406 ---------------------------
407 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
408 kcHsContext ctxt = wrapLocM (mapM kcHsLPred) ctxt
410 kcHsLPred :: LHsPred Name -> TcM (LHsPred Name)
411 kcHsLPred = wrapLocM kcHsPred
413 kcHsPred :: HsPred Name -> TcM (HsPred Name)
414 kcHsPred pred = do -- Checks that the result is of kind liftedType
415 (pred', kind) <- kc_pred pred
416 checkExpectedKind pred kind liftedTypeKind
419 ---------------------------
420 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
421 -- Does *not* check for a saturated
422 -- application (reason: used from TcDeriv)
423 kc_pred pred@(HsIParam name ty)
424 = do { (ty', kind) <- kcHsType ty
425 ; return (HsIParam name ty', kind)
427 kc_pred pred@(HsClassP cls tys)
428 = do { kind <- kcClass cls
429 ; (tys', res_kind) <- kcApps kind (ppr cls) tys
430 ; return (HsClassP cls tys', res_kind)
432 kc_pred pred@(HsEqualP ty1 ty2)
433 = do { (ty1', kind1) <- kcHsType ty1
434 -- ; checkExpectedKind ty1 kind1 liftedTypeKind
435 ; (ty2', kind2) <- kcHsType ty2
436 -- ; checkExpectedKind ty2 kind2 liftedTypeKind
437 ; checkExpectedKind ty2 kind2 kind1
438 ; return (HsEqualP ty1' ty2', liftedTypeKind)
441 ---------------------------
442 kcTyVar :: Name -> TcM TcKind
443 kcTyVar name = do -- Could be a tyvar or a tycon
444 traceTc (text "lk1" <+> ppr name)
445 thing <- tcLookup name
446 traceTc (text "lk2" <+> ppr name <+> ppr thing)
448 ATyVar _ ty -> return (typeKind ty)
449 AThing kind -> return kind
450 AGlobal (ATyCon tc) -> return (tyConKind tc)
451 other -> wrongThingErr "type" thing name
453 kcClass :: Name -> TcM TcKind
454 kcClass cls = do -- Must be a class
455 thing <- tcLookup cls
457 AThing kind -> return kind
458 AGlobal (AClass cls) -> return (tyConKind (classTyCon cls))
459 other -> wrongThingErr "class" thing cls
463 %************************************************************************
467 %************************************************************************
471 * Transforms from HsType to Type
474 It cannot fail, and does no validity checking, except for
475 structural matters, such as
476 (a) spurious ! annotations.
477 (b) a class used as a type
480 dsHsType :: LHsType Name -> TcM Type
481 -- All HsTyVarBndrs in the intput type are kind-annotated
482 dsHsType ty = ds_type (unLoc ty)
484 ds_type ty@(HsTyVar name)
487 ds_type (HsParTy ty) -- Remove the parentheses markers
490 ds_type ty@(HsBangTy _ _) -- No bangs should be here
491 = failWithTc (ptext (sLit "Unexpected strictness annotation:") <+> ppr ty)
493 ds_type (HsKindSig ty k)
494 = dsHsType ty -- Kind checking done already
496 ds_type (HsListTy ty) = do
497 tau_ty <- dsHsType ty
498 checkWiredInTyCon listTyCon
499 return (mkListTy tau_ty)
501 ds_type (HsPArrTy ty) = do
502 tau_ty <- dsHsType ty
503 checkWiredInTyCon parrTyCon
504 return (mkPArrTy tau_ty)
506 ds_type (HsTupleTy boxity tys) = do
507 tau_tys <- dsHsTypes tys
508 checkWiredInTyCon tycon
509 return (mkTyConApp tycon tau_tys)
511 tycon = tupleTyCon boxity (length tys)
513 ds_type (HsFunTy ty1 ty2) = do
514 tau_ty1 <- dsHsType ty1
515 tau_ty2 <- dsHsType ty2
516 return (mkFunTy tau_ty1 tau_ty2)
518 ds_type (HsOpTy ty1 (L span op) ty2) = do
519 tau_ty1 <- dsHsType ty1
520 tau_ty2 <- dsHsType ty2
521 setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
525 tc <- tcLookupTyCon genUnitTyConName
526 return (mkTyConApp tc [])
528 ds_type ty@(HsAppTy _ _)
531 ds_type (HsPredTy pred) = do
532 pred' <- dsHsPred pred
533 return (mkPredTy pred')
535 ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
536 = tcTyVarBndrs tv_names $ \ tyvars -> do
537 theta <- mapM dsHsLPred (unLoc ctxt)
539 return (mkSigmaTy tyvars theta tau)
541 ds_type (HsSpliceTy {}) = panic "ds_type: HsSpliceTy"
543 ds_type (HsDocTy ty _) -- Remove the doc comment
546 dsHsTypes arg_tys = mapM dsHsType arg_tys
549 Help functions for type applications
550 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
553 ds_app :: HsType Name -> [LHsType Name] -> TcM Type
554 ds_app (HsAppTy ty1 ty2) tys
555 = ds_app (unLoc ty1) (ty2:tys)
558 arg_tys <- dsHsTypes tys
560 HsTyVar fun -> ds_var_app fun arg_tys
561 other -> do fun_ty <- ds_type ty
562 return (mkAppTys fun_ty arg_tys)
564 ds_var_app :: Name -> [Type] -> TcM Type
565 ds_var_app name arg_tys = do
566 thing <- tcLookup name
568 ATyVar _ ty -> return (mkAppTys ty arg_tys)
569 AGlobal (ATyCon tc) -> return (mkTyConApp tc arg_tys)
570 other -> wrongThingErr "type" thing name
578 dsHsLPred :: LHsPred Name -> TcM PredType
579 dsHsLPred pred = dsHsPred (unLoc pred)
581 dsHsPred pred@(HsClassP class_name tys)
582 = do { arg_tys <- dsHsTypes tys
583 ; clas <- tcLookupClass class_name
584 ; return (ClassP clas arg_tys)
586 dsHsPred pred@(HsEqualP ty1 ty2)
587 = do { arg_ty1 <- dsHsType ty1
588 ; arg_ty2 <- dsHsType ty2
589 ; return (EqPred arg_ty1 arg_ty2)
591 dsHsPred (HsIParam name ty)
592 = do { arg_ty <- dsHsType ty
593 ; return (IParam name arg_ty)
597 GADT constructor signatures
600 tcLHsConResTy :: LHsType Name -> TcM (TyCon, [TcType])
601 tcLHsConResTy (L span res_ty)
603 case get_args res_ty [] of
604 (HsTyVar tc_name, args)
605 -> do { args' <- mapM dsHsType args
606 ; thing <- tcLookup tc_name
608 AGlobal (ATyCon tc) -> return (tc, args')
609 other -> failWithTc (badGadtDecl res_ty) }
610 other -> failWithTc (badGadtDecl res_ty)
612 -- We can't call dsHsType on res_ty, and then do tcSplitTyConApp_maybe
613 -- because that causes a black hole, and for good reason. Building
614 -- the type means expanding type synonyms, and we can't do that
615 -- inside the "knot". So we have to work by steam.
616 get_args (HsAppTy (L _ fun) arg) args = get_args fun (arg:args)
617 get_args (HsParTy (L _ ty)) args = get_args ty args
618 get_args (HsOpTy ty1 (L span tc) ty2) args = (HsTyVar tc, ty1:ty2:args)
619 get_args ty args = (ty, args)
622 = hang (ptext (sLit "Malformed constructor result type:"))
625 typeCtxt ty = ptext (sLit "In the type") <+> quotes (ppr ty)
628 %************************************************************************
630 Type-variable binders
632 %************************************************************************
636 kcHsTyVars :: [LHsTyVarBndr Name]
637 -> ([LHsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
638 -- They scope over the thing inside
640 kcHsTyVars tvs thing_inside = do
641 bndrs <- mapM (wrapLocM kcHsTyVar) tvs
642 tcExtendKindEnvTvs bndrs (thing_inside bndrs)
644 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
645 -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
646 kcHsTyVar (UserTyVar name) = KindedTyVar name <$> newKindVar
647 kcHsTyVar (KindedTyVar name kind) = return (KindedTyVar name kind)
650 tcTyVarBndrs :: [LHsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
651 -> ([TyVar] -> TcM r)
653 -- Used when type-checking types/classes/type-decls
654 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
655 tcTyVarBndrs bndrs thing_inside = do
656 tyvars <- mapM (zonk . unLoc) bndrs
657 tcExtendTyVarEnv tyvars (thing_inside tyvars)
659 zonk (KindedTyVar name kind) = do { kind' <- zonkTcKindToKind kind
660 ; return (mkTyVar name kind') }
661 zonk (UserTyVar name) = WARN( True, ptext (sLit "Un-kinded tyvar") <+> ppr name )
662 return (mkTyVar name liftedTypeKind)
664 -----------------------------------
665 tcDataKindSig :: Maybe Kind -> TcM [TyVar]
666 -- GADT decls can have a (perhaps partial) kind signature
667 -- e.g. data T :: * -> * -> * where ...
668 -- This function makes up suitable (kinded) type variables for
669 -- the argument kinds, and checks that the result kind is indeed *.
670 -- We use it also to make up argument type variables for for data instances.
671 tcDataKindSig Nothing = return []
672 tcDataKindSig (Just kind)
673 = do { checkTc (isLiftedTypeKind res_kind) (badKindSig kind)
674 ; span <- getSrcSpanM
675 ; us <- newUniqueSupply
676 ; let uniqs = uniqsFromSupply us
677 ; return [ mk_tv span uniq str kind
678 | ((kind, str), uniq) <- arg_kinds `zip` names `zip` uniqs ] }
680 (arg_kinds, res_kind) = splitKindFunTys kind
681 mk_tv loc uniq str kind = mkTyVar name kind
683 name = mkInternalName uniq occ loc
684 occ = mkOccName tvName str
686 names :: [String] -- a,b,c...aa,ab,ac etc
687 names = [ c:cs | cs <- "" : names, c <- ['a'..'z'] ]
689 badKindSig :: Kind -> SDoc
691 = hang (ptext (sLit "Kind signature on data type declaration has non-* return kind"))
696 %************************************************************************
698 Scoped type variables
700 %************************************************************************
703 tcAddScopedTyVars is used for scoped type variables added by pattern
705 e.g. \ ((x::a), (y::a)) -> x+y
706 They never have explicit kinds (because this is source-code only)
707 They are mutable (because they can get bound to a more specific type).
709 Usually we kind-infer and expand type splices, and then
710 tupecheck/desugar the type. That doesn't work well for scoped type
711 variables, because they scope left-right in patterns. (e.g. in the
712 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
714 The current not-very-good plan is to
715 * find all the types in the patterns
716 * find their free tyvars
718 * bring the kinded type vars into scope
719 * BUT throw away the kind-checked type
720 (we'll kind-check it again when we type-check the pattern)
722 This is bad because throwing away the kind checked type throws away
723 its splices. But too bad for now. [July 03]
726 We no longer specify that these type variables must be univerally
727 quantified (lots of email on the subject). If you want to put that
729 a) Do a checkSigTyVars after thing_inside
730 b) More insidiously, don't pass in expected_ty, else
731 we unify with it too early and checkSigTyVars barfs
732 Instead you have to pass in a fresh ty var, and unify
733 it with expected_ty afterwards
736 tcHsPatSigType :: UserTypeCtxt
737 -> LHsType Name -- The type signature
738 -> TcM ([TyVar], -- Newly in-scope type variables
739 Type) -- The signature
740 -- Used for type-checking type signatures in
741 -- (a) patterns e.g f (x::Int) = e
742 -- (b) result signatures e.g. g x :: Int = e
743 -- (c) RULE forall bndrs e.g. forall (x::Int). f x = x
745 tcHsPatSigType ctxt hs_ty
746 = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
747 do { -- Find the type variables that are mentioned in the type
748 -- but not already in scope. These are the ones that
749 -- should be bound by the pattern signature
750 in_scope <- getInLocalScope
751 ; let span = getLoc hs_ty
752 sig_tvs = [ L span (UserTyVar n)
753 | n <- nameSetToList (extractHsTyVars hs_ty),
756 ; (tyvars, sig_ty) <- tcHsQuantifiedType sig_tvs hs_ty
757 ; checkValidType ctxt sig_ty
758 ; return (tyvars, sig_ty)
761 tcPatSig :: UserTypeCtxt
764 -> TcM (TcType, -- The type to use for "inside" the signature
765 [(Name,TcType)]) -- The new bit of type environment, binding
766 -- the scoped type variables
767 tcPatSig ctxt sig res_ty
768 = do { (sig_tvs, sig_ty) <- tcHsPatSigType ctxt sig
770 ; if null sig_tvs then do {
771 -- The type signature binds no type variables,
772 -- and hence is rigid, so use it to zap the res_ty
773 boxyUnify sig_ty res_ty
774 ; return (sig_ty, [])
777 -- Type signature binds at least one scoped type variable
779 -- A pattern binding cannot bind scoped type variables
780 -- The renamer fails with a name-out-of-scope error
781 -- if a pattern binding tries to bind a type variable,
782 -- So we just have an ASSERT here
783 ; let in_pat_bind = case ctxt of
784 BindPatSigCtxt -> True
786 ; ASSERT( not in_pat_bind || null sig_tvs ) return ()
788 -- Check that pat_ty is rigid
789 ; checkTc (isRigidTy res_ty) (wobblyPatSig sig_tvs)
791 -- Now match the pattern signature against res_ty
792 -- For convenience, and uniform-looking error messages
793 -- we do the matching by allocating meta type variables,
794 -- unifying, and reading out the results.
795 -- This is a strictly local operation.
796 ; box_tvs <- mapM tcInstBoxyTyVar sig_tvs
797 ; boxyUnify (substTyWith sig_tvs (mkTyVarTys box_tvs) sig_ty) res_ty
798 ; sig_tv_tys <- mapM readFilledBox box_tvs
800 -- Check that each is bound to a distinct type variable,
801 -- and one that is not already in scope
802 ; let tv_binds = map tyVarName sig_tvs `zip` sig_tv_tys
803 ; binds_in_scope <- getScopedTyVarBinds
804 ; check binds_in_scope tv_binds
807 ; return (res_ty, tv_binds)
810 check in_scope [] = return ()
811 check in_scope ((n,ty):rest) = do { check_one in_scope n ty
812 ; check ((n,ty):in_scope) rest }
814 check_one in_scope n ty
815 = do { checkTc (tcIsTyVarTy ty) (scopedNonVar n ty)
816 -- Must bind to a type variable
818 ; checkTc (null dups) (dupInScope n (head dups) ty)
819 -- Must not bind to the same type variable
820 -- as some other in-scope type variable
824 dups = [n' | (n',ty') <- in_scope, tcEqType ty' ty]
828 %************************************************************************
830 Scoped type variables
832 %************************************************************************
835 pprHsSigCtxt :: UserTypeCtxt -> LHsType Name -> SDoc
836 pprHsSigCtxt ctxt hs_ty = vcat [ ptext (sLit "In") <+> pprUserTypeCtxt ctxt <> colon,
837 nest 2 (pp_sig ctxt) ]
839 pp_sig (FunSigCtxt n) = pp_n_colon n
840 pp_sig (ConArgCtxt n) = pp_n_colon n
841 pp_sig (ForSigCtxt n) = pp_n_colon n
842 pp_sig other = ppr (unLoc hs_ty)
844 pp_n_colon n = ppr n <+> dcolon <+> ppr (unLoc hs_ty)
848 = hang (ptext (sLit "A pattern type signature cannot bind scoped type variables")
849 <+> pprQuotedList sig_tvs)
850 2 (ptext (sLit "unless the pattern has a rigid type context"))
853 = vcat [sep [ptext (sLit "The scoped type variable") <+> quotes (ppr n),
854 nest 2 (ptext (sLit "is bound to the type") <+> quotes (ppr ty))],
855 nest 2 (ptext (sLit "You can only bind scoped type variables to type variables"))]
858 = hang (ptext (sLit "The scoped type variables") <+> quotes (ppr n) <+> ptext (sLit "and") <+> quotes (ppr n'))
859 2 (vcat [ptext (sLit "are bound to the same type (variable)"),
860 ptext (sLit "Distinct scoped type variables must be distinct")])
863 = failWithTc (text "Equality predicate used as a type")