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, pprKind )
47 import qualified Type ( splitFunTys )
48 import Inst ( Inst, InstOrigin(..), newMethod, instToId )
50 import Id ( mkLocalId, idName, idType )
51 import Var ( TyVar, mkTyVar, tyVarKind )
52 import TyCon ( TyCon, tyConKind )
53 import Class ( classTyCon )
56 import PrelNames ( genUnitTyConName )
57 import Subst ( deShadowTy )
58 import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy )
59 import BasicTypes ( Boxity(..) )
60 import SrcLoc ( SrcLoc )
66 ----------------------------
68 ----------------------------
70 Generally speaking we now type-check types in three phases
72 1. kcHsType: kind check the HsType
73 *includes* performing any TH type splices;
74 so it returns a translated, and kind-annotated, type
76 2. dsHsType: convert from HsType to Type:
78 expand type synonyms [mkGenTyApps]
79 hoist the foralls [tcHsType]
81 3. checkValidType: check the validity of the resulting type
83 Often these steps are done one after the other (tcHsSigType).
84 But in mutually recursive groups of type and class decls we do
85 1 kind-check the whole group
86 2 build TyCons/Classes in a knot-tied way
87 3 check the validity of types in the now-unknotted TyCons/Classes
89 For example, when we find
90 (forall a m. m a -> m a)
91 we bind a,m to kind varibles and kind-check (m a -> m a). This makes
92 a get kind *, and m get kind *->*. Now we typecheck (m a -> m a) in
93 an environment that binds a and m suitably.
95 The kind checker passed to tcHsTyVars needs to look at enough to
96 establish the kind of the tyvar:
97 * For a group of type and class decls, it's just the group, not
98 the rest of the program
99 * For a tyvar bound in a pattern type signature, its the types
100 mentioned in the other type signatures in that bunch of patterns
101 * For a tyvar bound in a RULE, it's the type signatures on other
102 universally quantified variables in the rule
104 Note that this may occasionally give surprising results. For example:
106 data T a b = MkT (a b)
108 Here we deduce a::*->*, b::*
109 But equally valid would be a::(*->*)-> *, b::*->*
114 Some of the validity check could in principle be done by the kind checker,
117 - During desugaring, we normalise by expanding type synonyms. Only
118 after this step can we check things like type-synonym saturation
119 e.g. type T k = k Int
121 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
122 and then S is saturated. This is a GHC extension.
124 - Similarly, also a GHC extension, we look through synonyms before complaining
125 about the form of a class or instance declaration
127 - Ambiguity checks involve functional dependencies, and it's easier to wait
128 until knots have been resolved before poking into them
130 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
131 finished building the loop. So to keep things simple, we postpone most validity
132 checking until step (3).
136 During step (1) we might fault in a TyCon defined in another module, and it might
137 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
138 knot around type declarations with ARecThing, so that the fault-in code can get
139 the TyCon being defined.
142 %************************************************************************
144 \subsection{Checking types}
146 %************************************************************************
149 tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
150 -- Do kind checking, and hoist for-alls to the top
151 tcHsSigType ctxt hs_ty
152 = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
153 do { kinded_ty <- kcTypeType hs_ty
154 ; ty <- tcHsKindedType kinded_ty
155 ; checkValidType ctxt ty
158 -- tcHsPred is happy with a partial application, e.g. (ST s)
161 = do { (kinded_pred,_) <- kc_pred pred -- kc_pred rather than kcHsPred
162 -- to avoid the partial application check
163 ; dsHsPred kinded_pred }
166 These functions are used during knot-tying in
167 type and class declarations, when we have to
168 separate kind-checking, desugaring, and validity checking
171 kcHsSigType, kcHsLiftedSigType :: HsType Name -> TcM (HsType Name)
172 -- Used for type signatures
173 kcHsSigType ty = kcTypeType ty
174 kcHsLiftedSigType ty = kcLiftedType ty
176 tcHsKindedType :: RenamedHsType -> TcM Type
177 -- Don't do kind checking, nor validity checking,
178 -- but do hoist for-alls to the top
179 -- This is used in type and class decls, where kinding is
180 -- done in advance, and validity checking is done later
181 -- [Validity checking done later because of knot-tying issues.]
183 = do { ty <- dsHsType hs_ty
184 ; return (hoistForAllTys ty) }
186 tcHsKindedContext :: RenamedContext -> TcM ThetaType
187 -- Used when we are expecting a ClassContext (i.e. no implicit params)
188 -- Does not do validity checking, like tcHsKindedType
189 tcHsKindedContext hs_theta = mappM dsHsPred hs_theta
193 %************************************************************************
195 The main kind checker: kcHsType
197 %************************************************************************
199 First a couple of simple wrappers for kcHsType
202 ---------------------------
203 kcLiftedType :: HsType Name -> TcM (HsType Name)
204 -- The type ty must be a *lifted* *type*
205 kcLiftedType ty = kcCheckHsType ty liftedTypeKind
207 ---------------------------
208 kcTypeType :: HsType Name -> TcM (HsType Name)
209 -- The type ty must be a *type*, but it can be lifted or unlifted
210 -- Be sure to use checkExpectedKind, rather than simply unifying
211 -- with (Type bx), because it gives better error messages
213 = kcHsType ty `thenM` \ (ty', kind) ->
214 if isTypeKind kind then
217 newOpenTypeKind `thenM` \ type_kind ->
218 traceTc (text "kcTypeType" $$ nest 2 (ppr ty $$ ppr ty' $$ ppr kind $$ ppr type_kind)) `thenM_`
219 checkExpectedKind (ppr ty) kind type_kind `thenM_`
222 ---------------------------
223 kcCheckHsType :: HsType Name -> TcKind -> TcM (HsType Name)
224 -- Check that the type has the specified kind
225 kcCheckHsType ty exp_kind
226 = kcHsType ty `thenM` \ (ty', act_kind) ->
227 checkExpectedKind (ppr ty) act_kind exp_kind `thenM_`
231 Here comes the main function
234 kcHsType :: HsType Name -> TcM (HsType Name, TcKind)
235 -- kcHsType *returns* the kind of the type, rather than taking an expected
236 -- kind as argument as tcExpr does.
238 -- (a) the kind of (->) is
239 -- forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
240 -- so we'd need to generate huge numbers of bx variables.
241 -- (b) kinds are so simple that the error messages are fine
243 -- The translated type has explicitly-kinded type-variable binders
245 kcHsType (HsParTy ty)
246 = kcHsType ty `thenM` \ (ty', kind) ->
247 returnM (HsParTy ty', kind)
249 kcHsType (HsTyVar name)
250 = kcTyVar name `thenM` \ kind ->
251 returnM (HsTyVar name, kind)
253 kcHsType (HsListTy ty)
254 = kcLiftedType ty `thenM` \ ty' ->
255 returnM (HsListTy ty', liftedTypeKind)
257 kcHsType (HsPArrTy ty)
258 = kcLiftedType ty `thenM` \ ty' ->
259 returnM (HsPArrTy ty', liftedTypeKind)
262 = returnM (HsNumTy n, liftedTypeKind)
264 kcHsType (HsKindSig ty k)
265 = kcCheckHsType ty k `thenM` \ ty' ->
266 returnM (HsKindSig ty' k, k)
268 kcHsType (HsTupleTy Boxed tys)
269 = mappM kcLiftedType tys `thenM` \ tys' ->
270 returnM (HsTupleTy Boxed tys', liftedTypeKind)
272 kcHsType (HsTupleTy Unboxed tys)
273 = mappM kcTypeType tys `thenM` \ tys' ->
274 returnM (HsTupleTy Unboxed tys', unliftedTypeKind)
276 kcHsType (HsFunTy ty1 ty2)
277 = kcTypeType ty1 `thenM` \ ty1' ->
278 kcTypeType ty2 `thenM` \ ty2' ->
279 returnM (HsFunTy ty1' ty2', liftedTypeKind)
281 kcHsType ty@(HsOpTy ty1 op ty2)
282 = kcTyVar op `thenM` \ op_kind ->
283 kcApps op_kind (ppr op) [ty1,ty2] `thenM` \ ([ty1',ty2'], res_kind) ->
284 returnM (HsOpTy ty1' op ty2', res_kind)
286 kcHsType ty@(HsAppTy ty1 ty2)
287 = kcHsType fun_ty `thenM` \ (fun_ty', fun_kind) ->
288 kcApps fun_kind (ppr fun_ty) arg_tys `thenM` \ (arg_tys', res_kind) ->
289 returnM (foldl HsAppTy fun_ty' arg_tys', res_kind)
291 (fun_ty, arg_tys) = split ty1 [ty2]
292 split (HsAppTy f a) as = split f (a:as)
295 kcHsType (HsPredTy pred)
296 = kcHsPred pred `thenM` \ pred' ->
297 returnM (HsPredTy pred', liftedTypeKind)
299 kcHsType (HsForAllTy exp tv_names context ty)
300 = kcHsTyVars tv_names $ \ tv_names' ->
301 kcHsContext context `thenM` \ ctxt' ->
302 kcLiftedType ty `thenM` \ ty' ->
303 -- The body of a forall must be a type, but in principle
304 -- there's no reason to prohibit *unlifted* types.
305 -- In fact, GHC can itself construct a function with an
306 -- unboxed tuple inside a for-all (via CPR analyis; see
307 -- typecheck/should_compile/tc170)
309 -- Still, that's only for internal interfaces, which aren't
310 -- kind-checked, and it's a bit inconvenient to use kcTypeType
311 -- here (because it doesn't return the result kind), so I'm
312 -- leaving it as lifted types for now.
313 returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
315 ---------------------------
316 kcApps :: TcKind -- Function kind
318 -> [HsType Name] -- Arg types
319 -> TcM ([HsType Name], TcKind) -- Kind-checked args
320 kcApps fun_kind ppr_fun args
321 = split_fk fun_kind (length args) `thenM` \ (arg_kinds, res_kind) ->
322 mappM kc_arg (args `zip` arg_kinds) `thenM` \ args' ->
323 returnM (args', res_kind)
325 split_fk fk 0 = returnM ([], fk)
326 split_fk fk n = unifyFunKind fk `thenM` \ mb_fk ->
328 Nothing -> failWithTc too_many_args
329 Just (ak,fk') -> split_fk fk' (n-1) `thenM` \ (aks, rk) ->
332 kc_arg (arg, arg_kind) = kcCheckHsType arg arg_kind
334 too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
335 ptext SLIT("is applied to too many type arguments")
337 ---------------------------
338 kcHsContext :: HsContext Name -> TcM (HsContext Name)
339 kcHsContext ctxt = mappM kcHsPred ctxt
341 kcHsPred pred -- Checks that the result is of kind liftedType
342 = kc_pred pred `thenM` \ (pred', kind) ->
343 checkExpectedKind (ppr pred) kind liftedTypeKind `thenM_`
346 ---------------------------
347 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
348 -- Does *not* check for a saturated
349 -- application (reason: used from TcDeriv)
350 kc_pred pred@(HsIParam name ty)
351 = kcHsType ty `thenM` \ (ty', kind) ->
352 returnM (HsIParam name ty', kind)
354 kc_pred pred@(HsClassP cls tys)
355 = kcClass cls `thenM` \ kind ->
356 kcApps kind (ppr cls) tys `thenM` \ (tys', res_kind) ->
357 returnM (HsClassP cls tys', res_kind)
359 ---------------------------
360 kcTyVar :: Name -> TcM TcKind
361 kcTyVar name -- Could be a tyvar or a tycon
362 = tcLookup name `thenM` \ thing ->
364 ATyVar tv -> returnM (tyVarKind tv)
365 ARecTyCon kind -> returnM kind
366 AGlobal (ATyCon tc) -> returnM (tyConKind tc)
367 other -> failWithTc (wrongThingErr "type" thing name)
369 kcClass :: Name -> TcM TcKind
370 kcClass cls -- Must be a class
371 = tcLookup cls `thenM` \ thing ->
373 ARecClass kind -> returnM kind
374 AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls))
375 other -> failWithTc (wrongThingErr "class" thing cls)
382 ---------------------------
383 -- We would like to get a decent error message from
384 -- (a) Under-applied type constructors
385 -- f :: (Maybe, Maybe)
386 -- (b) Over-applied type constructors
387 -- f :: Int x -> Int x
391 checkExpectedKind :: SDoc -> TcKind -> TcKind -> TcM TcKind
392 -- A fancy wrapper for 'unifyKind', which tries to give
393 -- decent error messages.
394 -- Returns the same kind that it is passed, exp_kind
395 checkExpectedKind pp_ty act_kind exp_kind
396 | act_kind `eqKind` exp_kind -- Short cut for a very common case
399 = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
401 Just _ -> returnM exp_kind ; -- Unification succeeded
404 -- So there's definitely an error
405 -- Now to find out what sort
406 zonkTcType exp_kind `thenM` \ exp_kind ->
407 zonkTcType act_kind `thenM` \ act_kind ->
409 let (exp_as, _) = Type.splitFunTys exp_kind
410 (act_as, _) = Type.splitFunTys act_kind
411 -- Use the Type versions for kinds
412 n_exp_as = length exp_as
413 n_act_as = length act_as
415 err | n_exp_as < n_act_as -- E.g. [Maybe]
416 = quotes pp_ty <+> ptext SLIT("is not applied to enough type arguments")
418 -- Now n_exp_as >= n_act_as. In the next two cases,
419 -- n_exp_as == 0, and hence so is n_act_as
420 | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
421 = ptext SLIT("Expecting a lifted type, but") <+> quotes pp_ty
422 <+> ptext SLIT("is unlifted")
424 | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
425 = ptext SLIT("Expecting an unlifted type, but") <+> quotes pp_ty
426 <+> ptext SLIT("is lifted")
428 | otherwise -- E.g. Monad [Int]
429 = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
430 ptext SLIT("but") <+> quotes pp_ty <+>
431 ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
433 failWithTc (ptext SLIT("Kind error:") <+> err)
437 %************************************************************************
441 %************************************************************************
445 * Transforms from HsType to Type
448 It cannot fail, and does no validity checking
451 dsHsType :: HsType Name -- All HsTyVarBndrs are kind-annotated
454 dsHsType ty@(HsTyVar name)
457 dsHsType (HsParTy ty) -- Remove the parentheses markers
460 dsHsType (HsKindSig ty k)
461 = dsHsType ty -- Kind checking done already
463 dsHsType (HsListTy ty)
464 = dsHsType ty `thenM` \ tau_ty ->
465 returnM (mkListTy tau_ty)
467 dsHsType (HsPArrTy ty)
468 = dsHsType ty `thenM` \ tau_ty ->
469 returnM (mkPArrTy tau_ty)
471 dsHsType (HsTupleTy boxity tys)
472 = dsHsTypes tys `thenM` \ tau_tys ->
473 returnM (mkTupleTy boxity (length tys) tau_tys)
475 dsHsType (HsFunTy ty1 ty2)
476 = dsHsType ty1 `thenM` \ tau_ty1 ->
477 dsHsType ty2 `thenM` \ tau_ty2 ->
478 returnM (mkFunTy tau_ty1 tau_ty2)
480 dsHsType (HsOpTy ty1 op ty2)
481 = dsHsType ty1 `thenM` \ tau_ty1 ->
482 dsHsType ty2 `thenM` \ tau_ty2 ->
483 ds_var_app op [tau_ty1,tau_ty2]
487 tcLookupTyCon genUnitTyConName `thenM` \ tc ->
488 returnM (mkTyConApp tc [])
490 dsHsType ty@(HsAppTy ty1 ty2)
493 dsHsType (HsPredTy pred)
494 = dsHsPred pred `thenM` \ pred' ->
495 returnM (mkPredTy pred')
497 dsHsType full_ty@(HsForAllTy exp tv_names ctxt ty)
498 = tcTyVarBndrs tv_names $ \ tyvars ->
499 mappM dsHsPred ctxt `thenM` \ theta ->
500 dsHsType ty `thenM` \ tau ->
501 returnM (mkSigmaTy tyvars theta tau)
503 dsHsTypes arg_tys = mappM dsHsType arg_tys
506 Help functions for type applications
507 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
510 ds_app :: HsType Name -> [HsType Name] -> TcM Type
511 ds_app (HsAppTy ty1 ty2) tys
512 = ds_app ty1 (ty2:tys)
515 = dsHsTypes tys `thenM` \ arg_tys ->
517 HsTyVar fun -> ds_var_app fun arg_tys
518 other -> dsHsType ty `thenM` \ fun_ty ->
519 returnM (mkAppTys fun_ty arg_tys)
521 ds_var_app :: Name -> [Type] -> TcM Type
522 ds_var_app name arg_tys
523 = tcLookup name `thenM` \ thing ->
525 ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
526 AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
527 ARecTyCon _ -> tcLookupTyCon name `thenM` \ tc ->
528 returnM (mkGenTyConApp tc arg_tys)
529 other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
536 dsHsPred :: HsPred Name -> TcM PredType
537 dsHsPred pred@(HsClassP class_name tys)
538 = dsHsTypes tys `thenM` \ arg_tys ->
539 tcLookupClass class_name `thenM` \ clas ->
540 returnM (ClassP clas arg_tys)
542 dsHsPred (HsIParam name ty)
543 = dsHsType ty `thenM` \ arg_ty ->
544 returnM (IParam name arg_ty)
548 %************************************************************************
550 Type-variable binders
552 %************************************************************************
556 kcHsTyVars :: [HsTyVarBndr Name]
557 -> ([HsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
558 -- They scope over the thing inside
560 kcHsTyVars tvs thing_inside
561 = mappM kcHsTyVar tvs `thenM` \ bndrs ->
562 tcExtendTyVarKindEnv bndrs $
565 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
566 -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
567 kcHsTyVar (UserTyVar name) = newKindVar `thenM` \ kind ->
568 returnM (KindedTyVar name kind)
569 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
572 tcTyVarBndrs :: [HsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
573 -> ([TyVar] -> TcM r)
575 -- Used when type-checking types/classes/type-decls
576 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
577 tcTyVarBndrs bndrs thing_inside
578 = mapM zonk bndrs `thenM` \ tyvars ->
579 tcExtendTyVarEnv tyvars (thing_inside tyvars)
581 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
582 returnM (mkTyVar name kind')
583 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
584 returnM (mkTyVar name liftedTypeKind)
588 %************************************************************************
590 Scoped type variables
592 %************************************************************************
595 tcAddScopedTyVars is used for scoped type variables added by pattern
597 e.g. \ ((x::a), (y::a)) -> x+y
598 They never have explicit kinds (because this is source-code only)
599 They are mutable (because they can get bound to a more specific type).
601 Usually we kind-infer and expand type splices, and then
602 tupecheck/desugar the type. That doesn't work well for scoped type
603 variables, because they scope left-right in patterns. (e.g. in the
604 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
606 The current not-very-good plan is to
607 * find all the types in the patterns
608 * find their free tyvars
610 * bring the kinded type vars into scope
611 * BUT throw away the kind-checked type
612 (we'll kind-check it again when we type-check the pattern)
614 This is bad because throwing away the kind checked type throws away
615 its splices. But too bad for now. [July 03]
618 We no longer specify that these type variables must be univerally
619 quantified (lots of email on the subject). If you want to put that
621 a) Do a checkSigTyVars after thing_inside
622 b) More insidiously, don't pass in expected_ty, else
623 we unify with it too early and checkSigTyVars barfs
624 Instead you have to pass in a fresh ty var, and unify
625 it with expected_ty afterwards
628 tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
629 tcAddScopedTyVars [] thing_inside
630 = thing_inside -- Quick get-out for the empty case
632 tcAddScopedTyVars sig_tys thing_inside
633 = getInLocalScope `thenM` \ in_scope ->
635 sig_tvs = [ UserTyVar n | ty <- sig_tys,
636 n <- nameSetToList (extractHsTyVars ty),
638 -- The tyvars we want are the free type variables of
639 -- the type that are not already in scope
641 -- Behave like kcHsType on a ForAll type
642 -- i.e. make kinded tyvars with mutable kinds,
643 -- and kind-check the enclosed types
644 kcHsTyVars sig_tvs (\ kinded_tvs -> do
645 { mappM kcTypeType sig_tys
646 ; return kinded_tvs }) `thenM` \ kinded_tvs ->
648 -- Zonk the mutable kinds and bring the tyvars into scope
649 -- Rather like tcTyVarBndrs, except that it brings *mutable*
650 -- tyvars into scope, not immutable ones
652 -- Furthermore, the tyvars are PatSigTvs, which means that we get better
653 -- error messages when type variables escape:
654 -- Inferred type is less polymorphic than expected
655 -- Quantified type variable `t' escapes
656 -- It is mentioned in the environment:
657 -- t is bound by the pattern type signature at tcfail103.hs:6
658 mapM zonk kinded_tvs `thenM` \ tyvars ->
659 tcExtendTyVarEnv tyvars thing_inside
662 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
663 newMutTyVar name kind' PatSigTv
664 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
665 returnM (mkTyVar name liftedTypeKind)
669 %************************************************************************
671 \subsection{Signatures}
673 %************************************************************************
675 @tcSigs@ checks the signatures for validity, and returns a list of
676 {\em freshly-instantiated} signatures. That is, the types are already
677 split up, and have fresh type variables installed. All non-type-signature
678 "RenamedSigs" are ignored.
680 The @TcSigInfo@ contains @TcTypes@ because they are unified with
681 the variable's type, and after that checked to see whether they've
687 TcId -- *Polymorphic* binder for this value...
694 TcId -- *Monomorphic* binder for this value
695 -- Does *not* have name = N
698 [Inst] -- Empty if theta is null, or
699 -- (method mono_id) otherwise
701 SrcLoc -- Of the signature
703 instance Outputable TcSigInfo where
704 ppr (TySigInfo id tyvars theta tau _ inst loc) =
705 ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
707 tcSigPolyId :: TcSigInfo -> TcId
708 tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
710 tcSigMonoId :: TcSigInfo -> TcId
711 tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
713 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
714 -- Search for a particular signature
715 maybeSig [] name = Nothing
716 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
717 | name == idName sig_id = Just sig
718 | otherwise = maybeSig sigs name
723 tcTySig :: RenamedSig -> TcM TcSigInfo
725 tcTySig (Sig v ty src_loc)
726 = addSrcLoc src_loc $
727 tcHsSigType (FunSigCtxt v) ty `thenM` \ sigma_tc_ty ->
728 mkTcSig (mkLocalId v sigma_tc_ty) `thenM` \ sig ->
731 mkTcSig :: TcId -> TcM TcSigInfo
733 = -- Instantiate this type
734 -- It's important to do this even though in the error-free case
735 -- we could just split the sigma_tc_ty (since the tyvars don't
736 -- unified with anything). But in the case of an error, when
737 -- the tyvars *do* get unified with something, we want to carry on
738 -- typechecking the rest of the program with the function bound
739 -- to a pristine type, namely sigma_tc_ty
740 tcInstType SigTv (idType poly_id) `thenM` \ (tyvars', theta', tau') ->
742 getInstLoc SignatureOrigin `thenM` \ inst_loc ->
743 newMethod inst_loc poly_id
745 theta' tau' `thenM` \ inst ->
746 -- We make a Method even if it's not overloaded; no harm
747 -- But do not extend the LIE! We're just making an Id.
749 getSrcLocM `thenM` \ src_loc ->
750 returnM (TySigInfo poly_id tyvars' theta' tau'
751 (instToId inst) [inst] src_loc)
755 %************************************************************************
757 \subsection{Errors and contexts}
759 %************************************************************************
763 hoistForAllTys :: Type -> Type
764 -- Used for user-written type signatures only
765 -- Move all the foralls and constraints to the top
766 -- e.g. T -> forall a. a ==> forall a. T -> a
767 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
769 -- Also: eliminate duplicate constraints. These can show up
770 -- when hoisting constraints, notably implicit parameters.
772 -- We want to 'look through' type synonyms when doing this
773 -- so it's better done on the Type than the HsType
777 no_shadow_ty = deShadowTy ty
778 -- Running over ty with an empty substitution gives it the
779 -- no-shadowing property. This is important. For example:
780 -- type Foo r = forall a. a -> r
781 -- foo :: Foo (Foo ())
782 -- Here the hoisting should give
783 -- foo :: forall a a1. a -> a1 -> ()
785 -- What about type vars that are lexically in scope in the envt?
786 -- We simply rely on them having a different unique to any
787 -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
788 -- out of the envt, which is boring and (I think) not necessary.
790 case hoist no_shadow_ty of
791 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
792 -- The 'nubBy' eliminates duplicate constraints,
793 -- notably implicit parameters
796 | (tvs1, body_ty) <- tcSplitForAllTys ty,
798 = case hoist body_ty of
799 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
801 | Just (arg, res) <- tcSplitFunTy_maybe ty
803 arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
804 in -- to the argument type
805 if (isPredTy arg') then
807 (tvs,theta,tau) -> (tvs, arg':theta, tau)
810 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
812 | otherwise = ([], [], ty)
816 %************************************************************************
818 \subsection{Errors and contexts}
820 %************************************************************************
823 wrongThingErr expected thing name
824 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
826 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
827 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
828 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
829 pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
830 pp_thing (ATyVar _) = ptext SLIT("Type variable")
831 pp_thing (ATcId _ _ _) = ptext SLIT("Local identifier")
832 pp_thing (ARecTyCon _) = ptext SLIT("Rec tycon")
833 pp_thing (ARecClass _) = ptext SLIT("Rec class")