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,
47 pprKind, pprThetaArrow )
48 import qualified Type ( splitFunTys )
49 import Inst ( Inst, InstOrigin(..), newMethod, instToId )
51 import Id ( mkLocalId, idName, idType )
52 import Var ( TyVar, mkTyVar, tyVarKind )
53 import ErrUtils ( Message )
54 import TyCon ( TyCon, tyConKind )
55 import Class ( classTyCon )
58 import PrelNames ( genUnitTyConName )
59 import Subst ( deShadowTy )
60 import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy )
61 import BasicTypes ( Boxity(..) )
62 import SrcLoc ( SrcLoc )
68 ----------------------------
70 ----------------------------
72 Generally speaking we now type-check types in three phases
74 1. kcHsType: kind check the HsType
75 *includes* performing any TH type splices;
76 so it returns a translated, and kind-annotated, type
78 2. dsHsType: convert from HsType to Type:
80 expand type synonyms [mkGenTyApps]
81 hoist the foralls [tcHsType]
83 3. checkValidType: check the validity of the resulting type
85 Often these steps are done one after the other (tcHsSigType).
86 But in mutually recursive groups of type and class decls we do
87 1 kind-check the whole group
88 2 build TyCons/Classes in a knot-tied way
89 3 check the validity of types in the now-unknotted TyCons/Classes
91 For example, when we find
92 (forall a m. m a -> m a)
93 we bind a,m to kind varibles and kind-check (m a -> m a). This makes
94 a get kind *, and m get kind *->*. Now we typecheck (m a -> m a) in
95 an environment that binds a and m suitably.
97 The kind checker passed to tcHsTyVars needs to look at enough to
98 establish the kind of the tyvar:
99 * For a group of type and class decls, it's just the group, not
100 the rest of the program
101 * For a tyvar bound in a pattern type signature, its the types
102 mentioned in the other type signatures in that bunch of patterns
103 * For a tyvar bound in a RULE, it's the type signatures on other
104 universally quantified variables in the rule
106 Note that this may occasionally give surprising results. For example:
108 data T a b = MkT (a b)
110 Here we deduce a::*->*, b::*
111 But equally valid would be a::(*->*)-> *, b::*->*
116 Some of the validity check could in principle be done by the kind checker,
119 - During desugaring, we normalise by expanding type synonyms. Only
120 after this step can we check things like type-synonym saturation
121 e.g. type T k = k Int
123 Then (T S) is ok, because T is saturated; (T S) expands to (S Int);
124 and then S is saturated. This is a GHC extension.
126 - Similarly, also a GHC extension, we look through synonyms before complaining
127 about the form of a class or instance declaration
129 - Ambiguity checks involve functional dependencies, and it's easier to wait
130 until knots have been resolved before poking into them
132 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
133 finished building the loop. So to keep things simple, we postpone most validity
134 checking until step (3).
138 During step (1) we might fault in a TyCon defined in another module, and it might
139 (via a loop) refer back to a TyCon defined in this module. So when we tie a big
140 knot around type declarations with ARecThing, so that the fault-in code can get
141 the TyCon being defined.
144 %************************************************************************
146 \subsection{Checking types}
148 %************************************************************************
151 tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
152 -- Do kind checking, and hoist for-alls to the top
153 tcHsSigType ctxt hs_ty
154 = addErrCtxt (pprHsSigCtxt ctxt hs_ty) $
155 do { kinded_ty <- kcTypeType hs_ty
156 ; ty <- tcHsKindedType kinded_ty
157 ; checkValidType ctxt ty
160 -- tcHsPred is happy with a partial application, e.g. (ST s)
163 = do { (kinded_pred,_) <- kc_pred pred -- kc_pred rather than kcHsPred
164 -- to avoid the partial application check
165 ; dsHsPred kinded_pred }
168 These functions are used during knot-tying in
169 type and class declarations, when we have to
170 separate kind-checking, desugaring, and validity checking
173 kcHsSigType, kcHsLiftedSigType :: HsType Name -> TcM (HsType Name)
174 -- Used for type signatures
175 kcHsSigType ty = kcTypeType ty
176 kcHsLiftedSigType ty = kcLiftedType ty
178 tcHsKindedType :: RenamedHsType -> TcM Type
179 -- Don't do kind checking, nor validity checking,
180 -- but do hoist for-alls to the top
181 -- This is used in type and class decls, where kinding is
182 -- done in advance, and validity checking is done later
183 -- [Validity checking done later because of knot-tying issues.]
185 = do { ty <- dsHsType hs_ty
186 ; return (hoistForAllTys ty) }
188 tcHsKindedContext :: RenamedContext -> TcM ThetaType
189 -- Used when we are expecting a ClassContext (i.e. no implicit params)
190 -- Does not do validity checking, like tcHsKindedType
191 tcHsKindedContext hs_theta = mappM dsHsPred hs_theta
195 %************************************************************************
197 The main kind checker: kcHsType
199 %************************************************************************
201 First a couple of simple wrappers for kcHsType
204 ---------------------------
205 kcLiftedType :: HsType Name -> TcM (HsType Name)
206 -- The type ty must be a *lifted* *type*
207 kcLiftedType ty = kcCheckHsType ty liftedTypeKind
209 ---------------------------
210 kcTypeType :: HsType Name -> TcM (HsType Name)
211 -- The type ty must be a *type*, but it can be lifted or unlifted
212 -- Be sure to use checkExpectedKind, rather than simply unifying
213 -- with (Type bx), because it gives better error messages
215 = kcHsType ty `thenM` \ (ty', kind) ->
216 if isTypeKind kind then
219 newOpenTypeKind `thenM` \ type_kind ->
220 traceTc (text "kcTypeType" $$ nest 2 (ppr ty $$ ppr ty' $$ ppr kind $$ ppr type_kind)) `thenM_`
221 checkExpectedKind (ppr ty) kind type_kind `thenM_`
224 ---------------------------
225 kcCheckHsType :: HsType Name -> TcKind -> TcM (HsType Name)
226 -- Check that the type has the specified kind
227 kcCheckHsType ty exp_kind
228 = kcHsType ty `thenM` \ (ty', act_kind) ->
229 checkExpectedKind (ppr ty) act_kind exp_kind `thenM_`
233 Here comes the main function
236 kcHsType :: HsType Name -> TcM (HsType Name, TcKind)
237 -- kcHsType *returns* the kind of the type, rather than taking an expected
238 -- kind as argument as tcExpr does.
240 -- (a) the kind of (->) is
241 -- forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
242 -- so we'd need to generate huge numbers of bx variables.
243 -- (b) kinds are so simple that the error messages are fine
245 -- The translated type has explicitly-kinded type-variable binders
247 kcHsType (HsParTy ty)
248 = kcHsType ty `thenM` \ (ty', kind) ->
249 returnM (HsParTy ty', kind)
251 kcHsType (HsTyVar name)
252 = kcTyVar name `thenM` \ kind ->
253 returnM (HsTyVar name, kind)
255 kcHsType (HsListTy ty)
256 = kcLiftedType ty `thenM` \ ty' ->
257 returnM (HsListTy ty', liftedTypeKind)
259 kcHsType (HsPArrTy ty)
260 = kcLiftedType ty `thenM` \ ty' ->
261 returnM (HsPArrTy ty', liftedTypeKind)
264 = returnM (HsNumTy n, liftedTypeKind)
266 kcHsType (HsKindSig ty k)
267 = kcCheckHsType ty k `thenM` \ ty' ->
268 returnM (HsKindSig ty' k, k)
270 kcHsType (HsTupleTy Boxed tys)
271 = mappM kcLiftedType tys `thenM` \ tys' ->
272 returnM (HsTupleTy Boxed tys', liftedTypeKind)
274 kcHsType (HsTupleTy Unboxed tys)
275 = mappM kcTypeType tys `thenM` \ tys' ->
276 returnM (HsTupleTy Unboxed tys', unliftedTypeKind)
278 kcHsType (HsFunTy ty1 ty2)
279 = kcTypeType ty1 `thenM` \ ty1' ->
280 kcTypeType ty2 `thenM` \ ty2' ->
281 returnM (HsFunTy ty1' ty2', liftedTypeKind)
283 kcHsType ty@(HsOpTy ty1 op ty2)
284 = kcTyVar op `thenM` \ op_kind ->
285 kcApps op_kind (ppr op) [ty1,ty2] `thenM` \ ([ty1',ty2'], res_kind) ->
286 returnM (HsOpTy ty1' op ty2', res_kind)
288 kcHsType ty@(HsAppTy ty1 ty2)
289 = kcHsType fun_ty `thenM` \ (fun_ty', fun_kind) ->
290 kcApps fun_kind (ppr fun_ty) arg_tys `thenM` \ (arg_tys', res_kind) ->
291 returnM (foldl HsAppTy fun_ty' arg_tys', res_kind)
293 (fun_ty, arg_tys) = split ty1 [ty2]
294 split (HsAppTy f a) as = split f (a:as)
297 kcHsType (HsPredTy pred)
298 = kcHsPred pred `thenM` \ pred' ->
299 returnM (HsPredTy pred', liftedTypeKind)
301 kcHsType (HsForAllTy exp tv_names context ty)
302 = kcHsTyVars tv_names $ \ tv_names' ->
303 kcHsContext context `thenM` \ ctxt' ->
304 kcLiftedType ty `thenM` \ ty' ->
305 -- The body of a forall must be a type, but in principle
306 -- there's no reason to prohibit *unlifted* types.
307 -- In fact, GHC can itself construct a function with an
308 -- unboxed tuple inside a for-all (via CPR analyis; see
309 -- typecheck/should_compile/tc170)
311 -- Still, that's only for internal interfaces, which aren't
312 -- kind-checked, and it's a bit inconvenient to use kcTypeType
313 -- here (because it doesn't return the result kind), so I'm
314 -- leaving it as lifted types for now.
315 returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
317 ---------------------------
318 kcApps :: TcKind -- Function kind
320 -> [HsType Name] -- Arg types
321 -> TcM ([HsType Name], TcKind) -- Kind-checked args
322 kcApps fun_kind ppr_fun args
323 = split_fk fun_kind (length args) `thenM` \ (arg_kinds, res_kind) ->
324 mappM kc_arg (args `zip` arg_kinds) `thenM` \ args' ->
325 returnM (args', res_kind)
327 split_fk fk 0 = returnM ([], fk)
328 split_fk fk n = unifyFunKind fk `thenM` \ mb_fk ->
330 Nothing -> failWithTc too_many_args
331 Just (ak,fk') -> split_fk fk' (n-1) `thenM` \ (aks, rk) ->
334 kc_arg (arg, arg_kind) = kcCheckHsType arg arg_kind
336 too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
337 ptext SLIT("is applied to too many type arguments")
339 ---------------------------
340 kcHsContext :: HsContext Name -> TcM (HsContext Name)
341 kcHsContext ctxt = mappM kcHsPred ctxt
343 kcHsPred pred -- Checks that the result is of kind liftedType
344 = kc_pred pred `thenM` \ (pred', kind) ->
345 checkExpectedKind (ppr pred) kind liftedTypeKind `thenM_`
348 ---------------------------
349 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
350 -- Does *not* check for a saturated
351 -- application (reason: used from TcDeriv)
352 kc_pred pred@(HsIParam name ty)
353 = kcHsType ty `thenM` \ (ty', kind) ->
354 returnM (HsIParam name ty', kind)
356 kc_pred pred@(HsClassP cls tys)
357 = kcClass cls `thenM` \ kind ->
358 kcApps kind (ppr cls) tys `thenM` \ (tys', res_kind) ->
359 returnM (HsClassP cls tys', res_kind)
361 ---------------------------
362 kcTyVar :: Name -> TcM TcKind
363 kcTyVar name -- Could be a tyvar or a tycon
364 = tcLookup name `thenM` \ thing ->
366 ATyVar tv -> returnM (tyVarKind tv)
367 ARecTyCon kind -> returnM kind
368 AGlobal (ATyCon tc) -> returnM (tyConKind tc)
369 other -> failWithTc (wrongThingErr "type" thing name)
371 kcClass :: Name -> TcM TcKind
372 kcClass cls -- Must be a class
373 = tcLookup cls `thenM` \ thing ->
375 ARecClass kind -> returnM kind
376 AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls))
377 other -> failWithTc (wrongThingErr "class" thing cls)
384 ---------------------------
385 -- We would like to get a decent error message from
386 -- (a) Under-applied type constructors
387 -- f :: (Maybe, Maybe)
388 -- (b) Over-applied type constructors
389 -- f :: Int x -> Int x
393 checkExpectedKind :: SDoc -> TcKind -> TcKind -> TcM TcKind
394 -- A fancy wrapper for 'unifyKind', which tries to give
395 -- decent error messages.
396 -- Returns the same kind that it is passed, exp_kind
397 checkExpectedKind pp_ty act_kind exp_kind
398 | act_kind `eqKind` exp_kind -- Short cut for a very common case
401 = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
403 Just _ -> returnM exp_kind ; -- Unification succeeded
406 -- So there's definitely an error
407 -- Now to find out what sort
408 zonkTcType exp_kind `thenM` \ exp_kind ->
409 zonkTcType act_kind `thenM` \ act_kind ->
411 let (exp_as, _) = Type.splitFunTys exp_kind
412 (act_as, _) = Type.splitFunTys act_kind
413 -- Use the Type versions for kinds
414 n_exp_as = length exp_as
415 n_act_as = length act_as
417 err | n_exp_as < n_act_as -- E.g. [Maybe]
418 = quotes pp_ty <+> ptext SLIT("is not applied to enough type arguments")
420 -- Now n_exp_as >= n_act_as. In the next two cases,
421 -- n_exp_as == 0, and hence so is n_act_as
422 | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
423 = ptext SLIT("Expecting a lifted type, but") <+> quotes pp_ty
424 <+> ptext SLIT("is unlifted")
426 | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
427 = ptext SLIT("Expecting an unlifted type, but") <+> quotes pp_ty
428 <+> ptext SLIT("is lifted")
430 | otherwise -- E.g. Monad [Int]
431 = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
432 ptext SLIT("but") <+> quotes pp_ty <+>
433 ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
435 failWithTc (ptext SLIT("Kind error:") <+> err)
439 %************************************************************************
443 %************************************************************************
447 * Transforms from HsType to Type
450 It cannot fail, and does no validity checking
453 dsHsType :: HsType Name -- All HsTyVarBndrs are kind-annotated
456 dsHsType ty@(HsTyVar name)
459 dsHsType (HsParTy ty) -- Remove the parentheses markers
462 dsHsType (HsKindSig ty k)
463 = dsHsType ty -- Kind checking done already
465 dsHsType (HsListTy ty)
466 = dsHsType ty `thenM` \ tau_ty ->
467 returnM (mkListTy tau_ty)
469 dsHsType (HsPArrTy ty)
470 = dsHsType ty `thenM` \ tau_ty ->
471 returnM (mkPArrTy tau_ty)
473 dsHsType (HsTupleTy boxity tys)
474 = dsHsTypes tys `thenM` \ tau_tys ->
475 returnM (mkTupleTy boxity (length tys) tau_tys)
477 dsHsType (HsFunTy ty1 ty2)
478 = dsHsType ty1 `thenM` \ tau_ty1 ->
479 dsHsType ty2 `thenM` \ tau_ty2 ->
480 returnM (mkFunTy tau_ty1 tau_ty2)
482 dsHsType (HsOpTy ty1 op ty2)
483 = dsHsType ty1 `thenM` \ tau_ty1 ->
484 dsHsType ty2 `thenM` \ tau_ty2 ->
485 ds_var_app op [tau_ty1,tau_ty2]
489 tcLookupTyCon genUnitTyConName `thenM` \ tc ->
490 returnM (mkTyConApp tc [])
492 dsHsType ty@(HsAppTy ty1 ty2)
495 dsHsType (HsPredTy pred)
496 = dsHsPred pred `thenM` \ pred' ->
497 returnM (mkPredTy pred')
499 dsHsType full_ty@(HsForAllTy exp tv_names ctxt ty)
500 = tcTyVarBndrs tv_names $ \ tyvars ->
501 mappM dsHsPred ctxt `thenM` \ theta ->
502 dsHsType ty `thenM` \ tau ->
503 returnM (mkSigmaTy tyvars theta tau)
505 dsHsTypes arg_tys = mappM dsHsType arg_tys
508 Help functions for type applications
509 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
512 ds_app :: HsType Name -> [HsType Name] -> TcM Type
513 ds_app (HsAppTy ty1 ty2) tys
514 = ds_app ty1 (ty2:tys)
517 = dsHsTypes tys `thenM` \ arg_tys ->
519 HsTyVar fun -> ds_var_app fun arg_tys
520 other -> dsHsType ty `thenM` \ fun_ty ->
521 returnM (mkAppTys fun_ty arg_tys)
523 ds_var_app :: Name -> [Type] -> TcM Type
524 ds_var_app name arg_tys
525 = tcLookup name `thenM` \ thing ->
527 ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
528 AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
529 ARecTyCon _ -> tcLookupTyCon name `thenM` \ tc ->
530 returnM (mkGenTyConApp tc arg_tys)
531 other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
538 dsHsPred :: HsPred Name -> TcM PredType
539 dsHsPred pred@(HsClassP class_name tys)
540 = dsHsTypes tys `thenM` \ arg_tys ->
541 tcLookupClass class_name `thenM` \ clas ->
542 returnM (ClassP clas arg_tys)
544 dsHsPred (HsIParam name ty)
545 = dsHsType ty `thenM` \ arg_ty ->
546 returnM (IParam name arg_ty)
550 %************************************************************************
552 Type-variable binders
554 %************************************************************************
558 kcHsTyVars :: [HsTyVarBndr Name]
559 -> ([HsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
560 -- They scope over the thing inside
562 kcHsTyVars tvs thing_inside
563 = mappM kcHsTyVar tvs `thenM` \ bndrs ->
564 tcExtendTyVarKindEnv bndrs $
567 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
568 -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
569 kcHsTyVar (UserTyVar name) = newKindVar `thenM` \ kind ->
570 returnM (KindedTyVar name kind)
571 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
574 tcTyVarBndrs :: [HsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
575 -> ([TyVar] -> TcM r)
577 -- Used when type-checking types/classes/type-decls
578 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
579 tcTyVarBndrs bndrs thing_inside
580 = mapM zonk bndrs `thenM` \ tyvars ->
581 tcExtendTyVarEnv tyvars (thing_inside tyvars)
583 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
584 returnM (mkTyVar name kind')
585 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
586 returnM (mkTyVar name liftedTypeKind)
590 %************************************************************************
592 Scoped type variables
594 %************************************************************************
597 tcAddScopedTyVars is used for scoped type variables added by pattern
599 e.g. \ ((x::a), (y::a)) -> x+y
600 They never have explicit kinds (because this is source-code only)
601 They are mutable (because they can get bound to a more specific type).
603 Usually we kind-infer and expand type splices, and then
604 tupecheck/desugar the type. That doesn't work well for scoped type
605 variables, because they scope left-right in patterns. (e.g. in the
606 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
608 The current not-very-good plan is to
609 * find all the types in the patterns
610 * find their free tyvars
612 * bring the kinded type vars into scope
613 * BUT throw away the kind-checked type
614 (we'll kind-check it again when we type-check the pattern)
616 This is bad because throwing away the kind checked type throws away
617 its splices. But too bad for now. [July 03]
620 We no longer specify that these type variables must be univerally
621 quantified (lots of email on the subject). If you want to put that
623 a) Do a checkSigTyVars after thing_inside
624 b) More insidiously, don't pass in expected_ty, else
625 we unify with it too early and checkSigTyVars barfs
626 Instead you have to pass in a fresh ty var, and unify
627 it with expected_ty afterwards
630 tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
631 tcAddScopedTyVars [] thing_inside
632 = thing_inside -- Quick get-out for the empty case
634 tcAddScopedTyVars sig_tys thing_inside
635 = getInLocalScope `thenM` \ in_scope ->
637 sig_tvs = [ UserTyVar n | ty <- sig_tys,
638 n <- nameSetToList (extractHsTyVars ty),
640 -- The tyvars we want are the free type variables of
641 -- the type that are not already in scope
643 -- Behave like kcHsType on a ForAll type
644 -- i.e. make kinded tyvars with mutable kinds,
645 -- and kind-check the enclosed types
646 kcHsTyVars sig_tvs (\ kinded_tvs -> do
647 { mappM kcTypeType sig_tys
648 ; return kinded_tvs }) `thenM` \ kinded_tvs ->
650 -- Zonk the mutable kinds and bring the tyvars into scope
651 -- Rather like tcTyVarBndrs, except that it brings *mutable*
652 -- tyvars into scope, not immutable ones
654 -- Furthermore, the tyvars are PatSigTvs, which means that we get better
655 -- error messages when type variables escape:
656 -- Inferred type is less polymorphic than expected
657 -- Quantified type variable `t' escapes
658 -- It is mentioned in the environment:
659 -- t is bound by the pattern type signature at tcfail103.hs:6
660 mapM zonk kinded_tvs `thenM` \ tyvars ->
661 tcExtendTyVarEnv tyvars thing_inside
664 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
665 newMutTyVar name kind' PatSigTv
666 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
667 returnM (mkTyVar name liftedTypeKind)
671 %************************************************************************
673 \subsection{Signatures}
675 %************************************************************************
677 @tcSigs@ checks the signatures for validity, and returns a list of
678 {\em freshly-instantiated} signatures. That is, the types are already
679 split up, and have fresh type variables installed. All non-type-signature
680 "RenamedSigs" are ignored.
682 The @TcSigInfo@ contains @TcTypes@ because they are unified with
683 the variable's type, and after that checked to see whether they've
689 TcId -- *Polymorphic* binder for this value...
696 TcId -- *Monomorphic* binder for this value
697 -- Does *not* have name = N
700 [Inst] -- Empty if theta is null, or
701 -- (method mono_id) otherwise
703 SrcLoc -- Of the signature
705 instance Outputable TcSigInfo where
706 ppr (TySigInfo id tyvars theta tau _ inst loc) =
707 ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
709 tcSigPolyId :: TcSigInfo -> TcId
710 tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
712 tcSigMonoId :: TcSigInfo -> TcId
713 tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
715 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
716 -- Search for a particular signature
717 maybeSig [] name = Nothing
718 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
719 | name == idName sig_id = Just sig
720 | otherwise = maybeSig sigs name
725 tcTySig :: RenamedSig -> TcM TcSigInfo
727 tcTySig (Sig v ty src_loc)
728 = addSrcLoc src_loc $
729 tcHsSigType (FunSigCtxt v) ty `thenM` \ sigma_tc_ty ->
730 mkTcSig (mkLocalId v sigma_tc_ty) `thenM` \ sig ->
733 mkTcSig :: TcId -> TcM TcSigInfo
735 = -- Instantiate this type
736 -- It's important to do this even though in the error-free case
737 -- we could just split the sigma_tc_ty (since the tyvars don't
738 -- unified with anything). But in the case of an error, when
739 -- the tyvars *do* get unified with something, we want to carry on
740 -- typechecking the rest of the program with the function bound
741 -- to a pristine type, namely sigma_tc_ty
742 tcInstType SigTv (idType poly_id) `thenM` \ (tyvars', theta', tau') ->
744 getInstLoc SignatureOrigin `thenM` \ inst_loc ->
745 newMethod inst_loc poly_id
747 theta' tau' `thenM` \ inst ->
748 -- We make a Method even if it's not overloaded; no harm
749 -- But do not extend the LIE! We're just making an Id.
751 getSrcLocM `thenM` \ src_loc ->
752 returnM (TySigInfo poly_id tyvars' theta' tau'
753 (instToId inst) [inst] src_loc)
757 %************************************************************************
759 \subsection{Errors and contexts}
761 %************************************************************************
765 hoistForAllTys :: Type -> Type
766 -- Used for user-written type signatures only
767 -- Move all the foralls and constraints to the top
768 -- e.g. T -> forall a. a ==> forall a. T -> a
769 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
771 -- Also: eliminate duplicate constraints. These can show up
772 -- when hoisting constraints, notably implicit parameters.
774 -- We want to 'look through' type synonyms when doing this
775 -- so it's better done on the Type than the HsType
779 no_shadow_ty = deShadowTy ty
780 -- Running over ty with an empty substitution gives it the
781 -- no-shadowing property. This is important. For example:
782 -- type Foo r = forall a. a -> r
783 -- foo :: Foo (Foo ())
784 -- Here the hoisting should give
785 -- foo :: forall a a1. a -> a1 -> ()
787 -- What about type vars that are lexically in scope in the envt?
788 -- We simply rely on them having a different unique to any
789 -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
790 -- out of the envt, which is boring and (I think) not necessary.
792 case hoist no_shadow_ty of
793 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
794 -- The 'nubBy' eliminates duplicate constraints,
795 -- notably implicit parameters
798 | (tvs1, body_ty) <- tcSplitForAllTys ty,
800 = case hoist body_ty of
801 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
803 | Just (arg, res) <- tcSplitFunTy_maybe ty
805 arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
806 in -- to the argument type
807 if (isPredTy arg') then
809 (tvs,theta,tau) -> (tvs, arg':theta, tau)
812 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
814 | otherwise = ([], [], ty)
818 %************************************************************************
820 \subsection{Errors and contexts}
822 %************************************************************************
825 wrongThingErr expected thing name
826 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
828 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
829 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
830 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
831 pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
832 pp_thing (ATyVar _) = ptext SLIT("Type variable")
833 pp_thing (ATcId _ _ _) = ptext SLIT("Local identifier")
834 pp_thing (ARecTyCon _) = ptext SLIT("Rec tycon")
835 pp_thing (ARecClass _) = ptext SLIT("Rec class")