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 tcInstSigTyVars, 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 ( TcType, TcRhoType, TcThetaType, TcTauType, TcPredType,
54 TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
56 tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
57 tcSplitTyConApp_maybe, tcSplitFunTy_maybe, tcSplitForAllTys,
58 tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy,
59 isUnLiftedType, isIPPred, isUserTyVar, isSkolemTyVar,
61 mkAppTy, mkTyVarTy, mkTyVarTys, mkFunTy, mkTyConApp,
62 tyVarsOfPred, getClassPredTys_maybe,
64 liftedTypeKind, unliftedTypeKind, openTypeKind, defaultKind, superKind,
65 superBoxity, liftedBoxity, hasMoreBoxityInfo, typeKind,
66 tyVarsOfType, tyVarsOfTypes, tidyOpenType, tidyOpenTypes, tidyOpenTyVar,
69 isFFIArgumentTy, isFFIImportResultTy
71 import Subst ( Subst, mkTopTyVarSubst, substTy )
72 import Class ( classArity, className )
73 import TyCon ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
74 isTupleTyCon, tyConArity, tupleTyConBoxity, tyConName )
75 import PrimRep ( PrimRep(VoidRep) )
76 import Var ( TyVar, varName, tyVarKind, tyVarName, isTyVar, mkTyVar,
77 isMutTyVar, mutTyVarDetails )
80 import TcMonad -- TcType, amongst others
81 import TysWiredIn ( voidTy, listTyCon, mkListTy, mkTupleTy )
82 import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
83 import ForeignCall ( Safety(..) )
84 import FunDeps ( grow )
85 import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
86 import Name ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
87 mkLocalName, mkDerivedTyConOcc, isSystemName
90 import BasicTypes ( Boxity, Arity, isBoxed )
91 import CmdLineOpts ( dopt, DynFlag(..) )
92 import Unique ( Uniquable(..) )
93 import SrcLoc ( noSrcLoc )
94 import Util ( nOfThem, isSingleton, equalLength )
95 import ListSetOps ( removeDups )
100 %************************************************************************
102 \subsection{New type variables}
104 %************************************************************************
107 newTyVar :: Kind -> NF_TcM TcTyVar
109 = tcGetUnique `thenNF_Tc` \ uniq ->
110 tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind VanillaTv
112 newTyVarTy :: Kind -> NF_TcM TcType
114 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
115 returnNF_Tc (TyVarTy tc_tyvar)
117 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
118 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
120 newKindVar :: NF_TcM TcKind
122 = tcGetUnique `thenNF_Tc` \ uniq ->
123 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind VanillaTv `thenNF_Tc` \ kv ->
124 returnNF_Tc (TyVarTy kv)
126 newKindVars :: Int -> NF_TcM [TcKind]
127 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
129 newBoxityVar :: NF_TcM TcKind
131 = tcGetUnique `thenNF_Tc` \ uniq ->
132 tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity VanillaTv `thenNF_Tc` \ kv ->
133 returnNF_Tc (TyVarTy kv)
137 %************************************************************************
139 \subsection{Type instantiation}
141 %************************************************************************
143 I don't understand why this is needed
144 An old comments says "No need for tcSplitForAllTyM because a type
145 variable can't be instantiated to a for-all type"
146 But the same is true of rho types!
149 tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
153 -- A type variable is never instantiated to a dictionary type,
154 -- so we don't need to do a tcReadVar on the "arg".
155 go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
156 Just pair -> go res res (pair:ts)
157 Nothing -> returnNF_Tc (reverse ts, syn_t)
158 go syn_t (NoteTy n t) ts = go syn_t t ts
159 go syn_t (TyVarTy tv) ts = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
161 Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
162 other -> returnNF_Tc (reverse ts, syn_t)
163 go syn_t (UsageTy _ t) ts = go syn_t t ts
164 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
168 %************************************************************************
170 \subsection{Type instantiation}
172 %************************************************************************
174 Instantiating a bunch of type variables
177 tcInstTyVars :: [TyVar]
178 -> NF_TcM ([TcTyVar], [TcType], Subst)
181 = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
183 tys = mkTyVarTys tc_tyvars
185 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
186 -- Since the tyvars are freshly made,
187 -- they cannot possibly be captured by
188 -- any existing for-alls. Hence mkTopTyVarSubst
191 = tcGetUnique `thenNF_Tc` \ uniq ->
193 name = setNameUnique (tyVarName tyvar) uniq
194 -- Note that we don't change the print-name
195 -- This won't confuse the type checker but there's a chance
196 -- that two different tyvars will print the same way
197 -- in an error message. -dppr-debug will show up the difference
198 -- Better watch out for this. If worst comes to worst, just
199 -- use mkSysLocalName.
201 tcNewMutTyVar name (tyVarKind tyvar) VanillaTv
203 tcInstSigTyVars :: TyVarDetails -> [TyVar] -> NF_TcM [TcTyVar]
204 tcInstSigTyVars details tyvars -- Very similar to tcInstTyVar
205 = tcGetUniques `thenNF_Tc` \ uniqs ->
206 listTc [ ASSERT( not (kind `eqKind` openTypeKind) ) -- Shouldn't happen
207 tcNewMutTyVar name kind details
208 | (tyvar, uniq) <- tyvars `zip` uniqs,
209 let name = setNameUnique (tyVarName tyvar) uniq,
210 let kind = tyVarKind tyvar
214 @tcInstType@ instantiates the outer-level for-alls of a TcType with
215 fresh type variables, splits off the dictionary part, and returns the results.
218 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
220 = case tcSplitForAllTys ty of
221 ([], rho) -> -- There may be overloading but no type variables;
222 -- (?x :: Int) => Int -> Int
224 (theta, tau) = tcSplitRhoTy rho -- Used to be tcSplitRhoTyM
226 returnNF_Tc ([], theta, tau)
228 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
230 (theta, tau) = tcSplitRhoTy (substTy tenv rho) -- Used to be tcSplitRhoTyM
232 returnNF_Tc (tyvars', theta, tau)
237 %************************************************************************
239 \subsection{Putting and getting mutable type variables}
241 %************************************************************************
244 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
245 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
252 | not (isMutTyVar tyvar)
253 = pprTrace "putTcTyVar" (ppr tyvar) $
257 = ASSERT( isMutTyVar tyvar )
258 UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
259 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
263 Getting is more interesting. The easy thing to do is just to read, thus:
266 getTcTyVar tyvar = tcReadMutTyVar tyvar
269 But it's more fun to short out indirections on the way: If this
270 version returns a TyVar, then that TyVar is unbound. If it returns
271 any other type, then there might be bound TyVars embedded inside it.
273 We return Nothing iff the original box was unbound.
277 | not (isMutTyVar tyvar)
278 = pprTrace "getTcTyVar" (ppr tyvar) $
279 returnNF_Tc (Just (mkTyVarTy tyvar))
282 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
283 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
285 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
286 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
287 returnNF_Tc (Just ty')
289 Nothing -> returnNF_Tc Nothing
291 short_out :: TcType -> NF_TcM TcType
292 short_out ty@(TyVarTy tyvar)
293 | not (isMutTyVar tyvar)
297 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
299 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
300 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
303 other -> returnNF_Tc ty
305 short_out other_ty = returnNF_Tc other_ty
309 %************************************************************************
311 \subsection{Zonking -- the exernal interfaces}
313 %************************************************************************
315 ----------------- Type variables
318 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
319 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
321 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
322 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
323 returnNF_Tc (tyVarsOfTypes tys)
325 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
326 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
328 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
329 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
330 -- Usually this job is done by checkSigTyVars, but in a couple of places
331 -- that is overkill, so we use this simpler chap
332 zonkTcSigTyVars tyvars
333 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
334 returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
337 ----------------- Types
340 zonkTcType :: TcType -> NF_TcM TcType
341 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
343 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
344 zonkTcTypes tys = mapNF_Tc zonkTcType tys
346 zonkTcClassConstraints cts = mapNF_Tc zonk cts
347 where zonk (clas, tys)
348 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
349 returnNF_Tc (clas, new_tys)
351 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
352 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
354 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
355 zonkTcPredType (ClassP c ts) =
356 zonkTcTypes ts `thenNF_Tc` \ new_ts ->
357 returnNF_Tc (ClassP c new_ts)
358 zonkTcPredType (IParam n t) =
359 zonkTcType t `thenNF_Tc` \ new_t ->
360 returnNF_Tc (IParam n new_t)
363 ------------------- These ...ToType, ...ToKind versions
364 are used at the end of type checking
367 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
369 = mapNF_Tc zonk_it pairs
371 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
372 returnNF_Tc (name, kind)
374 -- When zonking a kind, we want to
375 -- zonk a *kind* variable to (Type *)
376 -- zonk a *boxity* variable to *
377 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
378 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
379 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
381 zonkTcTypeToType :: TcType -> NF_TcM Type
382 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
384 -- Zonk a mutable but unbound type variable to
385 -- Void if it has kind Lifted
387 -- We know it's unbound even though we don't carry an environment,
388 -- because at the binding site for a type variable we bind the
389 -- mutable tyvar to a fresh immutable one. So the mutable store
390 -- plays the role of an environment. If we come across a mutable
391 -- type variable that isn't so bound, it must be completely free.
392 zonk_unbound_tyvar tv
393 | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
394 = putTcTyVar tv voidTy -- Just to avoid creating a new tycon in
395 -- this vastly common case
397 = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
401 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
402 -- type variable tv. Same name too, apart from
403 -- making it start with a colon (sigh)
404 -- I dread to think what will happen if this gets out into an
405 -- interface file. Catastrophe likely. Major sigh.
406 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
407 mkPrimTyCon tc_name kind 0 [] VoidRep
409 tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
411 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
412 -- of a type variable, at the *end* of type checking. It changes
413 -- the *mutable* type variable into an *immutable* one.
415 -- It does this by making an immutable version of tv and binds tv to it.
416 -- Now any bound occurences of the original type variable will get
417 -- zonked to the immutable version.
419 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
420 zonkTcTyVarToTyVar tv
422 -- Make an immutable version, defaulting
423 -- the kind to lifted if necessary
424 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
425 immut_tv_ty = mkTyVarTy immut_tv
427 zap tv = putTcTyVar tv immut_tv_ty
428 -- Bind the mutable version to the immutable one
430 -- If the type variable is mutable, then bind it to immut_tv_ty
431 -- so that all other occurrences of the tyvar will get zapped too
432 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
434 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
440 %************************************************************************
442 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
444 %* For internal use only! *
446 %************************************************************************
449 -- zonkType is used for Kinds as well
451 -- For unbound, mutable tyvars, zonkType uses the function given to it
452 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
453 -- type variable and zonks the kind too
455 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
456 -- see zonkTcType, and zonkTcTypeToType
459 zonkType unbound_var_fn ty
462 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
463 returnNF_Tc (TyConApp tycon tys')
465 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
466 go ty2 `thenNF_Tc` \ ty2' ->
467 returnNF_Tc (NoteTy (SynNote ty1') ty2')
469 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
471 go (SourceTy p) = go_pred p `thenNF_Tc` \ p' ->
472 returnNF_Tc (SourceTy p')
474 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
475 go res `thenNF_Tc` \ res' ->
476 returnNF_Tc (FunTy arg' res')
478 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
479 go arg `thenNF_Tc` \ arg' ->
480 returnNF_Tc (mkAppTy fun' arg')
482 go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
483 go ty `thenNF_Tc` \ ty' ->
484 returnNF_Tc (UsageTy u' ty')
486 -- The two interesting cases!
487 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
489 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
490 go ty `thenNF_Tc` \ ty' ->
491 returnNF_Tc (ForAllTy tyvar' ty')
493 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
494 returnNF_Tc (ClassP c tys')
495 go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
496 returnNF_Tc (NType tc tys')
497 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
498 returnNF_Tc (IParam n ty')
500 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
501 -> TcTyVar -> NF_TcM TcType
502 zonkTyVar unbound_var_fn tyvar
503 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
504 -- zonking a forall type, when the bound type variable
505 -- needn't be mutable
506 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
507 returnNF_Tc (TyVarTy tyvar)
510 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
512 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
513 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
518 %************************************************************************
520 \subsection{Checking a user type}
522 %************************************************************************
524 When dealing with a user-written type, we first translate it from an HsType
525 to a Type, performing kind checking, and then check various things that should
526 be true about it. We don't want to perform these checks at the same time
527 as the initial translation because (a) they are unnecessary for interface-file
528 types and (b) when checking a mutually recursive group of type and class decls,
529 we can't "look" at the tycons/classes yet. Also, the checks are are rather
530 diverse, and used to really mess up the other code.
532 One thing we check for is 'rank'.
534 Rank 0: monotypes (no foralls)
535 Rank 1: foralls at the front only, Rank 0 inside
536 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
538 basic ::= tyvar | T basic ... basic
540 r2 ::= forall tvs. cxt => r2a
541 r2a ::= r1 -> r2a | basic
542 r1 ::= forall tvs. cxt => r0
543 r0 ::= r0 -> r0 | basic
545 Another thing is to check that type synonyms are saturated.
546 This might not necessarily show up in kind checking.
548 data T k = MkT (k Int)
554 = FunSigCtxt Name -- Function type signature
555 | ExprSigCtxt -- Expression type signature
556 | ConArgCtxt Name -- Data constructor argument
557 | TySynCtxt Name -- RHS of a type synonym decl
558 | GenPatCtxt -- Pattern in generic decl
559 -- f{| a+b |} (Inl x) = ...
560 | PatSigCtxt -- Type sig in pattern
562 | ResSigCtxt -- Result type sig
564 | ForSigCtxt Name -- Foreign inport or export signature
565 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
567 -- Notes re TySynCtxt
568 -- We allow type synonyms that aren't types; e.g. type List = []
570 -- If the RHS mentions tyvars that aren't in scope, we'll
571 -- quantify over them:
572 -- e.g. type T = a->a
573 -- will become type T = forall a. a->a
575 -- With gla-exts that's right, but for H98 we should complain.
578 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
579 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
580 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
581 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
582 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
583 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
584 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
585 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
586 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
590 checkValidType :: UserTypeCtxt -> Type -> TcM ()
591 -- Checks that the type is valid for the given context
592 checkValidType ctxt ty
593 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
600 FunSigCtxt _ | gla_exts -> 2
602 ConArgCtxt _ | gla_exts -> 2 -- We are given the type of the entire
603 | otherwise -> 1 -- constructor; hence rank 1 is ok
604 TySynCtxt _ | gla_exts -> 1
609 actual_kind = typeKind ty
611 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
613 kind_ok = case ctxt of
614 TySynCtxt _ -> True -- Any kind will do
615 GenPatCtxt -> actual_kind_is_lifted
616 ForSigCtxt _ -> actual_kind_is_lifted
617 other -> isTypeKind actual_kind
619 tcAddErrCtxt (checkTypeCtxt ctxt ty) $
621 -- Check that the thing has kind Type, and is lifted if necessary
622 checkTc kind_ok (kindErr actual_kind) `thenTc_`
624 -- Check the internal validity of the type itself
625 check_poly_type rank ty
628 checkTypeCtxt ctxt ty
629 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
630 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
632 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
633 -- something strange like {Eq k} -> k -> k, because there is no
634 -- ForAll at the top of the type. Since this is going to the user
635 -- we want it to look like a proper Haskell type even then; hence the hack
637 -- This shows up in the complaint about
639 -- op :: Eq a => a -> a
640 ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
643 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
649 check_poly_type :: Rank -> Type -> TcM ()
650 check_poly_type rank ty
652 = check_tau_type 0 False ty
653 | otherwise -- rank > 0
655 (tvs, theta, tau) = tcSplitSigmaTy ty
657 check_valid_theta SigmaCtxt theta `thenTc_`
658 check_tau_type (rank-1) False tau `thenTc_`
659 checkAmbiguity tvs theta tau
661 ----------------------------------------
662 check_arg_type :: Type -> TcM ()
663 -- The sort of type that can instantiate a type variable,
664 -- or be the argument of a type constructor.
665 -- Not an unboxed tuple, not a forall.
666 -- Other unboxed types are very occasionally allowed as type
667 -- arguments depending on the kind of the type constructor
669 -- For example, we want to reject things like:
671 -- instance Ord a => Ord (forall s. T s a)
673 -- g :: T s (forall b.b)
675 -- NB: unboxed tuples can have polymorphic or unboxed args.
676 -- This happens in the workers for functions returning
677 -- product types with polymorphic components.
678 -- But not in user code
680 -- Question: what about nested unboxed tuples?
681 -- Currently rejected.
683 = check_tau_type 0 False ty `thenTc_`
684 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
686 ----------------------------------------
687 check_tau_type :: Rank -> Bool -> Type -> TcM ()
688 -- Rank is allowed rank for function args
689 -- No foralls otherwise
690 -- Bool is True iff unboxed tuple are allowed here
692 check_tau_type rank ubx_tup_ok ty@(UsageTy _ _) = failWithTc (usageTyErr ty)
693 check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
694 check_tau_type rank ubx_tup_ok (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
695 check_source_ty dflags TypeCtxt sty
696 check_tau_type rank ubx_tup_ok (TyVarTy _) = returnTc ()
697 check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
698 = check_poly_type rank arg_ty `thenTc_`
699 check_tau_type rank True res_ty
701 check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
702 = check_arg_type ty1 `thenTc_` check_arg_type ty2
704 check_tau_type rank ubx_tup_ok (NoteTy note ty)
705 = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty
707 check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
709 = checkTc syn_arity_ok arity_msg `thenTc_`
710 mapTc_ check_arg_type tys
712 | isUnboxedTupleTyCon tc
713 = checkTc ubx_tup_ok ubx_tup_msg `thenTc_`
714 mapTc_ (check_tau_type 0 True) tys -- Args are allowed to be unlifted, or
715 -- more unboxed tuples, so can't use check_arg_ty
718 = mapTc_ check_arg_type tys
721 syn_arity_ok = tc_arity <= n_args
722 -- It's OK to have an *over-applied* type synonym
723 -- data Tree a b = ...
724 -- type Foo a = Tree [a]
725 -- f :: Foo a b -> ...
727 tc_arity = tyConArity tc
729 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
730 ubx_tup_msg = ubxArgTyErr ty
732 ----------------------------------------
733 check_note (FTVNote _) = returnTc ()
734 check_note (SynNote ty) = check_tau_type 0 False ty
740 is ambiguous if P contains generic variables
741 (i.e. one of the Vs) that are not mentioned in tau
743 However, we need to take account of functional dependencies
744 when we speak of 'mentioned in tau'. Example:
745 class C a b | a -> b where ...
747 forall x y. (C x y) => x
748 is not ambiguous because x is mentioned and x determines y
750 NOTE: In addition, GHC insists that at least one type variable
751 in each constraint is in V. So we disallow a type like
752 forall a. Eq b => b -> b
753 even in a scope where b is in scope.
754 This is the is_free test below.
756 NB; the ambiguity check is only used for *user* types, not for types
757 coming from inteface files. The latter can legitimately have
758 ambiguous types. Example
760 class S a where s :: a -> (Int,Int)
761 instance S Char where s _ = (1,1)
762 f:: S a => [a] -> Int -> (Int,Int)
763 f (_::[a]) x = (a*x,b)
764 where (a,b) = s (undefined::a)
766 Here the worker for f gets the type
767 fw :: forall a. S a => Int -> (# Int, Int #)
769 If the list of tv_names is empty, we have a monotype, and then we
770 don't need to check for ambiguity either, because the test can't fail
774 checkAmbiguity :: [TyVar] -> ThetaType -> TauType -> TcM ()
775 checkAmbiguity forall_tyvars theta tau
776 = mapTc_ check_pred theta `thenTc_`
779 tau_vars = tyVarsOfType tau
780 extended_tau_vars = grow theta tau_vars
782 is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
783 not (ct_var `elemVarSet` extended_tau_vars)
784 is_free ct_var = not (ct_var `elem` forall_tyvars)
786 check_pred pred = checkTc (not any_ambig) (ambigErr pred) `thenTc_`
787 checkTc (isIPPred pred || not all_free) (freeErr pred)
789 ct_vars = varSetElems (tyVarsOfPred pred)
790 all_free = all is_free ct_vars
791 any_ambig = any is_ambig ct_vars
796 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
797 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
798 ptext SLIT("must be reachable from the type after the =>"))]
802 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
803 ptext SLIT("are already in scope"),
804 nest 4 (ptext SLIT("At least one must be universally quantified here"))
807 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
808 usageTyErr ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
809 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
810 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
811 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
814 %************************************************************************
816 \subsection{Checking a theta or source type}
818 %************************************************************************
822 = ClassSCCtxt Name -- Superclasses of clas
823 | SigmaCtxt -- Context of a normal for-all type
824 | DataTyCtxt Name -- Context of a data decl
825 | TypeCtxt -- Source type in an ordinary type
826 | InstThetaCtxt -- Context of an instance decl
827 | InstHeadCtxt -- Head of an instance decl
829 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
830 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
831 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
832 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
833 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
834 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
838 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
839 checkValidTheta ctxt theta
840 = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
842 -------------------------
843 check_valid_theta ctxt []
845 check_valid_theta ctxt theta
846 = getDOptsTc `thenNF_Tc` \ dflags ->
847 warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
848 mapTc_ (check_source_ty dflags ctxt) theta
850 (_,dups) = removeDups tcCmpPred theta
852 -------------------------
853 check_source_ty dflags ctxt pred@(ClassP cls tys)
854 = -- Class predicates are valid in all contexts
855 mapTc_ check_arg_type tys `thenTc_`
856 checkTc (arity == n_tys) arity_err `thenTc_`
857 checkTc (all tyvar_head tys || arby_preds_ok) (predTyVarErr pred)
860 class_name = className cls
861 arity = classArity cls
863 arity_err = arityErr "Class" class_name arity n_tys
865 arby_preds_ok = case ctxt of
866 InstHeadCtxt -> True -- We check for instance-head formation
867 -- in checkValidInstHead
868 InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
869 other -> dopt Opt_GlasgowExts dflags
871 check_source_ty dflags SigmaCtxt (IParam name ty) = check_arg_type ty
872 -- Implicit parameters only allows in type
873 -- signatures; not in instance decls, superclasses etc
874 -- The reason for not allowing implicit params in instances is a bit subtle
875 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
876 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
877 -- discharge all the potential usas of the ?x in e. For example, a
878 -- constraint Foo [Int] might come out of e,and applying the
879 -- instance decl would show up two uses of ?x.
881 check_source_ty dflags TypeCtxt (NType tc tys) = mapTc_ check_arg_type tys
884 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
886 -------------------------
887 tyvar_head ty -- Haskell 98 allows predicates of form
888 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
889 | otherwise -- where a is a type variable
890 = case tcSplitAppTy_maybe ty of
891 Just (ty, _) -> tyvar_head ty
896 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
897 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
898 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
900 checkThetaCtxt ctxt theta
901 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
902 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
906 %************************************************************************
908 \subsection{Checking for a decent instance head type}
910 %************************************************************************
912 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
913 it must normally look like: @instance Foo (Tycon a b c ...) ...@
915 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
916 flag is on, or (2)~the instance is imported (they must have been
917 compiled elsewhere). In these cases, we let them go through anyway.
919 We can also have instances for functions: @instance Foo (a -> b) ...@.
922 checkValidInstHead :: Type -> TcM ()
924 checkValidInstHead ty -- Should be a source type
925 = case tcSplitPredTy_maybe ty of {
926 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
929 case getClassPredTys_maybe pred of {
930 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
933 getDOptsTc `thenNF_Tc` \ dflags ->
934 mapTc_ check_arg_type tys `thenTc_`
935 check_inst_head dflags clas tys
938 check_inst_head dflags clas tys
940 -- A user declaration of a CCallable/CReturnable instance
941 -- must be for a "boxed primitive" type.
942 (clas `hasKey` cCallableClassKey
943 && not (ccallable_type first_ty))
944 || (clas `hasKey` cReturnableClassKey
945 && not (creturnable_type first_ty))
946 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
948 -- If GlasgowExts then check at least one isn't a type variable
949 | dopt Opt_GlasgowExts dflags
950 = check_tyvars dflags clas tys
952 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
954 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
955 not (isSynTyCon tycon), -- ...but not a synonym
956 all tcIsTyVarTy arg_tys, -- Applied to type variables
957 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
958 -- This last condition checks that all the type variables are distinct
962 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
967 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
968 creturnable_type ty = isFFIImportResultTy dflags ty
970 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
971 text "where T is not a synonym, and a,b,c are distinct type variables")
973 check_tyvars dflags clas tys
974 -- Check that at least one isn't a type variable
975 -- unless -fallow-undecideable-instances
976 | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
977 | not (all tcIsTyVarTy tys) = returnTc ()
978 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
980 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
981 $$ ptext SLIT("Use -fallow-undecidable-instances to lift this restriction"))
985 instTypeErr pp_ty msg
986 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
989 nonBoxedPrimCCallErr clas inst_ty
990 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
991 4 (pprClassPred clas [inst_ty])
995 %************************************************************************
997 \subsection{Kind unification}
999 %************************************************************************
1002 unifyKind :: TcKind -- Expected
1006 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
1009 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
1010 unifyKinds [] [] = returnTc ()
1011 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
1013 unifyKinds _ _ = panic "unifyKinds: length mis-match"
1017 unifyOpenTypeKind :: TcKind -> TcM ()
1018 -- Ensures that the argument kind is of the form (Type bx)
1019 -- for some boxity bx
1021 unifyOpenTypeKind ty@(TyVarTy tyvar)
1022 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1024 Just ty' -> unifyOpenTypeKind ty'
1025 other -> unify_open_kind_help ty
1027 unifyOpenTypeKind ty
1028 | isTypeKind ty = returnTc ()
1029 | otherwise = unify_open_kind_help ty
1031 unify_open_kind_help ty -- Revert to ordinary unification
1032 = newBoxityVar `thenNF_Tc` \ boxity ->
1033 unifyKind ty (mkTyConApp typeCon [boxity])
1037 %************************************************************************
1039 \subsection[Unify-exported]{Exported unification functions}
1041 %************************************************************************
1043 The exported functions are all defined as versions of some
1044 non-exported generic functions.
1046 Unify two @TauType@s. Dead straightforward.
1049 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
1050 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
1051 = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
1052 uTys ty1 ty1 ty2 ty2
1055 @unifyTauTyList@ unifies corresponding elements of two lists of
1056 @TauType@s. It uses @uTys@ to do the real work. The lists should be
1057 of equal length. We charge down the list explicitly so that we can
1058 complain if their lengths differ.
1061 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
1062 unifyTauTyLists [] [] = returnTc ()
1063 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
1064 unifyTauTyLists tys1 tys2
1065 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
1068 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
1069 all together. It is used, for example, when typechecking explicit
1070 lists, when all the elts should be of the same type.
1073 unifyTauTyList :: [TcTauType] -> TcM ()
1074 unifyTauTyList [] = returnTc ()
1075 unifyTauTyList [ty] = returnTc ()
1076 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
1080 %************************************************************************
1082 \subsection[Unify-uTys]{@uTys@: getting down to business}
1084 %************************************************************************
1086 @uTys@ is the heart of the unifier. Each arg happens twice, because
1087 we want to report errors in terms of synomyms if poss. The first of
1088 the pair is used in error messages only; it is always the same as the
1089 second, except that if the first is a synonym then the second may be a
1090 de-synonym'd version. This way we get better error messages.
1092 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
1095 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
1096 -- ty1 is the *expected* type
1098 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
1099 -- ty2 is the *actual* type
1102 -- Always expand synonyms (see notes at end)
1103 -- (this also throws away FTVs)
1104 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
1105 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
1107 -- Ignore usage annotations inside typechecker
1108 uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
1109 uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
1111 -- Variables; go for uVar
1112 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
1113 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
1114 -- "True" means args swapped
1117 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
1118 | n1 == n2 = uTys t1 t1 t2 t2
1119 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
1120 | c1 == c2 = unifyTauTyLists tys1 tys2
1121 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
1122 | tc1 == tc2 = unifyTauTyLists tys1 tys2
1124 -- Functions; just check the two parts
1125 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
1126 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
1128 -- Type constructors must match
1129 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
1130 | con1 == con2 && equalLength tys1 tys2
1131 = unifyTauTyLists tys1 tys2
1133 | con1 == openKindCon
1134 -- When we are doing kind checking, we might match a kind '?'
1135 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
1136 -- (CCallable Int) and (CCallable Int#) are both OK
1137 = unifyOpenTypeKind ps_ty2
1139 -- Applications need a bit of care!
1140 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1141 -- NB: we've already dealt with type variables and Notes,
1142 -- so if one type is an App the other one jolly well better be too
1143 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
1144 = case tcSplitAppTy_maybe ty2 of
1145 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
1146 Nothing -> unifyMisMatch ps_ty1 ps_ty2
1148 -- Now the same, but the other way round
1149 -- Don't swap the types, because the error messages get worse
1150 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
1151 = case tcSplitAppTy_maybe ty1 of
1152 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
1153 Nothing -> unifyMisMatch ps_ty1 ps_ty2
1155 -- Not expecting for-alls in unification
1156 -- ... but the error message from the unifyMisMatch more informative
1157 -- than a panic message!
1159 -- Anything else fails
1160 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
1166 If you are tempted to make a short cut on synonyms, as in this
1170 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
1171 -- NO = if (con1 == con2) then
1172 -- NO -- Good news! Same synonym constructors, so we can shortcut
1173 -- NO -- by unifying their arguments and ignoring their expansions.
1174 -- NO unifyTauTypeLists args1 args2
1176 -- NO -- Never mind. Just expand them and try again
1180 then THINK AGAIN. Here is the whole story, as detected and reported
1181 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
1183 Here's a test program that should detect the problem:
1187 x = (1 :: Bogus Char) :: Bogus Bool
1190 The problem with [the attempted shortcut code] is that
1194 is not a sufficient condition to be able to use the shortcut!
1195 You also need to know that the type synonym actually USES all
1196 its arguments. For example, consider the following type synonym
1197 which does not use all its arguments.
1202 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
1203 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
1204 would fail, even though the expanded forms (both \tr{Int}) should
1207 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
1208 unnecessarily bind \tr{t} to \tr{Char}.
1210 ... You could explicitly test for the problem synonyms and mark them
1211 somehow as needing expansion, perhaps also issuing a warning to the
1216 %************************************************************************
1218 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
1220 %************************************************************************
1222 @uVar@ is called when at least one of the types being unified is a
1223 variable. It does {\em not} assume that the variable is a fixed point
1224 of the substitution; rather, notice that @uVar@ (defined below) nips
1225 back into @uTys@ if it turns out that the variable is already bound.
1228 uVar :: Bool -- False => tyvar is the "expected"
1229 -- True => ty is the "expected" thing
1231 -> TcTauType -> TcTauType -- printing and real versions
1234 uVar swapped tv1 ps_ty2 ty2
1235 = getTcTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
1237 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
1238 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
1239 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
1241 -- Expand synonyms; ignore FTVs
1242 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
1243 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
1246 -- The both-type-variable case
1247 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
1249 -- Same type variable => no-op
1253 -- Distinct type variables
1254 -- ASSERT maybe_ty1 /= Just
1256 = getTcTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
1258 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
1260 Nothing | update_tv2
1262 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
1263 putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
1267 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
1268 (putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
1273 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
1274 -- Try to get rid of open type variables as soon as poss
1276 nicer_to_update_tv2 = isUserTyVar (mutTyVarDetails tv1)
1277 -- Don't unify a signature type variable if poss
1278 || isSystemName (varName tv2)
1279 -- Try to update sys-y type variables in preference to sig-y ones
1281 -- Second one isn't a type variable
1282 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
1283 = -- Check that the kinds match
1284 checkKinds swapped tv1 non_var_ty2 `thenTc_`
1286 -- Check that tv1 isn't a type-signature type variable
1287 checkTcM (not (isSkolemTyVar (mutTyVarDetails tv1)))
1288 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
1290 -- Check that we aren't losing boxity info (shouldn't happen)
1291 warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
1292 ((ppr tv1 <+> ppr (tyVarKind tv1)) $$
1293 (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2))) `thenNF_Tc_`
1296 -- Basically we want to update tv1 := ps_ty2
1297 -- because ps_ty2 has type-synonym info, which improves later error messages
1302 -- f :: (A a -> a -> ()) -> ()
1306 -- x = f (\ x p -> p x)
1308 -- In the application (p x), we try to match "t" with "A t". If we go
1309 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
1310 -- an infinite loop later.
1311 -- But we should not reject the program, because A t = ().
1312 -- Rather, we should bind t to () (= non_var_ty2).
1314 -- That's why we have this two-state occurs-check
1315 zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
1316 if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
1317 putTcTyVar tv1 ps_ty2' `thenNF_Tc_`
1320 zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
1321 if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
1322 -- This branch rarely succeeds, except in strange cases
1323 -- like that in the example above
1324 putTcTyVar tv1 non_var_ty2' `thenNF_Tc_`
1327 failWithTcM (unifyOccurCheck tv1 ps_ty2')
1330 checkKinds swapped tv1 ty2
1331 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
1332 -- We need to check that we don't unify a lifted type variable with an
1333 -- unlifted type: e.g. (id 3#) is illegal
1334 | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
1335 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
1340 (k1,k2) | swapped = (tk2,tk1)
1341 | otherwise = (tk1,tk2)
1347 %************************************************************************
1349 \subsection[Unify-fun]{@unifyFunTy@}
1351 %************************************************************************
1353 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
1356 unifyFunTy :: TcType -- Fail if ty isn't a function type
1357 -> TcM (TcType, TcType) -- otherwise return arg and result types
1359 unifyFunTy ty@(TyVarTy tyvar)
1360 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1362 Just ty' -> unifyFunTy ty'
1363 other -> unify_fun_ty_help ty
1366 = case tcSplitFunTy_maybe ty of
1367 Just arg_and_res -> returnTc arg_and_res
1368 Nothing -> unify_fun_ty_help ty
1370 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
1371 = newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
1372 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
1373 unifyTauTy ty (mkFunTy arg res) `thenTc_`
1378 unifyListTy :: TcType -- expected list type
1379 -> TcM TcType -- list element type
1381 unifyListTy ty@(TyVarTy tyvar)
1382 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1384 Just ty' -> unifyListTy ty'
1385 other -> unify_list_ty_help ty
1388 = case tcSplitTyConApp_maybe ty of
1389 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
1390 other -> unify_list_ty_help ty
1392 unify_list_ty_help ty -- Revert to ordinary unification
1393 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
1394 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
1399 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
1400 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
1401 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1403 Just ty' -> unifyTupleTy boxity arity ty'
1404 other -> unify_tuple_ty_help boxity arity ty
1406 unifyTupleTy boxity arity ty
1407 = case tcSplitTyConApp_maybe ty of
1408 Just (tycon, arg_tys)
1409 | isTupleTyCon tycon
1410 && tyConArity tycon == arity
1411 && tupleTyConBoxity tycon == boxity
1413 other -> unify_tuple_ty_help boxity arity ty
1415 unify_tuple_ty_help boxity arity ty
1416 = newTyVarTys arity kind `thenNF_Tc` \ arg_tys ->
1417 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
1420 kind | isBoxed boxity = liftedTypeKind
1421 | otherwise = openTypeKind
1425 %************************************************************************
1427 \subsection[Unify-context]{Errors and contexts}
1429 %************************************************************************
1435 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
1436 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
1437 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
1438 returnNF_Tc (err ty1' ty2')
1440 err ty1 ty2 = (env1,
1443 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
1444 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
1447 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
1449 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
1450 -- tv1 is zonked already
1451 = zonkTcType ty2 `thenNF_Tc` \ ty2' ->
1452 returnNF_Tc (err ty2')
1454 err ty2 = (env2, ptext SLIT("When matching types") <+>
1455 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
1457 (pp_expected, pp_actual) | swapped = (pp2, pp1)
1458 | otherwise = (pp1, pp2)
1459 (env1, tv1') = tidyOpenTyVar tidy_env tv1
1460 (env2, ty2') = tidyOpenType env1 ty2
1464 unifyMisMatch ty1 ty2
1465 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
1466 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
1468 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
1469 msg = hang (ptext SLIT("Couldn't match"))
1470 4 (sep [quotes (ppr tidy_ty1),
1471 ptext SLIT("against"),
1472 quotes (ppr tidy_ty2)])
1474 failWithTcM (env, msg)
1476 unifyWithSigErr tyvar ty
1477 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
1478 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
1480 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1481 (env2, tidy_ty) = tidyOpenType env1 ty
1483 unifyOccurCheck tyvar ty
1484 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
1485 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1487 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1488 (env2, tidy_ty) = tidyOpenType env1 ty