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, tidyOpenTyVar,
66 isFFIArgumentTy, isFFIImportResultTy
68 import Subst ( Subst, mkTopTyVarSubst, substTy )
69 import Class ( classArity, className )
70 import TyCon ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
71 isTupleTyCon, tyConArity, tupleTyConBoxity, tyConName )
72 import PrimRep ( PrimRep(VoidRep) )
73 import Var ( TyVar, varName, tyVarKind, tyVarName, isTyVar, mkTyVar,
74 isMutTyVar, isSigTyVar )
77 import TcMonad -- TcType, amongst others
78 import TysWiredIn ( voidTy, listTyCon, mkListTy, mkTupleTy )
79 import PrelNames ( cCallableClassKey, cReturnableClassKey, hasKey )
80 import ForeignCall ( Safety(..) )
81 import FunDeps ( grow )
82 import PprType ( pprPred, pprSourceType, pprTheta, pprClassPred )
83 import Name ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
84 mkLocalName, mkDerivedTyConOcc, isSystemName
87 import BasicTypes ( Boxity, Arity, isBoxed )
88 import CmdLineOpts ( dopt, DynFlag(..) )
89 import Unique ( Uniquable(..) )
90 import SrcLoc ( noSrcLoc )
91 import Util ( nOfThem, isSingleton, equalLength )
92 import ListSetOps ( removeDups )
97 %************************************************************************
99 \subsection{New type variables}
101 %************************************************************************
104 newTyVar :: Kind -> NF_TcM TcTyVar
106 = tcGetUnique `thenNF_Tc` \ uniq ->
107 tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
109 newTyVarTy :: Kind -> NF_TcM TcType
111 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
112 returnNF_Tc (TyVarTy tc_tyvar)
114 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
115 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
117 newKindVar :: NF_TcM TcKind
119 = tcGetUnique `thenNF_Tc` \ uniq ->
120 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv ->
121 returnNF_Tc (TyVarTy kv)
123 newKindVars :: Int -> NF_TcM [TcKind]
124 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
126 newBoxityVar :: NF_TcM TcKind
128 = tcGetUnique `thenNF_Tc` \ uniq ->
129 tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity `thenNF_Tc` \ kv ->
130 returnNF_Tc (TyVarTy kv)
134 %************************************************************************
136 \subsection{Type instantiation}
138 %************************************************************************
140 I don't understand why this is needed
141 An old comments says "No need for tcSplitForAllTyM because a type
142 variable can't be instantiated to a for-all type"
143 But the same is true of rho types!
146 tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
150 -- A type variable is never instantiated to a dictionary type,
151 -- so we don't need to do a tcReadVar on the "arg".
152 go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
153 Just pair -> go res res (pair:ts)
154 Nothing -> returnNF_Tc (reverse ts, syn_t)
155 go syn_t (NoteTy n t) ts = go syn_t t ts
156 go syn_t (TyVarTy tv) ts = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
158 Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
159 other -> returnNF_Tc (reverse ts, syn_t)
160 go syn_t (UsageTy _ t) ts = go syn_t t ts
161 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
165 %************************************************************************
167 \subsection{Type instantiation}
169 %************************************************************************
171 Instantiating a bunch of type variables
174 tcInstTyVars :: [TyVar]
175 -> NF_TcM ([TcTyVar], [TcType], Subst)
178 = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
180 tys = mkTyVarTys tc_tyvars
182 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
183 -- Since the tyvars are freshly made,
184 -- they cannot possibly be captured by
185 -- any existing for-alls. Hence mkTopTyVarSubst
188 = tcGetUnique `thenNF_Tc` \ uniq ->
190 name = setNameUnique (tyVarName tyvar) uniq
191 -- Note that we don't change the print-name
192 -- This won't confuse the type checker but there's a chance
193 -- that two different tyvars will print the same way
194 -- in an error message. -dppr-debug will show up the difference
195 -- Better watch out for this. If worst comes to worst, just
196 -- use mkSysLocalName.
198 tcNewMutTyVar name (tyVarKind tyvar)
200 tcInstSigVars tyvars -- Very similar to tcInstTyVar
201 = tcGetUniques `thenNF_Tc` \ uniqs ->
202 listTc [ ASSERT( not (kind `eqKind` openTypeKind) ) -- Shouldn't happen
203 tcNewSigTyVar name kind
204 | (tyvar, uniq) <- tyvars `zip` uniqs,
205 let name = setNameUnique (tyVarName tyvar) uniq,
206 let kind = tyVarKind tyvar
210 @tcInstType@ instantiates the outer-level for-alls of a TcType with
211 fresh type variables, splits off the dictionary part, and returns the results.
214 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
216 = case tcSplitForAllTys ty of
217 ([], rho) -> -- There may be overloading but no type variables;
218 -- (?x :: Int) => Int -> Int
220 (theta, tau) = tcSplitRhoTy rho -- Used to be tcSplitRhoTyM
222 returnNF_Tc ([], theta, tau)
224 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
226 (theta, tau) = tcSplitRhoTy (substTy tenv rho) -- Used to be tcSplitRhoTyM
228 returnNF_Tc (tyvars', theta, tau)
233 %************************************************************************
235 \subsection{Putting and getting mutable type variables}
237 %************************************************************************
240 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
241 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
248 | not (isMutTyVar tyvar)
249 = pprTrace "putTcTyVar" (ppr tyvar) $
253 = ASSERT( isMutTyVar tyvar )
254 UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
255 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
259 Getting is more interesting. The easy thing to do is just to read, thus:
262 getTcTyVar tyvar = tcReadMutTyVar tyvar
265 But it's more fun to short out indirections on the way: If this
266 version returns a TyVar, then that TyVar is unbound. If it returns
267 any other type, then there might be bound TyVars embedded inside it.
269 We return Nothing iff the original box was unbound.
273 | not (isMutTyVar tyvar)
274 = pprTrace "getTcTyVar" (ppr tyvar) $
275 returnNF_Tc (Just (mkTyVarTy tyvar))
278 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
279 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
281 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
282 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
283 returnNF_Tc (Just ty')
285 Nothing -> returnNF_Tc Nothing
287 short_out :: TcType -> NF_TcM TcType
288 short_out ty@(TyVarTy tyvar)
289 | not (isMutTyVar tyvar)
293 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
295 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
296 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
299 other -> returnNF_Tc ty
301 short_out other_ty = returnNF_Tc other_ty
305 %************************************************************************
307 \subsection{Zonking -- the exernal interfaces}
309 %************************************************************************
311 ----------------- Type variables
314 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
315 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
317 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
318 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
319 returnNF_Tc (tyVarsOfTypes tys)
321 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
322 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
324 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
325 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
326 -- Usually this job is done by checkSigTyVars, but in a couple of places
327 -- that is overkill, so we use this simpler chap
328 zonkTcSigTyVars tyvars
329 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
330 returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
333 ----------------- Types
336 zonkTcType :: TcType -> NF_TcM TcType
337 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
339 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
340 zonkTcTypes tys = mapNF_Tc zonkTcType tys
342 zonkTcClassConstraints cts = mapNF_Tc zonk cts
343 where zonk (clas, tys)
344 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
345 returnNF_Tc (clas, new_tys)
347 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
348 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
350 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
351 zonkTcPredType (ClassP c ts) =
352 zonkTcTypes ts `thenNF_Tc` \ new_ts ->
353 returnNF_Tc (ClassP c new_ts)
354 zonkTcPredType (IParam n t) =
355 zonkTcType t `thenNF_Tc` \ new_t ->
356 returnNF_Tc (IParam n new_t)
359 ------------------- These ...ToType, ...ToKind versions
360 are used at the end of type checking
363 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
365 = mapNF_Tc zonk_it pairs
367 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
368 returnNF_Tc (name, kind)
370 -- When zonking a kind, we want to
371 -- zonk a *kind* variable to (Type *)
372 -- zonk a *boxity* variable to *
373 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
374 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
375 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
377 zonkTcTypeToType :: TcType -> NF_TcM Type
378 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
380 -- Zonk a mutable but unbound type variable to
381 -- Void if it has kind Lifted
383 -- We know it's unbound even though we don't carry an environment,
384 -- because at the binding site for a type variable we bind the
385 -- mutable tyvar to a fresh immutable one. So the mutable store
386 -- plays the role of an environment. If we come across a mutable
387 -- type variable that isn't so bound, it must be completely free.
388 zonk_unbound_tyvar tv
389 | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
390 = putTcTyVar tv voidTy -- Just to avoid creating a new tycon in
391 -- this vastly common case
393 = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
397 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
398 -- type variable tv. Same name too, apart from
399 -- making it start with a colon (sigh)
400 -- I dread to think what will happen if this gets out into an
401 -- interface file. Catastrophe likely. Major sigh.
402 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
403 mkPrimTyCon tc_name kind 0 [] VoidRep
405 tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
407 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
408 -- of a type variable, at the *end* of type checking. It changes
409 -- the *mutable* type variable into an *immutable* one.
411 -- It does this by making an immutable version of tv and binds tv to it.
412 -- Now any bound occurences of the original type variable will get
413 -- zonked to the immutable version.
415 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
416 zonkTcTyVarToTyVar tv
418 -- Make an immutable version, defaulting
419 -- the kind to lifted if necessary
420 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
421 immut_tv_ty = mkTyVarTy immut_tv
423 zap tv = putTcTyVar tv immut_tv_ty
424 -- Bind the mutable version to the immutable one
426 -- If the type variable is mutable, then bind it to immut_tv_ty
427 -- so that all other occurrences of the tyvar will get zapped too
428 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
430 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
436 %************************************************************************
438 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
440 %* For internal use only! *
442 %************************************************************************
445 -- zonkType is used for Kinds as well
447 -- For unbound, mutable tyvars, zonkType uses the function given to it
448 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
449 -- type variable and zonks the kind too
451 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
452 -- see zonkTcType, and zonkTcTypeToType
455 zonkType unbound_var_fn ty
458 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
459 returnNF_Tc (TyConApp tycon tys')
461 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
462 go ty2 `thenNF_Tc` \ ty2' ->
463 returnNF_Tc (NoteTy (SynNote ty1') ty2')
465 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
467 go (SourceTy p) = go_pred p `thenNF_Tc` \ p' ->
468 returnNF_Tc (SourceTy p')
470 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
471 go res `thenNF_Tc` \ res' ->
472 returnNF_Tc (FunTy arg' res')
474 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
475 go arg `thenNF_Tc` \ arg' ->
476 returnNF_Tc (mkAppTy fun' arg')
478 go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
479 go ty `thenNF_Tc` \ ty' ->
480 returnNF_Tc (UsageTy u' ty')
482 -- The two interesting cases!
483 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
485 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
486 go ty `thenNF_Tc` \ ty' ->
487 returnNF_Tc (ForAllTy tyvar' ty')
489 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
490 returnNF_Tc (ClassP c tys')
491 go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
492 returnNF_Tc (NType tc tys')
493 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
494 returnNF_Tc (IParam n ty')
496 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
497 -> TcTyVar -> NF_TcM TcType
498 zonkTyVar unbound_var_fn tyvar
499 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
500 -- zonking a forall type, when the bound type variable
501 -- needn't be mutable
502 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
503 returnNF_Tc (TyVarTy tyvar)
506 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
508 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
509 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
514 %************************************************************************
516 \subsection{Checking a user type}
518 %************************************************************************
520 When dealing with a user-written type, we first translate it from an HsType
521 to a Type, performing kind checking, and then check various things that should
522 be true about it. We don't want to perform these checks at the same time
523 as the initial translation because (a) they are unnecessary for interface-file
524 types and (b) when checking a mutually recursive group of type and class decls,
525 we can't "look" at the tycons/classes yet. Also, the checks are are rather
526 diverse, and used to really mess up the other code.
528 One thing we check for is 'rank'.
530 Rank 0: monotypes (no foralls)
531 Rank 1: foralls at the front only, Rank 0 inside
532 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
534 basic ::= tyvar | T basic ... basic
536 r2 ::= forall tvs. cxt => r2a
537 r2a ::= r1 -> r2a | basic
538 r1 ::= forall tvs. cxt => r0
539 r0 ::= r0 -> r0 | basic
541 Another thing is to check that type synonyms are saturated.
542 This might not necessarily show up in kind checking.
544 data T k = MkT (k Int)
550 = FunSigCtxt Name -- Function type signature
551 | ExprSigCtxt -- Expression type signature
552 | ConArgCtxt Name -- Data constructor argument
553 | TySynCtxt Name -- RHS of a type synonym decl
554 | GenPatCtxt -- Pattern in generic decl
555 -- f{| a+b |} (Inl x) = ...
556 | PatSigCtxt -- Type sig in pattern
558 | ResSigCtxt -- Result type sig
560 | ForSigCtxt Name -- Foreign inport or export signature
561 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
563 -- Notes re TySynCtxt
564 -- We allow type synonyms that aren't types; e.g. type List = []
566 -- If the RHS mentions tyvars that aren't in scope, we'll
567 -- quantify over them:
568 -- e.g. type T = a->a
569 -- will become type T = forall a. a->a
571 -- With gla-exts that's right, but for H98 we should complain.
574 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
575 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
576 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
577 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
578 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
579 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
580 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
581 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
582 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
586 checkValidType :: UserTypeCtxt -> Type -> TcM ()
587 -- Checks that the type is valid for the given context
588 checkValidType ctxt ty
589 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
596 FunSigCtxt _ | gla_exts -> 2
598 ConArgCtxt _ | gla_exts -> 2 -- We are given the type of the entire
599 | otherwise -> 1 -- constructor; hence rank 1 is ok
600 TySynCtxt _ | gla_exts -> 1
605 actual_kind = typeKind ty
607 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
609 kind_ok = case ctxt of
610 TySynCtxt _ -> True -- Any kind will do
611 GenPatCtxt -> actual_kind_is_lifted
612 ForSigCtxt _ -> actual_kind_is_lifted
613 other -> isTypeKind actual_kind
615 tcAddErrCtxt (checkTypeCtxt ctxt ty) $
617 -- Check that the thing has kind Type, and is lifted if necessary
618 checkTc kind_ok (kindErr actual_kind) `thenTc_`
620 -- Check the internal validity of the type itself
621 check_poly_type rank ty
624 checkTypeCtxt ctxt ty
625 = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
626 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
628 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
629 -- something strange like {Eq k} -> k -> k, because there is no
630 -- ForAll at the top of the type. Since this is going to the user
631 -- we want it to look like a proper Haskell type even then; hence the hack
633 -- This shows up in the complaint about
635 -- op :: Eq a => a -> a
636 ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
639 (forall_tvs, theta, tau) = tcSplitSigmaTy ty
645 check_poly_type :: Rank -> Type -> TcM ()
646 check_poly_type rank ty
648 = check_tau_type 0 False ty
649 | otherwise -- rank > 0
651 (tvs, theta, tau) = tcSplitSigmaTy ty
653 check_valid_theta SigmaCtxt theta `thenTc_`
654 check_tau_type (rank-1) False tau `thenTc_`
655 checkAmbiguity tvs theta tau
657 ----------------------------------------
658 check_arg_type :: Type -> TcM ()
659 -- The sort of type that can instantiate a type variable,
660 -- or be the argument of a type constructor.
661 -- Not an unboxed tuple, not a forall.
662 -- Other unboxed types are very occasionally allowed as type
663 -- arguments depending on the kind of the type constructor
665 -- For example, we want to reject things like:
667 -- instance Ord a => Ord (forall s. T s a)
669 -- g :: T s (forall b.b)
671 -- NB: unboxed tuples can have polymorphic or unboxed args.
672 -- This happens in the workers for functions returning
673 -- product types with polymorphic components.
674 -- But not in user code
676 -- Question: what about nested unboxed tuples?
677 -- Currently rejected.
679 = check_tau_type 0 False ty `thenTc_`
680 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
682 ----------------------------------------
683 check_tau_type :: Rank -> Bool -> Type -> TcM ()
684 -- Rank is allowed rank for function args
685 -- No foralls otherwise
686 -- Bool is True iff unboxed tuple are allowed here
688 check_tau_type rank ubx_tup_ok ty@(UsageTy _ _) = failWithTc (usageTyErr ty)
689 check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
690 check_tau_type rank ubx_tup_ok (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
691 check_source_ty dflags TypeCtxt sty
692 check_tau_type rank ubx_tup_ok (TyVarTy _) = returnTc ()
693 check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
694 = check_poly_type rank arg_ty `thenTc_`
695 check_tau_type rank True res_ty
697 check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
698 = check_arg_type ty1 `thenTc_` check_arg_type ty2
700 check_tau_type rank ubx_tup_ok (NoteTy note ty)
701 = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty
703 check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
705 = checkTc syn_arity_ok arity_msg `thenTc_`
706 mapTc_ check_arg_type tys
708 | isUnboxedTupleTyCon tc
709 = checkTc ubx_tup_ok ubx_tup_msg `thenTc_`
710 mapTc_ (check_tau_type 0 True) tys -- Args are allowed to be unlifted, or
711 -- more unboxed tuples, so can't use check_arg_ty
714 = mapTc_ check_arg_type tys
717 syn_arity_ok = tc_arity <= n_args
718 -- It's OK to have an *over-applied* type synonym
719 -- data Tree a b = ...
720 -- type Foo a = Tree [a]
721 -- f :: Foo a b -> ...
723 tc_arity = tyConArity tc
725 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
726 ubx_tup_msg = ubxArgTyErr ty
728 ----------------------------------------
729 check_note (FTVNote _) = returnTc ()
730 check_note (SynNote ty) = check_tau_type 0 False ty
736 is ambiguous if P contains generic variables
737 (i.e. one of the Vs) that are not mentioned in tau
739 However, we need to take account of functional dependencies
740 when we speak of 'mentioned in tau'. Example:
741 class C a b | a -> b where ...
743 forall x y. (C x y) => x
744 is not ambiguous because x is mentioned and x determines y
746 NOTE: In addition, GHC insists that at least one type variable
747 in each constraint is in V. So we disallow a type like
748 forall a. Eq b => b -> b
749 even in a scope where b is in scope.
750 This is the is_free test below.
752 NB; the ambiguity check is only used for *user* types, not for types
753 coming from inteface files. The latter can legitimately have
754 ambiguous types. Example
756 class S a where s :: a -> (Int,Int)
757 instance S Char where s _ = (1,1)
758 f:: S a => [a] -> Int -> (Int,Int)
759 f (_::[a]) x = (a*x,b)
760 where (a,b) = s (undefined::a)
762 Here the worker for f gets the type
763 fw :: forall a. S a => Int -> (# Int, Int #)
765 If the list of tv_names is empty, we have a monotype, and then we
766 don't need to check for ambiguity either, because the test can't fail
770 checkAmbiguity :: [TyVar] -> ThetaType -> TauType -> TcM ()
771 checkAmbiguity forall_tyvars theta tau
772 = mapTc_ check_pred theta `thenTc_`
775 tau_vars = tyVarsOfType tau
776 extended_tau_vars = grow theta tau_vars
778 is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
779 not (ct_var `elemVarSet` extended_tau_vars)
780 is_free ct_var = not (ct_var `elem` forall_tyvars)
782 check_pred pred = checkTc (not any_ambig) (ambigErr pred) `thenTc_`
783 checkTc (isIPPred pred || not all_free) (freeErr pred)
785 ct_vars = varSetElems (tyVarsOfPred pred)
786 all_free = all is_free ct_vars
787 any_ambig = any is_ambig ct_vars
792 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
793 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
794 ptext SLIT("must be reachable from the type after the =>"))]
798 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
799 ptext SLIT("are already in scope"),
800 nest 4 (ptext SLIT("At least one must be universally quantified here"))
803 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
804 usageTyErr ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
805 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
806 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
807 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
810 %************************************************************************
812 \subsection{Checking a theta or source type}
814 %************************************************************************
818 = ClassSCCtxt Name -- Superclasses of clas
819 | SigmaCtxt -- Context of a normal for-all type
820 | DataTyCtxt Name -- Context of a data decl
821 | TypeCtxt -- Source type in an ordinary type
822 | InstThetaCtxt -- Context of an instance decl
823 | InstHeadCtxt -- Head of an instance decl
825 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
826 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
827 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
828 pprSourceTyCtxt InstThetaCtxt = ptext SLIT("the context of an instance declaration")
829 pprSourceTyCtxt InstHeadCtxt = ptext SLIT("the head of an instance declaration")
830 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
834 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
835 checkValidTheta ctxt theta
836 = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
838 -------------------------
839 check_valid_theta ctxt []
841 check_valid_theta ctxt theta
842 = getDOptsTc `thenNF_Tc` \ dflags ->
843 warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
844 mapTc_ (check_source_ty dflags ctxt) theta
846 (_,dups) = removeDups tcCmpPred theta
848 -------------------------
849 check_source_ty dflags ctxt pred@(ClassP cls tys)
850 = -- Class predicates are valid in all contexts
851 mapTc_ check_arg_type tys `thenTc_`
852 checkTc (arity == n_tys) arity_err `thenTc_`
853 checkTc (all tyvar_head tys || arby_preds_ok) (predTyVarErr pred)
856 class_name = className cls
857 arity = classArity cls
859 arity_err = arityErr "Class" class_name arity n_tys
861 arby_preds_ok = case ctxt of
862 InstHeadCtxt -> True -- We check for instance-head formation
863 -- in checkValidInstHead
864 InstThetaCtxt -> dopt Opt_AllowUndecidableInstances dflags
865 other -> dopt Opt_GlasgowExts dflags
867 check_source_ty dflags SigmaCtxt (IParam name ty) = check_arg_type ty
868 -- Implicit parameters only allows in type
869 -- signatures; not in instance decls, superclasses etc
870 -- The reason for not allowing implicit params in instances is a bit subtle
871 -- If we allowed instance (?x::Int, Eq a) => Foo [a] where ...
872 -- then when we saw (e :: (?x::Int) => t) it would be unclear how to
873 -- discharge all the potential usas of the ?x in e. For example, a
874 -- constraint Foo [Int] might come out of e,and applying the
875 -- instance decl would show up two uses of ?x.
877 check_source_ty dflags TypeCtxt (NType tc tys) = mapTc_ check_arg_type tys
880 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
882 -------------------------
883 tyvar_head ty -- Haskell 98 allows predicates of form
884 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
885 | otherwise -- where a is a type variable
886 = case tcSplitAppTy_maybe ty of
887 Just (ty, _) -> tyvar_head ty
892 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
893 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
894 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
896 checkThetaCtxt ctxt theta
897 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
898 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
902 %************************************************************************
904 \subsection{Checking for a decent instance head type}
906 %************************************************************************
908 @checkValidInstHead@ checks the type {\em and} its syntactic constraints:
909 it must normally look like: @instance Foo (Tycon a b c ...) ...@
911 The exceptions to this syntactic checking: (1)~if the @GlasgowExts@
912 flag is on, or (2)~the instance is imported (they must have been
913 compiled elsewhere). In these cases, we let them go through anyway.
915 We can also have instances for functions: @instance Foo (a -> b) ...@.
918 checkValidInstHead :: Type -> TcM ()
920 checkValidInstHead ty -- Should be a source type
921 = case tcSplitPredTy_maybe ty of {
922 Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
925 case getClassPredTys_maybe pred of {
926 Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
929 getDOptsTc `thenNF_Tc` \ dflags ->
930 mapTc_ check_arg_type tys `thenTc_`
931 check_inst_head dflags clas tys
934 check_inst_head dflags clas tys
936 -- A user declaration of a CCallable/CReturnable instance
937 -- must be for a "boxed primitive" type.
938 (clas `hasKey` cCallableClassKey
939 && not (ccallable_type first_ty))
940 || (clas `hasKey` cReturnableClassKey
941 && not (creturnable_type first_ty))
942 = failWithTc (nonBoxedPrimCCallErr clas first_ty)
944 -- If GlasgowExts then check at least one isn't a type variable
945 | dopt Opt_GlasgowExts dflags
946 = check_tyvars dflags clas tys
948 -- WITH HASKELL 1.4, MUST HAVE C (T a b c)
950 Just (tycon, arg_tys) <- tcSplitTyConApp_maybe first_ty,
951 not (isSynTyCon tycon), -- ...but not a synonym
952 all tcIsTyVarTy arg_tys, -- Applied to type variables
953 equalLength (varSetElems (tyVarsOfTypes arg_tys)) arg_tys
954 -- This last condition checks that all the type variables are distinct
958 = failWithTc (instTypeErr (pprClassPred clas tys) head_shape_msg)
963 ccallable_type ty = isFFIArgumentTy dflags PlayRisky ty
964 creturnable_type ty = isFFIImportResultTy dflags ty
966 head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
967 text "where T is not a synonym, and a,b,c are distinct type variables")
969 check_tyvars dflags clas tys
970 -- Check that at least one isn't a type variable
971 -- unless -fallow-undecideable-instances
972 | dopt Opt_AllowUndecidableInstances dflags = returnTc ()
973 | not (all tcIsTyVarTy tys) = returnTc ()
974 | otherwise = failWithTc (instTypeErr (pprClassPred clas tys) msg)
976 msg = parens (ptext SLIT("There must be at least one non-type-variable in the instance head")
977 $$ ptext SLIT("Use -fallow-undecidable-instances to lift this restriction"))
981 instTypeErr pp_ty msg
982 = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty,
985 nonBoxedPrimCCallErr clas inst_ty
986 = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
987 4 (pprClassPred clas [inst_ty])
991 %************************************************************************
993 \subsection{Kind unification}
995 %************************************************************************
998 unifyKind :: TcKind -- Expected
1002 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
1005 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
1006 unifyKinds [] [] = returnTc ()
1007 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
1009 unifyKinds _ _ = panic "unifyKinds: length mis-match"
1013 unifyOpenTypeKind :: TcKind -> TcM ()
1014 -- Ensures that the argument kind is of the form (Type bx)
1015 -- for some boxity bx
1017 unifyOpenTypeKind ty@(TyVarTy tyvar)
1018 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1020 Just ty' -> unifyOpenTypeKind ty'
1021 other -> unify_open_kind_help ty
1023 unifyOpenTypeKind ty
1024 | isTypeKind ty = returnTc ()
1025 | otherwise = unify_open_kind_help ty
1027 unify_open_kind_help ty -- Revert to ordinary unification
1028 = newBoxityVar `thenNF_Tc` \ boxity ->
1029 unifyKind ty (mkTyConApp typeCon [boxity])
1033 %************************************************************************
1035 \subsection[Unify-exported]{Exported unification functions}
1037 %************************************************************************
1039 The exported functions are all defined as versions of some
1040 non-exported generic functions.
1042 Unify two @TauType@s. Dead straightforward.
1045 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
1046 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
1047 = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
1048 uTys ty1 ty1 ty2 ty2
1051 @unifyTauTyList@ unifies corresponding elements of two lists of
1052 @TauType@s. It uses @uTys@ to do the real work. The lists should be
1053 of equal length. We charge down the list explicitly so that we can
1054 complain if their lengths differ.
1057 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
1058 unifyTauTyLists [] [] = returnTc ()
1059 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
1060 unifyTauTyLists tys1 tys2
1061 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
1064 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
1065 all together. It is used, for example, when typechecking explicit
1066 lists, when all the elts should be of the same type.
1069 unifyTauTyList :: [TcTauType] -> TcM ()
1070 unifyTauTyList [] = returnTc ()
1071 unifyTauTyList [ty] = returnTc ()
1072 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
1076 %************************************************************************
1078 \subsection[Unify-uTys]{@uTys@: getting down to business}
1080 %************************************************************************
1082 @uTys@ is the heart of the unifier. Each arg happens twice, because
1083 we want to report errors in terms of synomyms if poss. The first of
1084 the pair is used in error messages only; it is always the same as the
1085 second, except that if the first is a synonym then the second may be a
1086 de-synonym'd version. This way we get better error messages.
1088 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
1091 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
1092 -- ty1 is the *expected* type
1094 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
1095 -- ty2 is the *actual* type
1098 -- Always expand synonyms (see notes at end)
1099 -- (this also throws away FTVs)
1100 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
1101 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
1103 -- Ignore usage annotations inside typechecker
1104 uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
1105 uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
1107 -- Variables; go for uVar
1108 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
1109 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
1110 -- "True" means args swapped
1113 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
1114 | n1 == n2 = uTys t1 t1 t2 t2
1115 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
1116 | c1 == c2 = unifyTauTyLists tys1 tys2
1117 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
1118 | tc1 == tc2 = unifyTauTyLists tys1 tys2
1120 -- Functions; just check the two parts
1121 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
1122 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
1124 -- Type constructors must match
1125 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
1126 | con1 == con2 && equalLength tys1 tys2
1127 = unifyTauTyLists tys1 tys2
1129 | con1 == openKindCon
1130 -- When we are doing kind checking, we might match a kind '?'
1131 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
1132 -- (CCallable Int) and (CCallable Int#) are both OK
1133 = unifyOpenTypeKind ps_ty2
1135 -- Applications need a bit of care!
1136 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1137 -- NB: we've already dealt with type variables and Notes,
1138 -- so if one type is an App the other one jolly well better be too
1139 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
1140 = case tcSplitAppTy_maybe ty2 of
1141 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
1142 Nothing -> unifyMisMatch ps_ty1 ps_ty2
1144 -- Now the same, but the other way round
1145 -- Don't swap the types, because the error messages get worse
1146 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
1147 = case tcSplitAppTy_maybe ty1 of
1148 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
1149 Nothing -> unifyMisMatch ps_ty1 ps_ty2
1151 -- Not expecting for-alls in unification
1152 -- ... but the error message from the unifyMisMatch more informative
1153 -- than a panic message!
1155 -- Anything else fails
1156 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
1162 If you are tempted to make a short cut on synonyms, as in this
1166 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
1167 -- NO = if (con1 == con2) then
1168 -- NO -- Good news! Same synonym constructors, so we can shortcut
1169 -- NO -- by unifying their arguments and ignoring their expansions.
1170 -- NO unifyTauTypeLists args1 args2
1172 -- NO -- Never mind. Just expand them and try again
1176 then THINK AGAIN. Here is the whole story, as detected and reported
1177 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
1179 Here's a test program that should detect the problem:
1183 x = (1 :: Bogus Char) :: Bogus Bool
1186 The problem with [the attempted shortcut code] is that
1190 is not a sufficient condition to be able to use the shortcut!
1191 You also need to know that the type synonym actually USES all
1192 its arguments. For example, consider the following type synonym
1193 which does not use all its arguments.
1198 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
1199 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
1200 would fail, even though the expanded forms (both \tr{Int}) should
1203 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
1204 unnecessarily bind \tr{t} to \tr{Char}.
1206 ... You could explicitly test for the problem synonyms and mark them
1207 somehow as needing expansion, perhaps also issuing a warning to the
1212 %************************************************************************
1214 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
1216 %************************************************************************
1218 @uVar@ is called when at least one of the types being unified is a
1219 variable. It does {\em not} assume that the variable is a fixed point
1220 of the substitution; rather, notice that @uVar@ (defined below) nips
1221 back into @uTys@ if it turns out that the variable is already bound.
1224 uVar :: Bool -- False => tyvar is the "expected"
1225 -- True => ty is the "expected" thing
1227 -> TcTauType -> TcTauType -- printing and real versions
1230 uVar swapped tv1 ps_ty2 ty2
1231 = getTcTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
1233 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
1234 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
1235 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
1237 -- Expand synonyms; ignore FTVs
1238 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
1239 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
1242 -- The both-type-variable case
1243 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
1245 -- Same type variable => no-op
1249 -- Distinct type variables
1250 -- ASSERT maybe_ty1 /= Just
1252 = getTcTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
1254 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
1256 Nothing | update_tv2
1258 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
1259 putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
1263 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
1264 (putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
1269 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
1270 -- Try to get rid of open type variables as soon as poss
1272 nicer_to_update_tv2 = isSigTyVar tv1
1273 -- Don't unify a signature type variable if poss
1274 || isSystemName (varName tv2)
1275 -- Try to update sys-y type variables in preference to sig-y ones
1277 -- Second one isn't a type variable
1278 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
1279 = -- Check that the kinds match
1280 checkKinds swapped tv1 non_var_ty2 `thenTc_`
1282 -- Check that tv1 isn't a type-signature type variable
1283 checkTcM (not (isSigTyVar tv1))
1284 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
1286 -- Check that we aren't losing boxity info (shouldn't happen)
1287 warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
1288 ((ppr tv1 <+> ppr (tyVarKind tv1)) $$
1289 (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2))) `thenNF_Tc_`
1292 -- Basically we want to update tv1 := ps_ty2
1293 -- because ps_ty2 has type-synonym info, which improves later error messages
1298 -- f :: (A a -> a -> ()) -> ()
1302 -- x = f (\ x p -> p x)
1304 -- In the application (p x), we try to match "t" with "A t". If we go
1305 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
1306 -- an infinite loop later.
1307 -- But we should not reject the program, because A t = ().
1308 -- Rather, we should bind t to () (= non_var_ty2).
1310 -- That's why we have this two-state occurs-check
1311 zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
1312 if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
1313 putTcTyVar tv1 ps_ty2' `thenNF_Tc_`
1316 zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
1317 if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
1318 -- This branch rarely succeeds, except in strange cases
1319 -- like that in the example above
1320 putTcTyVar tv1 non_var_ty2' `thenNF_Tc_`
1323 failWithTcM (unifyOccurCheck tv1 ps_ty2')
1326 checkKinds swapped tv1 ty2
1327 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
1328 -- We need to check that we don't unify a lifted type variable with an
1329 -- unlifted type: e.g. (id 3#) is illegal
1330 | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
1331 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
1336 (k1,k2) | swapped = (tk2,tk1)
1337 | otherwise = (tk1,tk2)
1343 %************************************************************************
1345 \subsection[Unify-fun]{@unifyFunTy@}
1347 %************************************************************************
1349 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
1352 unifyFunTy :: TcType -- Fail if ty isn't a function type
1353 -> TcM (TcType, TcType) -- otherwise return arg and result types
1355 unifyFunTy ty@(TyVarTy tyvar)
1356 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1358 Just ty' -> unifyFunTy ty'
1359 other -> unify_fun_ty_help ty
1362 = case tcSplitFunTy_maybe ty of
1363 Just arg_and_res -> returnTc arg_and_res
1364 Nothing -> unify_fun_ty_help ty
1366 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
1367 = newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
1368 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
1369 unifyTauTy ty (mkFunTy arg res) `thenTc_`
1374 unifyListTy :: TcType -- expected list type
1375 -> TcM TcType -- list element type
1377 unifyListTy ty@(TyVarTy tyvar)
1378 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1380 Just ty' -> unifyListTy ty'
1381 other -> unify_list_ty_help ty
1384 = case tcSplitTyConApp_maybe ty of
1385 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
1386 other -> unify_list_ty_help ty
1388 unify_list_ty_help ty -- Revert to ordinary unification
1389 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
1390 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
1395 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
1396 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
1397 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1399 Just ty' -> unifyTupleTy boxity arity ty'
1400 other -> unify_tuple_ty_help boxity arity ty
1402 unifyTupleTy boxity arity ty
1403 = case tcSplitTyConApp_maybe ty of
1404 Just (tycon, arg_tys)
1405 | isTupleTyCon tycon
1406 && tyConArity tycon == arity
1407 && tupleTyConBoxity tycon == boxity
1409 other -> unify_tuple_ty_help boxity arity ty
1411 unify_tuple_ty_help boxity arity ty
1412 = newTyVarTys arity kind `thenNF_Tc` \ arg_tys ->
1413 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
1416 kind | isBoxed boxity = liftedTypeKind
1417 | otherwise = openTypeKind
1421 %************************************************************************
1423 \subsection[Unify-context]{Errors and contexts}
1425 %************************************************************************
1431 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
1432 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
1433 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
1434 returnNF_Tc (err ty1' ty2')
1436 err ty1 ty2 = (env1,
1439 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
1440 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
1443 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
1445 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
1446 -- tv1 is zonked already
1447 = zonkTcType ty2 `thenNF_Tc` \ ty2' ->
1448 returnNF_Tc (err ty2')
1450 err ty2 = (env2, ptext SLIT("When matching types") <+>
1451 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
1453 (pp_expected, pp_actual) | swapped = (pp2, pp1)
1454 | otherwise = (pp1, pp2)
1455 (env1, tv1') = tidyOpenTyVar tidy_env tv1
1456 (env2, ty2') = tidyOpenType env1 ty2
1460 unifyMisMatch ty1 ty2
1461 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
1462 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
1464 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
1465 msg = hang (ptext SLIT("Couldn't match"))
1466 4 (sep [quotes (ppr tidy_ty1),
1467 ptext SLIT("against"),
1468 quotes (ppr tidy_ty2)])
1470 failWithTcM (env, msg)
1472 unifyWithSigErr tyvar ty
1473 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
1474 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
1476 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1477 (env2, tidy_ty) = tidyOpenType env1 ty
1479 unifyOccurCheck tyvar ty
1480 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
1481 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1483 (env1, tidy_tyvar) = tidyOpenTyVar emptyTidyEnv tyvar
1484 (env2, tidy_ty) = tidyOpenType env1 ty