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 of kind *
307 -- In principle, I suppose, we could allow unlifted types,
308 -- but it seems simpler to stick to lifted types for now.
309 returnM (HsForAllTy exp tv_names' ctxt' ty', liftedTypeKind)
311 ---------------------------
312 kcApps :: TcKind -- Function kind
314 -> [HsType Name] -- Arg types
315 -> TcM ([HsType Name], TcKind) -- Kind-checked args
316 kcApps fun_kind ppr_fun args
317 = split_fk fun_kind (length args) `thenM` \ (arg_kinds, res_kind) ->
318 mappM kc_arg (args `zip` arg_kinds) `thenM` \ args' ->
319 returnM (args', res_kind)
321 split_fk fk 0 = returnM ([], fk)
322 split_fk fk n = unifyFunKind fk `thenM` \ mb_fk ->
324 Nothing -> failWithTc too_many_args
325 Just (ak,fk') -> split_fk fk' (n-1) `thenM` \ (aks, rk) ->
328 kc_arg (arg, arg_kind) = kcCheckHsType arg arg_kind
330 too_many_args = ptext SLIT("Kind error:") <+> quotes ppr_fun <+>
331 ptext SLIT("is applied to too many type arguments")
333 ---------------------------
334 kcHsContext :: HsContext Name -> TcM (HsContext Name)
335 kcHsContext ctxt = mappM kcHsPred ctxt
337 kcHsPred pred -- Checks that the result is of kind liftedType
338 = kc_pred pred `thenM` \ (pred', kind) ->
339 checkExpectedKind (ppr pred) kind liftedTypeKind `thenM_`
342 ---------------------------
343 kc_pred :: HsPred Name -> TcM (HsPred Name, TcKind)
344 -- Does *not* check for a saturated
345 -- application (reason: used from TcDeriv)
346 kc_pred pred@(HsIParam name ty)
347 = kcHsType ty `thenM` \ (ty', kind) ->
348 returnM (HsIParam name ty', kind)
350 kc_pred pred@(HsClassP cls tys)
351 = kcClass cls `thenM` \ kind ->
352 kcApps kind (ppr cls) tys `thenM` \ (tys', res_kind) ->
353 returnM (HsClassP cls tys', res_kind)
355 ---------------------------
356 kcTyVar :: Name -> TcM TcKind
357 kcTyVar name -- Could be a tyvar or a tycon
358 = tcLookup name `thenM` \ thing ->
360 ATyVar tv -> returnM (tyVarKind tv)
361 ARecTyCon kind -> returnM kind
362 AGlobal (ATyCon tc) -> returnM (tyConKind tc)
363 other -> failWithTc (wrongThingErr "type" thing name)
365 kcClass :: Name -> TcM TcKind
366 kcClass cls -- Must be a class
367 = tcLookup cls `thenM` \ thing ->
369 ARecClass kind -> returnM kind
370 AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls))
371 other -> failWithTc (wrongThingErr "class" thing cls)
378 ---------------------------
379 -- We would like to get a decent error message from
380 -- (a) Under-applied type constructors
381 -- f :: (Maybe, Maybe)
382 -- (b) Over-applied type constructors
383 -- f :: Int x -> Int x
387 checkExpectedKind :: SDoc -> TcKind -> TcKind -> TcM TcKind
388 -- A fancy wrapper for 'unifyKind', which tries to give
389 -- decent error messages.
390 -- Returns the same kind that it is passed, exp_kind
391 checkExpectedKind pp_ty act_kind exp_kind
392 | act_kind `eqKind` exp_kind -- Short cut for a very common case
395 = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
397 Just _ -> returnM exp_kind ; -- Unification succeeded
400 -- So there's definitely an error
401 -- Now to find out what sort
402 zonkTcType exp_kind `thenM` \ exp_kind ->
403 zonkTcType act_kind `thenM` \ act_kind ->
405 let (exp_as, _) = Type.splitFunTys exp_kind
406 (act_as, _) = Type.splitFunTys act_kind
407 -- Use the Type versions for kinds
408 n_exp_as = length exp_as
409 n_act_as = length act_as
411 err | n_exp_as < n_act_as -- E.g. [Maybe]
412 = quotes pp_ty <+> ptext SLIT("is not applied to enough type arguments")
414 -- Now n_exp_as >= n_act_as. In the next two cases,
415 -- n_exp_as == 0, and hence so is n_act_as
416 | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
417 = ptext SLIT("Expecting a lifted type, but") <+> quotes pp_ty
418 <+> ptext SLIT("is unlifted")
420 | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
421 = ptext SLIT("Expecting an unlifted type, but") <+> quotes pp_ty
422 <+> ptext SLIT("is lifted")
424 | otherwise -- E.g. Monad [Int]
425 = sep [ ptext SLIT("Expecting kind") <+> quotes (pprKind exp_kind) <> comma,
426 ptext SLIT("but") <+> quotes pp_ty <+>
427 ptext SLIT("has kind") <+> quotes (pprKind act_kind)]
429 failWithTc (ptext SLIT("Kind error:") <+> err)
433 %************************************************************************
437 %************************************************************************
441 * Transforms from HsType to Type
444 It cannot fail, and does no validity checking
447 dsHsType :: HsType Name -- All HsTyVarBndrs are kind-annotated
450 dsHsType ty@(HsTyVar name)
453 dsHsType (HsParTy ty) -- Remove the parentheses markers
456 dsHsType (HsKindSig ty k)
457 = dsHsType ty -- Kind checking done already
459 dsHsType (HsListTy ty)
460 = dsHsType ty `thenM` \ tau_ty ->
461 returnM (mkListTy tau_ty)
463 dsHsType (HsPArrTy ty)
464 = dsHsType ty `thenM` \ tau_ty ->
465 returnM (mkPArrTy tau_ty)
467 dsHsType (HsTupleTy boxity tys)
468 = dsHsTypes tys `thenM` \ tau_tys ->
469 returnM (mkTupleTy boxity (length tys) tau_tys)
471 dsHsType (HsFunTy ty1 ty2)
472 = dsHsType ty1 `thenM` \ tau_ty1 ->
473 dsHsType ty2 `thenM` \ tau_ty2 ->
474 returnM (mkFunTy tau_ty1 tau_ty2)
476 dsHsType (HsOpTy ty1 op ty2)
477 = dsHsType ty1 `thenM` \ tau_ty1 ->
478 dsHsType ty2 `thenM` \ tau_ty2 ->
479 ds_var_app op [tau_ty1,tau_ty2]
483 tcLookupTyCon genUnitTyConName `thenM` \ tc ->
484 returnM (mkTyConApp tc [])
486 dsHsType ty@(HsAppTy ty1 ty2)
489 dsHsType (HsPredTy pred)
490 = dsHsPred pred `thenM` \ pred' ->
491 returnM (mkPredTy pred')
493 dsHsType full_ty@(HsForAllTy exp tv_names ctxt ty)
494 = tcTyVarBndrs tv_names $ \ tyvars ->
495 mappM dsHsPred ctxt `thenM` \ theta ->
496 dsHsType ty `thenM` \ tau ->
497 returnM (mkSigmaTy tyvars theta tau)
499 dsHsTypes arg_tys = mappM dsHsType arg_tys
502 Help functions for type applications
503 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
506 ds_app :: HsType Name -> [HsType Name] -> TcM Type
507 ds_app (HsAppTy ty1 ty2) tys
508 = ds_app ty1 (ty2:tys)
511 = dsHsTypes tys `thenM` \ arg_tys ->
513 HsTyVar fun -> ds_var_app fun arg_tys
514 other -> dsHsType ty `thenM` \ fun_ty ->
515 returnM (mkAppTys fun_ty arg_tys)
517 ds_var_app :: Name -> [Type] -> TcM Type
518 ds_var_app name arg_tys
519 = tcLookup name `thenM` \ thing ->
521 ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
522 AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
523 ARecTyCon _ -> tcLookupTyCon name `thenM` \ tc ->
524 returnM (mkGenTyConApp tc arg_tys)
525 other -> pprPanic "ds_app_type" (ppr name <+> ppr arg_tys)
532 dsHsPred :: HsPred Name -> TcM PredType
533 dsHsPred pred@(HsClassP class_name tys)
534 = dsHsTypes tys `thenM` \ arg_tys ->
535 tcLookupClass class_name `thenM` \ clas ->
536 returnM (ClassP clas arg_tys)
538 dsHsPred (HsIParam name ty)
539 = dsHsType ty `thenM` \ arg_ty ->
540 returnM (IParam name arg_ty)
544 %************************************************************************
546 Type-variable binders
548 %************************************************************************
552 kcHsTyVars :: [HsTyVarBndr Name]
553 -> ([HsTyVarBndr Name] -> TcM r) -- These binders are kind-annotated
554 -- They scope over the thing inside
556 kcHsTyVars tvs thing_inside
557 = mappM kcHsTyVar tvs `thenM` \ bndrs ->
558 tcExtendTyVarKindEnv bndrs $
561 kcHsTyVar :: HsTyVarBndr Name -> TcM (HsTyVarBndr Name)
562 -- Return a *kind-annotated* binder, and a tyvar with a mutable kind in it
563 kcHsTyVar (UserTyVar name) = newKindVar `thenM` \ kind ->
564 returnM (KindedTyVar name kind)
565 kcHsTyVar (KindedTyVar name kind) = returnM (KindedTyVar name kind)
568 tcTyVarBndrs :: [HsTyVarBndr Name] -- Kind-annotated binders, which need kind-zonking
569 -> ([TyVar] -> TcM r)
571 -- Used when type-checking types/classes/type-decls
572 -- Brings into scope immutable TyVars, not mutable ones that require later zonking
573 tcTyVarBndrs bndrs thing_inside
574 = mapM zonk bndrs `thenM` \ tyvars ->
575 tcExtendTyVarEnv tyvars (thing_inside tyvars)
577 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
578 returnM (mkTyVar name kind')
579 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
580 returnM (mkTyVar name liftedTypeKind)
584 %************************************************************************
586 Scoped type variables
588 %************************************************************************
591 tcAddScopedTyVars is used for scoped type variables added by pattern
593 e.g. \ ((x::a), (y::a)) -> x+y
594 They never have explicit kinds (because this is source-code only)
595 They are mutable (because they can get bound to a more specific type).
597 Usually we kind-infer and expand type splices, and then
598 tupecheck/desugar the type. That doesn't work well for scoped type
599 variables, because they scope left-right in patterns. (e.g. in the
600 example above, the 'a' in (y::a) is bound by the 'a' in (x::a).
602 The current not-very-good plan is to
603 * find all the types in the patterns
604 * find their free tyvars
606 * bring the kinded type vars into scope
607 * BUT throw away the kind-checked type
608 (we'll kind-check it again when we type-check the pattern)
610 This is bad because throwing away the kind checked type throws away
611 its splices. But too bad for now. [July 03]
614 We no longer specify that these type variables must be univerally
615 quantified (lots of email on the subject). If you want to put that
617 a) Do a checkSigTyVars after thing_inside
618 b) More insidiously, don't pass in expected_ty, else
619 we unify with it too early and checkSigTyVars barfs
620 Instead you have to pass in a fresh ty var, and unify
621 it with expected_ty afterwards
624 tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
625 tcAddScopedTyVars [] thing_inside
626 = thing_inside -- Quick get-out for the empty case
628 tcAddScopedTyVars sig_tys thing_inside
629 = getInLocalScope `thenM` \ in_scope ->
631 sig_tvs = [ UserTyVar n | ty <- sig_tys,
632 n <- nameSetToList (extractHsTyVars ty),
634 -- The tyvars we want are the free type variables of
635 -- the type that are not already in scope
637 -- Behave like kcHsType on a ForAll type
638 -- i.e. make kinded tyvars with mutable kinds,
639 -- and kind-check the enclosed types
640 kcHsTyVars sig_tvs (\ kinded_tvs -> do
641 { mappM kcTypeType sig_tys
642 ; return kinded_tvs }) `thenM` \ kinded_tvs ->
644 -- Zonk the mutable kinds and bring the tyvars into scope
645 -- Rather like tcTyVarBndrs, except that it brings *mutable*
646 -- tyvars into scope, not immutable ones
648 -- Furthermore, the tyvars are PatSigTvs, which means that we get better
649 -- error messages when type variables escape:
650 -- Inferred type is less polymorphic than expected
651 -- Quantified type variable `t' escapes
652 -- It is mentioned in the environment:
653 -- t is bound by the pattern type signature at tcfail103.hs:6
654 mapM zonk kinded_tvs `thenM` \ tyvars ->
655 tcExtendTyVarEnv tyvars thing_inside
658 zonk (KindedTyVar name kind) = zonkTcKindToKind kind `thenM` \ kind' ->
659 newMutTyVar name kind' PatSigTv
660 zonk (UserTyVar name) = pprTrace "BAD: Un-kinded tyvar" (ppr name) $
661 returnM (mkTyVar name liftedTypeKind)
665 %************************************************************************
667 \subsection{Signatures}
669 %************************************************************************
671 @tcSigs@ checks the signatures for validity, and returns a list of
672 {\em freshly-instantiated} signatures. That is, the types are already
673 split up, and have fresh type variables installed. All non-type-signature
674 "RenamedSigs" are ignored.
676 The @TcSigInfo@ contains @TcTypes@ because they are unified with
677 the variable's type, and after that checked to see whether they've
683 TcId -- *Polymorphic* binder for this value...
690 TcId -- *Monomorphic* binder for this value
691 -- Does *not* have name = N
694 [Inst] -- Empty if theta is null, or
695 -- (method mono_id) otherwise
697 SrcLoc -- Of the signature
699 instance Outputable TcSigInfo where
700 ppr (TySigInfo id tyvars theta tau _ inst loc) =
701 ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
703 tcSigPolyId :: TcSigInfo -> TcId
704 tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
706 tcSigMonoId :: TcSigInfo -> TcId
707 tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
709 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
710 -- Search for a particular signature
711 maybeSig [] name = Nothing
712 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
713 | name == idName sig_id = Just sig
714 | otherwise = maybeSig sigs name
719 tcTySig :: RenamedSig -> TcM TcSigInfo
721 tcTySig (Sig v ty src_loc)
722 = addSrcLoc src_loc $
723 tcHsSigType (FunSigCtxt v) ty `thenM` \ sigma_tc_ty ->
724 mkTcSig (mkLocalId v sigma_tc_ty) `thenM` \ sig ->
727 mkTcSig :: TcId -> TcM TcSigInfo
729 = -- Instantiate this type
730 -- It's important to do this even though in the error-free case
731 -- we could just split the sigma_tc_ty (since the tyvars don't
732 -- unified with anything). But in the case of an error, when
733 -- the tyvars *do* get unified with something, we want to carry on
734 -- typechecking the rest of the program with the function bound
735 -- to a pristine type, namely sigma_tc_ty
736 tcInstType SigTv (idType poly_id) `thenM` \ (tyvars', theta', tau') ->
738 getInstLoc SignatureOrigin `thenM` \ inst_loc ->
739 newMethod inst_loc poly_id
741 theta' tau' `thenM` \ inst ->
742 -- We make a Method even if it's not overloaded; no harm
743 -- But do not extend the LIE! We're just making an Id.
745 getSrcLocM `thenM` \ src_loc ->
746 returnM (TySigInfo poly_id tyvars' theta' tau'
747 (instToId inst) [inst] src_loc)
751 %************************************************************************
753 \subsection{Errors and contexts}
755 %************************************************************************
759 hoistForAllTys :: Type -> Type
760 -- Used for user-written type signatures only
761 -- Move all the foralls and constraints to the top
762 -- e.g. T -> forall a. a ==> forall a. T -> a
763 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
765 -- Also: eliminate duplicate constraints. These can show up
766 -- when hoisting constraints, notably implicit parameters.
768 -- We want to 'look through' type synonyms when doing this
769 -- so it's better done on the Type than the HsType
773 no_shadow_ty = deShadowTy ty
774 -- Running over ty with an empty substitution gives it the
775 -- no-shadowing property. This is important. For example:
776 -- type Foo r = forall a. a -> r
777 -- foo :: Foo (Foo ())
778 -- Here the hoisting should give
779 -- foo :: forall a a1. a -> a1 -> ()
781 -- What about type vars that are lexically in scope in the envt?
782 -- We simply rely on them having a different unique to any
783 -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
784 -- out of the envt, which is boring and (I think) not necessary.
786 case hoist no_shadow_ty of
787 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
788 -- The 'nubBy' eliminates duplicate constraints,
789 -- notably implicit parameters
792 | (tvs1, body_ty) <- tcSplitForAllTys ty,
794 = case hoist body_ty of
795 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
797 | Just (arg, res) <- tcSplitFunTy_maybe ty
799 arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
800 in -- to the argument type
801 if (isPredTy arg') then
803 (tvs,theta,tau) -> (tvs, arg':theta, tau)
806 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
808 | otherwise = ([], [], ty)
812 %************************************************************************
814 \subsection{Errors and contexts}
816 %************************************************************************
819 wrongThingErr expected thing name
820 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
822 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
823 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
824 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
825 pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
826 pp_thing (ATyVar _) = ptext SLIT("Type variable")
827 pp_thing (ATcId _ _ _) = ptext SLIT("Local identifier")
828 pp_thing (ARecTyCon _) = ptext SLIT("Rec tycon")
829 pp_thing (ARecClass _) = ptext SLIT("Rec class")