2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 \section{Monadic type operations}
6 This module contains monadic operations over types that contain mutable type variables
10 TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcRhoType, TcTyVarSet,
12 --------------------------------
13 -- Creating new mutable type variables
15 newTyVarTy, -- Kind -> NF_TcM TcType
16 newTyVarTys, -- Int -> Kind -> NF_TcM [TcType]
17 newKindVar, newKindVars, newBoxityVar,
19 --------------------------------
21 tcInstTyVar, tcInstTyVars,
22 tcInstSigVars, tcInstType,
25 --------------------------------
26 -- Checking type validity
27 Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
28 SourceTyCtxt(..), checkValidTheta,
29 checkValidInstHead, instTypeErr,
31 --------------------------------
33 unifyTauTy, unifyTauTyList, unifyTauTyLists,
34 unifyFunTy, unifyListTy, unifyTupleTy,
35 unifyKind, unifyKinds, unifyOpenTypeKind,
37 --------------------------------
39 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
40 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
41 zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
45 #include "HsVersions.h"
49 import TypeRep ( Type(..), SourceType(..), TyNote(..), -- Friend; can see representation
50 Kind, TauType, ThetaType,
53 import TcType ( tcEqType, tcCmpPred,
54 tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
55 tcSplitTyConApp_maybe, tcSplitFunTy_maybe, tcSplitForAllTys,
56 tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy, isUnLiftedType, isIPPred,
58 mkAppTy, mkTyVarTy, mkTyVarTys, mkFunTy, mkTyConApp,
59 tyVarsOfPred, getClassPredTys_maybe,
61 liftedTypeKind, unliftedTypeKind, openTypeKind, defaultKind, superKind,
62 superBoxity, liftedBoxity, hasMoreBoxityInfo, typeKind,
63 tyVarsOfType, tyVarsOfTypes, tidyOpenType, tidyOpenTypes, tidyTyVar,
66 import Subst ( Subst, mkTopTyVarSubst, substTy )
67 import Class ( classArity, className )
68 import TyCon ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
69 isTupleTyCon, tyConArity, tupleTyConBoxity, tyConName )
70 import PrimRep ( PrimRep(VoidRep) )
71 import Var ( TyVar, varName, tyVarKind, tyVarName, isTyVar, mkTyVar,
72 isMutTyVar, isSigTyVar )
75 import TcMonad -- TcType, amongst others
76 import TysWiredIn ( voidTy, listTyCon, mkListTy, mkTupleTy,
77 isFFIArgumentTy, isFFIImportResultTy )
78 import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
79 import ForeignCall ( Safety(..) )
80 import FunDeps ( grow )
81 import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
82 import Name ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
83 mkLocalName, mkDerivedTyConOcc, isSystemName
86 import BasicTypes ( Boxity, Arity, isBoxed )
87 import CmdLineOpts ( dopt, DynFlag(..) )
88 import Unique ( Uniquable(..) )
89 import SrcLoc ( noSrcLoc )
90 import Util ( nOfThem )
91 import ListSetOps ( removeDups )
96 %************************************************************************
98 \subsection{New type variables}
100 %************************************************************************
103 newTyVar :: Kind -> NF_TcM TcTyVar
105 = tcGetUnique `thenNF_Tc` \ uniq ->
106 tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
108 newTyVarTy :: Kind -> NF_TcM TcType
110 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
111 returnNF_Tc (TyVarTy tc_tyvar)
113 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
114 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
116 newKindVar :: NF_TcM TcKind
118 = tcGetUnique `thenNF_Tc` \ uniq ->
119 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv ->
120 returnNF_Tc (TyVarTy kv)
122 newKindVars :: Int -> NF_TcM [TcKind]
123 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
125 newBoxityVar :: NF_TcM TcKind
127 = tcGetUnique `thenNF_Tc` \ uniq ->
128 tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity `thenNF_Tc` \ kv ->
129 returnNF_Tc (TyVarTy kv)
133 %************************************************************************
135 \subsection{Type instantiation}
137 %************************************************************************
139 I don't understand why this is needed
140 An old comments says "No need for tcSplitForAllTyM because a type
141 variable can't be instantiated to a for-all type"
142 But the same is true of rho types!
145 tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
149 -- A type variable is never instantiated to a dictionary type,
150 -- so we don't need to do a tcReadVar on the "arg".
151 go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
152 Just pair -> go res res (pair:ts)
153 Nothing -> returnNF_Tc (reverse ts, syn_t)
154 go syn_t (NoteTy n t) ts = go syn_t t ts
155 go syn_t (TyVarTy tv) ts = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
157 Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
158 other -> returnNF_Tc (reverse ts, syn_t)
159 go syn_t (UsageTy _ t) ts = go syn_t t ts
160 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
164 %************************************************************************
166 \subsection{Type instantiation}
168 %************************************************************************
170 Instantiating a bunch of type variables
173 tcInstTyVars :: [TyVar]
174 -> NF_TcM ([TcTyVar], [TcType], Subst)
177 = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
179 tys = mkTyVarTys tc_tyvars
181 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
182 -- Since the tyvars are freshly made,
183 -- they cannot possibly be captured by
184 -- any existing for-alls. Hence mkTopTyVarSubst
187 = tcGetUnique `thenNF_Tc` \ uniq ->
189 name = setNameUnique (tyVarName tyvar) uniq
190 -- Note that we don't change the print-name
191 -- This won't confuse the type checker but there's a chance
192 -- that two different tyvars will print the same way
193 -- in an error message. -dppr-debug will show up the difference
194 -- Better watch out for this. If worst comes to worst, just
195 -- use mkSysLocalName.
197 tcNewMutTyVar name (tyVarKind tyvar)
199 tcInstSigVars tyvars -- Very similar to tcInstTyVar
200 = tcGetUniques `thenNF_Tc` \ uniqs ->
201 listTc [ ASSERT( not (kind `eqKind` openTypeKind) ) -- Shouldn't happen
202 tcNewSigTyVar name kind
203 | (tyvar, uniq) <- tyvars `zip` uniqs,
204 let name = setNameUnique (tyVarName tyvar) uniq,
205 let kind = tyVarKind tyvar
209 @tcInstType@ instantiates the outer-level for-alls of a TcType with
210 fresh type variables, splits off the dictionary part, and returns the results.
213 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
215 = case tcSplitForAllTys ty of
216 ([], rho) -> -- There may be overloading but no type variables;
217 -- (?x :: Int) => Int -> Int
219 (theta, tau) = tcSplitRhoTy rho -- Used to be tcSplitRhoTyM
221 returnNF_Tc ([], theta, tau)
223 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
225 (theta, tau) = tcSplitRhoTy (substTy tenv rho) -- Used to be tcSplitRhoTyM
227 returnNF_Tc (tyvars', theta, tau)
232 %************************************************************************
234 \subsection{Putting and getting mutable type variables}
236 %************************************************************************
239 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
240 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
247 | not (isMutTyVar tyvar)
248 = pprTrace "putTcTyVar" (ppr tyvar) $
252 = ASSERT( isMutTyVar tyvar )
253 UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
254 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
258 Getting is more interesting. The easy thing to do is just to read, thus:
261 getTcTyVar tyvar = tcReadMutTyVar tyvar
264 But it's more fun to short out indirections on the way: If this
265 version returns a TyVar, then that TyVar is unbound. If it returns
266 any other type, then there might be bound TyVars embedded inside it.
268 We return Nothing iff the original box was unbound.
272 | not (isMutTyVar tyvar)
273 = pprTrace "getTcTyVar" (ppr tyvar) $
274 returnNF_Tc (Just (mkTyVarTy tyvar))
277 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
278 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
280 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
281 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
282 returnNF_Tc (Just ty')
284 Nothing -> returnNF_Tc Nothing
286 short_out :: TcType -> NF_TcM TcType
287 short_out ty@(TyVarTy tyvar)
288 | not (isMutTyVar tyvar)
292 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
294 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
295 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
298 other -> returnNF_Tc ty
300 short_out other_ty = returnNF_Tc other_ty
304 %************************************************************************
306 \subsection{Zonking -- the exernal interfaces}
308 %************************************************************************
310 ----------------- Type variables
313 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
314 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
316 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
317 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
318 returnNF_Tc (tyVarsOfTypes tys)
320 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
321 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
323 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
324 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
325 -- Usually this job is done by checkSigTyVars, but in a couple of places
326 -- that is overkill, so we use this simpler chap
327 zonkTcSigTyVars tyvars
328 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
329 returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
332 ----------------- Types
335 zonkTcType :: TcType -> NF_TcM TcType
336 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
338 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
339 zonkTcTypes tys = mapNF_Tc zonkTcType tys
341 zonkTcClassConstraints cts = mapNF_Tc zonk cts
342 where zonk (clas, tys)
343 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
344 returnNF_Tc (clas, new_tys)
346 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
347 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
349 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
350 zonkTcPredType (ClassP c ts) =
351 zonkTcTypes ts `thenNF_Tc` \ new_ts ->
352 returnNF_Tc (ClassP c new_ts)
353 zonkTcPredType (IParam n t) =
354 zonkTcType t `thenNF_Tc` \ new_t ->
355 returnNF_Tc (IParam n new_t)
358 ------------------- These ...ToType, ...ToKind versions
359 are used at the end of type checking
362 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
364 = mapNF_Tc zonk_it pairs
366 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
367 returnNF_Tc (name, kind)
369 -- When zonking a kind, we want to
370 -- zonk a *kind* variable to (Type *)
371 -- zonk a *boxity* variable to *
372 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
373 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
374 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
376 zonkTcTypeToType :: TcType -> NF_TcM Type
377 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
379 -- Zonk a mutable but unbound type variable to
380 -- Void if it has kind Lifted
382 -- We know it's unbound even though we don't carry an environment,
383 -- because at the binding site for a type variable we bind the
384 -- mutable tyvar to a fresh immutable one. So the mutable store
385 -- plays the role of an environment. If we come across a mutable
386 -- type variable that isn't so bound, it must be completely free.
387 zonk_unbound_tyvar tv
388 | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
389 = putTcTyVar tv voidTy -- Just to avoid creating a new tycon in
390 -- this vastly common case
392 = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
396 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
397 -- type variable tv. Same name too, apart from
398 -- making it start with a colon (sigh)
399 -- I dread to think what will happen if this gets out into an
400 -- interface file. Catastrophe likely. Major sigh.
401 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
402 mkPrimTyCon tc_name kind 0 [] VoidRep
404 tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
406 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
407 -- of a type variable, at the *end* of type checking. It changes
408 -- the *mutable* type variable into an *immutable* one.
410 -- It does this by making an immutable version of tv and binds tv to it.
411 -- Now any bound occurences of the original type variable will get
412 -- zonked to the immutable version.
414 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
415 zonkTcTyVarToTyVar tv
417 -- Make an immutable version, defaulting
418 -- the kind to lifted if necessary
419 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
420 immut_tv_ty = mkTyVarTy immut_tv
422 zap tv = putTcTyVar tv immut_tv_ty
423 -- Bind the mutable version to the immutable one
425 -- If the type variable is mutable, then bind it to immut_tv_ty
426 -- so that all other occurrences of the tyvar will get zapped too
427 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
429 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
435 %************************************************************************
437 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
439 %* For internal use only! *
441 %************************************************************************
444 -- zonkType is used for Kinds as well
446 -- For unbound, mutable tyvars, zonkType uses the function given to it
447 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
448 -- type variable and zonks the kind too
450 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
451 -- see zonkTcType, and zonkTcTypeToType
454 zonkType unbound_var_fn ty
457 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
458 returnNF_Tc (TyConApp tycon tys')
460 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
461 go ty2 `thenNF_Tc` \ ty2' ->
462 returnNF_Tc (NoteTy (SynNote ty1') ty2')
464 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
466 go (SourceTy p) = go_pred p `thenNF_Tc` \ p' ->
467 returnNF_Tc (SourceTy p')
469 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
470 go res `thenNF_Tc` \ res' ->
471 returnNF_Tc (FunTy arg' res')
473 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
474 go arg `thenNF_Tc` \ arg' ->
475 returnNF_Tc (mkAppTy fun' arg')
477 go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
478 go ty `thenNF_Tc` \ ty' ->
479 returnNF_Tc (UsageTy u' ty')
481 -- The two interesting cases!
482 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
484 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
485 go ty `thenNF_Tc` \ ty' ->
486 returnNF_Tc (ForAllTy tyvar' ty')
488 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
489 returnNF_Tc (ClassP c tys')
490 go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
491 returnNF_Tc (NType tc tys')
492 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
493 returnNF_Tc (IParam n ty')
495 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
496 -> TcTyVar -> NF_TcM TcType
497 zonkTyVar unbound_var_fn tyvar
498 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
499 -- zonking a forall type, when the bound type variable
500 -- needn't be mutable
501 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
502 returnNF_Tc (TyVarTy tyvar)
505 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
507 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
508 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
513 %************************************************************************
515 \subsection{Checking a user type}
517 %************************************************************************
519 When dealing with a user-written type, we first translate it from an HsType
520 to a Type, performing kind checking, and then check various things that should
521 be true about it. We don't want to perform these checks at the same time
522 as the initial translation because (a) they are unnecessary for interface-file
523 types and (b) when checking a mutually recursive group of type and class decls,
524 we can't "look" at the tycons/classes yet.
526 One thing we check for is 'rank'.
528 Rank 0: monotypes (no foralls)
529 Rank 1: foralls at the front only, Rank 0 inside
530 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
532 basic ::= tyvar | T basic ... basic
534 r2 ::= forall tvs. cxt => r2a
535 r2a ::= r1 -> r2a | basic
536 r1 ::= forall tvs. cxt => r0
537 r0 ::= r0 -> r0 | basic
542 = FunSigCtxt Name -- Function type signature
543 | ExprSigCtxt -- Expression type signature
544 | ConArgCtxt Name -- Data constructor argument
545 | TySynCtxt Name -- RHS of a type synonym decl
546 | GenPatCtxt -- Pattern in generic decl
547 -- f{| a+b |} (Inl x) = ...
548 | PatSigCtxt -- Type sig in pattern
550 | ResSigCtxt -- Result type sig
552 | ForSigCtxt Name -- Foreign inport or export signature
553 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
555 -- Notes re TySynCtxt
556 -- We allow type synonyms that aren't types; e.g. type List = []
558 -- If the RHS mentions tyvars that aren't in scope, we'll
559 -- quantify over them:
560 -- e.g. type T = a->a
561 -- will become type T = forall a. a->a
563 -- With gla-exts that's right, but for H98 we should complain.
566 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
567 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
568 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
569 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
570 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
571 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
572 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
573 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
574 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
578 checkValidType :: UserTypeCtxt -> Type -> TcM ()
579 -- Checks that the type is valid for the given context
580 checkValidType ctxt ty
581 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
588 FunSigCtxt _ | gla_exts -> 2
590 ConArgCtxt _ | gla_exts -> 2 -- We are given the type of the entire
591 | otherwise -> 1 -- constructor; hence rank 1 is ok
592 TySynCtxt _ | gla_exts -> 1
597 actual_kind = typeKind ty
599 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
601 kind_ok = case ctxt of
602 TySynCtxt _ -> True -- Any kind will do
603 GenPatCtxt -> actual_kind_is_lifted
604 ForSigCtxt _ -> actual_kind_is_lifted
605 other -> isTypeKind actual_kind
607 tcAddErrCtxt (checkTypeCtxt ctxt ty) $
609 -- Check that the thing has kind Type, and is lifted if necessary
610 checkTc kind_ok (kindErr actual_kind) `thenTc_`
612 -- Check the internal validity of the type itself
613 check_poly_type rank ty
616 checkTypeCtxt ctxt ty
617 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
618 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
620 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
621 -- something strange like {Eq k} -> k -> k, because there is no
622 -- ForAll at the top of the type. Since this is going to the user
623 -- we want it to look like a proper Haskell type even then; hence the hack
625 -- This shows up in the complaint about
627 -- op :: Eq a => a -> a
628 ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
631 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
637 check_poly_type :: Rank -> Type -> TcM ()
638 check_poly_type rank ty
640 = check_tau_type 0 False ty
641 | otherwise -- rank > 0
643 (tvs, theta, tau) = tcSplitSigmaTy ty
645 check_valid_theta SigmaCtxt theta `thenTc_`
646 check_tau_type (rank-1) False tau `thenTc_`
647 checkAmbiguity tvs theta tau
649 ----------------------------------------
650 check_arg_type :: Type -> TcM ()
651 -- The sort of type that can instantiate a type variable,
652 -- or be the argument of a type constructor.
653 -- Not an unboxed tuple, not a forall.
654 -- Other unboxed types are very occasionally allowed as type
655 -- arguments depending on the kind of the type constructor
657 -- For example, we want to reject things like:
659 -- instance Ord a => Ord (forall s. T s a)
661 -- g :: T s (forall b.b)
663 -- NB: unboxed tuples can have polymorphic or unboxed args.
664 -- This happens in the workers for functions returning
665 -- product types with polymorphic components.
666 -- But not in user code
668 -- Question: what about nested unboxed tuples?
669 -- Currently rejected.
671 = check_tau_type 0 False ty `thenTc_`
672 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
674 ----------------------------------------
675 check_tau_type :: Rank -> Bool -> Type -> TcM ()
676 -- Rank is allowed rank for function args
677 -- No foralls otherwise
678 -- Bool is True iff unboxed tuple are allowed here
680 check_tau_type rank ubx_tup_ok ty@(UsageTy _ _) = failWithTc (usageTyErr ty)
681 check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
682 check_tau_type rank ubx_tup_ok (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
683 check_source_ty dflags TypeCtxt sty
684 check_tau_type rank ubx_tup_ok (TyVarTy _) = returnTc ()
685 check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
686 = check_poly_type rank arg_ty `thenTc_`
687 check_tau_type rank True res_ty
689 check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
690 = check_arg_type ty1 `thenTc_` check_arg_type ty2
692 check_tau_type rank ubx_tup_ok (NoteTy note ty)
693 = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty
695 check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
697 = checkTc syn_arity_ok arity_msg `thenTc_`
698 mapTc_ check_arg_type tys
700 | isUnboxedTupleTyCon tc
701 = checkTc ubx_tup_ok ubx_tup_msg `thenTc_`
702 mapTc_ (check_tau_type 0 True) tys -- Args are allowed to be unlifted, or
703 -- more unboxed tuples, so can't use check_arg_ty
706 = mapTc_ check_arg_type tys
709 syn_arity_ok = tc_arity <= n_args
710 -- It's OK to have an *over-applied* type synonym
711 -- data Tree a b = ...
712 -- type Foo a = Tree [a]
713 -- f :: Foo a b -> ...
715 tc_arity = tyConArity tc
717 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
718 ubx_tup_msg = ubxArgTyErr ty
720 ----------------------------------------
721 check_note (FTVNote _) = returnTc ()
722 check_note (SynNote ty) = check_tau_type 0 False ty
728 is ambiguous if P contains generic variables
729 (i.e. one of the Vs) that are not mentioned in tau
731 However, we need to take account of functional dependencies
732 when we speak of 'mentioned in tau'. Example:
733 class C a b | a -> b where ...
735 forall x y. (C x y) => x
736 is not ambiguous because x is mentioned and x determines y
738 NOTE: In addition, GHC insists that at least one type variable
739 in each constraint is in V. So we disallow a type like
740 forall a. Eq b => b -> b
741 even in a scope where b is in scope.
742 This is the is_free test below.
744 NB; the ambiguity check is only used for *user* types, not for types
745 coming from inteface files. The latter can legitimately have
746 ambiguous types. Example
748 class S a where s :: a -> (Int,Int)
749 instance S Char where s _ = (1,1)
750 f:: S a => [a] -> Int -> (Int,Int)
751 f (_::[a]) x = (a*x,b)
752 where (a,b) = s (undefined::a)
754 Here the worker for f gets the type
755 fw :: forall a. S a => Int -> (# Int, Int #)
757 If the list of tv_names is empty, we have a monotype, and then we
758 don't need to check for ambiguity either, because the test can't fail
762 checkAmbiguity :: [TyVar] -> ThetaType -> TauType -> TcM ()
763 checkAmbiguity forall_tyvars theta tau
764 = mapTc_ check_pred theta `thenTc_`
767 tau_vars = tyVarsOfType tau
768 extended_tau_vars = grow theta tau_vars
770 is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
771 not (ct_var `elemVarSet` extended_tau_vars)
772 is_free ct_var = not (ct_var `elem` forall_tyvars)
774 check_pred pred = checkTc (not any_ambig) (ambigErr pred) `thenTc_`
775 checkTc (isIPPred pred || not all_free) (freeErr pred)
777 ct_vars = varSetElems (tyVarsOfPred pred)
778 all_free = all is_free ct_vars
779 any_ambig = any is_ambig ct_vars
784 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
785 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
786 ptext SLIT("must be reachable from the type after the =>"))]
790 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
791 ptext SLIT("are already in scope"),
792 nest 4 (ptext SLIT("At least one must be universally quantified here"))
795 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
796 usageTyErr ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
797 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
798 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
799 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
802 %************************************************************************
804 \subsection{Checking a theta or source type}
806 %************************************************************************
810 = ClassSCCtxt Name -- Superclasses of clas
811 | SigmaCtxt -- Context of a normal for-all type
812 | DataTyCtxt Name -- Context of a data decl
813 | TypeCtxt -- Source type in an ordinary type
814 | InstThetaCtxt -- Context of an instance decl
815 | InstHeadCtxt -- Head of an instance decl
817 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
818 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
819 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
820 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
821 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
822 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
826 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
827 checkValidTheta ctxt theta
828 = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
830 -------------------------
831 check_valid_theta ctxt []
833 check_valid_theta ctxt theta
834 = getDOptsTc `thenNF_Tc` \ dflags ->
835 warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
836 mapTc_ (check_source_ty dflags ctxt) theta
838 (_,dups) = removeDups tcCmpPred theta
840 -------------------------
841 check_source_ty dflags ctxt pred@(ClassP cls tys)
842 = -- Class predicates are valid in all contexts
843 mapTc_ check_arg_type tys `thenTc_`
844 checkTc (arity == n_tys) arity_err `thenTc_`
845 checkTc (all tyvar_head tys || arby_preds_ok) (predTyVarErr pred)
848 class_name = className cls
849 arity = classArity cls
851 arity_err = arityErr "Class" class_name arity n_tys
853 arby_preds_ok = case ctxt of
854 InstHeadCtxt -> True -- We check for instance-head formation
855 -- in checkValidInstHead
856 InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
857 other -> dopt Opt_GlasgowExts dflags
859 check_source_ty dflags SigmaCtxt (IParam name ty) = check_arg_type ty
860 check_source_ty dflags TypeCtxt (NType tc tys) = mapTc_ check_arg_type tys
863 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
865 -------------------------
866 tyvar_head ty -- Haskell 98 allows predicates of form
867 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
868 | otherwise -- where a is a type variable
869 = case tcSplitAppTy_maybe ty of
870 Just (ty, _) -> tyvar_head ty
875 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
876 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
877 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
879 checkThetaCtxt ctxt theta
880 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
881 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
885 %************************************************************************
887 \subsection{Checking for a decent instance head type}
889 %************************************************************************
891 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
892 it must normally look like: @instance Foo (Tycon a b c ...) ...@
894 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
895 flag is on, or (2)~the instance is imported (they must have been
896 compiled elsewhere). In these cases, we let them go through anyway.
898 We can also have instances for functions: @instance Foo (a -> b) ...@.
901 checkValidInstHead :: Type -> TcM ()
903 checkValidInstHead ty -- Should be a source type
904 = case tcSplitPredTy_maybe ty of {
905 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
908 case getClassPredTys_maybe pred of {
909 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
912 getDOptsTc `thenNF_Tc` \ dflags ->
913 mapTc_ check_arg_type tys `thenTc_`
914 check_inst_head dflags clas tys
917 check_inst_head dflags clas tys
919 -- A user declaration of a CCallable/CReturnable instance
920 -- must be for a "boxed primitive" type.
921 (clas `hasKey` cCallableClassKey
922 && not (ccallable_type first_ty))
923 || (clas `hasKey` cReturnableClassKey
924 && not (creturnable_type first_ty))
925 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
927 -- If GlasgowExts then check at least one isn't a type variable
928 | dopt Opt_GlasgowExts dflags
929 = check_tyvars dflags clas tys
931 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
933 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
934 not (isSynTyCon tycon), -- ...but not a synonym
935 all tcIsTyVarTy arg_tys, -- Applied to type variables
936 length (varSetElems (tyVarsOfTypes arg_tys)) == length arg_tys
937 -- This last condition checks that all the type variables are distinct
941 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
946 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
947 creturnable_type ty = isFFIImportResultTy dflags ty
949 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
950 text "where T is not a synonym, and a,b,c are distinct type variables")
952 check_tyvars dflags clas tys
953 -- Check that at least one isn't a type variable
954 -- unless -fallow-undecideable-instances
955 | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
956 | not (all tcIsTyVarTy tys) = returnTc ()
957 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
959 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
960 $$ ptext SLIT("Use -fallow-undecidable-instances to lift this restriction"))
964 instTypeErr pp_ty msg
965 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
968 nonBoxedPrimCCallErr clas inst_ty
969 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
970 4 (pprClassPred clas [inst_ty])
974 %************************************************************************
976 \subsection{Kind unification}
978 %************************************************************************
981 unifyKind :: TcKind -- Expected
985 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
988 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
989 unifyKinds [] [] = returnTc ()
990 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
992 unifyKinds _ _ = panic "unifyKinds: length mis-match"
996 unifyOpenTypeKind :: TcKind -> TcM ()
997 -- Ensures that the argument kind is of the form (Type bx)
998 -- for some boxity bx
1000 unifyOpenTypeKind ty@(TyVarTy tyvar)
1001 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1003 Just ty' -> unifyOpenTypeKind ty'
1004 other -> unify_open_kind_help ty
1006 unifyOpenTypeKind ty
1007 | isTypeKind ty = returnTc ()
1008 | otherwise = unify_open_kind_help ty
1010 unify_open_kind_help ty -- Revert to ordinary unification
1011 = newBoxityVar `thenNF_Tc` \ boxity ->
1012 unifyKind ty (mkTyConApp typeCon [boxity])
1016 %************************************************************************
1018 \subsection[Unify-exported]{Exported unification functions}
1020 %************************************************************************
1022 The exported functions are all defined as versions of some
1023 non-exported generic functions.
1025 Unify two @TauType@s. Dead straightforward.
1028 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
1029 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
1030 = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
1031 uTys ty1 ty1 ty2 ty2
1034 @unifyTauTyList@ unifies corresponding elements of two lists of
1035 @TauType@s. It uses @uTys@ to do the real work. The lists should be
1036 of equal length. We charge down the list explicitly so that we can
1037 complain if their lengths differ.
1040 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
1041 unifyTauTyLists [] [] = returnTc ()
1042 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
1043 unifyTauTyLists tys1 tys2
1044 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
1047 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
1048 all together. It is used, for example, when typechecking explicit
1049 lists, when all the elts should be of the same type.
1052 unifyTauTyList :: [TcTauType] -> TcM ()
1053 unifyTauTyList [] = returnTc ()
1054 unifyTauTyList [ty] = returnTc ()
1055 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
1059 %************************************************************************
1061 \subsection[Unify-uTys]{@uTys@: getting down to business}
1063 %************************************************************************
1065 @uTys@ is the heart of the unifier. Each arg happens twice, because
1066 we want to report errors in terms of synomyms if poss. The first of
1067 the pair is used in error messages only; it is always the same as the
1068 second, except that if the first is a synonym then the second may be a
1069 de-synonym'd version. This way we get better error messages.
1071 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
1074 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
1075 -- ty1 is the *expected* type
1077 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
1078 -- ty2 is the *actual* type
1081 -- Always expand synonyms (see notes at end)
1082 -- (this also throws away FTVs)
1083 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
1084 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
1086 -- Ignore usage annotations inside typechecker
1087 uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
1088 uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
1090 -- Variables; go for uVar
1091 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
1092 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
1093 -- "True" means args swapped
1096 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
1097 | n1 == n2 = uTys t1 t1 t2 t2
1098 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
1099 | c1 == c2 = unifyTauTyLists tys1 tys2
1100 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
1101 | tc1 == tc2 = unifyTauTyLists tys1 tys2
1103 -- Functions; just check the two parts
1104 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
1105 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
1107 -- Type constructors must match
1108 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
1109 | con1 == con2 && length tys1 == length tys2
1110 = unifyTauTyLists tys1 tys2
1112 | con1 == openKindCon
1113 -- When we are doing kind checking, we might match a kind '?'
1114 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
1115 -- (CCallable Int) and (CCallable Int#) are both OK
1116 = unifyOpenTypeKind ps_ty2
1118 -- Applications need a bit of care!
1119 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1120 -- NB: we've already dealt with type variables and Notes,
1121 -- so if one type is an App the other one jolly well better be too
1122 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
1123 = case tcSplitAppTy_maybe ty2 of
1124 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
1125 Nothing -> unifyMisMatch ps_ty1 ps_ty2
1127 -- Now the same, but the other way round
1128 -- Don't swap the types, because the error messages get worse
1129 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
1130 = case tcSplitAppTy_maybe ty1 of
1131 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
1132 Nothing -> unifyMisMatch ps_ty1 ps_ty2
1134 -- Not expecting for-alls in unification
1135 -- ... but the error message from the unifyMisMatch more informative
1136 -- than a panic message!
1138 -- Anything else fails
1139 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
1145 If you are tempted to make a short cut on synonyms, as in this
1149 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
1150 -- NO = if (con1 == con2) then
1151 -- NO -- Good news! Same synonym constructors, so we can shortcut
1152 -- NO -- by unifying their arguments and ignoring their expansions.
1153 -- NO unifyTauTypeLists args1 args2
1155 -- NO -- Never mind. Just expand them and try again
1159 then THINK AGAIN. Here is the whole story, as detected and reported
1160 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
1162 Here's a test program that should detect the problem:
1166 x = (1 :: Bogus Char) :: Bogus Bool
1169 The problem with [the attempted shortcut code] is that
1173 is not a sufficient condition to be able to use the shortcut!
1174 You also need to know that the type synonym actually USES all
1175 its arguments. For example, consider the following type synonym
1176 which does not use all its arguments.
1181 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
1182 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
1183 would fail, even though the expanded forms (both \tr{Int}) should
1186 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
1187 unnecessarily bind \tr{t} to \tr{Char}.
1189 ... You could explicitly test for the problem synonyms and mark them
1190 somehow as needing expansion, perhaps also issuing a warning to the
1195 %************************************************************************
1197 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
1199 %************************************************************************
1201 @uVar@ is called when at least one of the types being unified is a
1202 variable. It does {\em not} assume that the variable is a fixed point
1203 of the substitution; rather, notice that @uVar@ (defined below) nips
1204 back into @uTys@ if it turns out that the variable is already bound.
1207 uVar :: Bool -- False => tyvar is the "expected"
1208 -- True => ty is the "expected" thing
1210 -> TcTauType -> TcTauType -- printing and real versions
1213 uVar swapped tv1 ps_ty2 ty2
1214 = getTcTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
1216 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
1217 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
1218 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
1220 -- Expand synonyms; ignore FTVs
1221 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
1222 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
1225 -- The both-type-variable case
1226 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
1228 -- Same type variable => no-op
1232 -- Distinct type variables
1233 -- ASSERT maybe_ty1 /= Just
1235 = getTcTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
1237 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
1239 Nothing | update_tv2
1241 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
1242 putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
1246 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
1247 (putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
1252 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
1253 -- Try to get rid of open type variables as soon as poss
1255 nicer_to_update_tv2 = isSigTyVar tv1
1256 -- Don't unify a signature type variable if poss
1257 || isSystemName (varName tv2)
1258 -- Try to update sys-y type variables in preference to sig-y ones
1260 -- Second one isn't a type variable
1261 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
1262 = -- Check that the kinds match
1263 checkKinds swapped tv1 non_var_ty2 `thenTc_`
1265 -- Check that tv1 isn't a type-signature type variable
1266 checkTcM (not (isSigTyVar tv1))
1267 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
1269 -- Check that we aren't losing boxity info (shouldn't happen)
1270 warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
1271 ((ppr tv1 <+> ppr (tyVarKind tv1)) $$
1272 (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2))) `thenNF_Tc_`
1275 -- Basically we want to update tv1 := ps_ty2
1276 -- because ps_ty2 has type-synonym info, which improves later error messages
1281 -- f :: (A a -> a -> ()) -> ()
1285 -- x = f (\ x p -> p x)
1287 -- In the application (p x), we try to match "t" with "A t". If we go
1288 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
1289 -- an infinite loop later.
1290 -- But we should not reject the program, because A t = ().
1291 -- Rather, we should bind t to () (= non_var_ty2).
1293 -- That's why we have this two-state occurs-check
1294 zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
1295 if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
1296 putTcTyVar tv1 ps_ty2' `thenNF_Tc_`
1299 zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
1300 if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
1301 -- This branch rarely succeeds, except in strange cases
1302 -- like that in the example above
1303 putTcTyVar tv1 non_var_ty2' `thenNF_Tc_`
1306 failWithTcM (unifyOccurCheck tv1 ps_ty2')
1309 checkKinds swapped tv1 ty2
1310 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
1311 -- We need to check that we don't unify a lifted type variable with an
1312 -- unlifted type: e.g. (id 3#) is illegal
1313 | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
1314 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
1319 (k1,k2) | swapped = (tk2,tk1)
1320 | otherwise = (tk1,tk2)
1326 %************************************************************************
1328 \subsection[Unify-fun]{@unifyFunTy@}
1330 %************************************************************************
1332 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
1335 unifyFunTy :: TcType -- Fail if ty isn't a function type
1336 -> TcM (TcType, TcType) -- otherwise return arg and result types
1338 unifyFunTy ty@(TyVarTy tyvar)
1339 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1341 Just ty' -> unifyFunTy ty'
1342 other -> unify_fun_ty_help ty
1345 = case tcSplitFunTy_maybe ty of
1346 Just arg_and_res -> returnTc arg_and_res
1347 Nothing -> unify_fun_ty_help ty
1349 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
1350 = newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
1351 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
1352 unifyTauTy ty (mkFunTy arg res) `thenTc_`
1357 unifyListTy :: TcType -- expected list type
1358 -> TcM TcType -- list element type
1360 unifyListTy ty@(TyVarTy tyvar)
1361 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1363 Just ty' -> unifyListTy ty'
1364 other -> unify_list_ty_help ty
1367 = case tcSplitTyConApp_maybe ty of
1368 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
1369 other -> unify_list_ty_help ty
1371 unify_list_ty_help ty -- Revert to ordinary unification
1372 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
1373 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
1378 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
1379 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
1380 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1382 Just ty' -> unifyTupleTy boxity arity ty'
1383 other -> unify_tuple_ty_help boxity arity ty
1385 unifyTupleTy boxity arity ty
1386 = case tcSplitTyConApp_maybe ty of
1387 Just (tycon, arg_tys)
1388 | isTupleTyCon tycon
1389 && tyConArity tycon == arity
1390 && tupleTyConBoxity tycon == boxity
1392 other -> unify_tuple_ty_help boxity arity ty
1394 unify_tuple_ty_help boxity arity ty
1395 = newTyVarTys arity kind `thenNF_Tc` \ arg_tys ->
1396 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
1399 kind | isBoxed boxity = liftedTypeKind
1400 | otherwise = openTypeKind
1404 %************************************************************************
1406 \subsection[Unify-context]{Errors and contexts}
1408 %************************************************************************
1414 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
1415 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
1416 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
1417 returnNF_Tc (err ty1' ty2')
1419 err ty1 ty2 = (env1,
1422 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
1423 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
1426 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
1428 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
1429 -- tv1 is zonked already
1430 = zonkTcType ty2 `thenNF_Tc` \ ty2' ->
1431 returnNF_Tc (err ty2')
1433 err ty2 = (env2, ptext SLIT("When matching types") <+>
1434 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
1436 (pp_expected, pp_actual) | swapped = (pp2, pp1)
1437 | otherwise = (pp1, pp2)
1438 (env1, tv1') = tidyTyVar tidy_env tv1
1439 (env2, ty2') = tidyOpenType env1 ty2
1443 unifyMisMatch ty1 ty2
1444 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
1445 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
1447 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
1448 msg = hang (ptext SLIT("Couldn't match"))
1449 4 (sep [quotes (ppr tidy_ty1),
1450 ptext SLIT("against"),
1451 quotes (ppr tidy_ty2)])
1453 failWithTcM (env, msg)
1455 unifyWithSigErr tyvar ty
1456 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
1457 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
1459 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
1460 (env2, tidy_ty) = tidyOpenType env1 ty
1462 unifyOccurCheck tyvar ty
1463 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
1464 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1466 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
1467 (env2, tidy_ty) = tidyOpenType env1 ty