2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section[TcMonoType]{Typechecking user-specified @MonoTypes@}
7 module TcMonoType ( tcHsSigType, tcHsType, tcIfaceType, tcHsTheta, tcHsPred,
11 kcHsTyVar, kcHsTyVars, mkTyClTyVars,
12 kcHsType, kcHsSigType, kcHsSigTypes,
13 kcHsLiftedSigType, kcHsContext,
14 tcAddScopedTyVars, tcHsTyVars, mkImmutTyVars,
16 TcSigInfo(..), tcTySig, mkTcSig, maybeSig, tcSigPolyId, tcSigMonoId
19 #include "HsVersions.h"
21 import HsSyn ( HsType(..), HsTyVarBndr(..), HsTyOp(..),
22 Sig(..), HsPred(..), HsTupCon(..), hsTyVarNames )
23 import RnHsSyn ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig, extractHsTyVars )
24 import TcHsSyn ( TcId )
27 import TcEnv ( tcExtendTyVarEnv, tcLookup, tcLookupGlobal,
28 TyThing(..), TcTyThing(..), tcExtendKindEnv,
31 import TcMType ( newMutTyVar, newKindVar, zonkKindEnv, tcInstType, zonkTcType,
32 checkValidType, UserTypeCtxt(..), pprUserTypeCtxt, newOpenTypeKind
34 import TcUnify ( unifyKind, unifyFunKind )
35 import TcType ( Type, Kind, SourceType(..), ThetaType, TyVarDetails(..),
36 TcTyVar, TcKind, TcThetaType, TcTauType,
37 mkTyVarTy, mkTyVarTys, mkFunTy, isTypeKind,
38 zipFunTys, mkForAllTys, mkFunTys, tcEqType, isPredTy,
39 mkSigmaTy, mkPredTy, mkGenTyConApp, mkTyConApp, mkAppTys,
40 liftedTypeKind, unliftedTypeKind, eqKind,
41 tcSplitFunTy_maybe, tcSplitForAllTys
43 import qualified Type ( splitFunTys )
44 import Inst ( Inst, InstOrigin(..), newMethod, instToId )
46 import Id ( mkLocalId, idName, idType )
47 import Var ( TyVar, mkTyVar, tyVarKind )
48 import ErrUtils ( Message )
49 import TyCon ( TyCon, tyConKind )
50 import Class ( classTyCon )
53 import Subst ( deShadowTy )
54 import TysWiredIn ( mkListTy, mkPArrTy, mkTupleTy, genUnitTyCon )
55 import BasicTypes ( Boxity(..) )
56 import SrcLoc ( SrcLoc )
57 import Util ( lengthIs )
63 %************************************************************************
65 \subsection{Checking types}
67 %************************************************************************
69 Generally speaking we now type-check types in three phases
71 1. Kind check the HsType [kcHsType]
72 2. Convert from HsType to Type, and hoist the foralls [tcHsType]
73 3. Check the validity of the resulting type [checkValidType]
75 Often these steps are done one after the othe (tcHsSigType).
76 But in mutually recursive groups of type and class decls we do
77 1 kind-check the whole group
78 2 build TyCons/Classes in a knot-tied wa
79 3 check the validity of types in the now-unknotted TyCons/Classes
82 tcHsSigType :: UserTypeCtxt -> RenamedHsType -> TcM Type
83 -- Do kind checking, and hoist for-alls to the top
84 tcHsSigType ctxt ty = addErrCtxt (checkTypeCtxt ctxt ty) (
85 kcTypeType ty `thenM_`
88 checkValidType ctxt ty' `thenM_`
92 = vcat [ptext SLIT("In the type:") <+> ppr ty,
93 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
95 tcHsType :: RenamedHsType -> TcM Type
96 -- Don't do kind checking, nor validity checking,
97 -- but do hoist for-alls to the top
98 -- This is used in type and class decls, where kinding is
99 -- done in advance, and validity checking is done later
100 -- [Validity checking done later because of knot-tying issues.]
101 tcHsType ty = tc_type ty `thenM` \ ty' ->
102 returnM (hoistForAllTys ty')
104 tcHsTheta :: RenamedContext -> TcM ThetaType
105 -- Used when we are expecting a ClassContext (i.e. no implicit params)
106 -- Does not do validity checking, like tcHsType
107 tcHsTheta hs_theta = mappM tc_pred hs_theta
109 -- In interface files the type is already kinded,
110 -- and we definitely don't want to hoist for-alls.
111 -- Otherwise we'll change
112 -- dmfail :: forall m:(*->*) Monad m => forall a:* => String -> m a
114 -- dmfail :: forall m:(*->*) a:* Monad m => String -> m a
115 -- which definitely isn't right!
116 tcIfaceType ty = tc_type ty
120 %************************************************************************
122 \subsection{Kind checking}
124 %************************************************************************
128 When we come across the binding site for some type variables, we
129 proceed in two stages
131 1. Figure out what kind each tyvar has
133 2. Create suitably-kinded tyvars,
135 and typecheck the body
137 To do step 1, we proceed thus:
139 1a. Bind each type variable to a kind variable
140 1b. Apply the kind checker
141 1c. Zonk the resulting kinds
143 The kind checker is passed to tcHsTyVars as an argument.
145 For example, when we find
146 (forall a m. m a -> m a)
147 we bind a,m to kind varibles and kind-check (m a -> m a). This
148 makes a get kind *, and m get kind *->*. Now we typecheck (m a -> m a)
149 in an environment that binds a and m suitably.
151 The kind checker passed to tcHsTyVars needs to look at enough to
152 establish the kind of the tyvar:
153 * For a group of type and class decls, it's just the group, not
154 the rest of the program
155 * For a tyvar bound in a pattern type signature, its the types
156 mentioned in the other type signatures in that bunch of patterns
157 * For a tyvar bound in a RULE, it's the type signatures on other
158 universally quantified variables in the rule
160 Note that this may occasionally give surprising results. For example:
162 data T a b = MkT (a b)
164 Here we deduce a::*->*, b::*.
165 But equally valid would be
166 a::(*->*)-> *, b::*->*
169 -- tcHsTyVars is used for type variables in type signatures
170 -- e.g. forall a. a->a
171 -- They are immutable, because they scope only over the signature
172 -- They may or may not be explicitly-kinded
173 tcHsTyVars :: [HsTyVarBndr Name]
174 -> TcM a -- The kind checker
175 -> ([TyVar] -> TcM b)
178 tcHsTyVars [] kind_check thing_inside = thing_inside []
179 -- A useful short cut for a common case!
181 tcHsTyVars tv_names kind_check thing_inside
182 = kcHsTyVars tv_names `thenM` \ tv_names_w_kinds ->
183 tcExtendKindEnv tv_names_w_kinds kind_check `thenM_`
184 zonkKindEnv tv_names_w_kinds `thenM` \ tvs_w_kinds ->
186 tyvars = mkImmutTyVars tvs_w_kinds
188 tcExtendTyVarEnv tyvars (thing_inside tyvars)
192 tcAddScopedTyVars :: [RenamedHsType] -> TcM a -> TcM a
193 -- tcAddScopedTyVars is used for scoped type variables
194 -- added by pattern type signatures
195 -- e.g. \ (x::a) (y::a) -> x+y
196 -- They never have explicit kinds (because this is source-code only)
197 -- They are mutable (because they can get bound to a more specific type)
199 -- Find the not-already-in-scope signature type variables,
200 -- kind-check them, and bring them into scope
202 -- We no longer specify that these type variables must be univerally
203 -- quantified (lots of email on the subject). If you want to put that
204 -- back in, you need to
205 -- a) Do a checkSigTyVars after thing_inside
206 -- b) More insidiously, don't pass in expected_ty, else
207 -- we unify with it too early and checkSigTyVars barfs
208 -- Instead you have to pass in a fresh ty var, and unify
209 -- it with expected_ty afterwards
210 tcAddScopedTyVars [] thing_inside
211 = thing_inside -- Quick get-out for the empty case
213 tcAddScopedTyVars sig_tys thing_inside
214 = getInLocalScope `thenM` \ in_scope ->
216 all_sig_tvs = foldr (unionNameSets . extractHsTyVars) emptyNameSet sig_tys
217 sig_tvs = filter (not . in_scope) (nameSetToList all_sig_tvs)
219 mappM newNamedKindVar sig_tvs `thenM` \ kind_env ->
220 tcExtendKindEnv kind_env (kcHsSigTypes sig_tys) `thenM_`
221 zonkKindEnv kind_env `thenM` \ tvs_w_kinds ->
222 sequenceM [ newMutTyVar name kind PatSigTv
223 | (name, kind) <- tvs_w_kinds] `thenM` \ tyvars ->
224 tcExtendTyVarEnv tyvars thing_inside
229 kcHsTyVar :: HsTyVarBndr name -> TcM (name, TcKind)
230 kcHsTyVars :: [HsTyVarBndr name] -> TcM [(name, TcKind)]
232 kcHsTyVar (UserTyVar name) = newNamedKindVar name
233 kcHsTyVar (IfaceTyVar name kind) = returnM (name, kind)
235 kcHsTyVars tvs = mappM kcHsTyVar tvs
237 newNamedKindVar name = newKindVar `thenM` \ kind ->
240 ---------------------------
241 kcLiftedType :: RenamedHsType -> TcM Kind
242 -- The type ty must be a *lifted* *type*
243 kcLiftedType ty = kcHsType ty `thenM` \ act_kind ->
244 checkExpectedKind (ppr ty) act_kind liftedTypeKind
246 ---------------------------
247 kcTypeType :: RenamedHsType -> TcM ()
248 -- The type ty must be a *type*, but it can be lifted or unlifted.
250 = kcHsType ty `thenM` \ kind ->
251 if isTypeKind kind then
254 newOpenTypeKind `thenM` \ exp_kind ->
255 checkExpectedKind (ppr ty) kind exp_kind `thenM_`
258 ---------------------------
259 kcHsSigType, kcHsLiftedSigType :: RenamedHsType -> TcM ()
260 -- Used for type signatures
261 kcHsSigType ty = kcTypeType ty
262 kcHsSigTypes tys = mappM_ kcHsSigType tys
263 kcHsLiftedSigType ty = kcLiftedType ty `thenM_` returnM ()
265 ---------------------------
266 kcHsType :: RenamedHsType -> TcM TcKind
267 -- kcHsType *returns* the kind of the type, rather than taking an expected
268 -- kind as argument as tcExpr does. Reason: the kind of (->) is
269 -- forall bx1 bx2. Type bx1 -> Type bx2 -> Type Boxed
270 -- so we'd need to generate huge numbers of bx variables.
272 kcHsType (HsTyVar name) = kcTyVar name
273 kcHsType (HsListTy ty) = kcLiftedType ty
274 kcHsType (HsPArrTy ty) = kcLiftedType ty
275 kcHsType (HsParTy ty) = kcHsType ty -- Skip parentheses markers
276 kcHsType (HsNumTy _) = returnM liftedTypeKind -- The unit type for generics
277 kcHsType (HsKindSig ty k) = kcHsType ty `thenM` \ act_kind ->
278 checkExpectedKind (ppr ty) act_kind k
280 kcHsType (HsTupleTy (HsTupCon boxity _) tys)
281 = mappM kcTypeType tys `thenM_`
282 returnM (case boxity of
283 Boxed -> liftedTypeKind
284 Unboxed -> unliftedTypeKind)
286 kcHsType (HsFunTy ty1 ty2)
287 = kcTypeType ty1 `thenM_`
288 kcTypeType ty2 `thenM_`
289 returnM liftedTypeKind
291 kcHsType (HsOpTy ty1 HsArrow ty2)
292 = kcTypeType ty1 `thenM_`
293 kcTypeType ty2 `thenM_`
294 returnM liftedTypeKind
296 kcHsType ty@(HsOpTy ty1 op_ty@(HsTyOp op) ty2)
297 = addErrCtxt (appKindCtxt (ppr ty)) $
298 kcTyVar op `thenM` \ op_kind ->
299 kcApps (ppr op_ty) op_kind [ty1,ty2]
301 kcHsType (HsPredTy pred)
302 = kcHsPred pred `thenM_`
303 returnM liftedTypeKind
305 kcHsType ty@(HsAppTy ty1 ty2)
306 = addErrCtxt (appKindCtxt (ppr ty)) $
309 kc_app (HsAppTy f a) as = kc_app f (a:as)
310 kc_app f as = kcHsType f `thenM` \ fk ->
313 kcHsType (HsForAllTy (Just tv_names) context ty)
314 = kcHsTyVars tv_names `thenM` \ kind_env ->
315 tcExtendKindEnv kind_env $
316 kcHsContext context `thenM_`
318 -- The body of a forall must be of kind *
319 -- In principle, I suppose, we could allow unlifted types,
320 -- but it seems simpler to stick to lifted types for now.
322 ---------------------------
323 kcApps :: SDoc -- The function
324 -> TcKind -- Function kind
325 -> [RenamedHsType] -- Arg types
326 -> TcM TcKind -- Result kind
327 kcApps pp_fun fun_kind args
330 go fk [] = returnM fk
331 go fk (ty:tys) = unifyFunKind fk `thenM` \ mb_fk ->
333 Nothing -> failWithTc too_few_args ;
335 kcHsType ty `thenM` \ ak ->
336 checkExpectedKind (ppr ty) ak ak' `thenM_`
339 too_few_args = ptext SLIT("Kind error:") <+> quotes pp_fun <+>
340 ptext SLIT("is applied to too many type arguments")
342 ---------------------------
343 -- We would like to get a decent error message from
344 -- (a) Under-applied type constructors
345 -- f :: (Maybe, Maybe)
346 -- (b) Over-applied type constructors
347 -- f :: Int x -> Int x
350 checkExpectedKind :: SDoc -> TcKind -> TcKind -> TcM TcKind
351 -- A fancy wrapper for 'unifyKind', which tries to give
352 -- decent error messages.
353 -- Returns the same kind that it is passed, exp_kind
354 checkExpectedKind pp_ty act_kind exp_kind
355 | act_kind `eqKind` exp_kind -- Short cut for a very common case
358 = tryTc (unifyKind exp_kind act_kind) `thenM` \ (errs, mb_r) ->
360 Just _ -> returnM exp_kind ; -- Unification succeeded
363 -- So there's definitely an error
364 -- Now to find out what sort
365 zonkTcType exp_kind `thenM` \ exp_kind ->
366 zonkTcType act_kind `thenM` \ act_kind ->
368 let (exp_as, _) = Type.splitFunTys exp_kind
369 (act_as, _) = Type.splitFunTys act_kind
370 -- Use the Type versions for kinds
371 n_exp_as = length exp_as
372 n_act_as = length act_as
374 err | n_exp_as < n_act_as -- E.g. [Maybe]
375 = quotes pp_ty <+> ptext SLIT("is not applied to enough type arguments")
377 -- Now n_exp_as >= n_act_as. In the next two cases,
378 -- n_exp_as == 0, and hence so is n_act_as
379 | exp_kind `eqKind` liftedTypeKind && act_kind `eqKind` unliftedTypeKind
380 = ptext SLIT("Expecting a lifted type, but") <+> quotes pp_ty
381 <+> ptext SLIT("is unlifted")
383 | exp_kind `eqKind` unliftedTypeKind && act_kind `eqKind` liftedTypeKind
384 = ptext SLIT("Expecting an unlifted type, but") <+> quotes pp_ty
385 <+> ptext SLIT("is lifted")
387 | otherwise -- E.g. Monad [Int]
388 = sep [ ptext SLIT("Expecting kind") <+> quotes (ppr exp_kind) <> comma,
389 ptext SLIT("but") <+> quotes pp_ty <+>
390 ptext SLIT("has kind") <+> quotes (ppr act_kind)]
392 failWithTc (ptext SLIT("Kind error:") <+> err)
395 ---------------------------
396 kc_pred :: RenamedHsPred -> TcM TcKind -- Does *not* check for a saturated
397 -- application (reason: used from TcDeriv)
398 kc_pred pred@(HsIParam name ty)
401 kc_pred pred@(HsClassP cls tys)
402 = kcClass cls `thenM` \ kind ->
403 kcApps (ppr cls) kind tys
405 ---------------------------
406 kcHsContext ctxt = mappM_ kcHsPred ctxt
408 kcHsPred pred -- Checks that the result is of kind liftedType
409 = addErrCtxt (appKindCtxt (ppr pred)) $
410 kc_pred pred `thenM` \ kind ->
411 checkExpectedKind (ppr pred) kind liftedTypeKind
414 ---------------------------
415 kcTyVar name -- Could be a tyvar or a tycon
416 = tcLookup name `thenM` \ thing ->
418 AThing kind -> returnM kind
419 ATyVar tv -> returnM (tyVarKind tv)
420 AGlobal (ATyCon tc) -> returnM (tyConKind tc)
421 other -> failWithTc (wrongThingErr "type" thing name)
423 kcClass cls -- Must be a class
424 = tcLookup cls `thenM` \ thing ->
426 AThing kind -> returnM kind
427 AGlobal (AClass cls) -> returnM (tyConKind (classTyCon cls))
428 other -> failWithTc (wrongThingErr "class" thing cls)
431 %************************************************************************
435 %************************************************************************
437 tc_type, the main work horse
438 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
444 tc_type is used to typecheck the types in the RHS of data
445 constructors. In the case of recursive data types, that means that
446 the type constructors themselves are (partly) black holes. e.g.
448 data T a = MkT a [T a]
450 While typechecking the [T a] on the RHS, T itself is not yet fully
451 defined. That in turn places restrictions on what you can check in
452 tcHsType; if you poke on too much you get a black hole. I keep
453 forgetting this, hence this warning!
455 So tc_type does no validity-checking. Instead that's all done
456 by TcMType.checkValidType
458 --------------------------
459 *** END OF BIG WARNING ***
460 --------------------------
464 tc_type :: RenamedHsType -> TcM Type
466 tc_type ty@(HsTyVar name)
469 tc_type (HsKindSig ty k)
470 = tc_type ty -- Kind checking done already
472 tc_type (HsListTy ty)
473 = tc_type ty `thenM` \ tau_ty ->
474 returnM (mkListTy tau_ty)
476 tc_type (HsPArrTy ty)
477 = tc_type ty `thenM` \ tau_ty ->
478 returnM (mkPArrTy tau_ty)
480 tc_type (HsTupleTy (HsTupCon boxity arity) tys)
481 = ASSERT( tys `lengthIs` arity )
482 tc_types tys `thenM` \ tau_tys ->
483 returnM (mkTupleTy boxity arity tau_tys)
485 tc_type (HsFunTy ty1 ty2)
486 = tc_type ty1 `thenM` \ tau_ty1 ->
487 tc_type ty2 `thenM` \ tau_ty2 ->
488 returnM (mkFunTy tau_ty1 tau_ty2)
490 tc_type (HsOpTy ty1 HsArrow ty2)
491 = tc_type ty1 `thenM` \ tau_ty1 ->
492 tc_type ty2 `thenM` \ tau_ty2 ->
493 returnM (mkFunTy tau_ty1 tau_ty2)
495 tc_type (HsOpTy ty1 (HsTyOp op) ty2)
496 = tc_type ty1 `thenM` \ tau_ty1 ->
497 tc_type ty2 `thenM` \ tau_ty2 ->
498 tc_fun_type op [tau_ty1,tau_ty2]
500 tc_type (HsParTy ty) -- Remove the parentheses markers
505 returnM (mkTyConApp genUnitTyCon [])
507 tc_type ty@(HsAppTy ty1 ty2)
508 = addErrCtxt (appKindCtxt (ppr ty)) $
511 tc_type (HsPredTy pred)
512 = tc_pred pred `thenM` \ pred' ->
513 returnM (mkPredTy pred')
515 tc_type full_ty@(HsForAllTy (Just tv_names) ctxt ty)
517 kind_check = kcHsContext ctxt `thenM_` kcHsType ty
519 tcHsTyVars tv_names kind_check $ \ tyvars ->
520 mappM tc_pred ctxt `thenM` \ theta ->
521 tc_type ty `thenM` \ tau ->
522 returnM (mkSigmaTy tyvars theta tau)
524 tc_types arg_tys = mappM tc_type arg_tys
527 Help functions for type applications
528 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
531 tc_app :: RenamedHsType -> [RenamedHsType] -> TcM Type
532 tc_app (HsAppTy ty1 ty2) tys
533 = tc_app ty1 (ty2:tys)
536 = tc_types tys `thenM` \ arg_tys ->
538 HsTyVar fun -> tc_fun_type fun arg_tys
539 other -> tc_type ty `thenM` \ fun_ty ->
540 returnM (mkAppTys fun_ty arg_tys)
542 -- (tc_fun_type ty arg_tys) returns (mkAppTys ty arg_tys)
543 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
544 -- hence the rather strange functionality.
546 tc_fun_type name arg_tys
547 = tcLookup name `thenM` \ thing ->
549 ATyVar tv -> returnM (mkAppTys (mkTyVarTy tv) arg_tys)
551 AGlobal (ATyCon tc) -> returnM (mkGenTyConApp tc arg_tys)
553 other -> failWithTc (wrongThingErr "type constructor" thing name)
560 tcHsPred pred = kc_pred pred `thenM_` tc_pred pred
561 -- Is happy with a partial application, e.g. (ST s)
564 tc_pred assn@(HsClassP class_name tys)
565 = addErrCtxt (appKindCtxt (ppr assn)) $
566 tc_types tys `thenM` \ arg_tys ->
567 tcLookupGlobal class_name `thenM` \ thing ->
569 AClass clas -> returnM (ClassP clas arg_tys)
570 other -> failWithTc (wrongThingErr "class" (AGlobal thing) class_name)
572 tc_pred assn@(HsIParam name ty)
573 = addErrCtxt (appKindCtxt (ppr assn)) $
574 tc_type ty `thenM` \ arg_ty ->
575 returnM (IParam name arg_ty)
580 %************************************************************************
582 \subsection{Type variables, with knot tying!}
584 %************************************************************************
587 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
588 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
590 mkTyClTyVars :: Kind -- Kind of the tycon or class
591 -> [HsTyVarBndr Name]
593 mkTyClTyVars kind tyvar_names
594 = mkImmutTyVars tyvars_w_kinds
596 (tyvars_w_kinds, _) = zipFunTys (hsTyVarNames tyvar_names) kind
600 %************************************************************************
602 \subsection{Signatures}
604 %************************************************************************
606 @tcSigs@ checks the signatures for validity, and returns a list of
607 {\em freshly-instantiated} signatures. That is, the types are already
608 split up, and have fresh type variables installed. All non-type-signature
609 "RenamedSigs" are ignored.
611 The @TcSigInfo@ contains @TcTypes@ because they are unified with
612 the variable's type, and after that checked to see whether they've
618 TcId -- *Polymorphic* binder for this value...
625 TcId -- *Monomorphic* binder for this value
626 -- Does *not* have name = N
629 [Inst] -- Empty if theta is null, or
630 -- (method mono_id) otherwise
632 SrcLoc -- Of the signature
634 instance Outputable TcSigInfo where
635 ppr (TySigInfo id tyvars theta tau _ inst loc) =
636 ppr id <+> ptext SLIT("::") <+> ppr tyvars <+> ppr theta <+> ptext SLIT("=>") <+> ppr tau
638 tcSigPolyId :: TcSigInfo -> TcId
639 tcSigPolyId (TySigInfo id _ _ _ _ _ _) = id
641 tcSigMonoId :: TcSigInfo -> TcId
642 tcSigMonoId (TySigInfo _ _ _ _ id _ _) = id
644 maybeSig :: [TcSigInfo] -> Name -> Maybe (TcSigInfo)
645 -- Search for a particular signature
646 maybeSig [] name = Nothing
647 maybeSig (sig@(TySigInfo sig_id _ _ _ _ _ _) : sigs) name
648 | name == idName sig_id = Just sig
649 | otherwise = maybeSig sigs name
654 tcTySig :: RenamedSig -> TcM TcSigInfo
656 tcTySig (Sig v ty src_loc)
657 = addSrcLoc src_loc $
658 tcHsSigType (FunSigCtxt v) ty `thenM` \ sigma_tc_ty ->
659 mkTcSig (mkLocalId v sigma_tc_ty) `thenM` \ sig ->
662 mkTcSig :: TcId -> TcM TcSigInfo
664 = -- Instantiate this type
665 -- It's important to do this even though in the error-free case
666 -- we could just split the sigma_tc_ty (since the tyvars don't
667 -- unified with anything). But in the case of an error, when
668 -- the tyvars *do* get unified with something, we want to carry on
669 -- typechecking the rest of the program with the function bound
670 -- to a pristine type, namely sigma_tc_ty
671 tcInstType SigTv (idType poly_id) `thenM` \ (tyvars', theta', tau') ->
673 getInstLoc SignatureOrigin `thenM` \ inst_loc ->
674 newMethod inst_loc poly_id
676 theta' tau' `thenM` \ inst ->
677 -- We make a Method even if it's not overloaded; no harm
678 -- But do not extend the LIE! We're just making an Id.
680 getSrcLocM `thenM` \ src_loc ->
681 returnM (TySigInfo poly_id tyvars' theta' tau'
682 (instToId inst) [inst] src_loc)
686 %************************************************************************
688 \subsection{Errors and contexts}
690 %************************************************************************
694 hoistForAllTys :: Type -> Type
695 -- Used for user-written type signatures only
696 -- Move all the foralls and constraints to the top
697 -- e.g. T -> forall a. a ==> forall a. T -> a
698 -- T -> (?x::Int) -> Int ==> (?x::Int) -> T -> Int
700 -- Also: eliminate duplicate constraints. These can show up
701 -- when hoisting constraints, notably implicit parameters.
703 -- We want to 'look through' type synonyms when doing this
704 -- so it's better done on the Type than the HsType
708 no_shadow_ty = deShadowTy ty
709 -- Running over ty with an empty substitution gives it the
710 -- no-shadowing property. This is important. For example:
711 -- type Foo r = forall a. a -> r
712 -- foo :: Foo (Foo ())
713 -- Here the hoisting should give
714 -- foo :: forall a a1. a -> a1 -> ()
716 -- What about type vars that are lexically in scope in the envt?
717 -- We simply rely on them having a different unique to any
718 -- binder in 'ty'. Otherwise we'd have to slurp the in-scope-tyvars
719 -- out of the envt, which is boring and (I think) not necessary.
721 case hoist no_shadow_ty of
722 (tvs, theta, body) -> mkForAllTys tvs (mkFunTys (nubBy tcEqType theta) body)
723 -- The 'nubBy' eliminates duplicate constraints,
724 -- notably implicit parameters
727 | (tvs1, body_ty) <- tcSplitForAllTys ty,
729 = case hoist body_ty of
730 (tvs2,theta,tau) -> (tvs1 ++ tvs2, theta, tau)
732 | Just (arg, res) <- tcSplitFunTy_maybe ty
734 arg' = hoistForAllTys arg -- Don't forget to apply hoist recursively
735 in -- to the argument type
736 if (isPredTy arg') then
738 (tvs,theta,tau) -> (tvs, arg':theta, tau)
741 (tvs,theta,tau) -> (tvs, theta, mkFunTy arg' tau)
743 | otherwise = ([], [], ty)
747 %************************************************************************
749 \subsection{Errors and contexts}
751 %************************************************************************
754 typeKindCtxt :: RenamedHsType -> Message
755 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
756 nest 2 (quotes (ppr ty)),
757 ptext SLIT("is a type")]
759 appKindCtxt :: SDoc -> Message
760 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
762 wrongThingErr expected thing name
763 = pp_thing thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
765 pp_thing (AGlobal (ATyCon _)) = ptext SLIT("Type constructor")
766 pp_thing (AGlobal (AClass _)) = ptext SLIT("Class")
767 pp_thing (AGlobal (AnId _)) = ptext SLIT("Identifier")
768 pp_thing (AGlobal (ADataCon _)) = ptext SLIT("Data constructor")
769 pp_thing (ATyVar _) = ptext SLIT("Type variable")
770 pp_thing (ATcId _ _) = ptext SLIT("Local identifier")
771 pp_thing (AThing _) = ptext SLIT("Utterly bogus")