2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
12 kcHsTyVars, kcHsSigType, kcHsLiftedSigType,
13 kcCheckHsType, kcHsContext,
15 -- Typechecking kinded types
16 tcHsKindedContext, tcHsKindedType, tcTyVarBndrs, dsHsType,
20 TcSigInfo(..), tcTySig, mkTcSig, maybeSig, tcSigPolyId, tcSigMonoId
23 #include "HsVersions.h"
25 import HsSyn ( HsType(..), HsTyVarBndr(..), HsContext, Sig(..), HsPred(..) )
26 import RnHsSyn ( RenamedHsType, RenamedContext, RenamedSig, extractHsTyVars )
27 import TcHsSyn ( TcId )
30 import TcEnv ( tcExtendTyVarEnv, tcExtendTyVarKindEnv,
31 tcLookup, tcLookupClass, tcLookupTyCon,
32 TyThing(..), TcTyThing(..),
35 import TcMType ( newKindVar, newOpenTypeKind, tcInstType, newMutTyVar,
36 zonkTcType, zonkTcKindToKind,
37 checkValidType, UserTypeCtxt(..), pprHsSigCtxt
39 import TcUnify ( unifyKind, unifyFunKind )
40 import TcType ( Type, PredType(..), ThetaType, TyVarDetails(..),
41 TcTyVar, TcKind, TcThetaType, TcTauType,
42 mkTyVarTy, mkTyVarTys, mkFunTy, isTypeKind,
43 mkForAllTys, mkFunTys, tcEqType, isPredTy,
44 mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys,
45 liftedTypeKind, unliftedTypeKind, eqKind,
46 tcSplitFunTy_maybe, tcSplitForAllTys, tcSplitSigmaTy
48 import PprType ( pprKind, pprThetaArrow )
49 import qualified Type ( splitFunTys )
50 import Inst ( Inst, InstOrigin(..), newMethod, instToId )
52 import Id ( mkLocalId, idName, idType )
53 import Var ( TyVar, mkTyVar, tyVarKind )
54 import ErrUtils ( Message )
55 import TyCon ( TyCon, tyConKind )
56 import Class ( classTyCon )
59 import PrelNames ( genUnitTyConName )
60 import Subst ( deShadowTy )
61 import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy )
62 import BasicTypes ( Boxity(..) )
63 import SrcLoc ( SrcLoc )
69 ----------------------------
71 ----------------------------
73 Generally speaking we now type-check types in three phases
75 1. kcHsType: kind check the HsType
76 *includes* performing any TH type splices;
77 so it returns a translated, and kind-annotated, type
79 2. dsHsType: convert from HsType to Type:
81 expand type synonyms [mkGenTyApps]
82 hoist the foralls [tcHsType]
84 3. checkValidType: check the validity of the resulting type
86 Often these steps are done one after the other (tcHsSigType).
87 But in mutually recursive groups of type and class decls we do
88 1 kind-check the whole group
89 2 build TyCons/Classes in a knot-tied way
90 3 check the validity of types in the now-unknotted TyCons/Classes
92 For example, when we find
93 (forall a m. m a -> m a)
94 we bind a,m to kind varibles and kind-check (m a -> m a). This makes
95 a get kind *, and m get kind *->*. Now we typecheck (m a -> m a) in
96 an environment that binds a and m suitably.
98 The kind checker passed to tcHsTyVars needs to look at enough to
99 establish the kind of the tyvar:
100 * For a group of type and class decls, it's just the group, not
101 the rest of the program
102 * For a tyvar bound in a pattern type signature, its the types
103 mentioned in the other type signatures in that bunch of patterns
104 * For a tyvar bound in a RULE, it's the type signatures on other
105 universally quantified variables in the rule
107 Note that this may occasionally give surprising results. For example:
109 data T a b = MkT (a b)
111 Here we deduce a::*->*, b::*
112 But equally valid would be a::(*->*)-> *, b::*->*
117 Some of the validity check could in principle be done by the kind checker,
120 - During desugaring, we normalise by expanding type synonyms. Only
121 after this step can we check things like type-synonym saturation
122 e.g. type T k = k Int
124 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
125 and then S is saturated. This is a GHC extension.
127 - Similarly, also a GHC extension, we look through synonyms before complaining
128 about the form of a class or instance declaration
130 - Ambiguity checks involve functional dependencies, and it's easier to wait
131 until knots have been resolved before poking into them
133 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
134 finished building the loop. So to keep things simple, we postpone most validity
135 checking until step (3).
139 During step (1) we might fault in a TyCon defined in another module, and it might
140 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
141 knot around type declarations with ARecThing, so that the fault-in code can get
142 the TyCon being defined.
145 %************************************************************************
147 \subsection{Checking types}
149 %************************************************************************
152 tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
153 -- Do kind checking, and hoist for-alls to the top
154 tcHsSigType ctxt hs_ty
155 = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
156 do { kinded_ty <- kcTypeType hs_ty
157 ; ty <- tcHsKindedType kinded_ty
158 ; checkValidType ctxt ty
161 -- tcHsPred is happy with a partial application, e.g. (ST s)
164 = do { (kinded_pred,_) <- kc_pred pred -- kc_pred rather than kcHsPred
165 -- to avoid the partial application check
166 ; dsHsPred kinded_pred }
169 These functions are used during knot-tying in
170 type and class declarations, when we have to
171 separate kind-checking, desugaring, and validity checking
174 kcHsSigType, kcHsLiftedSigType :: HsType Name -> TcM (HsType Name)
175 -- Used for type signatures
176 kcHsSigType ty = kcTypeType ty
177 kcHsLiftedSigType ty = kcLiftedType ty
179 tcHsKindedType :: RenamedHsType -> TcM Type
180 -- Don't do kind checking, nor validity checking,
181 -- but do hoist for-alls to the top
182 -- This is used in type and class decls, where kinding is
183 -- done in advance, and validity checking is done later
184 -- [Validity checking done later because of knot-tying issues.]
186 = do { ty <- dsHsType hs_ty
187 ; return (hoistForAllTys ty) }
189 tcHsKindedContext :: RenamedContext -> TcM ThetaType
190 -- Used when we are expecting a ClassContext (i.e. no implicit params)
191 -- Does not do validity checking, like tcHsKindedType
192 tcHsKindedContext hs_theta = mappM dsHsPred hs_theta
196 %************************************************************************
198 The main kind checker: kcHsType
200 %************************************************************************
202 First a couple of simple wrappers for kcHsType
205 ---------------------------
206 kcLiftedType :: HsType Name -> TcM (HsType Name)
207 -- The type ty must be a *lifted* *type*
208 kcLiftedType ty = kcCheckHsType ty liftedTypeKind
210 ---------------------------
211 kcTypeType :: HsType Name -> TcM (HsType Name)
212 -- The type ty must be a *type*, but it can be lifted or unlifted
213 -- Be sure to use checkExpectedKind, rather than simply unifying
214 -- with (Type bx), because it gives better error messages
216 = kcHsType ty `thenM` \ (ty', kind) ->
217 if isTypeKind kind then
220 newOpenTypeKind `thenM` \ type_kind ->
221 traceTc (text "kcTypeType" $$ nest 2 (ppr ty $$ ppr ty' $$ ppr kind $$ ppr type_kind)) `thenM_`
222 checkExpectedKind (ppr ty) kind type_kind `thenM_`
225 ---------------------------
226 kcCheckHsType :: HsType Name -> TcKind -> TcM (HsType Name)
227 -- Check that the type has the specified kind
228 kcCheckHsType ty exp_kind
229 = kcHsType ty `thenM` \ (ty', act_kind) ->
230 checkExpectedKind (ppr ty) act_kind exp_kind `thenM_`
234 Here comes the main function
237 kcHsType :: HsType Name -> TcM (HsType Name, TcKind)
238 -- kcHsType *returns* the kind of the type, rather than taking an expected
239 -- kind as argument as tcExpr does.
241 -- (a) the kind of (->) is
242 -- forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
243 -- so we'd need to generate huge numbers of bx variables.
244 -- (b) kinds are so simple that the error messages are fine
246 -- The translated type has explicitly-kinded type-variable binders
248 kcHsType (HsParTy ty)
249 = kcHsType ty `thenM` \ (ty', kind) ->
250 returnM (HsParTy ty', kind)
252 kcHsType (HsTyVar name)
253 = kcTyVar name `thenM` \ kind ->
254 returnM (HsTyVar name, kind)
256 kcHsType (HsListTy ty)
257 = kcLiftedType ty `thenM` \ ty' ->
258 returnM (HsListTy ty', liftedTypeKind)
260 kcHsType (HsPArrTy ty)
261 = kcLiftedType ty `thenM` \ ty' ->
262 returnM (HsPArrTy ty', liftedTypeKind)
265 = returnM (HsNumTy n, liftedTypeKind)
267 kcHsType (HsKindSig ty k)
268 = kcCheckHsType ty k `thenM` \ ty' ->
269 returnM (HsKindSig ty' k, k)
271 kcHsType (HsTupleTy Boxed tys)
272 = mappM kcLiftedType tys `thenM` \ tys' ->
273 returnM (HsTupleTy Boxed tys', liftedTypeKind)
275 kcHsType (HsTupleTy Unboxed tys)
276 = mappM kcTypeType tys `thenM` \ tys' ->
277 returnM (HsTupleTy Unboxed tys', unliftedTypeKind)
279 kcHsType (HsFunTy ty1 ty2)
280 = kcTypeType ty1 `thenM` \ ty1' ->
281 kcTypeType ty2 `thenM` \ ty2' ->
282 returnM (HsFunTy ty1' ty2', liftedTypeKind)
284 kcHsType ty@(HsOpTy ty1 op ty2)
285 = kcTyVar op `thenM` \ op_kind ->
286 kcApps op_kind (ppr op) [ty1,ty2] `thenM` \ ([ty1',ty2'], res_kind) ->
287 returnM (HsOpTy ty1' op ty2', res_kind)
289 kcHsType ty@(HsAppTy ty1 ty2)
290 = kcHsType fun_ty `thenM` \ (fun_ty', fun_kind) ->
291 kcApps fun_kind (ppr fun_ty) arg_tys `thenM` \ (arg_tys', res_kind) ->
292 returnM (foldl HsAppTy fun_ty' arg_tys', res_kind)
294 (fun_ty, arg_tys) = split ty1 [ty2]
295 split (HsAppTy f a) as = split f (a:as)
298 kcHsType (HsPredTy pred)
299 = kcHsPred pred `thenM` \ pred' ->
300 returnM (HsPredTy pred', liftedTypeKind)
302 kcHsType (HsForAllTy exp tv_names context ty)
303 = kcHsTyVars tv_names $ \ tv_names' ->
304 kcHsContext context `thenM` \ ctxt' ->
305 kcLiftedType ty `thenM` \ ty' ->
306 -- The body of a forall must be a type, but in principle
307 -- there's no reason to prohibit *unlifted* types.
308 -- In fact, GHC can itself construct a function with an
309 -- unboxed tuple inside a for-all (via CPR analyis; see
310 -- typecheck/should_compile/tc170)
312 -- Still, that's only for internal interfaces, which aren't
313 -- kind-checked, and it's a bit inconvenient to use kcTypeType
314 -- here (because it doesn't return the result kind), so I'm
315 -- leaving it as lifted types for now.
316 returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
318 ---------------------------
319 kcApps :: TcKind -- Function kind
321 -> [HsType Name] -- Arg types
322 -> TcM ([HsType Name], TcKind) -- Kind-checked args
323 kcApps fun_kind ppr_fun args
324 = split_fk fun_kind (length args) `thenM` \ (arg_kinds, res_kind) ->
325 mappM kc_arg (args `zip` arg_kinds) `thenM` \ args' ->
326 returnM (args', res_kind)
328 split_fk fk 0 = returnM ([], fk)
329 split_fk fk n = unifyFunKind fk `thenM` \ mb_fk ->
331 Nothing -> failWithTc too_many_args
332 Just (ak,fk') -> split_fk fk' (n-1) `thenM` \ (aks, rk) ->
335 kc_arg (arg, arg_kind) = kcCheckHsType arg arg_kind
337 too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
338 ptext SLIT("is applied to too many type arguments")
340 ---------------------------
341 kcHsContext :: HsContext Name -> TcM (HsContext Name)
342 kcHsContext ctxt = mappM kcHsPred ctxt
344 kcHsPred pred -- Checks that the result is of kind liftedType
345 = kc_pred pred `thenM` \ (pred', kind) ->
346 checkExpectedKind (ppr pred) kind liftedTypeKind `thenM_`
349 ---------------------------
350 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
351 -- Does *not* check for a saturated
352 -- application (reason: used from TcDeriv)
353 kc_pred pred@(HsIParam name ty)
354 = kcHsType ty `thenM` \ (ty', kind) ->
355 returnM (HsIParam name ty', kind)
357 kc_pred pred@(HsClassP cls tys)
358 = kcClass cls `thenM` \ kind ->
359 kcApps kind (ppr cls) tys `thenM` \ (tys', res_kind) ->
360 returnM (HsClassP cls tys', res_kind)
362 ---------------------------
363 kcTyVar :: Name -> TcM TcKind
364 kcTyVar name -- Could be a tyvar or a tycon
365 = tcLookup name `thenM` \ thing ->
367 ATyVar tv -> returnM (tyVarKind tv)
368 ARecTyCon kind -> returnM kind
369 AGlobal (ATyCon tc) -> returnM (tyConKind tc)
370 other -> failWithTc (wrongThingErr "type" thing name)
372 kcClass :: Name -> TcM TcKind
373 kcClass cls -- Must be a class
374 = tcLookup cls `thenM` \ thing ->
376 ARecClass kind -> returnM kind
377 AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls))
378 other -> failWithTc (wrongThingErr "class" thing cls)
385 ---------------------------
386 -- We would like to get a decent error message from
387 -- (a) Under-applied type constructors
388 -- f :: (Maybe, Maybe)
389 -- (b) Over-applied type constructors
390 -- f :: Int x -> Int x
394 checkExpectedKind :: SDoc -> TcKind -> TcKind -> TcM TcKind
395 -- A fancy wrapper for 'unifyKind', which tries to give
396 -- decent error messages.
397 -- Returns the same kind that it is passed, exp_kind
398 checkExpectedKind pp_ty act_kind exp_kind
399 | act_kind `eqKind` exp_kind -- Short cut for a very common case
402 = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
404 Just _ -> returnM exp_kind ; -- Unification succeeded
407 -- So there's definitely an error
408 -- Now to find out what sort
409 zonkTcType exp_kind `thenM` \ exp_kind ->
410 zonkTcType act_kind `thenM` \ act_kind ->
412 let (exp_as, _) = Type.splitFunTys exp_kind
413 (act_as, _) = Type.splitFunTys act_kind
414 -- Use the Type versions for kinds
415 n_exp_as = length exp_as
416 n_act_as = length act_as
418 err | n_exp_as < n_act_as -- E.g. [Maybe]
419 = quotes pp_ty <+> ptext SLIT("is not applied to enough type arguments")
421 -- Now n_exp_as >= n_act_as. In the next two cases,
422 -- n_exp_as == 0, and hence so is n_act_as
423 | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
424 = ptext SLIT("Expecting a lifted type, but") <+> quotes pp_ty
425 <+> ptext SLIT("is unlifted")
427 | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
428 = ptext SLIT("Expecting an unlifted type, but") <+> quotes pp_ty
429 <+> ptext SLIT("is lifted")
431 | otherwise -- E.g. Monad [Int]
432 = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
433 ptext SLIT("but") <+> quotes pp_ty <+>
434 ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
436 failWithTc (ptext SLIT("Kind error:") <+> err)
440 %************************************************************************
444 %************************************************************************
448 * Transforms from HsType to Type
451 It cannot fail, and does no validity checking
454 dsHsType :: HsType Name -- All HsTyVarBndrs are kind-annotated
457 dsHsType ty@(HsTyVar name)
460 dsHsType (HsParTy ty) -- Remove the parentheses markers
463 dsHsType (HsKindSig ty k)
464 = dsHsType ty -- Kind checking done already
466 dsHsType (HsListTy ty)
467 = dsHsType ty `thenM` \ tau_ty ->
468 returnM (mkListTy tau_ty)
470 dsHsType (HsPArrTy ty)
471 = dsHsType ty `thenM` \ tau_ty ->
472 returnM (mkPArrTy tau_ty)
474 dsHsType (HsTupleTy boxity tys)
475 = dsHsTypes tys `thenM` \ tau_tys ->
476 returnM (mkTupleTy boxity (length tys) tau_tys)
478 dsHsType (HsFunTy ty1 ty2)
479 = dsHsType ty1 `thenM` \ tau_ty1 ->
480 dsHsType ty2 `thenM` \ tau_ty2 ->
481 returnM (mkFunTy tau_ty1 tau_ty2)
483 dsHsType (HsOpTy ty1 op ty2)
484 = dsHsType ty1 `thenM` \ tau_ty1 ->
485 dsHsType ty2 `thenM` \ tau_ty2 ->
486 ds_var_app op [tau_ty1,tau_ty2]
490 tcLookupTyCon genUnitTyConName `thenM` \ tc ->
491 returnM (mkTyConApp tc [])
493 dsHsType ty@(HsAppTy ty1 ty2)
496 dsHsType (HsPredTy pred)
497 = dsHsPred pred `thenM` \ pred' ->
498 returnM (mkPredTy pred')
500 dsHsType full_ty@(HsForAllTy exp tv_names ctxt ty)
501 = tcTyVarBndrs tv_names $ \ tyvars ->
502 mappM dsHsPred ctxt `thenM` \ theta ->
503 dsHsType ty `thenM` \ tau ->
504 returnM (mkSigmaTy tyvars theta tau)
506 dsHsTypes arg_tys = mappM dsHsType arg_tys
509 Help functions for type applications
510 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
513 ds_app :: HsType Name -> [HsType Name] -> TcM Type
514 ds_app (HsAppTy ty1 ty2) tys
515 = ds_app ty1 (ty2:tys)
518 = dsHsTypes tys `thenM` \ arg_tys ->
520 HsTyVar fun -> ds_var_app fun arg_tys
521 other -> dsHsType ty `thenM` \ fun_ty ->
522 returnM (mkAppTys fun_ty arg_tys)
524 ds_var_app :: Name -> [Type] -> TcM Type
525 ds_var_app name arg_tys
526 = tcLookup name `thenM` \ thing ->
528 ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
529 AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
530 ARecTyCon _ -> tcLookupTyCon name `thenM` \ tc ->
531 returnM (mkGenTyConApp tc arg_tys)
532 other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
539 dsHsPred :: HsPred Name -> TcM PredType
540 dsHsPred pred@(HsClassP class_name tys)
541 = dsHsTypes tys `thenM` \ arg_tys ->
542 tcLookupClass class_name `thenM` \ clas ->
543 returnM (ClassP clas arg_tys)
545 dsHsPred (HsIParam name ty)
546 = dsHsType ty `thenM` \ arg_ty ->
547 returnM (IParam name arg_ty)
551 %************************************************************************
553 Type-variable binders
555 %************************************************************************
559 kcHsTyVars :: [HsTyVarBndr Name]
560 -> ([HsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
561 -- They scope over the thing inside
563 kcHsTyVars tvs thing_inside
564 = mappM kcHsTyVar tvs `thenM` \ bndrs ->
565 tcExtendTyVarKindEnv bndrs $
568 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
569 -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
570 kcHsTyVar (UserTyVar name) = newKindVar `thenM` \ kind ->
571 returnM (KindedTyVar name kind)
572 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
575 tcTyVarBndrs :: [HsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
576 -> ([TyVar] -> TcM r)
578 -- Used when type-checking types/classes/type-decls
579 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
580 tcTyVarBndrs bndrs thing_inside
581 = mapM zonk bndrs `thenM` \ tyvars ->
582 tcExtendTyVarEnv tyvars (thing_inside tyvars)
584 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
585 returnM (mkTyVar name kind')
586 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
587 returnM (mkTyVar name liftedTypeKind)
591 %************************************************************************
593 Scoped type variables
595 %************************************************************************
598 tcAddScopedTyVars is used for scoped type variables added by pattern
600 e.g. \ ((x::a), (y::a)) -> x+y
601 They never have explicit kinds (because this is source-code only)
602 They are mutable (because they can get bound to a more specific type).
604 Usually we kind-infer and expand type splices, and then
605 tupecheck/desugar the type. That doesn't work well for scoped type
606 variables, because they scope left-right in patterns. (e.g. in the
607 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
609 The current not-very-good plan is to
610 * find all the types in the patterns
611 * find their free tyvars
613 * bring the kinded type vars into scope
614 * BUT throw away the kind-checked type
615 (we'll kind-check it again when we type-check the pattern)
617 This is bad because throwing away the kind checked type throws away
618 its splices. But too bad for now. [July 03]
621 We no longer specify that these type variables must be univerally
622 quantified (lots of email on the subject). If you want to put that
624 a) Do a checkSigTyVars after thing_inside
625 b) More insidiously, don't pass in expected_ty, else
626 we unify with it too early and checkSigTyVars barfs
627 Instead you have to pass in a fresh ty var, and unify
628 it with expected_ty afterwards
631 tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
632 tcAddScopedTyVars [] thing_inside
633 = thing_inside -- Quick get-out for the empty case
635 tcAddScopedTyVars sig_tys thing_inside
636 = getInLocalScope `thenM` \ in_scope ->
638 sig_tvs = [ UserTyVar n | ty <- sig_tys,
639 n <- nameSetToList (extractHsTyVars ty),
641 -- The tyvars we want are the free type variables of
642 -- the type that are not already in scope
644 -- Behave like kcHsType on a ForAll type
645 -- i.e. make kinded tyvars with mutable kinds,
646 -- and kind-check the enclosed types
647 kcHsTyVars sig_tvs (\ kinded_tvs -> do
648 { mappM kcTypeType sig_tys
649 ; return kinded_tvs }) `thenM` \ kinded_tvs ->
651 -- Zonk the mutable kinds and bring the tyvars into scope
652 -- Rather like tcTyVarBndrs, except that it brings *mutable*
653 -- tyvars into scope, not immutable ones
655 -- Furthermore, the tyvars are PatSigTvs, which means that we get better
656 -- error messages when type variables escape:
657 -- Inferred type is less polymorphic than expected
658 -- Quantified type variable `t' escapes
659 -- It is mentioned in the environment:
660 -- t is bound by the pattern type signature at tcfail103.hs:6
661 mapM zonk kinded_tvs `thenM` \ tyvars ->
662 tcExtendTyVarEnv tyvars thing_inside
665 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
666 newMutTyVar name kind' PatSigTv
667 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
668 returnM (mkTyVar name liftedTypeKind)
672 %************************************************************************
674 \subsection{Signatures}
676 %************************************************************************
678 @tcSigs@ checks the signatures for validity, and returns a list of
679 {\em freshly-instantiated} signatures. That is, the types are already
680 split up, and have fresh type variables installed. All non-type-signature
681 "RenamedSigs" are ignored.
683 The @TcSigInfo@ contains @TcTypes@ because they are unified with
684 the variable's type, and after that checked to see whether they've
690 TcId -- *Polymorphic* binder for this value...
697 TcId -- *Monomorphic* binder for this value
698 -- Does *not* have name = N
701 [Inst] -- Empty if theta is null, or
702 -- (method mono_id) otherwise
704 SrcLoc -- Of the signature
706 instance Outputable TcSigInfo where
707 ppr (TySigInfo id tyvars theta tau _ inst loc) =
708 ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
710 tcSigPolyId :: TcSigInfo -> TcId
711 tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
713 tcSigMonoId :: TcSigInfo -> TcId
714 tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
716 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
717 -- Search for a particular signature
718 maybeSig [] name = Nothing
719 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
720 | name == idName sig_id = Just sig
721 | otherwise = maybeSig sigs name
726 tcTySig :: RenamedSig -> TcM TcSigInfo
728 tcTySig (Sig v ty src_loc)
729 = addSrcLoc src_loc $
730 tcHsSigType (FunSigCtxt v) ty `thenM` \ sigma_tc_ty ->
731 mkTcSig (mkLocalId v sigma_tc_ty) `thenM` \ sig ->
734 mkTcSig :: TcId -> TcM TcSigInfo
736 = -- Instantiate this type
737 -- It's important to do this even though in the error-free case
738 -- we could just split the sigma_tc_ty (since the tyvars don't
739 -- unified with anything). But in the case of an error, when
740 -- the tyvars *do* get unified with something, we want to carry on
741 -- typechecking the rest of the program with the function bound
742 -- to a pristine type, namely sigma_tc_ty
743 tcInstType SigTv (idType poly_id) `thenM` \ (tyvars', theta', tau') ->
745 getInstLoc SignatureOrigin `thenM` \ inst_loc ->
746 newMethod inst_loc poly_id
748 theta' tau' `thenM` \ inst ->
749 -- We make a Method even if it's not overloaded; no harm
750 -- But do not extend the LIE! We're just making an Id.
752 getSrcLocM `thenM` \ src_loc ->
753 returnM (TySigInfo poly_id tyvars' theta' tau'
754 (instToId inst) [inst] src_loc)
758 %************************************************************************
760 \subsection{Errors and contexts}
762 %************************************************************************
766 hoistForAllTys :: Type -> Type
767 -- Used for user-written type signatures only
768 -- Move all the foralls and constraints to the top
769 -- e.g. T -> forall a. a ==> forall a. T -> a
770 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
772 -- Also: eliminate duplicate constraints. These can show up
773 -- when hoisting constraints, notably implicit parameters.
775 -- We want to 'look through' type synonyms when doing this
776 -- so it's better done on the Type than the HsType
780 no_shadow_ty = deShadowTy ty
781 -- Running over ty with an empty substitution gives it the
782 -- no-shadowing property. This is important. For example:
783 -- type Foo r = forall a. a -> r
784 -- foo :: Foo (Foo ())
785 -- Here the hoisting should give
786 -- foo :: forall a a1. a -> a1 -> ()
788 -- What about type vars that are lexically in scope in the envt?
789 -- We simply rely on them having a different unique to any
790 -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
791 -- out of the envt, which is boring and (I think) not necessary.
793 case hoist no_shadow_ty of
794 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
795 -- The 'nubBy' eliminates duplicate constraints,
796 -- notably implicit parameters
799 | (tvs1, body_ty) <- tcSplitForAllTys ty,
801 = case hoist body_ty of
802 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
804 | Just (arg, res) <- tcSplitFunTy_maybe ty
806 arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
807 in -- to the argument type
808 if (isPredTy arg') then
810 (tvs,theta,tau) -> (tvs, arg':theta, tau)
813 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
815 | otherwise = ([], [], ty)
819 %************************************************************************
821 \subsection{Errors and contexts}
823 %************************************************************************
826 wrongThingErr expected thing name
827 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
829 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
830 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
831 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
832 pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
833 pp_thing (ATyVar _) = ptext SLIT("Type variable")
834 pp_thing (ATcId _ _ _) = ptext SLIT("Local identifier")
835 pp_thing (ARecTyCon _) = ptext SLIT("Rec tycon")
836 pp_thing (ARecClass _) = ptext SLIT("Rec class")