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,
30 --------------------------------
32 unifyTauTy, unifyTauTyList, unifyTauTyLists,
33 unifyFunTy, unifyListTy, unifyTupleTy,
34 unifyKind, unifyKinds, unifyOpenTypeKind,
36 --------------------------------
38 zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
39 zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
40 zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
44 #include "HsVersions.h"
48 import TypeRep ( Type(..), SourceType(..), TyNote(..), -- Friend; can see representation
49 Kind, TauType, ThetaType,
52 import TcType ( tcEqType, tcCmpPred,
53 tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
54 tcSplitTyConApp_maybe, tcSplitFunTy_maybe, tcSplitForAllTys,
55 tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy, isUnLiftedType, isIPPred,
57 mkAppTy, mkTyVarTy, mkTyVarTys, mkFunTy, mkTyConApp,
60 liftedTypeKind, unliftedTypeKind, openTypeKind, defaultKind, superKind,
61 superBoxity, liftedBoxity, hasMoreBoxityInfo, typeKind,
62 tyVarsOfType, tyVarsOfTypes, tidyOpenType, tidyOpenTypes, tidyTyVar,
65 import Subst ( Subst, mkTopTyVarSubst, substTy )
66 import Class ( classArity, className )
67 import TyCon ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
68 isTupleTyCon, tyConArity, tupleTyConBoxity, tyConName )
69 import PrimRep ( PrimRep(VoidRep) )
70 import Var ( TyVar, varName, tyVarKind, tyVarName, isTyVar, mkTyVar,
71 isMutTyVar, isSigTyVar )
74 import TcMonad -- TcType, amongst others
75 import TysWiredIn ( voidTy, listTyCon, mkListTy, mkTupleTy )
76 import FunDeps ( grow )
77 import PprType ( pprPred, pprSourceType, pprTheta )
78 import Name ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
79 mkLocalName, mkDerivedTyConOcc, isSystemName
82 import BasicTypes ( Boxity, Arity, isBoxed )
83 import CmdLineOpts ( dopt, DynFlag(..) )
84 import Unique ( Uniquable(..) )
85 import SrcLoc ( noSrcLoc )
86 import Util ( nOfThem )
87 import ListSetOps ( removeDups )
92 %************************************************************************
94 \subsection{New type variables}
96 %************************************************************************
99 newTyVar :: Kind -> NF_TcM TcTyVar
101 = tcGetUnique `thenNF_Tc` \ uniq ->
102 tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
104 newTyVarTy :: Kind -> NF_TcM TcType
106 = newTyVar kind `thenNF_Tc` \ tc_tyvar ->
107 returnNF_Tc (TyVarTy tc_tyvar)
109 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
110 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
112 newKindVar :: NF_TcM TcKind
114 = tcGetUnique `thenNF_Tc` \ uniq ->
115 tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind `thenNF_Tc` \ kv ->
116 returnNF_Tc (TyVarTy kv)
118 newKindVars :: Int -> NF_TcM [TcKind]
119 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
121 newBoxityVar :: NF_TcM TcKind
123 = tcGetUnique `thenNF_Tc` \ uniq ->
124 tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity `thenNF_Tc` \ kv ->
125 returnNF_Tc (TyVarTy kv)
129 %************************************************************************
131 \subsection{Type instantiation}
133 %************************************************************************
135 I don't understand why this is needed
136 An old comments says "No need for tcSplitForAllTyM because a type
137 variable can't be instantiated to a for-all type"
138 But the same is true of rho types!
141 tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
145 -- A type variable is never instantiated to a dictionary type,
146 -- so we don't need to do a tcReadVar on the "arg".
147 go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
148 Just pair -> go res res (pair:ts)
149 Nothing -> returnNF_Tc (reverse ts, syn_t)
150 go syn_t (NoteTy n t) ts = go syn_t t ts
151 go syn_t (TyVarTy tv) ts = getTcTyVar tv `thenNF_Tc` \ maybe_ty ->
153 Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
154 other -> returnNF_Tc (reverse ts, syn_t)
155 go syn_t (UsageTy _ t) ts = go syn_t t ts
156 go syn_t t ts = returnNF_Tc (reverse ts, syn_t)
160 %************************************************************************
162 \subsection{Type instantiation}
164 %************************************************************************
166 Instantiating a bunch of type variables
169 tcInstTyVars :: [TyVar]
170 -> NF_TcM ([TcTyVar], [TcType], Subst)
173 = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
175 tys = mkTyVarTys tc_tyvars
177 returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
178 -- Since the tyvars are freshly made,
179 -- they cannot possibly be captured by
180 -- any existing for-alls. Hence mkTopTyVarSubst
183 = tcGetUnique `thenNF_Tc` \ uniq ->
185 name = setNameUnique (tyVarName tyvar) uniq
186 -- Note that we don't change the print-name
187 -- This won't confuse the type checker but there's a chance
188 -- that two different tyvars will print the same way
189 -- in an error message. -dppr-debug will show up the difference
190 -- Better watch out for this. If worst comes to worst, just
191 -- use mkSysLocalName.
193 tcNewMutTyVar name (tyVarKind tyvar)
195 tcInstSigVars tyvars -- Very similar to tcInstTyVar
196 = tcGetUniques `thenNF_Tc` \ uniqs ->
197 listTc [ ASSERT( not (kind `eqKind` openTypeKind) ) -- Shouldn't happen
198 tcNewSigTyVar name kind
199 | (tyvar, uniq) <- tyvars `zip` uniqs,
200 let name = setNameUnique (tyVarName tyvar) uniq,
201 let kind = tyVarKind tyvar
205 @tcInstType@ instantiates the outer-level for-alls of a TcType with
206 fresh type variables, splits off the dictionary part, and returns the results.
209 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
211 = case tcSplitForAllTys ty of
212 ([], rho) -> -- There may be overloading but no type variables;
213 -- (?x :: Int) => Int -> Int
215 (theta, tau) = tcSplitRhoTy rho -- Used to be tcSplitRhoTyM
217 returnNF_Tc ([], theta, tau)
219 (tyvars, rho) -> tcInstTyVars tyvars `thenNF_Tc` \ (tyvars', _, tenv) ->
221 (theta, tau) = tcSplitRhoTy (substTy tenv rho) -- Used to be tcSplitRhoTyM
223 returnNF_Tc (tyvars', theta, tau)
228 %************************************************************************
230 \subsection{Putting and getting mutable type variables}
232 %************************************************************************
235 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
236 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
243 | not (isMutTyVar tyvar)
244 = pprTrace "putTcTyVar" (ppr tyvar) $
248 = ASSERT( isMutTyVar tyvar )
249 UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
250 tcWriteMutTyVar tyvar (Just ty) `thenNF_Tc_`
254 Getting is more interesting. The easy thing to do is just to read, thus:
257 getTcTyVar tyvar = tcReadMutTyVar tyvar
260 But it's more fun to short out indirections on the way: If this
261 version returns a TyVar, then that TyVar is unbound. If it returns
262 any other type, then there might be bound TyVars embedded inside it.
264 We return Nothing iff the original box was unbound.
268 | not (isMutTyVar tyvar)
269 = pprTrace "getTcTyVar" (ppr tyvar) $
270 returnNF_Tc (Just (mkTyVarTy tyvar))
273 = ASSERT2( isMutTyVar tyvar, ppr tyvar )
274 tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
276 Just ty -> short_out ty `thenNF_Tc` \ ty' ->
277 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
278 returnNF_Tc (Just ty')
280 Nothing -> returnNF_Tc Nothing
282 short_out :: TcType -> NF_TcM TcType
283 short_out ty@(TyVarTy tyvar)
284 | not (isMutTyVar tyvar)
288 = tcReadMutTyVar tyvar `thenNF_Tc` \ maybe_ty ->
290 Just ty' -> short_out ty' `thenNF_Tc` \ ty' ->
291 tcWriteMutTyVar tyvar (Just ty') `thenNF_Tc_`
294 other -> returnNF_Tc ty
296 short_out other_ty = returnNF_Tc other_ty
300 %************************************************************************
302 \subsection{Zonking -- the exernal interfaces}
304 %************************************************************************
306 ----------------- Type variables
309 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
310 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
312 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
313 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars `thenNF_Tc` \ tys ->
314 returnNF_Tc (tyVarsOfTypes tys)
316 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
317 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
319 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
320 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
321 -- Usually this job is done by checkSigTyVars, but in a couple of places
322 -- that is overkill, so we use this simpler chap
323 zonkTcSigTyVars tyvars
324 = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
325 returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
328 ----------------- Types
331 zonkTcType :: TcType -> NF_TcM TcType
332 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
334 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
335 zonkTcTypes tys = mapNF_Tc zonkTcType tys
337 zonkTcClassConstraints cts = mapNF_Tc zonk cts
338 where zonk (clas, tys)
339 = zonkTcTypes tys `thenNF_Tc` \ new_tys ->
340 returnNF_Tc (clas, new_tys)
342 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
343 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
345 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
346 zonkTcPredType (ClassP c ts) =
347 zonkTcTypes ts `thenNF_Tc` \ new_ts ->
348 returnNF_Tc (ClassP c new_ts)
349 zonkTcPredType (IParam n t) =
350 zonkTcType t `thenNF_Tc` \ new_t ->
351 returnNF_Tc (IParam n new_t)
354 ------------------- These ...ToType, ...ToKind versions
355 are used at the end of type checking
358 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
360 = mapNF_Tc zonk_it pairs
362 zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
363 returnNF_Tc (name, kind)
365 -- When zonking a kind, we want to
366 -- zonk a *kind* variable to (Type *)
367 -- zonk a *boxity* variable to *
368 zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind = putTcTyVar kv liftedTypeKind
369 | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
370 | otherwise = pprPanic "zonkKindEnv" (ppr kv)
372 zonkTcTypeToType :: TcType -> NF_TcM Type
373 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
375 -- Zonk a mutable but unbound type variable to
376 -- Void if it has kind Lifted
378 -- We know it's unbound even though we don't carry an environment,
379 -- because at the binding site for a type variable we bind the
380 -- mutable tyvar to a fresh immutable one. So the mutable store
381 -- plays the role of an environment. If we come across a mutable
382 -- type variable that isn't so bound, it must be completely free.
383 zonk_unbound_tyvar tv
384 | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
385 = putTcTyVar tv voidTy -- Just to avoid creating a new tycon in
386 -- this vastly common case
388 = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
392 mk_void_tycon tv kind -- Make a new TyCon with the same kind as the
393 -- type variable tv. Same name too, apart from
394 -- making it start with a colon (sigh)
395 -- I dread to think what will happen if this gets out into an
396 -- interface file. Catastrophe likely. Major sigh.
397 = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
398 mkPrimTyCon tc_name kind 0 [] VoidRep
400 tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
402 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
403 -- of a type variable, at the *end* of type checking. It changes
404 -- the *mutable* type variable into an *immutable* one.
406 -- It does this by making an immutable version of tv and binds tv to it.
407 -- Now any bound occurences of the original type variable will get
408 -- zonked to the immutable version.
410 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
411 zonkTcTyVarToTyVar tv
413 -- Make an immutable version, defaulting
414 -- the kind to lifted if necessary
415 immut_tv = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
416 immut_tv_ty = mkTyVarTy immut_tv
418 zap tv = putTcTyVar tv immut_tv_ty
419 -- Bind the mutable version to the immutable one
421 -- If the type variable is mutable, then bind it to immut_tv_ty
422 -- so that all other occurrences of the tyvar will get zapped too
423 zonkTyVar zap tv `thenNF_Tc` \ ty2 ->
425 WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
431 %************************************************************************
433 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
435 %* For internal use only! *
437 %************************************************************************
440 -- zonkType is used for Kinds as well
442 -- For unbound, mutable tyvars, zonkType uses the function given to it
443 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
444 -- type variable and zonks the kind too
446 zonkType :: (TcTyVar -> NF_TcM Type) -- What to do with unbound mutable type variables
447 -- see zonkTcType, and zonkTcTypeToType
450 zonkType unbound_var_fn ty
453 go (TyConApp tycon tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
454 returnNF_Tc (TyConApp tycon tys')
456 go (NoteTy (SynNote ty1) ty2) = go ty1 `thenNF_Tc` \ ty1' ->
457 go ty2 `thenNF_Tc` \ ty2' ->
458 returnNF_Tc (NoteTy (SynNote ty1') ty2')
460 go (NoteTy (FTVNote _) ty2) = go ty2 -- Discard free-tyvar annotations
462 go (SourceTy p) = go_pred p `thenNF_Tc` \ p' ->
463 returnNF_Tc (SourceTy p')
465 go (FunTy arg res) = go arg `thenNF_Tc` \ arg' ->
466 go res `thenNF_Tc` \ res' ->
467 returnNF_Tc (FunTy arg' res')
469 go (AppTy fun arg) = go fun `thenNF_Tc` \ fun' ->
470 go arg `thenNF_Tc` \ arg' ->
471 returnNF_Tc (mkAppTy fun' arg')
473 go (UsageTy u ty) = go u `thenNF_Tc` \ u' ->
474 go ty `thenNF_Tc` \ ty' ->
475 returnNF_Tc (UsageTy u' ty')
477 -- The two interesting cases!
478 go (TyVarTy tyvar) = zonkTyVar unbound_var_fn tyvar
480 go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar `thenNF_Tc` \ tyvar' ->
481 go ty `thenNF_Tc` \ ty' ->
482 returnNF_Tc (ForAllTy tyvar' ty')
484 go_pred (ClassP c tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
485 returnNF_Tc (ClassP c tys')
486 go_pred (NType tc tys) = mapNF_Tc go tys `thenNF_Tc` \ tys' ->
487 returnNF_Tc (NType tc tys')
488 go_pred (IParam n ty) = go ty `thenNF_Tc` \ ty' ->
489 returnNF_Tc (IParam n ty')
491 zonkTyVar :: (TcTyVar -> NF_TcM Type) -- What to do for an unbound mutable variable
492 -> TcTyVar -> NF_TcM TcType
493 zonkTyVar unbound_var_fn tyvar
494 | not (isMutTyVar tyvar) -- Not a mutable tyvar. This can happen when
495 -- zonking a forall type, when the bound type variable
496 -- needn't be mutable
497 = ASSERT( isTyVar tyvar ) -- Should not be any immutable kind vars
498 returnNF_Tc (TyVarTy tyvar)
501 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
503 Nothing -> unbound_var_fn tyvar -- Mutable and unbound
504 Just other_ty -> zonkType unbound_var_fn other_ty -- Bound
509 %************************************************************************
511 \subsection{Checking a user type}
513 %************************************************************************
515 When dealing with a user-written type, we first translate it from an HsType
516 to a Type, performing kind checking, and then check various things that should
517 be true about it. We don't want to perform these checks at the same time
518 as the initial translation because (a) they are unnecessary for interface-file
519 types and (b) when checking a mutually recursive group of type and class decls,
520 we can't "look" at the tycons/classes yet.
522 One thing we check for is 'rank'.
524 Rank 0: monotypes (no foralls)
525 Rank 1: foralls at the front only, Rank 0 inside
526 Rank 2: foralls at the front, Rank 1 on left of fn arrow,
528 basic ::= tyvar | T basic ... basic
530 r2 ::= forall tvs. cxt => r2a
531 r2a ::= r1 -> r2a | basic
532 r1 ::= forall tvs. cxt => r0
533 r0 ::= r0 -> r0 | basic
538 = FunSigCtxt Name -- Function type signature
539 | ExprSigCtxt -- Expression type signature
540 | ConArgCtxt Name -- Data constructor argument
541 | TySynCtxt Name -- RHS of a type synonym decl
542 | GenPatCtxt -- Pattern in generic decl
543 -- f{| a+b |} (Inl x) = ...
544 | PatSigCtxt -- Type sig in pattern
546 | ResSigCtxt -- Result type sig
548 | ForSigCtxt Name -- Foreign inport or export signature
549 | RuleSigCtxt Name -- Signature on a forall'd variable in a RULE
551 pprUserTypeCtxt (FunSigCtxt n) = ptext SLIT("the type signature for") <+> quotes (ppr n)
552 pprUserTypeCtxt ExprSigCtxt = ptext SLIT("an expression type signature")
553 pprUserTypeCtxt (ConArgCtxt c) = ptext SLIT("the type of constructor") <+> quotes (ppr c)
554 pprUserTypeCtxt (TySynCtxt c) = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
555 pprUserTypeCtxt GenPatCtxt = ptext SLIT("the type pattern of a generic definition")
556 pprUserTypeCtxt PatSigCtxt = ptext SLIT("a pattern type signature")
557 pprUserTypeCtxt ResSigCtxt = ptext SLIT("a result type signature")
558 pprUserTypeCtxt (ForSigCtxt n) = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
559 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
563 checkValidType :: UserTypeCtxt -> Type -> TcM ()
564 -- Checks that the type is valid for the given context
565 checkValidType ctxt ty
566 = doptsTc Opt_GlasgowExts `thenNF_Tc` \ gla_exts ->
573 FunSigCtxt _ | gla_exts -> 2
575 ConArgCtxt _ | gla_exts -> 2 -- We are given the type of the entire
576 | otherwise -> 1 -- constructor; hence rank 1 is ok
577 TySynCtxt _ | gla_exts -> 1
582 actual_kind = typeKind ty
584 actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
586 kind_ok = case ctxt of
587 TySynCtxt _ -> True -- Any kind will do
588 GenPatCtxt -> actual_kind_is_lifted
589 ForSigCtxt _ -> actual_kind_is_lifted
590 other -> isTypeKind actual_kind
592 tcAddErrCtxt (checkTypeCtxt ctxt ty) $
594 -- Check that the thing has kind Type, and is lifted if necessary
595 checkTc kind_ok (kindErr actual_kind) `thenTc_`
597 -- Check the internal validity of the type itself
598 check_poly_type rank ty
600 -- Notes re TySynCtxt
601 -- We allow type synonyms that aren't types; e.g. type List = []
603 -- If the RHS mentions tyvars that aren't in scope, we'll
604 -- quantify over them:
605 -- e.g. type T = a->a
606 -- will become type T = forall a. a->a
608 -- With gla-exts that's right, but for H98 we should complain.
611 ----------------------------------------
613 check_poly_type :: Rank -> Type -> TcM ()
614 check_poly_type rank ty
616 = check_tau_type 0 False ty
617 | otherwise -- rank > 0
619 (tvs, theta, tau) = tcSplitSigmaTy ty
621 check_valid_theta SigmaCtxt theta `thenTc_`
622 check_tau_type (rank-1) False tau `thenTc_`
623 checkAmbiguity tvs theta tau
625 ----------------------------------------
626 check_arg_type :: Type -> TcM ()
627 -- The sort of type that can instantiate a type variable,
628 -- or be the argument of a type constructor.
629 -- Not an unboxed tuple, not a forall.
630 -- Other unboxed types are very occasionally allowed as type
631 -- arguments depending on the kind of the type constructor
633 -- For example, we want to reject things like:
635 -- instance Ord a => Ord (forall s. T s a)
637 -- g :: T s (forall b.b)
639 -- NB: unboxed tuples can have polymorphic or unboxed args.
640 -- This happens in the workers for functions returning
641 -- product types with polymorphic components.
642 -- But not in user code
644 -- Question: what about nested unboxed tuples?
645 -- Currently rejected.
647 = check_tau_type 0 False ty `thenTc_`
648 checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
650 ----------------------------------------
651 check_tau_type :: Rank -> Bool -> Type -> TcM ()
652 -- Rank is allowed rank for function args
653 -- No foralls otherwise
654 -- Bool is True iff unboxed tuple are allowed here
656 check_tau_type rank ubx_tup_ok ty@(UsageTy _ _) = addErrTc (usageTyErr ty)
657 check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = addErrTc (forAllTyErr ty)
658 check_tau_type rank ubx_tup_ok (SourceTy sty) = getDOptsTc `thenNF_Tc` \ dflags ->
659 check_source_ty dflags TypeCtxt sty
660 check_tau_type rank ubx_tup_ok (TyVarTy _) = returnTc ()
661 check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
662 = check_poly_type rank arg_ty `thenTc_`
663 check_tau_type rank True res_ty
665 check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
666 = check_arg_type ty1 `thenTc_` check_arg_type ty2
668 check_tau_type rank ubx_tup_ok (NoteTy note ty)
669 = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty
671 check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
673 = checkTc syn_arity_ok arity_msg `thenTc_`
674 mapTc_ check_arg_type tys
676 | isUnboxedTupleTyCon tc
677 = checkTc ubx_tup_ok ubx_tup_msg `thenTc_`
678 mapTc_ (check_tau_type 0 True) tys -- Args are allowed to be unlifted, or
679 -- more unboxed tuples, so can't use check_arg_ty
682 = mapTc_ check_arg_type tys
685 syn_arity_ok = tc_arity <= n_args
686 -- It's OK to have an *over-applied* type synonym
687 -- data Tree a b = ...
688 -- type Foo a = Tree [a]
689 -- f :: Foo a b -> ...
691 tc_arity = tyConArity tc
693 arity_msg = arityErr "Type synonym" (tyConName tc) tc_arity n_args
694 ubx_tup_msg = ubxArgTyErr ty
696 ----------------------------------------
697 check_note (FTVNote _) = returnTc ()
698 check_note (SynNote ty) = check_tau_type 0 False ty
704 = ClassSCCtxt Name -- Superclasses of clas
705 | SigmaCtxt -- Context of a normal for-all type
706 | DataTyCtxt Name -- Context of a data decl
707 | TypeCtxt -- Source type in an ordinary type
708 | InstDeclCtxt -- Context of an instance decl
710 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
711 pprSourceTyCtxt SigmaCtxt = ptext SLIT("the context of a polymorphic type")
712 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
713 pprSourceTyCtxt InstDeclCtxt = ptext SLIT("the context of an instance declaration")
714 pprSourceTyCtxt TypeCtxt = ptext SLIT("the context of a type")
718 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
719 checkValidTheta ctxt theta
720 = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
722 -------------------------
723 check_valid_theta ctxt []
725 check_valid_theta ctxt theta
726 = getDOptsTc `thenNF_Tc` \ dflags ->
727 warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
728 mapTc_ (check_source_ty dflags ctxt) theta
730 (_,dups) = removeDups tcCmpPred theta
732 -------------------------
733 check_source_ty dflags ctxt pred@(ClassP cls tys)
734 = -- Class predicates are valid in all contexts
735 mapTc_ check_arg_type tys `thenTc_`
736 checkTc (arity == n_tys) arity_err `thenTc_`
737 checkTc (all tyvar_head tys || arby_preds_ok) (predTyVarErr pred)
740 class_name = className cls
741 arity = classArity cls
743 arity_err = arityErr "Class" class_name arity n_tys
745 arby_preds_ok = case ctxt of
746 InstDeclCtxt -> dopt Opt_AllowUndecidableInstances dflags
747 other -> dopt Opt_GlasgowExts dflags
749 check_source_ty dflags SigmaCtxt (IParam name ty) = check_arg_type ty
750 check_source_ty dflags TypeCtxt (NType tc tys) = mapTc_ check_arg_type tys
753 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
755 -------------------------
756 tyvar_head ty -- Haskell 98 allows predicates of form
757 | tcIsTyVarTy ty = True -- C (a ty1 .. tyn)
758 | otherwise -- where a is a type variable
759 = case tcSplitAppTy_maybe ty of
760 Just (ty, _) -> tyvar_head ty
767 is ambiguous if P contains generic variables
768 (i.e. one of the Vs) that are not mentioned in tau
770 However, we need to take account of functional dependencies
771 when we speak of 'mentioned in tau'. Example:
772 class C a b | a -> b where ...
774 forall x y. (C x y) => x
775 is not ambiguous because x is mentioned and x determines y
777 NOTE: In addition, GHC insists that at least one type variable
778 in each constraint is in V. So we disallow a type like
779 forall a. Eq b => b -> b
780 even in a scope where b is in scope.
781 This is the is_free test below.
783 NB; the ambiguity check is only used for *user* types, not for types
784 coming from inteface files. The latter can legitimately have
785 ambiguous types. Example
787 class S a where s :: a -> (Int,Int)
788 instance S Char where s _ = (1,1)
789 f:: S a => [a] -> Int -> (Int,Int)
790 f (_::[a]) x = (a*x,b)
791 where (a,b) = s (undefined::a)
793 Here the worker for f gets the type
794 fw :: forall a. S a => Int -> (# Int, Int #)
796 If the list of tv_names is empty, we have a monotype, and then we
797 don't need to check for ambiguity either, because the test can't fail
801 checkAmbiguity :: [TyVar] -> ThetaType -> TauType -> TcM ()
802 checkAmbiguity forall_tyvars theta tau
803 = mapTc_ check_pred theta `thenTc_`
806 tau_vars = tyVarsOfType tau
807 extended_tau_vars = grow theta tau_vars
809 is_ambig ct_var = (ct_var `elem` forall_tyvars) &&
810 not (ct_var `elemVarSet` extended_tau_vars)
811 is_free ct_var = not (ct_var `elem` forall_tyvars)
813 check_pred pred = checkTc (not any_ambig) (ambigErr pred) `thenTc_`
814 checkTc (isIPPred pred || not all_free) (freeErr pred)
816 ct_vars = varSetElems (tyVarsOfPred pred)
817 all_free = all is_free ct_vars
818 any_ambig = any is_ambig ct_vars
824 = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
825 nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
826 ptext SLIT("must be reachable from the type after the =>"))]
829 = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
830 ptext SLIT("are already in scope"),
831 nest 4 (ptext SLIT("At least one must be universally quantified here"))
834 forAllTyErr ty = ptext SLIT("Illegal polymorphic type:") <+> ppr ty
835 usageTyErr ty = ptext SLIT("Illegal usage type:") <+> ppr ty
836 unliftedArgErr ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr ty
837 ubxArgTyErr ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
838 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
839 predTyVarErr pred = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
840 kindErr kind = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
841 dupPredWarn dups = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
843 checkTypeCtxt ctxt ty
844 = vcat [ptext SLIT("In the type:") <+> ppr_ty,
845 ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
847 -- Hack alert. If there are no tyvars, (ppr sigma_ty) will print
848 -- something strange like {Eq k} -> k -> k, because there is no
849 -- ForAll at the top of the type. Since this is going to the user
850 -- we want it to look like a proper Haskell type even then; hence the hack
852 -- This shows up in the complaint about
854 -- op :: Eq a => a -> a
855 ppr_ty | null forall_tyvars = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
857 (forall_tyvars, theta, tau) = tcSplitSigmaTy ty
859 checkThetaCtxt ctxt theta
860 = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
861 ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
865 %************************************************************************
867 \subsection{Kind unification}
869 %************************************************************************
872 unifyKind :: TcKind -- Expected
876 = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
879 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
880 unifyKinds [] [] = returnTc ()
881 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2 `thenTc_`
883 unifyKinds _ _ = panic "unifyKinds: length mis-match"
887 unifyOpenTypeKind :: TcKind -> TcM ()
888 -- Ensures that the argument kind is of the form (Type bx)
889 -- for some boxity bx
891 unifyOpenTypeKind ty@(TyVarTy tyvar)
892 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
894 Just ty' -> unifyOpenTypeKind ty'
895 other -> unify_open_kind_help ty
898 | isTypeKind ty = returnTc ()
899 | otherwise = unify_open_kind_help ty
901 unify_open_kind_help ty -- Revert to ordinary unification
902 = newBoxityVar `thenNF_Tc` \ boxity ->
903 unifyKind ty (mkTyConApp typeCon [boxity])
907 %************************************************************************
909 \subsection[Unify-exported]{Exported unification functions}
911 %************************************************************************
913 The exported functions are all defined as versions of some
914 non-exported generic functions.
916 Unify two @TauType@s. Dead straightforward.
919 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
920 unifyTauTy ty1 ty2 -- ty1 expected, ty2 inferred
921 = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
925 @unifyTauTyList@ unifies corresponding elements of two lists of
926 @TauType@s. It uses @uTys@ to do the real work. The lists should be
927 of equal length. We charge down the list explicitly so that we can
928 complain if their lengths differ.
931 unifyTauTyLists :: [TcTauType] -> [TcTauType] -> TcM ()
932 unifyTauTyLists [] [] = returnTc ()
933 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2 `thenTc_`
934 unifyTauTyLists tys1 tys2
935 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
938 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
939 all together. It is used, for example, when typechecking explicit
940 lists, when all the elts should be of the same type.
943 unifyTauTyList :: [TcTauType] -> TcM ()
944 unifyTauTyList [] = returnTc ()
945 unifyTauTyList [ty] = returnTc ()
946 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2 `thenTc_`
950 %************************************************************************
952 \subsection[Unify-uTys]{@uTys@: getting down to business}
954 %************************************************************************
956 @uTys@ is the heart of the unifier. Each arg happens twice, because
957 we want to report errors in terms of synomyms if poss. The first of
958 the pair is used in error messages only; it is always the same as the
959 second, except that if the first is a synonym then the second may be a
960 de-synonym'd version. This way we get better error messages.
962 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
965 uTys :: TcTauType -> TcTauType -- Error reporting ty1 and real ty1
966 -- ty1 is the *expected* type
968 -> TcTauType -> TcTauType -- Error reporting ty2 and real ty2
969 -- ty2 is the *actual* type
972 -- Always expand synonyms (see notes at end)
973 -- (this also throws away FTVs)
974 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
975 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
977 -- Ignore usage annotations inside typechecker
978 uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
979 uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
981 -- Variables; go for uVar
982 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
983 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True tyvar2 ps_ty1 ty1
984 -- "True" means args swapped
987 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
988 | n1 == n2 = uTys t1 t1 t2 t2
989 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
990 | c1 == c2 = unifyTauTyLists tys1 tys2
991 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
992 | tc1 == tc2 = unifyTauTyLists tys1 tys2
994 -- Functions; just check the two parts
995 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
996 = uTys fun1 fun1 fun2 fun2 `thenTc_` uTys arg1 arg1 arg2 arg2
998 -- Type constructors must match
999 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
1000 | con1 == con2 && length tys1 == length tys2
1001 = unifyTauTyLists tys1 tys2
1003 | con1 == openKindCon
1004 -- When we are doing kind checking, we might match a kind '?'
1005 -- against a kind '*' or '#'. Notably, CCallable :: ? -> *, and
1006 -- (CCallable Int) and (CCallable Int#) are both OK
1007 = unifyOpenTypeKind ps_ty2
1009 -- Applications need a bit of care!
1010 -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1011 -- NB: we've already dealt with type variables and Notes,
1012 -- so if one type is an App the other one jolly well better be too
1013 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
1014 = case tcSplitAppTy_maybe ty2 of
1015 Just (s2,t2) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
1016 Nothing -> unifyMisMatch ps_ty1 ps_ty2
1018 -- Now the same, but the other way round
1019 -- Don't swap the types, because the error messages get worse
1020 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
1021 = case tcSplitAppTy_maybe ty1 of
1022 Just (s1,t1) -> uTys s1 s1 s2 s2 `thenTc_` uTys t1 t1 t2 t2
1023 Nothing -> unifyMisMatch ps_ty1 ps_ty2
1025 -- Not expecting for-alls in unification
1026 -- ... but the error message from the unifyMisMatch more informative
1027 -- than a panic message!
1029 -- Anything else fails
1030 uTys ps_ty1 ty1 ps_ty2 ty2 = unifyMisMatch ps_ty1 ps_ty2
1036 If you are tempted to make a short cut on synonyms, as in this
1040 -- NO uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
1041 -- NO = if (con1 == con2) then
1042 -- NO -- Good news! Same synonym constructors, so we can shortcut
1043 -- NO -- by unifying their arguments and ignoring their expansions.
1044 -- NO unifyTauTypeLists args1 args2
1046 -- NO -- Never mind. Just expand them and try again
1050 then THINK AGAIN. Here is the whole story, as detected and reported
1051 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
1053 Here's a test program that should detect the problem:
1057 x = (1 :: Bogus Char) :: Bogus Bool
1060 The problem with [the attempted shortcut code] is that
1064 is not a sufficient condition to be able to use the shortcut!
1065 You also need to know that the type synonym actually USES all
1066 its arguments. For example, consider the following type synonym
1067 which does not use all its arguments.
1072 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
1073 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
1074 would fail, even though the expanded forms (both \tr{Int}) should
1077 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
1078 unnecessarily bind \tr{t} to \tr{Char}.
1080 ... You could explicitly test for the problem synonyms and mark them
1081 somehow as needing expansion, perhaps also issuing a warning to the
1086 %************************************************************************
1088 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
1090 %************************************************************************
1092 @uVar@ is called when at least one of the types being unified is a
1093 variable. It does {\em not} assume that the variable is a fixed point
1094 of the substitution; rather, notice that @uVar@ (defined below) nips
1095 back into @uTys@ if it turns out that the variable is already bound.
1098 uVar :: Bool -- False => tyvar is the "expected"
1099 -- True => ty is the "expected" thing
1101 -> TcTauType -> TcTauType -- printing and real versions
1104 uVar swapped tv1 ps_ty2 ty2
1105 = getTcTyVar tv1 `thenNF_Tc` \ maybe_ty1 ->
1107 Just ty1 | swapped -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
1108 | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
1109 other -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
1111 -- Expand synonyms; ignore FTVs
1112 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
1113 = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
1116 -- The both-type-variable case
1117 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
1119 -- Same type variable => no-op
1123 -- Distinct type variables
1124 -- ASSERT maybe_ty1 /= Just
1126 = getTcTyVar tv2 `thenNF_Tc` \ maybe_ty2 ->
1128 Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
1130 Nothing | update_tv2
1132 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
1133 putTcTyVar tv2 (TyVarTy tv1) `thenNF_Tc_`
1137 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
1138 (putTcTyVar tv1 ps_ty2 `thenNF_Tc_`
1143 update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
1144 -- Try to get rid of open type variables as soon as poss
1146 nicer_to_update_tv2 = isSigTyVar tv1
1147 -- Don't unify a signature type variable if poss
1148 || isSystemName (varName tv2)
1149 -- Try to update sys-y type variables in preference to sig-y ones
1151 -- Second one isn't a type variable
1152 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
1153 = -- Check that the kinds match
1154 checkKinds swapped tv1 non_var_ty2 `thenTc_`
1156 -- Check that tv1 isn't a type-signature type variable
1157 checkTcM (not (isSigTyVar tv1))
1158 (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
1160 -- Check that we aren't losing boxity info (shouldn't happen)
1161 warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
1162 ((ppr tv1 <+> ppr (tyVarKind tv1)) $$
1163 (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2))) `thenNF_Tc_`
1166 -- Basically we want to update tv1 := ps_ty2
1167 -- because ps_ty2 has type-synonym info, which improves later error messages
1172 -- f :: (A a -> a -> ()) -> ()
1176 -- x = f (\ x p -> p x)
1178 -- In the application (p x), we try to match "t" with "A t". If we go
1179 -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
1180 -- an infinite loop later.
1181 -- But we should not reject the program, because A t = ().
1182 -- Rather, we should bind t to () (= non_var_ty2).
1184 -- That's why we have this two-state occurs-check
1185 zonkTcType ps_ty2 `thenNF_Tc` \ ps_ty2' ->
1186 if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
1187 putTcTyVar tv1 ps_ty2' `thenNF_Tc_`
1190 zonkTcType non_var_ty2 `thenNF_Tc` \ non_var_ty2' ->
1191 if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
1192 -- This branch rarely succeeds, except in strange cases
1193 -- like that in the example above
1194 putTcTyVar tv1 non_var_ty2' `thenNF_Tc_`
1197 failWithTcM (unifyOccurCheck tv1 ps_ty2')
1200 checkKinds swapped tv1 ty2
1201 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
1202 -- We need to check that we don't unify a lifted type variable with an
1203 -- unlifted type: e.g. (id 3#) is illegal
1204 | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
1205 = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2) $
1210 (k1,k2) | swapped = (tk2,tk1)
1211 | otherwise = (tk1,tk2)
1217 %************************************************************************
1219 \subsection[Unify-fun]{@unifyFunTy@}
1221 %************************************************************************
1223 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
1226 unifyFunTy :: TcType -- Fail if ty isn't a function type
1227 -> TcM (TcType, TcType) -- otherwise return arg and result types
1229 unifyFunTy ty@(TyVarTy tyvar)
1230 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1232 Just ty' -> unifyFunTy ty'
1233 other -> unify_fun_ty_help ty
1236 = case tcSplitFunTy_maybe ty of
1237 Just arg_and_res -> returnTc arg_and_res
1238 Nothing -> unify_fun_ty_help ty
1240 unify_fun_ty_help ty -- Special cases failed, so revert to ordinary unification
1241 = newTyVarTy openTypeKind `thenNF_Tc` \ arg ->
1242 newTyVarTy openTypeKind `thenNF_Tc` \ res ->
1243 unifyTauTy ty (mkFunTy arg res) `thenTc_`
1248 unifyListTy :: TcType -- expected list type
1249 -> TcM TcType -- list element type
1251 unifyListTy ty@(TyVarTy tyvar)
1252 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1254 Just ty' -> unifyListTy ty'
1255 other -> unify_list_ty_help ty
1258 = case tcSplitTyConApp_maybe ty of
1259 Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
1260 other -> unify_list_ty_help ty
1262 unify_list_ty_help ty -- Revert to ordinary unification
1263 = newTyVarTy liftedTypeKind `thenNF_Tc` \ elt_ty ->
1264 unifyTauTy ty (mkListTy elt_ty) `thenTc_`
1269 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
1270 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
1271 = getTcTyVar tyvar `thenNF_Tc` \ maybe_ty ->
1273 Just ty' -> unifyTupleTy boxity arity ty'
1274 other -> unify_tuple_ty_help boxity arity ty
1276 unifyTupleTy boxity arity ty
1277 = case tcSplitTyConApp_maybe ty of
1278 Just (tycon, arg_tys)
1279 | isTupleTyCon tycon
1280 && tyConArity tycon == arity
1281 && tupleTyConBoxity tycon == boxity
1283 other -> unify_tuple_ty_help boxity arity ty
1285 unify_tuple_ty_help boxity arity ty
1286 = newTyVarTys arity kind `thenNF_Tc` \ arg_tys ->
1287 unifyTauTy ty (mkTupleTy boxity arity arg_tys) `thenTc_`
1290 kind | isBoxed boxity = liftedTypeKind
1291 | otherwise = openTypeKind
1295 %************************************************************************
1297 \subsection[Unify-context]{Errors and contexts}
1299 %************************************************************************
1305 unifyCtxt s ty1 ty2 tidy_env -- ty1 expected, ty2 inferred
1306 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
1307 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
1308 returnNF_Tc (err ty1' ty2')
1310 err ty1 ty2 = (env1,
1313 text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
1314 text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
1317 (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
1319 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
1320 -- tv1 is zonked already
1321 = zonkTcType ty2 `thenNF_Tc` \ ty2' ->
1322 returnNF_Tc (err ty2')
1324 err ty2 = (env2, ptext SLIT("When matching types") <+>
1325 sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
1327 (pp_expected, pp_actual) | swapped = (pp2, pp1)
1328 | otherwise = (pp1, pp2)
1329 (env1, tv1') = tidyTyVar tidy_env tv1
1330 (env2, ty2') = tidyOpenType env1 ty2
1334 unifyMisMatch ty1 ty2
1335 = zonkTcType ty1 `thenNF_Tc` \ ty1' ->
1336 zonkTcType ty2 `thenNF_Tc` \ ty2' ->
1338 (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
1339 msg = hang (ptext SLIT("Couldn't match"))
1340 4 (sep [quotes (ppr tidy_ty1),
1341 ptext SLIT("against"),
1342 quotes (ppr tidy_ty2)])
1344 failWithTcM (env, msg)
1346 unifyWithSigErr tyvar ty
1347 = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
1348 4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
1350 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
1351 (env2, tidy_ty) = tidyOpenType env1 ty
1353 unifyOccurCheck tyvar ty
1354 = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
1355 4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1357 (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
1358 (env2, tidy_ty) = tidyOpenType env1 ty