2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
8 tcHsSigType, tcHsDeriv,
12 kcHsTyVars, kcHsSigType, kcHsLiftedSigType,
13 kcCheckHsType, kcHsContext, kcHsType,
15 -- Typechecking kinded types
16 tcHsKindedContext, tcHsKindedType, tcHsBangType,
17 tcTyVarBndrs, dsHsType, tcLHsConSig,
19 tcHsPatSigType, tcAddLetBoundTyVars,
21 TcSigInfo(..), mkTcSig,
25 #include "HsVersions.h"
27 import HsSyn ( HsType(..), LHsType, HsTyVarBndr(..), LHsTyVarBndr, HsBang,
28 LHsContext, HsPred(..), LHsPred, LHsBinds,
29 getBangStrictness, collectSigTysFromHsBinds )
30 import RnHsSyn ( extractHsTyVars )
31 import TcHsSyn ( TcId )
34 import TcEnv ( tcExtendTyVarEnv, tcExtendKindEnv,
35 tcLookup, tcLookupClass, tcLookupTyCon,
36 TyThing(..), TcTyThing(..),
37 getInLocalScope, wrongThingErr
39 import TcMType ( newKindVar, tcSkolType, newMetaTyVar,
41 checkValidType, UserTypeCtxt(..), pprHsSigCtxt
43 import TcUnify ( unifyFunKind, checkExpectedKind )
44 import TcType ( Type, PredType(..), ThetaType,
45 SkolemInfo(SigSkol), MetaDetails(Flexi),
46 TcType, TcTyVar, TcKind, TcThetaType, TcTauType,
48 mkForAllTys, mkFunTys, tcEqType, isPredTy,
49 mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys,
50 tcSplitFunTy_maybe, tcSplitForAllTys )
51 import Kind ( liftedTypeKind, ubxTupleKind, openTypeKind, argTypeKind )
52 import Inst ( InstOrigin(..) )
54 import Id ( idName, idType )
55 import Var ( TyVar, mkTyVar, tyVarKind )
56 import TyCon ( TyCon, tyConKind )
57 import Class ( Class, classTyCon )
60 import PrelNames ( genUnitTyConName )
61 import Type ( deShadowTy )
62 import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy )
63 import Bag ( bagToList )
64 import BasicTypes ( Boxity(..) )
65 import SrcLoc ( Located(..), unLoc, noLoc )
71 ----------------------------
73 ----------------------------
75 Generally speaking we now type-check types in three phases
77 1. kcHsType: kind check the HsType
78 *includes* performing any TH type splices;
79 so it returns a translated, and kind-annotated, type
81 2. dsHsType: convert from HsType to Type:
83 expand type synonyms [mkGenTyApps]
84 hoist the foralls [tcHsType]
86 3. checkValidType: check the validity of the resulting type
88 Often these steps are done one after the other (tcHsSigType).
89 But in mutually recursive groups of type and class decls we do
90 1 kind-check the whole group
91 2 build TyCons/Classes in a knot-tied way
92 3 check the validity of types in the now-unknotted TyCons/Classes
94 For example, when we find
95 (forall a m. m a -> m a)
96 we bind a,m to kind varibles and kind-check (m a -> m a). This makes
97 a get kind *, and m get kind *->*. Now we typecheck (m a -> m a) in
98 an environment that binds a and m suitably.
100 The kind checker passed to tcHsTyVars needs to look at enough to
101 establish the kind of the tyvar:
102 * For a group of type and class decls, it's just the group, not
103 the rest of the program
104 * For a tyvar bound in a pattern type signature, its the types
105 mentioned in the other type signatures in that bunch of patterns
106 * For a tyvar bound in a RULE, it's the type signatures on other
107 universally quantified variables in the rule
109 Note that this may occasionally give surprising results. For example:
111 data T a b = MkT (a b)
113 Here we deduce a::*->*, b::*
114 But equally valid would be a::(*->*)-> *, b::*->*
119 Some of the validity check could in principle be done by the kind checker,
122 - During desugaring, we normalise by expanding type synonyms. Only
123 after this step can we check things like type-synonym saturation
124 e.g. type T k = k Int
126 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
127 and then S is saturated. This is a GHC extension.
129 - Similarly, also a GHC extension, we look through synonyms before complaining
130 about the form of a class or instance declaration
132 - Ambiguity checks involve functional dependencies, and it's easier to wait
133 until knots have been resolved before poking into them
135 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
136 finished building the loop. So to keep things simple, we postpone most validity
137 checking until step (3).
141 During step (1) we might fault in a TyCon defined in another module, and it might
142 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
143 knot around type declarations with ARecThing, so that the fault-in code can get
144 the TyCon being defined.
147 %************************************************************************
149 \subsection{Checking types}
151 %************************************************************************
154 tcHsSigType :: UserTypeCtxt -> LHsType Name -> TcM Type
155 -- Do kind checking, and hoist for-alls to the top
156 tcHsSigType ctxt hs_ty
157 = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
158 do { kinded_ty <- kcTypeType hs_ty
159 ; ty <- tcHsKindedType kinded_ty
160 ; checkValidType ctxt ty
162 -- Used for the deriving(...) items
163 tcHsDeriv :: LHsType Name -> TcM ([TyVar], Class, [Type])
164 tcHsDeriv = addLocM (tc_hs_deriv [])
166 tc_hs_deriv tv_names (HsPredTy (HsClassP cls_name hs_tys))
167 = kcHsTyVars tv_names $ \ tv_names' ->
168 do { cls_kind <- kcClass cls_name
169 ; (tys, res_kind) <- kcApps cls_kind (ppr cls_name) hs_tys
170 ; tcTyVarBndrs tv_names' $ \ tyvars ->
171 do { arg_tys <- dsHsTypes tys
172 ; cls <- tcLookupClass cls_name
173 ; return (tyvars, cls, arg_tys) }}
175 tc_hs_deriv tv_names1 (HsForAllTy _ tv_names2 (L _ []) (L _ ty))
176 = -- Funny newtype deriving form
178 -- where C has arity 2. Hence can't use regular functions
179 tc_hs_deriv (tv_names1 ++ tv_names2) ty
182 = failWithTc (ptext SLIT("Illegal deriving item") <+> ppr other)
185 These functions are used during knot-tying in
186 type and class declarations, when we have to
187 separate kind-checking, desugaring, and validity checking
190 kcHsSigType, kcHsLiftedSigType :: LHsType Name -> TcM (LHsType Name)
191 -- Used for type signatures
192 kcHsSigType ty = kcTypeType ty
193 kcHsLiftedSigType ty = kcLiftedType ty
195 tcHsKindedType :: LHsType Name -> TcM Type
196 -- Don't do kind checking, nor validity checking,
197 -- but do hoist for-alls to the top
198 -- This is used in type and class decls, where kinding is
199 -- done in advance, and validity checking is done later
200 -- [Validity checking done later because of knot-tying issues.]
202 = do { ty <- dsHsType hs_ty
203 ; return (hoistForAllTys ty) }
205 tcHsBangType :: LHsType Name -> TcM Type
206 -- Permit a bang, but discard it
207 tcHsBangType (L span (HsBangTy b ty)) = tcHsKindedType ty
208 tcHsBangType ty = tcHsKindedType ty
210 tcHsKindedContext :: LHsContext Name -> TcM ThetaType
211 -- Used when we are expecting a ClassContext (i.e. no implicit params)
212 -- Does not do validity checking, like tcHsKindedType
213 tcHsKindedContext hs_theta = addLocM (mappM dsHsLPred) hs_theta
217 %************************************************************************
219 The main kind checker: kcHsType
221 %************************************************************************
223 First a couple of simple wrappers for kcHsType
226 ---------------------------
227 kcLiftedType :: LHsType Name -> TcM (LHsType Name)
228 -- The type ty must be a *lifted* *type*
229 kcLiftedType ty = kcCheckHsType ty liftedTypeKind
231 ---------------------------
232 kcTypeType :: LHsType Name -> TcM (LHsType Name)
233 -- The type ty must be a *type*, but it can be lifted or
234 -- unlifted or an unboxed tuple.
235 kcTypeType ty = kcCheckHsType ty openTypeKind
237 ---------------------------
238 kcCheckHsType :: LHsType Name -> TcKind -> TcM (LHsType Name)
239 -- Check that the type has the specified kind
240 -- Be sure to use checkExpectedKind, rather than simply unifying
241 -- with OpenTypeKind, because it gives better error messages
242 kcCheckHsType (L span ty) exp_kind
244 kc_hs_type ty `thenM` \ (ty', act_kind) ->
245 checkExpectedKind ty act_kind exp_kind `thenM_`
249 Here comes the main function
252 kcHsType :: LHsType Name -> TcM (LHsType Name, TcKind)
253 kcHsType ty = wrapLocFstM kc_hs_type ty
254 -- kcHsType *returns* the kind of the type, rather than taking an expected
255 -- kind as argument as tcExpr does.
257 -- (a) the kind of (->) is
258 -- forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
259 -- so we'd need to generate huge numbers of bx variables.
260 -- (b) kinds are so simple that the error messages are fine
262 -- The translated type has explicitly-kinded type-variable binders
264 kc_hs_type (HsParTy ty)
265 = kcHsType ty `thenM` \ (ty', kind) ->
266 returnM (HsParTy ty', kind)
268 kc_hs_type (HsTyVar name)
269 = kcTyVar name `thenM` \ kind ->
270 returnM (HsTyVar name, kind)
272 kc_hs_type (HsListTy ty)
273 = kcLiftedType ty `thenM` \ ty' ->
274 returnM (HsListTy ty', liftedTypeKind)
276 kc_hs_type (HsPArrTy ty)
277 = kcLiftedType ty `thenM` \ ty' ->
278 returnM (HsPArrTy ty', liftedTypeKind)
280 kc_hs_type (HsNumTy n)
281 = returnM (HsNumTy n, liftedTypeKind)
283 kc_hs_type (HsKindSig ty k)
284 = kcCheckHsType ty k `thenM` \ ty' ->
285 returnM (HsKindSig ty' k, k)
287 kc_hs_type (HsTupleTy Boxed tys)
288 = mappM kcLiftedType tys `thenM` \ tys' ->
289 returnM (HsTupleTy Boxed tys', liftedTypeKind)
291 kc_hs_type (HsTupleTy Unboxed tys)
292 = mappM kcTypeType tys `thenM` \ tys' ->
293 returnM (HsTupleTy Unboxed tys', ubxTupleKind)
295 kc_hs_type (HsFunTy ty1 ty2)
296 = kcCheckHsType ty1 argTypeKind `thenM` \ ty1' ->
297 kcTypeType ty2 `thenM` \ ty2' ->
298 returnM (HsFunTy ty1' ty2', liftedTypeKind)
300 kc_hs_type ty@(HsOpTy ty1 op ty2)
301 = addLocM kcTyVar op `thenM` \ op_kind ->
302 kcApps op_kind (ppr op) [ty1,ty2] `thenM` \ ([ty1',ty2'], res_kind) ->
303 returnM (HsOpTy ty1' op ty2', res_kind)
305 kc_hs_type ty@(HsAppTy ty1 ty2)
306 = kcHsType fun_ty `thenM` \ (fun_ty', fun_kind) ->
307 kcApps fun_kind (ppr fun_ty) arg_tys `thenM` \ ((arg_ty':arg_tys'), res_kind) ->
308 returnM (foldl mk_app (HsAppTy fun_ty' arg_ty') arg_tys', res_kind)
310 (fun_ty, arg_tys) = split ty1 [ty2]
311 split (L _ (HsAppTy f a)) as = split f (a:as)
313 mk_app fun arg = HsAppTy (noLoc fun) arg -- Add noLocs for inner nodes of
314 -- the application; they are never used
316 kc_hs_type (HsPredTy pred)
317 = kcHsPred pred `thenM` \ pred' ->
318 returnM (HsPredTy pred', liftedTypeKind)
320 kc_hs_type (HsForAllTy exp tv_names context ty)
321 = kcHsTyVars tv_names $ \ tv_names' ->
322 kcHsContext context `thenM` \ ctxt' ->
323 kcLiftedType ty `thenM` \ ty' ->
324 -- The body of a forall is usually a type, but in principle
325 -- there's no reason to prohibit *unlifted* types.
326 -- In fact, GHC can itself construct a function with an
327 -- unboxed tuple inside a for-all (via CPR analyis; see
328 -- typecheck/should_compile/tc170)
330 -- Still, that's only for internal interfaces, which aren't
331 -- kind-checked, so we only allow liftedTypeKind here
332 returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
334 kc_hs_type (HsBangTy b ty)
335 = do { (ty', kind) <- kcHsType ty
336 ; return (HsBangTy b ty', kind) }
338 kc_hs_type ty@(HsSpliceTy _)
339 = failWithTc (ptext SLIT("Unexpected type splice:") <+> ppr ty)
342 ---------------------------
343 kcApps :: TcKind -- Function kind
345 -> [LHsType Name] -- Arg types
346 -> TcM ([LHsType Name], TcKind) -- Kind-checked args
347 kcApps fun_kind ppr_fun args
348 = split_fk fun_kind (length args) `thenM` \ (arg_kinds, res_kind) ->
349 zipWithM kc_arg args arg_kinds `thenM` \ args' ->
350 returnM (args', res_kind)
352 split_fk fk 0 = returnM ([], fk)
353 split_fk fk n = unifyFunKind fk `thenM` \ mb_fk ->
355 Nothing -> failWithTc too_many_args
356 Just (ak,fk') -> split_fk fk' (n-1) `thenM` \ (aks, rk) ->
359 kc_arg arg arg_kind = kcCheckHsType arg arg_kind
361 too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
362 ptext SLIT("is applied to too many type arguments")
364 ---------------------------
365 kcHsContext :: LHsContext Name -> TcM (LHsContext Name)
366 kcHsContext ctxt = wrapLocM (mappM kcHsLPred) ctxt
368 kcHsLPred :: LHsPred Name -> TcM (LHsPred Name)
369 kcHsLPred = wrapLocM kcHsPred
371 kcHsPred :: HsPred Name -> TcM (HsPred Name)
372 kcHsPred pred -- Checks that the result is of kind liftedType
373 = kc_pred pred `thenM` \ (pred', kind) ->
374 checkExpectedKind pred kind liftedTypeKind `thenM_`
377 ---------------------------
378 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
379 -- Does *not* check for a saturated
380 -- application (reason: used from TcDeriv)
381 kc_pred pred@(HsIParam name ty)
382 = kcHsType ty `thenM` \ (ty', kind) ->
383 returnM (HsIParam name ty', kind)
385 kc_pred pred@(HsClassP cls tys)
386 = kcClass cls `thenM` \ kind ->
387 kcApps kind (ppr cls) tys `thenM` \ (tys', res_kind) ->
388 returnM (HsClassP cls tys', res_kind)
390 ---------------------------
391 kcTyVar :: Name -> TcM TcKind
392 kcTyVar name -- Could be a tyvar or a tycon
393 = traceTc (text "lk1" <+> ppr name) `thenM_`
394 tcLookup name `thenM` \ thing ->
395 traceTc (text "lk2" <+> ppr name <+> ppr thing) `thenM_`
397 ATyVar tv -> returnM (tyVarKind tv)
398 AThing kind -> returnM kind
399 AGlobal (ATyCon tc) -> returnM (tyConKind tc)
400 other -> wrongThingErr "type" thing name
402 kcClass :: Name -> TcM TcKind
403 kcClass cls -- Must be a class
404 = tcLookup cls `thenM` \ thing ->
406 AThing kind -> returnM kind
407 AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls))
408 other -> wrongThingErr "class" thing cls
412 %************************************************************************
416 %************************************************************************
420 * Transforms from HsType to Type
423 It cannot fail, and does no validity checking, except for
424 structural matters, such as spurious ! annotations.
427 dsHsType :: LHsType Name -> TcM Type
428 -- All HsTyVarBndrs in the intput type are kind-annotated
429 dsHsType ty = ds_type (unLoc ty)
431 ds_type ty@(HsTyVar name)
434 ds_type (HsParTy ty) -- Remove the parentheses markers
437 ds_type ty@(HsBangTy _ _) -- No bangs should be here
438 = failWithTc (ptext SLIT("Unexpected strictness annotation:") <+> ppr ty)
440 ds_type (HsKindSig ty k)
441 = dsHsType ty -- Kind checking done already
443 ds_type (HsListTy ty)
444 = dsHsType ty `thenM` \ tau_ty ->
445 returnM (mkListTy tau_ty)
447 ds_type (HsPArrTy ty)
448 = dsHsType ty `thenM` \ tau_ty ->
449 returnM (mkPArrTy tau_ty)
451 ds_type (HsTupleTy boxity tys)
452 = dsHsTypes tys `thenM` \ tau_tys ->
453 returnM (mkTupleTy boxity (length tys) tau_tys)
455 ds_type (HsFunTy ty1 ty2)
456 = dsHsType ty1 `thenM` \ tau_ty1 ->
457 dsHsType ty2 `thenM` \ tau_ty2 ->
458 returnM (mkFunTy tau_ty1 tau_ty2)
460 ds_type (HsOpTy ty1 (L span op) ty2)
461 = dsHsType ty1 `thenM` \ tau_ty1 ->
462 dsHsType ty2 `thenM` \ tau_ty2 ->
463 setSrcSpan span (ds_var_app op [tau_ty1,tau_ty2])
467 tcLookupTyCon genUnitTyConName `thenM` \ tc ->
468 returnM (mkTyConApp tc [])
470 ds_type ty@(HsAppTy _ _)
473 ds_type (HsPredTy pred)
474 = dsHsPred pred `thenM` \ pred' ->
475 returnM (mkPredTy pred')
477 ds_type full_ty@(HsForAllTy exp tv_names ctxt ty)
478 = tcTyVarBndrs tv_names $ \ tyvars ->
479 mappM dsHsLPred (unLoc ctxt) `thenM` \ theta ->
480 dsHsType ty `thenM` \ tau ->
481 returnM (mkSigmaTy tyvars theta tau)
483 dsHsTypes arg_tys = mappM dsHsType arg_tys
486 Help functions for type applications
487 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
490 ds_app :: HsType Name -> [LHsType Name] -> TcM Type
491 ds_app (HsAppTy ty1 ty2) tys
492 = ds_app (unLoc ty1) (ty2:tys)
495 = dsHsTypes tys `thenM` \ arg_tys ->
497 HsTyVar fun -> ds_var_app fun arg_tys
498 other -> ds_type ty `thenM` \ fun_ty ->
499 returnM (mkAppTys fun_ty arg_tys)
501 ds_var_app :: Name -> [Type] -> TcM Type
502 ds_var_app name arg_tys
503 = tcLookup name `thenM` \ thing ->
505 ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
506 AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
507 -- AThing _ -> tcLookupTyCon name `thenM` \ tc ->
508 -- returnM (mkGenTyConApp tc arg_tys)
509 other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
517 dsHsLPred :: LHsPred Name -> TcM PredType
518 dsHsLPred pred = dsHsPred (unLoc pred)
520 dsHsPred pred@(HsClassP class_name tys)
521 = dsHsTypes tys `thenM` \ arg_tys ->
522 tcLookupClass class_name `thenM` \ clas ->
523 returnM (ClassP clas arg_tys)
525 dsHsPred (HsIParam name ty)
526 = dsHsType ty `thenM` \ arg_ty ->
527 returnM (IParam name arg_ty)
530 GADT constructor signatures
533 tcLHsConSig :: LHsType Name
534 -> TcM ([TcTyVar], TcThetaType,
537 -- Take apart the type signature for a data constructor
538 -- The difference is that there can be bangs at the top of
539 -- the argument types, and kind-checking is the right place to check
540 tcLHsConSig sig@(L span (HsForAllTy exp tv_names ctxt ty))
542 addErrCtxt (gadtSigCtxt sig) $
543 tcTyVarBndrs tv_names $ \ tyvars ->
544 do { theta <- mappM dsHsLPred (unLoc ctxt)
545 ; (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
546 ; return (tyvars, theta, bangs, arg_tys, tc, res_tys) }
548 = do { (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
549 ; return ([], [], bangs, arg_tys, tc, res_tys) }
552 tc_con_sig_tau (L _ (HsFunTy arg ty))
553 = do { (bangs, arg_tys, tc, res_tys) <- tc_con_sig_tau ty
554 ; arg_ty <- tcHsBangType arg
555 ; return (getBangStrictness arg : bangs,
556 arg_ty : arg_tys, tc, res_tys) }
559 = do { (tc, res_tys) <- tc_con_res ty []
560 ; return ([], [], tc, res_tys) }
563 tc_con_res (L _ (HsAppTy fun res_ty)) res_tys
564 = do { res_ty' <- dsHsType res_ty
565 ; tc_con_res fun (res_ty' : res_tys) }
567 tc_con_res ty@(L _ (HsTyVar name)) res_tys
568 = do { thing <- tcLookup name
570 AGlobal (ATyCon tc) -> return (tc, res_tys)
571 other -> failWithTc (badGadtDecl ty)
574 tc_con_res ty _ = failWithTc (badGadtDecl ty)
577 = hang (ptext SLIT("In the signature of a data constructor:"))
580 = hang (ptext SLIT("Malformed constructor signature:"))
584 %************************************************************************
586 Type-variable binders
588 %************************************************************************
592 kcHsTyVars :: [LHsTyVarBndr Name]
593 -> ([LHsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
594 -- They scope over the thing inside
596 kcHsTyVars tvs thing_inside
597 = mappM (wrapLocM kcHsTyVar) tvs `thenM` \ bndrs ->
598 tcExtendKindEnv [(n,k) | L _ (KindedTyVar n k) <- bndrs]
601 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
602 -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
603 kcHsTyVar (UserTyVar name) = newKindVar `thenM` \ kind ->
604 returnM (KindedTyVar name kind)
605 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
608 tcTyVarBndrs :: [LHsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
609 -> ([TyVar] -> TcM r)
611 -- Used when type-checking types/classes/type-decls
612 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
613 tcTyVarBndrs bndrs thing_inside
614 = mapM (zonk . unLoc) bndrs `thenM` \ tyvars ->
615 tcExtendTyVarEnv tyvars (thing_inside tyvars)
617 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
618 returnM (mkTyVar name kind')
619 zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
620 returnM (mkTyVar name liftedTypeKind)
624 %************************************************************************
626 Scoped type variables
628 %************************************************************************
631 tcAddScopedTyVars is used for scoped type variables added by pattern
633 e.g. \ ((x::a), (y::a)) -> x+y
634 They never have explicit kinds (because this is source-code only)
635 They are mutable (because they can get bound to a more specific type).
637 Usually we kind-infer and expand type splices, and then
638 tupecheck/desugar the type. That doesn't work well for scoped type
639 variables, because they scope left-right in patterns. (e.g. in the
640 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
642 The current not-very-good plan is to
643 * find all the types in the patterns
644 * find their free tyvars
646 * bring the kinded type vars into scope
647 * BUT throw away the kind-checked type
648 (we'll kind-check it again when we type-check the pattern)
650 This is bad because throwing away the kind checked type throws away
651 its splices. But too bad for now. [July 03]
654 We no longer specify that these type variables must be univerally
655 quantified (lots of email on the subject). If you want to put that
657 a) Do a checkSigTyVars after thing_inside
658 b) More insidiously, don't pass in expected_ty, else
659 we unify with it too early and checkSigTyVars barfs
660 Instead you have to pass in a fresh ty var, and unify
661 it with expected_ty afterwards
664 tcPatSigBndrs :: LHsType Name
665 -> TcM ([TcTyVar], -- Brought into scope
666 LHsType Name) -- Kinded, but not yet desugared
669 = do { in_scope <- getInLocalScope
670 ; span <- getSrcSpanM
671 ; let sig_tvs = [ L span (UserTyVar n)
672 | n <- nameSetToList (extractHsTyVars hs_ty),
674 -- The tyvars we want are the free type variables of
675 -- the type that are not already in scope
677 -- Behave like kcHsType on a ForAll type
678 -- i.e. make kinded tyvars with mutable kinds,
679 -- and kind-check the enclosed types
680 ; (kinded_tvs, kinded_ty) <- kcHsTyVars sig_tvs $ \ kinded_tvs -> do
681 { kinded_ty <- kcTypeType hs_ty
682 ; return (kinded_tvs, kinded_ty) }
684 -- Zonk the mutable kinds and bring the tyvars into scope
685 -- Just like the call to tcTyVarBndrs in ds_type (HsForAllTy case),
686 -- except that it brings *meta* tyvars into scope, not regular ones
688 -- [Out of date, but perhaps should be resurrected]
689 -- Furthermore, the tyvars are PatSigTvs, which means that we get better
690 -- error messages when type variables escape:
691 -- Inferred type is less polymorphic than expected
692 -- Quantified type variable `t' escapes
693 -- It is mentioned in the environment:
694 -- t is bound by the pattern type signature at tcfail103.hs:6
695 ; tyvars <- mapM (zonk . unLoc) kinded_tvs
696 ; return (tyvars, kinded_ty) }
698 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
699 newMetaTyVar name kind' Flexi
700 -- Scoped type variables are bound to a *type*, hence Flexi
701 zonk (UserTyVar name) = pprTrace "Un-kinded tyvar" (ppr name) $
702 returnM (mkTyVar name liftedTypeKind)
704 tcHsPatSigType :: UserTypeCtxt
705 -> LHsType Name -- The type signature
706 -> TcM ([TcTyVar], -- Newly in-scope type variables
707 TcType) -- The signature
709 tcHsPatSigType ctxt hs_ty
710 = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
711 do { (tyvars, kinded_ty) <- tcPatSigBndrs hs_ty
713 -- Complete processing of the type, and check its validity
714 ; tcExtendTyVarEnv tyvars $ do
715 { sig_ty <- tcHsKindedType kinded_ty
716 ; checkValidType ctxt sig_ty
717 ; return (tyvars, sig_ty) }
720 tcAddLetBoundTyVars :: LHsBinds Name -> TcM a -> TcM a
721 -- Turgid funciton, used for type variables bound by the patterns of a let binding
723 tcAddLetBoundTyVars binds thing_inside
724 = go (collectSigTysFromHsBinds (bagToList binds)) thing_inside
726 go [] thing_inside = thing_inside
727 go (hs_ty:hs_tys) thing_inside
728 = do { (tyvars, _kinded_ty) <- tcPatSigBndrs hs_ty
729 ; tcExtendTyVarEnv tyvars (go hs_tys thing_inside) }
733 %************************************************************************
735 \subsection{Signatures}
737 %************************************************************************
739 @tcSigs@ checks the signatures for validity, and returns a list of
740 {\em freshly-instantiated} signatures. That is, the types are already
741 split up, and have fresh type variables installed. All non-type-signature
742 "RenamedSigs" are ignored.
744 The @TcSigInfo@ contains @TcTypes@ because they are unified with
745 the variable's type, and after that checked to see whether they've
751 sig_id :: TcId, -- *Polymorphic* binder for this value...
752 sig_tvs :: [TcTyVar], -- tyvars
753 sig_theta :: TcThetaType, -- theta
754 sig_tau :: TcTauType, -- tau
755 sig_loc :: InstLoc -- The location of the signature
758 type TcSigFun = Name -> Maybe TcSigInfo
760 instance Outputable TcSigInfo where
761 ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau})
762 = ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
764 lookupSig :: [TcSigInfo] -> TcSigFun -- Search for a particular signature
765 lookupSig [] name = Nothing
766 lookupSig (sig : sigs) name
767 | name == idName (sig_id sig) = Just sig
768 | otherwise = lookupSig sigs name
770 mkTcSig :: TcId -> TcM TcSigInfo
772 = -- Instantiate this type
773 -- It's important to do this even though in the error-free case
774 -- we could just split the sigma_tc_ty (since the tyvars don't
775 -- unified with anything). But in the case of an error, when
776 -- the tyvars *do* get unified with something, we want to carry on
777 -- typechecking the rest of the program with the function bound
778 -- to a pristine type, namely sigma_tc_ty
779 do { let rigid_info = SigSkol (idName poly_id)
780 ; (tyvars', theta', tau') <- tcSkolType rigid_info (idType poly_id)
781 ; loc <- getInstLoc (SigOrigin rigid_info)
782 ; return (TcSigInfo { sig_id = poly_id, sig_tvs = tyvars',
783 sig_theta = theta', sig_tau = tau', sig_loc = loc }) }
787 %************************************************************************
789 \subsection{Errors and contexts}
791 %************************************************************************
795 hoistForAllTys :: Type -> Type
796 -- Used for user-written type signatures only
797 -- Move all the foralls and constraints to the top
798 -- e.g. T -> forall a. a ==> forall a. T -> a
799 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
801 -- Also: eliminate duplicate constraints. These can show up
802 -- when hoisting constraints, notably implicit parameters.
804 -- We want to 'look through' type synonyms when doing this
805 -- so it's better done on the Type than the HsType
809 no_shadow_ty = deShadowTy ty
810 -- Running over ty with an empty substitution gives it the
811 -- no-shadowing property. This is important. For example:
812 -- type Foo r = forall a. a -> r
813 -- foo :: Foo (Foo ())
814 -- Here the hoisting should give
815 -- foo :: forall a a1. a -> a1 -> ()
817 -- What about type vars that are lexically in scope in the envt?
818 -- We simply rely on them having a different unique to any
819 -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
820 -- out of the envt, which is boring and (I think) not necessary.
822 case hoist no_shadow_ty of
823 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
824 -- The 'nubBy' eliminates duplicate constraints,
825 -- notably implicit parameters
828 | (tvs1, body_ty) <- tcSplitForAllTys ty,
830 = case hoist body_ty of
831 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
833 | Just (arg, res) <- tcSplitFunTy_maybe ty
835 arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
836 in -- to the argument type
837 if (isPredTy arg') then
839 (tvs,theta,tau) -> (tvs, arg':theta, tau)
842 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
844 | otherwise = ([], [], ty)